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

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
 Source # Instance detailsDefined in What4.SemiRing Methods Source # Instance detailsDefined in What4.SemiRing MethodstestEquality :: SemiRingRepr a -> SemiRingRepr b -> Maybe (a :~: b) # Source # Instance detailsDefined in What4.SemiRing Methods Source # Instance detailsDefined in What4.SemiRing MethodscompareF :: SemiRingRepr x -> SemiRingRepr y -> OrderingF x y #leqF :: SemiRingRepr x -> SemiRingRepr y -> Bool #ltF :: SemiRingRepr x -> SemiRingRepr y -> Bool #geqF :: SemiRingRepr x -> SemiRingRepr y -> Bool #gtF :: SemiRingRepr x -> SemiRingRepr y -> Bool # Source # Instance detailsDefined in What4.SemiRing MethodshashF :: OrderedSemiRingRepr tp -> Int # Source # Instance detailsDefined in What4.SemiRing MethodshashWithSaltF :: Int -> SemiRingRepr tp -> Int #hashF :: SemiRingRepr tp -> Int # OrdF f => TestEquality (SemiRingProduct f :: SemiRing -> Type) Source # Instance detailsDefined in What4.Expr.WeightedSum MethodstestEquality :: SemiRingProduct f a -> SemiRingProduct f b -> Maybe (a :~: b) # OrdF f => TestEquality (WeightedSum f :: SemiRing -> Type) Source # Instance detailsDefined in What4.Expr.WeightedSum MethodstestEquality :: WeightedSum f a -> WeightedSum f b -> Maybe (a :~: b) #

Arguments

 = SemiRingNat :: SemiRing

Arguments

 = SemiRingInteger :: SemiRing

Arguments

 = SemiRingReal :: SemiRing

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
 Source # Instance detailsDefined in What4.SemiRing MethodstestEquality :: BVFlavorRepr a -> BVFlavorRepr b -> Maybe (a :~: b) # Source # Instance detailsDefined in What4.SemiRing MethodscompareF :: BVFlavorRepr x -> BVFlavorRepr y -> OrderingF x y #leqF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool #ltF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool #geqF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool #gtF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # Source # Instance detailsDefined in What4.SemiRing MethodshashWithSaltF :: Int -> BVFlavorRepr tp -> Int #hashF :: BVFlavorRepr tp -> Int #

type BVBits Source #

Arguments

 = BVBits :: BVFlavor

type BVArith Source #

Arguments

 = BVArith :: BVFlavor

# Semiring representations

data SemiRingRepr (sr :: SemiRing) where Source #

Constructors

 SemiRingNatRepr :: SemiRingRepr SemiRingNat SemiRingIntegerRepr :: SemiRingRepr SemiRingInteger SemiRingRealRepr :: SemiRingRepr SemiRingReal SemiRingBVRepr :: 1 <= w => !(BVFlavorRepr fv) -> !(NatRepr w) -> SemiRingRepr (SemiRingBV fv w)
Instances
 Source # Instance detailsDefined in What4.SemiRing MethodstestEquality :: SemiRingRepr a -> SemiRingRepr b -> Maybe (a :~: b) # Source # Instance detailsDefined in What4.SemiRing MethodscompareF :: SemiRingRepr x -> SemiRingRepr y -> OrderingF x y #leqF :: SemiRingRepr x -> SemiRingRepr y -> Bool #ltF :: SemiRingRepr x -> SemiRingRepr y -> Bool #geqF :: SemiRingRepr x -> SemiRingRepr y -> Bool #gtF :: SemiRingRepr x -> SemiRingRepr y -> Bool # Source # Instance detailsDefined in What4.SemiRing MethodshashWithSaltF :: Int -> SemiRingRepr tp -> Int #hashF :: SemiRingRepr tp -> Int # Source # Instance detailsDefined in What4.SemiRing MethodshashWithSalt :: 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
 Source # Instance detailsDefined in What4.SemiRing Methods Source # Instance detailsDefined in What4.SemiRing Methods Source # Instance detailsDefined in What4.SemiRing MethodshashF :: OrderedSemiRingRepr tp -> Int # Source # Instance detailsDefined in What4.SemiRing Methodshash :: OrderedSemiRingRepr sr -> Int #

data BVFlavorRepr (fv :: BVFlavor) where Source #

Constructors

 BVArithRepr :: BVFlavorRepr BVArith BVBitsRepr :: BVFlavorRepr BVBits
Instances
 Source # Instance detailsDefined in What4.SemiRing MethodstestEquality :: BVFlavorRepr a -> BVFlavorRepr b -> Maybe (a :~: b) # Source # Instance detailsDefined in What4.SemiRing MethodscompareF :: BVFlavorRepr x -> BVFlavorRepr y -> OrderingF x y #leqF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool #ltF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool #geqF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool #gtF :: BVFlavorRepr x -> BVFlavorRepr y -> Bool # Source # Instance detailsDefined in What4.SemiRing MethodshashWithSaltF :: Int -> BVFlavorRepr tp -> Int #hashF :: BVFlavorRepr tp -> Int # Source # Instance detailsDefined in What4.SemiRing MethodshashWithSalt :: Int -> BVFlavorRepr fv -> Int #hash :: BVFlavorRepr fv -> Int #

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

Equations

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

Compute the base type of the given semiring.

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 SemiRingNat = Natural Coefficient SemiRingInteger = Integer Coefficient SemiRingReal = Rational Coefficient (SemiRingBV fv w) = BV w

# 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 SemiRingNat = Natural Occurrence SemiRingInteger = Natural Occurrence SemiRingReal = Natural Occurrence (SemiRingBV BVArith w) = Natural Occurrence (SemiRingBV BVBits w) = ()