From 51da9db615a6de8fa6f36867e915c7981f58b0a8 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 27 May 2026 10:05:06 -0700 Subject: [PATCH] Add SMT-LIB `choice` support via array `OP_CHOICE` and instantiate choice axioms in array solvers (#9649) 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> --- src/ast/array_decl_plugin.cpp | 21 ++++++++++++++++-- src/ast/array_decl_plugin.h | 10 ++++++++- src/parsers/smt2/smt2parser.cpp | 6 ++--- src/sat/smt/array_axioms.cpp | 24 +++++++++++++++++++- src/sat/smt/array_diagnostics.cpp | 3 +++ src/sat/smt/array_internalize.cpp | 6 ++++- src/sat/smt/array_solver.h | 7 ++++-- src/smt/theory_array.h | 3 +-- src/smt/theory_array_base.h | 3 ++- src/smt/theory_array_full.cpp | 37 +++++++++++++++++++++++++++++-- src/smt/theory_array_full.h | 3 ++- src/test/smt2print_parse.cpp | 18 +++++++++++++++ 12 files changed, 124 insertions(+), 17 deletions(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 7da470221..b51972934 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -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& 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); } - diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index f225b9b23..4411ed3d2 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -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, ¶m, 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: }; - diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index a4e3a44a3..f7bfe6ed5 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -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); diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index cd20e6ae6..e5e98baf2 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -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 { } } - diff --git a/src/sat/smt/array_diagnostics.cpp b/src/sat/smt/array_diagnostics.cpp index 11ed4384d..0f03abf46 100644 --- a/src/sat/smt/array_diagnostics.cpp +++ b/src/sat/smt/array_diagnostics.cpp @@ -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); diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index 7a62286e6..b9018deb5 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -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 { } } - diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index fce3efaac..41337d726 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -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 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); diff --git a/src/smt/theory_array.h b/src/smt/theory_array.h index 6e840e342..899f3cd64 100644 --- a/src/smt/theory_array.h +++ b/src/smt/theory_array.h @@ -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 { }; - diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h index 9a6a6a173..87a84cfa3 100644 --- a/src/smt/theory_array_base.h +++ b/src/smt/theory_array_base.h @@ -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 { }; - diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 5b316249e..736e447d3 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -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); } } diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h index 1a5b72814..699730358 100644 --- a/src/smt/theory_array_full.h +++ b/src/smt/theory_array_full.h @@ -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 { }; - diff --git a/src/test/smt2print_parse.cpp b/src/test/smt2print_parse.cpp index 0f6f369fb..83920cabd 100644 --- a/src/test/smt2print_parse.cpp +++ b/src/test/smt2print_parse.cpp @@ -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();