Copyright | (c) Galois Inc 2015-2020 |
---|---|
License | BSD3 |
Maintainer | [email protected] |
Safe Haskell | None |
Language | Haskell2010 |
What4.Expr.WeightedSum
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 :: BaseType -> Type) = (HashableF f, OrdF f, HasAbsValue f)
- data WeightedSum (f :: BaseType -> Type) (sr :: SemiRing)
- sumRepr :: WeightedSum f sr -> SemiRingRepr sr
- sumOffset :: forall (f1 :: BaseType -> Type) (sr :: SemiRing) f2. Functor f2 => (Coefficient sr -> f2 (Coefficient sr)) -> WeightedSum f1 sr -> f2 (WeightedSum f1 sr)
- sumAbsValue :: forall (f :: BaseType -> Type) (sr :: SemiRing). OrdF f => WeightedSum f sr -> AbstractValue (SemiRingBase sr)
- constant :: forall (f :: BaseType -> Type) (sr :: SemiRing). Tm f => SemiRingRepr sr -> Coefficient sr -> WeightedSum f sr
- var :: forall f (sr :: SemiRing). Tm f => SemiRingRepr sr -> f (SemiRingBase sr) -> WeightedSum f sr
- scaledVar :: forall f (sr :: SemiRing). Tm f => SemiRingRepr sr -> Coefficient sr -> f (SemiRingBase sr) -> WeightedSum f sr
- asConstant :: forall (f :: BaseType -> Type) (sr :: SemiRing). WeightedSum f sr -> Maybe (Coefficient sr)
- asVar :: forall f (sr :: SemiRing). WeightedSum f sr -> Maybe (f (SemiRingBase sr))
- asWeightedVar :: forall f (sr :: SemiRing). WeightedSum f sr -> Maybe (Coefficient sr, f (SemiRingBase sr))
- asAffineVar :: forall f (sr :: SemiRing). WeightedSum f sr -> Maybe (Coefficient sr, f (SemiRingBase sr), Coefficient sr)
- isZero :: forall (sr :: SemiRing) (f :: BaseType -> Type). SemiRingRepr sr -> WeightedSum f sr -> Bool
- traverseVars :: forall k j m (sr :: SemiRing). (Applicative m, Tm k) => (j (SemiRingBase sr) -> m (k (SemiRingBase sr))) -> WeightedSum j sr -> m (WeightedSum k sr)
- traverseCoeffs :: forall m (f :: BaseType -> Type) (sr :: SemiRing). (Applicative m, Tm f) => (Coefficient sr -> m (Coefficient sr)) -> WeightedSum f sr -> m (WeightedSum f sr)
- add :: forall (f :: BaseType -> Type) (sr :: SemiRing). Tm f => SemiRingRepr sr -> WeightedSum f sr -> WeightedSum f sr -> WeightedSum f sr
- addVar :: forall f (sr :: SemiRing). Tm f => SemiRingRepr sr -> WeightedSum f sr -> f (SemiRingBase sr) -> WeightedSum f sr
- addVars :: forall f (sr :: SemiRing). Tm f => SemiRingRepr sr -> f (SemiRingBase sr) -> f (SemiRingBase sr) -> WeightedSum f sr
- addConstant :: forall (sr :: SemiRing) (f :: BaseType -> Type). SemiRingRepr sr -> WeightedSum f sr -> Coefficient sr -> WeightedSum f sr
- scale :: forall (f :: BaseType -> Type) (sr :: SemiRing). Tm f => SemiRingRepr sr -> Coefficient sr -> WeightedSum f sr -> WeightedSum f sr
- eval :: forall r (sr :: SemiRing) f. (r -> r -> r) -> (Coefficient sr -> f (SemiRingBase sr) -> r) -> (Coefficient sr -> r) -> WeightedSum f sr -> r
- evalM :: forall m r (sr :: SemiRing) f. Monad m => (r -> r -> m r) -> (Coefficient sr -> f (SemiRingBase sr) -> m r) -> (Coefficient sr -> m r) -> WeightedSum f sr -> m r
- extractCommon :: forall (f :: BaseType -> Type) (sr :: SemiRing). Tm f => WeightedSum f sr -> WeightedSum f sr -> (WeightedSum f sr, WeightedSum f sr, WeightedSum f sr)
- fromTerms :: forall f (sr :: SemiRing). Tm f => SemiRingRepr sr -> [(f (SemiRingBase sr), Coefficient sr)] -> Coefficient sr -> WeightedSum f sr
- transformSum :: forall m g (sr' :: SemiRing) (sr :: SemiRing) f. (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 :: forall (f :: BaseType -> Type). Tm f => WeightedSum f SemiRingInteger -> Integer -> WeightedSum f SemiRingInteger
- data SemiRingProduct (f :: BaseType -> Type) (sr :: SemiRing)
- traverseProdVars :: forall k j m (sr :: SemiRing). (Applicative m, Tm k) => (j (SemiRingBase sr) -> m (k (SemiRingBase sr))) -> SemiRingProduct j sr -> m (SemiRingProduct k sr)
- nullProd :: forall (f :: BaseType -> Type) (sr :: SemiRing). SemiRingProduct f sr -> Bool
- asProdVar :: forall f (sr :: SemiRing). SemiRingProduct f sr -> Maybe (f (SemiRingBase sr))
- prodRepr :: SemiRingProduct f sr -> SemiRingRepr sr
- prodVar :: forall f (sr :: SemiRing). Tm f => SemiRingRepr sr -> f (SemiRingBase sr) -> SemiRingProduct f sr
- prodAbsValue :: forall (f :: BaseType -> Type) (sr :: SemiRing). OrdF f => SemiRingProduct f sr -> AbstractValue (SemiRingBase sr)
- prodMul :: forall (f :: BaseType -> Type) (sr :: SemiRing). Tm f => SemiRingProduct f sr -> SemiRingProduct f sr -> SemiRingProduct f sr
- prodEval :: forall r f (sr :: SemiRing). (r -> r -> r) -> (f (SemiRingBase sr) -> r) -> SemiRingProduct f sr -> Maybe r
- prodEvalM :: forall m r f (sr :: SemiRing). Monad m => (r -> r -> m r) -> (f (SemiRingBase sr) -> m r) -> SemiRingProduct f sr -> m (Maybe r)
- prodContains :: forall f (sr :: SemiRing). OrdF f => SemiRingProduct f sr -> f (SemiRingBase sr) -> Bool
Utilities
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
OrdF f => TestEquality (WeightedSum f :: SemiRing -> Type) Source # | |
Defined in What4.Expr.WeightedSum Methods testEquality :: forall (a :: SemiRing) (b :: SemiRing). WeightedSum f a -> WeightedSum f b -> Maybe (a :~: b) # | |
OrdF f => Eq (WeightedSum f sr) Source # | |
Defined in What4.Expr.WeightedSum Methods (==) :: WeightedSum f sr -> WeightedSum f sr -> Bool # (/=) :: WeightedSum f sr -> WeightedSum f sr -> Bool # | |
OrdF f => Hashable (WeightedSum f sr) Source # | |
Defined in What4.Expr.WeightedSum |
sumRepr :: WeightedSum f sr -> SemiRingRepr sr Source #
Runtime representation of the semiring for this sum.
sumOffset :: forall (f1 :: BaseType -> Type) (sr :: SemiRing) f2. Functor f2 => (Coefficient sr -> f2 (Coefficient sr)) -> WeightedSum f1 sr -> f2 (WeightedSum f1 sr) Source #
Retrieve the constant addend of the weighted sum.
sumAbsValue :: forall (f :: BaseType -> Type) (sr :: SemiRing). OrdF f => WeightedSum f sr -> AbstractValue (SemiRingBase sr) Source #
constant :: forall (f :: BaseType -> Type) (sr :: SemiRing). Tm f => SemiRingRepr sr -> Coefficient sr -> WeightedSum f sr Source #
Create a sum from a constant coefficient value.
var :: forall f (sr :: SemiRing). Tm f => SemiRingRepr sr -> f (SemiRingBase sr) -> WeightedSum f sr Source #
Create a weighted sum corresponding to the given variable.
scaledVar :: forall f (sr :: SemiRing). Tm f => SemiRingRepr sr -> Coefficient sr -> f (SemiRingBase sr) -> WeightedSum f sr Source #
This returns a variable times a constant.
asConstant :: forall (f :: BaseType -> Type) (sr :: SemiRing). WeightedSum f sr -> Maybe (Coefficient sr) Source #
Attempt to parse a weighted sum as a constant.
asVar :: forall f (sr :: SemiRing). 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 :: forall f (sr :: SemiRing). 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 :: forall f (sr :: SemiRing). 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 :: forall (sr :: SemiRing) (f :: BaseType -> Type). SemiRingRepr sr -> WeightedSum f sr -> Bool Source #
Return true if a weighted sum is equal to constant 0.
traverseVars :: forall k j m (sr :: SemiRing). (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 :: BaseType -> Type) (sr :: SemiRing). (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 :: forall (f :: BaseType -> Type) (sr :: SemiRing). 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 :: forall f (sr :: SemiRing). Tm f => SemiRingRepr sr -> WeightedSum f sr -> f (SemiRingBase sr) -> WeightedSum f sr Source #
Add a variable to the sum.
addVars :: forall f (sr :: SemiRing). 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 :: forall (sr :: SemiRing) (f :: BaseType -> Type). SemiRingRepr sr -> WeightedSum f sr -> Coefficient sr -> WeightedSum f sr Source #
Add a constant to the sum.
scale :: forall (f :: BaseType -> Type) (sr :: SemiRing). Tm f => SemiRingRepr sr -> Coefficient sr -> WeightedSum f sr -> WeightedSum f sr Source #
Multiply a sum by a constant coefficient.
Arguments
:: forall r (sr :: SemiRing) f. (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.
Arguments
:: forall m r (sr :: SemiRing) f. 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 :: forall (f :: BaseType -> Type) (sr :: SemiRing). 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 :: forall f (sr :: SemiRing). 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 :: forall m g (sr' :: SemiRing) (sr :: SemiRing) f. (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.
Arguments
:: forall (f :: BaseType -> Type). 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
OrdF f => TestEquality (SemiRingProduct f :: SemiRing -> Type) Source # | |
Defined in What4.Expr.WeightedSum Methods testEquality :: forall (a :: SemiRing) (b :: SemiRing). SemiRingProduct f a -> SemiRingProduct f b -> Maybe (a :~: b) # | |
OrdF f => Eq (SemiRingProduct f sr) Source # | |
Defined in What4.Expr.WeightedSum Methods (==) :: SemiRingProduct f sr -> SemiRingProduct f sr -> Bool # (/=) :: SemiRingProduct f sr -> SemiRingProduct f sr -> Bool # | |
OrdF f => Hashable (SemiRingProduct f sr) Source # | |
Defined in What4.Expr.WeightedSum |
traverseProdVars :: forall k j m (sr :: SemiRing). (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 :: forall (f :: BaseType -> Type) (sr :: SemiRing). SemiRingProduct f sr -> Bool Source #
Returns true if the product is trivial (contains no terms).
asProdVar :: forall f (sr :: SemiRing). 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 :: forall f (sr :: SemiRing). Tm f => SemiRingRepr sr -> f (SemiRingBase sr) -> SemiRingProduct f sr Source #
Produce a product representing the single given term.
prodAbsValue :: forall (f :: BaseType -> Type) (sr :: SemiRing). OrdF f => SemiRingProduct f sr -> AbstractValue (SemiRingBase sr) Source #
prodMul :: forall (f :: BaseType -> Type) (sr :: SemiRing). Tm f => SemiRingProduct f sr -> SemiRingProduct f sr -> SemiRingProduct f sr Source #
Multiply two products, collecting terms and adding occurrences.
Arguments
:: forall r f (sr :: SemiRing). (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.
Arguments
:: forall m r f (sr :: SemiRing). 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 :: forall f (sr :: SemiRing). OrdF f => SemiRingProduct f sr -> f (SemiRingBase sr) -> Bool Source #
Returns true if the product contains at least on occurrence of the given term.