diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index d362dacb6..c0ab2ecbf 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -539,6 +539,8 @@ namespace array { if (!d.m_prop_upward) continue; euf::enode* n = var2enode(v); + if (!ctx.is_relevant(n)) + continue; if (add_as_array_eqs(n)) change = true; bool has_default = false; @@ -567,6 +569,8 @@ namespace array { return false; for (unsigned i = 0; i < ctx.get_egraph().enodes_of(f).size(); ++i) { euf::enode* p = ctx.get_egraph().enodes_of(f)[i]; + if (!ctx.is_relevant(p)) + continue; expr_ref_vector select(m); select.push_back(n->get_expr()); for (expr* arg : *to_app(p->get_expr())) @@ -615,7 +619,9 @@ namespace array { euf::enode * n = var2enode(i); if (!is_array(n)) - continue; + continue; + if (!ctx.is_relevant(n)) + continue; euf::enode * r = n->get_root(); if (r->is_marked1()) continue; diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index aa94f12a7..1076acc30 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -124,40 +124,49 @@ namespace array { mk_var(n); for (auto* arg : euf::enode_args(n)) ensure_var(arg); - switch (a->get_decl_kind()) { - case OP_STORE: - internalize_store(n); + if (ctx.is_relevant(n)) + relevant_eh(n); + return true; + } + + void solver::relevant_eh(euf::enode* n) { + if (!is_app(n->get_expr())) + return; + if (n->get_decl()->get_family_id() != a.get_family_id()) + return; + switch (n->get_decl()->get_decl_kind()) { + case OP_STORE: + internalize_store(n); break; - case OP_SELECT: - internalize_select(n); + case OP_SELECT: + internalize_select(n); break; case OP_AS_ARRAY: - case OP_CONST_ARRAY: - internalize_lambda(n); + case OP_CONST_ARRAY: + internalize_lambda(n); break; - case OP_ARRAY_EXT: - internalize_ext(n); + case OP_ARRAY_EXT: + internalize_ext(n); break; - case OP_ARRAY_DEFAULT: - internalize_default(n); + case OP_ARRAY_DEFAULT: + internalize_default(n); break; - case OP_ARRAY_MAP: - internalize_map(n); + case OP_ARRAY_MAP: + internalize_map(n); break; - case OP_SET_UNION: - case OP_SET_INTERSECT: - case OP_SET_DIFFERENCE: - case OP_SET_COMPLEMENT: - case OP_SET_SUBSET: - case OP_SET_HAS_SIZE: - case OP_SET_CARD: - ctx.unhandled_function(a->get_decl()); + case OP_SET_UNION: + case OP_SET_INTERSECT: + case OP_SET_DIFFERENCE: + case OP_SET_COMPLEMENT: + case OP_SET_SUBSET: + case OP_SET_HAS_SIZE: + case OP_SET_CARD: + ctx.unhandled_function(n->get_decl()); break; default: UNREACHABLE(); - break; + break; } - return true; } /** diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index 0c0fc82d6..8f9bd31f8 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -264,6 +264,7 @@ namespace array { void apply_sort_cnstr(euf::enode* n, sort* s) override; bool is_shared(theory_var v) const override; bool enable_self_propagate() const override { return true; } + void relevant_eh(euf::enode* n) override; 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) {} diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index b8fbc5bd9..5c94d21ba 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -739,6 +739,16 @@ namespace euf { } } + void solver::relevant_eh(euf::enode* n) { + if (m_qsolver) + m_qsolver->relevant_eh(n); + for (auto thv : enode_th_vars(n)) { + auto* th = m_id2solver.get(thv.get_id(), nullptr); + if (th && th != m_qsolver) + th->relevant_eh(n); + } + } + 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 c2a7776ef..1ff072b03 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -398,6 +398,7 @@ namespace euf { void add_auto_relevant(sat::literal lit); void pop_relevant(unsigned n); void push_relevant(); + void relevant_eh(euf::enode* n); smt::relevancy& relevancy() { return m_relevancy; } // model construction diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index 85287f47a..827405f85 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -70,15 +70,14 @@ namespace q { }; ctx.get_egraph().set_on_merge(_on_merge); - if (ctx.relevancy().enabled()) + if (!ctx.relevancy().enabled()) ctx.get_egraph().set_on_make(_on_make); - else - ctx.relevancy().add_relevant(&s); m_mam = mam::mk(ctx, *this); } void ematch::relevant_eh(euf::enode* n) { - m_mam->add_node(n, false); + if (ctx.relevancy().enabled()) + m_mam->add_node(n, false); } void ematch::ensure_ground_enodes(expr* e) { diff --git a/src/sat/smt/smt_relevant.cpp b/src/sat/smt/smt_relevant.cpp index 574ba0b42..14d164952 100644 --- a/src/sat/smt/smt_relevant.cpp +++ b/src/sat/smt/smt_relevant.cpp @@ -26,8 +26,7 @@ namespace smt { void relevancy::relevant_eh(euf::enode* n) { SASSERT(is_relevant(n)); - for (auto* th : m_relevant_eh) - th->relevant_eh(n); + ctx.relevant_eh(n); } void relevancy::relevant_eh(sat::literal lit) { diff --git a/src/sat/smt/smt_relevant.h b/src/sat/smt/smt_relevant.h index bd35e6f72..9e8ba00c3 100644 --- a/src/sat/smt/smt_relevant.h +++ b/src/sat/smt/smt_relevant.h @@ -120,7 +120,6 @@ namespace smt { vector m_occurs; // where do literals occur unsigned m_qhead = 0; // queue head for relevancy svector> m_queue; // propagation queue for relevancy - ptr_vector m_relevant_eh; // callbacks during propagation void relevant_eh(euf::enode* n); @@ -160,7 +159,5 @@ namespace smt { bool enabled() const { return m_enabled; } void set_enabled(bool e) { m_enabled = e; } - - void add_relevant(euf::th_solver* th) { m_relevant_eh.push_back(th); } }; }