If STP is compiled with minisat-core, add a command line option to enable simplifying...

We now have two versions of STP: one for cryptominisat1/2 another for minisat/simplifying minisat.

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index fe16bb25355c882104c053fa11875268e2a21f12..05a2c4e7ba93b41efc01a9a05a550d9197276fb0 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -35,14 +35,6 @@ ifeq ($(SAT),minisat)
   SOLVER_INCLUDE = $(TOP)/src/sat/core
 endif
 
-# OPTION to compile Simplifying MiniSAT
-ifeq ($(SAT),simp)
-  SIMP           = true
-  CFLAGS_BASE    = $(OPTIMIZE) -DSIMP
-  MTL            = $(TOP)/src/sat/mtl
-  SOLVER_INCLUDE = $(TOP)/src/sat/simp
-endif
-
 SHELL=/bin/bash
 
 # You can compile using make STATIC=true to compile a statically

diff --git a/scripts/configure b/scripts/configure
index d3773a3347e90b6a1979b4e9b9faab7a70dcf8de..039f084f359cccef3265e14eaf2e6dfe575a8084 100755 (executable)
--- a/scripts/configure
+++ b/scripts/configure
@@ -21,16 +21,13 @@ while [ $# -gt 0 ]; do
            echo "Using g++ instead of gcc";;
        --with-minisat-core)
            SAT=minisat;;
-       --with-minisat-simp)
-           SAT=simp;;
        --with-cryptominisat2)
            SAT=cryptominisat2;;
        *)
            echo "Usage: $0 [options]"
            echo "   --with-prefix=/prefix/path   Install STP at the specified path"
            echo "   --with-g++=/path/to/g++      Use g++ at the specified path"
-           echo "   --with-minisat-core          Use core MiniSAT solver (default)"
-           echo "   --with-minisat-simp          Use simplifying MiniSAT solver"
+           echo "   --with-minisat-core          Use core MiniSAT solver (default), runtime option to use simplifying"
            echo "   --with-cryptominisat2        Use CRYPTOMiniSAT 2.x solver"
            echo "$0 failed"
            exit 1;;

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 84aafb2ba6b58302ef04b233905e0bdc1e1e5c6e..d81daeeba26ec5a86eff530d949d30f374a61866 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -21,7 +21,7 @@ namespace BEEV {
                                            bm->CreateNode(NOT, query));
     
     //solver instantiated here
-#if defined CORE || defined CRYPTOMINISAT || defined CRYPTOMINISAT2
+#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2
     MINISAT::Solver NewSolver;
 #endif
 
@@ -32,8 +32,16 @@ namespace BEEV {
       }
 #endif
 
-#ifdef SIMP
-    MINISAT::SimpSolver NewSolver;
+#if defined CORE
+       MINISAT::Solver *newS;
+    if (bm->UserFlags.solver_to_use == UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER)
+               newS = new MINISAT::SimpSolver();
+    else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_SOLVER)
+               newS = new MINISAT::Solver();
+    else
+       FatalError("unknown option");
+
+    MINISAT::Solver& NewSolver = *newS;
 #endif
 
     if(bm->UserFlags.stats_flag)
@@ -41,16 +49,24 @@ namespace BEEV {
        NewSolver.verbosity = 1;
       }
     
+       SOLVER_RETURN_TYPE result;
     if(bm->UserFlags.num_absrefine_flag)
       {
-       return UserGuided_AbsRefine(NewSolver,
+     result =  UserGuided_AbsRefine(NewSolver,
                                    original_input);
       }
     else 
       {
-       return TopLevelSTPAux(NewSolver, 
+       result = TopLevelSTPAux(NewSolver,
                              original_input, original_input);
       }
+
+#if defined CORE
+    delete newS;
+#endif
+
+    return result;
+
   } //End of TopLevelSTP()
   
   //Acceps a query, calls the SAT solver and generates Valid/InValid.

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index ea3340f842520025c1a5717136275df0b8d68d90..4dc37231bd92b957d613ba833d0edcee043c2cef 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -106,6 +106,15 @@ namespace BEEV
   
     bool tseitin_are_decision_variables_flag;
 
+    // Available back-end SAT solvers.
+    enum SATSolvers
+      {
+        MINISAT_SOLVER =0,
+        SIMPLIFYING_MINISAT_SOLVER
+      };
+
+    enum SATSolvers solver_to_use;
+
     //CONSTRUCTOR    
     UserDefinedFlags()
     {  
@@ -192,6 +201,10 @@ namespace BEEV
       quick_statistics_flag=false;
 
       tseitin_are_decision_variables_flag=true;
+
+      // use minisat by default.
+      solver_to_use = MINISAT_SOLVER;
+
     } //End of constructor for UserDefinedFlags
 
   }; //End of struct UserDefinedFlags

