mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Update resolve_value

Browse source
This commit is contained in:
Jakob Rath 2022-11-22 13:47:31 +01:00
parent a144a09ede
commit 85a633a3e0
2 changed files with 26 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -209,8 +209,7 @@ namespace polysat {
}
else {
// Constraint c conflicts with the variable assignment
// SASSERT(c.bvalue(s) == l_true); // "morally" the bvalue should always be true. But (at least for now) some literals may be undef when they are only justified by a side lemma.
// TODO: maybe we can set them to true (without putting them on the search stack). But need to make sure to set them to false when finalizing the conflict; and before backjumping/learning. (tag:true_by_side_lemma)
SASSERT_EQ(c.bvalue(s), l_true);
SASSERT(c.is_currently_false(s));
insert(c);
insert_vars(c);
@ -223,7 +222,7 @@ namespace polysat {
m_level = s.m_level;
for (auto lit : cl) {
auto c = s.lit2cnstr(lit);
SASSERT(c.bvalue(s) == l_false);
SASSERT_EQ(c.bvalue(s), l_false);
insert(~c);
}
SASSERT(!empty());
@ -269,7 +268,7 @@ namespace polysat {
if (c.is_always_true())
return;
LOG("Inserting " << lit_pp(s, c));
// SASSERT_EQ(c.bvalue(s), l_true); // TODO: see comment in 'set_impl' (tag:true_by_side_lemma)
SASSERT_EQ(c.bvalue(s), l_true);
SASSERT(!c.is_always_false()); // if we added c, the core would be a tautology
SASSERT(!c->vars().empty());
m_literals.insert(c.blit().index());
@ -433,27 +432,22 @@ namespace polysat {
bool conflict::resolve_value(pvar v) {
SASSERT(contains_pvar(v));
auto const& j = s.m_justification[v];
SASSERT(s.m_justification[v].is_propagation());
s.inc_activity(v);
m_vars.remove(v);
if (j.is_propagation()) {
for (auto const& c : s.m_viable.get_constraints(v))
insert_eval(c);
for (auto const& i : s.m_viable.units(v)) {
insert_eval(s.eq(i.lo(), i.lo_val()));
insert_eval(s.eq(i.hi(), i.hi_val()));
}
m_vars.remove(v);
for (auto const& c : s.m_viable.get_constraints(v))
insert(c);
for (auto const& i : s.m_viable.units(v)) {
insert(s.eq(i.lo(), i.lo_val()));
insert(s.eq(i.hi(), i.hi_val()));
}
logger().log(inf_resolve_value(s, v));
if (m_resolver->try_resolve_value(v, *this))
return true;
// Need to keep the variable in case of decision
if (s.is_assigned(v) && j.is_decision())
m_vars.insert(v);
return false;
}

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

@ -700,18 +700,25 @@ namespace polysat {
// Resolve over variable assignment
pvar v = item.var();
if (!m_conflict.is_relevant_pvar(v)) {
// m_search.pop_assignment();
continue;
}
LOG_H2("Working on " << search_item_pp(m_search, item));
LOG(m_justification[v]);
LOG("Conflict: " << m_conflict);
justification& j = m_justification[v];
if (j.level() > base_level() && !m_conflict.resolve_value(v) && j.is_decision()) {
if (j.is_decision()) {
if (j.level() <= base_level())
break;
revert_decision(v);
return;
}
// m_search.pop_assignment();
if (j.level() <= base_level()) // propagation level may be out of order (cf. replay)
continue;
m_conflict.resolve_value(v);
// if (j.level() > base_level() && /* !m_conflict.resolve_value(v) && */ j.is_decision()) {
// revert_decision(v);
// return;
// }
}
else {
// Resolve over boolean literal
@ -724,11 +731,10 @@ namespace polysat {
LOG(bool_justification_pp(m_bvars, lit));
LOG("Literal " << lit << " is " << lit2cnstr(lit));
LOG("Conflict: " << m_conflict);
if (m_bvars.level(var) <= base_level()) {
// 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.
// 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.
if (m_bvars.level(var) <= base_level())
continue;
}
SASSERT(!m_bvars.is_assumption(var));
if (m_bvars.is_decision(var)) {
revert_bool_decision(lit);
@ -968,12 +974,11 @@ namespace polysat {
}
void solver::assign_eval(sat::literal lit) {
// SASSERT(lit2cnstr(lit).is_currently_true(*this)); // "morally" this should hold, but currently fails because of pop_assignment during resolve_conflict
SASSERT(!lit2cnstr(lit).is_currently_false(*this));
signed_constraint const c = lit2cnstr(lit);
SASSERT(c.is_currently_true(*this));
unsigned level = 0;
// NOTE: constraint may be evaluated even if some variables are still unassigned (e.g., 0*x doesn't depend on x).
// TODO: level might be too low! because pop_assignment may already have removed necessary variables (cf. comment on assertion above).
for (auto v : lit2cnstr(lit)->vars())
for (auto v : c->vars())
if (is_assigned(v))
level = std::max(get_level(v), level);
m_bvars.eval(lit, level);