no more changes (hopefully). Starting to upload final data.

uclid-org · Oct 15, 2020 · 8f227f4 · 8f227f4
1 parent e207fc1
commit 8f227f4
Show file tree

Hide file tree

Showing 129 changed files with 1,206,136 additions and 1,725,505 deletions.
diff --git a/bin/medley b/bin/medley
@@ -177,8 +177,7 @@ def main():
     if not args.output.endswith(".csv"):
         global_parser.error("The output file needs to be a csv file.")
 
-    if args.seed:
-        np.random.seed(args.seed)
+    np.random.seed(args.seed)
 
     problems = glob.glob(args.input + "/**.smt2", recursive=True)
     problems = sorted([p for p in problems if p.endswith(".smt2")])

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/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/bv.csv b/data/bv.csv
diff --git a/data/combined.csv b/data/combined.csv
@@ -2,31 +2,46 @@ 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
+MLP_bow_binary_expo_1.csv,21193.405126571655,1746
+MLP_bow_binary_expo_2.csv,17507.96491599083,1750
+MLP_bow_bump_expo_1.csv,21193.405126571655,1746
+MLP_bow_bump_expo_2.csv,17506.551240205765,1750
+MLP_probes_binary_expo_1.csv,21549.243874788284,1727
+MLP_probes_binary_expo_2.csv,19182.199524641037,1710
+MLP_probes_bump_expo_1.csv,21549.243874788284,1727
+MLP_probes_bump_expo_2.csv,19182.199524641037,1710
 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
+exp3a_bow_binary_expo_1.csv,25345.651545524597,1703
+exp3a_bow_binary_expo_2.csv,27453.63470363617,1671
+exp3a_bow_bump_expo_1.csv,27345.739029169083,1676
+exp3a_bow_bump_expo_2.csv,26174.77661538124,1705
+exp3a_probes_binary_expo_1.csv,25345.651545524597,1703
+exp3a_probes_binary_expo_2.csv,27453.63470363617,1671
+exp3a_probes_bump_expo_1.csv,27345.739029169083,1676
+exp3a_probes_bump_expo_2.csv,26174.77661538124,1705
+knearest_bow_binary_expo_1.csv,14322.840412139893,1813
+knearest_bow_binary_expo_2.csv,14669.279951095581,1811
+knearest_bow_bump_expo_1.csv,14322.840412139893,1813
+knearest_bow_bump_expo_2.csv,14669.279951095581,1811
+knearest_probes_binary_expo_1.csv,12711.868203878403,1834
+knearest_probes_binary_expo_2.csv,13079.922970294952,1824
+knearest_probes_bump_expo_1.csv,12711.868203878403,1834
+knearest_probes_bump_expo_2.csv,13079.922970294952,1824
+linear_bow_binary_expo_1.csv,27073.872908115387,1596
+linear_bow_binary_expo_2.csv,27404.57997059822,1586
+linear_bow_bump_expo_1.csv,27073.872908115387,1596
+linear_bow_bump_expo_2.csv,27404.57997059822,1586
+linear_probes_binary_expo_1.csv,27073.872908115387,1596
+linear_probes_binary_expo_2.csv,27404.57997059822,1586
+linear_probes_bump_expo_1.csv,27073.872908115387,1596
+linear_probes_bump_expo_2.csv,27404.57997059822,1586
+thompson_bow_binary_expo_1.csv,22361.841480970383,1709
+thompson_bow_binary_expo_2.csv,18590.749752044678,1758
+thompson_bow_bump_expo_1.csv,22361.841480970383,1709
+thompson_bow_bump_expo_2.csv,18590.749752044678,1758
+thompson_probes_binary_expo_1.csv,22361.841480970383,1709
+thompson_probes_binary_expo_2.csv,18590.749752044678,1758
+thompson_probes_bump_expo_1.csv,22361.841480970383,1709
+thompson_probes_bump_expo_2.csv,18590.749752044678,1758