diff --git a/src/main/main.cpp b/src/main/main.cpp
index bc70f3cae3b5a81e7e562869665d3823532cc4b7..bc129464943b17fb6a5c46957f260539a6a98895 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -47,7 +47,7 @@ static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000;
  * step 5. Call SAT to determine if input is SAT or UNSAT
  ********************************************************************/
 
-typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF} OptionType;
+typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER} OptionType;
 
 int main(int argc, char ** argv) {
   char * infile;
@@ -126,6 +126,12 @@ int main(int argc, char ** argv) {
     "-r  : switch refinement off (optimizations are ON by default)\n";
   helpstring +=  
     "-s  : print function statistics\n";
+
+  #if !defined CRYPTOMINISAT && !defined CRYPTOMINISAT2
+  helpstring +=
+    "--simplifying-minisat : use simplifying-minisat rather than minisat\n";
+  #endif
+
   helpstring +=  
     "-t  : print quick statistics\n";
   helpstring +=  
@@ -152,6 +158,8 @@ int main(int argc, char ** argv) {
                          lookup.insert(make_pair("--print-back-dot",PRINT_BACK_DOT));
                          lookup.insert(make_pair("--output-CNF",OUTPUT_CNF));
                          lookup.insert(make_pair("--output-bench",OUTPUT_BENCH));
+                         lookup.insert(make_pair("--simplifying-minisat",USE_SIMPLIFYING_SOLVER));
+
 
                          switch(lookup[argv[i]])
                          {
@@ -183,6 +191,13 @@ int main(int argc, char ** argv) {
                                  bm->UserFlags.output_bench_flag = true;
                                  break;
 
+#if !defined CRYPTOMINISAT && !defined CRYPTOMINISAT2
+                         case USE_SIMPLIFYING_SOLVER:
+                                 bm->UserFlags.solver_to_use = UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER;
+                                 break;
+#endif
+
+
                          default:
                                  fprintf(stderr,usage,prog);
                       cout << helpstring;

diff --git a/src/sat/Makefile b/src/sat/Makefile
index 5ac03f301d2f14bf4983cd907688640543c63083..010516e54be9ca4d52808819bbe3e072761c0adc 100644 (file)
--- a/src/sat/Makefile
+++ b/src/sat/Makefile
@@ -1,10 +1,6 @@
 .PHONY: core
 core:
        $(MAKE) -C core lib all 
-
-.PHONY: simp
-simp:
-       $(MAKE) -C core lib all 
        $(MAKE) -C simp lib all
 
 .PHONY: cryptominisat
@@ -15,7 +11,6 @@ cryptominisat:
 cryptominisat2:
        $(MAKE) -C cryptominisat2 lib all
 
-
 .PHONY: clean
 clean:
        rm -rf *.o *~ libminisat.a

diff --git a/src/sat/sat.h b/src/sat/sat.h
index 7892b9ec1ea8c62cdf70230c270bf3e45d4e9d10..bfd6c90db9092e18801bdc50c0f258b2b907d3ca 100644 (file)
--- a/src/sat/sat.h
+++ b/src/sat/sat.h
@@ -14,11 +14,7 @@
 #ifdef CORE
 #include "core/Solver.h"
 #include "core/SolverTypes.h"
-#endif
-
-#ifdef SIMP
 #include "simp/SimpSolver.h"
-#include "core/SolverTypes.h"
 #endif
 
 #endif