| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Tools.Range
Description
Single variable valid range detection.
Synopsis
- data Boundary a
- data Range a = Range (Boundary a) (Boundary a)
- ranges :: forall a. (Num a, SymWord a, SMTValue a, SatModel a, Metric (SBV a)) => (SBV a -> SBool) -> IO [Range a]
- rangesWith :: forall a. (Num a, SymWord a, SMTValue a, SatModel a, Metric (SBV a)) => SMTConfig -> (SBV a -> SBool) -> IO [Range a]
Boundaries and ranges
A boundary value
A range is a pair of boundaries: Lower and upper bounds
Computing valid ranges
ranges :: forall a. (Num a, SymWord a, SMTValue a, SatModel a, Metric (SBV 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) -> false)[]>>>ranges (\(_ :: SInteger) -> true)[(-oo,oo)]>>>ranges (\(x :: SInteger) -> bAnd [x .<= 120, x .>= -12, x ./= 3])[[-12,3),(3,120]]>>>ranges (\(x :: SInteger) -> bAnd [x .<= 75, x .>= 5, x ./= 6, x ./= 67])[[5,6),(6,67),(67,75]]>>>ranges (\(x :: SInteger) -> bAnd [x .<= 75, x ./= 3, x ./= 67])[(-oo,3),(3,67),(67,75]]>>>ranges (\(x :: SReal) -> bAnd [x .> 3.2, x .< 12.7])[(3.2,12.7)]>>>ranges (\(x :: SReal) -> bAnd [x .> 3.2, x .<= 12.7])[(3.2,12.7]]>>>ranges (\(x :: SReal) -> bAnd [x .<= 12.7, x ./= 8])[(-oo,8.0),(8.0,12.7]]>>>ranges (\(x :: SReal) -> bAnd [x .>= 12.7, x ./= 15])[[12.7,15.0),(15.0,oo)]>>>ranges (\(x :: SInt8) -> bAnd [x .<= 7, x ./= 6])[[-128,6),(6,7]]>>>ranges $ \x -> x .> (0::SReal)[(0.0,oo)]>>>ranges $ \x -> x .< (0::SReal)[(-oo,0.0)]