forked from hargoniX/Leanwuzla
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Bitwuzla.lean
79 lines (64 loc) · 2.1 KB
/
Bitwuzla.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
/-
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 Leanwuzla
variable (a b c : Bool)
variable (x y z : BitVec 32)
/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
#guard_msgs in
example : x + y = y + x := by
bv_bitwuzla
/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
#guard_msgs in
example : x - 1 ≠ x := by
bv_bitwuzla
/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
#guard_msgs in
example : (-x) + y = y - x:= by
bv_bitwuzla
/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
#guard_msgs in
example : x * y = y * x := by
bv_bitwuzla
/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
#guard_msgs in
example : x / y ≤ x := by
bv_bitwuzla
/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
#guard_msgs in
example (hx : BitVec.slt 0 x) (hy : BitVec.slt 0 y) : x.msb = y.msb := by
bv_bitwuzla
/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
#guard_msgs in
example : (x.zeroExtend 64).msb = false := by
bv_bitwuzla
/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
#guard_msgs in
example (hx : BitVec.slt 0 x) : (x.signExtend 64).msb = false := by
bv_bitwuzla
/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
#guard_msgs in
example : x &&& y = y &&& x := by
bv_bitwuzla
/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
#guard_msgs in
example : x ||| y = y ||| x := by
bv_bitwuzla
/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
#guard_msgs in
example : ~~~(x ||| y) = (~~~y &&& ~~~x) := by
bv_bitwuzla
/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
#guard_msgs in
example : x <<< 32 = 0 := by
bv_bitwuzla
/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
#guard_msgs in
example : x >>> x = 0 := by
bv_bitwuzla
/-- error: Bitwuzla thinks it's right but can't trust the wuzla! -/
#guard_msgs in
example : (x ++ x).extractLsb' 0 32 = x := by
bv_bitwuzla