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 /* Returns true if name is bound to a boolean variable. */
  99 bool Parser::isBoolean(const std::string& name) {
 100   return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
 101 }
 102
 103 /* Returns true if name is bound to a function-like thing (function,
 104  * constructor, tester, or selector). */
 105 bool Parser::isFunctionLike(const std::string& name) {
 106   if(!isDeclared(name, SYM_VARIABLE)) {
 107     return false;
 108   }
 109   Type type = getType(name);
 110   return type.isFunction() || type.isConstructor() ||
 111     type.isTester() || type.isSelector();
 112 }
 113
 114 /* Returns true if name is bound to a defined function. */
 115 bool Parser::isDefinedFunction(const std::string& name) {
 116   // more permissive in type than isFunction(), because defined
 117   // functions can be zero-ary and declared functions cannot.
 118   return d_declScope->isBoundDefinedFunction(name);
 119 }
 120
 121 /* Returns true if the Expr is a defined function. */
 122 bool Parser::isDefinedFunction(Expr func) {
 123   // more permissive in type than isFunction(), because defined
 124   // functions can be zero-ary and declared functions cannot.
 125   return d_declScope->isBoundDefinedFunction(func);
 126 }
 127
 128 /* Returns true if name is bound to a function returning boolean. */
 129 bool Parser::isPredicate(const std::string& name) {
 130   return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
 131 }
 132
 133 Expr
 134 Parser::mkVar(const std::string& name, const Type& type) {
 135   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
 136   Expr expr = d_exprManager->mkVar(name, type);
 137   defineVar(name, expr);
 138   return expr;
 139 }
 140
 141 Expr
 142 Parser::mkFunction(const std::string& name, const Type& type) {
 143   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
 144   Expr expr = d_exprManager->mkVar(name, type);
 145   defineFunction(name, expr);
 146   return expr;
 147 }
 148
 149 Expr
 150 Parser::mkAnonymousFunction(const std::string& prefix, const Type& type) {
 151   stringstream name;
 152   name << prefix << ':' << ++d_anonymousFunctionCount;
 153   return mkFunction(name.str(), type);
 154 }
 155
 156 std::vector<Expr>
 157 Parser::mkVars(const std::vector<std::string> names,
 158                const Type& type) {
 159   std::vector<Expr> vars;
 160   for(unsigned i = 0; i < names.size(); ++i) {
 161     vars.push_back(mkVar(names[i], type));
 162   }
 163   return vars;
 164 }
 165
 166 void
 167 Parser::defineVar(const std::string& name, const Expr& val) {
 168   d_declScope->bind(name, val);
 169   Assert( isDeclared(name) );
 170 }
 171
 172 void
 173 Parser::defineFunction(const std::string& name, const Expr& val) {
 174   d_declScope->bindDefinedFunction(name, val);
 175   Assert( isDeclared(name) );
 176 }
 177
 178 void
 179 Parser::defineType(const std::string& name, const Type& type) {
 180   d_declScope->bindType(name, type);
 181   Assert( isDeclared(name, SYM_SORT) );
 182 }
 183
 184 void
 185 Parser::defineType(const std::string& name,
 186                    const std::vector<Type>& params,
 187                    const Type& type) {
 188   d_declScope->bindType(name, params, type);
 189   Assert( isDeclared(name, SYM_SORT) );
 190 }
 191
 192 void
 193 Parser::defineParameterizedType(const std::string& name,
 194                                 const std::vector<Type>& params,
 195                                 const Type& type) {
 196   if(Debug.isOn("parser")) {
 197     Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", [";
 198     if(params.size() > 0) {
 199       copy(params.begin(), params.end() - 1,
 200            ostream_iterator<Type>(Debug("parser"), ", ") );
 201       Debug("parser") << params.back();
 202     }
 203     Debug("parser") << "], " << type << ")" << std::endl;
 204   }
 205   defineType(name, params, type);
 206 }
 207
 208 SortType
 209 Parser::mkSort(const std::string& name) {
 210   Debug("parser") << "newSort(" << name << ")" << std::endl;
 211   Type type = d_exprManager->mkSort(name);
 212   defineType(name, type);
 213   return type;
 214 }
 215
 216 SortConstructorType
 217 Parser::mkSortConstructor(const std::string& name, size_t arity) {
 218   Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
 219                   << std::endl;
 220   SortConstructorType type = d_exprManager->mkSortConstructor(name, arity);
 221   defineType(name, vector<Type>(arity), type);
 222   return type;
 223 }
 224
 225 std::vector<SortType>
 226 Parser::mkSorts(const std::vector<std::string>& names) {
 227   std::vector<SortType> types;
 228   for(unsigned i = 0; i < names.size(); ++i) {
 229     types.push_back(mkSort(names[i]));
 230   }
 231   return types;
 232 }
 233
 234 SortType Parser::mkUnresolvedType(const std::string& name) {
 235   SortType unresolved = mkSort(name);
 236   d_unresolved.insert(unresolved);
 237   return unresolved;
 238 }
 239
 240 bool Parser::isUnresolvedType(const std::string& name) {
 241   if(!isDeclared(name, SYM_SORT)) {
 242     return false;
 243   }
 244   return d_unresolved.find(getSort(name)) != d_unresolved.end();
 245 }
 246
 247 std::vector<DatatypeType>
 248 Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
 249
 250   std::vector<DatatypeType> types =
 251     d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
 252
 253   Assert(datatypes.size() == types.size());
 254
 255   for(unsigned i = 0; i < datatypes.size(); ++i) {
 256     DatatypeType t = types[i];
 257     const Datatype& dt = t.getDatatype();
 258     const std::string& name = dt.getName();
 259     Debug("parser-idt") << "define " << name << " as " << t << std::endl;
 260     if(isDeclared(name, SYM_SORT)) {
 261       throw ParserException(name + " already declared");
 262     }
 263     defineType(name, t);
 264     for(Datatype::const_iterator j = dt.begin(),
 265           j_end = dt.end();
 266         j != j_end;
 267         ++j) {
 268       const Datatype::Constructor& ctor = *j;
 269       Expr::printtypes::Scope pts(Debug("parser-idt"), true);
 270       Expr constructor = ctor.getConstructor();
 271       Debug("parser-idt") << "+ define " << constructor << std::endl;
 272       string constructorName = constructor.toString();
 273       if(isDeclared(constructorName, SYM_VARIABLE)) {
 274         throw ParserException(constructorName + " already declared");
 275       }
 276       defineVar(constructorName, constructor);
 277       Expr tester = ctor.getTester();
 278       Debug("parser-idt") << "+ define " << tester << std::endl;
 279       string testerName = tester.toString();
 280       if(isDeclared(testerName, SYM_VARIABLE)) {
 281         throw ParserException(testerName + " already declared");
 282       }
 283       defineVar(testerName, tester);
 284       for(Datatype::Constructor::const_iterator k = ctor.begin(),
 285             k_end = ctor.end();
 286           k != k_end;
 287           ++k) {
 288         Expr selector = (*k).getSelector();
 289         Debug("parser-idt") << "+++ define " << selector << std::endl;
 290         string selectorName = selector.toString();
 291         if(isDeclared(selectorName, SYM_VARIABLE)) {
 292           throw ParserException(selectorName + " already declared");
 293         }
 294         defineVar(selectorName, selector);
 295       }
 296     }
 297   }
 298
 299   // These are no longer used, and the ExprManager would have
 300   // complained of a bad substitution if anything is left unresolved.
 301   // Clear out the set.
 302   d_unresolved.clear();
 303
 304   return types;
 305 }
 306
 307 bool Parser::isDeclared(const std::string& name, SymbolType type) {
 308   switch(type) {
 309   case SYM_VARIABLE:
 310     return d_declScope->isBound(name);
 311   case SYM_SORT:
 312     return d_declScope->isBoundType(name);
 313   default:
 314     Unhandled(type);
 315   }
 316 }
 317
 318 void Parser::checkDeclaration(const std::string& varName,
 319                               DeclarationCheck check,
 320                               SymbolType type)
 321     throw(ParserException) {
 322   if(!d_checksEnabled) {
 323     return;
 324   }
 325
 326   switch(check) {
 327   case CHECK_DECLARED:
 328     if( !isDeclared(varName, type) ) {
 329       parseError("Symbol " + varName + " not declared as a " + (type == SYM_VARIABLE ? "variable" : "type"));
 330     }
 331     break;
 332
 333   case CHECK_UNDECLARED:
 334     if( isDeclared(varName, type) ) {
 335       parseError("Symbol " + varName + " previously declared as a " + (type == SYM_VARIABLE ? "variable" : "type"));
 336     }
 337     break;
 338
 339   case CHECK_NONE:
 340     break;
 341
 342   default:
 343     Unhandled(check);
 344   }
 345 }
 346
 347 void Parser::checkFunctionLike(const std::string& name) throw(ParserException) {
 348   if(d_checksEnabled && !isFunctionLike(name)) {
 349     parseError("Expecting function-like symbol, found '" + name + "'");
 350   }
 351 }
 352
 353 void Parser::checkArity(Kind kind, unsigned numArgs)
 354   throw(ParserException) {
 355   if(!d_checksEnabled) {
 356     return;
 357   }
 358
 359   unsigned min = d_exprManager->minArity(kind);
 360   unsigned max = d_exprManager->maxArity(kind);
 361
 362   if( numArgs < min || numArgs > max ) {
 363     stringstream ss;
 364     ss << "Expecting ";
 365     if( numArgs < min ) {
 366       ss << "at least " << min << " ";
 367     } else {
 368       ss << "at most " << max << " ";
 369     }
 370     ss << "arguments for operator '" << kind << "', ";
 371     ss << "found " << numArgs;
 372     parseError(ss.str());
 373   }
 374 }
 375
 376 void Parser::checkOperator(Kind kind, unsigned numArgs) throw(ParserException) {
 377   if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) {
 378     parseError( "Operator is not defined in the current logic: " + kindToString(kind) );
 379   }
 380   checkArity(kind, numArgs);
 381 }
 382
 383 void Parser::addOperator(Kind kind) {
 384   d_logicOperators.insert(kind);
 385 }
 386
 387 void Parser::preemptCommand(Command* cmd) {
 388   d_commandQueue.push_back(cmd);
 389 }
 390
 391 Command* Parser::nextCommand() throw(ParserException) {
 392   Debug("parser") << "nextCommand()" << std::endl;
 393   Command* cmd = NULL;
 394   if(!d_commandQueue.empty()) {
 395     cmd = d_commandQueue.front();
 396     d_commandQueue.pop_front();
 397     if(cmd == NULL) {
 398       setDone();
 399     }
 400   } else {
 401     if(!done()) {
 402       try {
 403         cmd = d_input->parseCommand();
 404         d_commandQueue.push_back(cmd);
 405         cmd = d_commandQueue.front();
 406         d_commandQueue.pop_front();
 407         if(cmd == NULL) {
 408           setDone();
 409         }
 410       } catch(ParserException& e) {
 411         setDone();
 412         throw;
 413       } catch(Exception& e) {
 414         setDone();
 415         stringstream ss;
 416         // set the language of the stream, otherwise if it contains
 417         // Exprs or Types it prints in the AST language
 418         OutputLanguage outlang =
 419           language::toOutputLanguage(d_input->getLanguage());
 420         ss << Expr::setlanguage(outlang) << e;
 421         parseError( ss.str() );
 422       }
 423     }
 424   }
 425   Debug("parser") << "nextCommand() => " << cmd << std::endl;
 426   return cmd;
 427 }
 428
 429 Expr Parser::nextExpression() throw(ParserException) {
 430   Debug("parser") << "nextExpression()" << std::endl;
 431   Expr result;
 432   if(!done()) {
 433     try {
 434       result = d_input->parseExpr();
 435       if(result.isNull()) {
 436         setDone();
 437       }
 438     } catch(ParserException& e) {
 439       setDone();
 440       throw;
 441     } catch(Exception& e) {
 442       setDone();
 443       stringstream ss;
 444       ss << e;
 445       parseError( ss.str() );
 446     }
 447   }
 448   Debug("parser") << "nextExpression() => " << result << std::endl;
 449   return result;
 450 }
 451
 452
 453 }/* CVC4::parser namespace */
 454 }/* CVC4 namespace */