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

Copyright | (c) Galois Inc 2019-2020
License | BSD3
Maintainer | rdockins@galois.com
Safe Haskell | None
Language | Haskell2010

What4.Expr.BoolMap

Description

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

Synopsis

- data BoolMap (f :: BaseType -> Type)
- var :: (HashableF f, OrdF f) => f BaseBoolType -> Polarity -> BoolMap f
- addVar :: (HashableF f, OrdF f) => f BaseBoolType -> Polarity -> BoolMap f -> BoolMap f
- fromVars :: (HashableF f, OrdF f) => [(f BaseBoolType, Polarity)] -> BoolMap f
- combine :: forall (f :: BaseType -> Type). OrdF f => BoolMap f -> BoolMap f -> BoolMap f
- data Polarity
  - = Positive
  - | Negative
- negatePolarity :: Polarity -> Polarity
- contains :: OrdF f => BoolMap f -> f BaseBoolType -> Maybe Polarity
- isInconsistent :: forall (f :: BaseType -> Type). BoolMap f -> Bool
- isNull :: forall (f :: BaseType -> Type). BoolMap f -> Bool
- data BoolMapView (f :: BaseType -> Type)
  - = BoolMapUnit
  - | BoolMapDualUnit
  - | BoolMapTerms (NonEmpty (f BaseBoolType, Polarity))
- viewBoolMap :: forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f
- traverseVars :: (Applicative m, HashableF g, OrdF g) => (f BaseBoolType -> m (g BaseBoolType)) -> BoolMap f -> m (BoolMap g)
- reversePolarities :: forall (f :: BaseType -> Type). OrdF f => BoolMap f -> BoolMap f
- removeVar :: OrdF f => BoolMap f -> f BaseBoolType -> BoolMap f
- newtype Wrap (f :: k -> Type) (x :: k) = Wrap {
  - unWrap :: f x
  }

# Documentation

data BoolMap (f :: BaseType -> Type) Source #

This data structure keeps track of a collection of expressions together with their polarities. Such a collection might represent either a conjunction or a disjunction of expressions. 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.

#### Instances

Instances details

OrdF f => Eq (BoolMap f) Source # |
Instance details Defined in What4.Expr.BoolMap Methods (==) :: BoolMap f -> BoolMap f -> Bool Source # (/=) :: BoolMap f -> BoolMap f -> Bool Source #
(OrdF f, HashableF f) => Hashable (BoolMap f) Source # |
Instance details Defined in What4.Expr.BoolMap Methods hashWithSalt :: Int -> BoolMap f -> Int Source # hash :: BoolMap f -> Int Source #

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

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

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

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

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

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

combine :: forall (f :: BaseType -> Type). OrdF f => BoolMap f -> BoolMap f -> BoolMap f Source #

Merge two bool maps, performing resolution as necessary.

data Polarity Source #

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

Constructors

Positive |
Negative |

#### Instances

Instances details

Show Polarity Source # |
Instance details Defined in What4.Expr.BoolMap Methods showsPrec :: Int -> Polarity -> ShowS Source # show :: Polarity -> String Source # showList :: [Polarity] -> ShowS Source #
Eq Polarity Source # |
Instance details Defined in What4.Expr.BoolMap Methods (==) :: Polarity -> Polarity -> Bool Source # (/=) :: Polarity -> Polarity -> Bool Source #
Ord Polarity Source # |
Instance details Defined in What4.Expr.BoolMap Methods compare :: Polarity -> Polarity -> Ordering Source # (<) :: Polarity -> Polarity -> Bool Source # (<=) :: Polarity -> Polarity -> Bool Source # (>) :: Polarity -> Polarity -> Bool Source # (>=) :: Polarity -> Polarity -> Bool Source # max :: Polarity -> Polarity -> Polarity Source # min :: Polarity -> Polarity -> Polarity Source #
Hashable Polarity Source # |
Instance details Defined in What4.Expr.BoolMap Methods hashWithSalt :: Int -> Polarity -> Int Source # hash :: Polarity -> Int Source #

negatePolarity :: Polarity -> Polarity Source #

Swap a polarity value

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

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

isInconsistent :: forall (f :: BaseType -> Type). BoolMap f -> Bool Source #

Returns true for an inconsistent bool map

isNull :: forall (f :: BaseType -> Type). BoolMap f -> Bool Source #

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

data BoolMapView (f :: BaseType -> Type) Source #

Represents the state of a bool map

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 :: forall (f :: BaseType -> Type). BoolMap f -> BoolMapView f Source #

Deconstruct the given bool map for later processing

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

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

reversePolarities :: forall (f :: BaseType -> Type). OrdF f => BoolMap f -> BoolMap f Source #

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

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

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

Constructors

Wrap |

Fields

- unWrap :: f x

#### Instances

Instances details

TestEquality f => Eq (Wrap f x) Source # |
Instance details Defined in What4.Expr.BoolMap Methods (==) :: Wrap f x -> Wrap f x -> Bool Source # (/=) :: Wrap f x -> Wrap f x -> Bool Source #
OrdF f => Ord (Wrap f x) Source # |
Instance details Defined in What4.Expr.BoolMap Methods compare :: Wrap f x -> Wrap f x -> Ordering Source # (<) :: Wrap f x -> Wrap f x -> Bool Source # (<=) :: Wrap f x -> Wrap f x -> Bool Source # (>) :: Wrap f x -> Wrap f x -> Bool Source # (>=) :: Wrap f x -> Wrap f x -> Bool Source # max :: Wrap f x -> Wrap f x -> Wrap f x Source # min :: Wrap f x -> Wrap f x -> Wrap f x Source #
(HashableF f, TestEquality f) => Hashable (Wrap f x) Source # |
Instance details Defined in What4.Expr.BoolMap Methods hashWithSalt :: Int -> Wrap f x -> Int Source # hash :: Wrap f x -> Int Source #