Giter Site home page Giter Site logo

black-sat / black Goto Github PK

View Code? Open in Web Editor NEW
14.0 7.0 3.0 192.7 MB

BLACK (Bounded Lᴛʟ sAtisfiability ChecKer)

Home Page: https://www.black-sat.org

License: MIT License

CMake 5.96% C++ 83.45% Shell 5.67% Python 4.91%
logic temporal-logic formal-verification formal-methods linear-temporal-logic

black's Introduction

BLACK Build Status appveyor MIT Latest release codecov

BLACK (short for Bounded Lᴛʟ sAtisfiability ChecKer) is a tool for testing the satisfiability of formulas in Linear Temporal Logic and related logics.

BLACK is:

  • Fast: based on a state-of-the-art SAT-based encoding
  • Lightweight: low memory consuption even for large formulas
  • Flexible: supports LTL and LTL+Past, LTLf both on infinite and finite models, and LTLf Modulo Theories
  • Robust: rock-solid stability with almost 100% test coverage
  • Multiplatform: works on Linux, macOS, Windows and FreeBSD
  • Easy to use: easy to install binary packages provided for all major platforms
  • Embeddable: use BLACK's library API to integrate BLACK's solver into your code

How to use BLACK

See the Documentation site to learn how to use BLACK.

Downloads

See the Documentation page for further information on BLACK's installation.

Linux

Ubuntu ≥ 22.04 Fedora 36
Download Download
sudo apt install ⟨file⟩ sudo dnf install ⟨file⟩

macOS

Install via Homebrew:

$ brew install black-sat/black/black-sat

Windows

Download the self-contained ZIP archive.

Download

black's People

Contributors

gabventurato avatar lucageatti avatar nicola-gigante avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar

black's Issues

Trace syntax

Is there documentation on the syntax of traces (-t option)?

I suspect it's some JSON syntax but I could not find any documentation.

Thanks!

P.S. Compilation on Debian bookworm worked out of the box!

Exception thrown

Dear,

I run Black on the top of some experiments around LTL. In the process we've found the following bug in the experiment:

Blacks run many hours (4h) and throw the message: Killed.

My manual analysis shows a non-explaneable behaviour to request memory. Among them, the execution continuously increases the memory space.

However, Black often stabilizes the memory request. By the Black design, I consider that the pruning rules reduce the memory stored during the execution, and then I consider it as the potential root cause.

The input is:

((!r1) & (!r2) & (!g1) & (!g2) & (G(((F(!r1)) | (F(!g1))))) & (G(((F(!r2)) | (F(!g2))))) & (G(((X(!g1)) | (X(!g2))))) & (((g1) | (X(g2)) | (F(G(((r1) | (g2))))))) & (G(((F(((r1) & (g1)))) | (F(((!r1) & (!g1))))))) & (G(((F(((r2) & (g2)))) | (F(((!r2) & (!g2))))))) & (G(((((r1) & (X(r1)))) | (((!r1) & (X(!r1)))) | (((((r1) | (!g1))) & (((!r1) | (g1)))))))) & (G(((((r2) & (X(r2)))) | (((!r2) & (X(!r2)))) | (((((r2) | (!g2))) & (((!r2) | (g2)))))))) & (G(((((g1) & (X(g1)))) | (((!g1) & (X(!g1)))) | (((((r1) | (g1))) & (((!r1) | (!g1)))))))) & (G(((((g2) & (X(g2)))) | (((!g2) & (X(!g2)))) | (((((r2) | (g2))) & (((!r2) | (!g2)))))))))

I ran in the versions 0.92, 0.74, and 0.52.
My computer is a conventional desktop: Core i7, 16Gb of memory, and SSD.

If you need to have additional information (e.g., I have other inputs with the same behaviour). Let me know.

By the way, thank you for the new LTL solver.

Homebrew installation fails

Hi! It's me again. Was trying to install the latest version of BLACK via homebrew but it failed with the following error log:

Last 15 lines from /Users/yangjunhui/Library/Logs/Homebrew/black-sat/02.make:
    io::println("\n{}", clipp::make_man_page(cli, cli::command_name, fmt));
        ^
/tmp/black-sat-20220830-35034-cq591j/black-0.9.1/src/frontend/src/cli.cpp:194:7: note: in instantiation of function template specialization 'black::frontend::print_help<clipp::group>' requested here
      print_help(cli);
      ^
