diff options
| -rw-r--r-- | lib/SMT/Makefile | 6 | ||||
| -rw-r--r-- | lib/SMT/parser.cpp | 2 | ||||
| -rw-r--r-- | lib/SMT/parser.h | 2 | ||||
| -rw-r--r-- | lib/SMT/parser_temp.h | 2 | ||||
| -rw-r--r-- | lib/SMT/smtlib.y | 18 |
5 files changed, 18 insertions, 12 deletions
diff --git a/lib/SMT/Makefile b/lib/SMT/Makefile index 5ab2d16f..92ec8018 100644 --- a/lib/SMT/Makefile +++ b/lib/SMT/Makefile @@ -14,10 +14,14 @@ include $(LEVEL)/Makefile.common smtlib_parser.cpp smtlib_parser.h: smtlib.y bison -d -o smtlib_parser.cpp -p smtlib smtlib.y - mv smtlib_parser.hpp smtlib_parser.h + mv smtlib_parser.hpp smtlib_parser.h + perl -pi -e 's/union/struct/g' smtlib_parser.cpp + perl -pi -e 's/union/struct/g' smtlib_parser.h + smtlib_lexer.cpp: smtlib.lex smtlib_parser.h flex -I -Psmtlib -osmtlib_lexer.cpp smtlib.lex + perl -pi -e 's/union/struct/g' smtlib_lexer.cpp .PHONY: regen regen: smtlib_lexer.cpp smtlib_parser.cpp smtlib_parser.h diff --git a/lib/SMT/parser.cpp b/lib/SMT/parser.cpp index 9284d7d0..439e189c 100644 --- a/lib/SMT/parser.cpp +++ b/lib/SMT/parser.cpp @@ -120,7 +120,7 @@ namespace CVC3 { } - klee::expr::ExprHandle* 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 c061841f..30a01ac2 100644 --- a/lib/SMT/parser.h +++ b/lib/SMT/parser.h @@ -48,7 +48,7 @@ namespace CVC3 { // Destructor ~Parser(); // Read the next command. - klee::expr::ExprHandle* 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 afd8af21..704157d9 100644 --- a/lib/SMT/parser_temp.h +++ b/lib/SMT/parser_temp.h @@ -47,7 +47,7 @@ namespace CVC3 { // File name std::string fileName; // The last parsed Expr - klee::expr::ExprHandle* 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 be1c5143..72185a93 100644 --- a/lib/SMT/smtlib.y +++ b/lib/SMT/smtlib.y @@ -23,8 +23,11 @@ commands in SMT-LIB language. */ -//#include "vc.h" #include "parser_temp.h" +#include "klee/Expr.h" + +using namespace klee; +using namespace klee::expr; // Exported shared data namespace CVC3 { @@ -75,9 +78,7 @@ int smtliberror(const char *s) %union { std::string *str; - std::vector<std::string> *strvec; - klee::expr::ExprHandle* node; - std::vector<void*> *vec; + klee::expr::ExprHandle node; }; @@ -176,13 +177,14 @@ benchmark: $$ = new CVC3::Expr(VC->listExpr("_SEQ",*$4)); delete $4; */ - $$ = NULL; + $$ = $4; } | EOF_TOK { TMP->done = true; //$$ = new CVC3::Expr(); - $$ = NULL; + //$$ = ConstantExpr::create(1, 1); + $$ = ExprHandle(); } ; @@ -761,12 +763,12 @@ prop_atom: TRUE_TOK { //$$ = new CVC3::Expr(VC->idExpr("_TRUE_EXPR")); - $$ = NULL; + $$ = ConstantExpr::create(1, 1); } | FALSE_TOK { //$$ = new CVC3::Expr(VC->idExpr("_FALSE_EXPR")); - $$ = NULL; + $$ = ConstantExpr::create(0, 1);; } /* | fvar |