mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-27 14:33:38 -08:00
commit 1264fe462d
2 changed files with 19 additions and 5 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; std::ostream& display(std::ostream& out) const override;
bool is_always_false(bool is_positive) const override; bool is_always_false(bool is_positive) const override;
void narrow(solver& s, bool is_positive) override; void narrow(solver& s, bool is_positive) override;
bool is_currently_false(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; 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_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; } bool is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const override { return false; }

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

@ -144,10 +144,10 @@ namespace polysat {
// Axioms for quotient/remainder: // Axioms for quotient/remainder:
// a = b*q + r // a = b*q + r
// multiplication does not overflow in b*q // 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 ==> r < b
// b = 0 ==> q = -1 // b = 0 ==> q = -1
add_eq(b * q + r - a); add_eq(a, b * q + r);
add_noovfl(b, q); add_noovfl(b, q);
add_ule(r, b*q+r); add_ule(r, b*q+r);
@ -1082,8 +1082,22 @@ namespace polysat {
all_ok = all_ok && ok; 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!"); if (all_ok) LOG("All good!");
return true; return all_ok;
} }
} }