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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 6d47734dff89577bab3299bba1dd15096518a816..2b74faa3476b390a93f40cf2553ce237108d9d16 100644 (file)
--- 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 b2bfeb8328d9ce1d0b2b7b983baa1c32142fb3b8..c8d9127e0c231998511414e72b67a2c65b31e71a 100644 (file)
--- 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