src/parser/parser.h

   1 /*********************                                                        */
   2 /** parser.h
   3  ** Original author: mdeters
   4  ** Major contributors: dejan
   5  ** Minor contributors (to current version): cconway
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** Parser abstraction.
  14  **/
  15
  16 #ifndef __CVC4__PARSER__PARSER_H
  17 #define __CVC4__PARSER__PARSER_H
  18
  19 #include <string>
  20 #include <iostream>
  21
  22 #include "cvc4_config.h"
  23 #include "parser/parser_exception.h"
  24 #include "util/Assert.h"
  25
  26 namespace antlr {
  27   class CharScanner;
  28   class InputBuffer;
  29 }
  30
  31 namespace CVC4 {
  32
  33 // Forward declarations
  34 class Expr;
  35 class Command;
  36 class ExprManager;
  37
  38 namespace parser {
  39
  40 class AntlrParser;
  41
  42 /**
  43  * The parser. The parser should be obtained by calling the static methods
  44  * getNewParser, and should be deleted when done.
  45  */
  46 class CVC4_PUBLIC Parser {
  47
  48 public:
  49
  50   /** The input language option */
  51   enum InputLanguage {
  52     /** The SMTLIB input language */
  53     LANG_SMTLIB,
  54     /** The CVC4 input language */
  55     LANG_CVC4,
  56     /** Auto-detect the language */
  57     LANG_AUTO
  58   };
  59
  60   static Parser* getMemoryMappedParser(ExprManager* em, InputLanguage lang, std::string filename);
  61   static Parser* getNewParser(ExprManager* em, InputLanguage lang, std::istream& input, std::string filename);
  62
  63   /**
  64    * Destructor.
  65    */
  66   ~Parser();
  67
  68   /**
  69    * Parse the next command of the input. If EOF is encountered a EmptyCommand
  70    * is returned and done flag is set.
  71    */
  72   Command* parseNextCommand() throw(ParserException, AssertionException);
  73
  74   /**
  75    * Parse the next expression of the stream. If EOF is encountered a null
  76    * expression is returned and done flag is set.
  77    * @return the parsed expression
  78    */
  79   Expr parseNextExpression() throw(ParserException, AssertionException);
  80
  81   /**
  82    * Check if we are done -- either the end of input has been reached, or some
  83    * error has been encountered.
  84    * @return true if parser is done
  85    */
  86   bool done() const;
  87
  88   /** Enable semantic checks during parsing. */
  89   void enableChecks();
  90
  91   /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
  92   void disableChecks();
  93
  94 private:
  95
  96   /**
  97    * Create a new parser.
  98    * @param em the expression manager to usee
  99    * @param lang the language to parse
 100    * @param inputBuffer the input buffer to parse
 101    * @param filename the filename to attach to the stream
 102    * @param deleteInput wheather to delete the input
 103    * @return the parser
 104    */
 105   static Parser* getNewParser(ExprManager* em, InputLanguage lang, antlr::InputBuffer* inputBuffer, std::string filename);
 106
 107   /**
 108    * Create a new parser given the actual antlr parser.
 109    * @param antlrParser the antlr parser to user
 110    */
 111   Parser(antlr::InputBuffer* inputBuffer, AntlrParser* antlrParser, antlr::CharScanner* antlrLexer);
 112
 113   /** Sets the done flag */
 114   void setDone(bool done = true);
 115
 116   /** Are we done */
 117   bool d_done;
 118
 119   /** The antlr parser */
 120   AntlrParser* d_antlrParser;
 121
 122   /** The entlr lexer */
 123   antlr::CharScanner* d_antlrLexer;
 124
 125   /** The input stream we are using */
 126   antlr::InputBuffer* d_inputBuffer;
 127
 128   /** Wherther to de-allocate the input */
 129   bool d_deleteInput;
 130 }; // end of class Parser
 131
 132 }/* CVC4::parser namespace */
 133 }/* CVC4 namespace */
 134
 135 #endif /* __CVC4__PARSER__PARSER_H */