From 33b7ed925aa5336730ece740b2ca4d6111b1ed81 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Tue, 27 Oct 2009 17:45:53 +0000 Subject: [PATCH] added compile flags and other necessary setup for cyrptominisat. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@346 e59a4935-1847-0410-ae03-e826735625c1 --- AUTHORS | 10 +++------- CODING_GUIDLINES | 2 +- INSTALL | 16 +++++----------- Makefile | 4 ++++ README | 6 +++++- scripts/Makefile.common | 7 +++++-- scripts/Makefile.in | 4 ++++ src/STPManager/STPManager.cpp | 3 +++ src/main/Globals.h | 3 +++ src/sat/Makefile | 12 ++++++++++-- src/sat/core/Makefile | 2 +- src/sat/sat.h | 13 +++++++++---- src/to-sat/ToSAT.cpp | 6 ++++-- 13 files changed, 57 insertions(+), 31 deletions(-) diff --git a/AUTHORS b/AUTHORS index 298b818..25cfc3c 100644 --- a/AUTHORS +++ b/AUTHORS @@ -13,17 +13,13 @@ Primary Author -------------- -Vijay Ganesh -Stanford University, Stanford, CA, USA (Nov, 2005 to 2007), -MIT (Oct, 2007 to present) - +Vijay Ganesh, Stanford University, Stanford, CA, USA (Nov, 2005 to 2007), +MIT, Cambridge, MA, USA (Oct, 2007 to present) Other Significant Author ------------------------ -Trevor Alexander Hansen -University of Melbourne, Australia (Sep, 2008 - present) - +Trevor Alexander Hansen, University of Melbourne, Australia (Sep, 2008 - present) Authors who contributed some code diff --git a/CODING_GUIDLINES b/CODING_GUIDLINES index 1508592..0d231fa 100644 --- a/CODING_GUIDLINES +++ b/CODING_GUIDLINES @@ -3,5 +3,5 @@ standards. Please visit the following website to learn more: http://www.gnu.org/prep/standards/standards.html -2. The code is automatically formatted with the indent tool before +2. The code is auto-formatted using an emacs-based script before check-in. diff --git a/INSTALL b/INSTALL index 17ca581..b609ba0 100644 --- a/INSTALL +++ b/INSTALL @@ -8,19 +8,13 @@ * LICENSE: Please view LICENSE file in the home dir of this Program ********************************************************************/ -1. To install STP: +1. To install STP on Linux, MacOS or Windows(Cygwin): ./clean-install.sh +2. To run on Windows Natively: -2. Download large tests: - - svn co https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/stp-tests/test - - - -3. Run tests: - - make regresscapi && make regresscvc && make regresssmt - + 2.1 Compile STP inside cygwin as above + 2.2 Add cygwin DLLs to PATH + 2.3 Run \ No newline at end of file diff --git a/Makefile b/Makefile index 8cc444e..42320f8 100644 --- a/Makefile +++ b/Makefile @@ -24,9 +24,13 @@ all: $(MAKE) -C $(SRC)/simplifier $(MAKE) -C $(SRC)/absrefine_counterexample $(MAKE) -C $(SRC)/to-sat +ifdef CRYPTOMINISAT + $(MAKE) -C $(SRC)/sat cryptominisat +else $(MAKE) -C $(SRC)/sat core # $(MAKE) -C $(SRC)/sat simp # $(MAKE) -C $(SRC)/sat unsound +endif $(MAKE) -C $(SRC)/c_interface $(MAKE) -C $(SRC)/parser $(MAKE) -C $(SRC)/main diff --git a/README b/README index 816bbe7..9e3f595 100644 --- a/README +++ b/README @@ -39,10 +39,14 @@ PAPERS ----- http://sites.google.com/site/stpfastprover + REGRESSIONS ----------- -Assumes you have downloaded the testcases +Assumes you have downloaded the testcases as follows: + +svn co https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/stp-tests/test + make regresssmt make regresscvc diff --git a/scripts/Makefile.common b/scripts/Makefile.common index da491e2..ac9e064 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -13,7 +13,9 @@ OPTIMIZE = -g # Debugging OPTIMIZE = -O3 -DNDEBUG # Maximum optimization #OPTIMIZE = -O3 -DNDEBUG -DLESSBYTES_PERNODE CFLAGS_BASE = $(OPTIMIZE) -CFLAGS_M32 = -m32 +#CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT +#CFLAGS_M32 = -m32 + # You can compile using make STATIC=true to compile a statically # linked executable Note that you should execute liblinks.sh first. @@ -50,7 +52,8 @@ else endif #CXXFLAGS = $(CFLAGS) -Wall -Wextra -DEXT_HASH_MAP -Wno-deprecated -CXXFLAGS = $(CFLAGS) -Wextra -DEXT_HASH_MAP -Wno-deprecated +#CXXFLAGS = $(CFLAGS) -Wextra -DEXT_HASH_MAP -Wno-deprecated +CXXFLAGS = $(CFLAGS) -DEXT_HASH_MAP -Wno-deprecated #CXXFLAGS = $(CFLAGS) -Wall -DTR1_UNORDERED_MAP -Wno-deprecated #CXXFLAGS = $(CFLAGS) -Wall #LDFLAGS= -lstdc++ diff --git a/scripts/Makefile.in b/scripts/Makefile.in index 8cc444e..42320f8 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -24,9 +24,13 @@ all: $(MAKE) -C $(SRC)/simplifier $(MAKE) -C $(SRC)/absrefine_counterexample $(MAKE) -C $(SRC)/to-sat +ifdef CRYPTOMINISAT + $(MAKE) -C $(SRC)/sat cryptominisat +else $(MAKE) -C $(SRC)/sat core # $(MAKE) -C $(SRC)/sat simp # $(MAKE) -C $(SRC)/sat unsound +endif $(MAKE) -C $(SRC)/c_interface $(MAKE) -C $(SRC)/parser $(MAKE) -C $(SRC)/main diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index 2e35d1a..8fa77d7 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -621,6 +621,8 @@ namespace BEEV { if (!UserFlags.stats_flag) return; +#ifdef CRYPTOMINISAT +#else double cpu_time = MINISAT::cpuTime(); uint64_t mem_used = MINISAT::memUsed(); reportf("restarts : %"PRIu64"\n", s.starts); @@ -632,6 +634,7 @@ namespace BEEV if (mem_used != 0) reportf("Memory used : %.2f MB\n", mem_used / 1048576.0); reportf("CPU time : %g s\n", cpu_time); +#endif } //end of PrintStats() diff --git a/src/main/Globals.h b/src/main/Globals.h index ef22d8d..7520196 100644 --- a/src/main/Globals.h +++ b/src/main/Globals.h @@ -23,7 +23,10 @@ namespace MINISAT { class Solver; +#if defined(CRYPTOMINISAT) +#else typedef int Var; +#endif } namespace BEEV diff --git a/src/sat/Makefile b/src/sat/Makefile index d52701e..ec8b899 100644 --- a/src/sat/Makefile +++ b/src/sat/Makefile @@ -1,16 +1,24 @@ .PHONY: core core: $(MAKE) -C core lib all + .PHONY: simp simp: $(MAKE) -C simp lib all + .PHONY: unsound unsound: $(MAKE) -C unsound lib all +.PHONY: cryptominisat +cryptominisat: + $(MAKE) -C cryptominisat + cp cryptominisat/libminisat.a . + .PHONY: clean clean: rm -rf *.or *~ libminisat.a - $(MAKE) -C core clean - $(MAKE) -C simp clean + $(MAKE) -C core clean + $(MAKE) -C simp clean $(MAKE) -C unsound clean + $(MAKE) -C cryptominisat clean \ No newline at end of file diff --git a/src/sat/core/Makefile b/src/sat/core/Makefile index a150a4f..50d1c04 100644 --- a/src/sat/core/Makefile +++ b/src/sat/core/Makefile @@ -2,7 +2,7 @@ include ../../../scripts/Makefile.common MTL = ../mtl CHDRS = $(wildcard *.h) $(wildcard $(MTL)/*.h) EXEC = minisat -CFLAGS = -I$(MTL) -Wall -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) +CFLAGS += -I$(MTL) -Wall -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) LFLAGS = -lz include ../mtl/template.mk diff --git a/src/sat/sat.h b/src/sat/sat.h index d753d3d..88f7dfb 100644 --- a/src/sat/sat.h +++ b/src/sat/sat.h @@ -1,9 +1,14 @@ #ifndef SAT_H_ #define SAT_H_ -#include "core/Solver.h" -#include "core/SolverTypes.h" -//#include "simp/SimpSolver.h" -//#include "unsound/UnsoundSimpSolver.h" +#ifdef CRYPTOMINISAT + #include "cryptominisat/Solver/Solver.h" + #include "cryptominisat/Solver/SolverTypes.h" +#else + #include "core/Solver.h" + #include "core/SolverTypes.h" + //#include "simp/SimpSolver.h" + //#include "unsound/UnsoundSimpSolver.h" +#endif #endif diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index c6714d3..60b4f34 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -55,9 +55,11 @@ namespace BEEV FatalError("toSATandSolve: Nothing to Solve", ASTUndefined); } +#ifdef CRYPTOMINISAT + newS.startClauseAdding(); +#endif //iterate through the list (conjunction) of ASTclauses cll - ClauseList::const_iterator i = cll.begin(), iend = cll.end(); - //ClauseList::reverse_iterator i = cll.rbegin(), iend = cll.rend(); + ClauseList::const_iterator i = cll.begin(), iend = cll.end(); for (int count=0, flag=0; i != iend; i++) { //Clause for the SATSolver -- 2.47.3