mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

adding band

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-11 14:51:21 -08:00
parent 5622b13ed3
commit 17c480f837
12 changed files with 246 additions and 183 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ast/arith_decl_plugin.cpp
View file

@ -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(), 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)); 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)) { 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)); 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(), 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)); 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)) { 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)); return mk_func_decl(fix_kind(k, num_args), has_real_arg(m_manager, num_args, args, m_real_decl));
} }

6
src/ast/arith_decl_plugin.h
View file

@ -70,6 +70,8 @@ enum arith_op_kind {
OP_ASINH, OP_ASINH,
OP_ACOSH, OP_ACOSH,
OP_ATANH, OP_ATANH,
// Bit-vector functions
OP_ARITH_BAND,
// constants // constants
OP_PI, OP_PI,
OP_E, 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(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_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_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_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); } 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_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_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_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_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); } app * mk_tan(expr * arg) { return m_manager.mk_app(arith_family_id, OP_TAN, arg); }

5
src/sat/smt/arith_internalize.cpp
View file

@ -252,6 +252,11 @@ namespace arith {
st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n1);
st.to_ensure_var().push_back(n2); 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)) { 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); found_unsupported(n);
ensure_arg_vars(to_app(n)); ensure_arg_vars(to_app(n));

323
src/sat/smt/intblast_solver.cpp
View file

