mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

more segfault sources #2205, examining bit2bool internalization for #2282

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-27 09:50:13 -07:00
parent 5478955199
commit 51a26ceb9e
2 changed files with 11 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/smt/theory_bv.cpp
View file

@ -97,30 +97,6 @@ namespace smt {
// This will also force the creation of all bits for x. // This will also force the creation of all bits for x.
enode * first_arg_enode = ctx.get_enode(first_arg); enode * first_arg_enode = ctx.get_enode(first_arg);
get_var(first_arg_enode); get_var(first_arg_enode);
#if 0
// constant axiomatization moved to catch all case in the end of function.
// numerals are not blasted into bit2bool, so we do this directly.
rational val;
unsigned sz;
if (!ctx.b_internalized(n) && m_util.is_numeral(first_arg, val, sz)) {
TRACE("bv", tout << "bit2bool constants\n";);
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) {
app* e = mk_bit2bool(owner, i);
ctx.internalize(e, 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);
}
}
#endif
} }
enode * arg = ctx.get_enode(first_arg); enode * arg = ctx.get_enode(first_arg);
@ -144,6 +120,13 @@ namespace smt {
unsigned idx = n->get_decl()->get_parameter(0).get_int(); unsigned idx = n->get_decl()->get_parameter(0).get_int();
SASSERT(a->m_occs == 0); SASSERT(a->m_occs == 0);
a->m_occs = new (get_region()) var_pos_occ(v_arg, idx); a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
#if 0
// possible fix for #2162, but effect of fix needs to be checked.
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));
}
#endif
} }
// axiomatize bit2bool on constants. // axiomatize bit2bool on constants.
rational val; rational val;
@ -782,6 +765,7 @@ namespace smt {
bits.swap(new_bits); \ bits.swap(new_bits); \
} \ } \
init_bits(e, bits); \ init_bits(e, bits); \
TRACE("bv", tout << arg_bits << " " << bits << " " << new_bits << "\n";); \
} }

7
src/smt/theory_datatype.cpp
View file

@ -175,7 +175,7 @@ namespace smt {
unsigned base_id = get_manager().has_trace_stream() && accessors.size() > 0 ? m_util.get_plugin()->get_axiom_base_id(d->get_name()) : 0; unsigned base_id = get_manager().has_trace_stream() && accessors.size() > 0 ? m_util.get_plugin()->get_axiom_base_id(d->get_name()) : 0;
unsigned i = 0; unsigned i = 0;
for (func_decl * acc : accessors) { for (func_decl * acc : accessors) {
app * acc_app = m.mk_app(acc, n->get_owner()); app_ref acc_app(m.mk_app(acc, n->get_owner()), m);
enode * arg = n->get_arg(i); enode * arg = n->get_arg(i);
if (m.has_trace_stream()) { if (m.has_trace_stream()) {
app_ref body(m); app_ref body(m);
@ -239,7 +239,7 @@ namespace smt {
ctx.internalize(acc_app, false); ctx.internalize(acc_app, false);
arg = ctx.get_enode(acc_app); arg = ctx.get_enode(acc_app);
} }
app * acc_own = m.mk_app(acc1, own); app_ref acc_own(m.mk_app(acc1, own), m);
if (m.has_trace_stream()) { if (m.has_trace_stream()) {
app_ref body(m); app_ref body(m);
body = m.mk_implies(rec_app, m.mk_eq(arg->get_owner(), acc_own)); body = m.mk_implies(rec_app, m.mk_eq(arg->get_owner(), acc_own));
@ -249,8 +249,7 @@ namespace smt {
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
} }
// update_field is identity if 'n' is not created by a matching constructor. // update_field is identity if 'n' is not created by a matching constructor.
app_ref imp(m); app_ref imp(m.mk_implies(m.mk_not(rec_app), m.mk_eq(n->get_owner(), arg1)), m);
imp = m.mk_implies(m.mk_not(rec_app), m.mk_eq(n->get_owner(), arg1));
if (m.has_trace_stream()) log_axiom_instantiation(imp, 1, &n); if (m.has_trace_stream()) log_axiom_instantiation(imp, 1, &n);
assert_eq_axiom(n, arg1, ~is_con); assert_eq_axiom(n, arg1, ~is_con);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";