Improvement. Ability to give a random number to the SAT solver.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 13fbad617f273d35f2bbe45c97c5ce2bb4a3ab22..683614434e11a2e2ecaccb94d72ce394d242340b 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -72,6 +72,11 @@ namespace BEEV {
        NewSolver.setVerbosity(1);
       }
     
+    if(bm->UserFlags.random_seed_flag)
+      {
+        NewSolver.setSeed(bm->UserFlags.random_seed);
+      }
+
        SOLVER_RETURN_TYPE result;
     result = TopLevelSTPAux(NewSolver,
                              original_input);

diff --git a/src/main/main.cpp b/src/main/main.cpp
index d2607852fa66cd78e53323fc5f9dcfeb9e8c8272..ac08bb2ab7a0b60adca40d2117503bd9569fa30c 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -78,7 +78,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_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP,EXIT_AFTER_CNF,USE_CRYPTOMINISAT_SOLVER,USE_MINISAT_SOLVER, DISABLE_SIMPLIFICATIONS, OLDSTYLE_REFINEMENT, DISABLE_EQUALITY} OptionType;
+typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP,EXIT_AFTER_CNF,USE_CRYPTOMINISAT_SOLVER,USE_MINISAT_SOLVER, DISABLE_SIMPLIFICATIONS, OLDSTYLE_REFINEMENT, DISABLE_EQUALITY, RANDOM_SEED} OptionType;
 
 
 int main(int argc, char ** argv) {
@@ -153,6 +153,7 @@ int main(int argc, char ** argv) {
     "-g <time_in_sec>       : timeout (seconds until STP gives up)\n"
     "-h                     : help\n"
     "-i <random_seed>       : Randomize STP's satisfiable output. Random_seed is an integer >= 0\n"
+    "--random-seed          : Generate a random number for the SAT solver.\n"
     "-p                     : print counterexample\n"
     "-s                     : print function statistics\n"
     "-t                     : print quick statistics\n"
@@ -190,6 +191,7 @@ int main(int argc, char ** argv) {
                          lookup.insert(make_pair(tolower("--disable-simplify"),DISABLE_SIMPLIFICATIONS));
                          lookup.insert(make_pair(tolower("--oldstyle-refinement"),OLDSTYLE_REFINEMENT));
                          lookup.insert(make_pair(tolower("--disable-equality"),DISABLE_EQUALITY));
+                         lookup.insert(make_pair(tolower("--random-seed"),RANDOM_SEED));
 
 
                          if (!strncmp(argv[i],"--config_",strlen("--config_")))
@@ -284,6 +286,13 @@ int main(int argc, char ** argv) {
                           case DISABLE_EQUALITY:
                                   bm->UserFlags.propagate_equalities = false;
                                   break;
+                          case RANDOM_SEED:
+                            {
+                                srand(time(NULL));
+                                bm->UserFlags.random_seed_flag = true;
+                                bm->UserFlags.random_seed = rand();
+                            }
+                            break;
 
                          default:
                                  fprintf(stderr,usage,prog);

diff --git a/src/sat/CryptoMinisat.h b/src/sat/CryptoMinisat.h
index c7832e0c885bf13a52e8968b08d06c79973a7c4d..4a45c97119cafc7669543f120d0061c49eeb24a6 100644 (file)
--- a/src/sat/CryptoMinisat.h
+++ b/src/sat/CryptoMinisat.h
@@ -1,8 +1,8 @@
 /*
- * Wraps around CORE minisat.
+ * Wraps around Cryptominisat minisat.
  */
-#ifndef MINISATCORE_H_
-#define MINIASTCORE_H_
+#ifndef CRYPTOMINISAT_H_
+#define CRYPTOMINISAT_H_
 
 #include "SATSolver.h"
 

diff --git a/src/sat/MinisatCore.cpp b/src/sat/MinisatCore.cpp
index 9733bdf1a26c78f73d20e7a487c3728b96eec7fb..c655fa2f252cd36b6338241d10ab80ba54321e88 100644 (file)
--- a/src/sat/MinisatCore.cpp
+++ b/src/sat/MinisatCore.cpp
@@ -63,6 +63,13 @@ namespace BEEV
     s->verbosity = v;
   }
 
+    template <class T>
+    void MinisatCore<T>::setSeed(int i)
+    {
+      s->random_seed = i;
+    }
+
+
   template <class T>
   int MinisatCore<T>::nVars()
   {return s->nVars();}

diff --git a/src/sat/MinisatCore.h b/src/sat/MinisatCore.h
index 58e89ba788c1f6c6dab76c8035cbd902e1bbc318..0f4d02edfdb0211a5a19090772440d758d3659cc 100644 (file)
--- a/src/sat/MinisatCore.h
+++ b/src/sat/MinisatCore.h
@@ -46,11 +46,11 @@ namespace BEEV
 
     void printStats();
 
+    virtual void setSeed(int i);
+
     virtual lbool true_literal() {return ((uint8_t)0);}
     virtual lbool false_literal()  {return ((uint8_t)1);}
     virtual lbool undef_literal()  {return ((uint8_t)2);}
-
-
   };
 }
 ;

diff --git a/src/sat/MinisatCore_prop.cpp b/src/sat/MinisatCore_prop.cpp
index 1a01b7fe8b46392f4dde9e87e6de2d921f829f32..4dacfb7966b5105e1ccbf457f4bd14c151115373 100644 (file)
--- a/src/sat/MinisatCore_prop.cpp
+++ b/src/sat/MinisatCore_prop.cpp
@@ -89,5 +89,11 @@ namespace BEEV
       printf("CPU time              : %g s\n", cpu_time);
     }
 
