mirror of
https://github.com/Z3Prover/z3
synced 2026-02-20 07:24:40 +00:00
0e6b3a922a
Add commands: (prefer <formula>) - will instruct case split queue to assign formula to true. - prefer commands added within a scope are forgotten after leaving the scope. (reset-preferences) - resets asserted preferences. Has to be invoked at base level. This provides functionality related to MathSAT and based on an ask by Tomáš Kolárik who is integrating the functionality with OpenSMT2
2060 lines
84 KiB
C++
2060 lines
84 KiB
C++
/*++
|
|
Copyright (c) 2006 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
theory_bv.cpp
|
|
|
|
Abstract:
|
|
|
|
<abstract>
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2008-06-06.
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
#include "smt/smt_context.h"
|
|
#include "smt/theory_bv.h"
|
|
#include "ast/ast_ll_pp.h"
|
|
#include "ast/ast_pp.h"
|
|
#include "ast/bv_decl_plugin.h"
|
|
#include "smt/smt_model_generator.h"
|
|
#include "util/stats.h"
|
|
|
|
#define ENABLE_QUOT_REM_ENCODING 0
|
|
|
|
namespace smt {
|
|
|
|
theory_var theory_bv::mk_var(enode * n) {
|
|
theory_var r = theory::mk_var(n);
|
|
m_find.mk_var();
|
|
m_bits.push_back(literal_vector());
|
|
m_wpos.push_back(0);
|
|
m_zero_one_bits.push_back(zero_one_bits());
|
|
ctx.attach_th_var(n, this, r);
|
|
return r;
|
|
}
|
|
|
|
app * theory_bv::mk_bit2bool(app * bv, unsigned idx) {
|
|
parameter p(idx);
|
|
expr * args[1] = {bv};
|
|
return get_manager().mk_app(get_id(), OP_BIT2BOOL, 1, &p, 1, args);
|
|
}
|
|
|
|
void theory_bv::mk_bits(theory_var v) {
|
|
enode * n = get_enode(v);
|
|
app * owner = n->get_expr();
|
|
unsigned bv_size = get_bv_size(n);
|
|
bool is_relevant = ctx.is_relevant(n);
|
|
literal_vector & bits = m_bits[v];
|
|
bits.reset();
|
|
m_bits_expr.reset();
|
|
|
|
for (unsigned i = 0; i < bv_size; i++)
|
|
m_bits_expr.push_back(mk_bit2bool(owner, i));
|
|
ctx.internalize(m_bits_expr.data(), bv_size, true);
|
|
|
|
for (unsigned i = 0; i < bv_size; i++) {
|
|
bool_var b = ctx.get_bool_var(m_bits_expr[i]);
|
|
bits.push_back(literal(b));
|
|
if (is_relevant && !ctx.is_relevant(b)) {
|
|
ctx.mark_as_relevant(b);
|
|
}
|
|
}
|
|
|
|
TRACE(bv, tout << "v" << v << " #" << owner->get_id() << "\n";
|
|
for (unsigned i = 0; i < bv_size; i++)
|
|
tout << mk_bounded_pp(m_bits_expr[i], m) << "\n";
|
|
);
|
|
|
|
}
|
|
|
|
class mk_atom_trail : public trail {
|
|
theory_bv& th;
|
|
bool_var m_var;
|
|
public:
|
|
mk_atom_trail(theory_bv& th, bool_var v):th(th), m_var(v) {}
|
|
void undo() override {
|
|
theory_bv::atom * a = th.get_bv2a(m_var);
|
|
a->~atom();
|
|
th.erase_bv2a(m_var);
|
|
}
|
|
};
|
|
|
|
void theory_bv::mk_bit2bool(app * n) {
|
|
SASSERT(!ctx.b_internalized(n));
|
|
|
|
TRACE(bv, tout << "bit2bool: " << mk_pp(n, ctx.get_manager()) << "\n";);
|
|
expr* first_arg = n->get_arg(0);
|
|
|
|
if (!ctx.e_internalized(first_arg)) {
|
|
// This may happen if bit2bool(x) is in a conflict
|
|
// clause that is being reinitialized, and x was not reinitialized
|
|
// yet.
|
|
// So, we internalize x (i.e., arg)
|
|
ctx.internalize(first_arg, false);
|
|
SASSERT(ctx.e_internalized(first_arg));
|
|
// In most cases, when x is internalized, its bits are created.
|
|
// They are created because x is a bit-vector operation or apply_sort_cnstr is invoked.
|
|
// However, there is an exception. The method apply_sort_cnstr is not invoked for ite-terms.
|
|
// So, I execute get_var on the enode attached to first_arg.
|
|
// This will force a theory variable to be created if it does not already exist.
|
|
// This will also force the creation of all bits for x.
|
|
enode * first_arg_enode = ctx.get_enode(first_arg);
|
|
get_var(first_arg_enode);
|
|
}
|
|
|
|
enode * arg = ctx.get_enode(first_arg);
|
|
// The argument was already internalized, but it may not have a theory variable associated with it.
|
|
// For example, for ite-terms the method apply_sort_cnstr is not invoked.
|
|
// See comment in the then-branch.
|
|
theory_var v_arg = arg->get_th_var(get_id());
|
|
if (v_arg == null_theory_var) {
|
|
// The method get_var will create a theory variable for arg.
|
|
// As a side-effect the bits for arg will also be created.
|
|
get_var(arg);
|
|
SASSERT(ctx.b_internalized(n));
|
|
}
|
|
else if (!ctx.b_internalized(n)) {
|
|
SASSERT(v_arg != null_theory_var);
|
|
bool_var bv = ctx.mk_bool_var(n);
|
|
ctx.set_var_theory(bv, get_id());
|
|
bit_atom * a = new (get_region()) bit_atom();
|
|
insert_bv2a(bv, a);
|
|
m_trail_stack.push(mk_atom_trail(*this, bv));
|
|
unsigned idx = n->get_decl()->get_parameter(0).get_int();
|
|
SASSERT(a->m_occs == 0);
|
|
a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
|
|
// Fix for #2182, and SPACER bit-vector
|
|
if (idx < m_bits[v_arg].size()) {
|
|
ctx.mk_th_axiom(get_id(), m_bits[v_arg][idx], literal(bv, true));
|
|
ctx.mk_th_axiom(get_id(), ~m_bits[v_arg][idx], literal(bv, false));
|
|
}
|
|
}
|
|
// axiomatize bit2bool on constants.
|
|
rational val;
|
|
unsigned sz;
|
|
if (m_util.is_numeral(first_arg, val, sz)) {
|
|
rational bit;
|
|
unsigned idx = n->get_decl()->get_parameter(0).get_int();
|
|
div(val, rational::power_of_two(idx), bit);
|
|
mod(bit, rational(2), bit);
|
|
literal lit = ctx.get_literal(n);
|
|
if (bit.is_zero()) lit.neg();
|
|
ctx.mark_as_relevant(lit);
|
|
ctx.mk_th_axiom(get_id(), 1, &lit);
|
|
}
|
|
}
|
|
|
|
void theory_bv::process_args(app * n) {
|
|
ctx.internalize(n->get_args(), n->get_num_args(), false);
|
|
}
|
|
|
|
enode * theory_bv::mk_enode(app * n) {
|
|
enode * e;
|
|
if (ctx.e_internalized(n)) {
|
|
e = ctx.get_enode(n);
|
|
}
|
|
else {
|
|
e = ctx.mk_enode(n, !params().m_bv_reflect, false, params().m_bv_cc);
|
|
mk_var(e);
|
|
}
|
|
// SASSERT(e->get_th_var(get_id()) != null_theory_var);
|
|
return e;
|
|
}
|
|
|
|
theory_var theory_bv::get_var(enode * n) {
|
|
theory_var v = n->get_th_var(get_id());
|
|
if (v == null_theory_var) {
|
|
v = mk_var(n);
|
|
mk_bits(v);
|
|
}
|
|
return v;
|
|
}
|
|
|
|
enode * theory_bv::get_arg(enode * n, unsigned idx) {
|
|
if (params().m_bv_reflect) {
|
|
return n->get_arg(idx);
|
|
}
|
|
else {
|
|
app * arg = to_app(n->get_expr()->get_arg(idx));
|
|
SASSERT(ctx.e_internalized(arg));
|
|
return ctx.get_enode(arg);
|
|
}
|
|
}
|
|
|
|
inline theory_var theory_bv::get_arg_var(enode * n, unsigned idx) {
|
|
return get_var(get_arg(n, idx));
|
|
}
|
|
|
|
void theory_bv::get_bits(theory_var v, expr_ref_vector & r) {
|
|
literal_vector & bits = m_bits[v];
|
|
for (literal lit : bits) {
|
|
expr_ref l(get_manager());
|
|
ctx.literal2expr(lit, l);
|
|
r.push_back(std::move(l));
|
|
}
|
|
}
|
|
|
|
inline void theory_bv::get_bits(enode * n, expr_ref_vector & r) {
|
|
get_bits(get_var(n), r);
|
|
}
|
|
|
|
inline void theory_bv::get_arg_bits(enode * n, unsigned idx, expr_ref_vector & r) {
|
|
get_bits(get_arg_var(n, idx), r);
|
|
}
|
|
|
|
inline void theory_bv::get_arg_bits(app * n, unsigned idx, expr_ref_vector & r) {
|
|
app * arg = to_app(n->get_arg(idx));
|
|
SASSERT(ctx.e_internalized(arg));
|
|
get_bits(ctx.get_enode(arg), r);
|
|
}
|
|
|
|
class add_var_pos_trail : public trail {
|
|
theory_bv::bit_atom * m_atom;
|
|
public:
|
|
add_var_pos_trail(theory_bv::bit_atom * a):m_atom(a) {}
|
|
void undo() override {
|
|
SASSERT(m_atom->m_occs);
|
|
m_atom->m_occs = m_atom->m_occs->m_next;
|
|
}
|
|
};
|
|
|
|
void theory_bv::add_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx) {
|
|
m_prop_diseqs.push_back(bv_diseq(v1, v2, idx));
|
|
ctx.push_trail(push_back_vector<svector<bv_diseq>>(m_prop_diseqs));
|
|
}
|
|
|
|
/**
|
|
\brief v1[idx] = ~v2[idx], then v1 /= v2 is a theory axiom.
|
|
*/
|
|
void theory_bv::assert_new_diseq_axiom(theory_var v1, theory_var v2, unsigned idx) {
|
|
SASSERT(m_bits[v1][idx] == ~m_bits[v2][idx]);
|
|
TRACE(bv_diseq_axiom, tout << "found new diseq axiom\n"; display_var(tout, v1); display_var(tout, v2););
|
|
// found new disequality
|
|
m_stats.m_num_diseq_static++;
|
|
app * e1 = get_expr(v1);
|
|
app * e2 = get_expr(v2);
|
|
expr_ref eq(m.mk_eq(e1, e2), m);
|
|
literal l = ~mk_literal(eq);
|
|
std::function<expr*(void)> logfn = [&]() {
|
|
return m.mk_implies(m.mk_eq(mk_bit2bool(e1, idx), m.mk_not(mk_bit2bool(e2, idx))), m.mk_not(eq));
|
|
};
|
|
scoped_trace_stream ts(*this, logfn);
|
|
ctx.mk_th_axiom(get_id(), 1, &l);
|
|
if (ctx.relevancy()) {
|
|
relevancy_eh * eh = ctx.mk_relevancy_eh(pair_relevancy_eh(e1, e2, eq));
|
|
ctx.add_relevancy_eh(e1, eh);
|
|
ctx.add_relevancy_eh(e2, eh);
|
|
}
|
|
}
|
|
|
|
void theory_bv::register_true_false_bit(theory_var v, unsigned idx) {
|
|
SASSERT(m_bits[v][idx] == true_literal || m_bits[v][idx] == false_literal);
|
|
bool is_true = (m_bits[v][idx] == true_literal);
|
|
zero_one_bits & bits = m_zero_one_bits[v];
|
|
bits.push_back(zero_one_bit(v, idx, is_true));
|
|
}
|
|
|
|
/**
|
|
\brief v[idx] = ~v'[idx], then v /= v' is a theory axiom.
|
|
*/
|
|
void theory_bv::find_new_diseq_axioms(var_pos_occ * occs, theory_var v, unsigned idx) {
|
|
literal l = m_bits[v][idx];
|
|
l.neg();
|
|
while (occs) {
|
|
theory_var v2 = occs->m_var;
|
|
unsigned idx2 = occs->m_idx;
|
|
if (idx == idx2 && m_bits[v2][idx2] == l && get_bv_size(v2) == get_bv_size(v))
|
|
add_new_diseq_axiom(v, v2, idx);
|
|
occs = occs->m_next;
|
|
}
|
|
}
|
|
|
|
/**
|
|
\brief Add bit l to the given variable.
|
|
*/
|
|
void theory_bv::add_bit(theory_var v, literal l) {
|
|
literal_vector & bits = m_bits[v];
|
|
unsigned idx = bits.size();
|
|
bits.push_back(l);
|
|
if (l.var() == true_bool_var) {
|
|
register_true_false_bit(v, idx);
|
|
}
|
|
else {
|
|
theory_id th_id = ctx.get_var_theory(l.var());
|
|
TRACE(init_bits, tout << l << " " << th_id << "\n";);
|
|
if (th_id == get_id()) {
|
|
atom * a = get_bv2a(l.var());
|
|
SASSERT(a && a->is_bit());
|
|
bit_atom * b = static_cast<bit_atom*>(a);
|
|
find_new_diseq_axioms(b->m_occs, v, idx);
|
|
m_trail_stack.push(add_var_pos_trail(b));
|
|
b->m_occs = new (get_region()) var_pos_occ(v, idx, b->m_occs);
|
|
}
|
|
else if (th_id == null_theory_id) {
|
|
ctx.set_var_theory(l.var(), get_id());
|
|
SASSERT(ctx.get_var_theory(l.var()) == get_id());
|
|
bit_atom * b = new (get_region()) bit_atom();
|
|
insert_bv2a(l.var(), b);
|
|
m_trail_stack.push(mk_atom_trail(*this, l.var()));
|
|
SASSERT(b->m_occs == 0);
|
|
b->m_occs = new (get_region()) var_pos_occ(v, idx);
|
|
}
|
|
}
|
|
}
|
|
|
|
void theory_bv::simplify_bit(expr * s, expr_ref & r) {
|
|
// proof_ref p(get_manager());
|
|
// if (ctx.at_base_level())
|
|
// ctx.get_rewriter()(s, r, p);
|
|
// else
|
|
r = s;
|
|
}
|
|
|
|
void theory_bv::init_bits(enode * n, expr_ref_vector const & bits) {
|
|
theory_var v = n->get_th_var(get_id());
|
|
SASSERT(v != null_theory_var);
|
|
unsigned sz = bits.size();
|
|
SASSERT(get_bv_size(n) == sz);
|
|
m_bits[v].reset();
|
|
|
|
ctx.internalize(bits.data(), sz, true);
|
|
|
|
for (unsigned i = 0; i < sz; i++) {
|
|
expr * bit = bits.get(i);
|
|
literal l = ctx.get_literal(bit);
|
|
TRACE(init_bits, tout << "bit " << i << " of #" << n->get_owner_id() << "\n" << mk_bounded_pp(bit, m) << "\n";);
|
|
add_bit(v, l);
|
|
}
|
|
find_wpos(v);
|
|
}
|
|
|
|
/**
|
|
\brief Find an unassigned bit for m_wpos[v], if such bit cannot be found invoke fixed_var_eh
|
|
*/
|
|
void theory_bv::find_wpos(theory_var v) {
|
|
literal_vector const & bits = m_bits[v];
|
|
unsigned sz = bits.size();
|
|
unsigned & wpos = m_wpos[v];
|
|
unsigned init = wpos;
|
|
for (; wpos < sz; wpos++) {
|
|
TRACE(find_wpos, tout << "curr bit: " << bits[wpos] << "\n";);
|
|
if (ctx.get_assignment(bits[wpos]) == l_undef) {
|
|
TRACE(find_wpos, tout << "moved wpos of v" << v << " to " << wpos << "\n";);
|
|
return;
|
|
}
|
|
}
|
|
wpos = 0;
|
|
for (; wpos < init; wpos++) {
|
|
if (ctx.get_assignment(bits[wpos]) == l_undef) {
|
|
TRACE(find_wpos, tout << "moved wpos of v" << v << " to " << wpos << "\n";);
|
|
return;
|
|
}
|
|
}
|
|
TRACE(find_wpos, tout << "v" << v << " is a fixed variable.\n";);
|
|
fixed_var_eh(v);
|
|
}
|
|
|
|
class fixed_eq_justification : public justification {
|
|
theory_bv & m_th;
|
|
theory_var m_var1;
|
|
theory_var m_var2;
|
|
|
|
void mark_bits(conflict_resolution & cr, literal_vector const & bits) {
|
|
context & ctx = cr.get_context();
|
|
for (literal lit : bits) {
|
|
if (lit.var() != true_bool_var) {
|
|
if (ctx.get_assignment(lit) == l_true)
|
|
cr.mark_literal(lit);
|
|
else
|
|
cr.mark_literal(~lit);
|
|
}
|
|
}
|
|
}
|
|
|
|
void get_proof(conflict_resolution & cr, literal l, ptr_buffer<proof> & prs, bool & visited) {
|
|
if (l.var() == true_bool_var)
|
|
return;
|
|
proof * pr = nullptr;
|
|
if (cr.get_context().get_assignment(l) == l_true)
|
|
pr = cr.get_proof(l);
|
|
else
|
|
pr = cr.get_proof(~l);
|
|
if (pr)
|
|
prs.push_back(pr);
|
|
else
|
|
visited = false;
|
|
}
|
|
|
|
public:
|
|
fixed_eq_justification(theory_bv & th, theory_var v1, theory_var v2):
|
|
m_th(th), m_var1(v1), m_var2(v2) {
|
|
}
|
|
|
|
void get_antecedents(conflict_resolution & cr) override {
|
|
mark_bits(cr, m_th.m_bits[m_var1]);
|
|
mark_bits(cr, m_th.m_bits[m_var2]);
|
|
}
|
|
|
|
proof * mk_proof(conflict_resolution & cr) override {
|
|
ptr_buffer<proof> prs;
|
|
context & ctx = cr.get_context();
|
|
bool visited = true;
|
|
literal_vector const & bits1 = m_th.m_bits[m_var1];
|
|
literal_vector const & bits2 = m_th.m_bits[m_var2];
|
|
literal_vector::const_iterator it1 = bits1.begin();
|
|
literal_vector::const_iterator it2 = bits2.begin();
|
|
literal_vector::const_iterator end1 = bits1.end();
|
|
for (; it1 != end1; ++it1, ++it2) {
|
|
get_proof(cr, *it1, prs, visited);
|
|
get_proof(cr, *it2, prs, visited);
|
|
}
|
|
if (!visited)
|
|
return nullptr;
|
|
expr * fact = ctx.mk_eq_atom(m_th.get_enode(m_var1)->get_expr(), m_th.get_enode(m_var2)->get_expr());
|
|
ast_manager & m = ctx.get_manager();
|
|
return m.mk_th_lemma(get_from_theory(), fact, prs.size(), prs.data());
|
|
}
|
|
|
|
theory_id get_from_theory() const override {
|
|
return m_th.get_id();
|
|
}
|
|
|
|
char const * get_name() const override { return "bv-fixed-eq"; }
|
|
|
|
};
|
|
|
|
void theory_bv::add_fixed_eq(theory_var v1, theory_var v2) {
|
|
|
|
if (v1 > v2)
|
|
std::swap(v1, v2);
|
|
|
|
unsigned act = m_eq_activity[hash_u_u(v1, v2) & 0xFF]++;
|
|
if ((act & 0xFF) != 0xFF) {
|
|
return;
|
|
}
|
|
++m_stats.m_num_eq_dynamic;
|
|
app* o1 = get_enode(v1)->get_expr();
|
|
app* o2 = get_enode(v2)->get_expr();
|
|
literal oeq = mk_eq(o1, o2, true);
|
|
ctx.mark_as_relevant(oeq);
|
|
|
|
unsigned sz = get_bv_size(v1);
|
|
TRACE(bv,
|
|
tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << " "
|
|
<< ctx.get_scope_level() << "\n";);
|
|
literal_vector eqs;
|
|
for (unsigned i = 0; i < sz; ++i) {
|
|
literal l1 = m_bits[v1][i];
|
|
literal l2 = m_bits[v2][i];
|
|
expr_ref e1(m), e2(m);
|
|
e1 = mk_bit2bool(o1, i);
|
|
e2 = mk_bit2bool(o2, i);
|
|
literal eq = mk_eq(e1, e2, true);
|
|
std::function<expr*()> logfn = [&]() {
|
|
return m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_not(ctx.bool_var2expr(oeq.var())));
|
|
};
|
|
scoped_trace_stream st(*this, logfn);
|
|
ctx.mk_th_axiom(get_id(), l1, ~l2, ~eq);
|
|
ctx.mk_th_axiom(get_id(), ~l1, l2, ~eq);
|
|
ctx.mk_th_axiom(get_id(), l1, l2, eq);
|
|
ctx.mk_th_axiom(get_id(), ~l1, ~l2, eq);
|
|
ctx.mk_th_axiom(get_id(), eq, ~oeq);
|
|
eqs.push_back(~eq);
|
|
}
|
|
eqs.push_back(oeq);
|
|
ctx.mk_th_axiom(get_id(), eqs.size(), eqs.data());
|
|
}
|
|
|
|
void theory_bv::fixed_var_eh(theory_var v) {
|
|
numeral val;
|
|
VERIFY(get_fixed_value(v, val));
|
|
enode* n = get_enode(v);
|
|
if (ctx.watches_fixed(n)) {
|
|
expr_ref num(m_util.mk_numeral(val, n->get_expr()->get_sort()), m);
|
|
literal_vector& lits = m_tmp_literals;
|
|
lits.reset();
|
|
for (literal b : m_bits[v]) {
|
|
if (ctx.get_assignment(b) == l_false)
|
|
b.neg();
|
|
lits.push_back(b);
|
|
}
|
|
ctx.assign_fixed(n, num, lits);
|
|
}
|
|
unsigned sz = get_bv_size(v);
|
|
value_sort_pair key(val, sz);
|
|
theory_var v2;
|
|
if (m_fixed_var_table.find(key, v2)) {
|
|
numeral val2;
|
|
if (v2 < static_cast<int>(get_num_vars()) && is_bv(v2) &&
|
|
get_bv_size(v2) == sz && get_fixed_value(v2, val2) && val == val2) {
|
|
if (get_enode(v)->get_root() != get_enode(v2)->get_root()) {
|
|
SASSERT(get_bv_size(v) == get_bv_size(v2));
|
|
TRACE(fixed_var_eh, tout << "detected equality: v" << v << " = v" << v2 << "\n";
|
|
display_var(tout, v);
|
|
display_var(tout, v2););
|
|
m_stats.m_num_th2core_eq++;
|
|
add_fixed_eq(v, v2);
|
|
justification * js = ctx.mk_justification(fixed_eq_justification(*this, v, v2));
|
|
ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js));
|
|
m_fixed_var_table.insert(key, v2);
|
|
}
|
|
}
|
|
else {
|
|
// the original fixed variable v2 was deleted or it is not fixed anymore.
|
|
m_fixed_var_table.erase(key);
|
|
m_fixed_var_table.insert(key, v);
|
|
}
|
|
}
|
|
else {
|
|
m_fixed_var_table.insert(key, v);
|
|
}
|
|
}
|
|
|
|
bool theory_bv::is_fixed_propagated(theory_var v, expr_ref& val, literal_vector& lits) {
|
|
numeral r;
|
|
enode* n = get_enode(v);
|
|
if (!get_fixed_value(v, r))
|
|
return false;
|
|
val = m_util.mk_numeral(r, n->get_sort());
|
|
for (literal b : m_bits[v]) {
|
|
if (ctx.get_assignment(b) == l_false)
|
|
b.neg();
|
|
lits.push_back(b);
|
|
}
|
|
return true;
|
|
}
|
|
|
|
bool theory_bv::get_fixed_value(theory_var v, numeral & result) const {
|
|
result.reset();
|
|
unsigned i = 0;
|
|
for (literal b : m_bits[v]) {
|
|
switch (ctx.get_assignment(b)) {
|
|
case l_false:
|
|
break;
|
|
case l_undef:
|
|
return false;
|
|
case l_true: {
|
|
for (unsigned j = m_power2.size(); j <= i; ++j)
|
|
m_power2.push_back(m_bb.power(j));
|
|
result += m_power2[i];
|
|
break;
|
|
}
|
|
}
|
|
++i;
|
|
}
|
|
return true;
|
|
}
|
|
|
|
bool theory_bv::get_fixed_value(app* x, numeral & result) const {
|
|
CTRACE(bv, !ctx.e_internalized(x), tout << "not internalized " << mk_pp(x, m) << "\n";);
|
|
if (!ctx.e_internalized(x)) return false;
|
|
enode * e = ctx.get_enode(x);
|
|
theory_var v = e->get_th_var(get_id());
|
|
return get_fixed_value(v, result);
|
|
}
|
|
|
|
|
|
void theory_bv::internalize_num(app * n) {
|
|
SASSERT(!ctx.e_internalized(n));
|
|
numeral val;
|
|
unsigned sz = 0;
|
|
VERIFY(m_util.is_numeral(n, val, sz));
|
|
enode * e = mk_enode(n);
|
|
// internalizer is marking enodes as interpreted whenever the associated ast is a value and a constant.
|
|
// e->mark_as_interpreted();
|
|
theory_var v = e->get_th_var(get_id());
|
|
expr_ref_vector bits(m);
|
|
m_bb.num2bits(val, sz, bits);
|
|
SASSERT(bits.size() == sz);
|
|
literal_vector & c_bits = m_bits[v];
|
|
for (unsigned i = 0; i < sz; i++) {
|
|
expr * l = bits.get(i);
|
|
if (m.is_true(l)) {
|
|
c_bits.push_back(true_literal);
|
|
}
|
|
else {
|
|
SASSERT(m.is_false(l));
|
|
c_bits.push_back(false_literal);
|
|
}
|
|
register_true_false_bit(v, i);
|
|
}
|
|
fixed_var_eh(v);
|
|
}
|
|
|
|
void theory_bv::internalize_mkbv(app* n) {
|
|
expr_ref_vector bits(m);
|
|
process_args(n);
|
|
enode * e = mk_enode(n);
|
|
bits.append(n->get_num_args(), n->get_args());
|
|
init_bits(e, bits);
|
|
}
|
|
|
|
void theory_bv::internalize_bv2int(app* n) {
|
|
SASSERT(!ctx.e_internalized(n));
|
|
TRACE(bv, tout << mk_bounded_pp(n, m) << "\n";);
|
|
process_args(n);
|
|
mk_enode(n);
|
|
m_bv2int.push_back(ctx.get_enode(n));
|
|
ctx.push_trail(push_back_vector<enode_vector>(m_bv2int));
|
|
if (!ctx.relevancy())
|
|
assert_bv2int_axiom(n);
|
|
}
|
|
|
|
|
|
void theory_bv::assert_bv2int_axiom(app * n) {
|
|
//
|
|
// create the axiom:
|
|
// n = bv2int(k) = ite(bit2bool(k[sz-1],2^{sz-1},0) + ... + ite(bit2bool(k[0],1,0))
|
|
//
|
|
SASSERT(ctx.e_internalized(n));
|
|
SASSERT(m_util.is_ubv2int(n));
|
|
TRACE(bv2int_bug, tout << "bv2int:\n" << mk_pp(n, m) << "\n";);
|
|
sort * int_sort = n->get_sort();
|
|
app * k = to_app(n->get_arg(0));
|
|
SASSERT(m_util.is_bv_sort(k->get_sort()));
|
|
expr_ref_vector k_bits(m);
|
|
enode * k_enode = mk_enode(k);
|
|
get_bits(k_enode, k_bits);
|
|
unsigned sz = m_util.get_bv_size(k);
|
|
expr_ref_vector args(m);
|
|
expr_ref zero(m_autil.mk_numeral(numeral(0), int_sort), m);
|
|
numeral num(1);
|
|
for (unsigned i = 0; i < sz; ++i) {
|
|
// Remark: A previous version of this method was using
|
|
//
|
|
// expr* b = mk_bit2bool(k,i);
|
|
//
|
|
// This is not correct. The predicate bit2bool is an
|
|
// internal construct, and it was not meant for building
|
|
// axioms directly. It is used to represent the bits of a
|
|
// constant, and in some cases the bits of a complicated
|
|
// bit-vector expression. In most cases, the bits of a
|
|
// composite bit-vector expression T are just boolean
|
|
// combinations of bit2bool atoms of the bit-vector
|
|
// constants contained in T. So, instead of using
|
|
// mk_bit2bool to access a particular bit of T, we should
|
|
// use the method get_bits.
|
|
//
|
|
expr * b = k_bits.get(i);
|
|
expr_ref n(m_autil.mk_numeral(num, int_sort), m);
|
|
args.push_back(m.mk_ite(b, n, zero));
|
|
num *= numeral(2);
|
|
}
|
|
expr_ref sum(m_autil.mk_add(sz, args.data()), m);
|
|
th_rewriter rw(m);
|
|
rw(sum);
|
|
literal l(mk_eq(n, sum, false));
|
|
TRACE(bv,
|
|
tout << mk_pp(n, m) << "\n";
|
|
tout << mk_pp(sum, m) << "\n";
|
|
ctx.display_literal_verbose(tout, l);
|
|
tout << "\n";
|
|
);
|
|
|
|
ctx.mark_as_relevant(l);
|
|
scoped_trace_stream _ts(*this, l);
|
|
ctx.mk_th_axiom(get_id(), 1, &l);
|
|
}
|
|
|
|
void theory_bv::internalize_int2bv(app* n) {
|
|
SASSERT(!ctx.e_internalized(n));
|
|
SASSERT(n->get_num_args() == 1);
|
|
process_args(n);
|
|
mk_enode(n);
|
|
theory_var v = ctx.get_enode(n)->get_th_var(get_id());
|
|
mk_bits(v);
|
|
enode* k = ctx.get_enode(n->get_arg(0));
|
|
if (!is_attached_to_var(k))
|
|
mk_var(k);
|
|
|
|
if (!ctx.relevancy())
|
|
assert_int2bv_axiom(n);
|
|
}
|
|
|
|
void theory_bv::assert_int2bv_axiom(app* n) {
|
|
//
|
|
// create the axiom:
|
|
// bv2int(n) = e mod 2^bit_width
|
|
// where n = int2bv(e)
|
|
//
|
|
// Create the axioms:
|
|
// bit2bool(i,n) == ((e div 2^i) mod 2 != 0)
|
|
// for i = 0,.., sz-1
|
|
//
|
|
SASSERT(ctx.e_internalized(n));
|
|
SASSERT(m_util.is_int2bv(n));
|
|
|
|
parameter param(m_autil.mk_int());
|
|
expr* n_expr = n;
|
|
expr* e = n->get_arg(0);
|
|
expr_ref lhs(m), rhs(m);
|
|
lhs = m.mk_app(get_id(), OP_UBV2INT, 1, ¶m, 1, &n_expr);
|
|
unsigned sz = m_util.get_bv_size(n);
|
|
numeral mod = power(numeral(2), sz);
|
|
rhs = m_autil.mk_mod(e, m_autil.mk_numeral(mod, true));
|
|
|
|
literal l(mk_eq(lhs, rhs, false));
|
|
ctx.mark_as_relevant(l);
|
|
{
|
|
scoped_trace_stream _ts(*this, l);
|
|
ctx.mk_th_axiom(get_id(), 1, &l);
|
|
}
|
|
|
|
TRACE(bv,
|
|
tout << mk_pp(lhs, m) << " == \n";
|
|
tout << mk_pp(rhs, m) << "\n";
|
|
);
|
|
|
|
expr_ref_vector n_bits(m);
|
|
enode * n_enode = mk_enode(n);
|
|
get_bits(n_enode, n_bits);
|
|
|
|
for (unsigned i = 0; i < sz; ++i) {
|
|
numeral div = power(numeral(2), i);
|
|
mod = numeral(2);
|
|
expr_ref div_rhs((i == 0) ? e : m_autil.mk_idiv(e, m_autil.mk_numeral(div, true)), m);
|
|
rhs = m_autil.mk_mod(div_rhs, m_autil.mk_numeral(mod, true));
|
|
rhs = ctx.mk_eq_atom(rhs, m_autil.mk_int(1));
|
|
lhs = n_bits.get(i);
|
|
TRACE(bv, tout << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";);
|
|
l = literal(mk_eq(lhs, rhs, false));
|
|
ctx.mark_as_relevant(l);
|
|
{
|
|
scoped_trace_stream _st(*this, l);
|
|
ctx.mk_th_axiom(get_id(), 1, &l);
|
|
}
|
|
{
|
|
// 0 < e < 2^i => e div 2^i = 0
|
|
expr_ref zero(m_autil.mk_int(0), m);
|
|
literal a = mk_literal(m_autil.mk_ge(e, m_autil.mk_int(div)));
|
|
literal b = mk_literal(m_autil.mk_ge(e, zero));
|
|
literal c = mk_eq(div_rhs, zero, false);
|
|
ctx.mark_as_relevant(a);
|
|
ctx.mark_as_relevant(b);
|
|
ctx.mark_as_relevant(c);
|
|
// scoped_trace_stream _st(*this, a, ~b);
|
|
ctx.mk_th_axiom(get_id(), a, ~b, c);
|
|
}
|
|
}
|
|
}
|
|
|
|
|
|
#define MK_UNARY(NAME, BLAST_OP) \
|
|
void theory_bv::NAME(app * n) { \
|
|
SASSERT(!ctx.e_internalized(n)); \
|
|
SASSERT(n->get_num_args() == 1); \
|
|
process_args(n); \
|
|
enode * e = mk_enode(n); \
|
|
expr_ref_vector arg1_bits(m), bits(m); \
|
|
get_arg_bits(e, 0, arg1_bits); \
|
|
m_bb.BLAST_OP(arg1_bits.size(), arg1_bits.data(), bits); \
|
|
init_bits(e, bits); \
|
|
}
|
|
|
|
#define MK_BINARY(NAME, BLAST_OP) \
|
|
void theory_bv::NAME(app * n) { \
|
|
SASSERT(!ctx.e_internalized(n)); \
|
|
SASSERT(n->get_num_args() == 2); \
|
|
process_args(n); \
|
|
enode * e = mk_enode(n); \
|
|
expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m); \
|
|
get_arg_bits(e, 0, arg1_bits); \
|
|
get_arg_bits(e, 1, arg2_bits); \
|
|
SASSERT(arg1_bits.size() == arg2_bits.size()); \
|
|
m_bb.BLAST_OP(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), bits); \
|
|
init_bits(e, bits); \
|
|
}
|
|
|
|
|
|
#define MK_AC_BINARY(NAME, BLAST_OP) \
|
|
void theory_bv::NAME(app * n) { \
|
|
SASSERT(!ctx.e_internalized(n)); \
|
|
SASSERT(n->get_num_args() >= 2); \
|
|
process_args(n); \
|
|
enode * e = mk_enode(n); \
|
|
expr_ref_vector arg_bits(m); \
|
|
expr_ref_vector bits(m); \
|
|
expr_ref_vector new_bits(m); \
|
|
unsigned i = n->get_num_args(); \
|
|
--i; \
|
|
get_arg_bits(e, i, bits); \
|
|
while (i > 0) { \
|
|
--i; \
|
|
arg_bits.reset(); \
|
|
get_arg_bits(e, i, arg_bits); \
|
|
SASSERT(arg_bits.size() == bits.size()); \
|
|
new_bits.reset(); \
|
|
m_bb.BLAST_OP(arg_bits.size(), arg_bits.data(), bits.data(), new_bits); \
|
|
bits.swap(new_bits); \
|
|
} \
|
|
init_bits(e, bits); \
|
|
TRACE(bv_verbose, tout << arg_bits << " " << bits << " " << new_bits << "\n";); \
|
|
}
|
|
|
|
void theory_bv::internalize_sub(app *n) {
|
|
SASSERT(!ctx.e_internalized(n));
|
|
SASSERT(n->get_num_args() == 2);
|
|
process_args(n);
|
|
enode * e = mk_enode(n);
|
|
expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m);
|
|
get_arg_bits(e, 0, arg1_bits);
|
|
get_arg_bits(e, 1, arg2_bits);
|
|
SASSERT(arg1_bits.size() == arg2_bits.size());
|
|
expr_ref carry(m);
|
|
m_bb.mk_subtracter(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), bits, carry);
|
|
init_bits(e, bits);
|
|
}
|
|
|
|
MK_UNARY(internalize_neg, mk_neg);
|
|
MK_UNARY(internalize_not, mk_not);
|
|
MK_UNARY(internalize_redand, mk_redand);
|
|
MK_UNARY(internalize_redor, mk_redor);
|
|
|
|
MK_AC_BINARY(internalize_add, mk_adder);
|
|
MK_AC_BINARY(internalize_mul, mk_multiplier);
|
|
MK_BINARY(internalize_udiv, mk_udiv);
|
|
MK_BINARY(internalize_sdiv, mk_sdiv);
|
|
MK_BINARY(internalize_urem, mk_urem);
|
|
MK_BINARY(internalize_srem, mk_srem);
|
|
MK_BINARY(internalize_smod, mk_smod);
|
|
MK_BINARY(internalize_shl, mk_shl);
|
|
MK_BINARY(internalize_lshr, mk_lshr);
|
|
MK_BINARY(internalize_ashr, mk_ashr);
|
|
MK_BINARY(internalize_ext_rotate_left, mk_ext_rotate_left);
|
|
MK_BINARY(internalize_ext_rotate_right, mk_ext_rotate_right);
|
|
MK_AC_BINARY(internalize_and, mk_and);
|
|
MK_AC_BINARY(internalize_or, mk_or);
|
|
MK_AC_BINARY(internalize_xor, mk_xor);
|
|
MK_AC_BINARY(internalize_nand, mk_nand);
|
|
MK_AC_BINARY(internalize_nor, mk_nor);
|
|
MK_AC_BINARY(internalize_xnor, mk_xnor);
|
|
MK_BINARY(internalize_comp, mk_comp);
|
|
|
|
#define MK_PARAMETRIC_UNARY(NAME, BLAST_OP) \
|
|
void theory_bv::NAME(app * n) { \
|
|
SASSERT(!ctx.e_internalized(n)); \
|
|
SASSERT(n->get_num_args() == 1); \
|
|
process_args(n); \
|
|
enode * e = mk_enode(n); \
|
|
expr_ref_vector arg1_bits(m), bits(m); \
|
|
get_arg_bits(e, 0, arg1_bits); \
|
|
unsigned param = n->get_decl()->get_parameter(0).get_int(); \
|
|
m_bb.BLAST_OP(arg1_bits.size(), arg1_bits.data(), param, bits); \
|
|
init_bits(e, bits); \
|
|
}
|
|
|
|
MK_PARAMETRIC_UNARY(internalize_sign_extend, mk_sign_extend);
|
|
MK_PARAMETRIC_UNARY(internalize_zero_extend, mk_zero_extend);
|
|
MK_PARAMETRIC_UNARY(internalize_rotate_left, mk_rotate_left);
|
|
MK_PARAMETRIC_UNARY(internalize_rotate_right, mk_rotate_right);
|
|
|
|
void theory_bv::internalize_concat(app * n) {
|
|
process_args(n);
|
|
enode * e = mk_enode(n);
|
|
theory_var v = e->get_th_var(get_id());
|
|
unsigned num_args = n->get_num_args();
|
|
unsigned i = num_args;
|
|
m_bits[v].reset();
|
|
while (i > 0) {
|
|
i--;
|
|
theory_var arg = get_arg_var(e, i);
|
|
for (literal lit : m_bits[arg]) {
|
|
add_bit(v, lit);
|
|
}
|
|
}
|
|
find_wpos(v);
|
|
}
|
|
|
|
void theory_bv::internalize_extract(app * n) {
|
|
SASSERT(n->get_num_args() == 1);
|
|
process_args(n);
|
|
enode * e = mk_enode(n);
|
|
theory_var v = e->get_th_var(get_id());
|
|
theory_var arg = get_arg_var(e, 0);
|
|
unsigned start = n->get_decl()->get_parameter(1).get_int();
|
|
unsigned end = n->get_decl()->get_parameter(0).get_int();
|
|
SASSERT(start <= end);
|
|
literal_vector & arg_bits = m_bits[arg];
|
|
m_bits[v].reset();
|
|
for (unsigned i = start; i <= end; ++i)
|
|
add_bit(v, arg_bits[i]);
|
|
find_wpos(v);
|
|
}
|
|
|
|
|
|
bool theory_bv::internalize_term_core(app * term) {
|
|
SASSERT(term->get_family_id() == get_family_id());
|
|
TRACE(bv, tout << "internalizing term: " << mk_bounded_pp(term, m) << "\n";);
|
|
if (approximate_term(term)) {
|
|
return false;
|
|
}
|
|
switch (term->get_decl_kind()) {
|
|
case OP_BV_NUM: internalize_num(term); return true;
|
|
case OP_BNEG: internalize_neg(term); return true;
|
|
case OP_BADD: internalize_add(term); return true;
|
|
case OP_BSUB: internalize_sub(term); return true;
|
|
case OP_BMUL: internalize_mul(term); return true;
|
|
case OP_BSDIV_I: internalize_sdiv(term); return true;
|
|
#if ENABLE_QUOT_REM_ENCODING
|
|
case OP_BUDIV_I: internalize_udiv_quot_rem(term); return true;
|
|
#else
|
|
case OP_BUDIV_I: internalize_udiv(term); return true;
|
|
#endif
|
|
case OP_BSREM_I: internalize_srem(term); return true;
|
|
case OP_BUREM_I: internalize_urem(term); return true;
|
|
case OP_BSMOD_I: internalize_smod(term); return true;
|
|
case OP_BAND: internalize_and(term); return true;
|
|
case OP_BOR: internalize_or(term); return true;
|
|
case OP_BNOT: internalize_not(term); return true;
|
|
case OP_BXOR: internalize_xor(term); return true;
|
|
case OP_BNAND: internalize_nand(term); return true;
|
|
case OP_BNOR: internalize_nor(term); return true;
|
|
case OP_BXNOR: internalize_xnor(term); return true;
|
|
case OP_CONCAT: internalize_concat(term); return true;
|
|
case OP_SIGN_EXT: internalize_sign_extend(term); return true;
|
|
case OP_ZERO_EXT: internalize_zero_extend(term); return true;
|
|
case OP_EXTRACT: internalize_extract(term); return true;
|
|
case OP_BREDOR: internalize_redor(term); return true;
|
|
case OP_BREDAND: internalize_redand(term); return true;
|
|
case OP_BCOMP: internalize_comp(term); return true;
|
|
case OP_BSHL: internalize_shl(term); return true;
|
|
case OP_BLSHR: internalize_lshr(term); return true;
|
|
case OP_BASHR: internalize_ashr(term); return true;
|
|
case OP_ROTATE_LEFT: internalize_rotate_left(term); return true;
|
|
case OP_ROTATE_RIGHT: internalize_rotate_right(term); return true;
|
|
case OP_EXT_ROTATE_LEFT: internalize_ext_rotate_left(term); return true;
|
|
case OP_EXT_ROTATE_RIGHT: internalize_ext_rotate_right(term); return true;
|
|
case OP_BSDIV0: return false;
|
|
case OP_BUDIV0: return false;
|
|
case OP_BSREM0: return false;
|
|
case OP_BUREM0: return false;
|
|
case OP_BSMOD0: return false;
|
|
case OP_MKBV: internalize_mkbv(term); return true;
|
|
case OP_INT2BV:
|
|
if (params().m_bv_enable_int2bv2int) {
|
|
internalize_int2bv(term);
|
|
}
|
|
return params().m_bv_enable_int2bv2int;
|
|
case OP_UBV2INT:
|
|
if (params().m_bv_enable_int2bv2int) {
|
|
internalize_bv2int(term);
|
|
}
|
|
return params().m_bv_enable_int2bv2int;
|
|
case OP_SBV2INT:
|
|
throw default_exception("sbv_to_int should have been removed by pre-processing");
|
|
case OP_BSREM: return false;
|
|
case OP_BUREM: return false;
|
|
case OP_BSMOD: return false;
|
|
default:
|
|
TRACE(bv_op, tout << "unsupported operator: " << mk_ll_pp(term, m) << "\n";);
|
|
UNREACHABLE();
|
|
return false;
|
|
}
|
|
}
|
|
|
|
bool theory_bv::internalize_term(app * term) {
|
|
scoped_suspend_rlimit _suspend_cancel(m.limit());
|
|
try {
|
|
return internalize_term_core(term);
|
|
}
|
|
catch (z3_exception& ex) {
|
|
IF_VERBOSE(1, verbose_stream() << "internalize_term: " << ex.what() << "\n";);
|
|
throw;
|
|
}
|
|
}
|
|
|
|
#define MK_NO_OVFL(NAME, OP) \
|
|
void theory_bv::NAME(app *n) { \
|
|
SASSERT(n->get_num_args() == 2); \
|
|
process_args(n); \
|
|
expr_ref_vector arg1_bits(m), arg2_bits(m); \
|
|
get_arg_bits(n, 0, arg1_bits); \
|
|
get_arg_bits(n, 1, arg2_bits); \
|
|
expr_ref out(m); \
|
|
m_bb.OP(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), out); \
|
|
expr_ref s_out(m); \
|
|
simplify_bit(out, s_out); \
|
|
ctx.internalize(s_out, true); \
|
|
literal def = ctx.get_literal(s_out); \
|
|
literal l(ctx.mk_bool_var(n)); \
|
|
ctx.set_var_theory(l.var(), get_id()); \
|
|
le_atom * a = new (get_region()) le_atom(l, def); /* abuse le_atom */ \
|
|
insert_bv2a(l.var(), a); \
|
|
m_trail_stack.push(mk_atom_trail(*this, l.var())); \
|
|
/* smul_no_overflow and umul_no_overflow are using the le_atom (THIS IS A BIG HACK)... */ \
|
|
/* the connection between the l and def was never realized when */ \
|
|
/* relevancy() is true and m_bv_lazy_le is false (the default configuration). */ \
|
|
/* So, we need to check also the m_bv_lazy_le flag here. */ \
|
|
/* Maybe, we should rename the le_atom to bridge_atom, and m_bv_lazy_le option to m_bv_lazy_bridge. */ \
|
|
if (!ctx.relevancy() || !params().m_bv_lazy_le) { \
|
|
ctx.mk_th_axiom(get_id(), l, ~def); \
|
|
ctx.mk_th_axiom(get_id(), ~l, def); \
|
|
} \
|
|
}
|
|
|
|
MK_NO_OVFL(internalize_umul_no_overflow, mk_umul_no_overflow);
|
|
MK_NO_OVFL(internalize_smul_no_overflow, mk_smul_no_overflow);
|
|
MK_NO_OVFL(internalize_smul_no_underflow, mk_smul_no_underflow);
|
|
|
|
template<bool Signed>
|
|
void theory_bv::internalize_le(app * n) {
|
|
SASSERT(n->get_num_args() == 2);
|
|
process_args(n);
|
|
expr_ref_vector arg1_bits(m), arg2_bits(m);
|
|
get_arg_bits(n, 0, arg1_bits);
|
|
get_arg_bits(n, 1, arg2_bits);
|
|
if (ctx.b_internalized(n))
|
|
return;
|
|
expr_ref le(m);
|
|
if (Signed)
|
|
m_bb.mk_sle(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), le);
|
|
else
|
|
m_bb.mk_ule(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), le);
|
|
expr_ref s_le(m);
|
|
simplify_bit(le, s_le);
|
|
ctx.internalize(s_le, true);
|
|
literal def = ctx.get_literal(s_le);
|
|
literal l(ctx.mk_bool_var(n));
|
|
ctx.set_var_theory(l.var(), get_id());
|
|
le_atom * a = new (get_region()) le_atom(l, def);
|
|
insert_bv2a(l.var(), a);
|
|
m_trail_stack.push(mk_atom_trail(*this, l.var()));
|
|
if (!ctx.relevancy() || !params().m_bv_lazy_le) {
|
|
ctx.mk_th_axiom(get_id(), l, ~def);
|
|
ctx.mk_th_axiom(get_id(), ~l, def);
|
|
}
|
|
}
|
|
|
|
bool theory_bv::internalize_carry(app * n, bool gate_ctx) {
|
|
ctx.internalize(n->get_args(), 3, true);
|
|
bool is_new_var = false;
|
|
bool_var v;
|
|
if (!ctx.b_internalized(n)) {
|
|
is_new_var = true;
|
|
v = ctx.mk_bool_var(n);
|
|
literal r(v);
|
|
literal l1 = ctx.get_literal(n->get_arg(0));
|
|
literal l2 = ctx.get_literal(n->get_arg(1));
|
|
literal l3 = ctx.get_literal(n->get_arg(2));
|
|
ctx.mk_gate_clause(~r, l1, l2);
|
|
ctx.mk_gate_clause(~r, l1, l3);
|
|
ctx.mk_gate_clause(~r, l2, l3);
|
|
ctx.mk_gate_clause( r, ~l1, ~l2);
|
|
ctx.mk_gate_clause( r, ~l1, ~l3);
|
|
ctx.mk_gate_clause( r, ~l2, ~l3);
|
|
}
|
|
else {
|
|
v = ctx.get_bool_var(n);
|
|
}
|
|
|
|
if (!ctx.e_internalized(n) && !gate_ctx) {
|
|
bool suppress_args = true;
|
|
bool merge_tf = !gate_ctx;
|
|
ctx.mk_enode(n, suppress_args, merge_tf, true);
|
|
ctx.set_enode_flag(v, is_new_var);
|
|
}
|
|
return true;
|
|
}
|
|
|
|
bool theory_bv::internalize_xor3(app * n, bool gate_ctx) {
|
|
ctx.internalize(n->get_args(), 3, true);
|
|
bool is_new_var = false;
|
|
bool_var v;
|
|
if (!ctx.b_internalized(n)) {
|
|
is_new_var = true;
|
|
v = ctx.mk_bool_var(n);
|
|
literal r(v);
|
|
literal l1 = ctx.get_literal(n->get_arg(0));
|
|
literal l2 = ctx.get_literal(n->get_arg(1));
|
|
literal l3 = ctx.get_literal(n->get_arg(2));
|
|
ctx.mk_gate_clause(~r, l1, l2, l3);
|
|
ctx.mk_gate_clause(~r, ~l1, ~l2, l3);
|
|
ctx.mk_gate_clause(~r, ~l1, l2, ~l3);
|
|
ctx.mk_gate_clause(~r, l1, ~l2, ~l3);
|
|
ctx.mk_gate_clause( r, ~l1, l2, l3);
|
|
ctx.mk_gate_clause( r, l1, ~l2, l3);
|
|
ctx.mk_gate_clause( r, l1, l2, ~l3);
|
|
ctx.mk_gate_clause( r, ~l1, ~l2, ~l3);
|
|
}
|
|
else {
|
|
v = ctx.get_bool_var(n);
|
|
}
|
|
|
|
if (!ctx.e_internalized(n) && !gate_ctx) {
|
|
bool suppress_args = true;
|
|
bool merge_tf = !gate_ctx;
|
|
ctx.mk_enode(n, suppress_args, merge_tf, true);
|
|
ctx.set_enode_flag(v, is_new_var);
|
|
}
|
|
return true;
|
|
}
|
|
|
|
bool theory_bv::internalize_atom(app * atom, bool gate_ctx) {
|
|
TRACE(bv, tout << "internalizing atom: " << mk_bounded_pp(atom, m) << "\n";);
|
|
SASSERT(atom->get_family_id() == get_family_id());
|
|
if (approximate_term(atom)) {
|
|
return false;
|
|
}
|
|
switch (atom->get_decl_kind()) {
|
|
case OP_BIT2BOOL: mk_bit2bool(atom); return true;
|
|
case OP_ULEQ: internalize_le<false>(atom); return true;
|
|
case OP_SLEQ: internalize_le<true>(atom); return true;
|
|
case OP_XOR3: return internalize_xor3(atom, gate_ctx);
|
|
case OP_CARRY: return internalize_carry(atom, gate_ctx);
|
|
case OP_BUMUL_NO_OVFL: internalize_umul_no_overflow(atom); return true;
|
|
case OP_BSMUL_NO_OVFL: internalize_smul_no_overflow(atom); return true;
|
|
case OP_BSMUL_NO_UDFL: internalize_smul_no_underflow(atom); return true;
|
|
default:
|
|
UNREACHABLE();
|
|
return false;
|
|
}
|
|
}
|
|
|
|
//
|
|
// Determine whether bit-vector expression should be approximated
|
|
// based on the number of bits used by the arguments.
|
|
//
|
|
bool theory_bv::approximate_term(app* n) {
|
|
if (params().m_bv_blast_max_size == INT_MAX) {
|
|
return false;
|
|
}
|
|
unsigned num_args = n->get_num_args();
|
|
for (unsigned i = 0; i <= num_args; i++) {
|
|
expr* arg = (i == num_args)?n:n->get_arg(i);
|
|
sort* s = arg->get_sort();
|
|
if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > params().m_bv_blast_max_size) {
|
|
if (!m_approximates_large_bvs) {
|
|
TRACE(bv, tout << "found large size bit-vector:\n" << mk_pp(n, m) << "\n";);
|
|
ctx.push_trail(value_trail<bool>(m_approximates_large_bvs));
|
|
m_approximates_large_bvs = true;
|
|
}
|
|
return true;
|
|
}
|
|
}
|
|
return false;
|
|
}
|
|
|
|
void theory_bv::apply_sort_cnstr(enode * n, sort * s) {
|
|
if (!is_attached_to_var(n) && !approximate_term(n->get_expr())) {
|
|
mk_bits(mk_var(n));
|
|
if (ctx.is_relevant(n)) {
|
|
relevant_eh(n->get_expr());
|
|
}
|
|
}
|
|
}
|
|
|
|
void theory_bv::new_eq_eh(theory_var v1, theory_var v2) {
|
|
TRACE(bv_eq, tout << "new_eq: " << mk_pp(get_enode(v1)->get_expr(), m) << " = " << mk_pp(get_enode(v2)->get_expr(), m) << "\n";);
|
|
TRACE(bv, tout << "new_eq_eh v" << v1 << " = v" << v2 << " @ " << ctx.get_scope_level() <<
|
|
" relevant1: " << ctx.is_relevant(get_enode(v1)) <<
|
|
" relevant2: " << ctx.is_relevant(get_enode(v2)) << "\n";);
|
|
m_find.merge(v1, v2);
|
|
}
|
|
|
|
void theory_bv::new_diseq_eh(theory_var v1, theory_var v2) {
|
|
if (is_bv(v1)) {
|
|
SASSERT(m_bits[v1].size() == m_bits[v2].size());
|
|
expand_diseq(v1, v2);
|
|
}
|
|
}
|
|
|
|
void theory_bv::expand_diseq(theory_var v1, theory_var v2) {
|
|
|
|
SASSERT(get_bv_size(v1) == get_bv_size(v2));
|
|
if (v1 > v2) {
|
|
std::swap(v1, v2);
|
|
}
|
|
literal_vector const & bits1 = m_bits[v1];
|
|
literal_vector::const_iterator it1 = bits1.begin();
|
|
literal_vector::const_iterator end1 = bits1.end();
|
|
literal_vector const & bits2 = m_bits[v2];
|
|
literal_vector::const_iterator it2 = bits2.begin();
|
|
for (; it1 != end1; ++it1, ++it2) {
|
|
if (*it1 == ~(*it2))
|
|
return;
|
|
lbool val1 = ctx.get_assignment(*it1);
|
|
lbool val2 = ctx.get_assignment(*it2);
|
|
if (val1 != l_undef && val2 != l_undef && val1 != val2) {
|
|
return;
|
|
}
|
|
}
|
|
|
|
if (params().m_bv_watch_diseq) {
|
|
bool_var watch_var = null_bool_var;
|
|
it1 = bits1.begin();
|
|
it2 = bits2.begin();
|
|
unsigned act = m_diseq_activity[hash_u_u(v1, v2) & 0xFF]++;
|
|
|
|
for (; it1 != end1 && ((act & 0x3) != 0x3); ++it1, ++it2) {
|
|
lbool val1 = ctx.get_assignment(*it1);
|
|
lbool val2 = ctx.get_assignment(*it2);
|
|
|
|
if (val1 == l_undef) {
|
|
watch_var = it1->var();
|
|
}
|
|
else if (val2 == l_undef) {
|
|
watch_var = it2->var();
|
|
}
|
|
else {
|
|
continue;
|
|
}
|
|
|
|
m_diseq_watch.reserve(watch_var+1);
|
|
m_diseq_watch[watch_var].push_back(std::make_pair(v1, v2));
|
|
m_diseq_watch_trail.push_back(watch_var);
|
|
return;
|
|
}
|
|
}
|
|
|
|
literal_vector & lits = m_tmp_literals;
|
|
lits.reset();
|
|
literal eq = mk_eq(get_enode(v1)->get_expr(), get_enode(v2)->get_expr(), true);
|
|
lits.push_back(eq);
|
|
it1 = bits1.begin();
|
|
it2 = bits2.begin();
|
|
for (; it1 != end1; ++it1, ++it2) {
|
|
expr_ref l1(m), l2(m), diff(m);
|
|
ctx.literal2expr(*it1, l1);
|
|
ctx.literal2expr(*it2, l2);
|
|
m_bb.mk_xor(l1, l2, diff);
|
|
ctx.internalize(diff, true);
|
|
literal arg = ctx.get_literal(diff);
|
|
lits.push_back(arg);
|
|
}
|
|
TRACE(bv,
|
|
tout << mk_pp(get_enode(v1)->get_expr(), m) << " = " << mk_pp(get_enode(v2)->get_expr(), m) << " "
|
|
<< ctx.get_scope_level()
|
|
<< "\n";
|
|
ctx.display_literals_smt2(tout, lits););
|
|
|
|
m_stats.m_num_diseq_dynamic++;
|
|
scoped_trace_stream st(*this, lits);
|
|
ctx.mk_th_axiom(get_id(), lits.size(), lits.data());
|
|
}
|
|
|
|
void theory_bv::assign_eh(bool_var v, bool is_true) {
|
|
atom * a = get_bv2a(v);
|
|
TRACE(bv, tout << "assert: p" << v << " #" << ctx.bool_var2expr(v)->get_id() << " is_true: " << is_true << " " << ctx.inconsistent() << "\n";);
|
|
if (a->is_bit()) {
|
|
m_prop_queue.reset();
|
|
bit_atom * b = static_cast<bit_atom*>(a);
|
|
var_pos_occ * curr = b->m_occs;
|
|
while (curr) {
|
|
m_prop_queue.push_back(var_pos(curr->m_var, curr->m_idx));
|
|
curr = curr->m_next;
|
|
}
|
|
propagate_bits();
|
|
|
|
if (params().m_bv_watch_diseq && !ctx.inconsistent() && m_diseq_watch.size() > static_cast<unsigned>(v)) {
|
|
unsigned sz = m_diseq_watch[v].size();
|
|
for (unsigned i = 0; i < sz; ++i) {
|
|
auto const & p = m_diseq_watch[v][i];
|
|
expand_diseq(p.first, p.second);
|
|
}
|
|
m_diseq_watch[v].reset();
|
|
}
|
|
}
|
|
}
|
|
|
|
void theory_bv::propagate_bits() {
|
|
for (unsigned i = 0; i < m_prop_queue.size(); i++) {
|
|
var_pos const & entry = m_prop_queue[i];
|
|
theory_var v = entry.first;
|
|
unsigned idx = entry.second;
|
|
|
|
if (m_wpos[v] == idx)
|
|
find_wpos(v);
|
|
|
|
literal_vector & bits = m_bits[v];
|
|
literal bit = bits[idx];
|
|
lbool val = ctx.get_assignment(bit);
|
|
if (val == l_undef) {
|
|
continue;
|
|
}
|
|
theory_var v2 = next(v);
|
|
TRACE(bv, tout << "propagating v" << v << " #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << " " << ctx.get_scope_level() << "\n";);
|
|
literal antecedent = bit;
|
|
|
|
if (val == l_false) {
|
|
antecedent.neg();
|
|
}
|
|
while (v2 != v) {
|
|
literal_vector & bits2 = m_bits[v2];
|
|
literal bit2 = bits2[idx];
|
|
lbool val2 = ctx.get_assignment(bit2);
|
|
TRACE(bv_bit_prop, tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";);
|
|
TRACE(bv, tout << bit << " -> " << bit2 << " " << val << " -> " << val2 << " " << ctx.get_scope_level() << "\n";);
|
|
|
|
if (bit == ~bit2) {
|
|
add_new_diseq_axiom(v, v2, idx);
|
|
return;
|
|
}
|
|
|
|
if (val != val2) {
|
|
literal consequent = bit2;
|
|
if (val == l_false) {
|
|
consequent.neg();
|
|
}
|
|
assign_bit(consequent, v, v2, idx, antecedent, false);
|
|
if (ctx.inconsistent()) {
|
|
TRACE(bv, tout << "inconsistent " << bit << " " << bit2 << "\n";);
|
|
m_prop_queue.reset();
|
|
return;
|
|
}
|
|
}
|
|
v2 = next(v2);
|
|
}
|
|
}
|
|
m_prop_queue.reset();
|
|
TRACE(bv_bit_prop, tout << "done propagating\n";);
|
|
}
|
|
|
|
void theory_bv::assign_bit(literal consequent, theory_var v1, theory_var v2, unsigned idx, literal antecedent, bool propagate_eqc) {
|
|
|
|
m_stats.m_num_bit2core++;
|
|
SASSERT(ctx.get_assignment(antecedent) == l_true);
|
|
SASSERT(m_bits[v2][idx].var() == consequent.var());
|
|
SASSERT(consequent.var() != antecedent.var());
|
|
TRACE(bv_bit_prop, tout << "assigning: " << consequent << " @ " << ctx.get_scope_level();
|
|
tout << " using "; ctx.display_literal(tout, antecedent);
|
|
tout << " " << enode_pp(get_enode(v1), ctx) << " " << enode_pp(get_enode(v2), ctx) << " idx: " << idx << "\n";
|
|
tout << "propagate_eqc: " << propagate_eqc << "\n";);
|
|
if (consequent == false_literal) {
|
|
m_stats.m_num_conflicts++;
|
|
ctx.set_conflict(mk_bit_eq_justification(v1, v2, consequent, antecedent));
|
|
}
|
|
else {
|
|
ctx.assign(consequent, mk_bit_eq_justification(v1, v2, consequent, antecedent));
|
|
|
|
literal_vector lits;
|
|
lits.push_back(~consequent);
|
|
lits.push_back(antecedent);
|
|
literal eq = mk_eq(get_expr(v1), get_expr(v2), false);
|
|
lits.push_back(~eq);
|
|
//
|
|
// Issue #3035:
|
|
// merge_eh invokes assign_bit, which updates the propagation queue and includes the
|
|
// theory axiom for the propagated equality. When relevancy is non-zero, propagation may get
|
|
// lost on backtracking because the propagation queue is reset on conflicts.
|
|
// An alternative approach is to ensure the propagation queue is chronological with
|
|
// backtracking scopes (ie., it doesn't get reset, but shrunk to a previous level, and similar
|
|
// with a qhead indicator.
|
|
//
|
|
ctx.mark_as_relevant(lits[0]);
|
|
ctx.mark_as_relevant(lits[1]);
|
|
ctx.mark_as_relevant(lits[2]);
|
|
{
|
|
scoped_trace_stream _sts(*this, lits);
|
|
ctx.mk_th_axiom(get_id(), lits.size(), lits.data());
|
|
}
|
|
|
|
if (m_wpos[v2] == idx)
|
|
find_wpos(v2);
|
|
// REMARK: bit_eq_justification is marked as a theory_bv justification.
|
|
// Thus, the assignment to consequent will not be notified back to the theory.
|
|
// So, we need to propagate the assignment to other bits.
|
|
bool_var bv = consequent.var();
|
|
atom * a = get_bv2a(bv);
|
|
CTRACE(bv, !a, tout << ctx.literal2expr(literal(bv, false)) << "\n");
|
|
if (!a)
|
|
return;
|
|
SASSERT(a->is_bit());
|
|
bit_atom * b = static_cast<bit_atom*>(a);
|
|
var_pos_occ * curr = b->m_occs;
|
|
while (curr) {
|
|
TRACE(assign_bit_bug, tout << "curr->m_var: v" << curr->m_var << ", curr->m_idx: " << curr->m_idx << ", v2: v" << v2 << ", idx: " << idx << "\n";
|
|
tout << "find(curr->m_var): v" << find(curr->m_var) << ", find(v2): v" << find(v2) << "\n";
|
|
tout << "is bit of #" << get_enode(curr->m_var)->get_owner_id() << "\n";
|
|
);
|
|
// If find(curr->m_var) == find(v2) && curr->m_idx == idx and propagate_eqc == false, then
|
|
// this bit will be propagated to the equivalence class of v2 by assign_bit caller.
|
|
if (propagate_eqc || find(curr->m_var) != find(v2) || curr->m_idx != idx)
|
|
m_prop_queue.push_back(var_pos(curr->m_var, curr->m_idx));
|
|
curr = curr->m_next;
|
|
}
|
|
}
|
|
}
|
|
|
|
void theory_bv::relevant_eh(app * n) {
|
|
TRACE(arith, tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_bounded_pp(n, m) << "\n";);
|
|
TRACE(bv, tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";);
|
|
if (m.is_bool(n)) {
|
|
bool_var v = ctx.get_bool_var(n);
|
|
atom * a = get_bv2a(v);
|
|
if (a && !a->is_bit()) {
|
|
le_atom * le = static_cast<le_atom*>(a);
|
|
ctx.mark_as_relevant(le->m_def);
|
|
if (params().m_bv_lazy_le) {
|
|
ctx.mk_th_axiom(get_id(), le->m_var, ~le->m_def);
|
|
ctx.mk_th_axiom(get_id(), ~le->m_var, le->m_def);
|
|
}
|
|
}
|
|
}
|
|
else if (params().m_bv_enable_int2bv2int && m_util.is_ubv2int(n)) {
|
|
ctx.mark_as_relevant(n->get_arg(0));
|
|
assert_bv2int_axiom(n);
|
|
}
|
|
else if (params().m_bv_enable_int2bv2int && m_util.is_int2bv(n)) {
|
|
ctx.mark_as_relevant(n->get_arg(0));
|
|
assert_int2bv_axiom(n);
|
|
}
|
|
#if ENABLE_QUOT_REM_ENCODING
|
|
else if (m_util.is_bv_udivi(n)) {
|
|
ctx.mark_as_relevant(n->get_arg(0));
|
|
ctx.mark_as_relevant(n->get_arg(1));
|
|
assert_udiv_quot_rem_axiom(n);
|
|
}
|
|
#endif
|
|
else if (ctx.e_internalized(n)) {
|
|
enode * e = ctx.get_enode(n);
|
|
theory_var v = e->get_th_var(get_id());
|
|
if (v != null_theory_var) {
|
|
literal_vector & bits = m_bits[v];
|
|
TRACE(bv, tout << "mark bits relevant: " << bits.size() << ": " << bits << "\n";);
|
|
SASSERT(!is_bv(v) || bits.size() == get_bv_size(v));
|
|
for (literal lit : bits) {
|
|
ctx.mark_as_relevant(lit);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
void theory_bv::push_scope_eh() {
|
|
theory::push_scope_eh();
|
|
m_trail_stack.push_scope();
|
|
// check_invariant();
|
|
m_diseq_watch_lim.push_back(m_diseq_watch_trail.size());
|
|
}
|
|
|
|
void theory_bv::pop_scope_eh(unsigned num_scopes) {
|
|
m_trail_stack.pop_scope(num_scopes);
|
|
unsigned num_old_vars = get_old_num_vars(num_scopes);
|
|
m_bits.shrink(num_old_vars);
|
|
m_wpos.shrink(num_old_vars);
|
|
m_zero_one_bits.shrink(num_old_vars);
|
|
unsigned old_trail_sz = m_diseq_watch_lim[m_diseq_watch_lim.size()-num_scopes];
|
|
for (unsigned i = m_diseq_watch_trail.size(); i-- > old_trail_sz;) {
|
|
if (!m_diseq_watch[m_diseq_watch_trail[i]].empty()) {
|
|
m_diseq_watch[m_diseq_watch_trail[i]].pop_back();
|
|
}
|
|
}
|
|
m_diseq_watch_trail.shrink(old_trail_sz);
|
|
m_diseq_watch_lim.shrink(m_diseq_watch_lim.size()-num_scopes);
|
|
theory::pop_scope_eh(num_scopes);
|
|
TRACE(bv_verbose, m_find.display(tout << ctx.get_scope_level() << " - "
|
|
<< num_scopes << " = " << (ctx.get_scope_level() - num_scopes) << "\n"););
|
|
}
|
|
|
|
final_check_status theory_bv::final_check_eh() {
|
|
SASSERT(check_invariant());
|
|
if (m_approximates_large_bvs) {
|
|
return FC_GIVEUP;
|
|
}
|
|
return FC_DONE;
|
|
}
|
|
|
|
void theory_bv::reset_eh() {
|
|
pop_scope_eh(m_trail_stack.get_num_scopes());
|
|
m_bool_var2atom.reset();
|
|
m_fixed_var_table.reset();
|
|
theory::reset_eh();
|
|
}
|
|
|
|
bool theory_bv::include_func_interp(func_decl* f) {
|
|
SASSERT(f->get_family_id() == get_family_id());
|
|
switch (f->get_decl_kind()) {
|
|
case OP_BSDIV0:
|
|
case OP_BUDIV0:
|
|
case OP_BSREM0:
|
|
case OP_BUREM0:
|
|
case OP_BSMOD0:
|
|
return true;
|
|
default:
|
|
return false;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
smt_params const& theory_bv::params() const {
|
|
return ctx.get_fparams();
|
|
}
|
|
|
|
theory_bv::theory_bv(context& ctx):
|
|
theory(ctx, ctx.get_manager().mk_family_id("bv")),
|
|
m_util(ctx.get_manager()),
|
|
m_autil(ctx.get_manager()),
|
|
m_bb(ctx.get_manager(), ctx.get_fparams()),
|
|
m_trail_stack(),
|
|
m_find(*this),
|
|
m_approximates_large_bvs(false) {
|
|
memset(m_eq_activity, 0, sizeof(m_eq_activity));
|
|
memset(m_diseq_activity, 0, sizeof(m_diseq_activity));
|
|
m_bb.set_flat_and_or(false);
|
|
}
|
|
|
|
theory* theory_bv::mk_fresh(context* new_ctx) {
|
|
return alloc(theory_bv, *new_ctx);
|
|
}
|
|
|
|
|
|
void theory_bv::merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {
|
|
TRACE(bv, tout << "merging: v" << v1 << " #" << get_enode(v1)->get_owner_id() << " v" << v2 << " #" << get_enode(v2)->get_owner_id() << "\n";);
|
|
TRACE(bv_bit_prop, tout << "merging: #" << get_enode(v1)->get_owner_id() << " #" << get_enode(v2)->get_owner_id() << "\n";);
|
|
if (!merge_zero_one_bits(r1, r2)) {
|
|
TRACE(bv, tout << "conflict detected\n";);
|
|
return; // conflict was detected
|
|
}
|
|
m_prop_queue.reset();
|
|
SASSERT(m_bits[v1].size() == m_bits[v2].size());
|
|
unsigned sz = m_bits[v1].size();
|
|
bool changed = true;
|
|
TRACE(bv, tout << "bits size: " << sz << "\n";);
|
|
if (sz == 0 && !m_bv2int.empty()) {
|
|
// int2bv(bv2int(x)) = x when int2bv(bv2int(x)) has same sort as x
|
|
enode* n1 = get_enode(r1);
|
|
auto propagate_bv2int = [&](enode* bv2int) {
|
|
enode* bv2int_arg = get_arg(bv2int, 0);
|
|
for (enode* p : enode::parents(n1->get_root())) {
|
|
if (m_util.is_int2bv(p->get_expr()) && p->get_root() != bv2int_arg->get_root() && p->get_sort() == bv2int_arg->get_sort()) {
|
|
enode_pair_vector eqs;
|
|
eqs.push_back({n1, get_arg(p, 0) });
|
|
eqs.push_back({n1, bv2int});
|
|
justification * js = ctx.mk_justification(
|
|
ext_theory_eq_propagation_justification(get_id(), ctx, 0, nullptr, eqs.size(), eqs.data(), p, bv2int_arg));
|
|
ctx.assign_eq(p, bv2int_arg, eq_justification(js));
|
|
break;
|
|
}
|
|
}
|
|
};
|
|
|
|
if (m_bv2int.size() < n1->get_class_size()) {
|
|
for (enode* bv2int : m_bv2int)
|
|
if (bv2int->get_root() == n1->get_root())
|
|
propagate_bv2int(bv2int);
|
|
}
|
|
else {
|
|
for (enode* bv2int : *n1) {
|
|
if (m_util.is_ubv2int(bv2int->get_expr()))
|
|
propagate_bv2int(bv2int);
|
|
}
|
|
}
|
|
}
|
|
do {
|
|
// This outerloop is necessary to avoid missing propagation steps.
|
|
// For example, let's assume that bits1 and bits2 contains the following
|
|
// sequence of bits:
|
|
// b4 b3 b2 b1
|
|
// b5 b4 b3 b2
|
|
// Let's also assume that b1 is assigned, and b2, b3, b4, and b5 are not.
|
|
// Only the propagation from b1 to b2 is performed by the first iteration of this
|
|
// loop.
|
|
//
|
|
// In the worst case, we need to execute this loop bits1.size() times.
|
|
//
|
|
// Remark: the assignment to b2 is marked as a bv theory propagation,
|
|
// then it is not notified to the bv theory.
|
|
changed = false;
|
|
for (unsigned idx = 0; idx < sz; idx++) {
|
|
literal bit1 = m_bits[v1][idx];
|
|
literal bit2 = m_bits[v2][idx];
|
|
if (bit1 == ~bit2) {
|
|
add_new_diseq_axiom(v1, v2, idx);
|
|
return;
|
|
}
|
|
lbool val1 = ctx.get_assignment(bit1);
|
|
lbool val2 = ctx.get_assignment(bit2);
|
|
TRACE(bv, tout << "merge v" << v1 << " " << bit1 << ":= " << val1 << " " << bit2 << ":= " << val2 << "\n";);
|
|
if (val1 == l_undef && !ctx.is_relevant(bit1))
|
|
ctx.mark_as_relevant(bit1);
|
|
if (val2 == l_undef && !ctx.is_relevant(bit2))
|
|
ctx.mark_as_relevant(bit2);
|
|
if (val1 == val2)
|
|
continue;
|
|
changed = true;
|
|
if (val1 != l_undef && val2 != l_undef) {
|
|
TRACE(bv, tout << "inconsistent "; display_var(tout, v1); display_var(tout, v2); tout << "idx: " << idx << "\n";);
|
|
}
|
|
if (val1 != l_undef && bit2 != false_literal && bit2 != true_literal) {
|
|
literal antecedent = bit1;
|
|
literal consequent = bit2;
|
|
if (val1 == l_false) {
|
|
consequent.neg();
|
|
antecedent.neg();
|
|
}
|
|
assign_bit(consequent, v1, v2, idx, antecedent, true);
|
|
}
|
|
else if (val2 != l_undef) {
|
|
literal antecedent = bit2;
|
|
literal consequent = bit1;
|
|
if (val2 == l_false) {
|
|
consequent.neg();
|
|
antecedent.neg();
|
|
}
|
|
assign_bit(consequent, v2, v1, idx, antecedent, true);
|
|
}
|
|
if (ctx.inconsistent())
|
|
return;
|
|
if (val1 != l_undef && val2 != l_undef && val1 != val2) {
|
|
UNREACHABLE();
|
|
}
|
|
|
|
}
|
|
}
|
|
while(changed);
|
|
|
|
propagate_bits();
|
|
}
|
|
|
|
bool theory_bv::merge_zero_one_bits(theory_var r1, theory_var r2) {
|
|
zero_one_bits & bits2 = m_zero_one_bits[r2];
|
|
if (bits2.empty())
|
|
return true;
|
|
zero_one_bits & bits1 = m_zero_one_bits[r1];
|
|
unsigned bv_size = get_bv_size(r1);
|
|
SASSERT(bv_size == get_bv_size(r2));
|
|
m_merge_aux[0].reserve(bv_size+1, null_theory_var);
|
|
m_merge_aux[1].reserve(bv_size+1, null_theory_var);
|
|
|
|
auto reset_merge_aux = [&]() { for (auto & zo : bits1) m_merge_aux[zo.m_is_true][zo.m_idx] = null_theory_var; };
|
|
|
|
DEBUG_CODE(for (unsigned i = 0; i < bv_size; i++) {
|
|
SASSERT(m_merge_aux[0][i] == null_theory_var || m_merge_aux[1][i] == null_theory_var); }
|
|
);
|
|
// save info about bits1
|
|
for (auto & zo : bits1) m_merge_aux[zo.m_is_true][zo.m_idx] = zo.m_owner;
|
|
// check if bits2 is consistent with bits1, and copy new bits to bits1
|
|
for (auto & zo : bits2) {
|
|
theory_var v2 = zo.m_owner;
|
|
theory_var v1 = m_merge_aux[!zo.m_is_true][zo.m_idx];
|
|
if (v1 != null_theory_var) {
|
|
// conflict was detected ... v1 and v2 have complementary bits
|
|
SASSERT(m_bits[v1][zo.m_idx] == ~(m_bits[v2][zo.m_idx]));
|
|
SASSERT(m_bits[v1].size() == m_bits[v2].size());
|
|
add_new_diseq_axiom(v1, v2, zo.m_idx);
|
|
reset_merge_aux();
|
|
return false;
|
|
}
|
|
if (m_merge_aux[zo.m_is_true][zo.m_idx] == null_theory_var) {
|
|
// copy missing variable to bits1
|
|
bits1.push_back(zo);
|
|
}
|
|
}
|
|
// reset m_merge_aux vector
|
|
reset_merge_aux();
|
|
DEBUG_CODE(for (unsigned i = 0; i < bv_size; i++) { SASSERT(m_merge_aux[0][i] == null_theory_var || m_merge_aux[1][i] == null_theory_var); });
|
|
return true;
|
|
}
|
|
|
|
void theory_bv::propagate() {
|
|
if (!can_propagate())
|
|
return;
|
|
ctx.push_trail(value_trail<unsigned>(m_prop_diseqs_qhead));
|
|
for (; m_prop_diseqs_qhead < m_prop_diseqs.size() && !ctx.inconsistent(); ++m_prop_diseqs_qhead) {
|
|
auto p = m_prop_diseqs[m_prop_diseqs_qhead];
|
|
assert_new_diseq_axiom(p.v1, p.v2, p.idx);
|
|
}
|
|
}
|
|
|
|
class bit_eq_justification : public justification {
|
|
enode * m_v1;
|
|
enode * m_v2;
|
|
theory_id m_th_id; // TODO: steal 4 bits from each one of the following literas and use them to represent the th_id.
|
|
literal m_consequent;
|
|
literal m_antecedent;
|
|
public:
|
|
bit_eq_justification(theory_id th_id, enode * v1, enode * v2, literal c, literal a):
|
|
m_v1(v1), m_v2(v2), m_th_id(th_id), m_consequent(c), m_antecedent(a) {}
|
|
|
|
void get_antecedents(conflict_resolution & cr) override {
|
|
cr.mark_eq(m_v1, m_v2);
|
|
if (m_antecedent.var() != true_bool_var)
|
|
cr.mark_literal(m_antecedent);
|
|
}
|
|
|
|
proof * mk_proof(conflict_resolution & cr) override {
|
|
bool visited = true;
|
|
ptr_buffer<proof> prs;
|
|
proof * pr = cr.get_proof(m_v1, m_v2);
|
|
if (pr)
|
|
prs.push_back(pr);
|
|
else
|
|
visited = false;
|
|
if (m_antecedent.var() != true_bool_var) {
|
|
proof * pr = cr.get_proof(m_antecedent);
|
|
if (pr)
|
|
prs.push_back(pr);
|
|
else
|
|
visited = false;
|
|
}
|
|
if (!visited)
|
|
return nullptr;
|
|
context & ctx = cr.get_context();
|
|
ast_manager & m = cr.get_manager();
|
|
expr_ref fact(m);
|
|
ctx.literal2expr(m_consequent, fact);
|
|
return m.mk_th_lemma(get_from_theory(), fact, prs.size(), prs.data());
|
|
}
|
|
|
|
theory_id get_from_theory() const override {
|
|
return m_th_id;
|
|
}
|
|
|
|
char const * get_name() const override { return "bv-bit-eq"; }
|
|
};
|
|
|
|
inline justification * theory_bv::mk_bit_eq_justification(theory_var v1, theory_var v2, literal consequent, literal antecedent) {
|
|
return ctx.mk_justification(bit_eq_justification(get_id(), get_enode(v1), get_enode(v2), consequent, antecedent));
|
|
}
|
|
|
|
void theory_bv::unmerge_eh(theory_var v1, theory_var v2) {
|
|
|
|
// v1 was the root of the equivalence class
|
|
// I must remove the zero_one_bits that are from v2.
|
|
|
|
// REMARK: it is unsafe to invoke check_zero_one_bits, since
|
|
// the enode associated with v1 and v2 may have already been
|
|
// deleted.
|
|
//
|
|
// The logical context trail_stack is popped before
|
|
// the theories pop_scope_eh is invoked.
|
|
|
|
zero_one_bits & bits = m_zero_one_bits[v1];
|
|
if (bits.empty()) {
|
|
// SASSERT(check_zero_one_bits(v1));
|
|
// SASSERT(check_zero_one_bits(v2));
|
|
return;
|
|
}
|
|
unsigned j = bits.size();
|
|
while (j > 0) {
|
|
--j;
|
|
zero_one_bit & bit = bits[j];
|
|
if (find(bit.m_owner) == v1) {
|
|
bits.shrink(j+1);
|
|
// SASSERT(check_zero_one_bits(v1));
|
|
// SASSERT(check_zero_one_bits(v2));
|
|
return;
|
|
}
|
|
}
|
|
bits.shrink(0);
|
|
// SASSERT(check_zero_one_bits(v1));
|
|
// SASSERT(check_zero_one_bits(v2));
|
|
}
|
|
|
|
bool theory_bv::get_lower(enode* n, rational& value) {
|
|
theory_var v = n->get_th_var(get_id());
|
|
if (v != null_theory_var && is_bv(v)) {
|
|
value = 0;
|
|
rational p(1);
|
|
for (literal bit : m_bits[v]) {
|
|
switch (ctx.get_assignment(bit)) {
|
|
case l_true:
|
|
value += p;
|
|
break;
|
|
default:
|
|
break;
|
|
}
|
|
p *= 2;
|
|
}
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
bool theory_bv::get_upper(enode* n, rational& value) {
|
|
theory_var v = n->get_th_var(get_id());
|
|
if (v != null_theory_var && is_bv(v)) {
|
|
literal_vector const & bits = m_bits[v];
|
|
rational p = rational::power_of_two(bits.size());
|
|
value = p - 1;
|
|
p /= 2;
|
|
for (unsigned i = bits.size(); i-- > 0; ) {
|
|
switch (ctx.get_assignment(bits[i])) {
|
|
case l_false:
|
|
value -= p;
|
|
break;
|
|
case l_true:
|
|
break;
|
|
default: {
|
|
break;
|
|
}
|
|
}
|
|
p /= 2;
|
|
}
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
void theory_bv::initialize_value(expr* var, expr* value) {
|
|
rational val;
|
|
unsigned sz;
|
|
TRACE(bv, tout << "initializing " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
|
|
if (!m_util.is_numeral(value, val, sz)) {
|
|
IF_VERBOSE(5, verbose_stream() << "value should be a bit-vector " << mk_pp(value, m) << "\n");
|
|
return;
|
|
}
|
|
if (!is_app(var))
|
|
return;
|
|
enode* n = mk_enode(to_app(var));
|
|
auto v = get_var(n);
|
|
unsigned idx = 0;
|
|
for (auto lit : m_bits[v]) {
|
|
auto & b = ctx.get_bdata(lit.var());
|
|
b.m_phase_available = true;
|
|
b.m_phase = val.get_bit(idx);
|
|
++idx;
|
|
}
|
|
}
|
|
|
|
void theory_bv::init_model(model_generator & mg) {
|
|
m_factory = alloc(bv_factory, m);
|
|
mg.register_factory(m_factory);
|
|
}
|
|
|
|
model_value_proc * theory_bv::mk_value(enode * n, model_generator & mg) {
|
|
numeral val;
|
|
theory_var v = n->get_th_var(get_id());
|
|
SASSERT(v != null_theory_var);
|
|
#ifdef Z3DEBUG
|
|
bool r =
|
|
#endif
|
|
get_fixed_value(v, val);
|
|
SASSERT(r);
|
|
return alloc(expr_wrapper_proc, m_factory->mk_num_value(val, get_bv_size(v)));
|
|
}
|
|
|
|
void theory_bv::display_var(std::ostream & out, theory_var v) const {
|
|
out << "v";
|
|
out.width(4);
|
|
out << std::left << v;
|
|
out << " #";
|
|
out.width(4);
|
|
out << get_enode(v)->get_owner_id() << " -> #";
|
|
out.width(4);
|
|
out << get_enode(find(v))->get_owner_id();
|
|
out << std::right << ", bits:";
|
|
literal_vector const & bits = m_bits[v];
|
|
for (literal lit : bits) {
|
|
out << " " << lit << ":";
|
|
ctx.display_literal(out, lit);
|
|
}
|
|
numeral val;
|
|
if (get_fixed_value(v, val))
|
|
out << ", value: " << val;
|
|
out << "\n";
|
|
}
|
|
|
|
void theory_bv::display_bit_atom(std::ostream & out, bool_var v, bit_atom const * a) const {
|
|
out << "#" << ctx.bool_var2expr(v)->get_id() << " ->";
|
|
var_pos_occ * curr = a->m_occs;
|
|
while (curr) {
|
|
out << " #" << get_enode(curr->m_var)->get_owner_id() << "[" << curr->m_idx << "]";
|
|
curr = curr->m_next;
|
|
}
|
|
out << "\n";
|
|
}
|
|
|
|
void theory_bv::display_atoms(std::ostream & out) const {
|
|
out << "atoms:\n";
|
|
unsigned num = ctx.get_num_bool_vars();
|
|
for (unsigned v = 0; v < num; v++) {
|
|
atom * a = get_bv2a(v);
|
|
if (a && a->is_bit())
|
|
display_bit_atom(out, v, static_cast<bit_atom*>(a));
|
|
}
|
|
}
|
|
|
|
void theory_bv::display(std::ostream & out) const {
|
|
unsigned num_vars = get_num_vars();
|
|
if (num_vars == 0) return;
|
|
out << "Theory bv:\n";
|
|
for (unsigned v = 0; v < num_vars; v++) {
|
|
display_var(out, v);
|
|
}
|
|
display_atoms(out);
|
|
}
|
|
|
|
void theory_bv::collect_statistics(::statistics & st) const {
|
|
st.update("bv conflicts", m_stats.m_num_conflicts);
|
|
st.update("bv diseqs", m_stats.m_num_diseq_static);
|
|
st.update("bv dynamic diseqs", m_stats.m_num_diseq_dynamic);
|
|
st.update("bv bit2core", m_stats.m_num_bit2core);
|
|
st.update("bv->core eq", m_stats.m_num_th2core_eq);
|
|
st.update("bv dynamic eqs", m_stats.m_num_eq_dynamic);
|
|
}
|
|
|
|
theory_bv::var_enode_pos theory_bv::get_bv_with_theory(bool_var v, theory_id id) const {
|
|
atom* a = get_bv2a(v);
|
|
if (!a)
|
|
return var_enode_pos(nullptr, UINT32_MAX);
|
|
svector<var_enode_pos> vec;
|
|
if (!a->is_bit())
|
|
return var_enode_pos(nullptr, UINT32_MAX);
|
|
bit_atom * b = static_cast<bit_atom*>(a);
|
|
var_pos_occ * curr = b->m_occs;
|
|
while (curr) {
|
|
enode* n = get_enode(curr->m_var);
|
|
if (n->get_th_var(id) != null_theory_var)
|
|
return var_enode_pos(n, curr->m_idx);
|
|
curr = curr->m_next;
|
|
}
|
|
return var_enode_pos(nullptr, UINT32_MAX);
|
|
}
|
|
|
|
bool_var theory_bv::get_bit(unsigned bit, enode* n) const {
|
|
theory_var v = n->get_th_var(get_family_id());
|
|
if (v == null_theory_var)
|
|
return null_bool_var;
|
|
auto& bits = m_bits[v];
|
|
if (bit >= bits.size())
|
|
return null_bool_var;
|
|
return bits[bit].var();
|
|
}
|
|
|
|
bool theory_bv::check_assignment(theory_var v) {
|
|
if (!is_root(v))
|
|
return true;
|
|
if (!ctx.is_relevant(get_enode(v))) {
|
|
return true;
|
|
}
|
|
|
|
theory_var v2 = v;
|
|
literal_vector const & bits2 = m_bits[v2];
|
|
theory_var v1 = v2;
|
|
do {
|
|
literal_vector const & bits1 = m_bits[v1];
|
|
SASSERT(bits1.size() == bits2.size());
|
|
unsigned sz = bits1.size();
|
|
VERIFY(ctx.is_relevant(get_enode(v1)));
|
|
for (unsigned i = 0; i < sz; i++) {
|
|
literal bit1 = bits1[i];
|
|
literal bit2 = bits2[i];
|
|
lbool val1 = ctx.get_assignment(bit1);
|
|
lbool val2 = ctx.get_assignment(bit2);
|
|
CTRACE(bv_bug, val1 != val2,
|
|
tout << "equivalence class is inconsistent, i: " << i << "\n";
|
|
display_var(tout, v1);
|
|
display_var(tout, v2);
|
|
if (bit1 != true_literal && bit1 != false_literal) tout << "bit1 relevant: " << ctx.is_relevant(bit1) << " ";
|
|
if (bit2 != true_literal && bit2 != false_literal) tout << "bit2 relevant: " << ctx.is_relevant(bit2) << "\n";
|
|
tout << "val1: " << val1 << " lvl: " << ctx.get_assign_level(bit1.var()) << " bit " << bit1 << "\n";
|
|
tout << "val2: " << val2 << " lvl: " << ctx.get_assign_level(bit2.var()) << " bit " << bit2 << "\n";
|
|
tout << "level: " << ctx.get_scope_level() << "\n";
|
|
);
|
|
VERIFY(val1 == val2);
|
|
}
|
|
v1 = next(v1);
|
|
}
|
|
while (v1 != v);
|
|
return true;
|
|
}
|
|
|
|
/**
|
|
\brief Check whether m_zero_one_bits is an accurate summary of the bits in the
|
|
equivalence class rooted by v.
|
|
|
|
\remark The method does nothing if v is not the root of the equivalence class.
|
|
*/
|
|
bool theory_bv::check_zero_one_bits(theory_var v) {
|
|
if (ctx.inconsistent())
|
|
return true; // property is only valid if the context is not in a conflict.
|
|
if (is_root(v) && is_bv(v)) {
|
|
bool_vector bits[2];
|
|
unsigned num_bits = 0;
|
|
unsigned bv_sz = get_bv_size(v);
|
|
bits[0].resize(bv_sz, false);
|
|
bits[1].resize(bv_sz, false);
|
|
theory_var curr = v;
|
|
do {
|
|
literal_vector const & lits = m_bits[curr];
|
|
for (unsigned i = 0; i < lits.size(); i++) {
|
|
literal l = lits[i];
|
|
if (l.var() == true_bool_var) {
|
|
unsigned is_true = (l == true_literal);
|
|
if (bits[!is_true][i]) {
|
|
// expect a conflict later on.
|
|
return true;
|
|
}
|
|
if (!bits[is_true][i]) {
|
|
bits[is_true][i] = true;
|
|
num_bits++;
|
|
}
|
|
}
|
|
}
|
|
curr = next(curr);
|
|
}
|
|
while (curr != v);
|
|
|
|
zero_one_bits const & _bits = m_zero_one_bits[v];
|
|
(void)num_bits;
|
|
SASSERT(_bits.size() == num_bits);
|
|
bool_vector already_found;
|
|
already_found.resize(bv_sz, false);
|
|
for (auto & zo : _bits) {
|
|
SASSERT(find(zo.m_owner) == v);
|
|
SASSERT(bits[zo.m_is_true][zo.m_idx]);
|
|
SASSERT(!already_found[zo.m_idx]);
|
|
already_found[zo.m_idx] = true;
|
|
}
|
|
}
|
|
return true;
|
|
}
|
|
|
|
bool theory_bv::check_invariant() {
|
|
if (m.limit().is_canceled())
|
|
return true;
|
|
if (ctx.inconsistent())
|
|
return true;
|
|
unsigned num = get_num_vars();
|
|
for (unsigned v = 0; v < num; v++) {
|
|
check_assignment(v);
|
|
check_zero_one_bits(v);
|
|
}
|
|
return true;
|
|
}
|
|
|
|
#if ENABLE_QUOT_REM_ENCODING
|
|
void theory_bv::internalize_udiv_quot_rem(app* n) {
|
|
process_args(n);
|
|
mk_enode(n);
|
|
theory_var v = ctx.get_enode(n)->get_th_var(get_id());
|
|
mk_bits(v);
|
|
if (!ctx.relevancy())
|
|
assert_udiv_quot_rem_axiom(n);
|
|
}
|
|
|
|
|
|
void theory_bv::assert_udiv_quot_rem_axiom(app * q) {
|
|
// Axioms for quotient/remainder:
|
|
// a = b*q + r
|
|
// no-mul-overflow(b,q)
|
|
// no-add-overflow(bq, r)
|
|
// b != 0 => r < b
|
|
// b = 0 => q = -1
|
|
expr* a, *b;
|
|
VERIFY(m_util.is_bv_udivi(q, a, b));
|
|
sort* srt = q->get_sort();
|
|
func_decl_ref rf(m.mk_func_decl(symbol("rem"), srt, srt, srt), m);
|
|
expr_ref r(m.mk_app(rf, a, b), m);
|
|
expr_ref bq(m_util.mk_bv_mul(b, q), m);
|
|
expr_ref bqr(m_util.mk_bv_add(bq, r), m);
|
|
literal eq = mk_literal(m.mk_eq(a, bqr));
|
|
literal obq = mk_literal(m_util.mk_bvumul_no_ovfl(b, q));
|
|
literal obqr = mk_literal(m_util.mk_ule(r, bqr));
|
|
literal b0 = mk_literal(m.mk_eq(b, m_util.mk_numeral(rational::zero(), srt)));
|
|
|
|
ctx.mk_th_axiom(get_id(), 1, &eq);
|
|
ctx.mk_th_axiom(get_id(), 1, &obq);
|
|
ctx.mk_th_axiom(get_id(), 1, &obqr);
|
|
ctx.mk_th_axiom(get_id(), b0, ~mk_literal(m_util.mk_ule(b, r)));
|
|
ctx.mk_th_axiom(get_id(), ~b0, mk_literal(m.mk_eq(q, m_util.mk_numeral(rational(-1), srt))));
|
|
}
|
|
#endif
|
|
|
|
|
|
};
|