1 /********************* */
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Morgan Deters, Christopher L. Conway
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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/kind.h"
30 #include "expr/symbol_table.h"
31 #include "parser/input.h"
32 #include "parser/parse_op.h"
33 #include "parser/parser_exception.h"
34 #include "util/unsafe_interrupt_exception.h"
38 // Forward declarations
43 class ResourceManager
;
45 //for sygus gterm two-pass parsing
46 class CVC4_PUBLIC SygusGTerm
{
59 /** The parsed operator */
61 std::vector
<api::Term
> d_let_vars
;
62 unsigned d_gterm_type
;
64 std::vector
< SygusGTerm
> d_children
;
66 unsigned getNumChildren() { return d_children
.size(); }
68 d_children
.push_back( SygusGTerm() );
76 /** Types of checks for the symbols */
77 enum DeclarationCheck
{
78 /** Enforce that the symbol has been declared */
80 /** Enforce that the symbol has not been declared */
82 /** Don't check anything */
84 };/* enum DeclarationCheck */
87 * Returns a string representation of the given object (for
90 inline std::ostream
& operator<<(std::ostream
& out
, DeclarationCheck check
) CVC4_PUBLIC
;
91 inline std::ostream
& operator<<(std::ostream
& out
, DeclarationCheck check
) {
94 return out
<< "CHECK_NONE";
96 return out
<< "CHECK_DECLARED";
97 case CHECK_UNDECLARED
:
98 return out
<< "CHECK_UNDECLARED";
100 return out
<< "DeclarationCheck!UNKNOWN";
105 * Types of symbols. Used to define namespaces.
112 };/* enum SymbolType */
115 * Returns a string representation of the given object (for
118 inline std::ostream
& operator<<(std::ostream
& out
, SymbolType type
) CVC4_PUBLIC
;
119 inline std::ostream
& operator<<(std::ostream
& out
, SymbolType type
) {
122 return out
<< "SYM_VARIABLE";
124 return out
<< "SYM_SORT";
126 return out
<< "SymbolType!UNKNOWN";
131 * This class encapsulates all of the state of a parser, including the
132 * name of the file, line number and column information, and in-scope
135 class CVC4_PUBLIC Parser
{
136 friend class ParserBuilder
;
139 /** The input that we're parsing. */
143 * The declaration scope that is "owned" by this parser. May or
144 * may not be the current declaration scope in use.
146 SymbolTable d_symtabAllocated
;
149 * This current symbol table used by this parser. Initially points
150 * to d_symtabAllocated, but can be changed (making this parser
151 * delegate its definitions and lookups to another parser).
152 * See useDeclarationsFrom().
154 SymbolTable
* d_symtab
;
157 * The level of the assertions in the declaration scope. Things declared
158 * after this level are bindings from e.g. a let, a quantifier, or a
161 size_t d_assertionLevel
;
164 * Whether we're in global declarations mode (all definitions and
165 * declarations are global).
167 bool d_globalDeclarations
;
170 * Maintains a list of reserved symbols at the assertion level that might
171 * not occur in our symbol table. This is necessary to e.g. support the
172 * proper behavior of the :named annotation in SMT-LIBv2 when used under
173 * a let or a quantifier, since inside a let/quant body the declaration
174 * scope is that of the let/quant body, but the defined name should be
175 * reserved at the assertion level.
177 std::set
<std::string
> d_reservedSymbols
;
179 /** How many anonymous functions we've created. */
180 size_t d_anonymousFunctionCount
;
185 /** Are semantic checks enabled during parsing? */
186 bool d_checksEnabled
;
188 /** Are we parsing in strict mode? */
191 /** Are we only parsing? */
195 * Can we include files? (Set to false for security purposes in
196 * e.g. the online version.)
198 bool d_canIncludeFile
;
201 * Whether the logic has been forced with --force-logic.
203 bool d_logicIsForced
;
206 * The logic, if d_logicIsForced == true.
208 std::string d_forcedLogic
;
210 /** The set of operators available in the current logic. */
211 std::set
<api::Kind
> d_logicOperators
;
213 /** The set of attributes already warned about. */
214 std::set
<std::string
> d_attributesWarnedAbout
;
217 * The current set of unresolved types. We can get by with this NOT
218 * being on the scope, because we can only have one DATATYPE
219 * definition going on at one time. This is a bit hackish; we
220 * depend on mkMutualDatatypeTypes() to check everything and clear
223 std::set
<api::Sort
> d_unresolved
;
226 * "Preemption commands": extra commands implied by subterms that
227 * should be issued before the currently-being-parsed command is
228 * issued. Used to support SMT-LIBv2 ":named" attribute on terms.
230 * Owns the memory of the Commands in the queue.
232 std::list
<Command
*> d_commandQueue
;
234 /** Lookup a symbol in the given namespace (as specified by the type).
235 * Only returns a symbol if it is not overloaded, returns null otherwise.
237 api::Term
getSymbol(const std::string
& var_name
, SymbolType type
);
240 /** The API Solver object. */
241 api::Solver
* d_solver
;
244 * Create a parser state.
246 * @attention The parser takes "ownership" of the given
247 * input and will delete it on destruction.
249 * @param the solver API object
250 * @param input the parser input
251 * @param strictMode whether to incorporate strict(er) compliance checks
252 * @param parseOnly whether we are parsing only (and therefore certain checks
253 * need not be performed, like those about unimplemented features, @see
254 * unimplementedFeature())
256 Parser(api::Solver
* solver
,
258 bool strictMode
= false,
259 bool parseOnly
= false);
265 /** Get the associated solver. */
266 api::Solver
* getSolver() const;
268 /** Get the associated input. */
269 inline Input
* getInput() const {
273 /** Get unresolved sorts */
274 inline std::set
<api::Sort
>& getUnresolvedSorts() { return d_unresolved
; }
276 /** Deletes and replaces the current parser input. */
277 void setInput(Input
* input
) {
280 d_input
->setParser(*this);
285 * Check if we are done -- either the end of input has been reached, or some
286 * error has been encountered.
287 * @return true if parser is done
289 inline bool done() const {
293 /** Sets the done flag */
294 inline void setDone(bool done
= true) {
298 /** Enable semantic checks during parsing. */
299 void enableChecks() { d_checksEnabled
= true; }
301 /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
302 void disableChecks() { d_checksEnabled
= false; }
304 /** Enable strict parsing, according to the language standards. */
305 void enableStrictMode() { d_strictMode
= true; }
307 /** Disable strict parsing. Allows certain syntactic infelicities to
308 pass without comment. */
309 void disableStrictMode() { d_strictMode
= false; }
311 bool strictModeEnabled() { return d_strictMode
; }
313 void allowIncludeFile() { d_canIncludeFile
= true; }
314 void disallowIncludeFile() { d_canIncludeFile
= false; }
315 bool canIncludeFile() const { return d_canIncludeFile
; }
317 /** Expose the functionality from SMT/SMT2 parsers, while making
318 implementation optional by returning false by default. */
319 virtual bool logicIsSet() { return false; }
321 virtual void forceLogic(const std::string
& logic
)
323 assert(!d_logicIsForced
);
324 d_logicIsForced
= true;
325 d_forcedLogic
= logic
;
327 const std::string
& getForcedLogic() const { return d_forcedLogic
; }
328 bool logicIsForced() const { return d_logicIsForced
; }
331 * Gets the variable currently bound to name.
333 * @param name the name of the variable
334 * @return the variable expression
335 * Only returns a variable if its name is not overloaded, returns null otherwise.
337 api::Term
getVariable(const std::string
& name
);
340 * Gets the function currently bound to name.
342 * @param name the name of the variable
343 * @return the variable expression
344 * Only returns a function if its name is not overloaded, returns null otherwise.
346 api::Term
getFunction(const std::string
& name
);
349 * Returns the expression that name should be interpreted as, based on the current binding.
351 * The symbol name should be declared.
352 * This creates the expression that the string "name" should be interpreted as.
353 * Typically this corresponds to a variable, but it may also correspond to
354 * a nullary constructor or a defined function.
355 * Only returns an expression if its name is not overloaded, returns null otherwise.
357 virtual api::Term
getExpressionForName(const std::string
& name
);
360 * Returns the expression that name should be interpreted as, based on the current binding.
362 * This is the same as above but where the name has been type cast to t.
364 virtual api::Term
getExpressionForNameAndType(const std::string
& name
,
368 * If this method returns true, then name is updated with the tester name
369 * for constructor cons.
371 * In detail, notice that (user-defined) datatypes associate a unary predicate
372 * for each constructor, called its "tester". This symbol is automatically
373 * defined when a datatype is defined. The tester name for a constructor
374 * (e.g. "cons") depends on the language:
375 * - In smt versions < 2.6, the (non-standard) syntax is "is-cons",
376 * - In smt versions >= 2.6, the indexed symbol "(_ is cons)" is used. Thus,
377 * no tester symbol is necessary, since "is" is a builtin symbol. We still use
378 * the above syntax if strict mode is disabled.
379 * - In cvc, the syntax for testers is "is_cons".
381 virtual bool getTesterName(api::Term cons
, std::string
& name
);
384 * Returns the kind that should be used for applications of expression fun.
385 * This is a generalization of ExprManager::operatorToKind that also
386 * handles variables whose types are "function-like", i.e. where
387 * checkFunctionLike(fun) returns true.
389 * For examples of the latter, this function returns
390 * APPLY_UF if fun has function type,
391 * APPLY_CONSTRUCTOR if fun has constructor type.
393 api::Kind
getKindForFunction(api::Term fun
);
396 * Returns a sort, given a name.
397 * @param sort_name the name to look up
399 api::Sort
getSort(const std::string
& sort_name
);
402 * Returns a (parameterized) sort, given a name and args.
404 api::Sort
getSort(const std::string
& sort_name
,
405 const std::vector
<api::Sort
>& params
);
408 * Returns arity of a (parameterized) sort, given a name and args.
410 size_t getArity(const std::string
& sort_name
);
413 * Checks if a symbol has been declared.
414 * @param name the symbol name
415 * @param type the symbol type
416 * @return true iff the symbol has been declared with the given type
418 bool isDeclared(const std::string
& name
, SymbolType type
= SYM_VARIABLE
);
421 * Checks if the declaration policy we want to enforce holds
422 * for the given symbol.
423 * @param name the symbol to check
424 * @param check the kind of check to perform
425 * @param type the type of the symbol
426 * @param notes notes to add to a parse error (if one is generated)
427 * @throws ParserException if checks are enabled and the check fails
429 void checkDeclaration(const std::string
& name
,
430 DeclarationCheck check
,
431 SymbolType type
= SYM_VARIABLE
,
432 std::string notes
= "");
435 * Reserve a symbol at the assertion level.
437 void reserveSymbolAtAssertionLevel(const std::string
& name
);
440 * Checks whether the given expression is function-like, i.e.
441 * it expects arguments. This is checked by looking at the type
442 * of fun. Examples of function types are function, constructor,
444 * @param fun the expression to check
445 * @throws ParserException if checks are enabled and fun is not
448 void checkFunctionLike(api::Term fun
);
450 /** Create a new CVC4 variable expression of the given type.
452 * flags specify information about the variable, e.g. whether it is global or defined
453 * (see enum in expr_manager_template.h).
455 * If a symbol with name already exists,
456 * then if doOverload is true, we create overloaded operators.
457 * else if doOverload is false, the existing expression is shadowed by the new expression.
459 api::Term
bindVar(const std::string
& name
,
460 const api::Sort
& type
,
461 uint32_t flags
= ExprManager::VAR_FLAG_NONE
,
462 bool doOverload
= false);
465 * Create a set of new CVC4 variable expressions of the given type.
467 * flags specify information about the variable, e.g. whether it is global or defined
468 * (see enum in expr_manager_template.h).
470 * For each name, if a symbol with name already exists,
471 * then if doOverload is true, we create overloaded operators.
472 * else if doOverload is false, the existing expression is shadowed by the new expression.
474 std::vector
<api::Term
> bindVars(const std::vector
<std::string
> names
,
475 const api::Sort
& type
,
476 uint32_t flags
= ExprManager::VAR_FLAG_NONE
,
477 bool doOverload
= false);
480 * Create a new CVC4 bound variable expression of the given type. This binds
481 * the symbol name to that variable in the current scope.
483 api::Term
bindBoundVar(const std::string
& name
, const api::Sort
& type
);
485 * Create a new CVC4 bound variable expressions of the given names and types.
486 * Like the method above, this binds these names to those variables in the
489 std::vector
<api::Term
> bindBoundVars(
490 std::vector
<std::pair
<std::string
, api::Sort
> >& sortedVarNames
);
493 * Create a set of new CVC4 bound variable expressions of the given type.
495 * flags specify information about the variable, e.g. whether it is global or defined
496 * (see enum in expr_manager_template.h).
498 * For each name, if a symbol with name already exists,
499 * then if doOverload is true, we create overloaded operators.
500 * else if doOverload is false, the existing expression is shadowed by the new expression.
502 std::vector
<api::Term
> bindBoundVars(const std::vector
<std::string
> names
,
503 const api::Sort
& type
);
506 * Create a new CVC4 function expression of the given type,
507 * appending a unique index to its name. (That's the ONLY
508 * difference between mkAnonymousFunction() and mkVar()).
510 * flags specify information about the variable, e.g. whether it is global or defined
511 * (see enum in expr_manager_template.h).
513 api::Term
mkAnonymousFunction(const std::string
& prefix
,
514 const api::Sort
& type
,
515 uint32_t flags
= ExprManager::VAR_FLAG_NONE
);
517 /** Create a new variable definition (e.g., from a let binding).
518 * levelZero is set if the binding must be done at level 0.
519 * If a symbol with name already exists,
520 * then if doOverload is true, we create overloaded operators.
521 * else if doOverload is false, the existing expression is shadowed by the new expression.
523 void defineVar(const std::string
& name
,
524 const api::Term
& val
,
525 bool levelZero
= false,
526 bool doOverload
= false);
529 * Create a new type definition.
531 * @param name The name of the type
532 * @param type The type that should be associated with the name
533 * @param levelZero If true, the type definition is considered global and
534 * cannot be removed by poppoing the user context
536 void defineType(const std::string
& name
,
537 const api::Sort
& type
,
538 bool levelZero
= false);
541 * Create a new (parameterized) type definition.
543 * @param name The name of the type
544 * @param params The type parameters
545 * @param type The type that should be associated with the name
546 * @param levelZero If true, the type definition is considered global and
547 * cannot be removed by poppoing the user context
549 void defineType(const std::string
& name
,
550 const std::vector
<api::Sort
>& params
,
551 const api::Sort
& type
,
552 bool levelZero
= false);
554 /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
555 void defineParameterizedType(const std::string
& name
,
556 const std::vector
<api::Sort
>& params
,
557 const api::Sort
& type
);
560 * Creates a new sort with the given name.
562 api::Sort
mkSort(const std::string
& name
,
563 uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
566 * Creates a new sort constructor with the given name and arity.
568 api::Sort
mkSortConstructor(const std::string
& name
,
570 uint32_t flags
= ExprManager::SORT_FLAG_NONE
);
573 * Creates a new "unresolved type," used only during parsing.
575 api::Sort
mkUnresolvedType(const std::string
& name
);
578 * Creates a new unresolved (parameterized) type constructor of the given
581 api::Sort
mkUnresolvedTypeConstructor(const std::string
& name
, size_t arity
);
583 * Creates a new unresolved (parameterized) type constructor given the type
586 api::Sort
mkUnresolvedTypeConstructor(const std::string
& name
,
587 const std::vector
<api::Sort
>& params
);
590 * Creates a new unresolved (parameterized) type constructor of the given
591 * arity. Calls either mkUnresolvedType or mkUnresolvedTypeConstructor
592 * depending on the arity.
594 api::Sort
mkUnresolvedType(const std::string
& name
, size_t arity
);
597 * Returns true IFF name is an unresolved type.
599 bool isUnresolvedType(const std::string
& name
);
602 * Creates and binds sorts of a list of mutually-recursive datatype
605 * For each symbol defined by the datatype, if a symbol with name already
606 * exists, then if doOverload is true, we create overloaded operators. Else, if
607 * doOverload is false, the existing expression is shadowed by the new
610 std::vector
<api::Sort
> bindMutualDatatypeTypes(
611 std::vector
<api::DatatypeDecl
>& datatypes
, bool doOverload
= false);
613 /** make flat function type
615 * Returns the "flat" function type corresponding to the function taking
616 * argument types "sorts" and range type "range". A flat function type is
617 * one whose range is not a function. Notice that if sorts is empty and range
618 * is not a function, then this function returns range itself.
620 * If range is a function type, we add its function argument sorts to sorts
621 * and consider its function range as the new range. For each sort S added
622 * to sorts in this process, we add a new bound variable of sort S to
626 * mkFlattenFunctionType( { Int, (-> Real Real) }, (-> Int Bool), {} ):
627 * - returns the the function type (-> Int (-> Real Real) Int Bool)
628 * - updates sorts to { Int, (-> Real Real), Int },
629 * - updates flattenVars to { x }, where x is bound variable of type Int.
631 * Notice that this method performs only one level of flattening, for example,
632 * mkFlattenFunctionType({ Int, (-> Real Real) }, (-> Int (-> Int Bool)), {}):
633 * - returns the the function type (-> Int (-> Real Real) Int (-> Int Bool))
634 * - updates sorts to { Int, (-> Real Real), Int },
635 * - updates flattenVars to { x }, where x is bound variable of type Int.
637 * This method is required so that we do not return functions
638 * that have function return type (these give an unhandled exception
639 * in the ExprManager). For examples of the equivalence between function
640 * definitions in the proposed higher-order extension of the smt2 language,
641 * see page 3 of http://matryoshka.gforge.inria.fr/pubs/PxTP2017.pdf.
643 * The argument flattenVars is needed in the case of defined functions
644 * with function return type. These have implicit arguments, for instance:
645 * (define-fun Q ((x Int)) (-> Int Int) (lambda y (P x)))
646 * is equivalent to the command:
647 * (define-fun Q ((x Int) (z Int)) Int (@ (lambda y (P x)) z))
648 * where @ is (higher-order) application. In this example, z is added to
651 api::Sort
mkFlatFunctionType(std::vector
<api::Sort
>& sorts
,
653 std::vector
<api::Term
>& flattenVars
);
655 /** make flat function type
657 * Same as above, but does not take argument flattenVars.
658 * This is used when the arguments of the function are not important (for
659 * instance, if we are only using this type in a declare-fun).
661 api::Sort
mkFlatFunctionType(std::vector
<api::Sort
>& sorts
, api::Sort range
);
663 /** make higher-order apply
665 * This returns the left-associative curried application of (function) expr to
666 * the arguments in args.
668 * For example, mkHoApply( f, { a, b }, 0 ) returns
669 * (HO_APPLY (HO_APPLY f a) b)
671 * If args is non-empty, the expected type of expr is (-> T0 ... Tn T), where
672 * args[i].getType() = Ti
673 * for each i where 0 <= i < args.size(). If expr is not of this
674 * type, the expression returned by this method will not be well typed.
676 api::Term
mkHoApply(api::Term expr
, const std::vector
<api::Term
>& args
);
678 /** Apply type ascription
680 * Return term t with a type ascription applied to it. This is used for
681 * syntax like (as t T) in smt2 and t::T in the CVC language. This includes:
682 * - (as emptyset (Set T))
683 * - (as univset (Set T))
686 * - ((as cons T) t1 ... tn) where cons is a parametric datatype constructor.
688 * The term to ascribe t is a term whose kind and children (but not type)
689 * are equivalent to that of the term returned by this method.
691 * Notice that method is not necessarily a cast. In actuality, the above terms
692 * should be understood as symbols indexed by types. However, SMT-LIB does not
693 * permit types as indices, so we must use, e.g. (as emptyset (Set T))
694 * instead of (_ emptyset (Set T)).
696 * @param t The term to ascribe a type
697 * @param s The sort to ascribe
698 * @return Term t with sort s ascribed.
700 api::Term
applyTypeAscription(api::Term t
, api::Sort s
);
702 //!!!!!!!!!!! temporary
704 * Make var, with flags required by the ExprManager, see ExprManager::mkVar.
706 api::Term
mkVar(const std::string
& name
,
707 const api::Sort
& type
,
709 //!!!!!!!!!!! temporary
712 * Add an operator to the current legal set.
714 * @param kind the built-in operator to add
716 void addOperator(api::Kind kind
);
719 * Preempt the next returned command with other ones; used to
720 * support the :named attribute in SMT-LIBv2, which implicitly
721 * inserts a new command before the current one. Also used in TPTP
722 * because function and predicate symbols are implicitly declared.
724 void preemptCommand(Command
* cmd
);
726 /** Is the symbol bound to a boolean variable? */
727 bool isBoolean(const std::string
& name
);
729 /** Is fun a function (or function-like thing)?
730 * Currently this means its type is either a function, constructor, tester, or selector.
732 bool isFunctionLike(api::Term fun
);
734 /** Is the symbol bound to a predicate? */
735 bool isPredicate(const std::string
& name
);
737 /** Parse and return the next command. */
738 Command
* nextCommand();
740 /** Parse and return the next expression. */
741 api::Term
nextExpression();
743 /** Issue a warning to the user. */
744 void warning(const std::string
& msg
) { d_input
->warning(msg
); }
745 /** Issue a warning to the user, but only once per attribute. */
746 void attributeNotSupported(const std::string
& attr
);
748 /** Raise a parse error with the given message. */
749 inline void parseError(const std::string
& msg
) { d_input
->parseError(msg
); }
750 /** Unexpectedly encountered an EOF */
751 inline void unexpectedEOF(const std::string
& msg
)
753 d_input
->parseError(msg
, true);
757 * If we are parsing only, don't raise an exception; if we are not,
758 * raise a parse error with the given message. There is no actual
759 * parse error, everything is as expected, but we cannot create the
760 * Expr, Type, or other requested thing yet due to internal
761 * limitations. Even though it's not a parse error, we throw a
762 * parse error so that the input line and column information is
765 * Think quantifiers. We don't have a TheoryQuantifiers yet, so we
766 * have no kind::FORALL or kind::EXISTS. But we might want to
767 * support parsing quantifiers (just not doing anything with them).
768 * So this mechanism gives you a way to do it with --parse-only.
770 inline void unimplementedFeature(const std::string
& msg
)
773 parseError("Unimplemented feature: " + msg
);
778 * Gets the current declaration level.
780 inline size_t scopeLevel() const { return d_symtab
->getLevel(); }
783 * Pushes a scope. All subsequent symbol declarations made are only valid in
784 * this scope, i.e. they are deleted on the next call to popScope.
786 * The argument bindingLevel is true, the assertion level is set to the
787 * current scope level. This determines which scope assertions are declared
790 inline void pushScope(bool bindingLevel
= false) {
791 d_symtab
->pushScope();
793 d_assertionLevel
= scopeLevel();
797 inline void popScope() {
798 d_symtab
->popScope();
799 if(scopeLevel() < d_assertionLevel
) {
800 d_assertionLevel
= scopeLevel();
801 d_reservedSymbols
.clear();
805 virtual void reset() {
809 void setGlobalDeclarations(bool flag
) {
810 d_globalDeclarations
= flag
;
813 bool getGlobalDeclarations() { return d_globalDeclarations
; }
815 inline SymbolTable
* getSymbolTable() const {
819 //------------------------ operator overloading
820 /** is this function overloaded? */
821 bool isOverloadedFunction(api::Term fun
)
823 return d_symtab
->isOverloadedFunction(fun
.getExpr());
826 /** Get overloaded constant for type.
827 * If possible, it returns a defined symbol with name
828 * that has type t. Otherwise returns null expression.
830 api::Term
getOverloadedConstantForType(const std::string
& name
, api::Sort t
)
832 return api::Term(d_solver
,
833 d_symtab
->getOverloadedConstantForType(name
, t
.getType()));
837 * If possible, returns a defined function for a name
838 * and a vector of expected argument types. Otherwise returns
841 api::Term
getOverloadedFunctionForTypes(const std::string
& name
,
842 std::vector
<api::Sort
>& argTypes
)
844 return api::Term(d_solver
,
845 d_symtab
->getOverloadedFunctionForTypes(
846 name
, api::sortVectorToTypes(argTypes
)));
848 //------------------------ end operator overloading
850 * Make string constant
852 * This makes the string constant based on the string s. This may involve
853 * processing ad-hoc escape sequences (if the language is not
854 * SMT-LIB 2.6 or higher), or otherwise calling the solver to construct
857 api::Term
mkStringConstant(const std::string
& s
);
860 /** ad-hoc string escaping
862 * Returns the (internal) vector of code points corresponding to processing
863 * the escape sequences in string s. This is to support string inputs that
864 * do no comply with the SMT-LIB standard.
866 * This method handles escape sequences, including \n, \t, \v, \b, \r, \f, \a,
867 * \\, \x[N] and octal escape sequences of the form \[c1]([c2]([c3])?)? where
868 * c1, c2, c3 are digits from 0 to 7.
870 std::vector
<unsigned> processAdHocStringEsc(const std::string
& s
);
873 }/* CVC4::parser namespace */
874 }/* CVC4 namespace */
876 #endif /* CVC4__PARSER__PARSER_STATE_H */