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

Copyright | (c) Galois Inc 2019-2020
License | BSD3
Maintainer | Langston Barrett <langston@galois.com>
Stability | provisional
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.LabeledPred

Description

Predicates alone do not record their semantic content, thus it is often useful to attach some sort of descriptor to them.

Synopsis

- data LabeledPred pred msg = LabeledPred {
  - _labeledPred :: !pred
  - _labeledPredMsg :: !msg
  }
- labeledPred :: Lens (LabeledPred pred msg) (LabeledPred pred' msg) pred pred'
- labeledPredMsg :: Lens (LabeledPred pred msg) (LabeledPred pred msg') msg msg'
- partitionByPreds :: (Foldable t, IsExprBuilder sym) => proxy sym -> (a -> Pred sym) -> t a -> ([a], [a], [a])
- partitionByPredsM :: (Monad m, Foldable t, IsExprBuilder sym) => proxy sym -> (a -> m (Pred sym)) -> t a -> m ([a], [a], [a])
- partitionLabeledPreds :: (Foldable t, IsExprBuilder sym) => proxy sym -> t (LabeledPred (Pred sym) msg) -> ([LabeledPred (Pred sym) msg], [LabeledPred (Pred sym) msg], [LabeledPred (Pred sym) msg])

# Documentation

data LabeledPred pred msg Source #

Information about an assertion that was previously made.

Constructors

LabeledPred |

Fields

- _labeledPred :: !pred

  Predicate that was asserted.

- _labeledPredMsg :: !msg

  Message added when assumption/assertion was made.

#### Instances

Instances details

Bifoldable LabeledPred Source # |
Instance details Defined in What4.LabeledPred Methods bifold :: Monoid m => LabeledPred m m -> m Source # bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> LabeledPred a b -> m Source # bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> LabeledPred a b -> c Source # bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> LabeledPred a b -> c Source #
Bifunctor LabeledPred Source # |
Instance details Defined in What4.LabeledPred Methods bimap :: (a -> b) -> (c -> d) -> LabeledPred a c -> LabeledPred b d Source # first :: (a -> b) -> LabeledPred a c -> LabeledPred b c Source # second :: (b -> c) -> LabeledPred a b -> LabeledPred a c Source #
Bitraversable LabeledPred Source # |
Instance details Defined in What4.LabeledPred Methods bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> LabeledPred a b -> f (LabeledPred c d) Source #
Eq2 LabeledPred Source # |
Instance details Defined in What4.LabeledPred Methods liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> LabeledPred a c -> LabeledPred b d -> Bool Source #
Ord2 LabeledPred Source # |
Instance details Defined in What4.LabeledPred Methods liftCompare2 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> LabeledPred a c -> LabeledPred b d -> Ordering Source #
Show2 LabeledPred Source # |
Instance details Defined in What4.LabeledPred Methods liftShowsPrec2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> Int -> LabeledPred a b -> ShowS Source # liftShowList2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> [LabeledPred a b] -> ShowS Source #
Generic1 (LabeledPred pred :: Type -> Type) Source # |
Instance details Defined in What4.LabeledPred Associated Types type Rep1 (LabeledPred pred) :: k -> Type Source # Methods from1 :: forall (a :: k). LabeledPred pred a -> Rep1 (LabeledPred pred) a Source # to1 :: forall (a :: k). Rep1 (LabeledPred pred) a -> LabeledPred pred a Source #
Foldable (LabeledPred pred) Source # |

Instance details

Defined in What4.LabeledPred

Methods

fold :: Monoid m => LabeledPred pred m -> m Source #

foldMap :: Monoid m => (a -> m) -> LabeledPred pred a -> m Source #

foldMap' :: Monoid m => (a -> m) -> LabeledPred pred a -> m Source #

foldr :: (a -> b -> b) -> b -> LabeledPred pred a -> b Source #

foldr' :: (a -> b -> b) -> b -> LabeledPred pred a -> b Source #

foldl :: (b -> a -> b) -> b -> LabeledPred pred a -> b Source #

foldl' :: (b -> a -> b) -> b -> LabeledPred pred a -> b Source #

foldr1 :: (a -> a -> a) -> LabeledPred pred a -> a Source #

foldl1 :: (a -> a -> a) -> LabeledPred pred a -> a Source #

toList :: LabeledPred pred a -> [a] Source #

null :: LabeledPred pred a -> Bool Source #

length :: LabeledPred pred a -> Int Source #

elem :: Eq a => a -> LabeledPred pred a -> Bool Source #

maximum :: Ord a => LabeledPred pred a -> a Source #

minimum :: Ord a => LabeledPred pred a -> a Source #

sum :: Num a => LabeledPred pred a -> a Source #

product :: Num a => LabeledPred pred a -> a Source #

Eq pred => Eq1 (LabeledPred pred) Source # |
Instance details Defined in What4.LabeledPred Methods liftEq :: (a -> b -> Bool) -> LabeledPred pred a -> LabeledPred pred b -> Bool Source #
Ord pred => Ord1 (LabeledPred pred) Source # |
Instance details Defined in What4.LabeledPred Methods liftCompare :: (a -> b -> Ordering) -> LabeledPred pred a -> LabeledPred pred b -> Ordering Source #
Show pred => Show1 (LabeledPred pred) Source # |
Instance details Defined in What4.LabeledPred Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> LabeledPred pred a -> ShowS Source # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [LabeledPred pred a] -> ShowS Source #
Traversable (LabeledPred pred) Source # |

Instance details

Defined in What4.LabeledPred

Methods

traverse :: Applicative f => (a -> f b) -> LabeledPred pred a -> f (LabeledPred pred b) Source #

sequenceA :: Applicative f => LabeledPred pred (f a) -> f (LabeledPred pred a) Source #

mapM :: Monad m => (a -> m b) -> LabeledPred pred a -> m (LabeledPred pred b) Source #

sequence :: Monad m => LabeledPred pred (m a) -> m (LabeledPred pred a) Source #

Functor (LabeledPred pred) Source # |
Instance details Defined in What4.LabeledPred Methods fmap :: (a -> b) -> LabeledPred pred a -> LabeledPred pred b Source # (<$) :: a -> LabeledPred pred b -> LabeledPred pred a Source #
(Data pred, Data msg) => Data (LabeledPred pred msg) Source # |

Instance details

Defined in What4.LabeledPred

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LabeledPred pred msg -> c (LabeledPred pred msg) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LabeledPred pred msg) Source #

toConstr :: LabeledPred pred msg -> Constr Source #

dataTypeOf :: LabeledPred pred msg -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LabeledPred pred msg)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (LabeledPred pred msg)) Source #

