src/parser/smt/smt_input.cpp

   1 /*********************                                                        */
   2 /*! \file smt_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/smt/smt_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/smt/generated/SmtLexer.h"
  27 #include "parser/smt/generated/SmtParser.h"
  28
  29 namespace CVC4 {
  30 namespace parser {
  31
  32 /* Use lookahead=2 */
  33 SmtInput::SmtInput(AntlrInputStream& inputStream) :
  34   AntlrInput(inputStream, 2) {
  35   pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
  36   AlwaysAssert( input != NULL );
  37
  38   d_pSmtLexer = SmtLexerNew(input);
  39   if( d_pSmtLexer == NULL ) {
  40     throw ParserException("Failed to create SMT lexer.");
  41   }
  42
  43   setAntlr3Lexer( d_pSmtLexer->pLexer );
  44
  45   pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
  46   AlwaysAssert( tokenStream != NULL );
  47
  48   d_pSmtParser = SmtParserNew(tokenStream);
  49   if( d_pSmtParser == NULL ) {
  50     throw ParserException("Failed to create SMT parser.");
  51   }
  52
  53   setAntlr3Parser(d_pSmtParser->pParser);
  54 }
  55
  56
  57 SmtInput::~SmtInput() {
  58   d_pSmtLexer->free(d_pSmtLexer);
  59   d_pSmtParser->free(d_pSmtParser);
  60 }
  61
  62 Command* SmtInput::parseCommand()
  63   throw (ParserException, TypeCheckingException, AssertionException) {
  64   return d_pSmtParser->parseCommand(d_pSmtParser);
  65 }
  66
  67 Expr SmtInput::parseExpr()
  68   throw (ParserException, TypeCheckingException, AssertionException) {
  69   return d_pSmtParser->parseExpr(d_pSmtParser);
  70 }
  71
  72 }/* CVC4::parser namespace */
  73 }/* CVC4 namespace */