src/parser/parser.cpp

   1 /*********************                                                        */
   2 /*! \file parser.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Christopher L. Conway
   6  ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Francois Bobot, Andrew Reynolds
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Parser state implementation.
  13  **
  14  ** Parser state implementation.
  15  **/
  16
  17 #include <iostream>
  18 #include <fstream>
  19 #include <sstream>
  20 #include <iterator>
  21 #include <stdint.h>
  22 #include <cassert>
  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
  34 using namespace std;
  35 using namespace CVC4::kind;
  36
  37 namespace CVC4 {
  38 namespace parser {
  39
  40 Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
  41   d_exprManager(exprManager),
  42   d_input(input),
  43   d_symtabAllocated(),
  44   d_symtab(&d_symtabAllocated),
  45   d_assertionLevel(0),
  46   d_anonymousFunctionCount(0),
  47   d_done(false),
  48   d_checksEnabled(true),
  49   d_strictMode(strictMode),
  50   d_parseOnly(parseOnly),
  51   d_canIncludeFile(true) {
  52   d_input->setParser(*this);
  53 }
  54
  55 Expr Parser::getSymbol(const std::string& name, SymbolType type) {
  56   checkDeclaration(name, CHECK_DECLARED, type);
  57   assert( isDeclared(name, type) );
  58
  59   if(type == SYM_VARIABLE) {
  60     // Functions share var namespace
  61     return d_symtab->lookup(name);
  62   }
  63
  64   assert(false);//Unhandled(type);
  65   return Expr();
  66 }
  67
  68
  69 Expr Parser::getVariable(const std::string& name) {
  70   return getSymbol(name, SYM_VARIABLE);
  71 }
  72
  73 Expr Parser::getFunction(const std::string& name) {
  74   return getSymbol(name, SYM_VARIABLE);
  75 }
  76
  77 Type Parser::getType(const std::string& var_name,
  78                      SymbolType type) {
  79   checkDeclaration(var_name, CHECK_DECLARED, 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   checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
  87   assert( isDeclared(name, SYM_SORT) );
  88   Type t = d_symtab->lookupType(name);
  89   return t;
  90 }
  91
  92 Type Parser::getSort(const std::string& name,
  93                      const std::vector<Type>& params) {
  94   checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
  95   assert( isDeclared(name, SYM_SORT) );
  96   Type t = d_symtab->lookupType(name, params);
  97   return t;
  98 }
  99
 100 size_t Parser::getArity(const std::string& sort_name){
 101   checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT);
 102   assert( isDeclared(sort_name, SYM_SORT) );
 103   return d_symtab->lookupArity(sort_name);
 104 }
 105
 106 /* Returns true if name is bound to a boolean variable. */
 107 bool Parser::isBoolean(const std::string& name) {
 108   return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
 109 }
 110
 111 /* Returns true if name is bound to a function-like thing (function,
 112  * constructor, tester, or selector). */
 113 bool Parser::isFunctionLike(const std::string& name) {
 114   if(!isDeclared(name, SYM_VARIABLE)) {
 115     return false;
 116   }
 117   Type type = getType(name);
 118   return type.isFunction() || type.isConstructor() ||
 119     type.isTester() || type.isSelector();
 120 }
 121
 122 /* Returns true if name is bound to a defined function. */
 123 bool Parser::isDefinedFunction(const std::string& name) {
 124   // more permissive in type than isFunction(), because defined
 125   // functions can be zero-ary and declared functions cannot.
 126   return d_symtab->isBoundDefinedFunction(name);
 127 }
 128
 129 /* Returns true if the Expr is a defined function. */
 130 bool Parser::isDefinedFunction(Expr func) {
 131   // more permissive in type than isFunction(), because defined
 132   // functions can be zero-ary and declared functions cannot.
 133   return d_symtab->isBoundDefinedFunction(func);
 134 }
 135
 136 /* Returns true if name is bound to a function returning boolean. */
 137 bool Parser::isPredicate(const std::string& name) {
 138   return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
 139 }
 140
 141 Expr
 142 Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) {
 143   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
 144   Expr expr = d_exprManager->mkVar(name, type, flags);
 145   defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL);
 146   return expr;
 147 }
 148
 149 Expr
 150 Parser::mkBoundVar(const std::string& name, const Type& type) {
 151   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
 152   Expr expr = d_exprManager->mkBoundVar(name, type);
 153   defineVar(name, expr, false);
 154   return expr;
 155 }
 156
 157 Expr
 158 Parser::mkFunction(const std::string& name, const Type& type, uint32_t flags) {
 159   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
 160   Expr expr = d_exprManager->mkVar(name, type, flags);
 161   defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL);
 162   return expr;
 163 }
 164
 165 Expr
 166 Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_t flags) {
 167   stringstream name;
 168   name << prefix << "_anon_" << ++d_anonymousFunctionCount;
 169   return d_exprManager->mkVar(name.str(), type, flags);
 170 }
 171
 172 std::vector<Expr>
 173 Parser::mkVars(const std::vector<std::string> names, const Type& type, uint32_t flags) {
 174   std::vector<Expr> vars;
 175   for(unsigned i = 0; i < names.size(); ++i) {
 176     vars.push_back(mkVar(names[i], type, flags));
 177   }
 178   return vars;
 179 }
 180
 181 std::vector<Expr>
 182 Parser::mkBoundVars(const std::vector<std::string> names, const Type& type) {
 183   std::vector<Expr> vars;
 184   for(unsigned i = 0; i < names.size(); ++i) {
 185     vars.push_back(mkBoundVar(names[i], type));
 186   }
 187   return vars;
 188 }
 189
 190 void
 191 Parser::defineVar(const std::string& name, const Expr& val, bool levelZero) {
 192   Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl;;
 193   d_symtab->bind(name, val, levelZero);
 194   assert( isDeclared(name) );
 195 }
 196
 197 void
 198 Parser::defineFunction(const std::string& name, const Expr& val, bool levelZero) {
 199   d_symtab->bindDefinedFunction(name, val, levelZero);
 200   assert( isDeclared(name) );
 201 }
 202
 203 void
 204 Parser::defineType(const std::string& name, const Type& type) {
 205   d_symtab->bindType(name, type);
 206   assert( isDeclared(name, SYM_SORT) );
 207 }
 208
 209 void
 210 Parser::defineType(const std::string& name,
 211                    const std::vector<Type>& params,
 212                    const Type& type) {
 213   d_symtab->bindType(name, params, type);
 214   assert( isDeclared(name, SYM_SORT) );
 215 }
 216
 217 void
 218 Parser::defineParameterizedType(const std::string& name,
 219                                 const std::vector<Type>& params,
 220                                 const Type& type) {
 221   if(Debug.isOn("parser")) {
 222     Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", [";
 223     if(params.size() > 0) {
 224       copy(params.begin(), params.end() - 1,
 225            ostream_iterator<Type>(Debug("parser"), ", ") );
 226       Debug("parser") << params.back();
 227     }
 228     Debug("parser") << "], " << type << ")" << std::endl;
 229   }
 230   defineType(name, params, type);
 231 }
 232
 233 SortType
 234 Parser::mkSort(const std::string& name) {
 235   Debug("parser") << "newSort(" << name << ")" << std::endl;
 236   Type type = d_exprManager->mkSort(name);
 237   defineType(name, type);
 238   return type;
 239 }
 240
 241 SortConstructorType
 242 Parser::mkSortConstructor(const std::string& name, size_t arity) {
 243   Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
 244                   << std::endl;
 245   SortConstructorType type = d_exprManager->mkSortConstructor(name, arity);
 246   defineType(name, vector<Type>(arity), type);
 247   return type;
 248 }
 249
 250 SortType Parser::mkUnresolvedType(const std::string& name) {
 251   SortType unresolved = mkSort(name);
 252   d_unresolved.insert(unresolved);
 253   return unresolved;
 254 }
 255
 256 SortConstructorType
 257 Parser::mkUnresolvedTypeConstructor(const std::string& name,
 258                                     size_t arity) {
 259   SortConstructorType unresolved = mkSortConstructor(name, arity);
 260   d_unresolved.insert(unresolved);
 261   return unresolved;
 262 }
 263
 264 SortConstructorType
 265 Parser::mkUnresolvedTypeConstructor(const std::string& name,
 266                                     const std::vector<Type>& params) {
 267   Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")"
 268                   << std::endl;
 269   SortConstructorType unresolved = d_exprManager->mkSortConstructor(name, params.size());
 270   defineType(name, params, unresolved);
 271   Type t = getSort( name, params );
 272   d_unresolved.insert(unresolved);
 273   return unresolved;
 274 }
 275
 276 bool Parser::isUnresolvedType(const std::string& name) {
 277   if(!isDeclared(name, SYM_SORT)) {
 278     return false;
 279   }
 280   return d_unresolved.find(getSort(name)) != d_unresolved.end();
 281 }
 282
 283 std::vector<DatatypeType>
 284 Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
 285
 286   try {
 287     std::vector<DatatypeType> types =
 288       d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
 289
 290     assert(datatypes.size() == types.size());
 291
 292     for(unsigned i = 0; i < datatypes.size(); ++i) {
 293       DatatypeType t = types[i];
 294       const Datatype& dt = t.getDatatype();
 295       const std::string& name = dt.getName();
 296       Debug("parser-idt") << "define " << name << " as " << t << std::endl;
 297       if(isDeclared(name, SYM_SORT)) {
 298         throw ParserException(name + " already declared");
 299       }
 300       if( t.isParametric() ) {
 301         std::vector< Type > paramTypes = t.getParamTypes();
 302         defineType(name, paramTypes, t );
 303       } else {
 304         defineType(name, t);
 305       }
 306       for(Datatype::const_iterator j = dt.begin(),
 307             j_end = dt.end();
 308           j != j_end;
 309           ++j) {
 310         const DatatypeConstructor& ctor = *j;
 311         Expr::printtypes::Scope pts(Debug("parser-idt"), true);
 312         Expr constructor = ctor.getConstructor();
 313         Debug("parser-idt") << "+ define " << constructor << std::endl;
 314         string constructorName = ctor.getName();
 315         if(isDeclared(constructorName, SYM_VARIABLE)) {
 316           throw ParserException(constructorName + " already declared");
 317         }
 318         defineVar(constructorName, constructor);
 319         Expr tester = ctor.getTester();
 320         Debug("parser-idt") << "+ define " << tester << std::endl;
 321         string testerName = ctor.getTesterName();
 322         if(isDeclared(testerName, SYM_VARIABLE)) {
 323           throw ParserException(testerName + " already declared");
 324         }
 325         defineVar(testerName, tester);
 326         for(DatatypeConstructor::const_iterator k = ctor.begin(),
 327               k_end = ctor.end();
 328             k != k_end;
 329             ++k) {
 330           Expr selector = (*k).getSelector();
 331           Debug("parser-idt") << "+++ define " << selector << std::endl;
 332           string selectorName = (*k).getName();
 333           if(isDeclared(selectorName, SYM_VARIABLE)) {
 334             throw ParserException(selectorName + " already declared");
 335           }
 336           defineVar(selectorName, selector);
 337         }
 338       }
 339     }
 340
 341     // These are no longer used, and the ExprManager would have
 342     // complained of a bad substitution if anything is left unresolved.
 343     // Clear out the set.
 344     d_unresolved.clear();
 345
 346     return types;
 347   } catch(IllegalArgumentException& ie) {
 348     throw ParserException(ie.getMessage());
 349   }
 350 }
 351
 352 bool Parser::isDeclared(const std::string& name, SymbolType type) {
 353   switch(type) {
 354   case SYM_VARIABLE:
 355     return d_reservedSymbols.find(name) != d_reservedSymbols.end() || d_symtab->isBound(name);
 356   case SYM_SORT:
 357     return d_symtab->isBoundType(name);
 358   }
 359   assert(false);//Unhandled(type);
 360   return false;
 361 }
 362
 363 void Parser::reserveSymbolAtAssertionLevel(const std::string& varName) {
 364   checkDeclaration(varName, CHECK_UNDECLARED, SYM_VARIABLE);
 365   d_reservedSymbols.insert(varName);
 366 }
 367
 368 void Parser::checkDeclaration(const std::string& varName,
 369                               DeclarationCheck check,
 370                               SymbolType type,
 371                               std::string notes)
 372     throw(ParserException) {
 373   if(!d_checksEnabled) {
 374     return;
 375   }
 376
 377   switch(check) {
 378   case CHECK_DECLARED:
 379     if( !isDeclared(varName, type) ) {
 380       parseError("Symbol " + varName + " not declared as a " +
 381                  (type == SYM_VARIABLE ? "variable" : "type") +
 382                  (notes.size() == 0 ? notes : "\n" + notes));
 383     }
 384     break;
 385
 386   case CHECK_UNDECLARED:
 387     if( isDeclared(varName, type) ) {
 388       parseError("Symbol " + varName + " previously declared as a " +
 389                  (type == SYM_VARIABLE ? "variable" : "type") +
 390                  (notes.size() == 0 ? notes : "\n" + notes));
 391     }
 392     break;
 393
 394   case CHECK_NONE:
 395     break;
 396
 397   default:
 398     assert(false);//Unhandled(check);
 399   }
 400 }
 401
 402 void Parser::checkFunctionLike(const std::string& name) throw(ParserException) {
 403   if(d_checksEnabled && !isFunctionLike(name)) {
 404     parseError("Expecting function-like symbol, found '" + name + "'");
 405   }
 406 }
 407
 408 void Parser::checkArity(Kind kind, unsigned numArgs)
 409   throw(ParserException) {
 410   if(!d_checksEnabled) {
 411     return;
 412   }
 413
 414   unsigned min = d_exprManager->minArity(kind);
 415   unsigned max = d_exprManager->maxArity(kind);
 416
 417   if( numArgs < min || numArgs > max ) {
 418     stringstream ss;
 419     ss << "Expecting ";
 420     if( numArgs < min ) {
 421       ss << "at least " << min << " ";
 422     } else {
 423       ss << "at most " << max << " ";
 424     }
 425     ss << "arguments for operator '" << kind << "', ";
 426     ss << "found " << numArgs;
 427     parseError(ss.str());
 428   }
 429 }
 430
 431 void Parser::checkOperator(Kind kind, unsigned numArgs) throw(ParserException) {
 432   if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) {
 433     parseError( "Operator is not defined in the current logic: " + kindToString(kind) );
 434   }
 435   checkArity(kind, numArgs);
 436 }
 437
 438 void Parser::addOperator(Kind kind) {
 439   d_logicOperators.insert(kind);
 440 }
 441
 442 void Parser::preemptCommand(Command* cmd) {
 443   d_commandQueue.push_back(cmd);
 444 }
 445
 446 Command* Parser::nextCommand() throw(ParserException) {
 447   Debug("parser") << "nextCommand()" << std::endl;
 448   Command* cmd = NULL;
 449   if(!d_commandQueue.empty()) {
 450     cmd = d_commandQueue.front();
 451     d_commandQueue.pop_front();
 452     setDone(cmd == NULL);
 453   } else {
 454     try {
 455       cmd = d_input->parseCommand();
 456       d_commandQueue.push_back(cmd);
 457       cmd = d_commandQueue.front();
 458       d_commandQueue.pop_front();
 459       setDone(cmd == NULL);
 460     } catch(ParserException& e) {
 461       setDone();
 462       throw;
 463     } catch(exception& e) {
 464       setDone();
 465       parseError(e.what());
 466     }
 467   }
 468   Debug("parser") << "nextCommand() => " << cmd << std::endl;
 469   return cmd;
 470 }
 471
 472 Expr Parser::nextExpression() throw(ParserException) {
 473   Debug("parser") << "nextExpression()" << std::endl;
 474   Expr result;
 475   if(!done()) {
 476     try {
 477       result = d_input->parseExpr();
 478       setDone(result.isNull());
 479     } catch(ParserException& e) {
 480       setDone();
 481       throw;
 482     } catch(exception& e) {
 483       setDone();
 484       parseError(e.what());
 485     }
 486   }
 487   Debug("parser") << "nextExpression() => " << result << std::endl;
 488   return result;
 489 }
 490
 491 void Parser::attributeNotSupported(const std::string& attr) {
 492   if(d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) {
 493     stringstream ss;
 494     ss << "warning: Attribute " << attr << " not supported (ignoring this and all following uses)";
 495     d_input->warning(ss.str());
 496     d_attributesWarnedAbout.insert(attr);
 497   }
 498 }
 499
 500 }/* CVC4::parser namespace */
 501 }/* CVC4 namespace */