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;
168 std::set<Kind> d_logicOperators;
171 std::set<std::string> d_attributesWarnedAbout;
180 std::set<Type> d_unresolved;
187 std::list<Command*> d_commandQueue;
216 return d_exprManager;
271 Expr getVariable(
const std::string& name);
279 Expr getFunction(
const std::string& name);
285 Type getSort(
const std::string& sort_name);
290 Type getSort(
const std::string& sort_name,
291 const std::vector<Type>& params);
296 size_t getArity(
const std::string& sort_name);
321 void reserveSymbolAtAssertionLevel(const std::
string& name);
329 void checkFunctionLike(const std::
string& name) throw(ParserException);
339 void checkArity(
Kind kind,
unsigned numArgs) throw(ParserException);
350 void checkOperator(
Kind kind,
unsigned numArgs) throw(ParserException);
361 Expr mkVar(const std::
string& name, const
Type& type,
368 mkVars(const std::vector<std::
string> names, const
Type& type,
372 Expr mkBoundVar(const std::
string& name, const
Type& type);
377 std::vector<
Expr> mkBoundVars(const std::vector<std::
string> names, const
Type& type);
380 Expr mkFunction(const std::
string& name, const
Type& type,
388 Expr mkAnonymousFunction(const std::
string& prefix, const
Type& type,
392 void defineVar(const std::
string& name, const
Expr& val,
393 bool levelZero = false);
396 void defineFunction(const std::
string& name, const
Expr& val,
397 bool levelZero = false);
400 void defineType(const std::
string& name, const
Type& type);
403 void defineType(const std::
string& name,
404 const std::vector<
Type>& params, const
Type& type);
407 void defineParameterizedType(const std::
string& name,
408 const std::vector<
Type>& params,
414 SortType mkSort(const std::
string& name,
425 SortType mkUnresolvedType(const std::
string& name);
438 const std::vector<
Type>& params);
443 bool isUnresolvedType(const std::
string& name);
449 mkMutualDatatypeTypes(const std::vector<
Datatype>& datatypes);
456 void addOperator(
Kind kind);
464 void preemptCommand(
Command* cmd);
467 bool isBoolean(const std::
string& name);
470 bool isFunctionLike(const std::
string& name);
473 bool isDefinedFunction(const std::
string& name);
476 bool isDefinedFunction(
Expr func);
479 bool isPredicate(const std::
string& name);
482 Command* nextCommand() throw(ParserException);
485 Expr nextExpression() throw(ParserException);
488 inline
void warning(const std::
string& msg) {
489 d_input->warning(msg);
493 void attributeNotSupported(
const std::string& attr);
497 d_input->parseError(msg);
502 d_input->parseError(msg,
true);
521 parseError(
"Unimplemented feature: " + msg);
528 inline size_t scopeLevel()
const {
return d_symtab->getLevel(); }
531 d_symtab->pushScope();
533 d_assertionLevel = scopeLevel();
538 d_symtab->popScope();
539 if(scopeLevel() < d_assertionLevel) {
540 d_assertionLevel = scopeLevel();
541 d_reservedSymbols.clear();
572 d_symtab = &d_symtabAllocated;
574 d_symtab = parser->d_symtab;
Enforce that the symbol has not been declared.
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Class encapsulating a user-defined sort.
Exception class for parse errors.
The representation of an inductive datatype.
void enableChecks()
Enable semantic checks during parsing.
This is CVC4 release version For build and installation notes
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 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).
void setDone(bool done=true)
Sets the done flag.
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
A convenience class for handling scoped declarations.
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.
struct CVC4::options::out__option_t out
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.
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.
struct CVC4::options::parseOnly__option_t parseOnly
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.