1 error generated.
make[2]: *** [src/frontend/CMakeFiles/frontend.dir/src/cli.cpp.o] Error 1
make[2]: *** Waiting for unfinished jobs....
make[1]: *** [src/frontend/CMakeFiles/frontend.dir/all] Error 2
make[1]: *** Waiting for unfinished jobs....
[ 96%] Linking CXX executable ../unit_tests
cd /tmp/black-sat-20220830-35034-cq591j/black-0.9.1/tests && /usr/local/Cellar/cmake/3.24.1/bin/cmake -E cmake_link_script CMakeFiles/unit_tests.dir/link.txt --verbose=1
/usr/local/opt/llvm/bin/clang++ -I/usr/local/opt/llvm/include -O3 -DNDEBUG -DBLACK_ASSERT_DISABLE -flto=thin -isysroot /Library/Developer/CommandLineTools/SDKs/MacOSX12.sdk -Wl,-search_paths_first -Wl,-headerpad_max_install_names -L/usr/local/opt/llvm/lib -Wl,-rpath,/usr/local/opt/llvm/lib CMakeFiles/unit_tests.dir/units/support.cpp.o CMakeFiles/unit_tests.dir/units/basics.cpp.o CMakeFiles/unit_tests.dir/units/match.cpp.o CMakeFiles/unit_tests.dir/units/namespaces.cpp.o CMakeFiles/unit_tests.dir/units/parser.cpp.o CMakeFiles/unit_tests.dir/units/past_remover.cpp.o CMakeFiles/unit_tests.dir/units/solver.cpp.o CMakeFiles/unit_tests.dir/units/sat.cpp.o CMakeFiles/unit_tests.dir/units/cnf.cpp.o -o ../unit_tests  -Wl,-rpath,/tmp/black-sat-20220830-35034-cq591j/black-0.9.1/src/lib ../src/lib/libblack.dylib /usr/local/lib/libCatch2Main.a /usr/local/lib/libCatch2.a
[ 96%] Built target unit_tests
make: *** [all] Error 2

Thanks in advance for your help!

Compile problem with GCC 9.1.1

When I try to compile with GCC 9.1.1 I get the following error:

$ make
[  9%] Built target remotery
[ 13%] Building CXX object external/fmt/CMakeFiles/fmt.dir/src/format.cc.o
In file included from /home/gabriele/programs/BLACK/external/fmt/include/fmt/format-inl.h:11,
                 from /home/gabriele/programs/BLACK/external/fmt/src/format.cc:8:
