mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

Handle boolean conflict from input

Browse source
This commit is contained in:
Jakob Rath 2021-09-14 09:09:50 +02:00
parent 18710a86d7
commit 50a5e24c69
1 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -141,6 +141,8 @@ namespace polysat {
VERIFY(at_base_level()); VERIFY(at_base_level());
SASSERT(c); SASSERT(c);
SASSERT(activate || dep != null_dependency); // if we don't activate the constraint, we need the dependency to access it again later. SASSERT(activate || dep != null_dependency); // if we don't activate the constraint, we need the dependency to access it again later.
if (is_conflict())
return; // no need to do anything if we already have a conflict at base level
m_constraints.ensure_bvar(c.get()); m_constraints.ensure_bvar(c.get());
clause* unit = m_constraints.store(clause::from_unit(m_level, c, mk_dep_ref(dep))); clause* unit = m_constraints.store(clause::from_unit(m_level, c, mk_dep_ref(dep)));
c->set_unit_clause(unit); c->set_unit_clause(unit);
@ -155,9 +157,12 @@ namespace polysat {
#if ENABLE_LINEAR_SOLVER #if ENABLE_LINEAR_SOLVER
m_linear_solver.new_constraint(*c.get()); m_linear_solver.new_constraint(*c.get());
#endif #endif
// TODO: there is an issue when the input contains both c and ~c. (see test_ineq_basic2) if (activate) {
if (activate && !is_conflict()) if (c.bvalue(*this) == l_false)
propagate_bool(c.blit(), unit); m_conflict.set(c); // we already added ~c => conflict at base level
else
propagate_bool(c.blit(), unit);
}
} }
void solver::assign_eh(unsigned dep, bool is_true) { void solver::assign_eh(unsigned dep, bool is_true) {
@ -486,7 +491,6 @@ namespace polysat {
revert_bool_decision(lit); revert_bool_decision(lit);
return; return;
} }
SASSERT(m_bvars.is_propagation(var)); SASSERT(m_bvars.is_propagation(var));
resolve_bool(lit); resolve_bool(lit);
} }