mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

Fix/simplify constraint_manager::watch

Browse source
This commit is contained in:
Jakob Rath 2023-02-01 14:52:06 +01:00
parent 0d56edb65c
commit fe164c843d
2 changed files with 7 additions and 57 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/math/polysat/constraint_manager.cpp
View file

@ -143,46 +143,6 @@ namespace polysat {
if (cl.empty()) if (cl.empty())
return; return;
{
// First, try to bool-propagate.
// Otherwise, we might get a clause-conflict and a missed propagation after resolving the conflict.
// With this, we will get a constraint-conflict instead.
// TODO: maybe it makes sense to choose bool vs. eval depending on which has the lower level?
sat::literal undef_lit = sat::null_literal;
for (sat::literal lit : cl) {
if (s.m_bvars.is_false(lit))
continue;
if (s.m_bvars.is_true(lit)) {
undef_lit = sat::null_literal;
break;
}
SASSERT(!s.m_bvars.is_assigned(lit));
if (undef_lit == sat::null_literal)
undef_lit = lit;
else {
undef_lit = sat::null_literal;
break;
}
}
if (undef_lit != sat::null_literal)
s.assign_propagate(undef_lit, cl);
// this should be already done with insert_eval when constructing the clause (maybe not for non-redundant clauses?)
// (this loop also masks the mistake of calling clause_builder::insert instead of clause_builder::insert_eval)
for (sat::literal lit : cl) {
if (s.m_bvars.is_false(lit))
continue;
signed_constraint sc = s.lit2cnstr(lit);
if (sc.is_currently_false(s)) {
if (s.m_bvars.is_true(lit)) {
s.set_conflict(sc);
return;
}
s.assign_eval(~lit);
}
}
}
if (cl.size() == 1) { if (cl.size() == 1) {
if (s.m_bvars.is_false(cl[0])) if (s.m_bvars.is_false(cl[0]))
s.set_conflict(cl); s.set_conflict(cl);

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

@ -1193,30 +1193,20 @@ namespace polysat {
} }
} }
// Add clause to storage // Add clause to solver
void solver::add_clause(clause& clause) { void solver::add_clause(clause& clause) {
LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause); LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause);
for (sat::literal lit : clause) { for (sat::literal lit : clause) {
LOG(" " << lit_pp(*this, lit)); // Try to evaluate literals without boolean value.
// TODO: move into constraint_manager::watch // (Normally this should have been done already by using clause_builder::insert_eval/insert_try_eval when constructing the clause.)
if (!m_bvars.is_assigned(lit)) { if (!m_bvars.is_assigned(lit)) {
switch (lit2cnstr(lit).eval(*this)) { lbool const status = lit2cnstr(lit).eval(*this);
case l_true: if (status == l_true)
assign_eval(lit); assign_eval(lit);
break; else if (status == l_false)
case l_false:
assign_eval(~lit); assign_eval(~lit);
break;
default:
break;
}
}
// it could be that such a literal has been created previously but we don't detect it when e.g. narrowing a mul_ovfl_constraint
if (m_bvars.value(lit) == l_true) {
// in this case the clause is useless
LOG(" Clause is already true, skipping...");
return;
} }
LOG(" " << lit_pp(*this, lit));
} }
SASSERT(!clause.empty()); SASSERT(!clause.empty());
m_constraints.store(&clause); m_constraints.store(&clause);