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