pass sampling vars to sampling modes as well

meelgroup · Nov 15, 2024 · b18d3c2 · b18d3c2
1 parent fb2fbe1
commit b18d3c2
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 11 deletions.
diff --git a/include/stp/Sat/CMSGen.h b/include/stp/Sat/CMSGen.h
@@ -33,6 +33,7 @@ THE SOFTWARE.
 #include "stp/Sat/SATSolver.h"
 #include "cmsgen/cmsgen.h"
 #include <unordered_set>
+#include <vector>
 // clang-format on
 namespace CMSGenNS
 {

diff --git a/include/stp/Sat/UniSamp.h b/include/stp/Sat/UniSamp.h
@@ -58,6 +58,7 @@ class UniSamp : public SATSolver
   uint64_t samples_generated = 0;
   uint64_t samples_needed = 0;
   bool unisamp_ran;
+  vector<uint32_t> sampling_vars_orig;
 
 public:
   UniSamp(uint64_t unisamp_seed, uint64_t samples_needed,

diff --git a/lib/Sat/ApxMC.cpp b/lib/Sat/ApxMC.cpp
@@ -116,7 +116,6 @@ bool ApxMC::solve(bool& timeout_expired) // Search without assumptions.
   for (uint32_t i = 0; i < arjun->nVars(); i++)
     sampling_vars.push_back(i);
 
-  arjun->set_seed(5);
   arjun->set_seed(seed);
   arjun->set_verbosity(0);
   arjun->set_simp(1);
@@ -149,9 +148,6 @@ bool ApxMC::solve(bool& timeout_expired) // Search without assumptions.
 
   delete arjun;
 
-  //TODO AS: this is debugging as Arjun is not performing correctly
-  //sampling_vars = sampling_vars_orig;
-
   a->set_sampl_vars(sampling_vars);
 
   auto sol_count = a->count();

diff --git a/lib/Sat/CMSGen.cpp b/lib/Sat/CMSGen.cpp
@@ -104,6 +104,8 @@ bool CMSGenC::solve(bool& timeout_expired) // Search without assumptions.
      s->set_max_time(max_time);
   }
 
+  s->set_sampling_vars(&sampling_vars_orig);
+
   CMSGen::lbool ret = s->solve();
   if (ret == CMSGen::l_Undef)
   {
@@ -119,7 +121,8 @@ uint8_t CMSGenC::modelValue(uint32_t x) const
 
 uint32_t CMSGenC::newProjVar(uint32_t x)
 {
-  return 42;
+  sampling_vars_orig.push_back(x);
+  return 1;
 }
 
 uint32_t CMSGenC::newVar()

diff --git a/lib/Sat/UniSamp.cpp b/lib/Sat/UniSamp.cpp
@@ -135,10 +135,10 @@ bool UniSamp::solve(bool& timeout_expired) // Search without assumptions.
   std::cout << "c [stp->unigen] UniSamp solving instance with "
             << arjun->nVars() << " variables." << std::endl;
 
-  vector<uint32_t> sampling_vars, sampling_vars_orig;
+  vector<uint32_t> sampling_vars, all_vars;
   for (uint32_t i = 0; i < arjun->nVars(); i++)
-    sampling_vars.push_back(i);
-  sampling_vars_orig = sampling_vars;
+    all_vars.push_back(i);
+
   arjun->set_sampl_vars(sampling_vars_orig);
 
   const uint32_t orig_num_vars = arjun->nVars();
@@ -192,8 +192,8 @@ bool UniSamp::solve(bool& timeout_expired) // Search without assumptions.
   unigen->set_verb_sampler_cls(0);
   unigen->set_kappa(0.1);
   unigen->set_multisample(false);
-  unigen->set_full_sampling_vars(sampling_vars_orig);
-  unigen->set_empty_sampling_vars(empty_sampl_vars);
+  unigen->set_full_sampling_vars(all_vars);
+  // unigen->set_empty_sampling_vars(empty_sampl_vars);
 
   unigen->sample(&sol_count, samples_needed);
   unisamp_ran = true;
@@ -217,7 +217,8 @@ uint8_t UniSamp::modelValue(uint32_t x) const
 
 uint32_t UniSamp::newProjVar(uint32_t x)
 {
-  return 42;
+  sampling_vars_orig.push_back(x);
+  return 1;
 }
 
 uint32_t UniSamp::newVar()