what4-1.6.3: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2021
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Safe HaskellNone
LanguageHaskell2010

What4.SpecialFunctions

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

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

show :: SpecialFunction args -> String

showList :: [SpecialFunction args] -> ShowS

Eq (SpecialFunction args) Source # 
Instance details

Defined in What4.SpecialFunctions

Methods

(==) :: SpecialFunction args -> SpecialFunction args -> Bool

(/=) :: SpecialFunction args -> SpecialFunction args -> Bool

Hashable (SpecialFunction args) Source # 
Instance details

Defined in What4.SpecialFunctions

Methods

hashWithSalt :: Int -> SpecialFunction args -> Int

hash :: SpecialFunction args -> Int

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

HashableF SpecialFunction Source # 
Instance details

Defined in What4.SpecialFunctions

Methods

hashWithSaltF :: forall (tp :: Ctx Type). Int -> SpecialFunction tp -> Int

hashF :: forall (tp :: Ctx Type). SpecialFunction tp -> Int

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

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

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

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

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

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 ith argument if it is even/odd when the other arguments are fixed.

Instances

Instances details
Show (FunctionSymmetry r) Source # 
Instance details

Defined in What4.SpecialFunctions

Methods

showsPrec :: Int -> FunctionSymmetry r -> ShowS

show :: FunctionSymmetry r -> String

showList :: [FunctionSymmetry r] -> ShowS

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

HashableF e => HashableF (SpecialFnArg e tp :: Type -> Type) Source # 
Instance details

Defined in What4.SpecialFunctions

Methods

hashWithSaltF :: Int -> SpecialFnArg e tp tp0 -> Int

hashF :: SpecialFnArg e tp tp0 -> Int

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

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

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

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

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

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

(/=) :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool

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

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

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

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

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

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

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

(HashableF e, OrdF e) => Hashable (SpecialFnArgs e tp args) Source # 
Instance details

Defined in What4.SpecialFunctions

Methods

hashWithSalt :: Int -> SpecialFnArgs e tp args -> Int

hash :: SpecialFnArgs e tp args -> Int

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.

Instances

Instances details
Show RealPoint Source # 
Instance details

Defined in What4.SpecialFunctions

Methods

showsPrec :: Int -> RealPoint -> ShowS

show :: RealPoint -> String

showList :: [RealPoint] -> ShowS

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

show :: RealInterval r -> String

showList :: [RealInterval r] -> ShowS

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.