mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

simplify: align choice axiom naming and inline literal in theory_array_full

Browse source 
- Rename 'ax' to 'body' in instantiate_choice_axiom to match the
  parallel implementation in sat/smt/array_axioms.cpp (assert_choice_axiom),
  where the same variable is already called 'body'
- Inline redundant 'literal l' variable: assert_axiom(mk_literal(q))
- Remove trailing whitespace in array_decl_plugin.h

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
github-actions[bot] 2026-05-28 05:45:50 +00:00 • committed by GitHub
parent 9d09a050e8
commit 62dd0b223a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 4 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/array_decl_plugin.h
View file

@ -107,7 +107,7 @@ class array_decl_plugin : public decl_plugin {
func_decl * mk_set_subset(unsigned arity, sort * const * domain);
func_decl * mk_as_array(func_decl * f);
func_decl * mk_choice(unsigned arity, sort* const* domain);
bool is_array_sort(sort* s) const;

7
src/smt/theory_array_full.cpp
View file

@ -619,12 +619,11 @@ namespace smt {
expr_ref px(mk_select(2, args1), m);
expr* args2[2] = { pred, choice_term };
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");
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);
literal l = mk_literal(q);
assert_axiom(l);
assert_axiom(mk_literal(q));
return true;
}