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

Copyright | (c) Galois Inc 2015-2020
License | BSD3
Maintainer | jhendrix@galois.com
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Expr.WeightedSum

Contents

- Utilities
- Weighted sums
- Ring products

Description

Declares a weighted sum type used for representing sums over variables and an offset in one of the supported semirings. This module also implements a representation of semiring products.

Synopsis

- type Tm f = (HashableF f, OrdF f, HasAbsValue f)
- data WeightedSum (f :: BaseType -> Type) (sr :: SemiRing)
- sumRepr :: WeightedSum f sr -> SemiRingRepr sr
- sumOffset :: Lens' (WeightedSum f sr) (Coefficient sr)
- sumAbsValue :: OrdF f => WeightedSum f sr -> AbstractValue (SemiRingBase sr)
- constant :: Tm f => SemiRingRepr sr -> Coefficient sr -> WeightedSum f sr
- var :: Tm f => SemiRingRepr sr -> f (SemiRingBase sr) -> WeightedSum f sr
- scaledVar :: Tm f => SemiRingRepr sr -> Coefficient sr -> f (SemiRingBase sr) -> WeightedSum f sr
- asConstant :: WeightedSum f sr -> Maybe (Coefficient sr)
- asVar :: WeightedSum f sr -> Maybe (f (SemiRingBase sr))
- asWeightedVar :: WeightedSum f sr -> Maybe (Coefficient sr, f (SemiRingBase sr))
- asAffineVar :: WeightedSum f sr -> Maybe (Coefficient sr, f (SemiRingBase sr), Coefficient sr)
- isZero :: SemiRingRepr sr -> WeightedSum f sr -> Bool
- traverseVars :: forall k j m sr. (Applicative m, Tm k) => (j (SemiRingBase sr) -> m (k (SemiRingBase sr))) -> WeightedSum j sr -> m (WeightedSum k sr)
- traverseCoeffs :: forall m f sr. (Applicative m, Tm f) => (Coefficient sr -> m (Coefficient sr)) -> WeightedSum f sr -> m (WeightedSum f sr)
- add :: Tm f => SemiRingRepr sr -> WeightedSum f sr -> WeightedSum f sr -> WeightedSum f sr
- addVar :: Tm f => SemiRingRepr sr -> WeightedSum f sr -> f (SemiRingBase sr) -> WeightedSum f sr
- addVars :: Tm f => SemiRingRepr sr -> f (SemiRingBase sr) -> f (SemiRingBase sr) -> WeightedSum f sr
- addConstant :: SemiRingRepr sr -> WeightedSum f sr -> Coefficient sr -> WeightedSum f sr
- scale :: Tm f => SemiRingRepr sr -> Coefficient sr -> WeightedSum f sr -> WeightedSum f sr
- eval :: (r -> r -> r) -> (Coefficient sr -> f (SemiRingBase sr) -> r) -> (Coefficient sr -> r) -> WeightedSum f sr -> r
- evalM :: Monad m => (r -> r -> m r) -> (Coefficient sr -> f (SemiRingBase sr) -> m r) -> (Coefficient sr -> m r) -> WeightedSum f sr -> m r
- extractCommon :: Tm f => WeightedSum f sr -> WeightedSum f sr -> (WeightedSum f sr, WeightedSum f sr, WeightedSum f sr)
- fromTerms :: Tm f => SemiRingRepr sr -> [(f (SemiRingBase sr), Coefficient sr)] -> Coefficient sr -> WeightedSum f sr
- transformSum :: (Applicative m, Tm g) => SemiRingRepr sr' -> (Coefficient sr -> m (Coefficient sr')) -> (f (SemiRingBase sr) -> m (g (SemiRingBase sr'))) -> WeightedSum f sr -> m (WeightedSum g sr')
- reduceIntSumMod :: Tm f => WeightedSum f SemiRingInteger -> Integer -> WeightedSum f SemiRingInteger
- data SemiRingProduct (f :: BaseType -> Type) (sr :: SemiRing)
- traverseProdVars :: forall k j m sr. (Applicative m, Tm k) => (j (SemiRingBase sr) -> m (k (SemiRingBase sr))) -> SemiRingProduct j sr -> m (SemiRingProduct k sr)
- nullProd :: SemiRingProduct f sr -> Bool
- asProdVar :: SemiRingProduct f sr -> Maybe (f (SemiRingBase sr))
- prodRepr :: SemiRingProduct f sr -> SemiRingRepr sr
- prodVar :: Tm f => SemiRingRepr sr -> f (SemiRingBase sr) -> SemiRingProduct f sr
- prodAbsValue :: OrdF f => SemiRingProduct f sr -> AbstractValue (SemiRingBase sr)
- prodMul :: Tm f => SemiRingProduct f sr -> SemiRingProduct f sr -> SemiRingProduct f sr
- prodEval :: (r -> r -> r) -> (f (SemiRingBase sr) -> r) -> SemiRingProduct f sr -> Maybe r
- prodEvalM :: Monad m => (r -> r -> m r) -> (f (SemiRingBase sr) -> m r) -> SemiRingProduct f sr -> m (Maybe r)
- prodContains :: OrdF f => SemiRingProduct f sr -> f (SemiRingBase sr) -> Bool

# Utilities

type Tm f = (HashableF f, OrdF f, HasAbsValue f) Source #

# Weighted sums

data WeightedSum (f :: BaseType -> Type) (sr :: SemiRing) Source #

A weighted sum of semiring values. Mathematically, this represents an affine operation on the underlying expressions.

#### Instances

Instances details

OrdF f => TestEquality (WeightedSum f :: SemiRing -> Type) Source # |
Instance details Defined in What4.Expr.WeightedSum Methods testEquality :: forall (a :: k) (b :: k). WeightedSum f a -> WeightedSum f b -> Maybe (a :~: b) Source #
OrdF f => Eq (WeightedSum f sr) Source # |
Instance details Defined in What4.Expr.WeightedSum Methods (==) :: WeightedSum f sr -> WeightedSum f sr -> Bool Source # (/=) :: WeightedSum f sr -> WeightedSum f sr -> Bool Source #
OrdF f => Hashable (WeightedSum f sr) Source # |
Instance details Defined in What4.Expr.WeightedSum Methods hashWithSalt :: Int -> WeightedSum f sr -> Int Source # hash :: WeightedSum f sr -> Int Source #

sumRepr :: WeightedSum f sr -> SemiRingRepr sr Source #

Runtime representation of the semiring for this sum.

sumOffset :: Lens' (WeightedSum f sr) (Coefficient sr) Source #

Retrieve the constant addend of the weighted sum.

sumAbsValue :: OrdF f => WeightedSum f sr -> AbstractValue (SemiRingBase sr) Source #

constant :: Tm f => SemiRingRepr sr -> Coefficient sr -> WeightedSum f sr Source #

Create a sum from a constant coefficient value.

var :: Tm f => SemiRingRepr sr -> f (SemiRingBase sr) -> WeightedSum f sr Source #

Create a weighted sum corresponding to the given variable.

scaledVar :: Tm f => SemiRingRepr sr -> Coefficient sr -> f (SemiRingBase sr) -> WeightedSum f sr Source #

This returns a variable times a constant.

asConstant :: WeightedSum f sr -> Maybe (Coefficient sr) Source #

Attempt to parse a weighted sum as a constant.

asVar :: WeightedSum f sr -> Maybe (f (SemiRingBase sr)) Source #

Attempt to parse a weighted sum as a single expression. `asVar w = Just r` when `denotation(w) = r`

asWeightedVar :: WeightedSum f sr -> Maybe (Coefficient sr, f (SemiRingBase sr)) Source #

Attempt to parse weighted sum as a single expression with a coefficient. `asWeightedVar w = Just (c,r)` when `denotation(w) = c*r`.

asAffineVar :: WeightedSum f sr -> Maybe (Coefficient sr, f (SemiRingBase sr), Coefficient sr) Source #

Attempt to parse a weighted sum as a single expression with a coefficient and offset. `asAffineVar w = Just (c,r,o)` when `denotation(w) = c*r + o`.

isZero :: SemiRingRepr sr -> WeightedSum f sr -> Bool Source #

Return true if a weighted sum is equal to constant 0.

traverseVars :: forall k j m sr. (Applicative m, Tm k) => (j (SemiRingBase sr) -> m (k (SemiRingBase sr))) -> WeightedSum j sr -> m (WeightedSum k sr) Source #

Traverse the expressions in a weighted sum.

traverseCoeffs :: forall m f sr. (Applicative m, Tm f) => (Coefficient sr -> m (Coefficient sr)) -> WeightedSum f sr -> m (WeightedSum f sr) Source #

Traverse the coefficients in a weighted sum.

add :: Tm f => SemiRingRepr sr -> WeightedSum f sr -> WeightedSum f sr -> WeightedSum f sr Source #

Add two sums, collecting terms as necessary and deleting terms whose coefficients sum to 0.

addVar :: Tm f => SemiRingRepr sr -> WeightedSum f sr -> f (SemiRingBase sr) -> WeightedSum f sr Source #

Add a variable to the sum.

addVars :: Tm f => SemiRingRepr sr -> f (SemiRingBase sr) -> f (SemiRingBase sr) -> WeightedSum f sr Source #

Create a weighted sum that represents the sum of two terms.

addConstant :: SemiRingRepr sr -> WeightedSum f sr -> Coefficient sr -> WeightedSum f sr Source #

Add a constant to the sum.

scale :: Tm f => SemiRingRepr sr -> Coefficient sr -> WeightedSum f sr -> WeightedSum f sr Source #

Multiply a sum by a constant coefficient.

eval Source #

Arguments

:: (r -> r -> r) | Addition function
-> (Coefficient sr -> f (SemiRingBase sr) -> r) | Scalar multiply
-> (Coefficient sr -> r) | Constant evaluation
-> WeightedSum f sr |
-> r |

Evaluate a sum given interpretations of addition, scalar multiplication, and a constant rational.

evalM Source #

Arguments

:: Monad m |
=> (r -> r -> m r) | Addition function
-> (Coefficient sr -> f (SemiRingBase sr) -> m r) | Scalar multiply
-> (Coefficient sr -> m r) | Constant evaluation
-> WeightedSum f sr |
-> m r |

Evaluate a sum given interpretations of addition, scalar multiplication, and a constant. This evaluation is threaded through a monad. The addition function is associated to the left, as in `foldlM`.

extractCommon :: Tm f => WeightedSum f sr -> WeightedSum f sr -> (WeightedSum f sr, WeightedSum f sr, WeightedSum f sr) Source #

Given two weighted sums `x` and `y`, this returns a triple `(z,x',y')` where `x = z + x'` and `y = z + y'` and `z` contains the "common" parts of `x` and `y`. We only extract common terms when both terms occur with the same coefficient in each sum.

This is primarily used to simplify if-then-else expressions to preserve shared subterms.

fromTerms :: Tm f => SemiRingRepr sr -> [(f (SemiRingBase sr), Coefficient sr)] -> Coefficient sr -> WeightedSum f sr Source #

Produce a weighted sum from a list of terms and an offset.

transformSum :: (Applicative m, Tm g) => SemiRingRepr sr' -> (Coefficient sr -> m (Coefficient sr')) -> (f (SemiRingBase sr) -> m (g (SemiRingBase sr'))) -> WeightedSum f sr -> m (WeightedSum g sr') Source #

Apply update functions to the terms and coefficients of a weighted sum.

reduceIntSumMod Source #

Arguments

:: Tm f |
=> WeightedSum f SemiRingInteger | The sum to reduce
-> Integer | The modulus, must not be 0
-> WeightedSum f SemiRingInteger |

Reduce a weighted sum of integers modulo a concrete integer. This reduces each of the coefficients modulo the given integer, removing any that are congruent to 0; the offset value is also reduced.

# Ring products

data SemiRingProduct (f :: BaseType -> Type) (sr :: SemiRing) Source #

A product of semiring values.

#### Instances

Instances details

OrdF f => TestEquality (SemiRingProduct f :: SemiRing -> Type) Source # |
Instance details Defined in What4.Expr.WeightedSum Methods testEquality :: forall (a :: k) (b :: k). SemiRingProduct f a -> SemiRingProduct f b -> Maybe (a :~: b) Source #
OrdF f => Eq (SemiRingProduct f sr) Source # |
Instance details Defined in What4.Expr.WeightedSum Methods (==) :: SemiRingProduct f sr -> SemiRingProduct f sr -> Bool Source # (/=) :: SemiRingProduct f sr -> SemiRingProduct f sr -> Bool Source #
OrdF f => Hashable (SemiRingProduct f sr) Source # |
Instance details Defined in What4.Expr.WeightedSum Methods hashWithSalt :: Int -> SemiRingProduct f sr -> Int Source # hash :: SemiRingProduct f sr -> Int Source #

traverseProdVars :: forall k j m sr. (Applicative m, Tm k) => (j (SemiRingBase sr) -> m (k (SemiRingBase sr))) -> SemiRingProduct j sr -> m (SemiRingProduct k sr) Source #

Traverse the expressions in a product.

nullProd :: SemiRingProduct f sr -> Bool Source #

Returns true if the product is trivial (contains no terms).

asProdVar :: SemiRingProduct f sr -> Maybe (f (SemiRingBase sr)) Source #

If the product consists of exactly on term, return it.

prodRepr :: SemiRingProduct f sr -> SemiRingRepr sr Source #

Runtime representation of the semiring for this product

prodVar :: Tm f => SemiRingRepr sr -> f (SemiRingBase sr) -> SemiRingProduct f sr Source #

Produce a product representing the single given term.

prodAbsValue :: OrdF f => SemiRingProduct f sr -> AbstractValue (SemiRingBase sr) Source #

prodMul :: Tm f => SemiRingProduct f sr -> SemiRingProduct f sr -> SemiRingProduct f sr Source #

Multiply two products, collecting terms and adding occurrences.

prodEval Source #

Arguments

:: (r -> r -> r) | multiplication evalation
-> (f (SemiRingBase sr) -> r) | term evaluation
-> SemiRingProduct f sr |
-> Maybe r |

Evaluate a product, given a function representing multiplication and a function to evaluate terms.

prodEvalM Source #

Arguments

:: Monad m |
=> (r -> r -> m r) | multiplication evalation
-> (f (SemiRingBase sr) -> m r) | term evaluation
-> SemiRingProduct f sr |
-> m (Maybe r) |

Evaluate a product, given a function representing multiplication and a function to evaluate terms, where both functions are threaded through a monad.

prodContains :: OrdF f => SemiRingProduct f sr -> f (SemiRingBase sr) -> Bool Source #

Returns true if the product contains at least on occurrence of the given term.