mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 12:48:53 +00:00
Code Activity

more fixes on relevancy

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-04 22:02:28 -08:00
parent 5ec7a66a45
commit bd8de964f7
3 changed files with 44 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/euf_model.cpp
View file

@ -199,6 +199,8 @@ namespace euf {
expr* e = n->get_expr(); expr* e = n->get_expr();
if (!is_app(e)) if (!is_app(e))
continue; continue;
if (!is_relevant(n))
continue;
app* a = to_app(e); app* a = to_app(e);
func_decl* f = a->get_decl(); func_decl* f = a->get_decl();
if (!include_func_interp(f)) if (!include_func_interp(f))
@ -297,6 +299,8 @@ namespace euf {
ev.set_model_completion(true); ev.set_model_completion(true);
TRACE("model", TRACE("model",
for (enode* n : m_egraph.nodes()) { for (enode* n : m_egraph.nodes()) {
if (!is_relevant(n))
continue;
unsigned id = n->get_root_id(); unsigned id = n->get_root_id();
expr* val = m_values.get(id, nullptr); expr* val = m_values.get(id, nullptr);
if (!val) if (!val)

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

@ -132,6 +132,35 @@ namespace euf {
m_trail.push_back(std::make_pair(update::relevant_var, lit.var())); m_trail.push_back(std::make_pair(update::relevant_var, lit.var()));
} }
void relevancy::set_asserted(sat::literal lit) {
SASSERT(!is_relevant(lit));
SASSERT(ctx.s().value(lit) == l_true);
set_relevant(lit);
add_to_propagation_queue(lit);
ctx.asserted(lit);
}
/**
* Boolean variable is set relevant because an E-node is relevant.
*
*/
void relevancy::relevant_eh(sat::bool_var v) {
if (is_relevant(v))
return;
sat::literal lit(v);
switch (ctx.s().value(lit)) {
case l_undef:
set_relevant(lit);
break;
case l_true:
set_asserted(lit);
break;
case l_false:
set_asserted(~lit);
break;
}
}
void relevancy::asserted(sat::literal lit) { void relevancy::asserted(sat::literal lit) {
TRACE("relevancy", tout << "asserted " << lit << " relevant " << is_relevant(lit) << "\n"); TRACE("relevancy", tout << "asserted " << lit << " relevant " << is_relevant(lit) << "\n");
if (!m_enabled) if (!m_enabled)
@ -239,11 +268,8 @@ namespace euf {
} }
} }
if (true_lit != sat::null_literal) { if (true_lit != sat::null_literal)
set_relevant(true_lit); set_asserted(true_lit);
add_to_propagation_queue(true_lit);
ctx.asserted(true_lit);
}
else { else {
m_trail.push_back(std::make_pair(update::set_root, idx)); m_trail.push_back(std::make_pair(update::set_root, idx));
m_roots[idx] = true; m_roots[idx] = true;
@ -276,8 +302,9 @@ namespace euf {
if (!n->is_relevant()) { if (!n->is_relevant()) {
ctx.get_egraph().set_relevant(n); ctx.get_egraph().set_relevant(n);
ctx.relevant_eh(n); ctx.relevant_eh(n);
if (n->bool_var() != sat::null_bool_var) sat::bool_var v = n->bool_var();
mark_relevant(sat::literal(n->bool_var())); if (v != sat::null_bool_var)
relevant_eh(v);
for (euf::enode* sib : euf::enode_class(n)) for (euf::enode* sib : euf::enode_class(n))
if (!sib->is_relevant()) if (!sib->is_relevant())
m_todo.push_back(sib); m_todo.push_back(sib);

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

@ -139,10 +139,14 @@ namespace euf {
void add_to_propagation_queue(sat::literal lit); void add_to_propagation_queue(sat::literal lit);
void propagate_relevant(euf::enode* n);
void set_relevant(sat::literal lit); void set_relevant(sat::literal lit);
void set_asserted(sat::literal lit);
void relevant_eh(sat::bool_var v);
void propagate_relevant(euf::enode* n);
public: public:
relevancy(euf::solver& ctx): ctx(ctx) {} relevancy(euf::solver& ctx): ctx(ctx) {}