src/parser/smt/smt_input.h

   1 /*********************                                                        */
   2 /*! \file smt_input.h
   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  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 "cvc4parser_private.h"
  20
  21 #ifndef __CVC4__PARSER__SMT_INPUT_H
  22 #define __CVC4__PARSER__SMT_INPUT_H
  23
  24 #include "parser/antlr_input.h"
  25 #include "parser/smt/generated/SmtLexer.h"
  26 #include "parser/smt/generated/SmtParser.h"
  27
  28 // extern void SmtParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser);
  29
  30 namespace CVC4 {
  31
  32 class Command;
  33 class Expr;
  34 class ExprManager;
  35
  36 namespace parser {
  37
  38 class SmtInput : public AntlrInput {
  39
  40   /** The ANTLR3 SMT lexer for the input. */
  41   pSmtLexer d_pSmtLexer;
  42
  43   /** The ANTLR3 CVC parser for the input. */
  44   pSmtParser d_pSmtParser;
  45
  46 public:
  47
  48   /**
  49    * Create an input.
  50    *
  51    * @param inputStream the input stream to use
  52    */
  53   SmtInput(AntlrInputStream& inputStream);
  54
  55   /**
  56    * Create a string input.
  57    *
  58    * @param exprManager the manager to use when building expressions from the input
  59    * @param input the string to read
  60    * @param name the "filename" to use when reporting errors
  61    */
  62 //  SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name);
  63
  64   /** Destructor. Frees the lexer and the parser. */
  65   ~SmtInput();
  66
  67 protected:
  68
  69   /**
  70    * Parse a command from the input. Returns <code>NULL</code> if
  71    * there is no command there to parse.
  72    *
  73    * @throws ParserException if an error is encountered during parsing.
  74    */
  75   Command* parseCommand() throw(ParserException);
  76
  77   /**
  78    * Parse an expression from the input. Returns a null
  79    * <code>Expr</code> if there is no expression there to parse.
  80    *
  81    * @throws ParserException if an error is encountered during parsing.
  82    */
  83   Expr parseExpr() throw(ParserException);
  84
  85 private:
  86
  87   /**
  88    * Initialize the class. Called from the constructors once the input
  89    * stream is initialized.
  90    */
  91   void init();
  92
  93 };/* class SmtInput */
  94
  95 }/* CVC4::parser namespace */
  96 }/* CVC4 namespace */
  97
  98 #endif /* __CVC4__PARSER__SMT_INPUT_H */