about summary refs log tree commit diff homepage
path: root/lib/SMT
diff options
context:
space:
mode:
authorCristian Cadar <cristic@cs.stanford.edu>2009-06-08 08:30:59 +0000
committerCristian Cadar <cristic@cs.stanford.edu>2009-06-08 08:30:59 +0000
commitef0bc0aee68cf791544865525005d91c73791bf2 (patch)
tree16df415a7fb249c7972e43df00e17ae013f385f3 /lib/SMT
parentff6e5265662f6756ac827a5a8faaeaf0db99c03d (diff)
downloadklee-ef0bc0aee68cf791544865525005d91c73791bf2.tar.gz
More changes needed to make the SMTLIB parser compile.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73063 91177308-0d34-0410-b5e6-96231b3b80d8
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;