mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
beta redex check is used in array theory to filter out safe as-arrays
This commit is contained in:
parent
3900c03b72
commit
7a55bd5687
|
@ -777,8 +777,6 @@ namespace smt {
|
|||
|
||||
bool has_lambda();
|
||||
|
||||
bool is_beta_redex(enode* p, enode* n) const;
|
||||
|
||||
void internalize_lambda(quantifier * q);
|
||||
|
||||
void internalize_formula_core(app * n, bool gate_ctx);
|
||||
|
@ -1035,6 +1033,8 @@ namespace smt {
|
|||
|
||||
bool is_shared(enode * n) const;
|
||||
|
||||
bool is_beta_redex(enode* p, enode* n) const;
|
||||
|
||||
void assign_eq(enode * lhs, enode * rhs, eq_justification const & js) {
|
||||
push_eq(lhs, rhs, js);
|
||||
}
|
||||
|
|
|
@ -825,8 +825,10 @@ namespace smt {
|
|||
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))
|
||||
if (!ctx.is_beta_redex(p, n)) {
|
||||
TRACE("array", tout << "not a beta redex " << enode_pp(p, ctx) << "\n");
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue