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

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

Data.SBV.Tools.Range

Contents

- Boundaries and ranges
- Computing valid ranges

Description

Single variable valid range detection.

Synopsis

- data Boundary a
  - = Unbounded
  - | Open a
  - | Closed a
- data Range a = Range (Boundary a) (Boundary a)
- ranges :: forall a. (Ord a, Num a, SymVal a, SatModel a, Metric a, SymVal (MetricSpace a), SatModel (MetricSpace a)) => (SBV a -> SBool) -> IO [Range a]
- rangesWith :: forall a. (Ord a, Num a, SymVal a, SatModel a, Metric a, SymVal (MetricSpace a), SatModel (MetricSpace a)) => SMTConfig -> (SBV a -> SBool) -> IO [Range a]

# Boundaries and ranges

data Boundary a Source #

A boundary value

Constructors

Unbounded | Unbounded
Open a | Exclusive of the point
Closed a | Inclusive of the point

data Range a Source #

A range is a pair of boundaries: Lower and upper bounds

Constructors

Range (Boundary a) (Boundary a) |

#### Instances

Instances details

Show a => Show (Range a) Source # | Show instance for `Range`
Instance details Defined in Data.SBV.Tools.Range Methods showsPrec :: Int -> Range a -> ShowS show :: Range a -> String showList :: [Range a] -> ShowS

# Computing valid ranges

ranges :: forall a. (Ord a, Num a, SymVal a, SatModel a, Metric a, SymVal (MetricSpace a), SatModel (MetricSpace a)) => (SBV a -> SBool) -> IO [Range a] Source #

Given a single predicate over a single variable, find the contiguous ranges over which the predicate is satisfied. SBV will make one call to the optimizer, and then as many calls to the solver as there are disjoint ranges that the predicate is satisfied over. (Linear in the number of ranges.) Note that the number of ranges is large, this can take a long time! Some examples:

    >>> ranges (\(_ :: SInteger) -> sFalse)
    []
    >>> ranges (\(_ :: SInteger) -> sTrue)
    [(-oo,oo)]
    >>> ranges (\(x :: SInteger) -> sAnd [x .<= 120, x .>= -12, x ./= 3])
    [[-12,3),(3,120]]
    >>> ranges (\(x :: SInteger) -> sAnd [x .<= 75, x .>= 5, x ./= 6, x ./= 67])
    [[5,6),(6,67),(67,75]]
    >>> ranges (\(x :: SInteger) -> sAnd [x .<= 75, x ./= 3, x ./= 67])
    [(-oo,3),(3,67),(67,75]]
    >>> ranges (\(x :: SReal) -> sAnd [x .> 3.2, x .<  12.7])
    [(3.2,12.7)]
    >>> ranges (\(x :: SReal) -> sAnd [x .> 3.2, x .<= 12.7])
    [(3.2,12.7]]
    >>> ranges (\(x :: SReal) -> sAnd [x .<= 12.7, x ./= 8])
    [(-oo,8.0),(8.0,12.7]]
    >>> ranges (\(x :: SReal) -> sAnd [x .>= 12.7, x ./= 15])
    [[12.7,15.0),(15.0,oo)]
    >>> ranges (\(x :: SInt8) -> sAnd [x .<= 7, x ./= 6])
    [[-128,6),(6,7]]
    >>> ranges $ \x -> x .> (0::SReal)
    [(0.0,oo)]
    >>> ranges $ \x -> x .< (0::SReal)
    [(-oo,0.0)]
    >>> ranges $ \(x :: SWord8) -> 2*x .== 4
    [[2,3),(129,130]]

rangesWith :: forall a. (Ord a, Num a, SymVal a, SatModel a, Metric a, SymVal (MetricSpace a), SatModel (MetricSpace a)) => SMTConfig -> (SBV a -> SBool) -> IO [Range a] Source #

Compute ranges, using the given solver configuration.