diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index 84021548e..8e96e0490 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -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 { + unsigned const N = p().power_of_2(); pdd pv = s.subst(p()); if (!pv.is_univariate_in(v)) return; @@ -731,22 +732,22 @@ namespace polysat { return; switch (m_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; 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; 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; 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; 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; 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; default: NOT_IMPLEMENTED_YET(); diff --git a/src/math/polysat/smul_fl_constraint.cpp b/src/math/polysat/smul_fl_constraint.cpp index 92cbb5f63..bdd60b414 100644 --- a/src/math/polysat/smul_fl_constraint.cpp +++ b/src/math/polysat/smul_fl_constraint.cpp @@ -127,9 +127,9 @@ namespace polysat { if (!q1.is_univariate_in(v)) return; 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 - 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); } } diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index e87c75898..eeb180abe 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -391,10 +391,10 @@ namespace polysat { bool q_ok = q.is_univariate_in(v); IF_VERBOSE(10, display(verbose_stream() << ";; ", to_lbool(is_positive), p, q) << "\n"); 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 - 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) - 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); } } diff --git a/src/math/polysat/umul_ovfl_constraint.cpp b/src/math/polysat/umul_ovfl_constraint.cpp index 5a02b3b31..833769a0e 100644 --- a/src/math/polysat/umul_ovfl_constraint.cpp +++ b/src/math/polysat/umul_ovfl_constraint.cpp @@ -198,6 +198,6 @@ namespace polysat { pdd q1 = s.subst(q()); if (!q1.is_univariate_in(v)) 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); } } diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp index fd0f214ca..ae4cbedf5 100644 --- a/src/math/polysat/univariate/univariate_solver.cpp +++ b/src/math/polysat/univariate/univariate_solver.cpp @@ -97,28 +97,36 @@ namespace polysat { scoped_ptr bv; scoped_ptr s; unsigned m_scope_level = 0; - func_decl_ref x_decl; - expr_ref x; + func_decl_ref m_x_decl; + expr_ref m_x; vector model_cache; public: univariate_bitblast_solver(solver_factory& mk_solver, unsigned bit_width) : univariate_solver(bit_width), - x_decl(m), - x(m) { + m_x_decl(m), + m_x(m) { reg_decl_plugins(m); bv = alloc(bv_util, m); params_ref p; p.set_bool("bv.polysat", false); // p.set_bool("smt", true); s = mk_solver(m, p, false, true, true, symbol::null); - x_decl = m.mk_const_decl("x", bv->mk_sort(bit_width)); - x = m.mk_const(x_decl); + m_x_decl = m.mk_const_decl("x", bv->mk_sort(bit_width)); + m_x = m.mk_const(m_x_decl); model_cache.push_back(rational(-1)); } ~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() { model_cache.back() = -1; } @@ -149,12 +157,12 @@ namespace polysat { return m_scope_level; } - expr* mk_numeral(rational const& r) const { - return bv->mk_numeral(r, bit_width); + expr* mk_numeral(rational const& r, unsigned num_bits) const { + return bv->mk_numeral(r, num_bits); } - expr* mk_numeral(uint64_t u) const { - return bv->mk_numeral(u, bit_width); + expr* mk_numeral(uint64_t u, unsigned num_bits) const { + return bv->mk_numeral(u, num_bits); } rational get_offset(univariate const& p) const { @@ -195,41 +203,41 @@ namespace polysat { #else // 2^k*x --> x << k // 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; SASSERT(!coeff.is_zero()); if (coeff.is_one()) return xpow; if (coeff.is_power_of_two(pow)) - return bv->mk_bv_shl(xpow, mk_numeral(rational(pow))); - return bv->mk_bv_mul(mk_numeral(coeff), xpow); + return bv->mk_bv_shl(xpow, mk_numeral(rational(pow), num_bits)); + 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) - expr_ref mk_poly(univariate const& p) { + expr_ref mk_poly(univariate const& p, unsigned num_bits) { expr_ref e(m); if (p.empty()) - e = mk_numeral(rational::zero()); + e = mk_numeral(rational::zero(), num_bits); else { if (!p[0].is_zero()) - e = mk_numeral(p[0]); - expr_ref xpow = x; + e = mk_numeral(p[0], num_bits); + expr_ref xpow{x(num_bits), m}; for (unsigned i = 1; i < p.size(); ++i) { 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; } if (i + 1 < p.size()) - xpow = bv->mk_bv_mul(xpow, x); + xpow = bv->mk_bv_mul(xpow, x(num_bits)); } if (!e) - e = mk_numeral(p[0]); + e = mk_numeral(p[0], num_bits); } return e; } - expr_ref mk_poly(rational const& p) { - return {mk_numeral(p), m}; + expr_ref mk_poly(rational const& p, unsigned num_bits) { + return {mk_numeral(p, num_bits), m}; } #endif @@ -249,104 +257,100 @@ namespace polysat { } template - 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)) - 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 - 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, rational 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, 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, 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, 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 { - add(bv->mk_bvumul_no_ovfl(mk_poly(lhs), mk_poly(rhs)), !sign, dep); + 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, 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 { - add(bv->mk_bvsmul_no_ovfl(mk_poly(lhs), mk_poly(rhs)), !sign, dep); + 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, 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 { - add(bv->mk_bvsmul_no_udfl(mk_poly(lhs), mk_poly(rhs)), !sign, dep); + 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, 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 { - add(m.mk_eq(bv->mk_bv_lshr(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep); + 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, 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 { - add(m.mk_eq(bv->mk_bv_ashr(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep); + 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, 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 { - add(m.mk_eq(bv->mk_bv_shl(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep); + 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, 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 { - add(m.mk_eq(bv->mk_bv_and(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep); + 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, 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 { - add(m.mk_eq(bv->mk_bv_or(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep); + 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, 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 { - add(m.mk_eq(bv->mk_bv_xor(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep); + 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, 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 { - add(m.mk_eq(bv->mk_bv_not(mk_poly(in)), mk_poly(out)), sign, dep); + 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, 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) - expr_ref v = mk_poly(in); - expr_ref v_inv = mk_poly(out); - expr_ref parity = mk_parity(v, in); + expr_ref v = mk_poly(in, num_bits); + expr_ref v_inv = mk_poly(out, num_bits); + expr_ref parity = mk_parity(v, in, num_bits); // 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 - 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); } - 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_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, 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 { - add(m.mk_eq(bv->mk_bv_urem(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, unsigned num_bits, dep_t dep) override { + 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) - 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 - 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 { - add(bv->mk_ule(mk_poly(val), x), sign, dep); + void add_uge_const(rational const& val, bool sign, unsigned num_bits, dep_t dep) override { + 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 { - 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 { - return r.is_zero() ? bit_width : r.trailing_zeros(); - } - - expr_ref mk_parity(expr* v, univariate const& v_coeff) { + expr_ref mk_parity(expr* v, univariate const& v_coeff, unsigned num_bits) { expr_ref parity(m); 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; } - parity = m.mk_fresh_const("parity", bv->mk_sort(bit_width), false); - expr* parity_1 = bv->mk_bv_add(parity, mk_numeral(1)); + parity = m.mk_fresh_const("parity", bv->mk_sort(num_bits), false); + expr* parity_1 = bv->mk_bv_add(parity, mk_numeral(1, num_bits)); // if v = 0 // then parity = N // 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: helper axioms like parity <= N etc.? add(m.mk_ite( - m.mk_eq(v, mk_numeral(0)), - m.mk_eq(parity, mk_numeral(bit_width)), + m.mk_eq(v, mk_numeral(0, num_bits)), + m.mk_eq(parity, mk_numeral(num_bits, num_bits)), m.mk_and( 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)) @@ -386,7 +390,7 @@ namespace polysat { model_ref model; s->get_model(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; VERIFY(bv->is_numeral(val, cached_model, sz)); } @@ -399,7 +403,7 @@ namespace polysat { out1 = model(); bool ok = true; 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()) { case l_true: out2 = model(); @@ -422,6 +426,7 @@ namespace polysat { } }; +#if 0 // stub for alternative int-blast solver. class univariate_intblast_solver : public univariate_solver { ast_manager m; @@ -697,6 +702,7 @@ namespace polysat { return out << *s; } }; +#endif class univariate_bitblast_factory : public univariate_solver_factory { symbol m_logic; diff --git a/src/math/polysat/univariate/univariate_solver.h b/src/math/polysat/univariate/univariate_solver.h index ad7840a4e..53ebac2cf 100644 --- a/src/math/polysat/univariate/univariate_solver.h +++ b/src/math/polysat/univariate/univariate_solver.h @@ -82,42 +82,42 @@ namespace polysat { virtual bool find_two(rational& out1, rational& out2) = 0; /** 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, rational const& rhs, bool sign, dep_t dep) = 0; - virtual void add_ule(rational 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, unsigned num_bits, 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 */ - 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, rational const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, sign, dep); } - void add_uge(rational 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, 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, unsigned num_bits, dep_t dep) { add_ule(rhs, lhs, sign, num_bits, dep); } /** 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, rational const& rhs, bool sign, dep_t dep) { add_ule(rhs, lhs, !sign, dep); } - void add_ult(rational 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, 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, unsigned num_bits, dep_t dep) { add_ule(rhs, lhs, !sign, num_bits, dep); } /** 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, rational const& rhs, bool sign, dep_t dep) { add_ule(lhs, rhs, !sign, dep); } - void add_ugt(rational 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, 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, 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_smul_ovfl(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, 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_ashr(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, 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_or(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, 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; + 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, unsigned num_bits, 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, unsigned num_bits, 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, unsigned num_bits, 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, unsigned num_bits, 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, unsigned num_bits, 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, unsigned num_bits, 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 - 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 - virtual void add_uge_const(rational const& val, bool sign, dep_t dep) = 0; - void add_ugt_const(rational const& val, bool sign, dep_t dep) { add_ule_const(val, !sign, dep); } - void add_ult_const(rational const& val, bool sign, dep_t dep) { add_uge_const(val, !sign, dep); } + 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, unsigned num_bits, dep_t dep) { add_ule_const(val, !sign, num_bits, 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 virtual void add_bit(unsigned idx, bool sign, dep_t dep) = 0;