diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp index cdd4d802d..124257e99 100644 --- a/src/math/polysat/constraint_manager.cpp +++ b/src/math/polysat/constraint_manager.cpp @@ -643,19 +643,43 @@ namespace polysat { pdd constraint_manager::zero_ext(pdd const& p, unsigned bit_width) { SASSERT(bit_width > p.power_of_2()); pdd const q = s.var(s.m_names.mk_name(p)); - constraint_dedup::zext_args args = {q.var(), bit_width}; - auto it = m_dedup.m_zext_expr.find_iterator(args); - if (it != m_dedup.m_zext_expr.end()) + constraint_dedup::bv_ext_args const args = {false, q.var(), bit_width}; + auto const it = m_dedup.m_bv_ext_expr.find_iterator(args); + if (it != m_dedup.m_bv_ext_expr.end()) return s.var(it->m_value); pdd const v = s.var(s.add_var(bit_width)); - m_dedup.m_zext_expr.insert(args, v.var()); - // v[|p|-1:0] = p + m_dedup.m_bv_ext_expr.insert(args, v.var()); + // (1) v[|p|-1:0] = p s.add_eq(q, extract(v, p.power_of_2() - 1, 0)); - // v < 2^|p| + // (2) v < 2^|p| s.add_ule(q, p.manager().max_value()); return v; } + pdd constraint_manager::sign_ext(pdd const& p, unsigned bit_width) { + unsigned const p_sz = p. power_of_2(); + SASSERT(bit_width > p_sz); + pdd const q = s.var(s.m_names.mk_name(p)); + constraint_dedup::bv_ext_args const args = {true, q.var(), bit_width}; + auto const it = m_dedup.m_bv_ext_expr.find_iterator(args); + if (it != m_dedup.m_bv_ext_expr.end()) + return s.var(it->m_value); + pdd const v = s.var(s.add_var(bit_width)); + m_dedup.m_bv_ext_expr.insert(args, v.var()); + // (1) v[|p|-1:0] = p + s.add_eq(q, extract(v, p_sz - 1, 0)); + // (2) Let h := v[bit_width-1:|p|] + pdd const h = extract(v, bit_width - 1, p_sz); + signed_constraint p_negative = s.uge(p, rational::power_of_two(p_sz - 1)); + // (3) p < 2^(|p|-1) ==> h = 0 + s.add_clause(p_negative, s.eq(h), false); + // (4) p >= 2^(|p|-1) ==> h = max_value + s.add_clause(~p_negative, s.eq(h, h.manager().max_value()), false); + // (5) h + 1 <= 1 (i.e., h = b000...0 or h = b111...1) ... implied by (3), (4); maybe better to just exclude h from decisions as it is basically a defined variable + s.add_ule(h + 1, 1); + return v; + } + /** unsigned quotient/remainder */ std::pair constraint_manager::div_rem_op_constraint(pdd const& a, pdd const& b) { auto& m = a.manager(); diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h index dd189aebd..0ba7987ca 100644 --- a/src/math/polysat/constraint_manager.h +++ b/src/math/polysat/constraint_manager.h @@ -42,15 +42,16 @@ namespace polysat { quot_rem_expr_map m_quot_rem_expr; vector> m_div_rem_list; - using zext_args = std::pair; - using zext_args_eq = default_eq; - struct zext_args_hash { - unsigned operator()(zext_args const& args) const { - return combine_hash(args.first, args.second); + // zero_ext or sign_ext + using bv_ext_args = std::tuple; + using bv_ext_args_eq = default_eq; + struct bv_ext_args_hash { + unsigned operator()(bv_ext_args const& args) const { + return mk_mix(std::get<0>(args), std::get<1>(args), std::get<2>(args)); } }; - using zext_expr_map = map; - zext_expr_map m_zext_expr; + using bv_ext_expr_map = map; + bv_ext_expr_map m_bv_ext_expr; }; // Manage constraint lifetime, deduplication, and connection to boolean variables/literals. @@ -172,6 +173,7 @@ namespace polysat { pdd concat(unsigned num_args, pdd const* args); pdd zero_ext(pdd const& p, unsigned bit_width); + pdd sign_ext(pdd const& p, unsigned bit_width); constraint* const* begin() const { return m_constraints.data(); } constraint* const* end() const { return m_constraints.data() + m_constraints.size(); } diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 043f68811..7dce13f19 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -421,6 +421,9 @@ namespace polysat { /** Create expression for zero-extension of p */ pdd zero_ext(pdd const& p, unsigned bit_width) { return m_constraints.zero_ext(p, bit_width); } + /** Create expression for signed-extension of p */ + pdd sign_ext(pdd const& p, unsigned bit_width) { return m_constraints.sign_ext(p, bit_width); } + /** * Create terms for unsigned quot-rem * diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp index a76bfcddf..40d5bf0f3 100644 --- a/src/sat/smt/bv_polysat.cpp +++ b/src/sat/smt/bv_polysat.cpp @@ -93,8 +93,8 @@ namespace bv { case OP_EXTRACT: polysat_extract(a); break; case OP_CONCAT: polysat_concat(a); break; - case OP_ZERO_EXT: polysat_zero_ext(a); break; - case OP_SIGN_EXT: + case OP_ZERO_EXT: polysat_par_unary(a, [&](pdd const& p, unsigned sz) { return m_polysat.zero_ext(p, sz); }); break; + case OP_SIGN_EXT: polysat_par_unary(a, [&](pdd const& p, unsigned sz) { return m_polysat.sign_ext(p, sz); }); break; // polysat::solver should also support at least: case OP_BREDAND: // x == 2^K - 1 @@ -197,11 +197,10 @@ namespace bv { polysat_set(e, p); } - void solver::polysat_zero_ext(app* e) { - pdd const arg = expr2pdd(e->get_arg(0)); + void solver::polysat_par_unary(app* e, std::function const& fn) { + pdd const p = expr2pdd(e->get_arg(0)); unsigned const sz = e->get_parameter(0).get_int(); - pdd const p = m_polysat.zero_ext(p, sz); - polysat_set(e, p); + polysat_set(e, fn(p, sz)); } void solver::polysat_binary(app* e, std::function const& fn) { diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index e4d237ef9..96b29cef5 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -325,9 +325,9 @@ namespace bv { void polysat_pop(unsigned n); void polysat_unary(app* e, std::function const& fn); void polysat_binary(app* e, std::function const& fn); + void polysat_par_unary(app* e, std::function const& fn); void polysat_extract(app* e); void polysat_concat(app* e); - void polysat_zero_ext(app* e); polysat::pdd expr2pdd(expr* e); void polysat_set(euf::theory_var v, polysat::pdd const& p); polysat::pdd var2pdd(euf::theory_var v);