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

Copyright(c) Galois Inc 2019-2020
LicenseBSD3
Maintainerrdockins@galois.com
Safe HaskellNone
LanguageHaskell2010

What4.SemiRing

Contents

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
TestEquality OrderedSemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

testEquality :: OrderedSemiRingRepr a -> OrderedSemiRingRepr b -> Maybe (a :~: b) #

TestEquality SemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

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

OrdF OrderedSemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

compareF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> OrderingF x y #

leqF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool #

ltF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool #

geqF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool #

gtF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool #

OrdF SemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

compareF :: 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 #

HashableF OrderedSemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

hashWithSaltF :: Int -> OrderedSemiRingRepr tp -> Int #

hashF :: OrderedSemiRingRepr tp -> Int #

HashableF SemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

hashWithSaltF :: Int -> SemiRingRepr tp -> Int #

hashF :: SemiRingRepr tp -> Int #

OrdF f => TestEquality (SemiRingProduct f :: SemiRing -> Type) Source # 
Instance details

Defined in What4.Expr.WeightedSum

Methods

testEquality :: 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 :: WeightedSum f a -> WeightedSum f b -> Maybe (a :~: b) #

type SemiRingNat Source #

Arguments

 = SemiRingNat
:: SemiRing

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
TestEquality BVFlavorRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

testEquality :: BVFlavorRepr a -> BVFlavorRepr b -> Maybe (a :~: b) #

OrdF BVFlavorRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

compareF :: 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 #

HashableF BVFlavorRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

hashWithSaltF :: 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
TestEquality SemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

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

OrdF SemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

compareF :: 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 #

HashableF SemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

hashWithSaltF :: Int -> SemiRingRepr tp -> Int #

hashF :: SemiRingRepr tp -> Int #

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.

Constructors

OrderedSemiRingNatRepr :: OrderedSemiRingRepr SemiRingNat 
OrderedSemiRingIntegerRepr :: OrderedSemiRingRepr SemiRingInteger 
OrderedSemiRingRealRepr :: OrderedSemiRingRepr SemiRingReal 
Instances
TestEquality OrderedSemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

testEquality :: OrderedSemiRingRepr a -> OrderedSemiRingRepr b -> Maybe (a :~: b) #

OrdF OrderedSemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

compareF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> OrderingF x y #

leqF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool #

ltF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool #

geqF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool #

gtF :: OrderedSemiRingRepr x -> OrderedSemiRingRepr y -> Bool #

HashableF OrderedSemiRingRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

hashWithSaltF :: Int -> OrderedSemiRingRepr tp -> Int #

hashF :: OrderedSemiRingRepr tp -> Int #

Hashable (OrderedSemiRingRepr sr) Source # 
Instance details

Defined in What4.SemiRing

Methods

hashWithSalt :: Int -> OrderedSemiRingRepr sr -> Int #

hash :: OrderedSemiRingRepr sr -> Int #

data BVFlavorRepr (fv :: BVFlavor) where Source #

Constructors

BVArithRepr :: BVFlavorRepr BVArith 
BVBitsRepr :: BVFlavorRepr BVBits 
Instances
TestEquality BVFlavorRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

testEquality :: BVFlavorRepr a -> BVFlavorRepr b -> Maybe (a :~: b) #

OrdF BVFlavorRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

compareF :: 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 #

HashableF BVFlavorRepr Source # 
Instance details

Defined in What4.SemiRing

Methods

hashWithSaltF :: Int -> BVFlavorRepr tp -> Int #

hashF :: BVFlavorRepr tp -> Int #

Hashable (BVFlavorRepr fv) Source # 
Instance details

Defined in What4.SemiRing

Methods

hashWithSalt :: 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 

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