diff --git a/src/appmc_constants.cpp b/src/appmc_constants.cpp index f49e75a..1345918 100644 --- a/src/appmc_constants.cpp +++ b/src/appmc_constants.cpp @@ -69,73 +69,6 @@ Constants::Constants() { "3600,1,11,13,20,25,26,54,57,63,72,79,81,88,91,105,108,115,122,129,145,153,161,170,191,204,231,246,280,301,351,381,458,508,641,736,1039,1308,", }}; - iterationConfidences = {{ - 0.64, 0.704512, 0.7491026944, 0.783348347699, - 0.81096404252, 0.833869604432, 0.853220223135, 0.869779929746, - 0.884087516258, 0.896540839559, 0.907443973174, 0.917035558936, - 0.92550684748, 0.933013712405, 0.939684956024, 0.945628233538, - 0.950934391703, 0.955680718969, 0.9599334282, 0.963749585636, - 0.967178632062, 0.970263598173, 0.973042086923, 0.975547075737, - 0.977807577642, 0.979849190627, 0.98169455749, 0.98336375333, - 0.984874614022, 0.98624301618, 0.987483116952, 0.988607560325, - 0.989627655353, 0.990553530695, 0.991394269076, 0.992158024647, - 0.99285212571, 0.993483164877, 0.994057078393, 0.994579216081, - 0.995054403148, 0.995486994909, 0.995880925327, 0.996239750132, - 0.996566685198, 0.99686464074, 0.99713625183, 0.997383905666, - 0.997609765964, 0.997815794807, 0.998003772226, 0.998175313784, - 0.998331886363, 0.998474822355, 0.998605332446, 0.998724517108, - 0.998833376973, 0.998932822179, 0.999023680805, 0.999106706494, - 0.999182585332, 0.999251942072, 0.999315345767, 0.999373314859, - 0.999426321798, 0.999474797213, 0.99951913371, 0.999559689296, - 0.9995967905, 0.999630735199, 0.99966179518, 0.999690218475, - 0.999716231474, 0.999740040852, 0.999761835313, 0.999781787183, - 0.999800053855, 0.999816779104, 0.999832094286, 0.999846119426, - 0.999858964211, 0.999870728891, 0.999881505109, 0.999891376644, - 0.999900420098, 0.999908705519, 0.999916296969, 0.99992325304, - 0.999929627331, 0.999935468875, 0.999940822533, 0.999945729354, - 0.999950226904, 0.999954349561, 0.999958128793, 0.999961593401, - 0.999964769754, 0.999967681991, 0.999970352216, 0.999972800666, - 0.999975045876, 0.999977104817, 0.999978993036, 0.999980724771, - 0.999982313065, 0.999983769866, 0.999985106122, 0.99998633186, - 0.99998745627, 0.999988487774, 0.999989434086, 0.999990302279, - 0.999991098834, 0.99999182969, 0.999992500293, 0.999993115634, - 0.999993680288, 0.999994198449, 0.999994673963, 0.999995110355, - 0.999995510858, 0.999995878437, 0.999996215809, 0.999996525467, - 0.999996809697, 0.999997070596, 0.999997310086, 0.999997529931, - 0.999997731749, 0.999997917023, 0.999998087116, 0.999998243274, - 0.999998386645, 0.999998518279, 0.99999863914, 0.999998750113, - 0.999998852009, 0.999998945574, 0.999999031492, 0.999999110388, - 0.99999918284, 0.999999249374, 0.999999310476, 0.999999366591, - 0.999999418127, 0.999999465459, 0.99999950893, 0.999999548857, - 0.99999958553, 0.999999619214, 0.999999650153, 0.999999678573, - 0.999999704678, 0.999999728658, 0.999999750687, 0.999999770922, - 0.999999789512, 0.999999806589, 0.999999822278, 0.999999836692, - 0.999999849933, 0.999999862099, 0.999999873277, 0.999999883546, - 0.999999892982, 0.999999901651, 0.999999909617, 0.999999916936, - 0.999999923661, 0.999999929841, 0.999999935519, 0.999999940737, - 0.999999945532, 0.999999949938, 0.999999953987, 0.999999957708, - 0.999999961128, 0.99999996427, 0.999999967158, 0.999999969812, - 0.999999972252, 0.999999974493, 0.999999976554, 0.999999978447, - 0.999999980188, 0.999999981788, 0.999999983258, 0.999999984609, - 0.999999985851, 0.999999986993, 0.999999988043, 0.999999989007, - 0.999999989894, 0.999999990709, 0.999999991458, 0.999999992147, - 0.99999999278, 0.999999993362, 0.999999993897, 0.999999994389, - 0.999999994841, 0.999999995257, 0.999999995639, 0.99999999599, - 0.999999996313, 0.99999999661, 0.999999996883, 0.999999997134, - 0.999999997364, 0.999999997577, 0.999999997772, 0.999999997951, - 0.999999998116, 0.999999998267, 0.999999998407, 0.999999998535, - 0.999999998653, 0.999999998761, 0.999999998861, 0.999999998952, - 0.999999999036, 0.999999999114, 0.999999999185, 0.999999999251, - 0.999999999311, 0.999999999366, 0.999999999417, 0.999999999464, - 0.999999999507, 0.999999999547, 0.999999999583, 0.999999999616, - 0.999999999647, 0.999999999676, 0.999999999702, 0.999999999726, - 0.999999999748, 0.999999999768, 0.999999999786, 0.999999999804, - 0.999999999819, 0.999999999834, 0.999999999847, 0.999999999859, - 0.999999999871, 0.999999999881, 0.999999999891, 0.999999999899, - 0.999999999907, 0.999999999915, 0.999999999922, 0.999999999928, - 0.999999999934, 0.999999999939, 0.999999999944, 0.999999999948 - }}; - readInSparseValues(); } diff --git a/src/appmc_constants.h b/src/appmc_constants.h index 12794bc..3129b85 100644 --- a/src/appmc_constants.h +++ b/src/appmc_constants.h @@ -55,7 +55,6 @@ class Constants Constants(); vector probval; vector index_var_maps; - vector iterationConfidences; private: vector sparseprobvalues; diff --git a/src/counter.cpp b/src/counter.cpp index d27a483..29705a5 100644 --- a/src/counter.cpp +++ b/src/counter.cpp @@ -333,6 +333,19 @@ void Counter::simplify() solver->set_full_bve(0); } +// compute the error bound +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--) { + curr *= double((k+1))/(t-k) * (1-p)/p; + sum += curr; + } + + return sum; +} + //Set up probabilities, threshold and measurements void Counter::set_up_probs_threshold_measurements( uint32_t& measurements, SparseData& sparse_data) @@ -363,12 +376,31 @@ void Counter::set_up_probs_threshold_measurements( ); verb_print(1, "[appmc] threshold set to " << threshold << " sparse: " << (int)using_sparse); - measurements = (int)std::ceil(std::log2(3.0/conf.delta)*17); - for (int count = 0; count < 256; count++) { - if (constants.iterationConfidences[count] >= 1 - conf.delta) { - measurements = count*2+1; - break; - } + + double p_L = 0; + if (conf.epsilon < sqrt(2)-1) { + p_L = 0.262; + } else if (conf.epsilon < 1) { + p_L = 0.157; + } else if (conf.epsilon < 3) { + p_L = 0.085; + } else if (conf.epsilon < 4*sqrt(2)-1) { + p_L = 0.055; + } else { + p_L = 0.023; + } + + double p_U = 0; + if (conf.epsilon < 3) { + p_U = 0.169; + } else { + p_U = 0.044; + } + + for (measurements = 1; ; measurements+=2) { + if (calc_error_bound(measurements, p_L) + calc_error_bound(measurements, p_U) <= conf.delta) { + break; + } } } @@ -417,6 +449,30 @@ ApproxMC::SolCount Counter::calc_est_count() ApproxMC::SolCount ret_count; if (num_hash_list.empty() || num_count_list.empty()) return ret_count; + // round model counts + if (num_hash_list[0] > 0) { + double pivot = 9.84*(1.0+(1.0/conf.epsilon))*(1.0+(1.0/conf.epsilon)); + for (auto cnt_it = num_count_list.begin(); cnt_it != num_count_list.end(); cnt_it++) { + if (conf.epsilon < sqrt(2)-1) { + if (*cnt_it < sqrt(1+2*conf.epsilon)/2 * pivot) { + *cnt_it = sqrt(1+2*conf.epsilon)/2 * pivot; + } + } else if (conf.epsilon < 1) { + if (*cnt_it < pivot / sqrt(2)) { + *cnt_it = pivot / sqrt(2); + } + } else if (conf.epsilon < 3) { + if (*cnt_it < pivot) { + *cnt_it = pivot; + } + } else if (conf.epsilon < 4*sqrt(2)-1) { + *cnt_it = pivot; + } else { + *cnt_it = sqrt(2)*pivot; + } + } + } + const auto min_hash = find_min(num_hash_list); auto cnt_it = num_count_list.begin(); for (auto hash_it = num_hash_list.begin() @@ -431,7 +487,7 @@ ApproxMC::SolCount Counter::calc_est_count() *cnt_it *= pow(2, (*hash_it) - min_hash); } ret_count.valid = true; - ret_count.cellSolCount = find_median(num_count_list); + ret_count.cellSolCount = std::round(find_median(num_count_list)); ret_count.hashCount = min_hash; return ret_count; diff --git a/src/counter.h b/src/counter.h index 7174f1e..325bfbe 100644 --- a/src/counter.h +++ b/src/counter.h @@ -168,10 +168,11 @@ class Counter { void read_stdin(SATSolver* solver2); int find_best_sparse_match(); void set_up_probs_threshold_measurements(uint32_t& measurements, SparseData& sparse_data); + double calc_error_bound(uint32_t t, double p); //Data so we can output temporary count when catching the signal vector num_hash_list; - vector num_count_list; + vector num_count_list; template T find_median(const vector& nums); template T find_min(const vector& nums);