From 316d249b3f7a8ebd2225d273bd18f5a2599584cd Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 26 May 2026 18:39:38 -0700 Subject: [PATCH] SMT2 front-end: accept `HO_ALL` and normalize curried expression-head applications (#9636) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The SMT2 front-end rejected valid higher-order inputs using `HO_ALL` and failed on curried applications where the function position is itself an expression (e.g., `((transfer top) 0)`). This update adds `HO_ALL` support and makes curried parsing consistently lower to implicit `select` chains. - **Logic recognition** - Treat `HO_ALL` as an `ALL`-class logic in SMT logic classification. - This unblocks `(set-logic HO_ALL)` in the standard SMT2 command path. - **Curried application parsing** - Extend application-frame handling to support parenthesized expression heads, not only symbol heads. - When the head is an expression, parse application arguments normally and construct nested implicit selects: - `(f a b)` → `(select (select f a) b)` - Preserve existing behavior for symbol-based applications, qualified identifiers, and lambda-led forms. - **Regression coverage** - Add a focused parser/eval regression using the reported higher-order case to lock in behavior. ```smt2 (set-logic HO_ALL) (declare-fun transfer () (-> (-> Int Bool) (-> Int Bool))) (assert (forall ((P (-> Int Bool))) (=> (P 0) ((transfer P) 0)))) (declare-fun top () (-> Int Bool)) (assert (forall ((x Int)) (top x))) (assert (not ((transfer top) 0))) (check-sat) ``` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/parsers/smt2/smt2parser.cpp | 87 +++++++++++++++++++++++++-------- src/solver/smt_logics.h | 2 +- src/test/smt2print_parse.cpp | 17 +++++++ 3 files changed, 84 insertions(+), 22 deletions(-) diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 3601c5a5e..6d1f3a4f2 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -156,12 +156,14 @@ namespace smt2 { unsigned m_expr_spos; unsigned m_param_spos; bool m_as_sort; - app_frame(symbol const & f, unsigned expr_spos, unsigned param_spos, bool as_sort): + bool m_expr_head; + app_frame(symbol const & f, unsigned expr_spos, unsigned param_spos, bool as_sort, bool expr_head = false): expr_frame(EF_APP), m_f(f), m_expr_spos(expr_spos), m_param_spos(param_spos), - m_as_sort(as_sort) {} + m_as_sort(as_sort), + m_expr_head(expr_head) {} }; struct quant_frame : public expr_frame { @@ -1888,23 +1890,7 @@ namespace smt2 { sexpr_stack().pop_back(); } - void push_app_frame() { - SASSERT(curr_is_lparen() || curr_is_identifier()); - unsigned param_spos = m_param_stack.size(); - unsigned expr_spos = expr_stack().size(); - bool has_as, is_lambda; - auto f = parse_qualified_identifier(has_as, is_lambda); - - void * mem = m_stack.allocate(sizeof(app_frame)); - new (mem) app_frame(f, expr_spos, param_spos, has_as); - m_num_expr_frames++; - if (is_lambda) - push_quant_frame(lambda_k); - } - - void push_expr_frame(expr_frame * curr) { - SASSERT(curr_is_lparen()); - next(); + void push_expr_frame_core(expr_frame * curr) { TRACE(push_expr_frame, tout << "push_expr_frame(), curr(): " << m_curr << "\n";); if (curr_is_identifier()) { TRACE(push_expr_frame, tout << "push_expr_frame(), curr_id(): " << curr_id() << "\n";); @@ -1944,6 +1930,49 @@ namespace smt2 { } } + void push_app_frame() { + SASSERT(curr_is_lparen() || curr_is_identifier()); + unsigned param_spos = m_param_stack.size(); + unsigned expr_spos = expr_stack().size(); + bool has_as = false, is_lambda = false; + symbol f = symbol::null; + bool expr_head = false; + + if (curr_is_lparen()) { + next(); + if (curr_is_identifier() && curr_id_is_lambda()) { + is_lambda = true; + f = symbol("select"); + } + else if (curr_is_identifier() && (curr_id_is_underscore() || curr_id_is_as())) { + f = parse_qualified_identifier_core(has_as); + } + else { + expr_head = true; + } + } + else { + f = parse_qualified_identifier(has_as, is_lambda); + } + + void * mem = m_stack.allocate(sizeof(app_frame)); + auto* frame = new (mem) app_frame(f, expr_spos, param_spos, has_as, expr_head); + m_num_expr_frames++; + + if (is_lambda) { + push_quant_frame(lambda_k); + } + else if (expr_head) { + push_expr_frame_core(frame); + } + } + + void push_expr_frame(expr_frame * curr) { + SASSERT(curr_is_lparen()); + next(); + push_expr_frame_core(curr); + } + void pop_app_frame(app_frame * fr) { SASSERT(expr_stack().size() >= fr->m_expr_spos); SASSERT(m_param_stack.size() >= fr->m_param_spos); @@ -1952,6 +1981,23 @@ namespace smt2 { unsigned num_args = expr_stack().size() - fr->m_expr_spos; unsigned num_indices = m_param_stack.size() - fr->m_param_spos; expr_ref t_ref(m()); + if (fr->m_expr_head) { + if (num_args < 2) + throw parser_exception("invalid function application, arguments missing"); + t_ref = expr_stack().get(fr->m_expr_spos); + for (unsigned i = 1; i < num_args; ++i) { + expr* arg = expr_stack().get(fr->m_expr_spos + i); + expr* args[2] = { t_ref.get(), arg }; + m_ctx.mk_app(symbol("select"), + 2, + args, + 0, + nullptr, + nullptr, + t_ref); + } + } + else { local l; if (m_env.find(fr->m_f, l)) { push_local(l); @@ -1977,6 +2023,7 @@ namespace smt2 { fr->m_as_sort ? sort_stack().back() : nullptr, t_ref); } + } expr_stack().shrink(fr->m_expr_spos); m_param_stack.shrink(fr->m_param_spos); if (fr->m_as_sort) @@ -3296,5 +3343,3 @@ sexpr_ref parse_sexpr(cmd_context& ctx, std::istream& is, params_ref const& ps, return p.parse_sexpr_ref(); } - - diff --git a/src/solver/smt_logics.h b/src/solver/smt_logics.h index 9a32e5708..f33ad7f17 100644 --- a/src/solver/smt_logics.h +++ b/src/solver/smt_logics.h @@ -22,7 +22,7 @@ class smt_logics { public: static bool supported_logic(symbol const & s); static bool logic_has_reals_only(symbol const& l); - static bool logic_is_all(symbol const& s) { return s == "ALL"; } + static bool logic_is_all(symbol const& s) { return s == "ALL" || s == "HO_ALL"; } static bool logic_has_uf(symbol const& s); static bool logic_has_arith(symbol const & s); static bool logic_has_bv(symbol const & s); diff --git a/src/test/smt2print_parse.cpp b/src/test/smt2print_parse.cpp index 76b169a4a..0f6f369fb 100644 --- a/src/test/smt2print_parse.cpp +++ b/src/test/smt2print_parse.cpp @@ -160,6 +160,22 @@ void test_repeated_eval() { Z3_del_context(ctx); } +void test_ho_curried_application() { + char const* spec = + "(set-logic HO_ALL)\n" + "(declare-fun transfer () (-> (-> Int Bool) (-> Int Bool)))\n" + "(assert (forall ((P (-> Int Bool))) (=> (P 0) ((transfer P) 0))))\n" + "(declare-fun top () (-> Int Bool))\n" + "(assert (forall ((x Int)) (top x)))\n" + "(assert (not ((transfer top) 0)))\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); @@ -289,6 +305,7 @@ void tst_smt2print_parse() { // Test ? test_repeated_eval(); + test_ho_curried_application(); test_symbol_escape();