diff --git a/Eval/Popcount.lean b/Eval/Popcount.lean index f5726509..f1afdb08 100644 --- a/Eval/Popcount.lean +++ b/Eval/Popcount.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide /- This is based on: https://saw.galois.com/intro/IntroToSAW.html#the-code diff --git a/Eval/WillOverflow.lean b/Eval/WillOverflow.lean index 977d1703..9dd9de21 100644 --- a/Eval/WillOverflow.lean +++ b/Eval/WillOverflow.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide /- This file is based on: https://grack.com/blog/2022/12/20/deriving-a-bit-twiddling-hack/ diff --git a/Eval/bitvec_152.lean b/Eval/bitvec_152.lean index 6a1a647b..e75b7321 100644 --- a/Eval/bitvec_152.lean +++ b/Eval/bitvec_152.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_152 : ∀ (x : BitVec 8), x * -1 = 0 - x diff --git a/Eval/bitvec_160.lean b/Eval/bitvec_160.lean index 2dea4eec..65838c47 100644 --- a/Eval/bitvec_160.lean +++ b/Eval/bitvec_160.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_160 : ∀ (x C1 C2 : BitVec 7), x <<< C2 * C1 = x * C1 <<< C2 diff --git a/Eval/bitvec_229.lean b/Eval/bitvec_229.lean index 3ff497b1..e04e0389 100644 --- a/Eval/bitvec_229.lean +++ b/Eval/bitvec_229.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_229 : ∀ (X C1 Op1 : BitVec 4), (X + C1) * Op1 = X * Op1 + C1 * Op1 diff --git a/Eval/bitvec_239.lean b/Eval/bitvec_239.lean index a17ef3f7..8316bd53 100644 --- a/Eval/bitvec_239.lean +++ b/Eval/bitvec_239.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_239 : ∀ (Y X : BitVec 8), (0 - X) * (0 - Y) = X * Y diff --git a/Eval/bitvec_283.lean b/Eval/bitvec_283.lean index 0c08ab2c..b6a0a42e 100644 --- a/Eval/bitvec_283.lean +++ b/Eval/bitvec_283.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_283 : ∀ (Y X : BitVec 1), X * Y = X &&& Y diff --git a/Eval/bitvec_290__292.lean b/Eval/bitvec_290__292.lean index f43201ae..750e2881 100644 --- a/Eval/bitvec_290__292.lean +++ b/Eval/bitvec_290__292.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec theorem bitvec_290__292 : diff --git a/Eval/bitvec_AddSub_1043.lean b/Eval/bitvec_AddSub_1043.lean index 44a130b2..e778c3da 100644 --- a/Eval/bitvec_AddSub_1043.lean +++ b/Eval/bitvec_AddSub_1043.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1043 : ∀ (C1 Z RHS : BitVec 64), (Z &&& C1 ^^^ C1) + 1 + RHS = RHS - (Z ||| ~~~C1) diff --git a/Eval/bitvec_AddSub_1152.lean b/Eval/bitvec_AddSub_1152.lean index fc497da0..d5db5005 100644 --- a/Eval/bitvec_AddSub_1152.lean +++ b/Eval/bitvec_AddSub_1152.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1152 : ∀ (y x : BitVec 1), x + y = x ^^^ y diff --git a/Eval/bitvec_AddSub_1156.lean b/Eval/bitvec_AddSub_1156.lean index b03504dd..d06e1b35 100644 --- a/Eval/bitvec_AddSub_1156.lean +++ b/Eval/bitvec_AddSub_1156.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1156 : ∀ (b : BitVec 64), b + b = b <<< 1 diff --git a/Eval/bitvec_AddSub_1164.lean b/Eval/bitvec_AddSub_1164.lean index cacd7a99..09eba133 100644 --- a/Eval/bitvec_AddSub_1164.lean +++ b/Eval/bitvec_AddSub_1164.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1164 : ∀ (a b : BitVec 64), 0 - a + b = b - a diff --git a/Eval/bitvec_AddSub_1165.lean b/Eval/bitvec_AddSub_1165.lean index 2774e8da..d1c2df4b 100644 --- a/Eval/bitvec_AddSub_1165.lean +++ b/Eval/bitvec_AddSub_1165.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1165 : ∀ (a b : BitVec 64), 0 - a + (0 - b) = 0 - (a + b) diff --git a/Eval/bitvec_AddSub_1176.lean b/Eval/bitvec_AddSub_1176.lean index 7e0dfd1e..e40ae116 100644 --- a/Eval/bitvec_AddSub_1176.lean +++ b/Eval/bitvec_AddSub_1176.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1176 : ∀ (a b : BitVec 64), a + (0 - b) = a - b diff --git a/Eval/bitvec_AddSub_1202.lean b/Eval/bitvec_AddSub_1202.lean index de19cd2e..d9168acd 100644 --- a/Eval/bitvec_AddSub_1202.lean +++ b/Eval/bitvec_AddSub_1202.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1202 : ∀ (x C : BitVec 64), (x ^^^ -1) + C = C - 1 - x diff --git a/Eval/bitvec_AddSub_1295.lean b/Eval/bitvec_AddSub_1295.lean index 5ea25d02..5b9f9593 100644 --- a/Eval/bitvec_AddSub_1295.lean +++ b/Eval/bitvec_AddSub_1295.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1295 : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b diff --git a/Eval/bitvec_AddSub_1309.lean b/Eval/bitvec_AddSub_1309.lean index 29b67efd..a095bd9d 100644 --- a/Eval/bitvec_AddSub_1309.lean +++ b/Eval/bitvec_AddSub_1309.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1309 : ∀ (a b : BitVec 64), (a &&& b) + (a ||| b) = a + b diff --git a/Eval/bitvec_AddSub_1539.lean b/Eval/bitvec_AddSub_1539.lean index 267ad7a4..8184eb79 100644 --- a/Eval/bitvec_AddSub_1539.lean +++ b/Eval/bitvec_AddSub_1539.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1539 : ∀ (a x : BitVec 64), x - (0 - a) = x + a diff --git a/Eval/bitvec_AddSub_1539_2.lean b/Eval/bitvec_AddSub_1539_2.lean index 3f6447da..6978ea27 100644 --- a/Eval/bitvec_AddSub_1539_2.lean +++ b/Eval/bitvec_AddSub_1539_2.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1539_2 : ∀ (x C : BitVec 64), x - C = x + -C diff --git a/Eval/bitvec_AddSub_1556.lean b/Eval/bitvec_AddSub_1556.lean index e9231942..7eff4281 100644 --- a/Eval/bitvec_AddSub_1556.lean +++ b/Eval/bitvec_AddSub_1556.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1556 : ∀ (y x : BitVec 1), x - y = x ^^^ y diff --git a/Eval/bitvec_AddSub_1560.lean b/Eval/bitvec_AddSub_1560.lean index 86d070a1..e062d381 100644 --- a/Eval/bitvec_AddSub_1560.lean +++ b/Eval/bitvec_AddSub_1560.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1560 : ∀ (a : BitVec 64), -1 - a = a ^^^ -1 diff --git a/Eval/bitvec_AddSub_1564.lean b/Eval/bitvec_AddSub_1564.lean index b97636f1..62d99671 100644 --- a/Eval/bitvec_AddSub_1564.lean +++ b/Eval/bitvec_AddSub_1564.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1564 : ∀ (x C : BitVec 64), C - (x ^^^ -1) = x + (C + 1) diff --git a/Eval/bitvec_AddSub_1574.lean b/Eval/bitvec_AddSub_1574.lean index 9066d21b..e9e9d0e4 100644 --- a/Eval/bitvec_AddSub_1574.lean +++ b/Eval/bitvec_AddSub_1574.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1574 : ∀ (X C C2 : BitVec 64), C - (X + C2) = C - C2 - X diff --git a/Eval/bitvec_AddSub_1614.lean b/Eval/bitvec_AddSub_1614.lean index 39c3654a..60a849f2 100644 --- a/Eval/bitvec_AddSub_1614.lean +++ b/Eval/bitvec_AddSub_1614.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1614 : ∀ (Y X : BitVec 64), X - (X + Y) = 0 - Y diff --git a/Eval/bitvec_AddSub_1619.lean b/Eval/bitvec_AddSub_1619.lean index bdc6c5b0..969859d7 100644 --- a/Eval/bitvec_AddSub_1619.lean +++ b/Eval/bitvec_AddSub_1619.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1619 : ∀ (Y X : BitVec 64), X - Y - X = 0 - Y diff --git a/Eval/bitvec_AddSub_1624.lean b/Eval/bitvec_AddSub_1624.lean index 6014a592..0a2dc865 100644 --- a/Eval/bitvec_AddSub_1624.lean +++ b/Eval/bitvec_AddSub_1624.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AddSub_1624 : ∀ (A B : BitVec 64), (A ||| B) - (A ^^^ B) = A &&& B diff --git a/Eval/bitvec_AndOrXor_1230__A__B___A__B.lean b/Eval/bitvec_AndOrXor_1230__A__B___A__B.lean index 7eab7dc2..c13f6ec5 100644 --- a/Eval/bitvec_AndOrXor_1230__A__B___A__B.lean +++ b/Eval/bitvec_AndOrXor_1230__A__B___A__B.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_1230__A__B___A__B : ∀ (notOp0 notOp1 : BitVec 64), (notOp0 ^^^ -1) &&& (notOp1 ^^^ -1) = (notOp0 ||| notOp1) ^^^ -1 diff --git a/Eval/bitvec_AndOrXor_1241_AB__AB__AB.lean b/Eval/bitvec_AndOrXor_1241_AB__AB__AB.lean index fd0b4fcd..4aa23929 100644 --- a/Eval/bitvec_AndOrXor_1241_AB__AB__AB.lean +++ b/Eval/bitvec_AndOrXor_1241_AB__AB__AB.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_1241_AB__AB__AB : ∀ (A B : BitVec 64), (A ||| B) &&& (A &&& B ^^^ -1) = A ^^^ B diff --git a/Eval/bitvec_AndOrXor_1247_AB__AB__AB.lean b/Eval/bitvec_AndOrXor_1247_AB__AB__AB.lean index d6905828..0335f4d8 100644 --- a/Eval/bitvec_AndOrXor_1247_AB__AB__AB.lean +++ b/Eval/bitvec_AndOrXor_1247_AB__AB__AB.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_1247_AB__AB__AB : ∀ (A B : BitVec 64), (A &&& B ^^^ -1) &&& (A ||| B) = A ^^^ B diff --git a/Eval/bitvec_AndOrXor_1253_A__AB___A__B.lean b/Eval/bitvec_AndOrXor_1253_A__AB___A__B.lean index e39af797..0662ec52 100644 --- a/Eval/bitvec_AndOrXor_1253_A__AB___A__B.lean +++ b/Eval/bitvec_AndOrXor_1253_A__AB___A__B.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_1253_A__AB___A__B : ∀ (A B : BitVec 64), (A ^^^ B) &&& A = A &&& (B ^^^ -1) diff --git a/Eval/bitvec_AndOrXor_1280_ABA___AB.lean b/Eval/bitvec_AndOrXor_1280_ABA___AB.lean index 741a096a..22a7f37e 100644 --- a/Eval/bitvec_AndOrXor_1280_ABA___AB.lean +++ b/Eval/bitvec_AndOrXor_1280_ABA___AB.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_1280_ABA___AB : ∀ (A B : BitVec 64), (A ^^^ -1 ||| B) &&& A = A &&& B diff --git a/Eval/bitvec_AndOrXor_1288_A__B__B__C__A___A__B__C.lean b/Eval/bitvec_AndOrXor_1288_A__B__B__C__A___A__B__C.lean index eb140cf2..8c0aae19 100644 --- a/Eval/bitvec_AndOrXor_1288_A__B__B__C__A___A__B__C.lean +++ b/Eval/bitvec_AndOrXor_1288_A__B__B__C__A___A__B__C.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_1288_A__B__B__C__A___A__B__C : ∀ (A C B : BitVec 64), (A ^^^ B) &&& (B ^^^ C ^^^ A) = (A ^^^ B) &&& (C ^^^ -1) diff --git a/Eval/bitvec_AndOrXor_1294_A__B__A__B___A__B.lean b/Eval/bitvec_AndOrXor_1294_A__B__A__B___A__B.lean index d2db7f4f..cf715e0f 100644 --- a/Eval/bitvec_AndOrXor_1294_A__B__A__B___A__B.lean +++ b/Eval/bitvec_AndOrXor_1294_A__B__A__B___A__B.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_1294_A__B__A__B___A__B : ∀ (A B : BitVec 64), (A ||| B) &&& (A ^^^ -1 ^^^ B) = A &&& B diff --git a/Eval/bitvec_AndOrXor_135.lean b/Eval/bitvec_AndOrXor_135.lean index fd601794..ca48ba62 100644 --- a/Eval/bitvec_AndOrXor_135.lean +++ b/Eval/bitvec_AndOrXor_135.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_135 : ∀ (X C1 C2 : BitVec 64), (X ^^^ C1) &&& C2 = X &&& C2 ^^^ C1 &&& C2 diff --git a/Eval/bitvec_AndOrXor_144.lean b/Eval/bitvec_AndOrXor_144.lean index f3d85a39..ef51d606 100644 --- a/Eval/bitvec_AndOrXor_144.lean +++ b/Eval/bitvec_AndOrXor_144.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_144 : ∀ (X C1 C2 : BitVec 64), (X ||| C1) &&& C2 = (X ||| C1 &&& C2) &&& C2 diff --git a/Eval/bitvec_AndOrXor_1683_1.lean b/Eval/bitvec_AndOrXor_1683_1.lean index 0a93383c..9e0febb2 100644 --- a/Eval/bitvec_AndOrXor_1683_1.lean +++ b/Eval/bitvec_AndOrXor_1683_1.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec diff --git a/Eval/bitvec_AndOrXor_1683_2.lean b/Eval/bitvec_AndOrXor_1683_2.lean index 085c9542..78e112f3 100644 --- a/Eval/bitvec_AndOrXor_1683_2.lean +++ b/Eval/bitvec_AndOrXor_1683_2.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_1683_2 : ∀ (a b : BitVec 64), (b ≤ a) || (a != b) = true diff --git a/Eval/bitvec_AndOrXor_1704.lean b/Eval/bitvec_AndOrXor_1704.lean index 3d7a3791..936e20aa 100644 --- a/Eval/bitvec_AndOrXor_1704.lean +++ b/Eval/bitvec_AndOrXor_1704.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_1704 : ∀ (A B : BitVec 64), ((B == 0) || (A < B)) = (A ≤ B + -1) diff --git a/Eval/bitvec_AndOrXor_1705.lean b/Eval/bitvec_AndOrXor_1705.lean index 07e8a30e..cd3d6b34 100644 --- a/Eval/bitvec_AndOrXor_1705.lean +++ b/Eval/bitvec_AndOrXor_1705.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_1705 : ∀ (A B : BitVec 64), ((B == 0) || (A < B)) = (A ≤ B + -1) diff --git a/Eval/bitvec_AndOrXor_1733.lean b/Eval/bitvec_AndOrXor_1733.lean index 6b86b888..362ea91f 100644 --- a/Eval/bitvec_AndOrXor_1733.lean +++ b/Eval/bitvec_AndOrXor_1733.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_1733 : ∀ (A B : BitVec 64), (A != 0) ∨ (B != 0) = (A ||| B != 0) diff --git a/Eval/bitvec_AndOrXor_2063__X__C1__C2____X__C2__C1__C2.lean b/Eval/bitvec_AndOrXor_2063__X__C1__C2____X__C2__C1__C2.lean index 23f20a2e..26683a9d 100644 --- a/Eval/bitvec_AndOrXor_2063__X__C1__C2____X__C2__C1__C2.lean +++ b/Eval/bitvec_AndOrXor_2063__X__C1__C2____X__C2__C1__C2.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2063__X__C1__C2____X__C2__C1__C2 : ∀ (x C1 C : BitVec 64), x ^^^ C1 ||| C = (x ||| C) ^^^ C1 &&& ~~~C diff --git a/Eval/bitvec_AndOrXor_2113___A__B__A___A__B.lean b/Eval/bitvec_AndOrXor_2113___A__B__A___A__B.lean index 469c5938..79155dd0 100644 --- a/Eval/bitvec_AndOrXor_2113___A__B__A___A__B.lean +++ b/Eval/bitvec_AndOrXor_2113___A__B__A___A__B.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2113___A__B__A___A__B : ∀ (A B : BitVec 64), (A ^^^ -1) &&& B ||| A = A ||| B diff --git a/Eval/bitvec_AndOrXor_2118___A__B__A___A__B.lean b/Eval/bitvec_AndOrXor_2118___A__B__A___A__B.lean index 373fd9e5..d641c6c1 100644 --- a/Eval/bitvec_AndOrXor_2118___A__B__A___A__B.lean +++ b/Eval/bitvec_AndOrXor_2118___A__B__A___A__B.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2118___A__B__A___A__B : ∀ (A B : BitVec 64), A &&& B ||| A ^^^ -1 = A ^^^ -1 ||| B diff --git a/Eval/bitvec_AndOrXor_2123___A__B__A__B___A__B.lean b/Eval/bitvec_AndOrXor_2123___A__B__A__B___A__B.lean index 1407e91b..5bced7e7 100644 --- a/Eval/bitvec_AndOrXor_2123___A__B__A__B___A__B.lean +++ b/Eval/bitvec_AndOrXor_2123___A__B__A__B___A__B.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2123___A__B__A__B___A__B : ∀ (A B : BitVec 64), A &&& (B ^^^ -1) ||| A ^^^ B = A ^^^ B diff --git a/Eval/bitvec_AndOrXor_2188.lean b/Eval/bitvec_AndOrXor_2188.lean index 80b05ab7..9f3a8f5f 100644 --- a/Eval/bitvec_AndOrXor_2188.lean +++ b/Eval/bitvec_AndOrXor_2188.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2188 : ∀ (A D : BitVec 64), A &&& (D ^^^ -1) ||| (A ^^^ -1) &&& D = A ^^^ D diff --git a/Eval/bitvec_AndOrXor_2231__A__B__B__C__A___A__B__C.lean b/Eval/bitvec_AndOrXor_2231__A__B__B__C__A___A__B__C.lean index 81119fcc..59604b2e 100644 --- a/Eval/bitvec_AndOrXor_2231__A__B__B__C__A___A__B__C.lean +++ b/Eval/bitvec_AndOrXor_2231__A__B__B__C__A___A__B__C.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2231__A__B__B__C__A___A__B__C : ∀ (A C B : BitVec 64), A ^^^ B ||| B ^^^ C ^^^ A = A ^^^ B ||| C diff --git a/Eval/bitvec_AndOrXor_2243__B__C__A__B___B__A__C.lean b/Eval/bitvec_AndOrXor_2243__B__C__A__B___B__A__C.lean index 354d3536..5222dffd 100644 --- a/Eval/bitvec_AndOrXor_2243__B__C__A__B___B__A__C.lean +++ b/Eval/bitvec_AndOrXor_2243__B__C__A__B___B__A__C.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2243__B__C__A__B___B__A__C : ∀ (A C B : BitVec 64), (B ||| C) &&& A ||| B = B ||| A &&& C diff --git a/Eval/bitvec_AndOrXor_2247__A__B__A__B.lean b/Eval/bitvec_AndOrXor_2247__A__B__A__B.lean index 2e4721f4..4db8b7fa 100644 --- a/Eval/bitvec_AndOrXor_2247__A__B__A__B.lean +++ b/Eval/bitvec_AndOrXor_2247__A__B__A__B.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2247__A__B__A__B : ∀ (A B : BitVec 64), A ^^^ -1 ||| B ^^^ -1 = A &&& B ^^^ -1 diff --git a/Eval/bitvec_AndOrXor_2263.lean b/Eval/bitvec_AndOrXor_2263.lean index 9a57e1c2..dfcae95a 100644 --- a/Eval/bitvec_AndOrXor_2263.lean +++ b/Eval/bitvec_AndOrXor_2263.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2263 : ∀ (B op0 : BitVec 64), op0 ||| op0 ^^^ B = op0 ||| B diff --git a/Eval/bitvec_AndOrXor_2264.lean b/Eval/bitvec_AndOrXor_2264.lean index 84459137..0dccd709 100644 --- a/Eval/bitvec_AndOrXor_2264.lean +++ b/Eval/bitvec_AndOrXor_2264.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2264 : ∀ (A B : BitVec 64), A ||| A ^^^ -1 ^^^ B = A ||| B ^^^ -1 diff --git a/Eval/bitvec_AndOrXor_2265.lean b/Eval/bitvec_AndOrXor_2265.lean index 01e522c2..a1280f57 100644 --- a/Eval/bitvec_AndOrXor_2265.lean +++ b/Eval/bitvec_AndOrXor_2265.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2265 : ∀ (A B : BitVec 64), A &&& B ||| A ^^^ B = A ||| B diff --git a/Eval/bitvec_AndOrXor_2284.lean b/Eval/bitvec_AndOrXor_2284.lean index f4b39663..ed78f582 100644 --- a/Eval/bitvec_AndOrXor_2284.lean +++ b/Eval/bitvec_AndOrXor_2284.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2284 : ∀ (A B : BitVec 64), A ||| (A ||| B) ^^^ -1 = A ||| B ^^^ -1 diff --git a/Eval/bitvec_AndOrXor_2285.lean b/Eval/bitvec_AndOrXor_2285.lean index 78ec6308..f8c6078f 100644 --- a/Eval/bitvec_AndOrXor_2285.lean +++ b/Eval/bitvec_AndOrXor_2285.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2285 : ∀ (A B : BitVec 64), A ||| A ^^^ B ^^^ -1 = A ||| B ^^^ -1 diff --git a/Eval/bitvec_AndOrXor_2297.lean b/Eval/bitvec_AndOrXor_2297.lean index 9ab43d36..3196aa37 100644 --- a/Eval/bitvec_AndOrXor_2297.lean +++ b/Eval/bitvec_AndOrXor_2297.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2297 : ∀ (A B : BitVec 64), A &&& B ||| A ^^^ -1 ^^^ B = A ^^^ -1 ^^^ B diff --git a/Eval/bitvec_AndOrXor_2367.lean b/Eval/bitvec_AndOrXor_2367.lean index c257ac42..8799d4d4 100644 --- a/Eval/bitvec_AndOrXor_2367.lean +++ b/Eval/bitvec_AndOrXor_2367.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2367 : ∀ (A C1 op1 : BitVec 64), A ||| C1 ||| op1 = A ||| op1 ||| C1 diff --git a/Eval/bitvec_AndOrXor_2416.lean b/Eval/bitvec_AndOrXor_2416.lean index fd081cfb..c568ee99 100644 --- a/Eval/bitvec_AndOrXor_2416.lean +++ b/Eval/bitvec_AndOrXor_2416.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2416 : ∀ (nx y : BitVec 64), (nx ^^^ -1) &&& y ^^^ -1 = nx ||| y ^^^ -1 diff --git a/Eval/bitvec_AndOrXor_2417.lean b/Eval/bitvec_AndOrXor_2417.lean index 91cafa02..37aa3b42 100644 --- a/Eval/bitvec_AndOrXor_2417.lean +++ b/Eval/bitvec_AndOrXor_2417.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2417 : ∀ (nx y : BitVec 64), (nx ^^^ -1 ||| y) ^^^ -1 = nx &&& (y ^^^ -1) diff --git a/Eval/bitvec_AndOrXor_2429.lean b/Eval/bitvec_AndOrXor_2429.lean index 2a93edb3..14885d60 100644 --- a/Eval/bitvec_AndOrXor_2429.lean +++ b/Eval/bitvec_AndOrXor_2429.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2429 : ∀ (y x : BitVec 64), x &&& y ^^^ -1 = x ^^^ -1 ||| y ^^^ -1 diff --git a/Eval/bitvec_AndOrXor_2430.lean b/Eval/bitvec_AndOrXor_2430.lean index 09a65825..41c6e469 100644 --- a/Eval/bitvec_AndOrXor_2430.lean +++ b/Eval/bitvec_AndOrXor_2430.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2430 : ∀ (y x : BitVec 64), (x ||| y) ^^^ -1 = (x ^^^ -1) &&& (y ^^^ -1) diff --git a/Eval/bitvec_AndOrXor_2443.lean b/Eval/bitvec_AndOrXor_2443.lean index 6e6e46c2..beae9c93 100644 --- a/Eval/bitvec_AndOrXor_2443.lean +++ b/Eval/bitvec_AndOrXor_2443.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec diff --git a/Eval/bitvec_AndOrXor_2475.lean b/Eval/bitvec_AndOrXor_2475.lean index 3315e2cd..35967af4 100644 --- a/Eval/bitvec_AndOrXor_2475.lean +++ b/Eval/bitvec_AndOrXor_2475.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2475 : ∀ (x C : BitVec 64), C - x ^^^ -1 = x + (-1 - C) diff --git a/Eval/bitvec_AndOrXor_2486.lean b/Eval/bitvec_AndOrXor_2486.lean index dc65ad32..0c3b99f5 100644 --- a/Eval/bitvec_AndOrXor_2486.lean +++ b/Eval/bitvec_AndOrXor_2486.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2486 : ∀ (x C : BitVec 64), x + C ^^^ -1 = -1 - C - x diff --git a/Eval/bitvec_AndOrXor_2581__BAB___A__B.lean b/Eval/bitvec_AndOrXor_2581__BAB___A__B.lean index b5363945..b8596f96 100644 --- a/Eval/bitvec_AndOrXor_2581__BAB___A__B.lean +++ b/Eval/bitvec_AndOrXor_2581__BAB___A__B.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2581__BAB___A__B : ∀ (a op1 : BitVec 64), (a ||| op1) ^^^ op1 = a &&& (op1 ^^^ -1) diff --git a/Eval/bitvec_AndOrXor_2587__BAA___B__A.lean b/Eval/bitvec_AndOrXor_2587__BAA___B__A.lean index c1a33962..da36903d 100644 --- a/Eval/bitvec_AndOrXor_2587__BAA___B__A.lean +++ b/Eval/bitvec_AndOrXor_2587__BAA___B__A.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2587__BAA___B__A : ∀ (a op1 : BitVec 64), a &&& op1 ^^^ op1 = (a ^^^ -1) &&& op1 diff --git a/Eval/bitvec_AndOrXor_2595.lean b/Eval/bitvec_AndOrXor_2595.lean index 1b147918..5016f462 100644 --- a/Eval/bitvec_AndOrXor_2595.lean +++ b/Eval/bitvec_AndOrXor_2595.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2595 : ∀ (a b : BitVec 64), a &&& b ^^^ (a ||| b) = a ^^^ b diff --git a/Eval/bitvec_AndOrXor_2607.lean b/Eval/bitvec_AndOrXor_2607.lean index 5d003ae2..d41056c6 100644 --- a/Eval/bitvec_AndOrXor_2607.lean +++ b/Eval/bitvec_AndOrXor_2607.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2607 : ∀ (a b : BitVec 64), (a ||| b ^^^ -1) ^^^ (a ^^^ -1 ||| b) = a ^^^ b diff --git a/Eval/bitvec_AndOrXor_2617.lean b/Eval/bitvec_AndOrXor_2617.lean index 82c9b3a1..7cae3a57 100644 --- a/Eval/bitvec_AndOrXor_2617.lean +++ b/Eval/bitvec_AndOrXor_2617.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2617 : ∀ (a b : BitVec 64), a &&& (b ^^^ -1) ^^^ (a ^^^ -1) &&& b = a ^^^ b diff --git a/Eval/bitvec_AndOrXor_2627.lean b/Eval/bitvec_AndOrXor_2627.lean index c75841b0..384bc47a 100644 --- a/Eval/bitvec_AndOrXor_2627.lean +++ b/Eval/bitvec_AndOrXor_2627.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2627 : ∀ (a c b : BitVec 64), a ^^^ c ^^^ (a ||| b) = (a ^^^ -1) &&& b ^^^ c diff --git a/Eval/bitvec_AndOrXor_2647.lean b/Eval/bitvec_AndOrXor_2647.lean index 875ab466..4fa3e30b 100644 --- a/Eval/bitvec_AndOrXor_2647.lean +++ b/Eval/bitvec_AndOrXor_2647.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2647 : ∀ (a b : BitVec 64), a &&& b ^^^ (a ^^^ b) = a ||| b diff --git a/Eval/bitvec_AndOrXor_2658.lean b/Eval/bitvec_AndOrXor_2658.lean index 9b300844..10002af9 100644 --- a/Eval/bitvec_AndOrXor_2658.lean +++ b/Eval/bitvec_AndOrXor_2658.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2658 : ∀ (a b : BitVec 64), a &&& (b ^^^ -1) ^^^ (a ^^^ -1) = a &&& b ^^^ -1 diff --git a/Eval/bitvec_AndOrXor_2663.lean b/Eval/bitvec_AndOrXor_2663.lean index 244787f7..2000b4c5 100644 --- a/Eval/bitvec_AndOrXor_2663.lean +++ b/Eval/bitvec_AndOrXor_2663.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_2663 : ∀ (a b : BitVec 64), xor (a ≤ b) (a != b) = (b ≤ a) diff --git a/Eval/bitvec_AndOrXor_698.lean b/Eval/bitvec_AndOrXor_698.lean index 7223a0b4..749cf6f2 100644 --- a/Eval/bitvec_AndOrXor_698.lean +++ b/Eval/bitvec_AndOrXor_698.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_698 : ∀ (a b d : BitVec 64), ((a &&& b == 0) && (a &&& d == 0)) = (a &&& (b ||| d) == 0) diff --git a/Eval/bitvec_AndOrXor_709.lean b/Eval/bitvec_AndOrXor_709.lean index b073f6d1..bc48924f 100644 --- a/Eval/bitvec_AndOrXor_709.lean +++ b/Eval/bitvec_AndOrXor_709.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_709 : ∀ (a b d : BitVec 64), ((a &&& b == b) && (a &&& d == d)) = (a &&& (b ||| d) == b ||| d) diff --git a/Eval/bitvec_AndOrXor_716.lean b/Eval/bitvec_AndOrXor_716.lean index 58b6b20c..c19ec7e7 100644 --- a/Eval/bitvec_AndOrXor_716.lean +++ b/Eval/bitvec_AndOrXor_716.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_716 : ∀ (a b d : BitVec 64), ((a &&& b == a) && (a &&& d == a)) = (a &&& (b &&& d) == a) diff --git a/Eval/bitvec_AndOrXor_794.lean b/Eval/bitvec_AndOrXor_794.lean index 4da36d3b..f7480600 100644 --- a/Eval/bitvec_AndOrXor_794.lean +++ b/Eval/bitvec_AndOrXor_794.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_794 : ∀ (a b : BitVec 64), ((BitVec.slt b a) && (a != b)) = (BitVec.slt b a) diff --git a/Eval/bitvec_AndOrXor_827.lean b/Eval/bitvec_AndOrXor_827.lean index bc18d5ae..ed3ad524 100644 --- a/Eval/bitvec_AndOrXor_827.lean +++ b/Eval/bitvec_AndOrXor_827.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_827 : ∀ (a b : BitVec 64), ((a == 0) && (b == 0)) = (a ||| b == 0) diff --git a/Eval/bitvec_AndOrXor_887_2.lean b/Eval/bitvec_AndOrXor_887_2.lean index a066c169..075313d2 100644 --- a/Eval/bitvec_AndOrXor_887_2.lean +++ b/Eval/bitvec_AndOrXor_887_2.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_AndOrXor_887_2 : ∀ (a C1 : BitVec 64), ((a == C1) && (a != C1)) = false diff --git a/Eval/bitvec_InstCombineShift__239.lean b/Eval/bitvec_InstCombineShift__239.lean index efeb84b6..dc790e2b 100644 --- a/Eval/bitvec_InstCombineShift__239.lean +++ b/Eval/bitvec_InstCombineShift__239.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_InstCombineShift__239 : ∀ (X C : BitVec 64), X <<< C >>> C = X &&& (-1 : BitVec _) >>> C diff --git a/Eval/bitvec_InstCombineShift__279.lean b/Eval/bitvec_InstCombineShift__279.lean index 1909ffce..6d97f3ea 100644 --- a/Eval/bitvec_InstCombineShift__279.lean +++ b/Eval/bitvec_InstCombineShift__279.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_InstCombineShift__279 : ∀ (X C : BitVec 64), X >>> C <<< C = X &&& (-1 : BitVec _) <<< C diff --git a/Eval/bitvec_InstCombineShift__351.lean b/Eval/bitvec_InstCombineShift__351.lean index 3f1cbb42..5fec20d9 100644 --- a/Eval/bitvec_InstCombineShift__351.lean +++ b/Eval/bitvec_InstCombineShift__351.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_InstCombineShift__351 : ∀ (X C1 C2 : BitVec 7), (X * C1) <<< C2 = X * C1 <<< C2 diff --git a/Eval/bitvec_InstCombineShift__422_1.lean b/Eval/bitvec_InstCombineShift__422_1.lean index 87a2a0a2..dc822f92 100644 --- a/Eval/bitvec_InstCombineShift__422_1.lean +++ b/Eval/bitvec_InstCombineShift__422_1.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_InstCombineShift__422_1 : ∀ (Y X C : BitVec 31), (Y + X >>> C) <<< C = Y <<< C + X &&& (-1 : BitVec _) <<< C diff --git a/Eval/bitvec_InstCombineShift__422_2.lean b/Eval/bitvec_InstCombineShift__422_2.lean index 9b5aba2b..a11db27d 100644 --- a/Eval/bitvec_InstCombineShift__422_2.lean +++ b/Eval/bitvec_InstCombineShift__422_2.lean @@ -1,5 +1,5 @@ -- set_option maxRecDepth 9999 in -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec diff --git a/Eval/bitvec_InstCombineShift__440.lean b/Eval/bitvec_InstCombineShift__440.lean index e2757208..7ff89fc1 100644 --- a/Eval/bitvec_InstCombineShift__440.lean +++ b/Eval/bitvec_InstCombineShift__440.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_InstCombineShift__440 : ∀ (Y X C C2 : BitVec 64), (Y ^^^ X >>> C &&& C2) <<< C = X &&& C2 <<< C ^^^ Y <<< C diff --git a/Eval/bitvec_InstCombineShift__458.lean b/Eval/bitvec_InstCombineShift__458.lean index ffa18a84..e53aa13f 100644 --- a/Eval/bitvec_InstCombineShift__458.lean +++ b/Eval/bitvec_InstCombineShift__458.lean @@ -1,5 +1,5 @@ -- set_option maxRecDepth 9999 in -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec diff --git a/Eval/bitvec_InstCombineShift__476.lean b/Eval/bitvec_InstCombineShift__476.lean index 42b4b2c9..16b49ae8 100644 --- a/Eval/bitvec_InstCombineShift__476.lean +++ b/Eval/bitvec_InstCombineShift__476.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_InstCombineShift__476 : ∀ (Y X C C2 : BitVec 64), (X >>> C &&& C2 ||| Y) <<< C = X &&& C2 <<< C ||| Y <<< C diff --git a/Eval/bitvec_InstCombineShift__497'''.lean b/Eval/bitvec_InstCombineShift__497'''.lean index 557083b3..55e1ba84 100644 --- a/Eval/bitvec_InstCombineShift__497'''.lean +++ b/Eval/bitvec_InstCombineShift__497'''.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_InstCombineShift__497''' : ∀ (X C C2 : BitVec 64), (X + C2) <<< C = X <<< C + C2 <<< C diff --git a/Eval/bitvec_InstCombineShift__497.lean b/Eval/bitvec_InstCombineShift__497.lean index 7f1b2d52..c7ad13bc 100644 --- a/Eval/bitvec_InstCombineShift__497.lean +++ b/Eval/bitvec_InstCombineShift__497.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_InstCombineShift__497 : ∀ (X C C2 : BitVec 64), (X ^^^ C2) >>> C = X >>> C ^^^ C2 >>> C diff --git a/Eval/bitvec_InstCombineShift__582.lean b/Eval/bitvec_InstCombineShift__582.lean index 91f893b5..0771306f 100644 --- a/Eval/bitvec_InstCombineShift__582.lean +++ b/Eval/bitvec_InstCombineShift__582.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec diff --git a/Eval/bitvec_InstCombineShift__724.lean b/Eval/bitvec_InstCombineShift__724.lean index edf2d0d6..42459359 100644 --- a/Eval/bitvec_InstCombineShift__724.lean +++ b/Eval/bitvec_InstCombineShift__724.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide theorem bitvec_InstCombineShift__724 : ∀ (A C2 C1 : BitVec 31), C1 <<< A <<< C2 = C1 <<< C2 <<< A diff --git a/LeanSAT.lean b/LeanSAT.lean index 441504e8..d67f33ff 100644 --- a/LeanSAT.lean +++ b/LeanSAT.lean @@ -1,2 +1 @@ -import LeanSAT.Reflect import LeanSAT.AIG diff --git a/LeanSAT/Reflect.lean b/LeanSAT/Reflect.lean deleted file mode 100644 index 9430bb61..00000000 --- a/LeanSAT/Reflect.lean +++ /dev/null @@ -1,11 +0,0 @@ -/- -Copyright (c) 2024 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Scott Morrison --/ -import LeanSAT.Reflect.Tactics.Attr -import LeanSAT.Reflect.Glue -import LeanSAT.Reflect.Tactics.BVDecide -import LeanSAT.Reflect.Tactics.BVTrace -import LeanSAT.Reflect.Tactics.BVCheck -import LeanSAT.Reflect.LRAT diff --git a/LeanSAT/Tactics.lean b/LeanSAT/Tactics.lean new file mode 100644 index 00000000..e69de29b diff --git a/LeanSAT/Reflect/Tactics/Attr.lean b/LeanSAT/Tactics/Attr.lean similarity index 100% rename from LeanSAT/Reflect/Tactics/Attr.lean rename to LeanSAT/Tactics/Attr.lean diff --git a/LeanSAT/Reflect/Tactics/BVCheck.lean b/LeanSAT/Tactics/BVCheck.lean similarity index 98% rename from LeanSAT/Reflect/Tactics/BVCheck.lean rename to LeanSAT/Tactics/BVCheck.lean index 48091027..3b357a14 100644 --- a/LeanSAT/Reflect/Tactics/BVCheck.lean +++ b/LeanSAT/Tactics/BVCheck.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open Lean Elab Meta diff --git a/LeanSAT/Reflect/Tactics/BVDecide.lean b/LeanSAT/Tactics/BVDecide.lean similarity index 99% rename from LeanSAT/Reflect/Tactics/BVDecide.lean rename to LeanSAT/Tactics/BVDecide.lean index cf762ba1..55f81d16 100644 --- a/LeanSAT/Reflect/Tactics/BVDecide.lean +++ b/LeanSAT/Tactics/BVDecide.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ import LeanSAT.BitBlast.BVExpr -import LeanSAT.Reflect.Tactics.Normalize -import LeanSAT.Reflect.LRAT +import LeanSAT.Tactics.Normalize +import LeanSAT.Tactics.LRAT import LeanSAT.AIG.CNF import LeanSAT.AIG.RelabelNat diff --git a/LeanSAT/Reflect/Tactics/BVTrace.lean b/LeanSAT/Tactics/BVTrace.lean similarity index 95% rename from LeanSAT/Reflect/Tactics/BVTrace.lean rename to LeanSAT/Tactics/BVTrace.lean index 1bafe92d..6ef83104 100644 --- a/LeanSAT/Reflect/Tactics/BVTrace.lean +++ b/LeanSAT/Tactics/BVTrace.lean @@ -3,8 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ -import LeanSAT.Reflect.Tactics.BVDecide -import LeanSAT.Reflect.Tactics.BVCheck +import LeanSAT.Tactics.BVDecide +import LeanSAT.Tactics.BVCheck import LeanSAT.LRAT.Trim import Lean.Meta.Tactic.TryThis diff --git a/LeanSAT/Reflect/Glue.lean b/LeanSAT/Tactics/Glue.lean similarity index 100% rename from LeanSAT/Reflect/Glue.lean rename to LeanSAT/Tactics/Glue.lean diff --git a/LeanSAT/Reflect/LRAT.lean b/LeanSAT/Tactics/LRAT.lean similarity index 99% rename from LeanSAT/Reflect/LRAT.lean rename to LeanSAT/Tactics/LRAT.lean index 9ba5158e..00c14ede 100644 --- a/LeanSAT/Reflect/LRAT.lean +++ b/LeanSAT/Tactics/LRAT.lean @@ -3,8 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ -import LeanSAT.Reflect.Glue -import LeanSAT.Reflect.Tactics.Attr +import LeanSAT.Tactics.Glue +import LeanSAT.Tactics.Attr import LeanSAT.LRAT.LRATChecker import LeanSAT.LRAT.LRATCheckerSound import LeanSAT.External.Solver diff --git a/LeanSAT/Reflect/Tactics/Normalize.lean b/LeanSAT/Tactics/Normalize.lean similarity index 84% rename from LeanSAT/Reflect/Tactics/Normalize.lean rename to LeanSAT/Tactics/Normalize.lean index bf1a03fd..d3d6a83c 100644 --- a/LeanSAT/Reflect/Tactics/Normalize.lean +++ b/LeanSAT/Tactics/Normalize.lean @@ -7,12 +7,12 @@ import Lean.Meta.AppBuilder import Lean.Elab.Tactic.Simp import Lean.Elab.Tactic.FalseOrByContra -import LeanSAT.Reflect.Tactics.Attr -import LeanSAT.Reflect.Tactics.Normalize.Canonicalize -import LeanSAT.Reflect.Tactics.Normalize.Prop -import LeanSAT.Reflect.Tactics.Normalize.Bool -import LeanSAT.Reflect.Tactics.Normalize.BitVec -import LeanSAT.Reflect.Tactics.Normalize.Equal +import LeanSAT.Tactics.Attr +import LeanSAT.Tactics.Normalize.Canonicalize +import LeanSAT.Tactics.Normalize.Prop +import LeanSAT.Tactics.Normalize.Bool +import LeanSAT.Tactics.Normalize.BitVec +import LeanSAT.Tactics.Normalize.Equal namespace BVDecide namespace Normalize diff --git a/LeanSAT/Reflect/Tactics/Normalize/BitVec.lean b/LeanSAT/Tactics/Normalize/BitVec.lean similarity index 97% rename from LeanSAT/Reflect/Tactics/Normalize/BitVec.lean rename to LeanSAT/Tactics/Normalize/BitVec.lean index 1c41b9e7..49b515d0 100644 --- a/LeanSAT/Reflect/Tactics/Normalize/BitVec.lean +++ b/LeanSAT/Tactics/Normalize/BitVec.lean @@ -3,9 +3,9 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ -import LeanSAT.Reflect.Tactics.Attr -import LeanSAT.Reflect.Tactics.Normalize.Bool -import LeanSAT.Reflect.Tactics.Normalize.Canonicalize +import LeanSAT.Tactics.Attr +import LeanSAT.Tactics.Normalize.Bool +import LeanSAT.Tactics.Normalize.Canonicalize namespace BVDecide namespace Normalize diff --git a/LeanSAT/Reflect/Tactics/Normalize/Bool.lean b/LeanSAT/Tactics/Normalize/Bool.lean similarity index 97% rename from LeanSAT/Reflect/Tactics/Normalize/Bool.lean rename to LeanSAT/Tactics/Normalize/Bool.lean index e855770a..5351ff58 100644 --- a/LeanSAT/Reflect/Tactics/Normalize/Bool.lean +++ b/LeanSAT/Tactics/Normalize/Bool.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ -import LeanSAT.Reflect.Tactics.Attr +import LeanSAT.Tactics.Attr namespace BVDecide namespace Normalize diff --git a/LeanSAT/Reflect/Tactics/Normalize/Canonicalize.lean b/LeanSAT/Tactics/Normalize/Canonicalize.lean similarity index 98% rename from LeanSAT/Reflect/Tactics/Normalize/Canonicalize.lean rename to LeanSAT/Tactics/Normalize/Canonicalize.lean index 9700a2cb..3b2a0c96 100644 --- a/LeanSAT/Reflect/Tactics/Normalize/Canonicalize.lean +++ b/LeanSAT/Tactics/Normalize/Canonicalize.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ -import LeanSAT.Reflect.Tactics.Attr +import LeanSAT.Tactics.Attr namespace BVDecide namespace Normalize diff --git a/LeanSAT/Reflect/Tactics/Normalize/Equal.lean b/LeanSAT/Tactics/Normalize/Equal.lean similarity index 95% rename from LeanSAT/Reflect/Tactics/Normalize/Equal.lean rename to LeanSAT/Tactics/Normalize/Equal.lean index 25f6f785..fdb68190 100644 --- a/LeanSAT/Reflect/Tactics/Normalize/Equal.lean +++ b/LeanSAT/Tactics/Normalize/Equal.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ -import LeanSAT.Reflect.Tactics.Attr +import LeanSAT.Tactics.Attr namespace BVDecide namespace Normalize diff --git a/LeanSAT/Reflect/Tactics/Normalize/Prop.lean b/LeanSAT/Tactics/Normalize/Prop.lean similarity index 91% rename from LeanSAT/Reflect/Tactics/Normalize/Prop.lean rename to LeanSAT/Tactics/Normalize/Prop.lean index b83c7a02..d32ac40f 100644 --- a/LeanSAT/Reflect/Tactics/Normalize/Prop.lean +++ b/LeanSAT/Tactics/Normalize/Prop.lean @@ -3,7 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ -import LeanSAT.Reflect.Tactics.Attr +import LeanSAT.Tactics.Attr namespace BVDecide namespace Normalize diff --git a/Main.lean b/Main.lean index 4211fc3c..2058b681 100644 --- a/Main.lean +++ b/Main.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.LRAT +import LeanSAT.Tactics.LRAT open LRAT diff --git a/Test/AIG/Stress.lean b/Test/AIG/Stress.lean index 4b4d5625..4583b2e7 100644 --- a/Test/AIG/Stress.lean +++ b/Test/AIG/Stress.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide -- Our benchmark terms are huge, no need to waste time on linting set_option linter.all false diff --git a/Test/Bv/Arith.lean b/Test/Bv/Arith.lean index d3a64282..eb8eaa31 100644 --- a/Test/Bv/Arith.lean +++ b/Test/Bv/Arith.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec diff --git a/Test/Bv/AxiomCheck.lean b/Test/Bv/AxiomCheck.lean index cf890b0f..8afd5a93 100644 --- a/Test/Bv/AxiomCheck.lean +++ b/Test/Bv/AxiomCheck.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec diff --git a/Test/Bv/Bitwise.lean b/Test/Bv/Bitwise.lean index 865f7414..557d8da1 100644 --- a/Test/Bv/Bitwise.lean +++ b/Test/Bv/Bitwise.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec diff --git a/Test/Bv/Cast.lean b/Test/Bv/Cast.lean index 718059c7..53d6764e 100644 --- a/Test/Bv/Cast.lean +++ b/Test/Bv/Cast.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec diff --git a/Test/Bv/Counterexample.lean b/Test/Bv/Counterexample.lean index 6ae88843..f43b570e 100644 --- a/Test/Bv/Counterexample.lean +++ b/Test/Bv/Counterexample.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec diff --git a/Test/Bv/Errors.lean b/Test/Bv/Errors.lean index 39554cb5..a8225154 100644 --- a/Test/Bv/Errors.lean +++ b/Test/Bv/Errors.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec diff --git a/Test/Bv/Inequality.lean b/Test/Bv/Inequality.lean index 4cb6260b..fdeccf58 100644 --- a/Test/Bv/Inequality.lean +++ b/Test/Bv/Inequality.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec diff --git a/Test/Bv/Sat.lean b/Test/Bv/Sat.lean index 7e0c18ce..8c494c9b 100644 --- a/Test/Bv/Sat.lean +++ b/Test/Bv/Sat.lean @@ -1,5 +1,5 @@ -import LeanSAT.Reflect.Tactics.BVDecide -import LeanSAT.Reflect.Tactics.BVTrace +import LeanSAT.Tactics.BVDecide +import LeanSAT.Tactics.BVTrace example (h : true = false) : False := by bv_decide example {x y z : Bool} (_ : (x && y) = z) (_ : x = !y) (_ : z = true) : False := by bv_decide diff --git a/Test/Bv/SatStress.lean b/Test/Bv/SatStress.lean index 53eafb04..42d74e8c 100644 --- a/Test/Bv/SatStress.lean +++ b/Test/Bv/SatStress.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide import Std.Data.HashMap import Std.Data.HashSet diff --git a/Test/Bv/Shift.lean b/Test/Bv/Shift.lean index dd48212c..f6961142 100644 --- a/Test/Bv/Shift.lean +++ b/Test/Bv/Shift.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec diff --git a/Test/Bv/Stress.lean b/Test/Bv/Stress.lean index 36f89e75..705f9fb3 100644 --- a/Test/Bv/Stress.lean +++ b/Test/Bv/Stress.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec set_option profiler true diff --git a/Test/Bv/Substructure.lean b/Test/Bv/Substructure.lean index 931c6151..01b57951 100644 --- a/Test/Bv/Substructure.lean +++ b/Test/Bv/Substructure.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVDecide +import LeanSAT.Tactics.BVDecide open BitVec diff --git a/Test/Bv/Trace.lean b/Test/Bv/Trace.lean index 8441f61f..6f53018b 100644 --- a/Test/Bv/Trace.lean +++ b/Test/Bv/Trace.lean @@ -1,4 +1,4 @@ -import LeanSAT.Reflect.Tactics.BVTrace +import LeanSAT.Tactics.BVTrace open BitVec