diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index f5249ab31..73df52762 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -189,10 +189,10 @@ namespace euf { add_th_diseq(id, v1, v2, n->get_expr()); return; } - for (auto p : euf::enode_th_vars(r1)) { + for (auto const& p : euf::enode_th_vars(r1)) { if (!th_propagates_diseqs(p.get_id())) continue; - for (auto q : euf::enode_th_vars(r2)) + for (auto const& q : euf::enode_th_vars(r2)) if (p.get_id() == q.get_id()) add_th_diseq(p.get_id(), p.get_var(), q.get_var(), n->get_expr()); } @@ -506,7 +506,7 @@ namespace euf { void egraph::merge_th_eq(enode* n, enode* root) { SASSERT(n != root); - for (auto iv : enode_th_vars(n)) { + for (auto const& iv : enode_th_vars(n)) { theory_id id = iv.get_id(); theory_var v = root->get_th_var(id); if (v == null_theory_var) { @@ -789,7 +789,7 @@ namespace euf { out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << (n->merge_tf()?"":" no merge") << "] "; if (n->has_th_vars()) { out << "[t"; - for (auto v : enode_th_vars(n)) + for (auto const& v : enode_th_vars(n)) out << " " << v.get_id() << ":" << v.get_var(); out << "] "; } diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h index 759c85fae..76c74f93d 100644 --- a/src/sat/smt/arith_solver.h +++ b/src/sat/smt/arith_solver.h @@ -445,6 +445,7 @@ namespace arith { bool is_shared(theory_var v) const override; lbool get_phase(bool_var v) override; bool include_func_interp(func_decl* f) const override; + bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_add(n->get_expr()); } // bounds and equality propagation callbacks lp::lar_solver& lp() { return *m_solver; } diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index 1e596bec1..dbcbb36df 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -261,7 +261,8 @@ namespace array { bool is_shared(theory_var v) const override; bool enable_self_propagate() const override { return true; } void relevant_eh(euf::enode* n) override; - + bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_array(n->get_sort()); } + void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2); void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {} void unmerge_eh(theory_var v1, theory_var v2) {} diff --git a/src/sat/smt/euf_ackerman.cpp b/src/sat/smt/euf_ackerman.cpp index c26835f99..c8639e302 100644 --- a/src/sat/smt/euf_ackerman.cpp +++ b/src/sat/smt/euf_ackerman.cpp @@ -99,14 +99,38 @@ namespace euf { m_tmp_inference->init(m_tmp_inference); } + bool ackerman::enable_cc(app* a, app* b) { + if (!s.enable_ackerman_axioms(a)) + return false; + if (!s.enable_ackerman_axioms(b)) + return false; + for (expr* arg : *a) + if (!s.enable_ackerman_axioms(arg)) + return false; + for (expr* arg : *b) + if (!s.enable_ackerman_axioms(arg)) + return false; + return true; + } + + bool ackerman::enable_eq(expr* a, expr* b, expr* c) { + return s.enable_ackerman_axioms(a) && + s.enable_ackerman_axioms(b) && + s.enable_ackerman_axioms(c); + } + void ackerman::cg_conflict_eh(expr * n1, expr * n2) { if (!is_app(n1) || !is_app(n2)) return; + if (!s.enable_ackerman_axioms(n1)) + return; SASSERT(!s.m_drating); app* a = to_app(n1); app* b = to_app(n2); if (a->get_decl() != b->get_decl() || a->get_num_args() != b->get_num_args()) return; + if (!enable_cc(a, b)) + return; TRACE("ack", tout << "conflict eh: " << mk_pp(a, m) << " == " << mk_pp(b, m) << "\n";); insert(a, b); gc(); @@ -117,6 +141,8 @@ namespace euf { return; if (s.m_drating) return; + if (!enable_eq(a, b, c)) + return; TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << " " << mk_pp(c, m) << "\n";); insert(a, b, c); gc(); @@ -128,6 +154,8 @@ namespace euf { TRACE("ack", tout << "used cc: " << mk_pp(a, m) << " == " << mk_pp(b, m) << "\n";); SASSERT(a->get_decl() == b->get_decl()); SASSERT(a->get_num_args() == b->get_num_args()); + if (!enable_cc(a, b)) + return; insert(a, b); gc(); } @@ -173,7 +201,7 @@ namespace euf { app* b = to_app(_b); TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << "\n";); sat::literal_vector lits; - unsigned sz = a->get_num_args(); + unsigned sz = a->get_num_args(); for (unsigned i = 0; i < sz; ++i) { expr_ref eq = s.mk_eq(a->get_arg(i), b->get_arg(i)); diff --git a/src/sat/smt/euf_ackerman.h b/src/sat/smt/euf_ackerman.h index 7b9c4c3d9..479ad2933 100644 --- a/src/sat/smt/euf_ackerman.h +++ b/src/sat/smt/euf_ackerman.h @@ -70,6 +70,9 @@ namespace euf { void add_cc(expr* a, expr* b); void add_eq(expr* a, expr* b, expr* c); void gc(); + bool enable_cc(app* a, app* b); + bool enable_eq(expr* a, expr* b, expr* c); + public: ackerman(solver& s, ast_manager& m); diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index eeb195429..f6d6e73dd 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -751,6 +751,18 @@ namespace euf { } } + bool solver::enable_ackerman_axioms(expr* e) const { + euf::enode* n = get_enode(e); + if (!n) + return false; + for (auto const& thv : enode_th_vars(n)) { + auto* th = m_id2solver.get(thv.get_id(), nullptr); + if (th && !th->enable_ackerman_axioms(n)) + return false; + } + return true; + } + 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 dc11637b8..12afc492f 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -372,6 +372,7 @@ namespace euf { th_rewriter& get_rewriter() { return m_rewriter; } void rewrite(expr_ref& e) { m_rewriter(e); } bool is_shared(euf::enode* n) const; + bool enable_ackerman_axioms(expr* n) const; // relevancy bool m_relevancy_enabled = true; diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 16138441c..9d1d9ebb1 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -111,6 +111,8 @@ namespace euf { virtual void new_diseq_eh(euf::th_eq const& eq) {} + virtual bool enable_ackerman_axioms(euf::enode* n) const { return true; } + virtual void relevant_eh(euf::enode* n) {} /**