added compile flags to select between the various SAT solvers (CryptoMiniSAT, MiniSAT...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@365 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/Makefile b/Makefile
index e9bf50f13229d668b10aa95c1b42bf372042962a..c0d5cd146a9fc99099837ed3d7b8dce99ff89426 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -20,10 +20,15 @@ all: AST STPManager absrefine_counterexample to-sat simplifier printer c_interfa
 
 ifdef CRYPTOMINISAT
        $(MAKE) -C $(SRC)/sat cryptominisat
-else
+endif
+ifdef CORE
        $(MAKE) -C $(SRC)/sat core
-#      $(MAKE) -C $(SRC)/sat simp
-#      $(MAKE) -C $(SRC)/sat unsound
+endif
+ifdef SIMP
+       $(MAKE) -C $(SRC)/sat simp
+endif
+ifdef UNSOUND
+       $(MAKE) -C $(SRC)/sat unsound
 endif
        $(MAKE) -C $(SRC)/parser
        $(MAKE) -C $(SRC)/main

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index be4d8125cc01b138dbcaee9d619c7513c7c49a39..f546940c709b92def85addc973fc4923936baa0c 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -12,10 +12,18 @@
 OPTIMIZE      = -g                # Debugging
 OPTIMIZE      = -O3 -DNDEBUG      # Maximum optimization
 #OPTIMIZE     = -O3 -DNDEBUG -DLESSBYTES_PERNODE
+#CFLAGS_M32   = -m32
 CFLAGS_BASE   = $(OPTIMIZE)
-#CFLAGS_BASE   = $(OPTIMIZE) -DCRYPTOMINISAT
+
 #CRYPTOMINISAT = true
-#CFLAGS_M32   = -m32
+#CFLAGS_BASE   = $(OPTIMIZE) -DCRYPTOMINISAT
+CORE          = true
+CFLAGS_BASE   = $(OPTIMIZE) -DCORE
+#UNSOUND       = true
+#CFLAGS_BASE   = $(OPTIMIZE) -DUNSOUND
+#SIMP          = true
+#CFLAGS_BASE   = $(OPTIMIZE) -DSIMP
+
 SHELL=/bin/bash
 
 # You can compile using make STATIC=true to compile a statically

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index e9bf50f13229d668b10aa95c1b42bf372042962a..c0d5cd146a9fc99099837ed3d7b8dce99ff89426 100644 (file)
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -20,10 +20,15 @@ all: AST STPManager absrefine_counterexample to-sat simplifier printer c_interfa
 
 ifdef CRYPTOMINISAT
        $(MAKE) -C $(SRC)/sat cryptominisat
-else
+endif
+ifdef CORE
        $(MAKE) -C $(SRC)/sat core
-#      $(MAKE) -C $(SRC)/sat simp
-#      $(MAKE) -C $(SRC)/sat unsound
+endif
+ifdef SIMP
+       $(MAKE) -C $(SRC)/sat simp
+endif
+ifdef UNSOUND
+       $(MAKE) -C $(SRC)/sat unsound
 endif
        $(MAKE) -C $(SRC)/parser
        $(MAKE) -C $(SRC)/main

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index f4b5ea4353a0ead19e6d9d05ecb54a158879be92..b2bfeb8328d9ce1d0b2b7b983baa1c32142fb3b8 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -119,10 +119,20 @@ namespace BEEV {
     bm->TermsAlreadySeenMap_Clear();
 
     SOLVER_RETURN_TYPE res;
+    
     //solver instantiated here
+#ifdef CORE
     MINISAT::Solver newS;
-    //MINISAT::SimpSolver newS;
-    //MINISAT::UnsoundSimpSolver newS;
+#endif
+
+#ifdef SIMP
+    MINISAT::SimpSolver newS;
+#endif
+
+#ifdef UNSOUND
+    MINISAT::UnsoundSimpSolver newS;
+#endif
+
     if (bm->UserFlags.arrayread_refinement_flag)
       {
         bm->counterexample_checking_during_refinement = true;

diff --git a/src/sat/Makefile b/src/sat/Makefile
index f7f96f28d2d7dbf52e3a96c2b5316a95526c87f0..f4524d93eb9d0555b24c31e35049dc67db6ace6e 100644 (file)
--- a/src/sat/Makefile
+++ b/src/sat/Makefile
@@ -5,11 +5,15 @@ core:
 
 .PHONY: simp
 simp:
+       $(MAKE) -C core lib all 
+       mv Solver.or Solver.o
        $(MAKE) -C simp lib all
        mv SimpSolver.or SimpSolver.o
 
 .PHONY: unsound
 unsound:
+       $(MAKE) -C core lib all 
+       mv Solver.or Solver.o
        $(MAKE) -C unsound lib all
        mv UnsoundSimpSolver.or UnsoundSimpSolver.o
 

diff --git a/src/sat/sat.h b/src/sat/sat.h
index 12b8033f946ec77a4babf8c079a9c90c6e454873..1c40435b1fbb2b8f5da85648a8b18d613c192447 100644 (file)
--- a/src/sat/sat.h
+++ b/src/sat/sat.h
@@ -2,13 +2,23 @@
 #define SAT_H_
 
 #ifdef CRYPTOMINISAT
-#include "cryptominisat/Solver.h"
-#include "cryptominisat/SolverTypes.h"
-#else
-#include "core/Solver.h"
-#include "core/SolverTypes.h"
-//#include "simp/SimpSolver.h"
-//#include "unsound/UnsoundSimpSolver.h"
+  #include "cryptominisat/Solver.h"
+  #include "cryptominisat/SolverTypes.h"
+#endif
+
+#ifdef CORE
+  #include "core/Solver.h"
+  #include "core/SolverTypes.h"
+#endif
+
+#ifdef SIMP
+  #include "simp/SimpSolver.h"
+  #include "core/SolverTypes.h"
+#endif
+
+#ifdef UNSOUND
+  #include "unsound/UnsoundSimpSolver.h"
+  #include "core/SolverTypes.h"
 #endif
 
 #endif

diff --git a/src/sat/simp/Makefile b/src/sat/simp/Makefile
index 3d5a7bbe59decadd1fea84a8125d1a89229a03ed..8ba14367f41a35e3d59515881b75ac850c0b387b 100644 (file)
--- a/src/sat/simp/Makefile
+++ b/src/sat/simp/Makefile
@@ -3,7 +3,7 @@ MTL       = ../mtl
 CORE      = ../core
 CHDRS     = $(wildcard *.h) $(wildcard $(MTL)/*.h)
 EXEC      = minisat
-CFLAGS    = -I$(MTL) -I$(CORE) -DEXT_HASH_MAP -Wall -ffloat-store $(CFLAGS_M32)
+CFLAGS    = -I$(MTL) -I$(CORE) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32)
 LFLAGS    = -lz
 
 CSRCS     = $(wildcard *.C)

diff --git a/src/sat/unsound/Makefile b/src/sat/unsound/Makefile
index f57ec3fc97ac3bd458266bdd4706c77a1b6de011..5d12328e5cb0b51be0a16108429d661ecee8cb29 100644 (file)
--- a/src/sat/unsound/Makefile
+++ b/src/sat/unsound/Makefile
@@ -3,7 +3,7 @@ MTL       = ../mtl
 CORE      = ../core
 CHDRS     = $(wildcard *.h) $(wildcard $(MTL)/*.h)
 EXEC      = minisat
-CFLAGS    = -I$(MTL) -I$(CORE) -Wall -ffloat-store $(CFLAGS_M32)
+CFLAGS    = -I$(MTL) -I$(CORE) -ffloat-store $(CFLAGS_M32)
 LFLAGS    = -lz
 
 CSRCS     = $(wildcard *.C)