From e5fab06ca13b723e748c70424581ad45ab351fc2 Mon Sep 17 00:00:00 2001
From: Arijit Shaw <if.arijit@gmail.com>
Date: Tue, 10 Dec 2024 20:23:51 -0500
Subject: [PATCH] approxmc combined with ganak

---
 lib/Sat/GnK.cpp    | 9 +++++++--
 tools/stp/main.cpp | 3 +--
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/lib/Sat/GnK.cpp b/lib/Sat/GnK.cpp
index 1a163960..02a5a7a9 100644
--- a/lib/Sat/GnK.cpp
+++ b/lib/Sat/GnK.cpp
@@ -131,7 +131,8 @@ bool GnK::solve(bool& timeout_expired) // Search without assumptions.
     sampling_vars.push_back(i);
 
   std::cout << "c [stp->gnk] GnK solving instance with " << cnf.nVars()
-            << " variables, " << sampling_vars.size() << " projection vars"
+            << " variables, " << sampling_vars.size() << " projection vars, "
+            << cnf.opt_sampl_vars.size() << " optional projection vars"
             << std::endl;
   // arjun->set_seed(seed);
   // arjun->set_verbosity(0);
@@ -140,6 +141,9 @@ bool GnK::solve(bool& timeout_expired) // Search without assumptions.
   //           << std::endl;
 
   conf.verb = 0;
+  if (seed == 0)
+    conf.appmc_timeout = 1;
+
   Ganak counter(conf, false, true);
   counter.new_vars(cnf.nVars());
 
@@ -169,7 +173,8 @@ bool GnK::solve(bool& timeout_expired) // Search without assumptions.
   delete arjun;
   mpz_class cnt;
   cnt = counter.unw_outer_count();
-  assert(!counter.get_is_approximate());
+  if (counter.get_is_approximate())
+    std::cout << "c count its approximate\n";
   cnt *= cnf.multiplier_weight;
 
   // use gmp to get the absolute count of solutions
diff --git a/tools/stp/main.cpp b/tools/stp/main.cpp
index 48d526aa..9f9aa536 100644
--- a/tools/stp/main.cpp
+++ b/tools/stp/main.cpp
@@ -294,7 +294,7 @@ void ExtraMain::create_options()
                   "use cmsgen as solver -- behave as a uniform like sampler")(
                   "approxmc,c",
                   "use approxmc as solver -- behave as a approximate counter")(
-                  "ganak,g",
+                  "ganak,e",
                   "use ganak as solver -- behave as a exact counter")(
                   "seed",
                   po::value<uint64_t>(&bm->UserFlags.unisamp_seed)
@@ -534,7 +534,6 @@ int ExtraMain::parse_options(int argc, char** argv)
   {
     bm->UserFlags.solver_to_use = UserDefinedFlags::GANAK_SOLVER;
     bm->UserFlags.counting_mode = true;
-    std::cout << "Ganak solver selected" << std::endl;
   }
 #endif