From 2e965578270c91cc6bf5d83f7c4d5266ba3f6d2b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Sep 2021 08:55:28 -0700 Subject: [PATCH 01/18] fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bool_rewriter.cpp | 20 ++++++++++++++++++++ src/math/lp/monomial_bounds.cpp | 13 +++++++++++-- src/math/lp/monomial_bounds.h | 1 + 3 files changed, 32 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 101bbd771..1ee0a53b3 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -905,7 +905,26 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re } } +#if 0 + expr* t1, *t2; + // (ite c (not (= t1 t2)) t1) ==> (not (= t1 (and c t2))) + if (m().is_not(t, t1) && m().is_eq(t1, t1, t2) && e == t1) { + expr_ref a(m()); + mk_and(c, t2, a); + result = m().mk_not(m().mk_eq(t1, a)); + return BR_REWRITE2; + } + if (m().is_not(t, t1) && m().is_eq(t1, t2, t1) && e == t1) { + expr_ref a(m()); + mk_and(c, t2, a); + result = m().mk_eq(t1, a); + return BR_REWRITE2; + } +#endif + + if (m().is_ite(t) && m_ite_extra_rules && m_elim_ite) { + std::cout << "extra rules\n"; // (ite c1 (ite c2 t1 t2) t1) ==> (ite (and c1 (not c2)) t2 t1) if (e == to_app(t)->get_arg(1)) { expr_ref not_c2(m()); @@ -923,6 +942,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re return BR_REWRITE1; } + if (m().is_ite(e)) { // (ite c1 (ite c2 t1 t2) (ite c3 t1 t2)) ==> (ite (or (and c1 c2) (and (not c1) c3)) t1 t2) if (to_app(t)->get_arg(1) == to_app(e)->get_arg(1) && diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 89f4b04cf..1ed0956dc 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -24,6 +24,11 @@ namespace nla { } } + bool monomial_bounds::is_too_big(mpq const& q) const { + return rational(q).bitsize() > 256; + } + + /** * Accumulate product of variables in monomial starting at position 'start' */ @@ -51,6 +56,8 @@ namespace nla { lp::explanation ex; dep.get_upper_dep(range, ex); auto const& upper = dep.upper(range); + if (is_too_big(upper)) + return false; auto cmp = dep.upper_is_open(range) ? llc::LT : llc::LE; new_lemma lemma(c(), "propagate value - upper bound of range is below value"); lemma &= ex; @@ -62,6 +69,8 @@ namespace nla { lp::explanation ex; dep.get_lower_dep(range, ex); auto const& lower = dep.lower(range); + if (is_too_big(lower)) + return false; auto cmp = dep.lower_is_open(range) ? llc::GT : llc::GE; new_lemma lemma(c(), "propagate value - lower bound of range is above value"); lemma &= ex; @@ -106,7 +115,7 @@ namespace nla { auto le = dep.upper_is_open(range) ? llc::LT : llc::LE; new_lemma lemma(c(), "propagate value - root case - upper bound of range is below value"); lemma &= ex; - lemma |= ineq(v, le, r); + lemma |= ineq(v, le, r); return true; } if (p % 2 == 0 && val_v.is_neg()) { @@ -114,7 +123,7 @@ namespace nla { auto ge = dep.upper_is_open(range) ? llc::GT : llc::GE; new_lemma lemma(c(), "propagate value - root case - upper bound of range is below negative value"); lemma &= ex; - lemma |= ineq(v, ge, -r); + lemma |= ineq(v, ge, -r); return true; } } diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index e170cf507..236f29bc0 100644 --- a/src/math/lp/monomial_bounds.h +++ b/src/math/lp/monomial_bounds.h @@ -17,6 +17,7 @@ namespace nla { class monomial_bounds : common { dep_intervals& dep; void var2interval(lpvar v, scoped_dep_interval& i); + bool is_too_big(mpq const& q) const; bool propagate_down(monic const& m, lpvar u); bool propagate_value(dep_interval& range, lpvar v); bool propagate_value(dep_interval& range, lpvar v, unsigned power); From 708602dfbb3bbb6d0d225d202a4b129fd90fd703 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Sep 2021 08:56:13 -0700 Subject: [PATCH 02/18] fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bool_rewriter.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 1ee0a53b3..4c2ed7e12 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -924,7 +924,6 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re if (m().is_ite(t) && m_ite_extra_rules && m_elim_ite) { - std::cout << "extra rules\n"; // (ite c1 (ite c2 t1 t2) t1) ==> (ite (and c1 (not c2)) t2 t1) if (e == to_app(t)->get_arg(1)) { expr_ref not_c2(m()); From de20bffafe9e03795253b4a94041fdce37091505 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Sep 2021 11:13:03 -0700 Subject: [PATCH 03/18] import goodies from ps Signed-off-by: Nikolaj Bjorner --- src/util/util.h | 5 +++++ src/util/vector.h | 18 +++++++++++++++++- 2 files changed, 22 insertions(+), 1 deletion(-) diff --git a/src/util/util.h b/src/util/util.h index 3470f59c0..8d3682943 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -269,6 +269,11 @@ public: return *this; } + scoped_ptr& operator=(scoped_ptr&& other) { + *this = other.detach(); + return *this; + }; + T * detach() { T* tmp = m_ptr; m_ptr = nullptr; diff --git a/src/util/vector.h b/src/util/vector.h index 665569c03..1cb25a8c4 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -641,7 +641,7 @@ public: return m_data; } - void swap(vector & other) { + void swap(vector & other) noexcept { std::swap(m_data, other.m_data); } @@ -720,6 +720,17 @@ public: ptr_vector(unsigned s):vector(s) {} ptr_vector(unsigned s, T * elem):vector(s, elem) {} ptr_vector(unsigned s, T * const * data):vector(s, const_cast(data)) {} + std::ostream& display(std::ostream& out, char const* delim = " ") const { + char const* d = ""; + for (auto const* u : *this) { + if (u) + out << d << *u; + else + out << d << ""; + d = delim; + } + return out; + } }; template @@ -746,6 +757,11 @@ inline std::ostream& operator<<(std::ostream& out, svector const& v) { return out; } +template +inline std::ostream& operator<<(std::ostream& out, ptr_vector const& v) { + return v.display(out); +} + template struct vector_hash_tpl { From cabd5b10faa741edc566457c769b822f552609c0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Sep 2021 18:56:55 -0700 Subject: [PATCH 04/18] #5532 --- src/sat/smt/euf_internalize.cpp | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 2302a8935..90a268661 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -13,6 +13,20 @@ Author: Nikolaj Bjorner (nbjorner) 2020-08-25 +Notes: + +(*) From smt_internalizer.cpp + This code is necessary because some theories may decide + not to create theory variables for a nested application. + Example: + Suppose (+ (* 2 x) y) is internalized by arithmetic + and an enode is created for the + and * applications, + but a theory variable is only created for the + application. + The (* 2 x) is internal to the arithmetic module. + Later, the core tries to internalize (f (* 2 x)). + Now, (* 2 x) is not internal to arithmetic anymore, + and a theory variable must be created for it. + --*/ #include "ast/pb_decl_plugin.h" @@ -72,6 +86,12 @@ namespace euf { bool solver::visit(expr* e) { euf::enode* n = m_egraph.find(e); + th_solver* s = nullptr; + if (n && !si.is_bool_op(e) && (s = expr2solver(e), s && euf::null_theory_var == n->get_th_var(s->get_id()))) { + // ensure that theory variables are attached in shared contexts. See notes (*) + s->internalize(e, false); + return true; + } if (n) return true; if (si.is_bool_op(e)) { From 18d1b368d1dde36e6119a008b9c52b271761983e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Sep 2021 20:12:32 -0700 Subject: [PATCH 05/18] #5532 --- src/ast/euf/euf_egraph.cpp | 6 +++++- src/ast/euf/euf_enode.h | 16 ++++++++-------- src/sat/smt/euf_solver.cpp | 5 +++-- 3 files changed, 16 insertions(+), 11 deletions(-) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index fd93ce943..691c42981 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -818,9 +818,13 @@ namespace euf { args.push_back(old_expr2new_enode[n1->get_arg(j)->get_expr_id()]); expr* e2 = tr(e1); enode* n2 = mk(e2, n1->generation(), args.size(), args.data()); + old_expr2new_enode.setx(e1->get_id(), n2, nullptr); - n2->set_value(n2->value()); + n2->set_value(n1->value()); n2->m_bool_var = n1->m_bool_var; + n2->m_commutative = n1->m_commutative; + n2->m_merge_enabled = n1->m_merge_enabled; + n2->m_is_equality = n1->m_is_equality; } for (unsigned i = 0; i < src.m_nodes.size(); ++i) { enode* n1 = src.m_nodes[i]; diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h index 73405b77e..8498c9790 100644 --- a/src/ast/euf/euf_enode.h +++ b/src/ast/euf/euf_enode.h @@ -55,17 +55,17 @@ namespace euf { unsigned m_table_id = UINT_MAX; unsigned m_generation = 0; // Tracks how many quantifier instantiation rounds were needed to generate this enode. enode_vector m_parents; - enode* m_next = nullptr; - enode* m_root = nullptr; - enode* m_target = nullptr; - enode* m_cg = nullptr; + enode* m_next = nullptr; + enode* m_root = nullptr; + enode* m_target = nullptr; + enode* m_cg = nullptr; th_var_list m_th_vars; justification m_justification; unsigned m_num_args = 0; - signed char m_lbl_hash = -1; // It is different from -1, if enode is used in a pattern - approx_set m_lbls; - approx_set m_plbls; - enode* m_args[0]; + signed char m_lbl_hash = -1; // It is different from -1, if enode is used in a pattern + approx_set m_lbls; + approx_set m_plbls; + enode* m_args[0]; friend class enode_args; friend class enode_parents; diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index e10225c9c..53fda2a2f 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -316,6 +316,7 @@ namespace euf { } if (n->is_equality()) { SASSERT(!m.is_iff(e)); + SASSERT(m.is_eq(e)); if (sign) m_egraph.new_diseq(n); else @@ -867,9 +868,9 @@ namespace euf { for (euf::enode* n : r->m_egraph.nodes()) { auto b = n->bool_var(); if (b != sat::null_bool_var) { - m_bool_var2expr.setx(b, n->get_expr(), nullptr); + r->m_bool_var2expr.setx(b, n->get_expr(), nullptr); SASSERT(r->m.is_bool(n->get_sort())); - IF_VERBOSE(11, verbose_stream() << "set bool_var " << r->bpp(n) << "\n"); + IF_VERBOSE(11, verbose_stream() << "set bool_var " << b << " " << r->bpp(n) << " " << mk_bounded_pp(n->get_expr(), m) << "\n"); } } for (auto* s_orig : m_id2solver) { From d174f87c5e3c99bf4eb37ea72249ccf023ded36f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Sep 2021 20:21:23 -0700 Subject: [PATCH 06/18] #5532 --- src/math/subpaving/tactic/expr2subpaving.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/math/subpaving/tactic/expr2subpaving.cpp b/src/math/subpaving/tactic/expr2subpaving.cpp index ba7bf3546..3afbc1ecb 100644 --- a/src/math/subpaving/tactic/expr2subpaving.cpp +++ b/src/math/subpaving/tactic/expr2subpaving.cpp @@ -19,9 +19,10 @@ Notes: --*/ #include "math/subpaving/tactic/expr2subpaving.h" #include "ast/expr2var.h" +#include "ast/arith_decl_plugin.h" +#include "ast/ast_pp.h" #include "util/ref_util.h" #include "util/z3_exception.h" -#include "ast/arith_decl_plugin.h" #include "util/scoped_numeral_buffer.h" #include "util/common_msgs.h" @@ -309,6 +310,10 @@ struct expr2subpaving::imp { case OP_MOD: case OP_REM: case OP_IRRATIONAL_ALGEBRAIC_NUM: + case OP_DIV0: + case OP_REM0: + case OP_MOD0: + case OP_IDIV0: throw default_exception("you must apply arithmetic purifier before internalizing expressions into the subpaving module."); case OP_SIN: case OP_COS: @@ -325,6 +330,7 @@ struct expr2subpaving::imp { // TODO throw default_exception("transcendental and hyperbolic functions are not supported yet."); default: + throw default_exception("unhandled arithmetic operator in subpaving"); UNREACHABLE(); } return subpaving::null_var; From 1dcbd2d86cfe5e4dfb24e71dc74600470dd97873 Mon Sep 17 00:00:00 2001 From: Kartik Singhal Date: Sat, 25 Sep 2021 11:04:06 -0500 Subject: [PATCH 07/18] Correct capitalization of package (#5569) See https://stackoverflow.com/a/50004273/1167061 --- examples/ml/README | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/ml/README b/examples/ml/README index a8d03eaea..953a270fe 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 -thread -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 -thread -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 From 6c71baf77b91a0972276f462922f9308009bfd3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Sep 2021 03:45:45 -0700 Subject: [PATCH 08/18] lifting iff to binary --- src/sat/smt/euf_solver.cpp | 4 +-- src/sat/smt/q_ematch.cpp | 65 +++++++++++++++++++++++--------------- src/sat/smt/q_ematch.h | 1 + src/sat/smt/q_eval.cpp | 4 +-- src/sat/smt/q_solver.cpp | 8 +++++ 5 files changed, 51 insertions(+), 31 deletions(-) diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 53fda2a2f..753ec37da 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -488,10 +488,8 @@ namespace euf { return sat::check_result::CR_CONTINUE; if (m_qsolver) apply_solver(m_qsolver); - if (num_nodes < m_egraph.num_nodes()) { - IF_VERBOSE(1, verbose_stream() << "new nodes created, but not detected\n"); + if (num_nodes < m_egraph.num_nodes()) return sat::check_result::CR_CONTINUE; - } TRACE("after_search", s().display(tout);); if (give_up) return sat::check_result::CR_GIVEUP; diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index 2e779cb80..096999572 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -427,33 +427,11 @@ namespace q { expr_ref body(mk_not(m, q->get_expr()), m); q = m.update_quantifier(q, forall_k, body); } - expr_ref_vector ors(m); + expr_ref_vector ors(m); flatten_or(q->get_expr(), ors); - for (expr* arg : ors) { - bool sign = m.is_not(arg, arg); - expr* l, *r; - if (m.is_distinct(arg) && to_app(arg)->get_num_args() == 2) { - l = to_app(arg)->get_arg(0); - r = to_app(arg)->get_arg(1); - sign = !sign; - } - else if (!m.is_eq(arg, l, r) || is_ground(arg)) { - l = arg; - 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)); - } + for (expr* arg : ors) + cl->m_lits.push_back(clausify_literal(arg)); + if (q->get_num_patterns() == 0) { expr_ref tmp(m); m_infer_patterns(q, tmp); @@ -468,6 +446,41 @@ namespace q { return cl; } + lit ematch::clausify_literal(expr* arg) { + bool sign = m.is_not(arg, arg); + expr* _l, *_r; + expr_ref l(m), r(m); + + // convert into equality or equivalence + if (m.is_distinct(arg) && to_app(arg)->get_num_args() == 2) { + l = to_app(arg)->get_arg(0); + r = to_app(arg)->get_arg(1); + sign = !sign; + } + else if (!is_ground(arg) && m.is_eq(arg, _l, _r)) { + l = _l; + r = _r; + } + else { + l = arg; + r = sign ? m.mk_false() : m.mk_true(); + sign = false; + } + + // convert Boolean disequalities into equality + 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; + } + return lit(l, r, sign); + } + /** * Attach ground subterms of patterns so they appear shared. */ diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h index 9c4cf9d98..e871a6077 100644 --- a/src/sat/smt/q_ematch.h +++ b/src/sat/smt/q_ematch.h @@ -112,6 +112,7 @@ namespace q { void attach_ground_pattern_terms(expr* pat); clause* clausify(quantifier* q); + lit clausify_literal(expr* arg); fingerprint* add_fingerprint(clause& c, binding& b, unsigned max_generation); void set_tmp_binding(fingerprint& fp); diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp index 600dcd2c5..200b05ec9 100644 --- a/src/sat/smt/q_eval.cpp +++ b/src/sat/smt/q_eval.cpp @@ -171,10 +171,10 @@ namespace q { } 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)) return m_eval[e->get_id()]; + if (is_ground(e)) + return ctx.get_egraph().find(e); ptr_buffer todo; ptr_buffer args; todo.push_back(e); diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 0f3eaf3d3..4727dfefa 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -232,6 +232,14 @@ namespace q { else UNREACHABLE(); + expr* a, *b; + if (m_expanded.size() == 1 && m.is_iff(m_expanded.get(0), a, b)) { + expr_ref f1(m.mk_implies(a, b), m); + expr_ref f2(m.mk_implies(b, a), m); + m_expanded.reset(); + m_expanded.push_back(f1); + m_expanded.push_back(f2); + } if (m_expanded.size() > 1) { for (unsigned i = m_expanded.size(); i-- > 0; ) { expr_ref tmp(m.update_quantifier(q, m_expanded.get(i)), m); From 3abecc34282107c5be45c9fb3e23aad6ac2b57b3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Sep 2021 14:19:43 -0700 Subject: [PATCH 09/18] add extra commands to API parser --- src/api/api_parsers.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index aeb1e3d3f..c40e0ccf3 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -23,8 +23,12 @@ Revision History: #include "api/api_ast_vector.h" #include "cmd_context/cmd_context.h" #include "smt/smt_solver.h" +#include "smt/smt2_extra_cmds.h" #include "parsers/smt2/smt2parser.h" #include "solver/solver_na2as.h" +#include "muz/fp/dl_cmds.h" +#include "opt/opt_cmds.h" + extern "C" { @@ -42,6 +46,10 @@ extern "C" { Z3_TRY; ast_manager& m = mk_c(c)->m(); scoped_ptr ctx = alloc(cmd_context, false, &(m)); + install_dl_cmds(*ctx.get()); + install_opt_cmds(*ctx.get()); + install_smt2_extra_cmds(*ctx.get()); + ctx->register_plist(); ctx->set_ignore_check(true); Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), m); From 2e176a0e02f164dbd27c0260b183f47eb15b045c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Sep 2021 08:27:46 -0700 Subject: [PATCH 10/18] count lazy bindings --- src/sat/smt/q_ematch.cpp | 2 ++ src/sat/smt/q_ematch.h | 1 + 2 files changed, 3 insertions(+) diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index 096999572..cb5144a2b 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -240,6 +240,7 @@ namespace q { b->m_nodes[i] = _binding[i]; binding::push_to_front(c.m_bindings, b); ctx.push(remove_binding(ctx, c, b)); + ++m_stats.m_num_delayed_bindings; } void ematch::on_binding(quantifier* q, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_gen, unsigned max_gen) { @@ -612,6 +613,7 @@ namespace q { st.update("q redundant", m_stats.m_num_redundant); st.update("q units", m_stats.m_num_propagations); st.update("q conflicts", m_stats.m_num_conflicts); + st.update("q delayed bindings", m_stats.m_num_delayed_bindings); } std::ostream& ematch::display(std::ostream& out) const { diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h index e871a6077..41e844572 100644 --- a/src/sat/smt/q_ematch.h +++ b/src/sat/smt/q_ematch.h @@ -41,6 +41,7 @@ namespace q { unsigned m_num_propagations; unsigned m_num_conflicts; unsigned m_num_redundant; + unsigned m_num_delayed_bindings; stats() { reset(); } From 92c1b600c3916c3c595366982ffbbe491a2f8eb5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Sep 2021 09:55:49 -0700 Subject: [PATCH 11/18] tuning eval --- src/ast/euf/euf_egraph.cpp | 45 ++++++++++++++++++++++++++------------ src/ast/euf/euf_egraph.h | 5 ++++- src/sat/smt/q_eval.cpp | 19 +++++++++++++--- src/sat/smt/q_eval.h | 1 + 4 files changed, 52 insertions(+), 18 deletions(-) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 691c42981..4e8e7327f 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -129,7 +129,7 @@ namespace euf { return n; } - egraph::egraph(ast_manager& m) : m(m), m_table(m), m_tmp_app(2), m_exprs(m) { + egraph::egraph(ast_manager& m) : m(m), m_table(m), m_tmp_app(2), m_exprs(m), m_eq_decls(m) { m_tmp_eq = enode::mk_tmp(m_region, 2); } @@ -592,7 +592,7 @@ namespace euf { SASSERT(!n1->get_root()->m_target); } - bool egraph::are_diseq(enode* a, enode* b) const { + bool egraph::are_diseq(enode* a, enode* b) { enode* ra = a->get_root(), * rb = b->get_root(); if (ra == rb) return false; @@ -600,12 +600,16 @@ namespace euf { return true; if (ra->get_sort() != rb->get_sort()) return true; - expr_ref eq(m.mk_eq(a->get_expr(), b->get_expr()), m); - m_tmp_eq->m_args[0] = a; - m_tmp_eq->m_args[1] = b; - m_tmp_eq->m_expr = eq; - SASSERT(m_tmp_eq->num_args() == 2); - enode* r = m_table.find(m_tmp_eq); + if (ra->num_parents() > rb->num_parents()) + std::swap(ra, rb); + if (ra->num_parents() <= 3) { + for (enode* p : enode_parents(ra)) + if (p->is_equality() && p->get_root()->value() == l_false && + (rb == p->get_arg(0)->get_root() || rb == p->get_arg(1)->get_root())) + return true; + return false; + } + enode* r = tmp_eq(ra, rb); if (r && r->get_root()->value() == l_false) return true; return false; @@ -617,6 +621,24 @@ namespace euf { return find(m_tmp_app.get_app(), num_args, args); } + enode* egraph::tmp_eq(enode* a, enode* b) { + func_decl* f = nullptr; + for (unsigned i = m_eq_decls.size(); i-- > 0; ) { + auto e = m_eq_decls.get(i); + if (e->get_domain(0) == a->get_sort()) { + f = e; + break; + } + } + if (!f) { + app_ref eq(m.mk_eq(a->get_expr(), b->get_expr()), m); + m_eq_decls.push_back(eq->get_decl()); + f = eq->get_decl(); + } + enode* args[2] = { a, b }; + return get_enode_eq_to(f, 2, args); + } + /** \brief generate an explanation for a congruence. Each pair of children under a congruence have the same roots @@ -714,12 +736,7 @@ namespace euf { explain_eq(justifications, b, rb); return sat::null_bool_var; } - expr_ref eq(m.mk_eq(a->get_expr(), b->get_expr()), m); - m_tmp_eq->m_args[0] = a; - m_tmp_eq->m_args[1] = b; - m_tmp_eq->m_expr = eq; - SASSERT(m_tmp_eq->num_args() == 2); - enode* r = m_table.find(m_tmp_eq); + enode* r = tmp_eq(a, b); SASSERT(r && r->get_root()->value() == l_false); explain_eq(justifications, r, r->get_root()); return r->get_root()->bool_var(); diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index 5c828678e..7c1f9e566 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -165,6 +165,7 @@ namespace euf { tmp_app m_tmp_app; enode_vector m_nodes; expr_ref_vector m_exprs; + func_decl_ref_vector m_eq_decls; vector m_decl2enodes; enode_vector m_empty_enodes; unsigned m_num_scopes = 0; @@ -263,10 +264,12 @@ namespace euf { /** * \brief check if two nodes are known to be disequal. */ - bool are_diseq(enode* a, enode* b) const; + bool are_diseq(enode* a, enode* b); enode* get_enode_eq_to(func_decl* f, unsigned num_args, enode* const* args); + enode* tmp_eq(enode* a, enode* b); + /** \brief Maintain and update cursor into propagated consequences. The result of get_literal() is a pair (n, is_eq) diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp index 200b05ec9..c506a52f7 100644 --- a/src/sat/smt/q_eval.cpp +++ b/src/sat/smt/q_eval.cpp @@ -25,7 +25,10 @@ namespace q { struct eval::scoped_mark_reset { eval& e; scoped_mark_reset(eval& e): e(e) {} - ~scoped_mark_reset() { e.m_mark.reset(); } + ~scoped_mark_reset() { + e.m_mark.reset(); + e.m_diseq_undef = euf::enode_pair(); + } }; eval::eval(euf::solver& ctx): @@ -97,12 +100,18 @@ namespace q { if (sn && sn == tn) return l_true; + if (sn && sn == m_diseq_undef.first && tn == m_diseq_undef.second) + return l_undef; + if (sn && tn && ctx.get_egraph().are_diseq(sn, tn)) { evidence.push_back(euf::enode_pair(sn, tn)); return l_false; } - if (sn && tn) + if (sn && tn) { + m_diseq_undef = euf::enode_pair(sn, tn); return l_undef; + } + if (!sn && !tn) return compare_rec(n, binding, s, t, evidence); @@ -115,7 +124,11 @@ namespace q { std::swap(t, s); } unsigned sz = evidence.size(); - for (euf::enode* t1 : euf::enode_class(tn)) { + unsigned count = 0; + for (euf::enode* t1 : euf::enode_class(tn)) { + if (!t1->is_cgr()) + continue; + ++count; expr* t2 = t1->get_expr(); if ((c = compare_rec(n, binding, s, t2, evidence), c != l_undef)) { evidence.push_back(euf::enode_pair(t1, tn)); diff --git a/src/sat/smt/q_eval.h b/src/sat/smt/q_eval.h index 0ead01061..76c219343 100644 --- a/src/sat/smt/q_eval.h +++ b/src/sat/smt/q_eval.h @@ -31,6 +31,7 @@ namespace q { euf::enode_vector m_eval; euf::enode_vector m_indirect_nodes; bool m_freeze_swap = false; + euf::enode_pair m_diseq_undef; struct scoped_mark_reset; From da124e42759ab4fb93e69f9bb49899d3d21fb8a3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Sep 2021 13:41:37 -0700 Subject: [PATCH 12/18] tune q-eval and q-ematch Signed-off-by: Nikolaj Bjorner --- src/ast/has_free_vars.cpp | 15 +++- src/ast/has_free_vars.h | 9 +++ src/ast/normal_forms/pull_quant.cpp | 14 ++-- src/sat/smt/q_eval.cpp | 2 +- src/sat/smt/q_eval.h | 2 + src/sat/smt/q_solver.cpp | 107 ++++++++++++++++++++-------- src/sat/smt/q_solver.h | 6 +- 7 files changed, 119 insertions(+), 36 deletions(-) diff --git a/src/ast/has_free_vars.cpp b/src/ast/has_free_vars.cpp index 09d6d7740..b1b74c7da 100644 --- a/src/ast/has_free_vars.cpp +++ b/src/ast/has_free_vars.cpp @@ -18,9 +18,10 @@ Revision History: --*/ #include "ast/ast.h" #include "ast/expr_delta_pair.h" +#include "ast/has_free_vars.h" #include "util/hashtable.h" -class contains_vars { +class contains_vars::imp { typedef hashtable, default_eq > cache; cache m_cache; svector m_todo; @@ -86,6 +87,18 @@ public: } }; +contains_vars::contains_vars() { + m_imp = alloc(imp); +} + +contains_vars::~contains_vars() { + dealloc(m_imp); +} + +bool contains_vars::operator()(expr* e) { + return (*m_imp)(e); +} + bool has_free_vars(expr * n) { contains_vars p; return p(n); diff --git a/src/ast/has_free_vars.h b/src/ast/has_free_vars.h index c1cbfa0e6..1f7cc62a3 100644 --- a/src/ast/has_free_vars.h +++ b/src/ast/has_free_vars.h @@ -20,6 +20,15 @@ Revision History: class expr; +class contains_vars { + class imp; + imp* m_imp; +public: + contains_vars(); + ~contains_vars(); + bool operator()(expr* n); +}; + bool has_free_vars(expr * n); diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp index 8a94a3482..486f4e949 100644 --- a/src/ast/normal_forms/pull_quant.cpp +++ b/src/ast/normal_forms/pull_quant.cpp @@ -20,6 +20,7 @@ Notes: #include "ast/rewriter/var_subst.h" #include "ast/rewriter/rewriter_def.h" #include "ast/ast_pp.h" +#include "ast/ast_util.h" struct pull_quant::imp { @@ -50,7 +51,7 @@ struct pull_quant::imp { quantifier * q = to_quantifier(child); expr * body = q->get_expr(); quantifier_kind k = q->get_kind() == forall_k ? exists_k : forall_k; - result = m.update_quantifier(q, k, m.mk_not(body)); + result = m.update_quantifier(q, k, mk_not(m, body)); return true; } else { @@ -78,9 +79,8 @@ struct pull_quant::imp { qid = nested_q->get_qid(); } w = std::min(w, nested_q->get_weight()); - unsigned j = nested_q->get_num_decls(); - while (j > 0) { - --j; + + for (unsigned j = nested_q->get_num_decls(); j-- > 0; ) { var_sorts.push_back(nested_q->get_decl_sort(j)); symbol s = nested_q->get_decl_name(j); if (std::find(var_names.begin(), var_names.end(), s) != var_names.end()) @@ -254,6 +254,10 @@ struct pull_quant::imp { } br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + if (m.is_not(f) && m.is_not(args[0])) { + result = to_app(args[0])->get_arg(0); + return BR_REWRITE1; + } if (!m.is_or(f) && !m.is_and(f) && !m.is_not(f)) return BR_FAILED; @@ -275,7 +279,7 @@ struct pull_quant::imp { proof_ref & result_pr) { if (is_exists(old_q)) { - result = m.mk_not(new_body); + result = mk_not(m, new_body); result = m.mk_not(m.update_quantifier(old_q, forall_k, result)); if (m.proofs_enabled()) m.mk_rewrite(old_q, result); diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp index c506a52f7..a01bb9d9d 100644 --- a/src/sat/smt/q_eval.cpp +++ b/src/sat/smt/q_eval.cpp @@ -198,7 +198,7 @@ namespace q { todo.pop_back(); continue; } - if (is_ground(t) || (has_quantifiers(t) && !has_free_vars(t))) { + if (is_ground(t) || (has_quantifiers(t) && !m_contains_vars(t))) { m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr); if (!m_eval[t->get_id()]) return nullptr; diff --git a/src/sat/smt/q_eval.h b/src/sat/smt/q_eval.h index 76c219343..ef016407a 100644 --- a/src/sat/smt/q_eval.h +++ b/src/sat/smt/q_eval.h @@ -16,6 +16,7 @@ Author: --*/ #pragma once +#include "ast/has_free_vars.h" #include "sat/smt/q_clause.h" namespace euf { @@ -32,6 +33,7 @@ namespace q { euf::enode_vector m_indirect_nodes; bool m_freeze_swap = false; euf::enode_pair m_diseq_undef; + contains_vars m_contains_vars; struct scoped_mark_reset; diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 4727dfefa..480853dbd 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -30,7 +30,8 @@ namespace q { th_euf_solver(ctx, ctx.get_manager().get_family_name(fid), fid), m_mbqi(ctx, *this), m_ematch(ctx, *this), - m_expanded(ctx.get_manager()) + m_expanded(ctx.get_manager()), + m_der(ctx.get_manager()) { } @@ -45,25 +46,22 @@ namespace q { add_clause(~l, lit); ctx.add_root(~l, lit); } - else { - 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); + else if (expand(q)) { + for (expr* e : m_expanded) { + sat::literal lit = ctx.internalize(e, 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); - } + } + 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++; } @@ -223,8 +221,16 @@ namespace q { return val; } - expr_ref_vector const& solver::expand(quantifier* q) { + bool solver::expand(quantifier* q) { + expr_ref r(m); + proof_ref pr(m); + m_der(q, r, pr); m_expanded.reset(); + if (r != q) { + ctx.get_rewriter()(r); + m_expanded.push_back(r); + return true; + } if (is_forall(q)) flatten_and(q->get_expr(), m_expanded); else if (is_exists(q)) @@ -232,13 +238,31 @@ namespace q { else UNREACHABLE(); - expr* a, *b; - if (m_expanded.size() == 1 && m.is_iff(m_expanded.get(0), a, b)) { - expr_ref f1(m.mk_implies(a, b), m); - expr_ref f2(m.mk_implies(b, a), m); + if (m_expanded.size() == 1 && is_forall(q)) { m_expanded.reset(); - m_expanded.push_back(f1); - m_expanded.push_back(f2); + flatten_or(q->get_expr(), m_expanded); + expr_ref split1(m), split2(m), e1(m), e2(m); + unsigned idx = 0; + for (unsigned i = m_expanded.size(); i-- > 0; ) { + expr* arg = m_expanded.get(i); + if (split(arg, split1, split2)) { + if (e1) + return false; + e1 = split1; + e2 = split2; + idx = i; + } + } + if (!e1) + return false; + + m_expanded[idx] = e1; + e1 = mk_or(m_expanded); + m_expanded[idx] = e2; + e2 = mk_or(m_expanded); + m_expanded.reset(); + m_expanded.push_back(e1); + m_expanded.push_back(e2); } if (m_expanded.size() > 1) { for (unsigned i = m_expanded.size(); i-- > 0; ) { @@ -246,12 +270,39 @@ namespace q { ctx.get_rewriter()(tmp); m_expanded[i] = tmp; } + return true; } - else { - m_expanded.reset(); - m_expanded.push_back(q); + return false; + } + + bool solver::split(expr* arg, expr_ref& e1, expr_ref& e2) { + expr* x, * y, * z; + if (m.is_not(arg, x) && m.is_or(x, y, z) && is_literal(y) && is_literal(z)) { + e1 = mk_not(m, y); + e2 = mk_not(m, z); + return true; } - return m_expanded; + if (m.is_iff(arg, x, y) && is_literal(x) && is_literal(y)) { + e1 = m.mk_implies(x, y); + e2 = m.mk_implies(y, x); + return true; + } + if (m.is_and(arg, x, y) && is_literal(x) && is_literal(y)) { + e1 = x; + e2 = y; + return true; + } + if (m.is_not(arg, z) && m.is_iff(z, x, y) && is_literal(x) && is_literal(y)) { + e1 = m.mk_or(x, y); + e2 = m.mk_or(mk_not(m, x), mk_not(m, y)); + return true; + } + return false; + } + + bool solver::is_literal(expr* arg) { + m.is_not(arg, arg); + return !m.is_and(arg) && !m.is_or(arg) && !m.is_iff(arg) && !m.is_implies(arg); } void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) { diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h index 426104c87..934864669 100644 --- a/src/sat/smt/q_solver.h +++ b/src/sat/smt/q_solver.h @@ -18,6 +18,7 @@ Author: #include "util/obj_hashtable.h" #include "ast/ast_trail.h" +#include "ast/rewriter/der.h" #include "sat/smt/sat_th.h" #include "sat/smt/q_mbi.h" #include "sat/smt/q_ematch.h" @@ -47,6 +48,7 @@ namespace q { sat::literal_vector m_universal; obj_map m_unit_table; expr_ref_vector m_expanded; + der_rewriter m_der; sat::literal instantiate(quantifier* q, bool negate, std::function& mk_var); sat::literal skolemize(quantifier* q); @@ -54,7 +56,9 @@ namespace q { void init_units(); expr* get_unit(sort* s); - expr_ref_vector const& expand(quantifier* q); + bool expand(quantifier* q); + bool split(expr* arg, expr_ref& e1, expr_ref& e2); + bool is_literal(expr* arg); friend class ematch; From 67ae75bac715229378a7c26911e21b9e4aca6e6e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Sep 2021 14:27:46 -0700 Subject: [PATCH 13/18] fix tmp_eq Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_egraph.cpp | 39 ++++++++++++++------------------------ 1 file changed, 14 insertions(+), 25 deletions(-) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 4e8e7327f..ba29d2dd8 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -600,15 +600,6 @@ namespace euf { return true; if (ra->get_sort() != rb->get_sort()) return true; - if (ra->num_parents() > rb->num_parents()) - std::swap(ra, rb); - if (ra->num_parents() <= 3) { - for (enode* p : enode_parents(ra)) - if (p->is_equality() && p->get_root()->value() == l_false && - (rb == p->get_arg(0)->get_root() || rb == p->get_arg(1)->get_root())) - return true; - return false; - } enode* r = tmp_eq(ra, rb); if (r && r->get_root()->value() == l_false) return true; @@ -622,21 +613,15 @@ namespace euf { } enode* egraph::tmp_eq(enode* a, enode* b) { - func_decl* f = nullptr; - for (unsigned i = m_eq_decls.size(); i-- > 0; ) { - auto e = m_eq_decls.get(i); - if (e->get_domain(0) == a->get_sort()) { - f = e; - break; - } - } - if (!f) { - app_ref eq(m.mk_eq(a->get_expr(), b->get_expr()), m); - m_eq_decls.push_back(eq->get_decl()); - f = eq->get_decl(); - } - enode* args[2] = { a, b }; - return get_enode_eq_to(f, 2, args); + SASSERT(a->is_root()); + SASSERT(b->is_root()); + if (a->num_parents() > b->num_parents()) + std::swap(a, b); + for (enode* p : enode_parents(a)) + if (p->is_equality() && + (b == p->get_arg(0)->get_root() || b == p->get_arg(1)->get_root())) + return p; + return nullptr; } /** @@ -736,7 +721,11 @@ namespace euf { explain_eq(justifications, b, rb); return sat::null_bool_var; } - enode* r = tmp_eq(a, b); + enode* r = tmp_eq(ra, rb); + if (!r) { + std::cout << bpp(a) << " " << bpp(b) << "\n"; + display(std::cout); + } SASSERT(r && r->get_root()->value() == l_false); explain_eq(justifications, r, r->get_root()); return r->get_root()->bool_var(); From 137e5c52633c5c8f6daf014cff3a59f715e3aaaa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Sep 2021 14:28:41 -0700 Subject: [PATCH 14/18] fix tmp_eq Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_egraph.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index ba29d2dd8..f5ad2a6f4 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -722,10 +722,6 @@ namespace euf { return sat::null_bool_var; } enode* r = tmp_eq(ra, rb); - if (!r) { - std::cout << bpp(a) << " " << bpp(b) << "\n"; - display(std::cout); - } SASSERT(r && r->get_root()->value() == l_false); explain_eq(justifications, r, r->get_root()); return r->get_root()->bool_var(); From 62fd22f55595cbf08e6bcea366496d300618c465 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 Sep 2021 09:33:46 -0700 Subject: [PATCH 15/18] disable macro finder tactic if there are recursive functions fix #5574 --- src/sat/smt/array_model.cpp | 1 - src/sat/smt/q_mam.cpp | 1 - src/tactic/ufbv/macro_finder_tactic.cpp | 7 +++++++ 3 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp index 0fbc4364a..33ad8e484 100644 --- a/src/sat/smt/array_model.cpp +++ b/src/sat/smt/array_model.cpp @@ -120,7 +120,6 @@ namespace array { bool solver::must_have_different_model_values(theory_var v1, theory_var v2) { euf::enode* else1 = nullptr, * else2 = nullptr; euf::enode* n1 = var2enode(v1), *n2 = var2enode(v2); - euf::enode* r1 = n1->get_root(), * r2 = n2->get_root(); expr* e1 = n1->get_expr(); if (!a.is_array(e1)) return true; diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index b1432a5ee..7999ecea9 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -2070,7 +2070,6 @@ namespace q { enode * n = m_registers[j2->m_reg]->get_root(); if (n->num_parents() == 0) return nullptr; - unsigned num_args = n->num_args(); enode_vector * v = mk_enode_vector(); for (enode* p : euf::enode_parents(n)) { if (p->get_decl() == j2->m_decl && diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index 2c0a529e6..86c606538 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -17,6 +17,7 @@ Notes: --*/ #include "tactic/tactical.h" +#include "ast/recfun_decl_plugin.h" #include "ast/macros/macro_manager.h" #include "ast/macros/macro_finder.h" #include "tactic/generic_model_converter.h" @@ -42,6 +43,12 @@ class macro_finder_tactic : public tactic { tactic_report report("macro-finder", *g); TRACE("macro-finder", g->display(tout);); + recfun::util rec(m()); + if (!rec.get_rec_funs().empty()) { + result.push_back(g.get()); + return; + } + bool produce_proofs = g->proofs_enabled(); bool unsat_core_enabled = g->unsat_core_enabled(); macro_manager mm(m_manager); From ff723f15ffcf83eebede32d3bf2d25833b7f73cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 Sep 2021 12:19:02 -0700 Subject: [PATCH 16/18] Update z3++.h --- src/api/c++/z3++.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 754f78857..f0c0cc3aa 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3927,7 +3927,7 @@ namespace z3 { user_propagator_base(solver* s): s(s), c(nullptr) { Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh); - } + } virtual void push() = 0; virtual void pop(unsigned num_scopes) = 0; @@ -3948,13 +3948,13 @@ namespace z3 { that were created using a solver. */ - void fixed(fixed_eh_t& f) { + void register_fixed(fixed_eh_t& f) { assert(s); m_fixed_eh = f; Z3_solver_propagate_fixed(ctx(), *s, fixed_eh); } - void eq(eq_eh_t& f) { + void register_eq(eq_eh_t& f) { assert(s); m_eq_eh = f; Z3_solver_propagate_eq(ctx(), *s, eq_eh); From cbe7dd4a48780db2268ec52a60b880af3a21ea48 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 Sep 2021 14:26:09 -0700 Subject: [PATCH 17/18] missing continue fixes unsound sat result from #5573 --- src/sat/smt/euf_solver.cpp | 2 ++ src/sat/smt/q_ematch.cpp | 4 +++- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 753ec37da..3c3b6e884 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -490,6 +490,8 @@ namespace euf { apply_solver(m_qsolver); if (num_nodes < m_egraph.num_nodes()) return sat::check_result::CR_CONTINUE; + if (cont) + return sat::check_result::CR_CONTINUE; TRACE("after_search", s().display(tout);); if (give_up) return sat::check_result::CR_GIVEUP; diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index cb5144a2b..2d8ac8afd 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -605,7 +605,9 @@ namespace q { } if (propagate(true)) return true; - return m_inst_queue.lazy_propagate(); + if (m_inst_queue.lazy_propagate()) + return true; + return false; } void ematch::collect_statistics(statistics& st) const { From 8a85cfdb128b1426c3e6bb5be20dc987e64a2e37 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Sep 2021 09:32:04 -0700 Subject: [PATCH 18/18] fix #5579 - It is only possible to reach this case when new assertions are created. --- src/smt/theory_special_relations.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 4a8070927..78d5984e5 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -325,14 +325,12 @@ namespace smt { ); continue; } - expr_ref f_app(m.mk_app(f, arg1, arg2), m); + expr_ref f_app(m.mk_app(f, arg1, arg2), m); ensure_enode(f_app); literal f_lit = ctx.get_literal(f_app); switch (ctx.get_assignment(f_lit)) { case l_true: - UNREACHABLE(); - // it should already be the case that v1 and reach v2 in the graph. - // whenever f(n1, n2) is asserted. + SASSERT(new_assertion); break; case l_false: { //