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

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

What4.SemiRing

Contents

- Semiring datakinds
- Semiring representations
- Semiring coefficients
- Semiring product occurrences

Description

The algebraic assumptions we make about our semirings are that:

- addition is commutative and associative, with a unit called zero,
- multiplication is commutative and associative, with a unit called one,
- one and zero are distinct values,
- multiplication distributes through addition, and
- multiplication by zero gives zero.

Note that we do not assume the existence of additive inverses (hence, semirings), but we do assume commutativity of multiplication.

Note, moreover, that bitvectors can be equipped with two different semirings (the usual arithmetic one and the XOR/AND boolean ring imposed by the boolean algebra structure), which occasionally requires some care.

In addition, some semirings are "ordered" semirings. These are equipped with a total ordering relation such that addition is both order-preserving and order-reflecting; that is, `x <= y` iff `x + z <= y + z`. Moreover ordered semirings satisfy: `0 <= x` and `0 <= y` implies `0 <= x*y`.

Synopsis

- data SemiRing
- type SemiRingInteger = 'SemiRingInteger
- type SemiRingReal = 'SemiRingReal
- type SemiRingBV = 'SemiRingBV
- data BVFlavor
- type BVBits = 'BVBits
- type BVArith = 'BVArith
- data SemiRingRepr (sr :: SemiRing) where
  - SemiRingIntegerRepr :: SemiRingRepr SemiRingInteger
  - SemiRingRealRepr :: SemiRingRepr SemiRingReal
  - SemiRingBVRepr :: 1 <= w => !(BVFlavorRepr fv) -> !(NatRepr w) -> SemiRingRepr (SemiRingBV fv w)
- data OrderedSemiRingRepr (sr :: SemiRing) where
  - OrderedSemiRingIntegerRepr :: OrderedSemiRingRepr SemiRingInteger
  - OrderedSemiRingRealRepr :: OrderedSemiRingRepr SemiRingReal
- data BVFlavorRepr (fv :: BVFlavor) where
  - BVArithRepr :: BVFlavorRepr BVArith
  - BVBitsRepr :: BVFlavorRepr BVBits
- type family SemiRingBase (sr :: SemiRing) :: BaseType where ...
- semiRingBase :: SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr)
- orderedSemiRing :: OrderedSemiRingRepr sr -> SemiRingRepr sr
- type family Coefficient (sr :: SemiRing) :: Type where ...
- zero :: SemiRingRepr sr -> Coefficient sr
- one :: SemiRingRepr sr -> Coefficient sr
- add :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Coefficient sr
- mul :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Coefficient sr
- eq :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
- le :: OrderedSemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
- lt :: OrderedSemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool
- sr_compare :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Ordering
- sr_hashWithSalt :: SemiRingRepr sr -> Int -> Coefficient sr -> Int
- type family Occurrence (sr :: SemiRing) :: Type where ...
- occ_add :: SemiRingRepr sr -> Occurrence sr -> Occurrence sr -> Occurrence sr
- occ_one :: SemiRingRepr sr -> Occurrence sr
- occ_eq :: SemiRingRepr sr -> Occurrence sr -> Occurrence sr -> Bool
- occ_hashWithSalt :: SemiRingRepr sr -> Int -> Occurrence sr -> Int
- occ_compare :: SemiRingRepr sr -> Occurrence sr -> Occurrence sr -> Ordering
- occ_count :: SemiRingRepr sr -> Occurrence sr -> Natural

# Semiring datakinds

data SemiRing Source #

Data-kind representing the semirings What4 supports.

#### Instances

Instances details

TestEquality OrderedSemiRingRepr Source # |
Instance details Defined in What4.SemiRing Methods testEquality :: forall (a :: k) (b :: k). OrderedSemiRingRepr a -> OrderedSemiRingRepr b -> Maybe (a :~: b) Source #
TestEquality SemiRingRepr Source # |
Instance details Defined in What4.SemiRing Methods testEquality :: forall (a :: k) (b :: k). SemiRingRepr a -> SemiRingRepr b -> Maybe (a :~: b) Source #
HashableF OrderedSemiRingRepr Source # |
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: forall (tp :: k). Int -> OrderedSemiRingRepr tp -> Int Source # hashF :: forall (tp :: k). OrderedSemiRingRepr tp -> Int Source #
HashableF SemiRingRepr Source # |
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: forall (tp :: k). Int -> SemiRingRepr tp -> Int Source # hashF :: forall (tp :: k). SemiRingRepr tp -> Int Source #
OrdF OrderedSemiRingRepr Source # |

Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

