mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

Find more undetected bool/eval conflicts in viable::resolve_interval

Browse source
This commit is contained in:
Jakob Rath 2023-03-29 15:47:10 +02:00
parent 810a68ace9
commit d7930b3997
2 changed files with 32 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -276,9 +276,10 @@ namespace polysat {
SASSERT(!s.is_assigned(v));
m_level = s.m_level;
logger().begin_conflict(header_with_var("viable_interval v", v));
VERIFY(s.m_viable.resolve_interval(v, *this));
if (s.m_viable.resolve_interval(v, *this)) {
revert_pvar(v); // at this point, v is not assigned
}
SASSERT(!empty());
revert_pvar(v); // at this point, v is not assigned
}
void conflict::init_by_viable_fallback(pvar v, univariate_solver& us) {
@ -319,6 +320,7 @@ namespace polysat {
}
bool conflict::insert_or_replace(signed_constraint c) {
// TODO: what if we have already passed c in the trail in resolve_conflict? should check that. (probably restart the resolve_conflict loop with the new conflict?)
switch (c.bvalue(s)) {
case l_true:
// regular case

35
src/math/polysat/viable.cpp
View file

@ -1908,8 +1908,7 @@ namespace {
bool viable::resolve_interval(pvar v, conflict& core) {
DEBUG_CODE( log(v); );
if (has_viable(v))
return false;
VERIFY(!has_viable(v)); // does a pass over interval refinement, making sure the intervals actually exist
#if 0
// Prefer bit information as justifications
@ -1981,10 +1980,15 @@ namespace {
n = n1;
}
// verbose_stream() << e->interval << " " << e->side_cond << " " << e->src << ";\n";
signed_constraint c = s.m_constraints.elem(e->interval.hi(), n->interval.symbolic());
lemma.insert_try_eval(~c);
// lemma.insert_try_eval(~c);
VERIFY(c.is_currently_true(s));
if (c.bvalue(s) == l_false) {
core.reset();
core.init(~c);
return false;
}
lemma.insert_eval(~c);
for (auto sc : e->side_cond)
lemma.insert_eval(~sc);
@ -1997,8 +2001,25 @@ namespace {
}
while (e != first);
// TODO: violated in bench27
SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) != l_true; }));
// TODO: violated in 5133-min.smt2:
//
// viable lemma:
// 35: -31 <= -1*v17 + -1*v11*v0 + -1*v5*v2 + 32 [ b:l_true p:l_false bprop@0 idx:28 pwatched ]
// -22: v17 + v11*v0 + v6 + v5*v2 != 0 [ b:l_false p:l_undef assert@0 idx:8 pwatched dep:16 ]
// 36: v17 + v11*v0 + v5*v2 + 1 == 0 [ b:l_false p:l_false eval@39 idx:75 ]
// -7: -31 > v6 + 32 [ b:l_false p:l_undef assert@0 idx:17 pwatched dep:33 ]
// ASSERTION VIOLATION
// File: /Users/jakob/projects/z3/src/math/polysat/viable.cpp
// Line: 2036
// all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) != l_true; })
//
// Reason: there is an eval/bool conflict that we didn't discover before,
// because not-yet-assigned variables are watched but the constraint already evaluates due to cancellation of some terms.
//
// verbose_stream() << "viable lemma:\n";
// for (auto lit : lemma)
// verbose_stream() << " " << lit_pp(s, lit) << "\n";
VERIFY(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) != l_true; }));
core.add_lemma("viable", lemma.build());
core.logger().log(inf_fi(*this, v));