src/parser/input.cpp

   1 /*********************                                                        */
   2 /** input.cpp
   3  ** Original author: dejan
   4  ** Major contributors: mdeters, cconway
   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 implementation.
  14  **/
  15
  16 #include <iostream>
  17 #include <fstream>
  18 #include <stdint.h>
  19
  20 #include "input.h"
  21 #include "expr/command.h"
  22 #include "expr/expr.h"
  23 #include "expr/kind.h"
  24 #include "expr/type.h"
  25 #include "util/output.h"
  26 #include "util/Assert.h"
  27 #include "parser/parser_exception.h"
  28 #include "parser/cvc/cvc_input.h"
  29 #include "parser/smt/smt_input.h"
  30
  31 using namespace std;
  32 using namespace CVC4::kind;
  33
  34 namespace CVC4 {
  35 namespace parser {
  36
  37 void Input::setDone(bool done) {
  38   d_done = done;
  39 }
  40
  41 bool Input::done() const {
  42   return d_done;
  43 }
  44
  45 Command* Input::parseNextCommand() throw (ParserException) {
  46   Debug("parser") << "parseNextCommand()" << std::endl;
  47   Command* cmd = NULL;
  48   if(!done()) {
  49     try {
  50       cmd = doParseCommand();
  51       if(cmd == NULL) {
  52         setDone();
  53       }
  54     } catch(ParserException& e) {
  55       setDone();
  56       throw ParserException(e.toString());
  57     }
  58   }
  59   Debug("parser") << "parseNextCommand() => " << cmd << std::endl;
  60   return cmd;
  61 }
  62
  63 Expr Input::parseNextExpression() throw (ParserException) {
  64   Debug("parser") << "parseNextExpression()" << std::endl;
  65   Expr result;
  66   if(!done()) {
  67     try {
  68       result = doParseExpr();
  69       if(result.isNull())
  70         setDone();
  71     } catch(ParserException& e) {
  72       setDone();
  73       throw ParserException(e.toString());
  74     }
  75   }
  76   Debug("parser") << "parseNextExpression() => " << result << std::endl;
  77   return result;
  78 }
  79
  80 Input::~Input() {
  81 }
  82
  83 Input::Input(ExprManager* exprManager, const std::string& filename) :
  84   d_exprManager(exprManager),
  85   d_filename(filename),
  86   d_done(false),
  87   d_checksEnabled(true) {
  88 }
  89
  90 Input* Input::newFileParser(ExprManager* em, InputLanguage lang,
  91                               const std::string& filename, bool useMmap) {
  92
  93   Input* parser = 0;
  94
  95   switch(lang) {
  96   case LANG_CVC4:
  97     parser = new CvcInput(em,filename,useMmap);
  98     break;
  99   case LANG_SMTLIB:
 100     parser = new SmtInput(em,filename,useMmap);
 101     break;
 102
 103   default:
 104     Unhandled(lang);
 105   }
 106
 107   return parser;
 108 }
 109
 110 /*
 111 Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
 112                              istream& input, string filename) {
 113   antlr::CharBuffer* inputBuffer = new CharBuffer(input);
 114   return getNewParser(em, lang, inputBuffer, filename);
 115 }
 116 */
 117
 118 /*
 119 Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
 120                              std::istream& input, const std::string& name) {
 121   Parser* parser = 0;
 122
 123   switch(lang) {
 124   case LANG_CVC4: {
 125     antlrLexer = new AntlrCvcLexer(*inputBuffer);
 126     antlrParser = new AntlrCvcParser(*antlrLexer);
 127     break;
 128   }
 129   case LANG_SMTLIB:
 130     parser = new Smt(em,input,name);
 131     break;
 132
 133   default:
 134     Unhandled("Unknown Input language!");
 135   }
 136   return parser;
 137 }
 138 */
 139
 140 Input* Input::newStringParser(ExprManager* em, InputLanguage lang,
 141                              const std::string& input, const std::string& name) {
 142   Input* parser = 0;
 143
 144   switch(lang) {
 145   case LANG_CVC4: {
 146     parser = new CvcInput(em,input,name);
 147     break;
 148   }
 149   case LANG_SMTLIB:
 150     parser = new SmtInput(em,input,name);
 151     break;
 152
 153   default:
 154     Unhandled(lang);
 155   }
 156   return parser;
 157 }
 158
 159 Expr Input::getSymbol(const std::string& name, SymbolType type) {
 160   Assert( isDeclared(name, type) );
 161
 162
 163   switch( type ) {
 164
 165   case SYM_VARIABLE: // Functions share var namespace
 166     return d_varSymbolTable.getObject(name);
 167
 168   default:
 169     Unhandled(type);
 170   }
 171 }
 172
 173
 174 Expr Input::getVariable(const std::string& name) {
 175   return getSymbol(name, SYM_VARIABLE);
 176 }
 177
 178 Type*
 179 Input::getType(const std::string& var_name,
 180                      SymbolType type) {
 181   Assert( isDeclared(var_name, type) );
 182   Type* t = getSymbol(var_name,type).getType();
 183   return t;
 184 }
 185
 186 Type* Input::getSort(const std::string& name) {
 187   Assert( isDeclared(name, SYM_SORT) );
 188   Type* t = d_sortTable.getObject(name);
 189   return t;
 190 }
 191
 192 /* Returns true if name is bound to a boolean variable. */
 193 bool Input::isBoolean(const std::string& name) {
 194   return isDeclared(name, SYM_VARIABLE) && getType(name)->isBoolean();
 195 }
 196
 197 /* Returns true if name is bound to a function. */
 198 bool Input::isFunction(const std::string& name) {
 199   return isDeclared(name, SYM_VARIABLE) && getType(name)->isFunction();
 200 }
 201
 202 /* Returns true if name is bound to a function returning boolean. */
 203 bool Input::isPredicate(const std::string& name) {
 204   return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate();
 205 }
 206
 207 Expr
 208 Input::mkVar(const std::string& name, Type* type) {
 209   Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
 210   Expr expr = d_exprManager->mkVar(type, name);
 211   defineVar(name,expr);
 212   return expr;
 213 }
 214
 215 const std::vector<Expr>
 216 Input::mkVars(const std::vector<std::string> names,
 217                     Type* type) {
 218   std::vector<Expr> vars;
 219   for(unsigned i = 0; i < names.size(); ++i) {
 220     vars.push_back(mkVar(names[i], type));
 221   }
 222   return vars;
 223 }
 224
 225 void
 226 Input::defineVar(const std::string& name, const Expr& val) {
 227   Assert(!isDeclared(name));
 228   d_varSymbolTable.bindName(name,val);
 229   Assert(isDeclared(name));
 230 }
 231
 232 void
 233 Input::undefineVar(const std::string& name) {
 234   Assert(isDeclared(name));
 235   d_varSymbolTable.unbindName(name);
 236   Assert(!isDeclared(name));
 237 }
 238
 239 void
 240 Input::setLogic(const std::string& name) {
 241   if( name == "QF_UF" ) {
 242     newSort("U");
 243   } else {
 244     Unhandled(name);
 245   }
 246 }
 247
 248 Type*
 249 Input::newSort(const std::string& name) {
 250   Debug("parser") << "newSort(" << name << ")" << std::endl;
 251   Assert( !isDeclared(name, SYM_SORT) ) ;
 252   Type* type = d_exprManager->mkSort(name);
 253   d_sortTable.bindName(name, type);
 254   Assert( isDeclared(name, SYM_SORT) ) ;
 255   return type;
 256 }
 257
 258 const std::vector<Type*>
 259 Input::newSorts(const std::vector<std::string>& names) {
 260   std::vector<Type*> types;
 261   for(unsigned i = 0; i < names.size(); ++i) {
 262     types.push_back(newSort(names[i]));
 263   }
 264   return types;
 265 }
 266
 267 bool Input::isDeclared(const std::string& name, SymbolType type) {
 268   switch(type) {
 269   case SYM_VARIABLE:
 270     return d_varSymbolTable.isBound(name);
 271   case SYM_SORT:
 272     return d_sortTable.isBound(name);
 273   default:
 274     Unhandled(type);
 275   }
 276 }
 277
 278 void Input::checkDeclaration(const std::string& varName,
 279                                    DeclarationCheck check,
 280                                    SymbolType type)
 281     throw (ParserException) {
 282   if(!d_checksEnabled) {
 283     return;
 284   }
 285
 286   switch(check) {
 287   case CHECK_DECLARED:
 288     if( !isDeclared(varName, type) ) {
 289       parseError("Symbol " + varName + " not declared");
 290     }
 291     break;
 292
 293   case CHECK_UNDECLARED:
 294     if( isDeclared(varName, type) ) {
 295       parseError("Symbol " + varName + " previously declared");
 296     }
 297     break;
 298
 299   case CHECK_NONE:
 300     break;
 301
 302   default:
 303     Unhandled(check);
 304   }
 305 }
 306
 307 void Input::checkFunction(const std::string& name)
 308   throw (ParserException) {
 309   if( d_checksEnabled && !isFunction(name) ) {
 310     parseError("Expecting function symbol, found '" + name + "'");
 311   }
 312 }
 313
 314 void Input::checkArity(Kind kind, unsigned int numArgs)
 315   throw (ParserException) {
 316   if(!d_checksEnabled) {
 317     return;
 318   }
 319
 320   unsigned int min = d_exprManager->minArity(kind);
 321   unsigned int max = d_exprManager->maxArity(kind);
 322
 323   if( numArgs < min || numArgs > max ) {
 324     stringstream ss;
 325     ss << "Expecting ";
 326     if( numArgs < min ) {
 327       ss << "at least " << min << " ";
 328     } else {
 329       ss << "at most " << max << " ";
 330     }
 331     ss << "arguments for operator '" << kind << "', ";
 332     ss << "found " << numArgs;
 333     parseError(ss.str());
 334   }
 335 }
 336
 337 void Input::enableChecks() {
 338   d_checksEnabled = true;
 339 }
 340
 341 void Input::disableChecks() {
 342   d_checksEnabled = false;
 343 }
 344
 345
 346 }/* CVC4::parser namespace */
 347 }/* CVC4 namespace */