move scripts to folder, add combined dataset, fix bugs in timers and …

…classifiers
uclid-org · Oct 15, 2020 · e207fc1 · e207fc1
1 parent 5f5d30e
commit e207fc1
Show file tree

Hide file tree

Showing 135 changed files with 1,959,989 additions and 11 deletions.
diff --git a/data/BV/Bitwuzla.csv b/data/BV/Bitwuzla.csv
diff --git a/data/BV/CVC4.csv b/data/BV/CVC4.csv
diff --git a/data/BV/MLP_both_bump_20_nearest_0.csv b/data/BV/MLP_both_bump_20_nearest_0.csv
diff --git a/data/BV/MLP_both_bump_const_0.csv b/data/BV/MLP_both_bump_const_0.csv
diff --git a/data/BV/MLP_both_bump_expo_0.csv b/data/BV/MLP_both_bump_expo_0.csv
diff --git a/data/BV/MLP_both_bump_perfect_0.csv b/data/BV/MLP_both_bump_perfect_0.csv
diff --git a/data/BV/MLP_both_bump_sdg_0.csv b/data/BV/MLP_both_bump_sdg_0.csv
diff --git a/data/BV/MathSAT.csv b/data/BV/MathSAT.csv
diff --git a/data/BV/YICES.csv b/data/BV/YICES.csv
diff --git a/data/BV/Z3.csv b/data/BV/Z3.csv
diff --git a/data/BV/exp3a_both_bump_20_nearest_0.csv b/data/BV/exp3a_both_bump_20_nearest_0.csv
diff --git a/data/BV/exp3a_both_bump_const_0.csv b/data/BV/exp3a_both_bump_const_0.csv
diff --git a/data/BV/exp3a_both_bump_expo_0.csv b/data/BV/exp3a_both_bump_expo_0.csv
diff --git a/data/BV/exp3a_both_bump_perfect_0.csv b/data/BV/exp3a_both_bump_perfect_0.csv
diff --git a/data/BV/exp3a_both_bump_sdg_0.csv b/data/BV/exp3a_both_bump_sdg_0.csv
diff --git a/data/BV/knearest_both_bump_20_nearest_0.csv b/data/BV/knearest_both_bump_20_nearest_0.csv
diff --git a/data/BV/knearest_both_bump_const_0.csv b/data/BV/knearest_both_bump_const_0.csv
diff --git a/data/BV/knearest_both_bump_expo_0.csv b/data/BV/knearest_both_bump_expo_0.csv
diff --git a/data/BV/knearest_both_bump_perfect_0.csv b/data/BV/knearest_both_bump_perfect_0.csv
diff --git a/data/BV/knearest_both_bump_sdg_0.csv b/data/BV/knearest_both_bump_sdg_0.csv
diff --git a/data/BV/linear_both_bump_20_nearest_0.csv b/data/BV/linear_both_bump_20_nearest_0.csv
diff --git a/data/BV/linear_both_bump_const_0.csv b/data/BV/linear_both_bump_const_0.csv
diff --git a/data/BV/linear_both_bump_expo_0.csv b/data/BV/linear_both_bump_expo_0.csv
diff --git a/data/BV/linear_both_bump_perfect_0.csv b/data/BV/linear_both_bump_perfect_0.csv
diff --git a/data/BV/linear_both_bump_sdg_0.csv b/data/BV/linear_both_bump_sdg_0.csv
diff --git a/data/BV/thompson_both_bump_20_nearest_0.csv b/data/BV/thompson_both_bump_20_nearest_0.csv
diff --git a/data/BV/thompson_both_bump_const_0.csv b/data/BV/thompson_both_bump_const_0.csv
diff --git a/data/BV/thompson_both_bump_expo_0.csv b/data/BV/thompson_both_bump_expo_0.csv
diff --git a/data/BV/thompson_both_bump_perfect_0.csv b/data/BV/thompson_both_bump_perfect_0.csv
diff --git a/data/BV/thompson_both_bump_sdg_0.csv b/data/BV/thompson_both_bump_sdg_0.csv
diff --git a/data/QF_ABV/BOOLECTOR.csv b/data/QF_ABV/BOOLECTOR.csv
diff --git a/data/QF_ABV/Bitwuzla.csv b/data/QF_ABV/Bitwuzla.csv
diff --git a/data/QF_ABV/CVC4.csv b/data/QF_ABV/CVC4.csv
diff --git a/data/QF_ABV/MathSAT.csv b/data/QF_ABV/MathSAT.csv
diff --git a/data/QF_ABV/YICES.csv b/data/QF_ABV/YICES.csv
diff --git a/data/QF_ABV/Z3.csv b/data/QF_ABV/Z3.csv
diff --git a/data/Sage2/BOOLECTOR.csv b/data/Sage2/BOOLECTOR.csv
diff --git a/data/Sage2/Bitwuzla.csv b/data/Sage2/Bitwuzla.csv
diff --git a/data/Sage2/CVC4.csv b/data/Sage2/CVC4.csv
diff --git a/data/Sage2/MathSAT.csv b/data/Sage2/MathSAT.csv
diff --git a/data/Sage2/YICES.csv b/data/Sage2/YICES.csv
diff --git a/data/Sage2/Z3.csv b/data/Sage2/Z3.csv
diff --git a/data/bv.csv b/data/bv.csv
@@ -0,0 +1,31 @@
+solver, total time, total solved
+Bitwuzla.csv,2132.088451385498,470
+CVC4.csv,1951.799156665802,476
+MLP_both_bump_20_nearest_0.csv,1426.4367904663086,488
+MLP_both_bump_const_0.csv,3590.9849066734314,442
+MLP_both_bump_expo_0.csv,1839.849244594574,481
+MLP_both_bump_perfect_0.csv,1379.5855858325958,492
+MLP_both_bump_sdg_0.csv,1777.3582065105438,414
+MathSAT.csv,214.84439992904663,405
+YICES.csv,3704.3572397232056,441
+Z3.csv,1508.5941886901855,476
+exp3a_both_bump_20_nearest_0.csv,1635.3121132850647,488
+exp3a_both_bump_const_0.csv,2187.4826426506042,449
+exp3a_both_bump_expo_0.csv,1706.939220905304,488
+exp3a_both_bump_perfect_0.csv,1718.9158220291138,492
+exp3a_both_bump_sdg_0.csv,1893.443407535553,451
+knearest_both_bump_20_nearest_0.csv,685.5414009094238,491
+knearest_both_bump_const_0.csv,3646.3979058265686,440
+knearest_both_bump_expo_0.csv,754.6313965320587,491
+knearest_both_bump_perfect_0.csv,1080.9781708717346,492
+knearest_both_bump_sdg_0.csv,215.41918969154358,404
+linear_both_bump_20_nearest_0.csv,1463.1399493217468,491
+linear_both_bump_const_0.csv,1800.3859157562256,377
+linear_both_bump_expo_0.csv,1883.7888672351837,484
+linear_both_bump_perfect_0.csv,1742.175933599472,492
+linear_both_bump_sdg_0.csv,1723.6534578800201,381
+thompson_both_bump_20_nearest_0.csv,1314.0283901691437,489
+thompson_both_bump_const_0.csv,1725.1051995754242,469
+thompson_both_bump_expo_0.csv,1351.3929171562195,486
+thompson_both_bump_perfect_0.csv,1990.9093935489655,492
+thompson_both_bump_sdg_0.csv,1888.557007074356,472
diff --git a/data/combined.csv b/data/combined.csv
@@ -0,0 +1,32 @@
+solver, total time, total solved
+BOOLECTOR.csv,18271.124001979828,756
+Bitwuzla.csv,15971.414064645767,1315
+CVC4.csv,37252.9752600193,1497
+MLP_both_bump_20_nearest_0.csv,24000.28667640686,1699
+MLP_bow_binary_20_nearest_0.csv,23666.175315380096,1690
+MLP_bow_bump_20_nearest_0.csv,25970.341287612915,1699
+MLP_probes_binary_20_nearest_0.csv,24285.87707233429,1697
+MLP_probes_bump_20_nearest_0.csv,23440.105539798737,1696
+MathSAT.csv,41766.19432759285,1195
+YICES.csv,12470.921966075897,1346
+Z3.csv,23649.47221469879,1675
+exp3a_both_bump_20_nearest_0.csv,24217.72628903389,1690
+exp3a_bow_binary_20_nearest_0.csv,24924.294432640076,1684
+exp3a_bow_bump_20_nearest_0.csv,26949.837604761124,1686
+exp3a_probes_binary_20_nearest_0.csv,25990.880749940872,1687
+exp3a_probes_bump_20_nearest_0.csv,23246.155936956406,1706
+knearest_both_bump_20_nearest_0.csv,19677.43110013008,1721
+knearest_bow_binary_20_nearest_0.csv,21720.859801054,1712
+knearest_bow_bump_20_nearest_0.csv,21241.43744826317,1713
+knearest_probes_binary_20_nearest_0.csv,18351.397936582565,1740
+knearest_probes_bump_20_nearest_0.csv,21766.65646648407,1751
+linear_both_bump_20_nearest_0.csv,26407.050674200058,1699
+linear_bow_binary_20_nearest_0.csv,27259.064215660095,1693
+linear_bow_bump_20_nearest_0.csv,26120.957041740417,1698
+linear_probes_binary_20_nearest_0.csv,27130.306678533554,1703
+linear_probes_bump_20_nearest_0.csv,25980.878583431244,1702
+thompson_both_bump_20_nearest_0.csv,23043.463824033737,1707
+thompson_bow_binary_20_nearest_0.csv,33487.47245287895,1682
+thompson_bow_bump_20_nearest_0.csv,23047.836333990097,1713
+thompson_probes_binary_20_nearest_0.csv,22301.159065485,1711
+thompson_probes_bump_20_nearest_0.csv,20532.167702913284,1719
diff --git a/data/combined/BOOLECTOR.csv b/data/combined/BOOLECTOR.csv
diff --git a/data/combined/Bitwuzla.csv b/data/combined/Bitwuzla.csv
diff --git a/data/combined/CVC4.csv b/data/combined/CVC4.csv
diff --git a/data/combined/MLP_both_bump_20_nearest_0.csv b/data/combined/MLP_both_bump_20_nearest_0.csv
diff --git a/data/combined/MLP_bow_binary_20_nearest_0.csv b/data/combined/MLP_bow_binary_20_nearest_0.csv
diff --git a/data/combined/MLP_bow_bump_20_nearest_0.csv b/data/combined/MLP_bow_bump_20_nearest_0.csv
diff --git a/data/combined/MLP_probes_binary_20_nearest_0.csv b/data/combined/MLP_probes_binary_20_nearest_0.csv
diff --git a/data/combined/MLP_probes_bump_20_nearest_0.csv b/data/combined/MLP_probes_bump_20_nearest_0.csv
diff --git a/data/combined/MathSAT.csv b/data/combined/MathSAT.csv
diff --git a/data/combined/YICES.csv b/data/combined/YICES.csv
diff --git a/data/combined/Z3.csv b/data/combined/Z3.csv
diff --git a/data/combined/exp3a_both_bump_20_nearest_0.csv b/data/combined/exp3a_both_bump_20_nearest_0.csv
diff --git a/data/combined/exp3a_bow_binary_20_nearest_0.csv b/data/combined/exp3a_bow_binary_20_nearest_0.csv
diff --git a/data/combined/exp3a_bow_bump_20_nearest_0.csv b/data/combined/exp3a_bow_bump_20_nearest_0.csv
diff --git a/data/combined/exp3a_probes_binary_20_nearest_0.csv b/data/combined/exp3a_probes_binary_20_nearest_0.csv
diff --git a/data/combined/exp3a_probes_bump_20_nearest_0.csv b/data/combined/exp3a_probes_bump_20_nearest_0.csv
diff --git a/data/combined/knearest_both_bump_20_nearest_0.csv b/data/combined/knearest_both_bump_20_nearest_0.csv
diff --git a/data/combined/knearest_bow_binary_20_nearest_0.csv b/data/combined/knearest_bow_binary_20_nearest_0.csv
diff --git a/data/combined/knearest_bow_bump_20_nearest_0.csv b/data/combined/knearest_bow_bump_20_nearest_0.csv
diff --git a/data/combined/knearest_probes_binary_20_nearest_0.csv b/data/combined/knearest_probes_binary_20_nearest_0.csv
diff --git a/data/combined/knearest_probes_bump_20_nearest_0.csv b/data/combined/knearest_probes_bump_20_nearest_0.csv
diff --git a/data/combined/linear_both_bump_20_nearest_0.csv b/data/combined/linear_both_bump_20_nearest_0.csv
diff --git a/data/combined/linear_bow_binary_20_nearest_0.csv b/data/combined/linear_bow_binary_20_nearest_0.csv
diff --git a/data/combined/linear_bow_bump_20_nearest_0.csv b/data/combined/linear_bow_bump_20_nearest_0.csv
diff --git a/data/combined/linear_probes_binary_20_nearest_0.csv b/data/combined/linear_probes_binary_20_nearest_0.csv
diff --git a/data/combined/linear_probes_bump_20_nearest_0.csv b/data/combined/linear_probes_bump_20_nearest_0.csv
diff --git a/data/combined/thompson_both_bump_20_nearest_0.csv b/data/combined/thompson_both_bump_20_nearest_0.csv