4.6 Pairs and Lists
A pair combines two values, and a list is either the constant null or a pair whose second element is a list. Pairs and lists are transparent immutable values, and they may be concrete or symbolic. Two pairs or two lists are eq? (resp. equal?) if their corresponding elements are eq? (resp. equal?).
As values of unsolvable types, symbolic pairs and lists cannot be created via define-symbolic[*]. Instead, they are created by applying pair- or list-producing procedures to symbolic inputs, or by controlling the application of such procedures with symbolic values. This pattern for creating non-primitive symbolic values generalizes to all unsolvable datatypes.
> (define-symbolic x y z n integer?) > (define xs (take (list x y z) n)) ; (1) xs is a symbolic list. > (define sol (solve (assert (null? xs)))) > (evaluate xs sol) '()
> (define sol (solve (begin (assert (= (length xs) 2)) (assert (not (equal? xs (reverse xs)))) (assert (equal? xs (sort xs <)))))) > (evaluate xs sol) '(-1 0)
> (define-symbolic b boolean?) > (define p (if b (cons 1 2) (cons 4 #f))) ; (2) p is a symbolic pair. > (define sol (solve (assert (boolean? (cdr p))))) > (evaluate p sol) '(4 . #f)
> (define sol (solve (assert (odd? (car p))))) > (evaluate p sol) '(1 . 2)
4.6.1 Lifted Operations on Pairs and Lists
Pair Operations | |
List Operations | |
List Iteration | |
List Filtering | |
List Searching | |
Additional Pair Operations | caar, cadr, cdar, cddr, caaar, caadr, cadar, caddr, cdaar, cdadr, cddar, cdddr, caaaar, caaadr, caadar, caaddr, cadaar, cadadr, caddar, cadddr, cdaaar, cdaadr, cdadar, cdaddr, cddaar, cddadr, cdddar, cddddr |
Additional List Operations | cons?, empty?, first, rest, second, third, fourth, fifth, sixth, seventh, eighth, ninth, tenth, last, last-pair, take, drop, split-at, take-right, drop-right, split-at-right, add-between, append*, flatten, remove-duplicates, filter-map, count, partition, append-map, filter-not, shuffle, argmin, argmax, list-set |
4.6.2 Additional Operations on Pairs and Lists
Rosette provides the following procedures for operating on lists using bitvector indices and lengths. These procedures produce symbolic values that avoid casting their bitvector arguments to integers, leading to more efficiently solvable queries.
> (define-symbolic b boolean?) > (define xs (if b '(1 2) '(3 4 5 6))) > xs (union [b (1 2)] [(! b) (3 4 5 6)])
> (integer->bitvector (length xs) (bitvector 4)) (integer->bitvector (ite b 2 4) (bitvector 4))
> (length-bv xs (bitvector 4)) (ite b (bv #x2 4) (bv #x4 4))
procedure
(list-ref-bv lst pos) → any/c
lst : list? pos : bv?
> (define-symbolic p (bitvector 1)) > (define xs '(1 2 3 4)) ; Uses a cast and generates a redundant assertion on the range of p: > (list-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: > (list-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)) > (list-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
(list-set-bv lst pos val) → list?
lst : list? pos : bv? val : any/c
> (define-symbolic p (bitvector 1)) > (define xs '(1 2 3 4)) ; Uses a cast and generates a redundant assertion on the range of p: > (list-set xs (bitvector->natural p) 5)
(list
(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: > (list-set-bv xs p 5) (list (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)) > (list-set-bv xs q 5)
(list
(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)))
procedure
lst : any/c pos : bv? (take-right-bv lst pos) → any/c lst : any/c pos : bv? (drop-bv lst pos) → any/c lst : any/c pos : bv? (drop-right-bv lst pos) → list? lst : any/c pos : bv? (list-tail-bv lst pos) → any/c lst : any/c pos : bv?
> (define-symbolic p (bitvector 1)) > (define xs (cons 1 (cons 2 (cons 3 4)))) ; Uses a cast and generates a redundant assertion on the range of p: > (take xs (bitvector->natural p))
(union
[(= 0 (bitvector->natural p)) ()]
[(= 1 (bitvector->natural p)) (1)]
[(= 2 (bitvector->natural p)) (1 2)]
[(= 3 (bitvector->natural p)) (1 2 3)])
> (vc) (vc #t (&& (<= 0 (bitvector->natural p)) (< (bitvector->natural p) 4)))
> (clear-vc!) ; No cast and no redundant range assertion: > (take-bv xs p) (union [(bveq (bv #b0 1) p) ()] [(bveq (bv #b1 1) p) (1)])
> (vc) (vc #t #t)
; But the range assertion is generated when needed: > (define-symbolic q (bitvector 4)) > (take-bv xs q)
(union
[(bveq (bv #x0 4) q) ()]
[(bveq (bv #x1 4) q) (1)]
[(bveq (bv #x2 4) q) (1 2)]
[(bveq (bv #x3 4) q) (1 2 3)])
> (vc) (vc #t (bvule q (bv #x3 4)))
procedure
(split-at-bv lst pos) → (list? any/c)
lst : any/c pos : bv? (split-at-right-bv lst pos) → (list? any/c) lst : any/c pos : bv?
> (define-symbolic p (bitvector 1)) > (define xs (cons 1 2)) ; Uses a cast and generates a redundant assertion on the range of p: > (split-at xs (bitvector->natural p))
(union [(= 0 (bitvector->natural p)) ()] [(= 1 (bitvector->natural p)) (1)])
(union [(= 0 (bitvector->natural p)) (1 . 2)] [(= 1 (bitvector->natural p)) 2])
> (vc) (vc #t (&& (<= 0 (bitvector->natural p)) (< (bitvector->natural p) 2)))
> (clear-vc!) ; No cast and no redundant range assertion: > (split-at-bv xs p)
(union [(bveq (bv #b0 1) p) ()] [(bveq (bv #b1 1) p) (1)])
(union [(bveq (bv #b0 1) p) (1 . 2)] [(bveq (bv #b1 1) p) 2])
> (vc) (vc #t #t)
; But the range assertion is generated when needed: > (define-symbolic q (bitvector 4)) > (split-at-bv xs q)
(union [(bveq (bv #x0 4) q) ()] [(bveq (bv #x1 4) q) (1)])
(union [(bveq (bv #x0 4) q) (1 . 2)] [(bveq (bv #x1 4) q) 2])
> (vc) (vc #t (bvule q (bv #x1 4)))