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

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Data.SBV.Tools.BoundedList

Contents

- General folds
- Map, filter, zipWith, elem
- Aggregates
- Miscellaneous: Reverse and sort

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

- bfoldr :: (SymVal a, SymVal b) => Int -> (SBV a -> SBV b -> SBV b) -> SBV b -> SList a -> SBV b
- 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)
- bfoldl :: (SymVal a, SymVal b) => Int -> (SBV b -> SBV a -> SBV b) -> SBV b -> SList a -> SBV b
- 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)
- bmap :: (SymVal a, SymVal b) => Int -> (SBV a -> SBV b) -> SList a -> SList b
- bmapM :: (SymVal a, SymVal b, Monad m, Mergeable (m (SBV [b]))) => Int -> (SBV a -> m (SBV b)) -> SList a -> m (SList b)
- bfilter :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SList a
- bzipWith :: (SymVal a, SymVal b, SymVal c) => Int -> (SBV a -> SBV b -> SBV c) -> SList a -> SList b -> SList c
- belem :: (Eq a, SymVal a) => Int -> SBV a -> SList a -> SBool
- bsum :: (SymVal a, Num a, Ord a) => Int -> SList a -> SBV a
- bprod :: (SymVal a, Num a, Ord a) => Int -> SList a -> SBV a
- band :: Int -> SList Bool -> SBool
- bor :: Int -> SList Bool -> SBool
- bany :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SBool
- ball :: SymVal a => Int -> (SBV a -> SBool) -> SList a -> SBool
- bmaximum :: (Ord a, SymVal a) => Int -> SList a -> SBV a
- bminimum :: (Ord a, SymVal a) => Int -> SList a -> SBV a
- breverse :: SymVal a => Int -> SList a -> SList a
- bsort :: (Ord a, SymVal a) => Int -> SList a -> SList a

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

Bounded monadic map.

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.

band :: Int -> SList Bool -> SBool Source #

Bounded logical and

bor :: Int -> SList Bool -> SBool Source #

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