src/parser/parser.h

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