@ -19,15 +19,15 @@ Author:
namespace intblast { namespace intblast {
solver::solver(euf::solver& ctx): solver::solver(euf::solver& ctx) :
ctx(ctx), ctx(ctx),
s(ctx.s()), s(ctx.s()),
m(ctx.get_manager()), m(ctx.get_manager()),
bv(m), bv(m),
a(m), a(m),
m_trail(m) m_trail(m)
{} {}
lbool solver::check() { lbool solver::check() {
sat::literal_vector literals; sat::literal_vector literals;
uint_set selected; 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)) if (s.value(b) == l_true && s.value(a) == l_true && s.lvl(b) < s.lvl(a))
std::swap(a, b); std::swap(a, b);
selected.insert(a.index()); selected.insert(a.index());
literals.push_back(a); literals.push_back(a);
} }
m_core.reset(); m_core.reset();
@ -98,9 +98,9 @@ namespace intblast {
} }
IF_VERBOSE(10, verbose_stream() << "check\n"; IF_VERBOSE(10, verbose_stream() << "check\n";
m_solver->display(verbose_stream()); m_solver->display(verbose_stream());
verbose_stream() << es << "\n"); verbose_stream() << es << "\n");
lbool r = m_solver->check_sat(es); lbool r = m_solver->check_sat(es);
IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n"); IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n");
@ -116,14 +116,14 @@ namespace intblast {
if (idx < literals.size()) if (idx < literals.size())
m_core.push_back(literals[idx]); m_core.push_back(literals[idx]);
else else
m_core.push_back(ctx.mk_literal(e)); m_core.push_back(ctx.mk_literal(e));
} }
} }
return r; return r;
}; };
bool solver::is_bv(sat::literal lit) { bool solver::is_bv(sat::literal lit) {
expr* e = ctx.bool_var2expr(lit.var()); expr* e = ctx.bool_var2expr(lit.var());
if (!e) if (!e)
return false; return false;
@ -185,9 +185,9 @@ namespace intblast {
void solver::translate(expr_ref_vector& es) { void solver::translate(expr_ref_vector& es) {
ptr_vector<expr> todo; ptr_vector<expr> todo;
obj_map<expr, expr*> translated; obj_map<expr, expr*> translated;
expr_ref_vector args(m); expr_ref_vector args(m);
sorted_subterms(es, todo); sorted_subterms(es, todo);
for (expr* e : todo) { for (expr* e : todo) {
@ -236,12 +236,12 @@ namespace intblast {
if (m_vars.contains(x)) if (m_vars.contains(x))
return x; return x;
return to_expr(a.mk_mod(x, a.mk_int(bv_size()))); return to_expr(a.mk_mod(x, a.mk_int(bv_size())));
}; };
auto mk_smod = [&](expr* x) { auto mk_smod = [&](expr* x) {
auto shift = bv_size() / 2; auto shift = bv_size() / 2;
return a.mk_mod(a.mk_add(x, a.mk_int(shift)), a.mk_int(bv_size())); return a.mk_mod(a.mk_add(x, a.mk_int(shift)), a.mk_int(bv_size()));
}; };
if (m.is_eq(e)) { if (m.is_eq(e)) {
bool has_bv_arg = any_of(*ap, [&](expr* arg) { return bv.is_bv(arg); }); bool has_bv_arg = any_of(*ap, [&](expr* arg) { return bv.is_bv(arg); });
@ -256,7 +256,7 @@ namespace intblast {
} }
continue; continue;
} }
if (m.is_ite(e)) { if (m.is_ite(e)) {
m_trail.push_back(m.mk_ite(args.get(0), args.get(1), args.get(2))); m_trail.push_back(m.mk_ite(args.get(0), args.get(1), args.get(2)));
translated.insert(e, m_trail.back()); translated.insert(e, m_trail.back());
@ -287,144 +287,179 @@ namespace intblast {
} }
f = g; f = g;
} }
m_trail.push_back(m.mk_app(f, args)); m_trail.push_back(m.mk_app(f, args));
translated.insert(e, m_trail.back()); translated.insert(e, m_trail.back());
if (has_bv_sort) if (has_bv_sort)
m_vars.insert(e, { m_trail.back(), bv_size() }); m_vars.insert(e, { m_trail.back(), bv_size() });
continue; 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()) { switch (ap->get_decl_kind()) {
case OP_BADD: case OP_BADD:
m_trail.push_back(a.mk_add(args)); m_trail.push_back(a.mk_add(args));
break; break;
case OP_BSUB: case OP_BSUB:
m_trail.push_back(a.mk_sub(args.size(), args.data())); m_trail.push_back(a.mk_sub(args.size(), args.data()));
break; break;
case OP_BMUL: case OP_BMUL:
m_trail.push_back(a.mk_mul(args)); m_trail.push_back(a.mk_mul(args));
break; break;
case OP_ULEQ: case OP_ULEQ:
bv_expr = ap->get_arg(0); bv_expr = ap->get_arg(0);
m_trail.push_back(a.mk_le(mk_mod(args.get(0)), mk_mod(args.get(1)))); m_trail.push_back(a.mk_le(mk_mod(args.get(0)), mk_mod(args.get(1))));
break; break;
case OP_UGEQ: case OP_UGEQ:
bv_expr = ap->get_arg(0); bv_expr = ap->get_arg(0);
m_trail.push_back(a.mk_ge(mk_mod(args.get(0)), mk_mod(args.get(1)))); m_trail.push_back(a.mk_ge(mk_mod(args.get(0)), mk_mod(args.get(1))));
break; break;
case OP_ULT: case OP_ULT:
bv_expr = ap->get_arg(0); bv_expr = ap->get_arg(0);
m_trail.push_back(a.mk_lt(mk_mod(args.get(0)), mk_mod(args.get(1)))); m_trail.push_back(a.mk_lt(mk_mod(args.get(0)), mk_mod(args.get(1))));
break; break;
case OP_UGT: case OP_UGT:
bv_expr = ap->get_arg(0); bv_expr = ap->get_arg(0);
m_trail.push_back(a.mk_gt(mk_mod(args.get(0)), mk_mod(args.get(1)))); m_trail.push_back(a.mk_gt(mk_mod(args.get(0)), mk_mod(args.get(1))));
break; break;
case OP_SLEQ: case OP_SLEQ:
bv_expr = ap->get_arg(0); bv_expr = ap->get_arg(0);
m_trail.push_back(a.mk_le(mk_smod(args.get(0)), mk_smod(args.get(1)))); m_trail.push_back(a.mk_le(mk_smod(args.get(0)), mk_smod(args.get(1))));
break; break;
case OP_SGEQ: case OP_SGEQ:
m_trail.push_back(a.mk_ge(mk_smod(args.get(0)), mk_smod(args.get(1)))); m_trail.push_back(a.mk_ge(mk_smod(args.get(0)), mk_smod(args.get(1))));
break; break;
case OP_SLT: case OP_SLT:
bv_expr = ap->get_arg(0); bv_expr = ap->get_arg(0);
m_trail.push_back(a.mk_lt(mk_smod(args.get(0)), mk_smod(args.get(1)))); m_trail.push_back(a.mk_lt(mk_smod(args.get(0)), mk_smod(args.get(1))));
break; break;
case OP_SGT: case OP_SGT:
bv_expr = ap->get_arg(0); bv_expr = ap->get_arg(0);
m_trail.push_back(a.mk_gt(mk_smod(args.get(0)), mk_smod(args.get(1)))); m_trail.push_back(a.mk_gt(mk_smod(args.get(0)), mk_smod(args.get(1))));
break; break;
case OP_BNEG: case OP_BNEG:
m_trail.push_back(a.mk_uminus(args.get(0))); m_trail.push_back(a.mk_uminus(args.get(0)));
break; break;
case OP_CONCAT: { case OP_CONCAT: {
expr_ref r(a.mk_int(0), m); expr_ref r(a.mk_int(0), m);
unsigned sz = 0; unsigned sz = 0;
for (unsigned i = 0; i < args.size(); ++i) { for (unsigned i = 0; i < args.size(); ++i) {
expr* old_arg = ap->get_arg(i); expr* old_arg = ap->get_arg(i);
expr* new_arg = args.get(i); expr* new_arg = args.get(i);
bv_expr = old_arg; bv_expr = old_arg;
new_arg = mk_mod(new_arg); new_arg = mk_mod(new_arg);
if (sz > 0) { if (sz > 0) {
new_arg = a.mk_mul(new_arg, a.mk_int(rational::power_of_two(sz))); new_arg = a.mk_mul(new_arg, a.mk_int(rational::power_of_two(sz)));
r = a.mk_add(r, new_arg); r = a.mk_add(r, new_arg);
}
else
r = new_arg;
sz += bv.get_bv_size(old_arg->get_sort());
} }
m_trail.push_back(r); else
break; r = new_arg;
sz += bv.get_bv_size(old_arg->get_sort());
} }
case OP_EXTRACT: { m_trail.push_back(r);
unsigned lo, hi; break;
expr* old_arg; }
VERIFY(bv.is_extract(e, lo, hi, old_arg)); case OP_EXTRACT: {
unsigned sz = hi - lo + 1; unsigned lo, hi;
expr* new_arg = args.get(0); expr* old_arg;
if (lo > 0) VERIFY(bv.is_extract(e, lo, hi, old_arg));
new_arg = a.mk_idiv(new_arg, a.mk_int(rational::power_of_two(lo))); unsigned sz = hi - lo + 1;
m_trail.push_back(new_arg); expr* new_arg = args.get(0);
break; if (lo > 0)
} new_arg = a.mk_idiv(new_arg, a.mk_int(rational::power_of_two(lo)));
case OP_BV_NUM: { m_trail.push_back(new_arg);
rational val; break;
unsigned sz; }
VERIFY(bv.is_numeral(e, val, sz)); case OP_BV_NUM: {
m_trail.push_back(a.mk_int(val)); rational val;
break; unsigned sz;
} VERIFY(bv.is_numeral(e, val, sz));
case OP_BUREM_I: { m_trail.push_back(a.mk_int(val));
expr* x = args.get(0), * y = args.get(1); break;
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_BUREM_I: {
} expr* x = args.get(0), * y = args.get(1);
case OP_BUDIV_I: { m_trail.push_back(m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), a.mk_mod(x, y)));
expr* x = args.get(0), * y = args.get(1); break;
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_BUDIV_I: {
} expr* x = args.get(0), * y = args.get(1);
case OP_BUMUL_NO_OVFL: { m_trail.push_back(m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(0), a.mk_idiv(x, y)));
expr* x = args.get(0), * y = args.get(1); break;
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()))); case OP_BUMUL_NO_OVFL: {
break; expr* x = args.get(0), * y = args.get(1);
} bv_expr = ap->get_arg(0);
case OP_BNOT: m_trail.push_back(a.mk_lt(a.mk_mul(mk_mod(x), mk_mod(y)), a.mk_int(bv_size())));
case OP_BNAND: break;
case OP_BNOR: }
case OP_BXOR: case OP_BSHL: {
case OP_BXNOR: expr* x = args.get(0), * y = args.get(1);
case OP_BCOMP: expr* r = a.mk_int(0);
case OP_BSHL: for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
case OP_BLSHR: 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);
case OP_BASHR: m_trail.push_back(r);
case OP_ROTATE_LEFT: break;
case OP_ROTATE_RIGHT: }
case OP_EXT_ROTATE_LEFT: case OP_BNOT:
case OP_EXT_ROTATE_RIGHT: m_trail.push_back(bnot(args.get(0)));
case OP_REPEAT: break;
case OP_ZERO_EXT: case OP_BLSHR: {
case OP_SIGN_EXT: expr* x = args.get(0), * y = args.get(1);
case OP_BREDOR: expr* r = a.mk_int(0);
case OP_BREDAND: for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
case OP_BUDIV: 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);
case OP_BSDIV: m_trail.push_back(r);
case OP_BUREM: break;
case OP_BSREM: }
case OP_BSMOD: case OP_BOR:
case OP_BAND: for (unsigned i = 0; i < args.size(); ++i)
verbose_stream() << mk_pp(e, m) << "\n"; args[i] = bnot(args.get(i));
NOT_IMPLEMENTED_YET(); m_trail.push_back(bnot(band(args)));
break; break;
default: case OP_BNAND:
verbose_stream() << mk_pp(e, m) << "\n"; m_trail.push_back(bnot(band(args)));
NOT_IMPLEMENTED_YET(); 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()); 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"; 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)]; es[i] = translated[es.get(i)];
@ -445,7 +480,7 @@ namespace intblast {
m_solver->get_model(mdl); m_solver->get_model(mdl);
expr_ref r(m); expr_ref r(m);
var_info vi; var_info vi;
rational val; rational val;
if (!m_vars.find(e, vi)) if (!m_vars.find(e, vi))
return rational::zero(); return rational::zero();
if (!mdl->eval_expr(vi.dst, r, true)) if (!mdl->eval_expr(vi.dst, r, true))

1
src/sat/smt/polysat/CMakeLists.txt
View file

@ -5,6 +5,7 @@ z3_add_component(polysat
core.cpp core.cpp
fixed_bits.cpp fixed_bits.cpp
forbidden_intervals.cpp forbidden_intervals.cpp
op_constraint.cpp
ule_constraint.cpp ule_constraint.cpp
umul_ovfl_constraint.cpp umul_ovfl_constraint.cpp
viable.cpp viable.cpp

31
src/sat/smt/polysat/constraints.cpp
View file

@ -17,6 +17,7 @@ Author:
#include "sat/smt/polysat/constraints.h" #include "sat/smt/polysat/constraints.h"
#include "sat/smt/polysat/ule_constraint.h" #include "sat/smt/polysat/ule_constraint.h"
#include "sat/smt/polysat/umul_ovfl_constraint.h" #include "sat/smt/polysat/umul_ovfl_constraint.h"
#include "sat/smt/polysat/op_constraint.h"
namespace polysat { namespace polysat {
@ -36,6 +37,30 @@ namespace polysat {
return signed_constraint(ckind_t::umul_ovfl_t, cnstr); 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) { bool signed_constraint::is_eq(pvar& v, rational& val) {
if (m_sign) if (m_sign)
return false; return false;
@ -64,10 +89,4 @@ namespace polysat {
return out << *m_constraint; 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();
}
} }

11
src/sat/smt/polysat/constraints.h
View file

@ -41,8 +41,6 @@ namespace polysat {
virtual std::ostream& display(std::ostream& out) const = 0; virtual std::ostream& display(std::ostream& out) const = 0;
virtual lbool eval() const = 0; virtual lbool eval() const = 0;
virtual lbool eval(assignment const& a) 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); } 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_vector const& vars() const { return m_constraint->vars(); }
unsigned var(unsigned idx) const { return m_constraint->var(idx); } unsigned var(unsigned idx) const { return m_constraint->var(idx); }
bool contains_var(pvar v) const { return m_constraint->contains_var(v); } bool contains_var(pvar v) const { return m_constraint->contains_var(v); }
bool is_always_true() const; bool is_always_true() const { return eval() == l_true; }
bool is_always_false() const; bool is_always_false() const { return eval() == l_false; }
lbool eval(assignment& a) const; lbool eval(assignment& a) const;
lbool eval() const { return m_sign ? ~m_constraint->eval() : m_constraint->eval();}
ckind_t op() const { return m_op; } ckind_t op() const { return m_op; }
bool is_ule() const { return m_op == ule_t; } bool is_ule() const { return m_op == ule_t; }
bool is_umul_ovfl() const { return m_op == umul_ovfl_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(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 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 even(pdd const& p) { return parity_at_least(p, 1); }
//signed_constraint odd(pdd const& p) { return ~even(p); } //signed_constraint odd(pdd const& p) { return ~even(p); }

8
src/sat/smt/polysat/core.h
View file

@ -115,10 +115,10 @@ namespace polysat {
signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); } 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"); } signed_constraint lshr(pdd const& a, pdd const& b, pdd const& r) { return m_constraints.lshr(a, b, r); }
void ashr(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("ashr nyi"); } signed_constraint ashr(pdd const& a, pdd const& b, pdd const& r) { return m_constraints.ashr(a, b, r); }
void shl(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("shlh nyi"); } signed_constraint shl(pdd const& a, pdd const& b, pdd const& r) { return m_constraints.shl(a, b, r); }
void band(pdd r, pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("band nyi"); } 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; } pdd bnot(pdd p) { return -p - 1; }

18
src/sat/smt/polysat/ule_constraint.cpp
View file

@ -343,22 +343,4 @@ namespace polysat {
return eval(a.apply_to(lhs()), a.apply_to(rhs())); 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;
}
} }

2
src/sat/smt/polysat/ule_constraint.h
View file

@ -35,8 +35,6 @@ namespace polysat {
std::ostream& display(std::ostream& out) const override; std::ostream& display(std::ostream& out) const override;
lbool eval() const override; lbool eval() const override;
lbool eval(assignment const& a) 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(); } bool is_eq() const { return m_rhs.is_zero(); }
unsigned power_of_2() const { return m_lhs.power_of_2(); } unsigned power_of_2() const { return m_lhs.power_of_2(); }

2
src/sat/smt/polysat/umul_ovfl_constraint.h
View file

@ -34,8 +34,6 @@ namespace polysat {
std::ostream& display(std::ostream& out) const override; std::ostream& display(std::ostream& out) const override;
lbool eval() const override; lbool eval() const override;
lbool eval(assignment const& a) 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; }
}; };
} }

8
src/sat/smt/polysat_internalize.cpp
View file

@ -234,7 +234,9 @@ namespace polysat {
if (n->get_num_args() == 2) { if (n->get_num_args() == 2) {
expr* x, * y; expr* x, * y;
VERIFY(bv.is_bv_and(n, 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 { else {
expr_ref z(n->get_arg(0), m); expr_ref z(n->get_arg(0), m);
@ -249,13 +251,13 @@ namespace polysat {
void solver::internalize_lshr(app* n) { void solver::internalize_lshr(app* n) {
expr* x, * y; expr* x, * y;
VERIFY(bv.is_bv_lshr(n, 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) { void solver::internalize_shl(app* n) {
expr* x, * y; expr* x, * y;
VERIFY(bv.is_bv_shl(n, 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) { void solver::internalize_urem_i(app* rem) {