OrdF SemiRingRepr Source # |

Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

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

type SemiRingInteger Source #

Arguments

= 'SemiRingInteger

    :: SemiRing

type SemiRingReal Source #

Arguments

= 'SemiRingReal

    :: SemiRing

type SemiRingBV Source #

Arguments

= 'SemiRingBV

    :: BVFlavor -> Nat -> SemiRing

data BVFlavor Source #

Data-kind indicating the two flavors of bitvector semirings. The ordinary arithmetic semiring consists of addition and multiplication, and the "bits" semiring consists of bitwise xor and bitwise and.

#### Instances

Instances details

TestEquality BVFlavorRepr Source # |
Instance details Defined in What4.SemiRing Methods testEquality :: forall (a :: k) (b :: k). BVFlavorRepr a -> BVFlavorRepr b -> Maybe (a :~: b) Source #
HashableF BVFlavorRepr Source # |
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: forall (tp :: k). Int -> BVFlavorRepr tp -> Int Source # hashF :: forall (tp :: k). BVFlavorRepr tp -> Int Source #
OrdF BVFlavorRepr Source # |

Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

type BVBits Source #

Arguments

= 'BVBits

    :: BVFlavor

type BVArith Source #

Arguments

= 'BVArith

    :: BVFlavor

# Semiring representations

data SemiRingRepr (sr :: SemiRing) where Source #

Constructors

SemiRingIntegerRepr :: SemiRingRepr SemiRingInteger |
SemiRingRealRepr :: SemiRingRepr SemiRingReal |
SemiRingBVRepr :: 1 <= w => !(BVFlavorRepr fv) -> !(NatRepr w) -> SemiRingRepr (SemiRingBV fv w) |

#### Instances

Instances details

TestEquality SemiRingRepr Source # |
Instance details Defined in What4.SemiRing Methods testEquality :: forall (a :: k) (b :: k). SemiRingRepr a -> SemiRingRepr b -> Maybe (a :~: b) Source #
HashableF SemiRingRepr Source # |
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: forall (tp :: k). Int -> SemiRingRepr tp -> Int Source # hashF :: forall (tp :: k). SemiRingRepr tp -> Int Source #
OrdF SemiRingRepr Source # |

Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

Eq (SemiRingRepr sr) Source # |
Instance details Defined in What4.SemiRing Methods (==) :: SemiRingRepr sr -> SemiRingRepr sr -> Bool Source # (/=) :: SemiRingRepr sr -> SemiRingRepr sr -> Bool Source #
Hashable (SemiRingRepr sr) Source # |
Instance details Defined in What4.SemiRing Methods hashWithSalt :: Int -> SemiRingRepr sr -> Int Source # hash :: SemiRingRepr sr -> Int Source #

data OrderedSemiRingRepr (sr :: SemiRing) where Source #

The subset of semirings that are equipped with an appropriate (order-respecting) total order.

Constructors

OrderedSemiRingIntegerRepr :: OrderedSemiRingRepr SemiRingInteger |
OrderedSemiRingRealRepr :: OrderedSemiRingRepr SemiRingReal |

#### Instances

Instances details

TestEquality OrderedSemiRingRepr Source # |
Instance details Defined in What4.SemiRing Methods testEquality :: forall (a :: k) (b :: k). OrderedSemiRingRepr a -> OrderedSemiRingRepr b -> Maybe (a :~: b) Source #
HashableF OrderedSemiRingRepr Source # |
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: forall (tp :: k). Int -> OrderedSemiRingRepr tp -> Int Source # hashF :: forall (tp :: k). OrderedSemiRingRepr tp -> Int Source #
OrdF OrderedSemiRingRepr Source # |

Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

