diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index f1e51ee1d..4a752781c 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -25,6 +25,8 @@ namespace euf { enode* egraph::mk_enode(expr* f, unsigned generation, unsigned num_args, enode * const* args) { enode* n = enode::mk(m_region, f, generation, num_args, args); + if (m_default_relevant) + n->set_relevant(true); m_nodes.push_back(n); m_exprs.push_back(f); if (is_app(f) && num_args > 0) { @@ -269,6 +271,13 @@ namespace euf { } } + void egraph::set_relevant(enode* n) { + if (n->is_relevant()) + return; + n->set_relevant(true); + m_updates.push_back(update_record(n, update_record::set_relevant())); + } + void egraph::toggle_merge_enabled(enode* n, bool backtracking) { bool enable_merge = !n->merge_enabled(); n->set_merge_enabled(enable_merge); @@ -380,6 +389,10 @@ namespace euf { case update_record::tag_t::is_lbl_set: p.r1->m_lbls.set(p.m_lbls); break; + case update_record::tag_t::is_set_relevant: + SASSERT(p.r1->is_relevant()); + p.r1->set_relevant(false); + break; case update_record::tag_t::is_update_children: for (unsigned i = 0; i < p.r1->num_args(); ++i) { SASSERT(p.r1->m_args[i]->get_root()->m_parents.back() == p.r1); diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index ef70fafd5..a91dbf4a4 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -106,10 +106,11 @@ namespace euf { struct lbl_hash {}; struct lbl_set {}; struct update_children {}; + struct set_relevant {}; enum class tag_t { is_set_parent, is_add_node, is_toggle_merge, is_update_children, is_add_th_var, is_replace_th_var, is_new_lit, is_new_th_eq, is_lbl_hash, is_new_th_eq_qhead, is_new_lits_qhead, - is_inconsistent, is_value_assignment, is_lbl_set }; + is_inconsistent, is_value_assignment, is_lbl_set, is_set_relevant }; tag_t tag; enode* r1; enode* n1; @@ -152,6 +153,8 @@ namespace euf { tag(tag_t::is_lbl_set), r1(n), n1(nullptr), m_lbls(n->m_lbls.get()) {} update_record(enode* n, update_children) : tag(tag_t::is_update_children), r1(n), n1(nullptr), r2_num_parents(UINT_MAX) {} + update_record(enode* n, set_relevant) : + tag(tag_t::is_set_relevant), r1(n), n1(nullptr), r2_num_parents(UINT_MAX) {} }; ast_manager& m; svector m_to_merge; @@ -182,6 +185,7 @@ namespace euf { enode_vector m_todo; stats m_stats; bool m_uses_congruence = false; + bool m_default_relevant = true; std::vector> m_on_merge; std::function m_on_make; std::function m_used_eq; @@ -293,6 +297,8 @@ namespace euf { void set_merge_enabled(enode* n, bool enable_merge); void set_value(enode* n, lbool value); void set_bool_var(enode* n, unsigned v) { n->set_bool_var(v); } + void set_relevant(enode* n); + void set_default_relevant(bool b) { m_default_relevant = b; } void set_on_merge(std::function& on_merge) { m_on_merge.push_back(on_merge); } void set_on_make(std::function& on_make) { m_on_make = on_make; } diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h index 8498c9790..9cd812a9a 100644 --- a/src/ast/euf/euf_enode.h +++ b/src/ast/euf/euf_enode.h @@ -49,6 +49,7 @@ namespace euf { bool m_interpreted = false; bool m_merge_enabled = true; bool m_is_equality = false; // Does the expression represent an equality + bool m_is_relevant = false; lbool m_value = l_undef; // Assignment by SAT solver for Boolean node sat::bool_var m_bool_var = sat::null_bool_var; // SAT solver variable associated with Boolean node unsigned m_class_size = 1; // Size of the equivalence class if the enode is the root. @@ -145,6 +146,8 @@ namespace euf { unsigned num_parents() const { return m_parents.size(); } bool interpreted() const { return m_interpreted; } bool is_equality() const { return m_is_equality; } + bool is_relevant() const { return m_is_relevant; } + void set_relevant(bool b) { m_is_relevant = b; } lbool value() const { return m_value; } bool value_conflict() const { return value() != l_undef && get_root()->value() != l_undef && value() != get_root()->value(); } sat::bool_var bool_var() const { return m_bool_var; } diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp index ca4841656..144ed105d 100644 --- a/src/sat/smt/bv_delay_internalize.cpp +++ b/src/sat/smt/bv_delay_internalize.cpp @@ -21,7 +21,10 @@ Author: namespace bv { bool solver::check_delay_internalized(expr* e) { - if (!ctx.is_relevant(e)) + euf::enode* n = expr2enode(e); + if (!n) + return true; + if (!ctx.is_relevant(n)) return true; if (get_internalize_mode(e) != internalize_mode::delay_i) return true; diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp index e4c2c1b4d..4851f4a04 100644 --- a/src/sat/smt/euf_relevancy.cpp +++ b/src/sat/smt/euf_relevancy.cpp @@ -31,7 +31,6 @@ namespace euf { return; for (; m_auto_relevant_scopes > 0; --m_auto_relevant_scopes) m_auto_relevant_lim.push_back(m_auto_relevant.size()); - // std::cout << "add-auto " << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; expr* e = bool_var2expr(lit.var()); m_auto_relevant.push_back(e); } @@ -61,12 +60,6 @@ namespace euf { ++m_auto_relevant_scopes; } - bool solver::is_relevant(expr* e) const { - if (m_relevancy.enabled()) - return m_relevancy.is_relevant(e); - return m_relevant_expr_ids.get(e->get_id(), true); - } - bool solver::is_relevant(enode* n) const { if (m_relevancy.enabled()) return m_relevancy.is_relevant(n); @@ -76,7 +69,7 @@ namespace euf { bool solver::is_relevant(bool_var v) const { if (m_relevancy.enabled()) return m_relevancy.is_relevant(v); - expr* e = bool_var2expr(v); + auto* e = bool_var2enode(v); return !e || is_relevant(e); } diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 1ff072b03..b3cdf99bc 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -392,7 +392,6 @@ namespace euf { 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; bool is_relevant(bool_var v) const; void add_auto_relevant(sat::literal lit); diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 20e65b8d6..000937700 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -51,7 +51,7 @@ namespace q { m_instantiations.reset(); for (sat::literal lit : m_qs.m_universal) { quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var())); - if (!ctx.is_relevant(q)) + if (!ctx.is_relevant(lit.var())) continue; init_model(); switch (check_forall(q)) { diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp index 3339daf2d..a87bf3397 100644 --- a/src/sat/smt/q_model_fixer.cpp +++ b/src/sat/smt/q_model_fixer.cpp @@ -66,7 +66,7 @@ namespace q { ptr_vector univ; for (sat::literal lit : m_qs.universal()) { quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var())); - if (ctx.is_relevant(q)) + if (ctx.is_relevant(lit.var())) univ.push_back(q); } if (univ.empty()) diff --git a/src/sat/smt/smt_relevant.cpp b/src/sat/smt/smt_relevant.cpp index 14d164952..d7f35b563 100644 --- a/src/sat/smt/smt_relevant.cpp +++ b/src/sat/smt/smt_relevant.cpp @@ -49,10 +49,6 @@ namespace smt { for (unsigned i = m_trail.size(); i-- > sz; ) { auto [u, idx] = m_trail[i]; switch (u) { - case update::relevant_expr: - m_relevant_expr_ids[idx] = false; - m_queue.pop_back(); - break; case update::relevant_var: m_relevant_var_ids[idx] = false; m_queue.pop_back(); @@ -191,10 +187,9 @@ namespace smt { } void relevancy::set_relevant(euf::enode* n) { - if (is_relevant(n)) + if (n->is_relevant()) return; - m_relevant_expr_ids.setx(n->get_expr_id(), true, false); - m_trail.push_back(std::make_pair(update::relevant_expr, n->get_expr_id())); + ctx.get_egraph().set_relevant(n); m_queue.push_back(std::make_pair(sat::null_literal, n)); } @@ -247,4 +242,9 @@ namespace smt { mark_relevant(arg); } + void relevancy::set_enabled(bool e) { + m_enabled = e; + ctx.get_egraph().set_default_relevant(!e); + } + } diff --git a/src/sat/smt/smt_relevant.h b/src/sat/smt/smt_relevant.h index 9e8ba00c3..73f04cf40 100644 --- a/src/sat/smt/smt_relevant.h +++ b/src/sat/smt/smt_relevant.h @@ -106,13 +106,12 @@ namespace smt { class relevancy { euf::solver& ctx; - enum class update { relevant_expr, relevant_var, add_clause, set_root, set_qhead }; + enum class update { relevant_var, add_clause, set_root, set_qhead }; bool m_enabled = false; svector> m_trail; unsigned_vector m_lim; unsigned m_num_scopes = 0; - bool_vector m_relevant_expr_ids; // identifiers of relevant expressions bool_vector m_relevant_var_ids; // identifiers of relevant Boolean variables sat::clause_allocator m_alloc; sat::clause_vector m_clauses; // clauses @@ -154,10 +153,9 @@ namespace smt { bool is_relevant(sat::bool_var v) const { return !m_enabled || m_relevant_var_ids.get(v, false); } bool is_relevant(sat::literal lit) const { return is_relevant(lit.var()); } - bool is_relevant(euf::enode* n) const { return !m_enabled || m_relevant_expr_ids.get(n->get_expr_id(), false); } - bool is_relevant(expr* e) const { return !m_enabled || m_relevant_expr_ids.get(e->get_id(), false); } + bool is_relevant(euf::enode* n) const { return !m_enabled || n->is_relevant(); } bool enabled() const { return m_enabled; } - void set_enabled(bool e) { m_enabled = e; } + void set_enabled(bool e); }; }