mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-14 23:05:26 +00:00
Code Activity

skip always-true constraints

Browse source
This commit is contained in:
Jakob Rath 2023-01-25 12:34:01 +01:00
parent 223f9fffed
commit 88d11c9381
1 changed files with 22 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -162,25 +162,34 @@ namespace polysat {
SASSERT(dep == null_dependency && "track dependencies is TODO"); SASSERT(dep == null_dependency && "track dependencies is TODO");
return; return;
case l_true: case l_true:
// constraint c is already asserted // constraint c is already asserted => ignore
SASSERT(m_bvars.level(lit) <= m_level); SASSERT(m_bvars.level(lit) <= m_level);
break; return;
case l_undef: case l_undef:
if (c.is_always_false()) {
LOG("Always false: " << c);
// asserted an always-false constraint
set_conflict_at_base_level();
return;
}
m_bvars.assumption(lit, m_level, dep);
m_trail.push_back(trail_instr_t::assign_bool_i);
m_search.push_boolean(lit);
if (c.is_currently_false(*this))
set_conflict(c);
break; break;
default: default:
UNREACHABLE(); UNREACHABLE();
} }
switch (c.eval()) {
case l_false:
// asserted an always-false constraint => conflict at base level
LOG("Always false: " << c);
set_conflict_at_base_level();
SASSERT(dep == null_dependency && "track dependencies is TODO");
return;
case l_true:
// asserted an always-true constraint => ignore
return;
case l_undef:
break;
default:
UNREACHABLE();
}
m_bvars.assumption(lit, m_level, dep);
m_trail.push_back(trail_instr_t::assign_bool_i);
m_search.push_boolean(lit);
if (c.is_currently_false(*this))
set_conflict(c);
#if ENABLE_LINEAR_SOLVER #if ENABLE_LINEAR_SOLVER
m_linear_solver.new_constraint(*c.get()); m_linear_solver.new_constraint(*c.get());
#endif #endif