debugged unigen and cmsgen to correctly give multisample [working]

meelgroup · Apr 3, 2024 · 7892cc6 · 7892cc6
1 parent da775a3
commit 7892cc6
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 20 deletions.
diff --git a/include/stp/Sat/UniSamp.h b/include/stp/Sat/UniSamp.h
@@ -60,7 +60,7 @@ class UniSamp : public SATSolver
 
 public:
   UniSamp(uint64_t unisamp_seed, uint64_t samples_needed,
-          uint64_t samples_generated);
+          uint64_t _samples_generated);
 
   ~UniSamp();
 

diff --git a/lib/STPManager/STP.cpp b/lib/STPManager/STP.cpp
@@ -115,7 +115,7 @@ SATSolver* STP::get_new_sat_solver()
     case UserDefinedFlags::UNIGEN_SOLVER:
 #ifdef USE_UNIGEN
       newS = new UniSamp(bm->UserFlags.unisamp_seed, bm->UserFlags.num_samples,
-                         bm->UserFlags.samples_generated);
+      bm->UserFlags.samples_generated);
 #else
       std::cerr << "UniSamp support was not enabled at configure time."
                 << std::endl;
@@ -125,7 +125,7 @@ SATSolver* STP::get_new_sat_solver()
     case UserDefinedFlags::APPROXMC_SOLVER:
 #ifdef USE_UNIGEN
       newS = new UniSamp(bm->UserFlags.unisamp_seed, bm->UserFlags.num_samples,
-                         bm->UserFlags.samples_generated);
+      bm->UserFlags.samples_generated);
 #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
@@ -123,8 +123,10 @@ bool UniSamp::solve(bool& timeout_expired) // Search without assumptions.
    */
 
   // CMSat::lbool ret = s->solve(); // TODO AS
-  samples_generated += 1;
-  if (unisamp_ran)
+  samples_generated++;
+  std::cout << "c [stp->unigen] Generating Sample number " << samples_generated
+            << std::endl;
+  if (samples_generated > 1)
     return true;
 
   std::cout << "c [stp->unigen] UniSamp solving instance with " << a->nVars()
@@ -189,7 +191,7 @@ uint8_t UniSamp::modelValue(uint32_t x) const
 {
   //   if (unigen_models[0].size() < sampling_vars.size())
   //     std::cout << "c [stp->unigen] ERROR! found model size is not large enough\n";
-  return (unigen_models[samples_generated - 1].at(x) > 0);
+  return (unigen_models[samples_generated].at(x) > 0);
 }
 
 uint32_t UniSamp::newVar()

diff --git a/tools/stp/main.cpp b/tools/stp/main.cpp
@@ -249,20 +249,19 @@ void ExtraMain::create_options()
                          "(default)"
 #endif
 #endif
-                  )("unisamp,u", "use unisamp as solver -- behave as a almost "
-                                 "uniform sampler")(
-                  "cmsgen,s",
-                  "use cmsgen as solver -- behave as a uniform like sampler")(
-                  "approxmc,c",
-                  "use approxmc as solver -- behave as a approximate counter")(
-                  "seed",
-                  po::value<uint64_t>(&bm->UserFlags.unisamp_seed)
-                      ->default_value(bm->UserFlags.unisamp_seed),
-                  "Seed for counting and sampling")(
-                  "num-samples,ns",
-                  po::value<uint64_t>(&bm->UserFlags.num_samples)
-                      ->default_value(bm->UserFlags.num_samples),
-                  "Number of samples to generate in case of sampling");
+          )("unisamp,u", "use unisamp as solver -- behave as a almost-uniform sampler")(
+          "cmsgen,s",
+          "use cmsgen as solver -- behave as a uniform like sampler")(
+          "approxmc,c",
+          "use approxmc as solver -- behave as a approximate counter")(
+          "seed",
+          po::value<uint64_t>(&bm->UserFlags.unisamp_seed)
+              ->default_value(bm->UserFlags.unisamp_seed),
+          "Seed for counting and sampling")(
+          "num-samples,ns",
+          po::value<uint64_t>(&bm->UserFlags.num_samples)
+              ->default_value(bm->UserFlags.num_samples),
+          "Number of samples to generate in sampling mode");
   ;
 
   po::options_description refinement_options("Refinement options");