1 /*********************                                                        */
2 /*! \file sygus_input.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Morgan Deters, Tim King
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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__SYGUS_INPUT_H
20 #define __CVC4__PARSER__SYGUS_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 SygusInput : 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   SygusInput(AntlrInputStream& inputStream);
60 
61   /** Destructor. Frees the lexer and the parser. */
62   virtual ~SygusInput();
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   Expr parseExpr() override;
80 
81 };/* class SygusInput */
82 
83 }/* CVC4::parser namespace */
84 }/* CVC4 namespace */
85 
86 #endif /* __CVC4__PARSER__SYGUS_INPUT_H */
87