Fixing small issues

src/appmc_constants.cpp

@@ -1,7 +1,7 @@
 /*
  ApproxMC
- 
- 
+
+
  Copyright (c) 2019, Mate Soos and Kuldeep S. Meel. All rights reserved
  Copyright (c) 2009-2018, Mate Soos. All rights reserved.
  Copyright (c) 2015, Supratik Chakraborty, Daniel J. Fremont,
@@ -28,14 +28,11 @@
  */
 
 #include "appmc_constants.h"
-#include <iostream>
 #include <sstream>
 #include <cassert>
 #include <string>
 
 using std::string;
-using std::cout;
-using std::endl;
 using std::vector;
 using namespace AppMCInt;
 
@@ -82,16 +79,16 @@ void Constants::readInSparseValues()
         std::getline(ss, value, ',');
         if (value == "header") {
             while(std::getline(ss, value, ',')) {
-                probval.push_back(std::stod(value.c_str()));
+                probval.push_back(std::stod(value));
             }
             continue;
         }
 
         //non-header
-        uint32_t numvars = std::stoul(value.c_str());
+        uint32_t numvars = std::stoul(value);
         vector<uint32_t> index_var_map;
         while(std::getline(ss, value, ',')) {
-            index_var_map.push_back(std::stoul(value.c_str()));
+            index_var_map.push_back(std::stoul(value));
         }
         assert(index_var_map.size() <= probval.size());
         VarMap vmap(numvars, index_var_map);

src/appmc_constants.h

@@ -35,7 +35,7 @@
 using std::vector;
 using std::string;
 
-#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/approxmc.cpp

@@ -61,20 +61,16 @@ using namespace ApproxMC;
 
 DLL_PUBLIC AppMC::AppMC(const std::unique_ptr<CMSat::FieldGen>& _fg)
 {
-    data = new AppMCPrivateData(_fg);
-    data->counter.solver = new SATSolver();
+    data = std::make_unique<AppMCPrivateData>(_fg);
+    data->counter.solver = std::make_unique<SATSolver>();
     data->counter.solver->set_up_for_scalmc();
     data->counter.solver->set_allow_otf_gauss();
 }
 
-DLL_PUBLIC AppMC::~AppMC()
-{
-    delete data->counter.solver;
-    delete data;
-}
+DLL_PUBLIC AppMC::~AppMC() = default;
 
 // Helper function, used only in this unit
-void setup_sampling_vars(AppMCPrivateData* data)
+void setup_sampling_vars(unique_ptr<AppMCPrivateData>& data)
 {
     if (data->conf.verb) {
         cout << "c o [appmc] Sampling set size: " << data->conf.sampl_vars.size() << endl;
@@ -279,11 +275,6 @@ DLL_PUBLIC bool AppMC::add_xor_clause(const vector<uint32_t>& vars, bool rhs)
     return data->counter.solver_add_xor_clause(vars, rhs);
 }
 
-DLL_PUBLIC CMSat::SATSolver* AppMC::get_solver()
-{
-    return data->counter.solver;
-}
-
 DLL_PUBLIC const std::vector<uint32_t>& AppMC::get_sampling_set() const
 {
     return data->conf.sampl_vars;

src/approxmc.h

@@ -33,6 +33,7 @@
 #include <memory>
 #include <string>
 #include <vector>
+#include <memory>
 #include <cryptominisat5/cryptominisat.h>
 namespace ApproxMC {
 
@@ -49,7 +50,7 @@ class SolCount
     }
     bool valid = false;
     uint32_t hashCount = 0;
-    uint32_t cellSolCount = 0;
+    uint64_t cellSolCount = 0;
 };
 
 struct AppMCPrivateData;
@@ -101,7 +102,6 @@ class AppMC
     void set_start_iter(uint32_t start_iter);
     void set_verb_cls(uint32_t verb_cls);
     void set_var_elim_ratio(double var_elim_ratio);
-    void set_detach_xors(uint32_t detach_xors);
     void set_reuse_models(uint32_t reuse_models);
     void set_sparse(uint32_t sparse);
     void set_simplify(uint32_t simplify);
@@ -123,7 +123,7 @@ class AppMC
     ////////////////////////////
     // Do not bother with this, it's private
     ////////////////////////////
-    AppMCPrivateData* data;
+    std::unique_ptr<AppMCPrivateData> data;
 };
 
 }

