src/parser/parser.cpp

   1 /*********************                                           -*- C++ -*-  */
   2 /** parser.cpp
   3  ** This file is part of the CVC4 prototype.
   4  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
   5  ** Courant Institute of Mathematical Sciences
   6  ** New York University
   7  ** See the file COPYING in the top-level source directory for licensing
   8  ** information.
   9  **
  10  ** Parser implementation.
  11  **/
  12
  13 #include <iostream>
  14 #include <fstream>
  15
  16 #include "parser.h"
  17 #include "util/command.h"
  18 #include "util/Assert.h"
  19 #include "parser_exception.h"
  20 #include "parser/antlr_parser.h"
  21 #include "parser/smt/generated/AntlrSmtParser.hpp"
  22 #include "parser/smt/generated/AntlrSmtLexer.hpp"
  23 #include "parser/cvc/generated/AntlrCvcParser.hpp"
  24 #include "parser/cvc/generated/AntlrCvcLexer.hpp"
  25
  26 using namespace std;
  27
  28 namespace CVC4 {
  29 namespace parser {
  30
  31 Parser::Parser(ExprManager* em) :
  32   d_expr_manager(em), d_done(false) {
  33 }
  34
  35 void Parser::setDone(bool done) {
  36   d_done = done;
  37 }
  38
  39 bool Parser::done() const {
  40   return d_done;
  41 }
  42
  43 Command* SmtParser::parseNextCommand() throw (ParserException) {
  44   Command* cmd = 0;
  45   if(!done()) {
  46     try {
  47       cmd = d_antlr_parser->benchmark();
  48       setDone();
  49     } catch(antlr::ANTLRException& e) {
  50       setDone();
  51       throw ParserException(e.toString());
  52     }
  53   }
  54   return cmd;
  55 }
  56
  57 Expr SmtParser::parseNextExpression() throw (ParserException) {
  58   Expr result;
  59   if (!done()) {
  60     try {
  61       result = d_antlr_parser->an_formula();
  62     } catch(antlr::ANTLRException& e) {
  63       setDone();
  64       throw ParserException(e.toString());
  65     }
  66   }
  67   return result;
  68 }
  69
  70 SmtParser::~SmtParser() {
  71   delete d_antlr_parser;
  72   delete d_antlr_lexer;
  73 }
  74
  75 SmtParser::SmtParser(ExprManager* em, istream& input) :
  76   Parser(em) {
  77   d_antlr_lexer = new AntlrSmtLexer(input);
  78   d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer);
  79   d_antlr_parser->setExpressionManager(d_expr_manager);
  80 }
  81
  82 SmtParser::SmtParser(ExprManager*em, const char* file_name) :
  83   Parser(em), d_input(file_name) {
  84   if(!d_input) {
  85     throw ParserException(string("File not found or inaccessible: ") + file_name);
  86   }
  87   d_antlr_lexer = new AntlrSmtLexer(d_input);
  88   d_antlr_lexer->setFilename(file_name);
  89   d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer);
  90   d_antlr_parser->setExpressionManager(d_expr_manager);
  91   d_antlr_parser->setFilename(file_name);
  92 }
  93
  94 Command* CvcParser::parseNextCommand() throw (ParserException) {
  95   Command* cmd = 0;
  96   if(!done()) {
  97     try {
  98       cmd = d_antlr_parser->command();
  99       if (cmd == 0) {
 100         setDone();
 101         cmd = new EmptyCommand("EOF");
 102       }
 103     } catch(antlr::ANTLRException& e) {
 104       setDone();
 105       throw ParserException(e.toString());
 106     }
 107   }
 108   return cmd;
 109 }
 110
 111 Expr CvcParser::parseNextExpression() throw (ParserException) {
 112   Expr result;
 113   if (!done()) {
 114     try {
 115       result = d_antlr_parser->formula();
 116     } catch(antlr::ANTLRException& e) {
 117       setDone();
 118       throw ParserException(e.toString());
 119     }
 120   }
 121   return result;
 122 }
 123
 124 CvcParser::~CvcParser() {
 125   delete d_antlr_parser;
 126   delete d_antlr_lexer;
 127 }
 128
 129 CvcParser::CvcParser(ExprManager* em, istream& input) :
 130   Parser(em) {
 131   d_antlr_lexer = new AntlrCvcLexer(input);
 132   d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer);
 133   d_antlr_parser->setExpressionManager(d_expr_manager);
 134 }
 135
 136 CvcParser::CvcParser(ExprManager*em, const char* file_name) :
 137   Parser(em), d_input(file_name) {
 138   if(!d_input) {
 139     throw ParserException(string("File not found or inaccessible: ") + file_name);
 140   }
 141   d_antlr_lexer = new AntlrCvcLexer(d_input);
 142   d_antlr_lexer->setFilename(file_name);
 143   d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer);
 144   d_antlr_parser->setExpressionManager(d_expr_manager);
 145   d_antlr_parser->setFilename(file_name);
 146 }
 147
 148
 149 }/* CVC4::parser namespace */
 150 }/* CVC4 namespace */
 151