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): ajreynol
   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 "parser/input.h"
  25 #include "parser/parser.h"
  26 #include "parser/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 SortType Parser::mkUnresolvedType(const std::string& name) {
 231   SortType unresolved = mkSort(name);
 232   d_unresolved.insert(unresolved);
 233   return unresolved;
 234 }
 235
 236 SortConstructorType
 237 Parser::mkUnresolvedTypeConstructor(const std::string& name,
 238                                     size_t arity) {
 239   SortConstructorType unresolved = mkSortConstructor(name,arity);
 240   d_unresolved.insert(unresolved);
 241   return unresolved;
 242 }
 243
 244 SortConstructorType
 245 Parser::mkUnresolvedTypeConstructor(const std::string& name,
 246                                     const std::vector<Type>& params) {
 247   Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")"
 248                   << std::endl;
 249   SortConstructorType unresolved = d_exprManager->mkSortConstructor(name, params.size());
 250   defineType(name, params, unresolved);
 251   Type t = getSort( name, params );
 252   d_unresolved.insert(unresolved);
 253   return unresolved;
 254 }
 255
 256 bool Parser::isUnresolvedType(const std::string& name) {
 257   if(!isDeclared(name, SYM_SORT)) {
 258     return false;
 259   }
 260   return d_unresolved.find(getSort(name)) != d_unresolved.end();
 261 }
 262
 263 std::vector<DatatypeType>
 264 Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
 265
 266   std::vector<DatatypeType> types =
 267     d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
 268
 269   Assert(datatypes.size() == types.size());
 270
 271   for(unsigned i = 0; i < datatypes.size(); ++i) {
 272     DatatypeType t = types[i];
 273     const Datatype& dt = t.getDatatype();
 274     const std::string& name = dt.getName();
 275     Debug("parser-idt") << "define " << name << " as " << t << std::endl;
 276     if(isDeclared(name, SYM_SORT)) {
 277       throw ParserException(name + " already declared");
 278     }
 279     if( t.isParametric() ) {
 280       std::vector< Type > paramTypes = t.getParamTypes();
 281       defineType(name, paramTypes, t );
 282     } else {
 283       defineType(name, t);
 284     }
 285     for(Datatype::const_iterator j = dt.begin(),
 286           j_end = dt.end();
 287         j != j_end;
 288         ++j) {
 289       const DatatypeConstructor& ctor = *j;
 290       Expr::printtypes::Scope pts(Debug("parser-idt"), true);
 291       Expr constructor = ctor.getConstructor();
 292       Debug("parser-idt") << "+ define " << constructor << std::endl;
 293       string constructorName = constructor.toString();
 294       if(isDeclared(constructorName, SYM_VARIABLE)) {
 295         throw ParserException(constructorName + " already declared");
 296       }
 297       defineVar(constructorName, constructor);
 298       Expr tester = ctor.getTester();
 299       Debug("parser-idt") << "+ define " << tester << std::endl;
 300       string testerName = tester.toString();
 301       if(isDeclared(testerName, SYM_VARIABLE)) {
 302         throw ParserException(testerName + " already declared");
 303       }
 304       defineVar(testerName, tester);
 305       for(DatatypeConstructor::const_iterator k = ctor.begin(),
 306             k_end = ctor.end();
 307           k != k_end;
 308           ++k) {
 309         Expr selector = (*k).getSelector();
 310         Debug("parser-idt") << "+++ define " << selector << std::endl;
 311         string selectorName = selector.toString();
 312         if(isDeclared(selectorName, SYM_VARIABLE)) {
 313           throw ParserException(selectorName + " already declared");
 314         }
 315         defineVar(selectorName, selector);
 316       }
 317     }
 318   }
 319
 320   // These are no longer used, and the ExprManager would have
 321   // complained of a bad substitution if anything is left unresolved.
 322   // Clear out the set.
 323   d_unresolved.clear();
 324
 325   return types;
 326 }
 327
 328 bool Parser::isDeclared(const std::string& name, SymbolType type) {
 329   switch(type) {
 330   case SYM_VARIABLE:
 331     return d_declScope->isBound(name);
 332   case SYM_SORT:
 333     return d_declScope->isBoundType(name);
 334   default:
 335     Unhandled(type);
 336   }
 337 }
 338
 339 void Parser::checkDeclaration(const std::string& varName,
 340                               DeclarationCheck check,
 341                               SymbolType type)
 342     throw(ParserException) {
 343   if(!d_checksEnabled) {
 344     return;
 345   }
 346
 347   switch(check) {
 348   case CHECK_DECLARED:
 349     if( !isDeclared(varName, type) ) {
 350       parseError("Symbol " + varName + " not declared as a " +
 351                  (type == SYM_VARIABLE ? "variable" : "type"));
 352     }
 353     break;
 354
 355   case CHECK_UNDECLARED:
 356     if( isDeclared(varName, type) ) {
 357       parseError("Symbol " + varName + " previously declared as a " +
 358                  (type == SYM_VARIABLE ? "variable" : "type"));
 359     }
 360     break;
 361
 362   case CHECK_NONE:
 363     break;
 364
 365   default:
 366     Unhandled(check);
 367   }
 368 }
 369
 370 void Parser::checkFunctionLike(const std::string& name) throw(ParserException) {
 371   if(d_checksEnabled && !isFunctionLike(name)) {
 372     parseError("Expecting function-like symbol, found '" + name + "'");
 373   }
 374 }
 375
 376 void Parser::checkArity(Kind kind, unsigned numArgs)
 377   throw(ParserException) {
 378   if(!d_checksEnabled) {
 379     return;
 380   }
 381
 382   unsigned min = d_exprManager->minArity(kind);
 383   unsigned max = d_exprManager->maxArity(kind);
 384
 385   if( numArgs < min || numArgs > max ) {
 386     stringstream ss;
 387     ss << "Expecting ";
 388     if( numArgs < min ) {
 389       ss << "at least " << min << " ";
 390     } else {
 391       ss << "at most " << max << " ";
 392     }
 393     ss << "arguments for operator '" << kind << "', ";
 394     ss << "found " << numArgs;
 395     parseError(ss.str());
 396   }
 397 }
 398
 399 void Parser::checkOperator(Kind kind, unsigned numArgs) throw(ParserException) {
 400   if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) {
 401     parseError( "Operator is not defined in the current logic: " + kindToString(kind) );
 402   }
 403   checkArity(kind, numArgs);
 404 }
 405
 406 void Parser::addOperator(Kind kind) {
 407   d_logicOperators.insert(kind);
 408 }
 409
 410 void Parser::preemptCommand(Command* cmd) {
 411   d_commandQueue.push_back(cmd);
 412 }
 413
 414 Command* Parser::nextCommand() throw(ParserException) {
 415   Debug("parser") << "nextCommand()" << std::endl;
 416   Command* cmd = NULL;
 417   if(!d_commandQueue.empty()) {
 418     cmd = d_commandQueue.front();
 419     d_commandQueue.pop_front();
 420     if(cmd == NULL) {
 421       setDone();
 422     }
 423   } else {
 424     if(!done()) {
 425       try {
 426         cmd = d_input->parseCommand();
 427         d_commandQueue.push_back(cmd);
 428         cmd = d_commandQueue.front();
 429         d_commandQueue.pop_front();
 430         if(cmd == NULL) {
 431           setDone();
 432         }
 433       } catch(ParserException& e) {
 434         setDone();
 435         throw;
 436       } catch(Exception& e) {
 437         setDone();
 438         stringstream ss;
 439         // set the language of the stream, otherwise if it contains
 440         // Exprs or Types it prints in the AST language
 441         OutputLanguage outlang =
 442           language::toOutputLanguage(d_input->getLanguage());
 443         ss << Expr::setlanguage(outlang) << e;
 444         parseError( ss.str() );
 445       }
 446     }
 447   }
 448   Debug("parser") << "nextCommand() => " << cmd << std::endl;
 449   return cmd;
 450 }
 451
 452 Expr Parser::nextExpression() throw(ParserException) {
 453   Debug("parser") << "nextExpression()" << std::endl;
 454   Expr result;
 455   if(!done()) {
 456     try {
 457       result = d_input->parseExpr();
 458       if(result.isNull()) {
 459         setDone();
 460       }
 461     } catch(ParserException& e) {
 462       setDone();
 463       throw;
 464     } catch(Exception& e) {
 465       setDone();
 466       stringstream ss;
 467       ss << e;
 468       parseError( ss.str() );
 469     }
 470   }
 471   Debug("parser") << "nextExpression() => " << result << std::endl;
 472   return result;
 473 }
 474
 475
 476 }/* CVC4::parser namespace */
 477 }/* CVC4 namespace */