From 33572934aa0efe07f18849ef98f29700873e4a64 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 9 Dec 2025 17:48:10 +0100 Subject: [PATCH 1/8] Small cosmetic fixes --- src/approxmc.h | 1 - src/counter.cpp | 9 ++------- src/counter.h | 3 --- src/main.cpp | 1 - 4 files changed, 2 insertions(+), 12 deletions(-) diff --git a/src/approxmc.h b/src/approxmc.h index ec0d4de..fe5e271 100644 --- a/src/approxmc.h +++ b/src/approxmc.h @@ -101,7 +101,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); diff --git a/src/counter.cpp b/src/counter.cpp index 3669153..3560918 100644 --- a/src/counter.cpp +++ b/src/counter.cpp @@ -27,7 +27,6 @@ */ #include -#include #include #include #include @@ -330,7 +329,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 +470,6 @@ 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); - } *cnt_it *= pow(2, (*hash_it) - min_hash); } ret_count.valid = true; diff --git a/src/counter.h b/src/counter.h index 9c1fe49..cef1cda 100644 --- a/src/counter.h +++ b/src/counter.h @@ -174,9 +174,6 @@ class Counter { uint32_t cnf_dump_no = 0; vector> cls_in_solver; // needed for accurate dumping vector, bool>> xors_in_solver; // needed for accurate dumping - - int argc; - char** argv; }; } diff --git a/src/main.cpp b/src/main.cpp index a5b8e5f..ba585f6 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -36,7 +36,6 @@ #include #include -#include "time_mem.h" #include "approxmc.h" #include "time_mem.h" #include From cb5dbf05d417f8ba85611e1b0f53d614634e2802 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 9 Dec 2025 17:57:50 +0100 Subject: [PATCH 2/8] Cleanup --- src/counter.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/counter.cpp b/src/counter.cpp index 3560918..9838d73 100644 --- a/src/counter.cpp +++ b/src/counter.cpp @@ -163,7 +163,8 @@ void Counter::dump_cnf_from_solver(const vector& 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) { @@ -504,7 +505,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()) { @@ -689,7 +690,7 @@ template inline T Counter::find_median(const vector& 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]; } From 03165c2df605538f855931e7dd9d2513eefa51d5 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 9 Dec 2025 17:58:33 +0100 Subject: [PATCH 3/8] Cleanup --- src/counter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/counter.cpp b/src/counter.cpp index 9838d73..5b48dde 100644 --- a/src/counter.cpp +++ b/src/counter.cpp @@ -628,11 +628,11 @@ void Counter::one_measurement_count( hash_prev = cur_hash_cnt; } } + bool Counter::gen_rhs() { std::uniform_int_distribution dist{0, 1}; - bool rhs = dist(rnd_engine); - return rhs; + return dist(rnd_engine); } string Counter::gen_rnd_bits( From f4ecb3e7e34a820c0a8336920b5b6708196961e4 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 9 Dec 2025 18:05:35 +0100 Subject: [PATCH 4/8] Use unique_ptr --- src/approxmc.cpp | 17 ++++------------- src/approxmc.h | 3 ++- src/counter.h | 7 ++++--- 3 files changed, 10 insertions(+), 17 deletions(-) diff --git a/src/approxmc.cpp b/src/approxmc.cpp index cc82674..7c92a6b 100644 --- a/src/approxmc.cpp +++ b/src/approxmc.cpp @@ -61,20 +61,16 @@ using namespace ApproxMC; DLL_PUBLIC AppMC::AppMC(const std::unique_ptr& _fg) { - data = new AppMCPrivateData(_fg); - data->counter.solver = new SATSolver(); + data = std::make_unique(_fg); + data->counter.solver = std::make_unique(); 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& 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& 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& AppMC::get_sampling_set() const { return data->conf.sampl_vars; diff --git a/src/approxmc.h b/src/approxmc.h index fe5e271..ff3fa49 100644 --- a/src/approxmc.h +++ b/src/approxmc.h @@ -33,6 +33,7 @@ #include #include #include +#include #include namespace ApproxMC { @@ -122,7 +123,7 @@ class AppMC //////////////////////////// // Do not bother with this, it's private //////////////////////////// - AppMCPrivateData* data; + std::unique_ptr data; }; } diff --git a/src/counter.h b/src/counter.h index cef1cda..6f464c8 100644 --- a/src/counter.h +++ b/src/counter.h @@ -41,6 +41,7 @@ using std::vector; using std::map; using std::pair; using namespace CMSat; +using std::unique_ptr; namespace AppMCInt { @@ -93,7 +94,7 @@ struct SparseData { class Counter { public: - Counter(Config& _conf, const std::unique_ptr& _fg) : fg(_fg->dup()), conf(_conf) {} + Counter(Config& _conf, const unique_ptr& _fg) : fg(_fg->dup()), conf(_conf) {} ApproxMC::SolCount solve(); string gen_rnd_bits(const uint32_t size, const uint32_t numhashes, SparseData& sparse_data); @@ -101,7 +102,7 @@ class Counter { bool find_one_solution(); bool gen_rhs(); uint32_t threshold_appmcgen; - SATSolver* solver = nullptr; + unique_ptr solver = nullptr; ApproxMC::SolCount calc_est_count(); const Constants constants; bool solver_add_clause(const vector& cl); @@ -109,7 +110,7 @@ class Counter { bool solver_add_xor_clause(const vector& lits, const bool rhs); private: - std::unique_ptr fg; + unique_ptr fg; Config& conf; ApproxMC::SolCount count(); void add_appmc_options(); From 6eaa356b329b387154403bd20e010a9f2aeea462 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 9 Dec 2025 19:18:26 +0100 Subject: [PATCH 5/8] Typo --- src/main.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main.cpp b/src/main.cpp index ba585f6..e704227 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -258,7 +258,7 @@ template 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 tmp; for(auto const& s: reader->get_sampl_vars()) { if (s >= reader->nVars()) { From ebc2094e49442786fae0f9af8b3029e242c38f02 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 9 Dec 2025 19:49:08 +0100 Subject: [PATCH 6/8] More defensive coding --- src/approxmc.h | 2 +- src/counter.cpp | 7 +++++-- src/counter.h | 1 - 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/approxmc.h b/src/approxmc.h index ff3fa49..9297da6 100644 --- a/src/approxmc.h +++ b/src/approxmc.h @@ -50,7 +50,7 @@ class SolCount } bool valid = false; uint32_t hashCount = 0; - uint32_t cellSolCount = 0; + uint64_t cellSolCount = 0; }; struct AppMCPrivateData; diff --git a/src/counter.cpp b/src/counter.cpp index 5b48dde..b9b66d8 100644 --- a/src/counter.cpp +++ b/src/counter.cpp @@ -471,6 +471,9 @@ ApproxMC::SolCount Counter::calc_est_count() ; hash_it != num_hash_list.end() && cnt_it != num_count_list.end() ; hash_it++, cnt_it++ ) { + 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; @@ -684,7 +687,7 @@ void Counter::print_xor(const vector& vars, const uint32_t rhs) cout << " = " << (rhs ? "True" : "False") << endl; } -template inline T Counter::find_median(const vector& nums) { +template T Counter::find_median(const vector& nums) { assert(!nums.empty()); auto tmp = nums; @@ -694,7 +697,7 @@ template inline T Counter::find_median(const vector& nums) { return tmp[med_index]; } -template inline T Counter::find_min(const vector& nums) { +template T Counter::find_min(const vector& nums) { T min = std::numeric_limits::max(); for (const auto a: nums) { if (a < min) min = a; diff --git a/src/counter.h b/src/counter.h index 6f464c8..5195c83 100644 --- a/src/counter.h +++ b/src/counter.h @@ -27,7 +27,6 @@ */ #include "appmcconfig.h" -#include #include #include #include From 949587e248b1fd873ea708fc4576e94a2a478741 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 9 Dec 2025 19:52:25 +0100 Subject: [PATCH 7/8] Fixing verb_print Fix --- src/appmc_constants.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/appmc_constants.h b/src/appmc_constants.h index a39f456..1b49aad 100644 --- a/src/appmc_constants.h +++ b/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;\ From 9b8d622f9a9201229cc7dc37977df24f274cdf7f Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 9 Dec 2025 22:12:11 +0100 Subject: [PATCH 8/8] Fixing small asserts, typos --- src/appmc_constants.cpp | 13 +++++-------- src/counter.cpp | 4 +++- src/main.cpp | 2 +- 3 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/appmc_constants.cpp b/src/appmc_constants.cpp index 1345918..8fc93b0 100644 --- a/src/appmc_constants.cpp +++ b/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 #include #include #include 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 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); diff --git a/src/counter.cpp b/src/counter.cpp index b9b66d8..2717cc6 100644 --- a/src/counter.cpp +++ b/src/counter.cpp @@ -651,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( @@ -667,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; } diff --git a/src/main.cpp b/src/main.cpp index e704227..7743028 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -158,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);