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