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

univariate solver: support constraints on lower bits

Browse source
This commit is contained in:
Jakob Rath 2023-11-29 14:57:09 +01:00
parent c29d04d431
commit 27bc858509
6 changed files with 124 additions and 117 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -720,6 +720,7 @@ namespace polysat {
} }
void op_constraint::add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const { void op_constraint::add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const {
unsigned const N = p().power_of_2();
pdd pv = s.subst(p()); pdd pv = s.subst(p());
if (!pv.is_univariate_in(v)) if (!pv.is_univariate_in(v))
return; return;
@ -731,22 +732,22 @@ namespace polysat {
return; return;
switch (m_op) { switch (m_op) {
case code::lshr_op: case code::lshr_op:
us.add_lshr(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep); us.add_lshr(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, N, dep);
break; break;
case code::shl_op: case code::shl_op:
us.add_shl(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep); us.add_shl(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, N, dep);
break; break;
case code::and_op: case code::and_op:
us.add_and(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep); us.add_and(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, N, dep);
break; break;
case code::inv_op: case code::inv_op:
us.add_inv(pv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep); us.add_inv(pv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, N, dep);
break; break;
case code::udiv_op: case code::udiv_op:
us.add_udiv(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep); us.add_udiv(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, N, dep);
break; break;
case code::urem_op: case code::urem_op:
us.add_urem(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, dep); us.add_urem(pv.get_univariate_coefficients(), qv.get_univariate_coefficients(), rv.get_univariate_coefficients(), !is_positive, N, dep);
break; break;
default: default:
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();

4
src/math/polysat/smul_fl_constraint.cpp
View file

@ -127,9 +127,9 @@ namespace polysat {
if (!q1.is_univariate_in(v)) if (!q1.is_univariate_in(v))
return; return;
if (is_overflow()) if (is_overflow())
us.add_smul_ovfl(p1.get_univariate_coefficients(), q1.get_univariate_coefficients(), !is_positive, dep); us.add_smul_ovfl(p1.get_univariate_coefficients(), q1.get_univariate_coefficients(), !is_positive, p1.power_of_2(), dep);
else else
us.add_smul_udfl(p1.get_univariate_coefficients(), q1.get_univariate_coefficients(), !is_positive, dep); us.add_smul_udfl(p1.get_univariate_coefficients(), q1.get_univariate_coefficients(), !is_positive, p1.power_of_2(), dep);
} }
} }

6
src/math/polysat/ule_constraint.cpp
View file

@ -391,10 +391,10 @@ namespace polysat {
bool q_ok = q.is_univariate_in(v); bool q_ok = q.is_univariate_in(v);
IF_VERBOSE(10, display(verbose_stream() << ";; ", to_lbool(is_positive), p, q) << "\n"); IF_VERBOSE(10, display(verbose_stream() << ";; ", to_lbool(is_positive), p, q) << "\n");
if (!is_positive && !q_ok) // add p > 0 if (!is_positive && !q_ok) // add p > 0
us.add_ugt(p.get_univariate_coefficients(), rational::zero(), false, dep); us.add_ugt(p.get_univariate_coefficients(), rational::zero(), false, p.power_of_2(), dep);
if (!is_positive && !p_ok) // add -1 > q <==> q+1 > 0 if (!is_positive && !p_ok) // add -1 > q <==> q+1 > 0
us.add_ugt((q + 1).get_univariate_coefficients(), rational::zero(), false, dep); us.add_ugt((q + 1).get_univariate_coefficients(), rational::zero(), false, p.power_of_2(), dep);
if (p_ok && q_ok) if (p_ok && q_ok)
us.add_ule(p.get_univariate_coefficients(), q.get_univariate_coefficients(), !is_positive, dep); us.add_ule(p.get_univariate_coefficients(), q.get_univariate_coefficients(), !is_positive, p.power_of_2(), dep);
} }
} }

2
src/math/polysat/umul_ovfl_constraint.cpp
View file

@ -198,6 +198,6 @@ namespace polysat {
pdd q1 = s.subst(q()); pdd q1 = s.subst(q());
if (!q1.is_univariate_in(v)) if (!q1.is_univariate_in(v))
return; return;
us.add_umul_ovfl(p1.get_univariate_coefficients(), q1.get_univariate_coefficients(), !is_positive, dep); us.add_umul_ovfl(p1.get_univariate_coefficients(), q1.get_univariate_coefficients(), !is_positive, p1.power_of_2(), dep);
} }
} }