gmapT :: (forall b. Data b => b -> b) -> LabeledPred pred msg -> LabeledPred pred msg Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LabeledPred pred msg -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> LabeledPred pred msg -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> LabeledPred pred msg -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LabeledPred pred msg -> m (LabeledPred pred msg) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LabeledPred pred msg -> m (LabeledPred pred msg) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LabeledPred pred msg -> m (LabeledPred pred msg) Source #

Generic (LabeledPred pred msg) Source # |
Instance details Defined in What4.LabeledPred Associated Types type Rep (LabeledPred pred msg) :: Type -> Type Source # Methods from :: LabeledPred pred msg -> Rep (LabeledPred pred msg) x Source # to :: Rep (LabeledPred pred msg) x -> LabeledPred pred msg Source #
(Show pred, Show msg) => Show (LabeledPred pred msg) Source # |
Instance details Defined in What4.LabeledPred Methods showsPrec :: Int -> LabeledPred pred msg -> ShowS Source # show :: LabeledPred pred msg -> String Source # showList :: [LabeledPred pred msg] -> ShowS Source #
(Eq pred, Eq msg) => Eq (LabeledPred pred msg) Source # |
Instance details Defined in What4.LabeledPred Methods (==) :: LabeledPred pred msg -> LabeledPred pred msg -> Bool Source # (/=) :: LabeledPred pred msg -> LabeledPred pred msg -> Bool Source #
(Ord pred, Ord msg) => Ord (LabeledPred pred msg) Source # |

Instance details

Defined in What4.LabeledPred

Methods

compare :: LabeledPred pred msg -> LabeledPred pred msg -> Ordering Source #

(<) :: LabeledPred pred msg -> LabeledPred pred msg -> Bool Source #

(<=) :: LabeledPred pred msg -> LabeledPred pred msg -> Bool Source #

(>) :: LabeledPred pred msg -> LabeledPred pred msg -> Bool Source #

(>=) :: LabeledPred pred msg -> LabeledPred pred msg -> Bool Source #

max :: LabeledPred pred msg -> LabeledPred pred msg -> LabeledPred pred msg Source #

min :: LabeledPred pred msg -> LabeledPred pred msg -> LabeledPred pred msg Source #

type Rep1 (LabeledPred pred :: Type -> Type) Source # |

Instance details

Defined in What4.LabeledPred

type Rep1 (LabeledPred pred :: Type -> Type) = D1 ('MetaData "LabeledPred" "What4.LabeledPred" "what4-1.5.1-9fvh8C3BlLdAuyfGuRwZek" 'False) (C1 ('MetaCons "LabeledPred" 'PrefixI 'True) (S1 ('MetaSel ('Just "_labeledPred") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 pred) :*: S1 ('MetaSel ('Just "_labeledPredMsg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) Par1))

type Rep (LabeledPred pred msg) Source # |

Instance details

Defined in What4.LabeledPred

type Rep (LabeledPred pred msg) = D1 ('MetaData "LabeledPred" "What4.LabeledPred" "what4-1.5.1-9fvh8C3BlLdAuyfGuRwZek" 'False) (C1 ('MetaCons "LabeledPred" 'PrefixI 'True) (S1 ('MetaSel ('Just "_labeledPred") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 pred) :*: S1 ('MetaSel ('Just "_labeledPredMsg") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 msg)))

labeledPred :: Lens (LabeledPred pred msg) (LabeledPred pred' msg) pred pred' Source #

Predicate that was asserted.

labeledPredMsg :: Lens (LabeledPred pred msg) (LabeledPred pred msg') msg msg' Source #

Message added when assumption/assertion was made.

partitionByPreds Source #

Arguments

:: (Foldable t, IsExprBuilder sym) |
=> proxy sym | avoid "ambiguous type variable" errors
-> (a -> Pred sym) |
-> t a |
-> ([a], [a], [a]) |

Partition datastructures containing predicates by their possibly concrete values.

The output format is (constantly true, constantly false, unknown/symbolic).

partitionByPredsM Source #

Arguments

:: (Monad m, Foldable t, IsExprBuilder sym) |
=> proxy sym | avoid "ambiguous type variable" errors
-> (a -> m (Pred sym)) |
-> t a |
-> m ([a], [a], [a]) |

Partition datastructures containing predicates by their possibly concrete values.

The output format is (constantly true, constantly false, unknown/symbolic).

partitionLabeledPreds Source #

Arguments

:: (Foldable t, IsExprBuilder sym) |
=> proxy sym | avoid "ambiguous type variable" errors
-> t (LabeledPred (Pred sym) msg) |
-> ([LabeledPred (Pred sym) msg], [LabeledPred (Pred sym) msg], [LabeledPred (Pred sym) msg]) |

Partition labeled predicates by their possibly concrete values.

The output format is (constantly true, constantly false, unknown/symbolic).