mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 16:33:18 +00:00
Code Activity

use slicing conflict clause

Browse source
This commit is contained in:
Jakob Rath 2023-07-26 09:47:55 +02:00
parent 19c1ba5158
commit 681293c23f
1 changed files with 1 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -353,15 +353,7 @@ namespace polysat {
} }
if (m_slicing.is_conflict()) { if (m_slicing.is_conflict()) {
SASSERT(!is_conflict()); SASSERT(!is_conflict());
sat::literal_vector lits; add_clause(m_slicing.build_conflict_clause());
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()); SASSERT(is_conflict());
} }
} // while (can_propagate_search()) } // while (can_propagate_search())