Data.SBV.Tools.BoundedList

A collection of bounded list utilities, useful when working with symbolic lists. These functions all take a concrete bound, and operate on the prefix of a symbolic list that is at most that long. Due to limitations on writing recursive functions over lists (the classic symbolic termination problem), we cannot write arbitrary recursive programs on symbolic lists. But most of the time all we need is a bounded prefix of this list, at which point these functions come in handy.

General folds

bfoldr :: (SymVal a, SymVal b) => Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b

Bounded fold from the right.

bfoldrM :: forall a b m. (SymVal a, SymVal b, Monad m, Mergeable (m (SBV b))) => Int -> (SBV a -> SBV b -> m (SBV b)) -> SBV b -> SList a -> m (SBV b)

Bounded monadic fold from the right.

bfoldl :: (SymVal a, SymVal b) => Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b

Bounded fold from the left.

bfoldlM :: forall a b m. (SymVal a, SymVal b, Monad m, Mergeable (m (SBV b))) => Int -> (SBV b -> SBV a -> m (SBV b)) -> SBV b -> SList a -> m (SBV b)

Bounded monadic fold from the left.

Map, filter, zipWith, elem

bmap :: (SymVal a, SymVal b) => Int -> (SBV a -> SBV b) -> SList a -> SList b

Bounded map.

bmapM :: (SymVal a, SymVal b, Monad m, Mergeable (m (SBV [b]))) => Int -> (SBV a -> m (SBV b)) -> SList a -> m (SList b)

Bounded monadic map.

bfilter :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SList a

Bounded filter.

bzipWith :: (SymVal a, SymVal b, SymVal c) => Int -> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c

Bounded zipWith

belem :: (Eq a, SymVal a) => Int -> SBV a -> SList a -> SBool

Bounded element check

Aggregates

bsum :: (SymVal a, Num a, Ord a) => Int -> SList a -> SBV a

Bounded sum.

bprod :: (SymVal a, Num a, Ord a) => Int -> SList a -> SBV a

Bounded product.

band :: Int -> SList Bool -> SBool

Bounded logical and

bor :: Int -> SList Bool -> SBool

Bounded logical or

bany :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SBool

Bounded any

ball :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SBool

Bounded all

bmaximum :: (Ord a, SymVal a) => Int -> SList a -> SBV a

Bounded maximum. Undefined if list is empty.

bminimum :: (Ord a, SymVal a) => Int -> SList a -> SBV a

Bounded minimum. Undefined if list is empty.

Miscellaneous: Reverse and sort

breverse :: SymVal a => Int -> SList a -> SList a

Bounded reverse

bsort :: (Ord a, SymVal a) => Int -> SList a -> SList a

Bounded insertion sort