what4-1.6.2: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2021
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Safe HaskellSafe-Inferred
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.

Instances

Instances details
Show (SpecialFunction args) Source # 
Instance details

Defined in What4.SpecialFunctions

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 :: k) (b :: k). SpecialFunction a -> SpecialFunction b -> Maybe (a :~: b) #

HashableF SpecialFunction Source # 
Instance details

Defined in What4.SpecialFunctions

Methods

hashWithSaltF :: forall (tp :: k). Int -> SpecialFunction tp -> Int #

hashF :: forall (tp :: k). SpecialFunction tp -> Int #

OrdF SpecialFunction Source # 
Instance details

Defined in What4.SpecialFunctions

Methods

compareF :: forall (x :: k) (y :: k). SpecialFunction x -> SpecialFunction y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). SpecialFunction x -> SpecialFunction y -> Bool #

ltF :: forall (x :: k) (y :: k). SpecialFunction x -> SpecialFunction y -> Bool #

geqF :: forall (x :: k) (y :: k). SpecialFunction x -> SpecialFunction y -> Bool #

gtF :: forall (x :: k) (y :: k). SpecialFunction x -> SpecialFunction y -> Bool #

Symmetry properties of special functions

data FunctionSymmetry r 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

specialFnSymmetry :: SpecialFunction args -> Assignment FunctionSymmetry args Source #

Compute function symmetry information for the given special function.

Packaging arguments to special functions

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

Data type for wrapping the actual arguments to special functions.

Constructors

SpecialFnArg :: 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 :: forall (a :: k) (b :: k). 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 :: forall (tp0 :: k). Int -> SpecialFnArg e tp tp0 -> Int #

hashF :: forall (tp0 :: k). SpecialFnArg e tp tp0 -> Int #

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

Defined in What4.SpecialFunctions

Methods

compareF :: forall (x :: k) (y :: k). SpecialFnArg e tp x -> SpecialFnArg e tp y -> OrderingF x y #

leqF :: forall (x :: k) (y :: k). SpecialFnArg e tp x -> SpecialFnArg e tp y -> Bool #

ltF :: forall (x :: k) (y :: k). SpecialFnArg e tp x -> SpecialFnArg e tp y -> Bool #

geqF :: forall (x :: k) (y :: k). SpecialFnArg e tp x -> SpecialFnArg e tp y -> Bool #

gtF :: forall (x :: k) (y :: k). SpecialFnArg e tp x -> SpecialFnArg e tp y -> Bool #

traverseSpecialFnArg :: 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 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 :: 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

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.

Instances

Instances details
Show (RealInterval r) Source # 
Instance details

Defined in What4.SpecialFunctions

specialFnDomain :: 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 :: 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.