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

SMT2 front-end: accept HO_ALL and normalize curried expression-head applications (#9636)

Browse source 
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>
This commit is contained in:
Copilot 2026-05-26 18:39:38 -07:00 • committed by GitHub
parent 73151f1960
commit 316d249b3f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 84 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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();
}

2
src/solver/smt_logics.h
View file

@ -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);

17
src/test/smt2print_parse.cpp
View file

@ -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();