mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

ups

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-15 14:13:01 -08:00
parent 02369647a0
commit 8f8d88bc9d
1 changed files with 31 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

56
src/math/polysat/op_constraint.cpp
View file

@ -25,7 +25,7 @@ Additional possible functionality on constraints:
namespace polysat { namespace polysat {
op_constraint::op_constraint(constraint_manager& m, code c, pdd const& p, pdd const& q, pdd const& r): op_constraint::op_constraint(constraint_manager& m, code c, pdd const& p, pdd const& q, pdd const& r) :
constraint(m, ckind_t::op_t), m_op(c), m_p(p), m_q(q), m_r(r) { constraint(m, ckind_t::op_t), m_op(c), m_p(p), m_q(q), m_r(r) {
m_vars.append(p.free_vars()); m_vars.append(p.free_vars());
for (auto v : q.free_vars()) for (auto v : q.free_vars())
@ -34,17 +34,17 @@ namespace polysat {
for (auto v : r.free_vars()) for (auto v : r.free_vars())
if (!m_vars.contains(v)) if (!m_vars.contains(v))
m_vars.push_back(v); m_vars.push_back(v);
} }
lbool op_constraint::eval(pdd const& p, pdd const& q, pdd const& r) const { lbool op_constraint::eval(pdd const& p, pdd const& q, pdd const& r) const {
switch (m_op) { switch (m_op) {
case code::lshr_op: case code::lshr_op:
return eval_lshr(p, q, r); return eval_lshr(p, q, r);
default: default:
return l_undef; return l_undef;
} }
} }
bool op_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const { bool op_constraint::is_always_false(bool is_positive, pdd const& p, pdd const& q, pdd const& r) const {
switch (eval(p, q, r)) { switch (eval(p, q, r)) {
case l_true: return !is_positive; case l_true: return !is_positive;
@ -111,7 +111,7 @@ namespace polysat {
/** /**
* Propagate consequences or detect conflicts based on partial assignments. * Propagate consequences or detect conflicts based on partial assignments.
* *
* We can assume that op_constraint is only asserted positive. * We can assume that op_constraint is only asserted positive.
*/ */
@ -132,8 +132,8 @@ namespace polysat {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
break; break;
} }
if (!s.is_conflict() && is_currently_false(s.assignment(), is_positive)) if (!s.is_conflict() && is_currently_false(s.assignment(), is_positive))
s.set_conflict(signed_constraint(this, is_positive)); s.set_conflict(signed_constraint(this, is_positive));
} }
unsigned op_constraint::hash() const { unsigned op_constraint::hash() const {
@ -175,16 +175,21 @@ namespace polysat {
signed_constraint lshr(this, true); signed_constraint lshr(this, true);
if (pv.is_val() && rv.is_val() && rv.val() > pv.val()) if (pv.is_val() && rv.is_val() && rv.val() > pv.val())
s.add_clause(~lshr, s.ule(r(), p()), true); // r <= p // r <= p
else if (qv.is_val() && qv.val() >= K && rv.is_val() && !rv.is_zero()) s.add_clause(~lshr, s.ule(r(), p()), true);
s.add_clause(~lshr, ~s.ule(K, q()), s.eq(r()), true); // q >= K -> r = 0 else if (qv.is_val() && qv.val() >= K && rv.is_val() && !rv.is_zero())
else if (qv.is_zero() && pv.is_val() && rv.is_val() && pv != rv) { // q >= K -> r = 0
s.add_clause(~lshr, ~s.eq(q()), s.eq(p(), r()), true); // q != 0 & p > 0 => r < p s.add_clause(~lshr, ~s.ule(K, q()), s.eq(r()), true);
else if (qv.is_val() && !qv.is_zero() && pv.is_val() && rv.is_val() && !pv.is_zero() && pv.val() <= rv.val()) { else if (qv.is_zero() && pv.is_val() && rv.is_val() && pv != rv)
s.add_clause(~lshr, s.eq(q()), s.ule(p(), 0), s.ult(r(), p()), true); // q >= k -> r <= 2^{K-k-1} // q = 0 -> p = r
else if (qv.is_val() && !qv.is_zero() && qv.val() < K && rv.is_val() && s.add_clause(~lshr, ~s.eq(q()), s.eq(p(), r()), true);
rv.val() > rational::power_of_two(K - qv.val().get_unsigned() - 1)) { else if (qv.is_val() && !qv.is_zero() && pv.is_val() && rv.is_val() && !pv.is_zero() && pv.val() <= rv.val())
// q != 0 & p > 0 => r < p
s.add_clause(~lshr, s.eq(q()), s.ule(p(), 0), s.ult(r(), p()), true);
else if (qv.is_val() && !qv.is_zero() && qv.val() < K && rv.is_val() &&
rv.val() > rational::power_of_two(K - qv.val().get_unsigned() - 1))
// q >= k -> r <= 2^{K-k-1}
s.add_clause(~lshr, ~s.ule(qv.val(), q()), s.ule(r(), rational::power_of_two(K - qv.val().get_unsigned() - 1)), true); s.add_clause(~lshr, ~s.ule(qv.val(), q()), s.ule(r(), rational::power_of_two(K - qv.val().get_unsigned() - 1)), true);
// q = k -> r[i - k] = p[i] for K - k <= i < K // q = k -> r[i - k] = p[i] for K - k <= i < K
else if (pv.is_val() && rv.is_val() && qv.is_val() && !qv.is_zero()) { else if (pv.is_val() && rv.is_val() && qv.is_val() && !qv.is_zero()) {
@ -234,16 +239,16 @@ namespace polysat {
auto rv = r().subst_val(s.assignment()); auto rv = r().subst_val(s.assignment());
signed_constraint andc(this, true); signed_constraint andc(this, true);
if (pv.is_val() && rv.is_val() && rv.val() > pv.val()) if (pv.is_val() && rv.is_val() && rv.val() > pv.val())
s.add_clause(~andc, s.ule(r(), p()), true); s.add_clause(~andc, s.ule(r(), p()), true);
else if (qv.is_val() && rv.is_val() && rv.val() > qv.val()) else if (qv.is_val() && rv.is_val() && rv.val() > qv.val())
s.add_clause(~andc, s.ule(r(), q()), true); s.add_clause(~andc, s.ule(r(), q()), true);
else if (pv.is_val() && qv.is_val() && rv.is_val() && pv == qv && rv != pv) else if (pv.is_val() && qv.is_val() && rv.is_val() && pv == qv && rv != pv)
s.add_clause(~andc, ~s.eq(p(), q()), s.eq(r(), p()), true); s.add_clause(~andc, ~s.eq(p(), q()), s.eq(r(), p()), true);
else if (pv.is_zero() && rv.is_val() && !rv.is_zero()) else if (pv.is_zero() && rv.is_val() && !rv.is_zero())
s.add_clause(~andc, ~s.eq(p()), s.eq(r()), true); s.add_clause(~andc, ~s.eq(p()), s.eq(r()), true);
else if (qv.is_zero() && rv.is_val() && !rv.is_zero()) else if (qv.is_zero() && rv.is_val() && !rv.is_zero())
s.add_clause(~andc, ~s.eq(q()), s.eq(r()), true); s.add_clause(~andc, ~s.eq(q()), s.eq(r()), true);
else if (pv.is_val() && qv.is_val() && rv.is_val()) { else if (pv.is_val() && qv.is_val() && rv.is_val()) {
unsigned K = p().manager().power_of_2(); unsigned K = p().manager().power_of_2();
for (unsigned i = 0; i < K; ++i) { for (unsigned i = 0; i < K; ++i) {
@ -261,6 +266,7 @@ namespace polysat {
else else
UNREACHABLE(); UNREACHABLE();
return; return;
}
} }
} }
} }