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 : : * A collection of state for use by parser implementations.
11 : : */
12 : :
13 : : #include "cvc5parser_public.h"
14 : :
15 : : #ifndef CVC5__PARSER__PARSER_STATE_H
16 : : #define CVC5__PARSER__PARSER_STATE_H
17 : :
18 : : #include <cvc5/cvc5.h>
19 : : #include <cvc5/cvc5_export.h>
20 : : #include <cvc5/cvc5_parser.h>
21 : :
22 : : #include <list>
23 : : #include <memory>
24 : : #include <string>
25 : :
26 : : #include "parser/parse_op.h"
27 : : #include "parser/parser_utils.h"
28 : : #include "parser/sym_manager.h"
29 : : #include "parser/symbol_table.h"
30 : :
31 : : namespace cvc5 {
32 : : namespace parser {
33 : :
34 : : class Command;
35 : :
36 : : /**
37 : : * The parsing mode, defines how strict we are on accepting non-conforming
38 : : * inputs.
39 : : */
40 : : enum class ParsingMode
41 : : {
42 : : DEFAULT, // reasonably strict
43 : : STRICT, // more strict
44 : : LENIENT, // less strict
45 : : };
46 : :
47 : : /**
48 : : * Callback from the parser state to the parser, for command preemption
49 : : * and error handling.
50 : : */
51 : : class ParserStateCallback
52 : : {
53 : : public:
54 : 24389 : ParserStateCallback() {}
55 : 24368 : virtual ~ParserStateCallback() {}
56 : : /** Issue a warning to the user. */
57 : : virtual void warning(const std::string& msg) = 0;
58 : : /** Raise a parse error with the given message. */
59 : : virtual void parseError(const std::string& msg) = 0;
60 : : /** Unexpectedly encountered an EOF */
61 : : virtual void unexpectedEOF(const std::string& msg) = 0;
62 : : };
63 : :
64 : : /**
65 : : * This class encapsulates all of the state of a parser, including the
66 : : * name of the file, line number and column information, and in-scope
67 : : * declarations.
68 : : */
69 : : class CVC5_EXPORT ParserState
70 : : {
71 : : public:
72 : : /**
73 : : * Create a parser state.
74 : : *
75 : : * @attention The parser takes "ownership" of the given
76 : : * input and will delete it on destruction.
77 : : *
78 : : * @param psc The callback for implementing parser-specific methods.
79 : : * @param solver The solver API object.
80 : : * @param symm The symbol manager.
81 : : * @param input The parser input.
82 : : * @param parsingMode The parsing mode.
83 : : */
84 : : ParserState(ParserStateCallback* psc,
85 : : Solver* solver,
86 : : SymManager* sm,
87 : : ParsingMode parsingMode = ParsingMode::DEFAULT);
88 : :
89 : : virtual ~ParserState();
90 : :
91 : : /** Get the associated solver. */
92 : : Solver* getSolver() const;
93 : :
94 : : /** Enable semantic checks during parsing. */
95 : : void enableChecks() { d_checksEnabled = true; }
96 : :
97 : : /** Disable semantic checks during parsing. Disabling checks may lead to
98 : : * crashes on bad inputs. */
99 : : void disableChecks() { d_checksEnabled = false; }
100 : :
101 : : /** Enable strict parsing, according to the language standards. */
102 : : void enableStrictMode() { d_parsingMode = ParsingMode::STRICT; }
103 : :
104 : : /** Disable strict parsing. Allows certain syntactic infelicities to
105 : : pass without comment. */
106 : : void disableStrictMode() { d_parsingMode = ParsingMode::DEFAULT; }
107 : :
108 : 10576001 : bool strictModeEnabled() { return d_parsingMode == ParsingMode::STRICT; }
109 : :
110 : 365393 : bool lenientModeEnabled() { return d_parsingMode == ParsingMode::LENIENT; }
111 : :
112 : : const std::string& getForcedLogic() const;
113 : : bool logicIsForced() const;
114 : :
115 : : /** Expose the functionality from SMT/SMT2 parsers, while making
116 : : implementation optional by returning false by default. */
117 : 0 : virtual bool logicIsSet() { return false; }
118 : :
119 : : /**
120 : : * Gets the variable currently bound to name.
121 : : *
122 : : * @param name the name of the variable
123 : : * @return the variable expression
124 : : * Only returns a variable if its name is not overloaded, returns null
125 : : * otherwise.
126 : : */
127 : : Term getVariable(const std::string& name);
128 : :
129 : : /**
130 : : * Returns the expression that name should be interpreted as, based on the
131 : : * current binding.
132 : : *
133 : : * This is the same as above but where the name has been type cast to t.
134 : : */
135 : : virtual Term getExpressionForNameAndType(const std::string& name, Sort t);
136 : :
137 : : /**
138 : : * If this method returns true, then name is updated with the tester name
139 : : * for constructor cons.
140 : : *
141 : : * In detail, notice that (user-defined) datatypes associate a unary predicate
142 : : * for each constructor, called its "tester". This symbol is automatically
143 : : * defined when a datatype is defined. The tester name for a constructor
144 : : * (e.g. "cons") depends on the language:
145 : : * - In smt versions < 2.6, the (non-standard) syntax is "is-cons",
146 : : * - In smt versions >= 2.6, the indexed symbol "(_ is cons)" is used. Thus,
147 : : * no tester symbol is necessary, since "is" is a builtin symbol. We still use
148 : : * the above syntax if strict mode is disabled.
149 : : * - In cvc, the syntax for testers is "is_cons".
150 : : */
151 : : virtual bool getTesterName(Term cons, std::string& name);
152 : :
153 : : /**
154 : : * Returns the kind that should be used for applications of expression fun.
155 : : * This is a generalization of ExprManager::operatorToKind that also
156 : : * handles variables whose types are "function-like", i.e. where
157 : : * checkFunctionLike(fun) returns true.
158 : : *
159 : : * For examples of the latter, this function returns
160 : : * APPLY_UF if fun has function type,
161 : : * APPLY_CONSTRUCTOR if fun has constructor type.
162 : : */
163 : : Kind getKindForFunction(Term fun);
164 : :
165 : : /**
166 : : * Returns a sort, given a name.
167 : : * @param sort_name the name to look up
168 : : */
169 : : Sort getSort(const std::string& sort_name);
170 : :
171 : : /**
172 : : * Returns a (parameterized) sort, given a name and args.
173 : : */
174 : : virtual Sort getParametricSort(const std::string& sort_name,
175 : : const std::vector<Sort>& params);
176 : :
177 : : /**
178 : : * Checks if a symbol has been declared.
179 : : * @param name the symbol name
180 : : * @param type the symbol type
181 : : * @return true iff the symbol has been declared with the given type
182 : : */
183 : : bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
184 : :
185 : : /**
186 : : * Checks if the declaration policy we want to enforce holds
187 : : * for the given symbol.
188 : : * @param name the symbol to check
189 : : * @param check the kind of check to perform
190 : : * @param type the type of the symbol
191 : : * @param notes notes to add to a parse error (if one is generated)
192 : : * @throws ParserException if checks are enabled and the check fails
193 : : */
194 : : void checkDeclaration(const std::string& name,
195 : : DeclarationCheck check,
196 : : SymbolType type = SYM_VARIABLE,
197 : : std::string notes = "");
198 : :
199 : : /**
200 : : * Checks whether the given expression is function-like, i.e.
201 : : * it expects arguments. This is checked by looking at the type
202 : : * of fun. Examples of function types are function, constructor,
203 : : * selector, tester.
204 : : * @param fun the expression to check
205 : : * @throws ParserException if checks are enabled and fun is not
206 : : * a function
207 : : */
208 : : void checkFunctionLike(Term fun);
209 : :
210 : : /** Create a new cvc5 variable expression of the given type.
211 : : *
212 : : * If a symbol with name already exists,
213 : : * then if doOverload is true, we create overloaded operators.
214 : : * else if doOverload is false, the existing expression is shadowed by the
215 : : * new expression.
216 : : */
217 : : Term bindVar(const std::string& name,
218 : : const Sort& type,
219 : : bool doOverload = false);
220 : :
221 : : /**
222 : : * Create a (possibly) new cvc5 bound variable expression of the given type.
223 : : * This binds the symbol name to that variable in the current scope.
224 : : *
225 : : * @param name The name of the variable
226 : : * @param type The type of the variable
227 : : * @param fresh If true, the variable is always new. If false, we lookup the
228 : : * variable in a cache and return a.
229 : : */
230 : : Term bindBoundVar(const std::string& name,
231 : : const Sort& type,
232 : : bool fresh = true);
233 : : /**
234 : : * Create new cvc5 bound variable expressions of the given names and types.
235 : : * Like the method above, this binds these names to those variables in the
236 : : * current scope.
237 : : *
238 : : * @param sortedVarNames The names and types of the variables.
239 : : * @param fresh If true, the variables are always new. If false, we lookup
240 : : * each variable in the cache.
241 : : */
242 : : std::vector<Term> bindBoundVars(
243 : : std::vector<std::pair<std::string, Sort>>& sortedVarNames,
244 : : bool fresh = true);
245 : : /**
246 : : * Same as above, but ensure that the shadowing is compatible with current
247 : : * let bindings.
248 : : *
249 : : * @param sortedVarNames The names and types of the variables.
250 : : * @param letBinders The current let binders in scope that may contain
251 : : * the shadowed variables we bind in this call.
252 : : * @param fresh If true, the variables are always new. If false, we lookup
253 : : * each variable in the cache.
254 : : */
255 : : std::vector<Term> bindBoundVarsCtx(
256 : : std::vector<std::pair<std::string, Sort>>& sortedVarNames,
257 : : std::vector<std::vector<std::pair<std::string, Term>>>& letBinders,
258 : : bool fresh = true);
259 : :
260 : : /**
261 : : * Create a set of new cvc5 bound variable expressions of the given type.
262 : : *
263 : : * For each name, if a symbol with name already exists,
264 : : * then if doOverload is true, we create overloaded operators.
265 : : * else if doOverload is false, the existing expression is shadowed by the
266 : : * new expression.
267 : : */
268 : : std::vector<Term> bindBoundVars(const std::vector<std::string> names,
269 : : const Sort& type);
270 : :
271 : : /** Create a new variable definition (e.g., from a let binding).
272 : : * If a symbol with name already exists,
273 : : * then if doOverload is true, we create overloaded operators.
274 : : * else if doOverload is false, the existing expression is shadowed by the
275 : : * new expression.
276 : : */
277 : : void defineVar(const std::string& name,
278 : : const Term& val,
279 : : bool doOverload = false);
280 : :
281 : : /**
282 : : * Create a new type definition.
283 : : *
284 : : * @param name The name of the type
285 : : * @param type The type that should be associated with the name
286 : : * @param isUser does this correspond to a user sort
287 : : */
288 : : void defineType(const std::string& name, const Sort& type, bool isUser);
289 : :
290 : : /**
291 : : * Create a new (parameterized) type definition.
292 : : *
293 : : * @param name The name of the type
294 : : * @param params The type parameters
295 : : * @param type The type that should be associated with the name
296 : : * @param isUser does this correspond to a user sort
297 : : */
298 : : void defineType(const std::string& name,
299 : : const std::vector<Sort>& params,
300 : : const Sort& type,
301 : : bool isUser);
302 : : /**
303 : : * Creates a new sort with the given name.
304 : : */
305 : : Sort mkSort(const std::string& name);
306 : :
307 : : /**
308 : : * Creates a new sort constructor with the given name and arity.
309 : : */
310 : : Sort mkSortConstructor(const std::string& name, size_t arity);
311 : :
312 : : /**
313 : : * Creates a new "unresolved type," used only during parsing.
314 : : */
315 : : Sort mkUnresolvedType(const std::string& name);
316 : :
317 : : /**
318 : : * Creates a new unresolved (parameterized) type constructor of the given
319 : : * arity.
320 : : */
321 : : Sort mkUnresolvedTypeConstructor(const std::string& name, size_t arity);
322 : : /**
323 : : * Creates a new unresolved (parameterized) type constructor given the type
324 : : * parameters.
325 : : */
326 : : Sort mkUnresolvedTypeConstructor(const std::string& name,
327 : : const std::vector<Sort>& params);
328 : :
329 : : /**
330 : : * Creates a new unresolved (parameterized) type constructor of the given
331 : : * arity. Calls either mkUnresolvedType or mkUnresolvedTypeConstructor
332 : : * depending on the arity.
333 : : */
334 : : Sort mkUnresolvedType(const std::string& name, size_t arity);
335 : :
336 : : /**
337 : : * Creates sorts of a list of mutually-recursive datatype declarations.
338 : : *
339 : : * For each symbol defined by the datatype, it checks whether the binding
340 : : * will succeed. However, it does not actually implement the binding yet,
341 : : * as this is only done when the command is executed.
342 : : */
343 : : std::vector<Sort> mkMutualDatatypeTypes(std::vector<DatatypeDecl>& datatypes);
344 : :
345 : : /** flatten function type
346 : : *
347 : : * Computes the "flat" function type corresponding to the function taking
348 : : * argument types "sorts" and range type "range". A flat function type is
349 : : * one whose range is not a function. Notice that if sorts is empty and range
350 : : * is not a function, then this function returns range itself.
351 : : *
352 : : * If range is a function type, we add its function argument sorts to sorts
353 : : * and consider its function range as the new range. For each sort S added
354 : : * to sorts in this process, we add a new bound variable of sort S to
355 : : * flattenVars.
356 : : *
357 : : * For example:
358 : : * flattenFunctionType( { Int, (-> Real Real) }, (-> Int Bool), {} ):
359 : : * - returns the the function type Bool
360 : : * - updates sorts to { Int, (-> Real Real), Int },
361 : : * - updates flattenVars to { x }, where x is bound variable of type Int.
362 : : *
363 : : * Notice that this method performs only one level of flattening, for example,
364 : : * mkFlattenFunctionType({ Int, (-> Real Real) }, (-> Int (-> Int Bool)), {}):
365 : : * - returns the the function type (-> Int Bool)
366 : : * - updates sorts to { Int, (-> Real Real), Int },
367 : : * - updates flattenVars to { x }, where x is bound variable of type Int.
368 : : *
369 : : * This method is required so that we do not return functions
370 : : * that have function return type (these give an unhandled exception
371 : : * in the ExprManager). For examples of the equivalence between function
372 : : * definitions in the proposed higher-order extension of the smt2 language,
373 : : * see page 3 of http://matryoshka.gforge.inria.fr/pubs/PxTP2017.pdf.
374 : : *
375 : : * The argument flattenVars is needed in the case of defined functions
376 : : * with function return type. These have implicit arguments, for instance:
377 : : * (define-fun Q ((x Int)) (-> Int Int) (lambda y (P x)))
378 : : * is equivalent to the command:
379 : : * (define-fun Q ((x Int) (z Int)) Int (@ (lambda y (P x)) z))
380 : : * where @ is (higher-order) application. In this example, z is added to
381 : : * flattenVars.
382 : : */
383 : : Sort flattenFunctionType(std::vector<Sort>& sorts,
384 : : Sort range,
385 : : std::vector<Term>& flattenVars);
386 : :
387 : : /** flatten function type
388 : : *
389 : : * Same as above, but does not take argument flattenVars.
390 : : * This is used when the arguments of the function are not important (for
391 : : * instance, if we are only using this type in a declare-fun). Also, in
392 : : * contrast to the above method, we flatten arbitrary nestings of function
393 : : * symbols in range.
394 : : */
395 : : Sort flattenFunctionType(std::vector<Sort>& sorts, Sort range);
396 : : /**
397 : : * Calls the above method and returns the (possibly) function type for
398 : : * the return range and updated vector sorts.
399 : : */
400 : : Sort mkFlatFunctionType(std::vector<Sort>& sorts, Sort range);
401 : :
402 : : /** make higher-order apply
403 : : *
404 : : * This returns the left-associative curried application of (function) expr to
405 : : * the arguments in args.
406 : : *
407 : : * For example, mkHoApply( f, { a, b }, 0 ) returns
408 : : * (HO_APPLY (HO_APPLY f a) b)
409 : : *
410 : : * If args is non-empty, the expected type of expr is (-> T0 ... Tn T), where
411 : : * args[i].getType() = Ti
412 : : * for each i where 0 <= i < args.size(). If expr is not of this
413 : : * type, the expression returned by this method will not be well typed.
414 : : */
415 : : Term mkHoApply(Term expr, const std::vector<Term>& args);
416 : :
417 : : /** Apply type ascription
418 : : *
419 : : * Return term t with a type ascription applied to it. This is used for
420 : : * syntax like (as t T) in smt2 and t::T in the CVC language. This includes:
421 : : * - (as set.empty (Set T))
422 : : * - (as emptybag (Bag T))
423 : : * - (as univset (Set T))
424 : : * - (as sep.nil T)
425 : : * - (cons T)
426 : : * - ((as cons T) t1 ... tn) where cons is a parametric datatype constructor.
427 : : *
428 : : * The term to ascribe t is a term whose kind and children (but not type)
429 : : * are equivalent to that of the term returned by this method.
430 : : *
431 : : * Notice that method is not necessarily a cast. In actuality, the above terms
432 : : * should be understood as symbols indexed by types. However, SMT-LIB does not
433 : : * permit types as indices, so we must use, e.g. (as set.empty (Set T))
434 : : * instead of (_ set.empty (Set T)).
435 : : *
436 : : * @param t The term to ascribe a type
437 : : * @param s The sort to ascribe
438 : : * @return Term t with sort s ascribed.
439 : : */
440 : : Term applyTypeAscription(Term t, Sort s);
441 : :
442 : : /**
443 : : * Add an operator to the current legal set.
444 : : *
445 : : * @param kind the built-in operator to add
446 : : */
447 : : void addOperator(Kind kind);
448 : :
449 : : /** Is fun a function (or function-like thing)?
450 : : * Currently this means its type is either a function, constructor, tester, or
451 : : * selector.
452 : : */
453 : : bool isFunctionLike(Term fun);
454 : :
455 : : //-------------------- callbacks to parser
456 : : /** Issue a warning to the user. */
457 : : void warning(const std::string& msg);
458 : : /** Raise a parse error with the given message. */
459 : : void parseError(const std::string& msg);
460 : : /** Unexpectedly encountered an EOF */
461 : : void unexpectedEOF(const std::string& msg);
462 : : //-------------------- end callbacks to parser
463 : : /** Issue a warning to the user, but only once per attribute. */
464 : : void attributeNotSupported(const std::string& attr);
465 : :
466 : : /**
467 : : * If we are parsing only, don't raise an exception; if we are not,
468 : : * raise a parse error with the given message. There is no actual
469 : : * parse error, everything is as expected, but we cannot create the
470 : : * Expr, Type, or other requested thing yet due to internal
471 : : * limitations. Even though it's not a parse error, we throw a
472 : : * parse error so that the input line and column information is
473 : : * available.
474 : : *
475 : : * Think quantifiers. We don't have a TheoryQuantifiers yet, so we
476 : : * have no kind::FORALL or kind::EXISTS. But we might want to
477 : : * support parsing quantifiers (just not doing anything with them).
478 : : * So this mechanism gives you a way to do it with --parse-only.
479 : : */
480 : : void unimplementedFeature(const std::string& msg)
481 : : {
482 : : parseError("Unimplemented feature: " + msg);
483 : : }
484 : :
485 : : /**
486 : : * Gets the current declaration level.
487 : : */
488 : : size_t scopeLevel() const;
489 : :
490 : : /**
491 : : * Pushes a scope. All subsequent symbol declarations made are only valid in
492 : : * this scope, i.e. they are deleted on the next call to popScope.
493 : : *
494 : : * The argument isUserContext is true, when we are pushing a user context
495 : : * e.g. via the smt2 command (push n). This may also include one initial
496 : : * pushScope when the parser is initialized. User-context pushes and pops
497 : : * have an impact on both expression names and the symbol table, whereas
498 : : * other pushes and pops only have an impact on the symbol table.
499 : : */
500 : : void pushScope(bool isUserContext = false);
501 : :
502 : : /** Push scope for get-value
503 : : *
504 : : * This pushes a scope by a call to pushScope that binds all relevant bindings
505 : : * required for parsing the SMT-LIB command `get-value`. This includes
506 : : * all uninterpreted constant values in user-defined uninterpreted sorts.
507 : : */
508 : : void pushGetValueScope();
509 : :
510 : : void popScope();
511 : :
512 : : virtual void reset();
513 : :
514 : : /** Return the symbol manager used by this parser. */
515 : : SymManager* getSymbolManager();
516 : :
517 : : //------------------------ operator overloading
518 : : /** is this function overloaded? */
519 : : bool isOverloadedFunction(Term fun)
520 : : {
521 : : return d_symtab->isOverloadedFunction(fun);
522 : : }
523 : :
524 : : /** Get overloaded constant for type.
525 : : * If possible, it returns a defined symbol with name
526 : : * that has type t. Otherwise returns null expression.
527 : : */
528 : 6 : Term getOverloadedConstantForType(const std::string& name, Sort t)
529 : : {
530 : 6 : return d_symtab->getOverloadedConstantForType(name, t);
531 : : }
532 : :
533 : : /**
534 : : * If possible, returns a defined function for a name
535 : : * and a vector of expected argument types. Otherwise returns
536 : : * null expression.
537 : : */
538 : 836 : Term getOverloadedFunctionForTypes(const std::string& name,
539 : : std::vector<Sort>& argTypes)
540 : : {
541 : 836 : return d_symtab->getOverloadedFunctionForTypes(name, argTypes);
542 : : }
543 : : //------------------------ end operator overloading
544 : :
545 : : /**
546 : : * Make string constant from a single character in hex representation
547 : : *
548 : : * This makes the string constant based on the character from the strings,
549 : : * represented as a hexadecimal code point.
550 : : */
551 : : Term mkCharConstant(const std::string& s);
552 : :
553 : : /**
554 : : * Strip quotes off a string, or return a parse error otherwise.
555 : : */
556 : : std::string stripQuotes(const std::string& s);
557 : :
558 : : /**
559 : : * Parse a non-negative numeral that must fit in uint32_t.
560 : : * Otherwise an exception is thrown.
561 : : * @param str The string to parse.
562 : : * @return the corresponding uint32_t if successful.
563 : : */
564 : : uint32_t parseStringToUnsigned(const std::string& str);
565 : :
566 : : protected:
567 : : /** The API Solver object. */
568 : : Solver* d_solver;
569 : : /** The term manager associated to the associated solver instance. */
570 : : TermManager& d_tm;
571 : :
572 : : private:
573 : : /** The callback */
574 : : ParserStateCallback* d_psc;
575 : : /**
576 : : * Reference to the symbol manager, which manages the symbol table used by
577 : : * this parser.
578 : : */
579 : : SymManager* d_symman;
580 : :
581 : : /**
582 : : * This current symbol table used by this parser, from symbol manager.
583 : : */
584 : : internal::parser::SymbolTable* d_symtab;
585 : :
586 : : /** Are semantic checks enabled during parsing? */
587 : : bool d_checksEnabled;
588 : :
589 : : /** Are we parsing in strict mode? */
590 : : ParsingMode d_parsingMode;
591 : :
592 : : /** Are we in parse-only mode? */
593 : : bool d_parseOnly;
594 : :
595 : : /** The set of operators available in the current logic. */
596 : : std::set<Kind> d_logicOperators;
597 : :
598 : : /** The set of attributes already warned about. */
599 : : std::set<std::string> d_attributesWarnedAbout;
600 : :
601 : : /**
602 : : * "Preemption commands": extra commands implied by subterms that
603 : : * should be issued before the currently-being-parsed command is
604 : : * issued. Used to support SMT-LIBv2 ":named" attribute on terms.
605 : : *
606 : : * Owns the memory of the Commands in the queue.
607 : : */
608 : : std::list<Command*> d_commandQueue;
609 : : /** A cache of variables, for implementing bindBoundVar when fresh is false */
610 : : std::map<std::pair<std::string, Sort>, Term> d_varCache;
611 : : }; /* class Parser */
612 : :
613 : : /**
614 : : * Parse a non-negative numeral that must fit in uint32_t.
615 : : * @param str The string to parse.
616 : : * @param result The result of parsing str to a uint32_t if successful.
617 : : * @param os If provided, errors are written on this stream.
618 : : * @return true if the parsing was successful.
619 : : */
620 : : bool stringToUnsigned(const std::string& str,
621 : : uint32_t& result,
622 : : std::ostream* os = nullptr);
623 : :
624 : : } // namespace parser
625 : : } // namespace cvc5
626 : :
627 : : #endif /* CVC5__PARSER__PARSER_STATE_H */
|
