cvc4-1.3
parser.h
Go to the documentation of this file.
1 /********************* */
17 #include "cvc4parser_public.h"
18 
19 #ifndef __CVC4__PARSER__PARSER_STATE_H
20 #define __CVC4__PARSER__PARSER_STATE_H
21 
22 #include <string>
23 #include <set>
24 #include <list>
25 #include <cassert>
26 
27 #include "parser/input.h"
29 #include "expr/expr.h"
30 #include "expr/symbol_table.h"
31 #include "expr/kind.h"
32 #include "expr/expr_stream.h"
33 
34 namespace CVC4 {
35 
36 // Forward declarations
37 class BooleanType;
38 class ExprManager;
39 class Command;
40 class FunctionType;
41 class Type;
42 
43 namespace parser {
44 
45 class Input;
46 
55 };/* enum DeclarationCheck */
56 
61 inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) CVC4_PUBLIC;
62 inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) {
63  switch(check) {
64  case CHECK_NONE:
65  return out << "CHECK_NONE";
66  case CHECK_DECLARED:
67  return out << "CHECK_DECLARED";
68  case CHECK_UNDECLARED:
69  return out << "CHECK_UNDECLARED";
70  default:
71  return out << "DeclarationCheck!UNKNOWN";
72  }
73 }
74 
78 enum SymbolType {
83 };/* enum SymbolType */
84 
89 inline std::ostream& operator<<(std::ostream& out, SymbolType type) CVC4_PUBLIC;
90 inline std::ostream& operator<<(std::ostream& out, SymbolType type) {
91  switch(type) {
92  case SYM_VARIABLE:
93  return out << "SYM_VARIABLE";
94  case SYM_SORT:
95  return out << "SYM_SORT";
96  default:
97  return out << "SymbolType!UNKNOWN";
98  }
99 }
100 
107  friend class ParserBuilder;
108 
110  ExprManager *d_exprManager;
111 
113  Input *d_input;
114 
119  SymbolTable d_symtabAllocated;
120 
127  SymbolTable* d_symtab;
128 
134  size_t d_assertionLevel;
135 
144  std::set<std::string> d_reservedSymbols;
145 
147  size_t d_anonymousFunctionCount;
148 
150  bool d_done;
151 
153  bool d_checksEnabled;
154 
156  bool d_strictMode;
157 
159  bool d_parseOnly;
160 
165  bool d_canIncludeFile;
166 
168  std::set<Kind> d_logicOperators;
169 
171  std::set<std::string> d_attributesWarnedAbout;
172 
180  std::set<Type> d_unresolved;
181 
187  std::list<Command*> d_commandQueue;
188 
190  Expr getSymbol(const std::string& var_name, SymbolType type);
191 
192 protected:
206  Parser(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
207 
208 public:
209 
210  virtual ~Parser() {
211  delete d_input;
212  }
213 
215  inline ExprManager* getExprManager() const {
216  return d_exprManager;
217  }
218 
220  inline Input* getInput() const {
221  return d_input;
222  }
223 
225  void setInput(Input* input) {
226  delete d_input;
227  d_input = input;
228  d_input->setParser(*this);
229  d_done = false;
230  }
231 
237  inline bool done() const {
238  return d_done;
239  }
240 
242  inline void setDone(bool done = true) {
243  d_done = done;
244  }
245 
247  void enableChecks() { d_checksEnabled = true; }
248 
250  void disableChecks() { d_checksEnabled = false; }
251 
253  void enableStrictMode() { d_strictMode = true; }
254 
257  void disableStrictMode() { d_strictMode = false; }
258 
259  bool strictModeEnabled() { return d_strictMode; }
260 
261  void allowIncludeFile() { d_canIncludeFile = true; }
262  void disallowIncludeFile() { d_canIncludeFile = false; }
263  bool canIncludeFile() const { return d_canIncludeFile; }
264 
271  Expr getVariable(const std::string& name);
272 
279  Expr getFunction(const std::string& name);
280 
285  Type getSort(const std::string& sort_name);
286 
290  Type getSort(const std::string& sort_name,
291  const std::vector<Type>& params);
292 
296  size_t getArity(const std::string& sort_name);
297 
304  bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
305 
314  void checkDeclaration(const std::string& name, DeclarationCheck check,
315  SymbolType type = SYM_VARIABLE,
316  std::string notes = "") throw(ParserException);
317 
321  void reserveSymbolAtAssertionLevel(const std::string& name);
322 
329  void checkFunctionLike(const std::string& name) throw(ParserException);
330 
339  void checkArity(Kind kind, unsigned numArgs) throw(ParserException);
340 
350  void checkOperator(Kind kind, unsigned numArgs) throw(ParserException);
351 
358  Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
359 
361  Expr mkVar(const std::string& name, const Type& type,
362  uint32_t flags = ExprManager::VAR_FLAG_NONE);
363 
367  std::vector<Expr>
368  mkVars(const std::vector<std::string> names, const Type& type,
369  uint32_t flags = ExprManager::VAR_FLAG_NONE);
370 
372  Expr mkBoundVar(const std::string& name, const Type& type);
373 
377  std::vector<Expr> mkBoundVars(const std::vector<std::string> names, const Type& type);
378 
380  Expr mkFunction(const std::string& name, const Type& type,
381  uint32_t flags = ExprManager::VAR_FLAG_NONE);
382 
388  Expr mkAnonymousFunction(const std::string& prefix, const Type& type,
389  uint32_t flags = ExprManager::VAR_FLAG_NONE);
390 
392  void defineVar(const std::string& name, const Expr& val,
393  bool levelZero = false);
394 
396  void defineFunction(const std::string& name, const Expr& val,
397  bool levelZero = false);
398 
400  void defineType(const std::string& name, const Type& type);
401 
403  void defineType(const std::string& name,
404  const std::vector<Type>& params, const Type& type);
405 
407  void defineParameterizedType(const std::string& name,
408  const std::vector<Type>& params,
409  const Type& type);
410 
414  SortType mkSort(const std::string& name,
415  uint32_t flags = ExprManager::SORT_FLAG_NONE);
416 
420  SortConstructorType mkSortConstructor(const std::string& name, size_t arity);
421 
425  SortType mkUnresolvedType(const std::string& name);
426 
431  SortConstructorType mkUnresolvedTypeConstructor(const std::string& name,
432  size_t arity);
437  SortConstructorType mkUnresolvedTypeConstructor(const std::string& name,
438  const std::vector<Type>& params);
439 
443  bool isUnresolvedType(const std::string& name);
444 
448  std::vector<DatatypeType>
449  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
450 
456  void addOperator(Kind kind);
457 
464  void preemptCommand(Command* cmd);
465 
467  bool isBoolean(const std::string& name);
468 
470  bool isFunctionLike(const std::string& name);
471 
473  bool isDefinedFunction(const std::string& name);
474 
476  bool isDefinedFunction(Expr func);
477 
479  bool isPredicate(const std::string& name);
480 
482  Command* nextCommand() throw(ParserException);
483 
485  Expr nextExpression() throw(ParserException);
486 
488  inline void warning(const std::string& msg) {
489  d_input->warning(msg);
490  }
491 
493  void attributeNotSupported(const std::string& attr);
494 
496  inline void parseError(const std::string& msg) throw(ParserException) {
497  d_input->parseError(msg);
498  }
499 
501  inline void unexpectedEOF(const std::string& msg) throw(ParserException) {
502  d_input->parseError(msg, true);
503  }
504 
519  inline void unimplementedFeature(const std::string& msg) throw(ParserException) {
520  if(!d_parseOnly) {
521  parseError("Unimplemented feature: " + msg);
522  }
523  }
524 
528  inline size_t scopeLevel() const { return d_symtab->getLevel(); }
529 
530  inline void pushScope(bool bindingLevel = false) {
531  d_symtab->pushScope();
532  if(!bindingLevel) {
533  d_assertionLevel = scopeLevel();
534  }
535  }
536 
537  inline void popScope() {
538  d_symtab->popScope();
539  if(scopeLevel() < d_assertionLevel) {
540  d_assertionLevel = scopeLevel();
541  d_reservedSymbols.clear();
542  }
543  }
544 
570  inline void useDeclarationsFrom(Parser* parser) {
571  if(parser == NULL) {
572  d_symtab = &d_symtabAllocated;
573  } else {
574  d_symtab = parser->d_symtab;
575  }
576  }
577 
578  inline void useDeclarationsFrom(SymbolTable* symtab) {
579  d_symtab = symtab;
580  }
581 
582  inline SymbolTable* getSymbolTable() const {
583  return d_symtab;
584  }
585 
595  class ExprStream : public CVC4::ExprStream {
596  Parser* d_parser;
597  public:
598  ExprStream(Parser* parser) : d_parser(parser) {}
599  ~ExprStream() { delete d_parser; }
600  Expr nextExpr() { return d_parser->nextExpression(); }
601  };/* class Parser::ExprStream */
602 };/* class Parser */
603 
604 }/* CVC4::parser namespace */
605 }/* CVC4 namespace */
606 
607 #endif /* __CVC4__PARSER__PARSER_STATE_H */
void allowIncludeFile()
Definition: parser.h:261
Enforce that the symbol has not been declared.
Definition: parser.h:52
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:226
Class encapsulating a user-defined sort.
Definition: type.h:494
Exception class for parse errors.
Base for parser inputs.
void * ExprManager
The representation of an inductive datatype.
Definition: datatype.h:382
void enableChecks()
Enable semantic checks during parsing.
Definition: parser.h:247
This is CVC4 release version For build and installation notes
Definition: README:1
An expression stream interface for a parser.
Definition: parser.h:595
Class encapsulating CVC4 expression types.
Definition: type.h:88
void disableChecks()
Disable semantic checks during parsing.
Definition: parser.h:250
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...
Definition: parser.h:519
bool canIncludeFile() const
Definition: parser.h:263
A stream interface for expressions.
void disallowIncludeFile()
Definition: parser.h:262
Enforce that the symbol has been declared.
Definition: parser.h:50
std::ostream & operator<<(std::ostream &out, DeclarationCheck check)
Returns a string representation of the given object (for debugging).
Definition: parser.h:62
Don't check anything.
Definition: parser.h:54
void setDone(bool done=true)
Sets the done flag.
Definition: parser.h:242
bool strictModeEnabled()
Definition: parser.h:259
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
Definition: README:39
A convenience class for handling scoped declarations.
Definition: symbol_table.h:48
void useDeclarationsFrom(SymbolTable *symtab)
Definition: parser.h:578
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Class encapsulating a user-defined sort constructor.
Definition: type.h:515
Class encapsulating the datatype type.
Definition: type.h:594
SymbolType
Types of symbols.
Definition: parser.h:78
ExprStream(Parser *parser)
Definition: parser.h:598
A pure-virtual stream interface for expressions.
Definition: expr_stream.h:30
Convenience class for scoping variable and type declarations.
void useDeclarationsFrom(Parser *parser)
Set the current symbol table used by this parser.
Definition: parser.h:570
A builder for input language parsers.
void pushScope(bool bindingLevel=false)
Definition: parser.h:530
void setInput(Input *input)
Deletes and replaces the current parser input.
Definition: parser.h:225
struct CVC4::options::out__option_t out
An input to be parsed.
Definition: input.h:86
Expr nextExpr()
Get the next expression in the stream (advancing the stream pointer as a side effect.)
Definition: parser.h:600
virtual void setParser(Parser &parser)=0
Set the Parser object for this input.
Input * getInput() const
Get the associated input.
Definition: parser.h:220
void unexpectedEOF(const std::string &msg)
Unexpectedly encountered an EOF.
Definition: parser.h:501
void disableStrictMode()
Disable strict parsing.
Definition: parser.h:257
void parseError(const std::string &msg)
Raise a parse error with the given message.
Definition: parser.h:496
kind.h
void enableStrictMode()
Enable strict parsing, according to the language standards.
Definition: parser.h:253
DeclarationCheck
Types of check for the symols.
Definition: parser.h:48
expr.h
Macros that should be defined everywhere during the building of the libraries and driver binary...
void * Type
size_t scopeLevel() const
Gets the current declaration level.
Definition: parser.h:528
~ExprStream()
Virtual destructor; this implementation does nothing.
Definition: parser.h:599
struct CVC4::options::parseOnly__option_t parseOnly
virtual ~Parser()
Definition: parser.h:210
ExprManager * getExprManager() const
Get the associated ExprManager.
Definition: parser.h:215
SymbolTable * getSymbolTable() const
Definition: parser.h:582
bool done() const
Check if we are done – either the end of input has been reached, or some error has been encountered...
Definition: parser.h:237
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.
Definition: parser.h:106
Kind_t
Definition: kind.h:60