src/parser/parser.cpp

   1 /*********************                                                        */
   2 /*! \file parser.cpp
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: cconway, mdeters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  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/options.h"
  33 #include "util/Assert.h"
  34 #include "parser/cvc/cvc_input.h"
  35 #include "parser/smt/smt_input.h"
  36
  37 using namespace std;
  38 using namespace CVC4::kind;
  39
  40 namespace CVC4 {
  41 namespace parser {
  42
  43 Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
  44   d_exprManager(exprManager),
  45   d_input(input),
  46   d_declScopeAllocated(),
  47   d_declScope(&d_declScopeAllocated),
  48   d_anonymousFunctionCount(0),
  49   d_done(false),
  50   d_checksEnabled(true),
  51   d_strictMode(strictMode),
  52   d_parseOnly(parseOnly) {
  53   d_input->setParser(*this);
  54 }
  55
  56 Expr Parser::getSymbol(const std::string& name, SymbolType type) {
  57   Assert( isDeclared(name, type) );
  58
  59   switch( type ) {
  60
  61   case SYM_VARIABLE: // Functions share var namespace
  62     return d_declScope->lookup(name);
  63
  64   default:
  65     Unhandled(type);
  66   }
  67 }
  68
  69
  70 Expr Parser::getVariable(const std::string& name) {
  71   return getSymbol(name, SYM_VARIABLE);
  72 }
  73
  74 Expr Parser::getFunction(const std::string& name) {
  75   return getSymbol(name, SYM_VARIABLE);
  76 }
  77
  78 Type Parser::getType(const std::string& var_name,
  79                      SymbolType type) {
  80   Assert( isDeclared(var_name, type) );
  81   Type t = getSymbol(var_name, type).getType();
  82   return t;
  83 }
  84
  85 Type Parser::getSort(const std::string& name) {
  86   Assert( isDeclared(name, SYM_SORT) );
  87   Type t = d_declScope->lookupType(name);
  88   return t;
  89 }
  90
  91 Type Parser::getSort(const std::string& name,
  92                      const std::vector<Type>& params) {
  93   Assert( isDeclared(name, SYM_SORT) );
  94   Type t = d_declScope->lookupType(name, params);
  95   return t;
  96 }
  97
  98 size_t Parser::getArity(const std::string& sort_name){
  99   Assert( isDeclared(sort_name, SYM_SORT) );
 100   return d_declScope->lookupArity(sort_name);
 101 }
 102
 103 /* Returns true if name is bound to a boolean variable. */
 104 bool Parser::isBoolean(const std::string& name) {
 105   return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
 106 }
 107
 108 /* Returns true if name is bound to a function-like thing (function,
 109  * constructor, tester, or selector). */
 110 bool Parser::isFunctionLike(const std::string& name) {
 111   if(!isDeclared(name, SYM_VARIABLE)) {
 112     return false;
 113   }
 114   Type type = getType(name);
 115   return type.isFunction() || type.isConstructor() ||
 116     type.isTester() || type.isSelector();
 117 }
 118
 119 /* Returns true if name is bound to a defined function. */
 120 bool Parser::isDefinedFunction(const std::string& name) {
 121   // more permissive in type than isFunction(), because defined
 122   // functions can be zero-ary and declared functions cannot.
 123   return d_declScope->isBoundDefinedFunction(name);
 124 }
 125
 126 /* Returns true if the Expr is a defined function. */
 127 bool Parser::isDefinedFunction(Expr func) {
 128   // more permissive in type than isFunction(), because defined
 129   // functions can be zero-ary and declared functions cannot.
 130   return d_declScope->isBoundDefinedFunction(func);
 131 }
 132
 133 /* Returns true if name is bound to a function returning boolean. */
 134 bool Parser::isPredicate(const std::string& name) {
 135   return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
 136 }
 137
 138 Expr
 139 Parser::mkVar(const std::string& name, const Type& type) {
 140   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
 141   Expr expr = d_exprManager->mkVar(name, type);
 142   defineVar(name, expr);
 143   return expr;
 144 }
 145
 146 Expr
 147 Parser::mkFunction(const std::string& name, const Type& type) {
 148   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
 149   Expr expr = d_exprManager->mkVar(name, type);
 150   defineFunction(name, expr);
 151   return expr;
 152 }
 153
 154 Expr
 155 Parser::mkAnonymousFunction(const std::string& prefix, const Type& type) {
 156   stringstream name;
 157   name << prefix << ':' << ++d_anonymousFunctionCount;
 158   return mkFunction(name.str(), type);
 159 }
 160
 161 std::vector<Expr>
 162 Parser::mkVars(const std::vector<std::string> names,
 163                const Type& type) {
 164   std::vector<Expr> vars;
 165   for(unsigned i = 0; i < names.size(); ++i) {
 166     vars.push_back(mkVar(names[i], type));
 167   }
 168   return vars;
 169 }
 170
 171 void
 172 Parser::defineVar(const std::string& name, const Expr& val) {
 173   d_declScope->bind(name, val);
 174   Assert( isDeclared(name) );
 175 }
 176
 177 void
 178 Parser::defineFunction(const std::string& name, const Expr& val) {
 179   d_declScope->bindDefinedFunction(name, val);
 180   Assert( isDeclared(name) );
 181 }
 182
 183 void
 184 Parser::defineType(const std::string& name, const Type& type) {
 185   d_declScope->bindType(name, type);
 186   Assert( isDeclared(name, SYM_SORT) );
 187 }
 188
 189 void
 190 Parser::defineType(const std::string& name,
 191                    const std::vector<Type>& params,
 192                    const Type& type) {
 193   d_declScope->bindType(name, params, type);
 194   Assert( isDeclared(name, SYM_SORT) );
 195 }
 196
 197 void
 198 Parser::defineParameterizedType(const std::string& name,
 199                                 const std::vector<Type>& params,
 200                                 const Type& type) {
 201   if(Debug.isOn("parser")) {
 202     Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", [";
 203     if(params.size() > 0) {
 204       copy(params.begin(), params.end() - 1,
 205            ostream_iterator<Type>(Debug("parser"), ", ") );
 206       Debug("parser") << params.back();
 207     }
 208     Debug("parser") << "], " << type << ")" << std::endl;
 209   }
 210   defineType(name, params, type);
 211 }
 212
 213 SortType
 214 Parser::mkSort(const std::string& name) {
 215   Debug("parser") << "newSort(" << name << ")" << std::endl;
 216   Type type = d_exprManager->mkSort(name);
 217   defineType(name, type);
 218   return type;
 219 }
 220
 221 SortConstructorType
 222 Parser::mkSortConstructor(const std::string& name, size_t arity) {
 223   Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
 224                   << std::endl;
 225   SortConstructorType type = d_exprManager->mkSortConstructor(name, arity);
 226   defineType(name, vector<Type>(arity), type);
 227   return type;
 228 }
 229
 230 std::vector<SortType>
 231 Parser::mkSorts(const std::vector<std::string>& names) {
 232   std::vector<SortType> types;
 233   for(unsigned i = 0; i < names.size(); ++i) {
 234     types.push_back(mkSort(names[i]));
 235   }
 236   return types;
 237 }
 238
 239 SortType Parser::mkUnresolvedType(const std::string& name) {
 240   SortType unresolved = mkSort(name);
 241   d_unresolved.insert(unresolved);
 242   return unresolved;
 243 }
 244
 245 SortConstructorType
 246 Parser::mkUnresolvedTypeConstructor(const std::string& name,
 247                                     size_t arity) {
 248   SortConstructorType unresolved = mkSortConstructor(name,arity);
 249   d_unresolved.insert(unresolved);
 250   return unresolved;
 251 }
 252
 253 SortConstructorType
 254 Parser::mkUnresolvedTypeConstructor(const std::string& name,
 255                                     const std::vector<Type>& params) {
 256   Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")"
 257                   << std::endl;
 258   SortConstructorType unresolved = d_exprManager->mkSortConstructor(name, params.size());
 259   defineType(name, params, unresolved);
 260   Type t = getSort( name, params );
 261   d_unresolved.insert(unresolved);
 262   return unresolved;
 263 }
 264
 265 bool Parser::isUnresolvedType(const std::string& name) {
 266   if(!isDeclared(name, SYM_SORT)) {
 267     return false;
 268   }
 269   return d_unresolved.find(getSort(name)) != d_unresolved.end();
 270 }
 271
 272 std::vector<DatatypeType>
 273 Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
 274
 275   std::vector<DatatypeType> types =
 276     d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
 277
 278   Assert(datatypes.size() == types.size());
 279
 280   for(unsigned i = 0; i < datatypes.size(); ++i) {
 281     DatatypeType t = types[i];
 282     const Datatype& dt = t.getDatatype();
 283     const std::string& name = dt.getName();
 284     Debug("parser-idt") << "define " << name << " as " << t << std::endl;
 285     if(isDeclared(name, SYM_SORT)) {
 286       throw ParserException(name + " already declared");
 287     }
 288     if( t.isParametric() ) {
 289       std::vector< Type > paramTypes = t.getParamTypes();
 290       defineType(name, paramTypes, t );
 291     } else {
 292       defineType(name, t);
 293     }
 294     for(Datatype::const_iterator j = dt.begin(),
 295           j_end = dt.end();
 296         j != j_end;
 297         ++j) {
 298       const Datatype::Constructor& ctor = *j;
 299       Expr::printtypes::Scope pts(Debug("parser-idt"), true);
 300       Expr constructor = ctor.getConstructor();
 301       Debug("parser-idt") << "+ define " << constructor << std::endl;
 302       string constructorName = constructor.toString();
 303       if(isDeclared(constructorName, SYM_VARIABLE)) {
 304         throw ParserException(constructorName + " already declared");
 305       }
 306       defineVar(constructorName, constructor);
 307       Expr tester = ctor.getTester();
 308       Debug("parser-idt") << "+ define " << tester << std::endl;
 309       string testerName = tester.toString();
 310       if(isDeclared(testerName, SYM_VARIABLE)) {
 311         throw ParserException(testerName + " already declared");
 312       }
 313       defineVar(testerName, tester);
 314       for(Datatype::Constructor::const_iterator k = ctor.begin(),
 315             k_end = ctor.end();
 316           k != k_end;
 317           ++k) {
 318         Expr selector = (*k).getSelector();
 319         Debug("parser-idt") << "+++ define " << selector << std::endl;
 320         string selectorName = selector.toString();
 321         if(isDeclared(selectorName, SYM_VARIABLE)) {
 322           throw ParserException(selectorName + " already declared");
 323         }
 324         defineVar(selectorName, selector);
 325       }
 326     }
 327   }
 328
 329   // These are no longer used, and the ExprManager would have
 330   // complained of a bad substitution if anything is left unresolved.
 331   // Clear out the set.
 332   d_unresolved.clear();
 333
 334   return types;
 335 }
 336
 337 bool Parser::isDeclared(const std::string& name, SymbolType type) {
 338   switch(type) {
 339   case SYM_VARIABLE:
 340     return d_declScope->isBound(name);
 341   case SYM_SORT:
 342     return d_declScope->isBoundType(name);
 343   default:
 344     Unhandled(type);
 345   }
 346 }
 347
 348 void Parser::checkDeclaration(const std::string& varName,
 349                               DeclarationCheck check,
 350                               SymbolType type)
 351     throw(ParserException) {
 352   if(!d_checksEnabled) {
 353     return;
 354   }
 355
 356   switch(check) {
 357   case CHECK_DECLARED:
 358     if( !isDeclared(varName, type) ) {
 359       parseError("Symbol " + varName + " not declared as a " + (type == SYM_VARIABLE ? "variable" : "type"));
 360     }
 361     break;
 362
 363   case CHECK_UNDECLARED:
 364     if( isDeclared(varName, type) ) {
 365       parseError("Symbol " + varName + " previously declared as a " + (type == SYM_VARIABLE ? "variable" : "type"));
 366     }
 367     break;
 368
 369   case CHECK_NONE:
 370     break;
 371
 372   default:
 373     Unhandled(check);
 374   }
 375 }
 376
 377 void Parser::checkFunctionLike(const std::string& name) throw(ParserException) {
 378   if(d_checksEnabled && !isFunctionLike(name)) {
 379     parseError("Expecting function-like symbol, found '" + name + "'");
 380   }
 381 }
 382
 383 void Parser::checkArity(Kind kind, unsigned numArgs)
 384   throw(ParserException) {
 385   if(!d_checksEnabled) {
 386     return;
 387   }
 388
 389   unsigned min = d_exprManager->minArity(kind);
 390   unsigned max = d_exprManager->maxArity(kind);
 391
 392   if( numArgs < min || numArgs > max ) {
 393     stringstream ss;
 394     ss << "Expecting ";
 395     if( numArgs < min ) {
 396       ss << "at least " << min << " ";
 397     } else {
 398       ss << "at most " << max << " ";
 399     }
 400     ss << "arguments for operator '" << kind << "', ";
 401     ss << "found " << numArgs;
 402     parseError(ss.str());
 403   }
 404 }
 405
 406 void Parser::checkOperator(Kind kind, unsigned numArgs) throw(ParserException) {
 407   if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) {
 408     parseError( "Operator is not defined in the current logic: " + kindToString(kind) );
 409   }
 410   checkArity(kind, numArgs);
 411 }
 412
 413 void Parser::addOperator(Kind kind) {
 414   d_logicOperators.insert(kind);
 415 }
 416
 417 void Parser::preemptCommand(Command* cmd) {
 418   d_commandQueue.push_back(cmd);
 419 }
 420
 421 Command* Parser::nextCommand() throw(ParserException) {
 422   Debug("parser") << "nextCommand()" << std::endl;
 423   Command* cmd = NULL;
 424   if(!d_commandQueue.empty()) {
 425     cmd = d_commandQueue.front();
 426     d_commandQueue.pop_front();
 427     if(cmd == NULL) {
 428       setDone();
 429     }
 430   } else {
 431     if(!done()) {
 432       try {
 433         cmd = d_input->parseCommand();
 434         d_commandQueue.push_back(cmd);
 435         cmd = d_commandQueue.front();
 436         d_commandQueue.pop_front();
 437         if(cmd == NULL) {
 438           setDone();
 439         }
 440       } catch(ParserException& e) {
 441         setDone();
 442         throw;
 443       } catch(Exception& e) {
 444         setDone();
 445         stringstream ss;
 446         // set the language of the stream, otherwise if it contains
 447         // Exprs or Types it prints in the AST language
 448         OutputLanguage outlang =
 449           language::toOutputLanguage(d_input->getLanguage());
 450         ss << Expr::setlanguage(outlang) << e;
 451         parseError( ss.str() );
 452       }
 453     }
 454   }
 455   Debug("parser") << "nextCommand() => " << cmd << std::endl;
 456   return cmd;
 457 }
 458
 459 Expr Parser::nextExpression() throw(ParserException) {
 460   Debug("parser") << "nextExpression()" << std::endl;
 461   Expr result;
 462   if(!done()) {
 463     try {
 464       result = d_input->parseExpr();
 465       if(result.isNull()) {
 466         setDone();
 467       }
 468     } catch(ParserException& e) {
 469       setDone();
 470       throw;
 471     } catch(Exception& e) {
 472       setDone();
 473       stringstream ss;
 474       ss << e;
 475       parseError( ss.str() );
 476     }
 477   }
 478   Debug("parser") << "nextExpression() => " << result << std::endl;
 479   return result;
 480 }
 481
 482
 483 }/* CVC4::parser namespace */
 484 }/* CVC4 namespace */