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)