blob: 0fb50f8cfa8a732942c82bdecb43d16b0824f78d (
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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
; "bitvec" is a term of type "sort"
(declare BitVec sort)
; bit type
(declare bit type)
(declare b0 bit)
(declare b1 bit)
; bit vector type
(declare bv type)
(declare bvn bv)
(declare bvc (! b bit (! v bv bv)))
; a bv constant term
(declare a_bv (! v bv (term BitVec)))
; calculate the length of a bitvector
(program bv_len ((v bv)) mpz
(match v
(bvn 0)
((bvc b v') (mp_add (bv_len v') 1))))
; a bv variable
(declare var_bv type)
; a bv variable term
(declare a_var_bv (! v var_bv (term BitVec)))
; bit vector operators
(define bvoper (! x (term BitVec)
(! y (term BitVec)
(term BitVec))))
(declare bvand bvoper)
(declare bvadd bvoper)
;....
; all bit-vector terms are mapped with "bv_atom" to:
; - a simply-typed term of type "var_bv", which is necessary for bit-blasting
; - a integer size
(declare bv_atom (! x (term BitVec) (! y var_bv (! n mpz type))))
(declare decl_bv_atom_var (! n mpz ; must be specified
(! x var_bv
(! p (! u (bv_atom (a_var_bv x) x n)
(holds cln))
(holds cln)))))
(declare decl_bv_atom_const (! n mpz
(! v bv
(! s (^ (bv_len v) n)
(! p (! w var_bv
(! u (bv_atom (a_bv v) w n)
(holds cln)))
(holds cln))))))
; other terms here?
; bit blasted terms
(declare bblt type)
(declare bbltn bblt)
(declare bbltc (! f formula (! v bblt bblt)))
; (bblast_term x y) means term x corresponds to bit level interpretation y
(declare bblast_term (! x (term BitVec) (! y bblt formula)))
; a predicate to represent the n^th bit of a bitvector term
(declare bblast (! x var_bv (! n mpz formula)))
; bit blast constant
(program bblast_const ((v bv) (n mpz)) bblt
(mp_ifneg n (match v (bvn bbltn)
(default (fail bblt)))
(match v ((bvc b v') (bbltc (match b (b0 false) (b1 true)) (bblast_const v' (mp_add n (~ 1)))))
(default (fail bblt)))))
(declare bv_bbl_const (! n mpz
(! v bv
(! x var_bv
(! f bblt
(! u (bv_atom (a_bv v) x n)
(! c (^ (bblast_const v (mp_add n (~ 1))) f)
(th_holds (bblast_term (a_bv v) f)))))))))
; bit blast variable
(program bblast_var ((x var_bv) (n mpz)) bblt
(mp_ifneg n bbltn
(bbltc (bblast x n) (bblast_var x (mp_add n (~ 1))))))
(declare bv_bbl_var (! n mpz
(! x var_bv
(! f bblt
(! u (bv_atom (a_var_bv x) x n)
(! c (^ (bblast_var x (mp_add n (~ 1))) f)
(th_holds (bblast_term (a_var_bv x) f))))))))
; bit blast x = y
; for x,y of size n, it will return a conjuction (x.{n-1} = y.{n-1} ^ ( ... ^ (x.0 = y.0 ^ true)))
(program bblast_eq ((x bblt) (y bblt)) formula
(match x
(bbltn (match y (bbltn true) (default (fail formula))))
((bbltc fx x') (match y
(bbltn (fail formula))
((bbltc fy y') (and (iff fx fy) (bblast_eq x' y')))))))
(declare bv_bbl_eq (! x (term BitVec)
(! y (term BitVec)
(! fx bblt
(! fy bblt
(! f formula
(! ux (th_holds (bblast_term x fx))
(! uy (th_holds (bblast_term y fy))
(! c (^ (bblast_eq fx fy) f)
(th_holds (impl (= BitVec x y) f)))))))))))
; rewrite rule :
; x + y = y + x
(declare bvadd_symm (! x (term BitVec)
(! y (term BitVec)
(! x' var_bv
(! y' var_bv
(! n mpz
(! ux (bv_atom x x' n)
(! uy (bv_atom y y' n)
(th_holds (= BitVec (bvadd x y) (bvadd y x)))))))))))
; necessary?
(program calc_bvand ((a bv) (b bv)) bv
(match a
(bvn (match b (bvn bvn) (default (fail bv))))
((bvc ba a') (match b
((bvc bb b') (bvc (match ba (b0 b0) (b1 bb)) (calc_bvand a' b')))
(default (fail bv))))))
; rewrite rule (w constants) :
; a & b = c
(declare bvand_const (! c bv
(! a bv
(! b bv
(! u (^ (calc_bvand a b) c)
(th_holds (= BitVec (bvand (a_bv a) (a_bv b)) (a_bv c))))))))
|
