src/parser/parser.h

   1 /*********************                                                        */
   2 /*! \file parser.h
   3  ** \verbatim
   4  ** Original author: cconway
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): dejan, mdeters
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  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
  27 #include "input.h"
  28 #include "parser_exception.h"
  29 #include "parser_options.h"
  30 #include "expr/declaration_scope.h"
  31 #include "expr/expr.h"
  32 #include "expr/kind.h"
  33 #include "util/Assert.h"
  34
  35 namespace CVC4 {
  36
  37 // Forward declarations
  38 class BooleanType;
  39 class ExprManager;
  40 class Command;
  41 class FunctionType;
  42 class KindType;
  43 class Type;
  44
  45 namespace parser {
  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 };
  56
  57 /** Returns a string representation of the given object (for
  58  debugging). */
  59 inline std::string toString(DeclarationCheck check) {
  60   switch(check) {
  61   case CHECK_NONE:
  62     return "CHECK_NONE";
  63   case CHECK_DECLARED:
  64     return "CHECK_DECLARED";
  65   case CHECK_UNDECLARED:
  66     return "CHECK_UNDECLARED";
  67   default:
  68     Unreachable();
  69   }
  70 }
  71
  72 /**
  73  * Types of symbols. Used to define namespaces.
  74  */
  75 enum SymbolType {
  76   /** Variables */
  77   SYM_VARIABLE,
  78   /** Sorts */
  79   SYM_SORT
  80 };
  81
  82 /** Returns a string representation of the given object (for
  83  debugging). */
  84 inline std::string toString(SymbolType type) {
  85   switch(type) {
  86   case SYM_VARIABLE:
  87     return "SYM_VARIABLE";
  88   case SYM_SORT:
  89     return "SYM_SORT";
  90   default:
  91     Unreachable();
  92   }
  93 }
  94
  95 /**
  96  * This class encapsulates all of the state of a parser, including the
  97  * name of the file, line number and column information, and in-scope
  98  * declarations.
  99  */
 100 class CVC4_PUBLIC Parser {
 101   friend class ParserBuilder;
 102
 103   /** The expression manager */
 104   ExprManager *d_exprManager;
 105
 106   /** The input that we're parsing. */
 107   Input *d_input;
 108
 109   /** The symbol table */
 110   DeclarationScope d_declScope;
 111
 112   /** The name of the input file. */
 113 //  std::string d_filename;
 114
 115   /** Are we done */
 116   bool d_done;
 117
 118   /** Are semantic checks enabled during parsing? */
 119   bool d_checksEnabled;
 120
 121   /** Are we parsing in strict mode? */
 122   bool d_strictMode;
 123
 124   /** The set of operators available in the current logic. */
 125   std::set<Kind> d_logicOperators;
 126
 127   /** Lookup a symbol in the given namespace. */
 128   Expr getSymbol(const std::string& var_name, SymbolType type);
 129
 130 protected:
 131   /** Create a parser state. NOTE: The parser takes "ownership" of the given
 132    * input and will delete it on destruction.
 133    *
 134    * @param exprManager the expression manager to use when creating expressions
 135    * @param input the parser input
 136    */
 137   Parser(ExprManager* exprManager, Input* input, bool strictMode = false);
 138
 139 public:
 140
 141   virtual ~Parser() {
 142     delete d_input;
 143   }
 144
 145   /** Get the associated <code>ExprManager</code>. */
 146   inline ExprManager* getExprManager() const {
 147     return d_exprManager;
 148   }
 149
 150   /** Get the associated input. */
 151   inline Input* getInput() const {
 152     return d_input;
 153   }
 154
 155   /** Set the declaration scope manager for this input. NOTE: This should <em>only</me> be
 156    * called before parsing begins. Otherwise, previous declarations will be lost. */
 157 /*  inline void setDeclarationScope(DeclarationScope declScope) {
 158     d_declScope = declScope;
 159   }*/
 160
 161   /**
 162    * Check if we are done -- either the end of input has been reached, or some
 163    * error has been encountered.
 164    * @return true if parser is done
 165    */
 166   inline bool done() const {
 167     return d_done;
 168   }
 169
 170   /** Sets the done flag */
 171   inline void setDone(bool done = true) {
 172     d_done = done;
 173   }
 174
 175   /** Enable semantic checks during parsing. */
 176   void enableChecks() { d_checksEnabled = true; }
 177
 178   /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
 179   void disableChecks() { d_checksEnabled = false; }
 180
 181   /** Enable strict parsing, according to the language standards. */
 182   void enableStrictMode() { d_strictMode = true; }
 183
 184   /** Disable strict parsing. Allows certain syntactic infelicities to pass without comment. */
 185   void disableStrictMode() { d_strictMode = false; }
 186
 187   bool strictModeEnabled() { return d_strictMode; }
 188
 189   /**
 190    * Returns a variable, given a name.
 191    *
 192    * @param name the name of the variable
 193    * @return the variable expression
 194    */
 195   Expr getVariable(const std::string& name);
 196
 197   /**
 198    * Returns a function, given a name.
 199    *
 200    * @param var_name the name of the variable
 201    * @return the variable expression
 202    */
 203   Expr getFunction(const std::string& name);
 204
 205   /**
 206    * Returns a sort, given a name.
 207    */
 208   Type getSort(const std::string& sort_name);
 209
 210   /**
 211    * Returns a (parameterized) sort, given a name and args.
 212    */
 213   Type getSort(const std::string& sort_name,
 214                const std::vector<Type>& params);
 215
 216   /**
 217    * Checks if a symbol has been declared.
 218    * @param name the symbol name
 219    * @param type the symbol type
 220    * @return true iff the symbol has been declared with the given type
 221    */
 222   bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
 223
 224   /**
 225    * Checks if the declaration policy we want to enforce holds
 226    * for the given symbol.
 227    * @param name the symbol to check
 228    * @param check the kind of check to perform
 229    * @param type the type of the symbol
 230    * @throws ParserException if checks are enabled and the check fails
 231    */
 232   void checkDeclaration(const std::string& name, DeclarationCheck check,
 233                         SymbolType type = SYM_VARIABLE) throw (ParserException);
 234
 235   /**
 236    * Checks whether the given name is bound to a function.
 237    * @param name the name to check
 238    * @throws ParserException if checks are enabled and name is not
 239    * bound to a function
 240    */
 241   void checkFunction(const std::string& name) throw (ParserException);
 242
 243   /**
 244    * Check that <code>kind</code> can accept <code>numArgs</code> arguments.
 245    * @param kind the built-in operator to check
 246    * @param numArgs the number of actual arguments
 247    * @throws ParserException if checks are enabled and the operator
 248    * <code>kind</code> cannot be applied to <code>numArgs</code>
 249    * arguments.
 250    */
 251   void checkArity(Kind kind, unsigned int numArgs) throw (ParserException);
 252
 253   /**
 254    * Check that <code>kind</code> is a legal operator in the current
 255    * logic and that it can accept <code>numArgs</code> arguments.
 256    *
 257    * @param kind the built-in operator to check
 258    * @param numArgs the number of actual arguments
 259    * @throws ParserException if the parser mode is strict and the
 260    * operator <code>kind</kind> has not been enabled
 261    */
 262   void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException);
 263
 264   /**
 265    * Returns the type for the variable with the given name.
 266    *
 267    * @param var_name the symbol to lookup
 268    * @param type the (namespace) type of the symbol
 269    */
 270   Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
 271
 272   /** Create a new CVC4 variable expression of the given type. */
 273   Expr mkVar(const std::string& name, const Type& type);
 274
 275   /**
 276    * Create a set of new CVC4 variable expressions of the given type.
 277    */
 278   const std::vector<Expr>
 279   mkVars(const std::vector<std::string> names, const Type& type);
 280
 281   /** Create a new CVC4 function expression of the given type. */
 282   Expr mkFunction(const std::string& name, const Type& type);
 283
 284   /** Create a new variable definition (e.g., from a let binding). */
 285   void defineVar(const std::string& name, const Expr& val);
 286
 287   /** Create a new function definition (e.g., from a define-fun). */
 288   void defineFunction(const std::string& name, const Expr& val);
 289
 290   /** Create a new type definition. */
 291   void defineType(const std::string& name, const Type& type);
 292
 293   /** Create a new (parameterized) type definition. */
 294   void defineType(const std::string& name,
 295                   const std::vector<Type>& params, const Type& type);
 296
 297   /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
 298   void defineParameterizedType(const std::string& name,
 299                                const std::vector<Type>& params,
 300                                const Type& type);
 301
 302   /**
 303    * Creates a new sort with the given name.
 304    */
 305   Type mkSort(const std::string& name);
 306
 307   /**
 308    * Creates a new sort constructor with the given name and arity.
 309    */
 310   Type mkSortConstructor(const std::string& name, size_t arity);
 311
 312   /**
 313    * Creates new sorts with the given names (all of arity 0).
 314    */
 315   const std::vector<Type>
 316   mkSorts(const std::vector<std::string>& names);
 317
 318   /** Add an operator to the current legal set.
 319    *
 320    * @param kind the built-in operator to add
 321    */
 322   void addOperator(Kind kind);
 323
 324   /** Is the symbol bound to a boolean variable? */
 325   bool isBoolean(const std::string& name);
 326
 327   /** Is the symbol bound to a function? */
 328   bool isFunction(const std::string& name);
 329
 330   /** Is the symbol bound to a defined function? */
 331   bool isDefinedFunction(const std::string& name);
 332
 333   /** Is the symbol bound to a predicate? */
 334   bool isPredicate(const std::string& name);
 335
 336   Command* nextCommand() throw(ParserException);
 337   Expr nextExpression() throw(ParserException);
 338
 339   inline void parseError(const std::string& msg) throw (ParserException) {
 340     d_input->parseError(msg);
 341   }
 342
 343   inline void pushScope() { d_declScope.pushScope(); }
 344   inline void popScope() { d_declScope.popScope(); }
 345 }; // class Parser
 346
 347 } // namespace parser
 348
 349 } // namespace CVC4
 350
 351 #endif /* __CVC4__PARSER__PARSER_STATE_H */