#include "smt/smt_context.h"
#include "smt/theory_intblast.h"
#include "smt/smt_model_generator.h"
namespace smt {
void theory_intblast::translator_trail::push(push_back_vector<expr_ref_vector> const& c) {
ctx.push_trail(c);
}
void theory_intblast::translator_trail::push(push_back_vector<ptr_vector<app>> const& c) {
ctx.push_trail(c);
}
void theory_intblast::translator_trail::push_idx(set_vector_idx_trail<expr_ref_vector> const& c) {
ctx.push_trail(c);
}
theory_intblast::theory_intblast(context& ctx):
theory(ctx, ctx.get_manager().mk_family_id("bv")),
m_trail(ctx),
m_translator(m, m_trail),
bv(m),
a(m)
{}
final_check_status theory_intblast::final_check_eh(unsigned) {
for (auto e : m_translator.bv2int()) {
auto* n = ctx.get_enode(e);
auto* r1 = n->get_arg(0)->get_root();
for (auto sib : *n) {
if (sib == n)
continue;
if (!bv.is_ubv2int(sib->get_expr()))
continue;
if (sib->get_arg(0)->get_root() == r1)
continue;
if (bv.get_bv_size(r1->get_expr()) != bv.get_bv_size(sib->get_arg(0)->get_expr()))
continue;
auto a = mk_eq(n->get_expr(), sib->get_expr(), false);
auto b = mk_eq(sib->get_arg(0)->get_expr(), n->get_arg(0)->get_expr(), false);
ctx.mark_as_relevant(a);
ctx.mark_as_relevant(b);
ctx.mk_th_axiom(m_id, ~a, b);
return final_check_status::FC_CONTINUE;
}
}
for (auto e : m_translator.int2bv()) {
auto n = ctx.get_enode(e);
auto x = n->get_arg(0)->get_expr();
auto bv2int = bv.mk_ubv2int(e);
ctx.internalize(bv2int, false);
auto N = rational::power_of_two(bv.get_bv_size(e));
auto xModN = a.mk_mod(x, a.mk_int(N));
ctx.internalize(xModN, false);
auto nBv2int = ctx.get_enode(bv2int);
auto nxModN = ctx.get_enode(xModN);
if (nBv2int->get_root() != nxModN->get_root()) {
auto a = mk_eq(nBv2int->get_expr(), nxModN->get_expr(), false);
ctx.mark_as_relevant(a);
ctx.mk_th_axiom(m_id, 1, &a);
return final_check_status::FC_CONTINUE;
}
}
return final_check_status::FC_DONE;
}
bool theory_intblast::add_bound_axioms() {
auto const& vars = m_translator.vars();
if (m_vars_qhead == vars.size())
return false;
ctx.push_trail(value_trail(m_vars_qhead));
for (; m_vars_qhead < vars.size(); ++m_vars_qhead) {
auto v = vars[m_vars_qhead];
auto w = m_translator.translated(v);
auto sz = rational::power_of_two(bv.get_bv_size(v->get_sort()));
auto lo = mk_literal(a.mk_ge(w, a.mk_int(0)));
auto hi = mk_literal(a.mk_le(w, a.mk_int(sz - 1)));
ctx.mark_as_relevant(lo);
ctx.mark_as_relevant(hi);
ctx.mk_th_axiom(m_id, 1, &lo);
ctx.mk_th_axiom(m_id, 1, &hi);
}
return true;
}
bool theory_intblast::add_predicate_axioms() {
auto const& preds = m_translator.preds();
if (m_preds_qhead == preds.size())
return false;
ctx.push_trail(value_trail(m_preds_qhead));
for (; m_preds_qhead < preds.size(); ++m_preds_qhead) {
expr* e = preds[m_preds_qhead];
expr_ref r(m_translator.translated(e), m);
ctx.get_rewriter()(r);
auto a = mk_literal(e);
auto b = mk_literal(r);
ctx.mark_as_relevant(a);
ctx.mark_as_relevant(b);
ctx.mk_th_axiom(m_id, ~a, b);
ctx.mk_th_axiom(m_id, a, ~b);
}
return true;
}
bool theory_intblast::add_bv2int_axioms() {
auto const& bv2int = m_translator.bv2int();
if (m_bv2int_qhead == bv2int.size())
return false;
ctx.push_trail(value_trail(m_bv2int_qhead));
for (; m_bv2int_qhead < bv2int.size(); ++m_bv2int_qhead) {
app* e = bv2int[m_bv2int_qhead];
expr_ref r(m_translator.translated(e), m);
if (r.get() == e)
continue;
ctx.get_rewriter()(r);
auto eq = mk_eq(e, r, false);
ctx.mark_as_relevant(eq);
ctx.mk_th_axiom(m_id, 1, &eq);
}
return true;
}
bool theory_intblast::can_propagate() {
return m_preds_qhead < m_translator.preds().size() || m_vars_qhead < m_translator.vars().size() ||
m_bv2int_qhead < m_translator.bv2int().size();
}
void theory_intblast::propagate() {
add_bound_axioms();
add_predicate_axioms();
add_bv2int_axioms();
}
bool theory_intblast::internalize_atom(app * atom, bool gate_ctx) {
return internalize_term(atom);
}
void theory_intblast::apply_sort_cnstr(enode* n, sort* s) {
SASSERT(bv.is_bv_sort(s));
if (!is_attached_to_var(n)) {
m_translator.internalize_bv(n->get_app());
auto v = mk_var(n);
ctx.attach_th_var(n, this, v);
}
}
bool theory_intblast::internalize_term(app* term) {
ctx.internalize(term->get_args(), term->get_num_args(), false);
m_translator.internalize_bv(term);
enode* n;
if (!ctx.e_internalized(term))
n = ctx.mk_enode(term, false, false, false);
else
n = ctx.get_enode(term);
if (!is_attached_to_var(n)) {
auto v = mk_var(n);
ctx.attach_th_var(n, this, v);
}
if (m.is_bool(term)) {
literal l(ctx.mk_bool_var(term));
ctx.set_var_theory(l.var(), get_id());
}
return true;
}
void theory_intblast::internalize_eq_eh(app * atom, bool_var v) {
m_translator.translate_eq(atom);
}
void theory_intblast::new_eq_eh(theory_var v1, theory_var v2) {
expr* x = get_enode(v1)->get_expr();
expr* y = get_enode(v2)->get_expr();
if (!bv.is_bv(x) || !bv.is_bv(y))
return;
expr_ref eq(m.mk_eq(x, y), m);
m_translator.translate_eq(eq);
auto lit1 = mk_literal(eq);
auto lit2 = mk_literal(m_translator.translated(eq));
ctx.mark_as_relevant(lit1);
ctx.mark_as_relevant(lit2);
ctx.mk_th_axiom(m_id, ~lit1, lit2);
}
void theory_intblast::init_model(model_generator& mg) {
m_factory = alloc(bv_factory, m);
mg.register_factory(m_factory);
}
model_value_proc* theory_intblast::mk_value(enode* n, model_generator& mg) {
expr* e = n->get_expr();
SASSERT(bv.is_bv(e));
rational r;
expr* ie = nullptr;
expr_ref val(m);
if (!bv.is_numeral(e, r)) {
for (enode* sib : *n) {
ie = m_translator.translated(sib->get_expr());
if (ctx.e_internalized(ie) && ctx.get_value(ctx.get_enode(ie), val) && a.is_numeral(val, r))
break;
}
}
return alloc(expr_wrapper_proc, m_factory->mk_num_value(r, bv.get_bv_size(e)));
}
}