mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

pending files

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-02 19:43:51 -08:00
parent b22daa9816
commit 1de25ed09c
3 changed files with 50 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
src/ast/euf/euf_egraph.cpp
View file

@ -81,14 +81,14 @@ namespace euf {
}
void egraph::reinsert_equality(enode* p) {
SASSERT(p->is_equality());
SASSERT(p->is_equality());
if (p->value() != l_true && p->get_arg(0)->get_root() == p->get_arg(1)->get_root())
queue_literal(p, nullptr);
}
void egraph::queue_literal(enode* p, enode* ante) {
void egraph::queue_literal(enode* p, enode* ante) {
if (m_on_propagate_literal)
m_to_merge.push_back({ p, ante });
m_to_merge.push_back(to_merge(p, ante));
}
void egraph::force_push() {
@ -180,6 +180,7 @@ namespace euf {
}
void egraph::add_literal(enode* n, enode* ante) {
TRACE("euf", tout << "propagate " << bpp(n) << " " << bpp(ante) << "\n");
if (!m_on_propagate_literal)
return;
if (!ante) ++m_stats.m_num_eqs; else ++m_stats.m_num_lits;
@ -518,7 +519,7 @@ namespace euf {
void egraph::remove_parents(enode* r) {
TRACE("euf", tout << bpp(r) << "\n");
DEBUG_CODE(for (enode* p : enode_parents(r)) SASSERT(!p->is_marked1()); );
SASSERT(all_of(enode_parents(r), [&](enode* p) { return !p->is_marked1(); }));
for (enode* p : enode_parents(r)) {
if (p->is_marked1())
continue;
@ -545,7 +546,7 @@ namespace euf {
if (p->cgc_enabled()) {
auto [p_other, comm] = insert_table(p);
SASSERT(m_table.contains_ptr(p) == (p_other == p));
TRACE("euf", tout << "other " << bpp(p_other) << "\n";);
CTRACE("euf", p_other != p, tout << "reinsert " << bpp(p) << " == " << bpp(p_other) << " " << p->value() << " " << p_other->value() << "\n");
if (p_other != p)
m_to_merge.push_back(to_merge(p_other, p, comm));
else
@ -606,20 +607,26 @@ namespace euf {
bool egraph::propagate() {
force_push();
for (unsigned i = 0; i < m_to_merge.size() && m.limit().inc() && !inconsistent(); ++i) {
auto const& w = m_to_merge[i];
switch (w.t) {
case to_merge_plain:
case to_merge_comm:
merge(w.a, w.b, justification::congruence(w.commutativity(), m_congruence_timestamp++));
break;
case to_justified:
merge(w.a, w.b, w.j);
break;
case to_add_literal:
add_literal(w.a, w.b);
break;
}
unsigned i = 0;
bool change = true;
while (change) {
change = false;
propagate_plugins();
for (; i < m_to_merge.size() && m.limit().inc() && !inconsistent(); ++i) {
auto const& w = m_to_merge[i];
switch (w.t) {
case to_merge_plain:
case to_merge_comm:
merge(w.a, w.b, justification::congruence(w.commutativity(), m_congruence_timestamp++));
break;
case to_justified:
merge(w.a, w.b, w.j);
break;
case to_add_literal:
add_literal(w.a, w.b);
break;
}
}
}
m_to_merge.reset();
return
@ -635,7 +642,7 @@ namespace euf {
m_updates.push_back(update_record(false, update_record::inconsistent()));
m_n1 = n1;
m_n2 = n2;
TRACE("euf", tout << "conflict " << bpp(n1) << " " << bpp(n2) << " " << j << "\n");
TRACE("euf", tout << "conflict " << bpp(n1) << " " << bpp(n2) << " " << j << " " << n1->get_root()->value() << " " << n2->get_root()->value() << "\n");
m_justification = j;
}

31
src/sat/sat_solver.cpp
View file

@ -962,6 +962,8 @@ namespace sat {
// -----------------------
bool solver::propagate_core(bool update) {
if (m_ext && (!is_probing() || at_base_lvl()))
m_ext->unit_propagate();
while (m_qhead < m_trail.size() && !m_inconsistent) {
do {
checkpoint();
@ -1783,7 +1785,7 @@ namespace sat {
}
bool solver::should_propagate() const {
return !inconsistent() && m_qhead < m_trail.size();
return !inconsistent() && (m_qhead < m_trail.size() || (m_ext && m_ext->should_propagate()));
}
lbool solver::final_check() {
@ -2533,17 +2535,8 @@ namespace sat {
case justification::EXT_JUSTIFICATION: {
fill_ext_antecedents(consequent, js, false);
TRACE("sat", tout << "ext antecedents: " << m_ext_antecedents << "\n";);
for (literal l : m_ext_antecedents)
process_antecedent(l, num_marks);
#if 0
if (m_ext_antecedents.size() <= 1) {
for (literal& l : m_ext_antecedents)
l.neg();
m_ext_antecedents.push_back(consequent);
mk_clause(m_ext_antecedents.size(), m_ext_antecedents.c_ptr(), sat::status::redundant());
}
#endif
for (literal l : m_ext_antecedents)
process_antecedent(l, num_marks);
break;
}
default:
@ -2822,25 +2815,27 @@ namespace sat {
switch (js.get_kind()) {
case justification::NONE:
level = std::max(level, js.level());
return level;
break;
case justification::BINARY:
level = update_max_level(js.get_literal(), level, unique_max);
return level;
break;
case justification::CLAUSE:
for (literal l : get_clause(js))
level = update_max_level(l, level, unique_max);
return level;
break;
case justification::EXT_JUSTIFICATION:
if (not_l != null_literal)
not_l.neg();
fill_ext_antecedents(not_l, js, true);
for (literal l : m_ext_antecedents)
level = update_max_level(l, level, unique_max);
return level;
break;
default:
UNREACHABLE();
return 0;
break;
}
TRACE("sat", tout << "max-level " << level << " " << unique_max << "\n");
return level;
}
/**
@ -3493,6 +3488,8 @@ namespace sat {
SASSERT(!inconsistent());
TRACE("sat_verbose", tout << "q:" << m_qhead << " trail: " << m_trail.size() << "\n";);
SASSERT(m_qhead == m_trail.size());
if (m_ext)
m_ext->unit_propagate();
m_scopes.push_back(scope());
scope & s = m_scopes.back();
m_scope_lvl++;

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

@ -435,6 +435,9 @@ namespace euf {
}
bool solver::should_propagate() {
return m_egraph.can_propagate();
}
bool solver::unit_propagate() {
bool propagated = false;
@ -477,6 +480,7 @@ namespace euf {
SASSERT(m.is_bool(e));
size_t cnstr;
literal lit;
if (!ante) {
VERIFY(m.is_eq(e, a, b));
cnstr = eq_constraint().to_index();
@ -494,7 +498,7 @@ namespace euf {
if (val == l_undef) {
SASSERT(m.is_value(ante->get_expr()));
val = m.is_true(ante->get_expr()) ? l_true : l_false;
}
}
auto& c = lit_constraint(ante);
cnstr = c.to_index();
lit = literal(v, val == l_false);
@ -1012,8 +1016,10 @@ namespace euf {
return out << "euf conflict";
case constraint::kind_t::eq:
return out << "euf equality propagation";
case constraint::kind_t::lit:
return out << "euf literal propagation " << m_egraph.bpp(c.node()) ;
case constraint::kind_t::lit: {
euf::enode* n = c.node();
return out << "euf literal propagation " << (sat::literal(n->bool_var(), n->value() == l_false)) << " " << m_egraph.bpp(n);
}
default:
UNREACHABLE();
return out;