src/parser/parser.h

   1 /*********************                                                        */
   2 /*! \file parser.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Christopher L. Conway
   6  ** Minor contributors (to current version): Dejan Jovanovic, Francois Bobot, Andrew Reynolds
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief A collection of state for use by parser implementations.
  13  **
  14  ** A collection of state for use by parser implementations.
  15  **/
  16
  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"
  28 #include "parser/parser_exception.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
  47 /** Types of check for the symols */
  48 enum DeclarationCheck {
  49   /** Enforce that the symbol has been declared */
  50   CHECK_DECLARED,
  51   /** Enforce that the symbol has not been declared */
  52   CHECK_UNDECLARED,
  53   /** Don't check anything */
  54   CHECK_NONE
  55 };/* enum DeclarationCheck */
  56
  57 /**
  58  * Returns a string representation of the given object (for
  59  * debugging).
  60  */
  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
  75 /**
  76  * Types of symbols. Used to define namespaces.
  77  */
  78 enum SymbolType {
  79   /** Variables */
  80   SYM_VARIABLE,
  81   /** Sorts */
  82   SYM_SORT
  83 };/* enum SymbolType */
  84
  85 /**
  86  * Returns a string representation of the given object (for
  87  * debugging).
  88  */
  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
 101 /**
 102  * This class encapsulates all of the state of a parser, including the
 103  * name of the file, line number and column information, and in-scope
 104  * declarations.
 105  */
 106 class CVC4_PUBLIC Parser {
 107   friend class ParserBuilder;
 108
 109   /** The expression manager */
 110   ExprManager *d_exprManager;
 111
 112   /** The input that we're parsing. */
 113   Input *d_input;
 114
 115   /**
 116    * The declaration scope that is "owned" by this parser.  May or
 117    * may not be the current declaration scope in use.
 118    */
 119   SymbolTable d_symtabAllocated;
 120
 121   /**
 122    * This current symbol table used by this parser.  Initially points
 123    * to d_symtabAllocated, but can be changed (making this parser
 124    * delegate its definitions and lookups to another parser).
 125    * See useDeclarationsFrom().
 126    */
 127   SymbolTable* d_symtab;
 128
 129   /**
 130    * The level of the assertions in the declaration scope.  Things declared
 131    * after this level are bindings from e.g. a let, a quantifier, or a
 132    * lambda.
 133    */
 134   size_t d_assertionLevel;
 135
 136   /**
 137    * Maintains a list of reserved symbols at the assertion level that might
 138    * not occur in our symbol table.  This is necessary to e.g. support the
 139    * proper behavior of the :named annotation in SMT-LIBv2 when used under
 140    * a let or a quantifier, since inside a let/quant body the declaration
 141    * scope is that of the let/quant body, but the defined name should be
 142    * reserved at the assertion level.
 143    */
 144   std::set<std::string> d_reservedSymbols;
 145
 146   /** How many anonymous functions we've created. */
 147   size_t d_anonymousFunctionCount;
 148
 149   /** Are we done */
 150   bool d_done;
 151
 152   /** Are semantic checks enabled during parsing? */
 153   bool d_checksEnabled;
 154
 155   /** Are we parsing in strict mode? */
 156   bool d_strictMode;
 157
 158   /** Are we only parsing? */
 159   bool d_parseOnly;
 160
 161   /**
 162    * Can we include files?  (Set to false for security purposes in
 163    * e.g. the online version.)
 164    */
 165   bool d_canIncludeFile;
 166
 167   /** The set of operators available in the current logic. */
 168   std::set<Kind> d_logicOperators;
 169
 170   /** The set of attributes already warned about. */
 171   std::set<std::string> d_attributesWarnedAbout;
 172
 173   /**
 174    * The current set of unresolved types.  We can get by with this NOT
 175    * being on the scope, because we can only have one DATATYPE
 176    * definition going on at one time.  This is a bit hackish; we
 177    * depend on mkMutualDatatypeTypes() to check everything and clear
 178    * this out.
 179    */
 180   std::set<Type> d_unresolved;
 181
 182   /**
 183    * "Preemption commands": extra commands implied by subterms that
 184    * should be issued before the currently-being-parsed command is
 185    * issued.  Used to support SMT-LIBv2 ":named" attribute on terms.
 186    */
 187   std::list<Command*> d_commandQueue;
 188
 189   /** Lookup a symbol in the given namespace. */
 190   Expr getSymbol(const std::string& var_name, SymbolType type);
 191
 192 protected:
 193   /**
 194    * Create a parser state.
 195    *
 196    * @attention The parser takes "ownership" of the given
 197    * input and will delete it on destruction.
 198    *
 199    * @param exprManager the expression manager to use when creating expressions
 200    * @param input the parser input
 201    * @param strictMode whether to incorporate strict(er) compliance checks
 202    * @param parseOnly whether we are parsing only (and therefore certain checks
 203    * need not be performed, like those about unimplemented features, @see
 204    * unimplementedFeature())
 205    */
 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
 214   /** Get the associated <code>ExprManager</code>. */
 215   inline ExprManager* getExprManager() const {
 216     return d_exprManager;
 217   }
 218
 219   /** Get the associated input. */
 220   inline Input* getInput() const {
 221     return d_input;
 222   }
 223
 224   /** Deletes and replaces the current parser input. */
 225   void setInput(Input* input)  {
 226     delete d_input;
 227     d_input = input;
 228     d_input->setParser(*this);
 229     d_done = false;
 230   }
 231
 232   /**
 233    * Check if we are done -- either the end of input has been reached, or some
 234    * error has been encountered.
 235    * @return true if parser is done
 236    */
 237   inline bool done() const {
 238     return d_done;
 239   }
 240
 241   /** Sets the done flag */
 242   inline void setDone(bool done = true) {
 243     d_done = done;
 244   }
 245
 246   /** Enable semantic checks during parsing. */
 247   void enableChecks() { d_checksEnabled = true; }
 248
 249   /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
 250   void disableChecks() { d_checksEnabled = false; }
 251
 252   /** Enable strict parsing, according to the language standards. */
 253   void enableStrictMode() { d_strictMode = true; }
 254
 255   /** Disable strict parsing. Allows certain syntactic infelicities to
 256       pass without comment. */
 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
 265   /**
 266    * Returns a variable, given a name.
 267    *
 268    * @param name the name of the variable
 269    * @return the variable expression
 270    */
 271   Expr getVariable(const std::string& name);
 272
 273   /**
 274    * Returns a function, given a name.
 275    *
 276    * @param name the name of the variable
 277    * @return the variable expression
 278    */
 279   Expr getFunction(const std::string& name);
 280
 281   /**
 282    * Returns a sort, given a name.
 283    * @param sort_name the name to look up
 284    */
 285   Type getSort(const std::string& sort_name);
 286
 287   /**
 288    * Returns a (parameterized) sort, given a name and args.
 289    */
 290   Type getSort(const std::string& sort_name,
 291                const std::vector<Type>& params);
 292
 293   /**
 294    * Returns arity of a (parameterized) sort, given a name and args.
 295    */
 296   size_t getArity(const std::string& sort_name);
 297
 298   /**
 299    * Checks if a symbol has been declared.
 300    * @param name the symbol name
 301    * @param type the symbol type
 302    * @return true iff the symbol has been declared with the given type
 303    */
 304   bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
 305
 306   /**
 307    * Checks if the declaration policy we want to enforce holds
 308    * for the given symbol.
 309    * @param name the symbol to check
 310    * @param check the kind of check to perform
 311    * @param type the type of the symbol
 312    * @throws ParserException if checks are enabled and the check fails
 313    */
 314   void checkDeclaration(const std::string& name, DeclarationCheck check,
 315                         SymbolType type = SYM_VARIABLE,
 316                         std::string notes = "") throw(ParserException);
 317
 318   /**
 319    * Reserve a symbol at the assertion level.
 320    */
 321   void reserveSymbolAtAssertionLevel(const std::string& name);
 322
 323   /**
 324    * Checks whether the given name is bound to a function.
 325    * @param name the name to check
 326    * @throws ParserException if checks are enabled and name is not
 327    * bound to a function
 328    */
 329   void checkFunctionLike(const std::string& name) throw(ParserException);
 330
 331   /**
 332    * Check that <code>kind</code> can accept <code>numArgs</code> arguments.
 333    * @param kind the built-in operator to check
 334    * @param numArgs the number of actual arguments
 335    * @throws ParserException if checks are enabled and the operator
 336    * <code>kind</code> cannot be applied to <code>numArgs</code>
 337    * arguments.
 338    */
 339   void checkArity(Kind kind, unsigned numArgs) throw(ParserException);
 340
 341   /**
 342    * Check that <code>kind</code> is a legal operator in the current
 343    * logic and that it can accept <code>numArgs</code> arguments.
 344    *
 345    * @param kind the built-in operator to check
 346    * @param numArgs the number of actual arguments
 347    * @throws ParserException if the parser mode is strict and the
 348    * operator <code>kind</code> has not been enabled
 349    */
 350   void checkOperator(Kind kind, unsigned numArgs) throw(ParserException);
 351
 352   /**
 353    * Returns the type for the variable with the given name.
 354    *
 355    * @param var_name the symbol to lookup
 356    * @param type the (namespace) type of the symbol
 357    */
 358   Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
 359
 360   /** Create a new CVC4 variable expression of the given type. */
 361   Expr mkVar(const std::string& name, const Type& type,
 362              uint32_t flags = ExprManager::VAR_FLAG_NONE);
 363
 364   /**
 365    * Create a set of new CVC4 variable expressions of the given type.
 366    */
 367   std::vector<Expr>
 368     mkVars(const std::vector<std::string> names, const Type& type,
 369            uint32_t flags = ExprManager::VAR_FLAG_NONE);
 370
 371   /** Create a new CVC4 bound variable expression of the given type. */
 372   Expr mkBoundVar(const std::string& name, const Type& type);
 373
 374   /**
 375    * Create a set of new CVC4 bound variable expressions of the given type.
 376    */
 377   std::vector<Expr> mkBoundVars(const std::vector<std::string> names, const Type& type);
 378
 379   /** Create a new CVC4 function expression of the given type. */
 380   Expr mkFunction(const std::string& name, const Type& type,
 381                   uint32_t flags = ExprManager::VAR_FLAG_NONE);
 382
 383   /**
 384    * Create a new CVC4 function expression of the given type,
 385    * appending a unique index to its name.  (That's the ONLY
 386    * difference between mkAnonymousFunction() and mkFunction()).
 387    */
 388   Expr mkAnonymousFunction(const std::string& prefix, const Type& type,
 389                            uint32_t flags = ExprManager::VAR_FLAG_NONE);
 390
 391   /** Create a new variable definition (e.g., from a let binding). */
 392   void defineVar(const std::string& name, const Expr& val,
 393                  bool levelZero = false);
 394
 395   /** Create a new function definition (e.g., from a define-fun). */
 396   void defineFunction(const std::string& name, const Expr& val,
 397                       bool levelZero = false);
 398
 399   /** Create a new type definition. */
 400   void defineType(const std::string& name, const Type& type);
 401
 402   /** Create a new (parameterized) type definition. */
 403   void defineType(const std::string& name,
 404                   const std::vector<Type>& params, const Type& type);
 405
 406   /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
 407   void defineParameterizedType(const std::string& name,
 408                                const std::vector<Type>& params,
 409                                const Type& type);
 410
 411   /**
 412    * Creates a new sort with the given name.
 413    */
 414   SortType mkSort(const std::string& name,
 415                   uint32_t flags = ExprManager::SORT_FLAG_NONE);
 416
 417   /**
 418    * Creates a new sort constructor with the given name and arity.
 419    */
 420   SortConstructorType mkSortConstructor(const std::string& name, size_t arity);
 421
 422   /**
 423    * Creates a new "unresolved type," used only during parsing.
 424    */
 425   SortType mkUnresolvedType(const std::string& name);
 426
 427   /**
 428    * Creates a new unresolved (parameterized) type constructor of the given
 429    * arity.
 430    */
 431   SortConstructorType mkUnresolvedTypeConstructor(const std::string& name,
 432                                                   size_t arity);
 433   /**
 434    * Creates a new unresolved (parameterized) type constructor given the type
 435    * parameters.
 436    */
 437   SortConstructorType mkUnresolvedTypeConstructor(const std::string& name,
 438                                                   const std::vector<Type>& params);
 439
 440   /**
 441    * Returns true IFF name is an unresolved type.
 442    */
 443   bool isUnresolvedType(const std::string& name);
 444
 445   /**
 446    * Create sorts of mutually-recursive datatypes.
 447    */
 448   std::vector<DatatypeType>
 449   mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
 450
 451   /**
 452    * Add an operator to the current legal set.
 453    *
 454    * @param kind the built-in operator to add
 455    */
 456   void addOperator(Kind kind);
 457
 458   /**
 459    * Preempt the next returned command with other ones; used to
 460    * support the :named attribute in SMT-LIBv2, which implicitly
 461    * inserts a new command before the current one. Also used in TPTP
 462    * because function and predicate symbols are implicitly declared.
 463    */
 464   void preemptCommand(Command* cmd);
 465
 466   /** Is the symbol bound to a boolean variable? */
 467   bool isBoolean(const std::string& name);
 468
 469   /** Is the symbol bound to a function (or function-like thing)? */
 470   bool isFunctionLike(const std::string& name);
 471
 472   /** Is the symbol bound to a defined function? */
 473   bool isDefinedFunction(const std::string& name);
 474
 475   /** Is the Expr a defined function? */
 476   bool isDefinedFunction(Expr func);
 477
 478   /** Is the symbol bound to a predicate? */
 479   bool isPredicate(const std::string& name);
 480
 481   /** Parse and return the next command. */
 482   Command* nextCommand() throw(ParserException);
 483
 484   /** Parse and return the next expression. */
 485   Expr nextExpression() throw(ParserException);
 486
 487   /** Issue a warning to the user. */
 488   inline void warning(const std::string& msg) {
 489     d_input->warning(msg);
 490   }
 491
 492   /** Issue a warning to the user, but only once per attribute. */
 493   void attributeNotSupported(const std::string& attr);
 494
 495   /** Raise a parse error with the given message. */
 496   inline void parseError(const std::string& msg) throw(ParserException) {
 497     d_input->parseError(msg);
 498   }
 499
 500   /** Unexpectedly encountered an EOF */
 501   inline void unexpectedEOF(const std::string& msg) throw(ParserException) {
 502     d_input->parseError(msg, true);
 503   }
 504
 505   /**
 506    * If we are parsing only, don't raise an exception; if we are not,
 507    * raise a parse error with the given message.  There is no actual
 508    * parse error, everything is as expected, but we cannot create the
 509    * Expr, Type, or other requested thing yet due to internal
 510    * limitations.  Even though it's not a parse error, we throw a
 511    * parse error so that the input line and column information is
 512    * available.
 513    *
 514    * Think quantifiers.  We don't have a TheoryQuantifiers yet, so we
 515    * have no kind::FORALL or kind::EXISTS.  But we might want to
 516    * support parsing quantifiers (just not doing anything with them).
 517    * So this mechanism gives you a way to do it with --parse-only.
 518    */
 519   inline void unimplementedFeature(const std::string& msg) throw(ParserException) {
 520     if(!d_parseOnly) {
 521       parseError("Unimplemented feature: " + msg);
 522     }
 523   }
 524
 525   /**
 526    * Gets the current declaration level.
 527    */
 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
 545   /**
 546    * Set the current symbol table used by this parser.
 547    * From now on, this parser will perform its definitions and
 548    * lookups in the declaration scope of the "parser" argument
 549    * (but doesn't re-delegate if the other parser's declaration scope
 550    * changes later).  A NULL argument restores this parser's
 551    * "primordial" declaration scope assigned at its creation.  Calling
 552    * p->useDeclarationsFrom(p) is a no-op.
 553    *
 554    * This feature is useful when e.g. reading out-of-band expression data:
 555    * 1. Parsing --replay log files produced with --replay-log.
 556    * 2. Perhaps a multi-query benchmark file is being single-stepped
 557    *    with intervening queries on stdin that must reference the same
 558    *    declaration scope(s).
 559    *
 560    * However, the feature must be used carefully.  Pushes and pops
 561    * should be performed with the correct current declaration scope.
 562    * Care must be taken to match up declaration scopes, of course;
 563    * If variables in the deferred-to parser go out of scope, the
 564    * secondary parser will give errors that they are undeclared.
 565    * Also, an outer-scope variable shadowed by an inner-scope one of
 566    * the same name may be temporarily inaccessible.
 567    *
 568    * In short, caveat emptor.
 569    */
 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
 586   /**
 587    * An expression stream interface for a parser.  This stream simply
 588    * pulls expressions from the given Parser object.
 589    *
 590    * Here, the ExprStream base class allows a Parser (from the parser
 591    * library) and core components of CVC4 (in the core library) to
 592    * communicate without polluting the public interface or having them
 593    * reach into private (undocumented) interfaces.
 594    */
 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 */