refactor: Move succesful eval to test suite

leanprover · Jul 16, 2024 · 37285a4 · 37285a4
1 parent 28e7d68
commit 37285a4
Show file tree

Hide file tree

Showing 78 changed files with 76 additions and 78 deletions.
diff --git a/Eval/success.txt b/Eval/success.txt
diff --git a/Test.lean b/Test.lean
@@ -3,3 +3,4 @@ import Test.LRAT
 import Test.LRATChecker
 import Test.AIG
 import Test.Bv
+import Test.Eval
diff --git a/Test/Eval.lean b/Test/Eval.lean
@@ -0,0 +1,74 @@
+import Test.Eval.Popcount
+import Test.Eval.WillOverflow
+import Test.Eval.bitvec_152
+import Test.Eval.bitvec_229
+import Test.Eval.bitvec_239
+import Test.Eval.bitvec_283
+import Test.Eval.bitvec_AddSub_1043
+import Test.Eval.bitvec_AddSub_1152
+import Test.Eval.bitvec_AddSub_1156
+import Test.Eval.bitvec_AddSub_1164
+import Test.Eval.bitvec_AddSub_1165
+import Test.Eval.bitvec_AddSub_1176
+import Test.Eval.bitvec_AddSub_1202
+import Test.Eval.bitvec_AddSub_1295
+import Test.Eval.bitvec_AddSub_1309
+import Test.Eval.bitvec_AddSub_1539
+import Test.Eval.bitvec_AddSub_1539_2
+import Test.Eval.bitvec_AddSub_1556
+import Test.Eval.bitvec_AddSub_1560
+import Test.Eval.bitvec_AddSub_1564
+import Test.Eval.bitvec_AddSub_1574
+import Test.Eval.bitvec_AddSub_1614
+import Test.Eval.bitvec_AddSub_1619
+import Test.Eval.bitvec_AddSub_1624
+import Test.Eval.bitvec_AndOrXor_1230__A__B___A__B
+import Test.Eval.bitvec_AndOrXor_1241_AB__AB__AB
+import Test.Eval.bitvec_AndOrXor_1247_AB__AB__AB
+import Test.Eval.bitvec_AndOrXor_1253_A__AB___A__B
+import Test.Eval.bitvec_AndOrXor_1280_ABA___AB
+import Test.Eval.bitvec_AndOrXor_1288_A__B__B__C__A___A__B__C
+import Test.Eval.bitvec_AndOrXor_1294_A__B__A__B___A__B
+import Test.Eval.bitvec_AndOrXor_135
+import Test.Eval.bitvec_AndOrXor_144
+import Test.Eval.bitvec_AndOrXor_1683_1
+import Test.Eval.bitvec_AndOrXor_1683_2
+import Test.Eval.bitvec_AndOrXor_1704
+import Test.Eval.bitvec_AndOrXor_1705
+import Test.Eval.bitvec_AndOrXor_1733
+import Test.Eval.bitvec_AndOrXor_2063__X__C1__C2____X__C2__C1__C2
+import Test.Eval.bitvec_AndOrXor_2113___A__B__A___A__B
+import Test.Eval.bitvec_AndOrXor_2118___A__B__A___A__B
+import Test.Eval.bitvec_AndOrXor_2123___A__B__A__B___A__B
+import Test.Eval.bitvec_AndOrXor_2188
+import Test.Eval.bitvec_AndOrXor_2231__A__B__B__C__A___A__B__C
+import Test.Eval.bitvec_AndOrXor_2243__B__C__A__B___B__A__C
+import Test.Eval.bitvec_AndOrXor_2247__A__B__A__B
+import Test.Eval.bitvec_AndOrXor_2263
+import Test.Eval.bitvec_AndOrXor_2264
+import Test.Eval.bitvec_AndOrXor_2265
+import Test.Eval.bitvec_AndOrXor_2284
+import Test.Eval.bitvec_AndOrXor_2285
+import Test.Eval.bitvec_AndOrXor_2297
+import Test.Eval.bitvec_AndOrXor_2367
+import Test.Eval.bitvec_AndOrXor_2416
+import Test.Eval.bitvec_AndOrXor_2417
+import Test.Eval.bitvec_AndOrXor_2429
+import Test.Eval.bitvec_AndOrXor_2430
+import Test.Eval.bitvec_AndOrXor_2475
+import Test.Eval.bitvec_AndOrXor_2486
+import Test.Eval.bitvec_AndOrXor_2581__BAB___A__B
+import Test.Eval.bitvec_AndOrXor_2587__BAA___B__A
+import Test.Eval.bitvec_AndOrXor_2595
+import Test.Eval.bitvec_AndOrXor_2607
+import Test.Eval.bitvec_AndOrXor_2617
+import Test.Eval.bitvec_AndOrXor_2627
+import Test.Eval.bitvec_AndOrXor_2647
+import Test.Eval.bitvec_AndOrXor_2658
+import Test.Eval.bitvec_AndOrXor_2663
+import Test.Eval.bitvec_AndOrXor_698
+import Test.Eval.bitvec_AndOrXor_709
+import Test.Eval.bitvec_AndOrXor_716
+import Test.Eval.bitvec_AndOrXor_794
+import Test.Eval.bitvec_AndOrXor_827
+import Test.Eval.bitvec_AndOrXor_887_2
diff --git a/Eval/Popcount.lean → Test/Eval/Popcount.lean b/Eval/Popcount.lean → Test/Eval/Popcount.lean
diff --git a/Eval/WillOverflow.lean → Test/Eval/WillOverflow.lean b/Eval/WillOverflow.lean → Test/Eval/WillOverflow.lean
diff --git a/Eval/bitvec_152.lean → Test/Eval/bitvec_152.lean b/Eval/bitvec_152.lean → Test/Eval/bitvec_152.lean
diff --git a/Eval/bitvec_229.lean → Test/Eval/bitvec_229.lean b/Eval/bitvec_229.lean → Test/Eval/bitvec_229.lean
diff --git a/Eval/bitvec_239.lean → Test/Eval/bitvec_239.lean b/Eval/bitvec_239.lean → Test/Eval/bitvec_239.lean
diff --git a/Eval/bitvec_283.lean → Test/Eval/bitvec_283.lean b/Eval/bitvec_283.lean → Test/Eval/bitvec_283.lean
diff --git a/Eval/bitvec_AddSub_1043.lean → Test/Eval/bitvec_AddSub_1043.lean b/Eval/bitvec_AddSub_1043.lean → Test/Eval/bitvec_AddSub_1043.lean
diff --git a/Eval/bitvec_AddSub_1152.lean → Test/Eval/bitvec_AddSub_1152.lean b/Eval/bitvec_AddSub_1152.lean → Test/Eval/bitvec_AddSub_1152.lean
diff --git a/Eval/bitvec_AddSub_1156.lean → Test/Eval/bitvec_AddSub_1156.lean b/Eval/bitvec_AddSub_1156.lean → Test/Eval/bitvec_AddSub_1156.lean
diff --git a/Eval/bitvec_AddSub_1164.lean → Test/Eval/bitvec_AddSub_1164.lean b/Eval/bitvec_AddSub_1164.lean → Test/Eval/bitvec_AddSub_1164.lean
diff --git a/Eval/bitvec_AddSub_1165.lean → Test/Eval/bitvec_AddSub_1165.lean b/Eval/bitvec_AddSub_1165.lean → Test/Eval/bitvec_AddSub_1165.lean
diff --git a/Eval/bitvec_AddSub_1176.lean → Test/Eval/bitvec_AddSub_1176.lean b/Eval/bitvec_AddSub_1176.lean → Test/Eval/bitvec_AddSub_1176.lean
diff --git a/Eval/bitvec_AddSub_1202.lean → Test/Eval/bitvec_AddSub_1202.lean b/Eval/bitvec_AddSub_1202.lean → Test/Eval/bitvec_AddSub_1202.lean
diff --git a/Eval/bitvec_AddSub_1295.lean → Test/Eval/bitvec_AddSub_1295.lean b/Eval/bitvec_AddSub_1295.lean → Test/Eval/bitvec_AddSub_1295.lean
diff --git a/Eval/bitvec_AddSub_1309.lean → Test/Eval/bitvec_AddSub_1309.lean b/Eval/bitvec_AddSub_1309.lean → Test/Eval/bitvec_AddSub_1309.lean
diff --git a/Eval/bitvec_AddSub_1539.lean → Test/Eval/bitvec_AddSub_1539.lean b/Eval/bitvec_AddSub_1539.lean → Test/Eval/bitvec_AddSub_1539.lean
diff --git a/Eval/bitvec_AddSub_1539_2.lean → Test/Eval/bitvec_AddSub_1539_2.lean b/Eval/bitvec_AddSub_1539_2.lean → Test/Eval/bitvec_AddSub_1539_2.lean
diff --git a/Eval/bitvec_AddSub_1556.lean → Test/Eval/bitvec_AddSub_1556.lean b/Eval/bitvec_AddSub_1556.lean → Test/Eval/bitvec_AddSub_1556.lean
diff --git a/Eval/bitvec_AddSub_1560.lean → Test/Eval/bitvec_AddSub_1560.lean b/Eval/bitvec_AddSub_1560.lean → Test/Eval/bitvec_AddSub_1560.lean
diff --git a/Eval/bitvec_AddSub_1564.lean → Test/Eval/bitvec_AddSub_1564.lean b/Eval/bitvec_AddSub_1564.lean → Test/Eval/bitvec_AddSub_1564.lean
diff --git a/Eval/bitvec_AddSub_1574.lean → Test/Eval/bitvec_AddSub_1574.lean b/Eval/bitvec_AddSub_1574.lean → Test/Eval/bitvec_AddSub_1574.lean
diff --git a/Eval/bitvec_AddSub_1614.lean → Test/Eval/bitvec_AddSub_1614.lean b/Eval/bitvec_AddSub_1614.lean → Test/Eval/bitvec_AddSub_1614.lean
diff --git a/Eval/bitvec_AddSub_1619.lean → Test/Eval/bitvec_AddSub_1619.lean b/Eval/bitvec_AddSub_1619.lean → Test/Eval/bitvec_AddSub_1619.lean
diff --git a/Eval/bitvec_AddSub_1624.lean → Test/Eval/bitvec_AddSub_1624.lean b/Eval/bitvec_AddSub_1624.lean → Test/Eval/bitvec_AddSub_1624.lean
diff --git a/Eval/bitvec_AndOrXor_1230__A__B___A__B.lean → ...al/bitvec_AndOrXor_1230__A__B___A__B.lean b/Eval/bitvec_AndOrXor_1230__A__B___A__B.lean → ...al/bitvec_AndOrXor_1230__A__B___A__B.lean
diff --git a/Eval/bitvec_AndOrXor_1241_AB__AB__AB.lean → ...Eval/bitvec_AndOrXor_1241_AB__AB__AB.lean b/Eval/bitvec_AndOrXor_1241_AB__AB__AB.lean → ...Eval/bitvec_AndOrXor_1241_AB__AB__AB.lean
diff --git a/Eval/bitvec_AndOrXor_1247_AB__AB__AB.lean → ...Eval/bitvec_AndOrXor_1247_AB__AB__AB.lean b/Eval/bitvec_AndOrXor_1247_AB__AB__AB.lean → ...Eval/bitvec_AndOrXor_1247_AB__AB__AB.lean
diff --git a/Eval/bitvec_AndOrXor_1253_A__AB___A__B.lean → ...al/bitvec_AndOrXor_1253_A__AB___A__B.lean b/Eval/bitvec_AndOrXor_1253_A__AB___A__B.lean → ...al/bitvec_AndOrXor_1253_A__AB___A__B.lean
diff --git a/Eval/bitvec_AndOrXor_1280_ABA___AB.lean → Test/Eval/bitvec_AndOrXor_1280_ABA___AB.lean b/Eval/bitvec_AndOrXor_1280_ABA___AB.lean → Test/Eval/bitvec_AndOrXor_1280_ABA___AB.lean
diff --git a/...ndOrXor_1288_A__B__B__C__A___A__B__C.lean → ...ndOrXor_1288_A__B__B__C__A___A__B__C.lean b/...ndOrXor_1288_A__B__B__C__A___A__B__C.lean → ...ndOrXor_1288_A__B__B__C__A___A__B__C.lean
diff --git a/...tvec_AndOrXor_1294_A__B__A__B___A__B.lean → ...tvec_AndOrXor_1294_A__B__A__B___A__B.lean b/...tvec_AndOrXor_1294_A__B__A__B___A__B.lean → ...tvec_AndOrXor_1294_A__B__A__B___A__B.lean
diff --git a/Eval/bitvec_AndOrXor_135.lean → Test/Eval/bitvec_AndOrXor_135.lean b/Eval/bitvec_AndOrXor_135.lean → Test/Eval/bitvec_AndOrXor_135.lean
diff --git a/Eval/bitvec_AndOrXor_144.lean → Test/Eval/bitvec_AndOrXor_144.lean b/Eval/bitvec_AndOrXor_144.lean → Test/Eval/bitvec_AndOrXor_144.lean
diff --git a/Eval/bitvec_AndOrXor_1683_1.lean → Test/Eval/bitvec_AndOrXor_1683_1.lean b/Eval/bitvec_AndOrXor_1683_1.lean → Test/Eval/bitvec_AndOrXor_1683_1.lean
diff --git a/Eval/bitvec_AndOrXor_1683_2.lean → Test/Eval/bitvec_AndOrXor_1683_2.lean b/Eval/bitvec_AndOrXor_1683_2.lean → Test/Eval/bitvec_AndOrXor_1683_2.lean
diff --git a/Eval/bitvec_AndOrXor_1704.lean → Test/Eval/bitvec_AndOrXor_1704.lean b/Eval/bitvec_AndOrXor_1704.lean → Test/Eval/bitvec_AndOrXor_1704.lean
diff --git a/Eval/bitvec_AndOrXor_1705.lean → Test/Eval/bitvec_AndOrXor_1705.lean b/Eval/bitvec_AndOrXor_1705.lean → Test/Eval/bitvec_AndOrXor_1705.lean
diff --git a/Eval/bitvec_AndOrXor_1733.lean → Test/Eval/bitvec_AndOrXor_1733.lean b/Eval/bitvec_AndOrXor_1733.lean → Test/Eval/bitvec_AndOrXor_1733.lean
diff --git a/...Xor_2063__X__C1__C2____X__C2__C1__C2.lean → ...Xor_2063__X__C1__C2____X__C2__C1__C2.lean b/...Xor_2063__X__C1__C2____X__C2__C1__C2.lean → ...Xor_2063__X__C1__C2____X__C2__C1__C2.lean
diff --git a/...itvec_AndOrXor_2113___A__B__A___A__B.lean → ...itvec_AndOrXor_2113___A__B__A___A__B.lean b/...itvec_AndOrXor_2113___A__B__A___A__B.lean → ...itvec_AndOrXor_2113___A__B__A___A__B.lean
diff --git a/...itvec_AndOrXor_2118___A__B__A___A__B.lean → ...itvec_AndOrXor_2118___A__B__A___A__B.lean b/...itvec_AndOrXor_2118___A__B__A___A__B.lean → ...itvec_AndOrXor_2118___A__B__A___A__B.lean
diff --git a/...ec_AndOrXor_2123___A__B__A__B___A__B.lean → ...ec_AndOrXor_2123___A__B__A__B___A__B.lean b/...ec_AndOrXor_2123___A__B__A__B___A__B.lean → ...ec_AndOrXor_2123___A__B__A__B___A__B.lean
diff --git a/Eval/bitvec_AndOrXor_2188.lean → Test/Eval/bitvec_AndOrXor_2188.lean b/Eval/bitvec_AndOrXor_2188.lean → Test/Eval/bitvec_AndOrXor_2188.lean
diff --git a/...dOrXor_2231__A__B__B__C__A___A__B__C.lean → ...dOrXor_2231__A__B__B__C__A___A__B__C.lean b/...dOrXor_2231__A__B__B__C__A___A__B__C.lean → ...dOrXor_2231__A__B__B__C__A___A__B__C.lean
diff --git a/..._AndOrXor_2243__B__C__A__B___B__A__C.lean → ..._AndOrXor_2243__B__C__A__B___B__A__C.lean b/..._AndOrXor_2243__B__C__A__B___B__A__C.lean → ..._AndOrXor_2243__B__C__A__B___B__A__C.lean
diff --git a/Eval/bitvec_AndOrXor_2247__A__B__A__B.lean → ...val/bitvec_AndOrXor_2247__A__B__A__B.lean b/Eval/bitvec_AndOrXor_2247__A__B__A__B.lean → ...val/bitvec_AndOrXor_2247__A__B__A__B.lean
diff --git a/Eval/bitvec_AndOrXor_2263.lean → Test/Eval/bitvec_AndOrXor_2263.lean b/Eval/bitvec_AndOrXor_2263.lean → Test/Eval/bitvec_AndOrXor_2263.lean
diff --git a/Eval/bitvec_AndOrXor_2264.lean → Test/Eval/bitvec_AndOrXor_2264.lean b/Eval/bitvec_AndOrXor_2264.lean → Test/Eval/bitvec_AndOrXor_2264.lean
diff --git a/Eval/bitvec_AndOrXor_2265.lean → Test/Eval/bitvec_AndOrXor_2265.lean b/Eval/bitvec_AndOrXor_2265.lean → Test/Eval/bitvec_AndOrXor_2265.lean
diff --git a/Eval/bitvec_AndOrXor_2284.lean → Test/Eval/bitvec_AndOrXor_2284.lean b/Eval/bitvec_AndOrXor_2284.lean → Test/Eval/bitvec_AndOrXor_2284.lean
diff --git a/Eval/bitvec_AndOrXor_2285.lean → Test/Eval/bitvec_AndOrXor_2285.lean b/Eval/bitvec_AndOrXor_2285.lean → Test/Eval/bitvec_AndOrXor_2285.lean
diff --git a/Eval/bitvec_AndOrXor_2297.lean → Test/Eval/bitvec_AndOrXor_2297.lean b/Eval/bitvec_AndOrXor_2297.lean → Test/Eval/bitvec_AndOrXor_2297.lean
diff --git a/Eval/bitvec_AndOrXor_2367.lean → Test/Eval/bitvec_AndOrXor_2367.lean b/Eval/bitvec_AndOrXor_2367.lean → Test/Eval/bitvec_AndOrXor_2367.lean
diff --git a/Eval/bitvec_AndOrXor_2416.lean → Test/Eval/bitvec_AndOrXor_2416.lean b/Eval/bitvec_AndOrXor_2416.lean → Test/Eval/bitvec_AndOrXor_2416.lean
diff --git a/Eval/bitvec_AndOrXor_2417.lean → Test/Eval/bitvec_AndOrXor_2417.lean b/Eval/bitvec_AndOrXor_2417.lean → Test/Eval/bitvec_AndOrXor_2417.lean
diff --git a/Eval/bitvec_AndOrXor_2429.lean → Test/Eval/bitvec_AndOrXor_2429.lean b/Eval/bitvec_AndOrXor_2429.lean → Test/Eval/bitvec_AndOrXor_2429.lean
diff --git a/Eval/bitvec_AndOrXor_2430.lean → Test/Eval/bitvec_AndOrXor_2430.lean b/Eval/bitvec_AndOrXor_2430.lean → Test/Eval/bitvec_AndOrXor_2430.lean
diff --git a/Eval/bitvec_AndOrXor_2475.lean → Test/Eval/bitvec_AndOrXor_2475.lean b/Eval/bitvec_AndOrXor_2475.lean → Test/Eval/bitvec_AndOrXor_2475.lean
diff --git a/Eval/bitvec_AndOrXor_2486.lean → Test/Eval/bitvec_AndOrXor_2486.lean b/Eval/bitvec_AndOrXor_2486.lean → Test/Eval/bitvec_AndOrXor_2486.lean
diff --git a/Eval/bitvec_AndOrXor_2581__BAB___A__B.lean → ...val/bitvec_AndOrXor_2581__BAB___A__B.lean b/Eval/bitvec_AndOrXor_2581__BAB___A__B.lean → ...val/bitvec_AndOrXor_2581__BAB___A__B.lean
diff --git a/Eval/bitvec_AndOrXor_2587__BAA___B__A.lean → ...val/bitvec_AndOrXor_2587__BAA___B__A.lean b/Eval/bitvec_AndOrXor_2587__BAA___B__A.lean → ...val/bitvec_AndOrXor_2587__BAA___B__A.lean
diff --git a/Eval/bitvec_AndOrXor_2595.lean → Test/Eval/bitvec_AndOrXor_2595.lean b/Eval/bitvec_AndOrXor_2595.lean → Test/Eval/bitvec_AndOrXor_2595.lean
diff --git a/Eval/bitvec_AndOrXor_2607.lean → Test/Eval/bitvec_AndOrXor_2607.lean b/Eval/bitvec_AndOrXor_2607.lean → Test/Eval/bitvec_AndOrXor_2607.lean
diff --git a/Eval/bitvec_AndOrXor_2617.lean → Test/Eval/bitvec_AndOrXor_2617.lean b/Eval/bitvec_AndOrXor_2617.lean → Test/Eval/bitvec_AndOrXor_2617.lean
diff --git a/Eval/bitvec_AndOrXor_2627.lean → Test/Eval/bitvec_AndOrXor_2627.lean b/Eval/bitvec_AndOrXor_2627.lean → Test/Eval/bitvec_AndOrXor_2627.lean
diff --git a/Eval/bitvec_AndOrXor_2647.lean → Test/Eval/bitvec_AndOrXor_2647.lean b/Eval/bitvec_AndOrXor_2647.lean → Test/Eval/bitvec_AndOrXor_2647.lean
diff --git a/Eval/bitvec_AndOrXor_2658.lean → Test/Eval/bitvec_AndOrXor_2658.lean b/Eval/bitvec_AndOrXor_2658.lean → Test/Eval/bitvec_AndOrXor_2658.lean
diff --git a/Eval/bitvec_AndOrXor_2663.lean → Test/Eval/bitvec_AndOrXor_2663.lean b/Eval/bitvec_AndOrXor_2663.lean → Test/Eval/bitvec_AndOrXor_2663.lean
diff --git a/Eval/bitvec_AndOrXor_698.lean → Test/Eval/bitvec_AndOrXor_698.lean b/Eval/bitvec_AndOrXor_698.lean → Test/Eval/bitvec_AndOrXor_698.lean
diff --git a/Eval/bitvec_AndOrXor_709.lean → Test/Eval/bitvec_AndOrXor_709.lean b/Eval/bitvec_AndOrXor_709.lean → Test/Eval/bitvec_AndOrXor_709.lean
diff --git a/Eval/bitvec_AndOrXor_716.lean → Test/Eval/bitvec_AndOrXor_716.lean b/Eval/bitvec_AndOrXor_716.lean → Test/Eval/bitvec_AndOrXor_716.lean
diff --git a/Eval/bitvec_AndOrXor_794.lean → Test/Eval/bitvec_AndOrXor_794.lean b/Eval/bitvec_AndOrXor_794.lean → Test/Eval/bitvec_AndOrXor_794.lean
diff --git a/Eval/bitvec_AndOrXor_827.lean → Test/Eval/bitvec_AndOrXor_827.lean b/Eval/bitvec_AndOrXor_827.lean → Test/Eval/bitvec_AndOrXor_827.lean
diff --git a/Eval/bitvec_AndOrXor_887_2.lean → Test/Eval/bitvec_AndOrXor_887_2.lean b/Eval/bitvec_AndOrXor_887_2.lean → Test/Eval/bitvec_AndOrXor_887_2.lean
diff --git a/check_eval.bash b/check_eval.bash
@@ -24,8 +24,5 @@ for path in $(find "${LIB}" -type f  -name "*.lean" | sort); do
     fi
 done
 
-# Compare with checked in results within [success|fail].txt
-diff -u "${LIB}/success.txt" $RUN_SUCCESSES
-ret1=$?
 diff -u "${LIB}/fail.txt" $RUN_FAILS
-exit $(($ret1 | $?))
+exit $?