blob: e8d2382d88e5fbdba26ea9e1e61e02dd3d3a0340 (
plain)
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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
(declare trusted_formula_rewrite
(! x formula
(! y formula
(! u (th_holds (iff x y))
(! z formula
(th_holds (iff x z)))))))
(declare trusted_term_rewrite
(! s sort
(! x (term s)
(! y (term s)
(! u (th_holds (= s x y))
(! z (term s)
(th_holds (= s x z))))))))
; TODO: Side condition that checks the evaluation
(declare const_eval_f
(! x formula
(! y formula
(! u (th_holds (iff x y))
(! z formula
(th_holds (iff x z)))))))
(declare symm_equal
(! s sort
(! x (term s)
(! y (term s)
(! z (term s)
(! w (term s)
(! u1 (th_holds (= s x y))
(! u2 (th_holds (= s z w))
(th_holds (iff (= s x z) (= s y w)))))))))))
; Apply a unary operator to the original and the rewritten formula
(declare symm_formula_op1
(! op formula_op1
(! x formula
(! y formula
(! u (th_holds (iff x y))
(th_holds (iff (op x) (op y))))))))
; Apply a binary operator to the original and the rewritten formulas
(declare symm_formula_op2
(! op formula_op2
(! x formula
(! y formula
(! z formula
(! w formula
(! u1 (th_holds (iff x z))
(! u2 (th_holds (iff y w))
(th_holds (iff (op x y) (op z w)))))))))))
(declare symm_bvpred
(! op bvpred
(! n mpz
(! x (term (BitVec n))
(! y (term (BitVec n))
(! z (term (BitVec n))
(! w (term (BitVec n))
(! u1 (th_holds (= (BitVec n) x z))
(! u2 (th_holds (= (BitVec n) y w))
(th_holds (iff (op n x y) (op n z w))))))))))))
(declare neg_idemp
(! n mpz
(! lhs (term (BitVec n))
(! y (term (BitVec n))
(! u (th_holds (= (BitVec n) lhs (bvneg _ (bvneg _ y))))
(th_holds (= _ lhs y)))))))
(declare reflexivity_eq
(! n mpz
(! x formula
(! y (term (BitVec n))
(! u (th_holds (iff x (= (BitVec n) y y)))
(th_holds (iff x true)))))))
(declare ult_zero
(! n mpz
(! bv0_n bv
(! original formula
(! x (term (BitVec n))
(! u (th_holds (iff original (bvult _ x (a_bv _ bv0_n))))
(th_holds (iff original false))))))))
(declare zero_extend_n_z
(! zeamount mpz
(! zebv mpz
(! n mpz
(! m mpz
(! original (term (BitVec n))
(! m (term (BitVec n))
(! x (term (BitVec n))
(! u (th_holds (= _ original (zero_extend zebv m _ x)))
(th_holds (= _ original (concat _ (a_bv _ bv0_m) x))))))))))))
(declare t_eq_n_f (th_holds (iff true (not false))))
|