158
src/math/polysat/univariate/univariate_solver.cpp
View file

@ -97,28 +97,36 @@ namespace polysat {
scoped_ptr<bv_util> bv; scoped_ptr<bv_util> bv;
scoped_ptr<solver> s; scoped_ptr<solver> s;
unsigned m_scope_level = 0; unsigned m_scope_level = 0;
func_decl_ref x_decl; func_decl_ref m_x_decl;
expr_ref x; expr_ref m_x;
vector<rational> model_cache; vector<rational> model_cache;
public: public:
univariate_bitblast_solver(solver_factory& mk_solver, unsigned bit_width) : univariate_bitblast_solver(solver_factory& mk_solver, unsigned bit_width) :
univariate_solver(bit_width), univariate_solver(bit_width),
x_decl(m), m_x_decl(m),
x(m) { m_x(m) {
reg_decl_plugins(m); reg_decl_plugins(m);
bv = alloc(bv_util, m); bv = alloc(bv_util, m);
params_ref p; params_ref p;
p.set_bool("bv.polysat", false); p.set_bool("bv.polysat", false);
// p.set_bool("smt", true); // p.set_bool("smt", true);
s = mk_solver(m, p, false, true, true, symbol::null); s = mk_solver(m, p, false, true, true, symbol::null);
x_decl = m.mk_const_decl("x", bv->mk_sort(bit_width)); m_x_decl = m.mk_const_decl("x", bv->mk_sort(bit_width));
x = m.mk_const(x_decl); m_x = m.mk_const(m_x_decl);
model_cache.push_back(rational(-1)); model_cache.push_back(rational(-1));
} }
~univariate_bitblast_solver() override = default; ~univariate_bitblast_solver() override = default;
expr* x(unsigned num_bits) {
SASSERT(1 <= num_bits);
SASSERT(num_bits <= bit_width);
if (num_bits == bit_width)
return m_x;
return bv->mk_extract(num_bits - 1, 0, m_x);
}
void reset_cache() { void reset_cache() {
model_cache.back() = -1; model_cache.back() = -1;
} }
@ -149,12 +157,12 @@ namespace polysat {
return m_scope_level; return m_scope_level;
} }
expr* mk_numeral(rational const& r) const { expr* mk_numeral(rational const& r, unsigned num_bits) const {
return bv->mk_numeral(r, bit_width); return bv->mk_numeral(r, num_bits);
} }
expr* mk_numeral(uint64_t u) const { expr* mk_numeral(uint64_t u, unsigned num_bits) const {
return bv->mk_numeral(u, bit_width); return bv->mk_numeral(u, num_bits);
} }
rational get_offset(univariate const& p) const { rational get_offset(univariate const& p) const {
@ -195,41 +203,41 @@ namespace polysat {
#else #else
// 2^k*x --> x << k // 2^k*x --> x << k
// n*x --> n * x // n*x --> n * x
expr* mk_poly_term(rational const& coeff, expr* xpow) const { expr* mk_poly_term(rational const& coeff, expr* xpow, unsigned num_bits) const {
unsigned pow; unsigned pow;
SASSERT(!coeff.is_zero()); SASSERT(!coeff.is_zero());
if (coeff.is_one()) if (coeff.is_one())
return xpow; return xpow;
if (coeff.is_power_of_two(pow)) if (coeff.is_power_of_two(pow))
return bv->mk_bv_shl(xpow, mk_numeral(rational(pow))); return bv->mk_bv_shl(xpow, mk_numeral(rational(pow), num_bits));
return bv->mk_bv_mul(mk_numeral(coeff), xpow); return bv->mk_bv_mul(mk_numeral(coeff, num_bits), xpow);
} }
// [d,c,b,a] --> d + c*x + b*(x*x) + a*(x*x*x) // [d,c,b,a] --> d + c*x + b*(x*x) + a*(x*x*x)
expr_ref mk_poly(univariate const& p) { expr_ref mk_poly(univariate const& p, unsigned num_bits) {
expr_ref e(m); expr_ref e(m);
if (p.empty()) if (p.empty())
e = mk_numeral(rational::zero()); e = mk_numeral(rational::zero(), num_bits);
else { else {
if (!p[0].is_zero()) if (!p[0].is_zero())
e = mk_numeral(p[0]); e = mk_numeral(p[0], num_bits);
expr_ref xpow = x; expr_ref xpow{x(num_bits), m};
for (unsigned i = 1; i < p.size(); ++i) { for (unsigned i = 1; i < p.size(); ++i) {
if (!p[i].is_zero()) { if (!p[i].is_zero()) {
expr* t = mk_poly_term(p[i], xpow); expr* t = mk_poly_term(p[i], xpow, num_bits);
e = e ? bv->mk_bv_add(e, t) : t; e = e ? bv->mk_bv_add(e, t) : t;
} }
if (i + 1 < p.size()) if (i + 1 < p.size())
xpow = bv->mk_bv_mul(xpow, x); xpow = bv->mk_bv_mul(xpow, x(num_bits));
} }
if (!e) if (!e)
e = mk_numeral(p[0]); e = mk_numeral(p[0], num_bits);
} }
return e; return e;
} }
expr_ref mk_poly(rational const& p) { expr_ref mk_poly(rational const& p, unsigned num_bits) {
return {mk_numeral(p), m}; return {mk_numeral(p, num_bits), m};
} }
#endif #endif
@ -249,104 +257,100 @@ namespace polysat {
} }
template <typename lhs_t, typename rhs_t> template <typename lhs_t, typename rhs_t>
void add_ule_impl(lhs_t const& lhs, rhs_t const& rhs, bool sign, dep_t dep) { void add_ule_impl(lhs_t const& lhs, rhs_t const& rhs, bool sign, unsigned num_bits, dep_t dep) {
if (is_zero(rhs)) if (is_zero(rhs))
add(m.mk_eq(mk_poly(lhs), mk_poly(rhs)), sign, dep); add(m.mk_eq(mk_poly(lhs, num_bits), mk_poly(rhs, num_bits)), sign, dep);
else else
add(bv->mk_ule(mk_poly(lhs), mk_poly(rhs)), sign, dep); add(bv->mk_ule(mk_poly(lhs, num_bits), mk_poly(rhs, num_bits)), sign, dep);
} }
void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override { add_ule_impl(lhs, rhs, sign, dep); } void add_ule(univariate const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) override { add_ule_impl(lhs, rhs, sign, num_bits, dep); }
void add_ule(univariate const& lhs, rational const& rhs, bool sign, dep_t dep) override { add_ule_impl(lhs, rhs, sign, dep); } void add_ule(univariate const& lhs, rational const& rhs, bool sign, unsigned num_bits, dep_t dep) override { add_ule_impl(lhs, rhs, sign, num_bits, dep); }
void add_ule(rational const& lhs, univariate const& rhs, bool sign, dep_t dep) override { add_ule_impl(lhs, rhs, sign, dep); } void add_ule(rational const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) override { add_ule_impl(lhs, rhs, sign, num_bits, dep); }
void add_umul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override { void add_umul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) override {
add(bv->mk_bvumul_no_ovfl(mk_poly(lhs), mk_poly(rhs)), !sign, dep); add(bv->mk_bvumul_no_ovfl(mk_poly(lhs, num_bits), mk_poly(rhs, num_bits)), !sign, dep);
} }
void add_smul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override { void add_smul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) override {
add(bv->mk_bvsmul_no_ovfl(mk_poly(lhs), mk_poly(rhs)), !sign, dep); add(bv->mk_bvsmul_no_ovfl(mk_poly(lhs, num_bits), mk_poly(rhs, num_bits)), !sign, dep);
} }
void add_smul_udfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override { void add_smul_udfl(univariate const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) override {
add(bv->mk_bvsmul_no_udfl(mk_poly(lhs), mk_poly(rhs)), !sign, dep); add(bv->mk_bvsmul_no_udfl(mk_poly(lhs, num_bits), mk_poly(rhs, num_bits)), !sign, dep);
} }
void add_lshr(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override { void add_lshr(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_lshr(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep); add(m.mk_eq(bv->mk_bv_lshr(mk_poly(in1, num_bits), mk_poly(in2, num_bits)), mk_poly(out, num_bits)), sign, dep);
} }
void add_ashr(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override { void add_ashr(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_ashr(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep); add(m.mk_eq(bv->mk_bv_ashr(mk_poly(in1, num_bits), mk_poly(in2, num_bits)), mk_poly(out, num_bits)), sign, dep);
} }
void add_shl(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override { void add_shl(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_shl(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep); add(m.mk_eq(bv->mk_bv_shl(mk_poly(in1, num_bits), mk_poly(in2, num_bits)), mk_poly(out, num_bits)), sign, dep);
} }
void add_and(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override { void add_and(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_and(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep); add(m.mk_eq(bv->mk_bv_and(mk_poly(in1, num_bits), mk_poly(in2, num_bits)), mk_poly(out, num_bits)), sign, dep);
} }
void add_or(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override { void add_or(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_or(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep); add(m.mk_eq(bv->mk_bv_or(mk_poly(in1, num_bits), mk_poly(in2, num_bits)), mk_poly(out, num_bits)), sign, dep);
} }
void add_xor(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override { void add_xor(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_xor(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep); add(m.mk_eq(bv->mk_bv_xor(mk_poly(in1, num_bits), mk_poly(in2, num_bits)), mk_poly(out, num_bits)), sign, dep);
} }
void add_not(univariate const& in, univariate const& out, bool sign, dep_t dep) override { void add_not(univariate const& in, univariate const& out, bool sign, unsigned num_bits, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_not(mk_poly(in)), mk_poly(out)), sign, dep); add(m.mk_eq(bv->mk_bv_not(mk_poly(in, num_bits)), mk_poly(out, num_bits)), sign, dep);
} }
void add_inv(univariate const& in, univariate const& out, bool sign, dep_t dep) override { void add_inv(univariate const& in, univariate const& out, bool sign, unsigned num_bits, dep_t dep) override {
// out == smallest_pseudo_inverse(in) // out == smallest_pseudo_inverse(in)
expr_ref v = mk_poly(in); expr_ref v = mk_poly(in, num_bits);
expr_ref v_inv = mk_poly(out); expr_ref v_inv = mk_poly(out, num_bits);
expr_ref parity = mk_parity(v, in); expr_ref parity = mk_parity(v, in, num_bits);
// 2^parity = v * v_inv // 2^parity = v * v_inv
add(m.mk_eq(bv->mk_bv_shl(mk_numeral(1), parity), bv->mk_bv_mul(v, v_inv)), false, dep); add(m.mk_eq(bv->mk_bv_shl(mk_numeral(1, num_bits), parity), bv->mk_bv_mul(v, v_inv)), false, dep);
// v_inv <= 2^(N - parity) - 1 // v_inv <= 2^(N - parity) - 1
expr* v_inv_max = bv->mk_bv_sub(bv->mk_bv_shl(mk_numeral(1), bv->mk_bv_sub(mk_numeral(bit_width), parity)), mk_numeral(1)); expr* v_inv_max = bv->mk_bv_sub(bv->mk_bv_shl(mk_numeral(1, num_bits), bv->mk_bv_sub(mk_numeral(num_bits, num_bits), parity)), mk_numeral(1, num_bits));
add(bv->mk_ule(v_inv, v_inv_max), false, dep); 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 { void add_udiv(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_udiv(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep); add(m.mk_eq(bv->mk_bv_udiv(mk_poly(in1, num_bits), mk_poly(in2, num_bits)), mk_poly(out, num_bits)), sign, dep);
} }
void add_urem(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override { void add_urem(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_urem(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep); add(m.mk_eq(bv->mk_bv_urem(mk_poly(in1, num_bits), mk_poly(in2, num_bits)), mk_poly(out, num_bits)), sign, dep);
} }
void add_ule_const(rational const& val, bool sign, dep_t dep) override { void add_ule_const(rational const& val, bool sign, unsigned num_bits, dep_t dep) override {
if (val == 0) if (val == 0)
add(m.mk_eq(x, mk_poly(val)), sign, dep); add(m.mk_eq(x(num_bits), mk_poly(val, num_bits)), sign, dep);
else else
add(bv->mk_ule(x, mk_poly(val)), sign, dep); add(bv->mk_ule(x(num_bits), mk_poly(val, num_bits)), sign, dep);
} }
void add_uge_const(rational const& val, bool sign, dep_t dep) override { void add_uge_const(rational const& val, bool sign, unsigned num_bits, dep_t dep) override {
add(bv->mk_ule(mk_poly(val), x), sign, dep); add(bv->mk_ule(mk_poly(val, num_bits), x(num_bits)), sign, dep);
} }
void add_bit(unsigned idx, bool sign, dep_t dep) override { void add_bit(unsigned idx, bool sign, dep_t dep) override {
add(bv->mk_bit2bool(x, idx), sign, dep); add(bv->mk_bit2bool(x(bit_width), idx), sign, dep);
} }
uint64_t get_parity(rational const& r) const { expr_ref mk_parity(expr* v, univariate const& v_coeff, unsigned num_bits) {
return r.is_zero() ? bit_width : r.trailing_zeros();
}
expr_ref mk_parity(expr* v, univariate const& v_coeff) {
expr_ref parity(m); expr_ref parity(m);
if (is_constant(v_coeff)) { if (is_constant(v_coeff)) {
parity = mk_numeral(get_parity(get_offset(v_coeff))); parity = mk_numeral(get_offset(v_coeff).parity(num_bits), num_bits);
return parity; return parity;
} }
parity = m.mk_fresh_const("parity", bv->mk_sort(bit_width), false); parity = m.mk_fresh_const("parity", bv->mk_sort(num_bits), false);
expr* parity_1 = bv->mk_bv_add(parity, mk_numeral(1)); expr* parity_1 = bv->mk_bv_add(parity, mk_numeral(1, num_bits));
// if v = 0 // if v = 0
// then parity = N // then parity = N
// else v = (v >> parity) << parity // else v = (v >> parity) << parity
@ -354,8 +358,8 @@ namespace polysat {
// TODO: what about: v[k:] = 0 && v[k+1:] != 0 ==> parity = k for each k? // TODO: what about: v[k:] = 0 && v[k+1:] != 0 ==> parity = k for each k?
// TODO: helper axioms like parity <= N etc.? // TODO: helper axioms like parity <= N etc.?
add(m.mk_ite( add(m.mk_ite(
m.mk_eq(v, mk_numeral(0)), m.mk_eq(v, mk_numeral(0, num_bits)),
m.mk_eq(parity, mk_numeral(bit_width)), m.mk_eq(parity, mk_numeral(num_bits, num_bits)),
m.mk_and( m.mk_and(
m.mk_eq(bv->mk_bv_shl(bv->mk_bv_lshr(v, parity), parity), v), m.mk_eq(bv->mk_bv_shl(bv->mk_bv_lshr(v, parity), parity), v),
m.mk_not(m.mk_eq(bv->mk_bv_shl(bv->mk_bv_lshr(v, parity_1), parity_1), v)) m.mk_not(m.mk_eq(bv->mk_bv_shl(bv->mk_bv_lshr(v, parity_1), parity_1), v))
@ -386,7 +390,7 @@ namespace polysat {
model_ref model; model_ref model;
s->get_model(model); s->get_model(model);
SASSERT(model); SASSERT(model);
app* val = to_app(model->get_const_interp(x_decl)); app* val = to_app(model->get_const_interp(m_x_decl));
unsigned sz; unsigned sz;
VERIFY(bv->is_numeral(val, cached_model, sz)); VERIFY(bv->is_numeral(val, cached_model, sz));
} }
@ -399,7 +403,7 @@ namespace polysat {
out1 = model(); out1 = model();
bool ok = true; bool ok = true;
push(); push();
add(m.mk_eq(mk_numeral(out1), x), true, null_dep); add(m.mk_eq(mk_numeral(out1, bit_width), x(bit_width)), true, null_dep);
switch (check()) { switch (check()) {
case l_true: case l_true:
out2 = model(); out2 = model();
@ -422,6 +426,7 @@ namespace polysat {
} }
}; };
#if 0
// stub for alternative int-blast solver. // stub for alternative int-blast solver.
class univariate_intblast_solver : public univariate_solver { class univariate_intblast_solver : public univariate_solver {
ast_manager m; ast_manager m;
@ -697,6 +702,7 @@ namespace polysat {
return out << *s; return out << *s;
} }
}; };
#endif
class univariate_bitblast_factory : public univariate_solver_factory { class univariate_bitblast_factory : public univariate_solver_factory {
symbol m_logic; symbol m_logic;

58
src/math/polysat/univariate/univariate_solver.h
View file

@ -82,42 +82,42 @@ namespace polysat {
virtual bool find_two(rational& out1, rational& out2) = 0; virtual bool find_two(rational& out1, rational& out2) = 0;
/** lhs <= rhs */ /** lhs <= rhs */
virtual void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; virtual void add_ule(univariate const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) = 0;
virtual void add_ule(univariate const& lhs, rational const& rhs, bool sign, dep_t dep) = 0; virtual void add_ule(univariate const& lhs, rational const& rhs, bool sign, unsigned num_bits, dep_t dep) = 0;
virtual void add_ule(rational const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; virtual void add_ule(rational const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) = 0;
/** lhs >= rhs */ /** lhs >= rhs */
void add_uge(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, sign, dep); } void add_uge(univariate const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) { add_ule(rhs, lhs, sign, num_bits, dep); }
void add_uge(univariate const& lhs, rational const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, sign, dep); } void add_uge(univariate const& lhs, rational const& rhs, bool sign, unsigned num_bits, dep_t dep) { add_ule(rhs, lhs, sign, num_bits, dep); }
void add_uge(rational const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, sign, dep); } void add_uge(rational const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) { add_ule(rhs, lhs, sign, num_bits, dep); }
/** lhs < rhs */ /** lhs < rhs */
void add_ult(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, !sign, dep); } void add_ult(univariate const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) { add_ule(rhs, lhs, !sign, num_bits, dep); }
void add_ult(univariate const& lhs, rational const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, !sign, dep); } void add_ult(univariate const& lhs, rational const& rhs, bool sign, unsigned num_bits, dep_t dep) { add_ule(rhs, lhs, !sign, num_bits, dep); }
void add_ult(rational const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, !sign, dep); } void add_ult(rational const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) { add_ule(rhs, lhs, !sign, num_bits, dep); }
/** lhs > rhs */ /** lhs > rhs */
void add_ugt(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(lhs, rhs, !sign, dep); } void add_ugt(univariate const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) { add_ule(lhs, rhs, !sign, num_bits, dep); }
void add_ugt(univariate const& lhs, rational const& rhs, bool sign, dep_t dep) { add_ule(lhs, rhs, !sign, dep); } void add_ugt(univariate const& lhs, rational const& rhs, bool sign, unsigned num_bits, dep_t dep) { add_ule(lhs, rhs, !sign, num_bits, dep); }
void add_ugt(rational const& lhs, univariate const& rhs, bool sign, dep_t dep) { add_ule(lhs, rhs, !sign, dep); } void add_ugt(rational const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) { add_ule(lhs, rhs, !sign, num_bits, dep); }
virtual void add_umul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; virtual void add_umul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) = 0;
virtual void add_smul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; virtual void add_smul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) = 0;
virtual void add_smul_udfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; virtual void add_smul_udfl(univariate const& lhs, univariate const& rhs, bool sign, unsigned num_bits, dep_t dep) = 0;
virtual void add_lshr(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0; virtual void add_lshr(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) = 0;
virtual void add_ashr(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0; virtual void add_ashr(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) = 0;
virtual void add_shl(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0; virtual void add_shl(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) = 0;
virtual void add_and(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0; virtual void add_and(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) = 0;
virtual void add_or(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0; virtual void add_or(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) = 0;
virtual void add_xor(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0; virtual void add_xor(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) = 0;
virtual void add_not(univariate const& in, univariate const& out, bool sign, dep_t dep) = 0; virtual void add_not(univariate const& in, univariate const& out, bool sign, unsigned num_bits, dep_t dep) = 0;
virtual void add_inv(univariate const& in, univariate const& out, bool sign, dep_t dep) = 0; virtual void add_inv(univariate const& in, univariate const& out, bool sign, unsigned num_bits, 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_udiv(univariate const& in1, univariate const& in2, univariate const& out, bool sign, unsigned num_bits, dep_t dep) = 0;
virtual void add_urem(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, unsigned num_bits, dep_t dep) = 0;
/// Add x <= val or x > val, depending on sign /// Add x <= val or x > val, depending on sign
virtual void add_ule_const(rational const& val, bool sign, dep_t dep) = 0; virtual void add_ule_const(rational const& val, bool sign, unsigned num_bits, dep_t dep) = 0;
/// Add x >= val or x < val, depending on sign /// Add x >= val or x < val, depending on sign
virtual void add_uge_const(rational const& val, bool sign, dep_t dep) = 0; virtual void add_uge_const(rational const& val, bool sign, unsigned num_bits, dep_t dep) = 0;
void add_ugt_const(rational const& val, bool sign, dep_t dep) { add_ule_const(val, !sign, dep); } void add_ugt_const(rational const& val, bool sign, unsigned num_bits, dep_t dep) { add_ule_const(val, !sign, num_bits, dep); }
void add_ult_const(rational const& val, bool sign, dep_t dep) { add_uge_const(val, !sign, dep); } void add_ult_const(rational const& val, bool sign, unsigned num_bits, dep_t dep) { add_uge_const(val, !sign, num_bits, dep); }
/// Assert i-th bit of x /// Assert i-th bit of x
virtual void add_bit(unsigned idx, bool sign, dep_t dep) = 0; virtual void add_bit(unsigned idx, bool sign, dep_t dep) = 0;