mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
relax giveup condition for as-array when it occurs only in beta redex positions.
This commit is contained in:
parent
0629353fdc
commit
4a652a4c0c
|
@ -330,7 +330,8 @@ namespace smt {
|
|||
// Even if there was, as-array on interpreted
|
||||
// functions will be incomplete.
|
||||
// The instantiation operations are still sound to include.
|
||||
found_unsupported_op(n);
|
||||
m_as_array.push_back(node);
|
||||
ctx.push_trail(push_back_vector(m_as_array));
|
||||
instantiate_default_as_array_axiom(node);
|
||||
}
|
||||
else if (is_array_ext(n)) {
|
||||
|
@ -815,12 +816,22 @@ namespace smt {
|
|||
if (r == FC_DONE && m_bapa) {
|
||||
r = m_bapa->final_check();
|
||||
}
|
||||
bool should_giveup = m_found_unsupported_op || has_propagate_up_trail();
|
||||
bool should_giveup = m_found_unsupported_op || has_propagate_up_trail() || has_non_beta_as_array();
|
||||
if (r == FC_DONE && should_giveup)
|
||||
r = FC_GIVEUP;
|
||||
return r;
|
||||
}
|
||||
|
||||
bool theory_array_full::has_non_beta_as_array() {
|
||||
for (enode* n : m_as_array) {
|
||||
for (enode* p : n->get_parents())
|
||||
if (!is_beta_redex(p, n))
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
bool theory_array_full::instantiate_parent_stores_default(theory_var v) {
|
||||
SASSERT(v != null_theory_var);
|
||||
TRACE("array", tout << "v" << v << "\n";);
|
||||
|
|
|
@ -85,6 +85,8 @@ namespace smt {
|
|||
bool has_large_domain(app* array_term);
|
||||
bool has_unitary_domain(app* array_term);
|
||||
std::pair<app*,func_decl*> mk_epsilon(sort* s);
|
||||
enode_vector m_as_array;
|
||||
bool has_non_beta_as_array();
|
||||
|
||||
bool instantiate_select_const_axiom(enode* select, enode* cnst);
|
||||
bool instantiate_select_as_array_axiom(enode* select, enode* arr);
|
||||
|
|
Loading…
Reference in a new issue