Adding --debug option

src/approxmc.cpp

@@ -133,6 +133,11 @@ DLL_PUBLIC void AppMC::set_delta(double delta)
     data->conf.delta = delta;
 }
 
+DLL_PUBLIC void AppMC::set_debug(int debug) { data->conf.debug = debug; }
+DLL_PUBLIC void AppMC::set_force_sol_extension(int val) {
+    data->conf.force_sol_extension = val;
+}
+
 DLL_PUBLIC void AppMC::set_start_iter(uint32_t start_iter)
 {
     data->conf.start_iter = start_iter;

src/approxmc.h

@@ -105,6 +105,8 @@ class AppMC
     void set_sparse(uint32_t sparse);
     void set_simplify(uint32_t simplify);
     void set_dump_intermediary_cnf(const int dump_intermediary_cnf);
+    void set_debug(int debug);
+    void set_force_sol_extension(int val);
 
     //Querying default values
     const std::vector<uint32_t>& get_sampling_set() const;

src/config.h

@@ -50,6 +50,8 @@ struct Config {
     std::string logfilename = "";
     int cms_detach_xor = 1;
     int dump_intermediary_cnf = 0;
+    int debug = 0;
+    int force_sol_extension = false;
 };
 
 }

src/counter.cpp

@@ -237,7 +237,7 @@ SolNum Counter::bounded_sol_count(
     double last_found_time = cpuTimeTotal();
     vector<vector<lbool>> models;
     while (solutions < maxSolutions) {
-        lbool ret = solver->solve(&new_assumps, true);
+        lbool ret = solver->solve(&new_assumps, !conf.force_sol_extension);
         assert(ret == l_False || ret == l_True);
         if ((conf.dump_intermediary_cnf >= 2 && ret == l_True) ||
             (conf.dump_intermediary_cnf >= 1 && ret == l_False)) {
@@ -794,9 +794,30 @@ void Counter::check_model(
     const vector<lbool>& model,
     const HashesModels* const hm,
     const uint32_t hashCount
-)
-{
+) {
     for(uint32_t var: conf.sampling_set) assert(model[var] != l_Undef);
+    if (conf.debug) {
+        assert(conf.force_sol_extension);
+        assert(conf.dump_intermediary_cnf);
+        for(const auto& cl: cls_in_solver) {
+            bool sat = false;
+            for(const auto& l: cl) {
+                assert(model[l.var()] != l_Undef);
+                if ((model[l.var()] == l_True && !l.sign()) ||
+                    (model[l.var()] == l_False && l.sign())) {sat = true; break;}
+            }
+            assert(sat);
+        }
+        for(const auto& x: xors_in_solver) {
+            bool sat = !x.second;
+            for(const auto& v: x.first) {
+                assert(model[v] != l_Undef);
+                sat ^= (model[v] == l_True);
+            }
+            assert(sat);
+        }
+    }
+
     if (!hm) return;
 
     for(const auto& h: hm->hashes) {

src/main.cpp

@@ -80,6 +80,7 @@ bool sampling_vars_found = false;
 int ignore_sampl_set = 0;
 int do_arjun = 1;
 int debug_arjun = 0;
+int debug = 0;
 int with_e = 1;
 
 void add_appmc_options()
@@ -115,6 +116,7 @@ void add_appmc_options()
          "Logs of ApproxMC execution")
     ("ignore", po::value(&ignore_sampl_set)->default_value(ignore_sampl_set)
         , "Ignore given sampling set and recompute it with Arjun")
+    ("debug", po::value(&debug)->default_value(debug), "Turn on more heavy internal debugging")
     ;
 
     ArjunNS::Arjun tmpa;
@@ -477,6 +479,12 @@ void set_approxmc_options()
     appmc->set_simplify(simplify);
     appmc->set_var_elim_ratio(var_elim_ratio);
     appmc->set_dump_intermediary_cnf(dump_intermediary_cnf);
+    appmc->set_force_sol_extension(force_sol_extension);
+    if (debug) {
+        appmc->set_force_sol_extension(1);
+        appmc->set_debug(1);
+        appmc->set_dump_intermediary_cnf(std::max(dump_intermediary_cnf, 1));
+    }
 
     if (logfilename != "") {
         appmc->set_up_log(logfilename);