mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-21 20:02:05 +00:00
Code Activity

fixup overflow rules

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-01-01 13:40:48 -08:00
parent fb5f81cf75
commit 7dea0b855b
2 changed files with 32 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/sat/smt/polysat/monomials.cpp
View file

@ -102,6 +102,8 @@ namespace polysat {
return l_false; return l_false;
if (any_of(m_to_refine, [&](auto i) { return non_overflow_unit(m_monomials[i]); })) if (any_of(m_to_refine, [&](auto i) { return non_overflow_unit(m_monomials[i]); }))
return l_false; return l_false;
if (any_of(m_to_refine, [&](auto i) { return non_overflow_zero(m_monomials[i]); }))
return l_false;
if (any_of(m_to_refine, [&](auto i) { return parity0(m_monomials[i]); })) if (any_of(m_to_refine, [&](auto i) { return parity0(m_monomials[i]); }))
return l_false; return l_false;
if (any_of(m_to_refine, [&](auto i) { return parity(m_monomials[i]); })) if (any_of(m_to_refine, [&](auto i) { return parity(m_monomials[i]); }))
@ -234,12 +236,12 @@ namespace polysat {
pdd p = mon.args[0]; pdd p = mon.args[0];
constraint_or_dependency_vector clause; constraint_or_dependency_vector clause;
for (unsigned i = 1; i < mon.args.size(); ++i) { for (unsigned i = 1; i < mon.args.size(); ++i) {
clause.push_back(~C.umul_ovfl(p, mon.args[i])); clause.push_back(C.umul_ovfl(p, mon.args[i]));
p *= mon.args[i]; p *= mon.args[i];
} }
for (unsigned i = 0; i < mon.args.size(); ++i) for (unsigned i = 0; i < mon.args.size(); ++i)
if (i != big_index) if (i != big_index)
clause.push_back(~C.eq(mon.args[i])); clause.push_back(C.eq(mon.args[i]));
clause.push_back(C.ule(mon.args[big_index], mon.var)); clause.push_back(C.ule(mon.args[big_index], mon.var));
c.add_axiom("~ovfl*(p,q) & q != 0 => p <= p*q", clause, true); c.add_axiom("~ovfl*(p,q) & q != 0 => p <= p*q", clause, true);
return true; return true;
@ -258,7 +260,7 @@ namespace polysat {
pdd p = mon.args[0]; pdd p = mon.args[0];
clause.push_back(~C.eq(mon.var, 1)); clause.push_back(~C.eq(mon.var, 1));
for (unsigned i = 1; i < mon.args.size(); ++i) { for (unsigned i = 1; i < mon.args.size(); ++i) {
clause.push_back(~C.umul_ovfl(p, mon.args[i])); clause.push_back(C.umul_ovfl(p, mon.args[i]));
p *= mon.args[i]; p *= mon.args[i];
} }
for (auto const& q : mon.args) { for (auto const& q : mon.args) {
@ -269,6 +271,32 @@ namespace polysat {
return true; return true;
} }
// ~ovfl*(p,q) & p*q = 0 => p = 0 or q = 0
bool monomials::non_overflow_zero(monomial const& mon) {
if (mon.val != 0)
return false;
for (auto const& val : mon.arg_vals)
if (val == 0)
return false;
rational product(1);
for (auto const& val : mon.arg_vals)
product *= val;
if (product > mon.var.manager().max_value())
return false;
constraint_or_dependency_vector clause;
clause.push_back(~C.eq(mon.var));
pdd p = mon.args[0];
for (unsigned i = 1; i < mon.args.size(); ++i) {
clause.push_back(C.umul_ovfl(p, mon.args[i]));
p *= mon.args[i];
}
for (auto const& q : mon.args)
clause.push_back(C.eq(q));
c.add_axiom("~ovfl*(p,q) & p*q = 0 => p = 0 or q = 0", clause, true);
return false;
}
// parity(p*q) > 0 => parity(p) > 0 or parity(q) > 0 // parity(p*q) > 0 => parity(p) > 0 or parity(q) > 0
bool monomials::parity0(monomial const& mon) { bool monomials::parity0(monomial const& mon) {
if (mon.val.is_odd()) if (mon.val.is_odd())

1
src/sat/smt/polysat/monomials.h
View file

@ -77,6 +77,7 @@ namespace polysat {
bool parity(monomial const& mon); bool parity(monomial const& mon);
bool non_overflow_monotone(monomial const& mon); bool non_overflow_monotone(monomial const& mon);
bool non_overflow_unit(monomial const& mon); bool non_overflow_unit(monomial const& mon);
bool non_overflow_zero(monomial const& mon);
bool parity0(monomial const& mon); bool parity0(monomial const& mon);
bool prefix_overflow(monomial const& mon); bool prefix_overflow(monomial const& mon);