What4.Expr.BoolMap

Declares a datatype for representing n-way conjunctions or disjunctions in a way that efficiently captures important algebraic laws like commutativity, associativity and resolution.

Documentation

data BoolMap (f :: BaseType -> Type)

A representation of a conjunction or a disjunction.

This data structure keeps track of a collection of expressions together with their polarities. The implementation uses a map from expression values to their polarities, and thus automatically implements the associative, commutative and idempotency laws common to both conjunctions and disjunctions. Moreover, if the same expression occurs in the collection with opposite polarities, the entire collection collapses via a resolution step to an "inconsistent" map. For conjunctions this corresponds to a contradiction and represents false; for disjunction, this corresponds to the law of the excluded middle and represents true.

The annotation on the AnnotatedMap is an incremental hash (IncrHash) of the map, used to support a fast Hashable instance.

Instances

FoldableF BoolMap

Specialized version of foldMapVars

Defined in What4.Expr.BoolMap

Methods

foldMapF :: Monoid m => (forall (s :: k). e s -> m) -> BoolMap e -> m

foldrF :: (forall (s :: k). e s -> b -> b) -> b -> BoolMap e -> b

foldlF :: (forall (s :: k). b -> e s -> b) -> b -> BoolMap e -> b

foldrF' :: (forall (s :: k). e s -> b -> b) -> b -> BoolMap e -> b

foldlF' :: (forall (s :: k). b -> e s -> b) -> b -> BoolMap e -> b

toListF :: (forall (tp :: k). f tp -> a) -> BoolMap f -> [a]

OrdF f => Semigroup (BoolMap f)

Defined in What4.Expr.BoolMap

Methods

(<>) :: BoolMap f -> BoolMap f -> BoolMap f

sconcat :: NonEmpty (BoolMap f) -> BoolMap f

stimes :: Integral b => b -> BoolMap f -> BoolMap f

OrdF f => Eq (BoolMap f)

Defined in What4.Expr.BoolMap

Methods

(==) :: BoolMap f -> BoolMap f -> Bool

(/=) :: BoolMap f -> BoolMap f -> Bool

(OrdF f, HashableF f) => Hashable (BoolMap f)

Defined in What4.Expr.BoolMap

Methods

hashWithSalt :: Int -> BoolMap f -> Int

hash :: BoolMap f -> Int

var :: (HashableF f, OrdF f) => f BaseBoolType -> Polarity -> BoolMap f

Produce a singleton bool map, consisting of just the given term

addVar :: (HashableF f, OrdF f) => f BaseBoolType -> Polarity -> BoolMap f -> BoolMap f

Add a variable to a bool map, performing a resolution step if possible

fromVars :: (HashableF f, OrdF f) => [(f BaseBoolType, Polarity)] -> BoolMap f

Generate a bool map from a list of terms and polarities by repeatedly calling addVar.

combine :: OrdF f => BoolMap f -> BoolMap f -> BoolMap f

Merge two bool maps, performing resolution as necessary.

data Polarity

Describes the occurrence of a variable or expression, whether it is negated or not.

Constructors

Positive

Negative

Instances

Show Polarity

Defined in What4.Expr.BoolMap

Methods

showsPrec :: Int -> Polarity -> ShowS

show :: Polarity -> String

showList :: [Polarity] -> ShowS

Eq Polarity

Defined in What4.Expr.BoolMap

Methods

(==) :: Polarity -> Polarity -> Bool

(/=) :: Polarity -> Polarity -> Bool

Ord Polarity

Defined in What4.Expr.BoolMap

Methods

compare :: Polarity -> Polarity -> Ordering

(<) :: Polarity -> Polarity -> Bool

(<=) :: Polarity -> Polarity -> Bool

(>) :: Polarity -> Polarity -> Bool

(>=) :: Polarity -> Polarity -> Bool

max :: Polarity -> Polarity -> Polarity

min :: Polarity -> Polarity -> Polarity

Hashable Polarity

Defined in What4.Expr.BoolMap

Methods

hashWithSalt :: Int -> Polarity -> Int

hash :: Polarity -> Int

negatePolarity :: Polarity -> Polarity

Swap a polarity value

contains :: OrdF f => BoolMap f -> f BaseBoolType -> Maybe Polarity

Test if the bool map contains the given term, and return the polarity of that term if so.

isInconsistent :: BoolMap f -> Bool

Returns true for an inconsistent bool map

isNull :: BoolMap f -> Bool

Returns true for a "null" bool map with no terms

data BoolMapView f

Represents the state of a BoolMap (either a conjunction or disjunction).

If you know you are dealing with a BoolMap that represents a conjunction, consider using ConjMap and viewConjMap for the sake of clarity.

