src/parser/parser.h

   1 /*********************                                           -*- C++ -*-  */
   2 /** parser.h
   3  ** This file is part of the CVC4 prototype.
   4  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
   5  ** Courant Institute of Mathematical Sciences
   6  ** New York University
   7  ** See the file COPYING in the top-level source directory for licensing
   8  ** information.
   9  **
  10  ** Parser abstraction.
  11  **/
  12
  13 #ifndef __CVC4__PARSER__PARSER_H
  14 #define __CVC4__PARSER__PARSER_H
  15
  16 #include <string>
  17 #include <iostream>
  18 #include <fstream>
  19 #include "cvc4_config.h"
  20 #include "parser_exception.h"
  21
  22 namespace CVC4 {
  23
  24 // Forward declarations
  25 class Expr;
  26 class Command;
  27 class ExprManager;
  28
  29 namespace parser {
  30
  31 class AntlrSmtLexer;
  32 class AntlrSmtParser;
  33 class AntlrCvcLexer;
  34 class AntlrCvcParser;
  35
  36 /**
  37  * The parser.
  38  */
  39 class CVC4_PUBLIC Parser {
  40
  41 public:
  42
  43   /**
  44    * Construct the parser that uses the given expression manager.
  45    * @param em the expression manager.
  46    */
  47   Parser(ExprManager* em);
  48
  49   /**
  50    * Destructor.
  51    */
  52   virtual ~Parser() {
  53   }
  54
  55   /**
  56    * Parse the next command of the input
  57    */
  58   virtual Command* parseNextCommand() throw (ParserException) = 0;
  59
  60   /**
  61    * Parse the next expression of the stream
  62    */
  63   virtual Expr parseNextExpression() throw (ParserException) = 0;
  64
  65   /**
  66    * Check if we are done -- either the end of input has been reached.
  67    */
  68   bool done() const;
  69
  70 protected:
  71
  72   /** Sets the done flag */
  73   void setDone(bool done = true);
  74
  75   /** Expression manager the parser will be using */
  76   ExprManager* d_expr_manager;
  77
  78   /** Are we done */
  79   bool d_done;
  80
  81 }; // end of class Parser
  82
  83 class CVC4_PUBLIC SmtParser : public Parser {
  84
  85 public:
  86
  87   /**
  88    * Construct the parser that uses the given expression manager and parses
  89    * from the given input stream.
  90    * @param em the expression manager to use
  91    * @param input the input stream to parse
  92    */
  93   SmtParser(ExprManager* em, std::istream& input);
  94
  95   /**
  96    * Construct the parser that uses the given expression manager and parses
  97    * from the file.
  98    * @param em the expression manager to use
  99    * @param file_name the file to parse
 100    */
 101   SmtParser(ExprManager* em, const char* file_name);
 102
 103   /**
 104    * Destructor.
 105    */
 106   ~SmtParser();
 107
 108   /**
 109    * Parses the next command. By default, the SMTLIB parser produces one
 110    * CommandSequence command. If parsing is successful, we should be done
 111    * after the first call to this command.
 112    * @return the CommandSequence command that includes the whole benchmark
 113    */
 114   Command* parseNextCommand() throw (ParserException);
 115
 116   /**
 117    * Parses the next complete expression of the stream.
 118    * @return the expression parsed
 119    */
 120   Expr parseNextExpression() throw (ParserException);
 121
 122 protected:
 123
 124   /** The ANTLR smt lexer */
 125   AntlrSmtLexer* d_antlr_lexer;
 126
 127   /** The ANTLR smt parser */
 128   AntlrSmtParser* d_antlr_parser;
 129
 130   /** The file stream we might be using */
 131   std::ifstream d_input;
 132 };
 133
 134 class CVC4_PUBLIC CvcParser : public Parser {
 135
 136 public:
 137
 138   /**
 139    * Construct the parser that uses the given expression manager and parses
 140    * from the given input stream.
 141    * @param em the expression manager to use
 142    * @param input the input stream to parse
 143    */
 144   CvcParser(ExprManager* em, std::istream& input);
 145
 146   /**
 147    * Construct the parser that uses the given expression manager and parses
 148    * from the file.
 149    * @param em the expression manager to use
 150    * @param file_name the file to parse
 151    */
 152   CvcParser(ExprManager* em, const char* file_name);
 153
 154   /**
 155    * Destructor.
 156    */
 157   ~CvcParser();
 158
 159   /**
 160    * Parses the next command. By default, the SMTLIB parser produces one
 161    * CommandSequence command. If parsing is successful, we should be done
 162    * after the first call to this command.
 163    * @return the CommandSequence command that includes the whole benchmark
 164    */
 165   Command* parseNextCommand() throw (ParserException);
 166
 167   /**
 168    * Parses the next complete expression of the stream.
 169    * @return the expression parsed
 170    */
 171   Expr parseNextExpression() throw (ParserException);
 172
 173 protected:
 174
 175   /** The ANTLR smt lexer */
 176   AntlrCvcLexer* d_antlr_lexer;
 177
 178   /** The ANTLR smt parser */
 179   AntlrCvcParser* d_antlr_parser;
 180
 181   /** The file stream we might be using */
 182   std::ifstream d_input;
 183 };
 184
 185
 186 }/* CVC4::parser namespace */
 187 }/* CVC4 namespace */
 188
 189 #endif /* __CVC4__PARSER__PARSER_H */