What4.SemiRing

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.

Semiring datakinds

data SemiRing

Data-kind representing the semirings What4 supports.

Instances

TestEquality OrderedSemiRingRepr

Defined in What4.SemiRing

Methods

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

TestEquality SemiRingRepr

Defined in What4.SemiRing

Methods

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

HashableF OrderedSemiRingRepr

Defined in What4.SemiRing

Methods

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

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

HashableF SemiRingRepr

Defined in What4.SemiRing

Methods

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

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

OrdF OrderedSemiRingRepr

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

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)

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)

Defined in What4.Expr.WeightedSum

Methods

testEquality :: forall (a :: k) (b :: k). WeightedSum f a -> WeightedSum f b -> Maybe (a :~: b)

type SemiRingInteger

Arguments

 = 'SemiRingInteger

:: SemiRing

type SemiRingReal

Arguments

 = 'SemiRingReal

:: SemiRing

type SemiRingBV

Arguments

 = 'SemiRingBV

:: BVFlavor -> Nat -> SemiRing

data BVFlavor

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

TestEquality BVFlavorRepr

Defined in What4.SemiRing

Methods

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

HashableF BVFlavorRepr

Defined in What4.SemiRing

Methods

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

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

OrdF BVFlavorRepr

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

Arguments

 = 'BVBits

:: BVFlavor

type BVArith

Arguments

 = 'BVArith

:: BVFlavor

Semiring representations

data SemiRingRepr (sr :: SemiRing) where

Constructors

SemiRingIntegerRepr :: SemiRingRepr SemiRingInteger

SemiRingRealRepr :: SemiRingRepr SemiRingReal

SemiRingBVRepr :: 1 <= w => !(BVFlavorRepr fv) -> !(NatRepr w) -> SemiRingRepr (SemiRingBV fv w)

Instances

TestEquality SemiRingRepr

Defined in What4.SemiRing

Methods

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

HashableF SemiRingRepr

Defined in What4.SemiRing

Methods

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

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

OrdF SemiRingRepr

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)

Defined in What4.SemiRing

Methods

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

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

Hashable (SemiRingRepr sr)

Defined in What4.SemiRing

Methods

hashWithSalt :: Int -> SemiRingRepr sr -> Int

hash :: SemiRingRepr sr -> Int

data OrderedSemiRingRepr (sr :: SemiRing) where

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

Constructors

OrderedSemiRingIntegerRepr :: OrderedSemiRingRepr SemiRingInteger

OrderedSemiRingRealRepr :: OrderedSemiRingRepr SemiRingReal

Instances

TestEquality OrderedSemiRingRepr

Defined in What4.SemiRing

Methods

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

HashableF OrderedSemiRingRepr

Defined in What4.SemiRing

Methods

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

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

OrdF OrderedSemiRingRepr

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)

Defined in What4.SemiRing

Methods

(==) :: OrderedSemiRingRepr sr -> OrderedSemiRingRepr sr -> Bool

(/=) :: OrderedSemiRingRepr sr -> OrderedSemiRingRepr sr -> Bool

Hashable (OrderedSemiRingRepr sr)

Defined in What4.SemiRing

Methods

hashWithSalt :: Int -> OrderedSemiRingRepr sr -> Int

hash :: OrderedSemiRingRepr sr -> Int

data BVFlavorRepr (fv :: BVFlavor) where

Constructors

BVArithRepr :: BVFlavorRepr BVArith

BVBitsRepr :: BVFlavorRepr BVBits

Instances

TestEquality BVFlavorRepr

Defined in What4.SemiRing

Methods

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

HashableF BVFlavorRepr

Defined in What4.SemiRing

Methods

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

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

OrdF BVFlavorRepr

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)

Defined in What4.SemiRing

Methods

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

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

Hashable (BVFlavorRepr fv)

Defined in What4.SemiRing

Methods

hashWithSalt :: Int -> BVFlavorRepr fv -> Int

hash :: BVFlavorRepr fv -> Int

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

Equations

SemiRingBase SemiRingInteger = BaseIntegerType

SemiRingBase SemiRingReal = BaseRealType

SemiRingBase (SemiRingBV fv w) = BaseBVType w

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

Compute the base type of the given semiring.

orderedSemiRing :: OrderedSemiRingRepr sr -> SemiRingRepr sr

Compute the semiring corresponding to the given ordered semiring.

Semiring coefficients

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

The constant values in the semiring.

Equations

Coefficient SemiRingInteger = Integer

Coefficient SemiRingReal = Rational

Coefficient (SemiRingBV fv w) = BV w

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

Semiring product occurrences

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

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

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