mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 17:45:32 +00:00
Merge remote-tracking branch 'origin/polysat' into polysat
This commit is contained in:
Jakob Rath
commit
8347c043e1
17 changed files with 1106 additions and 136 deletions
|
|
@ -234,7 +234,7 @@ namespace polysat {
|
|||
m_lemmas.push_back(&cl);
|
||||
|
||||
SASSERT(!empty());
|
||||
logger().begin_conflict();
|
||||
logger().begin_conflict(cl.name());
|
||||
}
|
||||
|
||||
void conflict::init_by_viable_interval(pvar v) {
|
||||
|
|
|
|||
|
|
@ -513,4 +513,49 @@ namespace polysat {
|
|||
return m.mk_val(p.val().pseudo_inverse(m.power_of_2()));
|
||||
return mk_op_term(op_constraint::code::inv_op, p, m.zero());
|
||||
}
|
||||
|
||||
pdd constraint_manager::udiv(pdd const& p, pdd const& q) {
|
||||
return div_rem_op_constraint(p, q).first;
|
||||
}
|
||||
|
||||
pdd constraint_manager::urem(pdd const& p, pdd const& q) {
|
||||
return div_rem_op_constraint(p, q).second;
|
||||
}
|
||||
|
||||
/** unsigned quotient/remainder */
|
||||
std::pair<pdd, pdd> constraint_manager::div_rem_op_constraint(pdd const& a, pdd const& b) {
|
||||
auto& m = a.manager();
|
||||
unsigned sz = m.power_of_2();
|
||||
if (b.is_zero()) {
|
||||
// By SMT-LIB specification, b = 0 ==> q = -1, r = a.
|
||||
return {m.mk_val(m.max_value()), a};
|
||||
}
|
||||
if (b.is_one()) {
|
||||
return {a, m.zero()};
|
||||
}
|
||||
if (a.is_val() && b.is_val()) {
|
||||
rational const av = a.val();
|
||||
rational const bv = b.val();
|
||||
SASSERT(!bv.is_zero());
|
||||
rational rv;
|
||||
rational qv = machine_div_rem(av, bv, rv);
|
||||
pdd q = m.mk_val(qv);
|
||||
pdd r = m.mk_val(rv);
|
||||
SASSERT_EQ(a, b * q + r);
|
||||
SASSERT(b.val()*q.val() + r.val() <= m.max_value());
|
||||
SASSERT(r.val() <= (b*q+r).val());
|
||||
SASSERT(r.val() < b.val());
|
||||
return {std::move(q), std::move(r)};
|
||||
}
|
||||
|
||||
pdd quot = mk_op_term(op_constraint::code::udiv_op, a, b);
|
||||
pdd rem = mk_op_term(op_constraint::code::urem_op, a, b);
|
||||
|
||||
op_constraint* op1 = (op_constraint*)mk_op_constraint(op_constraint::code::udiv_op, a, b, quot).get();
|
||||
op_constraint* op2 = (op_constraint*)mk_op_constraint(op_constraint::code::urem_op, a, b, quot).get();
|
||||
op1->m_linked = op2;
|
||||
op2->m_linked = op1;
|
||||
|
||||
return {std::move(quot), std::move(rem)};
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -87,6 +87,8 @@ namespace polysat {
|
|||
signed_constraint mk_op_constraint(op_constraint::code op, pdd const& p, pdd const& q, pdd const& r);
|
||||
pdd mk_op_term(op_constraint::code op, pdd const& p, pdd const& q);
|
||||
|
||||
std::pair<pdd, pdd> div_rem_op_constraint(const pdd& p, const pdd& q);
|
||||
|
||||
public:
|
||||
constraint_manager(solver& s);
|
||||
~constraint_manager();
|
||||
|
|
@ -132,6 +134,9 @@ namespace polysat {
|
|||
pdd bnor(pdd const& p, pdd const& q);
|
||||
pdd bxnor(pdd const& p, pdd const& q);
|
||||
pdd pseudo_inv(pdd const& p);
|
||||
|
||||
pdd udiv(pdd const& a, pdd const& b);
|
||||
pdd urem(pdd const& a, pdd const& b);
|
||||
|
||||
constraint* const* begin() const { return m_constraints.data(); }
|
||||
constraint* const* end() const { return m_constraints.data() + m_constraints.size(); }
|
||||
|
|
|
|||
|
|
@ -41,7 +41,7 @@ namespace polysat {
|
|||
backtrack _backtrack(fi.side_cond);
|
||||
|
||||
fi.coeff = 1;
|
||||
fi.src = c;
|
||||
fi.src.push_back(c);
|
||||
|
||||
// eval(lhs) = a1*v + eval(e1) = a1*v + b1
|
||||
// eval(rhs) = a2*v + eval(e2) = a2*v + b2
|
||||
|
|
@ -135,7 +135,7 @@ namespace polysat {
|
|||
backtrack _backtrack(fi.side_cond);
|
||||
|
||||
fi.coeff = 1;
|
||||
fi.src = c;
|
||||
fi.src.push_back(c);
|
||||
|
||||
struct show {
|
||||
forbidden_intervals& f;
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ namespace polysat {
|
|||
struct fi_record {
|
||||
eval_interval interval;
|
||||
vector<signed_constraint> side_cond;
|
||||
signed_constraint src;
|
||||
vector<signed_constraint> src; // only units may have multiple src (as they can consist of contracted bit constraints)
|
||||
rational coeff;
|
||||
|
||||
/** Create invalid fi_record */
|
||||
|
|
|
|||
|
|
@ -65,6 +65,10 @@ namespace polysat {
|
|||
return eval_and(p, q, r);
|
||||
case code::inv_op:
|
||||
return eval_inv(p, r);
|
||||
case code::udiv_op:
|
||||
return eval_udiv(p, q, r);
|
||||
case code::urem_op:
|
||||
return eval_urem(p, q, r);
|
||||
default:
|
||||
return l_undef;
|
||||
}
|
||||
|
|
@ -90,6 +94,10 @@ namespace polysat {
|
|||
return out << "&";
|
||||
case op_constraint::code::inv_op:
|
||||
return out << "inv";
|
||||
case op_constraint::code::udiv_op:
|
||||
return out << "/";
|
||||
case op_constraint::code::urem_op:
|
||||
return out << "%";
|
||||
default:
|
||||
UNREACHABLE();
|
||||
return out;
|
||||
|
|
@ -142,6 +150,10 @@ namespace polysat {
|
|||
return propagate_bits_shl(s, is_positive);
|
||||
case code::and_op:
|
||||
return propagate_bits_and(s, is_positive);
|
||||
case code::inv_op:
|
||||
case code::udiv_op:
|
||||
case code::urem_op:
|
||||
return false;
|
||||
default:
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return false;
|
||||
|
|
@ -180,15 +192,12 @@ namespace polysat {
|
|||
|
||||
void op_constraint::activate(solver& s) {
|
||||
switch (m_op) {
|
||||
case code::lshr_op:
|
||||
break;
|
||||
case code::shl_op:
|
||||
break;
|
||||
case code::and_op:
|
||||
// handle masking of high order bits
|
||||
activate_and(s);
|
||||
break;
|
||||
case code::inv_op:
|
||||
case code::udiv_op: // division & remainder axioms (as they always occur as pairs; we do this only for divisions)
|
||||
activate_udiv(s);
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
|
|
@ -266,7 +275,7 @@ namespace polysat {
|
|||
}
|
||||
else {
|
||||
// forward propagation
|
||||
SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
|
||||
/*SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
|
||||
if (qv.is_val() && !rv.is_val()) {
|
||||
const rational& qr = qv.val();
|
||||
if (qr >= m.power_of_2())
|
||||
|
|
@ -276,7 +285,7 @@ namespace polysat {
|
|||
const rational& pr = pv.val();
|
||||
return s.mk_clause(~lshr, ~s.eq(p(), m.mk_val(pr)), ~s.eq(q(), m.mk_val(qr)), s.eq(r(), m.mk_val(machine_div(pr, rational::power_of_two(qr.get_unsigned())))), true);
|
||||
}
|
||||
}
|
||||
}*/
|
||||
}
|
||||
return {};
|
||||
}
|
||||
|
|
@ -356,7 +365,7 @@ namespace polysat {
|
|||
}
|
||||
else {
|
||||
// forward propagation
|
||||
SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
|
||||
/*SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val()));
|
||||
if (qv.is_val() && !rv.is_val()) {
|
||||
const rational& qr = qv.val();
|
||||
if (qr >= m.power_of_2())
|
||||
|
|
@ -366,7 +375,7 @@ namespace polysat {
|
|||
const rational& pr = pv.val();
|
||||
return s.mk_clause(~shl, ~s.eq(p(), m.mk_val(pr)), ~s.eq(q(), m.mk_val(qr)), s.eq(r(), m.mk_val(rational::power_of_two(qr.get_unsigned()) * pr)), true);
|
||||
}
|
||||
}
|
||||
}*/
|
||||
}
|
||||
return {};
|
||||
}
|
||||
|
|
@ -543,8 +552,8 @@ namespace polysat {
|
|||
return s.mk_clause(~andc, s.bit(q(), i), ~s.bit(r(), i), true);
|
||||
else
|
||||
UNREACHABLE();
|
||||
return {};
|
||||
}
|
||||
return {};
|
||||
}
|
||||
|
||||
// Propagate r if p or q are 0
|
||||
|
|
@ -553,8 +562,9 @@ namespace polysat {
|
|||
if (qv.is_zero() && !rv.is_zero()) // rv not necessarily fully evaluated
|
||||
return s.mk_clause(~andc, s.ule(r(), q()), true);
|
||||
// p = a && q = b ==> r = a & b
|
||||
if (pv.is_val() && qv.is_val() && !rv.is_val())
|
||||
/*if (pv.is_val() && qv.is_val() && !rv.is_val()) {
|
||||
return s.mk_clause(~andc, ~s.eq(p(), pv), ~s.eq(q(), qv), s.eq(r(), bitwise_and(pv.val(), qv.val())), true);
|
||||
}*/
|
||||
|
||||
return {};
|
||||
}
|
||||
|
|
@ -643,8 +653,8 @@ namespace polysat {
|
|||
|
||||
// forward propagation: p assigned ==> r = pseudo_inverse(eval(p))
|
||||
// TODO: (later) this should be propagated instead of adding a clause
|
||||
if (pv.is_val() && !rv.is_val())
|
||||
return s.mk_clause(~invc, ~s.eq(p(), pv), s.eq(r(), pv.val().pseudo_inverse(m.power_of_2())), true);
|
||||
/*if (pv.is_val() && !rv.is_val())
|
||||
return s.mk_clause(~invc, ~s.eq(p(), pv), s.eq(r(), pv.val().pseudo_inverse(m.power_of_2())), true);*/
|
||||
|
||||
if (!pv.is_val() || !rv.is_val())
|
||||
return {};
|
||||
|
|
@ -699,6 +709,131 @@ namespace polysat {
|
|||
|
||||
return to_lbool(p.val().pseudo_inverse(p.power_of_2()) == r.val());
|
||||
}
|
||||
|
||||
void op_constraint::activate_udiv(solver& s) {
|
||||
// signed_constraint const udivc(this, true); Do we really need this premiss? We anyway assert these constraints as unit clauses
|
||||
|
||||
pdd const& quot = r();
|
||||
pdd const& rem = m_linked->r();
|
||||
|
||||
// Axioms for quotient/remainder:
|
||||
// a = b*q + r
|
||||
// multiplication does not overflow in b*q
|
||||
// addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r
|
||||
// b ≠ 0 ==> r < b
|
||||
// b = 0 ==> q = -1
|
||||
// TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it.
|
||||
// Maybe we need something like an op_constraint for better propagation.
|
||||
s.add_clause(s.eq(q() * quot + rem - p()), false);
|
||||
s.add_clause(~s.umul_ovfl(q(), quot), false);
|
||||
// r <= b*q+r
|
||||
// { apply equivalence: p <= q <=> q-p <= -p-1 }
|
||||
// b*q <= -r-1
|
||||
s.add_clause(s.ule(q() * quot, -rem - 1), false);
|
||||
|
||||
auto c_eq = s.eq(q());
|
||||
s.add_clause(c_eq, s.ult(rem, q()), false);
|
||||
s.add_clause(~c_eq, s.eq(quot + 1), false);
|
||||
}
|
||||
|
||||
/**
|
||||
* Produce lemmas for constraint: r == p / q
|
||||
* q = 0 ==> r = max_value
|
||||
* p = 0 ==> r = 0 || r = max_value
|
||||
* q = 1 ==> r = p
|
||||
*/
|
||||
clause_ref op_constraint::lemma_udiv(solver& s, assignment const& a) {
|
||||
auto& m = p().manager();
|
||||
auto pv = a.apply_to(p());
|
||||
auto qv = a.apply_to(q());
|
||||
auto rv = a.apply_to(r());
|
||||
|
||||
if (eval_udiv(pv, qv, rv) == l_true)
|
||||
return {};
|
||||
|
||||
signed_constraint const udivc(this, true);
|
||||
|
||||
if (qv.is_zero() && !rv.is_val())
|
||||
return s.mk_clause(~udivc, ~s.eq(q()), s.eq(r(), r().manager().max_value()), true);
|
||||
if (pv.is_zero() && !rv.is_val())
|
||||
return s.mk_clause(~udivc, ~s.eq(p()), s.eq(r()), s.eq(r(), r().manager().max_value()), true);
|
||||
if (qv.is_one())
|
||||
return s.mk_clause(~udivc, ~s.eq(q(), 1), s.eq(r(), p()), true);
|
||||
|
||||
if (pv.is_val() && qv.is_val() && !rv.is_val()) {
|
||||
SASSERT(!qv.is_zero());
|
||||
// TODO: We could actually propagate an interval. Instead of p = 9 & q = 4 => r = 2 we could do p >= 8 && p < 12 && q = 4 => r = 2
|
||||
return s.mk_clause(~udivc, ~s.eq(p(), pv.val()), ~s.eq(q(), qv.val()), s.eq(r(), div(pv.val(), qv.val())), true);
|
||||
}
|
||||
|
||||
return {};
|
||||
}
|
||||
|
||||
/** Evaluate constraint: r == p / q */
|
||||
lbool op_constraint::eval_udiv(pdd const& p, pdd const& q, pdd const& r) {
|
||||
|
||||
if (q.is_zero() && r.is_val()) {
|
||||
return r.val() == r.manager().max_value() ? l_true : l_false;
|
||||
}
|
||||
if (q.is_one()) {
|
||||
if (r == p)
|
||||
return l_true;
|
||||
}
|
||||
|
||||
if (!p.is_val() || !q.is_val() || !r.is_val())
|
||||
return l_undef;
|
||||
|
||||
return r.val() == div(p.val(), q.val()) ? l_true : l_false;
|
||||
}
|
||||
|
||||
/**
|
||||
* Produce lemmas for constraint: r == p % q
|
||||
* p = 0 ==> r = 0
|
||||
* q = 1 ==> r = 0
|
||||
* q = 0 ==> r = p
|
||||
*/
|
||||
clause_ref op_constraint::lemma_urem(solver& s, assignment const& a) {
|
||||
auto& m = p().manager();
|
||||
auto pv = a.apply_to(p());
|
||||
auto qv = a.apply_to(q());
|
||||
auto rv = a.apply_to(r());
|
||||
|
||||
if (eval_urem(pv, qv, rv) == l_true)
|
||||
return {};
|
||||
|
||||
signed_constraint const urem(this, true);
|
||||
|
||||
if (pv.is_zero() && !rv.is_val())
|
||||
return s.mk_clause(~urem, ~s.eq(p()), s.eq(r()), true);
|
||||
if (qv.is_one() && !rv.is_val())
|
||||
return s.mk_clause(~urem, ~s.eq(q(), 1), s.eq(r()), true);
|
||||
if (qv.is_zero())
|
||||
return s.mk_clause(~urem, ~s.eq(q()), s.eq(r(), p()), true);
|
||||
|
||||
if (pv.is_val() && qv.is_val() && !rv.is_val()) {
|
||||
SASSERT(!qv.is_zero());
|
||||
return s.mk_clause(~urem, ~s.eq(p(), pv.val()), ~s.eq(q(), qv.val()), s.eq(r(), mod(pv.val(), qv.val())), true);
|
||||
}
|
||||
|
||||
return {};
|
||||
}
|
||||
|
||||
/** Evaluate constraint: r == p % q */
|
||||
lbool op_constraint::eval_urem(pdd const& p, pdd const& q, pdd const& r) {
|
||||
|
||||
if (q.is_one() && r.is_val()) {
|
||||
return r.val().is_zero() ? l_true : l_false;
|
||||
}
|
||||
if (q.is_zero()) {
|
||||
if (r == p)
|
||||
return l_true;
|
||||
}
|
||||
|
||||
if (!p.is_val() || !q.is_val() || !r.is_val())
|
||||
return l_undef;
|
||||
|
||||
return r.val() == mod(p.val(), q.val()) ? l_true : l_false; // mod == rem as we know hat q > 0
|
||||
}
|
||||
|
||||
void op_constraint::add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
|
||||
pdd pv = s.subst(p());
|
||||
|
|
@ -723,6 +858,12 @@ namespace polysat {
|
|||
case code::inv_op:
|
||||
us.add_inv(pv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep);
|
||||
break;
|
||||
case code::udiv_op:
|
||||
us.add_udiv(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep);
|
||||
break;
|
||||
case code::urem_op:
|
||||
us.add_urem(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep);
|
||||
break;
|
||||
default:
|
||||
NOT_IMPLEMENTED_YET();
|
||||
break;
|
||||
|
|
|
|||
|
|
@ -38,7 +38,11 @@ namespace polysat {
|
|||
/// r is the smallest multiplicative pseudo-inverse of p;
|
||||
/// by definition we set r == 0 when p == 0.
|
||||
/// Note that in general, there are 2^parity(p) many pseudo-inverses of p.
|
||||
inv_op
|
||||
inv_op,
|
||||
// r is the quotient of dividing p by q
|
||||
udiv_op,
|
||||
// r is the remainder of dividing p by q
|
||||
urem_op,
|
||||
};
|
||||
protected:
|
||||
friend class constraint_manager;
|
||||
|
|
@ -47,6 +51,8 @@ namespace polysat {
|
|||
pdd m_p; // operand1
|
||||
pdd m_q; // operand2
|
||||
pdd m_r; // result
|
||||
|
||||
op_constraint* m_linked; // for linking remainder/quotient
|
||||
|
||||
op_constraint(code c, pdd const& p, pdd const& q, pdd const& r);
|
||||
lbool eval(pdd const& p, pdd const& q, pdd const& r) const;
|
||||
|
|
@ -66,12 +72,19 @@ namespace polysat {
|
|||
|
||||
clause_ref lemma_inv(solver& s, assignment const& a);
|
||||
static lbool eval_inv(pdd const& p, pdd const& r);
|
||||
|
||||
clause_ref lemma_udiv(solver& s, assignment const& a);
|
||||
static lbool eval_udiv(pdd const& p, pdd const& q, pdd const& r);
|
||||
|
||||
clause_ref lemma_urem(solver& s, assignment const& a);
|
||||
static lbool eval_urem(pdd const& p, pdd const& q, pdd const& r);
|
||||
|
||||
std::ostream& display(std::ostream& out, char const* eq) const;
|
||||
|
||||
void activate(solver& s);
|
||||
|
||||
void activate_and(solver& s);
|
||||
void activate_udiv(solver& s);
|
||||
|
||||
public:
|
||||
~op_constraint() override {}
|
||||
|
|
|
|||
|
|
@ -33,7 +33,7 @@ namespace polysat {
|
|||
saturation::saturation(solver& s) : s(s), m_lemma(s), m_parity_tracker(s) {}
|
||||
|
||||
void saturation::log_lemma(pvar v, conflict& core) {
|
||||
IF_VERBOSE(1, {
|
||||
IF_VERBOSE(2, {
|
||||
auto const& cl = core.lemmas().back();
|
||||
verbose_stream() << m_rule << " v" << v << " ";
|
||||
for (auto lit : *cl)
|
||||
|
|
@ -1987,6 +1987,17 @@ namespace polysat {
|
|||
<< s.var(q1) << "\n");
|
||||
};
|
||||
|
||||
// monotonicity0 lemma should be asserted eagerly.
|
||||
auto monotonicity0 = [&](auto& x1, auto& x1_val, auto& y1, auto& y1_val, auto& q1, auto& q1_val) {
|
||||
if (q1_val * y1_val <= x1_val)
|
||||
return;
|
||||
// q1*y1 + r1 = x1, q1*y1 <= -r1 - 1, q1*y1 <= x1
|
||||
propagated = true;
|
||||
set_rule("[x1, y1] (x1 / y1) * y1 <= x1");
|
||||
m_lemma.reset();
|
||||
propagate(q1, core, s.ule(s.var(q1) * y1, x1));
|
||||
};
|
||||
|
||||
auto monotonicity1 = [&](auto& x1, auto& x1_val, auto& y1, auto& y1_val, auto& q1, auto& q1_val,
|
||||
auto& x2, auto& x2_val, auto& y2, auto& y2_val, auto& q2, auto& q2_val) {
|
||||
if (!(x1_val <= x2_val && y1_val >= y2_val && q1_val > q2_val))
|
||||
|
|
@ -2023,6 +2034,10 @@ namespace polysat {
|
|||
|
||||
if (q1_val == expected1)
|
||||
continue;
|
||||
|
||||
// force that q1 * y1 <= x1 if it isn't the case.
|
||||
// monotonicity0(x1, x1_val, y1, y1_val, q1, q1_val);
|
||||
|
||||
|
||||
for (auto const& [x2, y2, q2, r2] : s.m_constraints.div_constraints()) {
|
||||
if (x1 == x2 && y1 == y2)
|
||||
|
|
|
|||
|
|
@ -86,6 +86,10 @@ namespace polysat {
|
|||
#endif
|
||||
if (try_equal_body_subsumptions(cl))
|
||||
simplified = true;
|
||||
#if 0
|
||||
if (try_bit_subsumptions(cl))
|
||||
simplified = true;
|
||||
#endif
|
||||
return simplified;
|
||||
}
|
||||
|
||||
|
|
@ -344,8 +348,257 @@ namespace polysat {
|
|||
return true;
|
||||
}
|
||||
|
||||
// decomposes into a plain constant and a part containing variables. e.g., 2*x*y + 3*z - 2 gets { 2*x*y + 3*z, -2 }
|
||||
static std::pair<pdd, pdd> decouple_constant(const pdd& p) {
|
||||
for (const auto& m : p) {
|
||||
if (m.vars.empty())
|
||||
return { p - m.coeff, p.manager().mk_val(m.coeff) };
|
||||
}
|
||||
return { p, p.manager().mk_val(0) };
|
||||
}
|
||||
|
||||
// 2^(k - d) * x = m * 2^(k - d)
|
||||
bool simplify_clause::get_trailing_mask(pdd lhs, pdd rhs, pdd& p, trailing_bits& mask, bool pos) {
|
||||
auto lhs_decomp = decouple_constant(lhs);
|
||||
auto rhs_decomp = decouple_constant(rhs);
|
||||
|
||||
lhs = lhs_decomp.first - rhs_decomp.first;
|
||||
rhs = rhs_decomp.second - lhs_decomp.second;
|
||||
|
||||
SASSERT(rhs.is_val());
|
||||
|
||||
unsigned k = lhs.manager().power_of_2();
|
||||
unsigned d = lhs.max_pow2_divisor();
|
||||
unsigned span = k - d;
|
||||
if (span == 0 || lhs.is_val())
|
||||
return false;
|
||||
|
||||
p = lhs.div(rational::power_of_two(d));
|
||||
rational rhs_val = rhs.val();
|
||||
mask.bits = rhs_val / rational::power_of_two(d);
|
||||
if (!mask.bits.is_int())
|
||||
return false;
|
||||
|
||||
auto it = p.begin();
|
||||
auto first = *it;
|
||||
it++;
|
||||
if (it == p.end()) {
|
||||
// if the lhs contains only one monomial it is of the form: odd * x = mask. We can multiply by the inverse to get the mask for x
|
||||
SASSERT(first.coeff.is_odd());
|
||||
rational inv;
|
||||
VERIFY(first.coeff.mult_inverse(lhs.power_of_2(), inv));
|
||||
p *= inv;
|
||||
mask.bits = mod2k(mask.bits * inv, span);
|
||||
}
|
||||
|
||||
mask.length = span;
|
||||
mask.positive = pos;
|
||||
return true;
|
||||
}
|
||||
|
||||
// 2^(k - 1) <= 2^(k - i - 1) * x (original definition) // TODO: Have this as well
|
||||
// 2^(k - i - 1) * x + 2^(k - 1) <= 2^(k - 1) - 1 (currently we test only for this form)
|
||||
bool simplify_clause::get_bit(const pdd& lhs, const pdd& rhs, pdd& p, single_bit& bit, bool pos) {
|
||||
if (!rhs.is_val())
|
||||
return false;
|
||||
|
||||
rational rhs_val = rhs.val() + 1;
|
||||
unsigned k = rhs.power_of_2();
|
||||
|
||||
if (rhs_val != rational::power_of_two(k - 1))
|
||||
return false;
|
||||
|
||||
pdd rest = lhs - rhs_val;
|
||||
unsigned d = rest.max_pow2_divisor();
|
||||
bit.position = k - d - 1;
|
||||
bit.positive = pos;
|
||||
p = rest.div(rational::power_of_two(d));
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
// Compares with respect to "subsumption"
|
||||
// -1: mask1 < mask2 (e.g., 101 < 0101)
|
||||
// 0: incomparable
|
||||
// 1: mask1 > mask2
|
||||
// failure mask1 == mask2
|
||||
static int compare(const trailing_bits& mask1, const trailing_bits& mask2) {
|
||||
if (mask1.length == mask2.length) {
|
||||
SASSERT(mask1.bits != mask2.bits); // otw. we would have already eliminated the duplicate constraint
|
||||
return 0;
|
||||
}
|
||||
if (mask1.length < mask2.length) {
|
||||
for (unsigned i = 0; i < mask1.length; i++)
|
||||
if (mask1.bits.get_bit(i) != mask2.bits.get_bit(i))
|
||||
return 0;
|
||||
return -1;
|
||||
}
|
||||
SASSERT(mask1.length > mask2.length);
|
||||
for (unsigned i = 0; i < mask2.length; i++)
|
||||
if (mask1.bits.get_bit(i) != mask2.bits.get_bit(i))
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**
|
||||
* Test simple subsumption between bit and parity constraints.
|
||||
*
|
||||
* let lsb(t, d) = m := 2^(k - d)*t = m * 2^(k - d) denotes that the last (least significant) d bits of t are the binary representation of m
|
||||
* let bit(t, i) := 2^(k - 1) <= 2^(k - i - 1)*t
|
||||
* TODO: 2^(k - 1 - d) <= 2^(k - i - 1)*t denotes that bits i-d...i are set to 0
|
||||
*
|
||||
* lsb(t, d) = m with log2(m) >= d => false
|
||||
*
|
||||
* parity(t) >= d denotes lsb(t, d) = 0
|
||||
* parity(t) <= d denotes lsb(t, d + 1) != 0
|
||||
*
|
||||
* parity(t) >= d1 || parity(t) >= d2 with d1 < d2 implies parity(t) >= d1
|
||||
* parity(t) <= d1 || parity(t) <= d2 with d1 < d2 implies parity(t) <= d2
|
||||
*
|
||||
* parity(t) >= d1 || !bit(t, d2) with d2 < d1 implies bit(t, d2)
|
||||
* parity(t) <= d1 || bit(t, d2) with d2 < d1 implies parity(t) <= d1
|
||||
*
|
||||
* parity(t) >= d1 || parity(t) <= d2 with d1 <= d2 implies true
|
||||
*
|
||||
* More generally: parity can be replaced by lsb in case we check for subsumption between the bit-masks rather than comparing the parities (special case)
|
||||
*/
|
||||
bool simplify_clause::try_bit_subsumptions(clause& cl) {
|
||||
|
||||
struct pdd_info {
|
||||
unsigned sz;
|
||||
vector<trailing_bits> leading;
|
||||
vector<single_bit> fixed_bits;
|
||||
};
|
||||
|
||||
struct optional_pdd_hash {
|
||||
unsigned operator()(optional<pdd> const& args) const {
|
||||
return args->hash();
|
||||
}
|
||||
};
|
||||
|
||||
ptr_vector<pdd_info> info_list;
|
||||
map<optional<pdd>, pdd_info*, optional_pdd_hash, default_eq<optional<pdd>>> info_table;
|
||||
bool is_valid = false;
|
||||
|
||||
auto get_info = [&info_table, &info_list](const pdd& p) -> pdd_info& {
|
||||
auto it = info_table.find_iterator(optional(p));
|
||||
if (it != info_table.end())
|
||||
return *it->m_value;
|
||||
auto* info = alloc(pdd_info);
|
||||
info->sz = p.manager().power_of_2();
|
||||
info_list.push_back(info);
|
||||
info_table.insert(optional(p), info);
|
||||
return *info;
|
||||
};
|
||||
|
||||
bool changed = false;
|
||||
bool_vector removed(cl.size(), false);
|
||||
|
||||
for (unsigned i = 0; i < cl.size(); i++) {
|
||||
signed_constraint c = s.lit2cnstr(cl[i]);
|
||||
if (!c->is_ule())
|
||||
continue;
|
||||
trailing_bits mask;
|
||||
single_bit bit;
|
||||
pdd p = c->to_ule().lhs();
|
||||
if ((c.is_eq() || c.is_diseq()) && get_trailing_mask(c->to_ule().lhs(), c->to_ule().rhs(), p, mask, c.is_positive())) {
|
||||
if (mask.bits.bitsize() > mask.length) {
|
||||
removed[i] = true; // skip this constraint. e.g., 2^(k-3)*x = 9*2^(k-3) is false as 9 >= 2^3
|
||||
continue;
|
||||
}
|
||||
|
||||
mask.src_idx = i;
|
||||
get_info(p).leading.push_back(mask);
|
||||
}
|
||||
else if (c->is_ule() && get_bit(c->to_ule().lhs(), c->to_ule().rhs(), p, bit, c.is_positive())) {
|
||||
bit.src_idx = i;
|
||||
get_info(p).fixed_bits.push_back(bit);
|
||||
}
|
||||
}
|
||||
|
||||
for (const auto& entry : info_list) {
|
||||
for (unsigned i = 0; i < entry->leading.size(); i++) {
|
||||
auto& p1 = entry->leading[i];
|
||||
// trailing vs. positive
|
||||
for (unsigned j = i + 1; !removed[p1.src_idx] && j < entry->leading.size(); j++) {
|
||||
auto& p2 = entry->leading[j];
|
||||
if (!removed[p2.src_idx])
|
||||
continue;
|
||||
|
||||
if (p1.positive == p2.positive) {
|
||||
int cmp = compare(p1, p2);
|
||||
if (cmp != 0) {
|
||||
if ((cmp == -1) == p1.positive) {
|
||||
LOG("Removed: " << s.lit2cnstr(cl[p2.src_idx]) << " because of " << s.lit2cnstr(cl[p1.src_idx]) << "\n");
|
||||
removed[p2.src_idx] = true;
|
||||
changed = true;
|
||||
}
|
||||
else if ((cmp == 1) == p1.positive) {
|
||||
LOG("Removed: " << s.lit2cnstr(cl[p1.src_idx]) << " because of " << s.lit2cnstr(cl[p2.src_idx]) << "\n");
|
||||
removed[p1.src_idx] = true;
|
||||
changed = true;
|
||||
}
|
||||
}
|
||||
}
|
||||
else {
|
||||
auto& pos = p1.positive ? p1 : p2;
|
||||
auto& neg = p1.positive ? p2 : p1;
|
||||
|
||||
int cmp = compare(pos, neg);
|
||||
if (cmp == -1) {
|
||||
is_valid = true;
|
||||
changed = true;
|
||||
LOG("Tautology: " << s.lit2cnstr(cl[pos.src_idx]) << " and " << s.lit2cnstr(cl[neg.src_idx]) << "\n");
|
||||
goto done;
|
||||
}
|
||||
}
|
||||
}
|
||||
// trailing vs. bit
|
||||
for (unsigned j = 0; !removed[p1.src_idx] && j < entry->fixed_bits.size(); j++) {
|
||||
auto& p2 = entry->fixed_bits[j];
|
||||
if (removed[p2.src_idx])
|
||||
continue;
|
||||
|
||||
if (p2.position >= p1.length)
|
||||
continue;
|
||||
|
||||
if (p1.positive) {
|
||||
if (p1.bits.get_bit(p2.position) == p2.positive) {
|
||||
LOG("Removed: " << s.lit2cnstr(cl[p1.src_idx]) << " because of " << s.lit2cnstr(cl[p2.src_idx]) << " (bit)\n");
|
||||
removed[p1.src_idx] = true;
|
||||
changed = true;
|
||||
}
|
||||
}
|
||||
else {
|
||||
if (p1.bits.get_bit(p2.position) != p2.positive) {
|
||||
LOG("Removed: " << s.lit2cnstr(cl[p2.src_idx]) << " (bit) because of " << s.lit2cnstr(cl[p1.src_idx]) << "\n");
|
||||
removed[p2.src_idx] = true;
|
||||
changed = true;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
done:
|
||||
for (auto entry : info_list)
|
||||
dealloc(entry);
|
||||
if (is_valid) {
|
||||
SASSERT(!cl.empty());
|
||||
cl.literals().clear();
|
||||
cl.literals().push_back(s.eq(s.value(rational::zero(), 1)).blit()); // an obvious tautology
|
||||
return true;
|
||||
}
|
||||
// Remove subsuming literals
|
||||
if (!changed)
|
||||
return false;
|
||||
verbose_stream() << "Bit simplified\n";
|
||||
unsigned cli = 0;
|
||||
for (unsigned i = 0; i < cl.size(); ++i)
|
||||
if (!removed[i])
|
||||
cl[cli++] = cl[i];
|
||||
cl.m_literals.shrink(cli);
|
||||
return true;
|
||||
}
|
||||
|
||||
#if 0
|
||||
// All variables of clause 'cl' except 'z' are assigned.
|
||||
|
|
|
|||
|
|
@ -17,6 +17,18 @@ Author:
|
|||
namespace polysat {
|
||||
|
||||
class solver;
|
||||
|
||||
struct trailing_bits {
|
||||
unsigned length;
|
||||
rational bits;
|
||||
bool positive;
|
||||
unsigned src_idx;
|
||||
};
|
||||
struct single_bit {
|
||||
bool positive;
|
||||
unsigned position;
|
||||
unsigned src_idx;
|
||||
};
|
||||
|
||||
class simplify_clause {
|
||||
|
||||
|
|
@ -33,6 +45,7 @@ namespace polysat {
|
|||
bool try_remove_equations(clause& cl);
|
||||
bool try_recognize_bailout(clause& cl);
|
||||
bool try_equal_body_subsumptions(clause& cl);
|
||||
bool try_bit_subsumptions(clause& cl);
|
||||
|
||||
void prepare_subs_entry(subs_entry& entry, signed_constraint c);
|
||||
|
||||
|
|
@ -46,6 +59,9 @@ namespace polysat {
|
|||
simplify_clause(solver& s);
|
||||
|
||||
bool apply(clause& cl);
|
||||
|
||||
static bool get_trailing_mask(pdd lhs, pdd rhs, pdd& p, trailing_bits& mask, bool pos);
|
||||
static bool get_bit(const pdd& lhs, const pdd& rhs, pdd& p, single_bit& bit, bool pos);
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -539,7 +539,9 @@ namespace polysat {
|
|||
#if ENABLE_LINEAR_SOLVER
|
||||
m_linear_solver.push();
|
||||
#endif
|
||||
#if 0
|
||||
m_fixed_bits.push();
|
||||
#endif
|
||||
}
|
||||
|
||||
void solver::pop_levels(unsigned num_levels) {
|
||||
|
|
@ -554,8 +556,9 @@ namespace polysat {
|
|||
#if ENABLE_LINEAR_SOLVER
|
||||
m_linear_solver.pop(num_levels);
|
||||
#endif
|
||||
#if 0
|
||||
m_fixed_bits.pop();
|
||||
|
||||
#endif
|
||||
while (num_levels > 0) {
|
||||
switch (m_trail.back()) {
|
||||
case trail_instr_t::qhead_i: {
|
||||
|
|
@ -1160,7 +1163,9 @@ namespace polysat {
|
|||
void solver::assign_eval(sat::literal lit) {
|
||||
signed_constraint const c = lit2cnstr(lit);
|
||||
LOG_V(10, "Evaluate: " << lit_pp(*this, lit));
|
||||
if (!c.is_currently_true(*this)) IF_VERBOSE(0, verbose_stream() << c << " is not currently true\n");
|
||||
if (!c.is_currently_true(*this)) {
|
||||
IF_VERBOSE(0, verbose_stream() << "\n" << c << " is not currently true\n");
|
||||
}
|
||||
SASSERT(c.is_currently_true(*this));
|
||||
VERIFY_EQ(c.eval(*this), l_true);
|
||||
unsigned level = 0;
|
||||
|
|
|
|||
|
|
@ -255,6 +255,14 @@ namespace polysat {
|
|||
add(bv->mk_ule(v_inv, v_inv_max), false, dep);
|
||||
}
|
||||
|
||||
void add_udiv(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override {
|
||||
add(m.mk_eq(bv->mk_bv_udiv(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep);
|
||||
}
|
||||
|
||||
void add_urem(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override {
|
||||
add(m.mk_eq(bv->mk_bv_urem(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep);
|
||||
}
|
||||
|
||||
void add_ule_const(rational const& val, bool sign, dep_t dep) override {
|
||||
if (val == 0)
|
||||
add(m.mk_eq(x, mk_poly(val)), sign, dep);
|
||||
|
|
|
|||
|
|
@ -105,6 +105,8 @@ namespace polysat {
|
|||
virtual void add_xor(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0;
|
||||
virtual void add_not(univariate const& in, univariate const& out, bool sign, dep_t dep) = 0;
|
||||
virtual void add_inv(univariate const& in, univariate const& out, bool sign, dep_t dep) = 0;
|
||||
virtual void add_udiv(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0;
|
||||
virtual void add_urem(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0;
|
||||
|
||||
/// Add x <= val or x > val, depending on sign
|
||||
virtual void add_ule_const(rational const& val, bool sign, dep_t dep) = 0;
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ Module Name:
|
|||
|
||||
Author:
|
||||
|
||||
Clemens Eisenhofer 2023-01-03
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-06
|
||||
|
||||
|
|
@ -33,9 +34,10 @@ namespace polysat {
|
|||
const unsigned char pattern_33 = 0x33; // 00110011
|
||||
const unsigned char pattern_0f = 0x0f; // 00001111
|
||||
const unsigned char pattern_01 = 0x01; // 00000001
|
||||
|
||||
unsigned to_alloc = (p.power_of_2() + sizeof(unsigned) - 1) / sizeof(unsigned);
|
||||
unsigned to_alloc_bits = to_alloc * sizeof(unsigned);
|
||||
|
||||
unsigned to_alloc_bits = p.power_of_2();
|
||||
unsigned to_alloc = to_alloc_bits / sizeof(unsigned);
|
||||
SASSERT(to_alloc_bits == sizeof(unsigned)*to_alloc && "8 already divides power of power_of_2");
|
||||
|
||||
// Cache this?
|
||||
auto* scaled_55 = (unsigned*)alloca(to_alloc_bits);
|
||||
|
|
@ -62,16 +64,33 @@ namespace polysat {
|
|||
//final_shift = (final_shift + 7) / 8 * 8 - 1; // ceil final_shift to the next multiple of 8
|
||||
return s.lshr(w * m.mk_val(rational_scaled_01), m.mk_val(p.power_of_2() - 8));
|
||||
}
|
||||
|
||||
|
||||
// [nsb cr]: m_reste_constants assume the clause added for power * rest == p is
|
||||
// alive even after backtracking. This assumes that irredundant clauses are retained, probably
|
||||
// still true for PolySAT, but fragile.
|
||||
// same comment goes for get_inverse.
|
||||
//
|
||||
// the caches should be invalidated if irredundant clauses get purged.
|
||||
// old z3 uses a deletion event handler with clauses to track state; it is
|
||||
// a bit fragile to program with.
|
||||
//
|
||||
|
||||
/**
|
||||
* Encode:
|
||||
*
|
||||
* p = rest << log(p)
|
||||
*
|
||||
*/
|
||||
pdd free_variable_elimination::get_odd(pdd p) {
|
||||
SASSERT(p.is_val() || p.is_var()); // For now
|
||||
auto& m = p.manager();
|
||||
|
||||
if (p.is_val()) {
|
||||
const rational& v = p.val();
|
||||
unsigned d = v.trailing_zeros();
|
||||
if (!d)
|
||||
return p.manager().mk_val(v);
|
||||
return p.manager().mk_val(div(v, rational::power_of_two(d))); // TODO: Is there no shift?
|
||||
if (d == 0)
|
||||
return p;
|
||||
return m.mk_val(div(v, rational::power_of_two(d))); // TODO: Is there no shift?
|
||||
}
|
||||
pvar v = p.var();
|
||||
if (m_rest_constants.size() > v && m_rest_constants[v] != -1)
|
||||
|
|
@ -80,7 +99,7 @@ namespace polysat {
|
|||
pdd power = get_dyadic_valuation(p).second;
|
||||
|
||||
pvar rest = s.add_var(p.power_of_2());
|
||||
pdd rest_pdd = p.manager().mk_var(rest);
|
||||
pdd rest_pdd = m.mk_var(rest);
|
||||
m_rest_constants.setx(v, rest, -1);
|
||||
s.add_clause(s.eq(power * rest_pdd, p), false);
|
||||
return rest_pdd;
|
||||
|
|
@ -88,9 +107,10 @@ namespace polysat {
|
|||
|
||||
optional<pdd> free_variable_elimination::get_inverse(pdd p) {
|
||||
SASSERT(p.is_val() || p.is_var()); // For now
|
||||
auto& m = p.manager();
|
||||
|
||||
if (p.is_val()) {
|
||||
pdd i = p.manager().zero();
|
||||
pdd i = m.zero();
|
||||
if (!inv(p, i))
|
||||
return {};
|
||||
return optional<pdd>(i);
|
||||
|
|
@ -100,9 +120,9 @@ namespace polysat {
|
|||
return optional<pdd>(s.var(m_inverse_constants[v]));
|
||||
|
||||
pvar inv = s.add_var(p.power_of_2());
|
||||
pdd inv_pdd = p.manager().mk_var(inv);
|
||||
pdd inv_pdd = m.mk_var(inv);
|
||||
m_inverse_constants.setx(v, inv, -1);
|
||||
s.add_clause(s.eq(inv_pdd * p, p.manager().one()), false);
|
||||
s.add_clause(s.eq(inv_pdd * p, m.one()), false);
|
||||
return optional<pdd>(inv_pdd);
|
||||
}
|
||||
|
||||
|
|
@ -118,10 +138,11 @@ namespace polysat {
|
|||
pvar pv2;
|
||||
bool new_var = false;
|
||||
if (m_pv_constants.size() <= v || m_pv_constants[v] == -1) {
|
||||
pv = s.add_var(m.power_of_2()); // TODO: What's a good value? Unfortunately we cannot use a integer
|
||||
pv = s.add_var(m.power_of_2()); // TODO: What's a good value? Unfortunately we cannot use an integer
|
||||
pv2 = s.add_var(m.power_of_2());
|
||||
m_pv_constants.setx(v, pv, -1);
|
||||
m_pv_power_constants.setx(v, pv2, -1);
|
||||
// [nsb cr]: why these calls to m.mk_var()?
|
||||
m.mk_var(pv);
|
||||
m.mk_var(pv2);
|
||||
new_var = true;
|
||||
|
|
@ -137,14 +158,20 @@ namespace polysat {
|
|||
// For testing some different implementations
|
||||
#if PV_MOD == 1
|
||||
// brute-force bit extraction and <=
|
||||
//
|
||||
// 2^N-k-1 * p = 0 <=> k <= pv
|
||||
// pv2 = 1 << pv
|
||||
//
|
||||
|
||||
// [nsb cr] why are these clauses always added, when some are only added by new_var?
|
||||
signed_constraint c1 = s.eq(rational::power_of_two(p.power_of_2() - k - 1) * p, m.zero());
|
||||
signed_constraint c2 = s.ule(m.mk_val(k), s.var(pv));
|
||||
s.add_clause(~c1, c2, false);
|
||||
s.add_clause(c1, ~c2, false);
|
||||
|
||||
if (new_var) {
|
||||
if (new_var)
|
||||
s.add_clause(s.eq(s.var(pv2), s.shl(m.one(), s.var(pv))), false);
|
||||
}
|
||||
|
||||
#elif PV_MOD == 2
|
||||
// symbolic "maximal divisible"
|
||||
signed_constraint c1 = s.eq(s.shl(s.lshr(p, s.var(pv)), s.var(pv)), p);
|
||||
|
|
@ -153,6 +180,8 @@ namespace polysat {
|
|||
signed_constraint z = ~s.eq(p, p.manager().zero());
|
||||
|
||||
// v != 0 ==> [(v >> pv) << pv == v && (v >> pv + 1) << pv + 1 != v]
|
||||
|
||||
// [nsb cr] why are these clauses always added, when some are only added by new_var?
|
||||
s.add_clause(~z, c1, false);
|
||||
s.add_clause(~z, c2, false);
|
||||
|
||||
|
|
@ -162,6 +191,8 @@ namespace polysat {
|
|||
#elif PV_MOD == 3
|
||||
// computing the complete function by hamming-distance
|
||||
// proven equivalent with case 2 via bit-blasting for small sizes
|
||||
|
||||
// [nsb cr] why are these clauses always added, when some are only added by new_var?
|
||||
s.add_clause(s.eq(s.var(pv), get_hamming_distance(s.bxor(p, p - 1)) - 1), false);
|
||||
|
||||
// in case v == 0 ==> pv == k - 1 (we don't care)
|
||||
|
|
@ -180,6 +211,8 @@ namespace polysat {
|
|||
signed_constraint c1 = s.eq(s.var(pv), k);
|
||||
signed_constraint c2 = s.eq(s.var(pv2), rational::power_of_two(k));
|
||||
signed_constraint c3 = s.eq(masked, rational::power_of_two(k));
|
||||
|
||||
// [nsb cr] why are these clauses always added, when some are only added by new_var?
|
||||
|
||||
s.add_clause(c1, ~c3, false);
|
||||
s.add_clause(c2, ~c3, false);
|
||||
|
|
@ -292,8 +325,8 @@ namespace polysat {
|
|||
signed_constraint p1 = s.ule(m.zero(), m.zero());
|
||||
signed_constraint p2 = s.ule(m.zero(), m.zero());
|
||||
|
||||
pdd new_lhs = p.manager().zero();
|
||||
pdd new_rhs = p.manager().zero();
|
||||
pdd new_lhs = m.zero();
|
||||
pdd new_rhs = m.zero();
|
||||
|
||||
pdd fac_lhs = m.zero();
|
||||
pdd fac_rhs = m.zero();
|
||||
|
|
@ -309,10 +342,10 @@ namespace polysat {
|
|||
LOG("fac_rhs: " << fac_rhs);
|
||||
LOG("rest_rhs: " << rest_rhs);
|
||||
|
||||
pdd pv_equality = p.manager().zero();
|
||||
pdd lhs_multiple = p.manager().zero();
|
||||
pdd rhs_multiple = p.manager().zero();
|
||||
pdd coeff_odd = p.manager().zero();
|
||||
pdd pv_equality = m.zero();
|
||||
pdd lhs_multiple = m.zero();
|
||||
pdd rhs_multiple = m.zero();
|
||||
pdd coeff_odd = m.zero();
|
||||
optional<pdd> fac_odd_inv;
|
||||
|
||||
get_multiple_result multiple1 = get_multiple(fac_lhs, fac, new_lhs);
|
||||
|
|
@ -642,7 +675,33 @@ namespace polysat {
|
|||
}
|
||||
|
||||
// a * x + b = 0 (x not in a or b; i.e., the equation is linear in x)
|
||||
// C[x, ...] resp., C[..., x]
|
||||
// replace x in p(x)
|
||||
//
|
||||
// 0. x does not occur in p
|
||||
// 1. a is an odd numeral.
|
||||
// x = a^-1 * -b, substitute in p(x)
|
||||
// 2. p has degree > 1.
|
||||
// bail
|
||||
// 3. p := a1*x + b1
|
||||
// 3.1 a1 = a*a2 - a divides a1
|
||||
// p := a2*a*x + b1 = a2*-b + b1
|
||||
// 3.2 a is known to not divide a1
|
||||
// bail
|
||||
// 3.3 min_parity(a) == max_parity(a), min_parity(a1) >= max_parity(a)
|
||||
// Result is modulo pre-conditions for min/max parity
|
||||
// 3.3.1 b = 0
|
||||
// p := b1
|
||||
// 3.3.2 b != 0
|
||||
// ainv:
|
||||
// with property: a * ainv = 2^min_parity(a)
|
||||
// 3.3.2.1. min_parity(a) > 0
|
||||
// shift := a1 >> min_parity(a)
|
||||
// lemma: shift << min_parity(a) == a1, note that lemma is implied by pre-conditions
|
||||
// p := ainv * -b * shift + b1
|
||||
// 3.3.2.2
|
||||
// p := ainv * -b * a + b1
|
||||
// [nsb cr: isn't it a1 not a in this definition?]
|
||||
//
|
||||
std::tuple<pdd, bool> parity_tracker::eliminate_variable(saturation& saturation, pvar x, const pdd& a, const pdd& b, const pdd& p, clause_builder& precondition) {
|
||||
|
||||
unsigned p_degree = p.degree(x);
|
||||
|
|
@ -684,30 +743,33 @@ namespace polysat {
|
|||
LOG("Warning: Inverting " << a << " although it is not a single variable - might not be a good idea");
|
||||
}
|
||||
|
||||
unsigned a_parity;
|
||||
if ((a_parity = saturation.min_parity(a)) != saturation.max_parity(a) || saturation.min_parity(a1) < a_parity)
|
||||
vector<signed_constraint> explain_a_parity;
|
||||
unsigned a_parity = saturation.min_parity(a, explain_a_parity);
|
||||
unsigned a_max_parity = saturation.max_parity(a, explain_a_parity);
|
||||
if (a_parity != a_max_parity || (a_parity > 0 && saturation.min_parity(a1, explain_a_parity) < a_parity))
|
||||
return { p, false }; // We need the parity of a and this has to be for sure less than the parity of a1
|
||||
|
||||
if (b.is_zero())
|
||||
return { b1, true };
|
||||
|
||||
#if 0
|
||||
pdd a_pi = get_pseudo_inverse(a, a_parity);
|
||||
#else
|
||||
pdd a_pi = s.pseudo_inv(a);
|
||||
//precondition.insert_eval(~s.eq(a_pi * a, rational::power_of_two(a_parity))); // TODO: This is unfortunately not a justification as the inverse might not be set yet (Can we make it to one?)
|
||||
precondition.insert_eval(~s.parity_at_most(a, a_parity));
|
||||
for (auto c : explain_a_parity)
|
||||
precondition.insert_eval(~c);
|
||||
|
||||
if (b.is_zero())
|
||||
return { b1, true };
|
||||
#endif
|
||||
|
||||
pdd shift = a;
|
||||
pdd shift = a1;
|
||||
|
||||
if (a_parity > 0) {
|
||||
shift = s.lshr(a1, a1.manager().mk_val(a_parity));
|
||||
signed_constraint least_parity = s.parity_at_least(a1, a_parity);
|
||||
signed_constraint shift_right_left = s.eq(rational::power_of_two(a_parity) * shift, a1);
|
||||
s.add_clause(~least_parity, shift_right_left, true);
|
||||
//signed_constraint least_parity = s.parity_at_least(a1, a_parity);
|
||||
//signed_constraint shift_right_left = s.eq(rational::power_of_two(a_parity) * shift, a1);
|
||||
//s.add_clause(~least_parity, shift_right_left, true);
|
||||
// s.add_clause(~shift_right_left, least_parity, true); Might be interesting as well [although not needed]; needs to consider special case 0
|
||||
precondition.insert_eval(~shift_right_left);
|
||||
// [nsb cr: this pre-condition is already implied from the parity explanations]
|
||||
// precondition.insert_eval(~shift_right_left);
|
||||
}
|
||||
LOG("Forced elimination: " << a_pi * (-b) * shift + b1);
|
||||
LOG("a: " << a);
|
||||
|
|
@ -716,7 +778,6 @@ namespace polysat {
|
|||
LOG("pseudo inverse: " << a_pi);
|
||||
LOG("-b: " << (-b));
|
||||
LOG("shifted a" << shift);
|
||||
LOG("Forced elimination: " << a_pi * (-b) * shift + b1);
|
||||
return { a_pi * (-b) * shift + b1, true };
|
||||
#endif
|
||||
}
|
||||
|
|
|
|||
|
|
@ -78,9 +78,10 @@ namespace polysat {
|
|||
if (m_alloc.empty())
|
||||
return alloc(entry);
|
||||
auto* e = m_alloc.back();
|
||||
e->src.reset();
|
||||
e->side_cond.reset();
|
||||
e->refined.reset();
|
||||
e->coeff = 1;
|
||||
e->refined = nullptr;
|
||||
m_alloc.pop_back();
|
||||
return e;
|
||||
}
|
||||
|
|
@ -238,6 +239,7 @@ namespace polysat {
|
|||
|
||||
bool viable::intersect(pvar v, entry* ne) {
|
||||
SASSERT(!s.is_assigned(v));
|
||||
SASSERT(!ne->src.empty());
|
||||
entry* e = m_units[v];
|
||||
if (e && e->interval.is_full()) {
|
||||
m_alloc.push_back(ne);
|
||||
|
|
@ -311,8 +313,9 @@ namespace polysat {
|
|||
return true;
|
||||
}
|
||||
|
||||
bool viable::refine_viable(pvar v, rational const& val) {
|
||||
return refine_equal_lin(v, val) && refine_disequal_lin(v, val);
|
||||
template<bool FORWARD>
|
||||
bool viable::refine_viable(pvar v, rational const& val, const svector<lbool>& fixed, const vector<ptr_vector<entry>>& justifications) {
|
||||
return refine_bits<FORWARD>(v, val, fixed, justifications) && refine_equal_lin(v, val) && refine_disequal_lin(v, val);
|
||||
}
|
||||
|
||||
namespace {
|
||||
|
|
@ -493,7 +496,7 @@ namespace {
|
|||
y_max = compute_y_max(y_max + 1, a, lo, hi, M);
|
||||
if (++i == max_refinements) {
|
||||
// verbose_stream() << "y0=" << y0 << ", a=" << a << ", lo=" << lo << ", hi=" << hi << "\n";
|
||||
verbose_stream() << "refined y_max: " << y_max << "\n";
|
||||
// verbose_stream() << "refined y_max: " << y_max << "\n";
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
|
@ -505,7 +508,7 @@ namespace {
|
|||
y_min = compute_y_min(y_min - 1, a, lo, hi, M);
|
||||
if (++i == max_refinements) {
|
||||
// verbose_stream() << "y0=" << y0 << ", a=" << a << ", lo=" << lo << ", hi=" << hi << "\n";
|
||||
verbose_stream() << "refined y_min: " << y_min << "\n";
|
||||
// verbose_stream() << "refined y_min: " << y_min << "\n";
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
|
@ -520,6 +523,35 @@ namespace {
|
|||
}
|
||||
}
|
||||
|
||||
template<bool FORWARD>
|
||||
bool viable::refine_bits(pvar v, rational const& val, const svector<lbool>& fixed, const vector<ptr_vector<entry>>& justifications) {
|
||||
|
||||
pdd v_pdd = s.var(v);
|
||||
|
||||
// TODO: We might also extend simultaneously up and downwards if we want the actual interval (however, this might make use of more fixed bits and is weaker - worse - therefore)
|
||||
entry* ne = alloc_entry();
|
||||
rational new_val = extend_by_bits<FORWARD>(v_pdd, val, fixed, justifications, ne->src, ne->side_cond, ne->refined);
|
||||
|
||||
if (new_val == val) {
|
||||
m_alloc.push_back(ne);
|
||||
return true;
|
||||
}
|
||||
|
||||
ne->coeff = 1;
|
||||
if (FORWARD) {
|
||||
LOG("refine-bits for v" << v << " [" << val << ", " << new_val << "[");
|
||||
ne->interval = eval_interval::proper(v_pdd.manager().mk_val(val), val, v_pdd.manager().mk_val(new_val), new_val);
|
||||
}
|
||||
else {
|
||||
rational upper_bound = val == v_pdd.manager().max_value() ? rational::zero() : val + 1;;
|
||||
LOG("refine-bits for v" << v << " [" << new_val << ", " << upper_bound << "[");
|
||||
ne->interval = eval_interval::proper(v_pdd.manager().mk_val(new_val), new_val, v_pdd.manager().mk_val(upper_bound), upper_bound);
|
||||
}
|
||||
SASSERT(ne->interval.currently_contains(val));
|
||||
intersect(v, ne);
|
||||
return false;
|
||||
}
|
||||
|
||||
/**
|
||||
* Traverse all interval constraints with coefficients to check whether current value 'val' for
|
||||
* 'v' is feasible. If not, extract a (maximal) interval to block 'v' from being assigned val.
|
||||
|
|
@ -547,7 +579,11 @@ namespace {
|
|||
do {
|
||||
rational coeff_val = mod(e->coeff * val, mod_value);
|
||||
if (e->interval.currently_contains(coeff_val)) {
|
||||
LOG("refine-equal-lin for v" << v << " in src: " << lit_pp(s, e->src));
|
||||
IF_LOGGING(
|
||||
verbose_stream() << "refine-equal-lin for v" << v << " in src: ";
|
||||
for (const auto& src : e->src)
|
||||
verbose_stream() << lit_pp(s, src) << "\n";
|
||||
);
|
||||
LOG("forbidden interval v" << v << " " << num_pp(s, v, val) << " " << num_pp(s, v, e->coeff, true) << " * " << e->interval);
|
||||
|
||||
if (mod(e->interval.hi_val() + 1, mod_value) == e->interval.lo_val()) {
|
||||
|
|
@ -561,7 +597,7 @@ namespace {
|
|||
// No solution
|
||||
LOG("refined: no solution due to parity");
|
||||
entry* ne = alloc_entry();
|
||||
ne->refined = e;
|
||||
ne->refined.push_back(e);
|
||||
ne->src = e->src;
|
||||
ne->side_cond = e->side_cond;
|
||||
ne->coeff = 1;
|
||||
|
|
@ -578,7 +614,7 @@ namespace {
|
|||
LOG("refined to [" << num_pp(s, v, lo) << ", " << num_pp(s, v, hi) << "[");
|
||||
SASSERT_EQ(mod(a * hi, mod_value), b); // hi is the solution
|
||||
entry* ne = alloc_entry();
|
||||
ne->refined = e;
|
||||
ne->refined.push_back(e);
|
||||
ne->src = e->src;
|
||||
ne->side_cond = e->side_cond;
|
||||
ne->coeff = 1;
|
||||
|
|
@ -610,7 +646,7 @@ namespace {
|
|||
SASSERT_EQ(mod(a * (lo - 1), mod_value), b); // lo-1 is a solution
|
||||
SASSERT_EQ(mod(a * hi, mod_value), b); // hi is a solution
|
||||
entry* ne = alloc_entry();
|
||||
ne->refined = e;
|
||||
ne->refined.push_back(e);
|
||||
ne->src = e->src;
|
||||
ne->side_cond = e->side_cond;
|
||||
ne->coeff = 1;
|
||||
|
|
@ -638,7 +674,7 @@ namespace {
|
|||
if (hi == mod_value)
|
||||
hi = 0;
|
||||
entry* ne = alloc_entry();
|
||||
ne->refined = e;
|
||||
ne->refined.push_back(e);
|
||||
ne->src = e->src;
|
||||
ne->side_cond = e->side_cond;
|
||||
ne->coeff = 1;
|
||||
|
|
@ -670,7 +706,11 @@ namespace {
|
|||
m_diseq_lin[v] = m_diseq_lin[v]->next();
|
||||
|
||||
do {
|
||||
LOG("refine-disequal-lin for src: " << e->src);
|
||||
IF_LOGGING(
|
||||
verbose_stream() << "refine-disequal-lin for v" << v << " in src: ";
|
||||
for (const auto& src : e->src)
|
||||
verbose_stream() << lit_pp(s, src) << "\n";
|
||||
);
|
||||
// We compute an interval if the concrete value 'val' violates the constraint:
|
||||
// p*val + q > r*val + s if e->src.is_positive()
|
||||
// p*val + q >= r*val + s if e->src.is_negative()
|
||||
|
|
@ -681,12 +721,13 @@ namespace {
|
|||
rational const& r = e->interval.hi_val();
|
||||
rational const& s_ = e->interval.hi().val();
|
||||
SASSERT(p != r && p != 0 && r != 0);
|
||||
SASSERT(e->src.size() == 1);
|
||||
|
||||
rational const a = mod(p * val + q_, mod_value);
|
||||
rational const b = mod(r * val + s_, mod_value);
|
||||
rational const np = mod_value - p;
|
||||
rational const nr = mod_value - r;
|
||||
int const corr = e->src.is_negative() ? 1 : 0;
|
||||
int const corr = e->src[0].is_negative() ? 1 : 0;
|
||||
|
||||
auto delta_l = [&](rational const& val) {
|
||||
rational num = a - b + corr;
|
||||
|
|
@ -719,7 +760,7 @@ namespace {
|
|||
return std::min(max_value - val, dmax);
|
||||
};
|
||||
|
||||
if (a > b || (e->src.is_negative() && a == b)) {
|
||||
if (a > b || (e->src[0].is_negative() && a == b)) {
|
||||
rational lo = val - delta_l(val);
|
||||
rational hi = val + delta_u(val) + 1;
|
||||
|
||||
|
|
@ -731,7 +772,7 @@ namespace {
|
|||
pdd lop = s.var2pdd(v).mk_val(lo);
|
||||
pdd hip = s.var2pdd(v).mk_val(hi);
|
||||
entry* ne = alloc_entry();
|
||||
ne->refined = e;
|
||||
ne->refined.push_back(e);
|
||||
ne->src = e->src;
|
||||
ne->side_cond = e->side_cond;
|
||||
ne->coeff = 1;
|
||||
|
|
@ -745,11 +786,280 @@ namespace {
|
|||
return true;
|
||||
}
|
||||
|
||||
// Skips all values that are not feasible w.r.t. fixed bits
|
||||
template<bool FORWARD>
|
||||
rational viable::extend_by_bits(const pdd& var, const rational& bound, const svector<lbool>& fixed, const vector<ptr_vector<entry>>& justifications, vector<signed_constraint>& src, vector<signed_constraint>& side_cond, ptr_vector<entry const>& refined) const {
|
||||
unsigned k = var.power_of_2();
|
||||
if (fixed.empty())
|
||||
return bound;
|
||||
|
||||
SASSERT(k == fixed.size());
|
||||
|
||||
auto add_justification = [&](unsigned i) {
|
||||
auto& to_add = justifications[i];
|
||||
SASSERT(!to_add.empty());
|
||||
for (auto& add : to_add) {
|
||||
// TODO: Check for duplicates; maybe we add the same src/side_cond over and over again
|
||||
for (auto& sc : add->side_cond)
|
||||
side_cond.push_back(sc);
|
||||
for (auto& c : add->src)
|
||||
src.push_back(c);
|
||||
refined.push_back(add);
|
||||
}
|
||||
};
|
||||
|
||||
unsigned firstFail;
|
||||
for (firstFail = k; firstFail > 0; firstFail--) {
|
||||
if (fixed[firstFail - 1] != l_undef) {
|
||||
lbool current = bound.get_bit(firstFail - 1) ? l_true : l_false;
|
||||
if (current != fixed[firstFail - 1])
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (firstFail == 0)
|
||||
return bound; // the value is feasible according to fixed bits
|
||||
|
||||
svector<lbool> new_bound(fixed.size());
|
||||
|
||||
for (unsigned i = 0; i < firstFail; i++) {
|
||||
if (fixed[i] != l_undef) {
|
||||
SASSERT(fixed[i] == l_true || fixed[i] == l_false);
|
||||
new_bound[i] = fixed[i];
|
||||
if (i == firstFail - 1 || FORWARD != (fixed[i] == l_false))
|
||||
add_justification(i); // Minimize number of responsible fixed bits; we only add those justifications we need for sure
|
||||
}
|
||||
else
|
||||
new_bound[i] = FORWARD ? l_false : l_true;
|
||||
}
|
||||
|
||||
bool carry = fixed[firstFail - 1] == (FORWARD ? l_false : l_true);
|
||||
|
||||
for (unsigned i = firstFail; i < new_bound.size(); i++) {
|
||||
if (fixed[i] == l_undef) {
|
||||
lbool current = bound.get_bit(i) ? l_true : l_false;
|
||||
if (carry) {
|
||||
if (FORWARD) {
|
||||
if (current == l_false) {
|
||||
new_bound[i] = l_true;
|
||||
carry = false;
|
||||
}
|
||||
else
|
||||
new_bound[i] = l_false;
|
||||
}
|
||||
else {
|
||||
if (current == l_true) {
|
||||
new_bound[i] = l_false;
|
||||
carry = false;
|
||||
}
|
||||
else
|
||||
new_bound[i] = l_true;
|
||||
}
|
||||
}
|
||||
else
|
||||
new_bound[i] = current;
|
||||
}
|
||||
else {
|
||||
new_bound[i] = fixed[i];
|
||||
if (carry)
|
||||
add_justification(i); // Again, we need this justification; if carry is false we don't need it
|
||||
}
|
||||
}
|
||||
SASSERT(!src.empty());
|
||||
if (carry) {
|
||||
// We covered everything
|
||||
/*if (FORWARD)
|
||||
return rational::power_of_two(k);
|
||||
else*/
|
||||
return rational::zero();
|
||||
}
|
||||
|
||||
// TODO: Directly convert new_bound in rational?
|
||||
rational ret = rational::zero();
|
||||
for (unsigned i = new_bound.size(); i > 0; i--) {
|
||||
ret *= 2;
|
||||
SASSERT(new_bound[i - 1] != l_undef);
|
||||
ret += new_bound[i - 1] == l_true ? 1 : 0;
|
||||
}
|
||||
if (!FORWARD)
|
||||
return ret + 1;
|
||||
return ret;
|
||||
}
|
||||
|
||||
// returns true iff no conflict was encountered
|
||||
bool viable::collect_bit_information(pvar v, bool add_conflict, svector<lbool>& fixed, vector<ptr_vector<entry>>& justifications) {
|
||||
|
||||
pdd p = s.var(v);
|
||||
// maybe pass them as arguments rather than having them as fields...
|
||||
fixed.clear();
|
||||
justifications.clear();
|
||||
fixed.resize(p.power_of_2(), l_undef);
|
||||
justifications.resize(p.power_of_2(), ptr_vector<entry>());
|
||||
|
||||
auto* e = m_equal_lin[v];
|
||||
auto* first = e;
|
||||
if (!e)
|
||||
return true;
|
||||
|
||||
clause_builder builder(s, "bit check");
|
||||
vector<std::pair<entry*, trailing_bits>> postponed;
|
||||
|
||||
auto add_entry = [&builder](entry* e) {
|
||||
for (const auto& sc : e->side_cond)
|
||||
builder.insert_eval(~sc);
|
||||
for (const auto& src : e->src)
|
||||
builder.insert_eval(~src);
|
||||
};
|
||||
|
||||
auto add_entry_list = [add_entry](const ptr_vector<entry>& list) {
|
||||
for (const auto& e : list)
|
||||
add_entry(e);
|
||||
};
|
||||
|
||||
unsigned largest_mask = 0;
|
||||
|
||||
do {
|
||||
if (e->src.size() != 1) {
|
||||
// We just consider the ordinary constraints and not already contracted ones
|
||||
e = e->next();
|
||||
continue;
|
||||
}
|
||||
signed_constraint& src = e->src[0];
|
||||
single_bit bit;
|
||||
trailing_bits mask;
|
||||
if (src->is_ule() &&
|
||||
simplify_clause::get_bit(s.subst(src->to_ule().lhs()), s.subst(src->to_ule().rhs()), p, bit, src.is_positive()) && p.is_var()) {
|
||||
|
||||
lbool prev = fixed[bit.position];
|
||||
fixed[bit.position] = bit.positive ? l_true : l_false;
|
||||
//verbose_stream() << "Setting bit " << bit.position << " to " << bit.positive << " because of " << e->src << "\n";
|
||||
if (prev != l_undef && fixed[bit.position] != prev) {
|
||||
LOG("Bit conflicting " << e->src << " with " << justifications[bit.position][0]->src);
|
||||
if (add_conflict) {
|
||||
add_entry_list(justifications[bit.position]);
|
||||
add_entry(e);
|
||||
s.set_conflict(*builder.build());
|
||||
}
|
||||
return false;
|
||||
}
|
||||
// just override; we prefer bit constraints over parity as those are easier for subsumption to remove
|
||||
// verbose_stream() << "Adding bit constraint: " << e->src[0] << " (" << bit.position << ")\n";
|
||||
justifications[bit.position].clear();
|
||||
justifications[bit.position].push_back(e);
|
||||
}
|
||||
else if ((src->is_eq() || src.is_diseq()) &&
|
||||
simplify_clause::get_trailing_mask(s.subst(src->to_ule().lhs()), s.subst(src->to_ule().rhs()), p, mask, src.is_positive()) && p.is_var()) {
|
||||
|
||||
if (src.is_positive()) {
|
||||
for (unsigned i = 0; i < mask.length; i++) {
|
||||
lbool prev = fixed[i];
|
||||
fixed[i] = mask.bits.get_bit(i) ? l_true : l_false;
|
||||
//verbose_stream() << "Setting bit " << i << " to " << mask.bits.get_bit(i) << " because of parity " << e->src << "\n";
|
||||
if (prev != l_undef) {
|
||||
if (fixed[i] != prev) {
|
||||
LOG("Positive parity conflicting " << e->src << " with " << justifications[i][0]->src);
|
||||
if (add_conflict) {
|
||||
add_entry_list(justifications[i]);
|
||||
add_entry(e);
|
||||
s.set_conflict(*builder.build());
|
||||
}
|
||||
return false;
|
||||
}
|
||||
else {
|
||||
// Prefer justifications from larger masks (less premisses)
|
||||
if (largest_mask < mask.length) {
|
||||
largest_mask = mask.length;
|
||||
justifications[i].clear();
|
||||
justifications[i].push_back(e);
|
||||
// verbose_stream() << "Adding parity constraint: " << e->src[0] << " (" << i << ")\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
else {
|
||||
SASSERT(justifications[i].empty());
|
||||
justifications[i].push_back(e);
|
||||
// verbose_stream() << "Adding parity constraint: " << e->src[0] << " (" << i << ")\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
postponed.push_back({ e, mask });
|
||||
}
|
||||
e = e->next();
|
||||
} while(e != first);
|
||||
|
||||
// TODO: Incomplete - e.g., if we know the trailing bits are not 00 not 10 not 01 and not 11 we could also detect a conflict
|
||||
// This would require partially clause solving (worth the effort?)
|
||||
bool_vector removed(postponed.size(), false);
|
||||
bool changed;
|
||||
do { // fixed-point required?
|
||||
changed = false;
|
||||
for (unsigned j = 0; j < postponed.size(); j++) {
|
||||
if (removed[j])
|
||||
continue;
|
||||
const auto& neg = postponed[j];
|
||||
unsigned indet = 0;
|
||||
unsigned last_indet = 0;
|
||||
unsigned i = 0;
|
||||
for (; i < neg.second.length; i++) {
|
||||
if (fixed[i] != l_undef) {
|
||||
if (fixed[i] != (neg.second.bits.get_bit(i) ? l_true : l_false)) {
|
||||
removed[j] = true;
|
||||
break; // this is already satisfied
|
||||
}
|
||||
}
|
||||
else {
|
||||
indet++;
|
||||
last_indet = i;
|
||||
}
|
||||
}
|
||||
if (i == neg.second.length) {
|
||||
if (indet == 0) {
|
||||
// Already false
|
||||
LOG("Found conflict with constraint " << neg.first->src);
|
||||
if (add_conflict) {
|
||||
for (unsigned k = 0; k < neg.second.length; k++)
|
||||
add_entry_list(justifications[k]);
|
||||
add_entry(neg.first);
|
||||
s.set_conflict(*builder.build());
|
||||
}
|
||||
return false;
|
||||
}
|
||||
else if (indet == 1) {
|
||||
// Simple BCP
|
||||
auto& justification = justifications[last_indet];
|
||||
SASSERT(justification.empty());
|
||||
for (unsigned k = 0; k < neg.second.length; k++) {
|
||||
if (k != last_indet) {
|
||||
SASSERT(fixed[k] != l_undef);
|
||||
for (const auto& just : justifications[k])
|
||||
justification.push_back(just);
|
||||
}
|
||||
}
|
||||
justification.push_back(neg.first);
|
||||
fixed[last_indet] = neg.second.bits.get_bit(last_indet) ? l_false : l_true;
|
||||
removed[j] = true;
|
||||
LOG("Applying fast BCP on bit " << last_indet << " from constraint " << neg.first->src);
|
||||
changed = true;
|
||||
}
|
||||
}
|
||||
}
|
||||
} while(changed);
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
bool viable::has_viable(pvar v) {
|
||||
|
||||
svector<lbool> fixed;
|
||||
vector<ptr_vector<entry>> justifications;
|
||||
|
||||
if (!collect_bit_information(v, false, fixed, justifications))
|
||||
return false;
|
||||
|
||||
refined:
|
||||
auto* e = m_units[v];
|
||||
|
||||
#define CHECK_RETURN(val) { if (refine_viable(v, val)) return true; else goto refined; }
|
||||
#define CHECK_RETURN(val) { if (refine_viable<true>(v, val, fixed, justifications)) return true; else goto refined; }
|
||||
|
||||
if (!e)
|
||||
CHECK_RETURN(rational::zero());
|
||||
|
|
@ -784,9 +1094,15 @@ namespace {
|
|||
}
|
||||
|
||||
bool viable::is_viable(pvar v, rational const& val) {
|
||||
|
||||
svector<lbool> fixed;
|
||||
vector<ptr_vector<entry>> justifications;
|
||||
|
||||
if (!collect_bit_information(v, false, fixed, justifications))
|
||||
return false;
|
||||
auto* e = m_units[v];
|
||||
if (!e)
|
||||
return refine_viable(v, val);
|
||||
return refine_viable<true>(v, val, fixed, justifications);
|
||||
entry* first = e;
|
||||
entry* last = first->prev();
|
||||
if (last->interval.currently_contains(val))
|
||||
|
|
@ -795,9 +1111,9 @@ namespace {
|
|||
if (e->interval.currently_contains(val))
|
||||
return false;
|
||||
if (val < e->interval.lo_val())
|
||||
return refine_viable(v, val);
|
||||
return refine_viable<true>(v, val, fixed, justifications);
|
||||
}
|
||||
return refine_viable(v, val);
|
||||
return refine_viable<true>(v, val, fixed, justifications);
|
||||
}
|
||||
|
||||
find_t viable::find_viable(pvar v, rational& lo) {
|
||||
|
|
@ -835,17 +1151,19 @@ namespace {
|
|||
do {
|
||||
found = false;
|
||||
do {
|
||||
if (!e->refined && e->side_cond.empty()) {
|
||||
if (e->refined.empty() && e->side_cond.empty()) {
|
||||
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() > hi.val()) {
|
||||
out_c.push_back(e->src);
|
||||
for (signed_constraint src : e->src)
|
||||
out_c.push_back(src);
|
||||
out_hi = lo.val() - 1;
|
||||
found = true;
|
||||
}
|
||||
else if (!out_c.empty() && lo.val() <= out_hi && out_hi < hi.val()) {
|
||||
out_c.push_back(e->src);
|
||||
for (signed_constraint src : e->src)
|
||||
out_c.push_back(src);
|
||||
out_hi = lo.val() - 1;
|
||||
found = true;
|
||||
}
|
||||
|
|
@ -869,17 +1187,19 @@ namespace {
|
|||
do {
|
||||
found = false;
|
||||
do {
|
||||
if (!e->refined && e->side_cond.empty()) {
|
||||
if (e->refined.empty() && e->side_cond.empty()) {
|
||||
auto const& lo = e->interval.lo();
|
||||
auto const& hi = e->interval.hi();
|
||||
if (lo.is_val() && hi.is_val()) {
|
||||
if (out_c.empty() && hi.val() != 0 && (lo.val() == 0 || lo.val() > hi.val())) {
|
||||
out_c.push_back(e->src);
|
||||
for (signed_constraint src : e->src)
|
||||
out_c.push_back(src);
|
||||
out_lo = hi.val();
|
||||
found = true;
|
||||
}
|
||||
else if (!out_c.empty() && lo.val() <= out_lo && out_lo < hi.val()) {
|
||||
out_c.push_back(e->src);
|
||||
for (signed_constraint src : e->src)
|
||||
out_c.push_back(src);
|
||||
out_lo = hi.val();
|
||||
found = true;
|
||||
}
|
||||
|
|
@ -904,14 +1224,17 @@ namespace {
|
|||
if (!e)
|
||||
return false;
|
||||
|
||||
bool found = false;
|
||||
|
||||
do {
|
||||
if (e->src == c)
|
||||
found = e->src.contains(c);
|
||||
if (found)
|
||||
break;
|
||||
e = e->next();
|
||||
}
|
||||
while (e != first);
|
||||
|
||||
if (e->src != c)
|
||||
if (!found)
|
||||
return false;
|
||||
entry const* e0 = e;
|
||||
|
||||
|
|
@ -945,7 +1268,7 @@ namespace {
|
|||
e0_prev = e;
|
||||
out_hi = e->interval.hi_val();
|
||||
}
|
||||
else if (e->src == c) {
|
||||
else if (e->src.contains(c)) {
|
||||
// multiple intervals from the same constraint c
|
||||
// TODO: adjacent intervals would fine but they should be merged at insertion instead of considering them here.
|
||||
return false;
|
||||
|
|
@ -956,9 +1279,10 @@ namespace {
|
|||
out_c.push_back(c);
|
||||
}
|
||||
if (e != e0) {
|
||||
for (auto sc : e->side_cond)
|
||||
for (signed_constraint sc : e->side_cond)
|
||||
out_c.push_back(sc);
|
||||
out_c.push_back(e->src);
|
||||
for (signed_constraint src : e->src)
|
||||
out_c.push_back(src);
|
||||
}
|
||||
e = n;
|
||||
}
|
||||
|
|
@ -991,6 +1315,13 @@ namespace {
|
|||
|
||||
template <query_t mode>
|
||||
lbool viable::query(pvar v, typename query_result<mode>::result_t& result) {
|
||||
|
||||
svector<lbool> fixed;
|
||||
vector<ptr_vector<entry>> justifications;
|
||||
|
||||
if (!collect_bit_information(v, true, fixed, justifications))
|
||||
return l_false; // conflict already added
|
||||
|
||||
// max number of interval refinements before falling back to the univariate solver
|
||||
unsigned const refinement_budget = 1000;
|
||||
unsigned refinements = refinement_budget;
|
||||
|
|
@ -999,11 +1330,11 @@ namespace {
|
|||
lbool res = l_undef;
|
||||
|
||||
if constexpr (mode == query_t::find_viable)
|
||||
res = query_find(v, result.first, result.second);
|
||||
res = query_find(v, result.first, result.second, fixed, justifications);
|
||||
else if constexpr (mode == query_t::min_viable)
|
||||
res = query_min(v, result);
|
||||
res = query_min(v, result, fixed, justifications);
|
||||
else if constexpr (mode == query_t::max_viable)
|
||||
res = query_max(v, result);
|
||||
res = query_max(v, result, fixed, justifications);
|
||||
else if constexpr (mode == query_t::has_viable) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
|
@ -1018,8 +1349,8 @@ namespace {
|
|||
LOG("Refinement budget exhausted! Fall back to univariate solver.");
|
||||
return query_fallback<mode>(v, result);
|
||||
}
|
||||
|
||||
lbool viable::query_find(pvar v, rational& lo, rational& hi) {
|
||||
|
||||
lbool viable::query_find(pvar v, rational& lo, rational& hi, const svector<lbool>& fixed, const vector<ptr_vector<entry>>& justifications) {
|
||||
auto const& max_value = s.var2pdd(v).max_value();
|
||||
lbool const refined = l_undef;
|
||||
|
||||
|
|
@ -1028,11 +1359,11 @@ namespace {
|
|||
// For this reason, we start chasing the intervals from the start again.
|
||||
lo = 0;
|
||||
hi = max_value;
|
||||
|
||||
|
||||
auto* e = m_units[v];
|
||||
if (!e && !refine_viable(v, lo))
|
||||
if (!e && !refine_viable<true>(v, lo, fixed, justifications))
|
||||
return refined;
|
||||
if (!e && !refine_viable(v, hi))
|
||||
if (!e && !refine_viable<false>(v, hi, fixed, justifications))
|
||||
return refined;
|
||||
if (!e)
|
||||
return l_true;
|
||||
|
|
@ -1049,9 +1380,9 @@ namespace {
|
|||
if (last->interval.lo_val() < last->interval.hi_val() &&
|
||||
last->interval.hi_val() < max_value) {
|
||||
lo = last->interval.hi_val();
|
||||
if (!refine_viable(v, lo))
|
||||
if (!refine_viable<true>(v, lo, fixed, justifications))
|
||||
return refined;
|
||||
if (!refine_viable(v, max_value))
|
||||
if (!refine_viable<false>(v, max_value, fixed, justifications))
|
||||
return refined;
|
||||
return l_true;
|
||||
}
|
||||
|
|
@ -1083,18 +1414,18 @@ namespace {
|
|||
}
|
||||
while (e != last);
|
||||
|
||||
if (!refine_viable(v, lo))
|
||||
if (!refine_viable<true>(v, lo, fixed, justifications))
|
||||
return refined;
|
||||
if (!refine_viable(v, hi))
|
||||
if (!refine_viable<false>(v, hi, fixed, justifications))
|
||||
return refined;
|
||||
return l_true;
|
||||
}
|
||||
|
||||
lbool viable::query_min(pvar v, rational& lo) {
|
||||
lbool viable::query_min(pvar v, rational& lo, const svector<lbool>& fixed, const vector<ptr_vector<entry>>& justifications) {
|
||||
// TODO: should be able to deal with UNSAT case; since also min_viable has to deal with it due to fallback solver
|
||||
lo = 0;
|
||||
entry* e = m_units[v];
|
||||
if (!e && !refine_viable(v, lo))
|
||||
if (!e && !refine_viable<true>(v, lo, fixed, justifications))
|
||||
return l_undef;
|
||||
if (!e)
|
||||
return l_true;
|
||||
|
|
@ -1109,17 +1440,17 @@ namespace {
|
|||
e = e->next();
|
||||
}
|
||||
while (e != first);
|
||||
if (!refine_viable(v, lo))
|
||||
if (!refine_viable<true>(v, lo, fixed, justifications))
|
||||
return l_undef;
|
||||
SASSERT(is_viable(v, lo));
|
||||
return l_true;
|
||||
}
|
||||
|
||||
lbool viable::query_max(pvar v, rational& hi) {
|
||||
lbool viable::query_max(pvar v, rational& hi, const svector<lbool>& fixed, const vector<ptr_vector<entry>>& justifications) {
|
||||
// TODO: should be able to deal with UNSAT case; since also max_viable has to deal with it due to fallback solver
|
||||
hi = s.var2pdd(v).max_value();
|
||||
auto* e = m_units[v];
|
||||
if (!e && !refine_viable(v, hi))
|
||||
if (!e && !refine_viable<false>(v, hi, fixed, justifications))
|
||||
return l_undef;
|
||||
if (!e)
|
||||
return l_true;
|
||||
|
|
@ -1132,7 +1463,7 @@ namespace {
|
|||
e = e->prev();
|
||||
}
|
||||
while (e != last);
|
||||
if (!refine_viable(v, hi))
|
||||
if (!refine_viable<false>(v, hi, fixed, justifications))
|
||||
return l_undef;
|
||||
SASSERT(is_viable(v, hi));
|
||||
return l_true;
|
||||
|
|
@ -1151,16 +1482,26 @@ namespace {
|
|||
entry const* first = m_units[v];
|
||||
entry const* e = first;
|
||||
do {
|
||||
entry const* origin = e;
|
||||
while (origin->refined)
|
||||
origin = origin->refined;
|
||||
signed_constraint const c = origin->src;
|
||||
sat::literal const lit = c.blit();
|
||||
if (!added.contains(lit)) {
|
||||
added.insert(lit);
|
||||
LOG("Adding " << lit_pp(s, lit));
|
||||
IF_VERBOSE(10, verbose_stream() << ";; " << lit_pp(s, lit) << "\n");
|
||||
c.add_to_univariate_solver(v, s, *us, lit.to_uint());
|
||||
ptr_vector<entry const> to_process = e->refined;
|
||||
while (!to_process.empty()) {
|
||||
auto current = to_process.back();
|
||||
to_process.pop_back();
|
||||
if (!current->refined.empty()) {
|
||||
for (auto& ref : current->refined)
|
||||
to_process.push_back(ref);
|
||||
continue;
|
||||
}
|
||||
const entry* origin = current;
|
||||
for (const auto& src : origin->src) {
|
||||
sat::literal const lit = src.blit();
|
||||
if (!added.contains(lit)) {
|
||||
added.insert(lit);
|
||||
LOG("Adding " << lit_pp(s, lit));
|
||||
IF_VERBOSE(10, verbose_stream() << ";; " << lit_pp(s, lit) << "\n");
|
||||
verbose_stream() << ";; " << lit_pp(s, lit) << "\n";
|
||||
src.add_to_univariate_solver(v, s, *us, lit.to_uint());
|
||||
}
|
||||
}
|
||||
}
|
||||
e = e->next();
|
||||
}
|
||||
|
|
@ -1250,6 +1591,7 @@ namespace {
|
|||
SASSERT(!core.vars().contains(v));
|
||||
core.add_lemma("viable unsat core", core.build_lemma());
|
||||
verbose_stream() << "unsat core " << core << "\n";
|
||||
//exit(0);
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -1262,9 +1604,23 @@ namespace {
|
|||
entry const* first = e;
|
||||
SASSERT(e);
|
||||
// If there is a full interval, all others would have been removed
|
||||
SASSERT(!e->interval.is_full() || e->next() == e);
|
||||
SASSERT(e->interval.is_full() || all_of(*e, [](entry const& f) { return !f.interval.is_full(); }));
|
||||
clause_builder lemma(s);
|
||||
if (first->interval.is_full()) {
|
||||
SASSERT(first->next() == first);
|
||||
for (auto sc : first->side_cond)
|
||||
lemma.insert_eval(~sc);
|
||||
for (const auto& src : first->src) {
|
||||
lemma.insert(~src);
|
||||
core.insert(src);
|
||||
core.insert_vars(src);
|
||||
}
|
||||
core.add_lemma("viable", lemma.build());
|
||||
core.logger().log(inf_fi(*this, v));
|
||||
return true;
|
||||
}
|
||||
|
||||
SASSERT(all_of(*first, [](entry const& f) { return !f.interval.is_full(); }));
|
||||
|
||||
do {
|
||||
// Build constraint: upper bound of each interval is not contained in the next interval,
|
||||
// using the equivalence: t \in [l;h[ <=> t-l < h-l
|
||||
|
|
@ -1310,15 +1666,16 @@ namespace {
|
|||
|
||||
// verbose_stream() << e->interval << " " << e->side_cond << " " << e->src << ";\n";
|
||||
|
||||
if (!e->interval.is_full()) {
|
||||
signed_constraint c = s.m_constraints.elem(e->interval.hi(), n->interval.symbolic());
|
||||
lemma.insert_try_eval(~c);
|
||||
}
|
||||
signed_constraint c = s.m_constraints.elem(e->interval.hi(), n->interval.symbolic());
|
||||
lemma.insert_try_eval(~c);
|
||||
|
||||
for (auto sc : e->side_cond)
|
||||
lemma.insert_eval(~sc);
|
||||
lemma.insert(~e->src);
|
||||
core.insert(e->src);
|
||||
core.insert_vars(e->src);
|
||||
for (const auto& src : e->src) {
|
||||
lemma.insert(~src);
|
||||
core.insert(src);
|
||||
core.insert_vars(src);
|
||||
}
|
||||
e = n;
|
||||
}
|
||||
while (e != first);
|
||||
|
|
@ -1339,7 +1696,12 @@ namespace {
|
|||
return;
|
||||
entry* first = e;
|
||||
do {
|
||||
LOG("v" << v << ": " << e->interval << " " << e->side_cond << " " << e->src);
|
||||
IF_LOGGING(
|
||||
verbose_stream() << "v" << v << ": " << e->interval << " " << e->side_cond << " ";
|
||||
for (const auto& src : e->src)
|
||||
verbose_stream() << src << " ";
|
||||
verbose_stream() << "\n";
|
||||
);
|
||||
e = e->next();
|
||||
}
|
||||
while (e != first);
|
||||
|
|
@ -1363,7 +1725,7 @@ namespace {
|
|||
rational const& s_ = e->interval.hi().val();
|
||||
out << "[ ";
|
||||
out << val_pp(m, p, true) << "*v" << v << " + " << val_pp(m, q_);
|
||||
out << (e->src.is_positive() ? " > " : " >= ");
|
||||
out << (e->src[0].is_positive() ? " > " : " >= ");
|
||||
out << val_pp(m, r, true) << "*v" << v << " + " << val_pp(m, s_);
|
||||
out << " ] ";
|
||||
}
|
||||
|
|
@ -1371,7 +1733,9 @@ namespace {
|
|||
out << e->coeff << " * v" << v << " " << e->interval << " ";
|
||||
else
|
||||
out << e->interval << " ";
|
||||
out << e->side_cond << " " << e->src << "; ";
|
||||
out << e->side_cond << " ";
|
||||
for (const auto& src : e->src)
|
||||
out << src << "; ";
|
||||
return out;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -72,12 +72,13 @@ namespace polysat {
|
|||
|
||||
class viable {
|
||||
friend class test_fi;
|
||||
friend class test_polysat;
|
||||
|
||||
solver& s;
|
||||
forbidden_intervals m_forbidden_intervals;
|
||||
|
||||
struct entry final : public dll_base<entry>, public fi_record {
|
||||
entry const* refined = nullptr;
|
||||
ptr_vector<entry const> refined;
|
||||
};
|
||||
enum class entry_kind { unit_e, equal_e, diseq_e };
|
||||
|
||||
|
|
@ -93,12 +94,21 @@ namespace polysat {
|
|||
|
||||
bool intersect(pvar v, entry* e);
|
||||
|
||||
bool refine_viable(pvar v, rational const& val);
|
||||
template<bool FORWARD>
|
||||
bool refine_viable(pvar v, rational const& val, const svector<lbool>& fixed, const vector<ptr_vector<entry>>& justifications);
|
||||
|
||||
template<bool FORWARD>
|
||||
bool refine_bits(pvar v, rational const& val, const svector<lbool>& fixed, const vector<ptr_vector<entry>>& justifications);
|
||||
|
||||
bool refine_equal_lin(pvar v, rational const& val);
|
||||
|
||||
bool refine_disequal_lin(pvar v, rational const& val);
|
||||
|
||||
template<bool FORWARD>
|
||||
rational extend_by_bits(const pdd& var, const rational& bounds, const svector<lbool>& fixed, const vector<ptr_vector<entry>>& justifications, vector<signed_constraint>& src, vector<signed_constraint>& side_cond, ptr_vector<entry const>& refined) const;
|
||||
|
||||
bool collect_bit_information(pvar v, bool add_conflict, svector<lbool>& fixed, vector<ptr_vector<entry>>& justifications);
|
||||
|
||||
std::ostream& display_one(std::ostream& out, pvar v, entry const* e) const;
|
||||
std::ostream& display_all(std::ostream& out, pvar v, entry const* e, char const* delimiter = "") const;
|
||||
|
||||
|
|
@ -110,9 +120,9 @@ namespace polysat {
|
|||
* Interval-based queries
|
||||
* @return l_true on success, l_false on conflict, l_undef on refinement
|
||||
*/
|
||||
lbool query_min(pvar v, rational& out_lo);
|
||||
lbool query_max(pvar v, rational& out_hi);
|
||||
lbool query_find(pvar v, rational& out_lo, rational& out_hi);
|
||||
lbool query_min(pvar v, rational& out_lo, const svector<lbool>& fixed, const vector<ptr_vector<entry>>& justifications);
|
||||
lbool query_max(pvar v, rational& out_hi, const svector<lbool>& fixed, const vector<ptr_vector<entry>>& justifications);
|
||||
lbool query_find(pvar v, rational& out_lo, rational& out_hi, const svector<lbool>& fixed, const vector<ptr_vector<entry>>& justifications);
|
||||
|
||||
/**
|
||||
* Bitblasting-based queries.
|
||||
|
|
@ -249,7 +259,7 @@ namespace polysat {
|
|||
curr(curr), visited(visited || !curr) {}
|
||||
|
||||
iterator& operator++() {
|
||||
if (idx < curr->side_cond.size())
|
||||
if (idx < curr->side_cond.size() + curr->src.size() - 1)
|
||||
++idx;
|
||||
else {
|
||||
idx = 0;
|
||||
|
|
@ -260,7 +270,7 @@ namespace polysat {
|
|||
}
|
||||
|
||||
signed_constraint& operator*() {
|
||||
return idx < curr->side_cond.size() ? curr->side_cond[idx] : curr->src;
|
||||
return idx < curr->side_cond.size() ? curr->side_cond[idx] : curr->src[idx - curr->side_cond.size()];
|
||||
}
|
||||
|
||||
bool operator==(iterator const& other) const {
|
||||
|
|
|
|||
|
|
@ -668,6 +668,36 @@ namespace polysat {
|
|||
VERIFY_EQ((*cl)[0], s.ule(p, q).blit());
|
||||
}
|
||||
|
||||
// 2^1*x + 2^1 == 0 and 2^2*x == 0
|
||||
static void test_fi_quickcheck1() {
|
||||
scoped_solver s(__func__);
|
||||
auto x = s.var(s.add_var(3));
|
||||
signed_constraint c1 = s.eq(x * 2 + 2, 0);
|
||||
signed_constraint c2 = s.eq(4 * x, 0);
|
||||
s.add_clause(c1, false);
|
||||
s.add_clause(c2, false);
|
||||
s.m_viable.intersect(x.var(), c1);
|
||||
s.m_viable.intersect(x.var(), c2);
|
||||
svector<lbool> fixed;
|
||||
vector<ptr_vector<viable::entry>> justifications;
|
||||
VERIFY(!s.m_viable.collect_bit_information(x.var(), false, fixed, justifications));
|
||||
}
|
||||
|
||||
// parity(x) >= 3 and bit_1(x)
|
||||
static void test_fi_quickcheck2() {
|
||||
scoped_solver s(__func__);
|
||||
auto x = s.var(s.add_var(4));
|
||||
signed_constraint c1 = s.parity_at_least(x, 3);
|
||||
signed_constraint c2 = s.bit(x, 1);
|
||||
s.add_clause(c1, false);
|
||||
s.add_clause(c2, false);
|
||||
s.m_viable.intersect(x.var(), c1);
|
||||
s.m_viable.intersect(x.var(), c2);
|
||||
svector<lbool> fixed;
|
||||
vector<ptr_vector<viable::entry>> justifications;
|
||||
VERIFY(!s.m_viable.collect_bit_information(x.var(), false, fixed, justifications));
|
||||
}
|
||||
|
||||
// 8 * x + 3 == 0 or 8 * x + 5 == 0 is unsat
|
||||
static void test_parity1() {
|
||||
scoped_solver s(__func__);
|
||||
|
|
@ -1462,9 +1492,9 @@ namespace polysat {
|
|||
}
|
||||
|
||||
// x*y <= b & a <= x & !Omega(x*y) => a*y <= b
|
||||
static void test_ineq_axiom4(unsigned bw = 32) {
|
||||
static void test_ineq_axiom4(unsigned bw = 32, unsigned i = 0) {
|
||||
auto const bound = rational::power_of_two(bw/2);
|
||||
for (unsigned i = 0; i < 24; ++i) {
|
||||
for (; i < 24; ++i) {
|
||||
scoped_solver s(concat(__func__, " bw=", bw, " perm=", i));
|
||||
auto x = s.var(s.add_var(bw));
|
||||
auto y = s.var(s.add_var(bw));
|
||||
|
|
@ -1922,7 +1952,7 @@ static void STD_CALL polysat_on_ctrl_c(int) {
|
|||
|
||||
void tst_polysat() {
|
||||
using namespace polysat;
|
||||
|
||||
test_polysat::test_ineq_axiom4(32, 7);
|
||||
#if 0 // Enable this block to run a single unit test with detailed output.
|
||||
collect_test_records = false;
|
||||
test_max_conflicts = 50;
|
||||
|
|
@ -2037,7 +2067,9 @@ void tst_polysat() {
|
|||
RUN(test_polysat::test_ineq_axiom6());
|
||||
RUN(test_polysat::test_ineq_non_axiom1());
|
||||
RUN(test_polysat::test_ineq_non_axiom4());
|
||||
|
||||
|
||||
RUN(test_polysat::test_fi_quickcheck1());
|
||||
RUN(test_polysat::test_fi_quickcheck2());
|
||||
if (collect_test_records)
|
||||
test_records.display(std::cout);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue