Skip to content

Commit

Permalink
add appmc6
Browse files Browse the repository at this point in the history
  • Loading branch information
@AL-JiongYang
AL-JiongYang committed Jun 2, 2024
1 parent 1cba322 commit 03829cb
Show file tree
Hide file tree
Showing 4 changed files with 65 additions and 76 deletions.
67 changes: 0 additions & 67 deletions src/appmc_constants.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}

Expand Down
1 change: 0 additions & 1 deletion src/appmc_constants.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,6 @@ class Constants
Constants();
vector<double> probval;
vector<VarMap> index_var_maps;
vector<double> iterationConfidences;

private:
vector<string> sparseprobvalues;
Expand Down
70 changes: 63 additions & 7 deletions src/counter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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;
}
}
}

Expand Down Expand Up @@ -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()
Expand All @@ -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;
Expand Down
3 changes: 2 additions & 1 deletion src/counter.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<uint64_t> num_hash_list;
vector<int64_t> num_count_list;
vector<double> num_count_list;
template<class T> T find_median(const vector<T>& nums);
template<class T> T find_min(const vector<T>& nums);

Expand Down

0 comments on commit 03829cb

Please sign in to comment.