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   return isFunction(name) && d_declScope.isBoundDefinedFunction(name);
 107 }
 108
 109 /* Returns true if name is bound to a function returning boolean. */
 110 bool Parser::isPredicate(const std::string& name) {
 111   return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
 112 }
 113
 114 Expr
 115 Parser::mkVar(const std::string& name, const Type& type) {
 116   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
 117   Expr expr = d_exprManager->mkVar(name, type);
 118   defineVar(name, expr);
 119   return expr;
 120 }
 121
 122 Expr
 123 Parser::mkFunction(const std::string& name, const Type& type) {
 124   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
 125   Expr expr = d_exprManager->mkVar(name, type);
 126   defineFunction(name, expr);
 127   return expr;
 128 }
 129
 130 const std::vector<Expr>
 131 Parser::mkVars(const std::vector<std::string> names,
 132                const Type& type) {
 133   std::vector<Expr> vars;
 134   for(unsigned i = 0; i < names.size(); ++i) {
 135     vars.push_back(mkVar(names[i], type));
 136   }
 137   return vars;
 138 }
 139
 140 void
 141 Parser::defineVar(const std::string& name, const Expr& val) {
 142   d_declScope.bind(name, val);
 143   Assert( isDeclared(name) );
 144 }
 145
 146 void
 147 Parser::defineFunction(const std::string& name, const Expr& val) {
 148   d_declScope.bindDefinedFunction(name, val);
 149   Assert( isDeclared(name) );
 150 }
 151
 152 void
 153 Parser::defineType(const std::string& name, const Type& type) {
 154   d_declScope.bindType(name, type);
 155   Assert( isDeclared(name, SYM_SORT) );
 156 }
 157
 158 void
 159 Parser::defineType(const std::string& name,
 160                    const std::vector<Type>& params,
 161                    const Type& type) {
 162   d_declScope.bindType(name, params, type);
 163   Assert( isDeclared(name, SYM_SORT) );
 164 }
 165
 166 void
 167 Parser::defineParameterizedType(const std::string& name,
 168                                 const std::vector<Type>& params,
 169                                 const Type& type) {
 170   if(Debug.isOn("parser")) {
 171     Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", [";
 172     if(params.size() > 0) {
 173       copy(params.begin(), params.end() - 1,
 174            ostream_iterator<Type>(Debug("parser"), ", ") );
 175       Debug("parser") << params.back();
 176     }
 177     Debug("parser") << "], " << type << ")" << std::endl;
 178   }
 179   defineType(name, params, type);
 180 }
 181
 182 Type
 183 Parser::mkSort(const std::string& name) {
 184   Debug("parser") << "newSort(" << name << ")" << std::endl;
 185   Type type = d_exprManager->mkSort(name);
 186   defineType(name, type);
 187   return type;
 188 }
 189
 190 Type
 191 Parser::mkSortConstructor(const std::string& name, size_t arity) {
 192   Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
 193                   << std::endl;
 194   Type type = d_exprManager->mkSortConstructor(name, arity);
 195   defineType(name, vector<Type>(arity), type);
 196   return type;
 197 }
 198
 199 const std::vector<Type>
 200 Parser::mkSorts(const std::vector<std::string>& names) {
 201   std::vector<Type> types;
 202   for(unsigned i = 0; i < names.size(); ++i) {
 203     types.push_back(mkSort(names[i]));
 204   }
 205   return types;
 206 }
 207
 208 bool Parser::isDeclared(const std::string& name, SymbolType type) {
 209   switch(type) {
 210   case SYM_VARIABLE:
 211     return d_declScope.isBound(name);
 212   case SYM_SORT:
 213     return d_declScope.isBoundType(name);
 214   default:
 215     Unhandled(type);
 216   }
 217 }
 218
 219 void Parser::checkDeclaration(const std::string& varName,
 220                                    DeclarationCheck check,
 221                                    SymbolType type)
 222     throw (ParserException) {
 223   if(!d_checksEnabled) {
 224     return;
 225   }
 226
 227   switch(check) {
 228   case CHECK_DECLARED:
 229     if( !isDeclared(varName, type) ) {
 230       parseError("Symbol " + varName + " not declared");
 231     }
 232     break;
 233
 234   case CHECK_UNDECLARED:
 235     if( isDeclared(varName, type) ) {
 236       parseError("Symbol " + varName + " previously declared");
 237     }
 238     break;
 239
 240   case CHECK_NONE:
 241     break;
 242
 243   default:
 244     Unhandled(check);
 245   }
 246 }
 247
 248 void Parser::checkFunction(const std::string& name)
 249   throw (ParserException) {
 250   if( d_checksEnabled && !isFunction(name) ) {
 251     parseError("Expecting function symbol, found '" + name + "'");
 252   }
 253 }
 254
 255 void Parser::checkArity(Kind kind, unsigned int numArgs)
 256   throw (ParserException) {
 257   if(!d_checksEnabled) {
 258     return;
 259   }
 260
 261   unsigned int min = d_exprManager->minArity(kind);
 262   unsigned int max = d_exprManager->maxArity(kind);
 263
 264   if( numArgs < min || numArgs > max ) {
 265     stringstream ss;
 266     ss << "Expecting ";
 267     if( numArgs < min ) {
 268       ss << "at least " << min << " ";
 269     } else {
 270       ss << "at most " << max << " ";
 271     }
 272     ss << "arguments for operator '" << kind << "', ";
 273     ss << "found " << numArgs;
 274     parseError(ss.str());
 275   }
 276 }
 277
 278 void Parser::checkOperator(Kind kind, unsigned int numArgs) throw (ParserException) {
 279   if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) {
 280     parseError( "Operator is not defined in the current logic: " + kindToString(kind) );
 281   }
 282   checkArity(kind, numArgs);
 283 }
 284
 285 void Parser::addOperator(Kind kind) {
 286   d_logicOperators.insert(kind);
 287 }
 288
 289 Command* Parser::nextCommand() throw(ParserException) {
 290   Debug("parser") << "nextCommand()" << std::endl;
 291   Command* cmd = NULL;
 292   if(!done()) {
 293     try {
 294       cmd = d_input->parseCommand();
 295       if(cmd == NULL) {
 296         setDone();
 297       }
 298     } catch(ParserException& e) {
 299       setDone();
 300       throw;
 301     } catch(Exception& e) {
 302       setDone();
 303       stringstream ss;
 304       ss << e;
 305       parseError( ss.str() );
 306     }
 307   }
 308   Debug("parser") << "nextCommand() => " << cmd << std::endl;
 309   return cmd;
 310 }
 311
 312 Expr Parser::nextExpression() throw(ParserException) {
 313   Debug("parser") << "nextExpression()" << std::endl;
 314   Expr result;
 315   if(!done()) {
 316     try {
 317       result = d_input->parseExpr();
 318       if(result.isNull()) {
 319         setDone();
 320       }
 321     } catch(ParserException& e) {
 322       setDone();
 323       throw;
 324     } catch(Exception& e) {
 325       setDone();
 326       stringstream ss;
 327       ss << e;
 328       parseError( ss.str() );
 329     }
 330   }
 331   Debug("parser") << "nextExpression() => " << result << std::endl;
 332   return result;
 333 }
 334
 335
 336 }/* CVC4::parser namespace */
 337 }/* CVC4 namespace */