4.7 Vectors
A vector is a fixed-length (im)mutable array. Vectors may be concrete or symbolic, and they may be accessed using concrete or symbolic indices. A concrete vector supports constant-time access for concrete slot indices, and linear-time access for symbolic slot indices. A symbolic vector supports (worst-case) linear- and quadratic-time access for concrete and symbolic indices, respectively. Access time for symbolic vectors is given with respect to the longest possible concrete array to which any symbolic vector could evaluate under any solution?.
Like pairs and lists, immutable vectors are transparent immutable values: two such vectors are eq? if they have the same length and eq? contents. Mutable vectors are references rather than values, and two mutable vectors are eq? if and only if they point to the same array object. Two vectors (regardless of mutability) are equal? if they have the same length and equal? contents.
> (define v1 (vector 1 2 #f)) > (define v2 (vector 1 2 #f)) > (eq? v1 v2) #f
> (equal? v1 v2) #t
> (define v3 (vector-immutable 1 2 #f)) > (define v4 (vector-immutable 1 2 #f)) > (eq? v3 v4) #t
> (equal? v1 v3) #t
> (define-symbolic x y z n integer?) > (define xs (take (list x y z) n)) ; xs is a symbolic list. > (define vs (list->vector xs)) ; vs is a symbolic vector.
> (define sol (solve (begin (assert (< n 3)) (assert (= 4 (vector-ref vs (sub1 n))))))) > (evaluate n sol) 1
> (evaluate (list x y z) sol) '(4 0 0)
> (evaluate vs sol) '#(4)
> (evaluate xs sol) '(4)
4.7.1 Lifted Operations on Vectors
Vector Operations | vector?, vector, vector-immutable, vector-length, vector-ref, vector-set!, vector->list, list->vector, vector->immutable-vector, vector-fill!, vector-copy!, vector-append |
4.7.2 Additional Operations on Vectors
Rosette provides the following procedures for operating on vectors using bitvector indices and lengths. These procedures produce symbolic values that avoid casting their bitvector arguments to integers, leading to more efficiently solvable queries.
procedure
(vector-length-bv vec t) → bv?
vec : vector? t : (or/c bitvector? union?)
> (define-symbolic b boolean?) > (define xs (if b (vector 1 2) (vector 3 4 5 6))) > xs (union [b #(1 2)] [(! b) #(3 4 5 6)])
> (integer->bitvector (vector-length xs) (bitvector 4)) (integer->bitvector (ite b 2 4) (bitvector 4))
> (vector-length-bv xs (bitvector 4)) (ite b (bv #x2 4) (bv #x4 4))
procedure
(vector-ref-bv vec pos) → any/c
vec : vector? pos : bv?
> (define-symbolic p (bitvector 1)) > (define xs (vector 1 2 3 4)) ; Uses a cast and generates a redundant assertion on the range of p: > (vector-ref xs (bitvector->natural p))
(ite*
(⊢ (= 0 (bitvector->natural p)) 1)
(⊢ (= 1 (bitvector->natural p)) 2)
(⊢ (= 2 (bitvector->natural p)) 3)
(⊢ (= 3 (bitvector->natural p)) 4))
> (vc) (vc #t (&& (<= 0 (bitvector->natural p)) (< (bitvector->natural p) 4)))
> (clear-vc!) ; No cast and no redundant range assertion: > (vector-ref-bv xs p) (ite* (⊢ (bveq (bv #b0 1) p) 1) (⊢ (bveq (bv #b1 1) p) 2))
> (vc) (vc #t #t)
; But the range assertion is generated when needed: > (define-symbolic q (bitvector 4)) > (vector-ref-bv xs q)
(ite*
(⊢ (bveq (bv #x0 4) q) 1)
(⊢ (bveq (bv #x1 4) q) 2)
(⊢ (bveq (bv #x2 4) q) 3)
(⊢ (bveq (bv #x3 4) q) 4))
> (vc) (vc #t (bvult q (bv #x4 4)))
procedure
(vector-set!-bv vec pos val) → void?
vec : vector? pos : bv? val : any/c
> (define-symbolic p (bitvector 1)) > (define xs (vector 1 2 3 4)) ; Uses a cast and generates a redundant assertion on the range of p: > (vector-set! xs (bitvector->natural p) 5) > xs
(vector
(ite (= 0 (bitvector->natural p)) 5 1)
(ite (= 1 (bitvector->natural p)) 5 2)
(ite (= 2 (bitvector->natural p)) 5 3)
(ite (= 3 (bitvector->natural p)) 5 4))
> (vc) (vc #t (&& (<= 0 (bitvector->natural p)) (< (bitvector->natural p) 4)))
> (clear-vc!) ; No cast and no redundant range assertion: > (define xs (vector 1 2 3 4)) > (vector-set!-bv xs p 5) > xs (vector (ite (bveq (bv #b0 1) p) 5 1) (ite (bveq (bv #b1 1) p) 5 2) 3 4)
> (vc) (vc #t #t)
; But the range assertion is generated when needed: > (define-symbolic q (bitvector 4)) > (define xs (vector 1 2 3 4)) > (vector-set!-bv xs q 5) > xs
(vector
(ite (bveq (bv #x0 4) q) 5 1)
(ite (bveq (bv #x1 4) q) 5 2)
(ite (bveq (bv #x2 4) q) 5 3)
(ite (bveq (bv #x3 4) q) 5 4))
> (vc) (vc #t (bvult q (bv #x4 4)))