From 17c480f8370bf91a0ae5315a210ae6c4c30c9238 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Dec 2023 14:51:21 -0800 Subject: [PATCH] adding band Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 14 + src/ast/arith_decl_plugin.h | 6 + src/sat/smt/arith_internalize.cpp | 5 + src/sat/smt/intblast_solver.cpp | 323 ++++++++++++--------- src/sat/smt/polysat/CMakeLists.txt | 1 + src/sat/smt/polysat/constraints.cpp | 31 +- src/sat/smt/polysat/constraints.h | 11 +- src/sat/smt/polysat/core.h | 8 +- src/sat/smt/polysat/ule_constraint.cpp | 18 -- src/sat/smt/polysat/ule_constraint.h | 2 - src/sat/smt/polysat/umul_ovfl_constraint.h | 2 - src/sat/smt/polysat_internalize.cpp | 8 +- 12 files changed, 246 insertions(+), 183 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index ba2b4b4a7..2d830d510 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -523,6 +523,12 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(), func_decl_info(m_family_id, k, num_parameters, parameters)); } + if (k == OP_ARITH_BAND) { + if (arity != 2 || domain[0] != m_int_decl || domain[1] != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) + m_manager->raise_exception("invalid bitwise and application. Expects integer parameter and two arguments of sort integer"); + return m_manager->mk_func_decl(symbol("band"), 2, domain, m_int_decl, + func_decl_info(m_family_id, k, num_parameters, parameters)); + } if (m_manager->int_real_coercions() && use_coercion(k)) { return mk_func_decl(fix_kind(k, arity), has_real_arg(arity, domain, m_real_decl)); @@ -548,6 +554,14 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return m_manager->mk_func_decl(symbol("divisible"), 1, &m_int_decl, m_manager->mk_bool_sort(), func_decl_info(m_family_id, k, num_parameters, parameters)); } + if (k == OP_ARITH_BAND) { + if (num_args != 2 || args[0]->get_sort() != m_int_decl || args[1]->get_sort() != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) + m_manager->raise_exception("invalid bitwise and application. Expects integer parameter and two arguments of sort integer"); + sort* domain[2] = { m_int_decl, m_int_decl }; + return m_manager->mk_func_decl(symbol("band"), 2, domain, m_int_decl, + func_decl_info(m_family_id, k, num_parameters, parameters)); + } + if (m_manager->int_real_coercions() && use_coercion(k)) { return mk_func_decl(fix_kind(k, num_args), has_real_arg(m_manager, num_args, args, m_real_decl)); } diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index fa359a9a7..a5ab60731 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -70,6 +70,8 @@ enum arith_op_kind { OP_ASINH, OP_ACOSH, OP_ATANH, + // Bit-vector functions + OP_ARITH_BAND, // constants OP_PI, OP_E, @@ -309,6 +311,8 @@ public: bool is_int_real(sort const * s) const { return s->get_family_id() == arith_family_id; } bool is_int_real(expr const * n) const { return is_int_real(n->get_sort()); } + bool is_band(expr const* n) const { return is_app_of(n, arith_family_id, OP_ARITH_BAND); } + bool is_sin(expr const* n) const { return is_app_of(n, arith_family_id, OP_SIN); } bool is_cos(expr const* n) const { return is_app_of(n, arith_family_id, OP_COS); } bool is_tan(expr const* n) const { return is_app_of(n, arith_family_id, OP_TAN); } @@ -471,6 +475,8 @@ public: app * mk_power(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER, arg1, arg2); } app * mk_power0(expr* arg1, expr* arg2) { return m_manager.mk_app(arith_family_id, OP_POWER0, arg1, arg2); } + app* mk_band(unsigned n, expr* arg1, expr* arg2) { parameter p(n); expr* args[2] = { arg1, arg2 }; return m_manager.mk_app(arith_family_id, OP_ARITH_BAND, 1, &p, 2, args); } + app * mk_sin(expr * arg) { return m_manager.mk_app(arith_family_id, OP_SIN, arg); } app * mk_cos(expr * arg) { return m_manager.mk_app(arith_family_id, OP_COS, arg); } app * mk_tan(expr * arg) { return m_manager.mk_app(arith_family_id, OP_TAN, arg); } diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index 3c6286317..66b25cb34 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -252,6 +252,11 @@ namespace arith { st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n2); } + else if (a.is_band(n)) { + // unsupported for now. + found_unsupported(n); + ensure_arg_vars(to_app(n)); + } else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n) && !a.is_power0(n)) { found_unsupported(n); ensure_arg_vars(to_app(n)); diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index a6fd38213..8bb3faa49 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -19,15 +19,15 @@ Author: namespace intblast { - solver::solver(euf::solver& ctx): - ctx(ctx), + solver::solver(euf::solver& ctx) : + ctx(ctx), s(ctx.s()), m(ctx.get_manager()), bv(m), a(m), m_trail(m) {} - + lbool solver::check() { sat::literal_vector literals; uint_set selected; @@ -76,7 +76,7 @@ namespace intblast { if (s.value(b) == l_true && s.value(a) == l_true && s.lvl(b) < s.lvl(a)) std::swap(a, b); selected.insert(a.index()); - literals.push_back(a); + literals.push_back(a); } m_core.reset(); @@ -98,9 +98,9 @@ namespace intblast { } IF_VERBOSE(10, verbose_stream() << "check\n"; - m_solver->display(verbose_stream()); - verbose_stream() << es << "\n"); - + m_solver->display(verbose_stream()); + verbose_stream() << es << "\n"); + lbool r = m_solver->check_sat(es); IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n"); @@ -116,14 +116,14 @@ namespace intblast { if (idx < literals.size()) m_core.push_back(literals[idx]); else - m_core.push_back(ctx.mk_literal(e)); + m_core.push_back(ctx.mk_literal(e)); } } return r; }; - bool solver::is_bv(sat::literal lit) { + bool solver::is_bv(sat::literal lit) { expr* e = ctx.bool_var2expr(lit.var()); if (!e) return false; @@ -185,9 +185,9 @@ namespace intblast { void solver::translate(expr_ref_vector& es) { ptr_vector todo; - obj_map translated; + obj_map translated; expr_ref_vector args(m); - + sorted_subterms(es, todo); for (expr* e : todo) { @@ -236,12 +236,12 @@ namespace intblast { if (m_vars.contains(x)) return x; return to_expr(a.mk_mod(x, a.mk_int(bv_size()))); - }; + }; auto mk_smod = [&](expr* x) { auto shift = bv_size() / 2; return a.mk_mod(a.mk_add(x, a.mk_int(shift)), a.mk_int(bv_size())); - }; + }; if (m.is_eq(e)) { bool has_bv_arg = any_of(*ap, [&](expr* arg) { return bv.is_bv(arg); }); @@ -256,7 +256,7 @@ namespace intblast { } continue; } - + if (m.is_ite(e)) { m_trail.push_back(m.mk_ite(args.get(0), args.get(1), args.get(2))); translated.insert(e, m_trail.back()); @@ -287,144 +287,179 @@ namespace intblast { } f = g; } - + m_trail.push_back(m.mk_app(f, args)); translated.insert(e, m_trail.back()); - if (has_bv_sort) + if (has_bv_sort) m_vars.insert(e, { m_trail.back(), bv_size() }); - + continue; } + auto bnot = [&](expr* e) { + return a.mk_sub(a.mk_int(-1), e); + }; + + auto band = [&](expr_ref_vector const& args) { + expr * r = args.get(0); + for (unsigned i = 1; i < args.size(); ++i) + r = a.mk_band(bv.get_bv_size(e), r, args.get(i)); + return r; + }; + switch (ap->get_decl_kind()) { - case OP_BADD: - m_trail.push_back(a.mk_add(args)); - break; - case OP_BSUB: - m_trail.push_back(a.mk_sub(args.size(), args.data())); - break; - case OP_BMUL: - m_trail.push_back(a.mk_mul(args)); - break; - case OP_ULEQ: - bv_expr = ap->get_arg(0); - m_trail.push_back(a.mk_le(mk_mod(args.get(0)), mk_mod(args.get(1)))); - break; - case OP_UGEQ: - bv_expr = ap->get_arg(0); - m_trail.push_back(a.mk_ge(mk_mod(args.get(0)), mk_mod(args.get(1)))); - break; - case OP_ULT: - bv_expr = ap->get_arg(0); - m_trail.push_back(a.mk_lt(mk_mod(args.get(0)), mk_mod(args.get(1)))); - break; - case OP_UGT: - bv_expr = ap->get_arg(0); - m_trail.push_back(a.mk_gt(mk_mod(args.get(0)), mk_mod(args.get(1)))); - break; - case OP_SLEQ: - bv_expr = ap->get_arg(0); - m_trail.push_back(a.mk_le(mk_smod(args.get(0)), mk_smod(args.get(1)))); - break; - case OP_SGEQ: - m_trail.push_back(a.mk_ge(mk_smod(args.get(0)), mk_smod(args.get(1)))); - break; - case OP_SLT: - bv_expr = ap->get_arg(0); - m_trail.push_back(a.mk_lt(mk_smod(args.get(0)), mk_smod(args.get(1)))); - break; - case OP_SGT: - bv_expr = ap->get_arg(0); - m_trail.push_back(a.mk_gt(mk_smod(args.get(0)), mk_smod(args.get(1)))); - break; - case OP_BNEG: - m_trail.push_back(a.mk_uminus(args.get(0))); - break; - case OP_CONCAT: { - expr_ref r(a.mk_int(0), m); - unsigned sz = 0; - for (unsigned i = 0; i < args.size(); ++i) { - expr* old_arg = ap->get_arg(i); - expr* new_arg = args.get(i); - bv_expr = old_arg; - new_arg = mk_mod(new_arg); - if (sz > 0) { - new_arg = a.mk_mul(new_arg, a.mk_int(rational::power_of_two(sz))); - r = a.mk_add(r, new_arg); - } - else - r = new_arg; - sz += bv.get_bv_size(old_arg->get_sort()); + case OP_BADD: + m_trail.push_back(a.mk_add(args)); + break; + case OP_BSUB: + m_trail.push_back(a.mk_sub(args.size(), args.data())); + break; + case OP_BMUL: + m_trail.push_back(a.mk_mul(args)); + break; + case OP_ULEQ: + bv_expr = ap->get_arg(0); + m_trail.push_back(a.mk_le(mk_mod(args.get(0)), mk_mod(args.get(1)))); + break; + case OP_UGEQ: + bv_expr = ap->get_arg(0); + m_trail.push_back(a.mk_ge(mk_mod(args.get(0)), mk_mod(args.get(1)))); + break; + case OP_ULT: + bv_expr = ap->get_arg(0); + m_trail.push_back(a.mk_lt(mk_mod(args.get(0)), mk_mod(args.get(1)))); + break; + case OP_UGT: + bv_expr = ap->get_arg(0); + m_trail.push_back(a.mk_gt(mk_mod(args.get(0)), mk_mod(args.get(1)))); + break; + case OP_SLEQ: + bv_expr = ap->get_arg(0); + m_trail.push_back(a.mk_le(mk_smod(args.get(0)), mk_smod(args.get(1)))); + break; + case OP_SGEQ: + m_trail.push_back(a.mk_ge(mk_smod(args.get(0)), mk_smod(args.get(1)))); + break; + case OP_SLT: + bv_expr = ap->get_arg(0); + m_trail.push_back(a.mk_lt(mk_smod(args.get(0)), mk_smod(args.get(1)))); + break; + case OP_SGT: + bv_expr = ap->get_arg(0); + m_trail.push_back(a.mk_gt(mk_smod(args.get(0)), mk_smod(args.get(1)))); + break; + case OP_BNEG: + m_trail.push_back(a.mk_uminus(args.get(0))); + break; + case OP_CONCAT: { + expr_ref r(a.mk_int(0), m); + unsigned sz = 0; + for (unsigned i = 0; i < args.size(); ++i) { + expr* old_arg = ap->get_arg(i); + expr* new_arg = args.get(i); + bv_expr = old_arg; + new_arg = mk_mod(new_arg); + if (sz > 0) { + new_arg = a.mk_mul(new_arg, a.mk_int(rational::power_of_two(sz))); + r = a.mk_add(r, new_arg); } - m_trail.push_back(r); - break; + else + r = new_arg; + sz += bv.get_bv_size(old_arg->get_sort()); } - case OP_EXTRACT: { - unsigned lo, hi; - expr* old_arg; - VERIFY(bv.is_extract(e, lo, hi, old_arg)); - unsigned sz = hi - lo + 1; - expr* new_arg = args.get(0); - if (lo > 0) - new_arg = a.mk_idiv(new_arg, a.mk_int(rational::power_of_two(lo))); - m_trail.push_back(new_arg); - break; - } - case OP_BV_NUM: { - rational val; - unsigned sz; - VERIFY(bv.is_numeral(e, val, sz)); - m_trail.push_back(a.mk_int(val)); - break; - } - case OP_BUREM_I: { - expr* x = args.get(0), * y = args.get(1); - m_trail.push_back(m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), a.mk_mod(x, y))); - break; - } - case OP_BUDIV_I: { - expr* x = args.get(0), * y = args.get(1); - m_trail.push_back(m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), a.mk_idiv(x, y))); - break; - } - case OP_BUMUL_NO_OVFL: { - expr* x = args.get(0), * y = args.get(1); - bv_expr = ap->get_arg(0); - m_trail.push_back(a.mk_lt(a.mk_mul(mk_mod(x), mk_mod(y)), a.mk_int(bv_size()))); - break; - } - case OP_BNOT: - case OP_BNAND: - case OP_BNOR: - case OP_BXOR: - case OP_BXNOR: - case OP_BCOMP: - case OP_BSHL: - case OP_BLSHR: - case OP_BASHR: - case OP_ROTATE_LEFT: - case OP_ROTATE_RIGHT: - case OP_EXT_ROTATE_LEFT: - case OP_EXT_ROTATE_RIGHT: - case OP_REPEAT: - case OP_ZERO_EXT: - case OP_SIGN_EXT: - case OP_BREDOR: - case OP_BREDAND: - case OP_BUDIV: - case OP_BSDIV: - case OP_BUREM: - case OP_BSREM: - case OP_BSMOD: - case OP_BAND: - verbose_stream() << mk_pp(e, m) << "\n"; - NOT_IMPLEMENTED_YET(); - break; - default: - verbose_stream() << mk_pp(e, m) << "\n"; - NOT_IMPLEMENTED_YET(); - } + m_trail.push_back(r); + break; + } + case OP_EXTRACT: { + unsigned lo, hi; + expr* old_arg; + VERIFY(bv.is_extract(e, lo, hi, old_arg)); + unsigned sz = hi - lo + 1; + expr* new_arg = args.get(0); + if (lo > 0) + new_arg = a.mk_idiv(new_arg, a.mk_int(rational::power_of_two(lo))); + m_trail.push_back(new_arg); + break; + } + case OP_BV_NUM: { + rational val; + unsigned sz; + VERIFY(bv.is_numeral(e, val, sz)); + m_trail.push_back(a.mk_int(val)); + break; + } + case OP_BUREM_I: { + expr* x = args.get(0), * y = args.get(1); + m_trail.push_back(m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), a.mk_mod(x, y))); + break; + } + case OP_BUDIV_I: { + expr* x = args.get(0), * y = args.get(1); + m_trail.push_back(m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), a.mk_idiv(x, y))); + break; + } + case OP_BUMUL_NO_OVFL: { + expr* x = args.get(0), * y = args.get(1); + bv_expr = ap->get_arg(0); + m_trail.push_back(a.mk_lt(a.mk_mul(mk_mod(x), mk_mod(y)), a.mk_int(bv_size()))); + break; + } + case OP_BSHL: { + expr* x = args.get(0), * y = args.get(1); + expr* r = a.mk_int(0); + for (unsigned i = 0; i < bv.get_bv_size(e); ++i) + r = m.mk_ite(a.mk_eq(y, a.mk_int(i)), a.mk_mul(x, a.mk_int(rational::power_of_two(i))), r); + m_trail.push_back(r); + break; + } + case OP_BNOT: + m_trail.push_back(bnot(args.get(0))); + break; + case OP_BLSHR: { + expr* x = args.get(0), * y = args.get(1); + expr* r = a.mk_int(0); + for (unsigned i = 0; i < bv.get_bv_size(e); ++i) + r = m.mk_ite(a.mk_eq(y, a.mk_int(i)), a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r); + m_trail.push_back(r); + break; + } + case OP_BOR: + for (unsigned i = 0; i < args.size(); ++i) + args[i] = bnot(args.get(i)); + m_trail.push_back(bnot(band(args))); + break; + case OP_BNAND: + m_trail.push_back(bnot(band(args))); + break; + case OP_BAND: + m_trail.push_back(band(args)); + break; + case OP_BXOR: + case OP_BXNOR: + case OP_BCOMP: + case OP_BASHR: + case OP_ROTATE_LEFT: + case OP_ROTATE_RIGHT: + case OP_EXT_ROTATE_LEFT: + case OP_EXT_ROTATE_RIGHT: + case OP_REPEAT: + case OP_ZERO_EXT: + case OP_SIGN_EXT: + case OP_BREDOR: + case OP_BREDAND: + case OP_BUDIV: + case OP_BSDIV: + case OP_BUREM: + case OP_BSREM: + case OP_BSMOD: + verbose_stream() << mk_pp(e, m) << "\n"; + NOT_IMPLEMENTED_YET(); + break; + default: + verbose_stream() << mk_pp(e, m) << "\n"; + NOT_IMPLEMENTED_YET(); + } translated.insert(e, m_trail.back()); } @@ -433,7 +468,7 @@ namespace intblast { tout << mk_pp(e, m) << "\n->\n" << mk_pp(translated[e], m) << "\n"; ); - for (unsigned i = 0; i < es.size(); ++i) + for (unsigned i = 0; i < es.size(); ++i) es[i] = translated[es.get(i)]; @@ -445,7 +480,7 @@ namespace intblast { m_solver->get_model(mdl); expr_ref r(m); var_info vi; - rational val; + rational val; if (!m_vars.find(e, vi)) return rational::zero(); if (!mdl->eval_expr(vi.dst, r, true)) diff --git a/src/sat/smt/polysat/CMakeLists.txt b/src/sat/smt/polysat/CMakeLists.txt index 1f943f48d..c7f5e49d5 100644 --- a/src/sat/smt/polysat/CMakeLists.txt +++ b/src/sat/smt/polysat/CMakeLists.txt @@ -5,6 +5,7 @@ z3_add_component(polysat core.cpp fixed_bits.cpp forbidden_intervals.cpp + op_constraint.cpp ule_constraint.cpp umul_ovfl_constraint.cpp viable.cpp diff --git a/src/sat/smt/polysat/constraints.cpp b/src/sat/smt/polysat/constraints.cpp index 0de987693..83476160a 100644 --- a/src/sat/smt/polysat/constraints.cpp +++ b/src/sat/smt/polysat/constraints.cpp @@ -17,6 +17,7 @@ Author: #include "sat/smt/polysat/constraints.h" #include "sat/smt/polysat/ule_constraint.h" #include "sat/smt/polysat/umul_ovfl_constraint.h" +#include "sat/smt/polysat/op_constraint.h" namespace polysat { @@ -36,6 +37,30 @@ namespace polysat { return signed_constraint(ckind_t::umul_ovfl_t, cnstr); } + signed_constraint constraints::lshr(pdd const& a, pdd const& b, pdd const& r) { + auto* cnstr = alloc(op_constraint, op_constraint::code::lshr_op, a, b, r); + c.trail().push(new_obj_trail(cnstr)); + return signed_constraint(ckind_t::op_t, cnstr); + } + + signed_constraint constraints::ashr(pdd const& a, pdd const& b, pdd const& r) { + auto* cnstr = alloc(op_constraint, op_constraint::code::ashr_op, a, b, r); + c.trail().push(new_obj_trail(cnstr)); + return signed_constraint(ckind_t::op_t, cnstr); + } + + signed_constraint constraints::shl(pdd const& a, pdd const& b, pdd const& r) { + auto* cnstr = alloc(op_constraint, op_constraint::code::shl_op, a, b, r); + c.trail().push(new_obj_trail(cnstr)); + return signed_constraint(ckind_t::op_t, cnstr); + } + + signed_constraint constraints::band(pdd const& a, pdd const& b, pdd const& r) { + auto* cnstr = alloc(op_constraint, op_constraint::code::and_op, a, b, r); + c.trail().push(new_obj_trail(cnstr)); + return signed_constraint(ckind_t::op_t, cnstr); + } + bool signed_constraint::is_eq(pvar& v, rational& val) { if (m_sign) return false; @@ -64,10 +89,4 @@ namespace polysat { return out << *m_constraint; } - bool signed_constraint::is_always_true() const { - return m_sign ? m_constraint->is_always_false() : m_constraint->is_always_true(); - } - bool signed_constraint::is_always_false() const { - return m_sign ? m_constraint->is_always_true() : m_constraint->is_always_false(); - } } diff --git a/src/sat/smt/polysat/constraints.h b/src/sat/smt/polysat/constraints.h index 81ba6f6a0..15d8dfa09 100644 --- a/src/sat/smt/polysat/constraints.h +++ b/src/sat/smt/polysat/constraints.h @@ -41,8 +41,6 @@ namespace polysat { virtual std::ostream& display(std::ostream& out) const = 0; virtual lbool eval() const = 0; virtual lbool eval(assignment const& a) const = 0; - virtual bool is_always_true() const = 0; - virtual bool is_always_false() const = 0; }; inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); } @@ -63,9 +61,10 @@ namespace polysat { unsigned_vector const& vars() const { return m_constraint->vars(); } unsigned var(unsigned idx) const { return m_constraint->var(idx); } bool contains_var(pvar v) const { return m_constraint->contains_var(v); } - bool is_always_true() const; - bool is_always_false() const; + bool is_always_true() const { return eval() == l_true; } + bool is_always_false() const { return eval() == l_false; } lbool eval(assignment& a) const; + lbool eval() const { return m_sign ? ~m_constraint->eval() : m_constraint->eval();} ckind_t op() const { return m_op; } bool is_ule() const { return m_op == ule_t; } bool is_umul_ovfl() const { return m_op == umul_ovfl_t; } @@ -138,6 +137,10 @@ namespace polysat { signed_constraint umul_ovfl(int p, pdd const& q) { return umul_ovfl(rational(p), q); } signed_constraint umul_ovfl(unsigned p, pdd const& q) { return umul_ovfl(rational(p), q); } + signed_constraint lshr(pdd const& a, pdd const& b, pdd const& r); + signed_constraint ashr(pdd const& a, pdd const& b, pdd const& r); + signed_constraint shl(pdd const& a, pdd const& b, pdd const& r); + signed_constraint band(pdd const& a, pdd const& b, pdd const& r); //signed_constraint even(pdd const& p) { return parity_at_least(p, 1); } //signed_constraint odd(pdd const& p) { return ~even(p); } diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h index e43633620..c6442a290 100644 --- a/src/sat/smt/polysat/core.h +++ b/src/sat/smt/polysat/core.h @@ -115,10 +115,10 @@ namespace polysat { signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); } - void lshr(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("lshr nyi"); } - void ashr(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("ashr nyi"); } - void shl(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("shlh nyi"); } - void band(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("band nyi"); } + signed_constraint lshr(pdd const& a, pdd const& b, pdd const& r) { return m_constraints.lshr(a, b, r); } + signed_constraint ashr(pdd const& a, pdd const& b, pdd const& r) { return m_constraints.ashr(a, b, r); } + signed_constraint shl(pdd const& a, pdd const& b, pdd const& r) { return m_constraints.shl(a, b, r); } + signed_constraint band(pdd const& a, pdd const& b, pdd const& r) { return m_constraints.band(a, b, r); } pdd bnot(pdd p) { return -p - 1; } diff --git a/src/sat/smt/polysat/ule_constraint.cpp b/src/sat/smt/polysat/ule_constraint.cpp index 3d6240bad..185dad0ee 100644 --- a/src/sat/smt/polysat/ule_constraint.cpp +++ b/src/sat/smt/polysat/ule_constraint.cpp @@ -343,22 +343,4 @@ namespace polysat { return eval(a.apply_to(lhs()), a.apply_to(rhs())); } - bool ule_constraint::is_always_true() const { - if (lhs().is_zero()) - return true; // 0 <= p - if (rhs().is_max()) - return true; // p <= -1 - if (lhs().is_val() && rhs().is_val()) - return lhs().val() <= rhs().val(); - return false; - } - - bool ule_constraint::is_always_false() const { - if (lhs().is_never_zero() && rhs().is_zero()) - return true; // p > 0, q = 0 - if (lhs().is_val() && rhs().is_val()) - return lhs().val() > rhs().val(); - return false; - } - } diff --git a/src/sat/smt/polysat/ule_constraint.h b/src/sat/smt/polysat/ule_constraint.h index 0d481c5ea..aa53e6a4f 100644 --- a/src/sat/smt/polysat/ule_constraint.h +++ b/src/sat/smt/polysat/ule_constraint.h @@ -35,8 +35,6 @@ namespace polysat { std::ostream& display(std::ostream& out) const override; lbool eval() const override; lbool eval(assignment const& a) const override; - bool is_always_true() const override; - bool is_always_false() const override; bool is_eq() const { return m_rhs.is_zero(); } unsigned power_of_2() const { return m_lhs.power_of_2(); } diff --git a/src/sat/smt/polysat/umul_ovfl_constraint.h b/src/sat/smt/polysat/umul_ovfl_constraint.h index 4ac03dfb3..c9d03fb01 100644 --- a/src/sat/smt/polysat/umul_ovfl_constraint.h +++ b/src/sat/smt/polysat/umul_ovfl_constraint.h @@ -34,8 +34,6 @@ namespace polysat { std::ostream& display(std::ostream& out) const override; lbool eval() const override; lbool eval(assignment const& a) const override; - bool is_always_true() const override { return false; } // todo port - bool is_always_false() const override { return false; } }; } diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 46c1e293f..4496dc759 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -234,7 +234,9 @@ namespace polysat { if (n->get_num_args() == 2) { expr* x, * y; VERIFY(bv.is_bv_and(n, x, y)); - m_core.band(expr2pdd(n), expr2pdd(x), expr2pdd(y)); + auto sc = m_core.band(expr2pdd(x), expr2pdd(y), expr2pdd(n)); + // auto index = m_core.register_constraint(sc, dependency::axiom()); + // } else { expr_ref z(n->get_arg(0), m); @@ -249,13 +251,13 @@ namespace polysat { void solver::internalize_lshr(app* n) { expr* x, * y; VERIFY(bv.is_bv_lshr(n, x, y)); - m_core.lshr(expr2pdd(n), expr2pdd(x), expr2pdd(y)); + auto sc = m_core.lshr(expr2pdd(x), expr2pdd(y), expr2pdd(n)); } void solver::internalize_shl(app* n) { expr* x, * y; VERIFY(bv.is_bv_shl(n, x, y)); - m_core.shl(expr2pdd(n), expr2pdd(x), expr2pdd(y)); + auto sc = m_core.shl(expr2pdd(x), expr2pdd(y), expr2pdd(n)); } void solver::internalize_urem_i(app* rem) {