src/parser/parser.cpp

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