src/parser/parser.cpp

   1 /*********************                                                        */
   2 /*! \file parser.cpp
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: mdeters, cconway
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  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 <stdint.h>
  22
  23 #include "input.h"
  24 #include "parser.h"
  25 #include "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 "util/Assert.h"
  32 #include "parser/cvc/cvc_input.h"
  33 #include "parser/smt/smt_input.h"
  34
  35 using namespace std;
  36 using namespace CVC4::kind;
  37
  38 namespace CVC4 {
  39 namespace parser {
  40
  41 Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode) :
  42   d_exprManager(exprManager),
  43   d_input(input),
  44   d_done(false),
  45   d_checksEnabled(true),
  46   d_strictMode(strictMode) {
  47   d_input->setParser(*this);
  48 }
  49
  50 Expr Parser::getSymbol(const std::string& name, SymbolType type) {
  51   Assert( isDeclared(name, type) );
  52
  53   switch( type ) {
  54
  55   case SYM_VARIABLE: // Functions share var namespace
  56     return d_declScope.lookup(name);
  57
  58   default:
  59     Unhandled(type);
  60   }
  61 }
  62
  63
  64 Expr Parser::getVariable(const std::string& name) {
  65   return getSymbol(name, SYM_VARIABLE);
  66 }
  67
  68 Type
  69 Parser::getType(const std::string& var_name,
  70                      SymbolType type) {
  71   Assert( isDeclared(var_name, type) );
  72   Type t = getSymbol(var_name,type).getType();
  73   return t;
  74 }
  75
  76 Type Parser::getSort(const std::string& name) {
  77   Assert( isDeclared(name, SYM_SORT) );
  78   Type t = d_declScope.lookupType(name);
  79   return t;
  80 }
  81
  82 /* Returns true if name is bound to a boolean variable. */
  83 bool Parser::isBoolean(const std::string& name) {
  84   return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
  85 }
  86
  87 /* Returns true if name is bound to a function. */
  88 bool Parser::isFunction(const std::string& name) {
  89   return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction();
  90 }
  91
  92 /* Returns true if name is bound to a function returning boolean. */
  93 bool Parser::isPredicate(const std::string& name) {
  94   return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
  95 }
  96
  97 Expr
  98 Parser::mkVar(const std::string& name, const Type& type) {
  99   Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl;
 100   Expr expr = d_exprManager->mkVar(name, type);
 101   defineVar(name,expr);
 102   return expr;
 103 }
 104
 105 const std::vector<Expr>
 106 Parser::mkVars(const std::vector<std::string> names,
 107                     const Type& type) {
 108   std::vector<Expr> vars;
 109   for(unsigned i = 0; i < names.size(); ++i) {
 110     vars.push_back(mkVar(names[i],type));
 111   }
 112   return vars;
 113 }
 114
 115 void
 116 Parser::defineVar(const std::string& name, const Expr& val) {
 117   d_declScope.bind(name,val);
 118   Assert(isDeclared(name));
 119 }
 120
 121 void
 122 Parser::defineType(const std::string& name, const Type& type) {
 123   d_declScope.bindType(name,type);
 124   Assert( isDeclared(name, SYM_SORT) ) ;
 125 }
 126
 127 Type
 128 Parser::mkSort(const std::string& name) {
 129   Debug("parser") << "newSort(" << name << ")" << std::endl;
 130   Type type = d_exprManager->mkSort(name);
 131   defineType(name,type);
 132   return type;
 133 }
 134
 135 const std::vector<Type>
 136 Parser::mkSorts(const std::vector<std::string>& names) {
 137   std::vector<Type> types;
 138   for(unsigned i = 0; i < names.size(); ++i) {
 139     types.push_back(mkSort(names[i]));
 140   }
 141   return types;
 142 }
 143
 144 bool Parser::isDeclared(const std::string& name, SymbolType type) {
 145   switch(type) {
 146   case SYM_VARIABLE:
 147     return d_declScope.isBound(name);
 148   case SYM_SORT:
 149     return d_declScope.isBoundType(name);
 150   default:
 151     Unhandled(type);
 152   }
 153 }
 154
 155 void Parser::checkDeclaration(const std::string& varName,
 156                                    DeclarationCheck check,
 157                                    SymbolType type)
 158     throw (ParserException) {
 159   if(!d_checksEnabled) {
 160     return;
 161   }
 162
 163   switch(check) {
 164   case CHECK_DECLARED:
 165     if( !isDeclared(varName, type) ) {
 166       parseError("Symbol " + varName + " not declared");
 167     }
 168     break;
 169
 170   case CHECK_UNDECLARED:
 171     if( isDeclared(varName, type) ) {
 172       parseError("Symbol " + varName + " previously declared");
 173     }
 174     break;
 175
 176   case CHECK_NONE:
 177     break;
 178
 179   default:
 180     Unhandled(check);
 181   }
 182 }
 183
 184 void Parser::checkFunction(const std::string& name)
 185   throw (ParserException) {
 186   if( d_checksEnabled && !isFunction(name) ) {
 187     parseError("Expecting function symbol, found '" + name + "'");
 188   }
 189 }
 190
 191 void Parser::checkArity(Kind kind, unsigned int numArgs)
 192   throw (ParserException) {
 193   if(!d_checksEnabled) {
 194     return;
 195   }
 196
 197   unsigned int min = d_exprManager->minArity(kind);
 198   unsigned int max = d_exprManager->maxArity(kind);
 199
 200   if( numArgs < min || numArgs > max ) {
 201     stringstream ss;
 202     ss << "Expecting ";
 203     if( numArgs < min ) {
 204       ss << "at least " << min << " ";
 205     } else {
 206       ss << "at most " << max << " ";
 207     }
 208     ss << "arguments for operator '" << kind << "', ";
 209     ss << "found " << numArgs;
 210     parseError(ss.str());
 211   }
 212 }
 213
 214 void Parser::checkOperator(Kind kind, unsigned int numArgs) throw (ParserException) {
 215   if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) {
 216     parseError( "Operator is not defined in the current logic: " + kindToString(kind) );
 217   }
 218   checkArity(kind,numArgs);
 219 }
 220
 221 void Parser::addOperator(Kind kind) {
 222   d_logicOperators.insert(kind);
 223 }
 224
 225 Command* Parser::nextCommand() throw(ParserException) {
 226   Debug("parser") << "nextCommand()" << std::endl;
 227   Command* cmd = NULL;
 228   if(!done()) {
 229     try {
 230       cmd = d_input->parseCommand();
 231       if(cmd == NULL) {
 232         setDone();
 233       }
 234     } catch(ParserException& e) {
 235       setDone();
 236       throw;
 237     }
 238   }
 239   Debug("parser") << "nextCommand() => " << cmd << std::endl;
 240   return cmd;
 241 }
 242
 243 Expr Parser::nextExpression() throw(ParserException) {
 244   Debug("parser") << "nextExpression()" << std::endl;
 245   Expr result;
 246   if(!done()) {
 247     try {
 248       result = d_input->parseExpr();
 249       if(result.isNull()) {
 250         setDone();
 251       }
 252     } catch(ParserException& e) {
 253       setDone();
 254       throw;
 255     }
 256   }
 257   Debug("parser") << "nextExpression() => " << result << std::endl;
 258   return result;
 259 }
 260
 261
 262 }/* CVC4::parser namespace */
 263 }/* CVC4 namespace */