mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-05 00:20:50 +00:00
Code Activity

[code-simplifier] Align choice axiom naming in theory_array_full (#9660)

Browse source 
This simplifies the recent `choice` axiom path in the SMT array solver
for consistency with the SAT-side implementation. The change is purely
structural: align local naming with the quantifier body it represents,
inline a single-use literal, and remove stray whitespace in the array
decl header.

- **Choice axiom cleanup**
- Rename the local implication term in
`theory_array_full::instantiate_choice_axiom` from `ax` to `body`
- Match the naming already used in
`sat/smt/array_axioms.cpp::assert_choice_axiom`

- **Single-use literal inlining**
- Replace the temporary `literal l = mk_literal(q); assert_axiom(l);`
with a direct call
  - Reduce noise without changing behavior

- **Header whitespace cleanup**
  - Remove trailing whitespace in `src/ast/array_decl_plugin.h`

```c++
expr_ref body(m.mk_implies(px, pc), m);
expr_ref q(m.mk_forall(1, &x_sort, &x_name, body), m);
ctx.get_rewriter()(q);
assert_axiom(mk_literal(q));
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Copilot 2026-06-01 16:03:42 -07:00 • committed by GitHub
parent b0536c3998
commit 947af23fc4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/array_decl_plugin.h
View file

@ -327,4 +327,3 @@ public:
}; };

4
src/smt/theory_array_full.cpp
View file

@ -618,9 +618,9 @@ namespace smt {
expr_ref px(mk_select(2, args1), m); expr_ref px(mk_select(2, args1), m);
expr* args2[2] = { pred, choice_term }; expr* args2[2] = { pred, choice_term };
expr_ref pc(mk_select(2, args2), m); expr_ref pc(mk_select(2, args2), m);
expr_ref ax(m.mk_implies(px, pc), m); expr_ref body(m.mk_implies(px, pc), m);
symbol x_name("x"); symbol x_name("x");
expr_ref q(m.mk_forall(1, &x_sort, &x_name, ax), m); expr_ref q(m.mk_forall(1, &x_sort, &x_name, body), m);
ctx.get_rewriter()(q); ctx.get_rewriter()(q);
TRACE(array, tout << "choice " << q << "\n"); TRACE(array, tout << "choice " << q << "\n");
ctx.assert_expr(q); ctx.assert_expr(q);