src/parser/parser.cpp

   1 /*********************                                                        */
   2 /*! \file parser.cpp
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: mdeters, cconway
   6  ** Minor contributors (to current version): none
   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 Parser state implementation.
  15  **
  16  ** Parser state implementation.
  17  **/
  18
  19 #include <iostream>
  20 #include <fstream>
  21 #include <iterator>
  22 #include <stdint.h>
  23
  24 #include "input.h"
  25 #include "parser.h"
  26 #include "parser_exception.h"
  27 #include "expr/command.h"
  28 #include "expr/expr.h"
  29 #include "expr/kind.h"
  30 #include "expr/type.h"
  31 #include "util/output.h"
  32 #include "util/Assert.h"
  33 #include "parser/cvc/cvc_input.h"
  34 #include "parser/smt/smt_input.h"
  35
  36 using namespace std;
  37 using namespace CVC4::kind;
  38
  39 namespace CVC4 {
  40 namespace parser {
  41
  42 Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode) :
  43   d_exprManager(exprManager),
  44   d_input(input),
  45   d_done(false),
  46   d_checksEnabled(true),
  47   d_strictMode(strictMode) {
  48   d_input->setParser(*this);
  49 }
  50
  51 Expr Parser::getSymbol(const std::string& name, SymbolType type) {
  52   Assert( isDeclared(name, type) );
  53
  54   switch( type ) {
  55
  56   case SYM_VARIABLE: // Functions share var namespace
  57     return d_declScope.lookup(name);
  58
  59   default:
  60     Unhandled(type);
  61   }
  62 }
  63
  64
  65 Expr Parser::getVariable(const std::string& name) {
  66   return getSymbol(name, SYM_VARIABLE);
  67 }
  68
  69 Expr Parser::getFunction(const std::string& name) {
  70   return getSymbol(name, SYM_VARIABLE);
  71 }
  72
  73 Type
  74 Parser::getType(const std::string& var_name,
  75                      SymbolType type) {
  76   Assert( isDeclared(var_name, type) );
  77   Type t = getSymbol(var_name, type).getType();
  78   return t;
  79 }
  80
  81 Type Parser::getSort(const std::string& name) {
  82   Assert( isDeclared(name, SYM_SORT) );
  83   Type t = d_declScope.lookupType(name);
  84   return t;
  85 }
  86
  87 Type Parser::getSort(const std::string& name,
  88                      const std::vector<Type>& params) {
  89   Assert( isDeclared(name, SYM_SORT) );
  90   Type t = d_declScope.lookupType(name, params);
  91   return t;
  92 }
  93
  94 /* Returns true if name is bound to a boolean variable. */
  95 bool Parser::isBoolean(const std::string& name) {
  96   return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
  97 }
  98
  99 /* Returns true if name is bound to a function. */
 100 bool Parser::isFunction(const std::string& name) {
 101   return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction();
 102 }
 103
 104 /* Returns true if name is bound to a defined function. */
 105 bool Parser::isDefinedFunction(const std::string& name) {
 106   // more permissive in type than isFunction(), because defined
 107   // functions can be zero-ary and declared functions cannot.
 108   return d_declScope.isBoundDefinedFunction(name);
 109 }
 110
 111 /* Returns true if name is bound to a function returning boolean. */
 112 bool Parser::isPredicate(const std::string& name) {
 113   return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
 114 }
 115
 116 Expr
 117 Parser::mkVar(const std::string& name, const Type& type) {
 118   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
 119   Expr expr = d_exprManager->mkVar(name, type);
 120   defineVar(name, expr);
 121   return expr;
 122 }
 123
 124 Expr
 125 Parser::mkFunction(const std::string& name, const Type& type) {
 126   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
 127   Expr expr = d_exprManager->mkVar(name, type);
 128   defineFunction(name, expr);
 129   return expr;
 130 }
 131
 132 const std::vector<Expr>
 133 Parser::mkVars(const std::vector<std::string> names,
 134                const Type& type) {
 135   std::vector<Expr> vars;
 136   for(unsigned i = 0; i < names.size(); ++i) {
 137     vars.push_back(mkVar(names[i], type));
 138   }
 139   return vars;
 140 }
 141
 142 void
 143 Parser::defineVar(const std::string& name, const Expr& val) {
 144   d_declScope.bind(name, val);
 145   Assert( isDeclared(name) );
 146 }
 147
 148 void
 149 Parser::defineFunction(const std::string& name, const Expr& val) {
 150   d_declScope.bindDefinedFunction(name, val);
 151   Assert( isDeclared(name) );
 152 }
 153
 154 void
 155 Parser::defineType(const std::string& name, const Type& type) {
 156   d_declScope.bindType(name, type);
 157   Assert( isDeclared(name, SYM_SORT) );
 158 }
 159
 160 void
 161 Parser::defineType(const std::string& name,
 162                    const std::vector<Type>& params,
 163                    const Type& type) {
 164   d_declScope.bindType(name, params, type);
 165   Assert( isDeclared(name, SYM_SORT) );
 166 }
 167
 168 void
 169 Parser::defineParameterizedType(const std::string& name,
 170                                 const std::vector<Type>& params,
 171                                 const Type& type) {
 172   if(Debug.isOn("parser")) {
 173     Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", [";
 174     if(params.size() > 0) {
 175       copy(params.begin(), params.end() - 1,
 176            ostream_iterator<Type>(Debug("parser"), ", ") );
 177       Debug("parser") << params.back();
 178     }
 179     Debug("parser") << "], " << type << ")" << std::endl;
 180   }
 181   defineType(name, params, type);
 182 }
 183
 184 Type
 185 Parser::mkSort(const std::string& name) {
 186   Debug("parser") << "newSort(" << name << ")" << std::endl;
 187   Type type = d_exprManager->mkSort(name);
 188   defineType(name, type);
 189   return type;
 190 }
 191
 192 Type
 193 Parser::mkSortConstructor(const std::string& name, size_t arity) {
 194   Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
 195                   << std::endl;
 196   Type type = d_exprManager->mkSortConstructor(name, arity);
 197   defineType(name, vector<Type>(arity), type);
 198   return type;
 199 }
 200
 201 const std::vector<Type>
 202 Parser::mkSorts(const std::vector<std::string>& names) {
 203   std::vector<Type> types;
 204   for(unsigned i = 0; i < names.size(); ++i) {
 205     types.push_back(mkSort(names[i]));
 206   }
 207   return types;
 208 }
 209
 210 bool Parser::isDeclared(const std::string& name, SymbolType type) {
 211   switch(type) {
 212   case SYM_VARIABLE:
 213     return d_declScope.isBound(name);
 214   case SYM_SORT:
 215     return d_declScope.isBoundType(name);
 216   default:
 217     Unhandled(type);
 218   }
 219 }
 220
 221 void Parser::checkDeclaration(const std::string& varName,
 222                                    DeclarationCheck check,
 223                                    SymbolType type)
 224     throw (ParserException) {
 225   if(!d_checksEnabled) {
 226     return;
 227   }
 228
 229   switch(check) {
 230   case CHECK_DECLARED:
 231     if( !isDeclared(varName, type) ) {
 232       parseError("Symbol " + varName + " not declared");
 233     }
 234     break;
 235
 236   case CHECK_UNDECLARED:
 237     if( isDeclared(varName, type) ) {
 238       parseError("Symbol " + varName + " previously declared");
 239     }
 240     break;
 241
 242   case CHECK_NONE:
 243     break;
 244
 245   default:
 246     Unhandled(check);
 247   }
 248 }
 249
 250 void Parser::checkFunction(const std::string& name)
 251   throw (ParserException) {
 252   if( d_checksEnabled && !isFunction(name) ) {
 253     parseError("Expecting function symbol, found '" + name + "'");
 254   }
 255 }
 256
 257 void Parser::checkArity(Kind kind, unsigned int numArgs)
 258   throw (ParserException) {
 259   if(!d_checksEnabled) {
 260     return;
 261   }
 262
 263   unsigned int min = d_exprManager->minArity(kind);
 264   unsigned int max = d_exprManager->maxArity(kind);
 265
 266   if( numArgs < min || numArgs > max ) {
 267     stringstream ss;
 268     ss << "Expecting ";
 269     if( numArgs < min ) {
 270       ss << "at least " << min << " ";
 271     } else {
 272       ss << "at most " << max << " ";
 273     }
 274     ss << "arguments for operator '" << kind << "', ";
 275     ss << "found " << numArgs;
 276     parseError(ss.str());
 277   }
 278 }
 279
 280 void Parser::checkOperator(Kind kind, unsigned int numArgs) throw (ParserException) {
 281   if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) {
 282     parseError( "Operator is not defined in the current logic: " + kindToString(kind) );
 283   }
 284   checkArity(kind, numArgs);
 285 }
 286
 287 void Parser::addOperator(Kind kind) {
 288   d_logicOperators.insert(kind);
 289 }
 290
 291 void Parser::preemptCommand(Command* cmd) {
 292   d_commandQueue.push_back(cmd);
 293 }
 294
 295 Command* Parser::nextCommand() throw(ParserException) {
 296   Debug("parser") << "nextCommand()" << std::endl;
 297   Command* cmd = NULL;
 298   if(!d_commandQueue.empty()) {
 299     cmd = d_commandQueue.front();
 300     d_commandQueue.pop_front();
 301     if(cmd == NULL) {
 302       setDone();
 303     }
 304   } else {
 305     if(!done()) {
 306       try {
 307         cmd = d_input->parseCommand();
 308         d_commandQueue.push_back(cmd);
 309         cmd = d_commandQueue.front();
 310         d_commandQueue.pop_front();
 311         if(cmd == NULL) {
 312           setDone();
 313         }
 314       } catch(ParserException& e) {
 315         setDone();
 316         throw;
 317       } catch(Exception& e) {
 318         setDone();
 319         stringstream ss;
 320         ss << e;
 321         parseError( ss.str() );
 322       }
 323     }
 324   }
 325   Debug("parser") << "nextCommand() => " << cmd << std::endl;
 326   return cmd;
 327 }
 328
 329
 330 }/* CVC4::parser namespace */
 331 }/* CVC4 namespace */