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);
358 void checkArity(
Kind kind,
unsigned numArgs) throw(ParserException);
369 void checkOperator(
Kind kind,
unsigned numArgs) 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,
444 SortType mkUnresolvedType(const
std::
string& name);
457 const
std::vector<
Type>& params);
462 bool isUnresolvedType(const
std::
string& name);
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);
501 Command* nextCommand() throw(ParserException);
504 Expr nextExpression() throw(ParserException);
507 inline
void warning(const
std::
string& msg) {
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;
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.
The representation of an inductive datatype.
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
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.
Class encapsulating the datatype type.
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.