src/parser/smt1/smt1_input.cpp

   1 /*********************                                                        */
   2 /*! \file smt1_input.cpp
   3  ** \verbatim
   4  ** Original author: cconway
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  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 [[ Add file-specific comments here ]].
  15  **
  16  ** [[ Add file-specific comments here ]]
  17  **/
  18
  19 #include <antlr3.h>
  20
  21 #include "parser/smt1/smt1_input.h"
  22 #include "expr/expr_manager.h"
  23 #include "parser/input.h"
  24 #include "parser/parser.h"
  25 #include "parser/parser_exception.h"
  26 #include "parser/smt1/generated/Smt1Lexer.h"
  27 #include "parser/smt1/generated/Smt1Parser.h"
  28
  29 namespace CVC4 {
  30 namespace parser {
  31
  32 /* Use lookahead=2 */
  33 Smt1Input::Smt1Input(AntlrInputStream& inputStream) :
  34   AntlrInput(inputStream, 2) {
  35   pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
  36   assert( input != NULL );
  37
  38   d_pSmt1Lexer = Smt1LexerNew(input);
  39   if( d_pSmt1Lexer == NULL ) {
  40     throw ParserException("Failed to create SMT lexer.");
  41   }
  42
  43   setAntlr3Lexer( d_pSmt1Lexer->pLexer );
  44
  45   pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
  46   assert( tokenStream != NULL );
  47
  48   d_pSmt1Parser = Smt1ParserNew(tokenStream);
  49   if( d_pSmt1Parser == NULL ) {
  50     throw ParserException("Failed to create SMT parser.");
  51   }
  52
  53   setAntlr3Parser(d_pSmt1Parser->pParser);
  54 }
  55
  56
  57 Smt1Input::~Smt1Input() {
  58   d_pSmt1Lexer->free(d_pSmt1Lexer);
  59   d_pSmt1Parser->free(d_pSmt1Parser);
  60 }
  61
  62 Command* Smt1Input::parseCommand()
  63   throw (ParserException, TypeCheckingException) {
  64   return d_pSmt1Parser->parseCommand(d_pSmt1Parser);
  65 }
  66
  67 Expr Smt1Input::parseExpr()
  68   throw (ParserException, TypeCheckingException) {
  69   return d_pSmt1Parser->parseExpr(d_pSmt1Parser);
  70 }
  71
  72 }/* CVC4::parser namespace */
  73 }/* CVC4 namespace */