src/counter.cpp

@@ -27,7 +27,6 @@
  */
 
 #include <ctime>
-#include <cerrno>
 #include <algorithm>
 #include <sstream>
 #include <iostream>
@@ -164,7 +163,8 @@ void Counter::dump_cnf_from_solver(const vector<Lit>& assumps, const uint32_t it
 
     std::ofstream f;
     f.open(ss.str(), std::ios::out);
-    f << "p cnf " << solver->nVars()+1 << " " << cls_in_solver.size()+xors_in_solver.size()+assumps.size() << endl;
+    f << "p cnf " << solver->nVars()+1 << " "
+        << cls_in_solver.size()+xors_in_solver.size()+assumps.size() << endl;
     for(const auto& cl: cls_in_solver) f << cl << " 0" << endl;
     f << "c XORs below" << endl;
     for(const auto& x: xors_in_solver) {
@@ -330,7 +330,8 @@ double Counter::calc_error_bound(uint32_t t, double p)
 {
     double curr = pow(p, t);
     double sum = curr;
-    for (auto k=t-1; k>=std::ceil(double(t)/2); k--) {
+    assert(t >= 1);
+    for (int32_t k=(int32_t)t-1; k>=std::ceil(double(t)/2); k--) {
        curr *= double((k+1))/(t-k) * (1-p)/p;
        sum += curr;
     }
@@ -470,11 +471,9 @@ ApproxMC::SolCount Counter::calc_est_count()
         ; hash_it != num_hash_list.end() && cnt_it != num_count_list.end()
         ; hash_it++, cnt_it++
     ) {
-        if ((*hash_it) - min_hash > 10) {
-            cout << "Internal ERROR: Something is VERY fishy, the difference between each count must"
-                " never be this large. Please report this bug to the maintainers" << endl;
-            exit(-1);
-        }
+        assert(*hash_it >= min_hash);
+        assert((*cnt_it) >= 0);
+        assert((*hash_it) - min_hash <= 100);
         *cnt_it *= pow(2, (*hash_it) - min_hash);
     }
     ret_count.valid = true;
@@ -509,7 +508,7 @@ int Counter::find_best_sparse_match()
 void Counter::one_measurement_count(
     int64_t& prev_measure,
     const uint32_t iter,
-    SparseData sparse_data,
+    SparseData sparse_data, // passed by value on purpose, will be modified
     HashesModels* hm)
 {
     if (conf.sampl_vars.empty()) {
@@ -632,11 +631,11 @@ void Counter::one_measurement_count(
         hash_prev = cur_hash_cnt;
     }
 }
+
 bool Counter::gen_rhs()
 {
     std::uniform_int_distribution<uint32_t> dist{0, 1};
-    bool rhs = dist(rnd_engine);
-    return rhs;
+    return dist(rnd_engine);
 }
 
 string Counter::gen_rnd_bits(
@@ -652,6 +651,7 @@ string Counter::gen_rnd_bits(
         //Do we need to update the probability?
         const auto& table = constants.index_var_maps[sparse_data.table_no];
         const auto next_var_index = table.index_var_map[sparse_data.next_index];
+        assert(!table.index_var_map.empty());
         if (hash_index >= next_var_index) {
             sparse_data.sparseprob = constants.probval[sparse_data.next_index];
             sparse_data.next_index = std::min<uint32_t>(
@@ -668,11 +668,12 @@ string Counter::gen_rnd_bits(
         }
     }
 
+    random_bits.reserve(size);
     while (random_bits.size() < size) {
         bool val = dist(rnd_engine) < cutoff;
         random_bits += '0' + val;
     }
-    assert(random_bits.size() >= size);
+    assert(random_bits.size() == size);
     return random_bits;
 }
 
@@ -688,17 +689,17 @@ void Counter::print_xor(const vector<uint32_t>& vars, const uint32_t rhs)
     cout << " = " << (rhs ? "True" : "False") << endl;
 }
 
-template<class T> inline T Counter::find_median(const vector<T>& nums) {
+template<class T> T Counter::find_median(const vector<T>& nums) {
     assert(!nums.empty());
     auto tmp = nums;
 
     std::sort(tmp.begin(), tmp.end());
     size_t med_index = tmp.size() / 2;
-    if (med_index >= tmp.size()) return tmp[tmp.size() - 1];
+    assert(med_index < tmp.size());
     return tmp[med_index];
 }
 
-template<class T> inline T Counter::find_min(const vector<T>& nums) {
+template<class T> T Counter::find_min(const vector<T>& nums) {
     T min = std::numeric_limits<T>::max();
     for (const auto a: nums) {
         if (a < min) min = a;

src/counter.h

@@ -27,7 +27,6 @@
  */
 
 #include "appmcconfig.h"
-#include <fstream>
 #include <memory>
 #include <random>
 #include <map>
@@ -41,6 +40,7 @@ using std::vector;
 using std::map;
 using std::pair;
 using namespace CMSat;
+using std::unique_ptr;
 
 namespace AppMCInt {
 
@@ -93,23 +93,23 @@ struct SparseData {
 
 class Counter {
 public:
-    Counter(Config& _conf, const std::unique_ptr<FieldGen>& _fg) : fg(_fg->dup()), conf(_conf) {}
+    Counter(Config& _conf, const unique_ptr<FieldGen>& _fg) : fg(_fg->dup()), conf(_conf) {}
     ApproxMC::SolCount solve();
     string gen_rnd_bits(const uint32_t size,
                         const uint32_t numhashes, SparseData& sparse_data);
     string binary(const uint32_t x, const uint32_t length);
     bool find_one_solution();
     bool gen_rhs();
     uint32_t threshold_appmcgen;
-    SATSolver* solver = nullptr;
+    unique_ptr<SATSolver> solver = nullptr;
     ApproxMC::SolCount calc_est_count();
     const Constants constants;
     bool solver_add_clause(const vector<Lit>& cl);
     bool solver_add_xor_clause(const vector<uint32_t>& vars, const bool rhs);
     bool solver_add_xor_clause(const vector<Lit>& lits, const bool rhs);
 
 private:
-    std::unique_ptr<FieldGen> fg;
+    unique_ptr<FieldGen> fg;
     Config& conf;
     ApproxMC::SolCount count();
     void add_appmc_options();
@@ -174,9 +174,6 @@ class Counter {
     uint32_t cnf_dump_no = 0;
     vector<vector<Lit>> cls_in_solver; // needed for accurate dumping
     vector<pair<vector<Lit>, bool>> xors_in_solver; // needed for accurate dumping
-
-    int argc;
-    char** argv;
 };
 
 }

src/main.cpp

@@ -36,7 +36,6 @@
 #include <set>
 #include <gmp.h>
 
-#include "time_mem.h"
 #include "approxmc.h"
 #include "time_mem.h"
 #include <cryptominisat5/solvertypesmini.h>
@@ -159,7 +158,7 @@ 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
+            cout << "Probabilistic Approximate Counter" << endl << endl
             << "approxmc [options] inputfile" << endl;
             cout << program << endl;
             exit(0);
@@ -259,7 +258,7 @@ template<class T> void parse_file(const std::string& filename, T* reader) {
     for(uint32_t i = 0; i < reader->nVars(); i++) tmp.push_back(i);
     reader->set_sampl_vars(tmp);
   } else {
-    // Check if CNF has all vars as indep. Then its's all_indep
+    // Check if CNF has all vars as indep. Then it's all_indep
     set<uint32_t> tmp;
     for(auto const& s: reader->get_sampl_vars()) {
       if (s >= reader->nVars()) {