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