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): mdeters, dejan
   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   /** Get the name of the input file. */
 190 /*
 191   inline const std::string getFilename() {
 192     return d_filename;
 193   }
 194 */
 195
 196   /**
 197    * Sets the logic for the current benchmark. Declares any logic symbols.
 198    *
 199    * @param name the name of the logic (e.g., QF_UF, AUFLIA)
 200    */
 201 //  void setLogic(const std::string& name);
 202
 203   /**
 204    * Returns a variable, given a name and a type.
 205    * @param var_name the name of the variable
 206    * @return the variable expression
 207    */
 208   Expr getVariable(const std::string& var_name);
 209
 210   /**
 211    * Returns a sort, given a name
 212    */
 213   Type getSort(const std::string& sort_name);
 214
 215   /**
 216    * Checks if a symbol has been declared.
 217    * @param name the symbol name
 218    * @param type the symbol type
 219    * @return true iff the symbol has been declared with the given type
 220    */
 221   bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
 222
 223   /**
 224    * Checks if the declaration policy we want to enforce holds
 225    * for the given symbol.
 226    * @param name the symbol to check
 227    * @param check the kind of check to perform
 228    * @param type the type of the symbol
 229    * @throws ParserException if checks are enabled and the check fails
 230    */
 231   void checkDeclaration(const std::string& name, DeclarationCheck check,
 232                         SymbolType type = SYM_VARIABLE) throw (ParserException);
 233
 234   /**
 235    * Checks whether the given name is bound to a function.
 236    * @param name the name to check
 237    * @throws ParserException if checks are enabled and name is not bound to a function
 238    */
 239   void checkFunction(const std::string& name) throw (ParserException);
 240
 241   /**
 242    * Check that <code>kind</code> can accept <code>numArgs</code> arguments.
 243    * @param kind the built-in operator to check
 244    * @param numArgs the number of actual arguments
 245    * @throws ParserException if checks are enabled and the operator <code>kind</code> cannot be
 246    * applied to <code>numArgs</code> arguments.
 247    */
 248   void checkArity(Kind kind, unsigned int numArgs) throw (ParserException);
 249
 250   /** Check that <code>kind</code> is a legal operator in the current logic and
 251    * that it can accept <code>numArgs</code> arguments.
 252    *
 253    * @param kind the built-in operator to check
 254    * @param numArgs the number of actual arguments
 255    * @throws ParserException if the parser mode is strict and the operator <code>kind</kind>
 256    * has not been enabled
 257    */
 258   void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException);
 259
 260   /**
 261    * Returns the type for the variable with the given name.
 262    * @param var_name the symbol to lookup
 263    * @param type the (namespace) type of the symbol
 264    */
 265   Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
 266
 267   /** Create a new CVC4 variable expression of the given type. */
 268   Expr mkVar(const std::string& name, const Type& type);
 269
 270   /** Create a set of new CVC4 variable expressions of the given
 271    type. */
 272   const std::vector<Expr>
 273   mkVars(const std::vector<std::string> names, const Type& type);
 274
 275   /** Create a new variable definition (e.g., from a let binding). */
 276   void defineVar(const std::string& name, const Expr& val);
 277
 278   /** Create a new type definition. */
 279   void defineType(const std::string& name, const Type& type);
 280
 281   /**
 282    * Creates a new sort with the given name.
 283    */
 284   Type mkSort(const std::string& name);
 285
 286   /**
 287    * Creates a new sorts with the given names.
 288    */
 289   const std::vector<Type>
 290   mkSorts(const std::vector<std::string>& names);
 291
 292   /** Add an operator to the current legal set.
 293    *
 294    * @param kind the built-in operator to add
 295    */
 296   void addOperator(Kind kind);
 297
 298   /** Is the symbol bound to a boolean variable? */
 299   bool isBoolean(const std::string& name);
 300
 301   /** Is the symbol bound to a function? */
 302   bool isFunction(const std::string& name);
 303
 304   /** Is the symbol bound to a predicate? */
 305   bool isPredicate(const std::string& name);
 306
 307   Command* nextCommand() throw(ParserException);
 308   Expr nextExpression() throw(ParserException);
 309
 310   inline void parseError(const std::string& msg) throw (ParserException) {
 311     d_input->parseError(msg);
 312   }
 313
 314   inline void pushScope() { d_declScope.pushScope(); }
 315   inline void popScope() { d_declScope.popScope(); }
 316 }; // class Parser
 317
 318 } // namespace parser
 319
 320 } // namespace CVC4
 321
 322 #endif /* __CVC4__PARSER__PARSER_STATE_H */