mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fix internalization bug when bit2bool is applied to numeral

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-06 15:43:24 -07:00
parent 6d8daacdec
commit 8438ac6e21
1 changed files with 27 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/smt/theory_bv.cpp
View file

@ -53,6 +53,7 @@ namespace smt {
unsigned bv_size = get_bv_size(n);
context & ctx = get_context();
literal_vector & bits = m_bits[v];
bits.reset();
for (unsigned i = 0; i < bv_size; i++) {
app * bit = mk_bit2bool(owner, i);
ctx.internalize(bit, true);
@ -75,12 +76,14 @@ namespace smt {
void theory_bv::mk_bit2bool(app * n) {
context & ctx = get_context();
SASSERT(!ctx.b_internalized(n));
if (!ctx.e_internalized(n->get_arg(0))) {
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., n->get_arg(0))
expr * first_arg = n->get_arg(0);
// 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.
@ -91,10 +94,27 @@ namespace smt {
// 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);
SASSERT(ctx.b_internalized(n));
// numerals are not blasted into bit2bool, so we do this directly.
if (!ctx.b_internalized(n)) {
rational val;
unsigned sz;
VERIFY(m_util.is_numeral(first_arg, val, sz));
theory_var v = first_arg_enode->get_th_var(get_id());
app* owner = first_arg_enode->get_owner();
for (unsigned i = 0; i < sz; ++i) {
ctx.internalize(mk_bit2bool(owner, i), true);
}
m_bits[v].reset();
rational bit;
for (unsigned i = 0; i < sz; ++i) {
div(val, rational::power_of_two(i), bit);
mod(bit, rational(2), bit);
m_bits[v].push_back(bit.is_zero()?false_literal:true_literal);
}
}
}
else {
enode * arg = ctx.get_enode(n->get_arg(0));
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.
@ -1041,6 +1061,7 @@ namespace smt {
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);
}
}
@ -1381,6 +1402,7 @@ namespace smt {
if (v1 != null_theory_var) {
// conflict was detected ... v1 and v2 have complementary bits
SASSERT(m_bits[v1][it->m_idx] == ~(m_bits[v2][it->m_idx]));
SASSERT(m_bits[v1].size() == m_bits[v2].size());
mk_new_diseq_axiom(v1, v2, it->m_idx);
RESET_MERGET_AUX();
return false;