cvc4-1.4
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 
106 class CVC4_PUBLIC Parser {
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 
170  bool d_logicIsForced;
171 
175  std::string d_forcedLogic;
176 
178  std::set<Kind> d_logicOperators;
179 
181  std::set<std::string> d_attributesWarnedAbout;
182 
190  std::set<Type> d_unresolved;
191 
197  std::list<Command*> d_commandQueue;
198 
200  Expr getSymbol(const std::string& var_name, SymbolType type);
201 
202 protected:
216  Parser(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
217 
218 public:
219 
220  virtual ~Parser() {
221  delete d_input;
222  }
223 
225  inline ExprManager* getExprManager() const {
226  return d_exprManager;
227  }
228 
230  inline Input* getInput() const {
231  return d_input;
232  }
233 
235  void setInput(Input* input) {
236  delete d_input;
237  d_input = input;
238  d_input->setParser(*this);
239  d_done = false;
240  }
241 
247  inline bool done() const {
248  return d_done;
249  }
250 
252  inline void setDone(bool done = true) {
253  d_done = done;
254  }
255 
257  void enableChecks() { d_checksEnabled = true; }
258 
260  void disableChecks() { d_checksEnabled = false; }
261 
263  void enableStrictMode() { d_strictMode = true; }
264 
267  void disableStrictMode() { d_strictMode = false; }
268 
269  bool strictModeEnabled() { return d_strictMode; }
270 
271  void allowIncludeFile() { d_canIncludeFile = true; }
272  void disallowIncludeFile() { d_canIncludeFile = false; }
273  bool canIncludeFile() const { return d_canIncludeFile; }
274 
277  virtual bool logicIsSet() { return false; }
278 
279  void forceLogic(const std::string& logic) { assert(!d_logicIsForced); d_logicIsForced = true; d_forcedLogic = logic; }
280  const std::string& getForcedLogic() const { return d_forcedLogic; }
281  bool logicIsForced() const { return d_logicIsForced; }
282 
289  Expr getVariable(const std::string& name);
290 
297  Expr getFunction(const std::string& name);
298 
303  Type getSort(const std::string& sort_name);
304 
308  Type getSort(const std::string& sort_name,
309  const std::vector<Type>& params);
310 
314  size_t getArity(const std::string& sort_name);
315 
322  bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
323 
333  void checkDeclaration(const std::string& name, DeclarationCheck check,
334  SymbolType type = SYM_VARIABLE,
335  std::string notes = "") throw(ParserException);
336 
340  void reserveSymbolAtAssertionLevel(const std::string& name);
341 
348  void checkFunctionLike(const std::string& name) throw(ParserException);
349 
358  void checkArity(Kind kind, unsigned numArgs) throw(ParserException);
359 
369  void checkOperator(Kind kind, unsigned numArgs) throw(ParserException);
370 
377  Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
378 
380  Expr mkVar(const std::string& name, const Type& type,
381  uint32_t flags = ExprManager::VAR_FLAG_NONE);
382 
386  std::vector<Expr>
387  mkVars(const std::vector<std::string> names, const Type& type,
388  uint32_t flags = ExprManager::VAR_FLAG_NONE);
389 
391  Expr mkBoundVar(const std::string& name, const Type& type);
392 
396  std::vector<Expr> mkBoundVars(const std::vector<std::string> names, const Type& type);
397 
399  Expr mkFunction(const std::string& name, const Type& type,
400  uint32_t flags = ExprManager::VAR_FLAG_NONE);
401 
407  Expr mkAnonymousFunction(const std::string& prefix, const Type& type,
408  uint32_t flags = ExprManager::VAR_FLAG_NONE);
409 
411  void defineVar(const std::string& name, const Expr& val,
412  bool levelZero = false);
413 
415  void defineFunction(const std::string& name, const Expr& val,
416  bool levelZero = false);
417 
419  void defineType(const std::string& name, const Type& type);
420 
422  void defineType(const std::string& name,
423  const std::vector<Type>& params, const Type& type);
424 
426  void defineParameterizedType(const std::string& name,
427  const std::vector<Type>& params,
428  const Type& type);
429 
433  SortType mkSort(const std::string& name,
434  uint32_t flags = ExprManager::SORT_FLAG_NONE);
435 
439  SortConstructorType mkSortConstructor(const std::string& name, size_t arity);
440 
444  SortType mkUnresolvedType(const std::string& name);
445 
450  SortConstructorType mkUnresolvedTypeConstructor(const std::string& name,
451  size_t arity);
456  SortConstructorType mkUnresolvedTypeConstructor(const std::string& name,
457  const std::vector<Type>& params);
458 
462  bool isUnresolvedType(const std::string& name);
463 
467  std::vector<DatatypeType>
468  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
469 
475  void addOperator(Kind kind);
476 
483  void preemptCommand(Command* cmd);
484 
486  bool isBoolean(const std::string& name);
487 
489  bool isFunctionLike(const std::string& name);
490 
492  bool isDefinedFunction(const std::string& name);
493 
495  bool isDefinedFunction(Expr func);
496 
498  bool isPredicate(const std::string& name);
499 
501  Command* nextCommand() throw(ParserException);
502 
504  Expr nextExpression() throw(ParserException);
505 
507  inline void warning(const std::string& msg) {
508  d_input->warning(msg);
509  }
510 
512  void attributeNotSupported(const std::string& attr);
513 
515  inline void parseError(const std::string& msg) throw(ParserException) {
516  d_input->parseError(msg);
517  }
518 
520  inline void unexpectedEOF(const std::string& msg) throw(ParserException) {
521  d_input->parseError(msg, true);
522  }
523 
538  inline void unimplementedFeature(const std::string& msg) throw(ParserException) {
539  if(!d_parseOnly) {
540  parseError("Unimplemented feature: " + msg);
541  }
542  }
543 
547  inline size_t scopeLevel() const { return d_symtab->getLevel(); }
548 
549  inline void pushScope(bool bindingLevel = false) {
550  d_symtab->pushScope();
551  if(!bindingLevel) {
552  d_assertionLevel = scopeLevel();
553  }
554  }
555 
556  inline void popScope() {
557  d_symtab->popScope();
558  if(scopeLevel() < d_assertionLevel) {
559  d_assertionLevel = scopeLevel();
560  d_reservedSymbols.clear();
561  }
562  }
563 
589  inline void useDeclarationsFrom(Parser* parser) {
590  if(parser == NULL) {
591  d_symtab = &d_symtabAllocated;
592  } else {
593  d_symtab = parser->d_symtab;
594  }
595  }
596 
597  inline void useDeclarationsFrom(SymbolTable* symtab) {
598  d_symtab = symtab;
599  }
600 
601  inline SymbolTable* getSymbolTable() const {
602  return d_symtab;
603  }
604 
614  class ExprStream : public CVC4::ExprStream {
615  Parser* d_parser;
616  public:
617  ExprStream(Parser* parser) : d_parser(parser) {}
618  ~ExprStream() { delete d_parser; }
619  Expr nextExpr() { return d_parser->nextExpression(); }
620  };/* class Parser::ExprStream */
621 };/* class Parser */
622 
623 }/* CVC4::parser namespace */
624 }/* CVC4 namespace */
625 
626 #endif /* __CVC4__PARSER__PARSER_STATE_H */
void allowIncludeFile()
Definition: parser.h:271
void warning(const std::string &msg)
Issue a warning to the user.
Definition: parser.h:507
Enforce that the symbol has not been declared.
Definition: parser.h:52
Input * getInput() const
Get the associated input.
Definition: parser.h:230
Expr nextExpression()
Parse and return the next expression.
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:227
Class encapsulating a user-defined sort.
Definition: type.h:515
Exception class for parse errors.
Base for parser inputs.
Definition: expr.h:106
void * ExprManager
SymbolTable * getSymbolTable() const
Definition: parser.h:601
virtual bool logicIsSet()
Expose the functionality from SMT/SMT2 parsers, while making implementation optional by returning fal...
Definition: parser.h:277
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:247
void enableChecks()
Enable semantic checks during parsing.
Definition: parser.h:257
An expression stream interface for a parser.
Definition: parser.h:614
Class encapsulating CVC4 expression types.
Definition: type.h:89
void disableChecks()
Disable semantic checks during parsing.
Definition: parser.h:260
void unimplementedFeature(const std::string &msg)
If we are parsing only, don&#39;t raise an exception; if we are not, raise a parse error with the given m...
Definition: parser.h:538
A stream interface for expressions.
void disallowIncludeFile()
Definition: parser.h:272
Enforce that the symbol has been declared.
Definition: parser.h:50
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).
Definition: parser.h:62
Don&#39;t check anything.
Definition: parser.h:54
void setDone(bool done=true)
Sets the done flag.
Definition: parser.h:252
bool strictModeEnabled()
Definition: parser.h:269
void forceLogic(const std::string &logic)
Definition: parser.h:279
A convenience class for handling scoped declarations.
Definition: symbol_table.h:48
void pushScope()
Push a scope level.
struct CVC4::options::parseOnly__option_t parseOnly
void useDeclarationsFrom(SymbolTable *symtab)
Definition: parser.h:597
const std::string & getForcedLogic() const
Definition: parser.h:280
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
virtual void warning(const std::string &msg)=0
Issue a warning to the user, with source file, line, and column info.
Class encapsulating a user-defined sort constructor.
Definition: type.h:536
SymbolType
Types of symbols.
Definition: parser.h:78
ExprStream(Parser *parser)
Definition: parser.h:617
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:589
A builder for input language parsers.
void pushScope(bool bindingLevel=false)
Definition: parser.h:549
void setInput(Input *input)
Deletes and replaces the current parser input.
Definition: parser.h:235
An input to be parsed.
Definition: input.h:86
bool canIncludeFile() const
Definition: parser.h:273
Expr nextExpr()
Get the next expression in the stream (advancing the stream pointer as a side effect.)
Definition: parser.h:619
virtual void setParser(Parser &parser)=0
Set the Parser object for this input.
void unexpectedEOF(const std::string &msg)
Unexpectedly encountered an EOF.
Definition: parser.h:520
void disableStrictMode()
Disable strict parsing.
Definition: parser.h:267
void parseError(const std::string &msg)
Raise a parse error with the given message.
Definition: parser.h:515
kind.h
void enableStrictMode()
Enable strict parsing, according to the language standards.
Definition: parser.h:263
virtual void parseError(const std::string &msg, bool eofException=false)=0
Throws a ParserException with the given message.
struct CVC4::options::out__option_t out
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
~ExprStream()
Virtual destructor; this implementation does nothing.
Definition: parser.h:618
ExprManager * getExprManager() const
Get the associated ExprManager.
Definition: parser.h:225
void popScope()
Pop a scope level.
virtual ~Parser()
Definition: parser.h:220
bool logicIsForced() const
Definition: parser.h:281
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
size_t scopeLevel() const
Gets the current declaration level.
Definition: parser.h:547
Kind_t
Definition: kind.h:60