From 9de1f476216d457c45033da50c44367d7b327230 Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 29 Oct 2009 22:23:00 +0000
Subject: [PATCH] added compile flags to select between the various SAT solvers
 (CryptoMiniSAT, MiniSAT, Simplifying MiniSAT, Unsound MiniSAT)

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@365 e59a4935-1847-0410-ae03-e826735625c1
---
 Makefile                 | 11 ++++++++---
 scripts/Makefile.common  | 12 ++++++++++--
 scripts/Makefile.in      | 11 ++++++++---
 src/STPManager/STP.cpp   | 14 ++++++++++++--
 src/sat/Makefile         |  4 ++++
 src/sat/sat.h            | 24 +++++++++++++++++-------
 src/sat/simp/Makefile    |  2 +-
 src/sat/unsound/Makefile |  2 +-
 8 files changed, 61 insertions(+), 19 deletions(-)

diff --git a/Makefile b/Makefile
index e9bf50f..c0d5cd1 100644
--- 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 be4d812..f546940 100644
--- 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 e9bf50f..c0d5cd1 100644
--- 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 f4b5ea4..b2bfeb8 100644
--- 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 f7f96f2..f4524d9 100644
--- 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 12b8033..1c40435 100644
--- 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 3d5a7bb..8ba1436 100644
--- 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 f57ec3f..5d12328 100644
--- 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)
-- 
2.47.3