mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Weaken evaluation for new constraints in viable lemma

Browse source
This commit is contained in:
Jakob Rath 2022-12-22 16:24:27 +01:00
parent be20c0d54e
commit 21ea05b31c
3 changed files with 27 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/math/polysat/clause_builder.cpp
View file

@ -75,15 +75,23 @@ namespace polysat {
m_literals.push_back(c.blit());
}
void clause_builder::insert_eval(sat::literal lit, bool status) {
insert_eval(m_solver->lit2cnstr(lit), status);
void clause_builder::insert_eval(sat::literal lit) {
insert_eval(m_solver->lit2cnstr(lit));
}
void clause_builder::insert_eval(signed_constraint c, bool status) {
if (c.bvalue(*m_solver) == l_undef) {
sat::literal lit = c.blit();
m_solver->assign_eval(status ? lit : ~lit);
}
void clause_builder::insert_eval(signed_constraint c) {
if (c.bvalue(*m_solver) == l_undef)
m_solver->assign_eval(~c.blit());
insert(c);
}
void clause_builder::insert_try_eval(sat::literal lit) {
insert_eval(m_solver->lit2cnstr(lit));
}
void clause_builder::insert_try_eval(signed_constraint c) {
if (c.bvalue(*m_solver) == l_undef && c.is_currently_false(*m_solver))
m_solver->assign_eval(~c.blit());
insert(c);
}
}

17
src/math/polysat/clause_builder.h
View file

@ -51,19 +51,20 @@ namespace polysat {
void insert(signed_constraint c);
void insert(inequality const& i) { insert(i.as_signed_constraint()); }
/// Insert constraints into the clause.
/// If they are not yet on the search stack, add them as evaluated to the given status.
/// \pre Constraint must evaluate to true or false according to the given status in the current assignment.
void insert_eval(sat::literal lit, bool status);
void insert_eval(signed_constraint c, bool status);
/// Insert constraints into the clause.
/// If they are not yet on the search stack, add them as evaluated to \b false.
/// \pre Constraint must be \b false in the current assignment.
void insert_eval(sat::literal lit) { insert_eval(lit, false); }
void insert_eval(signed_constraint c) { insert_eval(c, false); }
void insert_eval(sat::literal lit);
void insert_eval(signed_constraint c);
void insert_eval(inequality const& i) { insert_eval(i.as_signed_constraint()); }
/// Insert constraints into the clause.
/// If possible, evaluate them as in insert_eval.
/// Evaluation might not be possible if not all variables in the constraint are assigned.
/// \pre Constraint must be \b non-true in the current assignment.
void insert_try_eval(sat::literal lit);
void insert_try_eval(signed_constraint lit);
using const_iterator = decltype(m_literals)::const_iterator;
const_iterator begin() const { return m_literals.begin(); }
const_iterator end() const { return m_literals.end(); }

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

@ -969,7 +969,7 @@ namespace polysat {
auto lhs = hi - next_lo;
auto rhs = next_hi - next_lo;
signed_constraint c = s.m_constraints.ult(lhs, rhs);
lemma.insert_eval(~c);
lemma.insert_try_eval(~c); // "try" because linking constraint may contain unassigned variables, see test_polysat::test_bench23_fi_lemma for an example.
}
for (auto sc : e->side_cond)
lemma.insert_eval(~sc);
@ -980,7 +980,8 @@ namespace polysat {
}
while (e != first);
SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false || s.lit2cnstr(lit).is_currently_false(s); }));
// Doesn't hold anymore: we may get new constraints with unassigned variables, see test_polysat::test_bench23_fi_lemma.
// SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false || s.lit2cnstr(lit).is_currently_false(s); }));
// NSB review: bench23 exposes a scenario where s.m_bvars.value(lit) == l_true. So the viable lemma is mute, but the literal in the premise
// is a conflict.