seed to get different samples

meelgroup · Nov 30, 2023 · b9e3a2f · b9e3a2f
1 parent 4413e46
commit b9e3a2f
Show file tree

Hide file tree

Showing 6 changed files with 14 additions and 5 deletions.
diff --git a/README.markdown b/README.markdown
@@ -53,9 +53,10 @@ The [SMT-LIB2](https://smtlib.cs.uiowa.edu/language.shtml) format is the recomme
 Run with an SMT-LIB2 file:
 
 ```
-./stp --unisamp myproblem.smt2
+./stp --unisamp --seed 6 myproblem.smt2
 ```
 
+Change seed value to get different samples.
 
 ### Usage
 

diff --git a/include/stp/STPManager/UserDefinedFlags.h b/include/stp/STPManager/UserDefinedFlags.h
@@ -140,6 +140,7 @@ struct UserDefinedFlags
 
   int64_t timeout_max_conflicts = -1;
   int num_solver_threads = 1;
+  uint64_t unisamp_seed = 12345;
   int64_t timeout_max_time = -1; // seconds
 
   // check the counterexample against the original input to STP

diff --git a/include/stp/Sat/UniSamp.h b/include/stp/Sat/UniSamp.h
@@ -53,9 +53,10 @@ namespace stp
   ApproxMC::AppMC* a;
   UniGen::UniG* s;
   ArjunNS::Arjun* arjun;
+  uint64_t seed;
 
 public:
-  UniSamp();
+  UniSamp(uint64_t unisamp_seed);
 
   ~UniSamp();
 

diff --git a/lib/STPManager/STP.cpp b/lib/STPManager/STP.cpp
@@ -112,7 +112,7 @@ SATSolver* STP::get_new_sat_solver()
       break;
     case UserDefinedFlags::UNIGEN_SOLVER:
 #ifdef USE_UNIGEN
-      newS = new UniSamp();
+      newS = new UniSamp(bm->UserFlags.unisamp_seed);
 #else
       std::cerr << "UniSamp support was not enabled at configure time."
                 << std::endl;

diff --git a/lib/Sat/UniSamp.cpp b/lib/Sat/UniSamp.cpp
@@ -53,15 +53,17 @@ void UniSamp::enableRefinement(const bool enable)
   //   }
 }
 
-UniSamp::UniSamp()
+UniSamp::UniSamp(uint64_t unisamp_seed)
 {
 
   a = new ApproxMC::AppMC;
   s = new UniG(a);
   arjun = new ArjunNS::Arjun;
+  seed = unisamp_seed;
 
   s->set_callback(mycallback, NULL);
   a->set_verbosity(1);
+  a->set_seed(seed);
   // s->log_to_file("stp.cnf");
   //s->set_num_threads(num_threads);
   //s->set_default_polarity(false);

diff --git a/tools/stp/main.cpp b/tools/stp/main.cpp
@@ -250,7 +250,11 @@ void ExtraMain::create_options()
 #endif
 #endif
               )
-           ("unisamp", "use unisamp as solver -- behave as a uniform sampler");
+           ("unisamp", "use unisamp as solver -- behave as a uniform sampler")
+           ("seed",
+                     po::value<uint64_t>(&bm->UserFlags.unisamp_seed)
+                         ->default_value(bm->UserFlags.unisamp_seed),
+                     "Seed for UniSamp");
 
   po::options_description refinement_options("Refinement options");
   refinement_options.add_options()(