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.

Examples:

> (define-symbolic xyzninteger? )
> (define xs(take (list xyz)n));(1) xs is a symbolic list.
> (define sol(solve (assert (null? xs))))
> (evaluate xssol)

'()

> (define sol
(solve (begin
(assert (= (length xs)2))
(assert (not (equal? xs(reverse xs))))
(assert (equal? xs(sort xs< ))))))
> (evaluate xssol)

'(-1 0)

Examples:

> (define-symbolic bboolean? )
> (define p(if b(cons 12)(cons 4#f)));(2) p is a symbolic pair.
> (define sol(solve (assert (boolean? (cdr p)))))
> (evaluate psol)

'(4 . #f)
> (define sol(solve (assert (odd? (car p)))))
> (evaluate psol)

'(1 . 2)

4.6.1Lifted Operations on Pairs and Lists🔗 i

Rosette lifts the following operations on pairs and lists:

Pair Operations

pair? , null? , cons , car , cdr , null , list? , list

List Operations

length , list-ref , list-tail , append , reverse

List Iteration

map , andmap , ormap , for-each , foldl , foldr

List Filtering

filter , remove , remq , remove* , remq* , sort

List Searching

member , memq , memf , findf , assoc , assq , assf

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.2Additional Operations on Pairs and Lists🔗 i

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.

procedure
( length-bv lstt)→bv?
lst:list?
t:(or/c bitvector? union? )

Equivalent to (integer->bitvector (length lst)t) but avoids the integer->bitvector cast for better solving performance.

Examples:

> (define-symbolic bboolean? )
> (define xs(if b'(12)'(3456)))
> 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 lstpos)→any/c
lst:list?
pos:bv?

Equivalent to (list-ref lst(bitvector->natural pos)) but avoids the bitvector->natural cast for better solving performance.

Examples:

> (define-symbolic p(bitvector 1))
> (define xs'(1234))
;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 xsp)

(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 xsq)

(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 lstposval)→list?
lst:list?
pos:bv?
val:any/c

Equivalent to (list-set lst(bitvector->natural pos)val) but avoids the bitvector->natural cast for better solving performance.

Examples:

> (define-symbolic p(bitvector 1))
> (define xs'(1234))
;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 xsp5)

(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 xsq5)

(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
( take-bv lstpos)→list?
lst:any/c
pos:bv?
( take-right-bv lstpos)→any/c
lst:any/c
pos:bv?
( drop-bv lstpos)→any/c
lst:any/c
pos:bv?
( drop-right-bv lstpos)→list?
lst:any/c
pos:bv?
( list-tail-bv lstpos)→any/c
lst:any/c
pos:bv?

Equivalent to take , take-right , drop , drop-right , or list-tail applied to lst and (bitvector->natural pos), but avoids the bitvector->natural cast for better solving performance.

Examples:

> (define-symbolic p(bitvector 1))
> (define xs(cons 1(cons 2(cons 34))))
;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 xsp)

(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 xsq)

(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 lstpos)→(list? any/c )
lst:any/c
pos:bv?
( split-at-right-bv lstpos)→(list? any/c )
lst:any/c
pos:bv?

Equivalent to (split-at lst(bitvector->natural pos)) or (split-at-right lst(bitvector->natural pos)), but avoids the bitvector->natural cast for better solving performance.

Examples:

> (define-symbolic p(bitvector 1))
> (define xs(cons 12))
;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 xsp)

(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 xsq)

(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)))

top ← prev up next →