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 : 24377 : Smt2TermParser::Smt2TermParser(Smt2Lexer& lex, Smt2State& state)
92 : 24377 : : d_lex(lex), d_state(state)
93 : : {
94 : 24377 : }
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 [ - + ][ - + ]: 19188306 : Assert(tstack.size() == xstack.size());
[ - - ]
115 : : // At this point, we are ready to parse the next term
116 : 19188306 : tok = d_lex.nextToken();
117 : 19188305 : Term currTerm;
118 [ + + ][ + - ]: 19188305 : switch (tok)
[ + + ][ + + ]
[ + + ][ + + ]
119 : : {
120 : : // ------------------- open paren
121 : 6586629 : case Token::LPAREN_TOK:
122 : : {
123 [ + + ][ + + ]: 6586629 : 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 : 185184 : case Token::INDEX_TOK:
138 : : {
139 : : // a standalone indexed symbol
140 : 185184 : ParseOp op = continueParseIndexedIdentifier(false);
141 : 185180 : ret = op.d_expr;
142 [ - + ]: 185180 : if (ret.isNull())
143 : : {
144 : 0 : d_lex.parseError("Unexpected indexed symbol");
145 : : }
146 : 185180 : }
147 : 185180 : break;
148 : 178713 : case Token::LPAREN_TOK:
149 : : {
150 [ + + ][ - ]: 178713 : 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 : 178466 : case Token::INDEX_TOK:
162 : : {
163 : : // an indexed identifier operator
164 : 178466 : ParseOp op = continueParseIndexedIdentifier(true);
165 : 178465 : xstack.emplace_back(ParseCtx::NEXT_ARG);
166 : 178465 : tstack.emplace_back(op, std::vector<Term>());
167 : 178465 : }
168 : 178465 : break;
169 : 0 : default:
170 : 0 : d_lex.unexpectedTokenError(
171 : : tok, "Expected SMT-LIBv2 qualified indentifier");
172 : 0 : break;
173 : : }
174 : : }
175 : 178712 : break;
176 : 222718 : case Token::LET_TOK:
177 : : {
178 : 222718 : xstack.emplace_back(ParseCtx::LET_NEXT_BIND);
179 : 222718 : tstack.emplace_back(ParseOp(), std::vector<Term>());
180 : 222718 : needsUpdateCtx = true;
181 : 222718 : letBinders.emplace_back();
182 : : }
183 : 222718 : break;
184 : 163 : case Token::MATCH_TOK:
185 : : {
186 : 163 : xstack.emplace_back(ParseCtx::MATCH_HEAD);
187 : 163 : tstack.emplace_back();
188 : : }
189 : 163 : break;
190 : 20739 : case Token::ATTRIBUTE_TOK:
191 : : {
192 : 20739 : xstack.emplace_back(ParseCtx::TERM_ANNOTATE_BODY);
193 : 20739 : tstack.emplace_back();
194 : : }
195 : 20739 : break;
196 : 5977268 : case Token::SYMBOL:
197 : : case Token::QUOTED_SYMBOL:
198 : : {
199 : : // function identifier
200 : 5977268 : ParseOp op;
201 : 5977268 : op.d_name = tokenStrToSymbol(tok);
202 : 5977268 : std::vector<Term> args;
203 [ + + ]: 5977268 : if (d_state.isClosure(op.d_name))
204 : : {
205 : : // if it is a closure, immediately read the bound variable list
206 : 86884 : d_state.pushScope();
207 : : std::vector<std::pair<std::string, Sort>> sortedVarNames =
208 : 86884 : parseSortedVarList();
209 [ - + ]: 86883 : if (sortedVarNames.empty())
210 : : {
211 : 0 : d_lex.parseError("Expected non-empty sorted variable list");
212 : : }
213 : 86883 : 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 : 86883 : std::vector<Term> vs = d_state.bindBoundVarsCtx(
222 : 86883 : sortedVarNames, letBinders, freshBinders);
223 : 86883 : Term vl = tm.mkTerm(Kind::VARIABLE_LIST, vs);
224 : 86883 : args.push_back(vl);
225 : 86883 : xstack.emplace_back(ParseCtx::CLOSURE_NEXT_ARG);
226 : 86883 : }
227 : : else
228 : : {
229 : 5890384 : xstack.emplace_back(ParseCtx::NEXT_ARG);
230 : : }
231 : 5977267 : tstack.emplace_back(op, args);
232 : 5977269 : }
233 : 5977267 : 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 : 6586622 : break;
243 : : // ------------------- close paren
244 : 6165973 : case Token::RPAREN_TOK:
245 : : {
246 : : // should only be here if we are expecting arguments
247 [ + + ][ + + ]: 6252853 : if (tstack.empty() || (xstack.back() != ParseCtx::NEXT_ARG
[ + + ]
248 [ + + ]: 86880 : && xstack.back() != ParseCtx::CLOSURE_NEXT_ARG))
249 : : {
250 : 6 : d_lex.unexpectedTokenError(
251 : : tok, "Mismatched parentheses in SMT-LIBv2 term");
252 : : }
253 : : // Construct the application term specified by tstack.back()
254 : 6165971 : ParseOp& op = tstack.back().first;
255 : 6165971 : ret = d_state.applyParseOp(op, tstack.back().second);
256 : : // process the scope change if a closure
257 [ + + ]: 6165927 : if (xstack.back() == ParseCtx::CLOSURE_NEXT_ARG)
258 : : {
259 : : // if we were a closure, pop a scope
260 : 86879 : d_state.popScope();
261 : : }
262 : : // pop the stack
263 : 6165927 : tstack.pop_back();
264 : 6165927 : xstack.pop_back();
265 : : }
266 : 6165927 : break;
267 : : // ------------------- base cases
268 : 5482068 : case Token::SYMBOL:
269 : : case Token::QUOTED_SYMBOL:
270 : : {
271 : 5482068 : std::string name = tokenStrToSymbol(tok);
272 : 5482068 : ret = d_state.getVariable(name);
273 : 5482068 : }
274 : 5482057 : break;
275 : 0 : case Token::UNTERMINATED_QUOTED_SYMBOL:
276 : 0 : d_lex.parseError("Expected SMT-LIBv2 term", true);
277 : 0 : break;
278 : 840468 : case Token::INTEGER_LITERAL:
279 : : {
280 : 840470 : ret = d_state.mkRealOrIntFromNumeral(d_lex.tokenStr());
281 : : }
282 : 840467 : break;
283 : 65757 : case Token::DECIMAL_LITERAL:
284 : : {
285 : 65757 : ret = tm.mkReal(d_lex.tokenStr());
286 : : }
287 : 65757 : break;
288 : 12 : case Token::RATIONAL_LITERAL:
289 : : {
290 : 14 : ret = tm.mkReal(d_lex.tokenStr());
291 : : }
292 : 11 : break;
293 : 3335 : case Token::HEX_LITERAL:
294 : : {
295 : 3335 : std::string hexStr = d_lex.tokenStr();
296 : 3335 : hexStr = hexStr.substr(2);
297 : 3335 : ret = tm.mkBitVector(hexStr.size() * 4, hexStr, 16);
298 : 3335 : }
299 : 3335 : break;
300 : 13934 : case Token::BINARY_LITERAL:
301 : : {
302 : 13934 : std::string binStr = d_lex.tokenStr();
303 : 13934 : binStr = binStr.substr(2);
304 : 13934 : ret = tm.mkBitVector(binStr.size(), binStr, 2);
305 : 13934 : }
306 : 13934 : break;
307 : 2035 : case Token::FIELD_LITERAL:
308 : : {
309 : 2035 : std::string ffStr = d_lex.tokenStr();
310 [ - + ][ - + ]: 2035 : Assert(ffStr.find("#f") == 0);
[ - - ]
311 : 2035 : size_t mPos = ffStr.find("m");
312 [ - + ][ - + ]: 2035 : Assert(mPos > 2);
[ - - ]
313 : 2035 : std::string ffValStr = ffStr.substr(2, mPos - 2);
314 : 2035 : std::string ffModStr = ffStr.substr(mPos + 1);
315 : 2035 : Sort ffSort = tm.mkFiniteFieldSort(ffModStr);
316 : 2035 : ret = tm.mkFiniteFieldElem(ffValStr, ffSort);
317 : 2035 : }
318 : 2035 : break;
319 : 28093 : case Token::STRING_LITERAL:
320 : : {
321 : 28093 : std::string s = d_lex.tokenStr();
322 : 28093 : unescapeString(s);
323 : 28093 : ret = tm.mkString(s, true);
324 : 28093 : }
325 : 28093 : break;
326 : 1 : default:
327 : 3 : d_lex.unexpectedTokenError(tok, "Expected SMT-LIBv2 term");
328 : 0 : break;
329 : : }
330 : :
331 : : // Based on the current context, setup next parsed term.
332 : : // We do this only if a context is allocated (!tstack.empty()) and we
333 : : // either just finished parsing a term (!ret.isNull()), or otherwise have
334 : : // indicated that we need to update the context (needsUpdateCtx).
335 [ + + ][ + + ]: 32233483 : while (!tstack.empty() && (!ret.isNull() || needsUpdateCtx))
[ + + ][ + + ]
336 : : {
337 : 13045246 : needsUpdateCtx = false;
338 [ + + ][ + + ]: 13045246 : switch (xstack.back())
[ + + ][ + - ]
339 : : {
340 : : // ------------------------- argument lists
341 : 12278804 : case ParseCtx::NEXT_ARG:
342 : : case ParseCtx::CLOSURE_NEXT_ARG:
343 : : {
344 [ - + ][ - + ]: 12278804 : Assert(!ret.isNull());
[ - - ]
345 : : // add it to the list of arguments and clear
346 : 12278804 : tstack.back().second.push_back(ret);
347 : 12278804 : ret = Term();
348 : : }
349 : 12278804 : break;
350 : : // ------------------------- let terms
351 : 479858 : case ParseCtx::LET_NEXT_BIND:
352 : : {
353 : : // if we parsed a term, process it as a binding
354 [ + + ]: 479858 : if (!ret.isNull())
355 : : {
356 [ - + ][ - + ]: 257140 : Assert(!letBinders.empty());
[ - - ]
357 : 257140 : std::vector<std::pair<std::string, Term>>& bs = letBinders.back();
358 : : // add binding from the symbol to ret
359 : 257140 : bs.emplace_back(tstack.back().first.d_name, ret);
360 : 257140 : ret = Term();
361 : : // close the current binding
362 : 257140 : d_lex.eatToken(Token::RPAREN_TOK);
363 : : }
364 : : else
365 : : {
366 : : // eat the opening left parenthesis of the binding list
367 : 222718 : d_lex.eatToken(Token::LPAREN_TOK);
368 : : }
369 : : // see if there is another binding
370 [ + + ]: 479858 : if (d_lex.eatTokenChoice(Token::LPAREN_TOK, Token::RPAREN_TOK))
371 : : {
372 : : // (, another binding: setup parsing the next term
373 : : // get the symbol and store in the ParseOp
374 : 257141 : tstack.back().first.d_name = parseSymbol(CHECK_NONE, SYM_VARIABLE);
375 : : }
376 : : else
377 : : {
378 : : // ), we are now looking for the body of the let
379 : 222717 : xstack[xstack.size() - 1] = ParseCtx::LET_BODY;
380 : : // push scope
381 : 222717 : d_state.pushScope();
382 : : // implement the bindings
383 [ - + ][ - + ]: 222717 : Assert(!letBinders.empty());
[ - - ]
384 : : const std::vector<std::pair<std::string, Term>>& bs =
385 : 222717 : letBinders.back();
386 [ + + ]: 479857 : for (const std::pair<std::string, Term>& b : bs)
387 : : {
388 : 257140 : d_state.defineVar(b.first, b.second);
389 : : }
390 : : }
391 : : }
392 : 479858 : break;
393 : 222717 : case ParseCtx::LET_BODY:
394 : : {
395 : : // the let body is the returned term
396 : 222717 : d_lex.eatToken(Token::RPAREN_TOK);
397 : 222717 : xstack.pop_back();
398 : 222717 : tstack.pop_back();
399 : : // pop scope
400 : 222717 : d_state.popScope();
401 : : // Done with the binders now. We clear this only at this point since
402 : : // the let binders may to pertinent to avoid illegal substitutions
403 : : // from lets.
404 : 222717 : letBinders.pop_back();
405 : : }
406 : 222717 : break;
407 : : // ------------------------- match terms
408 : 163 : case ParseCtx::MATCH_HEAD:
409 : : {
410 [ - + ][ - + ]: 163 : Assert(!ret.isNull());
[ - - ]
411 : : // add the head
412 : 163 : tstack.back().second.push_back(ret);
413 : 163 : Sort retSort = ret.getSort();
414 : : // eagerly check if datatype
415 [ - + ]: 163 : if (!retSort.isDatatype())
416 : : {
417 : 0 : d_lex.parseError("Cannot match on non-datatype term.");
418 : : }
419 : : // we use a placeholder to store the type (retSort), which is
420 : : // used during MATCH_NEXT_CASE
421 : 163 : tstack.back().first.d_kind = Kind::INTERNAL_KIND;
422 : 163 : tstack.back().first.d_expr = tm.mkConst(retSort);
423 : 163 : ret = Term();
424 : 163 : xstack[xstack.size() - 1] = ParseCtx::MATCH_NEXT_CASE;
425 : 163 : needsUpdateCtx = true;
426 : 163 : }
427 : 163 : break;
428 : 525 : case ParseCtx::MATCH_NEXT_CASE:
429 : : {
430 [ + + ]: 525 : if (!ret.isNull())
431 : : {
432 : : // add it to the list of arguments and clear
433 : 362 : tstack.back().second.push_back(ret);
434 : 362 : ret = Term();
435 : : // pop the scope
436 : 362 : d_state.popScope();
437 : : }
438 : : else
439 : : {
440 : : // eat the opening left parenthesis of the case list
441 : 163 : d_lex.eatToken(Token::LPAREN_TOK);
442 : : }
443 : : // see if there is another case
444 [ + + ]: 525 : if (d_lex.eatTokenChoice(Token::LPAREN_TOK, Token::RPAREN_TOK))
445 : : {
446 : : // push the scope
447 : 362 : d_state.pushScope();
448 : : // parse the pattern, which also does the binding
449 [ - + ][ - + ]: 362 : Assert(!tstack.back().first.d_expr.isNull());
[ - - ]
450 : 362 : std::vector<Term> boundVars;
451 : : Term pattern = parseMatchCasePattern(
452 : 362 : tstack.back().first.d_expr.getSort(), boundVars);
453 : : // If we bound variables when parsing the pattern, we will construct
454 : : // a match bind case
455 : 362 : ParseOp op;
456 : 362 : std::vector<Term> args;
457 [ + + ]: 362 : if (!boundVars.empty())
458 : : {
459 : 188 : op.d_kind = Kind::MATCH_BIND_CASE;
460 : 188 : Term vl = tm.mkTerm(Kind::VARIABLE_LIST, boundVars);
461 : 188 : args.push_back(tm.mkTerm(Kind::VARIABLE_LIST, boundVars));
462 : 188 : }
463 : : else
464 : : {
465 : 174 : op.d_kind = Kind::MATCH_CASE;
466 : : }
467 : 362 : args.push_back(pattern);
468 : : // we now look for the body of the case + closing right parenthesis
469 : 362 : xstack.emplace_back(ParseCtx::NEXT_ARG);
470 : 362 : tstack.emplace_back(op, args);
471 : 362 : }
472 : : else
473 : : {
474 : : // Finished with match, now just wait for the closing right
475 : : // parenthesis. Set the kind to construct as MATCH and clear the
476 : : // head sort.
477 : 163 : ParseOp& op = tstack.back().first;
478 : 163 : op.d_kind = Kind::MATCH;
479 : 163 : op.d_expr = Term();
480 : 163 : xstack[xstack.size() - 1] = ParseCtx::NEXT_ARG;
481 : : }
482 : : }
483 : 525 : break;
484 : : // ------------------------- annotated terms
485 : 20739 : case ParseCtx::TERM_ANNOTATE_BODY:
486 : : {
487 : : // save ret as the expression and clear
488 : 20739 : tstack.back().first.d_expr = ret;
489 : 20739 : ret = Term();
490 : : // now parse attribute list
491 : 20739 : xstack[xstack.size() - 1] = ParseCtx::TERM_ANNOTATE_NEXT_ATTR;
492 : 20739 : needsUpdateCtx = true;
493 : : // ensure there is at least one attribute
494 : 20739 : tok = d_lex.peekToken();
495 [ - + ]: 20739 : if (tok == Token::RPAREN_TOK)
496 : : {
497 : 0 : d_lex.parseError(
498 : : "Expecting at least one attribute for term annotation.");
499 : : }
500 : : }
501 : 20739 : break;
502 : 42440 : case ParseCtx::TERM_ANNOTATE_NEXT_ATTR:
503 : : {
504 [ + + ]: 42440 : if (!ret.isNull())
505 : : {
506 : : // if we got here, we either:
507 : : // (1) parsed a single term (the current ParseOp::d_kind was set)
508 : : // (2) a list of terms in a nested context.
509 [ + + ]: 9542 : if (tstack.back().first.d_kind != Kind::NULL_TERM)
510 : : {
511 : : // if (1), apply d_kind to the argument and reset d_kind
512 : 24 : ret = tm.mkTerm(tstack.back().first.d_kind, {ret});
513 : 12 : tstack.back().first.d_kind = Kind::NULL_TERM;
514 : : }
515 : 9542 : tstack.back().second.push_back(ret);
516 : 9542 : ret = Term();
517 : : }
518 : : // see if there is another keyword
519 [ + + ]: 42440 : if (d_lex.eatTokenChoice(Token::KEYWORD, Token::RPAREN_TOK))
520 : : {
521 : 21702 : std::string key = d_lex.tokenStr();
522 : : // Based on the keyword, determine the context.
523 : : // Set needsUpdateCtx to true if we are finished parsing the
524 : : // current attribute.
525 : 21702 : Kind attrKind = Kind::NULL_TERM;
526 : 21702 : Term attrValue;
527 [ + + ]: 21702 : if (key == ":inst-add-to-pool")
528 : : {
529 : 28 : attrKind = Kind::INST_ADD_TO_POOL;
530 : : }
531 [ - + ]: 21674 : else if (key == ":quant-inst-max-level")
532 : : {
533 : : // a numeral
534 : 0 : d_lex.eatToken(Token::INTEGER_LITERAL);
535 : 0 : attrValue = tm.mkInteger(d_lex.tokenStr());
536 : : }
537 [ + + ]: 21674 : else if (key == ":named")
538 : : {
539 [ - + ][ - + ]: 11261 : Assert(!tstack.back().first.d_expr.isNull());
[ - - ]
540 : : // expression is the body of the term annotation
541 : 11261 : std::string sym = parseSymbol(CHECK_UNDECLARED, SYM_VARIABLE);
542 : 11262 : d_state.notifyNamedExpression(tstack.back().first.d_expr, sym);
543 : 11260 : needsUpdateCtx = true;
544 : 11261 : }
545 [ + + ]: 10413 : else if (key == ":no-pattern")
546 : : {
547 : : // a single term, set the current kind
548 : 12 : tstack.back().first.d_kind = Kind::INST_NO_PATTERN;
549 : : }
550 [ + + ]: 10401 : else if (key == ":pattern")
551 : : {
552 : 9449 : attrKind = Kind::INST_PATTERN;
553 : : }
554 [ + + ]: 952 : else if (key == ":pool")
555 : : {
556 : 44 : attrKind = Kind::INST_POOL;
557 : : }
558 [ + + ]: 908 : else if (key == ":qid")
559 : : {
560 : 539 : std::string sym = parseSymbol(CHECK_NONE, SYM_VARIABLE);
561 : : // must create a variable whose name is the name of the quantified
562 : : // formula, not a string.
563 : 539 : attrValue = tm.mkConst(tm.getBooleanSort(), sym);
564 : 539 : }
565 [ + + ]: 369 : else if (key == ":skolem-add-to-pool")
566 : : {
567 : 16 : attrKind = Kind::SKOLEM_ADD_TO_POOL;
568 : : }
569 : : else
570 : : {
571 : : // warn that the attribute is not supported
572 : 353 : d_state.attributeNotSupported(d_lex.tokenStr());
573 [ - + ]: 353 : tok = d_lex.nextToken();
574 : : // We don't know whether to expect an attribute value. Thus,
575 : : // we will either see keyword (the next attribute), rparen
576 : : // (the term annotation is finished), or else parse as generic
577 : : // symbolic expression for the current attribute.
578 : : switch (tok)
579 : : {
580 : 0 : case Token::KEYWORD:
581 : : case Token::RPAREN_TOK:
582 : : // finished with this attribute, go to the next one if it
583 : : // exists.
584 : 0 : d_lex.reinsertToken(tok);
585 : 0 : break;
586 : 353 : default:
587 : : // ignore the symbolic expression that follows
588 : 353 : d_lex.reinsertToken(tok);
589 : 353 : parseSymbolicExpr();
590 : : // will parse another attribute
591 : 353 : break;
592 : : }
593 : 353 : needsUpdateCtx = true;
594 : : }
595 [ + + ]: 21701 : if (attrKind != Kind::NULL_TERM)
596 : : {
597 : : // e.g. `:pattern (t1 ... tn)`, where we have parsed `:pattern (`
598 : 9537 : d_lex.eatToken(Token::LPAREN_TOK);
599 : : // Corner case: the list of terms is empty. This is a legal
600 : : // pattern in SMT-LIB, and hence we ignore it, for other
601 : : // attributes we throw an error.
602 [ + + ]: 9537 : if (d_lex.peekToken() == Token::RPAREN_TOK)
603 : : {
604 [ + - ]: 7 : if (attrKind == Kind::INST_PATTERN)
605 : : {
606 : : // silently ignores
607 : 7 : d_lex.eatToken(Token::RPAREN_TOK);
608 : : }
609 : : else
610 : : {
611 : 0 : d_lex.parseError(
612 : : "Expecting at least one term in annotation.");
613 : : }
614 : 7 : needsUpdateCtx = true;
615 : : }
616 : : else
617 : : {
618 : : // Will parse list as arguments to the kind + closing
619 : : // parenthesis.
620 : 9530 : ParseOp op;
621 : 9530 : op.d_kind = attrKind;
622 : 9530 : tstack.emplace_back(op, std::vector<Term>());
623 : 9530 : xstack.emplace_back(ParseCtx::NEXT_ARG);
624 : 9530 : }
625 : : }
626 [ + + ]: 12164 : else if (!attrValue.isNull())
627 : : {
628 : : // if we constructed a term as the attribute value, make into
629 : : // an INST_ATTRIBUTE and add it to args
630 : 539 : std::string keyName = key.substr(1);
631 : 539 : Term keyword = tm.mkString(keyName);
632 : : Term iattr =
633 : 2156 : tm.mkTerm(Kind::INST_ATTRIBUTE, {keyword, attrValue});
634 : 539 : tstack.back().second.push_back(iattr);
635 : 539 : needsUpdateCtx = true;
636 : 539 : }
637 : 21703 : }
638 : : // if we instead saw a RPAREN_TOK, we are finished
639 : : else
640 : : {
641 [ - + ][ - + ]: 20738 : Assert(!tstack.back().first.d_expr.isNull());
[ - - ]
642 : : // finished parsing attributes, we will return the original term
643 : 20738 : ret = tstack.back().first.d_expr;
644 : 20738 : Term ipl;
645 : : // if args non-empty, construct an instantiation pattern list
646 [ + + ]: 20738 : if (!tstack.back().second.empty())
647 : : {
648 : 9417 : ipl = tm.mkTerm(Kind::INST_PATTERN_LIST, tstack.back().second);
649 : : }
650 : 20738 : xstack.pop_back();
651 : 20738 : tstack.pop_back();
652 : : // If we constructed an instantiation pattern list, it should have
653 : : // been a quantified formula body. Check the next scope up.
654 [ + + ]: 20738 : if (!ipl.isNull())
655 : : {
656 [ + - ]: 18834 : if (tstack.empty() || xstack.back() != ParseCtx::CLOSURE_NEXT_ARG
657 [ + - ][ - + ]: 18834 : || tstack.back().second.size() != 1)
[ - + ]
658 : : {
659 : 0 : d_lex.parseError(
660 : : "Patterns and quantifier attributes should be applied to "
661 : : "quantified formula bodies only.");
662 : : }
663 : : // Push ret and the instantiation pattern list and clear. We
664 : : // wait for the closing parenthesis, which should follow.
665 : 9417 : tstack.back().second.push_back(ret);
666 : 9417 : tstack.back().second.push_back(ipl);
667 : 9417 : ret = Term();
668 : : }
669 : 20738 : }
670 : : }
671 : 42439 : break;
672 : 0 : default: break;
673 : : }
674 : : }
675 : : // otherwise ret will be returned
676 [ + + ]: 19188305 : } while (!tstack.empty());
677 : 466420 : return ret;
678 : 233486 : }
679 : :
680 : 4396 : std::vector<Term> Smt2TermParser::parseTermList()
681 : : {
682 : 4396 : d_lex.eatToken(Token::LPAREN_TOK);
683 : 4396 : std::vector<Term> terms;
684 : 4396 : Token tok = d_lex.nextToken();
685 [ + + ]: 8975 : while (tok != Token::RPAREN_TOK)
686 : : {
687 : 4584 : d_lex.reinsertToken(tok);
688 : 4584 : Term t = parseTerm();
689 : 4579 : terms.push_back(t);
690 : 4579 : tok = d_lex.nextToken();
691 : 4579 : }
692 : 4391 : return terms;
693 : 5 : }
694 : :
695 : 27129 : Term Smt2TermParser::parseSymbolicExpr()
696 : : {
697 : 27129 : Term ret;
698 : : Token tok;
699 : 27129 : std::vector<std::vector<Term>> sstack;
700 : 27129 : Solver* slv = d_state.getSolver();
701 : 27129 : TermManager& tm = slv->getTermManager();
702 : 27129 : Sort dummyType = tm.getBooleanSort();
703 : : do
704 : : {
705 : 27196 : tok = d_lex.nextToken();
706 [ + + ][ + + ]: 27196 : switch (tok)
707 : : {
708 : : // ------------------- open paren
709 : 12 : case Token::LPAREN_TOK:
710 : : {
711 : 12 : sstack.emplace_back(std::vector<Term>());
712 : : }
713 : 12 : break;
714 : : // ------------------- close paren
715 : 11 : case Token::RPAREN_TOK:
716 : : {
717 [ - + ]: 11 : if (sstack.empty())
718 : : {
719 : 0 : d_lex.unexpectedTokenError(
720 : : tok, "Mismatched parentheses in SMT-LIBv2 s-expression");
721 : : }
722 : 11 : ret = tm.mkTerm(Kind::SEXPR, sstack.back());
723 : : // pop the stack
724 : 11 : sstack.pop_back();
725 : : }
726 : 11 : break;
727 : 1 : case Token::EOF_TOK:
728 : : {
729 : 3 : d_lex.parseError("Expected SMT-LIBv2 s-expression");
730 : : }
731 : 0 : break;
732 : : // ------------------- base case
733 : 27172 : default:
734 : : {
735 : : // note that there are no tokens that are forbidden here
736 : 27172 : std::string str = d_lex.tokenStr();
737 : 27172 : ret = tm.mkVar(dummyType, str);
738 : 27172 : }
739 : 27172 : break;
740 : : }
741 [ + + ]: 27195 : if (!ret.isNull())
742 : : {
743 : : // add it to the list and reset ret
744 [ + + ]: 27183 : if (!sstack.empty())
745 : : {
746 : 55 : sstack.back().push_back(ret);
747 : 55 : ret = Term();
748 : : }
749 : : // otherwise it will be returned
750 : : }
751 [ + + ]: 27195 : } while (!sstack.empty());
752 [ - + ][ - + ]: 27128 : Assert(!ret.isNull());
[ - - ]
753 : 54256 : return ret;
754 : 27131 : }
755 : :
756 : 607396 : Sort Smt2TermParser::parseSort()
757 : : {
758 : 607396 : Sort ret;
759 : : Token tok;
760 : 607396 : std::vector<std::pair<std::string, std::vector<Sort>>> sstack;
761 : : do
762 : : {
763 : 728721 : tok = d_lex.nextToken();
764 [ + + ][ + - ]: 728721 : switch (tok)
765 : : {
766 : : // ------------------- open paren
767 : 75930 : case Token::LPAREN_TOK:
768 : : {
769 [ + + ][ - ]: 75930 : tok = d_lex.nextToken();
770 : : switch (tok)
771 : : {
772 : 34526 : case Token::INDEX_TOK:
773 : : {
774 : : // a standalone indexed symbol
775 : 34526 : std::string name = parseSymbol(CHECK_NONE, SYM_SORT);
776 : 34526 : std::vector<std::string> numerals = parseNumeralList();
777 : 34526 : d_lex.eatToken(Token::RPAREN_TOK);
778 : 34526 : ret = d_state.getIndexedSort(name, numerals);
779 : 34527 : }
780 : 34525 : break;
781 : 41404 : case Token::SYMBOL:
782 : : case Token::QUOTED_SYMBOL:
783 : : {
784 : : // sort constructor identifier
785 : 41404 : std::string name = tokenStrToSymbol(tok);
786 : : // open a new stack frame
787 : 41404 : std::vector<Sort> emptyArgs;
788 : 41404 : sstack.emplace_back(name, emptyArgs);
789 : 41404 : }
790 : 41404 : break;
791 : 0 : default:
792 : : // NOTE: it is possible to have sorts e.g.
793 : : // ((_ FixedSizeList 4) Real) where tok would be LPAREN_TOK here.
794 : : // However, we have no such examples in cvc5 currently.
795 : 0 : d_lex.unexpectedTokenError(tok,
796 : : "Expected SMT-LIBv2 sort constructor");
797 : 0 : break;
798 : : }
799 : : }
800 : 75929 : break;
801 : : // ------------------- close paren
802 : 41404 : case Token::RPAREN_TOK:
803 : : {
804 [ - + ]: 41404 : if (sstack.empty())
805 : : {
806 : 0 : d_lex.unexpectedTokenError(
807 : : tok, "Mismatched parentheses in SMT-LIBv2 sort");
808 : : }
809 : : // Construct the (parametric) sort specified by sstack.back()
810 : 82805 : ret = d_state.getParametricSort(sstack.back().first,
811 : 82805 : sstack.back().second);
812 : : // pop the stack
813 : 41401 : sstack.pop_back();
814 : : }
815 : 41401 : break;
816 : : // ------------------- a simple (defined or builtin) sort
817 : 611387 : case Token::SYMBOL:
818 : : case Token::QUOTED_SYMBOL:
819 : : {
820 : 611387 : std::string name = tokenStrToSymbol(tok);
821 : 611387 : ret = d_state.getSort(name);
822 : 611387 : }
823 : 611386 : break;
824 : 0 : default:
825 : 0 : d_lex.unexpectedTokenError(tok, "Expected SMT-LIBv2 sort");
826 : 0 : break;
827 : : }
828 [ + + ]: 728716 : if (!ret.isNull())
829 : : {
830 : : // add it to the list and reset ret
831 [ + + ]: 687312 : if (!sstack.empty())
832 : : {
833 : 79921 : sstack.back().second.push_back(ret);
834 : 79921 : ret = Sort();
835 : : }
836 : : // otherwise it will be returned
837 : : }
838 [ + + ]: 728716 : } while (!sstack.empty());
839 [ - + ][ - + ]: 607391 : Assert(!ret.isNull());
[ - - ]
840 : 1214782 : return ret;
841 : 607401 : }
842 : :
843 : 320615 : std::vector<Sort> Smt2TermParser::parseSortList()
844 : : {
845 : 320615 : d_lex.eatToken(Token::LPAREN_TOK);
846 : 320614 : std::vector<Sort> sorts;
847 : 320614 : Token tok = d_lex.nextToken();
848 [ + + ]: 395298 : while (tok != Token::RPAREN_TOK)
849 : : {
850 : 74685 : d_lex.reinsertToken(tok);
851 : 74685 : Sort s = parseSort();
852 : 74684 : sorts.push_back(s);
853 : 74684 : tok = d_lex.nextToken();
854 : 74684 : }
855 : 320613 : return sorts;
856 : 1 : }
857 : :
858 : 97358 : std::vector<std::pair<std::string, Sort>> Smt2TermParser::parseSortedVarList()
859 : : {
860 : 97358 : std::vector<std::pair<std::string, Sort>> varList;
861 : 97358 : d_lex.eatToken(Token::LPAREN_TOK);
862 : 97358 : std::string name;
863 : 97358 : Sort t;
864 : : // while the next token is LPAREN, exit if RPAREN
865 [ + + ]: 272988 : while (d_lex.eatTokenChoice(Token::LPAREN_TOK, Token::RPAREN_TOK))
866 : : {
867 : 175631 : name = parseSymbol(CHECK_NONE, SYM_VARIABLE);
868 : 175631 : t = parseSort();
869 : 175630 : varList.emplace_back(name, t);
870 : 175630 : d_lex.eatToken(Token::RPAREN_TOK);
871 : : }
872 : 194712 : return varList;
873 : 97362 : }
874 : :
875 : 1247422 : std::string Smt2TermParser::parseSymbol(DeclarationCheck check, SymbolType type)
876 : : {
877 : 1247422 : Token tok = d_lex.nextToken();
878 : 1247422 : std::string id = tokenStrToSymbol(tok);
879 : : // run the check
880 [ + - ]: 1247422 : if (!d_state.isAbstractValue(id))
881 : : {
882 : : // if an abstract value, SolverEngine handles declaration
883 : 1247424 : d_state.checkDeclaration(id, check, type);
884 : : }
885 : 1247421 : return id;
886 : 1 : }
887 : :
888 : 953 : std::vector<std::string> Smt2TermParser::parseSymbolList(DeclarationCheck check,
889 : : SymbolType type)
890 : : {
891 : 953 : d_lex.eatToken(Token::LPAREN_TOK);
892 : 953 : std::vector<std::string> symbols;
893 : 953 : Token tok = d_lex.nextToken();
894 [ + + ]: 1214 : while (tok != Token::RPAREN_TOK)
895 : : {
896 : 261 : d_lex.reinsertToken(tok);
897 : 261 : std::string sym = parseSymbol(check, type);
898 : 261 : symbols.push_back(sym);
899 : 261 : tok = d_lex.nextToken();
900 : 261 : }
901 : 953 : return symbols;
902 : 0 : }
903 : :
904 : 27137 : std::string Smt2TermParser::parseKeyword()
905 : : {
906 : 27137 : d_lex.eatToken(Token::KEYWORD);
907 : 27137 : std::string s = d_lex.tokenStr();
908 : : // strip off the initial colon
909 : 54274 : return s.erase(0, 1);
910 : 27137 : }
911 : :
912 : 808 : Grammar* Smt2TermParser::parseGrammar(const std::vector<Term>& sygusVars)
913 : : {
914 : : // We read a sorted variable list ((<symbol> <sort>)^n+1)
915 : : std::vector<std::pair<std::string, Sort>> sortedVarNames =
916 : 808 : parseSortedVarList();
917 : : // non-terminal symbols in the pre-declaration are locally scoped
918 : 808 : d_state.pushScope();
919 : 808 : std::vector<Term> ntSyms;
920 [ + + ]: 2602 : for (std::pair<std::string, Sort>& i : sortedVarNames)
921 : : {
922 : 1794 : d_state.checkDeclaration(i.first, CHECK_UNDECLARED, SYM_SORT);
923 : : // make the non-terminal symbol, which will be parsed as an ordinary
924 : : // free variable.
925 : 1794 : Term nts = d_state.bindBoundVar(i.first, i.second);
926 : 1794 : ntSyms.push_back(nts);
927 : 1794 : }
928 : 808 : Grammar* ret = d_state.mkGrammar(sygusVars, ntSyms);
929 : : // Parse (<GroupedRuleList>^n+1)
930 : 808 : d_lex.eatToken(Token::LPAREN_TOK);
931 [ + + ]: 2596 : for (size_t i = 0, nnts = ntSyms.size(); i < nnts; i++)
932 : : {
933 : : // start the non-terminal definition
934 : 1790 : d_lex.eatToken(Token::LPAREN_TOK);
935 : 1790 : std::string name = parseSymbol(CHECK_DECLARED, SYM_VARIABLE);
936 : 1790 : Sort t = parseSort();
937 : : // check that it matches sortedVarNames
938 [ - + ]: 1790 : if (sortedVarNames[i].first != name)
939 : : {
940 : 0 : std::stringstream sse;
941 : : sse << "Grouped rule listing " << name
942 : : << " does not match the name (in order) from the predeclaration ("
943 : 0 : << sortedVarNames[i].first << ")." << std::endl;
944 : 0 : d_lex.parseError(sse.str().c_str());
945 : 0 : }
946 [ - + ]: 1790 : if (sortedVarNames[i].second != t)
947 : : {
948 : 0 : std::stringstream sse;
949 : : sse << "Type for grouped rule listing " << name
950 : 0 : << " does not match the type (in order) from the predeclaration ("
951 : 0 : << sortedVarNames[i].second << ")." << std::endl;
952 : 0 : d_lex.parseError(sse.str().c_str());
953 : 0 : }
954 : : // read the grouped rule listing (<GTerm>+)
955 : 1790 : d_lex.eatToken(Token::LPAREN_TOK);
956 : 1790 : Token tok = d_lex.nextToken();
957 [ + + ]: 9422 : while (tok != Token::RPAREN_TOK)
958 : : {
959 : : // Lookahead for Constant/Variable.
960 : 7634 : bool parsedGTerm = false;
961 [ + + ]: 7634 : if (tok == Token::LPAREN_TOK)
962 : : {
963 : 4317 : Token tok2 = d_lex.nextToken();
964 [ + + ]: 4317 : if (tok2 == Token::SYMBOL)
965 : : {
966 : 4297 : std::string tokenStr(d_lex.tokenStr());
967 [ + + ]: 4297 : if (tokenStr == "Constant")
968 : : {
969 : 124 : t = parseSort();
970 : 124 : ret->addAnyConstant(ntSyms[i]);
971 : 124 : d_lex.eatToken(Token::RPAREN_TOK);
972 : 124 : parsedGTerm = true;
973 : : }
974 [ + + ]: 4173 : else if (tokenStr == "Variable")
975 : : {
976 : 51 : t = parseSort();
977 : 51 : ret->addAnyVariable(ntSyms[i]);
978 : 51 : d_lex.eatToken(Token::RPAREN_TOK);
979 : 51 : parsedGTerm = true;
980 : : }
981 : : else
982 : : {
983 : : // Did not process tok2.
984 : 4122 : d_lex.reinsertToken(tok2);
985 : : }
986 : 4297 : }
987 : : else
988 : : {
989 : : // Did not process tok2.
990 : 20 : d_lex.reinsertToken(tok2);
991 : : }
992 : : }
993 [ + + ]: 7634 : if (!parsedGTerm)
994 : : {
995 : : // We did not process tok. Note that Lex::d_peeked may contain
996 : : // {tok2, LPAREN_TOK} or {tok}.
997 : 7459 : d_lex.reinsertToken(tok);
998 : : // parse ordinary term
999 : 7459 : Term e = parseTerm();
1000 : 7457 : ret->addRule(ntSyms[i], e);
1001 : 7457 : }
1002 : 7632 : tok = d_lex.nextToken();
1003 : : }
1004 : : // finish the non-terminal
1005 : 1788 : d_lex.eatToken(Token::RPAREN_TOK);
1006 : 1792 : }
1007 : 806 : d_lex.eatToken(Token::RPAREN_TOK);
1008 : : // pop scope from the pre-declaration
1009 : 806 : d_state.popScope();
1010 : 806 : return ret;
1011 : 810 : }
1012 : :
1013 : 1907 : Grammar* Smt2TermParser::parseGrammarOrNull(const std::vector<Term>& sygusVars)
1014 : : {
1015 : 1907 : Token t = d_lex.peekToken();
1016 : : // note that we assume that the grammar is not present if the input continues
1017 : : // with anything other than left parenthesis.
1018 [ + + ]: 1907 : if (t != Token::LPAREN_TOK)
1019 : : {
1020 : 1099 : return nullptr;
1021 : : }
1022 : 808 : return parseGrammar(sygusVars);
1023 : : }
1024 : :
1025 : 25214 : uint32_t Smt2TermParser::parseIntegerNumeral()
1026 : : {
1027 : 25214 : d_lex.eatToken(Token::INTEGER_LITERAL);
1028 : 25213 : return tokenStrToUnsigned();
1029 : : }
1030 : :
1031 : 404956 : uint32_t Smt2TermParser::tokenStrToUnsigned()
1032 : : {
1033 : : // forbid leading zeroes if in strict mode
1034 : 404956 : std::string token = d_lex.tokenStr();
1035 [ + + ]: 404956 : if (d_lex.isStrict())
1036 : : {
1037 [ + + ][ - + ]: 17 : if (token.size() > 1 && token[0] == '0')
[ - + ]
1038 : : {
1039 : 0 : d_lex.parseError("Numerals with leading zeroes are forbidden");
1040 : : }
1041 : : }
1042 [ + + ][ + + ]: 404956 : if (token.size() > 1 && token[0] == '-')
[ + + ]
1043 : : {
1044 : 3 : d_lex.parseError("Negative numerals are forbidden in indices");
1045 : : }
1046 : 404955 : uint32_t result = d_state.parseStringToUnsigned(token);
1047 : 404955 : return result;
1048 : 404956 : }
1049 : :
1050 : 13361647 : std::string Smt2TermParser::tokenStrToSymbol(Token tok)
1051 : : {
1052 : 13361647 : std::string id;
1053 [ + + ][ - - ]: 13361647 : switch (tok)
1054 : : {
1055 : 13349978 : case Token::SYMBOL: id = d_lex.tokenStr(); break;
1056 : 11669 : case Token::QUOTED_SYMBOL:
1057 : 11669 : id = d_lex.tokenStr();
1058 : : // strip off the quotes
1059 : 11669 : id = id.erase(0, 1);
1060 : 11669 : id = id.erase(id.size() - 1, 1);
1061 : 11669 : break;
1062 : 0 : case Token::UNTERMINATED_QUOTED_SYMBOL:
1063 : 0 : d_lex.parseError("Expected SMT-LIBv2 symbol", true);
1064 : 0 : break;
1065 : 0 : default:
1066 : 0 : d_lex.unexpectedTokenError(tok, "Expected SMT-LIBv2 symbol");
1067 : 0 : break;
1068 : : }
1069 : 13361647 : return id;
1070 : 0 : }
1071 : :
1072 : 34526 : std::vector<std::string> Smt2TermParser::parseNumeralList()
1073 : : {
1074 : 34526 : std::vector<std::string> numerals;
1075 : 34526 : Token tok = d_lex.nextToken();
1076 [ + + ]: 69536 : while (tok == Token::INTEGER_LITERAL)
1077 : : {
1078 : 35010 : numerals.emplace_back(d_lex.tokenStr());
1079 : 35010 : tok = d_lex.nextToken();
1080 : : }
1081 : 34526 : d_lex.reinsertToken(tok);
1082 : 34526 : return numerals;
1083 : 0 : }
1084 : :
1085 : 3855 : std::vector<DatatypeDecl> Smt2TermParser::parseDatatypesDef(
1086 : : bool isCo,
1087 : : const std::vector<std::string>& dnames,
1088 : : const std::vector<size_t>& arities)
1089 : : {
1090 [ + + ][ + - ]: 3855 : Assert(dnames.size() == arities.size()
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
1091 : : || (dnames.size() == 1 && arities.empty()));
1092 : 3855 : TermManager& tm = d_state.getSolver()->getTermManager();
1093 : 3855 : std::vector<DatatypeDecl> dts;
1094 : 3855 : d_state.pushScope();
1095 : : // Declare the datatypes that are currently being defined as unresolved
1096 : : // types. If we do not know the arity of the datatype yet, we wait to
1097 : : // define it until parsing the preamble of its body, which may optionally
1098 : : // involve `par`. This is limited to the case of single datatypes defined
1099 : : // via declare-datatype, and hence no datatype body is parsed without
1100 : : // having all types declared. This ensures we can parse datatypes with
1101 : : // nested recursion, e.g. datatypes D having a subfield type
1102 : : // (Array Int D).
1103 [ + + ]: 8730 : for (unsigned i = 0, dsize = dnames.size(); i < dsize; i++)
1104 : : {
1105 [ + + ]: 4875 : if (i >= arities.size())
1106 : : {
1107 : : // do not know the arity yet
1108 : 609 : continue;
1109 : : }
1110 : 4266 : d_state.mkUnresolvedType(dnames[i], arities[i]);
1111 : : }
1112 : : // while we get another datatype declaration, or close the list
1113 : 3855 : Token tok = d_lex.nextToken();
1114 [ + + ]: 8730 : while (tok == Token::LPAREN_TOK)
1115 : : {
1116 : 4875 : std::vector<Sort> params;
1117 : 4875 : size_t i = dts.size();
1118 [ + - ]: 4875 : Trace("parser-dt") << "Processing datatype #" << i << std::endl;
1119 [ - + ]: 4875 : if (i >= dnames.size())
1120 : : {
1121 : 0 : d_lex.parseError("Too many datatypes defined in this block.");
1122 : : }
1123 : 4875 : tok = d_lex.nextToken();
1124 : 4875 : bool pushedScope = false;
1125 [ + + ]: 4875 : if (tok == Token::PAR_TOK)
1126 : : {
1127 : 200 : pushedScope = true;
1128 : 200 : d_state.pushScope();
1129 : : std::vector<std::string> symList =
1130 : 200 : parseSymbolList(CHECK_UNDECLARED, SYM_SORT);
1131 [ - + ]: 200 : if (symList.empty())
1132 : : {
1133 : 0 : d_lex.parseError("Expected non-empty parameter list");
1134 : : }
1135 [ + + ]: 457 : for (const std::string& sym : symList)
1136 : : {
1137 : 257 : params.push_back(d_state.mkSort(sym));
1138 : : }
1139 [ + - ]: 400 : Trace("parser-dt") << params.size() << " parameters for " << dnames[i]
1140 : 200 : << std::endl;
1141 : 200 : dts.push_back(tm.mkDatatypeDecl(dnames[i], params, isCo));
1142 : 200 : }
1143 : : else
1144 : : {
1145 : 4675 : d_lex.reinsertToken(tok);
1146 : : // we will parse the parentheses-enclosed construct list below
1147 : 4675 : d_lex.reinsertToken(Token::LPAREN_TOK);
1148 : 4675 : dts.push_back(tm.mkDatatypeDecl(dnames[i], params, isCo));
1149 : : }
1150 [ + + ]: 4875 : if (i >= arities.size())
1151 : : {
1152 : : // if the arity is not yet fixed, declare it as an unresolved type
1153 : 609 : d_state.mkUnresolvedType(dnames[i], params.size());
1154 : : }
1155 [ - + ]: 4266 : else if (params.size() != arities[i])
1156 : : {
1157 : : // if the arity was fixed by prelude and is not equal to the number of
1158 : : // parameters
1159 : 0 : d_lex.parseError("Wrong number of parameters for datatype.");
1160 : : }
1161 : : // read constructor definition list, populate into the current datatype
1162 : 4875 : parseConstructorDefinitionList(dts.back());
1163 [ + + ]: 4875 : if (pushedScope)
1164 : : {
1165 : 200 : d_lex.eatToken(Token::RPAREN_TOK);
1166 : 200 : d_state.popScope();
1167 : : }
1168 : 4875 : tok = d_lex.nextToken();
1169 : 4875 : }
1170 [ - + ]: 3855 : if (dts.size() != dnames.size())
1171 : : {
1172 : 0 : d_lex.unexpectedTokenError(tok, "Wrong number of datatypes provided.");
1173 : : }
1174 : 3855 : d_lex.reinsertToken(tok);
1175 : 3855 : d_state.popScope();
1176 : 3855 : return dts;
1177 : 0 : }
1178 : :
1179 : 4875 : void Smt2TermParser::parseConstructorDefinitionList(DatatypeDecl& type)
1180 : : {
1181 : 4875 : d_lex.eatToken(Token::LPAREN_TOK);
1182 : 4875 : TermManager& tm = d_state.getSolver()->getTermManager();
1183 : : // parse another constructor or close the list
1184 [ + + ]: 13725 : while (d_lex.eatTokenChoice(Token::LPAREN_TOK, Token::RPAREN_TOK))
1185 : : {
1186 : 8850 : std::string name = parseSymbol(CHECK_NONE, SYM_VARIABLE);
1187 : 8850 : DatatypeConstructorDecl ctor(tm.mkDatatypeConstructorDecl(name));
1188 : : // parse another selector or close the current constructor
1189 [ + + ]: 17187 : while (d_lex.eatTokenChoice(Token::LPAREN_TOK, Token::RPAREN_TOK))
1190 : : {
1191 : 8337 : std::string id = parseSymbol(CHECK_NONE, SYM_SORT);
1192 : 8337 : Sort t = parseSort();
1193 : 8337 : ctor.addSelector(id, t);
1194 [ + - ]: 16674 : Trace("parser-idt") << "selector: " << id << " of type " << t
1195 : 8337 : << std::endl;
1196 : 8337 : d_lex.eatToken(Token::RPAREN_TOK);
1197 : 8337 : }
1198 : : // make the constructor
1199 : 8850 : type.addConstructor(ctor);
1200 [ + - ]: 8850 : Trace("parser-idt") << "constructor: " << name << std::endl;
1201 : 8850 : }
1202 : 4875 : }
1203 : :
1204 : 28 : std::string Smt2TermParser::parseStr(bool unescape)
1205 : : {
1206 : 28 : d_lex.eatToken(Token::STRING_LITERAL);
1207 : 28 : std::string s = d_lex.tokenStr();
1208 [ + - ]: 28 : if (unescape)
1209 : : {
1210 : 28 : unescapeString(s);
1211 : : }
1212 : 28 : return s;
1213 : 0 : }
1214 : :
1215 : 28121 : void Smt2TermParser::unescapeString(std::string& s)
1216 : : {
1217 : : // strip off the quotes
1218 : 28121 : s = s.erase(0, 1);
1219 : 28121 : s = s.erase(s.size() - 1, 1);
1220 [ + + ]: 120092 : for (size_t i = 0, ssize = s.size(); i < ssize; i++)
1221 : : {
1222 [ - + ][ - - ]: 91971 : if ((unsigned)s[i] > 127 && !isprint(s[i]))
[ - + ]
1223 : : {
1224 : 0 : d_lex.parseError(
1225 : : "Extended/unprintable characters are not "
1226 : : "part of SMT-LIB, and they must be encoded "
1227 : : "as escape sequences");
1228 : : }
1229 : : }
1230 : 28121 : size_t dst = 0;
1231 [ + + ]: 120041 : for (size_t src = 0; src<s.size(); ++src, ++dst)
1232 : : {
1233 : 91920 : s[dst] = s[src];
1234 [ + + ]: 91920 : if (s[src]=='"')
1235 : : {
1236 : 51 : ++src;
1237 : : }
1238 : : }
1239 : 28121 : s.erase(dst);
1240 : 28121 : }
1241 : :
1242 : 363650 : ParseOp Smt2TermParser::continueParseIndexedIdentifier(bool isOperator)
1243 : : {
1244 : 363650 : ParseOp p;
1245 : 363650 : std::string name = parseSymbol(CHECK_NONE, SYM_VARIABLE);
1246 : : // parse the list of numerals or symbols
1247 : 363650 : std::vector<std::string> symbols;
1248 : 363650 : std::vector<uint32_t> numerals;
1249 : : // we currently only have symbols that are indexed by only numerals, or
1250 : : // are indexed by a symbol, followed by combinations of symbols/numerals.
1251 : 363650 : Token tok = d_lex.nextToken();
1252 [ + + ]: 748070 : while (tok != Token::RPAREN_TOK)
1253 : : {
1254 [ + + ][ + + ]: 384422 : switch (tok)
1255 : : {
1256 : 379847 : case Token::INTEGER_LITERAL:
1257 [ + + ]: 379847 : if (symbols.empty())
1258 : : {
1259 : 379743 : numerals.push_back(tokenStrToUnsigned());
1260 : : }
1261 : : else
1262 : : {
1263 : : // If we parsed a symbol, treat the remaining indices as symbols
1264 : : // This is required for parsing fmf.card.
1265 : 104 : symbols.push_back(d_lex.tokenStr());
1266 : : }
1267 : 379846 : break;
1268 : 4567 : case Token::SYMBOL:
1269 : : case Token::HEX_LITERAL:
1270 : : // (_ char <hex_literal>) expects a hex literal
1271 : 4567 : symbols.push_back(d_lex.tokenStr());
1272 : 4567 : break;
1273 : 7 : case Token::QUOTED_SYMBOL:
1274 : 7 : symbols.push_back(tokenStrToSymbol(tok));
1275 : 7 : break;
1276 : 1 : default:
1277 : 3 : d_lex.unexpectedTokenError(
1278 : : tok, "Expected index while parsing indexed identifier");
1279 : 0 : break;
1280 : : }
1281 : 384420 : tok = d_lex.nextToken();
1282 : : }
1283 [ + + ][ - + ]: 363648 : if (numerals.empty() && symbols.empty())
[ - + ]
1284 : : {
1285 : 0 : d_lex.parseError(std::string("No indices provided for symbol " + name));
1286 : : }
1287 : : // if indexed by numerals
1288 [ + + ]: 363648 : if (!numerals.empty())
1289 : : {
1290 [ + + ]: 359075 : if (!isOperator)
1291 : : {
1292 : : // resolve the index constant
1293 : 185065 : p.d_expr = d_state.mkIndexedConstant(name, numerals);
1294 : : }
1295 : : else
1296 : : {
1297 : : // In some cases, we don't know which kind to use until we know the type
1298 : : // of the arguments, which is the case for:
1299 : : // - to_fp
1300 : : // - (_ tuple.select n) and (_ tuple.update n)
1301 : : // For consistency, we always construct the op lazily.
1302 : 174010 : p.d_name = name;
1303 : 174010 : p.d_indices = numerals;
1304 : 174010 : p.d_kind = Kind::UNDEFINED_KIND;
1305 : : }
1306 : : }
1307 : : // otherwise, indexed by symbols
1308 [ + + ]: 4573 : else if (!isOperator)
1309 : : {
1310 : : // handles:
1311 : : // - fmf.card indexed by Type symbol + numeral
1312 : : // - char indexed by HEX
1313 : 118 : p.d_expr = d_state.mkIndexedConstant(name, symbols);
1314 : : }
1315 : : else
1316 : : {
1317 : : // handles:
1318 : : // - testers and updaters indexed by constructor names
1319 : 4455 : Kind k = d_state.getIndexedOpKind(name);
1320 [ + + ][ + + ]: 4455 : if (k != Kind::APPLY_UPDATER && k != Kind::APPLY_TESTER
1321 [ - + ]: 12 : && k != Kind::NULLABLE_LIFT)
1322 : : {
1323 : 0 : d_lex.parseError(std::string("Unexpected indexed symbol " + name));
1324 : : }
1325 [ - + ]: 4455 : if (symbols.size() != 1)
1326 : : {
1327 : 0 : d_lex.parseError(std::string("Unexpected number of indices for " + name));
1328 : : }
1329 : 4455 : p.d_kind = k;
1330 : 4455 : p.d_name = symbols[0];
1331 : : }
1332 : 727290 : return p;
1333 : 363665 : }
1334 : :
1335 : 2091 : ParseOp Smt2TermParser::continueParseQualifiedIdentifier(bool isOperator)
1336 : : {
1337 : 2091 : ParseOp op;
1338 : 2091 : Token tok = d_lex.nextToken();
1339 [ - + ][ - - ]: 2091 : switch (tok)
1340 : : {
1341 : 0 : case Token::LPAREN_TOK:
1342 [ - - ]: 0 : tok = d_lex.nextToken();
1343 : : switch (tok)
1344 : : {
1345 : 0 : case Token::INDEX_TOK:
1346 : 0 : op = continueParseIndexedIdentifier(isOperator);
1347 : 0 : break;
1348 : 0 : default:
1349 : 0 : d_lex.unexpectedTokenError(tok,
1350 : : "Expected (indexed) identifier while "
1351 : : "parsing qualified identifier");
1352 : 0 : break;
1353 : : }
1354 : 0 : break;
1355 : 2091 : case Token::SYMBOL:
1356 : 2091 : case Token::QUOTED_SYMBOL: op.d_name = tokenStrToSymbol(tok); break;
1357 : 0 : case Token::UNTERMINATED_QUOTED_SYMBOL:
1358 : 0 : d_lex.parseError("Expected identifier while parsing qualified identifier",
1359 : : true);
1360 : 0 : break;
1361 : 0 : default:
1362 : 0 : d_lex.unexpectedTokenError(
1363 : : tok, "Expected identifier while parsing qualified identifier");
1364 : 0 : break;
1365 : : }
1366 : : // parse a sort
1367 : 4182 : Sort type = parseSort();
1368 : : // close parentheses
1369 : 2091 : d_lex.eatToken(Token::RPAREN_TOK);
1370 : : // apply the type ascription to the parsed op
1371 : 2091 : d_state.parseOpApplyTypeAscription(op, type);
1372 : 4182 : return op;
1373 : 0 : }
1374 : :
1375 : 362 : Term Smt2TermParser::parseMatchCasePattern(Sort headSort,
1376 : : std::vector<Term>& boundVars)
1377 : : {
1378 [ + + ]: 362 : if (d_lex.eatTokenChoice(Token::SYMBOL, Token::LPAREN_TOK))
1379 : : {
1380 : : // a nullary constructor or variable, depending on if the symbol is declared
1381 : 88 : std::string name = d_lex.tokenStr();
1382 [ + + ]: 88 : if (d_state.isDeclared(name, SYM_VARIABLE))
1383 : : {
1384 : 76 : Term pat = d_state.getVariable(name);
1385 : 76 : Sort type = pat.getSort();
1386 [ - + ]: 76 : if (!type.isDatatype())
1387 : : {
1388 : 0 : d_lex.parseError(
1389 : : "Must apply constructors of arity greater than 0 to arguments in "
1390 : : "pattern.");
1391 : : }
1392 : : // make nullary constructor application
1393 : 76 : return pat;
1394 : 76 : }
1395 : : // it has the type of the head expr
1396 : 12 : Term pat = d_state.bindBoundVar(name, headSort);
1397 : 12 : boundVars.push_back(pat);
1398 : 12 : return pat;
1399 : 88 : }
1400 : : // a non-nullary constructor
1401 : : // We parse a constructor name
1402 : 274 : const Datatype& dt = headSort.getDatatype();
1403 : 274 : std::string cname = parseSymbol(CHECK_DECLARED, SYM_VARIABLE);
1404 : 274 : const DatatypeConstructor& dc = dt.getConstructor(cname);
1405 : : // get the constructor, which could be instantiated based on the head type
1406 : : // if we are a parametric datatype
1407 [ + + ]: 274 : Term f = dt.isParametric() ? dc.getInstantiatedTerm(headSort) : dc.getTerm();
1408 : : // f should be a constructor
1409 : 274 : Sort type = f.getSort();
1410 [ - + ][ - + ]: 274 : Assert(type.isDatatypeConstructor());
[ - - ]
1411 [ + - ]: 274 : Trace("parser-dt") << "Pattern head : " << f << " " << type << std::endl;
1412 : 274 : std::vector<Sort> argTypes = type.getDatatypeConstructorDomainSorts();
1413 : : // now, parse symbols that are interpreted as bindings for the argument
1414 : : // types
1415 [ + + ]: 527 : while (d_lex.eatTokenChoice(Token::SYMBOL, Token::RPAREN_TOK))
1416 : : {
1417 [ - + ]: 253 : if (boundVars.size() >= argTypes.size())
1418 : : {
1419 : 0 : d_state.parseError("Too many arguments for pattern.");
1420 : : }
1421 : : // make of proper type
1422 : : Term arg =
1423 : 506 : d_state.bindBoundVar(d_lex.tokenStr(), argTypes[boundVars.size()]);
1424 : 253 : boundVars.push_back(arg);
1425 : 253 : }
1426 : 274 : std::vector<Term> cargs;
1427 : 274 : cargs.push_back(f);
1428 : 274 : cargs.insert(cargs.end(), boundVars.begin(), boundVars.end());
1429 : : // make the pattern term
1430 : 274 : return d_state.getSolver()->getTermManager().mkTerm(Kind::APPLY_CONSTRUCTOR,
1431 : 274 : cargs);
1432 : 274 : }
1433 : :
1434 : : } // namespace parser
1435 : : } // namespace cvc5
|
