From e9a9f8b716fe1e01d0c5fa56eec19a94a51b471d Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Mon, 4 Nov 2024 23:54:08 +0000 Subject: [PATCH] chore: fix collection script --- bv-evaluation/collect-data-hdel.py | 10 ++- .../compare-leansat-vs-bitwuzla-hdel.py | 2 +- .../bvw16_ch2_1DeMorgan_proved_data.csv | 18 ++-- ...ch2_2AdditionAndLogicalOps_proved_data.csv | 44 +++++----- ...16_ch2_3LogicalArithmeticIneq_ceg_data.csv | 84 +++++++++---------- .../bvw32_ch2_1DeMorgan_proved_data.csv | 18 ++-- ...ch2_2AdditionAndLogicalOps_proved_data.csv | 44 +++++----- ...32_ch2_3LogicalArithmeticIneq_ceg_data.csv | 84 +++++++++---------- .../bvw4_ch2_1DeMorgan_proved_data.csv | 18 ++-- ...ch2_2AdditionAndLogicalOps_proved_data.csv | 44 +++++----- ...w4_ch2_3LogicalArithmeticIneq_ceg_data.csv | 84 +++++++++---------- .../bvw64_ch2_1DeMorgan_proved_data.csv | 18 ++-- ...ch2_2AdditionAndLogicalOps_proved_data.csv | 44 +++++----- ...64_ch2_3LogicalArithmeticIneq_ceg_data.csv | 84 +++++++++---------- .../bvw8_ch2_1DeMorgan_proved_data.csv | 18 ++-- ...ch2_2AdditionAndLogicalOps_proved_data.csv | 44 +++++----- ...w8_ch2_3LogicalArithmeticIneq_ceg_data.csv | 84 +++++++++---------- 17 files changed, 372 insertions(+), 370 deletions(-) diff --git a/bv-evaluation/collect-data-hdel.py b/bv-evaluation/collect-data-hdel.py index 50c4173d2..86cafc91c 100644 --- a/bv-evaluation/collect-data-hdel.py +++ b/bv-evaluation/collect-data-hdel.py @@ -5,7 +5,7 @@ benchmark_dir = "../SSA/Projects/InstCombine/HackersDelight/" res_dir = "results/HackersDelight/" -raw_data_dir = 'raw-data/' +raw_data_dir = '../../paper-lean-bitvectors/raw-data/HackersDelight/' reps = 1 bv_width = [4, 8, 16, 32, 64] @@ -102,6 +102,7 @@ cegl = False if "counter example" in l: tot = float(l.split("ms")[0].split("after ")[1]) + print(counter_leanSAT_rw_times_average) if r == 0: counter_leanSAT_tot_times_average.append([tot]) counter_leanSAT_rw_times_average.append([float(l.split(" SAT")[0].split("rewriting ")[1])]) @@ -185,13 +186,14 @@ for thm in counter_bitwuzla_times_average: counter_bitwuzla_times.append(np.mean(thm)) - for counter_thm in counter_leanSAT_tot_times_average: + for thm in counter_leanSAT_tot_times_average: counter_leanSAT_tot_times.append(np.mean(thm)) - for counter_thm in counter_leanSAT_rw_times_average: + for thm in counter_leanSAT_rw_times_average: counter_leanSAT_rw_times.append(np.mean(thm)) - for counter_thm in counter_leanSAT_sat_times_average: + for thm in counter_leanSAT_sat_times_average: + print(counter_leanSAT_sat_times_average) counter_leanSAT_sat_times.append(np.mean(thm)) print("\n\nwith bitwidth = "+str(bvw)) diff --git a/bv-evaluation/compare-leansat-vs-bitwuzla-hdel.py b/bv-evaluation/compare-leansat-vs-bitwuzla-hdel.py index 71174b69d..ee1a7a77f 100644 --- a/bv-evaluation/compare-leansat-vs-bitwuzla-hdel.py +++ b/bv-evaluation/compare-leansat-vs-bitwuzla-hdel.py @@ -14,7 +14,7 @@ for file in os.listdir(benchmark_dir_list): print(file) for bvw in bv_width: - subprocess.Popen('sed -i -E \'s/variable \{x y z : BitVec .+\}/variable \{x y z : BitVec '+str(bvw)+'\}/g\' '+benchmark_dir_list+file, shell=True).wait() + subprocess.Popen('sed -i -E \'s/variable \\{x y z : BitVec .+\\}/variable \\{x y z : BitVec '+str(bvw)+'\\}/g\' '+benchmark_dir_list+file, shell=True).wait() # replace any sorrys with bv_compare' subprocess.Popen('sed -i -E \'s,all_goals sorry,bv_compare\'\\\'\',g\' '+benchmark_dir_list+file, shell=True).wait() for r in range(reps): diff --git a/bv-evaluation/raw-data/bvw16_ch2_1DeMorgan_proved_data.csv b/bv-evaluation/raw-data/bvw16_ch2_1DeMorgan_proved_data.csv index 113efde79..181d9929b 100644 --- a/bv-evaluation/raw-data/bvw16_ch2_1DeMorgan_proved_data.csv +++ b/bv-evaluation/raw-data/bvw16_ch2_1DeMorgan_proved_data.csv @@ -1,10 +1,10 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c -0,74.298435,80.396675,16.455224,0.0,55.543381,0.0,5.826306 -1,72.01669,80.094915,16.808351,0.0,55.751404,0.0,5.068354 -2,11.793657,11.47676,11.465999,0.0,0.0,0.0,0.0 -3,77.392578,80.375295,18.610391,0.0,54.021159,2.60192,3.883349 -4,9.818269,10.249333,10.23753,0.0,0.0,0.0,0.0 -5,67.896485,73.55371,11.803626,0.0,54.080661,0.0,5.158505 -6,68.331224,77.304229,17.405027,0.0,53.308384,0.0,4.163286 -7,76.966923,108.454276,36.044964,0.0,56.201444,7.840046,6.606608 -8,80.67495,110.0302,34.368801,0.0,55.612192,10.60878,7.89479 +0,78.140528,85.550821,16.724231,0.0,60.400822,0.0,5.806677 +1,75.441052,81.788411,13.720732,0.0,60.51121,0.0,5.13553 +2,10.61995,10.376751,10.365901,0.0,0.0,0.0,0.0 +3,80.636247,89.963016,22.19868,0.0,59.972171,2.480871,3.927914 +4,9.864515,9.872,9.860588,0.0,0.0,0.0,0.0 +5,73.295454,84.502232,17.2349,0.0,59.461098,0.0,5.27291 +6,73.456558,80.359625,14.233079,0.0,59.348295,0.0,4.240562 +7,83.190798,106.426705,21.386167,0.0,60.115231,7.625069,15.072343 +8,83.178815,116.881543,29.029732,0.0,60.540695,11.33997,13.722085 diff --git a/bv-evaluation/raw-data/bvw16_ch2_2AdditionAndLogicalOps_proved_data.csv b/bv-evaluation/raw-data/bvw16_ch2_2AdditionAndLogicalOps_proved_data.csv index ab52031b7..80a4203df 100644 --- a/bv-evaluation/raw-data/bvw16_ch2_2AdditionAndLogicalOps_proved_data.csv +++ b/bv-evaluation/raw-data/bvw16_ch2_2AdditionAndLogicalOps_proved_data.csv @@ -1,23 +1,23 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c -0,8.174278,7.65695,7.644376,0.0,0.0,0.0,0.0 -1,78.42752,90.602658,25.068318,0.0,54.191141,2.677073,6.757064 -2,10.874422,10.906604,10.894861,0.0,0.0,0.0,0.0 -3,7.866577,7.935004,7.923633,0.0,0.0,0.0,0.0 -4,10.635231,10.636444,10.624621,0.0,0.0,0.0,0.0 -5,81.666393,112.4303,26.026047,0.0,54.226658,15.454124,14.347696 -6,77.794867,89.042894,20.372748,0.0,53.899921,4.647902,7.327168 -7,73.168074,89.076487,21.169683,0.0,54.12713,3.949753,7.819377 -8,85.97836,117.532669,27.790827,0.0,53.855015,18.390898,14.133152 -9,81.330628,105.021699,29.78949,0.0,54.019646,8.750173,10.792768 -10,91.116929,148.51104,34.05666,1.011769,54.105998,33.394983,23.384232 -11,89.564709,115.880581,31.275522,0.0,54.207902,15.229031,13.268612 -12,93.220146,156.656225,39.34369,1.079917,54.524299,35.738034,23.28764 -13,80.48937,103.536145,29.548114,0.0,54.391539,5.746035,11.677116 -14,82.801154,91.51487,28.234944,0.0,55.678027,2.737216,3.436627 -15,78.907285,89.509414,25.591818,0.0,54.346253,4.204524,3.858132 -16,90.283095,142.930241,38.794563,0.0,54.219234,26.893785,21.091414 -17,79.74116,90.620159,21.25907,0.0,54.322919,5.499639,7.956997 -18,85.910472,105.73785,32.980011,0.0,54.334861,4.634808,11.469185 -19,72.960853,85.070616,22.808092,0.0,53.899109,0.0,5.876409 -20,70.037687,80.719704,17.392423,0.0,53.572121,1.704617,6.241921 -21,75.213112,93.486509,20.749439,0.0,53.368348,5.594748,11.718646 +0,9.015013,8.204822,8.190115,0.0,0.0,0.0,0.0 +1,82.260602,94.926454,26.60216,0.0,58.078881,2.736956,6.100241 +2,10.676999,9.998188,9.987447,0.0,0.0,0.0,0.0 +3,7.40803,7.3125,7.301448,0.0,0.0,0.0,0.0 +4,9.649029,9.758796,9.747905,0.0,0.0,0.0,0.0 +5,82.555569,116.197304,27.411438,0.0,57.812127,15.523424,13.122374 +6,80.094674,115.890182,30.336528,0.0,57.948212,6.628348,17.498672 +7,76.142116,89.945675,16.673935,0.0,58.037231,3.861647,9.439434 +8,87.30405,124.258446,29.933166,0.0,57.876887,17.809549,15.419026 +9,85.933484,124.030675,26.476032,0.0,58.302872,15.618643,21.206628 +10,95.452136,154.467581,35.980037,0.0,57.963402,32.973353,24.051507 +11,90.686793,117.734334,31.338909,0.0,58.062899,12.549452,13.884271 +12,93.922599,152.566395,34.383014,1.052176,57.843516,31.766556,24.729728 +13,85.100312,101.502213,25.6481,0.0,57.956188,5.561395,10.22353 +14,83.195486,96.125867,24.187965,0.0,58.047811,3.460762,8.385473 +15,82.650369,100.272362,26.949757,0.0,58.214716,4.250662,8.75996 +16,93.130305,143.136931,30.075164,0.0,58.170733,32.162553,20.779995 +17,81.946341,104.851071,21.400083,0.0,58.415173,11.10144,11.612664 +18,87.961381,100.298451,27.94295,0.0,58.501337,5.070007,6.957059 +19,77.990804,83.085248,17.939604,0.0,58.144644,1.00134,4.280739 +20,75.004439,80.619375,15.960338,0.0,57.971156,1.687745,3.686596 +21,82.867747,90.999503,22.262381,0.0,58.406217,3.593912,5.341962 diff --git a/bv-evaluation/raw-data/bvw16_ch2_3LogicalArithmeticIneq_ceg_data.csv b/bv-evaluation/raw-data/bvw16_ch2_3LogicalArithmeticIneq_ceg_data.csv index 2fa2975b3..3572a4c34 100644 --- a/bv-evaluation/raw-data/bvw16_ch2_3LogicalArithmeticIneq_ceg_data.csv +++ b/bv-evaluation/raw-data/bvw16_ch2_3LogicalArithmeticIneq_ceg_data.csv @@ -1,43 +1,43 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-sat -0,67.624229,68.964006,68.964006,68.964006 -1,66.230327,68.964006,68.964006,68.964006 -2,96.254569,68.964006,68.964006,68.964006 -3,100.854038,68.964006,68.964006,68.964006 -4,83.936832,68.964006,68.964006,68.964006 -5,85.661196,68.964006,68.964006,68.964006 -6,79.697662,68.964006,68.964006,68.964006 -7,84.970864,68.964006,68.964006,68.964006 -8,88.605584,68.964006,68.964006,68.964006 -9,82.853197,68.964006,68.964006,68.964006 -10,88.093908,68.964006,68.964006,68.964006 -11,84.495567,68.964006,68.964006,68.964006 -12,72.740393,68.964006,68.964006,68.964006 -13,73.175164,68.964006,68.964006,68.964006 -14,77.93119,68.964006,68.964006,68.964006 -15,79.583596,68.964006,68.964006,68.964006 -16,75.650003,68.964006,68.964006,68.964006 -17,102.746881,68.964006,68.964006,68.964006 -18,73.568443,68.964006,68.964006,68.964006 -19,69.861851,68.964006,68.964006,68.964006 -20,79.956341,68.964006,68.964006,68.964006 -21,71.771344,68.964006,68.964006,68.964006 -22,78.553885,68.964006,68.964006,68.964006 -23,80.221991,68.964006,68.964006,68.964006 -24,72.658526,68.964006,68.964006,68.964006 -25,71.855393,68.964006,68.964006,68.964006 -26,82.627321,68.964006,68.964006,68.964006 -27,91.051617,68.964006,68.964006,68.964006 -28,87.400448,68.964006,68.964006,68.964006 -29,90.87753,68.964006,68.964006,68.964006 -30,93.458211,68.964006,68.964006,68.964006 -31,83.604526,68.964006,68.964006,68.964006 -32,92.505893,68.964006,68.964006,68.964006 -33,87.331698,68.964006,68.964006,68.964006 -34,98.325657,68.964006,68.964006,68.964006 -35,85.687817,68.964006,68.964006,68.964006 -36,87.550211,68.964006,68.964006,68.964006 -37,96.164056,68.964006,68.964006,68.964006 -38,99.407747,68.964006,68.964006,68.964006 -39,67.124815,68.964006,68.964006,68.964006 -40,67.676215,68.964006,68.964006,68.964006 -41,68.964006,68.964006,68.964006,68.964006 +0,71.689644,75.160494,75.160494,75.160494 +1,70.38942,75.160494,75.160494,75.160494 +2,97.902831,75.160494,75.160494,75.160494 +3,102.067008,75.160494,75.160494,75.160494 +4,87.57377,75.160494,75.160494,75.160494 +5,89.157016,75.160494,75.160494,75.160494 +6,83.965921,75.160494,75.160494,75.160494 +7,81.484967,75.160494,75.160494,75.160494 +8,92.168448,75.160494,75.160494,75.160494 +9,87.703365,75.160494,75.160494,75.160494 +10,91.604778,75.160494,75.160494,75.160494 +11,87.390073,75.160494,75.160494,75.160494 +12,76.383191,75.160494,75.160494,75.160494 +13,76.967794,75.160494,75.160494,75.160494 +14,80.476306,75.160494,75.160494,75.160494 +15,82.24915,75.160494,75.160494,75.160494 +16,79.099108,75.160494,75.160494,75.160494 +17,104.26692,75.160494,75.160494,75.160494 +18,78.086866,75.160494,75.160494,75.160494 +19,75.970493,75.160494,75.160494,75.160494 +20,82.311407,75.160494,75.160494,75.160494 +21,76.699738,75.160494,75.160494,75.160494 +22,82.53543,75.160494,75.160494,75.160494 +23,85.379258,75.160494,75.160494,75.160494 +24,76.479032,75.160494,75.160494,75.160494 +25,76.459996,75.160494,75.160494,75.160494 +26,87.185246,75.160494,75.160494,75.160494 +27,94.09772,75.160494,75.160494,75.160494 +28,92.29604,75.160494,75.160494,75.160494 +29,93.293152,75.160494,75.160494,75.160494 +30,96.145324,75.160494,75.160494,75.160494 +31,88.324015,75.160494,75.160494,75.160494 +32,94.832948,75.160494,75.160494,75.160494 +33,93.199326,75.160494,75.160494,75.160494 +34,100.530899,75.160494,75.160494,75.160494 +35,90.430068,75.160494,75.160494,75.160494 +36,90.500952,75.160494,75.160494,75.160494 +37,101.128157,75.160494,75.160494,75.160494 +38,101.85053,75.160494,75.160494,75.160494 +39,73.390183,75.160494,75.160494,75.160494 +40,74.503112,75.160494,75.160494,75.160494 +41,75.160494,75.160494,75.160494,75.160494 diff --git a/bv-evaluation/raw-data/bvw32_ch2_1DeMorgan_proved_data.csv b/bv-evaluation/raw-data/bvw32_ch2_1DeMorgan_proved_data.csv index f73edafd5..f7d4a59f2 100644 --- a/bv-evaluation/raw-data/bvw32_ch2_1DeMorgan_proved_data.csv +++ b/bv-evaluation/raw-data/bvw32_ch2_1DeMorgan_proved_data.csv @@ -1,10 +1,10 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c -0,74.852382,79.157458,13.186396,0.0,56.175826,1.455347,6.218676 -1,73.266689,79.6146,13.974813,0.0,56.146531,1.36704,6.149054 -2,10.695255,10.671971,10.66123,0.0,0.0,0.0,0.0 -3,76.881422,97.991299,19.896899,0.0,55.977201,6.086215,13.383457 -4,9.837144,9.811958,9.801628,0.0,0.0,0.0,0.0 -5,69.345351,84.211433,18.313351,0.0,55.617361,1.415702,6.800564 -6,70.159805,80.556507,16.641716,0.0,54.645719,1.476135,5.779026 -7,79.208353,111.266311,21.559116,0.0,55.784305,18.036749,13.460052 -8,80.023881,111.851597,22.179779,0.0,55.706639,18.611684,12.701591 +0,76.384173,83.679671,18.127277,0.0,54.86732,1.374974,7.157617 +1,71.237802,90.757546,20.795312,0.0,60.105856,1.382118,6.445021 +2,11.509629,11.211406,11.200245,0.0,0.0,0.0,0.0 +3,76.386407,95.312522,19.665691,0.0,54.03619,5.763066,13.460189 +4,10.292252,10.307752,10.295738,0.0,0.0,0.0,0.0 +5,68.008198,82.291089,18.314159,0.0,53.756113,1.366509,6.860747 +6,68.722374,83.24,16.858733,0.0,57.144437,1.428235,5.841564 +7,81.136761,97.401695,21.43025,0.0,53.295473,8.263875,12.008034 +8,76.094676,110.219243,21.213251,0.0,53.474601,18.094054,15.079957 diff --git a/bv-evaluation/raw-data/bvw32_ch2_2AdditionAndLogicalOps_proved_data.csv b/bv-evaluation/raw-data/bvw32_ch2_2AdditionAndLogicalOps_proved_data.csv index 7adf78b1d..f84ece986 100644 --- a/bv-evaluation/raw-data/bvw32_ch2_2AdditionAndLogicalOps_proved_data.csv +++ b/bv-evaluation/raw-data/bvw32_ch2_2AdditionAndLogicalOps_proved_data.csv @@ -1,23 +1,23 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c -0,8.670172,7.78957,7.776335,0.0,0.0,0.0,0.0 -1,79.75753,87.334579,19.985167,0.0,55.716879,4.227558,5.355878 -2,10.106763,10.354451,10.342779,0.0,0.0,0.0,0.0 -3,7.467382,7.362904,7.351483,0.0,0.0,0.0,0.0 -4,9.728289,9.744421,9.734151,0.0,0.0,0.0,0.0 -5,80.45753,187.942519,27.886589,0.0,105.782925,25.15342,26.294512 -6,79.759154,133.545147,22.799286,3.425505,55.97719,22.064492,23.980797 -7,74.223616,91.883713,20.172049,0.0,56.429553,6.786227,6.499307 -8,84.639072,158.352966,26.930464,3.700424,55.753529,28.854625,37.248587 -9,85.233496,129.958458,24.901113,0.0,54.033783,26.284916,22.066725 -10,92.337821,265.235426,35.149825,3.759004,106.178291,51.704287,61.988205 -11,92.743876,190.860325,31.168301,0.0,106.249555,26.640216,23.817348 -12,91.5791,271.927246,40.918642,4.029184,106.157803,49.524484,64.546664 -13,81.979102,114.041832,32.573384,0.0,56.18579,7.455224,14.856856 -14,81.274522,110.708521,37.730987,0.0,56.071669,7.251074,7.383403 -15,80.09112,101.862977,21.976324,0.0,54.14765,11.596793,11.447117 -16,89.087438,362.377996,33.146684,0.0,206.496333,59.090377,59.925964 -17,80.835353,112.612383,23.126224,0.0,56.479538,17.554828,12.672857 -18,86.380468,133.829795,29.2496,0.0,55.747748,23.725265,21.714941 -19,75.346295,82.265973,18.261262,0.0,56.147422,1.82262,4.097681 -20,74.020984,86.501388,18.856305,0.0,56.089142,2.727086,6.850197 -21,80.23449,114.94779,29.018755,0.0,56.589646,8.666205,17.748134 +0,8.697162,7.664523,7.650076,0.0,0.0,0.0,0.0 +1,83.308089,100.207901,28.09638,0.0,60.57479,4.105458,5.458199 +2,9.950386,10.250144,10.239113,0.0,0.0,0.0,0.0 +3,7.136397,7.26997,7.259289,0.0,0.0,0.0,0.0 +4,9.708501,10.060905,10.050386,0.0,0.0,0.0,0.0 +5,85.185703,187.905372,25.047237,0.0,110.357694,22.787332,27.140505 +6,81.423281,132.496882,21.281941,3.377484,59.936715,20.308574,22.406362 +7,78.463607,90.980197,17.798638,0.0,60.095013,5.14542,6.070786 +8,89.276571,166.685408,26.316582,3.572452,60.432922,35.742919,34.94302 +9,86.745145,184.064516,30.384066,0.0,110.456444,19.00317,21.407858 +10,96.175419,280.713429,41.610964,3.736021,110.848099,61.54498,56.649724 +11,93.341192,146.90978,30.722857,0.0,61.111453,28.941886,22.85515 +12,96.862568,269.878601,39.743049,3.856909,111.424936,48.605862,59.44099 +13,85.604632,103.088245,23.159814,0.0,61.182135,7.641269,8.815646 +14,85.489766,102.829166,21.952486,0.0,61.489766,7.306748,9.46517 +15,84.925782,112.184731,22.040241,0.0,61.422118,11.719947,14.200478 +16,93.186411,357.122877,29.870918,0.0,211.679824,58.084931,54.193407 +17,84.238004,116.862419,23.015493,0.0,61.532457,17.480035,12.334435 +18,91.149316,133.547775,27.688681,0.0,61.420205,23.029057,18.392508 +19,80.407777,96.662789,22.366677,0.0,61.534801,1.948967,8.315961 +20,79.174317,95.638257,14.667418,0.0,61.636425,4.871583,12.179124 +21,83.774139,111.377077,25.067724,0.0,61.699361,8.562168,13.309808 diff --git a/bv-evaluation/raw-data/bvw32_ch2_3LogicalArithmeticIneq_ceg_data.csv b/bv-evaluation/raw-data/bvw32_ch2_3LogicalArithmeticIneq_ceg_data.csv index 8de5b372d..293c0a387 100644 --- a/bv-evaluation/raw-data/bvw32_ch2_3LogicalArithmeticIneq_ceg_data.csv +++ b/bv-evaluation/raw-data/bvw32_ch2_3LogicalArithmeticIneq_ceg_data.csv @@ -1,43 +1,43 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-sat -0,69.112455,71.859619,71.859619,71.859619 -1,67.032781,71.859619,71.859619,71.859619 -2,95.977914,71.859619,71.859619,71.859619 -3,101.204479,71.859619,71.859619,71.859619 -4,83.669478,71.859619,71.859619,71.859619 -5,85.576565,71.859619,71.859619,71.859619 -6,82.237323,71.859619,71.859619,71.859619 -7,78.575414,71.859619,71.859619,71.859619 -8,89.35144,71.859619,71.859619,71.859619 -9,84.797505,71.859619,71.859619,71.859619 -10,88.611963,71.859619,71.859619,71.859619 -11,84.636571,71.859619,71.859619,71.859619 -12,73.175653,71.859619,71.859619,71.859619 -13,73.546854,71.859619,71.859619,71.859619 -14,78.022931,71.859619,71.859619,71.859619 -15,79.81887,71.859619,71.859619,71.859619 -16,74.592868,71.859619,71.859619,71.859619 -17,100.371336,71.859619,71.859619,71.859619 -18,67.312838,71.859619,71.859619,71.859619 -19,68.83954,71.859619,71.859619,71.859619 -20,77.851756,71.859619,71.859619,71.859619 -21,68.671553,71.859619,71.859619,71.859619 -22,80.812285,71.859619,71.859619,71.859619 -23,80.323141,71.859619,71.859619,71.859619 -24,71.178574,71.859619,71.859619,71.859619 -25,72.198991,71.859619,71.859619,71.859619 -26,81.768599,71.859619,71.859619,71.859619 -27,90.033245,71.859619,71.859619,71.859619 -28,88.809476,71.859619,71.859619,71.859619 -29,89.310251,71.859619,71.859619,71.859619 -30,96.601401,71.859619,71.859619,71.859619 -31,83.276906,71.859619,71.859619,71.859619 -32,91.439218,71.859619,71.859619,71.859619 -33,89.884054,71.859619,71.859619,71.859619 -34,97.310979,71.859619,71.859619,71.859619 -35,86.862823,71.859619,71.859619,71.859619 -36,88.903092,71.859619,71.859619,71.859619 -37,99.188273,71.859619,71.859619,71.859619 -38,101.672108,71.859619,71.859619,71.859619 -39,70.73617,71.859619,71.859619,71.859619 -40,71.332794,71.859619,71.859619,71.859619 -41,71.859619,71.859619,71.859619,71.859619 +0,71.035048,74.92517,74.92517,74.92517 +1,70.471054,74.92517,74.92517,74.92517 +2,98.504036,74.92517,74.92517,74.92517 +3,102.935909,74.92517,74.92517,74.92517 +4,87.681793,74.92517,74.92517,74.92517 +5,89.749614,74.92517,74.92517,74.92517 +6,84.6381,74.92517,74.92517,74.92517 +7,82.441484,74.92517,74.92517,74.92517 +8,92.198797,74.92517,74.92517,74.92517 +9,88.721676,74.92517,74.92517,74.92517 +10,92.0633,74.92517,74.92517,74.92517 +11,87.993781,74.92517,74.92517,74.92517 +12,77.402663,74.92517,74.92517,74.92517 +13,77.052916,74.92517,74.92517,74.92517 +14,80.784025,74.92517,74.92517,74.92517 +15,85.131971,74.92517,74.92517,74.92517 +16,79.300068,74.92517,74.92517,74.92517 +17,104.251231,74.92517,74.92517,74.92517 +18,79.077375,74.92517,74.92517,74.92517 +19,77.881528,74.92517,74.92517,74.92517 +20,83.101249,74.92517,74.92517,74.92517 +21,77.534894,74.92517,74.92517,74.92517 +22,83.822319,74.92517,74.92517,74.92517 +23,86.512215,74.92517,74.92517,74.92517 +24,77.916765,74.92517,74.92517,74.92517 +25,77.906035,74.92517,74.92517,74.92517 +26,88.51741,74.92517,74.92517,74.92517 +27,95.162851,74.92517,74.92517,74.92517 +28,93.03342,74.92517,74.92517,74.92517 +29,94.2672,74.92517,74.92517,74.92517 +30,96.95931,74.92517,74.92517,74.92517 +31,89.295278,74.92517,74.92517,74.92517 +32,96.098446,74.92517,74.92517,74.92517 +33,93.987562,74.92517,74.92517,74.92517 +34,101.595968,74.92517,74.92517,74.92517 +35,90.735936,74.92517,74.92517,74.92517 +36,92.235125,74.92517,74.92517,74.92517 +37,102.398965,74.92517,74.92517,74.92517 +38,102.713808,74.92517,74.92517,74.92517 +39,74.508494,74.92517,74.92517,74.92517 +40,76.054321,74.92517,74.92517,74.92517 +41,74.92517,74.92517,74.92517,74.92517 diff --git a/bv-evaluation/raw-data/bvw4_ch2_1DeMorgan_proved_data.csv b/bv-evaluation/raw-data/bvw4_ch2_1DeMorgan_proved_data.csv index eced5ab02..050d6ab34 100644 --- a/bv-evaluation/raw-data/bvw4_ch2_1DeMorgan_proved_data.csv +++ b/bv-evaluation/raw-data/bvw4_ch2_1DeMorgan_proved_data.csv @@ -1,10 +1,10 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c -0,74.461205,73.197468,12.692883,0.0,53.914048,0.0,3.718748 -1,69.419551,77.738157,18.062958,0.0,53.770716,0.0,3.227462 -2,10.706354,10.488705,10.478475,0.0,0.0,0.0,0.0 -3,74.149025,79.960994,18.765715,0.0,53.392925,0.0,5.492936 -4,9.766822,10.257989,10.247508,0.0,0.0,0.0,0.0 -5,70.369092,72.787695,11.639977,0.0,55.357381,0.0,3.060986 -6,67.821773,75.910159,16.738419,0.0,54.489584,0.0,1.996798 -7,79.294185,88.018779,23.692803,0.0,53.700014,2.147492,6.924257 -8,80.050421,81.635464,21.402421,0.0,53.348422,2.011636,3.949815 +0,77.698052,79.192392,12.773354,0.0,60.105394,0.0,3.79779 +1,76.015272,78.633615,13.680425,0.0,59.456348,0.0,3.153842 +2,10.618583,10.45503,10.443889,0.0,0.0,0.0,0.0 +3,81.124809,86.510744,18.670191,0.0,60.252653,0.0,5.396835 +4,9.789224,9.813289,9.801748,0.0,0.0,0.0,0.0 +5,73.206736,77.071451,11.380606,0.0,59.792914,0.0,3.045728 +6,73.05502,78.422029,13.905241,0.0,59.807612,0.0,2.022257 +7,82.849855,92.494374,21.428277,0.0,60.396342,2.180786,6.944975 +8,84.311441,95.958152,25.252343,0.0,60.244857,2.080065,6.812766 diff --git a/bv-evaluation/raw-data/bvw4_ch2_2AdditionAndLogicalOps_proved_data.csv b/bv-evaluation/raw-data/bvw4_ch2_2AdditionAndLogicalOps_proved_data.csv index eb2cda2eb..e69917704 100644 --- a/bv-evaluation/raw-data/bvw4_ch2_2AdditionAndLogicalOps_proved_data.csv +++ b/bv-evaluation/raw-data/bvw4_ch2_2AdditionAndLogicalOps_proved_data.csv @@ -1,23 +1,23 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c -0,8.751015,8.235302,8.222608,0.0,0.0,0.0,0.0 -1,79.728506,93.121761,28.853924,0.0,56.232383,0.0,5.76532 -2,10.958061,11.018184,11.005929,0.0,0.0,0.0,0.0 -3,7.859953,8.012332,8.0009,0.0,0.0,0.0,0.0 -4,10.723227,10.825982,10.81474,0.0,0.0,0.0,0.0 -5,83.487829,91.994124,23.835914,0.0,55.336343,2.987207,8.278062 -6,77.242394,92.441318,27.814062,0.0,55.62745,1.224501,6.158603 -7,75.31721,78.277718,16.899503,0.0,55.281599,1.127207,2.984853 -8,86.077117,94.870512,27.970397,0.0,55.469392,1.985938,7.68384 -9,83.053511,98.510521,28.855076,0.0,56.137304,3.335443,8.533674 -10,93.008578,103.296263,34.619454,0.0,55.68413,5.43118,6.363238 -11,92.12515,100.174271,31.600408,0.0,55.80172,3.266485,7.91243 -12,95.581754,103.031683,34.22523,0.0,55.91249,4.509019,7.118714 -13,82.776639,95.901708,31.112796,0.0,56.05563,1.285777,5.853406 -14,82.994429,90.898565,28.508732,0.0,55.942035,1.009816,3.345984 -15,81.23079,89.794031,28.185162,0.0,56.046655,1.395102,3.14775 -16,89.455413,107.483065,32.795573,0.0,55.857245,5.342973,11.828412 -17,81.420948,88.367291,25.050025,0.0,55.889618,2.193079,4.259809 -18,87.595091,95.124051,28.169672,0.0,55.961383,1.847466,7.496158 -19,75.823715,83.578039,21.73569,0.0,55.645655,0.0,4.21777 -20,75.276242,78.603412,19.678418,0.0,55.323218,0.0,1.58457 -21,80.500432,87.090067,24.670257,0.0,56.216603,1.420541,3.836261 +0,8.680992,8.106618,8.092631,0.0,0.0,0.0,0.0 +1,131.587747,85.809069,20.609622,0.0,57.23124,0.0,5.705997 +2,10.187666,9.934277,9.923697,0.0,0.0,0.0,0.0 +3,7.20174,7.279236,7.267083,0.0,0.0,0.0,0.0 +4,10.580507,10.670085,10.658724,0.0,0.0,0.0,0.0 +5,84.31023,97.018462,31.368084,0.0,57.560061,3.037912,4.057968 +6,79.2014,90.893943,23.791606,0.0,57.978819,1.16582,6.21576 +7,75.694161,80.701169,16.27939,0.0,57.913717,1.077623,2.931211 +8,83.11787,100.047367,31.468684,0.0,57.413103,1.930713,7.459466 +9,86.233649,96.723966,25.916577,0.0,57.624552,3.127721,8.451138 +10,95.870935,112.261185,39.752786,0.0,57.614594,5.400721,8.222967 +11,91.940286,100.856964,31.128612,0.0,57.817636,3.173058,7.149723 +12,93.43617,105.900602,35.343737,0.0,58.085652,4.591604,6.707627 +13,82.74698,89.43852,23.292825,0.0,57.58561,1.318077,5.715737 +14,81.377187,91.871638,28.541579,0.0,57.575028,0.0,3.235074 +15,81.059818,94.089943,27.506417,0.0,57.572964,1.215844,6.313172 +16,91.752254,103.699109,31.274888,0.0,57.536938,5.232514,8.144269 +17,77.190746,88.40558,24.443335,0.0,57.817558,2.088231,2.953383 +18,87.28387,97.340168,28.437333,0.0,58.038123,1.872974,7.447845 +19,77.829581,84.200884,20.521215,0.0,57.608833,0.0,4.182213 +20,70.675741,79.655935,16.041702,0.0,57.587322,0.0,4.066683 +21,80.693815,91.431649,26.518021,0.0,57.856951,1.383611,3.489556 diff --git a/bv-evaluation/raw-data/bvw4_ch2_3LogicalArithmeticIneq_ceg_data.csv b/bv-evaluation/raw-data/bvw4_ch2_3LogicalArithmeticIneq_ceg_data.csv index acfdcdc78..f066e932a 100644 --- a/bv-evaluation/raw-data/bvw4_ch2_3LogicalArithmeticIneq_ceg_data.csv +++ b/bv-evaluation/raw-data/bvw4_ch2_3LogicalArithmeticIneq_ceg_data.csv @@ -1,43 +1,43 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-sat -0,68.713176,73.31011,73.31011,73.31011 -1,67.723789,73.31011,73.31011,73.31011 -2,94.524546,73.31011,73.31011,73.31011 -3,99.495899,73.31011,73.31011,73.31011 -4,84.965817,73.31011,73.31011,73.31011 -5,87.124882,73.31011,73.31011,73.31011 -6,81.967649,73.31011,73.31011,73.31011 -7,79.09126,73.31011,73.31011,73.31011 -8,88.631011,73.31011,73.31011,73.31011 -9,84.166529,73.31011,73.31011,73.31011 -10,88.672582,73.31011,73.31011,73.31011 -11,84.512312,73.31011,73.31011,73.31011 -12,73.516691,73.31011,73.31011,73.31011 -13,74.692921,73.31011,73.31011,73.31011 -14,81.046492,73.31011,73.31011,73.31011 -15,83.679259,73.31011,73.31011,73.31011 -16,75.208192,73.31011,73.31011,73.31011 -17,101.034151,73.31011,73.31011,73.31011 -18,82.343047,73.31011,73.31011,73.31011 -19,72.080139,73.31011,73.31011,73.31011 -20,78.351635,73.31011,73.31011,73.31011 -21,72.193313,73.31011,73.31011,73.31011 -22,78.306399,73.31011,73.31011,73.31011 -23,82.26017,73.31011,73.31011,73.31011 -24,73.443222,73.31011,73.31011,73.31011 -25,73.853286,73.31011,73.31011,73.31011 -26,82.658252,73.31011,73.31011,73.31011 -27,90.58971,73.31011,73.31011,73.31011 -28,88.170093,73.31011,73.31011,73.31011 -29,89.086735,73.31011,73.31011,73.31011 -30,92.691355,73.31011,73.31011,73.31011 -31,85.665227,73.31011,73.31011,73.31011 -32,90.5736,73.31011,73.31011,73.31011 -33,89.442365,73.31011,73.31011,73.31011 -34,97.551127,73.31011,73.31011,73.31011 -35,86.581736,73.31011,73.31011,73.31011 -36,85.841168,73.31011,73.31011,73.31011 -37,97.399511,73.31011,73.31011,73.31011 -38,98.099171,73.31011,73.31011,73.31011 -39,78.706163,73.31011,73.31011,73.31011 -40,71.240063,73.31011,73.31011,73.31011 -41,73.31011,73.31011,73.31011,73.31011 +0,70.996756,75.119547,75.119547,75.119547 +1,70.737007,75.119547,75.119547,75.119547 +2,97.38802,75.119547,75.119547,75.119547 +3,102.814229,75.119547,75.119547,75.119547 +4,86.66348,75.119547,75.119547,75.119547 +5,88.691679,75.119547,75.119547,75.119547 +6,83.886902,75.119547,75.119547,75.119547 +7,81.482724,75.119547,75.119547,75.119547 +8,91.704603,75.119547,75.119547,75.119547 +9,87.523524,75.119547,75.119547,75.119547 +10,92.632293,75.119547,75.119547,75.119547 +11,87.138738,75.119547,75.119547,75.119547 +12,77.059618,75.119547,75.119547,75.119547 +13,77.364222,75.119547,75.119547,75.119547 +14,81.384768,75.119547,75.119547,75.119547 +15,81.985485,75.119547,75.119547,75.119547 +16,78.413961,75.119547,75.119547,75.119547 +17,104.177882,75.119547,75.119547,75.119547 +18,78.007906,75.119547,75.119547,75.119547 +19,76.144181,75.119547,75.119547,75.119547 +20,82.355822,75.119547,75.119547,75.119547 +21,76.576051,75.119547,75.119547,75.119547 +22,81.95198,75.119547,75.119547,75.119547 +23,85.287474,75.119547,75.119547,75.119547 +24,76.849482,75.119547,75.119547,75.119547 +25,76.694559,75.119547,75.119547,75.119547 +26,86.698525,75.119547,75.119547,75.119547 +27,93.363654,75.119547,75.119547,75.119547 +28,92.080293,75.119547,75.119547,75.119547 +29,93.072766,75.119547,75.119547,75.119547 +30,96.157696,75.119547,75.119547,75.119547 +31,88.602499,75.119547,75.119547,75.119547 +32,95.426898,75.119547,75.119547,75.119547 +33,93.180949,75.119547,75.119547,75.119547 +34,99.576389,75.119547,75.119547,75.119547 +35,89.31259,75.119547,75.119547,75.119547 +36,90.861754,75.119547,75.119547,75.119547 +37,101.816596,75.119547,75.119547,75.119547 +38,102.175613,75.119547,75.119547,75.119547 +39,74.931751,75.119547,75.119547,75.119547 +40,74.525816,75.119547,75.119547,75.119547 +41,75.119547,75.119547,75.119547,75.119547 diff --git a/bv-evaluation/raw-data/bvw64_ch2_1DeMorgan_proved_data.csv b/bv-evaluation/raw-data/bvw64_ch2_1DeMorgan_proved_data.csv index 4a02bd8a4..9f8addc7c 100644 --- a/bv-evaluation/raw-data/bvw64_ch2_1DeMorgan_proved_data.csv +++ b/bv-evaluation/raw-data/bvw64_ch2_1DeMorgan_proved_data.csv @@ -1,10 +1,10 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c -0,73.64312,86.275611,16.052233,0.0,55.84969,2.401262,9.140249 -1,71.52869,81.116992,13.852491,0.0,54.797832,2.281506,7.647352 -2,10.724339,10.489316,10.478425,0.0,0.0,0.0,0.0 -3,76.116427,106.818007,18.636321,0.0,55.450297,17.624911,12.182683 -4,9.83459,9.834329,9.82415,0.0,0.0,0.0,0.0 -5,69.734383,80.585321,12.04901,0.0,55.658018,2.475953,7.578031 -6,69.744773,96.686527,25.985589,0.0,55.703894,2.548039,9.574609 -7,78.873826,178.713808,22.021549,0.0,105.572969,21.960683,24.951928 -8,78.606067,263.504886,28.586527,0.0,155.938467,36.738361,37.977081 +0,76.344488,90.906758,18.21356,0.0,60.012268,2.493786,6.482724 +1,75.410616,94.709794,22.82358,0.0,57.855809,2.332491,9.23675 +2,10.758261,10.488843,10.478273,0.0,0.0,0.0,0.0 +3,78.43837,107.762676,19.112365,0.0,58.231899,15.577947,12.014062 +4,9.792941,9.778002,9.767121,0.0,0.0,0.0,0.0 +5,71.203217,93.847838,19.80815,0.0,58.350271,2.674767,10.110018 +6,72.144923,82.271662,13.836981,0.0,53.957462,2.51191,9.159174 +7,80.453361,189.144441,21.783347,0.0,108.223626,31.299384,23.698521 +8,81.815172,268.171398,23.70396,0.0,158.524127,41.947799,39.456867 diff --git a/bv-evaluation/raw-data/bvw64_ch2_2AdditionAndLogicalOps_proved_data.csv b/bv-evaluation/raw-data/bvw64_ch2_2AdditionAndLogicalOps_proved_data.csv index 2fff13cb1..8ec581a41 100644 --- a/bv-evaluation/raw-data/bvw64_ch2_2AdditionAndLogicalOps_proved_data.csv +++ b/bv-evaluation/raw-data/bvw64_ch2_2AdditionAndLogicalOps_proved_data.csv @@ -1,23 +1,23 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c -0,8.793735,8.198672,8.184887,0.0,0.0,0.0,0.0 -1,80.438404,115.788769,27.897888,0.0,56.322162,10.265854,17.439721 -2,10.686959,10.434141,10.422399,0.0,0.0,0.0,0.0 -3,7.147389,7.261113,7.250714,0.0,0.0,0.0,0.0 -4,9.705366,9.758707,9.730834,0.0,0.0,0.0,0.0 -5,80.673618,450.45808,28.440162,0.0,256.438494,81.938755,79.052408 -6,78.685446,357.55447,23.475983,14.474897,156.322724,58.003144,86.951415 -7,76.784608,107.377544,16.770228,0.0,57.097335,14.296741,15.299134 -8,87.010118,569.022585,28.794952,16.067422,306.94434,90.437584,106.563468 -9,86.755034,380.019266,28.093088,0.0,206.756563,64.59187,75.374976 -10,193.217723,805.345196,36.984146,16.120793,457.9034,125.175283,149.426838 -11,93.417709,320.952435,40.33477,0.0,156.89313,61.271782,56.658306 -12,243.839397,1011.936537,34.763045,15.783888,558.434523,182.272487,200.803298 -13,84.478258,137.474782,25.262796,0.0,57.179989,28.301872,22.200256 -14,84.077011,114.373166,27.406722,0.0,57.173778,13.636245,11.910869 -15,81.486222,119.114675,22.322107,0.0,57.026301,20.285994,15.946314 -16,88.771742,792.167285,30.41605,0.0,458.2481,143.529219,153.712758 -17,82.668231,260.926483,24.593412,0.0,157.736012,35.314476,38.672653 -18,87.951704,208.741828,29.957636,0.0,108.117901,33.373191,32.598992 -19,76.867205,87.482178,18.318501,0.0,57.484464,2.992307,5.803453 -20,74.359832,105.563421,20.251398,0.0,57.683151,10.308774,14.468887 -21,81.528661,122.782016,28.425886,0.0,57.42298,17.668945,15.364127 +0,8.958715,8.259567,8.244377,0.0,0.0,0.0,0.0 +1,82.645579,95.316681,21.876844,0.0,54.791165,6.437347,8.978703 +2,9.976296,9.991865,9.980443,0.0,0.0,0.0,0.0 +3,7.375408,7.576458,7.565206,0.0,0.0,0.0,0.0 +4,9.917445,10.277013,10.265902,0.0,0.0,0.0,0.0 +5,78.637207,450.880615,24.06412,0.0,254.598805,84.409138,83.230993 +6,83.867494,351.636996,20.505476,12.933035,154.420013,61.067529,86.323799 +7,81.598904,105.133485,23.523518,0.0,54.646232,12.467637,11.394031 +8,90.507253,521.190768,29.982188,13.944084,254.990547,97.600871,102.945747 +9,90.331059,377.47834,26.864105,0.0,205.008376,64.425887,75.926829 +10,201.908256,805.383971,37.159754,16.303367,460.831808,124.178173,146.673172 +11,147.403993,319.407246,31.75822,0.0,155.424389,64.167208,62.329381 +12,250.509712,976.149971,36.557326,15.932987,514.099045,186.286278,202.24924 +13,91.620886,133.613828,30.700885,0.0,55.429589,25.123059,18.723311 +14,88.810612,121.635606,23.204849,0.0,60.587595,13.658505,19.917307 +15,87.895977,118.707238,21.879718,0.0,55.268256,21.928953,16.004891 +16,96.052389,779.411799,31.224022,0.0,457.428832,139.350585,144.786314 +17,89.187494,270.770655,26.531377,0.0,155.701982,45.676605,38.188455 +18,94.807387,214.115864,30.283136,0.0,114.376096,30.708158,34.070112 +19,82.743294,93.57883,22.759849,0.0,54.847742,4.175459,8.349536 +20,81.072903,113.088856,17.937138,0.0,55.568811,13.303755,22.940049 +21,87.06565,111.827146,20.202824,0.0,55.517547,17.637113,14.886282 diff --git a/bv-evaluation/raw-data/bvw64_ch2_3LogicalArithmeticIneq_ceg_data.csv b/bv-evaluation/raw-data/bvw64_ch2_3LogicalArithmeticIneq_ceg_data.csv index 0b8738687..5a3aa4f4b 100644 --- a/bv-evaluation/raw-data/bvw64_ch2_3LogicalArithmeticIneq_ceg_data.csv +++ b/bv-evaluation/raw-data/bvw64_ch2_3LogicalArithmeticIneq_ceg_data.csv @@ -1,43 +1,43 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-sat -0,69.708289,71.302206,71.302206,71.302206 -1,68.457778,71.302206,71.302206,71.302206 -2,98.298522,71.302206,71.302206,71.302206 -3,102.696963,71.302206,71.302206,71.302206 -4,86.036112,71.302206,71.302206,71.302206 -5,84.930455,71.302206,71.302206,71.302206 -6,85.703023,71.302206,71.302206,71.302206 -7,83.72967,71.302206,71.302206,71.302206 -8,91.743302,71.302206,71.302206,71.302206 -9,84.616583,71.302206,71.302206,71.302206 -10,87.652993,71.302206,71.302206,71.302206 -11,88.243315,71.302206,71.302206,71.302206 -12,73.191172,71.302206,71.302206,71.302206 -13,74.275257,71.302206,71.302206,71.302206 -14,76.912484,71.302206,71.302206,71.302206 -15,86.558606,71.302206,71.302206,71.302206 -16,75.750482,71.302206,71.302206,71.302206 -17,104.769294,71.302206,71.302206,71.302206 -18,120.459353,71.302206,71.302206,71.302206 -19,71.287278,71.302206,71.302206,71.302206 -20,76.727625,71.302206,71.302206,71.302206 -21,73.252297,71.302206,71.302206,71.302206 -22,78.767094,71.302206,71.302206,71.302206 -23,79.688462,71.302206,71.302206,71.302206 -24,74.019655,71.302206,71.302206,71.302206 -25,75.578887,71.302206,71.302206,71.302206 -26,84.086091,71.302206,71.302206,71.302206 -27,91.693407,71.302206,71.302206,71.302206 -28,91.402967,71.302206,71.302206,71.302206 -29,91.021068,71.302206,71.302206,71.302206 -30,94.535291,71.302206,71.302206,71.302206 -31,85.313147,71.302206,71.302206,71.302206 -32,92.79131,71.302206,71.302206,71.302206 -33,92.422553,71.302206,71.302206,71.302206 -34,99.54241,71.302206,71.302206,71.302206 -35,89.313676,71.302206,71.302206,71.302206 -36,91.314321,71.302206,71.302206,71.302206 -37,100.072379,71.302206,71.302206,71.302206 -38,102.223188,71.302206,71.302206,71.302206 -39,68.517719,71.302206,71.302206,71.302206 -40,71.471666,71.302206,71.302206,71.302206 -41,71.302206,71.302206,71.302206,71.302206 +0,69.315794,75.57742,75.57742,75.57742 +1,68.146307,75.57742,75.57742,75.57742 +2,96.51906,75.57742,75.57742,75.57742 +3,103.877746,75.57742,75.57742,75.57742 +4,85.164212,75.57742,75.57742,75.57742 +5,87.413999,75.57742,75.57742,75.57742 +6,82.563615,75.57742,75.57742,75.57742 +7,80.041985,75.57742,75.57742,75.57742 +8,89.634987,75.57742,75.57742,75.57742 +9,85.998717,75.57742,75.57742,75.57742 +10,90.243136,75.57742,75.57742,75.57742 +11,87.49522,75.57742,75.57742,75.57742 +12,75.675927,75.57742,75.57742,75.57742 +13,76.08572,75.57742,75.57742,75.57742 +14,78.747823,75.57742,75.57742,75.57742 +15,81.156818,75.57742,75.57742,75.57742 +16,76.188103,75.57742,75.57742,75.57742 +17,104.464502,75.57742,75.57742,75.57742 +18,125.191256,75.57742,75.57742,75.57742 +19,76.697775,75.57742,75.57742,75.57742 +20,83.147336,75.57742,75.57742,75.57742 +21,76.545027,75.57742,75.57742,75.57742 +22,84.077389,75.57742,75.57742,75.57742 +23,85.271272,75.57742,75.57742,75.57742 +24,77.037506,75.57742,75.57742,75.57742 +25,77.278991,75.57742,75.57742,75.57742 +26,86.995456,75.57742,75.57742,75.57742 +27,94.573297,75.57742,75.57742,75.57742 +28,92.35937,75.57742,75.57742,75.57742 +29,94.010887,75.57742,75.57742,75.57742 +30,95.72,75.57742,75.57742,75.57742 +31,88.281985,75.57742,75.57742,75.57742 +32,95.510725,75.57742,75.57742,75.57742 +33,93.925566,75.57742,75.57742,75.57742 +34,101.112165,75.57742,75.57742,75.57742 +35,89.589323,75.57742,75.57742,75.57742 +36,92.128314,75.57742,75.57742,75.57742 +37,104.950249,75.57742,75.57742,75.57742 +38,101.706618,75.57742,75.57742,75.57742 +39,75.062288,75.57742,75.57742,75.57742 +40,75.607658,75.57742,75.57742,75.57742 +41,75.57742,75.57742,75.57742,75.57742 diff --git a/bv-evaluation/raw-data/bvw8_ch2_1DeMorgan_proved_data.csv b/bv-evaluation/raw-data/bvw8_ch2_1DeMorgan_proved_data.csv index be3d527a8..9f8fd072e 100644 --- a/bv-evaluation/raw-data/bvw8_ch2_1DeMorgan_proved_data.csv +++ b/bv-evaluation/raw-data/bvw8_ch2_1DeMorgan_proved_data.csv @@ -1,10 +1,10 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c -0,74.433813,76.150391,14.953681,0.0,54.045174,0.0,5.114522 -1,70.16758,79.149141,16.763696,0.0,55.954007,0.0,4.41871 -2,10.84743,10.532577,10.522608,0.0,0.0,0.0,0.0 -3,76.893765,78.340996,18.902923,0.0,53.517859,1.525048,3.381481 -4,10.059715,9.992599,9.981527,0.0,0.0,0.0,0.0 -5,69.096449,74.028336,11.80141,0.0,55.514549,0.0,4.613075 -6,67.208988,78.530974,17.638637,0.0,55.527171,0.0,3.449699 -7,81.339755,93.648664,22.644755,0.0,55.790878,3.962706,9.376314 -8,79.850004,98.575543,29.52507,0.0,55.720307,6.873091,5.305842 +0,78.138082,81.981136,15.010756,0.0,59.565376,0.0,5.181888 +1,75.955184,73.989785,13.627085,0.0,54.139805,0.0,4.360279 +2,10.870865,10.512218,10.501407,0.0,0.0,0.0,0.0 +3,74.779865,82.281382,19.459902,0.0,54.174391,1.440268,5.5953 +4,10.573593,10.671598,10.658784,0.0,0.0,0.0,0.0 +5,68.732564,75.718126,11.482929,0.0,57.710795,0.0,4.461689 +6,67.063594,79.953919,16.75612,0.0,57.598923,0.0,3.527187 +7,81.466063,94.04458,21.343457,0.0,57.409246,3.971474,9.403474 +8,81.234747,98.155476,28.256603,0.0,57.70823,5.705006,5.319569 diff --git a/bv-evaluation/raw-data/bvw8_ch2_2AdditionAndLogicalOps_proved_data.csv b/bv-evaluation/raw-data/bvw8_ch2_2AdditionAndLogicalOps_proved_data.csv index d5084dee8..392c0419a 100644 --- a/bv-evaluation/raw-data/bvw8_ch2_2AdditionAndLogicalOps_proved_data.csv +++ b/bv-evaluation/raw-data/bvw8_ch2_2AdditionAndLogicalOps_proved_data.csv @@ -1,23 +1,23 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-bb,leanSAT-sat,leanSAT-lrat-t,leanSAT-lrat-c -0,8.870691,8.266271,8.252744,0.0,0.0,0.0,0.0 -1,80.961112,85.343412,19.912889,0.0,54.936207,1.7858,7.09558 -2,10.760708,10.554488,10.542907,0.0,0.0,0.0,0.0 -3,7.375549,7.44972,7.438819,0.0,0.0,0.0,0.0 -4,9.842365,10.067228,10.056569,0.0,0.0,0.0,0.0 -5,79.332929,101.928912,23.233998,0.0,55.93903,9.064497,11.809809 -6,77.670341,93.363126,24.180083,0.0,55.809966,2.499537,8.766003 -7,74.59638,80.082493,16.169344,0.0,54.117472,2.00314,6.200842 -8,84.873965,112.061566,28.952038,0.0,54.107442,14.89475,12.374123 -9,80.904425,101.943448,26.320913,0.0,55.689459,8.333276,9.760069 -10,91.970469,115.971445,39.566711,0.0,55.210424,9.918439,9.474281 -11,90.022573,106.239086,32.920318,0.0,55.586514,8.988835,7.478374 -12,89.868822,137.336302,45.785516,0.0,54.981372,19.088455,15.612103 -13,81.311143,93.088457,24.049916,0.0,53.626084,4.03215,9.592535 -14,81.307576,91.75915,28.976936,0.0,54.209144,2.720154,4.701823 -15,79.620101,90.383794,26.409951,0.0,54.066987,3.619812,5.121364 -16,87.870932,110.766701,30.178434,0.0,54.087564,14.552894,10.664448 -17,78.923958,96.124065,27.802318,0.0,53.870314,6.776589,6.415547 -18,83.628224,99.001508,28.21652,0.0,55.646817,3.584835,9.736005 -19,75.681808,78.745081,17.943002,0.0,55.587869,0.0,2.683234 -20,73.099212,78.65476,15.441361,0.0,55.855773,0.0,4.873217 -21,80.18146,93.035929,22.080361,0.0,55.485252,3.935046,9.779847 +0,8.34603,7.55156,7.536722,0.0,0.0,0.0,0.0 +1,83.211708,94.883061,26.572774,0.0,60.706089,1.729925,4.750354 +2,9.93587,9.977849,9.966157,0.0,0.0,0.0,0.0 +3,7.128121,7.412798,7.402509,0.0,0.0,0.0,0.0 +4,9.812648,9.802658,9.791307,0.0,0.0,0.0,0.0 +5,85.145798,109.213565,26.225158,0.0,60.447359,8.873145,11.898062 +6,82.264219,94.004432,20.521105,0.0,59.965269,2.334645,9.143002 +7,78.510536,85.692929,15.973123,0.0,60.316462,1.783576,5.986247 +8,88.651372,116.088688,29.729842,0.0,59.827068,14.960712,9.958943 +9,86.65258,112.677551,30.606357,0.0,60.418134,8.38383,11.39807 +10,96.358807,115.240958,36.847744,0.0,60.504466,8.453542,7.671957 +11,93.268713,119.098268,30.828646,0.0,60.374591,10.30104,15.62196 +12,95.881175,135.774427,33.2206,0.0,60.311693,24.869931,15.597284 +13,86.340641,102.07843,32.953065,0.0,60.425417,3.599714,4.005328 +14,84.472978,94.018049,21.97075,0.0,60.413746,2.675027,7.277774 +15,84.023238,100.528446,26.170486,0.0,60.51083,3.475007,8.697503 +16,92.408202,125.433953,29.922897,0.0,60.634913,16.639249,16.272446 +17,82.748154,99.772878,20.977766,0.0,59.668929,6.831582,10.574686 +18,91.318966,99.123524,27.504644,0.0,59.620769,3.603561,6.599153 +19,79.505133,82.835847,17.661237,0.0,59.698656,0.0,2.944927 +20,77.626958,88.95691,21.825356,0.0,60.183922,0.0,4.564563 +21,82.590504,94.71263,26.424295,0.0,60.155629,3.006844,4.132077 diff --git a/bv-evaluation/raw-data/bvw8_ch2_3LogicalArithmeticIneq_ceg_data.csv b/bv-evaluation/raw-data/bvw8_ch2_3LogicalArithmeticIneq_ceg_data.csv index c72d1606a..424b31657 100644 --- a/bv-evaluation/raw-data/bvw8_ch2_3LogicalArithmeticIneq_ceg_data.csv +++ b/bv-evaluation/raw-data/bvw8_ch2_3LogicalArithmeticIneq_ceg_data.csv @@ -1,43 +1,43 @@ ,bitwuzla,leanSAT,leanSAT-rw,leanSAT-sat -0,67.815801,68.011691,68.011691,68.011691 -1,67.649427,68.011691,68.011691,68.011691 -2,96.62692,68.011691,68.011691,68.011691 -3,101.167892,68.011691,68.011691,68.011691 -4,84.750169,68.011691,68.011691,68.011691 -5,86.157595,68.011691,68.011691,68.011691 -6,82.319392,68.011691,68.011691,68.011691 -7,85.572261,68.011691,68.011691,68.011691 -8,87.202037,68.011691,68.011691,68.011691 -9,84.989381,68.011691,68.011691,68.011691 -10,89.464636,68.011691,68.011691,68.011691 -11,83.901717,68.011691,68.011691,68.011691 -12,71.661077,68.011691,68.011691,68.011691 -13,72.094345,68.011691,68.011691,68.011691 -14,75.035575,68.011691,68.011691,68.011691 -15,83.852735,68.011691,68.011691,68.011691 -16,73.73034,68.011691,68.011691,68.011691 -17,100.819284,68.011691,68.011691,68.011691 -18,80.320529,68.011691,68.011691,68.011691 -19,70.949514,68.011691,68.011691,68.011691 -20,78.252587,68.011691,68.011691,68.011691 -21,70.384137,68.011691,68.011691,68.011691 -22,77.460192,68.011691,68.011691,68.011691 -23,79.739511,68.011691,68.011691,68.011691 -24,70.57664,68.011691,68.011691,68.011691 -25,70.437058,68.011691,68.011691,68.011691 -26,81.871826,68.011691,68.011691,68.011691 -27,89.359617,68.011691,68.011691,68.011691 -28,87.038898,68.011691,68.011691,68.011691 -29,88.84169,68.011691,68.011691,68.011691 -30,91.683483,68.011691,68.011691,68.011691 -31,83.248054,68.011691,68.011691,68.011691 -32,88.934274,68.011691,68.011691,68.011691 -33,88.500886,68.011691,68.011691,68.011691 -34,95.601346,68.011691,68.011691,68.011691 -35,85.797455,68.011691,68.011691,68.011691 -36,87.265486,68.011691,68.011691,68.011691 -37,96.16091,68.011691,68.011691,68.011691 -38,97.37867,68.011691,68.011691,68.011691 -39,72.47359,68.011691,68.011691,68.011691 -40,66.402452,68.011691,68.011691,68.011691 -41,68.011691,68.011691,68.011691,68.011691 +0,71.193328,75.01543,75.01543,75.01543 +1,70.301574,75.01543,75.01543,75.01543 +2,97.465887,75.01543,75.01543,75.01543 +3,102.302103,75.01543,75.01543,75.01543 +4,87.177471,75.01543,75.01543,75.01543 +5,89.177635,75.01543,75.01543,75.01543 +6,84.625084,75.01543,75.01543,75.01543 +7,82.297542,75.01543,75.01543,75.01543 +8,92.026061,75.01543,75.01543,75.01543 +9,87.70188,75.01543,75.01543,75.01543 +10,92.034616,75.01543,75.01543,75.01543 +11,88.320436,75.01543,75.01543,75.01543 +12,77.279392,75.01543,75.01543,75.01543 +13,76.938148,75.01543,75.01543,75.01543 +14,81.182437,75.01543,75.01543,75.01543 +15,82.31705,75.01543,75.01543,75.01543 +16,78.69882,75.01543,75.01543,75.01543 +17,103.740396,75.01543,75.01543,75.01543 +18,74.763134,75.01543,75.01543,75.01543 +19,76.183745,75.01543,75.01543,75.01543 +20,82.020428,75.01543,75.01543,75.01543 +21,76.414892,75.01543,75.01543,75.01543 +22,82.141517,75.01543,75.01543,75.01543 +23,85.276313,75.01543,75.01543,75.01543 +24,75.904608,75.01543,75.01543,75.01543 +25,76.099866,75.01543,75.01543,75.01543 +26,86.37743,75.01543,75.01543,75.01543 +27,93.38658,75.01543,75.01543,75.01543 +28,91.597522,75.01543,75.01543,75.01543 +29,93.090459,75.01543,75.01543,75.01543 +30,95.47061,75.01543,75.01543,75.01543 +31,88.325787,75.01543,75.01543,75.01543 +32,94.642318,75.01543,75.01543,75.01543 +33,93.218352,75.01543,75.01543,75.01543 +34,99.682992,75.01543,75.01543,75.01543 +35,89.529618,75.01543,75.01543,75.01543 +36,90.551198,75.01543,75.01543,75.01543 +37,100.897691,75.01543,75.01543,75.01543 +38,101.46912,75.01543,75.01543,75.01543 +39,73.948859,75.01543,75.01543,75.01543 +40,74.418103,75.01543,75.01543,75.01543 +41,75.01543,75.01543,75.01543,75.01543