Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Term parser for smt2
11 : : */
12 : :
13 : : #include "parser/smt2/smt2_term_parser.h"
14 : :
15 : : #include <string.h>
16 : :
17 : : #include "base/check.h"
18 : : #include "base/output.h"
19 : :
20 : : namespace cvc5 {
21 : : namespace parser {
22 : :
23 : : /**
24 : : * Definition of state identifiers when parsing terms
25 : : *
26 : : * This is required for non-recursive parsing of terms. Note that in SMT-LIB,
27 : : * terms generally are of the form (...anything not involving terms... <term>*)
28 : : * However, let-terms, match-terms, and terms appearing within attributes
29 : : * for term annotations (e.g. quantifier patterns) are exceptions to this.
30 : : * Thus, in the main parsing loop in parseTerm below, we require tracking
31 : : * the context we are in, which dictates how to setup parsing the term after
32 : : * the current one.
33 : : *
34 : : * In each state, the stack contains a topmost ParseOp `op` and a list of
35 : : * arguments `args`, which give a recipe for the term we are parsing. The data
36 : : * in these depend on the context we are in, as documented below.
37 : : */
38 : : enum class ParseCtx
39 : : {
40 : : /**
41 : : * NEXT_ARG: in context (<op> <term>* <term>
42 : : * `op` specifies the operator we parsed.
43 : : * `args` contain the accumulated list of arguments.
44 : : */
45 : : NEXT_ARG,
46 : : /**
47 : : * CLOSURE_NEXT_ARG: in context (<closure> <variable_list> <term>* <term>
48 : : * `op` specifies the (closure) operator we parsed.
49 : : * `args` contain the variable list and the accumulated list of arguments.
50 : : */
51 : : CLOSURE_NEXT_ARG,
52 : : /**
53 : : * Let bindings
54 : : *
55 : : * LET_NEXT_BIND: in context (let (<binding>* (<symbol> <term>
56 : : * `op` contains:
57 : : * - d_name: the name of last bound variable.
58 : : *
59 : : * LET_BODY: in context (let (<binding>*) <term>
60 : : */
61 : : LET_NEXT_BIND,
62 : : LET_BODY,
63 : : /**
64 : : * Match terms
65 : : *
66 : : * MATCH_HEAD: in context (match <term>
67 : : *
68 : : * MATCH_NEXT_CASE: in context (match <term> (<case>* (<pattern> <term>
69 : : * `op` contains:
70 : : * - d_type: set to the type of the head.
71 : : * `args` contain the head term and the accumulated list of case terms.
72 : : */
73 : : MATCH_HEAD,
74 : : MATCH_NEXT_CASE,
75 : : /**
76 : : * Term annotations
77 : : *
78 : : * TERM_ANNOTATE_BODY: in context (! <term>
79 : : *
80 : : * TERM_ANNOTATE_NEXT_ATTR: in context (! <term> <attr>* <keyword> <term_spec>
81 : : * where notice that <term_spec> may be a term or a list of terms.
82 : : * `op` contains:
83 : : * - d_expr: the body of the term annotation.
84 : : * - d_kind: the kind to apply to the current <term_spec> (if any).
85 : : * `args` contain the accumulated patterns or quantifier attributes.
86 : : */
87 : : TERM_ANNOTATE_BODY,
88 : : TERM_ANNOTATE_NEXT_ATTR
89 : : };
90 : :
91 : 24437 : Smt2TermParser::Smt2TermParser(Smt2Lexer& lex, Smt2State& state)
92 : 24437 : : d_lex(lex), d_state(state)
93 : : {
94 : 24437 : }
95 : :
96 : 233279 : Term Smt2TermParser::parseTerm()
97 : : {
98 : : // the last parsed term
99 : 233279 : Term ret;
100 : : // a request was made to update the current parse context
101 : 233279 : bool needsUpdateCtx = false;
102 : : // the last token we read
103 : : Token tok;
104 : : // The stack(s) containing the parse context, and the recipe for the
105 : : // current we are building.
106 : 233279 : std::vector<ParseCtx> xstack;
107 : 233279 : std::vector<std::pair<ParseOp, std::vector<Term>>> tstack;
108 : : // Let bindings, dynamically allocated for each let in scope.
109 : 233279 : std::vector<std::vector<std::pair<std::string, Term>>> letBinders;
110 : 233279 : Solver* slv = d_state.getSolver();
111 : 233279 : TermManager& tm = slv->getTermManager();
112 : : do
113 : : {
114 [ - + ][ - + ]: 19179009 : Assert(tstack.size() == xstack.size());
[ - - ]
115 : : // At this point, we are ready to parse the next term
116 : 19179009 : tok = d_lex.nextToken();
117 : 19179008 : Term currTerm;
118 [ + + ][ + - ]: 19179008 : switch (tok)
[ + + ][ + + ]
[ + + ][ + + ]
119 : : {
120 : : // ------------------- open paren
121 : 6583589 : case Token::LPAREN_TOK:
122 : : {
123 [ + + ][ + + ]: 6583589 : tok = d_lex.nextToken();
[ + + ][ + - ]
[ - ]
124 : : switch (tok)
125 : : {
126 : 1844 : case Token::AS_TOK:
127 : : {
128 : : // a standalone qualified identifier
129 : 1844 : ParseOp op = continueParseQualifiedIdentifier(false);
130 : 1844 : ret = op.d_expr;
131 [ + - ][ + + ]: 1844 : if (ret.isNull() || op.d_kind == Kind::INTERNAL_KIND)
[ + + ]
132 : : {
133 : 3 : d_lex.parseError("Unexpected qualified identifier");
134 : : }
135 : 1844 : }
136 : 1843 : break;
137 : 185229 : case Token::INDEX_TOK:
138 : : {
139 : : // a standalone indexed symbol
140 : 185229 : ParseOp op = continueParseIndexedIdentifier(false);
141 : 185225 : ret = op.d_expr;
142 [ - + ]: 185225 : if (ret.isNull())
143 : : {
144 : 0 : d_lex.parseError("Unexpected indexed symbol");
145 : : }
146 : 185225 : }
147 : 185225 : break;
148 : 178753 : case Token::LPAREN_TOK:
149 : : {
150 [ + + ][ - ]: 178753 : tok = d_lex.nextToken();
151 : : switch (tok)
152 : : {
153 : 247 : case Token::AS_TOK:
154 : : {
155 : : // a qualified identifier operator
156 : 247 : ParseOp op = continueParseQualifiedIdentifier(true);
157 : 247 : xstack.emplace_back(ParseCtx::NEXT_ARG);
158 : 247 : tstack.emplace_back(op, std::vector<Term>());
159 : 247 : }
160 : 247 : break;
161 : 178506 : case Token::INDEX_TOK:
162 : : {
163 : : // an indexed identifier operator
164 : 178506 : ParseOp op = continueParseIndexedIdentifier(true);
165 : 178505 : xstack.emplace_back(ParseCtx::NEXT_ARG);
166 : 178505 : tstack.emplace_back(op, std::vector<Term>());
167 : 178505 : }
168 : 178505 : break;
169 : 0 : default:
170 : 0 : d_lex.unexpectedTokenError(
171 : : tok, "Expected SMT-LIBv2 qualified indentifier");
172 : 0 : break;
173 : : }
174 : : }
175 : 178752 : break;
176 : 222599 : case Token::LET_TOK:
177 : : {
178 : 222599 : xstack.emplace_back(ParseCtx::LET_NEXT_BIND);
179 : 222599 : tstack.emplace_back(ParseOp(), std::vector<Term>());
180 : 222599 : needsUpdateCtx = true;
181 : 222599 : letBinders.emplace_back();
182 : : }
183 : 222599 : break;
184 : 164 : case Token::MATCH_TOK:
185 : : {
186 : 164 : xstack.emplace_back(ParseCtx::MATCH_HEAD);
187 : 164 : tstack.emplace_back();
188 : : }
189 : 164 : break;
190 : 20719 : case Token::ATTRIBUTE_TOK:
191 : : {
192 : 20719 : xstack.emplace_back(ParseCtx::TERM_ANNOTATE_BODY);
193 : 20719 : tstack.emplace_back();
194 : : }
195 : 20719 : break;
196 : 5974281 : case Token::SYMBOL:
197 : : case Token::QUOTED_SYMBOL:
198 : : {
199 : : // function identifier
200 : 5974281 : ParseOp op;
201 : 5974281 : op.d_name = tokenStrToSymbol(tok);
202 : 5974281 : std::vector<Term> args;
203 [ + + ]: 5974281 : if (d_state.isClosure(op.d_name))
204 : : {
205 : : // if it is a closure, immediately read the bound variable list
206 : 86800 : d_state.pushScope();
207 : : std::vector<std::pair<std::string, Sort>> sortedVarNames =
208 : 86800 : parseSortedVarList();
209 [ - + ]: 86799 : if (sortedVarNames.empty())
210 : : {
211 : 0 : d_lex.parseError("Expected non-empty sorted variable list");
212 : : }
213 : 86799 : bool freshBinders = d_state.usingFreshBinders();
214 : : // If freshBinders is false, we set fresh to false here. This
215 : : // means that (x Int) appearing in a quantified formula always
216 : : // constructs the same variable.
217 : : // We use the context-dependent version of this method since we
218 : : // may have to account for variables that have appeared in let
219 : : // binders to ensure our let bindings do not lead to variable
220 : : // capturing.
221 : 86799 : std::vector<Term> vs = d_state.bindBoundVarsCtx(
222 : 86799 : sortedVarNames, letBinders, freshBinders);
223 : 86799 : Term vl = tm.mkTerm(Kind::VARIABLE_LIST, vs);
224 : 86799 : args.push_back(vl);
225 : 86799 : xstack.emplace_back(ParseCtx::CLOSURE_NEXT_ARG);
226 : 86799 : }
227 : : else
228 : : {
229 : 5887481 : xstack.emplace_back(ParseCtx::NEXT_ARG);
230 : : }
231 : 5974280 : tstack.emplace_back(op, args);
232 : 5974282 : }
233 : 5974280 : break;
234 : 0 : case Token::UNTERMINATED_QUOTED_SYMBOL:
235 : 0 : d_lex.parseError("Expected SMT-LIBv2 operator", true);
236 : 0 : break;
237 : 0 : default:
238 : 0 : d_lex.unexpectedTokenError(tok, "Expected SMT-LIBv2 operator");
239 : 0 : break;
240 : : }
241 : : }
242 : 6583582 : break;
243 : : // ------------------- close paren
244 : 6163009 : case Token::RPAREN_TOK:
245 : : {
246 : : // should only be here if we are expecting arguments
247 : 6163009 : if (tstack.empty()
248 [ + + ][ + + ]: 6249805 : || (xstack.back() != ParseCtx::NEXT_ARG
[ + + ]
249 [ + + ]: 86796 : && xstack.back() != ParseCtx::CLOSURE_NEXT_ARG))
250 : : {
251 : 6 : d_lex.unexpectedTokenError(
252 : : tok, "Mismatched parentheses in SMT-LIBv2 term");
253 : : }
254 : : // Construct the application term specified by tstack.back()
255 : 6163007 : ParseOp& op = tstack.back().first;
256 : 6163007 : ret = d_state.applyParseOp(op, tstack.back().second);
257 : : // process the scope change if a closure
258 [ + + ]: 6162962 : if (xstack.back() == ParseCtx::CLOSURE_NEXT_ARG)
259 : : {
260 : : // if we were a closure, pop a scope
261 : 86795 : d_state.popScope();
262 : : }
263 : : // pop the stack
264 : 6162962 : tstack.pop_back();
265 : 6162962 : xstack.pop_back();
266 : : }
267 : 6162962 : break;
268 : : // ------------------- base cases
269 : 5479008 : case Token::SYMBOL:
270 : : case Token::QUOTED_SYMBOL:
271 : : {
272 : 5479008 : std::string name = tokenStrToSymbol(tok);
273 : 5479008 : ret = d_state.getVariable(name);
274 : 5479008 : }
275 : 5478997 : break;
276 : 0 : case Token::UNTERMINATED_QUOTED_SYMBOL:
277 : 0 : d_lex.parseError("Expected SMT-LIBv2 term", true);
278 : 0 : break;
279 : 840176 : case Token::INTEGER_LITERAL:
280 : : {
281 : 840178 : ret = d_state.mkRealOrIntFromNumeral(d_lex.tokenStr());
282 : : }
283 : 840175 : break;
284 : 65765 : case Token::DECIMAL_LITERAL:
285 : : {
286 : 65765 : ret = tm.mkReal(d_lex.tokenStr());
287 : : }
288 : 65765 : break;
289 : 12 : case Token::RATIONAL_LITERAL:
290 : : {
291 : 14 : ret = tm.mkReal(d_lex.tokenStr());
292 : : }
293 : 11 : break;
294 : 3335 : case Token::HEX_LITERAL:
295 : : {
296 : 3335 : std::string hexStr = d_lex.tokenStr();
297 : 3335 : hexStr = hexStr.substr(2);
298 : 3335 : ret = tm.mkBitVector(hexStr.size() * 4, hexStr, 16);
299 : 3335 : }
300 : 3335 : break;
301 : 13973 : case Token::BINARY_LITERAL:
302 : : {
303 : 13973 : std::string binStr = d_lex.tokenStr();
304 : 13973 : binStr = binStr.substr(2);
305 : 13973 : ret = tm.mkBitVector(binStr.size(), binStr, 2);
306 : 13973 : }
307 : 13973 : break;
308 : 2047 : case Token::FIELD_LITERAL:
309 : : {
310 : 2047 : std::string ffStr = d_lex.tokenStr();
311 [ - + ][ - + ]: 2047 : Assert(ffStr.find("#f") == 0);
[ - - ]
312 : 2047 : size_t mPos = ffStr.find("m");
313 [ - + ][ - + ]: 2047 : Assert(mPos > 2);
[ - - ]
314 : 2047 : std::string ffValStr = ffStr.substr(2, mPos - 2);
315 : 2047 : std::string ffModStr = ffStr.substr(mPos + 1);
316 : 2047 : Sort ffSort = tm.mkFiniteFieldSort(ffModStr);
317 : 2047 : ret = tm.mkFiniteFieldElem(ffValStr, ffSort);
318 : 2047 : }
319 : 2047 : break;
320 : 28093 : case Token::STRING_LITERAL:
321 : : {
322 : 28093 : std::string s = d_lex.tokenStr();
323 : 28093 : unescapeString(s);
324 : 28093 : ret = tm.mkString(s, true);
325 : 28093 : }
326 : 28093 : break;
327 : 1 : default:
328 : 3 : d_lex.unexpectedTokenError(tok, "Expected SMT-LIBv2 term");
329 : 0 : break;
330 : : }
331 : :
332 : : // Based on the current context, setup next parsed term.
333 : : // We do this only if a context is allocated (!tstack.empty()) and we
334 : : // either just finished parsing a term (!ret.isNull()), or otherwise have
335 : : // indicated that we need to update the context (needsUpdateCtx).
336 [ + + ][ + + ]: 32217716 : while (!tstack.empty() && (!ret.isNull() || needsUpdateCtx))
[ + + ][ + + ]
337 : : {
338 : 13038777 : needsUpdateCtx = false;
339 [ + + ][ + + ]: 13038777 : switch (xstack.back())
[ + + ][ + - ]
340 : : {
341 : : // ------------------------- argument lists
342 : 12272786 : case ParseCtx::NEXT_ARG:
343 : : case ParseCtx::CLOSURE_NEXT_ARG:
344 : : {
345 [ - + ][ - + ]: 12272786 : Assert(!ret.isNull());
[ - - ]
346 : : // add it to the list of arguments and clear
347 : 12272786 : tstack.back().second.push_back(ret);
348 : 12272786 : ret = Term();
349 : : }
350 : 12272786 : break;
351 : : // ------------------------- let terms
352 : 479582 : case ParseCtx::LET_NEXT_BIND:
353 : : {
354 : : // if we parsed a term, process it as a binding
355 [ + + ]: 479582 : if (!ret.isNull())
356 : : {
357 [ - + ][ - + ]: 256983 : Assert(!letBinders.empty());
[ - - ]
358 : 256983 : std::vector<std::pair<std::string, Term>>& bs = letBinders.back();
359 : : // add binding from the symbol to ret
360 : 256983 : bs.emplace_back(tstack.back().first.d_name, ret);
361 : 256983 : ret = Term();
362 : : // close the current binding
363 : 256983 : d_lex.eatToken(Token::RPAREN_TOK);
364 : : }
365 : : else
366 : : {
367 : : // eat the opening left parenthesis of the binding list
368 : 222599 : d_lex.eatToken(Token::LPAREN_TOK);
369 : : }
370 : : // see if there is another binding
371 [ + + ]: 479582 : if (d_lex.eatTokenChoice(Token::LPAREN_TOK, Token::RPAREN_TOK))
372 : : {
373 : : // (, another binding: setup parsing the next term
374 : : // get the symbol and store in the ParseOp
375 : 256984 : tstack.back().first.d_name = parseSymbol(CHECK_NONE, SYM_VARIABLE);
376 : : }
377 : : else
378 : : {
379 : : // ), we are now looking for the body of the let
380 : 222598 : xstack[xstack.size() - 1] = ParseCtx::LET_BODY;
381 : : // push scope
382 : 222598 : d_state.pushScope();
383 : : // implement the bindings
384 [ - + ][ - + ]: 222598 : Assert(!letBinders.empty());
[ - - ]
385 : : const std::vector<std::pair<std::string, Term>>& bs =
386 : 222598 : letBinders.back();
387 [ + + ]: 479581 : for (const std::pair<std::string, Term>& b : bs)
388 : : {
389 : 256983 : d_state.defineVar(b.first, b.second);
390 : : }
391 : : }
392 : : }
393 : 479582 : break;
394 : 222598 : case ParseCtx::LET_BODY:
395 : : {
396 : : // the let body is the returned term
397 : 222598 : d_lex.eatToken(Token::RPAREN_TOK);
398 : 222598 : xstack.pop_back();
399 : 222598 : tstack.pop_back();
400 : : // pop scope
401 : 222598 : d_state.popScope();
402 : : // Done with the binders now. We clear this only at this point since
403 : : // the let binders may to pertinent to avoid illegal substitutions
404 : : // from lets.
405 : 222598 : letBinders.pop_back();
406 : : }
407 : 222598 : break;
408 : : // ------------------------- match terms
409 : 164 : case ParseCtx::MATCH_HEAD:
410 : : {
411 [ - + ][ - + ]: 164 : Assert(!ret.isNull());
[ - - ]
412 : : // add the head
413 : 164 : tstack.back().second.push_back(ret);
414 : 164 : Sort retSort = ret.getSort();
415 : : // eagerly check if datatype
416 [ - + ]: 164 : if (!retSort.isDatatype())
417 : : {
418 : 0 : d_lex.parseError("Cannot match on non-datatype term.");
419 : : }
420 : : // we use a placeholder to store the type (retSort), which is
421 : : // used during MATCH_NEXT_CASE
422 : 164 : tstack.back().first.d_kind = Kind::INTERNAL_KIND;
423 : 164 : tstack.back().first.d_expr = tm.mkConst(retSort);
424 : 164 : ret = Term();
425 : 164 : xstack[xstack.size() - 1] = ParseCtx::MATCH_NEXT_CASE;
426 : 164 : needsUpdateCtx = true;
427 : 164 : }
428 : 164 : break;
429 : 528 : case ParseCtx::MATCH_NEXT_CASE:
430 : : {
431 [ + + ]: 528 : if (!ret.isNull())
432 : : {
433 : : // add it to the list of arguments and clear
434 : 364 : tstack.back().second.push_back(ret);
435 : 364 : ret = Term();
436 : : // pop the scope
437 : 364 : d_state.popScope();
438 : : }
439 : : else
440 : : {
441 : : // eat the opening left parenthesis of the case list
442 : 164 : d_lex.eatToken(Token::LPAREN_TOK);
443 : : }
444 : : // see if there is another case
445 [ + + ]: 528 : if (d_lex.eatTokenChoice(Token::LPAREN_TOK, Token::RPAREN_TOK))
446 : : {
447 : : // push the scope
448 : 364 : d_state.pushScope();
449 : : // parse the pattern, which also does the binding
450 [ - + ][ - + ]: 364 : Assert(!tstack.back().first.d_expr.isNull());
[ - - ]
451 : 364 : std::vector<Term> boundVars;
452 : : Term pattern = parseMatchCasePattern(
453 : 364 : tstack.back().first.d_expr.getSort(), boundVars);
454 : : // If we bound variables when parsing the pattern, we will construct
455 : : // a match bind case
456 : 364 : ParseOp op;
457 : 364 : std::vector<Term> args;
458 [ + + ]: 364 : if (!boundVars.empty())
459 : : {
460 : 190 : op.d_kind = Kind::MATCH_BIND_CASE;
461 : 190 : Term vl = tm.mkTerm(Kind::VARIABLE_LIST, boundVars);
462 : 190 : args.push_back(tm.mkTerm(Kind::VARIABLE_LIST, boundVars));
463 : 190 : }
464 : : else
465 : : {
466 : 174 : op.d_kind = Kind::MATCH_CASE;
467 : : }
468 : 364 : args.push_back(pattern);
469 : : // we now look for the body of the case + closing right parenthesis
470 : 364 : xstack.emplace_back(ParseCtx::NEXT_ARG);
471 : 364 : tstack.emplace_back(op, args);
472 : 364 : }
473 : : else
474 : : {
475 : : // Finished with match, now just wait for the closing right
476 : : // parenthesis. Set the kind to construct as MATCH and clear the
477 : : // head sort.
478 : 164 : ParseOp& op = tstack.back().first;
479 : 164 : op.d_kind = Kind::MATCH;
480 : 164 : op.d_expr = Term();
481 : 164 : xstack[xstack.size() - 1] = ParseCtx::NEXT_ARG;
482 : : }
483 : : }
484 : 528 : break;
485 : : // ------------------------- annotated terms
486 : 20719 : case ParseCtx::TERM_ANNOTATE_BODY:
487 : : {
488 : : // save ret as the expression and clear
489 : 20719 : tstack.back().first.d_expr = ret;
490 : 20719 : ret = Term();
491 : : // now parse attribute list
492 : 20719 : xstack[xstack.size() - 1] = ParseCtx::TERM_ANNOTATE_NEXT_ATTR;
493 : 20719 : needsUpdateCtx = true;
494 : : // ensure there is at least one attribute
495 : 20719 : tok = d_lex.peekToken();
496 [ - + ]: 20719 : if (tok == Token::RPAREN_TOK)
497 : : {
498 : 0 : d_lex.parseError(
499 : : "Expecting at least one attribute for term annotation.");
500 : : }
501 : : }
502 : 20719 : break;
503 : 42400 : case ParseCtx::TERM_ANNOTATE_NEXT_ATTR:
504 : : {
505 [ + + ]: 42400 : if (!ret.isNull())
506 : : {
507 : : // if we got here, we either:
508 : : // (1) parsed a single term (the current ParseOp::d_kind was set)
509 : : // (2) a list of terms in a nested context.
510 [ + + ]: 9522 : if (tstack.back().first.d_kind != Kind::NULL_TERM)
511 : : {
512 : : // if (1), apply d_kind to the argument and reset d_kind
513 : 24 : ret = tm.mkTerm(tstack.back().first.d_kind, {ret});
514 : 12 : tstack.back().first.d_kind = Kind::NULL_TERM;
515 : : }
516 : 9522 : tstack.back().second.push_back(ret);
517 : 9522 : ret = Term();
518 : : }
519 : : // see if there is another keyword
520 [ + + ]: 42400 : if (d_lex.eatTokenChoice(Token::KEYWORD, Token::RPAREN_TOK))
521 : : {
522 : 21682 : std::string key = d_lex.tokenStr();
523 : : // Based on the keyword, determine the context.
524 : : // Set needsUpdateCtx to true if we are finished parsing the
525 : : // current attribute.
526 : 21682 : Kind attrKind = Kind::NULL_TERM;
527 : 21682 : Term attrValue;
528 [ + + ]: 21682 : if (key == ":inst-add-to-pool")
529 : : {
530 : 28 : attrKind = Kind::INST_ADD_TO_POOL;
531 : : }
532 [ - + ]: 21654 : else if (key == ":quant-inst-max-level")
533 : : {
534 : : // a numeral
535 : 0 : d_lex.eatToken(Token::INTEGER_LITERAL);
536 : 0 : attrValue = tm.mkInteger(d_lex.tokenStr());
537 : : }
538 [ + + ]: 21654 : else if (key == ":named")
539 : : {
540 [ - + ][ - + ]: 11261 : Assert(!tstack.back().first.d_expr.isNull());
[ - - ]
541 : : // expression is the body of the term annotation
542 : 11261 : std::string sym = parseSymbol(CHECK_UNDECLARED, SYM_VARIABLE);
543 : 11262 : d_state.notifyNamedExpression(tstack.back().first.d_expr, sym);
544 : 11260 : needsUpdateCtx = true;
545 : 11261 : }
546 [ + + ]: 10393 : else if (key == ":no-pattern")
547 : : {
548 : : // a single term, set the current kind
549 : 12 : tstack.back().first.d_kind = Kind::INST_NO_PATTERN;
550 : : }
551 [ + + ]: 10381 : else if (key == ":pattern")
552 : : {
553 : 9429 : attrKind = Kind::INST_PATTERN;
554 : : }
555 [ + + ]: 952 : else if (key == ":pool")
556 : : {
557 : 44 : attrKind = Kind::INST_POOL;
558 : : }
559 [ + + ]: 908 : else if (key == ":qid")
560 : : {
561 : 539 : std::string sym = parseSymbol(CHECK_NONE, SYM_VARIABLE);
562 : : // must create a variable whose name is the name of the quantified
563 : : // formula, not a string.
564 : 539 : attrValue = tm.mkConst(tm.getBooleanSort(), sym);
565 : 539 : }
566 [ + + ]: 369 : else if (key == ":skolem-add-to-pool")
567 : : {
568 : 16 : attrKind = Kind::SKOLEM_ADD_TO_POOL;
569 : : }
570 : : else
571 : : {
572 : : // warn that the attribute is not supported
573 : 353 : d_state.attributeNotSupported(d_lex.tokenStr());
574 [ - + ]: 353 : tok = d_lex.nextToken();
575 : : // We don't know whether to expect an attribute value. Thus,
576 : : // we will either see keyword (the next attribute), rparen
577 : : // (the term annotation is finished), or else parse as generic
578 : : // symbolic expression for the current attribute.
579 : : switch (tok)
580 : : {
581 : 0 : case Token::KEYWORD:
582 : : case Token::RPAREN_TOK:
583 : : // finished with this attribute, go to the next one if it
584 : : // exists.
585 : 0 : d_lex.reinsertToken(tok);
586 : 0 : break;
587 : 353 : default:
588 : : // ignore the symbolic expression that follows
589 : 353 : d_lex.reinsertToken(tok);
590 : 353 : parseSymbolicExpr();
591 : : // will parse another attribute
592 : 353 : break;
593 : : }
594 : 353 : needsUpdateCtx = true;
595 : : }
596 [ + + ]: 21681 : if (attrKind != Kind::NULL_TERM)
597 : : {
598 : : // e.g. `:pattern (t1 ... tn)`, where we have parsed `:pattern (`
599 : 9517 : d_lex.eatToken(Token::LPAREN_TOK);
600 : : // Corner case: the list of terms is empty. This is a legal
601 : : // pattern in SMT-LIB, and hence we ignore it, for other
602 : : // attributes we throw an error.
603 [ + + ]: 9517 : if (d_lex.peekToken() == Token::RPAREN_TOK)
604 : : {
605 [ + - ]: 7 : if (attrKind == Kind::INST_PATTERN)
606 : : {
607 : : // silently ignores
608 : 7 : d_lex.eatToken(Token::RPAREN_TOK);
609 : : }
610 : : else
611 : : {
612 : 0 : d_lex.parseError(
613 : : "Expecting at least one term in annotation.");
614 : : }
615 : 7 : needsUpdateCtx = true;
616 : : }
617 : : else
618 : : {
619 : : // Will parse list as arguments to the kind + closing
620 : : // parenthesis.
621 : 9510 : ParseOp op;
622 : 9510 : op.d_kind = attrKind;
623 : 9510 : tstack.emplace_back(op, std::vector<Term>());
624 : 9510 : xstack.emplace_back(ParseCtx::NEXT_ARG);
625 : 9510 : }
626 : : }
627 [ + + ]: 12164 : else if (!attrValue.isNull())
628 : : {
629 : : // if we constructed a term as the attribute value, make into
630 : : // an INST_ATTRIBUTE and add it to args
631 : 539 : std::string keyName = key.substr(1);
632 : 539 : Term keyword = tm.mkString(keyName);
633 : : Term iattr =
634 : 2156 : tm.mkTerm(Kind::INST_ATTRIBUTE, {keyword, attrValue});
635 : 539 : tstack.back().second.push_back(iattr);
636 : 539 : needsUpdateCtx = true;
637 : 539 : }
638 : 21683 : }
639 : : // if we instead saw a RPAREN_TOK, we are finished
640 : : else
641 : : {
642 [ - + ][ - + ]: 20718 : Assert(!tstack.back().first.d_expr.isNull());
[ - - ]
643 : : // finished parsing attributes, we will return the original term
644 : 20718 : ret = tstack.back().first.d_expr;
645 : 20718 : Term ipl;
646 : : // if args non-empty, construct an instantiation pattern list
647 [ + + ]: 20718 : if (!tstack.back().second.empty())
648 : : {
649 : 9397 : ipl = tm.mkTerm(Kind::INST_PATTERN_LIST, tstack.back().second);
650 : : }
651 : 20718 : xstack.pop_back();
652 : 20718 : tstack.pop_back();
653 : : // If we constructed an instantiation pattern list, it should have
654 : : // been a quantified formula body. Check the next scope up.
655 [ + + ]: 20718 : if (!ipl.isNull())
656 : : {
657 [ + - ]: 18794 : if (tstack.empty() || xstack.back() != ParseCtx::CLOSURE_NEXT_ARG
658 [ + - ][ - + ]: 18794 : || tstack.back().second.size() != 1)
[ - + ]
659 : : {
660 : 0 : d_lex.parseError(
661 : : "Patterns and quantifier attributes should be applied to "
662 : : "quantified formula bodies only.");
663 : : }
664 : : // Push ret and the instantiation pattern list and clear. We
665 : : // wait for the closing parenthesis, which should follow.
666 : 9397 : tstack.back().second.push_back(ret);
667 : 9397 : tstack.back().second.push_back(ipl);
668 : 9397 : ret = Term();
669 : : }
670 : 20718 : }
671 : : }
672 : 42399 : break;
673 : 0 : default: break;
674 : : }
675 : : }
676 : : // otherwise ret will be returned
677 [ + + ]: 19179008 : } while (!tstack.empty());
678 : 466418 : return ret;
679 : 233489 : }
680 : :
681 : 4404 : std::vector<Term> Smt2TermParser::parseTermList()
682 : : {
683 : 4404 : d_lex.eatToken(Token::LPAREN_TOK);
684 : 4404 : std::vector<Term> terms;
685 : 4404 : Token tok = d_lex.nextToken();
686 [ + + ]: 8991 : while (tok != Token::RPAREN_TOK)
687 : : {
688 : 4592 : d_lex.reinsertToken(tok);
689 : 4592 : Term t = parseTerm();
690 : 4587 : terms.push_back(t);
691 : 4587 : tok = d_lex.nextToken();
692 : 4587 : }
693 : 4399 : return terms;
694 : 5 : }
695 : :
696 : 27147 : Term Smt2TermParser::parseSymbolicExpr()
697 : : {
698 : 27147 : Term ret;
699 : : Token tok;
700 : 27147 : std::vector<std::vector<Term>> sstack;
701 : 27147 : Solver* slv = d_state.getSolver();
702 : 27147 : TermManager& tm = slv->getTermManager();
703 : 27147 : Sort dummyType = tm.getBooleanSort();
704 : : do
705 : : {
706 : 27214 : tok = d_lex.nextToken();
707 [ + + ][ + + ]: 27214 : switch (tok)
708 : : {
709 : : // ------------------- open paren
710 : 12 : case Token::LPAREN_TOK:
711 : : {
712 : 12 : sstack.emplace_back(std::vector<Term>());
713 : : }
714 : 12 : break;
715 : : // ------------------- close paren
716 : 11 : case Token::RPAREN_TOK:
717 : : {
718 [ - + ]: 11 : if (sstack.empty())
719 : : {
720 : 0 : d_lex.unexpectedTokenError(
721 : : tok, "Mismatched parentheses in SMT-LIBv2 s-expression");
722 : : }
723 : 11 : ret = tm.mkTerm(Kind::SEXPR, sstack.back());
724 : : // pop the stack
725 : 11 : sstack.pop_back();
726 : : }
727 : 11 : break;
728 : 1 : case Token::EOF_TOK:
729 : : {
730 : 3 : d_lex.parseError("Expected SMT-LIBv2 s-expression");
731 : : }
732 : 0 : break;
733 : : // ------------------- base case
734 : 27190 : default:
735 : : {
736 : : // note that there are no tokens that are forbidden here
737 : 27190 : std::string str = d_lex.tokenStr();
738 : 27190 : ret = tm.mkVar(dummyType, str);
739 : 27190 : }
740 : 27190 : break;
741 : : }
742 [ + + ]: 27213 : if (!ret.isNull())
743 : : {
744 : : // add it to the list and reset ret
745 [ + + ]: 27201 : if (!sstack.empty())
746 : : {
747 : 55 : sstack.back().push_back(ret);
748 : 55 : ret = Term();
749 : : }
750 : : // otherwise it will be returned
751 : : }
752 [ + + ]: 27213 : } while (!sstack.empty());
753 [ - + ][ - + ]: 27146 : Assert(!ret.isNull());
[ - - ]
754 : 54292 : return ret;
755 : 27149 : }
756 : :
757 : 605897 : Sort Smt2TermParser::parseSort()
758 : : {
759 : 605897 : Sort ret;
760 : : Token tok;
761 : 605897 : std::vector<std::pair<std::string, std::vector<Sort>>> sstack;
762 : : do
763 : : {
764 : 726446 : tok = d_lex.nextToken();
765 [ + + ][ + - ]: 726446 : switch (tok)
766 : : {
767 : : // ------------------- open paren
768 : 75724 : case Token::LPAREN_TOK:
769 : : {
770 [ + + ][ - ]: 75724 : tok = d_lex.nextToken();
771 : : switch (tok)
772 : : {
773 : 34578 : case Token::INDEX_TOK:
774 : : {
775 : : // a standalone indexed symbol
776 : 34578 : std::string name = parseSymbol(CHECK_NONE, SYM_SORT);
777 : 34578 : std::vector<std::string> numerals = parseNumeralList();
778 : 34578 : d_lex.eatToken(Token::RPAREN_TOK);
779 : 34578 : ret = d_state.getIndexedSort(name, numerals);
780 : 34579 : }
781 : 34577 : break;
782 : 41146 : case Token::SYMBOL:
783 : : case Token::QUOTED_SYMBOL:
784 : : {
785 : : // sort constructor identifier
786 : 41146 : std::string name = tokenStrToSymbol(tok);
787 : : // open a new stack frame
788 : 41146 : std::vector<Sort> emptyArgs;
789 : 41146 : sstack.emplace_back(name, emptyArgs);
790 : 41146 : }
791 : 41146 : break;
792 : 0 : default:
793 : : // NOTE: it is possible to have sorts e.g.
794 : : // ((_ FixedSizeList 4) Real) where tok would be LPAREN_TOK here.
795 : : // However, we have no such examples in cvc5 currently.
796 : 0 : d_lex.unexpectedTokenError(tok,
797 : : "Expected SMT-LIBv2 sort constructor");
798 : 0 : break;
799 : : }
800 : : }
801 : 75723 : break;
802 : : // ------------------- close paren
803 : 41146 : case Token::RPAREN_TOK:
804 : : {
805 [ - + ]: 41146 : if (sstack.empty())
806 : : {
807 : 0 : d_lex.unexpectedTokenError(
808 : : tok, "Mismatched parentheses in SMT-LIBv2 sort");
809 : : }
810 : : // Construct the (parametric) sort specified by sstack.back()
811 : 82289 : ret = d_state.getParametricSort(sstack.back().first,
812 : 82289 : sstack.back().second);
813 : : // pop the stack
814 : 41143 : sstack.pop_back();
815 : : }
816 : 41143 : break;
817 : : // ------------------- a simple (defined or builtin) sort
818 : 609576 : case Token::SYMBOL:
819 : : case Token::QUOTED_SYMBOL:
820 : : {
821 : 609576 : std::string name = tokenStrToSymbol(tok);
822 : 609576 : ret = d_state.getSort(name);
823 : 609576 : }
824 : 609575 : break;
825 : 0 : default:
826 : 0 : d_lex.unexpectedTokenError(tok, "Expected SMT-LIBv2 sort");
827 : 0 : break;
828 : : }
829 [ + + ]: 726441 : if (!ret.isNull())
830 : : {
831 : : // add it to the list and reset ret
832 [ + + ]: 685295 : if (!sstack.empty())
833 : : {
834 : 79403 : sstack.back().second.push_back(ret);
835 : 79403 : ret = Sort();
836 : : }
837 : : // otherwise it will be returned
838 : : }
839 [ + + ]: 726441 : } while (!sstack.empty());
840 [ - + ][ - + ]: 605892 : Assert(!ret.isNull());
[ - - ]
841 : 1211784 : return ret;
842 : 605902 : }
843 : :
844 : 320532 : std::vector<Sort> Smt2TermParser::parseSortList()
845 : : {
846 : 320532 : d_lex.eatToken(Token::LPAREN_TOK);
847 : 320531 : std::vector<Sort> sorts;
848 : 320531 : Token tok = d_lex.nextToken();
849 [ + + ]: 395031 : while (tok != Token::RPAREN_TOK)
850 : : {
851 : 74501 : d_lex.reinsertToken(tok);
852 : 74501 : Sort s = parseSort();
853 : 74500 : sorts.push_back(s);
854 : 74500 : tok = d_lex.nextToken();
855 : 74500 : }
856 : 320530 : return sorts;
857 : 1 : }
858 : :
859 : 97258 : std::vector<std::pair<std::string, Sort>> Smt2TermParser::parseSortedVarList()
860 : : {
861 : 97258 : std::vector<std::pair<std::string, Sort>> varList;
862 : 97258 : d_lex.eatToken(Token::LPAREN_TOK);
863 : 97258 : std::string name;
864 : 97258 : Sort t;
865 : : // while the next token is LPAREN, exit if RPAREN
866 [ + + ]: 271669 : while (d_lex.eatTokenChoice(Token::LPAREN_TOK, Token::RPAREN_TOK))
867 : : {
868 : 174412 : name = parseSymbol(CHECK_NONE, SYM_VARIABLE);
869 : 174412 : t = parseSort();
870 : 174411 : varList.emplace_back(name, t);
871 : 174411 : d_lex.eatToken(Token::RPAREN_TOK);
872 : : }
873 : 194512 : return varList;
874 : 97262 : }
875 : :
876 : 1246129 : std::string Smt2TermParser::parseSymbol(DeclarationCheck check, SymbolType type)
877 : : {
878 : 1246129 : Token tok = d_lex.nextToken();
879 : 1246129 : std::string id = tokenStrToSymbol(tok);
880 : : // run the check
881 [ + - ]: 1246129 : if (!d_state.isAbstractValue(id))
882 : : {
883 : : // if an abstract value, SolverEngine handles declaration
884 : 1246131 : d_state.checkDeclaration(id, check, type);
885 : : }
886 : 1246128 : return id;
887 : 1 : }
888 : :
889 : 954 : std::vector<std::string> Smt2TermParser::parseSymbolList(DeclarationCheck check,
890 : : SymbolType type)
891 : : {
892 : 954 : d_lex.eatToken(Token::LPAREN_TOK);
893 : 954 : std::vector<std::string> symbols;
894 : 954 : Token tok = d_lex.nextToken();
895 [ + + ]: 1216 : while (tok != Token::RPAREN_TOK)
896 : : {
897 : 262 : d_lex.reinsertToken(tok);
898 : 262 : std::string sym = parseSymbol(check, type);
899 : 262 : symbols.push_back(sym);
900 : 262 : tok = d_lex.nextToken();
901 : 262 : }
902 : 954 : return symbols;
903 : 0 : }
904 : :
905 : 27155 : std::string Smt2TermParser::parseKeyword()
906 : : {
907 : 27155 : d_lex.eatToken(Token::KEYWORD);
908 : 27155 : std::string s = d_lex.tokenStr();
909 : : // strip off the initial colon
910 : 54310 : return s.erase(0, 1);
911 : 27155 : }
912 : :
913 : 808 : Grammar* Smt2TermParser::parseGrammar(const std::vector<Term>& sygusVars)
914 : : {
915 : : // We read a sorted variable list ((<symbol> <sort>)^n+1)
916 : : std::vector<std::pair<std::string, Sort>> sortedVarNames =
917 : 808 : parseSortedVarList();
918 : : // non-terminal symbols in the pre-declaration are locally scoped
919 : 808 : d_state.pushScope();
920 : 808 : std::vector<Term> ntSyms;
921 [ + + ]: 2602 : for (std::pair<std::string, Sort>& i : sortedVarNames)
922 : : {
923 : 1794 : d_state.checkDeclaration(i.first, CHECK_UNDECLARED, SYM_SORT);
924 : : // make the non-terminal symbol, which will be parsed as an ordinary
925 : : // free variable.
926 : 1794 : Term nts = d_state.bindBoundVar(i.first, i.second);
927 : 1794 : ntSyms.push_back(nts);
928 : 1794 : }
929 : 808 : Grammar* ret = d_state.mkGrammar(sygusVars, ntSyms);
930 : : // Parse (<GroupedRuleList>^n+1)
931 : 808 : d_lex.eatToken(Token::LPAREN_TOK);
932 [ + + ]: 2596 : for (size_t i = 0, nnts = ntSyms.size(); i < nnts; i++)
933 : : {
934 : : // start the non-terminal definition
935 : 1790 : d_lex.eatToken(Token::LPAREN_TOK);
936 : 1790 : std::string name = parseSymbol(CHECK_DECLARED, SYM_VARIABLE);
937 : 1790 : Sort t = parseSort();
938 : : // check that it matches sortedVarNames
939 [ - + ]: 1790 : if (sortedVarNames[i].first != name)
940 : : {
941 : 0 : std::stringstream sse;
942 : : sse << "Grouped rule listing " << name
943 : : << " does not match the name (in order) from the predeclaration ("
944 : 0 : << sortedVarNames[i].first << ")." << std::endl;
945 : 0 : d_lex.parseError(sse.str().c_str());
946 : 0 : }
947 [ - + ]: 1790 : if (sortedVarNames[i].second != t)
948 : : {
949 : 0 : std::stringstream sse;
950 : : sse << "Type for grouped rule listing " << name
951 : 0 : << " does not match the type (in order) from the predeclaration ("
952 : 0 : << sortedVarNames[i].second << ")." << std::endl;
953 : 0 : d_lex.parseError(sse.str().c_str());
954 : 0 : }
955 : : // read the grouped rule listing (<GTerm>+)
956 : 1790 : d_lex.eatToken(Token::LPAREN_TOK);
957 : 1790 : Token tok = d_lex.nextToken();
958 [ + + ]: 9422 : while (tok != Token::RPAREN_TOK)
959 : : {
960 : : // Lookahead for Constant/Variable.
961 : 7634 : bool parsedGTerm = false;
962 [ + + ]: 7634 : if (tok == Token::LPAREN_TOK)
963 : : {
964 : 4317 : Token tok2 = d_lex.nextToken();
965 [ + + ]: 4317 : if (tok2 == Token::SYMBOL)
966 : : {
967 : 4297 : std::string tokenStr(d_lex.tokenStr());
968 [ + + ]: 4297 : if (tokenStr == "Constant")
969 : : {
970 : 124 : t = parseSort();
971 : 124 : ret->addAnyConstant(ntSyms[i]);
972 : 124 : d_lex.eatToken(Token::RPAREN_TOK);
973 : 124 : parsedGTerm = true;
974 : : }
975 [ + + ]: 4173 : else if (tokenStr == "Variable")
976 : : {
977 : 51 : t = parseSort();
978 : 51 : ret->addAnyVariable(ntSyms[i]);
979 : 51 : d_lex.eatToken(Token::RPAREN_TOK);
980 : 51 : parsedGTerm = true;
981 : : }
982 : : else
983 : : {
984 : : // Did not process tok2.
985 : 4122 : d_lex.reinsertToken(tok2);
986 : : }
987 : 4297 : }
988 : : else
989 : : {
990 : : // Did not process tok2.
991 : 20 : d_lex.reinsertToken(tok2);
992 : : }
993 : : }
994 [ + + ]: 7634 : if (!parsedGTerm)
995 : : {
996 : : // We did not process tok. Note that Lex::d_peeked may contain
997 : : // {tok2, LPAREN_TOK} or {tok}.
998 : 7459 : d_lex.reinsertToken(tok);
999 : : // parse ordinary term
1000 : 7459 : Term e = parseTerm();
1001 : 7457 : ret->addRule(ntSyms[i], e);
1002 : 7457 : }
1003 : 7632 : tok = d_lex.nextToken();
1004 : : }
1005 : : // finish the non-terminal
1006 : 1788 : d_lex.eatToken(Token::RPAREN_TOK);
1007 : 1792 : }
1008 : 806 : d_lex.eatToken(Token::RPAREN_TOK);
1009 : : // pop scope from the pre-declaration
1010 : 806 : d_state.popScope();
1011 : 806 : return ret;
1012 : 810 : }
1013 : :
1014 : 1905 : Grammar* Smt2TermParser::parseGrammarOrNull(const std::vector<Term>& sygusVars)
1015 : : {
1016 : 1905 : Token t = d_lex.peekToken();
1017 : : // note that we assume that the grammar is not present if the input continues
1018 : : // with anything other than left parenthesis.
1019 [ + + ]: 1905 : if (t != Token::LPAREN_TOK)
1020 : : {
1021 : 1097 : return nullptr;
1022 : : }
1023 : 808 : return parseGrammar(sygusVars);
1024 : : }
1025 : :
1026 : 25211 : uint32_t Smt2TermParser::parseIntegerNumeral()
1027 : : {
1028 : 25211 : d_lex.eatToken(Token::INTEGER_LITERAL);
1029 : 25210 : return tokenStrToUnsigned();
1030 : : }
1031 : :
1032 : 405062 : uint32_t Smt2TermParser::tokenStrToUnsigned()
1033 : : {
1034 : : // forbid leading zeroes if in strict mode
1035 : 405062 : std::string token = d_lex.tokenStr();
1036 [ + + ]: 405062 : if (d_lex.isStrict())
1037 : : {
1038 [ + + ][ - + ]: 17 : if (token.size() > 1 && token[0] == '0')
[ - + ]
1039 : : {
1040 : 0 : d_lex.parseError("Numerals with leading zeroes are forbidden");
1041 : : }
1042 : : }
1043 [ + + ][ + + ]: 405062 : if (token.size() > 1 && token[0] == '-')
[ + + ]
1044 : : {
1045 : 3 : d_lex.parseError("Negative numerals are forbidden in indices");
1046 : : }
1047 : 405061 : uint32_t result = d_state.parseStringToUnsigned(token);
1048 : 405061 : return result;
1049 : 405062 : }
1050 : :
1051 : 13352238 : std::string Smt2TermParser::tokenStrToSymbol(Token tok)
1052 : : {
1053 : 13352238 : std::string id;
1054 [ + + ][ - - ]: 13352238 : switch (tok)
1055 : : {
1056 : 13340569 : case Token::SYMBOL: id = d_lex.tokenStr(); break;
1057 : 11669 : case Token::QUOTED_SYMBOL:
1058 : 11669 : id = d_lex.tokenStr();
1059 : : // strip off the quotes
1060 : 11669 : id = id.erase(0, 1);
1061 : 11669 : id = id.erase(id.size() - 1, 1);
1062 : 11669 : break;
1063 : 0 : case Token::UNTERMINATED_QUOTED_SYMBOL:
1064 : 0 : d_lex.parseError("Expected SMT-LIBv2 symbol", true);
1065 : 0 : break;
1066 : 0 : default:
1067 : 0 : d_lex.unexpectedTokenError(tok, "Expected SMT-LIBv2 symbol");
1068 : 0 : break;
1069 : : }
1070 : 13352238 : return id;
1071 : 0 : }
1072 : :
1073 : 34578 : std::vector<std::string> Smt2TermParser::parseNumeralList()
1074 : : {
1075 : 34578 : std::vector<std::string> numerals;
1076 : 34578 : Token tok = d_lex.nextToken();
1077 [ + + ]: 69664 : while (tok == Token::INTEGER_LITERAL)
1078 : : {
1079 : 35086 : numerals.emplace_back(d_lex.tokenStr());
1080 : 35086 : tok = d_lex.nextToken();
1081 : : }
1082 : 34578 : d_lex.reinsertToken(tok);
1083 : 34578 : return numerals;
1084 : 0 : }
1085 : :
1086 : 3852 : std::vector<DatatypeDecl> Smt2TermParser::parseDatatypesDef(
1087 : : bool isCo,
1088 : : const std::vector<std::string>& dnames,
1089 : : const std::vector<size_t>& arities)
1090 : : {
1091 [ + + ][ + - ]: 3852 : Assert(dnames.size() == arities.size()
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
1092 : : || (dnames.size() == 1 && arities.empty()));
1093 : 3852 : TermManager& tm = d_state.getSolver()->getTermManager();
1094 : 3852 : std::vector<DatatypeDecl> dts;
1095 : 3852 : d_state.pushScope();
1096 : : // Declare the datatypes that are currently being defined as unresolved
1097 : : // types. If we do not know the arity of the datatype yet, we wait to
1098 : : // define it until parsing the preamble of its body, which may optionally
1099 : : // involve `par`. This is limited to the case of single datatypes defined
1100 : : // via declare-datatype, and hence no datatype body is parsed without
1101 : : // having all types declared. This ensures we can parse datatypes with
1102 : : // nested recursion, e.g. datatypes D having a subfield type
1103 : : // (Array Int D).
1104 [ + + ]: 8724 : for (unsigned i = 0, dsize = dnames.size(); i < dsize; i++)
1105 : : {
1106 [ + + ]: 4872 : if (i >= arities.size())
1107 : : {
1108 : : // do not know the arity yet
1109 : 609 : continue;
1110 : : }
1111 : 4263 : d_state.mkUnresolvedType(dnames[i], arities[i]);
1112 : : }
1113 : : // while we get another datatype declaration, or close the list
1114 : 3852 : Token tok = d_lex.nextToken();
1115 [ + + ]: 8724 : while (tok == Token::LPAREN_TOK)
1116 : : {
1117 : 4872 : std::vector<Sort> params;
1118 : 4872 : size_t i = dts.size();
1119 [ + - ]: 4872 : Trace("parser-dt") << "Processing datatype #" << i << std::endl;
1120 [ - + ]: 4872 : if (i >= dnames.size())
1121 : : {
1122 : 0 : d_lex.parseError("Too many datatypes defined in this block.");
1123 : : }
1124 : 4872 : tok = d_lex.nextToken();
1125 : 4872 : bool pushedScope = false;
1126 [ + + ]: 4872 : if (tok == Token::PAR_TOK)
1127 : : {
1128 : 201 : pushedScope = true;
1129 : 201 : d_state.pushScope();
1130 : : std::vector<std::string> symList =
1131 : 201 : parseSymbolList(CHECK_UNDECLARED, SYM_SORT);
1132 [ - + ]: 201 : if (symList.empty())
1133 : : {
1134 : 0 : d_lex.parseError("Expected non-empty parameter list");
1135 : : }
1136 [ + + ]: 459 : for (const std::string& sym : symList)
1137 : : {
1138 : 258 : params.push_back(d_state.mkSort(sym));
1139 : : }
1140 [ + - ]: 402 : Trace("parser-dt") << params.size() << " parameters for " << dnames[i]
1141 : 201 : << std::endl;
1142 : 201 : dts.push_back(tm.mkDatatypeDecl(dnames[i], params, isCo));
1143 : 201 : }
1144 : : else
1145 : : {
1146 : 4671 : d_lex.reinsertToken(tok);
1147 : : // we will parse the parentheses-enclosed construct list below
1148 : 4671 : d_lex.reinsertToken(Token::LPAREN_TOK);
1149 : 4671 : dts.push_back(tm.mkDatatypeDecl(dnames[i], params, isCo));
1150 : : }
1151 [ + + ]: 4872 : if (i >= arities.size())
1152 : : {
1153 : : // if the arity is not yet fixed, declare it as an unresolved type
1154 : 609 : d_state.mkUnresolvedType(dnames[i], params.size());
1155 : : }
1156 [ - + ]: 4263 : else if (params.size() != arities[i])
1157 : : {
1158 : : // if the arity was fixed by prelude and is not equal to the number of
1159 : : // parameters
1160 : 0 : d_lex.parseError("Wrong number of parameters for datatype.");
1161 : : }
1162 : : // read constructor definition list, populate into the current datatype
1163 : 4872 : parseConstructorDefinitionList(dts.back());
1164 [ + + ]: 4872 : if (pushedScope)
1165 : : {
1166 : 201 : d_lex.eatToken(Token::RPAREN_TOK);
1167 : 201 : d_state.popScope();
1168 : : }
1169 : 4872 : tok = d_lex.nextToken();
1170 : 4872 : }
1171 [ - + ]: 3852 : if (dts.size() != dnames.size())
1172 : : {
1173 : 0 : d_lex.unexpectedTokenError(tok, "Wrong number of datatypes provided.");
1174 : : }
1175 : 3852 : d_lex.reinsertToken(tok);
1176 : 3852 : d_state.popScope();
1177 : 3852 : return dts;
1178 : 0 : }
1179 : :
1180 : 4872 : void Smt2TermParser::parseConstructorDefinitionList(DatatypeDecl& type)
1181 : : {
1182 : 4872 : d_lex.eatToken(Token::LPAREN_TOK);
1183 : 4872 : TermManager& tm = d_state.getSolver()->getTermManager();
1184 : : // parse another constructor or close the list
1185 [ + + ]: 13716 : while (d_lex.eatTokenChoice(Token::LPAREN_TOK, Token::RPAREN_TOK))
1186 : : {
1187 : 8844 : std::string name = parseSymbol(CHECK_NONE, SYM_VARIABLE);
1188 : 8844 : DatatypeConstructorDecl ctor(tm.mkDatatypeConstructorDecl(name));
1189 : : // parse another selector or close the current constructor
1190 [ + + ]: 17178 : while (d_lex.eatTokenChoice(Token::LPAREN_TOK, Token::RPAREN_TOK))
1191 : : {
1192 : 8334 : std::string id = parseSymbol(CHECK_NONE, SYM_SORT);
1193 : 8334 : Sort t = parseSort();
1194 : 8334 : ctor.addSelector(id, t);
1195 [ + - ]: 16668 : Trace("parser-idt") << "selector: " << id << " of type " << t
1196 : 8334 : << std::endl;
1197 : 8334 : d_lex.eatToken(Token::RPAREN_TOK);
1198 : 8334 : }
1199 : : // make the constructor
1200 : 8844 : type.addConstructor(ctor);
1201 [ + - ]: 8844 : Trace("parser-idt") << "constructor: " << name << std::endl;
1202 : 8844 : }
1203 : 4872 : }
1204 : :
1205 : 28 : std::string Smt2TermParser::parseStr(bool unescape)
1206 : : {
1207 : 28 : d_lex.eatToken(Token::STRING_LITERAL);
1208 : 28 : std::string s = d_lex.tokenStr();
1209 [ + - ]: 28 : if (unescape)
1210 : : {
1211 : 28 : unescapeString(s);
1212 : : }
1213 : 28 : return s;
1214 : 0 : }
1215 : :
1216 : 28121 : void Smt2TermParser::unescapeString(std::string& s)
1217 : : {
1218 : : // strip off the quotes
1219 : 28121 : s = s.erase(0, 1);
1220 : 28121 : s = s.erase(s.size() - 1, 1);
1221 [ + + ]: 120092 : for (size_t i = 0, ssize = s.size(); i < ssize; i++)
1222 : : {
1223 [ - + ][ - - ]: 91971 : if ((unsigned)s[i] > 127 && !isprint(s[i]))
[ - + ]
1224 : : {
1225 : 0 : d_lex.parseError(
1226 : : "Extended/unprintable characters are not "
1227 : : "part of SMT-LIB, and they must be encoded "
1228 : : "as escape sequences");
1229 : : }
1230 : : }
1231 : 28121 : size_t dst = 0;
1232 [ + + ]: 120041 : for (size_t src = 0; src < s.size(); ++src, ++dst)
1233 : : {
1234 : 91920 : s[dst] = s[src];
1235 [ + + ]: 91920 : if (s[src] == '"')
1236 : : {
1237 : 51 : ++src;
1238 : : }
1239 : : }
1240 : 28121 : s.erase(dst);
1241 : 28121 : }
1242 : :
1243 : 363735 : ParseOp Smt2TermParser::continueParseIndexedIdentifier(bool isOperator)
1244 : : {
1245 : 363735 : ParseOp p;
1246 : 363735 : std::string name = parseSymbol(CHECK_NONE, SYM_VARIABLE);
1247 : : // parse the list of numerals or symbols
1248 : 363735 : std::vector<std::string> symbols;
1249 : 363735 : std::vector<uint32_t> numerals;
1250 : : // we currently only have symbols that are indexed by only numerals, or
1251 : : // are indexed by a symbol, followed by combinations of symbols/numerals.
1252 : 363735 : Token tok = d_lex.nextToken();
1253 [ + + ]: 748264 : while (tok != Token::RPAREN_TOK)
1254 : : {
1255 [ + + ][ + + ]: 384531 : switch (tok)
1256 : : {
1257 : 379956 : case Token::INTEGER_LITERAL:
1258 [ + + ]: 379956 : if (symbols.empty())
1259 : : {
1260 : 379852 : numerals.push_back(tokenStrToUnsigned());
1261 : : }
1262 : : else
1263 : : {
1264 : : // If we parsed a symbol, treat the remaining indices as symbols
1265 : : // This is required for parsing fmf.card.
1266 : 104 : symbols.push_back(d_lex.tokenStr());
1267 : : }
1268 : 379955 : break;
1269 : 4567 : case Token::SYMBOL:
1270 : : case Token::HEX_LITERAL:
1271 : : // (_ char <hex_literal>) expects a hex literal
1272 : 4567 : symbols.push_back(d_lex.tokenStr());
1273 : 4567 : break;
1274 : 7 : case Token::QUOTED_SYMBOL:
1275 : 7 : symbols.push_back(tokenStrToSymbol(tok));
1276 : 7 : break;
1277 : 1 : default:
1278 : 3 : d_lex.unexpectedTokenError(
1279 : : tok, "Expected index while parsing indexed identifier");
1280 : 0 : break;
1281 : : }
1282 : 384529 : tok = d_lex.nextToken();
1283 : : }
1284 [ + + ][ - + ]: 363733 : if (numerals.empty() && symbols.empty())
[ - + ]
1285 : : {
1286 : 0 : d_lex.parseError(std::string("No indices provided for symbol " + name));
1287 : : }
1288 : : // if indexed by numerals
1289 [ + + ]: 363733 : if (!numerals.empty())
1290 : : {
1291 [ + + ]: 359160 : if (!isOperator)
1292 : : {
1293 : : // resolve the index constant
1294 : 185110 : p.d_expr = d_state.mkIndexedConstant(name, numerals);
1295 : : }
1296 : : else
1297 : : {
1298 : : // In some cases, we don't know which kind to use until we know the type
1299 : : // of the arguments, which is the case for:
1300 : : // - to_fp
1301 : : // - (_ tuple.select n) and (_ tuple.update n)
1302 : : // For consistency, we always construct the op lazily.
1303 : 174050 : p.d_name = name;
1304 : 174050 : p.d_indices = numerals;
1305 : 174050 : p.d_kind = Kind::UNDEFINED_KIND;
1306 : : }
1307 : : }
1308 : : // otherwise, indexed by symbols
1309 [ + + ]: 4573 : else if (!isOperator)
1310 : : {
1311 : : // handles:
1312 : : // - fmf.card indexed by Type symbol + numeral
1313 : : // - char indexed by HEX
1314 : 118 : p.d_expr = d_state.mkIndexedConstant(name, symbols);
1315 : : }
1316 : : else
1317 : : {
1318 : : // handles:
1319 : : // - testers and updaters indexed by constructor names
1320 : 4455 : Kind k = d_state.getIndexedOpKind(name);
1321 [ + + ][ + + ]: 4455 : if (k != Kind::APPLY_UPDATER && k != Kind::APPLY_TESTER
1322 [ - + ]: 12 : && k != Kind::NULLABLE_LIFT)
1323 : : {
1324 : 0 : d_lex.parseError(std::string("Unexpected indexed symbol " + name));
1325 : : }
1326 [ - + ]: 4455 : if (symbols.size() != 1)
1327 : : {
1328 : 0 : d_lex.parseError(std::string("Unexpected number of indices for " + name));
1329 : : }
1330 : 4455 : p.d_kind = k;
1331 : 4455 : p.d_name = symbols[0];
1332 : : }
1333 : 727460 : return p;
1334 : 363750 : }
1335 : :
1336 : 2091 : ParseOp Smt2TermParser::continueParseQualifiedIdentifier(bool isOperator)
1337 : : {
1338 : 2091 : ParseOp op;
1339 : 2091 : Token tok = d_lex.nextToken();
1340 [ - + ][ - - ]: 2091 : switch (tok)
1341 : : {
1342 : 0 : case Token::LPAREN_TOK:
1343 [ - - ]: 0 : tok = d_lex.nextToken();
1344 : : switch (tok)
1345 : : {
1346 : 0 : case Token::INDEX_TOK:
1347 : 0 : op = continueParseIndexedIdentifier(isOperator);
1348 : 0 : break;
1349 : 0 : default:
1350 : 0 : d_lex.unexpectedTokenError(tok,
1351 : : "Expected (indexed) identifier while "
1352 : : "parsing qualified identifier");
1353 : 0 : break;
1354 : : }
1355 : 0 : break;
1356 : 2091 : case Token::SYMBOL:
1357 : 2091 : case Token::QUOTED_SYMBOL: op.d_name = tokenStrToSymbol(tok); break;
1358 : 0 : case Token::UNTERMINATED_QUOTED_SYMBOL:
1359 : 0 : d_lex.parseError("Expected identifier while parsing qualified identifier",
1360 : : true);
1361 : 0 : break;
1362 : 0 : default:
1363 : 0 : d_lex.unexpectedTokenError(
1364 : : tok, "Expected identifier while parsing qualified identifier");
1365 : 0 : break;
1366 : : }
1367 : : // parse a sort
1368 : 4182 : Sort type = parseSort();
1369 : : // close parentheses
1370 : 2091 : d_lex.eatToken(Token::RPAREN_TOK);
1371 : : // apply the type ascription to the parsed op
1372 : 2091 : d_state.parseOpApplyTypeAscription(op, type);
1373 : 4182 : return op;
1374 : 0 : }
1375 : :
1376 : 364 : Term Smt2TermParser::parseMatchCasePattern(Sort headSort,
1377 : : std::vector<Term>& boundVars)
1378 : : {
1379 [ + + ]: 364 : if (d_lex.eatTokenChoice(Token::SYMBOL, Token::LPAREN_TOK))
1380 : : {
1381 : : // A bare pattern symbol is either a nullary constructor of the matched
1382 : : // datatype or a fresh binder for the default case. Existing declarations
1383 : : // must not affect this choice since match patterns may shadow outer names.
1384 : 89 : std::string name = d_lex.tokenStr();
1385 : 89 : const Datatype& dt = headSort.getDatatype();
1386 [ + + ]: 169 : for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
1387 : : {
1388 : 156 : const DatatypeConstructor& dc = dt[i];
1389 [ + + ]: 156 : if (dc.getName() != name)
1390 : : {
1391 : 80 : continue;
1392 : : }
1393 [ - + ]: 76 : if (dc.getNumSelectors() > 0)
1394 : : {
1395 : 0 : d_lex.parseError(
1396 : : "Must apply constructors of arity greater than 0 to arguments in "
1397 : : "pattern.");
1398 : : }
1399 : : Term f =
1400 [ + + ]: 76 : dt.isParametric() ? dc.getInstantiatedTerm(headSort) : dc.getTerm();
1401 : 152 : return d_state.getSolver()->getTermManager().mkTerm(
1402 : 152 : Kind::APPLY_CONSTRUCTOR, {f});
1403 [ + + ]: 232 : }
1404 : : // Otherwise, it is a fresh variable with the type of the head expression.
1405 : 13 : Term pat = d_state.bindBoundVar(name, headSort);
1406 : 13 : boundVars.push_back(pat);
1407 : 13 : return pat;
1408 : 89 : }
1409 : : // a non-nullary constructor
1410 : : // We parse a constructor name
1411 : 275 : const Datatype& dt = headSort.getDatatype();
1412 : 275 : std::string cname = parseSymbol(CHECK_DECLARED, SYM_VARIABLE);
1413 : 275 : const DatatypeConstructor& dc = dt.getConstructor(cname);
1414 : : // get the constructor, which could be instantiated based on the head type
1415 : : // if we are a parametric datatype
1416 [ + + ]: 275 : Term f = dt.isParametric() ? dc.getInstantiatedTerm(headSort) : dc.getTerm();
1417 : : // f should be a constructor
1418 : 275 : Sort type = f.getSort();
1419 [ - + ][ - + ]: 275 : Assert(type.isDatatypeConstructor());
[ - - ]
1420 [ + - ]: 275 : Trace("parser-dt") << "Pattern head : " << f << " " << type << std::endl;
1421 : 275 : std::vector<Sort> argTypes = type.getDatatypeConstructorDomainSorts();
1422 : : // now, parse symbols that are interpreted as bindings for the argument
1423 : : // types
1424 [ + + ]: 529 : while (d_lex.eatTokenChoice(Token::SYMBOL, Token::RPAREN_TOK))
1425 : : {
1426 [ - + ]: 254 : if (boundVars.size() >= argTypes.size())
1427 : : {
1428 : 0 : d_state.parseError("Too many arguments for pattern.");
1429 : : }
1430 : : // make of proper type
1431 : : Term arg =
1432 : 508 : d_state.bindBoundVar(d_lex.tokenStr(), argTypes[boundVars.size()]);
1433 : 254 : boundVars.push_back(arg);
1434 : 254 : }
1435 : 275 : std::vector<Term> cargs;
1436 : 275 : cargs.push_back(f);
1437 : 275 : cargs.insert(cargs.end(), boundVars.begin(), boundVars.end());
1438 : : // make the pattern term
1439 : 275 : return d_state.getSolver()->getTermManager().mkTerm(Kind::APPLY_CONSTRUCTOR,
1440 : 275 : cargs);
1441 : 275 : }
1442 : :
1443 : : } // namespace parser
1444 : : } // namespace cvc5
|
