what4-1.6.3: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc 2021
License | BSD3
Maintainer | Rob Dockins <rdockins@galois.com>
Safe Haskell | None
Language | Haskell2010

What4.SpecialFunctions

Contents

- Representation of special functions
  - Symmetry properties of special functions
  - Packaging arguments to special functions
  - Interval data for domain and range

Description

Utilties for representing and handling certain "special" functions arising from analysis. Although many of these functions are most properly understood as complex valued functions on complex arguments, here we are primarily interested in their restriction to real-valued functions or their floating-point approximations.

The functions considered here include functions from standard and hyperbolic trigonometry, exponential and logarithmic functions, etc. Some of these functions are defineable in terms of others (e.g. `tan(x) = sin(x)/cos(x)` or expm1(x) = exp(x) - 1@) but are commonly implemented separately in math libraries for increased precision. Some popular constant values are also included.

Synopsis

- data R
- data SpecialFunction (args :: Ctx Type) where
  - Pi :: SpecialFunction ('EmptyCtx :: Ctx Type)
  - HalfPi :: SpecialFunction ('EmptyCtx :: Ctx Type)
  - QuarterPi :: SpecialFunction ('EmptyCtx :: Ctx Type)
  - OneOverPi :: SpecialFunction ('EmptyCtx :: Ctx Type)
  - TwoOverPi :: SpecialFunction ('EmptyCtx :: Ctx Type)
  - TwoOverSqrt_Pi :: SpecialFunction ('EmptyCtx :: Ctx Type)
  - Sqrt_2 :: SpecialFunction ('EmptyCtx :: Ctx Type)
  - Sqrt_OneHalf :: SpecialFunction ('EmptyCtx :: Ctx Type)
  - E :: SpecialFunction ('EmptyCtx :: Ctx Type)
  - Log2_E :: SpecialFunction ('EmptyCtx :: Ctx Type)
  - Log10_E :: SpecialFunction ('EmptyCtx :: Ctx Type)
  - Ln_2 :: SpecialFunction ('EmptyCtx :: Ctx Type)
  - Ln_10 :: SpecialFunction ('EmptyCtx :: Ctx Type)
  - Sin :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Cos :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Tan :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Arcsin :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Arccos :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Arctan :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Sinh :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Cosh :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Tanh :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Arcsinh :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Arccosh :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Arctanh :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Hypot :: SpecialFunction (((EmptyCtx :: Ctx Type) ::> R) '::> R)
  - Arctan2 :: SpecialFunction (((EmptyCtx :: Ctx Type) ::> R) '::> R)
  - Pow :: SpecialFunction (((EmptyCtx :: Ctx Type) ::> R) '::> R)
  - Exp :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Log :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Expm1 :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Log1p :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Exp2 :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Log2 :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Exp10 :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
  - Log10 :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R)
- data FunctionSymmetry (r :: k)
  - = NoSymmetry
  - | EvenFunction
  - | OddFunction
- specialFnSymmetry :: forall (args :: Ctx Type). SpecialFunction args -> Assignment (FunctionSymmetry :: Type -> Type) args
- data SpecialFnArg (e :: k -> Type) (tp :: k) r where
  - SpecialFnArg :: forall {k} (e :: k -> Type) (tp :: k). e tp -> SpecialFnArg e tp R
- traverseSpecialFnArg :: forall {k} m e (tp :: k) f r. Applicative m => (e tp -> m (f tp)) -> SpecialFnArg e tp r -> m (SpecialFnArg f tp r)
- newtype SpecialFnArgs (e :: k -> Type) (tp :: k) (args :: Ctx Type) = SpecialFnArgs (Assignment (SpecialFnArg e tp) args)
- traverseSpecialFnArgs :: forall {k} m e (tp :: k) f (r :: Ctx Type). Applicative m => (e tp -> m (f tp)) -> SpecialFnArgs e tp r -> m (SpecialFnArgs f tp r)
- data RealPoint
  - = Zero
  - | NegOne
  - | PosOne
  - | NegInf
  - | PosInf
  - | NegPi
  - | PosPi
  - | NegHalfPi
  - | PosHalfPi
- data RealBound
  - = Incl RealPoint
  - | Excl RealPoint
- data RealInterval r where
  - RealPoint :: SpecialFunction (EmptyCtx :: Ctx Type) -> RealInterval R
  - RealInterval :: RealBound -> RealBound -> RealInterval R
- specialFnDomain :: forall (args :: Ctx Type). SpecialFunction args -> Assignment RealInterval args
- specialFnRange :: forall (args :: Ctx Type). SpecialFunction args -> RealInterval R

# Representation of special functions

data R Source #

Phantom data index representing the real number line. Used for specifying the arity of special functions.

data SpecialFunction (args :: Ctx Type) where Source #

Data type for representing "special" functions. These include functions from standard and hyperbolic trigonometry, exponential and logarithmic functions, as well as other well-known mathematical functions.

Generally, little solver support exists for such functions (although systems like dReal and Metatarski can prove some properties). Nonetheless, we may have some information about specific values these functions take, the domains on which they are defined, or the range of values their outputs may take, or specific relationships that may exists between these functions (e.g., trig identities). This information may, in some circumstances, be sufficent to prove properties of interest, even if the functions cannot be represented in their entirety.

Constructors

Pi :: SpecialFunction ('EmptyCtx :: Ctx Type) |
HalfPi :: SpecialFunction ('EmptyCtx :: Ctx Type) |
QuarterPi :: SpecialFunction ('EmptyCtx :: Ctx Type) |
OneOverPi :: SpecialFunction ('EmptyCtx :: Ctx Type) |
TwoOverPi :: SpecialFunction ('EmptyCtx :: Ctx Type) |
TwoOverSqrt_Pi :: SpecialFunction ('EmptyCtx :: Ctx Type) |
Sqrt_2 :: SpecialFunction ('EmptyCtx :: Ctx Type) |
Sqrt_OneHalf :: SpecialFunction ('EmptyCtx :: Ctx Type) |
E :: SpecialFunction ('EmptyCtx :: Ctx Type) |
Log2_E :: SpecialFunction ('EmptyCtx :: Ctx Type) |
Log10_E :: SpecialFunction ('EmptyCtx :: Ctx Type) |
Ln_2 :: SpecialFunction ('EmptyCtx :: Ctx Type) |
Ln_10 :: SpecialFunction ('EmptyCtx :: Ctx Type) |
Sin :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Cos :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Tan :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Arcsin :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Arccos :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Arctan :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Sinh :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Cosh :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Tanh :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Arcsinh :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Arccosh :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Arctanh :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Hypot :: SpecialFunction (((EmptyCtx :: Ctx Type) ::> R) '::> R) |
Arctan2 :: SpecialFunction (((EmptyCtx :: Ctx Type) ::> R) '::> R) |
Pow :: SpecialFunction (((EmptyCtx :: Ctx Type) ::> R) '::> R) |
Exp :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Log :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Expm1 :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Log1p :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Exp2 :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Log2 :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Exp10 :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |
Log10 :: SpecialFunction ((EmptyCtx :: Ctx Type) '::> R) |

#### Instances

Instances details

Show (SpecialFunction args) Source # |
Instance details Defined in What4.SpecialFunctions Methods showsPrec :: Int -> SpecialFunction args -> ShowS Source # show :: SpecialFunction args -> String Source # showList :: [SpecialFunction args] -> ShowS Source #
Eq (SpecialFunction args) Source # |
Instance details Defined in What4.SpecialFunctions Methods (==) :: SpecialFunction args -> SpecialFunction args -> Bool Source # (/=) :: SpecialFunction args -> SpecialFunction args -> Bool Source #
Hashable (SpecialFunction args) Source # |
Instance details Defined in What4.SpecialFunctions Methods hashWithSalt :: Int -> SpecialFunction args -> Int Source # hash :: SpecialFunction args -> Int Source #
TestEquality SpecialFunction Source # |
Instance details Defined in What4.SpecialFunctions Methods testEquality :: forall (a :: Ctx Type) (b :: Ctx Type). SpecialFunction a -> SpecialFunction b -> Maybe (a :~: b) Source #
HashableF SpecialFunction Source # |
Instance details Defined in What4.SpecialFunctions Methods hashWithSaltF :: forall (tp :: Ctx Type). Int -> SpecialFunction tp -> Int Source # hashF :: forall (tp :: Ctx Type). SpecialFunction tp -> Int Source #
OrdF SpecialFunction Source # |

Instance details

Defined in What4.SpecialFunctions

Methods

compareF :: forall (x :: Ctx Type) (y :: Ctx Type). SpecialFunction x -> SpecialFunction y -> OrderingF x y Source #

leqF :: forall (x :: Ctx Type) (y :: Ctx Type). SpecialFunction x -> SpecialFunction y -> Bool Source #

ltF :: forall (x :: Ctx Type) (y :: Ctx Type). SpecialFunction x -> SpecialFunction y -> Bool Source #

geqF :: forall (x :: Ctx Type) (y :: Ctx Type). SpecialFunction x -> SpecialFunction y -> Bool Source #

gtF :: forall (x :: Ctx Type) (y :: Ctx Type). SpecialFunction x -> SpecialFunction y -> Bool Source #

## Symmetry properties of special functions

data FunctionSymmetry (r :: k) Source #

Some special functions exhibit useful symmetries in their arguments. A function `f` is an odd function if `f(-x) = -f(x)`, and is even if `f(-x) = f(x)`. We extend this notion to arguments of more than one function by saying that a function is even/odd in its `i`th argument if it is even/odd when the other arguments are fixed.

Constructors

NoSymmetry |
EvenFunction |
OddFunction |

#### Instances

Instances details

Show (FunctionSymmetry r) Source # |
Instance details Defined in What4.SpecialFunctions Methods showsPrec :: Int -> FunctionSymmetry r -> ShowS Source # show :: FunctionSymmetry r -> String Source # showList :: [FunctionSymmetry r] -> ShowS Source #

specialFnSymmetry :: forall (args :: Ctx Type). SpecialFunction args -> Assignment (FunctionSymmetry :: Type -> Type) args Source #

Compute function symmetry information for the given special function.

## Packaging arguments to special functions

data SpecialFnArg (e :: k -> Type) (tp :: k) r where Source #

Data type for wrapping the actual arguments to special functions.

Constructors

SpecialFnArg :: forall {k} (e :: k -> Type) (tp :: k). e tp -> SpecialFnArg e tp R |

#### Instances

Instances details

OrdF e => TestEquality (SpecialFnArg e tp :: Type -> Type) Source # |
Instance details Defined in What4.SpecialFunctions Methods testEquality :: SpecialFnArg e tp a -> SpecialFnArg e tp b -> Maybe (a :~: b) Source #
HashableF e => HashableF (SpecialFnArg e tp :: Type -> Type) Source # |
Instance details Defined in What4.SpecialFunctions Methods hashWithSaltF :: Int -> SpecialFnArg e tp tp0 -> Int Source # hashF :: SpecialFnArg e tp tp0 -> Int Source #
OrdF e => OrdF (SpecialFnArg e tp :: Type -> Type) Source # |

Instance details

Defined in What4.SpecialFunctions

Methods

compareF :: SpecialFnArg e tp x -> SpecialFnArg e tp y -> OrderingF x y Source #

leqF :: SpecialFnArg e tp x -> SpecialFnArg e tp y -> Bool Source #

ltF :: SpecialFnArg e tp x -> SpecialFnArg e tp y -> Bool Source #

geqF :: SpecialFnArg e tp x -> SpecialFnArg e tp y -> Bool Source #

gtF :: SpecialFnArg e tp x -> SpecialFnArg e tp y -> Bool Source #

traverseSpecialFnArg :: forall {k} m e (tp :: k) f r. Applicative m => (e tp -> m (f tp)) -> SpecialFnArg e tp r -> m (SpecialFnArg f tp r) Source #

newtype SpecialFnArgs (e :: k -> Type) (tp :: k) (args :: Ctx Type) Source #

Data type for wrapping a collction of actual arguments to special functions.

Constructors

SpecialFnArgs (Assignment (SpecialFnArg e tp) args) |

#### Instances

Instances details

OrdF e => Eq (SpecialFnArgs e tp r) Source # |
Instance details Defined in What4.SpecialFunctions Methods (==) :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool Source # (/=) :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool Source #
OrdF e => Ord (SpecialFnArgs e tp r) Source # |

Instance details

Defined in What4.SpecialFunctions

Methods

compare :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Ordering Source #

(<) :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool Source #

(<=) :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool Source #

(>) :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool Source #

(>=) :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool Source #

max :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> SpecialFnArgs e tp r Source #

min :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> SpecialFnArgs e tp r Source #

(HashableF e, OrdF e) => Hashable (SpecialFnArgs e tp args) Source # |
Instance details Defined in What4.SpecialFunctions Methods hashWithSalt :: Int -> SpecialFnArgs e tp args -> Int Source # hash :: SpecialFnArgs e tp args -> Int Source #

traverseSpecialFnArgs :: forall {k} m e (tp :: k) f (r :: Ctx Type). Applicative m => (e tp -> m (f tp)) -> SpecialFnArgs e tp r -> m (SpecialFnArgs f tp r) Source #

## Interval data for domain and range

data RealPoint Source #

Values that can appear in the definition of domain and range intervals for special functions.

Constructors

Zero |
NegOne |
PosOne |
NegInf |
PosInf |
NegPi |
PosPi |
NegHalfPi |
PosHalfPi |

#### Instances

Instances details

Show RealPoint Source # |
Instance details Defined in What4.SpecialFunctions Methods showsPrec :: Int -> RealPoint -> ShowS Source # show :: RealPoint -> String Source # showList :: [RealPoint] -> ShowS Source #

data RealBound Source #

The endpoint of an interval, which may be inclusive or exclusive.

Constructors

Incl RealPoint |
Excl RealPoint |

data RealInterval r where Source #

An interval on real values, or a point.

Constructors

RealPoint :: SpecialFunction (EmptyCtx :: Ctx Type) -> RealInterval R |
RealInterval :: RealBound -> RealBound -> RealInterval R |

#### Instances

Instances details

Show (RealInterval r) Source # |
Instance details Defined in What4.SpecialFunctions Methods showsPrec :: Int -> RealInterval r -> ShowS Source # show :: RealInterval r -> String Source # showList :: [RealInterval r] -> ShowS Source #

specialFnDomain :: forall (args :: Ctx Type). SpecialFunction args -> Assignment RealInterval args Source #

Compute the domain of the given special function. As a mathematical entity, the value of the given function is not well-defined outside its domain. In floating-point terms, a special function will return a `NaN` when evaluated on arguments outside its domain.

specialFnRange :: forall (args :: Ctx Type). SpecialFunction args -> RealInterval R Source #

Compute the range of values that may be returned by the given special function as its arguments take on the possible values of its domain. This may include limiting values if the function's domain includes infinities; for example `exp(-inf) = 0`.