mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-04 06:53:58 +00:00
Code Activity

fix #7956

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-30 15:41:40 -07:00
parent 339f0cd5f9
commit 65c9a18c3a
1 changed files with 16 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1621,7 +1621,7 @@ namespace smt2 {
if (curr_id_is_underscore()) { if (curr_id_is_underscore()) {
has_as = false; has_as = false;
return parse_indexed_identifier_core(); return parse_indexed_identifier_core();
} }
else { else {
SASSERT(curr_id_is_as()); SASSERT(curr_id_is_as());
has_as = true; has_as = true;
@ -1638,8 +1638,10 @@ namespace smt2 {
// '(' 'as' <identifier> <sort> ')' // '(' 'as' <identifier> <sort> ')'
// '(' '_' <identifier> <num>+ ')' // '(' '_' <identifier> <num>+ ')'
// '(' 'as' <identifier '(' '_' <identifier> (<num>|<func-decl-ref>)+ ')' <sort> ')' // '(' 'as' <identifier '(' '_' <identifier> (<num>|<func-decl-ref>)+ ')' <sort> ')'
symbol parse_qualified_identifier(bool & has_as) { // '(' lambda (...) <expr> ')'
symbol parse_qualified_identifier(bool & has_as, bool & is_lambda) {
SASSERT(curr_is_lparen() || curr_is_identifier()); SASSERT(curr_is_lparen() || curr_is_identifier());
is_lambda = false;
if (curr_is_identifier()) { if (curr_is_identifier()) {
has_as = false; has_as = false;
symbol r = curr_id(); symbol r = curr_id();
@ -1648,6 +1650,12 @@ namespace smt2 {
} }
SASSERT(curr_is_lparen()); SASSERT(curr_is_lparen());
next(); next();
if (curr_id_is_lambda()) {
is_lambda = true;
has_as = false;
return symbol("select");
}
if (!curr_is_identifier() || (!curr_id_is_underscore() && !curr_id_is_as())) if (!curr_is_identifier() || (!curr_id_is_underscore() && !curr_id_is_as()))
throw parser_exception("invalid qualified/indexed identifier, '_' or 'as' expected"); throw parser_exception("invalid qualified/indexed identifier, '_' or 'as' expected");
return parse_qualified_identifier_core(has_as); return parse_qualified_identifier_core(has_as);
@ -1860,11 +1868,14 @@ namespace smt2 {
SASSERT(curr_is_lparen() || curr_is_identifier()); SASSERT(curr_is_lparen() || curr_is_identifier());
unsigned param_spos = m_param_stack.size(); unsigned param_spos = m_param_stack.size();
unsigned expr_spos = expr_stack().size(); unsigned expr_spos = expr_stack().size();
bool has_as; bool has_as, is_lambda;
symbol f = parse_qualified_identifier(has_as); auto f = parse_qualified_identifier(has_as, is_lambda);
void * mem = m_stack.allocate(sizeof(quant_frame));
void * mem = m_stack.allocate(sizeof(app_frame));
new (mem) app_frame(f, expr_spos, param_spos, has_as); new (mem) app_frame(f, expr_spos, param_spos, has_as);
m_num_expr_frames++; m_num_expr_frames++;
if (is_lambda)
push_quant_frame(lambda_k);
} }
void push_expr_frame(expr_frame * curr) { void push_expr_frame(expr_frame * curr) {