19 #ifndef __CVC4__PARSER__PARSER_STATE_H 20 #define __CVC4__PARSER__PARSER_STATE_H 65 return out <<
"CHECK_NONE";
67 return out <<
"CHECK_DECLARED";
69 return out <<
"CHECK_UNDECLARED";
71 return out <<
"DeclarationCheck!UNKNOWN";
93 return out <<
"SYM_VARIABLE";
95 return out <<
"SYM_SORT";
97 return out <<
"SymbolType!UNKNOWN";
134 size_t d_assertionLevel;
144 std::set<std::string> d_reservedSymbols;
147 size_t d_anonymousFunctionCount;
153 bool d_checksEnabled;
165 bool d_canIncludeFile;
170 bool d_logicIsForced;
175 std::string d_forcedLogic;
178 std::set<Kind> d_logicOperators;
181 std::set<std::string> d_attributesWarnedAbout;
190 std::set<Type> d_unresolved;
197 std::list<Command*> d_commandQueue;
226 return d_exprManager;
279 void forceLogic(
const std::string& logic) { assert(!d_logicIsForced); d_logicIsForced =
true; d_forcedLogic = logic; }
289 Expr getVariable(
const std::string& name);
297 Expr getFunction(
const std::string& name);
303 Type getSort(
const std::string& sort_name);
308 Type getSort(
const std::string& sort_name,
309 const std::vector<Type>& params);
314 size_t getArity(
const std::string& sort_name);
340 void reserveSymbolAtAssertionLevel(
const std::string& name);
348 void checkFunctionLike(
const std::string& name)
throw(
ParserException);
380 Expr mkVar(
const std::string& name,
const Type& type,
387 mkVars(
const std::vector<std::string> names,
const Type& type,
391 Expr mkBoundVar(
const std::string& name,
const Type& type);
396 std::vector<Expr> mkBoundVars(
const std::vector<std::string> names,
const Type& type);
399 Expr mkFunction(
const std::string& name,
const Type& type,
407 Expr mkAnonymousFunction(
const std::string& prefix,
const Type& type,
411 void defineVar(
const std::string& name,
const Expr& val,
412 bool levelZero =
false);
415 void defineFunction(
const std::string& name,
const Expr& val,
416 bool levelZero =
false);
419 void defineType(
const std::string& name,
const Type& type);
422 void defineType(
const std::string& name,
423 const std::vector<Type>& params,
const Type& type);
426 void defineParameterizedType(
const std::string& name,
427 const std::vector<Type>& params,
433 SortType mkSort(
const std::string& name,
444 SortType mkUnresolvedType(
const std::string& name);
457 const std::vector<Type>& params);
462 bool isUnresolvedType(
const std::string& name);
467 std::vector<DatatypeType>
468 mkMutualDatatypeTypes(
const std::vector<Datatype>& datatypes);
475 void addOperator(
Kind kind);
483 void preemptCommand(
Command* cmd);
486 bool isBoolean(
const std::string& name);
489 bool isFunctionLike(
const std::string& name);
492 bool isDefinedFunction(
const std::string& name);
495 bool isDefinedFunction(
Expr func);
498 bool isPredicate(
const std::string& name);
512 void attributeNotSupported(
const std::string& attr);
540 parseError(
"Unimplemented feature: " + msg);
552 d_assertionLevel = scopeLevel();
558 if(scopeLevel() < d_assertionLevel) {
559 d_assertionLevel = scopeLevel();
560 d_reservedSymbols.clear();
591 d_symtab = &d_symtabAllocated;
593 d_symtab = parser->d_symtab;
void warning(const std::string &msg)
Issue a warning to the user.
Enforce that the symbol has not been declared.
Expr nextExpression()
Parse and return the next expression.
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Class encapsulating a user-defined sort.
Exception class for parse errors.
size_t getLevel() const
Get the current level of this symbol table.
virtual bool logicIsSet()
Expose the functionality from SMT/SMT2 parsers, while making implementation optional by returning fal...
void enableChecks()
Enable semantic checks during parsing.
An expression stream interface for a parser.
Class encapsulating CVC4 expression types.
void disableChecks()
Disable semantic checks during parsing.
void unimplementedFeature(const std::string &msg)
If we are parsing only, don't raise an exception; if we are not, raise a parse error with the given m...
bool logicIsForced() const
bool canIncludeFile() const
A stream interface for expressions.
void disallowIncludeFile()
Enforce that the symbol has been declared.
std::ostream & operator<<(std::ostream &out, DeclarationCheck check)
Returns a string representation of the given object (for debugging).
const std::string & getForcedLogic() const
Don't check anything.
void setDone(bool done=true)
Sets the done flag.
void forceLogic(const std::string &logic)
A convenience class for handling scoped declarations.
void pushScope()
Push a scope level.
struct CVC4::options::parseOnly__option_t parseOnly
void useDeclarationsFrom(SymbolTable *symtab)
Class encapsulating a user-defined sort constructor.
SymbolType
Types of symbols.
ExprStream(Parser *parser)
A pure-virtual stream interface for expressions.
Convenience class for scoping variable and type declarations.
void useDeclarationsFrom(Parser *parser)
Set the current symbol table used by this parser.
A builder for input language parsers.
void pushScope(bool bindingLevel=false)
void setInput(Input *input)
Deletes and replaces the current parser input.
Expr nextExpr()
Get the next expression in the stream (advancing the stream pointer as a side effect.)
Input * getInput() const
Get the associated input.
void unexpectedEOF(const std::string &msg)
Unexpectedly encountered an EOF.
void disableStrictMode()
Disable strict parsing.
void parseError(const std::string &msg)
Raise a parse error with the given message.
void enableStrictMode()
Enable strict parsing, according to the language standards.
struct CVC4::options::out__option_t out
DeclarationCheck
Types of check for the symols.
Macros that should be defined everywhere during the building of the libraries and driver binary...
size_t scopeLevel() const
Gets the current declaration level.
~ExprStream()
Virtual destructor; this implementation does nothing.
void popScope()
Pop a scope level.
ExprManager * getExprManager() const
Get the associated ExprManager.
SymbolTable * getSymbolTable() const
bool done() const
Check if we are done – either the end of input has been reached, or some error has been encountered...
This class encapsulates all of the state of a parser, including the name of the file, line number and column information, and in-scope declarations.