src/parser/parser.h

   1 /*********************                                                        */
   2 /** parser.h
   3  ** Original author: mdeters
   4  ** Major contributors: dejan
   5  ** Minor contributors (to current version): none
   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 }
  29
  30 namespace CVC4 {
  31
  32 // Forward declarations
  33 class Expr;
  34 class Command;
  35 class ExprManager;
  36
  37 namespace parser {
  38
  39 class AntlrParser;
  40
  41 /**
  42  * The parser. The parser should be obtained by calling the static methods
  43  * getNewParser, and should be deleted when done.
  44  */
  45 class CVC4_PUBLIC Parser {
  46
  47 public:
  48
  49   /** The input language option */
  50   enum InputLanguage {
  51     /** The SMTLIB input language */
  52     LANG_SMTLIB,
  53     /** The CVC4 input language */
  54     LANG_CVC4,
  55     /** Auto-detect the language */
  56     LANG_AUTO
  57   };
  58
  59   static Parser* getNewParser(ExprManager* em, InputLanguage lang, std::string filename);
  60   static Parser* getNewParser(ExprManager* em, InputLanguage lang, std::istream& input);
  61
  62   /**
  63    * Destructor.
  64    */
  65   ~Parser();
  66
  67   /**
  68    * Parse the next command of the input. If EOF is encountered a EmptyCommand
  69    * is returned and done flag is set.
  70    */
  71   Command* parseNextCommand() throw(ParserException, AssertionException);
  72
  73   /**
  74    * Parse the next expression of the stream. If EOF is encountered a null
  75    * expression is returned and done flag is set.
  76    * @return the parsed expression
  77    */
  78   Expr parseNextExpression() throw(ParserException, AssertionException);
  79
  80   /**
  81    * Check if we are done -- either the end of input has been reached, or some
  82    * error has been encountered.
  83    * @return true if parser is done
  84    */
  85   bool done() const;
  86
  87   /** Enable semantic checks during parsing. */
  88   void enableChecks();
  89
  90   /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
  91   void disableChecks();
  92
  93 private:
  94
  95   /**
  96    * Create a new parser.
  97    * @param em the expression manager to usee
  98    * @param lang the language to parse
  99    * @param input the input stream to parse
 100    * @param filename the filename to attach to the stream
 101    * @param deleteInput wheather to delete the input
 102    * @return the parser
 103    */
 104   static Parser* getNewParser(ExprManager* em, InputLanguage lang, std::istream* input, std::string filename, bool deleteInput);
 105
 106   /**
 107    * Create a new parser given the actual antlr parser.
 108    * @param antlrParser the antlr parser to user
 109    */
 110   Parser(std::istream* input, AntlrParser* antlrParser, antlr::CharScanner* antlrLexer, bool deleteInput);
 111
 112   /** Sets the done flag */
 113   void setDone(bool done = true);
 114
 115   /** Are we done */
 116   bool d_done;
 117
 118   /** The antlr parser */
 119   AntlrParser* d_antlrParser;
 120
 121   /** The entlr lexer */
 122   antlr::CharScanner* d_antlrLexer;
 123
 124   /** The input stream we are using */
 125   std::istream* d_input;
 126
 127   /** Wherther to de-allocate the input */
 128   bool d_deleteInput;
 129 }; // end of class Parser
 130
 131 }/* CVC4::parser namespace */
 132 }/* CVC4 namespace */
 133
 134 #endif /* __CVC4__PARSER__PARSER_H */