sbv-8.6: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Data.SBV.Tools.BoundedList

Description

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.

Synopsis

# General folds

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

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) Source #

Bounded monadic fold from the right.

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

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) Source #

Bounded monadic fold from the left.

# Map, filter, zipWith, elem

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

Bounded map.

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

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

Bounded filter.

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

Bounded zipWith

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

Bounded element check

# Aggregates

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

Bounded sum.

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

Bounded product.

Bounded logical and

Bounded logical or

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

Bounded any

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

Bounded all

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

Bounded maximum. Undefined if list is empty.

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

Bounded minimum. Undefined if list is empty.

# Miscellaneous: Reverse and sort

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

Bounded reverse

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

Bounded insertion sort