various fixes and updates to use and support parser

5 files changed, 42 insertions, 14 deletions

diff --git a/src/parser/language.h b/src/parser/language.h
new file mode 100644
index 000000000..7ea6547cd
--- /dev/null
+++ b/src/parser/language.h
@@ -0,0 +1,31 @@
+/*********************                                           -*- C++ -*-  */
+/** language.h
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Input languages.
+ **/
+
+#ifndef __CVC4__PARSER__LANGUAGE_H
+#define __CVC4__PARSER__LANGUAGE_H
+
+#include "util/exception.h"
+#include "parser/language.h"
+
+namespace CVC4 {
+namespace parser {
+
+enum Language {
+  AUTO = 0,
+  PL,
+  SMTLIB,
+};/* enum Language */
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__LANGUAGE_H */
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 36b8c34eb..73565b8c4 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -13,13 +13,13 @@
 #ifndef __CVC4__PARSER__PARSER_H
 #define __CVC4__PARSER__PARSER_H
 
-#include "core/exception.h"
-#include "core/lang.h"
+#include "util/exception.h"
+#include "parser/language.h"
+#include "util/command.h"
 
 namespace CVC4 {
 namespace parser {
 
-  class ValidityChecker;
   class Expr;
   
   // Internal parser state and other data
@@ -33,16 +33,11 @@ namespace parser {
     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);
+    Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, Options* opts, bool interactive = false);
     // Destructor
     ~Parser();
     // Read the next command.  
-    Expr next();
+    CVC4::Command* 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
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index 4eda5eb38..1d013a0b4 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -19,7 +19,7 @@
 
 #include <iostream>
 #include <sstream>
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "util/exception.h"
 
diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
index e7d752419..b59c7c69e 100644
--- a/src/parser/pl.ypp
+++ b/src/parser/pl.ypp
@@ -13,10 +13,10 @@
 
 %{
 
-#include "cvc4.h"
-#include "cvc4_expr.h"
+#include "smt/smt_engine.h"
 #include "parser/parser_exception.h"
 #include "parser/parser_state.h"
+#include "expr/expr.h"
 #include "expr/expr_builder.h"
 #include "expr/expr_manager.h"
 #include "util/command.h"
diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp
index 692a9cda5..e616b3a65 100644
--- a/src/parser/smtlib.ypp
+++ b/src/parser/smtlib.ypp
@@ -11,10 +11,12 @@
  ** commands in SMT-LIB language.
  **/
 
-#include "cvc4.h"
+#include "smt/smt_engine.h"
 #include "parser/parser_exception.h"
 #include "parser/parser_state.h"
 
+#include <vector>
+
 // Exported shared data
 namespace CVC4 {
   extern ParserState* parserState;