mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

import updates from poly branch

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-10 19:42:58 -08:00
parent 2ca1187b3a
commit 955c80e98b
8 changed files with 408 additions and 217 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/arith_decl_plugin.h
View file

@ -401,6 +401,7 @@ public:
// return true if \c n is a term of the form (* -1 r) // return true if \c n is a term of the form (* -1 r)
bool is_zero(expr const* n) const { rational val; return is_numeral(n, val) && val.is_zero(); } bool is_zero(expr const* n) const { rational val; return is_numeral(n, val) && val.is_zero(); }
bool is_one(expr const* n) const{ rational val; return is_numeral(n, val) && val.is_one(); }
bool is_minus_one(expr* n) const { rational tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); } bool is_minus_one(expr* n) const { rational tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); }
bool is_times_minus_one(expr* n, expr*& r) const { bool is_times_minus_one(expr* n, expr*& r) const {
if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) { if (is_mul(n) && to_app(n)->get_num_args() == 2 && is_minus_one(to_app(n)->get_arg(0))) {

162
src/ast/euf/euf_bv_plugin.cpp
View file

@ -69,18 +69,15 @@ The formal properties of saturation have to be established.
- Saturation does not complete with respect to associativity. - Saturation does not complete with respect to associativity.
Instead the claim is along the lines that the resulting E-graph can be used as a canonizer. Instead the claim is along the lines that the resulting E-graph can be used as a canonizer.
If given a set of equations E that are saturated, and terms t1, t2 that are If given a set of equations E that are saturated, and terms t1, t2 that are
both simplified with respect to left-associativity of concatenation, and t1, t2 belong to the E-graph, both simplified with respect to left-associativity of concatentation, and t1, t2 belong to the E-graph,
then t1 = t2 iff t1 ~ t2 in the E-graph. then t1 = t2 iff t1 ~ t2 in the E-graph.
TODO: Is saturation for (7) overkill for the purpose of canonization? TODO: Is saturation for (7) overkill for the purpose of canonization?
TODO: revisit re-entrancy during register_node. It can be called when creating internal extract terms.
Instead of allowing re-entrancy we can accumulate nodes that are registered during recursive calls
and have the main call perform recursive slicing.
--*/ --*/
#include "ast/ast_pp.h"
#include "ast/euf/euf_bv_plugin.h" #include "ast/euf/euf_bv_plugin.h"
#include "ast/euf/euf_egraph.h" #include "ast/euf/euf_egraph.h"
@ -91,19 +88,22 @@ namespace euf {
bv(g.get_manager()) bv(g.get_manager())
{} {}
enode* bv_plugin::mk_value_concat(enode* a, enode* b) { enode* bv_plugin::mk_value_concat(enode* hi, enode* lo) {
auto v1 = get_value(a); auto v1 = get_value(hi);
auto v2 = get_value(b); auto v2 = get_value(lo);
auto v3 = v1 + v2 * power(rational(2), width(a)); auto v3 = v2 + v1 * rational::power_of_two(width(lo));
return mk_value(v3, width(a) + width(b)); return mk_value(v3, width(lo) + width(hi));
} }
enode* bv_plugin::mk_value(rational const& v, unsigned sz) { enode* bv_plugin::mk_value(rational const& v, unsigned sz) {
auto e = bv.mk_numeral(v, sz); auto e = bv.mk_numeral(v, sz);
return mk(e, 0, nullptr); auto n = mk(e, 0, nullptr);
if (m_ensure_th_var)
m_ensure_th_var(n);
return n;
} }
void bv_plugin::merge_eh(enode* x, enode* y) { void bv_plugin::propagate_merge(enode* x, enode* y) {
if (!bv.is_bv(x->get_expr())) if (!bv.is_bv(x->get_expr()))
return; return;
@ -128,7 +128,36 @@ namespace euf {
propagate_extract(n); propagate_extract(n);
} }
// enforce concat(v1, v2) = v2*2^|v1| + v1 void bv_plugin::register_node(enode* n) {
m_queue.push_back(n);
m_trail.push_back(new (get_region()) push_back_vector(m_queue));
push_plugin_undo(bv.get_family_id());
}
void bv_plugin::merge_eh(enode* n1, enode* n2) {
m_queue.push_back(enode_pair(n1, n2));
m_trail.push_back(new (get_region()) push_back_vector(m_queue));
push_plugin_undo(bv.get_family_id());
}
void bv_plugin::propagate() {
if (m_qhead == m_queue.size())
return;
m_trail.push_back(new (get_region()) value_trail(m_qhead));
push_plugin_undo(bv.get_family_id());
for (; m_qhead < m_queue.size(); ++m_qhead) {
if (std::holds_alternative<enode*>(m_queue[m_qhead])) {
auto n = *std::get_if<enode*>(&m_queue[m_qhead]);
propagate_register_node(n);
}
else {
auto [a, b] = *std::get_if<enode_pair>(&m_queue[m_qhead]);
propagate_merge(a, b);
}
}
}
// enforce concat(v1, v2) = v1*2^|v2| + v2
void bv_plugin::propagate_values(enode* x) { void bv_plugin::propagate_values(enode* x) {
if (!is_value(x)) if (!is_value(x))
return; return;
@ -142,9 +171,9 @@ namespace euf {
if (is_concat(sib, a, b)) { if (is_concat(sib, a, b)) {
if (!is_value(a) || !is_value(b)) { if (!is_value(a) || !is_value(b)) {
auto val = get_value(x); auto val = get_value(x);
auto v1 = mod2k(val, width(a)); auto val_a = machine_div2k(val, width(b));
auto v2 = machine_div2k(val, width(a)); auto val_b = mod2k(val, width(b));
push_merge(mk_concat(mk_value(v1, width(a)), mk_value(v2, width(b))), x->get_interpreted()); push_merge(mk_concat(mk_value(val_a, width(a)), mk_value(val_b, width(b))), x->get_interpreted());
} }
} }
} }
@ -176,18 +205,18 @@ namespace euf {
if (is_extract(p1, lo_, hi_) && lo_ == lo && hi_ == hi && p1->get_arg(0)->get_root() == arg_r) if (is_extract(p1, lo_, hi_) && lo_ == lo && hi_ == hi && p1->get_arg(0)->get_root() == arg_r)
return; return;
// add the axiom instead of merge(p, mk_extract(arg, lo, hi)), which would require tracking justifications // add the axiom instead of merge(p, mk_extract(arg, lo, hi)), which would require tracking justifications
push_merge(mk_concat(mk_extract(arg, lo, mid), mk_extract(arg, mid + 1, hi)), mk_extract(arg, lo, hi)); push_merge(mk_concat(mk_extract(arg, mid + 1, hi), mk_extract(arg, lo, mid)), mk_extract(arg, lo, hi));
}; };
auto propagate_left = [&](enode* b) { auto propagate_above = [&](enode* b) {
TRACE("bv", tout << "propagate-left " << g.bpp(b) << "\n"); TRACE("bv", tout << "propagate-above " << g.bpp(b) << "\n");
for (enode* sib : enode_class(b)) for (enode* sib : enode_class(b))
if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi1 + 1 == lo2) if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi1 + 1 == lo2)
ensure_concat(lo1, hi1, hi2); ensure_concat(lo1, hi1, hi2);
}; };
auto propagate_right = [&](enode* a) { auto propagate_below = [&](enode* a) {
TRACE("bv", tout << "propagate-right " << g.bpp(a) << "\n"); TRACE("bv", tout << "propagate-below " << g.bpp(a) << "\n");
for (enode* sib : enode_class(a)) for (enode* sib : enode_class(a))
if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi2 + 1 == lo1) if (is_extract(sib, lo2, hi2) && sib->get_arg(0)->get_root() == arg_r && hi2 + 1 == lo1)
ensure_concat(lo2, hi2, hi1); ensure_concat(lo2, hi2, hi1);
@ -196,46 +225,65 @@ namespace euf {
for (enode* p : enode_parents(n)) { for (enode* p : enode_parents(n)) {
if (is_concat(p, a, b)) { if (is_concat(p, a, b)) {
if (a->get_root() == n_r) if (a->get_root() == n_r)
propagate_left(b); propagate_below(b);
if (b->get_root() == n_r) if (b->get_root() == n_r)
propagate_right(a); propagate_above(a);
} }
} }
} }
void bv_plugin::push_undo_split(enode* n) { class bv_plugin::undo_split : public trail {
m_undo_split.push_back(n); bv_plugin& p;
enode* n;
public:
undo_split(bv_plugin& p, enode* n): p(p), n(n) {}
void undo() override {
auto& i = p.info(n);
i.value = nullptr;
i.lo = nullptr;
i.hi = nullptr;
i.cut = null_cut;
}
};
void bv_plugin::push_undo_split(enode* n) {
m_trail.push_back(new (get_region()) undo_split(*this, n));
push_plugin_undo(bv.get_family_id()); push_plugin_undo(bv.get_family_id());
} }
void bv_plugin::undo() { void bv_plugin::undo() {
enode* n = m_undo_split.back(); m_trail.back()->undo();
m_undo_split.pop_back(); m_trail.pop_back();
auto& i = info(n);
i.lo = nullptr;
i.hi = nullptr;
i.cut = null_cut;
} }
void bv_plugin::register_node(enode* n) { void bv_plugin::propagate_register_node(enode* n) {
TRACE("bv", tout << "register " << g.bpp(n) << "\n"); TRACE("bv", tout << "register " << g.bpp(n) << "\n");
auto& i = info(n);
i.value = n;
enode* a, * b; enode* a, * b;
unsigned lo, hi;
if (is_concat(n, a, b)) { if (is_concat(n, a, b)) {
i.lo = a; auto& i = info(n);
i.hi = b; i.value = n;
i.cut = width(a); i.hi = a;
i.lo = b;
i.cut = width(b);
push_undo_split(n); push_undo_split(n);
} }
unsigned lo, hi; else if (is_concat(n) && n->num_args() != 2) {
if (is_extract(n, lo, hi) && (lo != 0 || hi + 1 != width(n->get_arg(0)))) { SASSERT(n->num_args() != 0);
auto last = n->get_arg(n->num_args() - 1);
for (unsigned i = n->num_args() - 1; i-- > 0;)
last = mk_concat(n->get_arg(i), last);
push_merge(last, n);
}
else if (is_extract(n, lo, hi) && (lo != 0 || hi + 1 != width(n->get_arg(0)))) {
enode* arg = n->get_arg(0); enode* arg = n->get_arg(0);
unsigned w = width(arg); unsigned w = width(arg);
if (all_of(enode_parents(arg), [&](enode* p) { unsigned _lo, _hi; return !is_extract(p, _lo, _hi) || _lo != 0 || _hi + 1 != w; })) if (all_of(enode_parents(arg), [&](enode* p) { unsigned _lo, _hi; return !is_extract(p, _lo, _hi) || _lo != 0 || _hi + 1 != w; }))
push_merge(mk_extract(arg, 0, w - 1), arg); push_merge(mk_extract(arg, 0, w - 1), arg);
ensure_slice(arg, lo, hi); ensure_slice(arg, lo, hi);
} }
TRACE("bv", tout << "done register " << g.bpp(n) << "\n");
} }
// //
@ -250,7 +298,8 @@ namespace euf {
SASSERT(ub - lb + 1 == width(r)); SASSERT(ub - lb + 1 == width(r));
if (lb == lo && ub == hi) if (lb == lo && ub == hi)
return; return;
slice_info& i = info(r); slice_info const& i = info(r);
if (!i.lo) { if (!i.lo) {
if (lo > lb) { if (lo > lb) {
split(r, lo - lb); split(r, lo - lb);
@ -287,12 +336,20 @@ namespace euf {
hi += lo1; hi += lo1;
n = n->get_arg(0); n = n->get_arg(0);
} }
if (n->interpreted()) {
auto v = get_value(n);
if (lo > 0)
v = div(v, rational::power_of_two(lo));
if (hi + 1 != width(n))
v = mod(v, rational::power_of_two(hi + 1));
return mk_value(v, hi - lo + 1);
}
return mk(bv.mk_extract(hi, lo, n->get_expr()), 1, &n); return mk(bv.mk_extract(hi, lo, n->get_expr()), 1, &n);
} }
enode* bv_plugin::mk_concat(enode* lo, enode* hi) { enode* bv_plugin::mk_concat(enode* hi, enode* lo) {
enode* args[2] = { lo, hi }; enode* args[2] = { hi, lo };
return mk(bv.mk_concat(lo->get_expr(), hi->get_expr()), 2, args); return mk(bv.mk_concat(hi->get_expr(), lo->get_expr()), 2, args);
} }
void bv_plugin::merge(enode_vector& xs, enode_vector& ys, justification dep) { void bv_plugin::merge(enode_vector& xs, enode_vector& ys, justification dep) {
@ -300,6 +357,7 @@ namespace euf {
SASSERT(!ys.empty()); SASSERT(!ys.empty());
auto x = xs.back(); auto x = xs.back();
auto y = ys.back(); auto y = ys.back();
TRACE("bv", tout << "merge " << g.bpp(x) << " " << g.bpp(y) << "\n");
if (unfold_sub(x, xs)) if (unfold_sub(x, xs))
continue; continue;
else if (unfold_sub(y, ys)) else if (unfold_sub(y, ys))
@ -342,14 +400,13 @@ namespace euf {
SASSERT(0 < cut && cut < w); SASSERT(0 < cut && cut < w);
enode* hi = mk_extract(n, cut, w - 1); enode* hi = mk_extract(n, cut, w - 1);
enode* lo = mk_extract(n, 0, cut - 1); enode* lo = mk_extract(n, 0, cut - 1);
auto& i = info(n); auto& i = info(n);
if (!i.value) i.value = n;
i.value = n;
i.hi = hi; i.hi = hi;
i.lo = lo; i.lo = lo;
i.cut = cut; i.cut = cut;
push_undo_split(n); push_undo_split(n);
push_merge(mk_concat(lo, hi), n); push_merge(mk_concat(hi, lo), n);
} }
void bv_plugin::sub_slices(enode* n, std::function<bool(enode*, unsigned)>& consumer) { void bv_plugin::sub_slices(enode* n, std::function<bool(enode*, unsigned)>& consumer) {
@ -442,9 +499,12 @@ namespace euf {
continue; continue;
offsets.push_back(offs); offsets.push_back(offs);
if (n->get_root() == b->get_root() && offs == offset) { if (n->get_root() == b->get_root() && offs == offset) {
if (n != b)
consumer(n, b);
while (j != UINT_MAX) { while (j != UINT_MAX) {
auto [x, y, j2] = just[j]; auto [x, y, j2] = just[j];
consumer(x, y); if (x != y)
consumer(x, y);
j = j2; j = j2;
} }
for (auto const& [n, offset, j] : m_jtodo) { for (auto const& [n, offset, j] : m_jtodo) {
@ -487,10 +547,10 @@ namespace euf {
} }
std::ostream& bv_plugin::display(std::ostream& out) const { std::ostream& bv_plugin::display(std::ostream& out) const {
out << "bv\n"; out << "bv\n";
for (auto const& i : m_info) for (auto const& i : m_info)
if (i.lo) if (i.lo)
out << g.bpp(i.value) << " cut " << i.cut << " lo " << g.bpp(i.lo) << " hi " << g.bpp(i.hi) << "\n"; out << g.bpp(i.value) << " cut " << i.cut << " lo " << g.bpp(i.lo) << " hi " << g.bpp(i.hi) << "\n";
return out; return out;
} }
} }

27
src/ast/euf/euf_bv_plugin.h
View file

@ -19,6 +19,7 @@ Author:
#pragma once #pragma once
#include "util/trail.h"
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
#include "ast/euf/euf_plugin.h" #include "ast/euf/euf_plugin.h"
@ -40,26 +41,24 @@ namespace euf {
bv_util bv; bv_util bv;
slice_info_vector m_info; // indexed by enode::get_id() slice_info_vector m_info; // indexed by enode::get_id()
enode_vector m_xs, m_ys; enode_vector m_xs, m_ys;
std::function<void(enode*)> m_ensure_th_var;
bool is_concat(enode* n) const { return bv.is_concat(n->get_expr()); } bool is_concat(enode* n) const { return bv.is_concat(n->get_expr()); }
bool is_concat(enode* n, enode*& a, enode*& b) { return is_concat(n) && (a = n->get_arg(0), b = n->get_arg(1), true); } bool is_concat(enode* n, enode*& a, enode*& b) { return is_concat(n) && n->num_args() == 2 && (a = n->get_arg(0), b = n->get_arg(1), true); }
bool is_extract(enode* n, unsigned& lo, unsigned& hi) { expr* body; return bv.is_extract(n->get_expr(), lo, hi, body); } bool is_extract(enode* n, unsigned& lo, unsigned& hi) { expr* body; return bv.is_extract(n->get_expr(), lo, hi, body); }
bool is_extract(enode* n) const { return bv.is_extract(n->get_expr()); } bool is_extract(enode* n) const { return bv.is_extract(n->get_expr()); }
unsigned width(enode* n) const { return bv.get_bv_size(n->get_expr()); } unsigned width(enode* n) const { return bv.get_bv_size(n->get_expr()); }
enode* mk_extract(enode* n, unsigned lo, unsigned hi); enode* mk_extract(enode* n, unsigned lo, unsigned hi);
enode* mk_concat(enode* lo, enode* hi); enode* mk_concat(enode* hi, enode* lo);
enode* mk_value_concat(enode* lo, enode* hi); enode* mk_value_concat(enode* hi, enode* lo);
enode* mk_value(rational const& v, unsigned sz); enode* mk_value(rational const& v, unsigned sz);
unsigned width(enode* n) { return bv.get_bv_size(n->get_expr()); } unsigned width(enode* n) { return bv.get_bv_size(n->get_expr()); }
bool is_value(enode* n) { return n->get_root()->interpreted(); } bool is_value(enode* n) { return n->get_root()->interpreted(); }
rational get_value(enode* n) { rational val; VERIFY(bv.is_numeral(n->get_interpreted()->get_expr(), val)); return val; } rational get_value(enode* n) { rational val; VERIFY(bv.is_numeral(n->get_interpreted()->get_expr(), val)); return val; }
slice_info& info(enode* n) { unsigned id = n->get_id(); m_info.reserve(id + 1); return m_info[id]; } slice_info& info(enode* n) { unsigned id = n->get_id(); m_info.reserve(id + 1); return m_info[id]; }
slice_info& root_info(enode* n) { unsigned id = n->get_root_id(); m_info.reserve(id + 1); return m_info[id]; }
bool has_sub(enode* n) { return !!info(n).lo; } bool has_sub(enode* n) { return !!info(n).lo; }
enode* sub_lo(enode* n) { return info(n).lo; } enode* sub_lo(enode* n) { return info(n).lo; }
enode* sub_hi(enode* n) { return info(n).hi; } enode* sub_hi(enode* n) { return info(n).hi; }
@ -81,8 +80,16 @@ namespace euf {
svector<std::tuple<enode*, unsigned, unsigned>> m_jtodo; svector<std::tuple<enode*, unsigned, unsigned>> m_jtodo;
void clear_offsets(); void clear_offsets();
enode_vector m_undo_split;
ptr_vector<trail> m_trail;
class undo_split;
void push_undo_split(enode* n); void push_undo_split(enode* n);
vector<std::variant<enode*, enode_pair>> m_queue;
unsigned m_qhead = 0;
void propagate_register_node(enode* n);
void propagate_merge(enode* a, enode* b);
public: public:
bv_plugin(egraph& g); bv_plugin(egraph& g);
@ -97,9 +104,11 @@ namespace euf {
void diseq_eh(enode* eq) override {} void diseq_eh(enode* eq) override {}
void propagate() override {} void propagate() override;
void undo() override; void undo() override;
void set_ensure_th_var(std::function<void(enode*)>& f) { m_ensure_th_var = f; }
std::ostream& display(std::ostream& out) const override; std::ostream& display(std::ostream& out) const override;

6
src/ast/euf/euf_egraph.cpp
View file

@ -107,6 +107,8 @@ namespace euf {
void egraph::update_children(enode* n) { void egraph::update_children(enode* n) {
for (enode* child : enode_args(n)) for (enode* child : enode_args(n))
child->get_root()->add_parent(n); child->get_root()->add_parent(n);
for (enode* child : enode_args(n))
SASSERT(child->get_root()->m_parents.back() == n);
m_updates.push_back(update_record(n, update_record::update_children())); m_updates.push_back(update_record(n, update_record::update_children()));
} }
@ -158,7 +160,7 @@ namespace euf {
} }
void egraph::add_th_eq(theory_id id, theory_var v1, theory_var v2, enode* c, enode* r) { void egraph::add_th_eq(theory_id id, theory_var v1, theory_var v2, enode* c, enode* r) {
TRACE("euf_verbose", tout << "eq: " << v1 << " == " << v2 << "\n";); TRACE("euf", tout << "eq: " << v1 << " == " << v2 << " - " << bpp(c) << " == " << bpp(r) << "\n";);
m_new_th_eqs.push_back(th_eq(id, v1, v2, c, r)); m_new_th_eqs.push_back(th_eq(id, v1, v2, c, r));
m_updates.push_back(update_record(update_record::new_th_eq())); m_updates.push_back(update_record(update_record::new_th_eq()));
++m_stats.m_num_th_eqs; ++m_stats.m_num_th_eqs;
@ -442,6 +444,8 @@ namespace euf {
break; break;
case update_record::tag_t::is_update_children: case update_record::tag_t::is_update_children:
for (unsigned i = 0; i < p.r1->num_args(); ++i) { for (unsigned i = 0; i < p.r1->num_args(); ++i) {
CTRACE("euf", (p.r1->m_args[i]->get_root()->m_parents.back() != p.r1),
display(tout << bpp(p.r1->m_args[i]) << " " << bpp(p.r1->m_args[i]->get_root()) << " "););
SASSERT(p.r1->m_args[i]->get_root()->m_parents.back() == p.r1); SASSERT(p.r1->m_args[i]->get_root()->m_parents.back() == p.r1);
p.r1->m_args[i]->get_root()->m_parents.pop_back(); p.r1->m_args[i]->get_root()->m_parents.pop_back();
} }

31
src/ast/euf/euf_egraph.h
View file

@ -192,8 +192,8 @@ namespace euf {
enode_vector m_empty_enodes; enode_vector m_empty_enodes;
unsigned m_num_scopes = 0; unsigned m_num_scopes = 0;
bool m_inconsistent = false; bool m_inconsistent = false;
enode* m_n1 = nullptr; enode *m_n1 = nullptr;
enode* m_n2 = nullptr; enode *m_n2 = nullptr;
justification m_justification; justification m_justification;
unsigned m_new_th_eqs_qhead = 0; unsigned m_new_th_eqs_qhead = 0;
svector<th_eq> m_new_th_eqs; svector<th_eq> m_new_th_eqs;
@ -205,11 +205,11 @@ namespace euf {
uint64_t m_congruence_timestamp = 0; uint64_t m_congruence_timestamp = 0;
std::vector<std::function<void(enode*,enode*)>> m_on_merge; std::vector<std::function<void(enode*,enode*)>> m_on_merge;
std::function<void(enode*,enode*)> m_on_propagate_literal; std::function<void(enode*, enode*)> m_on_propagate_literal;
std::function<void(enode*)> m_on_make; std::function<void(enode*)> m_on_make;
std::function<void(expr*,expr*,expr*)> m_used_eq; std::function<void(expr*,expr*,expr*)> m_used_eq;
std::function<void(app*,app*)> m_used_cc; std::function<void(app*,app*)> m_used_cc;
std::function<void(std::ostream&,void*)> m_display_justification; std::function<void(std::ostream&, void*)> m_display_justification;
void push_eq(enode* r1, enode* n1, unsigned r2_num_parents) { void push_eq(enode* r1, enode* n1, unsigned r2_num_parents) {
m_updates.push_back(update_record(r1, n1, r2_num_parents)); m_updates.push_back(update_record(r1, n1, r2_num_parents));
@ -218,7 +218,7 @@ namespace euf {
// plugin related methods // plugin related methods
void push_plugin_undo(unsigned th_id) { m_updates.push_back(update_record(th_id, update_record::plugin_undo())); } void push_plugin_undo(unsigned th_id) { m_updates.push_back(update_record(th_id, update_record::plugin_undo())); }
void push_merge(enode* a, enode* b, justification j) { m_to_merge.push_back({ a, b, j }); } void push_merge(enode* a, enode* b, justification j) { SASSERT(a->get_sort() == b->get_sort()); m_to_merge.push_back({ a, b, j }); }
void push_merge(enode* a, enode* b, bool comm) { m_to_merge.push_back({ a, b, comm }); } void push_merge(enode* a, enode* b, bool comm) { m_to_merge.push_back({ a, b, comm }); }
void propagate_plugins(); void propagate_plugins();
@ -279,6 +279,7 @@ namespace euf {
void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); } void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); }
void new_diseq(enode* n); void new_diseq(enode* n);
/** /**
\brief propagate set of merges. \brief propagate set of merges.
This call may detect an inconsistency. Then inconsistent() is true. This call may detect an inconsistency. Then inconsistent() is true.
@ -325,13 +326,13 @@ namespace euf {
void set_relevant(enode* n); void set_relevant(enode* n);
void set_default_relevant(bool b) { m_default_relevant = b; } void set_default_relevant(bool b) { m_default_relevant = b; }
void set_on_merge(std::function<void(enode* root,enode* other)> on_merge) { m_on_merge.push_back(std::move(on_merge)); } void set_on_merge(std::function<void(enode* root,enode* other)>& on_merge) { m_on_merge.push_back(on_merge); }
void set_on_propagate(std::function<void(enode* lit,enode* ante)> on_propagate) { m_on_propagate_literal = std::move(on_propagate); } void set_on_propagate(std::function<void(enode* lit,enode* ante)>& on_propagate) { m_on_propagate_literal = on_propagate; }
void set_on_make(std::function<void(enode* n)> on_make) { m_on_make = std::move(on_make); } void set_on_make(std::function<void(enode* n)>& on_make) { m_on_make = on_make; }
void set_used_eq(std::function<void(expr*,expr*,expr*)> used_eq) { m_used_eq = std::move(used_eq); } void set_used_eq(std::function<void(expr*,expr*,expr*)>& used_eq) { m_used_eq = used_eq; }
void set_used_cc(std::function<void(app*,app*)> used_cc) { m_used_cc = std::move(used_cc); } void set_used_cc(std::function<void(app*,app*)>& used_cc) { m_used_cc = used_cc; }
void set_display_justification(std::function<void(std::ostream&, void*)> d) { m_display_justification = std::move(d); } void set_display_justification(std::function<void (std::ostream&, void*)> & d) { m_display_justification = d; }
void begin_explain(); void begin_explain();
void end_explain(); void end_explain();
bool uses_congruence() const { return m_uses_congruence; } bool uses_congruence() const { return m_uses_congruence; }

29
src/sat/smt/arith_axioms.cpp
View file

@ -260,9 +260,6 @@ namespace arith {
if (valy >= sz || valy == 0) if (valy >= sz || valy == 0)
return true; return true;
unsigned k = valy.get_unsigned(); unsigned k = valy.get_unsigned();
rational r = mod(valx * rational::power_of_two(k), N);
if (r == valn)
return true;
sat::literal eq = eq_internalize(n, a.mk_mod(a.mk_mul(_x, a.mk_int(rational::power_of_two(k))), a.mk_int(N))); sat::literal eq = eq_internalize(n, a.mk_mod(a.mk_mul(_x, a.mk_int(rational::power_of_two(k))), a.mk_int(N)));
if (s().value(eq) == l_true) if (s().value(eq) == l_true)
return true; return true;
@ -275,9 +272,6 @@ namespace arith {
if (valy >= sz || valy == 0) if (valy >= sz || valy == 0)
return true; return true;
unsigned k = valy.get_unsigned(); unsigned k = valy.get_unsigned();
rational r = mod(div(valx, rational::power_of_two(k)), N);
if (r == valn)
return true;
sat::literal eq = eq_internalize(n, a.mk_idiv(x, a.mk_int(rational::power_of_two(k)))); sat::literal eq = eq_internalize(n, a.mk_idiv(x, a.mk_int(rational::power_of_two(k))));
if (s().value(eq) == l_true) if (s().value(eq) == l_true)
return true; return true;
@ -290,12 +284,6 @@ namespace arith {
if (valy >= sz || valy == 0) if (valy >= sz || valy == 0)
return true; return true;
unsigned k = valy.get_unsigned(); unsigned k = valy.get_unsigned();
bool signvalx = x >= N/2;
rational valxdiv2k = div(valx, rational::power_of_two(k));
if (signvalx)
valxdiv2k = mod(valxdiv2k - rational::power_of_two(sz - k), N);
if (valn == valxdiv2k)
return true;
sat::literal signx = mk_literal(a.mk_ge(x, a.mk_int(N/2))); sat::literal signx = mk_literal(a.mk_ge(x, a.mk_int(N/2)));
sat::literal eq; sat::literal eq;
expr* xdiv2k; expr* xdiv2k;
@ -334,11 +322,7 @@ namespace arith {
return true; return true;
} }
/*
* 0 <= x&y < 2^sz
* x&y <= x
* x&y <= y
*/
void solver::mk_bv_axiom(app* n) { void solver::mk_bv_axiom(app* n) {
unsigned sz; unsigned sz;
expr* _x, * _y; expr* _x, * _y;
@ -347,10 +331,15 @@ namespace arith {
expr_ref x(a.mk_mod(_x, a.mk_int(N)), m); expr_ref x(a.mk_mod(_x, a.mk_int(N)), m);
expr_ref y(a.mk_mod(_y, a.mk_int(N)), m); expr_ref y(a.mk_mod(_y, a.mk_int(N)), m);
add_clause(mk_literal(a.mk_ge(n, a.mk_int(0))));
add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1))));
if (a.is_band(n)) { if (a.is_band(n)) {
// 0 <= x&y < 2^sz
// x&y <= x
// x&y <= y
// TODO? x = y => x&y = x
add_clause(mk_literal(a.mk_ge(n, a.mk_int(0))));
add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1))));
add_clause(mk_literal(a.mk_le(n, x))); add_clause(mk_literal(a.mk_le(n, x)));
add_clause(mk_literal(a.mk_le(n, y))); add_clause(mk_literal(a.mk_le(n, y)));
} }

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

@ -37,6 +37,7 @@ namespace intblast {
euf::theory_var solver::mk_var(euf::enode* n) { euf::theory_var solver::mk_var(euf::enode* n) {
auto r = euf::th_euf_solver::mk_var(n); auto r = euf::th_euf_solver::mk_var(n);
ctx.attach_th_var(n, this, r); ctx.attach_th_var(n, this, r);
TRACE("bv", tout << "mk-var: v" << r << " " << ctx.bpp(n) << "\n";);
return r; return r;
} }
@ -97,16 +98,16 @@ namespace intblast {
ensure_translated(y); ensure_translated(y);
m_args.reset(); m_args.reset();
m_args.push_back(a.mk_sub(translated(x), translated(y))); m_args.push_back(a.mk_sub(translated(x), translated(y)));
set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0))); set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0)));
} }
m_preds.push_back(e); m_preds.push_back(e);
ctx.push(push_back_vector(m_preds)); ctx.push(push_back_vector(m_preds));
} }
void solver::set_translated(expr* e, expr* r) { void solver::set_translated(expr* e, expr* r) {
SASSERT(r); SASSERT(r);
SASSERT(!is_translated(e)); SASSERT(!is_translated(e));
m_translate.setx(e->get_id(), r); m_translate.setx(e->get_id(), r);
ctx.push(set_vector_idx_trail(m_translate, e->get_id())); ctx.push(set_vector_idx_trail(m_translate, e->get_id()));
} }
@ -147,7 +148,7 @@ namespace intblast {
auto a = expr2literal(e); auto a = expr2literal(e);
auto b = mk_literal(r); auto b = mk_literal(r);
ctx.mark_relevant(b); ctx.mark_relevant(b);
TRACE("intblast", tout << "add-predicate-axiom: " << mk_bounded_pp(e, m) << " \n" << r << "\n"); // verbose_stream() << "add-predicate-axiom: " << mk_pp(e, m) << " == " << r << "\n";
add_equiv(a, b); add_equiv(a, b);
} }
return true; return true;
@ -156,7 +157,6 @@ namespace intblast {
bool solver::unit_propagate() { bool solver::unit_propagate() {
return add_bound_axioms() || add_predicate_axioms(); return add_bound_axioms() || add_predicate_axioms();
} }
void solver::ensure_translated(expr* e) { void solver::ensure_translated(expr* e) {
if (m_translate.get(e->get_id(), nullptr)) if (m_translate.get(e->get_id(), nullptr))
return; return;
@ -178,10 +178,96 @@ namespace intblast {
} }
} }
std::stable_sort(todo.begin(), todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); }); std::stable_sort(todo.begin(), todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); });
for (expr* e : todo) for (expr* e : todo)
translate_expr(e); translate_expr(e);
} }
lbool solver::check_axiom(sat::literal_vector const& lits) {
sat::literal_vector core;
for (auto lit : lits)
core.push_back(~lit);
return check_core(core, {});
}
lbool solver::check_propagation(sat::literal lit, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) {
sat::literal_vector core;
core.append(lits);
core.push_back(~lit);
return check_core(core, eqs);
}
lbool solver::check_core(sat::literal_vector const& lits, euf::enode_pair_vector const& eqs) {
m_core.reset();
m_vars.reset();
m_is_plugin = false;
m_solver = mk_smt2_solver(m, s.params(), symbol::null);
for (unsigned i = 0; i < m_translate.size(); ++i)
m_translate[i] = nullptr;
expr_ref_vector es(m), original_es(m);
for (auto lit : lits)
es.push_back(ctx.literal2expr(lit));
for (auto [a, b] : eqs)
es.push_back(m.mk_eq(a->get_expr(), b->get_expr()));
original_es.append(es);
lbool r;
if (false) {
r = m_solver->check_sat(es);
}
else {
translate(es);
for (auto e : m_vars) {
auto v = translated(e);
auto b = rational::power_of_two(bv.get_bv_size(e));
m_solver->assert_expr(a.mk_le(a.mk_int(0), v));
m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
}
for (unsigned i = 0; i < es.size(); ++i) {
expr_ref tmp(es.get(i), m);
ctx.get_rewriter()(tmp);
es[i] = tmp;
}
IF_VERBOSE(2, verbose_stream() << "check\n" << original_es << "\n");
IF_VERBOSE(2,
{
m_solver->push();
m_solver->assert_expr(es);
m_solver->display(verbose_stream()) << "(check-sat)\n";
m_solver->pop(1);
});
r = m_solver->check_sat(es);
}
m_solver->collect_statistics(m_stats);
IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n");
if (r == l_true) {
IF_VERBOSE(0,
model_ref mdl;
m_solver->get_model(mdl);
verbose_stream() << original_es << "\n";
verbose_stream() << *mdl << "\n";
verbose_stream() << es << "\n";
m_solver->display(verbose_stream()););
SASSERT(false);
}
m_solver = nullptr;
return r;
}
lbool solver::check_solver_state() { lbool solver::check_solver_state() {
sat::literal_vector literals; sat::literal_vector literals;
uint_set selected; uint_set selected;
@ -291,6 +377,8 @@ namespace intblast {
for (expr* e : es) { for (expr* e : es) {
if (is_translated(e)) if (is_translated(e))
continue; continue;
if (visited.is_marked(e))
continue;
sorted.push_back(e); sorted.push_back(e);
visited.mark(e); visited.mark(e);
} }
@ -304,6 +392,7 @@ namespace intblast {
sorted.push_back(arg); sorted.push_back(arg);
} }
} }
} }
else if (is_quantifier(e)) { else if (is_quantifier(e)) {
quantifier* q = to_quantifier(e); quantifier* q = to_quantifier(e);
@ -334,7 +423,7 @@ namespace intblast {
es[i] = translated(es.get(i)); es[i] = translated(es.get(i));
} }
sat::check_result solver::check() { sat::check_result solver::check() {
// ensure that bv2int is injective // ensure that bv2int is injective
for (auto e : m_bv2int) { for (auto e : m_bv2int) {
euf::enode* n = expr2enode(e); euf::enode* n = expr2enode(e);
@ -346,12 +435,10 @@ namespace intblast {
continue; continue;
if (sib->get_arg(0)->get_root() == r1) if (sib->get_arg(0)->get_root() == r1)
continue; continue;
if (sib->get_arg(0)->get_sort() != n->get_arg(0)->get_sort()) auto a = eq_internalize(n, sib);
continue; auto b = eq_internalize(sib->get_arg(0), n->get_arg(0));
auto a = eq_internalize(n, sib); ctx.mark_relevant(a);
auto b = eq_internalize(sib->get_arg(0), n->get_arg(0)); ctx.mark_relevant(b);
ctx.mark_relevant(a);
ctx.mark_relevant(b);
add_clause(~a, b, nullptr); add_clause(~a, b, nullptr);
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
} }
@ -369,27 +456,40 @@ namespace intblast {
auto nBv2int = ctx.get_enode(bv2int); auto nBv2int = ctx.get_enode(bv2int);
auto nxModN = ctx.get_enode(xModN); auto nxModN = ctx.get_enode(xModN);
if (nBv2int->get_root() != nxModN->get_root()) { if (nBv2int->get_root() != nxModN->get_root()) {
auto a = eq_internalize(nBv2int, nxModN); auto a = eq_internalize(nBv2int, nxModN);
ctx.mark_relevant(a); ctx.mark_relevant(a);
add_unit(a); add_unit(a);
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
} }
} }
return sat::check_result::CR_DONE; return sat::check_result::CR_DONE;
}
bool solver::is_bounded(expr* x, rational const& N) {
return any_of(m_vars, [&](expr* v) {
return is_translated(v) && translated(v) == x && bv.get_bv_size(v) <= N;
});
}
bool solver::is_non_negative(expr* bv_expr, expr* e) {
auto N = rational::power_of_two(bv.get_bv_size(bv_expr));
rational r;
if (a.is_numeral(e, r))
return r >= 0;
if (is_bounded(e, N))
return true;
expr* x, * y;
if (a.is_mul(e, x, y))
return is_non_negative(bv_expr, x) && is_non_negative(bv_expr, y);
if (a.is_add(e, x, y))
return is_non_negative(bv_expr, x) && is_non_negative(bv_expr, y);
return false;
} }
expr* solver::umod(expr* bv_expr, unsigned i) { expr* solver::umod(expr* bv_expr, unsigned i) {
expr* x = arg(i); expr* x = arg(i);
rational r;
rational N = bv_size(bv_expr); rational N = bv_size(bv_expr);
if (a.is_numeral(x, r)) { return amod(bv_expr, x, N);
if (0 <= r && r < N)
return x;
return a.mk_int(mod(r, N));
}
if (any_of(m_vars, [&](expr* v) { return translated(v) == x && bv.get_bv_size(v) == bv.get_bv_size(bv_expr); }))
return x;
return a.mk_mod(x, a.mk_int(N));
} }
expr* solver::smod(expr* bv_expr, unsigned i) { expr* solver::smod(expr* bv_expr, unsigned i) {
@ -399,7 +499,61 @@ namespace intblast {
rational r; rational r;
if (a.is_numeral(x, r)) if (a.is_numeral(x, r))
return a.mk_int(mod(r + shift, N)); return a.mk_int(mod(r + shift, N));
return a.mk_mod(a.mk_add(x, a.mk_int(shift)), a.mk_int(N)); return amod(bv_expr, add(x, a.mk_int(shift)), N);
}
expr_ref solver::mul(expr* x, expr* y) {
expr_ref _x(x, m), _y(y, m);
if (a.is_zero(x))
return _x;
if (a.is_zero(y))
return _y;
if (a.is_one(x))
return _y;
if (a.is_one(y))
return _x;
rational v1, v2;
if (a.is_numeral(x, v1) && a.is_numeral(y, v2))
return expr_ref(a.mk_int(v1 * v2), m);
_x = a.mk_mul(x, y);
return _x;
}
expr_ref solver::add(expr* x, expr* y) {
expr_ref _x(x, m), _y(y, m);
if (a.is_zero(x))
return _y;
if (a.is_zero(y))
return _x;
rational v1, v2;
if (a.is_numeral(x, v1) && a.is_numeral(y, v2))
return expr_ref(a.mk_int(v1 + v2), m);
_x = a.mk_add(x, y);
return _x;
}
/*
* Perform simplifications that are claimed sound when the bit-vector interpretations of
* mod/div always guard the mod and dividend to be non-zero.
* Potentially shady area is for arithmetic expressions created by int2bv.
* They will be guarded by a modulus which dose not disappear.
*/
expr* solver::amod(expr* bv_expr, expr* x, rational const& N) {
rational v;
expr* r, *c, * t, * e;
if (m.is_ite(x, c, t, e))
r = m.mk_ite(c, amod(bv_expr, t, N), amod(bv_expr, e, N));
else if (a.is_idiv(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N && is_non_negative(bv_expr, e))
r = x;
else if (a.is_mod(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N)
r = x;
else if (a.is_numeral(x, v))
r = a.mk_int(mod(v, N));
else if (is_bounded(x, N))
r = x;
else
r = a.mk_mod(x, a.mk_int(N));
return r;
} }
rational solver::bv_size(expr* bv_expr) { rational solver::bv_size(expr* bv_expr) {
@ -483,8 +637,7 @@ namespace intblast {
m_args[i] = bv.mk_int2bv(bv.get_bv_size(e->get_arg(i)), m_args.get(i)); m_args[i] = bv.mk_int2bv(bv.get_bv_size(e->get_arg(i)), m_args.get(i));
if (has_bv_sort) if (has_bv_sort)
m_vars.push_back(e); m_vars.push_back(e);
if (m_is_plugin) { if (m_is_plugin) {
expr* r = m.mk_app(f, m_args); expr* r = m.mk_app(f, m_args);
if (has_bv_sort) { if (has_bv_sort) {
@ -505,7 +658,7 @@ namespace intblast {
f = g; f = g;
m_pinned.push_back(f); m_pinned.push_back(f);
} }
set_translated(e, m.mk_app(f, m_args)); set_translated(e, m.mk_app(f, m_args));
} }
void solver::translate_bv(app* e) { void solver::translate_bv(app* e) {
@ -532,15 +685,15 @@ namespace intblast {
auto N = bv_size(e); auto N = bv_size(e);
auto A = rational::power_of_two(sz - n); auto A = rational::power_of_two(sz - n);
auto B = rational::power_of_two(n); auto B = rational::power_of_two(n);
auto hi = a.mk_mul(r, a.mk_int(A)); auto hi = mul(r, a.mk_int(A));
auto lo = a.mk_mod(a.mk_idiv(umod(e, 0), a.mk_int(B)), a.mk_int(A)); auto lo = amod(e, a.mk_idiv(umod(e, 0), a.mk_int(B)), A);
r = a.mk_add(hi, lo); r = add(hi, lo);
} }
return r; return r;
}; };
expr* bv_expr = e; expr* bv_expr = e;
expr* r = nullptr; expr_ref r(m);
auto const& args = m_args; auto const& args = m_args;
switch (e->get_decl_kind()) { switch (e->get_decl_kind()) {
case OP_BADD: case OP_BADD:
@ -573,7 +726,6 @@ namespace intblast {
r = a.mk_le(smod(bv_expr, 0), smod(bv_expr, 1)); r = a.mk_le(smod(bv_expr, 0), smod(bv_expr, 1));
break; break;
case OP_SGEQ: case OP_SGEQ:
bv_expr = e->get_arg(0);
r = a.mk_ge(smod(bv_expr, 0), smod(bv_expr, 1)); r = a.mk_ge(smod(bv_expr, 0), smod(bv_expr, 1));
break; break;
case OP_SLT: case OP_SLT:
@ -589,12 +741,13 @@ namespace intblast {
break; break;
case OP_CONCAT: { case OP_CONCAT: {
unsigned sz = 0; unsigned sz = 0;
expr_ref new_arg(m);
for (unsigned i = args.size(); i-- > 0;) { for (unsigned i = args.size(); i-- > 0;) {
expr* old_arg = e->get_arg(i); expr* old_arg = e->get_arg(i);
expr* new_arg = umod(old_arg, i); new_arg = umod(old_arg, i);
if (sz > 0) { if (sz > 0) {
new_arg = a.mk_mul(new_arg, a.mk_int(rational::power_of_two(sz))); new_arg = mul(new_arg, a.mk_int(rational::power_of_two(sz)));
r = a.mk_add(r, new_arg); r = add(r, new_arg);
} }
else else
r = new_arg; r = new_arg;
@ -606,10 +759,9 @@ namespace intblast {
unsigned lo, hi; unsigned lo, hi;
expr* old_arg; expr* old_arg;
VERIFY(bv.is_extract(e, lo, hi, old_arg)); VERIFY(bv.is_extract(e, lo, hi, old_arg));
r = arg(0);
if (lo > 0) if (lo > 0)
r = a.mk_idiv(umod(old_arg, 0), a.mk_int(rational::power_of_two(lo))); r = a.mk_idiv(r, a.mk_int(rational::power_of_two(lo)));
else
r = arg(0);
break; break;
} }
case OP_BV_NUM: { case OP_BV_NUM: {
@ -627,32 +779,32 @@ namespace intblast {
} }
case OP_BUDIV: case OP_BUDIV:
case OP_BUDIV_I: { case OP_BUDIV_I: {
expr* x = umod(e, 0), * y = umod(e, 1); expr* x = arg(0), * y = umod(e, 1);
r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(-1), a.mk_idiv(x, y)); r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(-1), a.mk_idiv(x, y));
break; break;
} }
case OP_BUMUL_NO_OVFL: { case OP_BUMUL_NO_OVFL: {
bv_expr = e->get_arg(0); bv_expr = e->get_arg(0);
r = a.mk_lt(a.mk_mul(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(bv_size(bv_expr))); r = a.mk_lt(mul(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(bv_size(bv_expr)));
break; break;
} }
case OP_BSHL: { case OP_BSHL: {
if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1))) if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1)))
r = a.mk_shl(bv.get_bv_size(e), arg(0), arg(1)); r = a.mk_shl(bv.get_bv_size(e), arg(0),arg(1));
else { else {
expr* x = arg(0), * y = umod(e, 1); expr* x = arg(0), * y = umod(e, 1);
r = a.mk_int(0); r = a.mk_int(0);
IF_VERBOSE(2, verbose_stream() << "shl " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); IF_VERBOSE(2, verbose_stream() << "shl " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
for (unsigned i = 0; i < bv.get_bv_size(e); ++i) for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_mul(x, a.mk_int(rational::power_of_two(i))), r); r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), mul(x, a.mk_int(rational::power_of_two(i))), r);
} }
break; break;
} }
case OP_BNOT: case OP_BNOT:
r = bnot(arg(0)); r = bnot(arg(0));
break; break;
case OP_BLSHR: case OP_BLSHR:
if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1))) if (!a.is_numeral(arg(0)) && !a.is_numeral(arg(1)))
r = a.mk_lshr(bv.get_bv_size(e), arg(0), arg(1)); r = a.mk_lshr(bv.get_bv_size(e), arg(0), arg(1));
else { else {
expr* x = arg(0), * y = umod(e, 1); expr* x = arg(0), * y = umod(e, 1);
@ -662,11 +814,11 @@ namespace intblast {
r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r); r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r);
} }
break; break;
case OP_BASHR: case OP_BASHR:
if (!a.is_numeral(arg(1))) if (!a.is_numeral(arg(1)))
r = a.mk_ashr(bv.get_bv_size(e), arg(0), arg(1)); r = a.mk_ashr(bv.get_bv_size(e), arg(0), arg(1));
else { else {
// //
// ashr(x, y) // ashr(x, y)
// if y = k & x >= 0 -> x / 2^k // if y = k & x >= 0 -> x / 2^k
@ -674,15 +826,15 @@ namespace intblast {
// //
unsigned sz = bv.get_bv_size(e); unsigned sz = bv.get_bv_size(e);
rational N = bv_size(e); rational N = bv_size(e);
expr* x = umod(e, 0), * y = umod(e, 1); expr* x = umod(e, 0), *y = umod(e, 1);
expr* signx = a.mk_ge(x, a.mk_int(N / 2)); expr* signx = a.mk_ge(x, a.mk_int(N / 2));
r = m.mk_ite(signx, a.mk_int(-1), a.mk_int(0)); r = m.mk_ite(signx, a.mk_int(- 1), a.mk_int(0));
IF_VERBOSE(1, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); IF_VERBOSE(1, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i))); expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));
r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), r = m.mk_ite(m.mk_eq(y, a.mk_int(i)),
m.mk_ite(signx, a.mk_add(d, a.mk_int(-rational::power_of_two(sz - i))), d), m.mk_ite(signx, add(d, a.mk_int(- rational::power_of_two(sz-i))), d),
r); r);
} }
} }
break; break;
@ -691,7 +843,7 @@ namespace intblast {
IF_VERBOSE(2, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); IF_VERBOSE(2, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
r = arg(0); r = arg(0);
for (unsigned i = 1; i < args.size(); ++i) for (unsigned i = 1; i < args.size(); ++i)
r = a.mk_sub(a.mk_add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i))); r = a.mk_sub(add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i)));
break; break;
} }
case OP_BNAND: case OP_BNAND:
@ -709,7 +861,7 @@ namespace intblast {
r = arg(0); r = arg(0);
for (unsigned i = 1; i < args.size(); ++i) { for (unsigned i = 1; i < args.size(); ++i) {
expr* q = arg(i); expr* q = arg(i);
r = a.mk_sub(a.mk_add(r, q), a.mk_mul(a.mk_int(2), a.mk_band(sz, r, q))); r = a.mk_sub(add(r, q), mul(a.mk_int(2), a.mk_band(sz, r, q)));
} }
if (e->get_decl_kind() == OP_BXNOR) if (e->get_decl_kind() == OP_BXNOR)
r = bnot(r); r = bnot(r);
@ -747,11 +899,11 @@ namespace intblast {
r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(0)); r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(0));
break; break;
case OP_BSMOD_I: case OP_BSMOD_I:
case OP_BSMOD: { case OP_BSMOD: {
expr* x = umod(e, 0), * y = umod(e, 1); expr* x = umod(e, 0), *y = umod(e, 1);
rational N = bv_size(e); rational N = bv_size(e);
expr* signx = a.mk_ge(x, a.mk_int(N / 2)); expr* signx = a.mk_ge(x, a.mk_int(N/2));
expr* signy = a.mk_ge(y, a.mk_int(N / 2)); expr* signy = a.mk_ge(y, a.mk_int(N/2));
expr* u = a.mk_mod(x, y); expr* u = a.mk_mod(x, y);
// u = 0 -> 0 // u = 0 -> 0
// y = 0 -> x // y = 0 -> x
@ -759,14 +911,14 @@ namespace intblast {
// x < 0, y >= 0 -> y - u // x < 0, y >= 0 -> y - u
// x >= 0, y < 0 -> y + u // x >= 0, y < 0 -> y + u
// x >= 0, y >= 0 -> u // x >= 0, y >= 0 -> u
r = a.mk_uminus(u); r = a.mk_uminus(u);
r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), a.mk_add(u, y), r); r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), add(u, y), r);
r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r); r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r);
r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r); r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r);
r = m.mk_ite(m.mk_eq(u, a.mk_int(0)), a.mk_int(0), r); r = m.mk_ite(m.mk_eq(u, a.mk_int(0)), a.mk_int(0), r);
r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r); r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r);
break; break;
} }
case OP_BSDIV_I: case OP_BSDIV_I:
case OP_BSDIV: { case OP_BSDIV: {
// d = udiv(abs(x), abs(y)) // d = udiv(abs(x), abs(y))
@ -800,9 +952,9 @@ namespace intblast {
expr* absy = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y); expr* absy = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
expr* d = a.mk_idiv(absx, absy); expr* d = a.mk_idiv(absx, absy);
d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d)); d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
r = a.mk_sub(x, a.mk_mul(d, y)); r = a.mk_sub(x, mul(d, y));
r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r); r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r);
break; break;
} }
case OP_ROTATE_LEFT: { case OP_ROTATE_LEFT: {
auto n = e->get_parameter(0).get_int(); auto n = e->get_parameter(0).get_int();
@ -815,11 +967,11 @@ namespace intblast {
r = rotate_left(sz - n); r = rotate_left(sz - n);
break; break;
} }
case OP_EXT_ROTATE_LEFT: { case OP_EXT_ROTATE_LEFT: {
unsigned sz = bv.get_bv_size(e); unsigned sz = bv.get_bv_size(e);
expr* y = umod(e, 1); expr* y = umod(e, 1);
r = a.mk_int(0); r = a.mk_int(0);
for (unsigned i = 0; i < sz; ++i) for (unsigned i = 0; i < sz; ++i)
r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(i), r); r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(i), r);
break; break;
} }
@ -827,7 +979,7 @@ namespace intblast {
unsigned sz = bv.get_bv_size(e); unsigned sz = bv.get_bv_size(e);
expr* y = umod(e, 1); expr* y = umod(e, 1);
r = a.mk_int(0); r = a.mk_int(0);
for (unsigned i = 0; i < sz; ++i) for (unsigned i = 0; i < sz; ++i)
r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(sz - i), r); r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(sz - i), r);
break; break;
} }
@ -838,9 +990,9 @@ namespace intblast {
rational N = bv_size(e->get_arg(0)); rational N = bv_size(e->get_arg(0));
rational N0 = N; rational N0 = N;
for (unsigned i = 1; i < n; ++i) for (unsigned i = 1; i < n; ++i)
r = a.mk_add(a.mk_mul(a.mk_int(N), x), r), N *= N0; r = add(mul(a.mk_int(N), x), r), N *= N0;
break; break;
} }
case OP_BREDOR: { case OP_BREDOR: {
r = umod(e->get_arg(0), 0); r = umod(e->get_arg(0), 0);
r = m.mk_not(m.mk_eq(r, a.mk_int(0))); r = m.mk_not(m.mk_eq(r, a.mk_int(0)));
@ -864,8 +1016,15 @@ namespace intblast {
bool has_bv_arg = any_of(*e, [&](expr* arg) { return bv.is_bv(arg); }); bool has_bv_arg = any_of(*e, [&](expr* arg) { return bv.is_bv(arg); });
if (has_bv_arg) { if (has_bv_arg) {
expr* bv_expr = e->get_arg(0); expr* bv_expr = e->get_arg(0);
m_args[0] = a.mk_sub(arg(0), arg(1)); rational N = rational::power_of_two(bv.get_bv_size(bv_expr));
set_translated(e, m.mk_eq(umod(bv_expr, 0), a.mk_int(0))); if (a.is_numeral(arg(0)) || a.is_numeral(arg(1)) ||
is_bounded(arg(0), N) || is_bounded(arg(1), N)) {
set_translated(e, m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)));
}
else {
m_args[0] = a.mk_sub(arg(0), arg(1));
set_translated(e, m.mk_eq(umod(bv_expr, 0), a.mk_int(0)));
}
} }
else else
set_translated(e, m.mk_eq(arg(0), arg(1))); set_translated(e, m.mk_eq(arg(0), arg(1)));
@ -874,8 +1033,8 @@ namespace intblast {
set_translated(e, m.mk_ite(arg(0), arg(1), arg(2))); set_translated(e, m.mk_ite(arg(0), arg(1), arg(2)));
else if (m_is_plugin) else if (m_is_plugin)
set_translated(e, e); set_translated(e, e);
else else
set_translated(e, m.mk_app(e->get_decl(), m_args)); set_translated(e, m.mk_app(e->get_decl(), m_args));
} }
rational solver::get_value(expr* e) const { rational solver::get_value(expr* e) const {
@ -903,12 +1062,6 @@ namespace intblast {
if (!is_app(n->get_expr())) if (!is_app(n->get_expr()))
return false; return false;
app* e = to_app(n->get_expr()); app* e = to_app(n->get_expr());
expr *th, * el, * c;
if (m.is_ite(e, c, th, el)) {
dep.add(n, expr2enode(th)->get_root());
dep.add(n, expr2enode(el)->get_root());
return true;
}
if (n->num_args() == 0) { if (n->num_args() == 0) {
dep.insert(n, nullptr); dep.insert(n, nullptr);
return true; return true;
@ -925,7 +1078,6 @@ namespace intblast {
void solver::add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values) { void solver::add_value_solver(euf::enode* n, model& mdl, expr_ref_vector& values) {
expr* e = n->get_expr(); expr* e = n->get_expr();
SASSERT(bv.is_bv(e)); SASSERT(bv.is_bv(e));
if (bv.is_numeral(e)) { if (bv.is_numeral(e)) {
values.setx(n->get_root_id(), e); values.setx(n->get_root_id(), e);
return; return;
@ -947,15 +1099,6 @@ namespace intblast {
void solver::add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values) { void solver::add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values) {
expr_ref value(m); expr_ref value(m);
expr* e = n->get_expr(), *c, *th, *el;
while (m.is_ite(e, c, th, el)) {
auto thn = expr2enode(th);
if (thn->get_root() == n->get_root())
e = th;
else
e = el;
n = expr2enode(e);
}
if (n->interpreted()) if (n->interpreted())
value = n->get_expr(); value = n->get_expr();
else if (to_app(n->get_expr())->get_family_id() == bv.get_family_id()) { else if (to_app(n->get_expr())->get_family_id() == bv.get_family_id()) {
@ -975,35 +1118,12 @@ namespace intblast {
rational r; rational r;
VERIFY(av.get_value(b2i->get_expr(), r)); VERIFY(av.get_value(b2i->get_expr(), r));
value = bv.mk_numeral(r, bv.get_bv_size(n->get_expr())); value = bv.mk_numeral(r, bv.get_bv_size(n->get_expr()));
verbose_stream() << ctx.bpp(n) << " := " << value << "\n";
} }
values.set(n->get_root_id(), value); values.set(n->get_root_id(), value);
TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n"); TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n");
} }
void solver::finalize_model(model& mdl) {
for (auto n : ctx.get_egraph().nodes()) {
expr* e = n->get_expr();
if (!bv.is_bv(e))
continue;
if (!is_translated(e))
continue;
expr* f = translated(e);
rational r1, r2;
expr_ref val1 = mdl(e);
expr_ref val2 = mdl(f);
if (bv.is_numeral(val1, r1) && a.is_numeral(val2, r2) && r1 != r2) {
rational N = rational::power_of_two(bv.get_bv_size(e));
r2 = mod(r2, N);
if (r1 == r2)
continue;
verbose_stream() << "value mismatch : " << mk_bounded_pp(e, m) << " := " << val1 << "\n";
verbose_stream() << mk_bounded_pp(f, m) << " := " << r2 << "\n";
for (expr* arg : *to_app(e))
verbose_stream() << mk_bounded_pp(arg, m) << " := " << mdl(arg) << "\n";
}
}
}
sat::literal_vector const& solver::unsat_core() { sat::literal_vector const& solver::unsat_core() {
return m_core; return m_core;
} }

11
src/sat/smt/intblast_solver.h
View file

@ -73,6 +73,11 @@ namespace intblast {
expr* umod(expr* bv_expr, unsigned i); expr* umod(expr* bv_expr, unsigned i);
expr* smod(expr* bv_expr, unsigned i); expr* smod(expr* bv_expr, unsigned i);
bool is_bounded(expr* v, rational const& N);
bool is_non_negative(expr* bv_expr, expr* e);
expr_ref mul(expr* x, expr* y);
expr_ref add(expr* x, expr* y);
expr* amod(expr* bv_expr, expr* x, rational const& N);
rational bv_size(expr* bv_expr); rational bv_size(expr* bv_expr);
void translate_expr(expr* e); void translate_expr(expr* e);
@ -100,6 +105,10 @@ namespace intblast {
~solver() override {} ~solver() override {}
lbool check_axiom(sat::literal_vector const& lits);
lbool check_core(sat::literal_vector const& lits, euf::enode_pair_vector const& eqs);
lbool check_propagation(sat::literal lit, sat::literal_vector const& lits, euf::enode_pair_vector const& eqs);
lbool check_solver_state(); lbool check_solver_state();
sat::literal_vector const& unsat_core(); sat::literal_vector const& unsat_core();
@ -108,8 +117,6 @@ namespace intblast {
bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override; bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
void finalize_model(model& mdl) override;
std::ostream& display(std::ostream& out) const override; std::ostream& display(std::ostream& out) const override;
void collect_statistics(statistics& st) const override; void collect_statistics(statistics& st) const override;