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