diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index 2c373f6b9..6877b328f 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -788,6 +788,32 @@ namespace intblast { r = a.mk_lt(mul(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(bv_size(bv_expr))); break; } + case OP_BSMUL_NO_OVFL: { + bv_expr = e->get_arg(0); + expr* x = umod(bv_expr, 0), *y = umod(bv_expr, 1); + rational N = bv_size(bv_expr); + expr* lim = a.mk_int(N/2); + expr* signx = a.mk_ge(x, lim); + expr* signy = a.mk_ge(y, lim); + x = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x); + y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y); + // signx != signy || x * y < N/2 + r = m.mk_or(m.mk_not(m.mk_eq(signx, signy)), a.mk_lt(a.mk_mul(x, y), lim)); + break; + } + case OP_BSMUL_NO_UDFL: { + bv_expr = e->get_arg(0); + expr* x = umod(bv_expr, 0), *y = umod(bv_expr, 1); + rational N = bv_size(bv_expr); + expr* lim = a.mk_int(N/2); + expr* signx = a.mk_ge(x, lim); + expr* signy = a.mk_ge(y, lim); + x = m.mk_ite(signx, a.mk_sub(a.mk_int(N), x), x); + y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y); + // signx == signy || x * y <= N/2 + r = m.mk_or(m.mk_eq(signx, signy), a.mk_le(a.mk_mul(x, y), lim)); + break; + } case OP_BSHL: { if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1))) r = a.mk_shl(bv.get_bv_size(e), arg(0),arg(1)); diff --git a/src/sat/smt/polysat/constraints.h b/src/sat/smt/polysat/constraints.h index 871b027c2..d089c9105 100644 --- a/src/sat/smt/polysat/constraints.h +++ b/src/sat/smt/polysat/constraints.h @@ -110,8 +110,6 @@ namespace polysat { signed_constraint ult(pdd const& p, pdd const& q) { return ~ule(q, p); } signed_constraint slt(pdd const& p, pdd const& q) { return ~sle(q, p); } signed_constraint umul_ovfl(pdd const& p, pdd const& q); - signed_constraint smul_ovfl(pdd const& p, pdd const& q) { throw default_exception("smul ovfl nyi"); } - signed_constraint smul_udfl(pdd const& p, pdd const& q) { throw default_exception("smult-udfl nyi"); } signed_constraint bit(pdd const& p, unsigned i); signed_constraint diseq(pdd const& p) { return ~eq(p); } diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index 50c98b8b9..4996fe33f 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -133,8 +133,6 @@ namespace polysat { signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); } signed_constraint sle(pdd const& p, pdd const& q) { return m_constraints.sle(p, q); } signed_constraint umul_ovfl(pdd const& p, pdd const& q) { return m_constraints.umul_ovfl(p, q); } - signed_constraint smul_ovfl(pdd const& p, pdd const& q) { return m_constraints.smul_ovfl(p, q); } - signed_constraint smul_udfl(pdd const& p, pdd const& q) { return m_constraints.smul_udfl(p, q); } signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); } diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index fa3860d3f..530ee3340 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -107,9 +107,9 @@ namespace polysat { case OP_SGT: internalize_le(a); break; case OP_BUMUL_NO_OVFL: internalize_binary_predicate(a, [&](pdd const& p, pdd const& q) { return ~m_core.umul_ovfl(p, q); }); break; - case OP_BSMUL_NO_OVFL: internalize_binary_predicate(a, [&](pdd const& p, pdd const& q) { return ~m_core.smul_ovfl(p, q); }); break; - case OP_BSMUL_NO_UDFL: internalize_binary_predicate(a, [&](pdd const& p, pdd const& q) { return ~m_core.smul_udfl(p, q); }); break; - + case OP_BSMUL_NO_OVFL: internalize_smul_no_ovfl(a); break; + case OP_BSMUL_NO_UDFL: internalize_smul_no_udfl(a); break; + case OP_BUMUL_OVFL: internalize_binary_predicate(a, [&](pdd const& p, pdd const& q) { return m_core.umul_ovfl(p, q); }); break; case OP_BSMUL_OVFL: case OP_BSDIV_OVFL: @@ -509,6 +509,60 @@ namespace polysat { m_var2pdd_valid.setx(v, false, false); quot_rem(quot, rem, x, y); } + + void solver::internalize_smul_no_ovfl(app* e) { + auto x = e->get_arg(0); + auto y = e->get_arg(1); + auto sz = bv.get_bv_size(x); + auto lit = mk_literal(e); + // x' = ite(signx, -x, x) + // y' = ite(signy, -y, y) + // lit <=> signx != signy || (not umul_ovfl(x',y') && x'*y' < 2^{N-1}) + // expands to: + // lit => signx != signy or not umul_ovfl(x',y') + // lit => signx != signy or not x'*y' < 2^{N-1} + // signx != signy => lit + // not umul_ovfl(x',y') & x'*y' < 2^{N-1} => lit + + auto signx = bv.mk_slt(x, bv.mk_zero(sz)); + auto signy = bv.mk_slt(y, bv.mk_zero(sz)); + auto same_sign = eq_internalize(signx, signy); + auto x1 = m.mk_ite(signx, bv.mk_bv_neg(x), x); + auto y1 = m.mk_ite(signy, bv.mk_bv_neg(y), y); + auto umul_noovfl = mk_literal(bv.mk_bvumul_no_ovfl(x1, y1)); + auto small = ~mk_literal(bv.mk_ule(bv.mk_numeral(rational::power_of_two(sz - 1), sz), bv.mk_bv_mul(x1, y1))); + add_axiom("smul_no_ovfl", { ~lit, ~same_sign, ~umul_noovfl }, false); + add_axiom("smul_no_ovfl", { ~lit, ~same_sign, small }, false); + add_axiom("smul_no_ovfl", { same_sign, lit }, false); + add_axiom("smul_no_ovfl", { umul_noovfl, ~small, lit }, false); + } + + void solver::internalize_smul_no_udfl(app* e) { + auto x = e->get_arg(0); + auto y = e->get_arg(1); + auto sz = bv.get_bv_size(x); + auto lit = mk_literal(e); + // x' = ite(signx, -x, x) + // y' = ite(signy, -y, y) + // lit <=> signx = signy || (not umul_ovfl(x',y') && x'*y' <= 2^{N-1}) + // expands to: + // lit => signx = signy or not umul_ovfl(x',y') + // lit => signx = signy or not x'*y' <= 2^{N-1} + // signx = signy => lit + // not umul_ovfl(x',y') & x'*y' <= 2^{N-1} => lit + + auto signx = bv.mk_slt(x, bv.mk_zero(sz)); + auto signy = bv.mk_slt(y, bv.mk_zero(sz)); + auto same_sign = eq_internalize(signx, signy); + auto x1 = m.mk_ite(signx, bv.mk_bv_neg(x), x); + auto y1 = m.mk_ite(signy, bv.mk_bv_neg(y), y); + auto umul_noovfl = mk_literal(bv.mk_bvumul_no_ovfl(x1, y1)); + auto small = mk_literal(bv.mk_ule(bv.mk_bv_mul(x1, y1), bv.mk_numeral(rational::power_of_two(sz - 1), sz))); + add_axiom("smul_no_udfl", { ~lit, same_sign, ~umul_noovfl }, false); + add_axiom("smul_no_udfl", { ~lit, same_sign, small }, false); + add_axiom("smul_no_udfl", { ~same_sign, lit }, false); + add_axiom("smul_no_udfl", { umul_noovfl, ~small, lit }, false); + } void solver::quot_rem(expr* quot, expr* rem, expr* x, expr* y) { pdd a = expr2pdd(x); diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index b64e8fb7c..c94918ff9 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -142,6 +142,8 @@ namespace polysat { void internalize_binary(app* e, std::function const& fn); void internalize_binary(app* e, std::function const& fn); void internalize_binary_predicate(app* e, std::function const& fn); + void internalize_smul_no_ovfl(app* e); + void internalize_smul_no_udfl(app* e); void internalize_par_unary(app* e, std::function const& fn); void internalize_novfl(app* n, std::function& fn); void internalize_interp(app* n, std::function& ibin, std::function& un);