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

Also check clauses when returning SAT

Browse source
This commit is contained in:
Jakob Rath 2022-01-27 12:23:57 +01:00
parent be790b8892
commit 4236830a8e
2 changed files with 20 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/mul_ovfl_constraint.h
View file

@ -38,8 +38,8 @@ namespace polysat {
std::ostream& display(std::ostream& out) const override;
bool is_always_false(bool is_positive) const override;
void narrow(solver& s, bool is_positive) override;
bool is_currently_false(solver & s, bool is_positive) const;
bool is_currently_true(solver& s, bool is_positive) const;
bool is_currently_false(solver & s, bool is_positive) const override;
bool is_currently_true(solver& s, bool is_positive) const override;
bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override { return false; }
bool is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const override { return false; }

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

@ -144,12 +144,12 @@ namespace polysat {
// Axioms for quotient/remainder:
// a = b*q + r
// multiplication does not overflow in b*q
// addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r
// addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r (TODO: maybe the version with disjunction is easier for the solver; should compare later)
// b ≠ 0 ==> r < b
// b = 0 ==> q = -1
add_eq(b * q + r - a);
add_eq(a, b * q + r);
add_noovfl(b, q);
add_ule(r, b*q+r);
add_ule(r, b * q + r);
auto c1 = eq(b);
auto c2 = ult(r, b);
auto c3 = diseq(b);
@ -1081,8 +1081,22 @@ namespace polysat {
all_ok = all_ok && ok;
}
}
for (auto clauses : m_constraints.clauses()) {
for (auto cl : clauses) {
bool clause_ok = false;
for (sat::literal lit : *cl) {
bool ok = lit2cnstr(lit).is_currently_true(*this);
if (ok) {
clause_ok = true;
break;
}
}
LOG((clause_ok ? "PASS" : "FAIL") << ": " << show_deref(cl) << (cl->is_redundant() ? " (redundant)" : ""));
all_ok = all_ok && clause_ok;
}
}
if (all_ok) LOG("All good!");
return true;
return all_ok;
}
}