mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

Fix lira/array regression: lambda equality wrongly forces "unknown"

Browse source 
theory_array_full::has_non_beta_as_array() is an incompleteness guard that
forces FC_GIVEUP (result "unknown") when a lambda term registered with the
legacy array solver has a relevant parent that is neither `default` nor a
beta redex.

After lambdas began being registered with the legacy array solver (so that
`select(lambda, i)` beta axioms and the `default(lambda)` axiom are emitted),
this guard started firing on parents that are actually intrinsic to the array
decision procedure itself:

  * `(= lambda other-array)` array (dis)equality atoms, which are decided by
    extensionality (new_diseq_eh -> instantiate_extensionality), and
  * `(array-ext lambda other-array)` witness-index terms introduced by that
    same extensionality axiom.

Neither is an uninterpreted use of the lambda: extensionality asserts
`select(a, ext(a,b)) != select(b, ext(a,b))`, and the select-lambda beta axiom
reduces those selects, so the lambda is fully axiomatized in these cases.
Treating them as "non beta as array" made the solver give up with "unknown" on
satisfiable (and unsatisfiable) instances that it can in fact decide.

Exclude `is_eq` and `is_array_ext` parents from the lambda giveup check. The
`m_as_array` loop is intentionally left unchanged, since as-array equality is
genuinely incomplete.

Validated by rebuilding z3 and re-running the regressing benchmark
inputs/issues/iss-5454/bug-11.smt2, which returns to `sat` (matching the
recorded oracle), while several nested-store lambda equality/disequality tests
with known answers agree between the `lira` and default tactics.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-07-03 05:21:07 -07:00 • committed by GitHub
parent f15584cdae
commit 25e58ebd76
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_array_full.cpp
View file

@ -854,7 +854,16 @@ namespace smt {
}
for (enode* n : m_lambdas)
for (enode* p : n->get_parents())
if (ctx.is_relevant(p) && !is_default(p) && !ctx.is_beta_redex(p, n)) {
// Equality and array-ext parents are not genuine non-beta-redex uses:
// an array (dis)equality between a lambda and another array is decided by
// extensionality (new_diseq_eh / instantiate_extensionality), which itself
// introduces the array-ext witness index and the select(lambda, ext) beta
// redex. Together with the select-lambda beta axiom these fully axiomatize
// the lambda, so they must not force the solver into "unknown" the way a
// real uninterpreted use (e.g. an uninterpreted function applied to the
// lambda) does.
if (ctx.is_relevant(p) && !is_default(p) && !m.is_eq(p->get_expr()) &&
!is_array_ext(p->get_expr()) && !ctx.is_beta_redex(p, n)) {
TRACE(array, tout << "lambda is not a beta redex " << enode_pp(p, ctx) << "\n");
return true;
}