mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-28 12:56:28 +00:00
Code Activity

Add SMT-LIB choice support via array OP_CHOICE and instantiate choice axioms in array solvers (#9649)

Browse source 
This change wires SMT-LIB Hilbert choice parsing to a concrete
array-theory operator and ensures both array backends enforce the
expected semantic axiom. Previously, `(choice ((x T)) phi)` parsed as
NYI and had no solver-side instantiation path.

- **Parser: lower `choice_k` into array `OP_CHOICE`**
- `pop_quant_frame(choice_k)` now builds `(choice p)` instead of
throwing.
- Added parser include/use of array utilities to construct the term
directly from the generated lambda predicate.

- **Array decl plugin: add `OP_CHOICE` typing + surface syntax**
  - Added declaration support for `choice` with signature:
- `(Array T Bool) -> T` (encoded as `('a -> Bool) -> 'a` in HO view).
- Added recognizer/util helpers (`is_choice`, `mk_choice`) and exposed
`"choice"` in op names.

- **SMT array theory (`theory_array_full`): instantiate choice axiom**
  - Added instantiation for each encountered `choice(p)`:
    - `forall x . p(x) => p(choice(p))`
  - Integrated into internalization/relevancy paths and statistics.

- **SAT/SMT array backend (`sat/smt/array_*`): instantiate choice
axiom**
- Added new axiom record kind for choice, internalization hook,
assertion routine, and diagnostics/stat tracking.
  - Uses the same quantified implication schema as above.

- **Regression coverage**
- Extended SMT2 parser regression with an HO `choice` example to ensure
parser/eval pipeline accepts and processes choice terms.

Example of the now-supported input:

```smt2
(set-logic HO_ALL)
(declare-sort U 0)
(declare-fun P () (-> U Bool))
(assert (exists ((x U)) (P x)))
(assert (= witness (choice ((x U)) (P x))))
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-05-27 10:05:06 -07:00 • committed by GitHub
parent 690cdd3f25
commit 51da9db615
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
12 changed files with 124 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/ast/array_decl_plugin.cpp
View file

@ -36,7 +36,8 @@ array_decl_plugin::array_decl_plugin():
m_set_complement_sym("complement"),
m_set_subset_sym("subset"),
m_array_ext_sym("array-ext"),
m_as_array_sym("as-array") {
m_as_array_sym("as-array"),
m_choice_sym("choice") {
}
#define ARRAY_SORT_STR "Array"
@ -433,6 +434,20 @@ func_decl * array_decl_plugin::mk_as_array(func_decl * f) {
return m_manager->mk_const_decl(m_as_array_sym, s, info);
}
func_decl* array_decl_plugin::mk_choice(unsigned arity, sort* const* domain) {
if (arity != 1) {
m_manager->raise_exception("choice takes one argument");
return nullptr;
}
sort* s = domain[0];
if (!is_array_sort(s) || get_array_arity(s) != 1 || !m_manager->is_bool(get_array_range(s))) {
m_manager->raise_exception("choice expects an argument with sort (Array T Bool)");
return nullptr;
}
return m_manager->mk_func_decl(m_choice_sym, arity, domain, get_array_domain(s, 0),
func_decl_info(m_family_id, OP_CHOICE));
}
func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
@ -501,6 +516,8 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
func_decl * f = to_func_decl(parameters[0].get_ast());
return mk_as_array(f);
}
case OP_CHOICE:
return mk_choice(arity, domain);
default: return nullptr;
}
}
@ -529,6 +546,7 @@ void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
op_names.push_back(builtin_name("complement",OP_SET_COMPLEMENT));
op_names.push_back(builtin_name("subset",OP_SET_SUBSET));
op_names.push_back(builtin_name("as-array", OP_AS_ARRAY));
op_names.push_back(builtin_name("choice", OP_CHOICE));
op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT));
#if 0
@ -655,4 +673,3 @@ func_decl* array_util::mk_array_ext(sort *domain, unsigned i) {
parameter p(i);
return m_manager.mk_func_decl(m_fid, OP_ARRAY_EXT, 1, &p, 2, domains);
}

10
src/ast/array_decl_plugin.h
View file

@ -80,6 +80,7 @@ class array_decl_plugin : public decl_plugin {
symbol m_set_subset_sym;
symbol m_array_ext_sym;
symbol m_as_array_sym;
symbol m_choice_sym;
bool check_set_arguments(unsigned arity, sort * const * domain);
@ -106,6 +107,8 @@ 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;
public:
@ -165,6 +168,7 @@ public:
bool is_difference(expr* n) const { return is_app_of(n, m_fid, OP_SET_DIFFERENCE); }
bool is_complement(expr* n) const { return is_app_of(n, m_fid, OP_SET_COMPLEMENT); }
bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); }
bool is_choice(expr* n) const { return is_app_of(n, m_fid, OP_CHOICE); }
bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); }
bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); }
bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); }
@ -173,6 +177,7 @@ public:
bool is_union(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_UNION); }
bool is_intersect(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_INTERSECT); }
bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); }
bool is_choice(func_decl* f) const { return is_decl_of(f, m_fid, OP_CHOICE); }
bool is_default(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_DEFAULT); }
bool is_default(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_DEFAULT); }
bool is_subset(expr const* n) const { return is_app_of(n, m_fid, OP_SET_SUBSET); }
@ -309,6 +314,10 @@ public:
return m_manager.mk_app(m_fid, OP_AS_ARRAY, 1, &param, 0, nullptr, nullptr);
}
app* mk_choice(expr* p) const {
return m_manager.mk_app(m_fid, OP_CHOICE, p);
}
sort* get_array_range_rec(sort* s) {
while (is_array(s)) {
s = get_array_range(s);
@ -319,4 +328,3 @@ public:
};

6
src/parsers/smt2/smt2parser.cpp
View file

@ -21,6 +21,7 @@ Revision History:
#include "ast/bv_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "ast/seq_decl_plugin.h"
#include "ast/array_decl_plugin.h"
#include "ast/ast_pp.h"
#include "ast/well_sorted.h"
#include "ast/rewriter/rewriter.h"
@ -2140,10 +2141,7 @@ namespace smt2 {
SASSERT(num_decls <= m_num_bindings);
m_num_bindings -= num_decls;
if (fr->m_kind == choice_k) {
// create expression (choice new_q)
// add to expr_stack().push_back(choice_expr);
//
throw default_exception("parsing of choice expressions is NYI");
expr_stack().push_back(array_util(m()).mk_choice(new_q));
}
else
expr_stack().push_back(new_q);

24
src/sat/smt/array_axioms.cpp
View file

@ -68,6 +68,8 @@ namespace array {
return assert_extensionality(r.n->get_expr(), r.select->get_expr());
case axiom_record::kind_t::is_congruence:
return assert_congruent_axiom(r.n->get_expr(), r.select->get_expr());
case axiom_record::kind_t::is_choice:
return assert_choice_axiom(r.n->get_app());
default:
UNREACHABLE();
break;
@ -469,6 +471,27 @@ namespace array {
return ctx.propagate(e_internalize(alpha), e_internalize(beta), array_axiom());
}
bool solver::assert_choice_axiom(app* choice_term) {
++m_stats.m_num_choice_axiom;
SASSERT(a.is_choice(choice_term));
expr* pred = choice_term->get_arg(0);
sort* pred_sort = pred->get_sort();
SASSERT(a.is_array(pred_sort));
SASSERT(get_array_arity(pred_sort) == 1);
SASSERT(m.is_bool(get_array_range(pred_sort)));
sort* x_sort = get_array_domain(pred_sort, 0);
expr_ref x(m.mk_var(0, x_sort), m);
expr* args1[2] = { pred, x };
expr_ref px(a.mk_select(2, args1), m);
expr* args2[2] = { pred, choice_term };
expr_ref pc(a.mk_select(2, args2), 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, body), m);
rewrite(q);
return add_unit(mk_literal(q));
}
/**
\brief assert n1 = n2 => forall vars . (n1 vars) = (n2 vars)
*/
@ -691,4 +714,3 @@ namespace array {
}
}

3
src/sat/smt/array_diagnostics.cpp
View file

@ -55,6 +55,8 @@ namespace array {
return out << "extensionality " << ctx.bpp(r.n) << " " << ctx.bpp(r.select);
case axiom_record::kind_t::is_congruence:
return out << "congruence " << ctx.bpp(r.n) << " " << ctx.bpp(r.select);
case axiom_record::kind_t::is_choice:
return out << "choice " << ctx.bpp(r.n);
default:
UNREACHABLE();
}
@ -75,6 +77,7 @@ namespace array {
st.update("array def/map", m_stats.m_num_default_map_axiom);
st.update("array def/const", m_stats.m_num_default_const_axiom);
st.update("array def/store", m_stats.m_num_default_store_axiom);
st.update("array choice ax", m_stats.m_num_choice_axiom);
st.update("array ext ax", m_stats.m_num_extensionality_axiom);
st.update("array cong ax", m_stats.m_num_congruence_axiom);
st.update("array exp ax2", m_stats.m_num_select_store_axiom_delayed);

6
src/sat/smt/array_internalize.cpp
View file

@ -111,6 +111,9 @@ namespace array {
case OP_CONST_ARRAY:
internalize_lambda_eh(n);
break;
case OP_CHOICE:
push_axiom(choice_axiom(n));
break;
case OP_ARRAY_EXT:
SASSERT(is_array(n->get_arg(0)));
push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1)));
@ -169,6 +172,8 @@ namespace array {
case OP_ARRAY_DEFAULT:
set_prop_upward(find(n->get_arg(0)));
break;
case OP_CHOICE:
break;
case OP_ARRAY_MAP:
case OP_SET_UNION:
case OP_SET_INTERSECT:
@ -255,4 +260,3 @@ namespace array {
}
}

7
src/sat/smt/array_solver.h
View file

@ -43,7 +43,7 @@ namespace array {
unsigned m_num_select_const_axiom, m_num_select_store_axiom_delayed;
unsigned m_num_default_store_axiom, m_num_default_map_axiom;
unsigned m_num_default_const_axiom, m_num_default_as_array_axiom;
unsigned m_num_select_lambda_axiom;
unsigned m_num_select_lambda_axiom, m_num_choice_axiom;
void reset() { memset(this, 0, sizeof(*this)); }
stats() { reset(); }
};
@ -86,7 +86,8 @@ namespace array {
is_select,
is_extensionality,
is_default,
is_congruence
is_congruence,
is_choice
};
enum class state_t {
is_new,
@ -165,6 +166,7 @@ namespace array {
axiom_record store_axiom(euf::enode* n) { return axiom_record(axiom_record::kind_t::is_store, n); }
axiom_record extensionality_axiom(euf::enode* x, euf::enode* y) { return axiom_record(axiom_record::kind_t::is_extensionality, x, y); }
axiom_record congruence_axiom(euf::enode* a, euf::enode* b) { return axiom_record(axiom_record::kind_t::is_congruence, a, b); }
axiom_record choice_axiom(euf::enode* n) { return axiom_record(axiom_record::kind_t::is_choice, n); }
scoped_ptr<sat::constraint_base> m_constraint;
@ -176,6 +178,7 @@ namespace array {
bool assert_select_as_array_axiom(app* select, app* arr);
bool assert_select_map_axiom(app* select, app* map);
bool assert_select_lambda_axiom(app* select, expr* lambda);
bool assert_choice_axiom(app* choice_term);
bool assert_extensionality(expr* e1, expr* e2);
bool assert_default_map_axiom(app* map);
bool assert_default_const_axiom(app* cnst);

3
src/smt/theory_array.h
View file

@ -28,7 +28,7 @@ namespace smt {
unsigned m_num_axiom1, m_num_axiom2a, m_num_axiom2b, m_num_extensionality, m_num_eq_splits;
unsigned m_num_map_axiom, m_num_default_map_axiom;
unsigned m_num_select_const_axiom, m_num_default_store_axiom, m_num_default_const_axiom, m_num_default_as_array_axiom;
unsigned m_num_select_as_array_axiom, m_num_default_lambda_axiom;
unsigned m_num_select_as_array_axiom, m_num_default_lambda_axiom, m_num_choice_axiom;
void reset() { memset(this, 0, sizeof(theory_array_stats)); }
theory_array_stats() { reset(); }
};
@ -115,4 +115,3 @@ namespace smt {
};

3
src/smt/theory_array_base.h
View file

@ -43,6 +43,7 @@ namespace smt {
bool is_const(app const* n) const { return n->is_app_of(get_id(), OP_CONST_ARRAY); }
bool is_array_ext(app const * n) const { return n->is_app_of(get_id(), OP_ARRAY_EXT); }
bool is_as_array(app const * n) const { return n->is_app_of(get_id(), OP_AS_ARRAY); }
bool is_choice(app const* n) const { return n->is_app_of(get_id(), OP_CHOICE); }
bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); }
bool is_array_sort(app const* n) const { return is_array_sort(n->get_sort()); }
@ -51,6 +52,7 @@ namespace smt {
bool is_select(enode const* n) const { return is_select(n->get_expr()); }
bool is_const(enode const* n) const { return is_const(n->get_expr()); }
bool is_as_array(enode const * n) const { return is_as_array(n->get_expr()); }
bool is_choice(enode const* n) const { return is_choice(n->get_expr()); }
bool is_default(enode const* n) const { return is_default(n->get_expr()); }
bool is_array_sort(enode const* n) const { return is_array_sort(n->get_expr()); }
bool is_select_arg(enode* r);
@ -208,4 +210,3 @@ namespace smt {
};

37
src/smt/theory_array_full.cpp
View file

@ -271,7 +271,7 @@ namespace smt {
return theory_array::internalize_term(n);
}
if (!is_const(n) && !is_default(n) && !is_map(n) && !is_as_array(n)) {
if (!is_const(n) && !is_default(n) && !is_map(n) && !is_as_array(n) && !is_choice(n)) {
if (!is_array_ext(n))
found_unsupported_op(n);
return false;
@ -329,6 +329,9 @@ namespace smt {
ctx.push_trail(push_back_vector(m_as_array));
instantiate_default_as_array_axiom(node);
}
else if (is_choice(n)) {
instantiate_choice_axiom(node);
}
else if (is_array_ext(n)) {
SASSERT(n->get_num_args() == 2);
instantiate_extensionality(ctx.get_enode(n->get_arg(0)), ctx.get_enode(n->get_arg(1)));
@ -406,7 +409,7 @@ namespace smt {
void theory_array_full::relevant_eh(app* n) {
TRACE(array, tout << mk_pp(n, m) << "\n";);
theory_array::relevant_eh(n);
if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n)){
if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n) && !is_choice(n)){
return;
}
ctx.ensure_internalized(n);
@ -442,6 +445,9 @@ namespace smt {
else if (is_as_array(n)) {
instantiate_default_as_array_axiom(node);
}
else if (is_choice(n)) {
instantiate_choice_axiom(node);
}
}
bool theory_array_full::should_research(expr_ref_vector & unsat_core) {
@ -596,6 +602,32 @@ namespace smt {
return try_assign_eq(val.get(), def);
}
bool theory_array_full::instantiate_choice_axiom(enode* ch) {
if (!ctx.add_fingerprint(this, m_choice_fingerprint, 1, &ch))
return false;
++m_stats.m_num_choice_axiom;
SASSERT(is_choice(ch));
app* choice_term = ch->get_expr();
expr* pred = choice_term->get_arg(0);
sort* pred_sort = pred->get_sort();
SASSERT(is_array_sort(pred_sort));
SASSERT(get_array_arity(pred_sort) == 1);
SASSERT(m.is_bool(get_array_range(pred_sort)));
sort* x_sort = get_array_domain(pred_sort, 0);
expr_ref x(m.mk_var(0, x_sort), m);
expr* args1[2] = { pred, x };
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);
symbol x_name("x");
expr_ref q(m.mk_forall(1, &x_sort, &x_name, ax), m);
ctx.get_rewriter()(q);
literal l = mk_literal(q);
assert_axiom(l);
return true;
}
//
// Assert axiom:
// select(const v, i_1, ..., i_n) = v
@ -839,5 +871,6 @@ namespace smt {
st.update("array def as-array", m_stats.m_num_default_as_array_axiom);
st.update("array sel as-array", m_stats.m_num_select_as_array_axiom);
st.update("array def lambda", m_stats.m_num_default_lambda_axiom);
st.update("array choice ax", m_stats.m_num_choice_axiom);
}
}

3
src/smt/theory_array_full.h
View file

@ -43,6 +43,7 @@ namespace smt {
static unsigned const m_default_const_fingerprint = UINT_MAX - 115;
static unsigned const m_default_as_array_fingerprint = UINT_MAX - 116;
static unsigned const m_default_lambda_fingerprint = UINT_MAX - 117;
static unsigned const m_choice_fingerprint = UINT_MAX - 118;
protected:
@ -80,6 +81,7 @@ namespace smt {
bool instantiate_default_map_axiom(enode* map);
bool instantiate_default_as_array_axiom(enode* arr);
bool instantiate_default_lambda_def_axiom(enode* arr);
bool instantiate_choice_axiom(enode* ch);
bool instantiate_parent_stores_default(theory_var v);
@ -112,4 +114,3 @@ namespace smt {
};

18
src/test/smt2print_parse.cpp
View file

@ -176,6 +176,23 @@ void test_ho_curried_application() {
Z3_del_context(ctx);
}
void test_ho_choice_expression() {
char const* spec =
"(set-logic HO_ALL)\n"
"(declare-sort U 0)\n"
"(declare-fun P () (-> U Bool))\n"
"(assert (exists ((x U)) (P x)))\n"
"(declare-fun witness () U)\n"
"(assert (= witness (choice ((x U)) (P x))))\n"
"(assert (not (P witness)))\n"
"(check-sat)\n";
Z3_context ctx = Z3_mk_context(nullptr);
Z3_set_error_handler(ctx, setError);
test_eval(ctx, spec, false);
Z3_del_context(ctx);
}
void test_name(Z3_string spec, Z3_string expected_name) {
Z3_context ctx = Z3_mk_context(nullptr);
Z3_set_error_handler(ctx, setError);
@ -306,6 +323,7 @@ void tst_smt2print_parse() {
test_repeated_eval();
test_ho_curried_application();
test_ho_choice_expression();
test_symbol_escape();