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.
Input * getInput() const
Get the associated input.
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.
SymbolTable * getSymbolTable() const
virtual bool logicIsSet()
Expose the functionality from SMT/SMT2 parsers, while making implementation optional by returning fal...
bool done() const
Check if we are done – either the end of input has been reached, or some error has been encountered...
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...
A stream interface for expressions.
void disallowIncludeFile()
Enforce that the symbol has been declared.
size_t getLevel() const
Get the current level of this symbol table.
std::ostream & operator<<(std::ostream &out, DeclarationCheck check)
Returns a string representation of the given object (for debugging).
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)
const std::string & getForcedLogic() const
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.
bool canIncludeFile() const
Expr nextExpr()
Get the next expression in the stream (advancing the stream pointer as a side effect.)
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...
~ExprStream()
Virtual destructor; this implementation does nothing.
ExprManager * getExprManager() const
Get the associated ExprManager.
void popScope()
Pop a scope level.
bool logicIsForced() const
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.
size_t scopeLevel() const
Gets the current declaration level.