parser, minisat, other things..

5 files changed, 205 insertions, 43 deletions

diff --git a/src/include/Makefile.am b/src/include/Makefile.am
deleted file mode 100644
index fa37abd9a..000000000
--- a/src/include/Makefile.am
+++ /dev/null
@@ -1,14 +0,0 @@
-EXTRA_DIST = \
-	assert.h \
-	attr_type.h \
-	command.h
-	expr_attribute.h \
-	expr_builder.h \
-	expr.h \
-	expr_manager.h \
-	expr_value.h \
-	kind.h \
-	parser.h \
-	sat.h \
-	unique_id.h \
-	vc.h
diff --git a/src/include/exception.h b/src/include/exception.h
new file mode 100644
index 000000000..3502fdf0c
--- /dev/null
+++ b/src/include/exception.h
@@ -0,0 +1,47 @@
+/*********************                                           -*- C++ -*-  */
+/** exception.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** Exception class.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_EXCEPTION_H
+#ifndef __CVC4_EXCEPTION_H
+
+#include <string>
+#include <iostream>
+
+namespace CVC4 {
+
+  class Exception {
+  protected:
+    std::string d_msg;
+  public:
+    // Constructors
+    Exception(): d_msg("Unknown exception") { }
+    Exception(const std::string& msg): d_msg(msg) { }
+    Exception(const char* msg): d_msg(msg) { }
+    // Destructor
+    virtual ~Exception() { }
+    // NON-VIRTUAL METHODs for setting and printing the error message
+    void setMessage(const std::string& msg) { d_msg = msg; }
+    // Printing: feel free to redefine toString().  When inherited,
+    // it's recommended that this method print the type of exception
+    // before the actual message.
+    virtual std::string toString() const { return d_msg; }
+    // No need to overload operator<< for the inherited classes
+    friend std::ostream& operator<<(std::ostream& os, const Exception& e);
+
+  }; // end of class Exception
+
+  inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
+    return os << e.toString();
+  }
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_EXCEPTION_H */
diff --git a/src/include/parser.h b/src/include/parser.h
index c5af769e3..63a448b28 100644
--- a/src/include/parser.h
+++ b/src/include/parser.h
@@ -2,6 +2,8 @@
 /** parser.h
  ** This file is part of the CVC4 prototype.
  **
+ ** Parser abstraction.
+ **
  ** The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
@@ -10,37 +12,52 @@
 #ifndef __CVC4_PARSER_H
 #define __CVC4_PARSER_H
 
-#include <iostream>
-#include "vc.h"
-#include "expr.h"
+#include "exception.h"
+#include "lang.h"
 
 namespace CVC4 {
 
-// In terms of abstraction, this is below (and provides services to)
-// the main CVC4 binary and above (and requires the services of)
-// ValidityChecker.
-
-class Parser {
-private:// maybe protected is better ?
-  ValidityChecker *d_vc;
-
-public:
-  Parser(ValidityChecker* vc);
-
-  /**
-   * Process a file.  Overridden in subclasses to support SMT-LIB
-   * format, CVC4 presentation language, etc.  In subclasses, this
-   * function should parse terms, build Command objects, and pass them
-   * to dispatch().
-   */
-  virtual Expr process(std::istream&) = 0;
-
-  /**
-   * Dispatch a command.
-   */
-  void dispatch(const Command&);
-};/* class Parser */
-
-} /* CVC4 namespace */
+  class ValidityChecker;
+  class Expr;
+  
+  // Internal parser state and other data
+  class ParserData;
+
+  class Parser {
+  private:
+    ParserData* d_data;
+    // Internal methods for constructing and destroying the actual parser
+    void initParser();
+    void deleteParser();
+  public:
+    // Constructors
+    Parser(ValidityChecker* vc, InputLanguage lang,
+	   // The 'interactive' flag is ignored when fileName != ""
+	   bool interactive = true,
+	   const std::string& fileName = "");
+    Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is,
+	   bool interactive = false);
+    // Destructor
+    ~Parser();
+    // Read the next command.  
+    Expr next();
+    // Check if we are done (end of input has been reached)
+    bool done() const;
+    // The same check can be done by using the class Parser's value as
+    // a Boolean
+    operator bool() const { return done(); }
+    void printLocation(std::ostream & out) const;
+    // Reset any local data that depends on validity checker
+    void reset();
+  }; // end of class Parser
+
+  // The global pointer to ParserTemp.  Each instance of class Parser
+  // sets this pointer before any calls to the lexer.  We do it this
+  // way because flex and bison use global vars, and we want each
+  // Parser object to appear independent.
+  class ParserTemp;
+  extern ParserTemp* parserTemp;
+
+}/* CVC4 namespace */
 
 #endif /* __CVC4_PARSER_H */
