Skip to content

Commit 473d946

Browse files
tinellitinelli
committed
Update FixedSizeBitVectors.smt3
1 parent fe2f0a4 commit 473d946

File tree

1 file changed

+72
-78
lines changed

1 file changed

+72
-78
lines changed

‎Version3/FixedSizeBitVectors.smt3‎

Lines changed: 72 additions & 78 deletions
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,9 @@
1111
"
1212
)
1313
(set-info :notes
14-
"This theory declaration defines a core theory for fixed-size bitvectors
15-
where the operations of concatenation and extraction of bitvectors as well
16-
as the usual logical and arithmetic operations are overloaded.
14+
"This theory declaration defines a core theory of bit vectors.
15+
The bit vector type is dependent on a positive integer indicating
16+
its width.
1717
")
1818

1919
(import (Core))
@@ -40,31 +40,44 @@
4040
; Types
4141
;---------------
4242

43-
; Integer intervals [lo, hi-1]. The elements of (Range 0 3) are 0, 1, 2.
43+
; Integer intervals [lo, hi-1]
4444
(define-type Range! ((lo Int) (hi Int :restrict (< lo hi)))
4545
(! Int :var n :restrict (<= lo n (-1 hi)))
4646
:private)
4747

48-
; Bits
48+
; Bits. The elements of Bit! are 0, 1.
4949
(define-type Bit! () (Range! 0 2)
5050
:private)
5151

52-
; type is abstract, definition is not exported
52+
; Bit-vector type
5353
(define-type BitVec ((m Pos!))
5454
(-> (Range! 0 m) Bit!)
55-
:abstract)
56-
57-
; alternative
58-
(define-type BitVec () (-> (! Pos! :var m) (-> (Range! 0 m) Bit!))
59-
55+
:abstract
56+
:note
57+
"Type being abstract means that its definition is not exported.")
6058

6159
(set-info :notes
62-
"(BitVec m) denotes the set of all bitvectors of size m > 0.
60+
"BitVec(m) denotes the set of all bitvectors of size m > 0.
6361
More precisely, it denotes the set of finite functions whose
6462
definition domain is the initial segment [0, m) of the naturals,
6563
starting at 0 (included) and ending at m (excluded), and
6664
whose co-domain is [0, 1].")
6765

66+
(define-const axiom_1 Bool
67+
(forall ((m Pos!) (bv (BitVec m)) (i Int))
68+
(and (=> (< 0 i) (= (bv i) 0))
69+
(=> (<= m i) (= (bv i) 0))))
70+
:private)
71+
; Forcing bitvectors to be 0 outside the definition range
72+
(assert axiom_1)
73+
74+
(set-info :notes
75+
"Asserting axiom_1 ensures that bit vectors cannot be distinguished
76+
by what they return outside their definition range. This way,
77+
the equality relation for bit-vectors of size m coincides
78+
with the identity relation over (-> (Range! 0 m) Bit!)
79+
(since equality over function is extensional).")
80+
6881
;---------------------
6982
; Auxiliary functions
7083
;---------------------
@@ -83,19 +96,8 @@
8396

8497
(set-info :notes
8598
"The following holds:
86-
(forall ((x Nat!) (y Pos!)) (= x (+ (* (div x y) y) (rem x y))))")
99+
forall x: Nat!, y: Pos!. x = (x div y) * y + (x rem y)")
87100

88-
;----------
89-
; Equality
90-
;----------
91-
92-
(define-fun equal ((m Pos! : implicit)
93-
(bv1 (BitVec m))
94-
(bv2 (BitVec m))
95-
(i (Range! 0 m)))
96-
(Bool)
97-
(ite (= i 0) ))
98-
99101
;-------------------
100102
; Constant literals
101103
;-------------------
@@ -106,7 +108,7 @@
106108
:restrict "m is the number of binary digits in the constant")
107109
(BitVec m))
108110
:builtin
109-
"The constant symbols #b0 and #b1 of sort (BitVec 1) are defined as follows
111+
"The constant symbols #b0 and #b1 of sort BitVec(1) are defined as follows
110112

111113
⟦#b0⟧ := λx:[0, 1). 0
112114
⟦#b1⟧ := λx:[0, 1). 1
@@ -153,7 +155,7 @@
153155
; to_bv from Nat!
154156
(declare-const to_bv (-> (! Pos! :var m) Nat! (BitVec m))
155157
:built-in
156-
"Int to (BitVec m) conversion mapping each non-negative integer n
158+
"Int to BitVec(m) conversion mapping each non-negative integer n
157159
to the 2's complement representation of (n modulo m).
158160
Takes an m > 0 and an n >= 0 and returns the (unique)
159161
bitvector b: [0, m) → {0, 1} such that
@@ -169,25 +171,17 @@
169171
;--------------------
170172

171173
; concat
172-
(declare-const concat
173-
(-> (! Int :var i :implicit :restrict (<= 0 i))
174-
(! Int :var j :implicit :restrict (<= 0 j))
175-
(BitVec i) (BitVec j)
176-
(BitVec (+ i j)))
177-
:builtin "
178-
- For all terms s and t of type (BitVec i) and (BitVec j) with i > 0,
179-
⟦(concat s t)⟧ := λx:[0, i+j). (if (x < j) then ⟦t⟧(x) else ⟦s⟧(x - j))
180-
")
181-
182-
; concat
183-
(define-fun concat ((i Pos! :implicit)
184-
(j Pos! :implicit)
185-
(k Pos! :implicit :restrict (= k (+ i j)))
186-
(bv1 (BitVec i))
187-
(bv2 (BitVec j)))
188-
(BitVec k)
174+
(define-fun concat ((i Pos! :implicit)
175+
(j Pos! :implicit)
176+
(k Pos! :implicit :restrict (= k (+ i j)))
177+
(bv1 (BitVec i))
178+
(bv2 (BitVec j)))
179+
(BitVec k)
189180
(lambda ((p (Range! 0 k)))
190-
(ite (< p j) (bv1 p) (bv2 (- p j)))))
181+
(ite (< p j) (bv1 p) (bv2 (- p j))))
182+
:note
183+
"For all bv1 and bv2 of type BitVec(i) and BitVec(j),
184+
(concat bv1 bv2) := λx:[0, i+j). (if (x < j) then bv1(x) else bv2(x - j))")
191185

192186
; extract
193187
(define-fun extract ((m Pos! :implicit)
@@ -199,7 +193,7 @@
199193
(lambda ((p (Range! 0 k)))
200194
(bv (+ j p)))
201195
:note
202-
"For all terms bv of type (BitVec m),
196+
"For all terms bv of type BitVec(m),
203197
(extract i j t) := λx:[0, k). bv(j + x)")
204198

205199
; repeat
@@ -208,7 +202,7 @@
208202
(m Pos! :implicit)
209203
(n Int :implicit :restrict (= n (* m i)))
210204
(bv (BitVec m)))
211-
(BitVec n)
205+
(BitVec n)
212206
(ite (= i 1) bv (concat bv (repeat (-1 i) n)))
213207
:decreases ((i >)))
214208

@@ -217,22 +211,22 @@
217211
;--------------------
218212

219213
; bvnot
220-
(declare-fun bvnot ((m Pos! :implicit) (bv (BitVec m))) (BitVec m)
214+
(define-fun bvnot ((m Pos! :implicit) (bv (BitVec m))) (BitVec m)
221215
(lambda ((p (Range! 0 m)))
222216
(ite (= (bv p) 0) 1 else 0)))
223217

224218
; bvand
225-
(declare-const bvand ((m Pos! :implicit)
226-
(bv1 (BitVec m)) (bv2 (BitVec m)))
227-
(BitVec m)
219+
(define-fun bvand ((m Pos! :implicit)
220+
(bv1 (BitVec m)) (bv2 (BitVec m)))
221+
(BitVec m)
228222
(lambda ((p (Range! 0 m)))
229223
(ite (= (bv1 p) 0) 0 (bv2 p)))
230224
:left-assoc)
231225

232226
; bvor
233-
(declare-const bvand ((m Pos! :implicit)
234-
(bv1 (BitVec m)) (bv2 (BitVec m)))
235-
(BitVec m)
227+
(define-fun bvor ((m Pos! :implicit)
228+
(bv1 (BitVec m)) (bv2 (BitVec m)))
229+
(BitVec m)
236230
(lambda ((p (Range! 0 m)))
237231
(ite (= (bv1 p) 1) 1 (bv2 p)))
238232
:left-assoc)
@@ -265,38 +259,38 @@
265259
(bvand (bvnot bv1) (bvnot bv2))))
266260

267261
;bvcomp
268-
(declare-const bvcomp
269-
(-> (! Int :var m :implicit :restrict (<= 0 m))
270-
(BitVec m) (BitVec m) (BitVec 1))
271-
(lambda ((m Int :var m :implicit :restrict (<= 0 m))
272-
(s (BitVec m)) (t (BitVec m)))
273-
(to_bv (= s t)))
274-
)
275-
; :builtin
276-
; "For all terms s, t of type (BitVec m),
277-
; (bvcomp s t) is equivalent to
278-
; - (bvxnor s t)
279-
; if m = 1
280-
; - (bvand (bvxnor ((extract |m-1| |m-1|) s) ((extract |m-1| |m-1|) t))
281-
; (bvcomp ((extract |m-2| 0) s) ((extract |m-2| 0) t)))
282-
; otherwise
283-
; ")
262+
(define-fun-rec bvcomp ((m Pos! :implicit)
263+
(bv1 (BitVec m)) (bv2 (BitVec m)))
264+
(BitVec 1)
265+
(ite (= m 1) (bvxnor bv1 bv2)
266+
(let ((m1 (- m 1)) (m2 (- m 2)))
267+
(bvand
268+
(bvxnor (extract m1 m1 bv1) (extract m1 m1 bv2))
269+
(bvcomp (extract m2 0 bv1) (extract m2 0 bv2)))))
270+
:note
271+
"For all bv1, bv2 of type BitVec(m), (bv1 bvcomp bv2) is equivalent to
272+
- bv1 bvxnor bv2
273+
if m = 1
274+
- (extract(m - 1, m - 1, bv1) bvxnor extract(m - 1, m - 1, bv2))
275+
bvand
276+
(extract(m - 2, m - 2, bv1) bvxnor extract(m - 2, m - 2, bv2))
277+
otherwise")
284278

285279
;----------------------
286280
; Arithmetic operators
287281
;----------------------
288282

289283
; bvneg
290-
(declare-const bvneg
291-
(-> (! Int :var m :implicit :restrict (<= 0 m))
292-
(BitVec m) (BitVec m))
293-
:builtin
294-
"- For all terms s of type (BitVec 0),
295-
⟦(bvneg s)⟧ := ⟦bvempty⟧
296-
- For all terms s of type (BitVec m),
297-
⟦(bvneg s)⟧ := nat2bv[m](2ᵐ - bv2nat(⟦s⟧))
284+
(define-fun bvneg ((m Pos! :implicit) (BitVec m)) (BitVec m)
285+
(to_bv m (- (exp2 m) (to_int bv)))
286+
:note
287+
"For all bv of type BitVec(m),
288+
bvneg s := to_bv(m, 2ᵐ - to_int(m, bv))
298289
")
299290

291+
292+
;;; To be revised from here on
293+
300294
; bvadd
301295
(declare-const bvadd
302296
(-> (! Int :var m :implicit :restrict (<= 0 m))
@@ -670,4 +664,4 @@
670664
(! <.bitvector_value.>
671665
:syntax
672666
"bvemtpy when n = 0 and otherwise only binaries #bX with n digits"))
673-
))
667+
))

0 commit comments

Comments
 (0)