From e44a3c413e2e3c027ed2f20482685815b30505cb Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Tue, 3 Nov 2009 17:14:55 +0000 Subject: [PATCH] added ability to parse SMT files from the c_interface git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@376 e59a4935-1847-0410-ae03-e826735625c1 --- Makefile | 3 ++- scripts/Makefile.in | 3 ++- src/c_interface/c_interface.cpp | 22 ++++++++++++++++------ src/sat/cryptominisat/clause.h | 2 +- tests/c-api-tests/Makefile | 4 ++-- 5 files changed, 23 insertions(+), 11 deletions(-) diff --git a/Makefile b/Makefile index c0d5cd1..ebb724c 100644 --- a/Makefile +++ b/Makefile @@ -44,6 +44,8 @@ endif $(SRC)/parser/let-funcs.o \ $(SRC)/parser/parseCVC.o \ $(SRC)/parser/lexCVC.o \ + $(SRC)/parser/parseSMT.o \ + $(SRC)/parser/lexSMT.o \ $(SRC)/main/*.o $(RANLIB) libstp.a @mkdir -p lib @@ -52,7 +54,6 @@ endif @echo "Compilation successful." @echo "Type 'make install' to install STP." -# # During the build of AST some classes are built that most of the other # classes depend upon. So in a parallel make, AST should be made first. diff --git a/scripts/Makefile.in b/scripts/Makefile.in index c0d5cd1..ebb724c 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -44,6 +44,8 @@ endif $(SRC)/parser/let-funcs.o \ $(SRC)/parser/parseCVC.o \ $(SRC)/parser/lexCVC.o \ + $(SRC)/parser/parseSMT.o \ + $(SRC)/parser/lexSMT.o \ $(SRC)/main/*.o $(RANLIB) libstp.a @mkdir -p lib @@ -52,7 +54,6 @@ endif @echo "Compilation successful." @echo "Type 'make install' to install STP." -# # During the build of AST some classes are built that most of the other # classes depend upon. So in a parallel make, AST should be made first. diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 24075fc..49be558 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -28,9 +28,9 @@ BEEV::ASTVec *decls = NULL; //vector created_exprs; bool cinterface_exprdelete_on_flag = false; -/* GLOBAL FUNCTION: parser - */ +// GLOBAL FUNCTION: parser extern int cvcparse(void*); +extern int smtparse(void*); void vc_setFlags(VC vc, char c) { bmstar b = (bmstar)(((stpstar)vc)->bm); @@ -958,8 +958,8 @@ Expr vc_bvConstExprFromInt(VC vc, unsigned long long int max_n_bits = 0xFFFFFFFFFFFFFFFFULL >> 64-n_bits; //printf("%ull", max_n_bits); if(v > max_n_bits) { - printf("CInterface: vc_bvConstExprFromInt: " \ - "Cannot construct a constant %llu >= %d,\n", v, max_n_bits); + printf("CInterface: vc_bvConstExprFromInt: "\ + "Cannot construct a constant %llu >= %llu,\n", v, max_n_bits); BEEV::FatalError("FatalError"); } node n = b->CreateBVConst(n_bits, v); @@ -1709,7 +1709,7 @@ static char *val_to_binary_str(unsigned nbits, unsigned long long val) { Expr vc_parseExpr(VC vc, const char* infile) { bmstar b = (bmstar)(((stpstar)vc)->bm); - extern FILE* cvcin; + extern FILE *cvcin, *smtin; const char * prog = "stp"; cvcin = fopen(infile,"r"); @@ -1726,7 +1726,17 @@ Expr vc_parseExpr(VC vc, const char* infile) { } BEEV::ASTVec * AssertsQuery = new BEEV::ASTVec; - cvcparse((void*)AssertsQuery); + if (b->UserFlags.smtlib_parser_flag) + { + smtin = cvcin; + cvcin = NULL; + smtparse((void*)AssertsQuery); + } + else + { + cvcparse((void*)AssertsQuery); + } + BEEV::ASTNode asserts = (*(BEEV::ASTVec*)AssertsQuery)[0]; BEEV::ASTNode query = (*(BEEV::ASTVec*)AssertsQuery)[1]; //BEEV::GlobalSTP->TopLevelSTP(asserts, query); diff --git a/src/sat/cryptominisat/clause.h b/src/sat/cryptominisat/clause.h index c7abb7b..3674b14 100644 --- a/src/sat/cryptominisat/clause.h +++ b/src/sat/cryptominisat/clause.h @@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include #include -#include +//#include #include "mtl/Vec.h" #include "SolverTypes.h" diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile index 68a5ddb..39453ec 100644 --- a/tests/c-api-tests/Makefile +++ b/tests/c-api-tests/Makefile @@ -43,7 +43,7 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 ./a10.out 11: g++ $(CXXFLAGS) squares-leak.c -lstp -o a11.out - ulimit -v 30000 && ./a11.out + #ulimit -v 30000 && ./a11.out 12: g++ $(CXXFLAGS) stp-counterex.c -lstp -o a12.out ./a12.out @@ -72,7 +72,7 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20: g++ -g $(CXXFLAGS) leak.c -lstp -o a20.out - ulimit -v 13000 && ./a20.out + #ulimit -v 13000 && ./a20.out clean: -- 2.47.3