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