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