mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

integrating int-blaster

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-10 19:55:25 -08:00
parent 09c2e0dd6e
commit 701671466b
14 changed files with 285 additions and 77 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/smt/euf_solver.cpp
View file

@ -135,11 +135,8 @@ namespace euf {
special_relations_util sp(m);
if (pb.get_family_id() == fid)
ext = alloc(pb::solver, *this, fid);
else if (bvu.get_family_id() == fid) {
ext = alloc(bv::solver, *this, fid);
dealloc(ext);
ext = alloc(polysat::solver, *this, fid);
}
else if (bvu.get_family_id() == fid)
ext = alloc(polysat::solver, *this, fid);
else if (au.get_family_id() == fid)
ext = alloc(array::solver, *this, fid);
else if (fpa.get_family_id() == fid)

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

@ -79,6 +79,8 @@ namespace intblast {
}
m_core.reset();
m_vars.reset();
m_trail.reset();
m_solver = mk_smt2_solver(m, s.params(), symbol::null);
expr_ref_vector es(m);
@ -89,12 +91,19 @@ namespace intblast {
for (auto const& [src, vi] : m_vars) {
auto const& [v, b] = vi;
verbose_stream() << "asserting " << mk_pp(v, m) << " < " << b << "\n";
m_solver->assert_expr(a.mk_le(a.mk_int(0), v));
m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
}
verbose_stream() << "check\n";
m_solver->display(verbose_stream());
verbose_stream() << es << "\n";
lbool r = m_solver->check_sat(es);
verbose_stream() << "result " << r << "\n";
if (r == l_false) {
expr_ref_vector core(m);
m_solver->get_unsat_core(core);
@ -114,8 +123,6 @@ namespace intblast {
return false;
if (m.is_and(e) || m.is_or(e) || m.is_not(e) || m.is_implies(e) || m.is_iff(e))
return false;
if (is_quantifier(e))
return false;
return any_of(subterms::all(expr_ref(e, m)), [&](auto* p) { return bv.is_bv_sort(p->get_sort()); });
}
@ -145,22 +152,34 @@ namespace intblast {
}
}
}
std::stable_sort(sorted.begin(), sorted.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); });
}
void solver::translate(expr_ref_vector& es) {
ptr_vector<expr> todo;
obj_map<expr, expr*> translated;
expr_ref_vector args(m);
m_trail.reset();
m_vars.reset();
sorted_subterms(es, todo);
for (unsigned i = todo.size(); i-- > 0; ) {
expr* e = todo[i];
for (expr* e : todo) {
if (is_quantifier(e)) {
quantifier* q = to_quantifier(e);
expr* b = q->get_expr();
m_trail.push_back(m.update_quantifier(q, translated[b]));
unsigned nd = q->get_num_decls();
ptr_vector<sort> sorts;
for (unsigned i = 0; i < nd; ++i) {
auto s = q->get_decl_sort(i);
if (bv.is_bv_sort(s)) {
NOT_IMPLEMENTED_YET();
sorts.push_back(a.mk_int());
}
else
sorts.push_back(s);
}
b = translated[b];
// TODO if sorts contain integer, then created bounds variables.
m_trail.push_back(m.update_quantifier(q, b));
translated.insert(e, m_trail.back());
continue;
}
@ -177,11 +196,12 @@ namespace intblast {
continue;
}
app* ap = to_app(e);
expr* bv_expr = e;
args.reset();
for (auto arg : *ap)
args.push_back(translated[arg]);
auto bv_size = [&]() { return rational::power_of_two(bv.get_bv_size(e->get_sort())); };
auto bv_size = [&]() { return rational::power_of_two(bv.get_bv_size(bv_expr->get_sort())); };
auto mk_mod = [&](expr* x) {
if (m_vars.contains(x))
@ -197,6 +217,7 @@ namespace intblast {
if (m.is_eq(e)) {
bool has_bv_arg = any_of(*ap, [&](expr* arg) { return bv.is_bv(arg); });
if (has_bv_arg) {
bv_expr = ap->get_arg(0);
m_trail.push_back(m.mk_eq(mk_mod(args.get(0)), mk_mod(args.get(1))));
translated.insert(e, m_trail.back());
}
@ -229,6 +250,8 @@ namespace intblast {
m_trail.push_back(m.mk_app(f, args));
translated.insert(e, m_trail.back());
verbose_stream() << "translate " << mk_pp(e, m) << " " << has_bv_sort << "\n";
if (has_bv_sort)
m_vars.insert(e, { m_trail.back(), bv_size() });
@ -272,6 +295,53 @@ namespace intblast {
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());
}
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_div(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_BNOT:
case OP_BNAND:
case OP_BNOR:
@ -296,9 +366,14 @@ namespace intblast {
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();
}
verbose_stream() << "insert " << mk_pp(e, m) << " -> " << mk_pp(m_trail.back(), m) << "\n";
translated.insert(e, m_trail.back());
}
for (unsigned i = 0; i < es.size(); ++i)

40
src/sat/smt/polysat/polysat_constraints.cpp
View file

@ -1,4 +1,4 @@
/*++
/*++
Copyright (c) 2021 Microsoft Corporation
Module Name:
@ -12,6 +12,7 @@ Author:
--*/
#include "util/log.h"
#include "sat/smt/polysat/polysat_core.h"
#include "sat/smt/polysat/polysat_constraints.h"
#include "sat/smt/polysat/polysat_ule.h"
@ -23,16 +24,34 @@ namespace polysat {
pdd lhs = p, rhs = q;
bool is_positive = true;
ule_constraint::simplify(is_positive, lhs, rhs);
auto* c = alloc(ule_constraint, p, q);
m_trail.push(new_obj_trail(c));
auto sc = signed_constraint(ckind_t::ule_t, c);
auto* cnstr = alloc(ule_constraint, p, q);
c.trail().push(new_obj_trail(cnstr));
auto sc = signed_constraint(ckind_t::ule_t, cnstr);
return is_positive ? sc : ~sc;
}
signed_constraint constraints::umul_ovfl(pdd const& p, pdd const& q) {
auto* c = alloc(umul_ovfl_constraint, p, q);
m_trail.push(new_obj_trail(c));
return signed_constraint(ckind_t::umul_ovfl_t, c);
auto* cnstr = alloc(umul_ovfl_constraint, p, q);
c.trail().push(new_obj_trail(cnstr));
return signed_constraint(ckind_t::umul_ovfl_t, cnstr);
}
bool signed_constraint::is_eq(pvar& v, rational& val) {
if (m_sign)
return false;
if (!is_ule())
return false;
auto const& ule = to_ule();
auto const& l = ule.lhs(), &r = ule.rhs();
if (!r.is_zero())
return false;
if (!l.is_unilinear())
return false;
if (!l.hi().is_one())
return false;
v = l.var();
val = -l.lo().val();
return true;
}
lbool signed_constraint::eval(assignment& a) const {
@ -44,4 +63,11 @@ namespace polysat {
if (m_sign) out << "~";
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();
}
}

24
src/sat/smt/polysat/polysat_constraints.h
View file

@ -41,6 +41,8 @@ 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); }
@ -61,6 +63,8 @@ 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;
lbool eval(assignment& a) const;
ckind_t op() const { return m_op; }
bool is_ule() const { return m_op == ule_t; }
@ -68,27 +72,27 @@ namespace polysat {
bool is_smul_fl() const { return m_op == smul_fl_t; }
ule_constraint const& to_ule() const { return *reinterpret_cast<ule_constraint*>(m_constraint); }
umul_ovfl_constraint const& to_umul_ovfl() const { return *reinterpret_cast<umul_ovfl_constraint*>(m_constraint); }
bool is_eq(pvar& v, rational& val) { throw default_exception("nyi"); }
bool is_eq(pvar& v, rational& val);
std::ostream& display(std::ostream& out) const;
};
inline std::ostream& operator<<(std::ostream& out, signed_constraint const& c) { return c.display(out); }
class constraints {
trail_stack& m_trail;
core& c;
public:
constraints(trail_stack& c) : m_trail(c) {}
constraints(core& c) : c(c) {}
signed_constraint eq(pdd const& p) { return ule(p, p.manager().mk_val(0)); }
signed_constraint eq(pdd const& p, rational const& v) { return eq(p - p.manager().mk_val(v)); }
signed_constraint ule(pdd const& p, pdd const& q);
signed_constraint sle(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
signed_constraint ult(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
signed_constraint slt(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
signed_constraint sle(pdd const& p, pdd const& q) { auto sh = rational::power_of_two(p.power_of_2() - 1); return ule(p + sh, q + sh); }
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("nyi"); }
signed_constraint smul_udfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); }
signed_constraint bit(pdd const& p, unsigned i) { throw default_exception("nyi"); }
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) { throw default_exception("bit nyi"); }
signed_constraint diseq(pdd const& p) { return ~eq(p); }
signed_constraint diseq(pdd const& p, pdd const& q) { return diseq(p - q); }
@ -138,4 +142,4 @@ namespace polysat {
//signed_constraint even(pdd const& p) { return parity_at_least(p, 1); }
//signed_constraint odd(pdd const& p) { return ~even(p); }
};
}
}

2
src/sat/smt/polysat/polysat_core.cpp
View file

@ -80,7 +80,7 @@ namespace polysat {
core::core(solver_interface& s) :
s(s),
m_viable(*this),
m_constraints(s.trail()),
m_constraints(*this),
m_assignment(*this),
m_var_queue(m_activity)
{}

36
src/sat/smt/polysat/polysat_core.h
View file

@ -84,7 +84,8 @@ namespace polysat {
void get_bitvector_prefixes(pvar v, pvar_vector& out);
void get_fixed_bits(pvar v, svector<justified_fixed_bits>& fixed_bits);
bool inconsistent() const;
void add_clause(char const* name, std::initializer_list<signed_constraint> cs, bool is_redundant);
void add_watch(unsigned idx, unsigned var);
@ -114,29 +115,28 @@ namespace polysat {
signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
pdd lshr(pdd a, pdd b) { throw default_exception("nyi"); }
pdd ashr(pdd a, pdd b) { throw default_exception("nyi"); }
pdd shl(pdd a, pdd b) { throw default_exception("nyi"); }
pdd band(pdd a, pdd b) { throw default_exception("nyi"); }
pdd bxor(pdd a, pdd b) { throw default_exception("nyi"); }
pdd bor(pdd a, pdd b) { throw default_exception("nyi"); }
pdd bnand(pdd a, pdd b) { throw default_exception("nyi"); }
pdd bxnor(pdd a, pdd b) { throw default_exception("nyi"); }
pdd bnor(pdd a, pdd b) { throw default_exception("nyi"); }
pdd bnot(pdd a) { throw default_exception("nyi"); }
std::pair<pdd, pdd> quot_rem(pdd const& n, pdd const& d) { throw default_exception("nyi"); }
pdd zero_ext(pdd a, unsigned sz) { throw default_exception("nyi"); }
pdd sign_ext(pdd a, unsigned sz) { throw default_exception("nyi"); }
pdd extract(pdd src, unsigned hi, unsigned lo) { throw default_exception("nyi"); }
pdd concat(unsigned n, pdd const* args) { throw default_exception("nyi"); }
pdd lshr(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("lshr nyi"); }
pdd ashr(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("ashr nyi"); }
pdd shl(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("shlh nyi"); }
pdd band(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("band nyi"); }
pdd bxor(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bxor nyi"); }
pdd bor(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bir ==nyi"); }
pdd bnand(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bnand nyi"); }
pdd bxnor(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bxnor nyi"); }
pdd bnor(pdd a, pdd b) { NOT_IMPLEMENTED_YET(); throw default_exception("bnotr nyi"); }
pdd bnot(pdd a) { NOT_IMPLEMENTED_YET(); throw default_exception("bnot nyi"); }
pdd zero_ext(pdd a, unsigned sz) { NOT_IMPLEMENTED_YET(); throw default_exception("zero ext nyi"); }
pdd sign_ext(pdd a, unsigned sz) { NOT_IMPLEMENTED_YET(); throw default_exception("sign ext nyi"); }
pdd extract(pdd src, unsigned hi, unsigned lo) { NOT_IMPLEMENTED_YET(); throw default_exception("extract nyi"); }
pdd concat(unsigned n, pdd const* args) { NOT_IMPLEMENTED_YET(); throw default_exception("concat nyi"); }
pvar add_var(unsigned sz);
pdd var(pvar p) { return m_vars[p]; }
unsigned size(pvar v) const { return var2pdd(v).power_of_2(); }
unsigned size(pvar v) const { return m_vars[v].power_of_2(); }
constraints& cs() { return m_constraints; }
trail_stack& trail();
std::ostream& display(std::ostream& out) const { throw default_exception("nyi"); }
std::ostream& display(std::ostream& out) const { NOT_IMPLEMENTED_YET(); throw default_exception("nyi"); }
};
}

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

@ -343,4 +343,22 @@ 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;
}
}

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

@ -35,6 +35,8 @@ 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(); }

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

@ -34,6 +34,8 @@ 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; }
};
}

4
src/sat/smt/polysat/polysat_viable.cpp
View file

@ -90,6 +90,8 @@ namespace polysat {
}
lbool viable::find_viable(pvar v, rational& lo, rational& hi) {
return l_undef;
fixed_bits_info fbi;
#if 0
@ -1007,7 +1009,7 @@ namespace polysat {
}
void viable::log(pvar v) {
throw default_exception("nyi");
//
}

14
src/sat/smt/polysat/polysat_viable.h
View file

@ -186,36 +186,36 @@ namespace polysat {
template <bool FORWARD>
bool refine_viable(pvar v, rational const& val, fixed_bits_info const& fbi) {
throw default_exception("nyi");
throw default_exception("refine nyi");
}
bool refine_viable(pvar v, rational const& val) {
throw default_exception("nyi");
throw default_exception("refine nyi");
}
template <bool FORWARD>
bool refine_bits(pvar v, rational const& val, fixed_bits_info const& fbi) {
throw default_exception("nyi");
throw default_exception("refine nyi");
}
template <bool FORWARD>
entry* refine_bits(pvar v, rational const& val, unsigned num_bits, fixed_bits_info const& fbi) {
throw default_exception("nyi");
throw default_exception("refine nyi");
}
bool refine_equal_lin(pvar v, rational const& val) {
throw default_exception("nyi");
throw default_exception("refine nyi");
}
bool refine_disequal_lin(pvar v, rational const& val) {
throw default_exception("nyi");
throw default_exception("refine nyi");
}
void set_conflict_by_interval(pvar v, unsigned w, ptr_vector<entry>& intervals, unsigned first_interval);
bool set_conflict_by_interval_rec(pvar v, unsigned w, entry** intervals, unsigned num_intervals, bool& create_lemma, uint_set& vars_to_explain);
std::pair<entry*, bool> find_value(rational const& val, entry* entries) {
throw default_exception("nyi");
throw default_exception("fine_value nyi");
}
bool collect_bit_information(pvar v, bool add_conflict, fixed_bits_info& out_fbi);

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

@ -1,4 +1,4 @@
/*++
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
@ -22,7 +22,9 @@ Author:
namespace polysat {
euf::theory_var solver::mk_var(euf::enode* n) {
return euf::th_euf_solver::mk_var(n);
theory_var v = euf::th_euf_solver::mk_var(n);
ctx.attach_th_var(n, this, v);
return v;
}
sat::literal solver::internalize(expr* e, bool sign, bool root) {
@ -115,12 +117,13 @@ namespace polysat {
case OP_BSADD_OVFL:
case OP_BUSUB_OVFL:
case OP_BSSUB_OVFL:
verbose_stream() << mk_pp(a, m) << "\n";
// handled by bv_rewriter for now
UNREACHABLE();
break;
case OP_BUDIV_I: internalize_div_rem_i(a, true); break;
case OP_BUREM_I: internalize_div_rem_i(a, false); break;
case OP_BUDIV_I: internalize_udiv_i(a); break;
case OP_BUREM_I: internalize_urem_i(a); break;
case OP_BUDIV: internalize_div_rem(a, true); break;
case OP_BUREM: internalize_div_rem(a, false); break;
@ -187,17 +190,93 @@ namespace polysat {
mk_atom(lit.var(), sc);
}
void solver::internalize_div_rem_i(app* e, bool is_div) {
auto p = expr2pdd(e->get_arg(0));
auto q = expr2pdd(e->get_arg(1));
auto [quot, rem] = m_core.quot_rem(p, q);
internalize_set(e, is_div ? quot : rem);
void solver::internalize_udiv_i(app* e) {
expr* x, *y;
VERIFY(bv.is_bv_udivi(e, x, y) || bv.is_bv_udiv(e, x, y));
app_ref rm(bv.mk_bv_urem_i(x, y), m);
internalize(rm);
}
void solver::internalize_urem_i(app* e) {
expr* x, *y;
if (expr2enode(e))
return;
VERIFY(bv.is_bv_uremi(e, x, y) || bv.is_bv_urem(e, x, y));
auto [quot, rem] = quot_rem(x, y);
internalize_set(e, rem);
internalize_set(bv.mk_bv_udiv_i(x, y), quot);
}
std::pair<pdd, pdd> solver::quot_rem(expr* x, expr* y) {
pdd a = expr2pdd(x);
pdd b = expr2pdd(y);
auto& m = a.manager();
unsigned sz = m.power_of_2();
if (b.is_zero())
// By SMT-LIB specification, b = 0 ==> q = -1, r = a.
return { m.mk_val(m.max_value()), a };
if (b.is_one())
return { a, m.zero() };
if (a.is_val() && b.is_val()) {
rational const av = a.val();
rational const bv = b.val();
SASSERT(!bv.is_zero());
rational rv;
rational qv = machine_div_rem(av, bv, rv);
pdd q = m.mk_val(qv);
pdd r = m.mk_val(rv);
SASSERT_EQ(a, b * q + r);
SASSERT(b.val() * q.val() + r.val() <= m.max_value());
SASSERT(r.val() <= (b * q + r).val());
SASSERT(r.val() < b.val());
return { std::move(q), std::move(r) };
}
expr* quot = bv.mk_bv_udiv_i(x, y);
expr* rem = bv.mk_bv_urem_i(x, y);
ctx.internalize(quot);
ctx.internalize(rem);
auto quotv = expr2enode(quot)->get_th_var(get_id());
auto remv = expr2enode(rem)->get_th_var(get_id());
pdd q = var2pdd(quotv);
pdd r = var2pdd(remv);
// Axioms for quotient/remainder
//
// a = b*q + r
// multiplication does not overflow in b*q
// addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r
// b ≠ 0 ==> r < b
// b = 0 ==> q = -1
// TODO: when a,b become evaluable, can we actually propagate q,r? doesn't seem like it.
// Maybe we need something like an op_constraint for better propagation.
add_polysat_clause("[axiom] quot_rem 1", { m_core.eq(b * q + r - a) }, false);
add_polysat_clause("[axiom] quot_rem 2", { ~m_core.umul_ovfl(b, q) }, false);
// r <= b*q+r
// { apply equivalence: p <= q <=> q-p <= -p-1 }
// b*q <= -r-1
add_polysat_clause("[axiom] quot_rem 3", { m_core.ule(b * q, -r - 1) }, false);
auto c_eq = m_core.eq(b);
if (!c_eq.is_always_true())
add_polysat_clause("[axiom] quot_rem 4", { c_eq, ~m_core.ule(b, r) }, false);
if (!c_eq.is_always_false())
add_polysat_clause("[axiom] quot_rem 5", { ~c_eq, m_core.eq(q + 1) }, false);
return { std::move(q), std::move(r) };
}
void solver::internalize_div_rem(app* e, bool is_div) {
bv_rewriter_params p(s().params());
if (p.hi_div0()) {
internalize_div_rem_i(e, is_div);
if (bv.is_bv_udivi(e))
internalize_udiv_i(e);
else
internalize_urem_i(e);
return;
}
expr* arg1 = e->get_arg(0);

14
src/sat/smt/polysat_solver.cpp
View file

@ -84,6 +84,8 @@ namespace polysat {
}
}
}
UNREACHABLE();
return sat::check_result::CR_GIVEUP;
}
void solver::asserted(literal l) {
@ -249,11 +251,11 @@ namespace polysat {
return ctx.get_trail_stack();
}
void solver::add_lemma(vector<signed_constraint> const& lemma) {
void solver::add_polysat_clause(char const* name, std::initializer_list<signed_constraint> cs, bool is_redundant) {
sat::literal_vector lits;
for (auto sc : lemma)
for (auto sc : cs)
lits.push_back(ctx.mk_literal(constraint2expr(sc)));
s().add_clause(lits.size(), lits.data(), sat::status::th(true, get_id(), nullptr));
s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), nullptr));
}
void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) {
@ -271,14 +273,14 @@ namespace polysat {
case ckind_t::umul_ovfl_t: {
auto l = pdd2expr(sc.to_umul_ovfl().p());
auto r = pdd2expr(sc.to_umul_ovfl().q());
return expr_ref(bv.mk_bvumul_ovfl(l, r), m);
return expr_ref(m.mk_not(bv.mk_bvumul_no_ovfl(l, r)), m);
}
case ckind_t::smul_fl_t:
case ckind_t::op_t:
NOT_IMPLEMENTED_YET();
break;
}
throw default_exception("nyi");
throw default_exception("constraint2expr nyi");
}
expr_ref solver::pdd2expr(pdd const& p) {
@ -346,7 +348,7 @@ namespace polysat {
continue;
for (auto sib : euf::enode_class(p)) {
if (bv.is_extract(sib->get_expr(), lo, hi, e) && r == expr2enode(e)->get_root()) {
throw default_exception("nyi");
throw default_exception("get_fixed nyi");
// TODO
// dependency d = dependency(p->get_th_var(get_id()), n->get_th_var(get_id()), s().scope_lvl());
// fixed_bits.push_back({ hi, lo, rational::zero(), null_dependency()});

9
src/sat/smt/polysat_solver.h
View file

@ -113,10 +113,10 @@ namespace polysat {
void internalize_extract(app* n);
void internalize_repeat(app* n);
void internalize_bit2bool(app* n);
void internalize_udiv_i(app* n);
template<bool Signed, bool Reverse, bool Negated>
void internalize_le(app* n);
void internalize_div_rem_i(app* e, bool is_div);
void internalize_udiv_i(app* e);
void internalize_urem_i(app* e);
void internalize_div_rem(app* e, bool is_div);
void internalize_polysat(app* a);
void assert_bv2int_axiom(app * n);
@ -126,6 +126,8 @@ namespace polysat {
pdd var2pdd(euf::theory_var v);
void internalize_set(expr* e, pdd const& p);
void internalize_set(euf::theory_var v, pdd const& p);
std::pair<pdd, pdd> quot_rem(expr* x, expr* y);
// callbacks from core
void add_eq_literal(pvar v, rational const& val) override;
@ -137,8 +139,7 @@ namespace polysat {
bool inconsistent() const override;
void get_bitvector_prefixes(pvar v, pvar_vector& out) override;
void get_fixed_bits(pvar v, svector<justified_fixed_bits>& fixed_bits) override;
void add_lemma(vector<signed_constraint> const& lemma);
void add_polysat_clause(char const* name, std::initializer_list<signed_constraint> cs, bool is_redundant);
std::pair<sat::literal_vector, euf::enode_pair_vector> explain_deps(dependency_vector const& deps);