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