mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

Avoid creating tautological clauses for quot_rem

Browse source
This commit is contained in:
Jakob Rath 2023-10-16 12:01:20 +02:00
parent e96f69e76c
commit bb93a2ccb2
2 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -421,6 +421,8 @@ namespace polysat {
m_dedup.m_quot_rem_expr.insert(args, { q.var(), r.var() });
m_dedup.m_div_rem_list.push_back({ a, b, q.var(), r.var() });
LOG("quot_rem(" << a << ", " << b << ") = (" << q << ", " << r << ")");
// Axioms for quotient/remainder:
// a = b*q + r
// multiplication does not overflow in b*q
@ -443,8 +445,10 @@ namespace polysat {
#endif
auto c_eq = eq(b);
s.add_clause("[axiom] quot_rem 4", { c_eq, ult(r, b) }, false);
s.add_clause("[axiom] quot_rem 5", { ~c_eq, eq(q + 1) }, false);
if (!c_eq.is_always_true())
s.add_clause("[axiom] quot_rem 4", { c_eq, ult(r, b) }, false);
if (!c_eq.is_always_false())
s.add_clause("[axiom] quot_rem 5", { ~c_eq, eq(q + 1) }, false);
return {std::move(q), std::move(r)};
}

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

@ -1387,9 +1387,9 @@ namespace polysat {
clause_ref solver::mk_clause(char const* name, unsigned n, signed_constraint const* cs, bool is_redundant) {
clause_builder cb(*this, name);
cb.set_redundant(is_redundant);
for (unsigned i = 0; i < n; ++i)
cb.insert(cs[i]);
cb.set_redundant(is_redundant);
return cb.build();
}