Improving the dumping capabilities

meelgroup · Oct 3, 2023 · 7fa25b2 · 7fa25b2
1 parent 8ab5426
commit 7fa25b2
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 12 deletions.
diff --git a/src/approxmc.cpp b/src/approxmc.cpp
@@ -301,7 +301,7 @@ DLL_PUBLIC const std::vector<uint32_t>& AppMC::get_sampling_set() const
     return data->conf.sampling_set;
 }
 
-DLL_PUBLIC void AppMC::set_dump_intermediary_cnf(const bool dump_intermediary_cnf)
+DLL_PUBLIC void AppMC::set_dump_intermediary_cnf(const int dump_intermediary_cnf)
 {
     data->conf.dump_intermediary_cnf = dump_intermediary_cnf;
 }

diff --git a/src/approxmc.h b/src/approxmc.h
@@ -104,7 +104,7 @@ class AppMC
     void set_reuse_models(uint32_t reuse_models);
     void set_sparse(uint32_t sparse);
     void set_simplify(uint32_t simplify);
-    void set_dump_intermediary_cnf(const bool dump_intermediary_cnf);
+    void set_dump_intermediary_cnf(const int dump_intermediary_cnf);
 
     //Querying default values
     const std::vector<uint32_t>& get_sampling_set() const;

diff --git a/src/counter.cpp b/src/counter.cpp
@@ -149,7 +149,7 @@ uint64_t Counter::add_glob_banning_cls(
     return repeat;
 }
 
-void Counter::dump_cnf_from_solver(const vector<Lit>& assumps)
+void Counter::dump_cnf_from_solver(const vector<Lit>& assumps, const uint32_t iter, const lbool result)
 {
     vector<vector<Lit>> cnf;
     solver->start_getting_small_clauses(
@@ -178,8 +178,12 @@ void Counter::dump_cnf_from_solver(const vector<Lit>& assumps)
     solver->end_getting_small_clauses();
 
     std::stringstream ss;
-    ss << "cnf_dump-" << cnf_dump_no << ".cnf";
-    cnf_dump_no++;
+    std::string result_str;
+    if (result == l_True) result_str = "SAT";
+    else if (result == l_False) result_str = "UNSAT";
+    else assert(false && "Should not be called with unknown!");
+    ss << "cnfdump" << "-res-" << result_str << "-iter-" << iter
+        << "-active-xors-" << assumps.size() << "-out-" << cnf_dump_no++ << ".cnf";
 
     std::ofstream f;
     f.open(ss.str(), std::ios::out);
@@ -198,6 +202,7 @@ SolNum Counter::bounded_sol_count(
         uint32_t maxSolutions,
         const vector<Lit>* assumps,
         const uint32_t hashCount,
+        const uint32_t iter,
         HashesModels* hm
 ) {
     if (conf.verb) {
@@ -234,18 +239,17 @@ SolNum Counter::bounded_sol_count(
         }
     }
 
+    cnf_dump_no = 0;
     const uint64_t repeat = add_glob_banning_cls(hm, sol_ban_var, hashCount);
     uint64_t solutions = repeat;
     double last_found_time = cpuTimeTotal();
     vector<vector<lbool>> models;
     while (solutions < maxSolutions) {
         lbool ret = solver->solve(&new_assumps, true);
         assert(ret == l_False || ret == l_True);
-        if (conf.dump_intermediary_cnf >= 2 && ret == l_True) {
-            dump_cnf_from_solver(new_assumps);
-        }
-        if (conf.dump_intermediary_cnf >= 1 && ret == l_False) {
-            dump_cnf_from_solver(new_assumps);
+        if ((conf.dump_intermediary_cnf >= 2 && ret == l_True) ||
+            (conf.dump_intermediary_cnf >= 1 && ret == l_False)) {
+            dump_cnf_from_solver(new_assumps, iter, ret);
         }
 
         if (conf.verb >= 2) {
@@ -502,7 +506,7 @@ int Counter::find_best_sparse_match()
 //https://www.ijcai.org/Proceedings/16/Papers/503.pdf
 void Counter::one_measurement_count(
     int64_t& mPrev,
-    const unsigned iter,
+    const uint32_t iter,
     SparseData sparse_data,
     HashesModels* hm)
 {
@@ -553,6 +557,7 @@ void Counter::one_measurement_count(
             threshold + 1, //max no. solutions
             &assumps, //assumptions to use
             hashCount,
+            iter,
             hm
         );
         const uint64_t num_sols = std::min<uint64_t>(sols.solutions, threshold + 1);

diff --git a/src/counter.h b/src/counter.h
@@ -131,6 +131,7 @@ class Counter {
         uint32_t maxSolutions,
         const vector<Lit>* assumps,
         const uint32_t hashCount,
+        const uint32_t iter,
         HashesModels* hm = NULL
     );
     vector<Lit> set_num_hashes(
@@ -143,7 +144,7 @@ class Counter {
     ////////////////
     //Helper functions
     ////////////////
-    void dump_cnf_from_solver(const vector<Lit>& assumps);
+    void dump_cnf_from_solver(const vector<Lit>& assumps, const uint32_t iter, const lbool result);
     void print_xor(const vector<uint32_t>& vars, const uint32_t rhs);
     void one_measurement_count(
         int64_t& mPrev,