mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 11:20:26 +00:00
Code Activity

don't saturate immediately after forbidden intervals

Browse source
This commit is contained in:
Jakob Rath 2022-04-13 12:45:14 +02:00
parent 3533bf486f
commit fc2633c964
1 changed files with 1 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -572,17 +572,8 @@ namespace polysat {
pvar v = m_conflict.conflict_var(); pvar v = m_conflict.conflict_var();
// This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack. // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
// TODO: use unsat core from m_viable_fallback if the conflict is from there // TODO: use unsat core from m_viable_fallback if the conflict is from there
// TODO: we could try simpler backtracking loop if we get a lemma from forbidden intervals
VERIFY(m_viable.resolve(v, m_conflict)); VERIFY(m_viable.resolve(v, m_conflict));
// TBD: saturate resulting conflict to get better lemmas.
LOG("try-eliminate v" << v);
if (m_conflict.try_explain(v))
;
else if (m_conflict.try_eliminate(v))
;
else
m_conflict.try_saturate(v);
LOG("end-try-eliminate v");
} }
search_iterator search_it(m_search); search_iterator search_it(m_search);