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

diff --git a/AUTHORS b/AUTHORS
index 298b818b87b8251051826df9491f51655315971a..25cfc3c3b74c280019e80787b17d032f2c392824 100644 (file)
--- 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 1508592f0b65ae73173da920133d3a9314653ed1..0d231fabadfb065234e55cbbb73f14adb23b7f42 100644 (file)
--- 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 17ca581e37804471aa2e9fa91fa19e69bceafde1..b609ba09c06f2a5c6036a180ddeb57273c6ca058 100644 (file)
--- 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 8cc444e1f8921d832be29b6d1828afb7501f5346..42320f87796f07eb3cbd12d127400b9f797970e3 100644 (file)
--- 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 816bbe75d46437a23ba48c91e3c46b0ee6b2fa15..9e3f5954fa2e0fb27f9b56cb2cce4b0c25ee53ac 100644 (file)
--- 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 da491e20042177800e46d145b5b60c5ebd0c6b2b..ac9e064f5e766cd0ef43c5935764fab1aaebbae7 100644 (file)
--- 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 8cc444e1f8921d832be29b6d1828afb7501f5346..42320f87796f07eb3cbd12d127400b9f797970e3 100644 (file)
--- 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 2e35d1a1ee320437e6a616dda29474c739d09512..8fa77d78e6bfe2580c0f349098950ee903c47aa5 100644 (file)
--- 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 ef22d8dcadbe2ee4fb53e54995b312be132bcaf8..7520196c3aceb161e88240147954e31f4139c74b 100644 (file)
--- 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 d52701eb958b5ed179605f67b3bfe057ee1b93c0..ec8b899df8d0b3f64da473ed7775c15f33787bab 100644 (file)
--- 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 a150a4fd93bf4ce7bcf284cceff324e8b976120b..50d1c0404c36ad114bf5e7cada0cf9e285753821 100644 (file)
--- 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 d753d3d6ad77fa6826a5a868ba16f918481a67b7..88f7dfb48b80179aa6ee27856864765397a110f8 100644 (file)
--- 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 c6714d3d7747dfdccca15a6f0b04cfe275593da0..60b4f34dc6c80d1fde490628ece4eb10c8c5abe9 100644 (file)
--- 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