stanford-centaur / smt-switch Goto Github PK

Could include the solver in every term which would allow term construction without a separate solver object. But this could be expensive. Another option is to just have an interface for asking a term if it belongs to a solver. Depending on underlying solver, could depend on its API instead of using smt switch objects

Hi, @makaimann , @yoni206 , I'd like to report a vulnerability issue in smt-switch_0.3.0.

Dependency Graph between Python and Shared Libraries

Issue Description

As shown in the above dependency graph, smt-switch_0.3.0 directly or transitively depends on 6 C libraries (.so). However, I noticed that some C libraries are vulnerable, containing the following CVEs:
libgmp-afec2dd4.so.10.2.0 and libgmpxx-25f6cf8d.so.4.4.0from C project gmp(version:6.1.0) exposed 1 vulnerabilities:
CVE-2021-43618

Suggested Vulnerability Patch Versions

No official patch version released, but gmp has fixed the vulnerability in patch.

Python build tools cannot report vulnerable C libraries, which may induce potential security issues to many downstream Python projects.
As a popular python package (smt-switch has 790 downloads per month), could you please upgrade the above shared libraries to their patch versions?

Thanks for your help~
Best regards,
Andy

It seems like to_int assumes that the bitvector gets converted to a string of the form #bxxx, but for bitvectors of size 1 it is actually true or false (at least when using the bitwuzla solver). For example, the following code causes a crash in to_int:

SmtSolver solver = BitwuzlaSolverFactory::create(false);
solver->set_opt("produce-models", "true");
solver->set_opt("incremental", "true");

Sort sort = solver->make_sort(BV, 1);
Term x = solver->make_symbol("x", sort);
solver->check_sat();
uint64_t i = solver->get_value(x)->to_int();
std::cout << i << "\n";

I would instead expect to_int to return 0 or 1.

compare is defined recursively on a LoggingTerm because it needs to check that its operator is the same and all of it's children are the same. On large term DAGs this can easily blow up.

I'm parsing an smt file got from SyGuS and cvc5 above, and I would like to ask how I can obtain the smt::term formula shown in the red frame in the figure? (Just like the function behavior in PySMT --> TSSmtLibParser --> get_fs_fname) Thank you so much for your assistance!

Get arguments lazily

The unit-transfer test is failing due to this line:

For now, it is commented out.

Add a convenience function for running several solvers in a portfolio.

The CMake files for building the Boolector component assume that the dependencies for Boolector (Cadical and Btor2parser) are in the Boolector tree. This is not necessarily the case, e.g., if the dependencies were linked in from somewhere else, which the Boolector build scripts permit.

Some solvers require that assumptions to check-sat-assuming be propositional literals. This is based on the SMT-LIB documentation. However, in smt-lib you can use a define-fun rather than introducing a new constant. Thus it seems overly restrictive to require boolean literals in the API, rather than any boolean formula. Some solvers require boolean literals in the API, but we could consider hiding that from the user.

Add support for get-value/get-model/get-unsat-core to the SmtLibReader and flex/bison parse infrastructure.

Prior to the change in #210, the portfolio test would segfault somewhere in the logging solver for Yices2. Disabling logging fixed the test, so it could be a bug in the logging solver which is exposed by multi-threading.

Running substitute on a simple term, e.g. just updating a symbol (x -> y) can be much slower than caching. Although I would expect a cache look up to be faster, the massive difference in speed is surprising. See the review on stanford-centaur/pono#116. It might be out of our control if all the time is spent in the underlying solver, but it's worth looking into.

Hi,
I'm currently using the cvc5 solver, which distinguishes the boolean and bv1 sorts. So I would like to ask that is there a way to convert bv1 terms to boolean terms, and conversely, from boolean to bv1?

Thank you so much for your time!

When i import skbuild with python3 on my system I get the following printouts:

>>> import skbuild
Generating grammar tables from /usr/lib/python3.8/lib2to3/Grammar.txt
Generating grammar tables from /usr/lib/python3.8/lib2to3/PatternGrammar.txt

This causes issues in python/CMakeLists.txt since line 48 is not expecting this extra printout.

