From b87b464e6954d56e12ab61f3d457307b4800cc61 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 29 Dec 2021 17:57:28 -0800
Subject: [PATCH] set relevancy flag on enode
---
src/ast/euf/euf_egraph.cpp | 13 +++++++++++++
src/ast/euf/euf_egraph.h | 8 +++++++-
src/ast/euf/euf_enode.h | 3 +++
src/sat/smt/bv_delay_internalize.cpp | 5 ++++-
src/sat/smt/euf_relevancy.cpp | 9 +--------
src/sat/smt/euf_solver.h | 1 -
src/sat/smt/q_mbi.cpp | 2 +-
src/sat/smt/q_model_fixer.cpp | 2 +-
src/sat/smt/smt_relevant.cpp | 14 +++++++-------
src/sat/smt/smt_relevant.h | 8 +++-----
10 files changed, 40 insertions(+), 25 deletions(-)
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<to_merge> 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<std::function<void(enode*,enode*)>> m_on_merge;
std::function<void(enode*)> m_on_make;
std::function<void(expr*,expr*,expr*)> 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<void(enode* root,enode* other)>& on_merge) { m_on_merge.push_back(on_merge); }
void set_on_make(std::function<void(enode* n)>& 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<quantifier> 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<std::pair<update, unsigned>> 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);
};
}