More small cleanups of the code (#80)

* This todo has been achieved

* Removing useless variable

* Defensive verb_print

* Better usage of mutex thanks to @clonker

* Update description

* Clenup

* Update to satisfy macos gmp

* Cleaner code

* Add clang analyzer code

* Cannot set opt_sampling_vars here

* This should fix the mac build

* Finally fixing this

* Fixing outer_counter

* Better printing of error

Author: msoos

CMakeLists.txt

@@ -307,6 +307,13 @@ if (SANITIZE)
     #add_compile_options("-Wconversion")
 endif()
 
+option(ANALYZE "Run Clang static analyzer. You MUST use clang++ as the compiler for this to work" OFF)
+if (ANALYZE)
+    MESSAGE(WARNING " --Using clang static analyzer -- you MUST use clang++ or the compile WILL fail")
+    set(CMAKE_CXX_CLANG_TIDY "clang-tidy;-checks=clang-analyzer-*")
+    set(CMAKE_C_CLANG_TIDY "clang-tidy;-checks=clang-analyzer-*")
+endif()
+
 # -----------------------------------------------------------------------------
 # Dependencies
 # -----------------------------------------------------------------------------

scripts/build_clang_analyze.sh

@@ -0,0 +1,3 @@
+rm -rf CMake* src cmake* ganak* sharp* Make*
+cmake -DANALYZE=ON -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_C_COMPILER=clang ..
+make -j16

src/common.hpp

@@ -103,7 +103,7 @@ using FF = std::unique_ptr<Field>;
 #define CHECK_COUNT_DO(x) do { } while (0)
 #endif
 
-#define verb_print(a, b) if (conf.verb >= a) cout << "c o " << b << endl
+#define verb_print(a, b) do { if (conf.verb >= a) cout << "c o " << b << endl; } while (0)
 #define clear_toclear_seen() \
     do {\
       for(const auto& x: to_clear) seen[x] = 0;\

src/comp_types/difference_packed_comp.hpp

@@ -69,7 +69,7 @@ class DiffPackedComp  {
   DiffPackedComp() = default;
   ~DiffPackedComp() { delete[] data; }
   DiffPackedComp& operator=(const DiffPackedComp& other) noexcept{
-    if (data != nullptr) delete[] data;
+    delete[] data;
     data_size = other.data_size;
     data = new uint32_t[data_size];
     std::memcpy(data, other.data, data_size * sizeof(uint32_t));
@@ -173,7 +173,7 @@ class DiffPackedComp  {
 
 private:
   uint32_t* data = nullptr; // the packed data
-  uint32_t data_size = 0; // the size of the packed data in bytes
+  uint32_t data_size = 0; // the size of the packed data in uint32_t units
 };
 
 }

src/counter.cpp

@@ -354,13 +354,13 @@ void Counter::td_decompose() {
     return;
   }
 
-  TWD::Graph primal(nVars());
+  auto primal = std::make_unique<TWD::Graph>(nVars());
   all_lits(i) {
     Lit l(i/2, i%2 == 0);
     for(const auto& l2: watches[l].binaries) {
       if (!l2.red() && l < l2.lit()) {
         debug_print("bin cl: " << l.var() << " " << l2.lit().var());
-        primal.addEdge(l.var()-1, l2.lit().var()-1);
+        primal->addEdge(l.var()-1, l2.lit().var()-1);
       }
     }
   }
@@ -370,7 +370,7 @@ void Counter::td_decompose() {
     for(uint32_t i = 0; i < cl.sz; i++) {
       for(uint32_t i2 = i+1; i2 < cl.sz; i2++) {
         debug_print("long cl: " <<  cl[i].var() << " " << cl[i2].var());
-        primal.addEdge(cl[i].var()-1, cl[i2].var()-1);
+        primal->addEdge(cl[i].var()-1, cl[i2].var()-1);
       }
     }
   }
@@ -379,22 +379,22 @@ void Counter::td_decompose() {
   if (!conf.do_td_use_opt_indep) nodes = indep_support_end-1;
   if (conf.do_td_contract) {
     for(uint32_t i = nodes; i < nVars(); i++) {
-      primal.contract(i, conf.td_max_edges*100);
-      if (primal.numEdges() > conf.td_max_edges*100 ) break;
+      primal->contract(i, conf.td_max_edges*100);
+      if (primal->numEdges() > conf.td_max_edges*100 ) break;
     }
   }
-  verb_print(1, "[td] nodes: " << nodes << " nvars: " << nVars() << " edges: " << primal.numEdges());
+  verb_print(1, "[td] nodes: " << nodes << " nvars: " << nVars() << " edges: " << primal->numEdges());
 
   const uint64_t n = (uint64_t)nVars()*(uint64_t)nVars();
-  const double density = (double)primal.numEdges()/(double)n;
-  const double edge_var_ratio = (double)primal.numEdges()/(double)nVars();
+  const double density = (double)primal->numEdges()/(double)n;
+  const double edge_var_ratio = (double)primal->numEdges()/(double)nVars();
   verb_print(1, "[td] Primal graph  "
-    << " nodes: " << primal.numNodes()
-    << " edges: " <<  primal.numEdges()
+    << " nodes: " << primal->numNodes()
+    << " edges: " <<  primal->numEdges()
     << " density: " << std::fixed << setprecision(3) << density
     << " edge/var: " << std::fixed << setprecision(3) << edge_var_ratio);
-  if (primal.numEdges() > conf.td_max_edges) {
-    verb_print(1, "[td] Too many edges, " << primal.numEdges() << " skipping TD");
+  if (primal->numEdges() > conf.td_max_edges) {
+    verb_print(1, "[td] Too many edges, " << primal->numEdges() << " skipping TD");
     return;
   }
   if (density > conf.td_max_density) {
@@ -406,21 +406,22 @@ void Counter::td_decompose() {
     return;
   }
 
-  TWD::Graph* primal_alt = nullptr;
+  std::unique_ptr<TWD::Graph> primal_alt = nullptr;
   if (conf.do_td_contract) {
-    primal_alt = new TWD::Graph(nodes);
+    primal_alt = std::make_unique<TWD::Graph>(nodes);
     for(uint32_t i = 0 ; i < nodes; i++) {
-      const auto& k = primal.get_adj_list()[i];
+      const auto& k = primal->get_adj_list()[i];
       for(const auto& i2: k) {
         if (i2 < (int)nodes)
           primal_alt->addEdge(i, i2);
       }
     }
-  } else primal_alt = &primal;
+  } else primal_alt = std::move(primal);
 
   if (!primal_alt->isConnected()) {
-    verb_print(1, "ERROR: Primal graph is not connected, this is NOT going to go well!");
-    verb_print(1, "ERROR: Counter should NOT be fed a disconnected CNF");
+    cerr << "ERROR: Primal graph is not connected, this is NOT going to go well!" << endl;
+    cerr << "ERROR: Counter should NOT be fed a disconnected CNF" << endl;
+    assert(false);
     exit(-1);
   }
 
@@ -434,7 +435,6 @@ void Counter::td_decompose() {
 
   compute_td_score(td, conf.do_td_contract ? nodes : nVars(), true);
   verb_print(1, "[td] decompose time: " << cpu_time() - my_time);
-  if (conf.do_td_contract) delete primal_alt;
 }
 
 // Self-check count without restart with CMS only
@@ -831,7 +831,7 @@ FF Counter::do_appmc_count() {
 
   mpz_class num_sols(2);
   mpz_pow_ui(num_sols.get_mpz_t(), num_sols.get_mpz_t(), appmc_cnt.hashCount);
-  num_sols *= appmc_cnt.cellSolCount;
+  num_sols *= mpz_class(static_cast<unsigned long>(appmc_cnt.cellSolCount));
   verb_print(1, "[appmc] ApproxMC count: " << num_sols);
   return std::make_unique<ArjunNS::FMpz>(num_sols);
 }
@@ -1222,9 +1222,7 @@ double Counter::score_of(const uint32_t v, bool ignore_td) const {
   double act_score = 0;
   double td_score = 0;
   double freq_score = 0;
-  vector<uint32_t> occ_cnt; // number of occurrences of a variable in the component
 
-  // TODO Yash idea: let's cut this into activities and incidence
   if (!tdscore.empty() && !ignore_td) td_score = td_weight*tdscore[v];
   act_score = var_act(v)/conf.act_score_divisor;
   freq_score = (double)comp_manager->freq_score_of(v)/conf.freq_score_divisor;

src/main.cpp

@@ -267,8 +267,8 @@ void parse_supported_options(int argc, char** argv) {
     try {
         program.parse_args(argc, argv);
         if (program.is_used("--help")) {
-            cout << "Probilistic Approximate Counter" << endl << endl
-            << "approxmc [options] inputfile" << endl;
+            cout << "Flexible Weighted Model Counter" << endl << endl
+            << "ganak [options] inputfile" << endl;
             cout << program << endl;
             exit(0);
         }

src/outer_counter.cpp

@@ -31,6 +31,7 @@ THE SOFTWARE.
 #include "counter.hpp"
 #include "time_mem.hpp"
 #include "common.hpp"
+#include "ganak.hpp"
 
 namespace GanakInt {
 
@@ -128,7 +129,8 @@ void run_arjun(ArjunNS::SimplifiedCNF& cnf) {
   /* verb_print(1, "Arjun T: " << (cpu_time()-my_time)); */
 }
 
-void setup_ganak(const ArjunNS::SimplifiedCNF& cnf, OuterCounter& counter) {
+template<class T>
+void setup_ganak(const ArjunNS::SimplifiedCNF& cnf, T& counter) {
   cnf.check_sanity();
   counter.new_vars(cnf.nVars());
 
@@ -235,7 +237,7 @@ FF OuterCounter::count_with_parallel(uint8_t bits_jobs, int num_threads) {
     ArjunNS::SimplifiedCNF cnf(fg);
     cnf.new_vars(nvars);
     cnf.set_sampl_vars(ganak_to_cms_vars(indep_support));
-    cnf.set_opt_sampl_vars(ganak_to_cms_vars(opt_indep_support));
+    /* cnf.set_opt_sampl_vars(ganak_to_cms_vars(opt_indep_support)); */
     for (const auto& [lit, weight] : lit_weights)
       cnf.set_lit_weight(ganak_to_cms_lit(lit), weight->dup());
     for (const auto& cl : irred_cls) cnf.add_clause(ganak_to_cms_cl(cl));
@@ -255,14 +257,15 @@ FF OuterCounter::count_with_parallel(uint8_t bits_jobs, int num_threads) {
     if (cnf.multiplier_weight != fg->zero()) {
       auto local_conf = conf;
       local_conf.verb = 0; // disable verb for threads
-      auto counter = std::make_unique<OuterCounter>(local_conf, fg);
+      auto counter = std::make_unique<Ganak>(local_conf, fg);
       setup_ganak(cnf, *counter);
       auto ret = counter->count();
       num_cache_lookups += counter->get_num_cache_lookups();
-      stats_mutex.lock();
-      max_cache_elems = std::max(max_cache_elems, counter->get_max_cache_elems());
-      count_is_approximate |= counter->get_is_approximate();
-      stats_mutex.unlock();
+      {
+        std::lock_guard<std::mutex> lock(stats_mutex);
+        max_cache_elems = std::max(max_cache_elems, counter->get_max_cache_elems());
+        count_is_approximate |= counter->get_is_approximate();
+      }
       *ret *= *cnf.multiplier_weight;
       return ret;
     } else {

src/outer_counter.hpp

@@ -28,6 +28,7 @@ THE SOFTWARE.
 #include <set>
 #include <vector>
 #include <atomic>
+#include <mutex>
 
 #include "counter.hpp"
 #include "counter_config.hpp"

src/statistics.cpp

@@ -113,8 +113,8 @@ void DataAndStatistics::print_short(const Counter* counter, const std::unique_pt
 
   verb_print(1, "comp sortsK/avg sz             "
     << setw(5) << comp_sorts/1000 << " / "
-    << setw(5) << setprecision(8) << safe_div(comp_sizes, comp_sorts))
-    << setprecision(2);
+    << setw(5) << setprecision(8) << safe_div(comp_sizes, comp_sorts)
+    << setprecision(2));
   verb_print(1, "comps recordK/non-reset ratio  " << comps_recorded/1000 << " / "
         << safe_div(comps_non_reset, comps_reset+comps_non_reset));