From 505e5c658116bbad3e2feaf33e8458274624a43e Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 30 Oct 2009 18:20:38 +0000
Subject: [PATCH] added missing #ifdef CRYPTOMINISAT in STP.cpp to instantiate
 appropriate solver

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@370 e59a4935-1847-0410-ae03-e826735625c1
---
 scripts/Makefile.common |  8 ++++----
 src/STPManager/STP.cpp  | 31 ++++++++++++++++++++-----------
 2 files changed, 24 insertions(+), 15 deletions(-)

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 6d47734..2b74faa 100644
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -20,16 +20,16 @@ CFLAGS_BASE   = $(OPTIMIZE)
 #CFLAGS_BASE   = $(OPTIMIZE) -DCRYPTOMINISAT
 
 # OPTION to compile in MiniSAT
-CORE          = true
-CFLAGS_BASE   = $(OPTIMIZE) -DCORE
+#CORE          = true
+#CFLAGS_BASE   = $(OPTIMIZE) -DCORE
 
 # OPTION to compile in UNSOUND MiniSAT
 #UNSOUND       = true
 #CFLAGS_BASE   = $(OPTIMIZE) -DUNSOUND
 
 # OPTION to compile in Simplifying MiniSAT
-#SIMP          = true
-#CFLAGS_BASE   = $(OPTIMIZE) -DSIMP
+SIMP          = true
+CFLAGS_BASE   = $(OPTIMIZE) -DSIMP
 
 SHELL=/bin/bash
 
diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index b2bfeb8..c8d9127 100644
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -34,19 +34,23 @@ namespace BEEV {
 
         if(bm->UserFlags.optimize_flag) 
           {
-
             bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap);
             simplified_solved_InputToSAT = 
-              arrayTransformer->CreateSubstitutionMap(simplified_solved_InputToSAT);
+              arrayTransformer->
+	      CreateSubstitutionMap(simplified_solved_InputToSAT);
+
             bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap);
             //printf("##################################################\n");
-            bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+            bm->ASTNodeStats("after pure substitution: ", 
+			     simplified_solved_InputToSAT);
 
 
             simplified_solved_InputToSAT = 
-              simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
+              simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, 
+					     false);
 
-            bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
+            bm->ASTNodeStats("after simplification: ", 
+			     simplified_solved_InputToSAT);
           }
 
         if(bm->UserFlags.wordlevel_solve_flag)
@@ -74,13 +78,17 @@ namespace BEEV {
           {
             bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap);
             simplified_solved_InputToSAT = 
-              arrayTransformer->CreateSubstitutionMap(simplified_solved_InputToSAT);
+              arrayTransformer->
+	      CreateSubstitutionMap(simplified_solved_InputToSAT);
             bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap);
-            bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+            bm->ASTNodeStats("after pure substitution: ",
+			     simplified_solved_InputToSAT);
 
             simplified_solved_InputToSAT = 
-              simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
-            bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
+              simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, 
+					     false);
+            bm->ASTNodeStats("after simplification: ", 
+			     simplified_solved_InputToSAT);
           }
         
         if(bm->UserFlags.wordlevel_solve_flag)
@@ -124,11 +132,12 @@ namespace BEEV {
 #ifdef CORE
     MINISAT::Solver newS;
 #endif
-
+#ifdef CRYPTOMINISAT
+    MINISAT::Solver newS;
+#endif
 #ifdef SIMP
     MINISAT::SimpSolver newS;
 #endif
-
 #ifdef UNSOUND
     MINISAT::UnsoundSimpSolver newS;
 #endif
-- 
2.47.3