about summary refs log tree commit diff homepage
path: root/lib/SMT
diff options
context:
space:
mode:
Diffstat (limited to 'lib/SMT')
-rw-r--r--lib/SMT/lang.h7
-rw-r--r--lib/SMT/parser.h8
-rw-r--r--lib/SMT/smtlib.lex4
3 files changed, 11 insertions, 8 deletions
diff --git a/lib/SMT/lang.h b/lib/SMT/lang.h
index c021e63a..d4683f96 100644
--- a/lib/SMT/lang.h
+++ b/lib/SMT/lang.h
@@ -22,7 +22,12 @@
 #ifndef _cvc3__lang_h_
 #define _cvc3__lang_h_
 
-#include "debug.h"
+#include <assert.h>
+#include <stdlib.h>
+
+//#include "debug.h"
+#define FatalAssert(cond, msg) assert(#cond && msg)
+#define DebugAssert(cond, msg) assert(#cond && msg)
 
 namespace CVC3 {
 
diff --git a/lib/SMT/parser.h b/lib/SMT/parser.h
index 2e580a31..4e7f05ba 100644
--- a/lib/SMT/parser.h
+++ b/lib/SMT/parser.h
@@ -33,8 +33,7 @@
 
 namespace CVC3 {
 
-  class ValidityChecker;
-  class Expr;
+  //class Expr;
   
   // Internal parser state and other data
   class ParserData;
@@ -47,12 +46,11 @@ namespace CVC3 {
     void deleteParser();
   public:
     // Constructors
-    Parser(ValidityChecker* vc, InputLanguage lang,
+    Parser(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(InputLanguage lang, std::istream& is, bool interactive = false);
     // Destructor
     ~Parser();
     // Read the next command.  
diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex
index 15c06fc5..25032eeb 100644
--- a/lib/SMT/smtlib.lex
+++ b/lib/SMT/smtlib.lex
@@ -21,9 +21,9 @@
 
 #include <iostream>
 #include "parser_temp.h"
-#include "expr_manager.h" /* for the benefit of parsesmtlib_defs.h */
+//#include "expr_manager.h" /* for the benefit of parsesmtlib_defs.h */
 #include "parsesmtlib_defs.h"
-#include "debug.h"
+//#include "debug.h"
 
 namespace CVC3 {
   extern ParserTemp* parserTemp;