1 /********************* */
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andrew Reynolds, Christopher L. Conway
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
12 ** \brief A collection of state for use by parser implementations.
14 ** A collection of state for use by parser implementations.
17 #include "cvc4parser_public.h"
19 #ifndef CVC4__PARSER__PARSER_STATE_H
20 #define CVC4__PARSER__PARSER_STATE_H
27 #include "api/cvc4cpp.h"
28 #include "expr/expr.h"
29 #include "expr/expr_stream.h"
30 #include "expr/kind.h"
31 #include "expr/symbol_table.h"
32 #include "parser/input.h"
33 #include "parser/parse_op.h"
34 #include "parser/parser_exception.h"
35 #include "util/unsafe_interrupt_exception.h"
39 // Forward declarations
44 class ResourceManager
;
49 //for sygus gterm two-pass parsing
50 class CVC4_PUBLIC SygusGTerm
{
63 /** The parsed operator */
65 std::vector
< Expr
> d_let_vars
;
66 unsigned d_gterm_type
;
68 std::vector
< SygusGTerm
> d_children
;
70 unsigned getNumChildren() { return d_children
.size(); }
72 d_children
.push_back( SygusGTerm() );
80 /** Types of checks for the symbols */
81 enum DeclarationCheck
{
82 /** Enforce that the symbol has been declared */
84 /** Enforce that the symbol has not been declared */
86 /** Don't check anything */
88 };/* enum DeclarationCheck */
91 * Returns a string representation of the given object (for
94 inline std::ostream
& operator<<(std::ostream
& out
, DeclarationCheck check
) CVC4_PUBLIC
;
95 inline std::ostream
& operator<<(std::ostream
& out
, DeclarationCheck check
) {
98 return out
<< "CHECK_NONE";
100 return out
<< "CHECK_DECLARED";
101 case CHECK_UNDECLARED
:
102 return out
<< "CHECK_UNDECLARED";
104 return out
<< "DeclarationCheck!UNKNOWN";
109 * Types of symbols. Used to define namespaces.
116 };/* enum SymbolType */
119 * Returns a string representation of the given object (for
122 inline std::ostream
& operator<<(std::ostream
& out
, SymbolType type
) CVC4_PUBLIC
;
123 inline std::ostream
& operator<<(std::ostream
& out
, SymbolType type
) {
126 return out
<< "SYM_VARIABLE";
128 return out
<< "SYM_SORT";
130 return out
<< "SymbolType!UNKNOWN";
135 * This class encapsulates all of the state of a parser, including the
136 * name of the file, line number and column information, and in-scope
139 class CVC4_PUBLIC Parser
{
140 friend class ParserBuilder
;
142 /** The resource manager associated with this expr manager */
143 ResourceManager
* d_resourceManager
;
145 /** The input that we're parsing. */
149 * The declaration scope that is "owned" by this parser. May or
150 * may not be the current declaration scope in use.
152 SymbolTable d_symtabAllocated
;
155 * This current symbol table used by this parser. Initially points
156 * to d_symtabAllocated, but can be changed (making this parser
157 * delegate its definitions and lookups to another parser).
158 * See useDeclarationsFrom().
160 SymbolTable
* d_symtab
;
163 * The level of the assertions in the declaration scope. Things declared
164 * after this level are bindings from e.g. a let, a quantifier, or a
167 size_t d_assertionLevel
;
170 * Whether we're in global declarations mode (all definitions and
171 * declarations are global).
173 bool d_globalDeclarations
;
176 * Maintains a list of reserved symbols at the assertion level that might
177 * not occur in our symbol table. This is necessary to e.g. support the
178 * proper behavior of the :named annotation in SMT-LIBv2 when used under
179 * a let or a quantifier, since inside a let/quant body the declaration
180 * scope is that of the let/quant body, but the defined name should be
181 * reserved at the assertion level.
183 std::set
<std::string
> d_reservedSymbols
;
185 /** How many anonymous functions we've created. */
186 size_t d_anonymousFunctionCount
;
191 /** Are semantic checks enabled during parsing? */
192 bool d_checksEnabled
;
194 /** Are we parsing in strict mode? */
197 /** Are we only parsing? */
201 * Can we include files? (Set to false for security purposes in
202 * e.g. the online version.)
204 bool d_canIncludeFile
;
207 * Whether the logic has been forced with --force-logic.
209 bool d_logicIsForced
;
212 * The logic, if d_logicIsForced == true.
214 std::string d_forcedLogic
;
216 /** The set of operators available in the current logic. */
217 std::set
<Kind
> d_logicOperators
;
219 /** The set of attributes already warned about. */
220 std::set
<std::string
> d_attributesWarnedAbout
;
223 * The current set of unresolved types. We can get by with this NOT
224 * being on the scope, because we can only have one DATATYPE
225 * definition going on at one time. This is a bit hackish; we
226 * depend on mkMutualDatatypeTypes() to check everything and clear
229 std::set
<Type
> d_unresolved
;
232 * "Preemption commands": extra commands implied by subterms that
233 * should be issued before the currently-being-parsed command is
234 * issued. Used to support SMT-LIBv2 ":named" attribute on terms.
236 * Owns the memory of the Commands in the queue.
238 std::list
<Command
*> d_commandQueue
;
240 /** Lookup a symbol in the given namespace (as specified by the type).
241 * Only returns a symbol if it is not overloaded, returns null otherwise.
243 Expr
getSymbol(const std::string
& var_name
, SymbolType type
);
246 /** The API Solver object. */
247 api::Solver
* d_solver
;
250 * Create a parser state.
252 * @attention The parser takes "ownership" of the given
253 * input and will delete it on destruction.
255 * @param the solver API object
256 * @param input the parser input
257 * @param strictMode whether to incorporate strict(er) compliance checks
258 * @param parseOnly whether we are parsing only (and therefore certain checks
259 * need not be performed, like those about unimplemented features, @see
260 * unimplementedFeature())
262 Parser(api::Solver
* solver
,
264 bool strictMode
= false,
265 bool parseOnly
= false);
271 /** Get the associated <code>ExprManager</code>. */
272 ExprManager
* getExprManager() const;
274 /** Get the associated solver. */
275 api::Solver
* getSolver() const;
277 /** Get the associated input. */
278 inline Input
* getInput() const {
282 /** Deletes and replaces the current parser input. */
283 void setInput(Input
* input
) {
286 d_input
->setParser(*this);
291 * Check if we are done -- either the end of input has been reached, or some
292 * error has been encountered.
293 * @return true if parser is done
295 inline bool done() const {
299 /** Sets the done flag */
300 inline void setDone(bool done
= true) {
304 /** Enable semantic checks during parsing. */
305 void enableChecks() { d_checksEnabled
= true; }
307 /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
308 void disableChecks() { d_checksEnabled
= false; }
310 /** Enable strict parsing, according to the language standards. */
311 void enableStrictMode() { d_strictMode
= true; }
313 /** Disable strict parsing. Allows certain syntactic infelicities to
314 pass without comment. */
315 void disableStrictMode() { d_strictMode
= false; }
317 bool strictModeEnabled() { return d_strictMode
; }
319 void allowIncludeFile() { d_canIncludeFile
= true; }
320 void disallowIncludeFile() { d_canIncludeFile
= false; }
321 bool canIncludeFile() const { return d_canIncludeFile
; }
323 /** Expose the functionality from SMT/SMT2 parsers, while making
324 implementation optional by returning false by default. */
325 virtual bool logicIsSet() { return false; }
327 virtual void forceLogic(const std::string
& logic
)
329 assert(!d_logicIsForced
);
330 d_logicIsForced
= true;
331 d_forcedLogic
= logic
;
333 const std::string
& getForcedLogic() const { return d_forcedLogic
; }
334 bool logicIsForced() const { return d_logicIsForced
; }
337 * Gets the variable currently bound to name.
339 * @param name the name of the variable
340 * @return the variable expression
341 * Only returns a variable if its name is not overloaded, returns null otherwise.
343 Expr
getVariable(const std::string
& name
);
346 * Gets the function currently bound to name.
348 * @param name the name of the variable
349 * @return the variable expression
350 * Only returns a function if its name is not overloaded, returns null otherwise.
352 Expr
getFunction(const std::string
& name
);
355 * Returns the expression that name should be interpreted as, based on the current binding.
357 * The symbol name should be declared.
358 * This creates the expression that the string "name" should be interpreted as.
359 * Typically this corresponds to a variable, but it may also correspond to
360 * a nullary constructor or a defined function.
361 * Only returns an expression if its name is not overloaded, returns null otherwise.
363 virtual Expr
getExpressionForName(const std::string
& name
);
366 * Returns the expression that name should be interpreted as, based on the current binding.
368 * This is the same as above but where the name has been type cast to t.
370 virtual Expr
getExpressionForNameAndType(const std::string
& name
, Type t
);
373 * Returns the kind that should be used for applications of expression fun.
374 * This is a generalization of ExprManager::operatorToKind that also
375 * handles variables whose types are "function-like", i.e. where
376 * checkFunctionLike(fun) returns true.
378 * For examples of the latter, this function returns
379 * APPLY_UF if fun has function type,
380 * APPLY_CONSTRUCTOR if fun has constructor type.
382 Kind
getKindForFunction(Expr fun
);
385 * Returns a sort, given a name.
386 * @param sort_name the name to look up
388 Type
getSort(const std::string
& sort_name
);
391 * Returns a (parameterized) sort, given a name and args.
393 Type
getSort(const std::string
& sort_name
,
394 const std::vector
<Type
>& params
);
397 * Returns arity of a (parameterized) sort, given a name and args.
399 size_t getArity(const std::string
& sort_name
);
402 * Checks if a symbol has been declared.
403 * @param name the symbol name
404 * @param type the symbol type
405 * @return true iff the symbol has been declared with the given type
407 bool isDeclared(const std::string
& name
, SymbolType type
= SYM_VARIABLE
);
410 * Checks if the declaration policy we want to enforce holds
411 * for the given symbol.
412 * @param name the symbol to check
413 * @param check the kind of check to perform
414 * @param type the type of the symbol
415 * @param notes notes to add to a parse error (if one is generated)
416 * @throws ParserException if checks are enabled and the check fails
418 void checkDeclaration(const std::string
& name
,
419 DeclarationCheck check
,
420 SymbolType type
= SYM_VARIABLE
,
421 std::string notes
= "");
424 * Reserve a symbol at the assertion level.
426 void reserveSymbolAtAssertionLevel(const std::string
& name
);
429 * Checks whether the given expression is function-like, i.e.
430 * it expects arguments. This is checked by looking at the type
431 * of fun. Examples of function types are function, constructor,
433 * @param fun the expression to check
434 * @throws ParserException if checks are enabled and fun is not
437 void checkFunctionLike(Expr fun
);
440 * Check that <code>kind</code> can accept <code>numArgs</code> arguments.
441 * @param kind the built-in operator to check
442 * @param numArgs the number of actual arguments
443 * @throws ParserException if checks are enabled and the operator
444 * <code>kind</code> cannot be applied to <code>numArgs</code>
447 void checkArity(Kind kind
, unsigned numArgs
);
450 * Check that <code>kind</code> is a legal operator in the current
451 * logic and that it can accept <code>numArgs</code> arguments.
453 * @param kind the built-in operator to check
454 * @param numArgs the number of actual arguments
455 * @throws ParserException if the parser mode is strict and the
456 * operator <code>kind</code> has not been enabled
458 void checkOperator(Kind kind
, unsigned numArgs
);
460 /** Create a new CVC4 variable expression of the given type.
462 * flags specify information about the variable, e.g. whether it is global or defined
463 * (see enum in expr_manager_template.h).
465 * If a symbol with name already exists,
466 * then if doOverload is true, we create overloaded operators.
467 * else if doOverload is false, the existing expression is shadowed by the new expression.
469 Expr
mkVar(const std::string
& name
, const Type
& type
,
470 uint32_t flags
= ExprManager::VAR_FLAG_NONE
,
471 bool doOverload
= false);
474 * Create a set of new CVC4 variable expressions of the given type.
476 * flags specify information about the variable, e.g. whether it is global or defined
477 * (see enum in expr_manager_template.h).
479 * For each name, if a symbol with name already exists,
480 * then if doOverload is true, we create overloaded operators.
481 * else if doOverload is false, the existing expression is shadowed by the new expression.
484 mkVars(const std::vector
<std::string
> names
, const Type
& type
,
485 uint32_t flags
= ExprManager::VAR_FLAG_NONE
,
486 bool doOverload
= false);
489 * Create a new CVC4 bound variable expression of the given type. This binds
490 * the symbol name to that variable in the current scope.
492 Expr
mkBoundVar(const std::string
& name
, const Type
& type
);
494 * Create a new CVC4 bound variable expressions of the given names and types.
495 * Like the method above, this binds these names to those variables in the
498 std::vector
<Expr
> mkBoundVars(
499 std::vector
<std::pair
<std::string
, Type
> >& sortedVarNames
);
502 * Create a set of new CVC4 bound variable expressions of the given type.
504 * flags specify information about the variable, e.g. whether it is global or defined
505 * (see enum in expr_manager_template.h).
507 * For each name, if a symbol with name already exists,
508 * then if doOverload is true, we create overloaded operators.
509 * else if doOverload is false, the existing expression is shadowed by the new expression.
511 std::vector
<Expr
> mkBoundVars(const std::vector
<std::string
> names
, const Type
& type
);
514 * Create a new CVC4 function expression of the given type,
515 * appending a unique index to its name. (That's the ONLY
516 * difference between mkAnonymousFunction() and mkVar()).
518 * flags specify information about the variable, e.g. whether it is global or defined
519 * (see enum in expr_manager_template.h).
521 Expr
mkAnonymousFunction(const std::string
& prefix
, const Type
& type
,
522 uint32_t flags
= ExprManager::VAR_FLAG_NONE
);
524 /** Create a new variable definition (e.g., from a let binding).
525 * levelZero is set if the binding must be done at level 0.
526 * If a symbol with name already exists,
527 * then if doOverload is true, we create overloaded operators.
528 * else if doOverload is false, the existing expression is shadowed by the new expression.
530 void defineVar(const std::string
& name
, const Expr
& val
,
531 bool levelZero
= false, bool doOverload
= false);
534 * Create a new type definition.
536 * @param name The name of the type
537 * @param type The type that should be associated with the name
538 * @param levelZero If true, the type definition is considered global and
539 * cannot be removed by poppoing the user context
541 void defineType(const std::string
& name
,
543 bool levelZero
= false);
546 * Create a new (parameterized) type definition.
548 * @param name The name of the type
549 * @param params The type parameters
550 * @param type The type that should be associated with the name
551 * @param levelZero If true, the type definition is considered global and
552 * cannot be removed by poppoing the user context
554 void defineType(const std::string
& name
,
555 const std::vector
<Type
>& params
,
557 bool levelZero
= false);
559 /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
560 void defineParameterizedType(const std::string
& name
,
561 const std::vector
<Type
>& params
,
565 * Creates a new sort with the given name.
567 SortType
mkSort(const std::string
& name
,
568 uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
571 * Creates a new sort constructor with the given name and arity.
573 SortConstructorType
mkSortConstructor(
574 const std::string
& name
,
576 uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
579 * Creates a new "unresolved type," used only during parsing.
581 SortType
mkUnresolvedType(const std::string
& name
);
584 * Creates a new unresolved (parameterized) type constructor of the given
587 SortConstructorType
mkUnresolvedTypeConstructor(const std::string
& name
,
590 * Creates a new unresolved (parameterized) type constructor given the type
593 SortConstructorType
mkUnresolvedTypeConstructor(const std::string
& name
,
594 const std::vector
<Type
>& params
);
597 * Returns true IFF name is an unresolved type.
599 bool isUnresolvedType(const std::string
& name
);
602 * Create sorts of mutually-recursive datatypes.
603 * For each symbol defined by the datatype, if a symbol with name already exists,
604 * then if doOverload is true, we create overloaded operators.
605 * else if doOverload is false, the existing expression is shadowed by the new expression.
607 * flags specify information about the datatype, e.g. whether it should be
608 * printed out as a definition in models or not
609 * (see enum in expr_manager_template.h).
611 std::vector
<DatatypeType
> mkMutualDatatypeTypes(
612 std::vector
<Datatype
>& datatypes
,
613 bool doOverload
= false,
614 uint32_t flags
= ExprManager::DATATYPE_FLAG_NONE
);
616 /** make flat function type
618 * Returns the "flat" function type corresponding to the function taking
619 * argument types "sorts" and range type "range". A flat function type is
620 * one whose range is not a function. Notice that if sorts is empty and range
621 * is not a function, then this function returns range itself.
623 * If range is a function type, we add its function argument sorts to sorts
624 * and consider its function range as the new range. For each sort S added
625 * to sorts in this process, we add a new bound variable of sort S to
629 * mkFlattenFunctionType( { Int, (-> Real Real) }, (-> Int Bool), {} ):
630 * - returns the the function type (-> Int (-> Real Real) Int Bool)
631 * - updates sorts to { Int, (-> Real Real), Int },
632 * - updates flattenVars to { x }, where x is bound variable of type Int.
634 * Notice that this method performs only one level of flattening, for example,
635 * mkFlattenFunctionType({ Int, (-> Real Real) }, (-> Int (-> Int Bool)), {}):
636 * - returns the the function type (-> Int (-> Real Real) Int (-> Int Bool))
637 * - updates sorts to { Int, (-> Real Real), Int },
638 * - updates flattenVars to { x }, where x is bound variable of type Int.
640 * This method is required so that we do not return functions
641 * that have function return type (these give an unhandled exception
642 * in the ExprManager). For examples of the equivalence between function
643 * definitions in the proposed higher-order extension of the smt2 language,
644 * see page 3 of http://matryoshka.gforge.inria.fr/pubs/PxTP2017.pdf.
646 * The argument flattenVars is needed in the case of defined functions
647 * with function return type. These have implicit arguments, for instance:
648 * (define-fun Q ((x Int)) (-> Int Int) (lambda y (P x)))
649 * is equivalent to the command:
650 * (define-fun Q ((x Int) (z Int)) Int (@ (lambda y (P x)) z))
651 * where @ is (higher-order) application. In this example, z is added to
654 Type
mkFlatFunctionType(std::vector
<Type
>& sorts
,
656 std::vector
<Expr
>& flattenVars
);
658 /** make flat function type
660 * Same as above, but does not take argument flattenVars.
661 * This is used when the arguments of the function are not important (for
662 * instance, if we are only using this type in a declare-fun).
664 Type
mkFlatFunctionType(std::vector
<Type
>& sorts
, Type range
);
666 /** make higher-order apply
668 * This returns the left-associative curried application of (function) expr to
669 * the arguments in args.
671 * For example, mkHoApply( f, { a, b }, 0 ) returns
672 * (HO_APPLY (HO_APPLY f a) b)
674 * If args is non-empty, the expected type of expr is (-> T0 ... Tn T), where
675 * args[i].getType() = Ti
676 * for each i where 0 <= i < args.size(). If expr is not of this
677 * type, the expression returned by this method will not be well typed.
679 Expr
mkHoApply(Expr expr
, std::vector
<Expr
>& args
);
681 /** Apply type ascription
683 * Return term t with a type ascription applied to it. This is used for
684 * syntax like (as t T) in smt2 and t::T in the CVC language. This includes:
685 * - (as emptyset (Set T))
686 * - (as univset (Set T))
689 * - ((as cons T) t1 ... tn) where cons is a parametric datatype constructor.
691 * The term to ascribe t is a term whose kind and children (but not type)
692 * are equivalent to that of the term returned by this method.
694 * Notice that method is not necessarily a cast. In actuality, the above terms
695 * should be understood as symbols indexed by types. However, SMT-LIB does not
696 * permit types as indices, so we must use, e.g. (as emptyset (Set T))
697 * instead of (_ emptyset (Set T)).
699 * @param t The term to ascribe a type
700 * @param s The sort to ascribe
701 * @return Term t with sort s ascribed.
703 api::Term
applyTypeAscription(api::Term t
, api::Sort s
);
706 * Add an operator to the current legal set.
708 * @param kind the built-in operator to add
710 void addOperator(Kind kind
);
713 * Preempt the next returned command with other ones; used to
714 * support the :named attribute in SMT-LIBv2, which implicitly
715 * inserts a new command before the current one. Also used in TPTP
716 * because function and predicate symbols are implicitly declared.
718 void preemptCommand(Command
* cmd
);
720 /** Is the symbol bound to a boolean variable? */
721 bool isBoolean(const std::string
& name
);
723 /** Is fun a function (or function-like thing)?
724 * Currently this means its type is either a function, constructor, tester, or selector.
726 bool isFunctionLike(Expr fun
);
728 /** Is the symbol bound to a predicate? */
729 bool isPredicate(const std::string
& name
);
731 /** Parse and return the next command. */
732 Command
* nextCommand();
734 /** Parse and return the next expression. */
735 api::Term
nextExpression();
737 /** Issue a warning to the user. */
738 void warning(const std::string
& msg
) { d_input
->warning(msg
); }
739 /** Issue a warning to the user, but only once per attribute. */
740 void attributeNotSupported(const std::string
& attr
);
742 /** Raise a parse error with the given message. */
743 inline void parseError(const std::string
& msg
) { d_input
->parseError(msg
); }
744 /** Unexpectedly encountered an EOF */
745 inline void unexpectedEOF(const std::string
& msg
)
747 d_input
->parseError(msg
, true);
751 * If we are parsing only, don't raise an exception; if we are not,
752 * raise a parse error with the given message. There is no actual
753 * parse error, everything is as expected, but we cannot create the
754 * Expr, Type, or other requested thing yet due to internal
755 * limitations. Even though it's not a parse error, we throw a
756 * parse error so that the input line and column information is
759 * Think quantifiers. We don't have a TheoryQuantifiers yet, so we
760 * have no kind::FORALL or kind::EXISTS. But we might want to
761 * support parsing quantifiers (just not doing anything with them).
762 * So this mechanism gives you a way to do it with --parse-only.
764 inline void unimplementedFeature(const std::string
& msg
)
767 parseError("Unimplemented feature: " + msg
);
772 * Gets the current declaration level.
774 inline size_t scopeLevel() const { return d_symtab
->getLevel(); }
777 * Pushes a scope. All subsequent symbol declarations made are only valid in
778 * this scope, i.e. they are deleted on the next call to popScope.
780 * The argument bindingLevel is true, the assertion level is set to the
781 * current scope level. This determines which scope assertions are declared
784 inline void pushScope(bool bindingLevel
= false) {
785 d_symtab
->pushScope();
787 d_assertionLevel
= scopeLevel();
791 inline void popScope() {
792 d_symtab
->popScope();
793 if(scopeLevel() < d_assertionLevel
) {
794 d_assertionLevel
= scopeLevel();
795 d_reservedSymbols
.clear();
799 virtual void reset() {
803 void setGlobalDeclarations(bool flag
) {
804 d_globalDeclarations
= flag
;
808 * Set the current symbol table used by this parser.
809 * From now on, this parser will perform its definitions and
810 * lookups in the declaration scope of the "parser" argument
811 * (but doesn't re-delegate if the other parser's declaration scope
812 * changes later). A NULL argument restores this parser's
813 * "primordial" declaration scope assigned at its creation. Calling
814 * p->useDeclarationsFrom(p) is a no-op.
816 * This feature is useful when e.g. reading out-of-band expression data:
817 * 1. Parsing --replay log files produced with --replay-log.
818 * 2. Perhaps a multi-query benchmark file is being single-stepped
819 * with intervening queries on stdin that must reference the same
820 * declaration scope(s).
822 * However, the feature must be used carefully. Pushes and pops
823 * should be performed with the correct current declaration scope.
824 * Care must be taken to match up declaration scopes, of course;
825 * If variables in the deferred-to parser go out of scope, the
826 * secondary parser will give errors that they are undeclared.
827 * Also, an outer-scope variable shadowed by an inner-scope one of
828 * the same name may be temporarily inaccessible.
830 * In short, caveat emptor.
832 inline void useDeclarationsFrom(Parser
* parser
) {
834 d_symtab
= &d_symtabAllocated
;
836 d_symtab
= parser
->d_symtab
;
840 inline void useDeclarationsFrom(SymbolTable
* symtab
) {
844 inline SymbolTable
* getSymbolTable() const {
849 * An expression stream interface for a parser. This stream simply
850 * pulls expressions from the given Parser object.
852 * Here, the ExprStream base class allows a Parser (from the parser
853 * library) and core components of CVC4 (in the core library) to
854 * communicate without polluting the public interface or having them
855 * reach into private (undocumented) interfaces.
857 class ExprStream
: public CVC4::ExprStream
{
860 ExprStream(Parser
* parser
) : d_parser(parser
) {}
861 ~ExprStream() { delete d_parser
; }
862 Expr
nextExpr() override
{ return d_parser
->nextExpression().getExpr(); }
863 };/* class Parser::ExprStream */
865 //------------------------ operator overloading
866 /** is this function overloaded? */
867 bool isOverloadedFunction(Expr fun
) {
868 return d_symtab
->isOverloadedFunction(fun
);
871 /** Get overloaded constant for type.
872 * If possible, it returns a defined symbol with name
873 * that has type t. Otherwise returns null expression.
875 Expr
getOverloadedConstantForType(const std::string
& name
, Type t
) {
876 return d_symtab
->getOverloadedConstantForType(name
, t
);
880 * If possible, returns a defined function for a name
881 * and a vector of expected argument types. Otherwise returns
884 Expr
getOverloadedFunctionForTypes(const std::string
& name
, std::vector
< Type
>& argTypes
) {
885 return d_symtab
->getOverloadedFunctionForTypes(name
, argTypes
);
887 //------------------------ end operator overloading
890 }/* CVC4::parser namespace */
891 }/* CVC4 namespace */
893 #endif /* CVC4__PARSER__PARSER_STATE_H */