src/parser/parser.cpp

   1 /*********************                                           -*- C++ -*-  */
   2 /** parser.cpp
   3  ** Original author: mdeters
   4  ** Major contributors: dejan
   5  ** Minor contributors (to current version): none
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009 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 <antlr/CharScanner.hpp>
  19
  20 #include "parser.h"
  21 #include "util/command.h"
  22 #include "util/Assert.h"
  23 #include "parser_exception.h"
  24 #include "parser/antlr_parser.h"
  25 #include "parser/smt/generated/AntlrSmtParser.hpp"
  26 #include "parser/smt/generated/AntlrSmtLexer.hpp"
  27 #include "parser/cvc/generated/AntlrCvcParser.hpp"
  28 #include "parser/cvc/generated/AntlrCvcLexer.hpp"
  29
  30 using namespace std;
  31 using namespace antlr;
  32
  33 namespace CVC4 {
  34 namespace parser {
  35
  36 void Parser::setDone(bool done) {
  37   d_done = done;
  38 }
  39
  40 bool Parser::done() const {
  41   return d_done;
  42 }
  43
  44 Command* Parser::parseNextCommand() throw(ParserException, AssertionException) {
  45   Command* cmd = NULL;
  46   if(!done()) {
  47     try {
  48       cmd = d_antlrParser->parseCommand();
  49       if (cmd == NULL) setDone();
  50     } catch(antlr::ANTLRException& e) {
  51       setDone();
  52       throw ParserException(e.toString());
  53     }
  54   }
  55   return cmd;
  56 }
  57
  58 Expr Parser::parseNextExpression() throw(ParserException, AssertionException) {
  59   Expr result;
  60   if(!done()) {
  61     try {
  62       result = d_antlrParser->parseExpr();
  63       if(result.isNull())
  64         setDone();
  65     } catch(antlr::ANTLRException& e) {
  66       setDone();
  67       throw ParserException(e.toString());
  68     }
  69   }
  70   return result;
  71 }
  72
  73 Parser::~Parser() {
  74   delete d_antlrParser;
  75   delete d_antlrLexer;
  76   if(d_deleteInput) {
  77     delete d_input;
  78   }
  79 }
  80
  81 Parser::Parser(istream* input, AntlrParser* antlrParser, CharScanner* antlrLexer, bool deleteInput) :
  82   d_done(false), d_input(input), d_antlrParser(antlrParser), d_antlrLexer(antlrLexer), d_deleteInput(deleteInput) {
  83 }
  84
  85 Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
  86                              istream* input, string filename, bool deleteInput) {
  87
  88   AntlrParser* antlrParser = 0;
  89   antlr::CharScanner* antlrLexer = 0;
  90
  91   switch(lang) {
  92   case LANG_CVC4: {
  93     antlrLexer = new AntlrCvcLexer(*input);
  94     antlrLexer->setFilename(filename);
  95     antlrParser = new AntlrCvcParser(*antlrLexer);
  96     antlrParser->setFilename(filename);
  97     antlrParser->setExpressionManager(em);
  98     break;
  99   }
 100   case LANG_SMTLIB: {
 101     antlrLexer = new AntlrSmtLexer(*input);
 102     antlrLexer->setFilename(filename);
 103     antlrParser = new AntlrSmtParser(*antlrLexer);
 104     antlrParser->setFilename(filename);
 105     antlrParser->setExpressionManager(em);
 106     break;
 107   }
 108   default:
 109     Unhandled("Unknown Input language!");
 110   }
 111
 112   return new Parser(input, antlrParser, antlrLexer, deleteInput);
 113 }
 114
 115 Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
 116                              string filename) {
 117   istream* input = new ifstream(filename.c_str());
 118   return getNewParser(em, lang, input, filename, true);
 119 }
 120
 121 Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
 122                              istream& input) {
 123   return getNewParser(em, lang, &input, "", false);
 124 }
 125
 126 }/* CVC4::parser namespace */
 127 }/* CVC4 namespace */