Skip to content

Commit

Permalink
relevancy overhaul
Browse files Browse the repository at this point in the history
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Jan 5, 2022
1 parent 4a19750 commit d1fb831
Show file tree
Hide file tree
Showing 6 changed files with 96 additions and 79 deletions.
11 changes: 9 additions & 2 deletions src/ast/euf/euf_egraph.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -785,8 +785,15 @@ namespace euf {
out << " " << p->get_expr_id();
out << "] ";
}
if (n->value() != l_undef)
out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << (n->merge_tf()?"":" no merge") << "] ";
auto value_of = [&]() {
switch (n->value()) {
case l_true: return "T";
case l_false: return "F";
default: return "?";
}
};
if (n->bool_var() != sat::null_bool_var)
out << "[b" << n->bool_var() << " := " << value_of() << (n->merge_tf() ? "" : " no merge") << "] ";
if (n->has_th_vars()) {
out << "[t";
for (auto const& v : enode_th_vars(n))
Expand Down
7 changes: 3 additions & 4 deletions src/sat/smt/euf_model.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -161,10 +161,9 @@ namespace euf {
default:
break;
}
if (is_app(e) && to_app(e)->get_family_id() == m.get_basic_family_id())
continue;
sat::bool_var v = get_enode(e)->bool_var();
SASSERT(v != sat::null_bool_var);
if (v == sat::null_bool_var)
continue;
switch (s().value(v)) {
case l_true:
m_values.set(id, m.mk_true());
Expand Down Expand Up @@ -224,7 +223,7 @@ namespace euf {
enode* earg = get_enode(arg);
expr* val = m_values.get(earg->get_root_id());
args.push_back(val);
CTRACE("euf", !val, tout << "no value for " << bpp(earg) << "\n";);
CTRACE("euf", !val, tout << "no value for " << bpp(earg) << "\n" << bpp(n) << "\n"; display(tout););
SASSERT(val);
}
SASSERT(args.size() == arity);
Expand Down
107 changes: 61 additions & 46 deletions src/sat/smt/euf_relevancy.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,28 +20,6 @@ Module Name:


namespace euf {

relevancy::relevancy(euf::solver& ctx): ctx(ctx) {
}

void relevancy::relevant_eh(euf::enode* n) {
SASSERT(is_relevant(n));
ctx.relevant_eh(n);
}

void relevancy::relevant_eh(sat::literal lit) {
SASSERT(is_relevant(lit));
switch (ctx.s().value(lit)) {
case l_true:
ctx.asserted(lit);
break;
case l_false:
ctx.asserted(~lit);
break;
default:
break;
}
}

void relevancy::pop(unsigned n) {
if (!m_enabled)
Expand All @@ -61,9 +39,8 @@ namespace euf {
switch (u) {
case update::relevant_var:
m_relevant_var_ids[idx] = false;
m_queue.pop_back();
break;
case update::relevant_node:
case update::add_queue:
m_queue.pop_back();
break;
case update::add_clause: {
Expand Down Expand Up @@ -120,10 +97,11 @@ namespace euf {
}
}

void relevancy::add_def(unsigned n, sat::literal const* lits) {
void relevancy::add_def(unsigned n, sat::literal const* lits) {
if (!m_enabled)
return;
flush();
TRACE("relevancy", tout << "def " << sat::literal_vector(n, lits) << "\n");
for (unsigned i = 0; i < n; ++i) {
if (ctx.s().value(lits[i]) == l_false && is_relevant(lits[i])) {
add_root(n, lits);
Expand All @@ -141,21 +119,42 @@ namespace euf {
}
}

void relevancy::add_to_propagation_queue(sat::literal lit) {
m_trail.push_back(std::make_pair(update::add_queue, lit.var()));
m_queue.push_back(std::make_pair(lit, nullptr));
}

void relevancy::set_relevant(sat::literal lit) {
euf::enode* n = ctx.bool_var2enode(lit.var());
if (n)
mark_relevant(n);
m_relevant_var_ids.setx(lit.var(), true, false);
m_trail.push_back(std::make_pair(update::relevant_var, lit.var()));
}

void relevancy::asserted(sat::literal lit) {
TRACE("relevancy", tout << "asserted " << lit << " relevant " << is_relevant(lit) << "\n");
if (!m_enabled)
return;
flush();
if (is_relevant(lit)) {
add_to_propagation_queue(lit);
return;
}
if (ctx.s().lvl(lit) <= ctx.s().search_lvl()) {
mark_relevant(lit);
set_relevant(lit);
add_to_propagation_queue(lit);
return;
}

for (auto idx : occurs(lit)) {
if (!m_roots[idx])
continue;
for (sat::literal lit2 : *m_clauses[idx])
if (lit2 != lit && ctx.s().value(lit2) == l_true && is_relevant(lit2))
goto next;
mark_relevant(lit);
goto next;
set_relevant(lit);
add_to_propagation_queue(lit);
return;
next:
;
Expand All @@ -181,6 +180,7 @@ namespace euf {
}

void relevancy::merge(euf::enode* root, euf::enode* other) {
TRACE("relevancy", tout << "merge #" << ctx.bpp(root) << " " << is_relevant(root) << " #" << ctx.bpp(other) << " " << is_relevant(other) << "\n");
if (is_relevant(root))
mark_relevant(other);
else if (is_relevant(other))
Expand All @@ -193,28 +193,36 @@ namespace euf {
flush();
if (is_relevant(n))
return;
if (ctx.get_si().is_bool_op(n->get_expr()))
return;
m_trail.push_back(std::make_pair(update::relevant_node, 0));
TRACE("relevancy", tout << "mark #" << ctx.bpp(n) << "\n");
m_trail.push_back(std::make_pair(update::add_queue, 0));
m_queue.push_back(std::make_pair(sat::null_literal, n));
}

void relevancy::mark_relevant(sat::literal lit) {
TRACE("relevancy", tout << "mark " << lit << " " << is_relevant(lit) << " " << ctx.s().value(lit) << " lim: " << m_lim.size() << "\n");
if (!m_enabled)
return;
flush();
if (is_relevant(lit))
return;
euf::enode* n = ctx.bool_var2enode(lit.var());
if (n)
mark_relevant(n);
m_relevant_var_ids.setx(lit.var(), true, false);
m_trail.push_back(std::make_pair(update::relevant_var, lit.var()));
m_queue.push_back(std::make_pair(lit, nullptr));
set_relevant(lit);
switch (ctx.s().value(lit)) {
case l_true:
break;
case l_false:
lit.neg();
break;
default:
return;
}
add_to_propagation_queue(lit);
}

void relevancy::propagate_relevant(sat::literal lit) {
relevant_eh(lit);
SASSERT(m_num_scopes == 0);
TRACE("relevancy", tout << "propagate " << lit << " lim: " << m_lim.size() << "\n");
SASSERT(ctx.s().value(lit) == l_true);
SASSERT(is_relevant(lit));
euf::enode* n = ctx.bool_var2enode(lit.var());
if (n && !ctx.get_si().is_bool_op(n->get_expr()))
return;
Expand All @@ -231,13 +239,17 @@ namespace euf {
}
}

if (true_lit != sat::null_literal)
mark_relevant(true_lit);
if (true_lit != sat::null_literal) {
set_relevant(true_lit);
add_to_propagation_queue(true_lit);
ctx.asserted(true_lit);
}
else {
m_trail.push_back(std::make_pair(update::set_root, idx));
m_roots[idx] = true;
}
next:
TRACE("relevancy", tout << "propagate " << lit << " " << true_lit << " " << m_roots[idx] << "\n");
;
}
}
Expand All @@ -247,22 +259,25 @@ namespace euf {
while (!m_todo.empty()) {
n = m_todo.back();
m_todo.pop_back();
TRACE("relevancy", tout << "propagate #" << ctx.bpp(n) << " lim: " << m_lim.size() << "\n");
if (n->is_relevant())
continue;
if (ctx.get_si().is_bool_op(n->get_expr()))
continue;
m_stack.push_back(n);
while (!m_stack.empty()) {
n = m_stack.back();
unsigned sz = m_stack.size();
for (euf::enode* arg : euf::enode_args(n))
if (!arg->is_relevant())
m_stack.push_back(arg);
bool is_bool_op = ctx.get_si().is_bool_op(n->get_expr());
if (!is_bool_op)
for (euf::enode* arg : euf::enode_args(n))
if (!arg->is_relevant())
m_stack.push_back(arg);
if (sz != m_stack.size())
continue;
if (!n->is_relevant()) {
ctx.get_egraph().set_relevant(n);
relevant_eh(n);
ctx.relevant_eh(n);
if (n->bool_var() != sat::null_bool_var)
mark_relevant(sat::literal(n->bool_var()));
for (euf::enode* sib : euf::enode_class(n))
if (!sib->is_relevant())
m_todo.push_back(sib);
Expand Down
22 changes: 16 additions & 6 deletions src/sat/smt/euf_relevancy.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,16 @@ Do we need full watch lists instead of 2-watch lists?
roots.
State machine for literals: relevant(lit), assigned(lit)
relevant(lit) transitions false -> true
if assigned(lit): add to propagation queue
if not assigned(lit): no-op (or mark enodes as relevant)
assigned(lit) transitions false -> true
if relevant(lit): add to propagation queue
if not relevant(lit): set relevant if member of root, add to propagation queue
--*/
#pragma once
Expand All @@ -105,7 +115,7 @@ namespace euf {
class relevancy {
euf::solver& ctx;

enum class update { relevant_var, relevant_node, add_clause, set_root, set_qhead };
enum class update { relevant_var, add_queue, add_clause, set_root, set_qhead };

bool m_enabled = false;
svector<std::pair<update, unsigned>> m_trail;
Expand All @@ -120,21 +130,21 @@ namespace euf {
svector<std::pair<sat::literal, euf::enode*>> m_queue; // propagation queue for relevancy
euf::enode_vector m_stack, m_todo;

// callbacks during propagation
void relevant_eh(euf::enode* n);
void relevant_eh(sat::literal lit);

void push_core() { m_lim.push_back(m_trail.size()); }
void flush() { for (; m_num_scopes > 0; --m_num_scopes) push_core(); }

unsigned_vector& occurs(sat::literal lit) { m_occurs.reserve(lit.index() + 1); return m_occurs[lit.index()]; }

void propagate_relevant(sat::literal lit);

void add_to_propagation_queue(sat::literal lit);

void propagate_relevant(euf::enode* n);

void set_relevant(sat::literal lit);

public:
relevancy(euf::solver& ctx);
relevancy(euf::solver& ctx): ctx(ctx) {}

void push() { if (m_enabled) ++m_num_scopes; }
void pop(unsigned n);
Expand Down
8 changes: 3 additions & 5 deletions src/sat/smt/euf_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -297,11 +297,9 @@ namespace euf {

void solver::asserted(literal l) {

if (m_relevancy.enabled() && !m_relevancy.is_relevant(l)) {
m_relevancy.asserted(l);
if (!m_relevancy.is_relevant(l))
return;
}
m_relevancy.asserted(l);
if (!m_relevancy.is_relevant(l))
return;

expr* e = m_bool_var2expr.get(l.var(), nullptr);
TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";);
Expand Down
20 changes: 4 additions & 16 deletions src/sat/tactic/goal2sat.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,20 +125,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
bool top_level_relevant() {
return m_top_level && relevancy_enabled();
}

void add_dual_def(unsigned n, sat::literal const* lits) {
if (relevancy_enabled())
ensure_euf()->add_aux(n, lits);
}

void add_dual_root(unsigned n, sat::literal const* lits) {
if (relevancy_enabled())
ensure_euf()->add_root(n, lits);
}

void add_dual_root(sat::literal lit) {
add_dual_root(1, &lit);
}

void mk_clause(sat::literal l) {
mk_clause(1, &l);
Expand All @@ -156,7 +142,8 @@ struct goal2sat::imp : public sat::sat_internalizer {

void mk_clause(unsigned n, sat::literal * lits) {
TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
add_dual_def(n, lits);
if (relevancy_enabled())
ensure_euf()->add_aux(n, lits);
m_solver.add_clause(n, lits, mk_status());
}

Expand All @@ -176,7 +163,8 @@ struct goal2sat::imp : public sat::sat_internalizer {

void mk_root_clause(unsigned n, sat::literal * lits) {
TRACE("goal2sat", tout << "mk_root_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
add_dual_root(n, lits);
if (relevancy_enabled())
ensure_euf()->add_root(n, lits);
m_solver.add_clause(n, lits, m_is_redundant ? mk_status() : sat::status::input());
}

Expand Down

0 comments on commit d1fb831

Please sign in to comment.