what4-1.6.2: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2019-2020
LicenseBSD3
Maintainerrdockins@galois.com
Safe HaskellSafe-Inferred
LanguageHaskell2010

What4.SemiRing

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

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

TestEquality SemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

testEquality :: forall (a :: k) (b :: k). SemiRingRepr a -> SemiRingRepr b -> Maybe (a :~: b) #

HashableF OrderedSemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

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

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

HashableF SemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

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

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

OrdF OrderedSemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

OrdF SemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

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

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

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

HashableF BVFlavorRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

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

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

OrdF BVFlavorRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

type BVBits Source #

Arguments

 = 'BVBits
:: BVFlavor

type BVArith Source #

Arguments

 = 'BVArith
:: BVFlavor

Semiring representations

data SemiRingRepr (sr :: SemiRing) where Source #

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

HashableF SemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

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

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

OrdF SemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

Eq (SemiRingRepr sr) Source # 
Instance details

Defined in What4.SemiRing

Methods

(==) :: SemiRingRepr sr -> SemiRingRepr sr -> Bool #

(/=) :: SemiRingRepr sr -> SemiRingRepr sr -> Bool #

Hashable (SemiRingRepr sr) Source # 
Instance details

Defined in What4.SemiRing

Methods

hashWithSalt :: Int -> SemiRingRepr sr -> Int #

hash :: SemiRingRepr sr -> Int #

data OrderedSemiRingRepr (sr :: SemiRing) where Source #

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

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

HashableF OrderedSemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

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

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

OrdF OrderedSemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

Eq (OrderedSemiRingRepr sr) Source # 
Instance details

Defined in What4.SemiRing

Hashable (OrderedSemiRingRepr sr) Source # 
Instance details

Defined in What4.SemiRing

data BVFlavorRepr (fv :: BVFlavor) where Source #

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

HashableF BVFlavorRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

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

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

OrdF BVFlavorRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

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

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

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

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

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

Eq (BVFlavorRepr fv) Source # 
Instance details

Defined in What4.SemiRing

Methods

(==) :: BVFlavorRepr fv -> BVFlavorRepr fv -> Bool #

(/=) :: BVFlavorRepr fv -> BVFlavorRepr fv -> Bool #

Hashable (BVFlavorRepr fv) Source # 
Instance details

Defined in What4.SemiRing

Methods

hashWithSalt :: Int -> BVFlavorRepr fv -> Int #

hash :: BVFlavorRepr fv -> Int #

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.

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.