/home/gabriele/programs/BLACK/external/fmt/include/fmt/format.h:3620:55: error: ISO C++ did not adopt string literal operator templates taking an argument pack of characters [-Wpedantic]
 3620 | FMT_CONSTEXPR internal::udl_formatter<Char, CHARS...> operator""_format() {
      |                                                       ^~~~~~~~
make[2]: *** [external/fmt/CMakeFiles/fmt.dir/build.make:63: external/fmt/CMakeFiles/fmt.dir/src/format.cc.o] Error 1
make[1]: *** [CMakeFiles/Makefile2:164: external/fmt/CMakeFiles/fmt.dir/all] Error 2
make: *** [Makefile:141: all] Error 2

should the black compilation require sudo for making install?

On last step:

  1. Build, test (optional), and install the tool, I got the following message.

make install
[ 20%] Built target glucose
[ 70%] Built target black
[ 83%] Built target frontend
[ 91%] Built target random_formulas_generator
[100%] Built target crscounter_generator
Install the project...
-- Install configuration: "Release"
-- Installing: /usr/local/lib/libblack.so
CMake Error at src/lib/cmake_install.cmake:47 (file):
file INSTALL cannot copy file
"/home/gab/Documentos/t-crowd/black/build/src/lib/libblack.so" to
"/usr/local/lib/libblack.so".
Call Stack (most recent call first):
cmake_install.cmake:42 (include)

make: *** [Makefile:74: install] Error 1

Hang Loop

Hi.

For this formula, the memory behavior is unpredictable, as usually.

However, It runs for more than 24 hours in my conventional desktop (Core i7, 16Gb of memory, and SSD), and the execution does not end.

The formula is:

((!r1) & (!r2) & (!g1) & (!g2) & (G(((F(!r1)) | (F(!g1))))) & (G(((F(!r2)) | (F(!g2))))) & (G(((X(!g1)) | (X(!g2))))) & (((g1) | (X(g2)) | (F(G(((r1) | (g2))))))) & (G(((F(((r1) & (g1)))) | (F(((!r1) & (!g1))))))) & (G(((F(((r2) & (g2)))) | (F(((!r2) & (!g2))))))) & (G(((((r1) & (X(r1)))) | (((!r1) & (X(!r1)))) | (((((r1) | (!g1))) & (((!r1) | (g1)))))))) & (G(((((r2) & (X(r2)))) | (((!r2) & (X(!r2)))) | (((((r2) | (!g2))) & (((!r2) | (g2)))))))) & (G(((((g1) & (X(g1)))) | (((!g1) & (X(!g1)))) | (((((r1) | (g1))) & (((!r1) | (!g1)))))))) & (G(((((g2) & (X(g2)))) | (((!g2) & (X(!g2)))) | (((((r2) | (g2))) & (((!g2) | (((!r2) & (g2)))))))))))

I checked with other solvers (NuSMV and PLTL) and the answer is UNSAT. However, I also do not have an estimation of the model.

Thank you for your attention.

Code coverage report tracking

This issue tracks the improvement of the code coverage reports through codecov.io

Current status: codecov

The issue will be closed with a coverage percentage greater than 95%.

Work in this direction is made on the fix/coverage branch, and periodically merged in master

Random formula generator ignores `--dim` option when `--seed` is setted

Hi,

I noticed that --seed option creates deterministic formula but ignores the option --dim.

> random_formulas_generator --seed 1024 --dim 1024
F((((Z (p3) W (!!((p4) | H (p3)) | (p4))) M (F wX wX (p2) S ((p2) S (p2)))) U O((G X True -> (p4)) M ((p5) R Z Y Y((F True M Y H((p5) R Z (p3))) S X !(p4))))) T ((F G((p5) | (p1)) -> ((p5) U H X((p2) <-> wX X !((p3) T (p6))))) M (p1)))

> random_formulas_generator --seed 1024 --dim 102
F((((Z (p3) W (!!((p4) | H (p3)) | (p4))) M (F wX wX (p2) S ((p2) S (p2)))) U O((G X True -> (p4)) M ((p5) R Z Y Y((F True M Y H((p5) R Z (p3))) S X !(p4))))) T ((F G((p5) | (p1)) -> ((p5) U H X((p2) <-> wX X !((p3) T (p6))))) M (p1)))

Failed assert with randomly-generated formula

The attached files make black crash with a failed assertion.
formulas.zip

$ black random.pltl
[black]: failed assert at /Users/gigabytes/Projects/BLACK/src/frontend/src/main.cpp:81, "f.has_value()"
[1]    38315 abort      ./black

Thanks to Germán Braun for reporting.

Support cgroups v2 in run benchmarks script

At the moment the script /benchmarks/run uses cgroups v1 to limit the memory usage during benchmarks. However it would be nice to enable cgroups v2 support too.

Motivation

https://www.redhat.com/sysadmin/fedora-31-control-group-v2
https://www.redhat.com/en/blog/world-domination-cgroups-rhel-8-welcome-cgroups-v2
https://www.kernel.org/doc/html/latest/admin-guide/cgroup-v2.html

Workarounds

If not interested in limiting resources:

  • If libcgroup is not installed the memory limit is not set.
  • Thanks to #32 can be executed export MCAP=false before running the script to manually disable cgroup usage.

If interested in limiting resources

  • Force the use of cgroups v1, e.g. explained here.
  • To actually use cgroups v2 can be used a wrapper command, for example exploiting systemd in this way:
    systemd-run --user --scope -p MemoryHigh=60% -p MemoryMax=70% <actual-command>
    more details on parameters can be found here. Note that the MemoryHigh parameter make the system trying to keep the process under control. If one wants to put an hard limit on the memory usage, it should be used systemd-run --user --scope -p MemorySwapMax=0 -p MemoryMax=4G <actual-command>. The MemorySwapMax it's necessary to prevent the system to start swapping when the limit is reached.

Input syntax documentation could be useful

It could be useful to have a description of the input accepted by BLACK, e.g., all the operators allowed with their priority.

For example, a formula of the type: A /\ B -> C is parsed as A /\ (B -> C) and not as (A /\ B) -> C. So it's not obvious what one should expect without a detailed description of the operators precedence.

Compilation error with GCC 10.1.1 in Fedora 32

I have troubles in compiling with the new GCC 10.1.1 in Fedora 32.

Here you can find the compilation error I get:

Scanning dependencies of target fmt
[  5%] Building CXX object external/fmt/CMakeFiles/fmt.dir/src/format.cc.o
[ 11%] Building CXX object external/fmt/CMakeFiles/fmt.dir/src/posix.cc.o
[ 17%] Linking CXX static library libfmt.a
[ 17%] Built target fmt
Scanning dependencies of target black
[ 23%] Building CXX object src/lib/CMakeFiles/black.dir/src/logic/lex.cpp.o
In file included from /home/gabriele/programs/black/src/lib/include/black/logic/lex.hpp:27,
                 from /home/gabriele/programs/black/src/lib/src/logic/lex.cpp:18:
/home/gabriele/programs/black/src/lib/include/black/logic/formula.hpp:35:8: error: elaborated-type-specifier for a scoped enum must not use the ‘class’ keyword [-Werror]
   35 |   enum class formula_type : uint8_t {
      |   ~~~~ ^~~~~
      |        -----
/home/gabriele/programs/black/src/lib/include/black/logic/formula.hpp:35:27: error: found ‘:’ in nested-name-specifier, expected ‘::’
   35 |   enum class formula_type : uint8_t {
      |                           ^
      |                           ::
/home/gabriele/programs/black/src/lib/include/black/logic/formula.hpp:35:14: error: ‘formula_type’ has not been declared
   35 |   enum class formula_type : uint8_t {
      |              ^~~~~~~~~~~~
/home/gabriele/programs/black/src/lib/include/black/logic/formula.hpp:35:37: error: expected unqualified-id before ‘{’ token
   35 |   enum class formula_type : uint8_t {
      |                                     ^
In file included from /home/gabriele/programs/black/src/lib/include/black/logic/formula.hpp:58,
                 from /home/gabriele/programs/black/src/lib/include/black/logic/lex.hpp:27,
                 from /home/gabriele/programs/black/src/lib/src/logic/lex.cpp:18:
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:49:34: error: ‘formula_type’ was not declared in this scope
   49 |   constexpr bool is_boolean_type(formula_type type) {
      |                                  ^~~~~~~~~~~~
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:53:31: error: ‘formula_type’ was not declared in this scope
   53 |   constexpr bool is_atom_type(formula_type type) {
      |                               ^~~~~~~~~~~~
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:57:32: error: ‘formula_type’ was not declared in this scope
   57 |   constexpr bool is_unary_type(formula_type type) {
      |                                ^~~~~~~~~~~~
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:62:33: error: ‘formula_type’ was not declared in this scope
   62 |   constexpr bool is_binary_type(formula_type type) {
      |                                 ^~~~~~~~~~~~
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:69:30: error: expected ‘)’ before ‘t’
   69 |     formula_base(formula_type t);
      |                 ~            ^~
      |                              )
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:72:11: error: ‘formula_type’ does not name a type; did you mean ‘formula_base’?
   72 |     const formula_type type{};
      |           ^~~~~~~~~~~~
      |           formula_base
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:72:30: error: extra ‘;’ [-Werror=pedantic]
   72 |     const formula_type type{};
      |                              ^
      |                              -
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp: In constructor ‘black::internal::boolean_t::boolean_t(bool)’:
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:80:22: error: ‘formula_type’ has not been declared
   80 |       : formula_base{formula_type::boolean}, value(v) {}
      |                      ^~~~~~~~~~~~
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp: In constructor ‘black::internal::atom_t::atom_t(const black::internal::any_hashable&)’:
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:90:22: error: ‘formula_type’ has not been declared
   90 |       : formula_base{formula_type::atom}, label{_label} {}
      |                      ^~~~~~~~~~~~
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp: At global scope:
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:99:25: error: expected ‘)’ before ‘t’
   99 |     unary_t(formula_type t, formula_base *f)
      |            ~            ^~
      |                         )
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:100:24: error: expected unqualified-id before ‘,’ token
  100 |       : formula_base{t}, operand{f}
      |                        ^
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:101:5: error: expected unqualified-id before ‘{’ token
  101 |     {
      |     ^
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:113:26: error: expected ‘)’ before ‘t’
  113 |     binary_t(formula_type t, formula_base*f1, formula_base*f2)
      |             ~            ^~
      |                          )
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:114:24: error: expected unqualified-id before ‘,’ token
  114 |       : formula_base{t}, left{f1}, right{f2}
      |                        ^
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:114:34: error: expected unqualified-id before ‘,’ token
  114 |       : formula_base{t}, left{f1}, right{f2}
      |                                  ^
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:115:5: error: expected unqualified-id before ‘{’ token
  115 |     {
      |     ^
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp: In function ‘F* black::internal::formula_cast(black::internal::formula_base*)’:
/home/gabriele/programs/black/src/lib/include/black/internal/formula/base.hpp:129:27: error: ‘struct black::internal::formula_base’ has no member named ‘type’
  129 |     if(F::accepts_type(f->type))
      |                           ^~~~
In file included from /home/gabriele/programs/black/src/lib/include/black/logic/lex.hpp:27,
                 from /home/gabriele/programs/black/src/lib/src/logic/lex.cpp:18:
/home/gabriele/programs/black/src/lib/include/black/logic/formula.hpp: At global scope:
/home/gabriele/programs/black/src/lib/include/black/logic/formula.hpp:89:35: error: ‘formula_type’ in namespace ‘black::internal’ does not name a type; did you mean ‘formula_base’?
   89 |     using type = black::internal::formula_type;
      |                                   ^~~~~~~~~~~~
      |                                   formula_base
/home/gabriele/programs/black/src/lib/include/black/logic/formula.hpp:92:5: error: ‘type’ does not name a type
   92 |     type formula_type() const;
      |     ^~~~
/home/gabriele/programs/black/src/lib/include/black/logic/formula.hpp:182:45: error: ‘black::internal::formula::type’ has not been declared
  182 |       negation     = to_underlying(formula::type::negation),
      |                                             ^~~~
/home/gabriele/programs/black/src/lib/include/black/logic/formula.hpp:214:44: error: ‘black::internal::formula::type’ has not been declared
  214 |       conjunction = to_underlying(formula::type::conjunction),
      |                                            ^~~~
In file included from /home/gabriele/programs/black/src/lib/include/black/logic/formula.hpp:316,
                 from /home/gabriele/programs/black/src/lib/include/black/logic/lex.hpp:27,
                 from /home/gabriele/programs/black/src/lib/src/logic/lex.cpp:18:
/home/gabriele/programs/black/src/lib/include/black/internal/formula/impl.hpp:39:10: error: ISO C++ forbids declaration of ‘formula_base’ with no type [-fpermissive]
   39 |   inline formula_base::formula_base(formula_type t) : type{t} { }
      |          ^~~~~~~~~~~~
/home/gabriele/programs/black/src/lib/include/black/internal/formula/impl.hpp:39:10: error: ‘int black::internal::formula_base::formula_base’ is not a static data member of ‘struct black::internal::formula_base’
/home/gabriele/programs/black/src/lib/include/black/internal/formula/impl.hpp:39:37: error: ‘formula_type’ was not declared in this scope; did you mean ‘formula_base’?
   39 |   inline formula_base::formula_base(formula_type t) : type{t} { }
      |                                     ^~~~~~~~~~~~
      |                                     formula_base
/home/gabriele/programs/black/src/lib/include/black/internal/formula/impl.hpp:39:63: error: expected unqualified-id before ‘{’ token
   39 |   inline formula_base::formula_base(formula_type t) : type{t} { }
      |                                                               ^
/home/gabriele/programs/black/src/lib/include/black/internal/formula/impl.hpp:52:19: error: ‘type’ in ‘class black::internal::formula’ does not name a type
   52 |   inline formula::type formula::formula_type() const {
      |                   ^~~~
/home/gabriele/programs/black/src/lib/include/black/internal/formula/impl.hpp: In member function ‘black::internal::unary::type black::internal::unary::formula_type() const’:
/home/gabriele/programs/black/src/lib/include/black/internal/formula/impl.hpp:157:47: error: ‘struct black::internal::unary_t’ has no member named ‘type’
  157 |     return static_cast<unary::type>(_formula->type);
      |                                               ^~~~
/home/gabriele/programs/black/src/lib/include/black/internal/formula/impl.hpp: In member function ‘black::internal::binary::type black::internal::binary::formula_type() const’:
/home/gabriele/programs/black/src/lib/include/black/internal/formula/impl.hpp:170:48: error: ‘struct black::internal::binary_t’ has no member named ‘type’
  170 |     return static_cast<binary::type>(_formula->type);
      |                                                ^~~~
/home/gabriele/programs/black/src/lib/include/black/internal/formula/impl.hpp: In static member function ‘static std::optional<_Tp> black::internal::operator_base<H, F, OT>::cast(black::alphabet*, black::internal::formula_base*)’:
/home/gabriele/programs/black/src/lib/include/black/internal/formula/impl.hpp:197:43: error: ‘formula_type’ does not name a type; did you mean ‘formula_base’?
  197 |       if( ptr && ptr->type == static_cast<formula_type>(OT))
      |                                           ^~~~~~~~~~~~
      |                                           formula_base
cc1plus: all warnings being treated as errors
make[2]: *** [src/lib/CMakeFiles/black.dir/build.make:83: src/lib/CMakeFiles/black.dir/src/logic/lex.cpp.o] Error 1
make[1]: *** [CMakeFiles/Makefile2:282: src/lib/CMakeFiles/black.dir/all] Error 2
make: *** [Makefile:161: all] Error 2

Compilation steps are not working propertly

  1. Create a build directory and cd into it:

$ mkdir build

  1. Run cmake, pointing it to the build directory

$ cmake -S . -B build

the execution of step 4 gives the following Cmake error

CMake Error: The source directory "/home/gab/Documentos/t-crowd/black/build" does not appear to contain CMakeLists.txt.
Specify --help for usage, or press the help button on the CMake GUI

I guess that you should use

cmake -S ../ -B .

if you previously did cd into build. according to cmake help

cmake [options] -S <path-to-source> -B <path-to-build>

Issues compiling BLACK on MacOS Catalina 10.15

/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:314:9: error: no member named 'signbit' in the global namespace
using ::signbit;
~~^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:315:9: error: no member named 'fpclassify' in the global namespace
using ::fpclassify;
~~^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:316:9: error: no member named 'isfinite' in the global namespace; did
you mean 'finite'?
using ::isfinite;
~~^

Mixed namespaces for variables, propositions, functions and relations

BLACK's input syntax is currently not consistent with regards to whether variables, propositions, functions and relations share the same namespace or not.

The following is not accepted because r is used twice with different meanings:

$ black solve -s -d integers -f 'r(x) & r(x) = 0'
black: syntax error: <stdin>: Function symbol 'r' already used as a relation symbol

This would suggest that different kinds of symbols cannot reuse the same names, to avoid confusion, but the following are accepted:

$ black solve -s -d integers -f 'x & x = 0'      
SAT
$ black solve -s -d integers -f 'x & x(y)' 
SAT

BLACK syntax should either allow to use the same name for different kinds of entities or not. The latter is preferred.

Fresh installation error on Z3

I tried a new fresh installation but I got this error:

-- Could NOT find PkgConfig (missing: PKG_CONFIG_EXECUTABLE) 
CMake Error at /usr/share/cmake-3.13/Modules/FindPackageHandleStandardArgs.cmake:137 (message):
  Could NOT find Z3 (missing: Z3_LIBRARY Z3_INCLUDE_DIR)
Call Stack (most recent call first):
  /usr/share/cmake-3.13/Modules/FindPackageHandleStandardArgs.cmake:378 (_FPHSA_FAILURE_MESSAGE)
  cmake/FindZ3.cmake:44 (find_package_handle_standard_args)
  src/lib/CMakeLists.txt:30 (find_package)

however, i understand that Z3 is an optional dependency

Inconsistent sat-solvers backends

With the trivially satisfiable formula (False | G True) & (F False | True) the default Glucose backend and CryptoMiniSAT say that it is UNSAT. The other backends (MathSAT and Z3) say correctly that it is SAT.

Can be found attached here the output of the encoding produced by BLACK for Glucose and MathSAT, in which can be seen that Glucose fails at recognizing the k_unraveling & (k_empty | k_loop) formula as SAT.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.