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

add hooks for multiplication overflow

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-23 15:48:03 -08:00
parent d18a2427a4
commit 4e0604bc22
3 changed files with 72 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

71
src/math/polysat/saturation.cpp
View file

@ -54,11 +54,8 @@ namespace polysat {
auto i = inequality::from_ule(c);
return try_inequality(v, i, core);
}
#if 0
if (c->is_umul_ovfl())
return try_umul_ovfl(v, c, core);
#endif
return false;
}
@ -96,6 +93,24 @@ namespace polysat {
}
bool saturation::try_umul_ovfl(pvar v, signed_constraint const& c, conflict& core) {
#if 1
return false;
#else
SASSERT(c->is_umul_ovfl());
bool prop = false;
if (c.is_positive()) {
prop = try_umul_ovfl_bounds(v, c, core);
}
else {
prop = try_umul_noovfl_bounds(v, c, core);
if (false && try_umul_noovfl_lo(v, c, core))
prop = true;
}
return prop;
#endif
}
bool saturation::try_umul_noovfl_lo(pvar v, signed_constraint const& c, conflict& core) {
set_rule("[x] ~ovfl(x, y) => y = 0 or x <= x * y");
SASSERT(c->is_umul_ovfl());
if (!c.is_negative())
@ -117,6 +132,54 @@ namespace polysat {
return false;
}
/**
* ~ovfl(p, q) & p >= k => q < 2^N/k
*/
bool saturation::try_umul_noovfl_bounds(pvar x, signed_constraint const& c, conflict& core) {
set_rule("[x] ~ovfl(x, q) & x >= k => q <= (2^N-1)/k");
SASSERT(c->is_umul_ovfl());
SASSERT(c.is_negative());
auto const& ovfl = c->to_umul_ovfl();
auto p = ovfl.p(), q = ovfl.q();
auto X = s.var(x);
auto& m = p.manager();
rational p_val, q_val;
if (q == X)
std::swap(p, q);
if (p == X) {
vector<signed_constraint> x_ge_bound;
if (!s.try_eval(q, q_val))
return false;
if (!has_lower_bound(x, core, p_val, x_ge_bound))
return false;
if (p_val * q_val <= m.max_value())
return false;
m_lemma.reset();
m_lemma.insert_eval(~s.uge(X, p_val));
signed_constraint conseq = s.ule(q, floor(m.max_value()/p_val));
return propagate(x, core, c, conseq);
}
if (!s.try_eval(p, p_val) || !s.try_eval(q, q_val))
return false;
if (p_val * q_val <= m.max_value())
return false;
m_lemma.reset();
m_lemma.insert_eval(~s.uge(q, q_val));
signed_constraint conseq = s.ule(p, floor(m.max_value()/q_val));
return propagate(x, core, c, conseq);
}
/**
* ovfl(p, q) & p <= k => q > 2^N/k
*/
bool saturation::try_umul_ovfl_bounds(pvar v, signed_constraint const& c, conflict& core) {
SASSERT(c->is_umul_ovfl());
SASSERT(c.is_positive());
auto const& ovfl = c->to_umul_ovfl();
auto p = ovfl.p(), q = ovfl.q();
rational p_val, q_val;
return false;
}
signed_constraint saturation::ineq(bool is_strict, pdd const& lhs, pdd const& rhs) {
if (is_strict)
@ -1313,10 +1376,12 @@ namespace polysat {
}
// verbose_stream() << "TODO bound 1 " << a_l_b << " " << x_ge_bound << " " << b << " " << b_val << " " << y << "\n";
}
#if 0
if (has_lower_bound(x, core, x_bound, x_le_bound) && !x_le_bound.contains(a_l_b.as_signed_constraint())) {
// verbose_stream() << "TODO bound 2 " << a_l_b << " " << x_le_bound << "\n";
}
#endif
}
if (is_Y_l_AxB(x, a_l_b, y, a, b) && y.is_val() && s.try_eval(b, b_val)) {
// verbose_stream() << "TODO bound 3 " << a_l_b << "\n";

3
src/math/polysat/saturation.h
View file

@ -142,6 +142,9 @@ namespace polysat {
bool try_inequality(pvar v, inequality const& i, conflict& core);
bool try_umul_ovfl(pvar v, signed_constraint const& c, conflict& core);
bool try_umul_noovfl_lo(pvar v, signed_constraint const& c, conflict& core);
bool try_umul_noovfl_bounds(pvar v, signed_constraint const& c, conflict& core);
bool try_umul_ovfl_bounds(pvar v, signed_constraint const& c, conflict& core);
public:
saturation(solver& s);

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

@ -675,7 +675,6 @@ namespace polysat {
return !out_c.empty();
}
// TBD: generalize to multiple intervals similar to upper bound
bool viable::has_lower_bound(pvar v, rational& out_lo, vector<signed_constraint>& out_c) {
entry const* first = m_units[v];
entry const* e = first;
@ -688,7 +687,7 @@ namespace polysat {
auto const& lo = e->interval.lo();
auto const& hi = e->interval.hi();
if (lo.is_val() && hi.is_val()) {
if (out_c.empty() && (lo.val() == 0 || lo.val() > hi.val())) {
if (out_c.empty() && hi.val() != 0 && (lo.val() == 0 || lo.val() > hi.val())) {
out_c.push_back(e->src);
out_lo = hi.val();
found = true;