+  template <class T>
+  void MinisatCore_prop<T>::setSeed(int i)
+  {
+    s->random_seed = i;
+  }
+
   template class MinisatCore_prop<Minisat::Solver_prop>;
 };

diff --git a/src/sat/MinisatCore_prop.h b/src/sat/MinisatCore_prop.h
index 9145bb3dea2b31639384465bc6eb1cb4588b2175..5dc36886963007eaaa009827d9b63aa6cd25ea19 100644 (file)
--- a/src/sat/MinisatCore_prop.h
+++ b/src/sat/MinisatCore_prop.h
@@ -1,8 +1,8 @@
 /*
- * Wraps around CORE minisat.
+ * Wraps around minisat with array propagators
  */
-#ifndef MINISATCORE_H_
-#define MINIASTCORE_H_
+#ifndef MINISATCORE_PROP_H_
+#define MINIASTCORE_PROP_H_
 
 #include "SATSolver.h"
 
@@ -53,7 +53,7 @@ namespace BEEV
     virtual lbool false_literal()  {return ((uint8_t)1);}
     virtual lbool undef_literal()  {return ((uint8_t)2);}
 
-
+    virtual void setSeed(int i);
   };
 }
 ;

diff --git a/src/sat/SATSolver.h b/src/sat/SATSolver.h
index 38839dff530b86ff9f16d498a9a6a49c54f2a836..af0df23a214193ff5f89ac73939faa117c4980af 100644 (file)
--- a/src/sat/SATSolver.h
+++ b/src/sat/SATSolver.h
@@ -56,7 +56,10 @@ namespace BEEV
     virtual void printStats() = 0;
 
     virtual void setSeed(int i)
-    {}
+    {
+      std::cerr << "Setting the random seen is not implemented for this solver" << std::endl;
+      exit(1);
+    }
 
     virtual int setVerbosity(int v) =0;
 

diff --git a/src/sat/SimplifyingMinisat.cpp b/src/sat/SimplifyingMinisat.cpp
index 7bd529596dbe7b4c1925189a8cb7aa3bcbae7dfa..3794445ff0271e7b55c65c025d9489f38c82e4a8 100644 (file)
--- a/src/sat/SimplifyingMinisat.cpp
+++ b/src/sat/SimplifyingMinisat.cpp
@@ -52,6 +52,11 @@ namespace BEEV
     s->verbosity = v;
   }
 
+  void SimplifyingMinisat::setSeed(int i)
+    {
+      s->random_seed = i;
+    }
+
   Minisat::Var
   SimplifyingMinisat::newVar()
   {

diff --git a/src/sat/SimplifyingMinisat.h b/src/sat/SimplifyingMinisat.h
index 314b188b01c6bb49378a11ea38ee26ea0dbfa0d3..7c746e5d46ae7c5836a5e5c7c51ccf8e2f96bb4f 100644 (file)
--- a/src/sat/SimplifyingMinisat.h
+++ b/src/sat/SimplifyingMinisat.h
@@ -1,8 +1,8 @@
 /*
  * Wraps around Simplifying minisat.
  */
-#ifndef CORE_H_
-#define CORE_H_
+#ifndef SIMPLIFYINGMINISAT_H_
+#define SIMPLIFYINGMINISAT_H_
 
 #include "SATSolver.h"
 
@@ -44,6 +44,8 @@ namespace BEEV
 
     void printStats();
 
+    virtual void setSeed(int i);
+
     virtual lbool true_literal() {return ((uint8_t)0);}
     virtual lbool false_literal()  {return ((uint8_t)1);}
     virtual lbool undef_literal()  {return ((uint8_t)2);}