running

CMakeLists.txt

@@ -638,7 +638,7 @@ set(LIBS ${LIBS} ${MINISAT_LIBRARIES})
 # not provide new enough versions for us to use.
 if (CMAKE_HOST_SYSTEM_NAME MATCHES "Darwin")
     execute_process(
-        COMMAND brew --prefix bison 
+        COMMAND brew --prefix bison
         RESULT_VARIABLE BREW_BISON
         OUTPUT_VARIABLE BREW_BISON_PREFIX
         OUTPUT_STRIP_TRAILING_WHITESPACE

include/stp/STPManager/UserDefinedFlags.h

@@ -155,7 +155,9 @@ struct UserDefinedFlags
     MINISAT_SOLVER = 0,
     SIMPLIFYING_MINISAT_SOLVER,
     CRYPTOMINISAT5_SOLVER,
+    APPROXMC_SOLVER,
     UNIGEN_SOLVER,
+    CMSGEN_SOLVER,
     RISS_SOLVER
   };
 

lib/STPManager/STP.cpp

@@ -118,6 +118,24 @@ SATSolver* STP::get_new_sat_solver()
       std::cerr << "UniSamp support was not enabled at configure time."
                 << std::endl;
       exit(-1);
+#endif
+      break;
+    case UserDefinedFlags::APPROXMC_SOLVER:
+#ifdef USE_UNIGEN
+      newS = new UniSamp(bm->UserFlags.unisamp_seed);
+#else
+      std::cerr << "UniSamp support was not enabled at configure time."
+                << std::endl;
+      exit(-1);
+#endif
+      break;
+    case UserDefinedFlags::CMSGEN_SOLVER:
+#ifdef USE_UNIGEN
+      newS = new CMSGenC(bm->UserFlags.unisamp_seed);
+#else
+      std::cerr << "UniSamp support was not enabled at configure time."
+                << std::endl;
+      exit(-1);
 #endif
       break;
     case UserDefinedFlags::RISS_SOLVER:

lib/Sat/CMSGen.cpp

@@ -42,10 +42,12 @@ void CMSGenC::enableRefinement(const bool enable)
   }
 }
 
-CMSGenC::CMSGenC(int num_threads)
+CMSGenC::CMSGenC(int seed)
 {
   s = new CMSGen::SATSolver;
   temp_cl = (void*)new vector<CMSGen::Lit>;
+  // s->set_seed(seed);
+  // TODO - set seed
 }
 
 CMSGenC::~CMSGenC()

tools/stp/main.cpp

@@ -250,11 +250,13 @@ void ExtraMain::create_options()
 #endif
 #endif
               )
-           ("unisamp", "use unisamp as solver -- behave as a uniform sampler")
+           ("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 UniSamp");
+                     "Seed for counting and sampling");
 
   po::options_description refinement_options("Refinement options");
   refinement_options.add_options()(
@@ -290,7 +292,7 @@ void ExtraMain::create_options()
       "print-arrayval,q",
       po::bool_switch(&(bm->UserFlags.print_arrayval_declaredorder_flag)),
       "print arrayval declared order")(
-      "print-functionstat,s", po::bool_switch(&(bm->UserFlags.stats_flag)),
+      "print-functionstat", po::bool_switch(&(bm->UserFlags.stats_flag)),
       "print function statistics")(
       "print-quickstat,t",
       po::bool_switch(&(bm->UserFlags.quick_statistics_flag)),
@@ -482,6 +484,14 @@ int ExtraMain::parse_options(int argc, char** argv)
   {
     bm->UserFlags.solver_to_use = UserDefinedFlags::UNIGEN_SOLVER;
   }
+  if (vm.count("cmsgen"))
+  {
+    bm->UserFlags.solver_to_use = UserDefinedFlags::CMSGEN_SOLVER;
+  }
+  if (vm.count("approxmc"))
+  {
+    bm->UserFlags.solver_to_use = UserDefinedFlags::APPROXMC_SOLVER;
+  }
 #endif
 
   if (vm.count("disable-simplifications"))