src/parser/parser.h

   1 /*********************                                                        */
   2 /** parser.h
   3  ** Original author: cconway
   4  ** Major contributors: none
   5  ** Minor contributors (to current version): mdeters
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** A collection of state for use by parser implementations.
  14  **/
  15
  16 #include "cvc4parser_private.h"
  17
  18 #ifndef __CVC4__PARSER__PARSER_STATE_H
  19 #define __CVC4__PARSER__PARSER_STATE_H
  20
  21 #include <string>
  22
  23 #include "input.h"
  24 #include "parser_exception.h"
  25 #include "parser_options.h"
  26 #include "expr/declaration_scope.h"
  27 #include "expr/expr.h"
  28 #include "expr/kind.h"
  29 #include "util/Assert.h"
  30
  31 namespace CVC4 {
  32
  33 // Forward declarations
  34 class BooleanType;
  35 class ExprManager;
  36 class Command;
  37 class FunctionType;
  38 class KindType;
  39 class Type;
  40
  41 namespace parser {
  42
  43 /** Types of check for the symols */
  44 enum DeclarationCheck {
  45   /** Enforce that the symbol has been declared */
  46   CHECK_DECLARED,
  47   /** Enforce that the symbol has not been declared */
  48   CHECK_UNDECLARED,
  49   /** Don't check anything */
  50   CHECK_NONE
  51 };
  52
  53 /** Returns a string representation of the given object (for
  54  debugging). */
  55 inline std::string toString(DeclarationCheck check) {
  56   switch(check) {
  57   case CHECK_NONE:
  58     return "CHECK_NONE";
  59   case CHECK_DECLARED:
  60     return "CHECK_DECLARED";
  61   case CHECK_UNDECLARED:
  62     return "CHECK_UNDECLARED";
  63   default:
  64     Unreachable();
  65   }
  66 }
  67
  68 /**
  69  * Types of symbols. Used to define namespaces.
  70  */
  71 enum SymbolType {
  72   /** Variables */
  73   SYM_VARIABLE,
  74   /** Sorts */
  75   SYM_SORT
  76 };
  77
  78 /** Returns a string representation of the given object (for
  79  debugging). */
  80 inline std::string toString(SymbolType type) {
  81   switch(type) {
  82   case SYM_VARIABLE:
  83     return "SYM_VARIABLE";
  84   case SYM_SORT:
  85     return "SYM_SORT";
  86   default:
  87     Unreachable();
  88   }
  89 }
  90
  91 /**
  92  * This class encapsulates all of the state of a parser, including the
  93  * name of the file, line number and column information, and in-scope
  94  * declarations.
  95  */
  96 class CVC4_PUBLIC Parser {
  97
  98   /** The expression manager */
  99   ExprManager *d_exprManager;
 100
 101   /** The input that we're parsing. */
 102   Input *d_input;
 103
 104   /** The symbol table */
 105   DeclarationScope d_declScope;
 106
 107   /** The name of the input file. */
 108 //  std::string d_filename;
 109
 110   /** Are we done */
 111   bool d_done;
 112
 113   /** Are semantic checks enabled during parsing? */
 114   bool d_checksEnabled;
 115
 116
 117   /** Lookup a symbol in the given namespace. */
 118   Expr getSymbol(const std::string& var_name, SymbolType type);
 119
 120 public:
 121   /** Create a parser state.
 122    *
 123    * @param exprManager the expression manager to use when creating expressions
 124    * @param input the parser input
 125    */
 126   Parser(ExprManager* exprManager, Input* input);
 127
 128   virtual ~Parser() { }
 129
 130   /** Get the associated <code>ExprManager</code>. */
 131   inline ExprManager* getExprManager() const {
 132     return d_exprManager;
 133   }
 134
 135   /** Get the associated input. */
 136   inline Input* getInput() const {
 137     return d_input;
 138   }
 139
 140   /** Set the declaration scope manager for this input. NOTE: This should <em>only</me> be
 141    * called before parsing begins. Otherwise, previous declarations will be lost. */
 142   inline void setDeclarationScope(DeclarationScope declScope) {
 143     d_declScope = declScope;
 144   }
 145
 146   /**
 147    * Check if we are done -- either the end of input has been reached, or some
 148    * error has been encountered.
 149    * @return true if parser is done
 150    */
 151   inline bool done() const {
 152     return d_done;
 153   }
 154
 155   /** Sets the done flag */
 156   inline void setDone(bool done = true) {
 157     d_done = done;
 158   }
 159
 160   /** Enable semantic checks during parsing. */
 161   void enableChecks();
 162
 163   /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
 164   void disableChecks();
 165
 166   /** Get the name of the input file. */
 167 /*
 168   inline const std::string getFilename() {
 169     return d_filename;
 170   }
 171 */
 172
 173   /**
 174    * Sets the logic for the current benchmark. Declares any logic symbols.
 175    *
 176    * @param name the name of the logic (e.g., QF_UF, AUFLIA)
 177    */
 178   void setLogic(const std::string& name);
 179
 180   /**
 181    * Returns a variable, given a name and a type.
 182    * @param var_name the name of the variable
 183    * @return the variable expression
 184    */
 185   Expr getVariable(const std::string& var_name);
 186
 187   /**
 188    * Returns a sort, given a name
 189    */
 190   Type getSort(const std::string& sort_name);
 191
 192   /**
 193    * Checks if a symbol has been declared.
 194    * @param name the symbol name
 195    * @param type the symbol type
 196    * @return true iff the symbol has been declared with the given type
 197    */
 198   bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
 199
 200   /**
 201    * Checks if the declaration policy we want to enforce holds
 202    * for the given symbol.
 203    * @param name the symbol to check
 204    * @param check the kind of check to perform
 205    * @param type the type of the symbol
 206    * @throws ParserException if checks are enabled and the check fails
 207    */
 208   void checkDeclaration(const std::string& name, DeclarationCheck check,
 209                         SymbolType type = SYM_VARIABLE) throw (ParserException);
 210
 211   /**
 212    * Checks whether the given name is bound to a function.
 213    * @param name the name to check
 214    * @throws ParserException if checks are enabled and name is not bound to a function
 215    */
 216   void checkFunction(const std::string& name) throw (ParserException);
 217
 218   /**
 219    * Check that <code>kind</code> can accept <code>numArgs</code> arguments.
 220    * @param kind the built-in operator to check
 221    * @param numArgs the number of actual arguments
 222    * @throws ParserException if checks are enabled and the operator <code>kind</code> cannot be
 223    * applied to <code>numArgs</code> arguments.
 224    */
 225   void checkArity(Kind kind, unsigned int numArgs) throw (ParserException);
 226
 227   /**
 228    * Returns the type for the variable with the given name.
 229    * @param var_name the symbol to lookup
 230    * @param type the (namespace) type of the symbol
 231    */
 232   Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
 233
 234   /** Create a new CVC4 variable expression of the given type. */
 235   Expr mkVar(const std::string& name, const Type& type);
 236
 237   /** Create a set of new CVC4 variable expressions of the given
 238    type. */
 239   const std::vector<Expr>
 240   mkVars(const std::vector<std::string> names, const Type& type);
 241
 242   /** Create a new variable definition (e.g., from a let binding). */
 243   void defineVar(const std::string& name, const Expr& val);
 244
 245   /** Create a new type definition. */
 246   void defineType(const std::string& name, const Type& type);
 247
 248   /**
 249    * Creates a new sort with the given name.
 250    */
 251   Type mkSort(const std::string& name);
 252
 253   /**
 254    * Creates a new sorts with the given names.
 255    */
 256   const std::vector<Type>
 257   mkSorts(const std::vector<std::string>& names);
 258
 259   /** Is the symbol bound to a boolean variable? */
 260   bool isBoolean(const std::string& name);
 261
 262   /** Is the symbol bound to a function? */
 263   bool isFunction(const std::string& name);
 264
 265   /** Is the symbol bound to a predicate? */
 266   bool isPredicate(const std::string& name);
 267
 268   Command* nextCommand() throw(ParserException);
 269   Expr nextExpression() throw(ParserException);
 270
 271   inline void parseError(const std::string& msg) throw (ParserException) {
 272     d_input->parseError(msg);
 273   }
 274
 275   inline void pushScope() { d_declScope.pushScope(); }
 276   inline void popScope() { d_declScope.popScope(); }
 277 }; // class Parser
 278
 279 } // namespace parser
 280
 281 } // namespace CVC4
 282
 283 #endif /* __CVC4__PARSER__PARSER_STATE_H */