mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

Add lemma try_umul_ovfl_noovfl for bench23

Browse source
This commit is contained in:
Jakob Rath 2023-02-22 16:32:51 +01:00
parent a8bfd01190
commit 14b2c38e7f
2 changed files with 45 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -103,12 +103,12 @@ namespace polysat {
return prop; return prop;
} }
bool saturation::try_umul_ovfl(pvar v, signed_constraint const& c, conflict& core) { bool saturation::try_umul_ovfl(pvar v, signed_constraint c, conflict& core) {
#if 1
return false;
#else
SASSERT(c->is_umul_ovfl()); SASSERT(c->is_umul_ovfl());
bool prop = false; bool prop = false;
if (try_umul_ovfl_noovfl(v, c, core))
prop = true;
#if 0
if (c.is_positive()) { if (c.is_positive()) {
prop = try_umul_ovfl_bounds(v, c, core); prop = try_umul_ovfl_bounds(v, c, core);
} }
@ -117,11 +117,40 @@ namespace polysat {
if (false && try_umul_noovfl_lo(v, c, core)) if (false && try_umul_noovfl_lo(v, c, core))
prop = true; prop = true;
} }
return prop;
#endif #endif
return prop;
} }
bool saturation::try_umul_noovfl_lo(pvar v, signed_constraint const& c, conflict& core) { bool saturation::try_umul_ovfl_noovfl(pvar v, signed_constraint c1, conflict& core) {
set_rule("[y] ovfl(x, y) & ~ovfl(y, z) ==> x > z");
SASSERT(c1->is_umul_ovfl());
if (!c1.is_positive()) // since we search for both premises in the core, break symmetry by requiring c1 to be positive
return false;
pdd p = c1->to_umul_ovfl().p();
pdd q = c1->to_umul_ovfl().q();
for (auto c2 : core) {
if (!c2.is_negative())
continue;
if (!c2->is_umul_ovfl())
continue;
pdd r = c2->to_umul_ovfl().p();
pdd u = c2->to_umul_ovfl().q();
if (p == u || q == u)
swap(r, u);
if (q == r || q == u)
swap(p, q);
if (p != r)
continue;
m_lemma.reset();
m_lemma.insert(~c1);
m_lemma.insert(~c2);
if (propagate(v, core, s.ult(u, q)))
return true;
}
return false;
}
bool saturation::try_umul_noovfl_lo(pvar v, signed_constraint c, conflict& core) {
set_rule("[x] ~ovfl(x, y) => y = 0 or x <= x * y"); set_rule("[x] ~ovfl(x, y) => y = 0 or x <= x * y");
SASSERT(c->is_umul_ovfl()); SASSERT(c->is_umul_ovfl());
if (!c.is_negative()) if (!c.is_negative())
@ -145,9 +174,9 @@ namespace polysat {
/** /**
* ~ovfl(p, q) & p >= k => q < 2^N/k * ~ovfl(p, q) & p >= k => q < 2^N/k
* TODO: subusmed by narrowing inferences? * TODO: subsumed by narrowing inferences?
*/ */
bool saturation::try_umul_noovfl_bounds(pvar x, signed_constraint const& c, conflict& core) { bool saturation::try_umul_noovfl_bounds(pvar x, signed_constraint c, conflict& core) {
set_rule("[x] ~ovfl(x, q) & x >= k => q <= (2^N-1)/k"); set_rule("[x] ~ovfl(x, q) & x >= k => q <= (2^N-1)/k");
SASSERT(c->is_umul_ovfl()); SASSERT(c->is_umul_ovfl());
SASSERT(c.is_negative()); SASSERT(c.is_negative());
@ -184,7 +213,7 @@ namespace polysat {
/** /**
* ovfl(p, q) & p <= k => q > 2^N/k * ovfl(p, q) & p <= k => q > 2^N/k
*/ */
bool saturation::try_umul_ovfl_bounds(pvar v, signed_constraint const& c, conflict& core) { bool saturation::try_umul_ovfl_bounds(pvar v, signed_constraint c, conflict& core) {
SASSERT(c->is_umul_ovfl()); SASSERT(c->is_umul_ovfl());
SASSERT(c.is_positive()); SASSERT(c.is_positive());
auto const& ovfl = c->to_umul_ovfl(); auto const& ovfl = c->to_umul_ovfl();
@ -204,7 +233,7 @@ namespace polysat {
return propagate(v, core, crit.as_signed_constraint(), c); return propagate(v, core, crit.as_signed_constraint(), c);
} }
bool saturation::propagate(pvar v, conflict& core, signed_constraint const& crit, signed_constraint c) { bool saturation::propagate(pvar v, conflict& core, signed_constraint crit, signed_constraint c) {
m_lemma.insert(~crit); m_lemma.insert(~crit);
return propagate(v, core, c); return propagate(v, core, c);
} }

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

@ -39,7 +39,7 @@ namespace polysat {
signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs); signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs);
void log_lemma(pvar v, conflict& core); void log_lemma(pvar v, conflict& core);
bool propagate(pvar v, conflict& core, signed_constraint const& crit1, signed_constraint c); bool propagate(pvar v, conflict& core, signed_constraint crit1, signed_constraint c);
bool propagate(pvar v, conflict& core, inequality const& crit1, signed_constraint c); bool propagate(pvar v, conflict& core, inequality const& crit1, signed_constraint c);
bool propagate(pvar v, conflict& core, signed_constraint c); bool propagate(pvar v, conflict& core, signed_constraint c);
bool add_conflict(pvar v, conflict& core, inequality const& crit1, signed_constraint c); bool add_conflict(pvar v, conflict& core, inequality const& crit1, signed_constraint c);
@ -165,10 +165,11 @@ namespace polysat {
bool try_inequality(pvar v, inequality const& i, conflict& core); 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_ovfl(pvar v, signed_constraint c, conflict& core);
bool try_umul_noovfl_lo(pvar v, signed_constraint const& c, conflict& core); bool try_umul_ovfl_noovfl(pvar v, signed_constraint c, conflict& core);
bool try_umul_noovfl_bounds(pvar v, signed_constraint const& c, conflict& core); bool try_umul_noovfl_lo(pvar v, signed_constraint c, conflict& core);
bool try_umul_ovfl_bounds(pvar v, signed_constraint const& c, conflict& core); bool try_umul_noovfl_bounds(pvar v, signed_constraint c, conflict& core);
bool try_umul_ovfl_bounds(pvar v, signed_constraint c, conflict& core);
public: public:
saturation(solver& s); saturation(solver& s);