mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

#5528

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-01 14:01:15 -07:00
parent a7bc4719c0
commit 7ce4be8455
3 changed files with 25 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -342,6 +342,8 @@ namespace euf {
break; break;
} }
} }
if (m.is_bool(n->get_expr()) && th_id != m.get_basic_family_id())
return true;
for (enode* parent : euf::enode_parents(n)) { for (enode* parent : euf::enode_parents(n)) {
app* p = to_app(parent->get_expr()); app* p = to_app(parent->get_expr());

19
src/sat/smt/euf_solver.cpp
View file

@ -458,6 +458,8 @@ namespace euf {
give_up = true; give_up = true;
unsigned num_nodes = m_egraph.num_nodes(); unsigned num_nodes = m_egraph.num_nodes();
if (merge_shared_bools())
cont = true;
for (auto* e : m_solvers) { for (auto* e : m_solvers) {
if (!m.inc()) if (!m.inc())
return sat::check_result::CR_GIVEUP; return sat::check_result::CR_GIVEUP;
@ -485,6 +487,23 @@ namespace euf {
return sat::check_result::CR_DONE; return sat::check_result::CR_DONE;
} }
bool solver::merge_shared_bools() {
bool merged = false;
for (euf::enode* n : m_egraph.nodes()) {
if (!is_shared(n) || !m.is_bool(n->get_expr()))
continue;
if (n->value() == l_true && !m.is_true(n->get_root()->get_expr())) {
m_egraph.merge(n, mk_true(), to_ptr(sat::literal(n->bool_var())));
merged = true;
}
if (n->value() == l_false && !m.is_false(n->get_root()->get_expr())) {
m_egraph.merge(n, mk_false(), to_ptr(~sat::literal(n->bool_var())));
merged = true;
}
}
return merged;
}
void solver::push() { void solver::push() {
si.push(); si.push();
scope s; scope s;

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

@ -165,6 +165,7 @@ namespace euf {
bool is_self_propagated(th_eq const& e); bool is_self_propagated(th_eq const& e);
void get_antecedents(literal l, constraint& j, literal_vector& r, bool probing); void get_antecedents(literal l, constraint& j, literal_vector& r, bool probing);
void new_diseq(enode* a, enode* b, literal lit); void new_diseq(enode* a, enode* b, literal lit);
bool merge_shared_bools();
// proofs // proofs
void log_antecedents(std::ostream& out, literal l, literal_vector const& r); void log_antecedents(std::ostream& out, literal l, literal_vector const& r);
@ -286,6 +287,7 @@ namespace euf {
void propagate(literal lit, th_explain* p) { propagate(lit, p->to_index()); } void propagate(literal lit, th_explain* p) { propagate(lit, p->to_index()); }
bool propagate(enode* a, enode* b, th_explain* p) { return propagate(a, b, p->to_index()); } bool propagate(enode* a, enode* b, th_explain* p) { return propagate(a, b, p->to_index()); }
size_t* to_justification(sat::literal l) { return to_ptr(l); }
void set_conflict(th_explain* p) { set_conflict(p->to_index()); } void set_conflict(th_explain* p) { set_conflict(p->to_index()); }
bool set_root(literal l, literal r) override; bool set_root(literal l, literal r) override;