mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

basic slicing integration

Browse source
This commit is contained in:
Jakob Rath 2023-07-18 16:19:54 +02:00
parent 28ed3bd7ab
commit 66f813154b
1 changed files with 17 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/math/polysat/solver.cpp
View file

@ -318,7 +318,11 @@ namespace polysat {
m_slicing.add_constraint(c); m_slicing.add_constraint(c);
} }
} }
else if (m_slicing.can_propagate()) {
m_slicing.propagate();
}
else { else {
SASSERT(m_qhead < m_search.size());
// Third priority: activate/narrow // Third priority: activate/narrow
auto const& item = m_search[m_qhead++]; auto const& item = m_search[m_qhead++];
if (item.is_assignment()) { if (item.is_assignment()) {
@ -332,6 +336,19 @@ namespace polysat {
activate_constraint(c); activate_constraint(c);
} }
} }
if (m_slicing.is_conflict()) {
SASSERT(!is_conflict());
sat::literal_vector lits;
unsigned_vector vars;
m_slicing.explain(lits, vars);
clause_builder cb(*this, "slicing");
for (sat::literal lit : lits)
cb.insert(~lit);
for (pvar v : vars)
cb.insert_eval(~eq(var(v), get_value(v)));
add_clause(cb.build());
SASSERT(is_conflict());
}
} // while (can_propagate_search()) } // while (can_propagate_search())
SASSERT(wlist_invariant()); SASSERT(wlist_invariant());
SASSERT(eval_invariant()); SASSERT(eval_invariant());