diff --git a/src/include/parser_exception.h b/src/include/parser_exception.h
new file mode 100644
index 000000000..8bad801f4
--- /dev/null
+++ b/src/include/parser_exception.h
@@ -0,0 +1,36 @@
+/*********************                                           -*- C++ -*-  */
+/** exception.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** Exception class.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_PARSER_EXCEPTION_H
+#define __CVC4_PARSER_EXCEPTION_H
+
+#include "exception.h"
+#include <string>
+#include <iostream>
+
+namespace CVC4 {
+
+  class ParserException: public Exception {
+  public:
+    // Constructors
+    ParserException() { }
+    ParserException(const std::string& msg): Exception(msg) { }
+    ParserException(const char* msg): Exception(msg) { }
+    // Destructor
+    virtual ~ParserException() { }
+    virtual std::string toString() const {
+      return "Parse Error: " + d_msg;
+    }
+  }; // end of class ParserException
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_PARSER_EXCEPTION_H */
diff --git a/src/include/parser_temp.h b/src/include/parser_temp.h
new file mode 100644
index 000000000..d64a770e4
--- /dev/null
+++ b/src/include/parser_temp.h
@@ -0,0 +1,76 @@
+/*********************                                           -*- C++ -*-  */
+/** parser_temp.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** A temporary holder for data used with the parser.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_PARSER_TEMP_H
+#define __CVC4_PARSER_TEMP_H
+
+#include <iostream>
+
+#include "expr.h"
+#include "exception.h"
+
+namespace CVC4 {
+
+  class ValidityChecker;
+
+  class ParserTemp {
+  private:
+    // Counter for uniqueID of bound variables
+    int d_uid;
+    // The main prompt when running interactive
+    std::string prompt1;
+    // The interactive prompt in the middle of a multi-line command
+    std::string prompt2;
+    // The currently used prompt
+    std::string prompt;
+  public:
+    ValidityChecker* vc;
+    std::istream* is;
+    // The current input line
+    int lineNum;
+    // File name
+    std::string fileName;
+    // The last parsed Expr
+    Expr expr;
+    // Whether we are done or not
+    bool done;
+    // Whether we are running interactive
+    bool interactive;
+    // Whether arrays are enabled for smt-lib format
+    bool arrFlag;
+    // Whether bit-vectors are enabled for smt-lib format
+    bool bvFlag;
+    // Size of bit-vectors for smt-lib format
+    int bvSize;
+    // Did we encounter a formula query (smtlib)
+    bool queryParsed;
+    // Default constructor
+    ParserTemp() : d_uid(0), prompt1("CVC> "), prompt2("- "),
+      prompt("CVC> "), lineNum(1), done(false), arrFlag(false), queryParsed(false) { }
+    // Parser error handling (implemented in parser.cpp)
+    int error(const std::string& s);
+    // Get the next uniqueID as a string
+    std::string uniqueID() {
+      std::ostringstream ss;
+      ss << d_uid++;
+      return ss.str();
+    }
+    // Get the current prompt
+    std::string getPrompt() { return prompt; }
+    // Set the prompt to the main one
+    void setPrompt1() { prompt = prompt1; }
+    // Set the prompt to the secondary one
+    void setPrompt2() { prompt = prompt2; }
+  };
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_PARSER_TEMP_H */