mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

add bail #5825

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-02-16 23:30:12 +02:00
parent 33985ebcf5
commit 5bbb8fb807
1 changed files with 25 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/tactic/bv/bit_blaster_model_converter.cpp
View file

@ -70,7 +70,7 @@ struct bit_blaster_model_converter : public model_converter {
bits.insert(to_app(bit)->get_decl());
}
}
TRACE("blaster_mc",
TRACE("model_converter",
tout << "bits that should not be included in the model:\n";
for (func_decl* f : bits) {
tout << f->get_name() << " ";
@ -85,14 +85,14 @@ struct bit_blaster_model_converter : public model_converter {
func_decl * f = old_model->get_constant(i);
if (bits.contains(f))
continue;
TRACE("blaster_mc", tout << "non-bit: " << f->get_name() << "\n";);
TRACE("model_converter", tout << "non-bit: " << f->get_name() << "\n";);
expr * fi = old_model->get_const_interp(f);
new_model->register_decl(f, fi);
}
TRACE("blaster_mc", tout << "after copy non bits:\n"; model_pp(tout, *new_model););
TRACE("model_converter", tout << "after copy non bits:\n"; model_pp(tout, *new_model););
new_model->copy_func_interps(*old_model);
new_model->copy_usort_interps(*old_model);
TRACE("blaster_mc", tout << "after copying functions and sorts:\n"; model_pp(tout, *new_model););
TRACE("model_converter", tout << "after copying functions and sorts:\n"; model_pp(tout, *new_model););
}
void mk_bvs(model * old_model, model * new_model) {
@ -121,7 +121,9 @@ struct bit_blaster_model_converter : public model_converter {
SASSERT(is_uninterp_const(bit));
func_decl * bit_decl = to_app(bit)->get_decl();
expr * bit_val = old_model->get_const_interp(bit_decl);
if (bit_val != nullptr && m().is_true(bit_val))
if (bit_val && !m().is_true(bit_val) && !m().is_false(bit_val))
goto bail;
if (bit_val && m().is_true(bit_val))
val++;
}
}
@ -136,11 +138,27 @@ struct bit_blaster_model_converter : public model_converter {
func_decl * bit_decl = to_app(bit)->get_decl();
expr * bit_val = old_model->get_const_interp(bit_decl);
// remark: if old_model does not assign bit_val, then assume it is false.
if (bit_val != nullptr && !util.is_zero(bit_val))
if (bit_val && !util.is_one(bit_val) && !util.is_zero(bit_val))
goto bail;
if (bit_val && util.is_one(bit_val))
val++;
}
}
new_val = util.mk_numeral(val, bv_sz);
new_val = util.mk_numeral(val, bv_sz);
new_model->register_decl(m_vars.get(i), new_val);
continue;
bail:
expr_ref_vector vals(m());
for (expr* bit : *to_app(bs)) {
func_decl * bit_decl = to_app(bit)->get_decl();
expr * bit_val = old_model->get_const_interp(bit_decl);
SASSERT(bit_val);
vals.push_back(bit_val);
}
if (TO_BOOL)
new_val = util.mk_bv(vals.size(), vals.data());
else
new_val = util.mk_concat(vals);
new_model->register_decl(m_vars.get(i), new_val);
}
}