Eq (OrderedSemiRingRepr sr) Source # |
Instance details Defined in What4.SemiRing Methods (==) :: OrderedSemiRingRepr sr -> OrderedSemiRingRepr sr -> Bool Source # (/=) :: OrderedSemiRingRepr sr -> OrderedSemiRingRepr sr -> Bool Source #
Hashable (OrderedSemiRingRepr sr) Source # |
Instance details Defined in What4.SemiRing Methods hashWithSalt :: Int -> OrderedSemiRingRepr sr -> Int Source # hash :: OrderedSemiRingRepr sr -> Int Source #

data BVFlavorRepr (fv :: BVFlavor) where Source #

Constructors

BVArithRepr :: BVFlavorRepr BVArith |
BVBitsRepr :: BVFlavorRepr BVBits |

#### Instances

Instances details

TestEquality BVFlavorRepr Source # |
Instance details Defined in What4.SemiRing Methods testEquality :: forall (a :: k) (b :: k). BVFlavorRepr a -> BVFlavorRepr b -> Maybe (a :~: b) Source #
HashableF BVFlavorRepr Source # |
Instance details Defined in What4.SemiRing Methods hashWithSaltF :: forall (tp :: k). Int -> BVFlavorRepr tp -> Int Source # hashF :: forall (tp :: k). BVFlavorRepr tp -> Int Source #
OrdF BVFlavorRepr Source # |

Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

Eq (BVFlavorRepr fv) Source # |
Instance details Defined in What4.SemiRing Methods (==) :: BVFlavorRepr fv -> BVFlavorRepr fv -> Bool Source # (/=) :: BVFlavorRepr fv -> BVFlavorRepr fv -> Bool Source #
Hashable (BVFlavorRepr fv) Source # |
Instance details Defined in What4.SemiRing Methods hashWithSalt :: Int -> BVFlavorRepr fv -> Int Source # hash :: BVFlavorRepr fv -> Int Source #

type family SemiRingBase (sr :: SemiRing) :: BaseType where ... Source #

Equations

SemiRingBase SemiRingInteger = BaseIntegerType |
SemiRingBase SemiRingReal = BaseRealType |
SemiRingBase (SemiRingBV fv w) = BaseBVType w |

semiRingBase :: SemiRingRepr sr -> BaseTypeRepr (SemiRingBase sr) Source #

Compute the base type of the given semiring.

orderedSemiRing :: OrderedSemiRingRepr sr -> SemiRingRepr sr Source #

Compute the semiring corresponding to the given ordered semiring.

# Semiring coefficients

type family Coefficient (sr :: SemiRing) :: Type where ... Source #

The constant values in the semiring.

Equations

Coefficient SemiRingInteger = Integer |
Coefficient SemiRingReal = Rational |
Coefficient (SemiRingBV fv w) = BV w |

zero :: SemiRingRepr sr -> Coefficient sr Source #

one :: SemiRingRepr sr -> Coefficient sr Source #

add :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Coefficient sr Source #

mul :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Coefficient sr Source #

eq :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool Source #

le :: OrderedSemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool Source #

lt :: OrderedSemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Bool Source #

sr_compare :: SemiRingRepr sr -> Coefficient sr -> Coefficient sr -> Ordering Source #

sr_hashWithSalt :: SemiRingRepr sr -> Int -> Coefficient sr -> Int Source #

# Semiring product occurrences

type family Occurrence (sr :: SemiRing) :: Type where ... Source #

The `Occurrence` family counts how many times a term occurs in a product. For most semirings, this is just a natural number representing the exponent. For the boolean ring of bitvectors, however, it is unit because the lattice operations are idempotent.

Equations

Occurrence SemiRingInteger = Natural |
Occurrence SemiRingReal = Natural |
Occurrence (SemiRingBV BVArith w) = Natural |
Occurrence (SemiRingBV BVBits w) = () |

occ_add :: SemiRingRepr sr -> Occurrence sr -> Occurrence sr -> Occurrence sr Source #

occ_one :: SemiRingRepr sr -> Occurrence sr Source #

occ_eq :: SemiRingRepr sr -> Occurrence sr -> Occurrence sr -> Bool Source #

occ_hashWithSalt :: SemiRingRepr sr -> Int -> Occurrence sr -> Int Source #

occ_compare :: SemiRingRepr sr -> Occurrence sr -> Occurrence sr -> Ordering Source #

occ_count :: SemiRingRepr sr -> Occurrence sr -> Natural Source #