src/parser/smt2/smt2_input.h

   1 /*********************                                                        */
   2 /*! \file smt2_input.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Christopher L. Conway, Mathias Preiner, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief [[ Add file-specific comments here ]].
  13  **
  14  ** [[ Add file-specific comments here ]]
  15  **/
  16
  17 #include "cvc4parser_private.h"
  18
  19 #ifndef CVC4__PARSER__SMT2_INPUT_H
  20 #define CVC4__PARSER__SMT2_INPUT_H
  21
  22 #include "parser/antlr_input.h"
  23 #include "parser/smt2/Smt2Lexer.h"
  24 #include "parser/smt2/Smt2Parser.h"
  25
  26 // extern void Smt2ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser);
  27
  28 namespace CVC4 {
  29
  30 class Command;
  31 class Expr;
  32 class ExprManager;
  33
  34 namespace parser {
  35
  36 class Smt2;
  37
  38 class Smt2Input : public AntlrInput {
  39   typedef AntlrInput super;
  40
  41   /** The ANTLR3 SMT2 lexer for the input. */
  42   pSmt2Lexer d_pSmt2Lexer;
  43
  44   /** The ANTLR3 SMT2 parser for the input. */
  45   pSmt2Parser d_pSmt2Parser;
  46
  47   /**
  48    * Initialize the class. Called from the constructors once the input
  49    * stream is initialized.
  50    */
  51   void init();
  52
  53  public:
  54   /**
  55    * Create an input.
  56    *
  57    * @param inputStream the input stream to use
  58    */
  59   Smt2Input(AntlrInputStream& inputStream);
  60
  61   /** Destructor. Frees the lexer and the parser. */
  62   virtual ~Smt2Input();
  63
  64  protected:
  65   /**
  66    * Parse a command from the input. Returns <code>NULL</code> if
  67    * there is no command there to parse.
  68    *
  69    * @throws ParserException if an error is encountered during parsing.
  70    */
  71   Command* parseCommand() override;
  72
  73   /**
  74    * Parse an expression from the input. Returns a null
  75    * <code>Expr</code> if there is no expression there to parse.
  76    *
  77    * @throws ParserException if an error is encountered during parsing.
  78    */
  79   api::Term parseExpr() override;
  80
  81 };/* class Smt2Input */
  82
  83 }/* CVC4::parser namespace */
  84 }/* CVC4 namespace */
  85
  86 #endif /* CVC4__PARSER__SMT2_INPUT_H */