mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-09 15:43:25 +00:00
Code Activity

return unknown if m_array_weak was used and result is satisfiable

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-02 00:20:41 +08:00
parent 3f032e85e0
commit 0a29002c2f
6 changed files with 61 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/rewriter/seq_rewriter.cpp
View file

@ -954,6 +954,16 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
return BR_FAILED; return BR_FAILED;
} }
unsigned len = r.get_unsigned(); unsigned len = r.get_unsigned();
expr* a2 = nullptr, *i2 = nullptr;
if (m_util.str.is_at(a, a2, i2)) {
if (len > 0) {
result = m_util.str.mk_empty(m().get_sort(a));
}
else {
result = a2;
}
return BR_DONE;
}
expr_ref_vector as(m()); expr_ref_vector as(m());
m_util.str.get_concat_units(a, as); m_util.str.get_concat_units(a, as);

25
src/smt/theory_array.cpp
View file

@ -100,10 +100,14 @@ namespace smt {
for (enode* n : d->m_stores) { for (enode* n : d->m_stores) {
instantiate_axiom2a(s, n); instantiate_axiom2a(s, n);
} }
if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) { if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
for (enode* store : d->m_parent_stores) { for (enode* store : d->m_parent_stores) {
SASSERT(is_store(store)); SASSERT(is_store(store));
if (!m_params.m_array_cg || store->is_cgr()) { if (!m_params.m_array_cg || store->is_cgr()) {
if (m_params.m_array_weak) {
found_unsupported_op(store->get_owner());
break;
}
instantiate_axiom2b(s, store); instantiate_axiom2b(s, store);
} }
} }
@ -118,11 +122,18 @@ namespace smt {
var_data * d = m_var_data[v]; var_data * d = m_var_data[v];
d->m_parent_stores.push_back(s); d->m_parent_stores.push_back(s);
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_stores)); m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_stores));
if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) if (d->m_prop_upward && !m_params.m_array_delay_exp_axiom) {
for (enode* n : d->m_parent_selects) for (enode* n : d->m_parent_selects) {
if (!m_params.m_array_cg || n->is_cgr()) if (!m_params.m_array_cg || n->is_cgr()) {
if (m_params.m_array_weak) {
found_unsupported_op(s);
break;
}
instantiate_axiom2b(n, s); instantiate_axiom2b(n, s);
} }
}
}
}
bool theory_array::instantiate_axiom2b_for(theory_var v) { bool theory_array::instantiate_axiom2b_for(theory_var v) {
bool result = false; bool result = false;
@ -138,14 +149,16 @@ namespace smt {
\brief Mark v for upward propagation. That is, enables the propagation of select(v, i) to store(v,j,k). \brief Mark v for upward propagation. That is, enables the propagation of select(v, i) to store(v,j,k).
*/ */
void theory_array::set_prop_upward(theory_var v) { void theory_array::set_prop_upward(theory_var v) {
if (m_params.m_array_weak)
return;
v = find(v); v = find(v);
var_data * d = m_var_data[v]; var_data * d = m_var_data[v];
if (!d->m_prop_upward) { if (!d->m_prop_upward) {
TRACE("array", tout << "#" << v << "\n";); TRACE("array", tout << "#" << v << "\n";);
m_trail_stack.push(reset_flag_trail<theory_array>(d->m_prop_upward)); m_trail_stack.push(reset_flag_trail<theory_array>(d->m_prop_upward));
d->m_prop_upward = true; d->m_prop_upward = true;
if (m_params.m_array_weak) {
found_unsupported_op(v);
return;
}
if (!m_params.m_array_delay_exp_axiom) if (!m_params.m_array_delay_exp_axiom)
instantiate_axiom2b_for(v); instantiate_axiom2b_for(v);
for (enode * n : d->m_stores) for (enode * n : d->m_stores)

2
src/smt/theory_array_base.h
View file

@ -32,6 +32,8 @@ namespace smt {
bool m_found_unsupported_op; bool m_found_unsupported_op;
void found_unsupported_op(expr * n); void found_unsupported_op(expr * n);
void found_unsupported_op(enode* n) { found_unsupported_op(n->get_owner()); }
void found_unsupported_op(theory_var v) { found_unsupported_op(get_enode(v)->get_owner()); }
bool is_store(app const* n) const { return n->is_app_of(get_id(), OP_STORE); } bool is_store(app const* n) const { return n->is_app_of(get_id(), OP_STORE); }
bool is_map(app const* n) const { return n->is_app_of(get_id(), OP_ARRAY_MAP); } bool is_map(app const* n) const { return n->is_app_of(get_id(), OP_ARRAY_MAP); }

32
src/smt/theory_array_full.cpp
View file

@ -87,9 +87,13 @@ namespace smt {
var_data_full * d_full = m_var_data_full[v]; var_data_full * d_full = m_var_data_full[v];
d_full->m_parent_maps.push_back(s); d_full->m_parent_maps.push_back(s);
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d_full->m_parent_maps)); m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d_full->m_parent_maps));
if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) { if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
for (enode * n : d->m_parent_selects) { for (enode * n : d->m_parent_selects) {
if (!m_params.m_array_cg || n->is_cgr()) { if (!m_params.m_array_cg || n->is_cgr()) {
if (m_params.m_array_weak) {
found_unsupported_op(s);
break;
}
instantiate_select_map_axiom(n, s); instantiate_select_map_axiom(n, s);
} }
} }
@ -100,14 +104,16 @@ namespace smt {
// set set_prop_upward on root and recursively on children if necessary. // set set_prop_upward on root and recursively on children if necessary.
// //
void theory_array_full::set_prop_upward(theory_var v) { void theory_array_full::set_prop_upward(theory_var v) {
if (m_params.m_array_weak)
return;
v = find(v); v = find(v);
var_data * d = m_var_data[v]; var_data * d = m_var_data[v];
if (!d->m_prop_upward) { if (!d->m_prop_upward) {
m_trail_stack.push(reset_flag_trail<theory_array>(d->m_prop_upward)); m_trail_stack.push(reset_flag_trail<theory_array>(d->m_prop_upward));
d->m_prop_upward = true; d->m_prop_upward = true;
TRACE("array", tout << "#" << v << "\n";); TRACE("array", tout << "#" << v << "\n";);
if (m_params.m_array_weak) {
found_unsupported_op(v);
return;
}
if (!m_params.m_array_delay_exp_axiom) { if (!m_params.m_array_delay_exp_axiom) {
instantiate_axiom2b_for(v); instantiate_axiom2b_for(v);
instantiate_axiom_map_for(v); instantiate_axiom_map_for(v);
@ -355,10 +361,15 @@ namespace smt {
instantiate_default_store_axiom(store); instantiate_default_store_axiom(store);
} }
if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) { if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
if (m_params.m_array_weak) {
found_unsupported_op(v);
}
else {
instantiate_parent_stores_default(v); instantiate_parent_stores_default(v);
} }
} }
}
void theory_array_full::add_parent_select(theory_var v, enode * s) { void theory_array_full::add_parent_select(theory_var v, enode * s) {
TRACE("array", TRACE("array",
@ -376,10 +387,14 @@ namespace smt {
SASSERT(is_map(map)); SASSERT(is_map(map));
instantiate_select_map_axiom(s, map); instantiate_select_map_axiom(s, map);
} }
if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) { if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
for (enode * map : d_full->m_parent_maps) { for (enode * map : d_full->m_parent_maps) {
SASSERT(is_map(map)); SASSERT(is_map(map));
if (!m_params.m_array_cg || map->is_cgr()) { if (!m_params.m_array_cg || map->is_cgr()) {
if (m_params.m_array_weak) {
found_unsupported_op(s);
break;
}
instantiate_select_map_axiom(s, map); instantiate_select_map_axiom(s, map);
} }
} }
@ -748,8 +763,11 @@ namespace smt {
var_data * d = m_var_data[v]; var_data * d = m_var_data[v];
if (d->m_prop_upward && instantiate_axiom_map_for(v)) if (d->m_prop_upward && instantiate_axiom_map_for(v))
r = FC_CONTINUE; r = FC_CONTINUE;
if (d->m_prop_upward && !m_params.m_array_weak) { if (d->m_prop_upward) {
if (instantiate_parent_stores_default(v)) if (m_params.m_array_weak) {
found_unsupported_op(v);
}
else if (instantiate_parent_stores_default(v))
r = FC_CONTINUE; r = FC_CONTINUE;
} }
} }