Locally, I have fixed this by replacing the import skbuild at line 39 of the script with import sys; temp = sys.stdout; sys.stdout = open(os.devnull,\"w\"); import skbuild; sys.stdout = temp to silence the output.

When fed the CVC5 term:
(let ((_let_1 (f y))) (let ((_let_2 (f x))) (and (<= 0 _let_2) (<= 0 _let_1) (<= (+ _let_2 _let_1) 1) (not (p 0)) (p _let_1))))

The TermTranslator (to any solver), rewrites it as:
(let ((_let_1 (f y))) (let ((_let_2 (f x))) (and (= (ite (<= 0 _let_2) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (<= 0 _let_1) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (<= (+ _let_2 _let_1) 1) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (not (p 0)) (_ bv1 1) (_ bv0 1)) (_ bv1 1)) (= (ite (p _let_1) (_ bv1 1) (_ bv0 1)) (_ bv1 1)))))

We would like the option to disable such a rewrite.

It appears this may be caused by two related bugs:

1. Because the AND has more than two children, execution goes into the if-statement linked below. We think we would like an option to manually disable this check and/or make smt-switch allow for ANDs to support more than two children. The translated term should have as similar a structure to the original term as possible.
   https://github.com/stanford-centaur/smt-switch/blob/f2d7d3d6dfccc0b4d6b604563acd34629bac884d/src/term_translator.cpp#L269C12-L269C12
2. It looks like cast_op and/or cast_term are being called twice upon themselves, leading to a Boolean-to-BV rewrite immediately followed by a BV-to-Boolean rewrite— which I do not think is the intended behavior, and we would also like to turn off.

In contrib/setup-cvc4.sh, cvc4 is configured using

CXXFLAGS=-fPIC CFLAGS=-fPIC ./configure.sh --static

but cvc4 does not build in mode --static on MacOS X.
This seems to work:

CXXFLAGS=-fPIC CFLAGS=-fPIC ./configure.sh --static --no-static-binary

This can be reproduced by changing https://github.com/makaimann/smt-switch/blob/3ba9442aef2def27faeb79185065ac1d481d26f7/tests/test-sorting-network.cpp#L104 to include generic solvers. Then configuring, building and running with:

./configure.sh --debug --cvc4
cd build
make
./tests/test-sorting-network

I am trying to include smtlib_reader.h header file in my project and when compiling, I get a compilation error that smtlibparser.h header file is missing. And indeed, I couldn't find it in the repo directory. What is the appropriate way to approach this? I have installed the needed dependencies for parser, "flex" and "bison". I ran the following command g++ -o my_program main.cpp -Ismt-switch/include -Lsmt-switch/build -lsmt-switch and got this error message:

SMT-Lib when reading LIRA / LRA formulas, the parser requires that reals have a "."
Many smt-lib formulas do not comply with this spec, would it be possible to enhance the parser so it can interpret integers as reals depending on context?

CVC4 does not install cleanly on MacOS X so ./contrib/setup-cvc4.sh fails.
The bug is in CVC4's contrib/get-antlr-3.4. It use realpath, but
there's no realpath on the Mac.

After fixing the previous problem, I got a compilation error for sort.cpp:

./src/sort.cpp:12:55: error: implicit instantiation of undefined template 'std::__1::array<std::__1::basic_string_view<char, std::__1::char_traits >, 6>'
constexpr std::array<std::string_view, NUM_SORT_CONS> generate_sortcon2str()

You need to add

include <array>

at the beginning of sort.cpp. That fixes the problem.

https://github.com/makaimann/smt-switch/blob/5aa3c6a9fdc6c9ed386a2261cf8d7613763a1772/include/solver.h#L65

Hi I have a question on the declaration of the get_value function. As I use smt::Term with some STL containers, I feel it is sometimes more convenient to have const smt::Term & there instead of smt::Term &.

I looked into the implementations of get_value for MathSat and Boolector, and it seems that you are not doing any alternation to that shared pointer (I mean making it point to somewhere else). So is there any other reason that it has to be a non-constant pointer?

To be clear, I'm not referring to having AbsTerm as constant (like std::shared_ptr<const AbsTerm> &). I'm talking about the pointer itself: const std::shared_ptr<AbsTerm> &

Thanks!

Hello. I am trying to use the make_term(). However, I find that there is some different when using this function. For example, when I use the ts_.make_term(And, prop, eq). Sometime program will synthesis the "bvand", and program will generate something like "ite" format to represent the equal value. However, when I trying to create a new solver, I found that I cannot get the same format, the program can only synthesis "and" and cannot synthesis "ite". I want to know why this will happen? Do I need to set other options to get the former format? The solver I am using is the Boolector.

Thank you very much!

Compilation fails with the following error:

/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp: In member function ‘cvc5::Op smt::Cvc5Solver::make_cvc5_op(smt::Op) const’:
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:986:24: error: ‘numeric_limits’ is not a member of ‘std’
  986 |     if (op.idx0 > std::numeric_limits<uint32_t>::max())
      |                        ^~~~~~~~~~~~~~
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:986:47: error: expected primary-expression before ‘>’ token
  986 |     if (op.idx0 > std::numeric_limits<uint32_t>::max())
      |                                               ^
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:986:50: error: ‘::max’ has not been declared; did you mean ‘std::max’?
  986 |     if (op.idx0 > std::numeric_limits<uint32_t>::max())
      |                                                  ^~~
      |                                                  std::max
In file included from /usr/include/c++/12.2.0/functional:64,
                 from /mnt/data/git/smt-switch/../cvc5/src/api/cpp/cvc5.h:21,
                 from /mnt/data/git/smt-switch/cvc5/include/cvc5_solver.h:26,
                 from /mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:17:
/usr/include/c++/12.2.0/bits/stl_algo.h:5756:5: note: ‘std::max’ declared here
 5756 |     max(initializer_list<_Tp> __l, _Compare __comp)
      |     ^~~
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:996:24: error: ‘numeric_limits’ is not a member of ‘std’
  996 |     if (op.idx0 > std::numeric_limits<uint32_t>::max())
      |                        ^~~~~~~~~~~~~~
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:996:47: error: expected primary-expression before ‘>’ token
  996 |     if (op.idx0 > std::numeric_limits<uint32_t>::max())
      |                                               ^
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:996:50: error: ‘::max’ has not been declared; did you mean ‘std::max’?
  996 |     if (op.idx0 > std::numeric_limits<uint32_t>::max())
      |                                                  ^~~
      |                                                  std::max
/usr/include/c++/12.2.0/bits/stl_algo.h:5756:5: note: ‘std::max’ declared here
 5756 |     max(initializer_list<_Tp> __l, _Compare __comp)
      |     ^~~
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:1001:24: error: ‘numeric_limits’ is not a member of ‘std’
 1001 |     if (op.idx1 > std::numeric_limits<uint32_t>::max())
      |                        ^~~~~~~~~~~~~~
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:1001:47: error: expected primary-expression before ‘>’ token
 1001 |     if (op.idx1 > std::numeric_limits<uint32_t>::max())
      |                                               ^
/mnt/data/git/smt-switch/cvc5/src/cvc5_solver.cpp:1001:50: error: ‘::max’ has not been declared; did you mean ‘std::max’?
 1001 |     if (op.idx1 > std::numeric_limits<uint32_t>::max())
      |                                                  ^~~
      |                                                  std::max
/usr/include/c++/12.2.0/bits/stl_algo.h:5756:5: note: ‘std::max’ declared here
 5756 |     max(initializer_list<_Tp> __l, _Compare __comp)
      |     ^~~

This is due to https://www.gnu.org/software/gcc/gcc-11/porting_to.html#header-dep-changes. The limits library needs to be included everywhere it is used.

This program throws an exception:

#include <iostream>

#include "smt-switch/yices2_factory.h"
#include "smt-switch/smt.h"

using namespace smt;
using namespace std;

int main(int argc, char * argv[])
{
  SmtSolver solver = Yices2SolverFactory::create(false);
  solver->set_opt("incremental", "true");
  Term f = solver->make_term(false);
  solver->assert_formula(f);
  solver->push();
  solver->pop();
  Sort boolsort = solver->make_sort(BOOL);
  return 0;
}

throws: InternalSolverException: the context state does not allow operation

compiled with: $(CXX) -g -std=c++11 -I./local/include -L./local/lib debug-yices2.cpp -o debug-yices2 -lsmt-switch-yices2 -lsmt-switch -lgmp

It appears that since the context is trivially unsatisfiable, it does not allow more operations. https://yices.csl.sri.com/doc/context-operations.html#assertions-and-satisfiability-checks

However, the yices_smt2 binary handles the SMT-LIB version of this fine, so there must be a work around.

(set-logic QF_BV)
(assert false)
(push 1)
(define-fun _78 () Bool true)
(exit)

Found by using ddSMT to reduce this benchmark.

I noticed while working on #248, that the scanner uses global state. I was getting strange behavior when running the parser twice. The fix in that PR was to flush the buffer with YY_FLUSH_BUFFER in scan_begin. Ideally, we would not have global state at all.

https://github.com/makaimann/smt-switch/blob/53ad7bd0a88c6e8cb6e8989540fc7899a668b6f2/src/utils.cpp#L209

Hi I'm wondering, if you directly return after sat, wouldn't you cause unbalanced push/pop issue?
Thanks!

The current implementation using threads results in waster resources because the threads running the solvers cannot be stopped at any time. See the discussion in #185. The portfolio solver should spawn child processes instead.

In the current version of z3 in use, a problem is encountered with "Overflow encountered when expanding vector" during solving, which can be seen: Z3Prover/z3#864

It seems fixed in new version of z3. However, when I changed to use the new version of z3 in smt-switch, I meet:

Undefined symbols for architecture arm64:
  "mk_implies(probe*, probe*)", referenced from:
      sexpr2probe(cmd_context&, sexpr*) in libsmt-switch-z3.a(tactic_cmds.o)
  "fatal_error(int)", referenced from:
      datalog::check_table::empty() const in libsmt-switch-z3.a(dl_check_table.o)
  "mk_size_probe()", referenced from:
      install_tactics(tactic_manager&) in libsmt-switch-z3.a(install_tactic.o)
  "mk_const_probe(double)", referenced from:
      sexpr2probe(cmd_context&, sexpr*) in libsmt-switch-z3.a(tactic_cmds.o)
      mk_auflia_tactic(ast_manager&, params_ref const&) in libsmt-switch-z3.a(quant_tactics.o)
      mk_qfbv_tactic(ast_manager&, params_ref const&) in libsmt-switch-z3.a(qfbv_tactic.o)
      mk_qfidl_tactic(ast_manager&, params_ref const&) in libsmt-switch-z3.a(qfidl_tactic.o)
      mk_qflia_tactic(ast_manager&, params_ref const&) in libsmt-switch-z3.a(qflia_tactic.o)
 .....

It seems that api does not match.

Most of the tests/unit tests are not even being run now, and need to be ported to googletest

See #255 for the discussion.

Saw unexpected behaviour once (using MathSAT).

Essentially, I would like to be able to parse an SMT problem and traverse the AST etc. Is this possible with this library? The documentation points to the /test dir which leads me to smtlib_reader.h. However, this only contains SmtLibReader which also requires a solver and it is also not entirely clear to me how to SmtLibReader to traverse the AST of an SMT lib parsed problem.

Currently, the subsitution function in boolector solver backend doesn't support the term-->term substitution as the Pysmt does. I would like to ask that if I want to use the term-to-term substitution, is there any potential method? And when will the boolector solver support this kind of subsititution? Thank you so much!

Instead of creating a bunch of different vectors and solver maps, use attributes for the testing infrastructure to decide when to run tests on different solvers.

Instead of implementing all four forms of make_sort and make_term just implement the vector one in solver backends (for simplicity). The top level solver can dispatch to them.

Here are a couple specific issues I encountered when trying to use a newer cvc5 (1.0.5+)

1:

• https://github.com/cvc5/cvc5/blob/1e01d2a9c0777b035987af2b302dd71df86e7e84/include/cvc5/cvc5_kind.h#L1965
• https://github.com/cvc5/cvc5/blob/1e01d2a9c0777b035987af2b302dd71df86e7e84/include/cvc5/cvc5_kind.h#L936

This causes is_value() to return sometimes erroneously return false, and cause crashes down the line.

2:
Several header paths (e.g. cvc5_sort.h, cvc5_kind.h, and api/cpp/..) have changed in newer versions of cvc5.

Ideally, multiple versions of each solver could be supported within one smt-switch build. Though they may not be able to be used simultaneously at runtime.

The new cmake infrastructure has a custom uninstall target which uses install_manifest.txt, but it does not clean up the added directory, e.g. /usr/local/include/smt-switch.

Retrieving sort parameters appears to be broken in CVC4 (getUninterpretedSortParamSorts returns an empty vector). This needs to be fixed first, and then we can merge: #98