Constructors

BoolMapUnit

A bool map with no expressions, represents the unit of the corresponding operation

BoolMapDualUnit

An inconsistent bool map, represents the dual of the operation unit

BoolMapTerms (NonEmpty (f BaseBoolType, Polarity))

The terms appearing in the bool map, of which there is at least one

viewBoolMap :: BoolMap f -> BoolMapView f

Deconstruct the given bool map for later processing

foldMapVars :: Monoid m => (f BaseBoolType -> m) -> BoolMap f -> m

traverseVars :: (Applicative m, HashableF g, OrdF g) => (f BaseBoolType -> m (g BaseBoolType)) -> BoolMap f -> m (BoolMap g)

Traverse the expressions in a bool map, and rebuild the map.

reversePolarities :: OrdF f => BoolMap f -> BoolMap f

Swap the polarities of the terms in the given bool map.

removeVar :: OrdF f => BoolMap f -> f BaseBoolType -> BoolMap f

Remove the given term from the bool map. The map is unchanged if inconsistent or if the term does not occur.

newtype Wrap (f :: k -> Type) (x :: k)

Constructors

Wrap

Fields

• unWrap :: f x

Instances

TestEquality f => Eq (Wrap f x)

Defined in What4.Expr.BoolMap

Methods

(==) :: Wrap f x -> Wrap f x -> Bool

(/=) :: Wrap f x -> Wrap f x -> Bool

OrdF f => Ord (Wrap f x)

Defined in What4.Expr.BoolMap

Methods

compare :: Wrap f x -> Wrap f x -> Ordering

(<) :: Wrap f x -> Wrap f x -> Bool

(<=) :: Wrap f x -> Wrap f x -> Bool

(>) :: Wrap f x -> Wrap f x -> Bool

(>=) :: Wrap f x -> Wrap f x -> Bool

max :: Wrap f x -> Wrap f x -> Wrap f x

min :: Wrap f x -> Wrap f x -> Wrap f x

(HashableF f, TestEquality f) => Hashable (Wrap f x)

Defined in What4.Expr.BoolMap

Methods

hashWithSalt :: Int -> Wrap f x -> Int

hash :: Wrap f x -> Int

ConjMap

newtype ConjMap f

A BoolMap representing a conjunction.

Constructors

ConjMap

Fields

• getConjMap :: BoolMap f

Instances

FoldableF ConjMap

Defined in What4.Expr.BoolMap

Methods

foldMapF :: Monoid m => (forall (s :: k). e s -> m) -> ConjMap e -> m

foldrF :: (forall (s :: k). e s -> b -> b) -> b -> ConjMap e -> b

foldlF :: (forall (s :: k). b -> e s -> b) -> b -> ConjMap e -> b

foldrF' :: (forall (s :: k). e s -> b -> b) -> b -> ConjMap e -> b

foldlF' :: (forall (s :: k). b -> e s -> b) -> b -> ConjMap e -> b

toListF :: (forall (tp :: k). f tp -> a) -> ConjMap f -> [a]

OrdF f => Semigroup (ConjMap f)

Defined in What4.Expr.BoolMap

Methods

(<>) :: ConjMap f -> ConjMap f -> ConjMap f

sconcat :: NonEmpty (ConjMap f) -> ConjMap f

stimes :: Integral b => b -> ConjMap f -> ConjMap f

OrdF f => Eq (ConjMap f)

Defined in What4.Expr.BoolMap

Methods

(==) :: ConjMap f -> ConjMap f -> Bool

(/=) :: ConjMap f -> ConjMap f -> Bool

(OrdF f, HashableF f) => Hashable (ConjMap f)

Defined in What4.Expr.BoolMap

Methods

hashWithSalt :: Int -> ConjMap f -> Int

hash :: ConjMap f -> Int

data ConjMapView f

Represents the state of a ConjMap. See viewConjMap.

Like BoolMapView, but with more specific patterns for readability.

pattern ConjTrue :: ConjMapView f

pattern ConjFalse :: ConjMapView f

pattern Conjuncts :: NonEmpty (f BaseBoolType, Polarity) -> ConjMapView f

viewConjMap :: forall f. ConjMap f -> ConjMapView f

Deconstruct the given ConjMap for later processing

addConjunct :: forall f. (HashableF f, OrdF f) => f BaseBoolType -> Polarity -> ConjMap f -> ConjMap f

Add a conjunct to a ConjMap.

Wrapper around addVar.

evalConj :: Applicative m => (f BaseBoolType -> m Bool) -> ConjMap f -> m Bool

Given the means to evaluate the conjuncts of a ConjMap to a concrete Bool, evaluate the whole conjunction to a Bool.