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

less eval

Browse source
This commit is contained in:
Jakob Rath 2023-02-03 17:43:07 +01:00
parent 1a733a3a50
commit 539a4e4eae
2 changed files with 11 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/math/polysat/conflict.cpp
View file

@ -511,11 +511,17 @@ namespace polysat {
auto const enqueue_lit = [&](sat::literal lit) { auto const enqueue_lit = [&](sat::literal lit) {
if (done_lits.contains(lit)) if (done_lits.contains(lit))
return; return;
if (!s.m_bvars.is_assigned(lit))
return;
// verbose_stream() << "enqueue " << lit_pp(s, lit) << "\n"; // verbose_stream() << "enqueue " << lit_pp(s, lit) << "\n";
todo_lits.push_back(lit); todo_lits.push_back(lit);
done_lits.insert(lit); done_lits.insert(lit);
}; };
auto const enqueue_constraint = [&](signed_constraint c) {
enqueue_lit(c.blit());
};
auto const enqueue_var = [&](pvar v) { auto const enqueue_var = [&](pvar v) {
if (done_vars.contains(v)) if (done_vars.contains(v))
return; return;
@ -526,7 +532,7 @@ namespace polysat {
// Starting at literals/variables in the conflict, chase propagations backwards and accumulate dependencies. // Starting at literals/variables in the conflict, chase propagations backwards and accumulate dependencies.
for (signed_constraint c : *this) for (signed_constraint c : *this)
enqueue_lit(c.blit()); enqueue_constraint(c);
for (pvar v : m_vars) for (pvar v : m_vars)
enqueue_var(v); enqueue_var(v);
@ -540,10 +546,10 @@ namespace polysat {
SASSERT(s.m_justification[v].is_propagation()); SASSERT(s.m_justification[v].is_propagation());
for (signed_constraint c : s.m_viable.get_constraints(v)) for (signed_constraint c : s.m_viable.get_constraints(v))
enqueue_lit(c.blit()); enqueue_constraint(c);
for (auto const& i : s.m_viable.units(v)) { for (auto const& i : s.m_viable.units(v)) {
enqueue_lit(s.try_eval(s.eq(i.lo(), i.lo_val()))); enqueue_constraint(s.eq(i.lo(), i.lo_val()));
enqueue_lit(s.try_eval(s.eq(i.hi(), i.hi_val()))); enqueue_constraint(s.eq(i.hi(), i.hi_val()));
} }
} }
while (!todo_lits.empty()) { while (!todo_lits.empty()) {

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

@ -802,7 +802,7 @@ namespace polysat {
continue; continue;
LOG_H2("Working on " << search_item_pp(m_search, item)); LOG_H2("Working on " << search_item_pp(m_search, item));
LOG(bool_justification_pp(m_bvars, lit)); LOG(bool_justification_pp(m_bvars, lit));
LOG("Literal " << lit << " is " << lit2cnstr(lit)); LOG("Literal " << lit_pp(*this, lit));
LOG("Conflict: " << m_conflict); LOG("Conflict: " << m_conflict);
// NOTE: the levels of boolean literals on the stack aren't always ordered by level (cf. replay functionality in pop_levels). // NOTE: the levels of boolean literals on the stack aren't always ordered by level (cf. replay functionality in pop_levels).
// Thus we can only skip base level literals here, instead of aborting the loop. // Thus we can only skip base level literals here, instead of aborting the loop.