mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-03 13:55:47 +00:00
Code Activity

set relevancy flag on enode

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-29 17:57:28 -08:00
parent a90b66134d
commit b87b464e69
10 changed files with 40 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/bv_delay_internalize.cpp
View file

@ -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;

9
src/sat/smt/euf_relevancy.cpp
View file

@ -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);
}

1
src/sat/smt/euf_solver.h
View file

@ -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);

2
src/sat/smt/q_mbi.cpp
View file

@ -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)) {

2
src/sat/smt/q_model_fixer.cpp
View file

@ -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())

14
src/sat/smt/smt_relevant.cpp
View file

@ -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);
}
}

8
src/sat/smt/smt_relevant.h
View file

@ -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);
};
}