Made expression nodes int the SMT parser be pointers to ExprHandle.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73131 91177308-0d34-0410-b5e6-96231b3b80d8

7 files changed, 15 insertions, 33 deletions

diff --git a/lib/SMT/parser.cpp b/lib/SMT/parser.cpp
index b8191b50..9284d7d0 100644
--- a/lib/SMT/parser.cpp
+++ b/lib/SMT/parser.cpp
@@ -30,7 +30,6 @@ using namespace std;
 
 // The communication entry points of the actual parsers
 
-
 // for smtlib language (smtlib.y and smtlib.lex)
 extern int smtlibparse(); 
 extern void *smtlib_createBuffer(int);
@@ -121,7 +120,7 @@ namespace CVC3 {
   }
     
 
-  Expr Parser::next() {
+  klee::expr::ExprHandle* Parser::next() {
     // If no more commands are available, return a Null Expr
     if(d_data->temp.done) return NULL;//Expr();
     // Set the global var so the parser uses the right stream and EM
diff --git a/lib/SMT/parser.h b/lib/SMT/parser.h
index c55d7eda..c061841f 100644
--- a/lib/SMT/parser.h
+++ b/lib/SMT/parser.h
@@ -29,8 +29,6 @@
 #define _cvc3__parser_h_
 
 namespace CVC3 {
-
-  //class Expr;
   
   // Internal parser state and other data
   class ParserData;
@@ -50,7 +48,7 @@ namespace CVC3 {
     // Destructor
     ~Parser();
     // Read the next command.  
-    Expr next();
+    klee::expr::ExprHandle* 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/lib/SMT/parser_temp.h b/lib/SMT/parser_temp.h
index d6ad91a2..afd8af21 100644
--- a/lib/SMT/parser_temp.h
+++ b/lib/SMT/parser_temp.h
@@ -23,8 +23,7 @@
 #ifndef _cvc3__parser_temp_h_
 #define _cvc3__parser_temp_h_
 
-//#include "expr.h"
-#define Expr void*
+#include "expr/Parser.h"
 
 #include <sstream>
 #include <vector>
@@ -48,7 +47,7 @@ namespace CVC3 {
     // File name
     std::string fileName;
     // The last parsed Expr
-    Expr expr;
+    klee::expr::ExprHandle* expr;
     // Whether we are done or not
     bool done;
     // Whether we are running interactive
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index 10ed3c89..be1c5143 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -76,7 +76,7 @@ int smtliberror(const char *s)
 %union {
   std::string *str;
   std::vector<std::string> *strvec;
-  Expr node;
+  klee::expr::ExprHandle* node;
   std::vector<void*> *vec;
 };
 
diff --git a/lib/SMT/smtlib_lexer.cpp b/lib/SMT/smtlib_lexer.cpp
index c25e7f9a..f8a2b329 100644
--- a/lib/SMT/smtlib_lexer.cpp
+++ b/lib/SMT/smtlib_lexer.cpp
@@ -73,6 +73,7 @@ typedef int flex_int32_t;
 typedef unsigned char flex_uint8_t; 
 typedef unsigned short int flex_uint16_t;
 typedef unsigned int flex_uint32_t;
+#endif /* ! C99 */
 
 /* Limits of integral types. */
 #ifndef INT8_MIN
@@ -103,8 +104,6 @@ typedef unsigned int flex_uint32_t;
 #define UINT32_MAX             (4294967295U)
 #endif
 
-#endif /* ! C99 */
-
 #endif /* ! FLEXINT_H */
 
 #ifdef __cplusplus
@@ -161,15 +160,7 @@ typedef unsigned int flex_uint32_t;
 
 /* Size of default input buffer. */
 #ifndef YY_BUF_SIZE
-#ifdef __ia64__
-/* On IA-64, the buffer size is 16k, not 8k.
- * Moreover, YY_BUF_SIZE is 2*YY_READ_BUF_SIZE in the general case.
- * Ditto for the __ia64__ case accordingly.
- */
-#define YY_BUF_SIZE 32768
-#else
 #define YY_BUF_SIZE 16384
-#endif /* __ia64__ */
 #endif
 
 /* The state buf must be large enough to hold one state per character in the main buffer.
@@ -757,7 +748,7 @@ static std::string _string_lit;
 
 
 
-#line 761 "smtlib_lexer.cpp"
+#line 752 "smtlib_lexer.cpp"
 
 #define INITIAL 0
 #define COMMENT 1
@@ -840,12 +831,7 @@ static int input (void );
 
 /* Amount of stuff to slurp up with each read. */
 #ifndef YY_READ_BUF_SIZE
-#ifdef __ia64__
-/* On IA-64, the buffer size is 16k, not 8k */
-#define YY_READ_BUF_SIZE 16384
-#else
 #define YY_READ_BUF_SIZE 8192
-#endif /* __ia64__ */
 #endif
 
 /* Copy whatever the last rule matched to the standard output. */
@@ -853,7 +839,7 @@ static int input (void );
 /* This used to be an fputs(), but since the string might contain NUL's,
  * we now use fwrite().
  */
-#define ECHO do { if (fwrite( smtlibtext, smtlibleng, 1, smtlibout )) {} } while (0)
+#define ECHO fwrite( smtlibtext, smtlibleng, 1, smtlibout )
 #endif
 
 /* Gets input and stuffs it into "buf".  number of characters read, or YY_NULL,
@@ -864,7 +850,7 @@ static int input (void );
 	if ( YY_CURRENT_BUFFER_LVALUE->yy_is_interactive ) \
 		{ \
 		int c = '*'; \
-		size_t n; \
+		unsigned n; \
 		for ( n = 0; n < max_size && \
 			     (c = getc( smtlibin )) != EOF && c != '\n'; ++n ) \
 			buf[n] = (char) c; \
@@ -949,7 +935,7 @@ YY_DECL
 #line 126 "smtlib.lex"
 
 
-#line 953 "smtlib_lexer.cpp"
+#line 939 "smtlib_lexer.cpp"
 
 	if ( !(yy_init) )
 		{
@@ -1404,7 +1390,7 @@ YY_RULE_SETUP
 #line 221 "smtlib.lex"
 ECHO;
 	YY_BREAK
-#line 1408 "smtlib_lexer.cpp"
+#line 1394 "smtlib_lexer.cpp"
 
 	case YY_END_OF_BUFFER:
 		{
@@ -2128,8 +2114,8 @@ YY_BUFFER_STATE smtlib_scan_string (yyconst char * yystr )
 
 /** Setup the input buffer state to scan the given bytes. The next call to smtliblex() will
  * scan from a @e copy of @a bytes.
- * @param yybytes the byte buffer to scan
- * @param _yybytes_len the number of bytes in the buffer pointed to by @a bytes.
+ * @param bytes the byte buffer to scan
+ * @param len the number of bytes in the buffer pointed to by @a bytes.
  * 
  * @return the newly allocated buffer state object.
  */
diff --git a/lib/SMT/smtlib_parser.cpp b/lib/SMT/smtlib_parser.cpp
index e7d0e1d6..c97a95ff 100644
--- a/lib/SMT/smtlib_parser.cpp
+++ b/lib/SMT/smtlib_parser.cpp
@@ -275,7 +275,7 @@ typedef union YYSTYPE
 {
   std::string *str;
   std::vector<std::string> *strvec;
-  Expr node;
+  klee::expr::ExprHandle* node;
   std::vector<void*> *vec;
 }
 /* Line 187 of yacc.c.  */
diff --git a/lib/SMT/smtlib_parser.h b/lib/SMT/smtlib_parser.h
index c587a126..1544c35e 100644
--- a/lib/SMT/smtlib_parser.h
+++ b/lib/SMT/smtlib_parser.h
@@ -156,7 +156,7 @@ typedef union YYSTYPE
 {
   std::string *str;
   std::vector<std::string> *strvec;
-  Expr node;
+  klee::expr::ExprHandle* node;
   std::vector<void*> *vec;
 }
 /* Line 1489 of yacc.c.  */