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 : : * Parser state implementation.
11 : : */
12 : :
13 : : #include "parser/parser_state.h"
14 : :
15 : : #include <cvc5/cvc5.h>
16 : :
17 : : #include <clocale>
18 : : #include <fstream>
19 : : #include <iostream>
20 : : #include <iterator>
21 : : #include <limits>
22 : : #include <sstream>
23 : : #include <unordered_set>
24 : :
25 : : #include "base/check.h"
26 : : #include "base/output.h"
27 : : #include "expr/kind.h"
28 : : #include "parser/commands.h"
29 : :
30 : : using namespace std;
31 : :
32 : : namespace cvc5 {
33 : : namespace parser {
34 : :
35 : 23526 : ParserState::ParserState(ParserStateCallback* psc,
36 : : Solver* solver,
37 : : SymManager* sm,
38 : 23526 : ParsingMode parsingMode)
39 : 23526 : : d_solver(solver),
40 : 47052 : d_tm(d_solver->getTermManager()),
41 : 23526 : d_psc(psc),
42 : 23526 : d_symman(sm),
43 : 23526 : d_symtab(sm->getSymbolTable()),
44 : 23526 : d_checksEnabled(true),
45 : 23526 : d_parsingMode(parsingMode),
46 : 47052 : d_parseOnly(d_solver->getOptionInfo("parse-only").boolValue())
47 : : {
48 : 23526 : }
49 : :
50 : 23526 : ParserState::~ParserState() {}
51 : :
52 : 254835 : Solver* ParserState::getSolver() const { return d_solver; }
53 : :
54 : 5589888 : Term ParserState::getVariable(const std::string& name)
55 : : {
56 : 5589888 : Term ret = d_symtab->lookup(name);
57 : : // if the lookup failed, throw an error
58 [ + + ]: 5589888 : if (ret.isNull())
59 : : {
60 : 2126 : checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE);
61 : : }
62 : 5589879 : return ret;
63 : 9 : }
64 : :
65 : 5332 : Term ParserState::getExpressionForNameAndType(const std::string& name, Sort t)
66 : : {
67 [ - + ][ - + ]: 5332 : Assert(isDeclared(name));
[ - - ]
68 : : // first check if the variable is declared and not overloaded
69 : 5332 : Term expr = getVariable(name);
70 [ + + ]: 5332 : if (expr.isNull())
71 : : {
72 : : // the variable is overloaded, try with type if the type exists
73 [ + - ]: 6 : if (!t.isNull())
74 : : {
75 : : // if we decide later to support annotations for function types, this will
76 : : // update to separate t into ( argument types, return type )
77 : 6 : expr = getOverloadedConstantForType(name, t);
78 [ - + ]: 6 : if (expr.isNull())
79 : : {
80 : 0 : parseError("Cannot get overloaded constant for type ascription.");
81 : : }
82 : : }
83 : : else
84 : : {
85 : 0 : parseError("Overloaded constants must be type cast.");
86 : : }
87 : : }
88 [ - + ][ - + ]: 5332 : Assert(!expr.isNull());
[ - - ]
89 : 5332 : return expr;
90 : 0 : }
91 : :
92 : 0 : bool ParserState::getTesterName(CVC5_UNUSED Term cons,
93 : : CVC5_UNUSED std::string& name)
94 : : {
95 : 0 : return false;
96 : : }
97 : :
98 : 704672 : Kind ParserState::getKindForFunction(Term fun)
99 : : {
100 : 704672 : Sort t = fun.getSort();
101 [ + + ]: 704672 : if (t.isFunction())
102 : : {
103 : 668693 : return Kind::APPLY_UF;
104 : : }
105 [ + + ]: 35979 : else if (t.isDatatypeConstructor())
106 : : {
107 : 12780 : return Kind::APPLY_CONSTRUCTOR;
108 : : }
109 [ + + ]: 23199 : else if (t.isDatatypeSelector())
110 : : {
111 : 22831 : return Kind::APPLY_SELECTOR;
112 : : }
113 [ + - ]: 368 : else if (t.isDatatypeTester())
114 : : {
115 : 368 : return Kind::APPLY_TESTER;
116 : : }
117 [ - - ]: 0 : else if (t.isDatatypeUpdater())
118 : : {
119 : 0 : return Kind::APPLY_UPDATER;
120 : : }
121 : 0 : return Kind::UNDEFINED_KIND;
122 : 704672 : }
123 : :
124 : 539228 : Sort ParserState::getSort(const std::string& name)
125 : : {
126 : 539228 : Sort t = d_symtab->lookupType(name);
127 : : // if we fail, throw an error
128 [ + + ]: 539228 : if (t.isNull())
129 : : {
130 : 3 : checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
131 : : }
132 : 539227 : return t;
133 : 1 : }
134 : :
135 : 1568 : Sort ParserState::getParametricSort(const std::string& name,
136 : : const std::vector<Sort>& params)
137 : : {
138 : 1568 : Sort t = d_symtab->lookupType(name, params);
139 : : // if we fail, throw an error
140 [ + + ]: 1567 : if (t.isNull())
141 : : {
142 : 6 : checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
143 : : }
144 : 1565 : return t;
145 : 2 : }
146 : :
147 : 704643 : bool ParserState::isFunctionLike(Term fun)
148 : : {
149 [ - + ]: 704643 : if (fun.isNull())
150 : : {
151 : 0 : return false;
152 : : }
153 : 704643 : Sort type = fun.getSort();
154 [ + + ]: 740596 : return type.isFunction() || type.isDatatypeConstructor()
155 [ + + ][ + + ]: 740596 : || type.isDatatypeTester() || type.isDatatypeSelector();
[ + + ]
156 : 704643 : }
157 : :
158 : 705 : Term ParserState::bindVar(const std::string& name,
159 : : const Sort& type,
160 : : bool doOverload)
161 : : {
162 [ + - ]: 705 : Trace("parser") << "bindVar(" << name << ", " << type << ")" << std::endl;
163 : 705 : Term expr = d_tm.mkConst(type, name);
164 : 705 : defineVar(name, expr, doOverload);
165 : 705 : return expr;
166 : 0 : }
167 : :
168 : 157909 : Term ParserState::bindBoundVar(const std::string& name,
169 : : const Sort& type,
170 : : bool fresh)
171 : : {
172 [ + - ]: 315818 : Trace("parser") << "bindBoundVar(" << name << ", " << type << ")"
173 : 157909 : << std::endl;
174 : 157909 : std::pair<std::string, Sort> key(name, type);
175 : 157909 : Term expr;
176 [ + + ]: 157909 : if (fresh)
177 : : {
178 : 5711 : expr = d_tm.mkVar(type, name);
179 : : }
180 : : else
181 : : {
182 : : std::map<std::pair<std::string, Sort>, Term>::iterator itv =
183 : 152198 : d_varCache.find(key);
184 [ + + ]: 152198 : if (itv != d_varCache.end())
185 : : {
186 : 89202 : expr = itv->second;
187 : : }
188 : : else
189 : : {
190 : 62996 : expr = d_tm.mkVar(type, name);
191 : 62996 : d_varCache[key] = expr;
192 : : }
193 : : }
194 : 157909 : defineVar(name, expr);
195 : 315818 : return expr;
196 : 157909 : }
197 : :
198 : 79097 : std::vector<Term> ParserState::bindBoundVars(
199 : : std::vector<std::pair<std::string, Sort>>& sortedVarNames, bool fresh)
200 : : {
201 : 79097 : std::vector<Term> vars;
202 [ + + ]: 224123 : for (std::pair<std::string, Sort>& i : sortedVarNames)
203 : : {
204 : 145026 : vars.push_back(bindBoundVar(i.first, i.second, fresh));
205 : : }
206 : 79097 : return vars;
207 : 0 : }
208 : :
209 : 77635 : std::vector<Term> ParserState::bindBoundVarsCtx(
210 : : std::vector<std::pair<std::string, Sort>>& sortedVarNames,
211 : : std::vector<std::vector<std::pair<std::string, Term>>>& letBinders,
212 : : bool fresh)
213 : : {
214 [ + + ][ + + ]: 77635 : if (fresh || letBinders.empty())
[ + + ]
215 : : {
216 : : // does not matter if let binders are empty or if we are constructing fresh
217 : 70646 : return bindBoundVars(sortedVarNames, fresh);
218 : : }
219 : 6989 : std::vector<Term> vars;
220 [ + + ]: 16509 : for (std::pair<std::string, Sort>& i : sortedVarNames)
221 : : {
222 : : std::map<std::pair<std::string, Sort>, Term>::const_iterator itv =
223 : 9520 : d_varCache.find(i);
224 [ + + ][ + + ]: 9520 : if (itv == d_varCache.end() || !isDeclared(i.first))
[ + + ]
225 : : {
226 : : // haven't created this variable yet, or its not declared
227 : 9496 : Term v = bindBoundVar(i.first, i.second, fresh);
228 : 9496 : vars.push_back(v);
229 : 9496 : continue;
230 : 9496 : }
231 : 24 : Term v = itv->second;
232 : : // If we are here, then:
233 : : // (1) we are not using fresh declarations
234 : : // (2) there are let binders present,
235 : : // (3) the current variable was shadowed.
236 : : // We must check whether the variable is present in the let bindings.
237 : 24 : bool reqFresh = false;
238 : : // a dummy variable used for checking containment below
239 : 48 : Term vr = d_tm.mkVar(v.getSort(), "dummy");
240 : : // check if it is contained in a let binder, if so, we require making a
241 : : // fresh variable, despite fresh-binders being false.
242 [ + + ]: 45 : for (std::vector<std::pair<std::string, Term>>& lbs : letBinders)
243 : : {
244 [ + + ]: 44 : for (std::pair<std::string, Term>& lb : lbs)
245 : : {
246 : : // To test containment, we use Term::substitute.
247 : : // If the substitution does anything at all, then we will throw a
248 : : // warning. We expect this warning to be very rare.
249 : 23 : Term slbt = lb.second.substitute({v}, {vr});
250 [ + + ]: 23 : if (slbt != lb.second)
251 : : {
252 : 3 : reqFresh = true;
253 : 3 : break;
254 : : }
255 [ + + ]: 23 : }
256 [ + + ]: 24 : if (reqFresh)
257 : : {
258 : 3 : break;
259 : : }
260 : : }
261 [ + + ]: 24 : if (reqFresh)
262 : : {
263 : : // Note that if this warning is thrown:
264 : : // 1. proof reference checking will not be accurate in settings where
265 : : // variables are parsed as canonical.
266 : : // 2. the parser will not be deterministic for the same input even when
267 : : // fresh-binders is false, since we are constructing a fresh variable
268 : : // below.
269 [ - + ]: 6 : Warning() << "Constructing a fresh variable for " << i.first
270 : : << " since this symbol occurs in a let term that is present in "
271 : : "the current context. Set fresh-binders to true or use -q "
272 : : "to avoid "
273 : 3 : "this warning."
274 : 3 : << std::endl;
275 : : }
276 : 24 : v = bindBoundVar(i.first, i.second, reqFresh);
277 : 24 : vars.push_back(v);
278 : 24 : }
279 : 6989 : return vars;
280 : 6989 : }
281 : :
282 : 0 : std::vector<Term> ParserState::bindBoundVars(
283 : : const std::vector<std::string> names, const Sort& type)
284 : : {
285 : 0 : std::vector<Term> vars;
286 [ - - ]: 0 : for (unsigned i = 0; i < names.size(); ++i)
287 : : {
288 : 0 : vars.push_back(bindBoundVar(names[i], type));
289 : : }
290 : 0 : return vars;
291 : 0 : }
292 : :
293 : 688906 : void ParserState::defineVar(const std::string& name,
294 : : const Term& val,
295 : : bool doOverload)
296 : : {
297 [ + - ]: 688906 : Trace("parser") << "defineVar( " << name << " := " << val << ")" << std::endl;
298 [ - + ]: 688906 : if (!d_symtab->bind(name, val, doOverload))
299 : : {
300 : 0 : std::stringstream ss;
301 : 0 : ss << "Cannot bind " << name << " to symbol of type " << val.getSort();
302 : 0 : ss << ", maybe the symbol has already been defined?";
303 : 0 : parseError(ss.str());
304 : 0 : }
305 [ - + ][ - + ]: 688906 : Assert(isDeclared(name));
[ - - ]
306 : 688906 : }
307 : :
308 : 209804 : void ParserState::defineType(const std::string& name,
309 : : const Sort& type,
310 : : bool isUser)
311 : : {
312 [ + + ][ + + ]: 209804 : if (!isUser && isDeclared(name, SYM_SORT))
[ + + ]
313 : : {
314 [ - + ][ - + ]: 13715 : Assert(d_symtab->lookupType(name) == type);
[ - - ]
315 : 13715 : return;
316 : : }
317 : 196089 : d_symman->bindType(name, type, isUser);
318 [ - + ][ - + ]: 196089 : Assert(isDeclared(name, SYM_SORT));
[ - - ]
319 : : }
320 : :
321 : 207 : void ParserState::defineType(const std::string& name,
322 : : const std::vector<Sort>& params,
323 : : const Sort& type,
324 : : bool isUser)
325 : : {
326 : 207 : d_symman->bindType(name, params, type, isUser);
327 [ - + ][ - + ]: 207 : Assert(isDeclared(name, SYM_SORT));
[ - - ]
328 : 207 : }
329 : :
330 : 266 : Sort ParserState::mkSort(const std::string& name)
331 : : {
332 [ + - ]: 266 : Trace("parser") << "newSort(" << name << ")" << std::endl;
333 : 266 : Sort type = d_tm.mkUninterpretedSort(name);
334 : 266 : defineType(name, type, true);
335 : 266 : return type;
336 : 0 : }
337 : :
338 : 0 : Sort ParserState::mkSortConstructor(const std::string& name, size_t arity)
339 : : {
340 [ - - ]: 0 : Trace("parser") << "newSortConstructor(" << name << ", " << arity << ")"
341 : 0 : << std::endl;
342 : 0 : Sort type = d_tm.mkUninterpretedSortConstructorSort(arity, name);
343 : 0 : defineType(name, vector<Sort>(arity), type, true);
344 : 0 : return type;
345 : 0 : }
346 : :
347 : 4698 : Sort ParserState::mkUnresolvedType(const std::string& name)
348 : : {
349 : 4698 : Sort unresolved = d_tm.mkUnresolvedDatatypeSort(name);
350 : 4698 : defineType(name, unresolved, true);
351 : 4698 : return unresolved;
352 : 0 : }
353 : :
354 : 207 : Sort ParserState::mkUnresolvedTypeConstructor(const std::string& name,
355 : : size_t arity)
356 : : {
357 : 207 : Sort unresolved = d_tm.mkUnresolvedDatatypeSort(name, arity);
358 : 207 : defineType(name, vector<Sort>(arity), unresolved, true);
359 : 207 : return unresolved;
360 : 0 : }
361 : :
362 : 0 : Sort ParserState::mkUnresolvedTypeConstructor(const std::string& name,
363 : : const std::vector<Sort>& params)
364 : : {
365 [ - - ]: 0 : Trace("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
366 : 0 : << ")" << std::endl;
367 : 0 : Sort unresolved = d_tm.mkUnresolvedDatatypeSort(name, params.size());
368 : 0 : defineType(name, params, unresolved, true);
369 : 0 : Sort t = getParametricSort(name, params);
370 : 0 : return unresolved;
371 : 0 : }
372 : :
373 : 4905 : Sort ParserState::mkUnresolvedType(const std::string& name, size_t arity)
374 : : {
375 [ + + ]: 4905 : if (arity == 0)
376 : : {
377 : 4698 : return mkUnresolvedType(name);
378 : : }
379 : 207 : return mkUnresolvedTypeConstructor(name, arity);
380 : : }
381 : :
382 : 3635 : std::vector<Sort> ParserState::mkMutualDatatypeTypes(
383 : : std::vector<DatatypeDecl>& datatypes)
384 : : {
385 : : try
386 : : {
387 : 3635 : std::vector<Sort> types = d_tm.mkDatatypeSorts(datatypes);
388 : :
389 [ - + ][ - + ]: 3632 : Assert(datatypes.size() == types.size());
[ - - ]
390 : :
391 [ + + ]: 8532 : for (unsigned i = 0; i < datatypes.size(); ++i)
392 : : {
393 : 4900 : Sort t = types[i];
394 : 4900 : const Datatype& dt = t.getDatatype();
395 : 4900 : const std::string& name = dt.getName();
396 [ + - ]: 4900 : Trace("parser-idt") << "define " << name << " as " << t << std::endl;
397 [ - + ]: 4900 : if (isDeclared(name, SYM_SORT))
398 : : {
399 : 0 : throw ParserException(name + " already declared");
400 : : }
401 : 4900 : std::unordered_set<std::string> consNames;
402 : 4900 : std::unordered_set<std::string> selNames;
403 [ + + ]: 13598 : for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
404 : : {
405 : 8698 : const DatatypeConstructor& ctor = dt[j];
406 : 8698 : Term constructor = ctor.getTerm();
407 [ + - ]: 8698 : Trace("parser-idt") << "+ define " << constructor << std::endl;
408 : 8698 : std::string constructorName = ctor.getName();
409 [ + - ]: 8698 : if (consNames.find(constructorName) == consNames.end())
410 : : {
411 : 8698 : consNames.insert(constructorName);
412 : : }
413 : : else
414 : : {
415 : 0 : throw ParserException(constructorName
416 : 0 : + " already declared in this datatype");
417 : : }
418 [ + + ]: 16603 : for (size_t k = 0, nargs = ctor.getNumSelectors(); k < nargs; k++)
419 : : {
420 : 7905 : const DatatypeSelector& sel = ctor[k];
421 : 7905 : Term selector = sel.getTerm();
422 [ + - ]: 7905 : Trace("parser-idt") << "+++ define " << selector << std::endl;
423 : 7905 : std::string selectorName = sel.getName();
424 [ + - ]: 7905 : if (selNames.find(selectorName) == selNames.end())
425 : : {
426 : 7905 : selNames.insert(selectorName);
427 : : }
428 : : else
429 : : {
430 : 0 : throw ParserException(selectorName
431 : 0 : + " already declared in this datatype");
432 : : }
433 : 7905 : }
434 : 8698 : }
435 : 4900 : }
436 : 7264 : return types;
437 : 3632 : }
438 [ - - ]: 0 : catch (internal::IllegalArgumentException& ie)
439 : : {
440 : 0 : throw ParserException(ie.getMessage());
441 : 0 : }
442 : : }
443 : :
444 : 7555 : Sort ParserState::flattenFunctionType(std::vector<Sort>& sorts,
445 : : Sort range,
446 : : std::vector<Term>& flattenVars)
447 : : {
448 [ + + ]: 7555 : if (range.isFunction())
449 : : {
450 : 9 : std::vector<Sort> domainTypes = range.getFunctionDomainSorts();
451 [ + + ]: 24 : for (unsigned i = 0, size = domainTypes.size(); i < size; i++)
452 : : {
453 : 15 : sorts.push_back(domainTypes[i]);
454 : : // the introduced variable is internal (not parsable)
455 : 15 : std::stringstream ss;
456 : 15 : ss << "__flatten_var_" << i;
457 : 30 : Term v = d_tm.mkVar(domainTypes[i], ss.str());
458 : 15 : flattenVars.push_back(v);
459 : 15 : }
460 : 9 : range = range.getFunctionCodomainSort();
461 : 9 : }
462 : 7555 : return range;
463 : : }
464 : :
465 : 56031 : Sort ParserState::flattenFunctionType(std::vector<Sort>& sorts, Sort range)
466 : : {
467 [ - + ]: 56031 : if (TraceIsOn("parser"))
468 : : {
469 [ - - ]: 0 : Trace("parser") << "flattenFunctionType: range " << range
470 : 0 : << " and domains ";
471 [ - - ]: 0 : for (Sort t : sorts)
472 : : {
473 [ - - ]: 0 : Trace("parser") << " " << t;
474 : 0 : }
475 [ - - ]: 0 : Trace("parser") << "\n";
476 : : }
477 [ + + ]: 56441 : while (range.isFunction())
478 : : {
479 : 410 : std::vector<Sort> domainTypes = range.getFunctionDomainSorts();
480 : 410 : sorts.insert(sorts.end(), domainTypes.begin(), domainTypes.end());
481 : 410 : range = range.getFunctionCodomainSort();
482 : 410 : }
483 : 56031 : return range;
484 : : }
485 : 18206 : Sort ParserState::mkFlatFunctionType(std::vector<Sort>& sorts, Sort range)
486 : : {
487 : : // Note we require this flattening since the API explicitly checks that
488 : : // the range of functions is not a function.
489 : 18206 : Sort newRange = flattenFunctionType(sorts, range);
490 [ + - ]: 18206 : if (!sorts.empty())
491 : : {
492 : 18206 : return d_tm.mkFunctionSort(sorts, newRange);
493 : : }
494 : 0 : return newRange;
495 : 18206 : }
496 : :
497 : 9 : Term ParserState::mkHoApply(Term expr, const std::vector<Term>& args)
498 : : {
499 [ + + ]: 24 : for (size_t i = 0; i < args.size(); i++)
500 : : {
501 [ + + ][ - - ]: 45 : expr = d_tm.mkTerm(Kind::HO_APPLY, {expr, args[i]});
502 : : }
503 : 9 : return expr;
504 : : }
505 : :
506 : 1286 : Term ParserState::applyTypeAscription(Term t, Sort s)
507 : : {
508 : 1286 : Kind k = t.getKind();
509 [ + + ]: 1286 : if (k == Kind::SET_EMPTY)
510 : : {
511 : 511 : t = d_tm.mkEmptySet(s);
512 : : }
513 [ + + ]: 775 : else if (k == Kind::BAG_EMPTY)
514 : : {
515 : 110 : t = d_tm.mkEmptyBag(s);
516 : : }
517 [ + + ]: 665 : else if (k == Kind::CONST_SEQUENCE)
518 : : {
519 [ - + ]: 97 : if (!s.isSequence())
520 : : {
521 : 0 : std::stringstream ss;
522 : 0 : ss << "Type ascription on empty sequence must be a sequence, got " << s;
523 : 0 : parseError(ss.str());
524 : 0 : }
525 [ - + ]: 97 : if (!t.getSequenceValue().empty())
526 : : {
527 : 0 : std::stringstream ss;
528 : 0 : ss << "Cannot apply a type ascription to a non-empty sequence";
529 : 0 : parseError(ss.str());
530 : 0 : }
531 : 97 : t = d_tm.mkEmptySequence(s.getSequenceElementSort());
532 : : }
533 [ + + ]: 568 : else if (k == Kind::SET_UNIVERSE)
534 : : {
535 : 223 : t = d_tm.mkUniverseSet(s);
536 : : }
537 [ + + ]: 345 : else if (k == Kind::SEP_NIL)
538 : : {
539 : 104 : t = d_tm.mkSepNil(s);
540 : : }
541 [ + + ]: 241 : else if (k == Kind::APPLY_CONSTRUCTOR)
542 : : {
543 : : // For nullable.null we do not have a kind.
544 : : // so we need to check the sort here.
545 [ + + ]: 127 : if (s.isNullable())
546 : : {
547 : : // parsing (as nullable.null (Nullable T))
548 : 49 : t = d_tm.mkNullableNull(s);
549 : : }
550 : : else
551 : : {
552 : 156 : std::vector<Term> children(t.begin(), t.end());
553 : : // apply type ascription to the operator and reconstruct
554 : 78 : children[0] = applyTypeAscription(children[0], s);
555 : 78 : t = d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR, children);
556 : 78 : }
557 : : }
558 : 1286 : Sort etype = t.getSort();
559 [ + + ]: 1286 : if (etype.isDatatypeConstructor())
560 : : {
561 : : // Type ascriptions only have an effect on the node structure if this is a
562 : : // parametric datatype.
563 : : // get the datatype that t belongs to
564 : 105 : Sort etyped = etype.getDatatypeConstructorCodomainSort();
565 : 105 : Datatype d = etyped.getDatatype();
566 : : // Note that we check whether the datatype is parametric, and not whether
567 : : // etyped is a parametric datatype, since e.g. the smt2 parser constructs
568 : : // an arbitrary instantitated constructor term before it is resolved.
569 : : // Hence, etyped is an instantiated datatype type, but we correctly
570 : : // check if its datatype is parametric.
571 [ + + ]: 105 : if (d.isParametric())
572 : : {
573 : : // lookup by name, using the raw symbol since toString() may print
574 : : // the name as a quoted symbol, e.g. |C,|
575 : : DatatypeConstructor dc =
576 [ + - ]: 101 : d.getConstructor(t.hasSymbol() ? t.getSymbol() : t.toString());
577 : : // ask the constructor for the specialized constructor term
578 : 101 : t = dc.getInstantiatedTerm(s);
579 : 101 : }
580 : : // the type of t does not match the sort s by design (constructor type
581 : : // vs datatype type), thus we use an alternative check here.
582 [ - + ]: 105 : if (t.getSort().getDatatypeConstructorCodomainSort() != s)
583 : : {
584 : 0 : std::stringstream ss;
585 : 0 : ss << "Type ascription on constructor not satisfied, term " << t
586 : 0 : << " expected sort " << s << " but has sort " << etyped;
587 : 0 : parseError(ss.str());
588 : 0 : }
589 : 105 : return t;
590 : 105 : }
591 : : // Otherwise, check that the type is correct. Type ascriptions in SMT-LIB 2.6
592 : : // referred to the range of function sorts. Note that this is only a check
593 : : // and does not impact the returned term.
594 : 1181 : Sort checkSort = t.getSort();
595 [ + + ]: 1181 : if (checkSort.isFunction())
596 : : {
597 : 3 : checkSort = checkSort.getFunctionCodomainSort();
598 : : }
599 [ - + ]: 1181 : if (checkSort != s)
600 : : {
601 : 0 : std::stringstream ss;
602 : 0 : ss << "Type ascription not satisfied, term " << t
603 : 0 : << " expected (codomain) sort " << s << " but has sort " << t.getSort();
604 : 0 : parseError(ss.str());
605 : 0 : }
606 : 1181 : return t;
607 : 1286 : }
608 : :
609 : 1857302 : bool ParserState::isDeclared(const std::string& name, SymbolType type)
610 : : {
611 [ + + ][ - - ]: 1857302 : switch (type)
612 : : {
613 : 1433194 : case SYM_VARIABLE: return d_symtab->isBound(name);
614 : 424108 : case SYM_SORT: return d_symtab->isBoundType(name);
615 : 0 : case SYM_VERBATIM: Unreachable();
616 : : }
617 : 0 : DebugUnhandled(); // Unhandled(type);
618 : : return false;
619 : : }
620 : :
621 : 2155291 : void ParserState::checkDeclaration(const std::string& varName,
622 : : DeclarationCheck check,
623 : : SymbolType type,
624 : : std::string notes)
625 : : {
626 [ - + ]: 2155291 : if (!d_checksEnabled)
627 : : {
628 : 0 : return;
629 : : }
630 : :
631 [ + + ][ + - ]: 2155291 : switch (check)
632 : : {
633 : 712922 : case CHECK_DECLARED:
634 [ + + ]: 712922 : if (!isDeclared(varName, type))
635 : : {
636 : 125 : parseError("Symbol '" + varName + "' not declared as a "
637 [ + + ]: 100 : + (type == SYM_VARIABLE ? "variable" : "type")
638 [ + - ]: 150 : + (notes.size() == 0 ? notes : "\n" + notes));
639 : : }
640 : 712897 : break;
641 : :
642 : 38140 : case CHECK_UNDECLARED:
643 [ + + ]: 38140 : if (isDeclared(varName, type))
644 : : {
645 : 5 : parseError("Symbol '" + varName + "' previously declared as a "
646 [ - + ]: 4 : + (type == SYM_VARIABLE ? "variable" : "type")
647 [ + - ]: 6 : + (notes.size() == 0 ? notes : "\n" + notes));
648 : : }
649 : 38139 : break;
650 : :
651 : 1404229 : case CHECK_NONE: break;
652 : :
653 : 0 : default: DebugUnhandled(); // Unhandled(check);
654 : : }
655 : : }
656 : :
657 : 704643 : void ParserState::checkFunctionLike(Term fun)
658 : : {
659 [ + - ][ + + ]: 704643 : if (d_checksEnabled && !isFunctionLike(fun))
[ + - ][ + + ]
[ - - ]
660 : : {
661 : 1 : stringstream ss;
662 : 1 : ss << "Expecting function-like symbol, found '";
663 : 1 : ss << fun;
664 : 1 : ss << "'";
665 : 2 : parseError(ss.str());
666 : 1 : }
667 : 704642 : }
668 : :
669 : 3703669 : void ParserState::addOperator(Kind kind) { d_logicOperators.insert(kind); }
670 : :
671 : 210 : void ParserState::warning(const std::string& msg) { d_psc->warning(msg); }
672 : :
673 : 46 : void ParserState::parseError(const std::string& msg) { d_psc->parseError(msg); }
674 : :
675 : 0 : void ParserState::unexpectedEOF(const std::string& msg)
676 : : {
677 : 0 : d_psc->unexpectedEOF(msg);
678 : 0 : }
679 : :
680 : 308 : void ParserState::attributeNotSupported(const std::string& attr)
681 : : {
682 [ + + ]: 308 : if (d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end())
683 : : {
684 : 32 : stringstream ss;
685 : : ss << "warning: Attribute '" << attr
686 : 32 : << "' not supported (ignoring this and all following uses)";
687 : 32 : warning(ss.str());
688 : 32 : d_attributesWarnedAbout.insert(attr);
689 : 32 : }
690 : 308 : }
691 : :
692 : 0 : size_t ParserState::scopeLevel() const { return d_symman->scopeLevel(); }
693 : :
694 : 308817 : void ParserState::pushScope(bool isUserContext)
695 : : {
696 : 308817 : d_symman->pushScope(isUserContext);
697 : 308817 : }
698 : :
699 : 221 : void ParserState::pushGetValueScope()
700 : : {
701 : 221 : pushScope();
702 : : // We cannot ask for the model domain elements if we are in parse-only mode.
703 : : // Hence, we do nothing here.
704 [ + + ]: 221 : if (d_parseOnly)
705 : : {
706 : 104 : return;
707 : : }
708 : : // we must bind all relevant uninterpreted constants, which coincide with
709 : : // the set of uninterpreted constants that are printed in the definition
710 : : // of a model.
711 : 117 : std::vector<Sort> declareSorts = d_symman->getDeclaredSorts();
712 [ + - ]: 234 : Trace("parser") << "Push get value scope, with " << declareSorts.size()
713 : 117 : << " declared sorts" << std::endl;
714 : : try
715 : : {
716 [ + + ]: 135 : for (const Sort& s : declareSorts)
717 : : {
718 : 22 : std::vector<Term> elements = d_solver->getModelDomainElements(s);
719 [ + - ]: 18 : Trace("parser") << "elements for " << s << ":" << std::endl;
720 [ + + ]: 36 : for (const Term& e : elements)
721 : : {
722 [ + - ]: 18 : Trace("parser") << " " << e.getKind() << " " << e << std::endl;
723 [ + - ]: 18 : if (e.getKind() == Kind::UNINTERPRETED_SORT_VALUE)
724 : : {
725 : 18 : defineVar(e.getUninterpretedSortValue(), e);
726 : : }
727 : : else
728 : : {
729 : 0 : DebugUnhandled()
730 : 0 : << "model domain element is not an uninterpreted sort value: "
731 : : << e;
732 : : }
733 : : }
734 : 18 : }
735 : : }
736 [ - + ]: 4 : catch (const CVC5ApiRecoverableException& e)
737 : : {
738 : : // Let the get-value command report recoverable model-state errors itself
739 : : // instead of turning them into fatal parse errors while binding @U_i names.
740 [ + - ]: 8 : Trace("parser") << "Skipping get-value model bindings: " << e.what()
741 : 4 : << std::endl;
742 : 4 : }
743 : 117 : }
744 : :
745 : 284506 : void ParserState::popScope() { d_symman->popScope(); }
746 : :
747 : 0 : void ParserState::reset() {}
748 : :
749 : 66363 : SymManager* ParserState::getSymbolManager() { return d_symman; }
750 : :
751 : 12 : std::string ParserState::stripQuotes(const std::string& s)
752 : : {
753 [ + - ][ + - ]: 12 : if (s.size() < 2 || s[0] != '\"' || s[s.size() - 1] != '\"')
[ - + ][ - + ]
754 : : {
755 : 0 : parseError("Expected a string delimited by quotes, got invalid string `" + s
756 : 0 : + "`.");
757 : : }
758 : 12 : return s.substr(1, s.size() - 2);
759 : : }
760 : :
761 : 14 : Term ParserState::mkCharConstant(const std::string& s)
762 : : {
763 [ + - ][ - + ]: 28 : if (!(s.find_first_not_of("0123456789abcdefABCDEF", 0) == std::string::npos
[ + + ]
764 [ + + ]: 14 : && s.size() <= 5 && s.size() > 0))
765 : : {
766 : 3 : parseError("Unexpected string for hexadecimal character: `" + s + "'");
767 : : }
768 : 13 : char32_t val = static_cast<char32_t>(std::stoul(s, nullptr, 16));
769 : 26 : return d_tm.mkString(std::u32string(1, val));
770 : : }
771 : :
772 : 752243 : bool stringToUnsigned(const std::string& str,
773 : : uint32_t& result,
774 : : std::ostream* os)
775 : : {
776 [ + - ][ - + ]: 752243 : if (str.empty() || str.find_first_not_of("0123456789") != std::string::npos)
[ - + ]
777 : : {
778 [ - - ]: 0 : if (os != nullptr)
779 : : {
780 : 0 : (*os) << " String is not a numeral.";
781 : : }
782 : 0 : return false;
783 : : }
784 : 752243 : size_t pos = 0;
785 : 752243 : unsigned long long parsed = 0;
786 : : try
787 : : {
788 : 752243 : parsed = std::stoull(str, &pos);
789 : : }
790 [ - - ]: 0 : catch (const std::exception&)
791 : : {
792 [ - - ]: 0 : if (os != nullptr)
793 : : {
794 : 0 : (*os) << " Exception encountered in std::stoull.";
795 : : }
796 : 0 : return false;
797 : 0 : }
798 [ + - ][ + + ]: 752243 : if (pos != str.size() || parsed > std::numeric_limits<uint32_t>::max())
[ + + ]
799 : : {
800 [ + + ]: 2 : if (os != nullptr)
801 : : {
802 : 1 : (*os) << " Numerals must fit into 32-bit unsigned integers.";
803 : : }
804 : 2 : return false;
805 : : }
806 : 752241 : result = static_cast<uint32_t>(parsed);
807 : 752241 : return true;
808 : : }
809 : :
810 : 752242 : uint32_t ParserState::parseStringToUnsigned(const std::string& str)
811 : : {
812 : 752242 : uint32_t result = 0;
813 [ + + ]: 752242 : if (!stringToUnsigned(str, result))
814 : : {
815 : 1 : std::stringstream ss;
816 : 1 : ss << "Failed to parse numeral.";
817 : 1 : stringToUnsigned(str, result, &ss);
818 : 2 : parseError(ss.str());
819 : 1 : }
820 : 752241 : return result;
821 : : }
822 : :
823 : : } // namespace parser
824 : : } // namespace cvc5
|
