mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

split repropagate_units

Browse source
This commit is contained in:
Jakob Rath 2023-03-02 16:01:57 +01:00
parent 8249a075e1
commit d8c6ab3488
2 changed files with 17 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -80,9 +80,10 @@ namespace polysat {
SASSERT(var_queue_invariant()); SASSERT(var_queue_invariant());
if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; } if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; }
else if (is_conflict()) resolve_conflict(); else if (is_conflict()) resolve_conflict();
else if (can_repropagate()) repropagate(); else if (can_repropagate_units()) repropagate_units();
else if (should_add_pwatch()) add_pwatch(); else if (should_add_pwatch()) add_pwatch();
else if (can_propagate()) propagate(); else if (can_propagate()) propagate();
else if (can_repropagate()) repropagate();
else if (!can_decide()) { LOG_H2("SAT"); VERIFY(verify_sat()); return l_true; } else if (!can_decide()) { LOG_H2("SAT"); VERIFY(verify_sat()); return l_true; }
else if (m_constraints.should_gc()) m_constraints.gc(); else if (m_constraints.should_gc()) m_constraints.gc();
else if (m_simplify.should_apply()) m_simplify(); else if (m_simplify.should_apply()) m_simplify();
@ -213,15 +214,15 @@ namespace polysat {
if (!is_conflict()) if (!is_conflict())
linear_propagate(); linear_propagate();
SASSERT(wlist_invariant()); SASSERT(wlist_invariant());
SASSERT(bool_watch_invariant()); // VERIFY(bool_watch_invariant());
SASSERT(eval_invariant()); SASSERT(eval_invariant());
} }
bool solver::can_repropagate() { bool solver::can_repropagate_units() {
return !m_repropagate_units.empty() || !m_repropagate_lits.empty(); return !m_repropagate_units.empty();
} }
void solver::repropagate() { void solver::repropagate_units() {
while (!m_repropagate_units.empty() && !is_conflict()) { while (!m_repropagate_units.empty() && !is_conflict()) {
clause& cl = *m_repropagate_units.back(); clause& cl = *m_repropagate_units.back();
m_repropagate_units.pop_back(); m_repropagate_units.pop_back();
@ -232,6 +233,7 @@ namespace polysat {
assign_propagate(lit, cl); assign_propagate(lit, cl);
break; break;
case l_false: case l_false:
m_repropagate_units.push_back(&cl);
set_conflict(cl); set_conflict(cl);
break; break;
case l_true: case l_true:
@ -242,11 +244,19 @@ namespace polysat {
break; break;
} }
} }
}
bool solver::can_repropagate() {
return !m_repropagate_lits.empty();
}
void solver::repropagate() {
while (!m_repropagate_lits.empty() && !is_conflict()) { while (!m_repropagate_lits.empty() && !is_conflict()) {
sat::literal lit = m_repropagate_lits.back(); sat::literal lit = m_repropagate_lits.back();
m_repropagate_lits.pop_back(); m_repropagate_lits.pop_back();
repropagate(lit); repropagate(lit);
} }
SASSERT(bool_watch_invariant());
} }
/** /**

2
src/math/polysat/solver.h
View file

@ -254,6 +254,8 @@ namespace polysat {
void erase_pwatch(pvar v, constraint* c); void erase_pwatch(pvar v, constraint* c);
void erase_pwatch(constraint* c); void erase_pwatch(constraint* c);
bool can_repropagate_units();
void repropagate_units();
bool can_repropagate(); bool can_repropagate();
void repropagate(); void repropagate();
void repropagate(sat::literal lit); void repropagate(sat::literal lit);