diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml new file mode 100644 index 000000000..0833a0837 --- /dev/null +++ b/.github/workflows/coverage.yml @@ -0,0 +1,90 @@ +name: Code Coverage + +on: + push: + branches: [ master ] + schedule: + - cron: "0 11 * * *" + +env: + BUILD_TYPE: Debug + CMAKE_GENERATOR: Ninja + +jobs: + build: + runs-on: ubuntu-latest + + env: + CC: clang + CXX: clang++ + + steps: + - uses: actions/checkout@v2 + + - name: Setup + run: | + sudo apt-get remove -y --purge man-db + sudo apt-get update -y + sudo apt-get install -y gcovr ninja-build + + ## Building + - name: Configure CMake Z3 + run: CFLAGS=="--coverage" CXXFLAGS="--coverage" LDFLAGS="-lgcov" cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -DCMAKE_INSTALL_PREFIX=./install + + - name: Build Z3 + # Build your program with the given configuration + run: cmake --build ${{github.workspace}}/build --target install --config ${{env.BUILD_TYPE}} + + - name: Build test-z3 + run: cmake --build ${{github.workspace}}/build --target test-z3 --config ${{env.BUILD_TYPE}} + + - name: Build examples + run: | + cmake --build ${{github.workspace}}/build --target c_example + cmake --build ${{github.workspace}}/build --target cpp_example + cmake --build ${{github.workspace}}/build --target z3_tptp5 + cmake --build ${{github.workspace}}/build --target c_maxsat_example + + - name: Clone z3test + run: git clone https://github.com/z3prover/z3test z3test + + ## Testing + - name: Run test-z3 + run: | + cd ${{github.workspace}}/build + ./test-z3 -a + cd - + + - name: Run examples + run: | + ${{github.workspace}}/build/examples/c_example_build_dir/c_example + ${{github.workspace}}/build/examples/cpp_example_build_dir/cpp_example + ${{github.workspace}}/build/examples/tptp_build_dir/z3_tptp5 --help + ${{github.workspace}}/build/examples/c_maxsat_example_build_dir/c_maxsat_example ${{github.workspace}}/examples/maxsat/ex.smt + + - name: Run regressions + run: | + python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2 + python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2-debug + python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2-extra + + - name: Run coverage tests + run: python z3test/scripts/test_coverage_tests.py ./install z3test/coverage/cpp + + ## Artifact + - name: Gather coverage + run: | + cd ${{github.workspace}} + gcovr + #gcovr --html -o coverage.html . + cd - + + - name: Get date + id: date + run: echo "::set-output name=date::$(date +'%Y-%m-%d')" + + - uses: actions/upload-artifact@v2 + with: + name: coverage-${{steps.date.outputs.date}} + path: coverage.html + retention-days: 10 diff --git a/.github/workflows/wip.yml b/.github/workflows/wip.yml new file mode 100644 index 000000000..e0129757b --- /dev/null +++ b/.github/workflows/wip.yml @@ -0,0 +1,30 @@ +name: Open Issues + +on: + push: + branches: [ master ] + +env: + BUILD_TYPE: Debug + +jobs: + build: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v2 + + - name: Configure CMake + run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} + + - name: Build + # Build your program with the given configuration + run: cmake --build ${{github.workspace}}/build --config ${{env.BUILD_TYPE}} + + - name: Clone z3test + run: git clone https://github.com/z3prover/z3test z3test + + - name: Run regressions + run: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/issues + + diff --git a/README.md b/README.md index f9fad4f46..1eda3db92 100644 --- a/README.md +++ b/README.md @@ -14,9 +14,9 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z ## Build status -| Azure Pipelines | -| --------------- | -[![Build Status](https://dev.azure.com/Z3Public/Z3/_apis/build/status/Z3Prover.z3?branchName=master)](https://dev.azure.com/Z3Public/Z3/_build/latest?definitionId=1&branchName=master) +| Azure Pipelines | Code Coverage | Open Bugs | +| --------------- | --------------|-----------| +| [![Build Status](https://dev.azure.com/Z3Public/Z3/_apis/build/status/Z3Prover.z3?branchName=master)](https://dev.azure.com/Z3Public/Z3/_build/latest?definitionId=1&branchName=master) | [![CodeCoverage](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml) | [![Open Issues](https://github.com/Z3Prover/z3/actions/workflows/wip.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wip.yml) | [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 1735f2337..6c1cac8d5 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -149,6 +149,7 @@ jobs: # - template: scripts/test-java-cmake.yml - ${{if eq(variables['runTests'], 'True')}}: - template: scripts/test-regressions.yml + - job: "WindowsLatest" displayName: "Windows" diff --git a/contrib/ci/README.md b/contrib/ci/README.md index 8b48ac32e..9a8262e37 100644 --- a/contrib/ci/README.md +++ b/contrib/ci/README.md @@ -43,7 +43,7 @@ the future. * `Z3_CMAKE_GENERATOR` - CMake generator (`Ninja` or `Unix Makefiles`) * `Z3_VERBOSE_BUILD_OUTPUT` - Show compile commands in CMake builds (`0` or `1`) * `Z3_BUILD_LIBZ3_SHARED` - Build Z3 binaries and libraries dynamically/statically (`0` or `1`) -* `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty lastest revision will be used. +* `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty latest revision will be used. * `Z3_WARNINGS_AS_ERRORS` - Set the `WARNINGS_AS_ERRORS` CMake option passed to Z3 (`OFF`, `ON`, or `SERIOUS_ONLY`) ### Linux diff --git a/examples/ml/README b/examples/ml/README index 9797b85e3..a8d03eaea 100644 --- a/examples/ml/README +++ b/examples/ml/README @@ -14,9 +14,9 @@ for the byte-code version. If Z3 was installed into the ocamlfind package repository (see src/api/ml/README), then we can also compile this example as follows: -ocamlfind ocamlc -o ml_example.byte -package Z3 -linkpkg ml_example.ml +ocamlfind ocamlc -o ml_example.byte -thread -package Z3 -linkpkg ml_example.ml or -ocamlfind ocamlopt -o ml_example -package Z3 -linkpkg ml_example.ml +ocamlfind ocamlopt -o ml_example -thread -package Z3 -linkpkg ml_example.ml Note that the resulting binaries depend on the shared z3 library (libz3.dll/.so/.dylb), which needs to be in the PATH (Windows), LD_LIBRARY_PATH diff --git a/scripts/coverage.yml b/scripts/coverage.yml new file mode 100644 index 000000000..c091039b0 --- /dev/null +++ b/scripts/coverage.yml @@ -0,0 +1,37 @@ + +variables: + cmakeJulia: '-DZ3_BUILD_JULIA_BINDINGS=True' + cmakeJava: '-DZ3_BUILD_JAVA_BINDINGS=True' + cmakeNet: '-DZ3_BUILD_DOTNET_BINDINGS=True' + cmakePy: '-DZ3_BUILD_PYTHON_BINDINGS=True' + cmakeStdArgs: '-DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -G "Ninja" ../' + cmakeCovArgs: '-DCMAKE_INSTALL_PREFIX=./install -G "Ninja" ../' + asanEnv: 'CXXFLAGS="${CXXFLAGS} -fsanitize=address -fno-omit-frame-pointer" CFLAGS="${CFLAGS} -fsanitize=address -fno-omit-frame-pointer"' + ubsanEnv: 'CXXFLAGS="${CXXFLAGS} -fsanitize=undefined" CFLAGS="${CFLAGS} -fsanitize=undefined"' + msanEnv: 'CC=clang LDFLAGS="-L../libcxx/libcxx_msan/lib -lc++abi -Wl,-rpath=../libcxx/libcxx_msan/lib" CXX=clang++ CXXFLAGS="${CXXFLAGS} -stdlib=libc++ -fsanitize-memory-track-origins -fsanitize=memory -fPIE -fno-omit-frame-pointer -g -O2" CFLAGS="${CFLAGS} -stdlib=libc -fsanitize=memory -fsanitize-memory-track-origins -fno-omit-frame-pointer -g -O2"' + +jobs: + +- job: "UbuntuCMakeCoverage" + displayName: "Ubuntu build - cmake w/ coverage" + pool: + vmImage: "ubuntu-latest" + steps: + - script: sudo apt-get install ninja-build + - script: | + set -e + mkdir build + cd build + CXXFLAGS=--coverage LDFLAGS=-lgcov CC=clang CXX=clang++ cmake -DCMAKE_BUILD_TYPE=Debug $(cmakeCovArgs) + ninja + ninja test-z3 + ninja install + cd .. + - script: | + cd build + ./test-z3 -a + cd .. + - template: test-examples-cmake.yml + - template: test-regressions-coverage.yml + + diff --git a/scripts/test-regressions-coverage.yml b/scripts/test-regressions-coverage.yml new file mode 100644 index 000000000..363ea2c19 --- /dev/null +++ b/scripts/test-regressions-coverage.yml @@ -0,0 +1,4 @@ +steps: +- script: git clone https://github.com/z3prover/z3test z3test +- script: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2 +- script: python z3test/scripts/test_coverage_tests.py build/install z3test/coverage/cpp diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 648e3cd97..0d9b00351 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -159,7 +159,7 @@ extern "C" { return; } recfun_replace replace(m); - p.set_definition(replace, pd, n, _vars.data(), abs_body); + p.set_definition(replace, pd, true, n, _vars.data(), abs_body); Z3_CATCH; } @@ -1202,7 +1202,8 @@ extern "C" { case OP_STRING_STOI: return Z3_OP_STR_TO_INT; case OP_STRING_ITOS: return Z3_OP_INT_TO_STR; - case OP_STRING_UBVTOS: return Z3_OP_UBV_TO_STR; + case OP_STRING_UBVTOS: return Z3_OP_UBV_TO_STR; + case OP_STRING_SBVTOS: return Z3_OP_SBV_TO_STR; case OP_STRING_LT: return Z3_OP_STRING_LT; case OP_STRING_LE: return Z3_OP_STRING_LE; diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index fc336da74..9ce3ded09 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -245,6 +245,7 @@ extern "C" { MK_UNARY(Z3_mk_int_to_str, mk_c(c)->get_seq_fid(), OP_STRING_ITOS, SKIP); MK_UNARY(Z3_mk_str_to_int, mk_c(c)->get_seq_fid(), OP_STRING_STOI, SKIP); MK_UNARY(Z3_mk_ubv_to_str, mk_c(c)->get_seq_fid(), OP_STRING_UBVTOS, SKIP); + MK_UNARY(Z3_mk_sbv_to_str, mk_c(c)->get_seq_fid(), OP_STRING_SBVTOS, SKIP); Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) { diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 792b038e9..72cd364c6 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -506,7 +506,7 @@ namespace z3 { public: ast(context & c):object(c), m_ast(0) {} ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); } - ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); } + ast(ast const & s) :object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); } ast(ast && s) noexcept : object(std::forward(s)), m_ast(s.m_ast) { s.m_ast = nullptr; } ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); } operator Z3_ast() const { return m_ast; } @@ -519,14 +519,6 @@ namespace z3 { m_ast = s.m_ast; return *this; } - ast & operator=(ast && s) noexcept { - if (this != &s) { - object::operator=(std::forward(s)); - m_ast = s.m_ast; - s.m_ast = nullptr; - } - return *this; - } Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; } unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; } friend std::ostream & operator<<(std::ostream & out, ast const & n); @@ -1447,6 +1439,11 @@ namespace z3 { check_error(); return expr(ctx(), r); } + expr sbvtos() const { + Z3_ast r = Z3_mk_sbv_to_str(ctx(), *this); + check_error(); + return expr(ctx(), r); + } friend expr range(expr const& lo, expr const& hi); /** @@ -1874,11 +1871,15 @@ namespace z3 { Z3_ast r; if (a.is_int()) { expr zero = a.ctx().int_val(0); - r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a); + expr ge = a >= zero; + expr na = -a; + r = Z3_mk_ite(a.ctx(), ge, a, na); } else if (a.is_real()) { expr zero = a.ctx().real_val(0); - r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a); + expr ge = a >= zero; + expr na = -a; + r = Z3_mk_ite(a.ctx(), ge, a, na); } else { r = Z3_mk_fpa_abs(a.ctx(), a); diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index d40281a81..7279fe847 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -556,18 +556,18 @@ namespace Microsoft.Z3 /// /// Bind a definition to a recursive function declaration. - /// The function must have previously been created using - /// MkRecFuncDecl. The body may contain recursive uses of the function or - /// other mutually recursive functions. + /// The function must have previously been created using + /// MkRecFuncDecl. The body may contain recursive uses of the function or + /// other mutually recursive functions. /// - public void AddRecDef(FuncDecl f, Expr[] args, Expr body) - { - CheckContextMatch(f); - CheckContextMatch(args); - CheckContextMatch(body); + public void AddRecDef(FuncDecl f, Expr[] args, Expr body) + { + CheckContextMatch(f); + CheckContextMatch(args); + CheckContextMatch(body); IntPtr[] argsNative = AST.ArrayToNative(args); - Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject); - } + Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject); + } /// /// Creates a new function declaration. @@ -2405,6 +2405,15 @@ namespace Microsoft.Z3 return new SeqExpr(this, Native.Z3_mk_ubv_to_str(nCtx, e.NativeObject)); } + /// + /// Convert a bit-vector expression, represented as an signed number, to a string. + /// + public SeqExpr SbvToString(Expr e) { + Debug.Assert(e != null); + Debug.Assert(e is ArithExpr); + return new SeqExpr(this, Native.Z3_mk_sbv_to_str(nCtx, e.NativeObject)); + } + /// /// Convert an integer expression to a string. /// @@ -2474,7 +2483,7 @@ namespace Microsoft.Z3 /// /// Check if the string s1 is lexicographically strictly less than s2. /// - public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2) + public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2) { Debug.Assert(s1 != null); Debug.Assert(s2 != null); @@ -2485,7 +2494,7 @@ namespace Microsoft.Z3 /// /// Check if the string s1 is lexicographically strictly less than s2. /// - public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2) + public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2) { Debug.Assert(s1 != null); Debug.Assert(s2 != null); @@ -2655,7 +2664,7 @@ namespace Microsoft.Z3 /// /// Create the empty regular expression. - /// The sort s should be a regular expression. + /// The sort s should be a regular expression. /// public ReExpr MkEmptyRe(Sort s) { @@ -2665,7 +2674,7 @@ namespace Microsoft.Z3 /// /// Create the full regular expression. - /// The sort s should be a regular expression. + /// The sort s should be a regular expression. /// public ReExpr MkFullRe(Sort s) { @@ -3399,7 +3408,7 @@ namespace Microsoft.Z3 { Debug.Assert(t1 != null); Debug.Assert(t2 != null); - // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null)); + // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null)); return AndThen(t1, t2, ts); } @@ -4696,7 +4705,7 @@ namespace Microsoft.Z3 { foreach (Z3Object a in arr) { - Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert + Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert CheckContextMatch(a); } } diff --git a/src/api/java/Context.java b/src/api/java/Context.java index a6b867eb8..1e581c482 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2035,7 +2035,15 @@ public class Context implements AutoCloseable { { return (SeqExpr) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject())); } - + + /** + * Convert an signed bitvector expression to a string. + */ + public SeqExpr sbvToString(Expr e) + { + return (SeqExpr) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject())); + } + /** * Convert an integer expression to a string. */ diff --git a/src/api/z3_api.h b/src/api/z3_api.h index f636e7caa..79f7ca25d 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1203,6 +1203,7 @@ typedef enum { Z3_OP_STR_TO_INT, Z3_OP_INT_TO_STR, Z3_OP_UBV_TO_STR, + Z3_OP_SBV_TO_STR, Z3_OP_STRING_LT, Z3_OP_STRING_LE, @@ -3655,6 +3656,12 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s); + /** + \brief Signed bit-vector to string conversion. + + def_API('Z3_mk_sbv_to_str' ,AST ,(_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s); /** \brief Create a regular expression that accepts the sequence \c seq. diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp index f7ba8132f..de6efe020 100644 --- a/src/ast/ast_ll_pp.cpp +++ b/src/ast/ast_ll_pp.cpp @@ -248,8 +248,7 @@ public: } } - void operator()(quantifier * n) { - display_def_header(n); + void display_quantifier_header(quantifier* n) { m_out << "(" << (n->get_kind() == forall_k ? "forall" : (n->get_kind() == exists_k ? "exists" : "lambda")) << " "; unsigned num_decls = n->get_num_decls(); m_out << "(vars "; @@ -272,6 +271,12 @@ public: display_children(n->get_num_no_patterns(), n->get_no_patterns()); m_out << ") "; } + + } + + void operator()(quantifier * n) { + display_def_header(n); + display_quantifier_header(n); display_child(n->get_expr()); m_out << ")\n"; } @@ -281,6 +286,12 @@ public: m_out << "(:var " << to_var(n)->get_idx() << ")"; return; } + if (is_quantifier(n)) { + display_quantifier_header(to_quantifier(n)); + display(to_quantifier(n)->get_expr(), depth - 1); + m_out << ")"; + return; + } if (!is_app(n) || depth == 0 || to_app(n)->get_num_args() == 0) { display_child(n); @@ -304,16 +315,11 @@ public: void display_bounded(ast * n, unsigned depth) { if (!n) - m_out << "null"; - else if (is_app(n)) { - display(to_expr(n), depth); - } - else if (is_var(n)) { - m_out << "(:var " << to_var(n)->get_idx() << ")"; - } - else { - m_out << "#" << n->get_id(); - } + m_out << "null"; + else if (is_expr(n)) + display(to_expr(n), depth); + else + m_out << "#" << n->get_id(); } }; diff --git a/src/ast/ast_pp.h b/src/ast/ast_pp.h index 58ee3145c..1b3ca4a81 100644 --- a/src/ast/ast_pp.h +++ b/src/ast/ast_pp.h @@ -31,6 +31,7 @@ struct mk_pp : public mk_ismt2_pp { } }; + //get_expr()) || m.is_true(r2->get_expr()))) add_literal(n1, false); if (n1->is_equality() && n1->value() == l_false) @@ -594,6 +595,12 @@ namespace euf { return false; } + enode* egraph::get_enode_eq_to(func_decl* f, unsigned num_args, enode* const* args) { + m_tmp_app.set_decl(f); + m_tmp_app.set_num_args(num_args); + return find(m_tmp_app.get_app(), num_args, args); + } + /** \brief generate an explanation for a congruence. Each pair of children under a congruence have the same roots diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index 1e0252922..1ac54f6f0 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -156,26 +156,27 @@ namespace euf { svector m_updates; unsigned_vector m_scopes; enode_vector m_expr2enode; - enode* m_tmp_eq { nullptr }; - enode* m_tmp_node { nullptr }; - unsigned m_tmp_node_capacity { 0 }; + enode* m_tmp_eq = nullptr; + enode* m_tmp_node = nullptr; + unsigned m_tmp_node_capacity = 0; + tmp_app m_tmp_app; enode_vector m_nodes; expr_ref_vector m_exprs; vector m_decl2enodes; enode_vector m_empty_enodes; - unsigned m_num_scopes { 0 }; - bool m_inconsistent { false }; - enode *m_n1 { nullptr }; - enode *m_n2 { nullptr }; + unsigned m_num_scopes = 0; + bool m_inconsistent = false; + enode *m_n1 = nullptr; + enode *m_n2 = nullptr; justification m_justification; - unsigned m_new_lits_qhead { 0 }; - unsigned m_new_th_eqs_qhead { 0 }; + unsigned m_new_lits_qhead = 0; + unsigned m_new_th_eqs_qhead = 0; svector m_new_lits; svector m_new_th_eqs; bool_vector m_th_propagates_diseqs; enode_vector m_todo; stats m_stats; - bool m_uses_congruence { false }; + bool m_uses_congruence = false; std::function m_on_merge; std::function m_on_make; std::function m_used_eq; @@ -261,7 +262,7 @@ namespace euf { */ bool are_diseq(enode* a, enode* b) const; - enode * get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args) { UNREACHABLE(); return nullptr; } + enode* get_enode_eq_to(func_decl* f, unsigned num_args, enode* const* args); /** \brief Maintain and update cursor into propagated consequences. @@ -326,6 +327,7 @@ namespace euf { void collect_statistics(statistics& st) const; unsigned num_scopes() const { return m_scopes.size() + m_num_scopes; } + unsigned num_nodes() const { return m_nodes.size(); } }; inline std::ostream& operator<<(std::ostream& out, egraph const& g) { return g.display(out); } diff --git a/src/ast/euf/euf_etable.h b/src/ast/euf/euf_etable.h index 68ae95cd2..d6b64e756 100644 --- a/src/ast/euf/euf_etable.h +++ b/src/ast/euf/euf_etable.h @@ -125,7 +125,7 @@ namespace euf { ast_manager & m_manager; - bool m_commutativity{ false }; //!< true if the last found congruence used commutativity + bool m_commutativity = false; //!< true if the last found congruence used commutativity ptr_vector m_tables; map m_func_decl2id; diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index e439ae3e0..c024d870e 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -467,7 +467,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decl See normalize_expr */ void macro_util::mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const { - TRACE("macro_util", tout << mk_pp(head, m_manager) << "\n";); + TRACE("macro_util", tout << mk_pp(head, m_manager) << "\n" << mk_pp(def, m_manager) << "\n";); SASSERT(is_macro_head(head, head->get_num_args()) || is_quasi_macro_ok(head, head->get_num_args(), def)); SASSERT(!occurs(head->get_decl(), def)); diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp index f34336d84..a3e6c61e7 100644 --- a/src/ast/macros/quasi_macros.cpp +++ b/src/ast/macros/quasi_macros.cpp @@ -110,10 +110,9 @@ bool quasi_macros::fully_depends_on(app * a, quantifier * q) const { // direct argument of a, i.e., a->get_arg(i) == v for some i bit_vector bitset; bitset.resize(q->get_num_decls(), false); - for (unsigned i = 0 ; i < a->get_num_args() ; i++) { - if (is_var(a->get_arg(i))) - bitset.set(to_var(a->get_arg(i))->get_idx(), true); - } + for (expr* arg : *a) + if (is_var(arg)) + bitset.set(to_var(arg)->get_idx(), true); for (unsigned i = 0; i < bitset.size() ; i++) { if (!bitset.get(i)) @@ -198,6 +197,7 @@ bool quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant bit_vector v_seen; v_seen.resize(q->get_num_decls(), false); + unsigned num_seen = 0; for (unsigned i = 0; i < a->get_num_args(); ++i) { expr* arg = a->get_arg(i); if (!is_var(arg) && !is_ground(arg)) @@ -215,8 +215,11 @@ bool quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant var * v = to_var(arg); m_new_vars.push_back(v); v_seen.set(v->get_idx(), true); + ++num_seen; } } + if (num_seen < q->get_num_decls()) + return false; // Reverse the new variable names and sorts. [CMW: There is a smarter way to do this.] vector new_var_names_rev; diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp index 209772f3b..8a94a3482 100644 --- a/src/ast/normal_forms/pull_quant.cpp +++ b/src/ast/normal_forms/pull_quant.cpp @@ -281,9 +281,9 @@ struct pull_quant::imp { m.mk_rewrite(old_q, result); return true; } - if (is_lambda(old_q)) { - return false; - } + + if (is_lambda(old_q)) + return false; if (!is_forall(new_body)) return false; diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 3411f8cec..a702b4bfd 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -209,6 +209,7 @@ namespace recfun { void def::compute_cases(util& u, replace& subst, is_immediate_pred & is_i, + bool is_macro, unsigned n_vars, var *const * vars, expr* rhs) { VERIFY(m_cases.empty() && "cases cannot already be computed"); @@ -227,7 +228,7 @@ namespace recfun { expr_ref_vector conditions(m); // is the function a macro (unconditional body)? - if (n_vars == 0 || !contains_ite(u, rhs)) { + if (is_macro || n_vars == 0 || !contains_ite(u, rhs)) { // constant function or trivial control flow, only one (dummy) case add_case(name, 0, conditions, rhs); return; @@ -335,10 +336,11 @@ namespace recfun { return alloc(def, m(), m_fid, name, n, domain, range, is_generated); } - - void util::set_definition(replace& subst, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) { - expr_ref rhs1 = get_plugin().redirect_ite(subst, n_vars, vars, rhs); - d.set_definition(subst, n_vars, vars, rhs1); + void util::set_definition(replace& subst, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) { + expr_ref rhs1(rhs, m()); + if (!is_macro) + rhs1 = get_plugin().redirect_ite(subst, n_vars, vars, rhs); + d.set_definition(subst, is_macro, n_vars, vars, rhs1); } app_ref util::mk_num_rounds_pred(unsigned d) { @@ -369,11 +371,11 @@ namespace recfun { }; // set definition - void promise_def::set_definition(replace& r, unsigned n_vars, var * const * vars, expr * rhs) { + void promise_def::set_definition(replace& r, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) { SASSERT(n_vars == d->get_arity()); is_imm_pred is_i(*u); - d->compute_cases(*u, r, is_i, n_vars, vars, rhs); + d->compute_cases(*u, r, is_i, is_macro, n_vars, vars, rhs); } namespace decl { @@ -426,8 +428,8 @@ namespace recfun { } } - void plugin::set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) { - u().set_definition(r, d, n_vars, vars, rhs); + void plugin::set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) { + u().set_definition(r, d, is_macro, n_vars, vars, rhs); for (case_def & c : d.get_def()->get_cases()) { m_case_defs.insert(c.get_decl(), &c); } @@ -437,12 +439,12 @@ namespace recfun { return !m_case_defs.empty(); } - def* plugin::mk_def(replace& subst, + def* plugin::mk_def(replace& subst, bool is_macro, symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs) { promise_def d = mk_def(name, n, params, range); SASSERT(! m_defs.contains(d.get_def()->get_decl())); - set_definition(subst, d, n_vars, vars, rhs); + set_definition(subst, d, is_macro, n_vars, vars, rhs); return d.get_def(); } @@ -520,7 +522,7 @@ namespace recfun { auto pd = mk_def(fresh_name, n, domain.data(), max_expr->get_sort()); func_decl* f = pd.get_def()->get_decl(); expr_ref new_body(m().mk_app(f, n, args.data()), m()); - set_definition(subst, pd, n, vars, max_expr); + set_definition(subst, pd, false, n, vars, max_expr); subst.reset(); subst.insert(max_expr, new_body); result = subst(result); @@ -528,7 +530,6 @@ namespace recfun { } return result; } - } case_expansion::case_expansion(recfun::util& u, app * n) : diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index 22f2e76fe..dd6f5181a 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -114,7 +114,7 @@ namespace recfun { // compute cases for a function, given its RHS (possibly containing `ite`). void compute_cases(util& u, replace& subst, is_immediate_pred &, - unsigned n_vars, var *const * vars, expr* rhs); + bool is_macro, unsigned n_vars, var *const * vars, expr* rhs); void add_case(std::string & name, unsigned case_index, expr_ref_vector const& conditions, expr* rhs, bool is_imm = false); bool contains_ite(util& u, expr* e); // expression contains a test over a def? bool contains_def(util& u, expr* e); // expression contains a def @@ -138,7 +138,7 @@ namespace recfun { friend class util; util * u; def * d; - void set_definition(replace& r, unsigned n_vars, var * const * vars, expr * rhs); // call only once + void set_definition(replace& r, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs); // call only once public: promise_def(util * u, def * d) : u(u), d(d) {} promise_def(promise_def const & from) : u(from.u), d(from.d) {} @@ -182,9 +182,9 @@ namespace recfun { promise_def ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated = false); - void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs); + void set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs); - def* mk_def(replace& subst, symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs); + def* mk_def(replace& subst, bool is_macro, symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs); void erase_def(func_decl* f); @@ -216,7 +216,7 @@ namespace recfun { decl::plugin * m_plugin; bool compute_is_immediate(expr * rhs); - void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs); + void set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs); public: util(ast_manager &m); diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index cffef51a0..edc91e21f 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -776,48 +776,84 @@ namespace seq { rational pow(1); for (unsigned i = 0; i < k; ++i) pow *= 10; - if (k == 0) { - ge10k = m.mk_true(); - } - else { - ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b); - } + ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b); ge10k1 = bv.mk_ule(bv.mk_numeral(pow * 10, bv_sort), b); unsigned sz = bv.get_bv_size(b); expr_ref_vector es(m); expr_ref bb(b, m), ten(bv.mk_numeral(10, sz), m); - pow = 1; + rational p(1); for (unsigned i = 0; i <= k; ++i) { - if (pow > 1) - bb = bv.mk_bv_udiv(b, bv.mk_numeral(pow, bv_sort)); + if (p > 1) + bb = bv.mk_bv_udiv(b, bv.mk_numeral(p, bv_sort)); es.push_back(seq.str.mk_unit(m_sk.mk_ubv2ch(bv.mk_bv_urem(bb, ten)))); - pow *= 10; + p *= 10; } es.reverse(); eq = m.mk_eq(seq.str.mk_ubv2s(b), seq.str.mk_concat(es, seq.str.mk_string_sort())); - add_clause(~ge10k, ge10k1, eq); + SASSERT(pow < rational::power_of_two(sz)); + if (k == 0) + add_clause(ge10k1, eq); + else if (pow * 10 >= rational::power_of_two(sz)) + add_clause(~ge10k, eq); + else + add_clause(~ge10k, ge10k1, eq); + } + + /* + * 1 <= len(ubv2s(b)) <= k, where k is min such that 10^k > 2^sz + */ + void axioms::ubv2s_len_axiom(expr* b) { + bv_util bv(m); + sort* bv_sort = b->get_sort(); + unsigned sz = bv.get_bv_size(bv_sort); + unsigned k = 1; + rational pow(10); + while (pow <= rational::power_of_two(sz)) + ++k, pow *= 10; + expr_ref len(seq.str.mk_length(seq.str.mk_ubv2s(b)), m); + expr_ref ge(a.mk_ge(len, a.mk_int(1)), m); + expr_ref le(a.mk_le(len, a.mk_int(k)), m); + add_clause(le); + add_clause(ge); } /* * len(ubv2s(b)) = k => 10^k-1 <= b < 10^{k} k > 1 * len(ubv2s(b)) = 1 => b < 10^{1} k = 1 + * len(ubv2s(b)) >= k => is_digit(nth(ubv2s(b), 0)) & ... & is_digit(nth(ubv2s(b), k-1)) */ void axioms::ubv2s_len_axiom(expr* b, unsigned k) { - expr_ref ge10k(m), ge10k1(m), eq(m); + expr_ref ge10k(m), ge10k1(m), eq(m), is_digit(m); + expr_ref ubvs(seq.str.mk_ubv2s(b), m); + expr_ref len(seq.str.mk_length(ubvs), m); + expr_ref ge_len(a.mk_ge(len, a.mk_int(k)), m); bv_util bv(m); sort* bv_sort = b->get_sort(); unsigned sz = bv.get_bv_size(bv_sort); rational pow(1); for (unsigned i = 1; i < k; ++i) pow *= 10; - if (pow * 10 >= rational::power_of_two(sz)) - return; // TODO: add conflict when k is too large or avoid overflow bounds and limits + + if (pow >= rational::power_of_two(sz)) { + expr_ref ge(a.mk_ge(len, a.mk_int(k)), m); + add_clause(~ge); + return; + } + ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b); ge10k1 = bv.mk_ule(bv.mk_numeral(pow * 10, bv_sort), b); - eq = m.mk_eq(seq.str.mk_length(seq.str.mk_ubv2s(b)), a.mk_int(k)); - add_clause(~eq, ~ge10k1); + eq = m.mk_eq(len, a.mk_int(k)); + + if (pow * 10 < rational::power_of_two(sz)) + add_clause(~eq, ~ge10k1); if (k > 1) add_clause(~eq, ge10k); + + for (unsigned i = 0; i < k; ++i) { + expr* ch = seq.str.mk_nth_i(ubvs, i); + is_digit = seq.mk_char_is_digit(ch); + add_clause(~ge_len, is_digit); + } } void axioms::ubv2ch_axiom(sort* bv_sort) { diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h index c9cdbfc9a..6cd83b00f 100644 --- a/src/ast/rewriter/seq_axioms.h +++ b/src/ast/rewriter/seq_axioms.h @@ -96,6 +96,7 @@ namespace seq { void itos_axiom(expr* s, unsigned k); void ubv2s_axiom(expr* b, unsigned k); void ubv2s_len_axiom(expr* b, unsigned k); + void ubv2s_len_axiom(expr* b); void ubv2ch_axiom(sort* bv_sort); void lt_axiom(expr* n); void le_axiom(expr* n); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 0bd653232..6bf44f4ba 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -672,6 +672,14 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 3); st = mk_seq_replace_all(args[0], args[1], args[2], result); break; + case OP_SEQ_REPLACE_RE: + SASSERT(num_args == 3); + st = mk_seq_replace_re(args[0], args[1], args[2], result); + break; + case OP_SEQ_REPLACE_RE_ALL: + SASSERT(num_args == 3); + st = mk_seq_replace_re_all(args[0], args[1], args[2], result); + break; case OP_SEQ_TO_RE: SASSERT(num_args == 1); st = mk_str_to_regexp(args[0], result); @@ -718,6 +726,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 1); st = mk_str_ubv2s(args[0], result); break; + case OP_STRING_SBVTOS: + SASSERT(num_args == 1); + st = mk_str_sbv2s(args[0], result); + break; case _OP_STRING_CONCAT: case _OP_STRING_PREFIX: case _OP_STRING_SUFFIX: @@ -1900,6 +1912,8 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref& result = str().mk_concat(strs, a->get_sort()); return BR_REWRITE_FULL; } + // TBD: add case when a, b are concatenation of units that are values. + // in this case we can use a similar loop as for strings. return BR_FAILED; } @@ -1911,7 +1925,6 @@ br_status seq_rewriter::mk_seq_replace_re(expr* a, expr* b, expr* c, expr_ref& r return BR_FAILED; } - br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { TRACE("seq", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << "\n";); zstring s1, s2; @@ -2218,6 +2231,30 @@ br_status seq_rewriter::mk_str_ubv2s(expr* a, expr_ref& result) { return BR_FAILED; } +br_status seq_rewriter::mk_str_sbv2s(expr *a, expr_ref &result) { + bv_util bv(m()); + rational val; + unsigned bv_size = 0; + if (bv.is_numeral(a, val, bv_size)) { + rational r = mod(val, rational::power_of_two(bv_size)); + SASSERT(!r.is_neg()); + if (r >= rational::power_of_two(bv_size - 1)) { + r -= rational::power_of_two(bv_size); + } + result = str().mk_string(zstring(r)); + return BR_DONE; + } + + bv_size = bv.get_bv_size(a); + result = m().mk_ite( + bv.mk_slt(a,bv.mk_numeral(0, bv_size)), + str().mk_concat( + str().mk_string(zstring("-")), + str().mk_ubv2s(bv.mk_bv_neg(a)) + ), + str().mk_ubv2s(a)); + return BR_REWRITE_FULL; +} br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) { rational r; @@ -3158,7 +3195,7 @@ expr_ref seq_rewriter::mk_der_cond(expr* cond, expr* ele, sort* seq_sort) { expr *c1 = nullptr, *c2 = nullptr, *ch1 = nullptr, *ch2 = nullptr; unsigned ch = 0; expr_ref result(m()), r1(m()), r2(m()); - if (m().is_eq(cond, ch1, ch2)) { + if (m().is_eq(cond, ch1, ch2) && u().is_char(ch1)) { r1 = u().mk_le(ch1, ch2); r1 = mk_der_cond(r1, ele, seq_sort); r2 = u().mk_le(ch2, ch1); @@ -3219,11 +3256,17 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { } expr_ref dr2 = mk_derivative(ele, r2); is_n = re_predicate(is_n, seq_sort); - // Instead of mk_der_union here, we use mk_der_antimorov_union to - // force the two cases to be considered separately and lifted to - // the top level. This avoids blowup in cases where determinization - // is expensive. - return mk_der_antimorov_union(result, mk_der_concat(is_n, dr2)); + if (re().is_empty(dr2)) { + //do not concatenate [], it is a deade-end + return result; + } + else { + // Instead of mk_der_union here, we use mk_der_antimorov_union to + // force the two cases to be considered separately and lifted to + // the top level. This avoids blowup in cases where determinization + // is expensive. + return mk_der_antimorov_union(result, mk_der_concat(is_n, dr2)); + } } else if (re().is_star(r, r1)) { return mk_der_concat(mk_derivative(ele, r1), r); @@ -3256,8 +3299,15 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { if (lo > 0) { lo--; } - result = re().mk_loop(r1, lo); - return mk_der_concat(mk_derivative(ele, r1), result); + result = mk_derivative(ele, r1); + //do not concatenate with [] (emptyset) + if (re().is_empty(result)) { + return result; + } + else { + //do not create loop r1{0,}, instead create r1* + return mk_der_concat(result, (lo == 0 ? re().mk_star(r1) : re().mk_loop(r1, lo))); + } } else if (re().is_loop(r, r1, lo, hi)) { if (hi == 0) { @@ -3267,8 +3317,14 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { if (lo > 0) { lo--; } - result = re().mk_loop(r1, lo, hi); - return mk_der_concat(mk_derivative(ele, r1), result); + result = mk_derivative(ele, r1); + //do not concatenate with [] (emptyset) or handle the rest of the loop if no more iterations remain + if (re().is_empty(result) || hi == 0) { + return result; + } + else { + return mk_der_concat(result, re().mk_loop(r1, lo, hi)); + } } else if (re().is_full_seq(r) || re().is_empty(r)) { @@ -3288,20 +3344,23 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { return result; } else if (str().is_empty(r1)) { + //observe: str().is_empty(r1) checks that r = () = epsilon + //while mk_empty() = [], because deriv(epsilon) = [] = nothing return mk_empty(); } -#if 0 - else { + else if (str().is_itos(r1, r2)) { + // + // here r1 = (str.from_int r2) and r2 is non-ground + // or else the expression would have been simplified earlier + // so r1 must be nonempty and must consists of decimal digits + // '0' <= elem <= '9' + // if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else [] + // hd = str().mk_nth_i(r1, m_autil.mk_int(0)); - tl = str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1))); - result = re().mk_to_re(tl); - result = - m().mk_ite(m_br.mk_eq_rw(r1, str().mk_empty(m().get_sort(r1))), - mk_empty(), - re_and(m_br.mk_eq_rw(ele, hd), result)); - return result; + m_br.mk_and(u().mk_le(m_util.mk_char('0'), ele), u().mk_le(ele, m_util.mk_char('9')), m().mk_eq(hd, ele), result); + tl = re().mk_to_re(str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1)))); + return re_and(result, tl); } -#endif } else if (re().is_reverse(r, r1) && re().is_to_re(r1, r2)) { // Reverses are rewritten so that the only derivative case is @@ -3342,6 +3401,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { } expr* e1 = nullptr, *e2 = nullptr; if (str().is_unit(r1, e1) && str().is_unit(r2, e2)) { + SASSERT(u().is_char(e1)); // Use mk_der_cond to normalize STRACE("seq_verbose", tout << "deriv range str" << std::endl;); expr_ref p1(u().mk_le(e1, ele), m()); @@ -3900,6 +3960,7 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) { comp(none) -> all comp(all) -> none comp(comp(e1)) -> e1 + comp(epsilon) -> .+ */ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) { expr *e1 = nullptr, *e2 = nullptr; @@ -3923,6 +3984,10 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) { result = e1; return BR_DONE; } + if (re().is_to_re(a, e1) && str().is_empty(e1)) { + result = re().mk_plus(re().mk_full_char(a->get_sort())); + return BR_DONE; + } return BR_FAILED; } @@ -4110,6 +4175,7 @@ br_status seq_rewriter::mk_re_power(func_decl* f, expr* a, expr_ref& result) { a+* = a* emp* = "" all* = all + .+* = all */ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { expr* b, *c, *b1, *c1; @@ -4132,7 +4198,10 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { return BR_DONE; } if (re().is_plus(a, b)) { - result = re().mk_star(b); + if (re().is_full_char(b)) + result = re().mk_full_seq(a->get_sort()); + else + result = re().mk_star(b); return BR_DONE; } if (re().is_union(a, b, c)) { diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 7d102a5fb..c779a5f73 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -229,6 +229,7 @@ class seq_rewriter { br_status mk_str_itos(expr* a, expr_ref& result); br_status mk_str_stoi(expr* a, expr_ref& result); br_status mk_str_ubv2s(expr* a, expr_ref& result); + br_status mk_str_sbv2s(expr* a, expr_ref& result); br_status mk_str_in_regexp(expr* a, expr* b, expr_ref& result); br_status mk_str_to_regexp(expr* a, expr_ref& result); br_status mk_str_le(expr* a, expr* b, expr_ref& result); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index ea073f23f..6695d9497 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -350,7 +350,7 @@ func_decl* seq_decl_plugin::mk_left_assoc_fun(decl_kind k, unsigned arity, sort* return mk_assoc_fun(k, arity, domain, range, k_seq, k_string, false); } -func_decl* seq_decl_plugin::mk_ubv2s(unsigned arity, sort* const* domain) { +func_decl* seq_decl_plugin::mk_ubv2s(unsigned arity, sort* const* domain) const { ast_manager& m = *m_manager; if (arity != 1) m.raise_exception("Invalid str.from_ubv expects one bit-vector argument"); @@ -361,6 +361,17 @@ func_decl* seq_decl_plugin::mk_ubv2s(unsigned arity, sort* const* domain) { return m.mk_func_decl(symbol("str.from_ubv"), arity, domain, rng, func_decl_info(m_family_id, OP_STRING_UBVTOS)); } +func_decl* seq_decl_plugin::mk_sbv2s(unsigned arity, sort* const* domain) const { + ast_manager &m = *m_manager; + if (arity != 1) + m.raise_exception("Invalid str.from_sbv expects one bit-vector argument"); + bv_util bv(m); + if (!bv.is_bv_sort(domain[0])) + m.raise_exception("Invalid str.from_sbv expects one bit-vector argument"); + sort *rng = m_string; + return m.mk_func_decl(symbol("str.from_sbv"), arity, domain, rng, func_decl_info(m_family_id, OP_STRING_SBVTOS)); +} + func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq, decl_kind k_string, bool is_right) { ast_manager& m = *m_manager; sort_ref rng(m); @@ -376,7 +387,7 @@ func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* cons } -func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { init(); m_has_seq = true; @@ -416,8 +427,12 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_STRING_FROM_CODE: match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); + case OP_STRING_UBVTOS: - return mk_ubv2s(arity, domain); + return mk_ubv2s(arity, domain); + + case OP_STRING_SBVTOS: + return mk_sbv2s(arity, domain); case _OP_REGEXP_FULL_CHAR: m_has_re = true; @@ -627,6 +642,7 @@ void seq_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("re.nostr", _OP_REGEXP_EMPTY)); op_names.push_back(builtin_name("re.complement", OP_RE_COMPLEMENT)); op_names.push_back(builtin_name("str.from_ubv", OP_STRING_UBVTOS)); + op_names.push_back(builtin_name("str.from_sbv", OP_STRING_SBVTOS)); } void seq_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 61bbf7ba1..3c0f28ca6 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -80,6 +80,7 @@ enum seq_op_kind { OP_STRING_ITOS, OP_STRING_STOI, OP_STRING_UBVTOS, + OP_STRING_SBVTOS, OP_STRING_LT, OP_STRING_LE, OP_STRING_IS_DIGIT, @@ -150,7 +151,8 @@ class seq_decl_plugin : public decl_plugin { func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq); func_decl* mk_left_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq); func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq, bool is_right); - func_decl* mk_ubv2s(unsigned arity, sort* const* domain); + func_decl* mk_ubv2s(unsigned arity, sort* const* domain) const; + func_decl* mk_sbv2s(unsigned arity, sort* const* domain) const; void init(); @@ -297,6 +299,7 @@ public: app* mk_itos(expr* i) const { return m.mk_app(m_fid, OP_STRING_ITOS, 1, &i); } app* mk_stoi(expr* s) const { return m.mk_app(m_fid, OP_STRING_STOI, 1, &s); } app* mk_ubv2s(expr* b) const { return m.mk_app(m_fid, OP_STRING_UBVTOS, 1, &b); } + app* mk_sbv2s(expr* b) const { return m.mk_app(m_fid, OP_STRING_SBVTOS, 1, &b); } app* mk_is_empty(expr* s) const; app* mk_lex_lt(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LT, 2, es); } app* mk_lex_le(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LE, 2, es); } @@ -336,6 +339,7 @@ public: bool is_itos(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_ITOS); } bool is_stoi(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STOI); } bool is_ubv2s(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_UBVTOS); } + bool is_sbv2s(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_SBVTOS); } bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); } bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); } bool is_lt(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_LT); } @@ -374,6 +378,7 @@ public: MATCH_UNARY(is_itos); MATCH_UNARY(is_stoi); MATCH_UNARY(is_ubv2s); + MATCH_UNARY(is_sbv2s); MATCH_UNARY(is_is_digit); MATCH_UNARY(is_from_code); MATCH_UNARY(is_to_code); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 2ec910595..2133a1c00 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -365,7 +365,7 @@ void cmd_context::insert_macro(symbol const& s, unsigned arity, sort*const* doma // recursive functions have opposite calling convention from macros! var_subst sub(m(), true); expr_ref tt = sub(t, rvars); - p.set_definition(replace, d, vars.size(), vars.data(), tt); + p.set_definition(replace, d, true, vars.size(), vars.data(), tt); register_fun(s, d.get_def()->get_decl()); } @@ -1004,7 +1004,7 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s recfun::promise_def d = p.get_promise_def(f); recfun_replace replace(m()); - p.set_definition(replace, d, vars.size(), vars.data(), rhs); + p.set_definition(replace, d, false, vars.size(), vars.data(), rhs); } func_decl * cmd_context::find_func_decl(symbol const & s) const { diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index 6a05de93f..e63e71be6 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -134,7 +134,15 @@ namespace opt { } void model_based_opt::def::normalize() { - SASSERT(m_div.is_int()); + if (!m_div.is_int()) { + rational den = denominator(m_div); + SASSERT(den > 1); + for (var& v : m_vars) + v.m_coeff *= den; + m_coeff *= den; + m_div *= den; + + } if (m_div.is_neg()) { for (var& v : m_vars) v.m_coeff.neg(); @@ -528,6 +536,13 @@ namespace opt { } } + /** + * a1 > 0 + * a1*x + r1 = value + * a2*x + r2 <= 0 + * ------------------ + * a1*r2 - a2*r1 <= value + */ void model_based_opt::solve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x) { SASSERT(a1 == get_coefficient(row_src, x)); SASSERT(a1.is_pos()); @@ -1195,22 +1210,25 @@ namespace opt { model_based_opt::def model_based_opt::solve_for(unsigned row_id1, unsigned x, bool compute_def) { TRACE("opt", tout << "v" << x << " := " << eval(x) << "\n" << m_rows[row_id1] << "\n";); rational a = get_coefficient(row_id1, x), b; - ineq_type ty = m_rows[row_id1].m_type; + row& r1 = m_rows[row_id1]; + ineq_type ty = r1.m_type; SASSERT(!a.is_zero()); - SASSERT(m_rows[row_id1].m_alive); + SASSERT(r1.m_alive); if (a.is_neg()) { a.neg(); - m_rows[row_id1].neg(); + r1.neg(); } SASSERT(a.is_pos()); if (ty == t_lt) { SASSERT(compute_def); - m_rows[row_id1].m_coeff += a; - m_rows[row_id1].m_type = t_le; - m_rows[row_id1].m_value += a; - } - if (m_var2is_int[x] && !a.is_one()) { - row& r1 = m_rows[row_id1]; + r1.m_coeff -= r1.m_value; + r1.m_type = t_le; + r1.m_value = 0; + } + + if (m_var2is_int[x] && !a.is_one()) { + r1.m_coeff -= r1.m_value; + r1.m_value = 0; vector coeffs; mk_coeffs_without(coeffs, r1.m_vars, x); rational c = mod(-eval(coeffs), a); diff --git a/src/model/model.cpp b/src/model/model.cpp index f2861292f..e93e80bfe 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -22,6 +22,7 @@ Revision History: #include "ast/ast_ll_pp.h" #include "ast/rewriter/var_subst.h" #include "ast/rewriter/th_rewriter.h" +#include "ast/rewriter/expr_safe_replace.h" #include "ast/array_decl_plugin.h" #include "ast/bv_decl_plugin.h" #include "ast/recfun_decl_plugin.h" @@ -605,12 +606,13 @@ void model::add_rec_funs() { func_interp* fi = alloc(func_interp, m, f->get_arity()); // reverse argument order so that variable 0 starts at the beginning. - expr_ref_vector subst(m); - for (unsigned i = 0; i < f->get_arity(); ++i) { - subst.push_back(m.mk_var(i, f->get_domain(i))); + expr_safe_replace subst(m); + unsigned arity = f->get_arity(); + for (unsigned i = 0; i < arity; ++i) { + subst.insert(m.mk_var(arity - i - 1, f->get_domain(i)), m.mk_var(i, f->get_domain(i))); } - var_subst sub(m, true); - expr_ref bodyr = sub(rhs, subst); + expr_ref bodyr(m); + subst(rhs, bodyr); fi->set_else(bodyr); register_decl(f, fi); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 23bab1761..fc620d757 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -150,9 +150,9 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { auto st = reduce_app_core(f, num, args, result, result_pr); CTRACE("model_evaluator", st != BR_FAILED, - tout << f->get_name() << "\n"; - for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << "\n"; - tout << result << "\n";); + tout << f->get_name() << " "; + for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << " "; + tout << "\n--> " << result << "\n";); return st; } diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp index ba20e5f24..e8d769621 100644 --- a/src/muz/spacer/spacer_manager.cpp +++ b/src/muz/spacer/spacer_manager.cpp @@ -247,7 +247,7 @@ bool is_zk_const (const app *a, int &n) { } bool sk_lt_proc::operator()(const app *a1, const app *a2) { if (a1 == a2) return false; - int n1, n2; + int n1 = 0, n2 = 0; bool z1, z2; z1 = is_zk_const(a1, n1); z2 = is_zk_const(a2, n2); diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index e87965133..27b3b7260 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -871,6 +871,8 @@ public: m_dump_benchmarks = p.dump_benchmarks(); m_enable_lns = p.enable_lns(); m_lns_conflicts = p.lns_conflicts(); + if (m_c.num_objectives() > 1) + m_add_upper_bound_block = false; } lbool init_local() { diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 344c61283..953b1979f 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -3118,6 +3118,23 @@ namespace smt2 { return sexpr_ref(nullptr, sm()); } + sort_ref parse_sort_ref(char const* context) { + m_num_bindings = 0; + m_num_open_paren = 0; + + try { + scan_core(); + parse_sort(context); + if (!sort_stack().empty()) + return sort_ref(sort_stack().back(), m()); + } + catch (z3_exception & ex) { + error(ex.msg()); + } + return sort_ref(nullptr, m()); + } + + bool operator()() { m_num_bindings = 0; unsigned found_errors = 0; @@ -3190,6 +3207,11 @@ bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive, return p(); } +sort_ref parse_smt2_sort(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps, char const * filename) { + smt2::parser p(ctx, is, interactive, ps, filename); + return p.parse_sort_ref(filename); +} + sexpr_ref parse_sexpr(cmd_context& ctx, std::istream& is, params_ref const& ps, char const* filename) { smt2::parser p(ctx, is, false, ps, filename); return p.parse_sexpr_ref(); diff --git a/src/parsers/smt2/smt2parser.h b/src/parsers/smt2/smt2parser.h index 1b7834c9e..ad8f040b4 100644 --- a/src/parsers/smt2/smt2parser.h +++ b/src/parsers/smt2/smt2parser.h @@ -24,3 +24,4 @@ bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive sexpr_ref parse_sexpr(cmd_context& ctx, std::istream& is, params_ref const& ps, char const* filename); +sort_ref parse_smt2_sort(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps, char const * filename); diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index 31329b3dd..8b855a758 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -47,7 +47,6 @@ namespace mbp { ~imp() {} void insert_mul(expr* x, rational const& v, obj_map& ts) { - // TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << " " << v << "\n";); rational w; if (ts.find(x, w)) ts.insert(x, w + v); @@ -320,6 +319,14 @@ namespace mbp { tids.insert(v, mbo.add_var(r, a.is_int(v))); } } + + // bail on variables in non-linear sub-terms + for (auto& kv : tids) { + expr* e = kv.m_key; + if (is_arith(e) && !var_mark.is_marked(e)) + mark_rec(fmls_mark, e); + } + if (m_check_purified) { for (expr* fml : fmls) mark_rec(fmls_mark, fml); @@ -362,6 +369,10 @@ namespace mbp { optdefs2mbpdef(defs, index2expr, real_vars, result); if (m_apply_projection) apply_projection(result, fmls); + TRACE("qe", + for (auto [v, t] : result) + tout << v << " := " << t << "\n"; + tout << "fmls:" << fmls << "\n";); return result; } diff --git a/src/qe/mbp/mbp_plugin.cpp b/src/qe/mbp/mbp_plugin.cpp index 723ef26fa..7731f803c 100644 --- a/src/qe/mbp/mbp_plugin.cpp +++ b/src/qe/mbp/mbp_plugin.cpp @@ -95,6 +95,97 @@ namespace mbp { lits.push_back(e); } + bool project_plugin::reduce(model_evaluator& eval, model& model, expr* fml, expr_ref_vector& fmls) { + expr* nfml, * f1, * f2, * f3; + expr_ref val(m); + if (m.is_not(fml, nfml) && m.is_distinct(nfml)) + push_back(fmls, pick_equality(m, model, nfml)); + else if (m.is_or(fml)) { + for (expr* arg : *to_app(fml)) { + val = eval(arg); + if (m.is_true(val)) { + fmls.push_back(arg); + break; + } + } + } + else if (m.is_and(fml)) { + fmls.append(to_app(fml)->get_num_args(), to_app(fml)->get_args()); + } + else if (m.is_iff(fml, f1, f2) || (m.is_not(fml, nfml) && m.is_xor(nfml, f1, f2))) { + val = eval(f1); + if (m.is_false(val)) { + push_back(fmls, mk_not(m, f1)); + push_back(fmls, mk_not(m, f2)); + } + else { + push_back(fmls, f1); + push_back(fmls, f2); + } + } + else if (m.is_implies(fml, f1, f2)) { + val = eval(f2); + if (m.is_true(val)) + push_back(fmls, f2); + else + push_back(fmls, mk_not(m, f1)); + } + else if (m.is_ite(fml, f1, f2, f3)) { + val = eval(f1); + if (m.is_true(val)) { + push_back(fmls, f1); + push_back(fmls, f2); + } + else { + push_back(fmls, mk_not(m, f1)); + push_back(fmls, f3); + } + } + else if (m.is_not(fml, nfml) && m.is_not(nfml, nfml)) { + push_back(fmls, nfml); + } + else if (m.is_not(fml, nfml) && m.is_and(nfml)) { + for (expr* arg : *to_app(nfml)) { + val = eval(arg); + if (m.is_false(val)) { + push_back(fmls, mk_not(m, arg)); + break; + } + } + } + else if (m.is_not(fml, nfml) && m.is_or(nfml)) { + for (expr* arg : *to_app(nfml)) + push_back(fmls, mk_not(m, arg)); + } + else if ((m.is_not(fml, nfml) && m.is_iff(nfml, f1, f2)) || m.is_xor(fml, f1, f2)) { + val = eval(f1); + if (m.is_true(val)) + f2 = mk_not(m, f2); + else + f1 = mk_not(m, f1); + push_back(fmls, f1); + push_back(fmls, f2); + } + else if (m.is_not(fml, nfml) && m.is_implies(nfml, f1, f2)) { + push_back(fmls, f1); + push_back(fmls, mk_not(m, f2)); + } + else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) { + val = eval(f1); + if (m.is_true(val)) { + push_back(fmls, f1); + push_back(fmls, mk_not(m, f2)); + } + else { + push_back(fmls, mk_not(m, f1)); + push_back(fmls, mk_not(m, f3)); + } + } + else + return false; + return true; + } + void project_plugin::extract_literals(model& model, app_ref_vector const& vars, expr_ref_vector& fmls) { m_cache.reset(); m_bool_visited.reset(); @@ -105,100 +196,9 @@ namespace mbp { DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n" << model;); SASSERT(!m.is_false(eval(fml))); }); for (unsigned i = 0; i < fmls.size(); ++i) { - expr* fml = fmls.get(i), * nfml, * f1, * f2, * f3; - SASSERT(m.is_bool(fml)); - if (m.is_not(fml, nfml) && m.is_distinct(nfml)) - fmls[i--] = pick_equality(m, model, nfml); - else if (m.is_or(fml)) { - for (expr* arg : *to_app(fml)) { - val = eval(arg); - if (m.is_true(val)) { - fmls[i] = arg; - --i; - break; - } - } - } - else if (m.is_and(fml)) { - fmls.append(to_app(fml)->get_num_args(), to_app(fml)->get_args()); - erase(fmls, i); - } - else if (m.is_iff(fml, f1, f2) || (m.is_not(fml, nfml) && m.is_xor(nfml, f1, f2))) { - val = eval(f1); - if (m.is_false(val)) { - f1 = mk_not(m, f1); - f2 = mk_not(m, f2); - } - fmls[i--] = f1; - push_back(fmls, f2); - } - else if (m.is_implies(fml, f1, f2)) { - val = eval(f2); - if (m.is_true(val)) { - fmls[i] = f2; - } - else { - fmls[i] = mk_not(m, f1); - } - --i; - } - else if (m.is_ite(fml, f1, f2, f3)) { - val = eval(f1); - if (m.is_true(val)) { - push_back(fmls, f1); - push_back(fmls, f2); - } - else { - push_back(fmls, mk_not(m, f1)); - push_back(fmls, f3); - } - erase(fmls, i); - } - else if (m.is_not(fml, nfml) && m.is_not(nfml, nfml)) { - push_back(fmls, nfml); - erase(fmls, i); - } - else if (m.is_not(fml, nfml) && m.is_and(nfml)) { - for (expr* arg : *to_app(nfml)) { - val = eval(arg); - if (m.is_false(val)) { - fmls[i--] = mk_not(m, arg); - break; - } - } - } - else if (m.is_not(fml, nfml) && m.is_or(nfml)) { - for (expr* arg : *to_app(nfml)) - push_back(fmls, mk_not(m, arg)); - erase(fmls, i); - } - else if ((m.is_not(fml, nfml) && m.is_iff(nfml, f1, f2)) || m.is_xor(fml, f1, f2)) { - val = eval(f1); - if (m.is_true(val)) - f2 = mk_not(m, f2); - else - f1 = mk_not(m, f1); - push_back(fmls, f1); - push_back(fmls, f2); - erase(fmls, i); - } - else if (m.is_not(fml, nfml) && m.is_implies(nfml, f1, f2)) { - push_back(fmls, f1); - push_back(fmls, mk_not(m, f2)); - erase(fmls, i); - } - else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) { - val = eval(f1); - if (m.is_true(val)) { - push_back(fmls, f1); - push_back(fmls, mk_not(m, f2)); - } - else { - push_back(fmls, mk_not(m, f1)); - push_back(fmls, mk_not(m, f3)); - } - erase(fmls, i); - } + expr* nfml, * fml = fmls.get(i); + if (reduce(eval, model, fml, fmls)) + erase(fmls, i); else if (m.is_not(fml, nfml)) extract_bools(eval, fmls, i, nfml, false); else diff --git a/src/qe/mbp/mbp_plugin.h b/src/qe/mbp/mbp_plugin.h index 121c7672e..741639aaa 100644 --- a/src/qe/mbp/mbp_plugin.h +++ b/src/qe/mbp/mbp_plugin.h @@ -43,6 +43,7 @@ namespace mbp { expr_mark m_non_ground; expr_ref_vector m_cache, m_args, m_pure_eqs; + bool reduce(model_evaluator& eval, model& model, expr* fml, expr_ref_vector& fmls); void extract_bools(model_evaluator& eval, expr_ref_vector& fmls, unsigned i, expr* fml, bool is_true); void visit_app(expr* e); bool visit_ite(model_evaluator& eval, expr* e, expr_ref_vector& fmls); diff --git a/src/sat/dimacs.cpp b/src/sat/dimacs.cpp index 6800b5c8d..9c9a40a24 100644 --- a/src/sat/dimacs.cpp +++ b/src/sat/dimacs.cpp @@ -165,6 +165,10 @@ namespace dimacs { return out << "f " << r.m_node_id << " " << r.m_name << " " << r.m_args << "0\n"; case drat_record::tag_t::is_bool_def: return out << "b " << r.m_node_id << " " << r.m_args << "0\n"; + case drat_record::tag_t::is_var: + return out << "v " << r.m_node_id << " " << r.m_name << " " << r.m_args << "0\n"; + case drat_record::tag_t::is_quantifier: + return out << "q " << r.m_node_id << " " << r.m_name << " " << r.m_args << "0\n"; } return out; } @@ -256,6 +260,23 @@ namespace dimacs { m_record.m_args.push_back(n); } }; + auto parse_var = [&]() { + ++in; + skip_whitespace(in); + n = parse_int(in, err); + skip_whitespace(in); + m_record.m_name = parse_sexpr(); + m_record.m_tag = drat_record::tag_t::is_var; + m_record.m_node_id = n; + m_record.m_args.reset(); + n = parse_int(in, err); + if (n < 0) + throw lex_error(); + m_record.m_args.push_back(n); + n = parse_int(in, err); + if (n != 0) + throw lex_error(); + }; try { loop: skip_whitespace(in); @@ -290,6 +311,12 @@ namespace dimacs { // parse expression definition parse_ast(drat_record::tag_t::is_node); break; + case 'v': + parse_var(); + break; + case 'q': + parse_ast(drat_record::tag_t::is_quantifier); + break; case 'f': // parse function declaration parse_ast(drat_record::tag_t::is_decl); diff --git a/src/sat/dimacs.h b/src/sat/dimacs.h index eb5fea442..cc4b27182 100644 --- a/src/sat/dimacs.h +++ b/src/sat/dimacs.h @@ -53,7 +53,7 @@ namespace dimacs { }; struct drat_record { - enum class tag_t { is_clause, is_node, is_decl, is_sort, is_bool_def }; + enum class tag_t { is_clause, is_node, is_decl, is_sort, is_bool_def, is_var, is_quantifier }; tag_t m_tag{ tag_t::is_clause }; // a clause populates m_lits and m_status // a node populates m_node_id, m_name, m_args diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 982b6bb9b..6d8c4d477 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -37,9 +37,8 @@ namespace sat { if (s.get_config().m_drat && s.get_config().m_drat_file.is_non_empty_string()) { auto mode = s.get_config().m_drat_binary ? (std::ios_base::binary | std::ios_base::out | std::ios_base::trunc) : std::ios_base::out; m_out = alloc(std::ofstream, s.get_config().m_drat_file.str(), mode); - if (s.get_config().m_drat_binary) { - std::swap(m_out, m_bout); - } + if (s.get_config().m_drat_binary) + std::swap(m_out, m_bout); } } @@ -50,9 +49,8 @@ namespace sat { dealloc(m_bout); for (unsigned i = 0; i < m_proof.size(); ++i) { clause* c = m_proof[i]; - if (c) { - m_alloc.del_clause(c); - } + if (c) + m_alloc.del_clause(c); } m_proof.reset(); m_out = nullptr; @@ -133,7 +131,7 @@ namespace sat { memcpy(buffer + len, d, lastd - d); len += static_cast(lastd - d); buffer[len++] = ' '; - if (len + 50 > sizeof(buffer)) { + if (static_cast(len) + 50 > sizeof(buffer)) { m_out->write(buffer, len); len = 0; } @@ -208,15 +206,14 @@ namespace sat { declare(l); IF_VERBOSE(20, trace(verbose_stream(), 1, &l, st);); - if (st.is_redundant() && st.is_sat()) { + if (st.is_redundant() && st.is_sat()) verify(1, &l); - } - if (st.is_deleted()) { + + if (st.is_deleted()) return; - } - if (m_check_unsat) { - assign_propagate(l); - } + + if (m_check_unsat) + assign_propagate(l); m_units.push_back(l); } @@ -233,9 +230,9 @@ namespace sat { // don't record binary as deleted. } else { - if (st.is_redundant() && st.is_sat()) { + if (st.is_redundant() && st.is_sat()) verify(2, lits); - } + clause* c = m_alloc.mk_clause(2, lits, st.is_redundant()); m_proof.push_back(c); m_status.push_back(st); @@ -245,15 +242,12 @@ namespace sat { m_watches[(~l1).index()].push_back(idx); m_watches[(~l2).index()].push_back(idx); - if (value(l1) == l_false && value(l2) == l_false) { - m_inconsistent = true; - } - else if (value(l1) == l_false) { - assign_propagate(l2); - } - else if (value(l2) == l_false) { - assign_propagate(l1); - } + if (value(l1) == l_false && value(l2) == l_false) + m_inconsistent = true; + else if (value(l1) == l_false) + assign_propagate(l2); + else if (value(l2) == l_false) + assign_propagate(l1); } } @@ -403,16 +397,14 @@ namespace sat { if (n == 0) return false; unsigned num_units = m_units.size(); - for (unsigned i = 0; !m_inconsistent && i < n; ++i) { + for (unsigned i = 0; !m_inconsistent && i < n; ++i) assign_propagate(~c[i]); - } - if (!m_inconsistent) { - DEBUG_CODE(validate_propagation();); - } + + DEBUG_CODE(if (!m_inconsistent) validate_propagation();); DEBUG_CODE( - for (literal u : m_units) { + for (literal u : m_units) SASSERT(m_assignment[u.var()] != l_undef); - }); + ); #if 0 if (!m_inconsistent) { @@ -465,9 +457,9 @@ namespace sat { } #endif - for (unsigned i = num_units; i < m_units.size(); ++i) { + for (unsigned i = num_units; i < m_units.size(); ++i) m_assignment[m_units[i].var()] = l_undef; - } + m_units.shrink(num_units); bool ok = m_inconsistent; m_inconsistent = false; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index faa940869..7a6957467 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -656,6 +656,7 @@ namespace sat { s.propagate_core(false); // must not use propagate(), since s.m_clauses is not in a consistent state. if (s.inconsistent()) return; + m_use_list.reserve(s.num_vars()); unsigned new_trail_sz = s.m_trail.size(); for (unsigned i = old_trail_sz; i < new_trail_sz; i++) { literal l = s.m_trail[i]; diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 0b512275e..a1bd18901 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -40,15 +40,17 @@ namespace sat { class use_list { vector m_use_list; + public: void init(unsigned num_vars); + void reserve(unsigned num_vars) { while (m_use_list.size() <= 2*num_vars) m_use_list.push_back(clause_use_list()); } void insert(clause & c); void block(clause & c); void unblock(clause & c); void erase(clause & c); void erase(clause & c, literal l); - clause_use_list & get(literal l) { return m_use_list[l.index()]; } - clause_use_list const & get(literal l) const { return m_use_list[l.index()]; } + clause_use_list& get(literal l) { return m_use_list[l.index()]; } + clause_use_list const& get(literal l) const { return m_use_list[l.index()]; } void finalize() { m_use_list.finalize(); } std::ostream& display(std::ostream& out, literal l) const { return m_use_list[l.index()].display(out); } }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index d923014c1..3c4569907 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1304,7 +1304,8 @@ namespace sat { flet _searching(m_searching, true); m_clone = nullptr; if (m_mc.empty() && gparams::get_ref().get_bool("model_validate", false)) { - m_clone = alloc(solver, m_params, m_rlimit); + + m_clone = alloc(solver, m_no_drat_params, m_rlimit); m_clone->copy(*this); m_clone->set_extension(nullptr); } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 10e5bd06d..a5d83f273 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -82,6 +82,10 @@ namespace sat { void reset(); void collect_statistics(statistics & st) const; }; + + struct no_drat_params : public params_ref { + no_drat_params() { set_sym("drat.file", symbol()); } + }; class solver : public solver_core { public: @@ -183,6 +187,7 @@ namespace sat { scoped_limit_trail m_vars_lim; stopwatch m_stopwatch; params_ref m_params; + no_drat_params m_no_drat_params; scoped_ptr m_clone; // for debugging purposes literal_vector m_assumptions; // additional assumptions during check literal_set m_assumption_set; // set of enabled assumptions diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index 129026b34..2e8a0603d 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -427,9 +427,11 @@ namespace array { app_ref sel1(m), sel2(m); sel1 = a.mk_select(args1); sel2 = a.mk_select(args2); + prop |= !ctx.get_enode(sel1) || !ctx.get_enode(sel2); if (ctx.propagate(e_internalize(sel1), e_internalize(sel2), array_axiom())) prop = true; } + prop |= !ctx.get_enode(def1) || !ctx.get_enode(def2); if (ctx.propagate(e_internalize(def1), e_internalize(def2), array_axiom())) prop = true; return prop; @@ -538,7 +540,7 @@ namespace array { for (euf::enode* p : euf::enode_parents(n)) has_default |= a.is_default(p->get_expr()); if (has_default) - propagate_parent_default(v); + propagate_parent_default(v); } bool change = false; unsigned sz = m_axiom_trail.size(); diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index 9d5476e31..55496a729 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -177,6 +177,8 @@ namespace array { auto set_index = [&](euf::enode* arg) { if (arg->get_root() == r) is_index = true; }; auto set_value = [&](euf::enode* arg) { if (arg->get_root() == r) is_value = true; }; + if (a.is_ext(n->get_expr())) + return true; for (euf::enode* parent : euf::enode_parents(r)) { app* p = parent->get_app(); unsigned num_args = parent->num_args(); @@ -193,7 +195,7 @@ namespace array { } else if (a.is_const(p)) { set_value(parent->get_arg(0)); - } + } if (is_array + is_index + is_value > 1) return true; } diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp index 964f6902d..b4e7d3cab 100644 --- a/src/sat/smt/array_model.cpp +++ b/src/sat/smt/array_model.cpp @@ -26,8 +26,8 @@ namespace array { if (!a.is_array(n->get_expr())) { dep.insert(n, nullptr); return true; - } - for (euf::enode* p : euf::enode_parents(n)) { + } + for (euf::enode* p : euf::enode_parents(n->get_root())) { if (a.is_default(p->get_expr())) { dep.add(n, p); continue; @@ -51,6 +51,7 @@ namespace array { SASSERT(a.is_array(n->get_expr())); ptr_vector args; sort* srt = n->get_sort(); + n = n->get_root(); unsigned arity = get_array_arity(srt); func_decl * f = mk_aux_decl_for_array_sort(m, srt); func_interp * fi = alloc(func_interp, m, arity); @@ -70,7 +71,7 @@ namespace array { expr* else_value = nullptr; unsigned max_occ_num = 0; obj_map num_occ; - for (euf::enode* p : euf::enode_parents(n)) { + for (euf::enode* p : euf::enode_parents(n->get_root())) { if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n->get_root()) { expr* v = values.get(p->get_root_id()); if (!v) @@ -90,7 +91,7 @@ namespace array { } for (euf::enode* p : euf::enode_parents(n)) { - if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n->get_root()) { + if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n) { expr* value = values.get(p->get_root_id()); if (!value || value == fi->get_else()) continue; @@ -102,7 +103,7 @@ namespace array { } parameter p(f); - values.set(n->get_root_id(), m.mk_app(get_id(), OP_AS_ARRAY, 1, &p)); + values.set(n->get_expr_id(), m.mk_app(get_id(), OP_AS_ARRAY, 1, &p)); } diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp index 4e6f75c4d..b56f4efb1 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -174,8 +174,10 @@ namespace array { ctx.push_vec(get_var_data(v_child).m_parent_selects, select); euf::enode* child = var2enode(v_child); TRACE("array", tout << "v" << v_child << " - " << ctx.bpp(select) << " " << ctx.bpp(child) << " prop: " << should_prop_upward(get_var_data(v_child)) << "\n";); + TRACE("array", tout << "can beta reduce " << can_beta_reduce(child) << "\n";); if (can_beta_reduce(child)) push_axiom(select_axiom(select, child)); + propagate_parent_select_axioms(v_child); } void solver::add_lambda(theory_var v, euf::enode* lambda) { @@ -226,6 +228,12 @@ namespace array { auto& d = get_var_data(v); + for (euf::enode* lambda : d.m_lambdas) { + expr* e = lambda->get_expr(); + if (a.is_const(e) || a.is_map(e)) + propagate_select_axioms(d, lambda); + } + for (euf::enode* lambda : d.m_parent_lambdas) propagate_select_axioms(d, lambda); } diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index e3c193f5a..e8e4305d0 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -653,9 +653,8 @@ namespace bv { if (!argn->is_attached_to(get_id())) { mk_var(argn); } - theory_var v_arg = argn->get_th_var(get_id()); - unsigned arg_sz = get_bv_size(v_arg); - SASSERT(idx < arg_sz); + theory_var v_arg = argn->get_th_var(get_id()); + SASSERT(idx < get_bv_size(v_arg)); sat::literal lit = expr2literal(n); sat::literal lit0 = m_bits[v_arg][idx]; if (lit0 == sat::null_literal) { diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index 4df92596e..d030394a8 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -478,6 +478,9 @@ namespace bv { if (!assign_bit(bit2, v1, v2, idx, bit1, false)) break; } + if (s().value(m_bits[v1][m_wpos[v1]]) != l_undef) + find_wpos(v1); + return num_assigned > 0; } diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index 07c269d48..76c154a4a 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -714,6 +714,7 @@ namespace dt { if (v == euf::null_theory_var) return false; euf::enode* con = m_var_data[m_find.find(v)]->m_constructor; + CTRACE("dt", !con, display(tout) << ctx.bpp(n) << "\n";); if (con->num_args() == 0) dep.insert(n, nullptr); for (enode* arg : euf::enode_args(con)) diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index a7476bc5d..020d29baa 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -34,7 +34,11 @@ namespace euf { sat::literal solver::mk_literal(expr* e) { expr_ref _e(e, m); - return internalize(e, false, false, m_is_redundant); + bool is_not = m.is_not(e, e); + sat::literal lit = internalize(e, false, false, m_is_redundant); + if (is_not) + lit.neg(); + return lit; } sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { @@ -129,8 +133,7 @@ namespace euf { sat::literal solver::attach_lit(literal lit, expr* e) { sat::bool_var v = lit.var(); s().set_external(v); - s().set_eliminated(v, false); - + s().set_eliminated(v, false); if (lit.sign()) { v = si.add_bool_var(e); @@ -281,17 +284,11 @@ namespace euf { s().add_clause(1, &lit_th, st); } else { - sat::bool_var v = si.to_bool_var(c); - s().set_external(v); - VERIFY(v != sat::null_bool_var); - VERIFY(s().is_external(v)); - SASSERT(v != sat::null_bool_var); - VERIFY(!s().was_eliminated(v)); + sat::literal lit_c = mk_literal(c); expr_ref eq_el = mk_eq(e, el); - sat::literal lit_el = mk_literal(eq_el); - literal lits1[2] = { literal(v, true), lit_th }; - literal lits2[2] = { literal(v, false), lit_el }; + literal lits1[2] = { ~lit_c, lit_th }; + literal lits2[2] = { lit_c, lit_el }; s().add_clause(2, lits1, st); s().add_clause(2, lits2, st); } diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index 5ac8e7caa..d2fa19eee 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -61,6 +61,7 @@ namespace euf { }; void solver::update_model(model_ref& mdl) { + mdl->reset_eval_cache(); for (auto* mb : m_solvers) mb->init_model(); m_values.reset(); @@ -178,6 +179,10 @@ namespace euf { mbS->add_value(n, *mdl, m_values); else if (auto* mbE = expr2solver(e)) mbE->add_value(n, *mdl, m_values); + else if (is_app(e) && to_app(e)->get_family_id() != m.get_basic_family_id()) { + m_values.set(id, e); + IF_VERBOSE(1, verbose_stream() << "creating self-value for " << mk_pp(e, m) << "\n"); + } else { IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n"); } @@ -212,9 +217,10 @@ namespace euf { args.reset(); for (expr* arg : *a) { enode* earg = get_enode(arg); - args.push_back(m_values.get(earg->get_root_id())); - CTRACE("euf", !args.back(), tout << "no value for " << bpp(earg) << "\n";); - SASSERT(args.back()); + expr* val = m_values.get(earg->get_root_id()); + args.push_back(val); + CTRACE("euf", !val, tout << "no value for " << bpp(earg) << "\n";); + SASSERT(val); } SASSERT(args.size() == arity); if (!fi->get_entry(args.data())) @@ -278,6 +284,7 @@ namespace euf { tout << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n"; s().display(tout); tout << mdl << "\n";); + (void)first; first = false; } diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp index 42fc8ccde..9335e283f 100644 --- a/src/sat/smt/euf_proof.cpp +++ b/src/sat/smt/euf_proof.cpp @@ -33,20 +33,32 @@ namespace euf { drat_log_decl(a->get_decl()); std::stringstream strm; strm << mk_ismt2_func(a->get_decl(), m); - if (a->get_num_parameters() == 0) - get_drat().def_begin('e', e->get_id(), strm.str()); - else { - get_drat().def_begin('e', e->get_id(), strm.str()); - } + get_drat().def_begin('e', e->get_id(), strm.str()); for (expr* arg : *a) get_drat().def_add_arg(arg->get_id()); get_drat().def_end(); - m_drat_asts.insert(e); - push(insert_obj_trail(m_drat_asts, e)); } - else { - IF_VERBOSE(0, verbose_stream() << "logging binders is TBD\n"); + else if (is_var(e)) { + var* v = to_var(e); + get_drat().def_begin('v', v->get_id(), "" + mk_pp(e->get_sort(), m)); + get_drat().def_add_arg(v->get_idx()); + get_drat().def_end(); } + else if (is_quantifier(e)) { + quantifier* q = to_quantifier(e); + std::stringstream strm; + strm << "(" << (is_forall(q) ? "forall" : (is_exists(q) ? "exists" : "lambda")); + for (unsigned i = 0; i < q->get_num_decls(); ++i) + strm << " (" << q->get_decl_name(i) << " " << mk_pp(q->get_decl_sort(i), m) << ")"; + strm << ")"; + get_drat().def_begin('q', q->get_id(), strm.str()); + get_drat().def_add_arg(q->get_expr()->get_id()); + get_drat().def_end(); + } + else + UNREACHABLE(); + m_drat_asts.insert(e); + push(insert_obj_trail(m_drat_asts, e)); } void solver::drat_log_expr(expr* e) { @@ -61,9 +73,15 @@ namespace euf { for (expr* arg : *to_app(e)) if (!m_drat_asts.contains(arg)) m_drat_todo.push_back(arg); + if (is_quantifier(e)) { + expr* arg = to_quantifier(e)->get_expr(); + if (!m_drat_asts.contains(arg)) + m_drat_todo.push_back(arg); + } if (m_drat_todo.size() != sz) continue; - drat_log_expr1(e); + if (!m_drat_asts.contains(e)) + drat_log_expr1(e); m_drat_todo.pop_back(); } } @@ -154,6 +172,8 @@ namespace euf { void solver::drat_eq_def(literal lit, expr* eq) { expr *a = nullptr, *b = nullptr; VERIFY(m.is_eq(eq, a, b)); + drat_log_expr(a); + drat_log_expr(b); get_drat().def_begin('e', eq->get_id(), std::string("=")); get_drat().def_add_arg(a->get_id()); get_drat().def_add_arg(b->get_id()); diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp index f5c05cea9..28ac99d9a 100644 --- a/src/sat/smt/euf_relevancy.cpp +++ b/src/sat/smt/euf_relevancy.cpp @@ -38,12 +38,22 @@ namespace euf { } } + /** + * Add a root clause. Root clauses must all be satisfied by the + * final assignment. If a clause is added above search level it + * is subject to removal on backtracking. These clauses are therefore + * not tracked. + */ void solver::add_root(unsigned n, sat::literal const* lits) { + if (!relevancy_enabled()) + return; ensure_dual_solver(); m_dual_solver->add_root(n, lits); } void solver::add_aux(unsigned n, sat::literal const* lits) { + if (!relevancy_enabled()) + return; ensure_dual_solver(); m_dual_solver->add_aux(n, lits); } diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index f66c4a331..3e1620090 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -211,7 +211,7 @@ namespace euf { for (sat::literal lit : r) if (s().lvl(lit) > 0) r[j++] = lit; r.shrink(j); - TRACE("euf", tout << "eplain " << l << " <- " << r << " " << probing << "\n";); + TRACE("euf", tout << "explain " << l << " <- " << r << " " << probing << "\n";); DEBUG_CODE(for (auto lit : r) SASSERT(s().value(lit) == l_true);); if (!probing) @@ -236,7 +236,7 @@ namespace euf { sat::bool_var v = get_egraph().explain_diseq(m_explain, a, b); SASSERT(v == sat::null_bool_var || s().value(v) == l_false); if (v != sat::null_bool_var) - m_explain.push_back(to_ptr(sat::literal(v, false))); + m_explain.push_back(to_ptr(sat::literal(v, true))); } bool solver::propagate(enode* a, enode* b, ext_justification_idx idx) { @@ -286,13 +286,13 @@ namespace euf { void solver::asserted(literal l) { expr* e = m_bool_var2expr.get(l.var(), nullptr); - TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";); + TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";); if (!e) - return; + return; euf::enode* n = m_egraph.find(e); if (!n) return; - bool sign = l.sign(); + bool sign = l.sign(); m_egraph.set_value(n, sign ? l_false : l_true); for (auto th : enode_th_vars(n)) m_id2solver[th.get_id()]->asserted(l); @@ -302,20 +302,25 @@ namespace euf { SASSERT(l == get_literal(c)); if (n->value_conflict()) { euf::enode* nb = sign ? mk_false() : mk_true(); + euf::enode* r = n->get_root(); + euf::enode* rb = sign ? mk_true() : mk_false(); + sat::literal rl(r->bool_var(), r->value() == l_false); m_egraph.merge(n, nb, c); + m_egraph.merge(r, rb, to_ptr(rl)); + SASSERT(m_egraph.inconsistent()); + return; } - else if (!sign && n->is_equality()) { - SASSERT(!m.is_iff(e)); - euf::enode* na = n->get_arg(0); - euf::enode* nb = n->get_arg(1); - m_egraph.merge(na, nb, c); - } - else if (n->merge_tf()) { + if (n->merge_tf()) { euf::enode* nb = sign ? mk_false() : mk_true(); m_egraph.merge(n, nb, c); } - else if (sign && n->is_equality()) - m_egraph.new_diseq(n); + if (n->is_equality()) { + SASSERT(!m.is_iff(e)); + if (sign) + m_egraph.new_diseq(n); + else + m_egraph.merge(n->get_arg(0), n->get_arg(1), c); + } } @@ -342,21 +347,19 @@ namespace euf { break; propagated = true; } - DEBUG_CODE(if (!s().inconsistent()) check_missing_eq_propagation();); + DEBUG_CODE(if (!propagated && !s().inconsistent()) check_missing_eq_propagation();); return propagated; } void solver::propagate_literals() { for (; m_egraph.has_literal() && !s().inconsistent() && !m_egraph.inconsistent(); m_egraph.next_literal()) { - euf::enode_bool_pair p = m_egraph.get_literal(); - euf::enode* n = p.first; - bool is_eq = p.second; + auto [n, is_eq] = m_egraph.get_literal(); expr* e = n->get_expr(); expr* a = nullptr, *b = nullptr; bool_var v = n->bool_var(); SASSERT(m.is_bool(e)); size_t cnstr; - literal lit; + literal lit; if (is_eq) { VERIFY(m.is_eq(e, a, b)); cnstr = eq_constraint().to_index(); @@ -364,6 +367,10 @@ namespace euf { } else { lbool val = n->get_root()->value(); + if (val == l_undef && m.is_false(n->get_root()->get_expr())) + val = l_false; + if (val == l_undef && m.is_true(n->get_root()->get_expr())) + val = l_true; a = e; b = (val == l_true) ? m.mk_true() : m.mk_false(); SASSERT(val != l_undef); @@ -449,8 +456,8 @@ namespace euf { if (!init_relevancy()) give_up = true; - - + + unsigned num_nodes = m_egraph.num_nodes(); for (auto* e : m_solvers) { if (!m.inc()) return sat::check_result::CR_GIVEUP; @@ -468,6 +475,10 @@ namespace euf { return sat::check_result::CR_CONTINUE; if (give_up) return sat::check_result::CR_GIVEUP; + if (num_nodes < m_egraph.num_nodes()) { + IF_VERBOSE(1, verbose_stream() << "new nodes created, but not detected\n"); + return sat::check_result::CR_CONTINUE; + } if (m_qsolver) return m_qsolver->check(); TRACE("after_search", s().display(tout);); @@ -483,6 +494,8 @@ namespace euf { for (auto* e : m_solvers) e->push(); m_egraph.push(); + if (m_dual_solver) + m_dual_solver->push(); } void solver::pop(unsigned n) { @@ -500,20 +513,18 @@ namespace euf { } m_var_trail.shrink(sc.m_var_lim); m_scopes.shrink(m_scopes.size() - n); + if (m_dual_solver) + m_dual_solver->pop(n); SASSERT(m_egraph.num_scopes() == m_scopes.size()); TRACE("euf_verbose", display(tout << "pop to: " << m_scopes.size() << "\n");); } void solver::user_push() { - push(); - if (m_dual_solver) - m_dual_solver->push(); + push(); } void solver::user_pop(unsigned n) { pop(n); - if (m_dual_solver) - m_dual_solver->pop(n); } void solver::start_reinit(unsigned n) { @@ -547,14 +558,11 @@ namespace euf { scoped_set_replay replay(*this); scoped_suspend_rlimit suspend_rlimit(m.limit()); - for (auto const& t : m_reinit) - replay.m.insert(std::get<0>(t), std::get<2>(t)); - + for (auto const& [e, generation, v] : m_reinit) + replay.m.insert(e, v); + TRACE("euf", for (auto const& kv : replay.m) tout << kv.m_value << "\n";); - for (auto const& t : m_reinit) { - expr_ref e = std::get<0>(t); - unsigned generation = std::get<1>(t); - sat::bool_var v = std::get<2>(t); + for (auto const& [e, generation, v] : m_reinit) { scoped_generation _sg(*this, generation); TRACE("euf", tout << "replay: " << v << " " << mk_bounded_pp(e, m) << "\n";); sat::literal lit; @@ -565,9 +573,112 @@ namespace euf { VERIFY(lit.var() == v); attach_lit(lit, e); } + + if (relevancy_enabled()) + for (auto const& [e, generation, v] : m_reinit) + if (si.is_bool_op(e)) + relevancy_reinit(e); TRACE("euf", display(tout << "replay done\n");); } + /** + * Boolean structure needs to be replayed for relevancy tracking. + * Main cases for replaying Boolean functions are included. When a replay + * is not supported, we just disable relevancy. + */ + void solver::relevancy_reinit(expr* e) { + TRACE("euf", tout << "internalize again " << mk_pp(e, m) << "\n";); + if (to_app(e)->get_family_id() != m.get_basic_family_id()) { + disable_relevancy(e); + return; + } + auto lit = si.internalize(e, true); + switch (to_app(e)->get_decl_kind()) { + case OP_NOT: { + auto lit2 = si.internalize(to_app(e)->get_arg(0), true); + add_aux(lit, lit2); + add_aux(~lit, ~lit2); + break; + } + case OP_EQ: { + if (to_app(e)->get_num_args() != 2) { + disable_relevancy(e); + return; + } + auto lit1 = si.internalize(to_app(e)->get_arg(0), true); + auto lit2 = si.internalize(to_app(e)->get_arg(1), true); + add_aux(~lit, ~lit1, lit2); + add_aux(~lit, lit1, ~lit2); + add_aux(lit, lit1, lit2); + add_aux(lit, ~lit1, ~lit2); + break; + } + case OP_OR: { + sat::literal_vector lits; + for (expr* arg : *to_app(e)) + lits.push_back(si.internalize(arg, true)); + for (auto lit2 : lits) + add_aux(~lit2, lit); + lits.push_back(~lit); + add_aux(lits); + break; + } + case OP_AND: { + sat::literal_vector lits; + for (expr* arg : *to_app(e)) + lits.push_back(~si.internalize(arg, true)); + for (auto nlit2 : lits) + add_aux(~lit, ~nlit2); + lits.push_back(lit); + add_aux(lits); + break; + } + case OP_TRUE: + add_root(lit); + break; + case OP_FALSE: + add_root(~lit); + break; + case OP_ITE: { + auto lit1 = si.internalize(to_app(e)->get_arg(0), true); + auto lit2 = si.internalize(to_app(e)->get_arg(1), true); + auto lit3 = si.internalize(to_app(e)->get_arg(2), true); + add_aux(~lit, ~lit1, lit2); + add_aux(~lit, lit1, lit3); + add_aux(lit, ~lit1, ~lit2); + add_aux(lit, lit1, ~lit3); + break; + } + case OP_XOR: { + if (to_app(e)->get_num_args() != 2) { + disable_relevancy(e); + break; + } + auto lit1 = si.internalize(to_app(e)->get_arg(0), true); + auto lit2 = si.internalize(to_app(e)->get_arg(1), true); + add_aux(lit, ~lit1, lit2); + add_aux(lit, lit1, ~lit2); + add_aux(~lit, lit1, lit2); + add_aux(~lit, ~lit1, ~lit2); + break; + } + case OP_IMPLIES: { + if (to_app(e)->get_num_args() != 2) { + disable_relevancy(e); + break; + } + auto lit1 = si.internalize(to_app(e)->get_arg(0), true); + auto lit2 = si.internalize(to_app(e)->get_arg(1), true); + add_aux(~lit, ~lit1, lit2); + add_aux(lit, lit1); + add_aux(lit, ~lit2); + break; + } + default: + UNREACHABLE(); + } + } + void solver::pre_simplify() { for (auto* e : m_solvers) e->pre_simplify(); diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 73c44649c..e8e707897 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -96,27 +96,27 @@ namespace euf { stats m_stats; th_rewriter m_rewriter; func_decl_ref_vector m_unhandled_functions; - sat::lookahead* m_lookahead{ nullptr }; + sat::lookahead* m_lookahead = nullptr; ast_manager* m_to_m; sat::sat_internalizer* m_to_si; scoped_ptr m_ackerman; scoped_ptr m_dual_solver; - user::solver* m_user_propagator{ nullptr }; - th_solver* m_qsolver { nullptr }; - unsigned m_generation { 0 }; + user::solver* m_user_propagator = nullptr; + th_solver* m_qsolver = nullptr; + unsigned m_generation = 0; mutable ptr_vector m_todo; ptr_vector m_bool_var2expr; ptr_vector m_explain; - unsigned m_num_scopes{ 0 }; + unsigned m_num_scopes = 0; unsigned_vector m_var_trail; svector m_scopes; scoped_ptr_vector m_solvers; ptr_vector m_id2solver; - constraint* m_conflict{ nullptr }; - constraint* m_eq{ nullptr }; - constraint* m_lit{ nullptr }; + constraint* m_conflict = nullptr; + constraint* m_eq = nullptr; + constraint* m_lit = nullptr; // internalization bool visit(expr* e) override; @@ -134,8 +134,9 @@ namespace euf { typedef std::tuple reinit_t; vector m_reinit; - void start_reinit(unsigned num_scopes); + void start_reinit(unsigned num_scopes); void finish_reinit(); + void relevancy_reinit(expr* e); // extensions th_solver* get_solver(family_id fid, func_decl* f); @@ -356,13 +357,17 @@ namespace euf { bool is_shared(euf::enode* n) const; // relevancy - bool relevancy_enabled() const { return get_config().m_relevancy_lvl > 0; } + bool m_relevancy = true; + bool relevancy_enabled() const { return m_relevancy && get_config().m_relevancy_lvl > 0; } + void disable_relevancy(expr* e) { IF_VERBOSE(0, verbose_stream() << "disabling relevancy " << mk_pp(e, m) << "\n"); m_relevancy = false; } void add_root(unsigned n, sat::literal const* lits); void add_root(sat::literal_vector const& lits) { add_root(lits.size(), lits.data()); } void add_root(sat::literal lit) { add_root(1, &lit); } void add_root(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_root(2, lits); } + void add_aux(sat::literal_vector const& lits) { add_aux(lits.size(), lits.data()); } void add_aux(unsigned n, sat::literal const* lits); void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); } + void add_aux(sat::literal a, sat::literal b, sat::literal c) { sat::literal lits[3] = { a, b, c }; add_aux(3, lits); } void track_relevancy(sat::bool_var v); bool is_relevant(expr* e) const; bool is_relevant(enode* n) const; diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp index ef2fd731c..590929a91 100644 --- a/src/sat/smt/fpa_solver.cpp +++ b/src/sat/smt/fpa_solver.cpp @@ -15,6 +15,8 @@ Author: Revision History: + Ported from theory_fpa by nbjorner in 2020. + --*/ #include "sat/smt/fpa_solver.h" @@ -91,7 +93,10 @@ namespace fpa { SASSERT(m.is_bool(e)); if (!visit_rec(m, e, sign, root, redundant)) return sat::null_literal; - return expr2literal(e); + sat::literal lit = expr2literal(e); + if (sign) + lit.neg(); + return lit; } void solver::internalize(expr* e, bool redundant) { @@ -116,12 +121,11 @@ namespace fpa { bool solver::post_visit(expr* e, bool sign, bool root) { euf::enode* n = expr2enode(e); - app* a = to_app(e); SASSERT(!n || !n->is_attached_to(get_id())); if (!n) n = mk_enode(e, false); SASSERT(!n->is_attached_to(get_id())); - mk_var(n); + attach_new_th_var(n); TRACE("fp", tout << "post: " << mk_bounded_pp(e, m) << "\n";); m_nodes.push_back(std::tuple(n, sign, root)); ctx.push(push_back_trail(m_nodes)); @@ -310,7 +314,9 @@ namespace fpa { if (!wrapped) wrapped = m_converter.wrap(e); return expr2enode(wrapped) != nullptr; }; - if (m_fpa_util.is_fp(e)) { + if (m_fpa_util.is_rm_numeral(e) || m_fpa_util.is_numeral(e)) + value = e; + else if (m_fpa_util.is_fp(e)) { SASSERT(n->num_args() == 3); expr* a = values.get(n->get_arg(0)->get_root_id()); expr* b = values.get(n->get_arg(1)->get_root_id()); diff --git a/src/sat/smt/q_clause.cpp b/src/sat/smt/q_clause.cpp index 7c8a260e5..097a61a14 100644 --- a/src/sat/smt/q_clause.cpp +++ b/src/sat/smt/q_clause.cpp @@ -23,9 +23,9 @@ namespace q { std::ostream& lit::display(std::ostream& out) const { ast_manager& m = lhs.m(); if (m.is_true(rhs) && !sign) - return out << mk_bounded_pp(lhs, m, 2); + return out << lhs; if (m.is_false(rhs) && !sign) - return out << "(not " << mk_bounded_pp(lhs, m, 2) << ")"; + return out << "(not " << lhs << ")"; return out << mk_bounded_pp(lhs, m, 2) << (sign ? " != " : " == ") @@ -43,13 +43,13 @@ namespace q { for (auto const& lit : m_lits) lit.display(out) << "\n"; binding* b = m_bindings; - if (b) { - do { - b->display(ctx, num_decls(), out) << "\n"; - b = b->next(); - } - while (b != m_bindings); - } + if (!b) + return out; + do { + b->display(ctx, num_decls(), out) << "\n"; + b = b->next(); + } + while (b != m_bindings); return out; } diff --git a/src/sat/smt/q_clause.h b/src/sat/smt/q_clause.h index 7278d1db1..66daf07ea 100644 --- a/src/sat/smt/q_clause.h +++ b/src/sat/smt/q_clause.h @@ -29,7 +29,9 @@ namespace q { expr_ref rhs; bool sign; lit(expr_ref const& lhs, expr_ref const& rhs, bool sign): - lhs(lhs), rhs(rhs), sign(sign) {} + lhs(lhs), rhs(rhs), sign(sign) { + SASSERT(!rhs.m().is_false(rhs) || !sign); + } std::ostream& display(std::ostream& out) const; }; @@ -57,10 +59,12 @@ namespace q { unsigned m_index; vector m_lits; quantifier_ref m_q; - sat::literal m_literal; + unsigned m_watch = 0; + sat::literal m_literal = sat::null_literal; q::quantifier_stat* m_stat = nullptr; binding* m_bindings = nullptr; + clause(ast_manager& m, unsigned idx): m_index(idx), m_q(m) {} std::ostream& display(euf::solver& ctx, std::ostream& out) const; @@ -75,10 +79,12 @@ namespace q { struct justification { expr* m_lhs, *m_rhs; bool m_sign; + unsigned m_num_ev; + euf::enode_pair* m_evidence; clause& m_clause; euf::enode* const* m_binding; - justification(lit const& l, clause& c, euf::enode* const* b): - m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_clause(c), m_binding(b) {} + justification(lit const& l, clause& c, euf::enode* const* b, unsigned n, euf::enode_pair* ev): + m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_num_ev(n), m_evidence(ev), m_clause(c), m_binding(b) {} sat::ext_constraint_idx to_index() const { return sat::constraint_base::mem2base(this); } diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index e997476ed..c83680f72 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -94,7 +94,10 @@ namespace q { lit lit(expr_ref(l, m), expr_ref(r, m), sign); if (idx != UINT_MAX) lit = c[idx]; - auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(lit, c, b); + auto* ev = static_cast(ctx.get_region().allocate(sizeof(euf::enode_pair) * m_evidence.size())); + for (unsigned i = m_evidence.size(); i-- > 0; ) + ev[i] = m_evidence[i]; + auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(lit, c, b, m_evidence.size(), ev); return constraint->to_index(); } @@ -251,7 +254,8 @@ namespace q { bool ematch::propagate(bool is_owned, euf::enode* const* binding, unsigned max_generation, clause& c, bool& propagated) { TRACE("q", c.display(ctx, tout) << "\n";); unsigned idx = UINT_MAX; - lbool ev = m_eval(binding, c, idx); + m_evidence.reset(); + lbool ev = m_eval(binding, c, idx, m_evidence); if (ev == l_true) { ++m_stats.m_num_redundant; return true; @@ -267,17 +271,39 @@ namespace q { if (ev == l_undef && max_generation > m_generation_propagation_threshold) return false; if (!is_owned) - binding = alloc_binding(c, binding); - auto j_idx = mk_justification(idx, c, binding); - if (ev == l_false) { + binding = alloc_binding(c, binding); + + auto j_idx = mk_justification(idx, c, binding); + + if (is_owned) + propagate(ev == l_false, idx, j_idx); + else + m_prop_queue.push_back(prop(ev == l_false, idx, j_idx)); + propagated = true; + return true; + } + + void ematch::propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx) { + if (is_conflict) { ++m_stats.m_num_conflicts; ctx.set_conflict(j_idx); } else { ++m_stats.m_num_propagations; - ctx.propagate(instantiate(c, binding, c[idx]), j_idx); + auto& j = justification::from_index(j_idx); + auto lit = instantiate(j.m_clause, j.m_binding, j.m_clause[idx]); + ctx.propagate(lit, j_idx); } - propagated = true; + } + + bool ematch::flush_prop_queue() { + if (m_prop_queue.empty()) + return false; + for (unsigned i = 0; i < m_prop_queue.size(); ++i) { + auto [is_conflict, idx, j_idx] = m_prop_queue[i]; + propagate(is_conflict, idx, j_idx); + } + m_prop_queue.reset(); return true; } @@ -295,6 +321,7 @@ namespace q { } void ematch::add_instantiation(clause& c, binding& b, sat::literal lit) { + m_evidence.reset(); ctx.propagate(lit, mk_justification(UINT_MAX, c, b.nodes())); } @@ -411,6 +438,16 @@ namespace q { r = sign ? m.mk_false() : m.mk_true(); sign = false; } + if (m.is_true(l) || m.is_false(l)) + std::swap(l, r); + if (sign && m.is_false(r)) { + r = m.mk_true(); + sign = false; + } + else if (sign && m.is_true(r)) { + r = m.mk_false(); + sign = false; + } cl->m_lits.push_back(lit(expr_ref(l, m), expr_ref(r, m), sign)); } if (q->get_num_patterns() == 0) { @@ -490,7 +527,7 @@ namespace q { bool ematch::propagate(bool flush) { m_mam->propagate(); - bool propagated = false; + bool propagated = flush_prop_queue(); if (m_qhead >= m_clause_queue.size()) return m_inst_queue.propagate(); ctx.push(value_trail(m_qhead)); diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h index 443b9d947..9c4cf9d98 100644 --- a/src/sat/smt/q_ematch.h +++ b/src/sat/smt/q_ematch.h @@ -49,6 +49,13 @@ namespace q { } }; + struct prop { + bool is_conflict; + unsigned idx; + sat::ext_justification_idx j; + prop(bool is_conflict, unsigned idx, sat::ext_justification_idx j) : is_conflict(is_conflict), idx(idx), j(j) {} + }; + struct remove_binding; struct insert_binding; struct pop_clause; @@ -63,8 +70,9 @@ namespace q { quantifier_stat_gen m_qstat_gen; fingerprints m_fingerprints; scoped_ptr m_tmp_binding; - unsigned m_tmp_binding_capacity { 0 }; + unsigned m_tmp_binding_capacity = 0; queue m_inst_queue; + svector m_prop_queue; pattern_inference_rw m_infer_patterns; scoped_ptr m_mam, m_lazy_mam; ptr_vector m_clauses; @@ -72,13 +80,14 @@ namespace q { vector m_watch; // expr_id -> clause-index* stats m_stats; expr_fast_mark1 m_mark; - unsigned m_generation_propagation_threshold{ 3 }; + unsigned m_generation_propagation_threshold = 3; ptr_vector m_ground; - bool m_in_queue_set{ false }; + bool m_in_queue_set = false; nat_set m_node_in_queue; nat_set m_clause_in_queue; - unsigned m_qhead { 0 }; + unsigned m_qhead = 0; unsigned_vector m_clause_queue; + euf::enode_pair_vector m_evidence; binding* alloc_binding(unsigned n, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top); euf::enode* const* alloc_binding(clause& c, euf::enode* const* _binding); @@ -107,6 +116,9 @@ namespace q { fingerprint* add_fingerprint(clause& c, binding& b, unsigned max_generation); void set_tmp_binding(fingerprint& fp); + bool flush_prop_queue(); + void propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx); + public: ematch(euf::solver& ctx, solver& s); @@ -115,7 +127,7 @@ namespace q { bool propagate(bool flush); - void init_search(); + // void init_search(); void add(quantifier* q); @@ -127,7 +139,7 @@ namespace q { void on_binding(quantifier* q, app* pat, euf::enode* const* binding, unsigned max_generation, unsigned min_gen, unsigned max_gen); // callbacks from queue - lbool evaluate(euf::enode* const* binding, clause& c) { return m_eval(binding, c); } + lbool evaluate(euf::enode* const* binding, clause& c) { m_evidence.reset(); return m_eval(binding, c, m_evidence); } void add_instantiation(clause& c, binding& b, sat::literal lit); diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp index 5e5cc83b8..e341979de 100644 --- a/src/sat/smt/q_eval.cpp +++ b/src/sat/smt/q_eval.cpp @@ -15,6 +15,7 @@ Author: --*/ +#include "ast/has_free_vars.h" #include "sat/smt/q_eval.h" #include "sat/smt/euf_solver.h" #include "sat/smt/q_solver.h" @@ -32,89 +33,96 @@ namespace q { m(ctx.get_manager()) {} - lbool eval::operator()(euf::enode* const* binding, clause& c, unsigned& idx) { + lbool eval::operator()(euf::enode* const* binding, clause& c, unsigned& idx, euf::enode_pair_vector& evidence) { scoped_mark_reset _sr(*this); idx = UINT_MAX; unsigned sz = c.m_lits.size(); unsigned n = c.num_decls(); m_indirect_nodes.reset(); - for (unsigned i = 0; i < sz; ++i) { + for (unsigned j = 0; j < sz; ++j) { + unsigned i = (j + c.m_watch) % sz; unsigned lim = m_indirect_nodes.size(); lit l = c[i]; - lbool cmp = compare(n, binding, l.lhs, l.rhs); + lbool cmp = compare(n, binding, l.lhs, l.rhs, evidence); switch (cmp) { case l_false: m_indirect_nodes.shrink(lim); if (!l.sign) break; - if (i > 0) - std::swap(c[0], c[i]); + c.m_watch = i; return l_true; case l_true: m_indirect_nodes.shrink(lim); if (l.sign) break; - if (i > 0) - std::swap(c[0], c[i]); + c.m_watch = i; return l_true; case l_undef: TRACE("q", tout << l.lhs << " ~~ " << l.rhs << " is undef\n";); - if (idx == 0) { + if (idx != UINT_MAX) { idx = UINT_MAX; return l_undef; } - if (i > 0) - std::swap(c[0], c[i]); - idx = 0; + idx = i; break; } } if (idx == UINT_MAX) return l_false; - + c.m_watch = idx; return l_undef; } - lbool eval::operator()(euf::enode* const* binding, clause& c) { + lbool eval::operator()(euf::enode* const* binding, clause& c, euf::enode_pair_vector& evidence) { unsigned idx = 0; - return (*this)(binding, c, idx); + return (*this)(binding, c, idx, evidence); } - lbool eval::compare(unsigned n, euf::enode* const* binding, expr* s, expr* t) { + lbool eval::compare(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& evidence) { if (s == t) return l_true; if (m.are_distinct(s, t)) return l_false; - euf::enode* sn = (*this)(n, binding, s); - euf::enode* tn = (*this)(n, binding, t); - if (sn) sn = sn->get_root(); - if (tn) tn = tn->get_root(); + euf::enode* sn = (*this)(n, binding, s, evidence); + euf::enode* tn = (*this)(n, binding, t, evidence); + euf::enode* sr = sn ? sn->get_root() : sn; + euf::enode* tr = tn ? tn->get_root() : tn; + if (sn != sr) evidence.push_back(euf::enode_pair(sn, sr)), sn = sr; + if (tn != tr) evidence.push_back(euf::enode_pair(tn, tr)), tn = tr; TRACE("q", tout << mk_pp(s, m) << " ~~ " << mk_pp(t, m) << "\n"; tout << ctx.bpp(sn) << " " << ctx.bpp(tn) << "\n";); lbool c; - if (sn && sn == tn) + if (sn && sn == tn) return l_true; - if (sn && tn && ctx.get_egraph().are_diseq(sn, tn)) + + if (sn && tn && ctx.get_egraph().are_diseq(sn, tn)) { + evidence.push_back(euf::enode_pair(sn, tn)); return l_false; + } if (sn && tn) return l_undef; if (!sn && !tn) - return compare_rec(n, binding, s, t); + return compare_rec(n, binding, s, t, evidence); if (!tn && sn) { std::swap(tn, sn); std::swap(t, s); } - for (euf::enode* t1 : euf::enode_class(tn)) - if (c = compare_rec(n, binding, s, t1->get_expr()), c != l_undef) + unsigned sz = evidence.size(); + for (euf::enode* t1 : euf::enode_class(tn)) { + if (c = compare_rec(n, binding, s, t1->get_expr(), evidence), c != l_undef) { + evidence.push_back(euf::enode_pair(t1, tn)); return c; + } + evidence.shrink(sz); + } return l_undef; } // f(p1) = f(p2) if p1 = p2 // f(p1) != f(p2) if p1 != p2 and f is injective - lbool eval::compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t) { + lbool eval::compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& evidence) { if (m.are_equal(s, t)) return l_true; if (m.are_distinct(s, t)) @@ -127,14 +135,20 @@ namespace q { return l_undef; bool is_injective = to_app(s)->get_decl()->is_injective(); bool has_undef = false; + unsigned sz = evidence.size(); for (unsigned i = to_app(s)->get_num_args(); i-- > 0; ) { - switch (compare(n, binding, to_app(s)->get_arg(i), to_app(t)->get_arg(i))) { + unsigned sz1 = evidence.size(), sz2; + switch (compare(n, binding, to_app(s)->get_arg(i), to_app(t)->get_arg(i), evidence)) { case l_true: break; - case l_false: - if (is_injective) - return l_false; - return l_undef; + case l_false: + if (!is_injective) + return l_undef; + sz2 = evidence.size(); + for (unsigned i = 0; i < sz2 - sz1; ++i) + evidence[sz + i] = evidence[sz1 + i]; + evidence.shrink(sz + sz2 - sz1); + return l_false; case l_undef: if (!is_injective) return l_undef; @@ -142,10 +156,15 @@ namespace q { break; } } - return has_undef ? l_undef : l_true; + + if (!has_undef) + return l_true; + + evidence.shrink(sz); + return l_undef; } - euf::enode* eval::operator()(unsigned n, euf::enode* const* binding, expr* e) { + euf::enode* eval::operator()(unsigned n, euf::enode* const* binding, expr* e, euf::enode_pair_vector& evidence) { if (is_ground(e)) return ctx.get_egraph().find(e); if (m_mark.is_marked(e)) @@ -156,10 +175,11 @@ namespace q { while (!todo.empty()) { expr* t = todo.back(); SASSERT(!is_ground(t) || ctx.get_egraph().find(t)); - if (is_ground(t)) { + if (is_ground(t) || (has_quantifiers(t) && !has_free_vars(t))) { m_mark.mark(t); - m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr); - SASSERT(m_eval[t->get_id()]); + m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr); + if (!m_eval[t->get_id()]) + return nullptr; todo.pop_back(); continue; } @@ -186,6 +206,15 @@ namespace q { euf::enode* n = ctx.get_egraph().find(t, args.size(), args.data()); if (!n) return nullptr; + for (unsigned i = args.size(); i-- > 0; ) { + if (args[i] != n->get_arg(i)) { + // roots could be different when using commutativity + // instead of compensating for this, we just bail out + if (args[i]->get_root() != n->get_arg(i)->get_root()) + return nullptr; + evidence.push_back(euf::enode_pair(args[i], n->get_arg(i))); + } + } m_indirect_nodes.push_back(n); m_eval.setx(t->get_id(), n, nullptr); m_mark.mark(t); @@ -195,99 +224,18 @@ namespace q { return m_eval[e->get_id()]; } - void eval::explain(clause& c, unsigned literal_idx, euf::enode* const* b) { - unsigned n = c.num_decls(); - for (unsigned i = c.size(); i-- > 0; ) { - if (i == literal_idx) - continue; - auto const& lit = c[i]; - if (lit.sign) - explain_eq(n, b, lit.lhs, lit.rhs); - else - explain_diseq(n, b, lit.lhs, lit.rhs); - } - } - - void eval::explain_eq(unsigned n, euf::enode* const* binding, expr* s, expr* t) { - SASSERT(l_true == compare(n, binding, s, t)); - if (s == t) - return; - euf::enode* sn = (*this)(n, binding, s); - euf::enode* tn = (*this)(n, binding, t); - if (sn && tn) { - SASSERT(sn->get_root() == tn->get_root()); - ctx.add_antecedent(sn, tn); - return; - } - if (!sn && tn) { - std::swap(sn, tn); - std::swap(s, t); - } - if (sn && !tn) { - for (euf::enode* s1 : euf::enode_class(sn)) { - if (l_true == compare_rec(n, binding, t, s1->get_expr())) { - ctx.add_antecedent(sn, s1); - explain_eq(n, binding, t, s1->get_expr()); - return; - } - } - UNREACHABLE(); - } - SASSERT(is_app(s) && is_app(t)); - SASSERT(to_app(s)->get_decl() == to_app(t)->get_decl()); - for (unsigned i = to_app(s)->get_num_args(); i-- > 0; ) - explain_eq(n, binding, to_app(s)->get_arg(i), to_app(t)->get_arg(i)); - } - - void eval::explain_diseq(unsigned n, euf::enode* const* binding, expr* s, expr* t) { - SASSERT(l_false == compare(n, binding, s, t)); - if (m.are_distinct(s, t)) - return; - euf::enode* sn = (*this)(n, binding, s); - euf::enode* tn = (*this)(n, binding, t); - if (sn && tn && ctx.get_egraph().are_diseq(sn, tn)) { - ctx.add_diseq_antecedent(sn, tn); - return; - } - if (!sn && tn) { - std::swap(sn, tn); - std::swap(s, t); - } - if (sn && !tn) { - for (euf::enode* s1 : euf::enode_class(sn)) { - if (l_false == compare_rec(n, binding, t, s1->get_expr())) { - ctx.add_antecedent(sn, s1); - explain_diseq(n, binding, t, s1->get_expr()); - return; - } - } - UNREACHABLE(); - } - SASSERT(is_app(s) && is_app(t)); - app* at = to_app(t); - app* as = to_app(s); - SASSERT(as->get_decl() == at->get_decl()); - for (unsigned i = as->get_num_args(); i-- > 0; ) { - if (l_false == compare_rec(n, binding, as->get_arg(i), at->get_arg(i))) { - explain_eq(n, binding, as->get_arg(i), at->get_arg(i)); - return; - } - } - UNREACHABLE(); - } - - void eval::explain(sat::literal l, justification& j, sat::literal_vector& r, bool probing) { - scoped_mark_reset _sr(*this); - unsigned l_idx = 0; clause& c = j.m_clause; - for (; l_idx < c.size(); ++l_idx) { - if (c[l_idx].lhs == j.m_lhs && c[l_idx].rhs == j.m_rhs && c[l_idx].sign == j.m_sign) - break; + for (unsigned i = 0; i < j.m_num_ev; ++i) { + auto [a, b] = j.m_evidence[i]; + SASSERT(a->get_root() == b->get_root() || ctx.get_egraph().are_diseq(a, b)); + if (a->get_root() == b->get_root()) + ctx.add_antecedent(a, b); + else + ctx.add_diseq_antecedent(a, b); } - explain(c, l_idx, j.m_binding); r.push_back(c.m_literal); - (void)probing; // ignored + (void)probing; // ignored } diff --git a/src/sat/smt/q_eval.h b/src/sat/smt/q_eval.h index 6219c473a..5e520dc17 100644 --- a/src/sat/smt/q_eval.h +++ b/src/sat/smt/q_eval.h @@ -30,25 +30,20 @@ namespace q { expr_fast_mark1 m_mark; euf::enode_vector m_eval; euf::enode_vector m_indirect_nodes; - ptr_vector m_explain; struct scoped_mark_reset; - void explain(clause& c, unsigned literal_idx, euf::enode* const* binding); - void explain_eq(unsigned n, euf::enode* const* binding, expr* s, expr* t); - void explain_diseq(unsigned n, euf::enode* const* binding, expr* s, expr* t); - // compare s, t modulo binding - lbool compare(unsigned n, euf::enode* const* binding, expr* s, expr* t); - lbool compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t); + lbool compare(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& evidence); + lbool compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& evidence); public: eval(euf::solver& ctx); void explain(sat::literal l, justification& j, sat::literal_vector& r, bool probing); - lbool operator()(euf::enode* const* binding, clause& c); - lbool operator()(euf::enode* const* binding, clause& c, unsigned& idx); - euf::enode* operator()(unsigned n, euf::enode* const* binding, expr* e); + lbool operator()(euf::enode* const* binding, clause& c, euf::enode_pair_vector& evidence); + lbool operator()(euf::enode* const* binding, clause& c, unsigned& idx, euf::enode_pair_vector& evidence); + euf::enode* operator()(unsigned n, euf::enode* const* binding, expr* e, euf::enode_pair_vector& evidence); euf::enode_vector const& get_watch() { return m_indirect_nodes; } }; diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 30c6c7e23..da6fe4191 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -42,6 +42,7 @@ namespace q { add_plugin(ap); add_plugin(alloc(mbp::datatype_project_plugin, m)); add_plugin(alloc(mbp::array_project_plugin, m)); + } lbool mbqi::operator()() { @@ -66,10 +67,11 @@ namespace q { } } m_max_cex += ctx.get_config().m_mbqi_max_cexs; - for (auto p : m_instantiations) { - unsigned generation = std::get<2>(p); + for (auto [qlit, fml, generation] : m_instantiations) { euf::solver::scoped_generation sg(ctx, generation + 1); - m_qs.add_clause(~std::get<0>(p), ~ctx.mk_literal(std::get<1>(p))); + sat::literal lit = ctx.mk_literal(fml); + m_qs.add_clause(~qlit, ~lit); + ctx.add_root(~qlit, ~lit); } m_instantiations.reset(); return result; @@ -162,12 +164,13 @@ namespace q { return r; if (r == l_true) { model_ref mdl; - expr_ref proj(m); m_solver->get_model(mdl); if (check_forall_subst(q, *qb, *mdl)) return l_false; if (check_forall_default(q, *qb, *mdl)) return l_false; + else + return l_undef; } if (m_generation_bound >= m_generation_max) return l_true; @@ -279,8 +282,9 @@ namespace q { bool fmls_extracted = false; TRACE("q", tout << "Project\n"; - tout << *m_model << "\n"; tout << fmls << "\n"; + tout << "model\n"; + tout << *m_model << "\n"; tout << "model of projection\n" << mdl << "\n"; tout << "var args: " << qb.var_args.size() << "\n"; tout << "domain eqs: " << qb.domain_eqs << "\n"; @@ -294,8 +298,13 @@ namespace q { app* v = vars.get(i); auto* p = get_plugin(v); if (p && !fmls_extracted) { + TRACE("q", tout << "domain eqs\n" << qb.domain_eqs << "\n";); + fmls.append(qb.domain_eqs); eliminate_nested_vars(fmls, qb); + for (expr* e : fmls) + if (!m_model->is_true(e)) + return expr_ref(nullptr, m); mbp::project_plugin proj(m); proj.extract_literals(*m_model, vars, fmls); fmls_extracted = true; @@ -312,6 +321,7 @@ namespace q { eqs.push_back(m.mk_eq(v, val)); } rep(fmls); + TRACE("q", tout << "generated formulas\n" << fmls << "\ngenerated eqs:\n" << eqs;); return mk_and(fmls); } @@ -326,8 +336,8 @@ namespace q { qb.domain_eqs.reset(); var_subst subst(m); - for (auto p : qb.var_args) { - expr_ref bounds = m_model_fixer.restrict_arg(p.first, p.second); + for (auto [t, idx] : qb.var_args) { + expr_ref bounds = m_model_fixer.restrict_arg(t, idx); if (m.is_true(bounds)) continue; expr_ref vbounds = subst(bounds, qb.vars); @@ -382,11 +392,11 @@ namespace q { if (qb.var_args.empty()) return; var_subst subst(m); - for (auto p : qb.var_args) { - expr_ref _term = subst(p.first, qb.vars); + for (auto [t, idx] : qb.var_args) { + expr_ref _term = subst(t, qb.vars); app_ref term(to_app(_term), m); - expr_ref value = (*m_model)(term->get_arg(p.second)); - m_model_fixer.invert_arg(term, p.second, value, qb.domain_eqs); + expr_ref value = (*m_model)(term->get_arg(idx)); + m_model_fixer.invert_arg(term, idx, value, qb.domain_eqs); } } @@ -555,7 +565,7 @@ namespace q { void mbqi::init_solver() { if (!m_solver) - m_solver = mk_smt2_solver(m, ctx.s().params()); + m_solver = mk_smt2_solver(m, m_no_drat_params); } void mbqi::init_search() { diff --git a/src/sat/smt/q_mbi.h b/src/sat/smt/q_mbi.h index 174462ca4..1920baa52 100644 --- a/src/sat/smt/q_mbi.h +++ b/src/sat/smt/q_mbi.h @@ -20,6 +20,7 @@ Author: #include "qe/mbp/mbp_plugin.h" #include "sat/smt/sat_th.h" #include "sat/smt/q_model_fixer.h" +#include "sat/sat_solver.h" namespace euf { class solver; @@ -60,6 +61,7 @@ namespace q { stats m_stats; model_fixer m_model_fixer; model_ref m_model; + sat::no_drat_params m_no_drat_params; ref<::solver> m_solver; scoped_ptr_vector> m_values; scoped_ptr_vector m_plugins; diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp index 86c502932..41b6f31fb 100644 --- a/src/sat/smt/q_model_fixer.cpp +++ b/src/sat/smt/q_model_fixer.cpp @@ -111,6 +111,18 @@ namespace q { add_projection_functions(mdl, f); } + /** + * we are given f with interpretation: + * if x = v0 and y = w0 then f0 + * else if x = v1 and y = w1 then f1 + * ... + * Create a new interpretation for f as follows: + * f := f_aux(project1(x), project2(y)) + * f_aux uses the original interpretation of f + * project1 sorts the values of v0, v1, ..., and maps arguments below v0 to v0, between v0, v1 to v1 etc. + * project2 sorts values of w0, w1, ... and maps argument y to values w0, w1, .. + * + */ void model_fixer::add_projection_functions(model& mdl, func_decl* f) { // update interpretation of f so that the graph of f is fully determined by the // ground values of its arguments. @@ -141,6 +153,19 @@ namespace q { mdl.register_decl(f_new, fi); } + /* + * For function f(...,t_idx, ..) collect the values of terms at position idx of f + * as "values". + * Map t_idx |-> mdl(t_idx) + * and mdl(t_idx) |-> t_idx + * Sort the values as [v_1, v_2, ..., v_n] with corresponding terms + * [t_1, t_2, ..., t_n] + * + * Create the term if p(x) = if x <= v_1 then t_1 else if x <= v_2 then t_2 else ... t_n + * where p is a fresh function + * and return p(x) + */ + expr_ref model_fixer::add_projection_function(model& mdl, func_decl* f, unsigned idx) { sort* srt = f->get_domain(idx); projection_function* proj = get_projection(srt); @@ -230,6 +255,15 @@ namespace q { return value; } + /** + * We are given a term f(...,arg_i,..) and value = mdl(arg_i) + * Create + * 1 the bounds t_j <= arg_i < t_{j+1} where + * v_j <= value < v_{j+1} for the corresponding values of t_j, t_{j+1} + * 2 or the bound arg_i < t_0 if value < v_0 + * 3 or the bound arg_i >= t_last if value > v_last + */ + void model_fixer::invert_arg(app* t, unsigned i, expr* value, expr_ref_vector& lits) { TRACE("q", tout << "invert-arg " << mk_pp(t, m) << " " << i << " " << mk_pp(value, m) << "\n";); auto const* md = get_projection_data(t->get_decl(), i); diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index af670297c..0f3eaf3d3 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -40,35 +40,30 @@ namespace q { return; quantifier* q = to_quantifier(e); - auto const& exp = expand(q); - if (exp.size() > 1 && is_forall(q) && !l.sign()) { - for (expr* e : exp) { - sat::literal lit = ctx.internalize(e, l.sign(), false, false); - add_clause(~l, lit); - if (ctx.relevancy_enabled()) - ctx.add_root(~l, lit); - } - return; - } - if (exp.size() > 1 && is_exists(q) && l.sign()) { - sat::literal_vector lits; - lits.push_back(~l); - for (expr* e : exp) - lits.push_back(ctx.internalize(e, l.sign(), false, false)); - add_clause(lits); - ctx.add_root(lits); - return; - } - if (l.sign() == is_forall(e)) { sat::literal lit = skolemize(q); add_clause(~l, lit); ctx.add_root(~l, lit); } else { - ctx.push_vec(m_universal, l); - if (ctx.get_config().m_ematching) - m_ematch.add(q); + auto const& exp = expand(q); + if (exp.size() > 1) { + for (expr* e : exp) { + sat::literal lit = ctx.internalize(e, l.sign(), false, false); + add_clause(~l, lit); + ctx.add_root(~l, lit); + } + } + else if (is_ground(q->get_expr())) { + auto lit = ctx.internalize(q->get_expr(), l.sign(), false, false); + add_clause(~l, lit); + ctx.add_root(~l, lit); + } + else { + ctx.push_vec(m_universal, l); + if (ctx.get_config().m_ematching) + m_ematch.add(q); + } } m_stats.m_num_quantifier_asserts++; } @@ -88,8 +83,7 @@ namespace q { } std::ostream& solver::display(std::ostream& out) const { - m_ematch.display(out); - return out; + return m_ematch.display(out); } std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const { @@ -147,9 +141,9 @@ namespace q { } /* - * Find initial values to instantiate quantifier with so to make it as hard as possible for solver - * to find values to free variables. - */ + * Find initial values to instantiate quantifier with so to make it as hard as possible for solver + * to find values to free variables. + */ sat::literal solver::specialize(quantifier* q) { std::function mk_var = [&](quantifier* q, unsigned i) { return get_unit(q->get_decl_sort(i)); @@ -244,46 +238,11 @@ namespace q { ctx.get_rewriter()(tmp); m_expanded[i] = tmp; } - return m_expanded; } - -#if 0 - m_expanded.reset(); - m_expanded2.reset(); - if (is_forall(q)) - flatten_or(q->get_expr(), m_expanded2); - else if (is_exists(q)) - flatten_and(q->get_expr(), m_expanded2); - else - UNREACHABLE(); - for (unsigned i = m_expanded2.size(); i-- > 0; ) { - expr* lit = m_expanded2.get(i); - if (!is_ground(lit) && is_and(lit) && is_forall(q)) { - - // get free vars of lit - // create fresh predicate over free vars - // replace in expanded, pack and push on m_expanded - - expr_ref p(m); - // TODO introduce fresh p. - flatten_and(lit, m_expanded); - for (unsigned i = m_expanded.size(); i-- > 0; ) { - tmp = m.mk_or(m.mk_not(p), m_expanded.get(i)); - expr_ref tmp(m.update_quantifier(q, tmp), m); - ctx.get_rewriter()(tmp); - m_expanded[i] = tmp; - } - m_expanded2[i] = p; - tmp = m.mk_or(m_expanded2); - expr_ref tmp(m.update_quantifier(q, tmp), m); - ctx.get_rewriter()(tmp); - m_expanded.push_back(tmp); - return m_expanded; - } + else { + m_expanded.reset(); + m_expanded.push_back(q); } -#endif - m_expanded.reset(); - m_expanded.push_back(q); return m_expanded; } diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp index b392254a1..dcc90ddb0 100644 --- a/src/sat/smt/sat_dual_solver.cpp +++ b/src/sat/smt/sat_dual_solver.cpp @@ -18,25 +18,34 @@ Author: namespace sat { - dual_solver::no_drat_params::no_drat_params() { - set_sym("drat.file", symbol()); - } - dual_solver::dual_solver(reslimit& l): m_solver(m_params, l) { SASSERT(!m_solver.get_config().m_drat); } - void dual_solver::push() { - m_solver.user_push(); - m_roots.push_scope(); - m_tracked_vars.push_scope(); - m_units.push_scope(); - m_vars.push_scope(); + void dual_solver::flush() { + while (m_num_scopes > 0) { + m_solver.user_push(); + m_roots.push_scope(); + m_tracked_vars.push_scope(); + m_units.push_scope(); + m_vars.push_scope(); + --m_num_scopes; + } } - void dual_solver::pop(unsigned num_scopes) { + void dual_solver::push() { + ++m_num_scopes; + } + + void dual_solver::pop(unsigned num_scopes) { + if (m_num_scopes >= num_scopes) { + m_num_scopes -= num_scopes; + return; + } + num_scopes -= m_num_scopes; + m_num_scopes = 0; m_solver.user_pop(num_scopes); unsigned old_sz = m_tracked_vars.old_size(num_scopes); for (unsigned i = m_tracked_vars.size(); i-- > old_sz; ) @@ -66,6 +75,7 @@ namespace sat { } void dual_solver::track_relevancy(bool_var w) { + flush(); bool_var v = ext2var(w); if (!m_is_tracked.get(v, false)) { m_is_tracked.setx(v, true, false); @@ -81,27 +91,36 @@ namespace sat { return literal(m_var2ext[lit.var()], lit.sign()); } - void dual_solver::add_root(unsigned sz, literal const* clause) { - TRACE("dual", tout << "root: " << literal_vector(sz, clause) << "\n";); - if (sz == 1) { + void dual_solver::add_root(unsigned sz, literal const* clause) { + flush(); + if (false && sz == 1) { + TRACE("dual", tout << "unit: " << clause[0] << "\n";); m_units.push_back(clause[0]); return; } - literal root(m_solver.mk_var(), false); - for (unsigned i = 0; i < sz; ++i) - m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input()); + literal root; + if (sz == 1) + root = ext2lit(clause[0]); + else { + root = literal(m_solver.mk_var(), false); + for (unsigned i = 0; i < sz; ++i) + m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input()); + } m_roots.push_back(~root); + TRACE("dual", tout << "root: " << ~root << " => " << literal_vector(sz, clause) << "\n";); } void dual_solver::add_aux(unsigned sz, literal const* clause) { - TRACE("dual", tout << "aux: " << literal_vector(sz, clause) << "\n";); + flush(); m_lits.reset(); for (unsigned i = 0; i < sz; ++i) m_lits.push_back(ext2lit(clause[i])); + TRACE("dual", tout << "aux: " << literal_vector(sz, clause) << " -> " << m_lits << "\n";); m_solver.mk_clause(sz, m_lits.data(), status::input()); } void dual_solver::add_assumptions(solver const& s) { + flush(); m_lits.reset(); for (bool_var v : m_tracked_vars) m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v]))); @@ -112,7 +131,7 @@ namespace sat { } } - bool dual_solver::operator()(solver const& s) { + bool dual_solver::operator()(solver const& s) { m_core.reset(); m_core.append(m_units); if (m_roots.empty()) diff --git a/src/sat/smt/sat_dual_solver.h b/src/sat/smt/sat_dual_solver.h index 2b040128c..d0465ac32 100644 --- a/src/sat/smt/sat_dual_solver.h +++ b/src/sat/smt/sat_dual_solver.h @@ -23,9 +23,6 @@ Author: namespace sat { class dual_solver { - struct no_drat_params : public params_ref { - no_drat_params(); - }; no_drat_params m_params; solver m_solver; lim_svector m_units, m_roots; @@ -35,6 +32,7 @@ namespace sat { unsigned_vector m_ext2var; unsigned_vector m_var2ext; lim_svector m_vars; + unsigned m_num_scopes = 0; void add_literal(literal lit); bool_var ext2var(bool_var v); @@ -46,6 +44,8 @@ namespace sat { std::ostream& display(solver const& s, std::ostream& out) const; + void flush(); + public: dual_solver(reslimit& l); void push(); diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 925dac7f8..9be810e9d 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -69,7 +69,6 @@ struct goal2sat::imp : public sat::sat_internalizer { atom2bool_var & m_map; dep2asm_map & m_dep2asm; obj_map* m_expr2var_replay { nullptr }; - sat::literal m_true; bool m_ite_extra; unsigned long long m_max_memory; expr_ref_vector m_trail; @@ -92,7 +91,6 @@ struct goal2sat::imp : public sat::sat_internalizer { m_unhandled_funs(m), m_default_external(default_external) { updt_params(p); - m_true = sat::null_literal; } ~imp() override { @@ -198,16 +196,6 @@ struct goal2sat::imp : public sat::sat_internalizer { ensure_euf()->drat_bool_def(v, n); } - sat::literal mk_true() { - if (m_true == sat::null_literal) { - // create fake variable to represent true; - m_true = sat::literal(add_var(false, m.mk_true()), false); - mk_clause(m_true); // v is true - add_dual_root(1, &m_true); - } - return m_true; - } - sat::bool_var to_bool_var(expr* e) override { sat::literal l; sat::bool_var v = m_map.to_bool_var(e); @@ -228,8 +216,10 @@ struct goal2sat::imp : public sat::sat_internalizer { if (!m_expr2var_replay || !m_expr2var_replay->find(t, v)) v = add_var(true, t); m_map.insert(t, v); - if (relevancy_enabled() && (m.is_true(t) || m.is_false(t))) + if (relevancy_enabled() && (m.is_true(t) || m.is_false(t))) { add_dual_root(sat::literal(v, m.is_false(t))); + ensure_euf()->track_relevancy(v); + } return v; } @@ -285,7 +275,6 @@ struct goal2sat::imp : public sat::sat_internalizer { } } - void cache(app* t, sat::literal l) override { force_push(); SASSERT(!m_app2lit.contains(t)); @@ -294,36 +283,40 @@ struct goal2sat::imp : public sat::sat_internalizer { m_lit2app.insert(l.index(), t); m_cache_trail.push_back(t); } - - void convert_atom(expr * t, bool root, bool sign) { + + void convert_atom(expr * t, bool root, bool sign) { SASSERT(m.is_bool(t)); sat::literal l; sat::bool_var v = m_map.to_bool_var(t); if (v == sat::null_bool_var) { if (m.is_true(t)) { - l = sign ? ~mk_true() : mk_true(); + sat::literal tt = sat::literal(mk_bool_var(t), false); + mk_root_clause(tt); + l = sign ? ~tt : tt; } else if (m.is_false(t)) { - l = sign ? mk_true() : ~mk_true(); + sat::literal ff = sat::literal(mk_bool_var(t), false); + mk_root_clause(~ff); + l = sign ? ~ff : ff; } - else { - if (m_euf) { - convert_euf(t, root, sign); - return; - } + else if (m_euf) { + convert_euf(t, root, sign); + return; + } + else { if (!is_uninterp_const(t)) { if (!is_app(t)) { std::ostringstream strm; strm << mk_ismt2_pp(t, m); throw_op_not_handled(strm.str()); } - else - m_unhandled_funs.push_back(to_app(t)->get_decl()); + m_unhandled_funs.push_back(to_app(t)->get_decl()); } + v = mk_bool_var(t); l = sat::literal(v, sign); bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t); - if (ext) + if (ext) m_solver.set_external(v); TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << " " << is_uninterp_const(t) << "\n";); } @@ -550,6 +543,29 @@ struct goal2sat::imp : public sat::sat_internalizer { } } + void convert_not(app* t, bool root, bool sign) { + SASSERT(t->get_num_args() == 1); + unsigned sz = m_result_stack.size(); + SASSERT(sz >= 1); + sat::literal lit = m_result_stack[sz - 1]; + m_result_stack.shrink(sz - 1); + if (root) { + SASSERT(sz == 1); + mk_root_clause(sign ? lit : ~lit); + } + else { + sat::bool_var k = add_var(false, t); + sat::literal l(k, false); + cache(t, l); + // l <=> ~lit + mk_clause(lit, l); + mk_clause(~lit, ~l); + if (sign) + l.neg(); + m_result_stack.push_back(l); + } + } + void convert_implies(app* t, bool root, bool sign) { SASSERT(t->get_num_args() == 2); unsigned sz = m_result_stack.size(); @@ -582,8 +598,8 @@ struct goal2sat::imp : public sat::sat_internalizer { } void convert_iff(app * t, bool root, bool sign) { - if (t->get_num_args() != 2) - throw default_exception("unexpected number of arguments to xor"); + if (t->get_num_args() != 2) + throw default_exception("unexpected number of arguments to " + mk_pp(t, m)); SASSERT(t->get_num_args() == 2); unsigned sz = m_result_stack.size(); SASSERT(sz >= 2); @@ -591,6 +607,8 @@ struct goal2sat::imp : public sat::sat_internalizer { sat::literal l2 = m_result_stack[sz-2]; m_result_stack.shrink(sz - 2); if (root) { + if (m.is_xor(t)) + sign = !sign; SASSERT(sz == 2); if (sign) { mk_root_clause(l1, l2); @@ -599,17 +617,20 @@ struct goal2sat::imp : public sat::sat_internalizer { else { mk_root_clause(l1, ~l2); mk_root_clause(~l1, l2); - } + } } else { sat::bool_var k = add_var(false, t); sat::literal l(k, false); + if (m.is_xor(t)) + l1.neg(); mk_clause(~l, l1, ~l2); mk_clause(~l, ~l1, l2); - mk_clause(l, l1, l2); + mk_clause(l, l1, l2); mk_clause(l, ~l1, ~l2); - if (aig()) aig()->add_iff(l, l1, l2); - cache(t, m.is_xor(t) ? ~l : l); + if (aig()) aig()->add_iff(l, l1, l2); + + cache(t, l); if (sign) l.neg(); m_result_stack.push_back(l); @@ -703,11 +724,14 @@ struct goal2sat::imp : public sat::sat_internalizer { convert_iff(t, root, sign); break; case OP_XOR: - convert_iff(t, root, !sign); + convert_iff(t, root, sign); break; case OP_IMPLIES: convert_implies(t, root, sign); break; + case OP_NOT: + convert_not(t, root, sign); + break; default: UNREACHABLE(); } @@ -773,7 +797,7 @@ struct goal2sat::imp : public sat::sat_internalizer { m_frame_stack.pop_back(); continue; } - if (m.is_not(t)) { + if (m.is_not(t) && (root || (!m.is_not(t->get_arg(0)) && fsz != sz + 1))) { m_frame_stack.pop_back(); visit(t->get_arg(0), root, !sign); continue; @@ -808,6 +832,7 @@ struct goal2sat::imp : public sat::sat_internalizer { process(n, false, redundant); SASSERT(m_result_stack.size() == sz + 1); sat::literal result = m_result_stack.back(); + TRACE("goal2sat", tout << "done internalize " << result << " " << mk_bounded_pp(n, m, 2) << "\n";); m_result_stack.pop_back(); if (!result.sign() && m_map.to_bool_var(n) == sat::null_bool_var) { force_push(); @@ -932,7 +957,6 @@ struct goal2sat::imp : public sat::sat_internalizer { } void user_pop(unsigned n) { - m_true = sat::null_literal; } }; @@ -1006,6 +1030,10 @@ bool goal2sat::has_interpreted_funs() const { return m_imp && !m_imp->interpreted_funs().empty(); } +bool goal2sat::has_euf() const { + return m_imp && m_imp->m_euf; +} + void goal2sat::update_model(model_ref& mdl) { if (m_imp) m_imp->update_model(mdl); diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index 940777447..bc6b8dcb1 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -66,6 +66,8 @@ public: bool has_interpreted_funs() const; + bool has_euf() const; + sat::sat_internalizer& si(ast_manager& m, params_ref const& p, sat::solver_core& t, atom2bool_var& a2b, dep2asm_map& dep2asm, bool default_external = false); void update_model(model_ref& mdl); diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 4d7b23166..c8c009bbf 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -113,8 +113,11 @@ class sat_tactic : public tactic { break; } } + + bool euf = m_goal2sat.has_euf(); + for (auto* f : fmls_to_validate) - if (md->is_false(f)) + if (!euf && md->is_false(f)) IF_VERBOSE(0, verbose_stream() << "failed to validate: " << mk_pp(f, m) << "\n";); m_goal2sat.update_model(md); diff --git a/src/shell/drat_frontend.cpp b/src/shell/drat_frontend.cpp index 6972571e0..1dba2e768 100644 --- a/src/shell/drat_frontend.cpp +++ b/src/shell/drat_frontend.cpp @@ -122,12 +122,17 @@ class smt_checker { m_input_solver->assert_expr(lit2expr(~lit)); lbool is_sat = m_input_solver->check_sat(); if (is_sat != l_false) { - std::cout << "did not verify: " << lits << "\n"; - for (sat::literal lit : lits) { - std::cout << lit2expr(lit) << "\n"; - } + std::cout << "did not verify: " << is_sat << " " << lits << "\n"; + for (sat::literal lit : lits) + std::cout << lit2expr(lit) << "\n"; std::cout << "\n"; m_input_solver->display(std::cout); + if (is_sat == l_true) { + model_ref mdl; + m_input_solver->get_model(mdl); + std::cout << *mdl << "\n"; + } + exit(0); } m_input_solver->pop(1); @@ -171,6 +176,49 @@ public: unsigned_vector params; ptr_vector sorts; + void parse_quantifier(sexpr_ref const& sexpr, cmd_context& ctx, quantifier_kind& k, sort_ref_vector& domain, svector& names) { + k = quantifier_kind::forall_k; + symbol q; + unsigned sz; + if (sexpr->get_kind() != sexpr::kind_t::COMPOSITE) + goto bail; + sz = sexpr->get_num_children(); + if (sz == 0) + goto bail; + q = sexpr->get_child(0)->get_symbol(); + if (q == "forall") + k = quantifier_kind::forall_k; + else if (q == "exists") + k = quantifier_kind::exists_k; + else if (q == "lambda") + k = quantifier_kind::lambda_k; + else + goto bail; + for (unsigned i = 1; i < sz; ++i) { + auto* e = sexpr->get_child(i); + if (e->get_kind() != sexpr::kind_t::COMPOSITE) + goto bail; + if (2 != e->get_num_children()) + goto bail; + symbol name = e->get_child(0)->get_symbol(); + std::ostringstream ostrm; + e->get_child(1)->display(ostrm); + std::istringstream istrm(ostrm.str()); + params_ref p; + auto srt = parse_smt2_sort(ctx, istrm, false, p, "quantifier"); + if (!srt) + goto bail; + names.push_back(name); + domain.push_back(srt); + } + return; + bail: + std::cout << "Could not parse expression\n"; + sexpr->display(std::cout); + std::cout << "\n"; + exit(0); + } + void parse_sexpr(sexpr_ref const& sexpr, cmd_context& ctx, expr_ref_vector const& args, expr_ref& result) { params.reset(); sorts.reset(); @@ -310,7 +358,17 @@ static void verify_smt(char const* drat_file, char const* smt_file) { std::istringstream strm(r.m_name); auto sexpr = parse_sexpr(ctx, strm, p, drat_file); checker.parse_sexpr(sexpr, ctx, args, e); - exprs.reserve(r.m_node_id+1); + exprs.reserve(r.m_node_id + 1); + exprs.set(r.m_node_id, e); + break; + } + case dimacs::drat_record::tag_t::is_var: { + var_ref e(m); + SASSERT(r.m_args.size() == 1); + std::istringstream strm(r.m_name); + auto srt = parse_smt2_sort(ctx, strm, false, p, drat_file); + e = m.mk_var(r.m_args[0], srt); + exprs.reserve(r.m_node_id + 1); exprs.set(r.m_node_id, e); break; } @@ -331,12 +389,26 @@ static void verify_smt(char const* drat_file, char const* smt_file) { srt = pd->instantiate(ctx.pm(), sargs.size(), sargs.data()); else srt = m.mk_uninterpreted_sort(name); - sorts.reserve(r.m_node_id+1); + sorts.reserve(r.m_node_id + 1); sorts.set(r.m_node_id, srt); break; } + case dimacs::drat_record::tag_t::is_quantifier: { + VERIFY(r.m_args.size() == 1); + quantifier_ref q(m); + std::istringstream strm(r.m_name); + auto sexpr = parse_sexpr(ctx, strm, p, drat_file); + sort_ref_vector domain(m); + svector names; + quantifier_kind k; + checker.parse_quantifier(sexpr, ctx, k, domain, names); + q = m.mk_quantifier(k, domain.size(), domain.data(), names.data(), exprs.get(r.m_args[0])); + exprs.reserve(r.m_node_id + 1); + exprs.set(r.m_node_id, q); + break; + } case dimacs::drat_record::tag_t::is_bool_def: - bool_var2expr.reserve(r.m_node_id+1); + bool_var2expr.reserve(r.m_node_id + 1); bool_var2expr.set(r.m_node_id, exprs.get(r.m_args[0])); break; default: @@ -347,7 +419,6 @@ static void verify_smt(char const* drat_file, char const* smt_file) { statistics st; drat_checker.collect_statistics(st); std::cout << st << "\n"; - } @@ -359,5 +430,3 @@ unsigned read_drat(char const* drat_file, char const* problem_file) { verify_smt(drat_file, problem_file); return 0; } - - diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index f8d99f398..0d09f07ea 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -121,7 +121,7 @@ namespace { struct instruction { opcode m_opcode; - instruction * m_next; + instruction* m_next = nullptr; #ifdef _PROFILE_MAM unsigned m_counter; // how often it was executed #endif @@ -1224,9 +1224,10 @@ namespace { return; SASSERT(head->m_next == 0); + m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast(m_vars.begin()))); - for (instruction * curr : m_seq) { + for (instruction* curr : m_seq) { head->m_next = curr; head = curr; } @@ -2309,7 +2310,10 @@ namespace { main_loop: + if (!m_pc) + goto backtrack; TRACE("mam_int", display_pc_info(tout);); + #ifdef _PROFILE_MAM const_cast(m_pc)->m_counter++; #endif diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index c3e34f0de..d1614f521 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -213,11 +213,12 @@ void proto_model::cleanup() { TRACE("model_bug", model_v2_pp(tout, *this);); func_decl_set found_aux_fs; expr_ref_vector trail(m); - for (auto const& kv : m_finterp) { - TRACE("model_bug", tout << kv.m_key->get_name() << "\n";); - func_interp * fi = kv.m_value; + ptr_buffer finterps; + for (auto const& kv : m_finterp) + finterps.push_back(kv.m_value); + for (auto* fi : finterps) cleanup_func_interp(trail, fi, found_aux_fs); - } + for (unsigned i = 0; i < m_const_decls.size(); ++i) { func_decl* d = m_const_decls[i]; expr* e = m_interp[d].second; diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h index c5aa68e0a..e9fc3cb53 100644 --- a/src/smt/seq_axioms.h +++ b/src/smt/seq_axioms.h @@ -81,6 +81,7 @@ namespace smt { void add_itos_axiom(expr* s, unsigned k) { m_ax.itos_axiom(s, k); } void add_ubv2s_axiom(expr* b, unsigned k) { m_ax.ubv2s_axiom(b, k); } void add_ubv2s_len_axiom(expr* b, unsigned k) { m_ax.ubv2s_len_axiom(b, k); } + void add_ubv2s_len_axiom(expr* b) { m_ax.ubv2s_len_axiom(b); } void add_ubv2ch_axioms(sort* s) { m_ax.ubv2ch_axiom(s); } void add_lt_axiom(expr* n) { m_ax.lt_axiom(n); } void add_le_axiom(expr* n) { m_ax.le_axiom(n); } diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index c35e413ba..80282c3f8 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -272,13 +272,15 @@ namespace smt { << "PA(" << mk_pp(s, m) << "@" << idx << "," << state_str(r) << ") ";); - if (re().is_empty(r)) { + auto info = re().get_info(r); + + //if the minlength of the regex is UINT_MAX then the regex is a deadend + if (re().is_empty(r) || info.min_length == UINT_MAX) { STRACE("seq_regex_brief", tout << "(empty) ";); th.add_axiom(~lit); return; } - auto info = re().get_info(r); if (info.interpreted) { update_state_graph(r); diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 47bc13242..14a71ae28 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -315,7 +315,7 @@ namespace smt { void conflict_resolution::process_antecedent(literal antecedent, unsigned & num_marks) { bool_var var = antecedent.var(); unsigned lvl = m_ctx.get_assign_level(var); - SASSERT(var < static_cast(m_ctx.get_num_bool_vars())); + SASSERT(var < m_ctx.get_num_bool_vars()); TRACE("conflict_", tout << "processing antecedent (level " << lvl << "):"; m_ctx.display_literal(tout, antecedent); m_ctx.display_detailed_literal(tout << " ", antecedent) << "\n";); diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index 9422c2963..dcdb9a198 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -389,8 +389,7 @@ namespace smt { if (fid == null_family_id) return !m_hidden_ufs.contains(f); if (fid == m.get_basic_family_id()) return false; theory * th = m_context->get_theory(fid); - if (!th) return true; - return th->include_func_interp(f); + return !th || th->include_func_interp(f); } /** diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index c4bf2634b..fab30ae71 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1542,6 +1542,7 @@ void theory_seq::add_ubv_string(expr* e) { } if (!has_sort) m_ax.add_ubv2ch_axioms(b->get_sort()); + m_ax.add_ubv2s_len_axiom(b); m_ubv_string.push_back(e); m_trail_stack.push(push_back_vector(m_ubv_string)); add_length_to_eqc(e); @@ -1557,7 +1558,6 @@ bool theory_seq::check_ubv_string() { } bool theory_seq::check_ubv_string(expr* e) { - expr* n = nullptr; if (ctx.inconsistent()) return true; if (m_has_ubv_axiom.contains(e)) diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index c612d4938..4a8070927 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -903,7 +903,7 @@ namespace smt { m.mk_app(memf, x, m.mk_app(tl, S)))); recfun_replace rep(m); var* vars[2] = { xV, SV }; - p.set_definition(rep, mem, 2, vars, mem_body); + p.set_definition(rep, mem, false, 2, vars, mem_body); } sort_ref tup(dt.mk_pair_datatype(listS, listS, fst, snd, pair), m); @@ -926,7 +926,7 @@ namespace smt { recfun_replace rep(m); var* vars[5] = { aV, bV, AV, SV, tupV }; - p.set_definition(rep, nxt, 5, vars, next_body); + p.set_definition(rep, nxt, false, 5, vars, next_body); } { @@ -961,7 +961,7 @@ namespace smt { TRACE("special_relations", tout << connected_body << "\n";); recfun_replace rep(m); var* vars[3] = { AV, dstV, SV }; - p.set_definition(rep, connected, 3, vars, connected_body); + p.set_definition(rep, connected, false, 3, vars, connected_body); } { diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index e5c1469a6..0b772f17d 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1859,18 +1859,18 @@ namespace smt { axiomatized_terms.insert(ex); TRACE("str", tout << "instantiate str.from_code axiom for " << mk_pp(ex, m) << std::endl;); - expr * arg; - u.str.is_from_code(ex, arg); + expr * arg = nullptr; + VERIFY(u.str.is_from_code(ex, arg)); // (str.from_code N) == "" if N is not in the range [0, max_char]. { - expr_ref premise(m.mk_or(m_autil.mk_le(arg, mk_int(-1)), m_autil.mk_ge(arg, mk_int(u.max_char() + 1))), m); + expr_ref premise(m.mk_or(m_autil.mk_le(arg, mk_int(-1)), m_autil.mk_ge(arg, mk_int(u.max_char() + 1))), m); expr_ref conclusion(ctx.mk_eq_atom(ex, mk_string("")), m); expr_ref axiom(rewrite_implication(premise, conclusion), m); assert_axiom_rw(axiom); } // len (str.from_code N) == 1 if N is in the range [0, max_char]. { - expr_ref premise(m.mk_and(m_autil.mk_ge(arg, mk_int(0)), m_autil.mk_le(arg, mk_int(u.max_char() + 1))), m); + expr_ref premise(m.mk_and(m_autil.mk_ge(arg, mk_int(0)), m_autil.mk_le(arg, mk_int(u.max_char() + 1))), m); expr_ref conclusion(ctx.mk_eq_atom(mk_strlen(ex), mk_int(1)), m); expr_ref axiom(rewrite_implication(premise, conclusion), m); assert_axiom_rw(axiom); @@ -1895,8 +1895,8 @@ namespace smt { axiomatized_terms.insert(ex); TRACE("str", tout << "instantiate str.to_code axiom for " << mk_pp(ex, m) << std::endl;); - expr * arg; - u.str.is_to_code(ex, arg); + expr * arg = nullptr; + VERIFY(u.str.is_to_code(ex, arg)); // (str.to_code S) == -1 if len(S) != 1. { expr_ref premise(m.mk_not(ctx.mk_eq_atom(mk_strlen(arg), mk_int(1))), m); @@ -5523,6 +5523,7 @@ namespace smt { TRACE("str", tout << mk_pp(node, get_manager()) << std::endl;); if (groundedMap.find(node) != groundedMap.end()) { for (auto const &itor : groundedMap[node]) { + (void) itor; TRACE("str", tout << "\t[grounded] "; for (auto const &vIt : itor.first) { diff --git a/src/solver/assertions/CMakeLists.txt b/src/solver/assertions/CMakeLists.txt index 3e1c1c0e3..7cc320458 100644 --- a/src/solver/assertions/CMakeLists.txt +++ b/src/solver/assertions/CMakeLists.txt @@ -2,7 +2,6 @@ z3_add_component(solver_assertions SOURCES asserted_formulas.cpp COMPONENT_DEPENDENCIES - solver smt2parser smt_params ) diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index 816ccb4e1..be931ccd6 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -424,7 +424,8 @@ void asserted_formulas::apply_quasi_macros() { TRACE("before_quasi_macros", display(tout);); vector new_fmls; quasi_macros proc(m, m_macro_manager); - while (proc(m_formulas.size() - m_qhead, + while (m_qhead == 0 && + proc(m_formulas.size() - m_qhead, m_formulas.data() + m_qhead, new_fmls)) { swap_asserted_formulas(new_fmls); diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 32cb0b940..b53e3daed 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -202,12 +202,6 @@ bool solver::is_literal(ast_manager& m, expr* e) { void solver::assert_expr(expr* f) { expr_ref fml(f, get_manager()); - if (m_enforce_model_conversion) { - model_converter_ref mc = get_model_converter(); - if (mc) { - (*mc)(fml); - } - } assert_expr_core(fml); } @@ -215,13 +209,6 @@ void solver::assert_expr(expr* f, expr* t) { ast_manager& m = get_manager(); expr_ref fml(f, m); expr_ref a(t, m); - if (m_enforce_model_conversion) { - model_converter_ref mc = get_model_converter(); - if (mc) { - (*mc)(fml); - // (*mc)(a); - } - } assert_expr_core2(fml, a); } @@ -241,14 +228,12 @@ void solver::collect_param_descrs(param_descrs & r) { void solver::reset_params(params_ref const & p) { m_params = p; solver_params sp(m_params); - m_enforce_model_conversion = sp.enforce_model_conversion(); m_cancel_backup_file = sp.cancel_backup_file(); } void solver::updt_params(params_ref const & p) { m_params.copy(p); solver_params sp(m_params); - m_enforce_model_conversion = sp.enforce_model_conversion(); m_cancel_backup_file = sp.cancel_backup_file(); } diff --git a/src/solver/solver.h b/src/solver/solver.h index b65dc2fe8..14fd49bce 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -49,10 +49,9 @@ solver* mk_smt2_solver(ast_manager& m, params_ref const& p); */ class solver : public check_sat_result { params_ref m_params; - bool m_enforce_model_conversion; symbol m_cancel_backup_file; public: - solver(): m_enforce_model_conversion(false) {} + solver() {} ~solver() override {} /** diff --git a/src/solver/solver_params.pyg b/src/solver/solver_params.pyg index b852afbaa..21d0ab530 100644 --- a/src/solver/solver_params.pyg +++ b/src/solver/solver_params.pyg @@ -2,8 +2,7 @@ def_module_params('solver', description='solver parameters', export=True, - params=(('enforce_model_conversion', BOOL, False, "apply model transformation on new assertions"), - ('smtlib2_log', SYMBOL, '', "file to save solver interaction"), + params=(('smtlib2_log', SYMBOL, '', "file to save solver interaction"), ('cancel_backup_file', SYMBOL, '', "file to save partial search state if search is canceled"), ('timeout', UINT, UINT_MAX, "timeout on the solver object; overwrites a global timeout"), )) diff --git a/src/tactic/CMakeLists.txt b/src/tactic/CMakeLists.txt index 495078afc..114e4f849 100644 --- a/src/tactic/CMakeLists.txt +++ b/src/tactic/CMakeLists.txt @@ -12,7 +12,6 @@ z3_add_component(tactic probe.cpp proof_converter.cpp replace_proof_converter.cpp - sine_filter.cpp tactical.cpp tactic.cpp COMPONENT_DEPENDENCIES @@ -20,7 +19,6 @@ z3_add_component(tactic model TACTIC_HEADERS probe.h - sine_filter.h tactic.h PYG_FILES tactic_params.pyg diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index 44b771d53..4f10b0b3f 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -93,7 +93,8 @@ class fm_tactic : public tactic { expr * lhs = to_app(l)->get_arg(0); expr * rhs = to_app(l)->get_arg(1); rational c; - u.is_numeral(rhs, c); + if (!u.is_numeral(rhs, c)) + return NONE; if (neg) c.neg(); unsigned num_mons; @@ -112,7 +113,8 @@ class fm_tactic : public tactic { expr * xi; rational ai_val; if (u.is_mul(monomial, ai, xi)) { - u.is_numeral(ai, ai_val); + if (!u.is_numeral(ai, ai_val)) + return NONE; } else { xi = monomial; @@ -120,7 +122,8 @@ class fm_tactic : public tactic { } if (u.is_to_real(xi)) xi = to_app(xi)->get_arg(0); - SASSERT(is_uninterp_const(xi)); + if (!is_uninterp_const(xi)) + return NONE; if (x == to_app(xi)->get_decl()) { a_val = ai_val; if (neg) @@ -129,9 +132,9 @@ class fm_tactic : public tactic { else { expr_ref val(m); val = ev(monomial); - SASSERT(u.is_numeral(val)); rational tmp; - u.is_numeral(val, tmp); + if (!u.is_numeral(val, tmp)) + return NONE; if (neg) tmp.neg(); c -= tmp; @@ -162,11 +165,9 @@ class fm_tactic : public tactic { fm_model_converter(ast_manager & _m):m(_m) {} ~fm_model_converter() override { - m.dec_array_ref(m_xs.size(), m_xs.data()); - vector::iterator it = m_clauses.begin(); - vector::iterator end = m_clauses.end(); - for (; it != end; ++it) - m.dec_array_ref(it->size(), it->data()); + m.dec_array_ref(m_xs.size(), m_xs.data()); + for (auto& c : m_clauses) + m.dec_array_ref(c.size(), c.data()); } void insert(func_decl * x, clauses & c) { @@ -177,6 +178,7 @@ class fm_tactic : public tactic { m_clauses.back().swap(c); } + void get_units(obj_map& units) override { units.reset(); } void operator()(model_ref & md) override { @@ -252,11 +254,8 @@ class fm_tactic : public tactic { for (unsigned i = 0; i < sz; i++) { out << "\n(" << m_xs[i]->get_name(); clauses const & cs = m_clauses[i]; - clauses::const_iterator it = cs.begin(); - clauses::const_iterator end = cs.end(); - for (; it != end; ++it) { - out << "\n " << mk_ismt2_pp(*it, m, 2); - } + for (auto& c : cs) + out << "\n " << mk_ismt2_pp(c, m, 2); out << ")"; } out << ")\n"; @@ -274,10 +273,8 @@ class fm_tactic : public tactic { clauses const & cs = m_clauses[i]; res->m_clauses.push_back(clauses()); clauses & new_cs = res->m_clauses.back(); - clauses::const_iterator it = cs.begin(); - clauses::const_iterator end = cs.end(); - for (; it != end; ++it) { - app * new_c = translator(*it); + for (auto& c : cs) { + app * new_c = translator(c); to_m.inc_ref(new_c); new_cs.push_back(new_c); } @@ -1598,7 +1595,7 @@ class fm_tactic : public tactic { report_tactic_progress(":fm-cost", m_counter); if (!m_inconsistent) { copy_remaining(); - m_new_goal->add(concat(g->mc(), m_mc.get())); + m_new_goal->add(m_mc.get()); } } reset_constraints(); diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index dc193f9a8..7e1fe17ca 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -321,8 +321,6 @@ class recover_01_tactic : public tactic { SASSERT(new_goal->depth() == g->depth()); SASSERT(new_goal->prec() == g->prec()); new_goal->inc_depth(); - new_goal->add(g->mc()); - new_goal->add(g->pc()); for (unsigned i = 0; i < g->size(); i++) { expr * f = g->form(i); @@ -375,7 +373,7 @@ class recover_01_tactic : public tactic { new_goal->update(idx, new_curr); } result.push_back(new_goal.get()); - TRACE("recover_01", new_goal->display(tout);); + TRACE("recover_01", new_goal->display(tout); if (new_goal->mc()) new_goal->mc()->display(tout);); SASSERT(new_goal->is_well_formed()); } diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index 87f10dfc2..c9ee5d532 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -139,7 +139,8 @@ public: } for (unsigned i = 0; i < m_ge.size(); ++i) { - classify_vars(i, to_app(g->form(m_ge[i]))); + if (!classify_vars(i, to_app(g->form(m_ge[i])))) + return false; } declassifier dcl(m_vars); @@ -199,7 +200,7 @@ public: expr* fml = g->form(m_ge[i]); if (!to_ge(fml, args1, coeffs1, k1)) continue; if (args1.empty()) continue; - expr* arg = args1[0].get(); + expr* arg = args1.get(0); bool neg = m.is_not(arg, arg); if (!is_uninterp_const(arg)) continue; if (!m_vars.contains(to_app(arg))) continue; @@ -377,15 +378,15 @@ private: } } - void classify_vars(unsigned idx, app* e) { + bool classify_vars(unsigned idx, app* e) { expr* r; if (m.is_not(e, r) && is_uninterp_const(r)) { insert(idx, to_app(r), false); - return; + return true; } if (is_uninterp_const(e)) { insert(idx, e, true); - return; + return true; } for (unsigned i = 0; i < e->get_num_args(); ++i) { expr* arg = e->get_arg(i); @@ -393,14 +394,17 @@ private: // no-op } else if (m.is_not(arg, r)) { - SASSERT(is_uninterp_const(r)); + if (!is_uninterp_const(r)) + return false; insert(idx, to_app(r), false); } else { - SASSERT(is_uninterp_const(arg)); + if (!is_uninterp_const(arg)) + return false; insert(idx, to_app(arg), true); } } + return true; } void insert(unsigned i, app* e, bool pos) { @@ -478,24 +482,28 @@ private: expr_ref_vector args1(m), args2(m); vector coeffs1, coeffs2; rational k1, k2; - if (!to_ge(fml1, args1, coeffs1, k1)) return; - if (!k1.is_one()) return; - if (!to_ge(g->form(idx2), args2, coeffs2, k2)) return; + if (!to_ge(fml1, args1, coeffs1, k1) || !k1.is_one()) + return; + if (!to_ge(fml2, args2, coeffs2, k2)) + return; // check that each variable in idx1 occurs only in idx2 unsigned min_index = 0; rational min_coeff(0); unsigned_vector indices; for (unsigned i = 0; i < args1.size(); ++i) { - expr* x = args1[i].get(); + expr* x = args1.get(i); m.is_not(x, x); - if (!is_app(x)) return; - if (!m_vars.contains(to_app(x))) return; + if (!is_app(x) || !m_vars.contains(to_app(x))) + return; TRACE("pb", tout << mk_pp(x, m) << "\n";); rec const& r = m_vars.find(to_app(x)); - if (r.pos.size() != 1 || r.neg.size() != 1) return; - if (r.pos[0] != idx2 && r.neg[0] != idx2) return; + if (r.pos.size() != 1 || r.neg.size() != 1) + return; + if (r.pos[0] != idx2 && r.neg[0] != idx2) + return; + bool found = false; for (unsigned j = 0; j < args2.size(); ++j) { - if (is_complement(args1[i].get(), args2[j].get())) { + if (is_complement(args1.get(i), args2.get(j))) { if (i == 0) { min_coeff = coeffs2[j]; } @@ -504,12 +512,15 @@ private: min_index = j; } indices.push_back(j); + found = true; } } + if (!found) + return; } for (unsigned i = 0; i < indices.size(); ++i) { unsigned j = indices[i]; - expr* arg = args2[j].get(); + expr* arg = args2.get(j); if (j == min_index) { args2[j] = m.mk_false(); } @@ -521,9 +532,7 @@ private: tmp1 = pb.mk_ge(args2.size(), coeffs2.data(), args2.data(), k2); IF_VERBOSE(3, verbose_stream() << " " << tmp1 << "\n"; - for (unsigned i = 0; i < args2.size(); ++i) { - verbose_stream() << mk_pp(args2[i].get(), m) << " "; - } + verbose_stream() << args2 << "\n"; verbose_stream() << "\n"; ); m_r(tmp1, tmp2); diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index 8ef21d9c9..2886eb6ab 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -139,68 +139,6 @@ void generic_model_converter::set_env(ast_pp_util* visitor) { } } -struct min_app_idx_proc { - unsigned m_min; - obj_map& m_idxs; - min_app_idx_proc(obj_map& idxs) : m_min(UINT_MAX), m_idxs(idxs) {} - void operator()(app * n) { - unsigned idx; - if (m_idxs.find(n->get_decl(), idx)) { - m_min = std::min(m_min, idx); - } - } - void operator()(var * n) {} - void operator()(quantifier * n) {} -}; - -void generic_model_converter::operator()(expr_ref& fml) { - min_app_idx_proc min_proc(m_first_idx); - for_each_expr(min_proc, fml); - unsigned min_idx = min_proc.m_min; - if (min_idx == UINT_MAX) return; - expr_ref_vector fmls(m); - fmls.push_back(fml); - for (unsigned i = m_entries.size(); i-- > min_idx;) { - entry const& e = m_entries[i]; - if (e.m_instruction != instruction::ADD) { - continue; - } - unsigned arity = e.m_f->get_arity(); - if (arity == 0) { - fmls.push_back(simplify_def(e)); - } - else { - expr_ref_vector args(m); - sort_ref_vector sorts(m); - svector names; - for (unsigned i = 0; i < arity; ++i) { - sorts.push_back(e.m_f->get_domain(i)); - names.push_back(symbol(i)); - args.push_back(m.mk_var(i, sorts.back())); - } - // TBD: check if order is correct with respect to quantifier binding ordering - expr_ref lhs(m.mk_app(e.m_f, arity, args.data()), m); - expr_ref body(m.mk_eq(lhs, e.m_def), m); - fmls.push_back(m.mk_forall(arity, sorts.data(), names.data(), body)); - } - if (m_first_idx[e.m_f] == i) { - m_first_idx.remove(e.m_f); - } - } - unsigned j = min_idx; - for (unsigned i = min_idx; i < m_entries.size(); ++i) { - entry& e = m_entries[i]; - if (e.m_instruction == instruction::HIDE) { - if (i != j) { - m_entries[j] = e; - } - ++j; - } - } - m_entries.shrink(j); - fml = mk_and(fmls); -} - void generic_model_converter::get_units(obj_map& units) { th_rewriter rw(m); expr_safe_replace rep(m); diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index 54268ac1b..e809fe734 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -54,6 +54,8 @@ public: void operator()(model_ref & md) override; + void operator()(expr_ref& fml) override { UNREACHABLE(); } + void cancel() override {} void display(std::ostream & out) override; @@ -64,8 +66,6 @@ public: void set_env(ast_pp_util* visitor) override; - void operator()(expr_ref& fml) override; - void get_units(obj_map& units) override; }; diff --git a/src/tactic/horn_subsume_model_converter.cpp b/src/tactic/horn_subsume_model_converter.cpp index 38e6a42c5..79b9a038f 100644 --- a/src/tactic/horn_subsume_model_converter.cpp +++ b/src/tactic/horn_subsume_model_converter.cpp @@ -169,10 +169,6 @@ void horn_subsume_model_converter::add_default_false_interpretation(expr* e, mod } -void horn_subsume_model_converter::operator()(expr_ref& fml) { - NOT_IMPLEMENTED_YET(); -} - void horn_subsume_model_converter::operator()(model_ref& mr) { func_decl_ref pred(m); diff --git a/src/tactic/horn_subsume_model_converter.h b/src/tactic/horn_subsume_model_converter.h index f007a63f3..41e59070e 100644 --- a/src/tactic/horn_subsume_model_converter.h +++ b/src/tactic/horn_subsume_model_converter.h @@ -72,8 +72,6 @@ public: void operator()(model_ref& _m) override; - void operator()(expr_ref& fml) override; - model_converter * translate(ast_translation & translator) override; ast_manager& get_manager() { return m; } diff --git a/src/tactic/model_converter.h b/src/tactic/model_converter.h index 2b3a1b510..3ed9f298b 100644 --- a/src/tactic/model_converter.h +++ b/src/tactic/model_converter.h @@ -76,6 +76,8 @@ public: virtual void operator()(model_ref & m) = 0; virtual void operator()(labels_vec & r) {} + + virtual void operator()(expr_ref& fml) { UNREACHABLE(); } virtual model_converter * translate(ast_translation & translator) = 0; @@ -86,7 +88,6 @@ public: The operator has as side effect of adding definitions as assertions to the formula and removing these definitions from the model converter. */ - virtual void operator()(expr_ref& formula) { UNREACHABLE(); } virtual void get_units(obj_map& fmls) { UNREACHABLE(); } }; diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt index 0913bf7f0..6e954717f 100644 --- a/src/tactic/portfolio/CMakeLists.txt +++ b/src/tactic/portfolio/CMakeLists.txt @@ -3,6 +3,7 @@ z3_add_component(portfolio default_tactic.cpp smt_strategic_solver.cpp solver2lookahead.cpp + solver_subsumption_tactic.cpp COMPONENT_DEPENDENCIES aig_tactic fp @@ -16,4 +17,6 @@ z3_add_component(portfolio fd_solver TACTIC_HEADERS default_tactic.h + solver_subsumption_tactic.h + ) diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp new file mode 100644 index 000000000..ac6cdede2 --- /dev/null +++ b/src/tactic/portfolio/solver_subsumption_tactic.cpp @@ -0,0 +1,172 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + solver_subsumption_tactic.cpp + +Author: + + Nikolaj Bjorner (nbjorner) 2021-7-23 + +--*/ +#include "ast/ast_util.h" +#include "tactic/tactical.h" +#include "tactic/portfolio/solver_subsumption_tactic.h" +#include "solver/solver.h" + +class solver_subsumption_tactic : public tactic { + ast_manager& m; + params_ref m_params; + solver_ref m_solver; + + void push() { + m_solver->push(); + } + + void pop() { + m_solver->pop(1); + } + + void assert_expr(expr* f) { + m_solver->assert_expr(f); + } + + bool subsumed(expr* f) { + expr_ref_vector fmls(m); + fmls.push_back(m.mk_not(f)); + lbool is_sat = m_solver->check_sat(fmls); + return (is_sat == l_false); + } + + /** + * Check subsumption (a \/ b \/ c) + * if (a \/ b) is already implied + * Use a naive algorithm (not binary disection here) + */ + + bool simplify(expr_ref& f) { + if (!m.is_or(f)) + return false; + expr_ref_vector ors(m); + ors.append(to_app(f)->get_num_args(), to_app(f)->get_args()); + expr_ref_vector prefix(m); + for (unsigned i = 0; i < ors.size(); ++i) { + expr_ref_vector fmls(m); + fmls.append(prefix); + for (unsigned k = i + 1; k < ors.size(); ++k) + fmls.push_back(m.mk_not(ors.get(k))); + lbool is_sat = m_solver->check_sat(fmls); + if (is_sat == l_false) + continue; + fmls.reset(); + fmls.push_back(ors.get(i)); + + is_sat = m_solver->check_sat(fmls); + if (is_sat == l_false) + continue; + prefix.push_back(ors.get(i)); + } + if (ors.size() != prefix.size()) { + ors.reset(); + ors.append(prefix.size(), prefix.data()); + f = mk_or(ors); + return true; + } + return false; + } + + void simplify(vector>& fmls, unsigned_vector& change) { + + if (fmls.size() == 0) + return; + + if (fmls.size() == 1) { + if (subsumed(fmls[0].second)) { + change.push_back(fmls[0].first); + fmls[0].second = m.mk_true(); + } + else if (simplify(fmls[0].second)) + change.push_back(fmls[0].first); + return; + } + unsigned mid = fmls.size() / 2; + + vector> pre(mid, fmls.data()); + vector> post(fmls.size() - mid, fmls.data() + mid); + push(); + for (auto [p, f] : post) + assert_expr(f); + simplify(pre, change); + pop(); + push(); + for (auto [p, f] : pre) + assert_expr(f); + simplify(post, change); + pop(); + if (!change.empty()) { + fmls.reset(); + fmls.append(pre); + fmls.append(post); + } + } + +public: + solver_subsumption_tactic(ast_manager& m, params_ref const& p) : + m(m), + m_params(p) { + } + + tactic* translate(ast_manager& other_m) override { + return alloc(solver_subsumption_tactic, other_m, m_params); + } + + ~solver_subsumption_tactic() override {} + + void updt_params(params_ref const& p) override { + m_params = p; + unsigned max_conflicts = p.get_uint("max_conflicts", 2); + m_params.set_uint("sat.max_conflicts", max_conflicts); + m_params.set_uint("smt.max_conflicts", max_conflicts); + } + + void collect_param_descrs(param_descrs& r) override { + r.insert("max_conflicts", CPK_UINT, "(default: 10) maximal number of conflicts allowed per solver call."); + } + + void operator()(goal_ref const& g, goal_ref_buffer& result) override { + TRACE("tactic", tout << "params: " << m_params << "\n"; g->display(tout);); + tactic_report report("subsumption", *g); + + vector> fmls; + unsigned_vector change; + unsigned sz = g->size(); + if (sz == 1) { + result.push_back(g.get()); + return; + } + for (unsigned i = 0; i < sz; i++) + fmls.push_back(std::make_pair(i, expr_ref(g->form(i), m))); + if (!m_solver) { + scoped_ptr f = mk_smt_strategic_solver_factory(); + m_solver = (*f)(m, m_params, false, false, true, symbol::null); + } + simplify(fmls, change); + if (change.empty()) { + result.push_back(g.get()); + return; + } + g->inc_depth(); + for (unsigned idx : change) + g->update(idx, fmls[idx].second); + g->elim_true(); + result.push_back(g.get()); + } + + void cleanup() override {} +}; + +tactic* mk_solver_subsumption_tactic(ast_manager& m, params_ref const& p) { + return alloc(solver_subsumption_tactic, m, p); +} + diff --git a/src/tactic/portfolio/solver_subsumption_tactic.h b/src/tactic/portfolio/solver_subsumption_tactic.h new file mode 100644 index 000000000..c088aa0b0 --- /dev/null +++ b/src/tactic/portfolio/solver_subsumption_tactic.h @@ -0,0 +1,25 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + solver_subsumption_tactic.h + +Author: + + Nikolaj Bjorner (nbjorner) 2021-7-23 + +--*/ +#pragma once + +#include "util/params.h" +class ast_manager; +class tactic; + +tactic * mk_solver_subsumption_tactic(ast_manager & m, params_ref const & p = params_ref()); + +/* + ADD_TACTIC("solver_subsumption", "remove assertions that are subsumed.", "mk_solver_subsumption_tactic(m, p)") +*/ + + diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp deleted file mode 100644 index 781150a6a..000000000 --- a/src/tactic/sine_filter.cpp +++ /dev/null @@ -1,236 +0,0 @@ -/*++ -Copyright (c) 2016 Microsoft Corporation - -Module Name: - - sine_filter.cpp - -Abstract: - - Tactic that performs Sine Qua Non premise selection - -Author: - - Doug Woos - -Revision History: ---*/ - -#include "tactic/sine_filter.h" -#include "tactic/tactical.h" -#include "tactic/generic_model_converter.h" -#include "ast/datatype_decl_plugin.h" -#include "ast/rewriter/rewriter_def.h" -#include "ast/rewriter/var_subst.h" -#include "ast/ast_util.h" -#include "util/obj_pair_hashtable.h" -#include "ast/ast_pp.h" - -class sine_tactic : public tactic { - - ast_manager& m; - params_ref m_params; - -public: - - sine_tactic(ast_manager& m, params_ref const& p): - m(m), m_params(p) {} - - tactic * translate(ast_manager & m) override { - return alloc(sine_tactic, m, m_params); - } - - void updt_params(params_ref const & p) override { - } - - void collect_param_descrs(param_descrs & r) override { - } - - void operator()(goal_ref const & g, goal_ref_buffer& result) override { - TRACE("sine", g->display(tout);); - TRACE("sine", tout << g->size();); - ptr_vector new_forms; - filter_expressions(g, new_forms); - TRACE("sine", tout << new_forms.size();); - g->reset(); - for (unsigned i = 0; i < new_forms.size(); i++) { - g->assert_expr(new_forms.get(i), nullptr, nullptr); - } - g->inc_depth(); - g->updt_prec(goal::OVER); - result.push_back(g.get()); - TRACE("sine", result[0]->display(tout);); - SASSERT(g->is_well_formed()); - } - - void cleanup() override { - } - -private: - - typedef std::pair t_work_item; - - t_work_item work_item(expr * e, expr * root) { - return std::pair(e, root); - } - - void find_constants(expr * e, obj_hashtable &consts) { - ptr_vector stack; - stack.push_back(e); - expr * curr; - while (!stack.empty()) { - curr = stack.back(); - stack.pop_back(); - if (is_app(curr) && is_uninterp(curr)) { - app *a = to_app(curr); - func_decl *f = a->get_decl(); - consts.insert_if_not_there(f); - } - } - } - - bool quantifier_matches(quantifier * q, - obj_hashtable const & consts, - ptr_vector & next_consts) { - TRACE("sine", - tout << "size of consts is "; tout << consts.size(); tout << "\n"; - for (func_decl* f : consts) tout << f->get_name() << "\n";); - - bool matched = false; - for (unsigned i = 0; i < q->get_num_patterns(); i++) { - bool p_matched = true; - ptr_vector stack; - expr * curr; - - // patterns are wrapped with "pattern" - if (!m.is_pattern(q->get_pattern(i), stack)) - continue; - - while (!stack.empty()) { - curr = stack.back(); - stack.pop_back(); - - if (is_app(curr)) { - app * a = to_app(curr); - func_decl * f = a->get_decl(); - if (!consts.contains(f)) { - TRACE("sine", tout << mk_pp(f, m) << "\n";); - p_matched = false; - next_consts.push_back(f); - break; - } - for (unsigned j = 0; j < a->get_num_args(); j++) - stack.push_back(a->get_arg(j)); - } - } - - if (p_matched) { - matched = true; - break; - } - } - - return matched; - } - - void filter_expressions(goal_ref const & g, ptr_vector & new_exprs) { - obj_map > const2exp; - obj_map > exp2const; - obj_map > const2quantifier; - obj_hashtable consts; - vector stack; - t_work_item curr; - - for (unsigned i = 0; i < g->size(); i++) - stack.push_back(work_item(g->form(i), g->form(i))); - - while (!stack.empty()) { - curr = stack.back(); - stack.pop_back(); - if (is_app(curr.first) && is_uninterp(curr.first)) { - app * a = to_app(curr.first); - func_decl * f = a->get_decl(); - if (!consts.contains(f)) { - consts.insert(f); - if (const2quantifier.contains(f)) { - for (auto const& p : const2quantifier[f]) - stack.push_back(p); - const2quantifier.remove(f); - } - } - if (!const2exp.contains(f)) { - const2exp.insert(f, obj_hashtable()); - } - if (!const2exp[f].contains(curr.second)) { - const2exp[f].insert(curr.second); - } - if (!exp2const.contains(curr.second)) { - exp2const.insert(curr.second, obj_hashtable()); - } - if (!exp2const[curr.second].contains(f)) { - exp2const[curr.second].insert(f); - } - - for (unsigned i = 0; i < a->get_num_args(); i++) { - stack.push_back(work_item(a->get_arg(i), curr.second)); - } - } - else if (is_quantifier(curr.first)) { - quantifier *q = to_quantifier(curr.first); - if (is_forall(q)) { - if (q->has_patterns()) { - ptr_vector next_consts; - if (quantifier_matches(q, consts, next_consts)) { - stack.push_back(work_item(q->get_expr(), curr.second)); - } - else { - for (unsigned i = 0; i < next_consts.size(); i++) { - func_decl *c = next_consts.get(i); - if (!const2quantifier.contains(c)) { - const2quantifier.insert(c, obj_pair_hashtable()); - } - if (!const2quantifier[c].contains(curr)) { - const2quantifier[c].insert(curr); - } - } - } - } - else { - stack.push_back(work_item(q->get_expr(), curr.second)); - } - } - else if (is_exists(q)) { - stack.push_back(work_item(q->get_expr(), curr.second)); - } - } - } - - // ok, now we just need to find the connected component of the last term - obj_hashtable visited; - ptr_vector to_visit; - to_visit.push_back(g->form(g->size() - 1)); - expr * visiting; - - while (!to_visit.empty()) { - visiting = to_visit.back(); - to_visit.pop_back(); - visited.insert(visiting); - if (!exp2const.contains(visiting)) - continue; - for (func_decl* f : exp2const[visiting]) - for (expr* e : const2exp[f]) { - if (!visited.contains(e)) - to_visit.push_back(e); - } - } - - for (unsigned i = 0; i < g->size(); i++) { - if (visited.contains(g->form(i))) - new_exprs.push_back(g->form(i)); - } - } -}; - -tactic * mk_sine_tactic(ast_manager & m, params_ref const & p) { - return alloc(sine_tactic, m, p); -} diff --git a/src/tactic/sine_filter.h b/src/tactic/sine_filter.h deleted file mode 100644 index d7e5ed59a..000000000 --- a/src/tactic/sine_filter.h +++ /dev/null @@ -1,30 +0,0 @@ -/*++ -Copyright (c) 2016 Microsoft Corporation - -Module Name: - - sine_filter.h - -Abstract: - - Tactic that performs Sine Qua Non premise selection - -Author: - - Doug Woos - -Revision History: - ---*/ -#pragma once - -#include "util/params.h" -class ast_manager; -class tactic; - -tactic * mk_sine_tactic(ast_manager & m, params_ref const & p = params_ref()); - -/* - ADD_TACTIC("sine-filter", "eliminate premises using Sine Qua Non", "mk_sine_tactic(m, p)") -*/ - diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp index 296fd6886..ed73e21f0 100644 --- a/src/util/mpq.cpp +++ b/src/util/mpq.cpp @@ -260,6 +260,7 @@ void mpq_manager::set(mpq & a, char const * val) { if (exp > 0) { _scoped_numeral> _exp(*this); _scoped_numeral> _qten(*this); + _qten = 10; power(_qten, static_cast(exp), _exp); TRACE("mpq_set", tout << "a: " << to_string(a) << ", exp_sign:" << exp_sign << ", exp: " << exp << " " << to_string(_exp) << std::endl;); if (exp_sign) diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index bebce4273..e20c56234 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -185,8 +185,10 @@ void sexpr::display_atom(std::ostream & out) const { } void sexpr::display(std::ostream & out) const { - if (!is_composite()) + if (!is_composite()) { display_atom(out); + return; + } vector > todo; todo.push_back(std::make_pair(static_cast(this), 0)); while (!todo.empty()) {