| Copyright | (c) Sirui Lu 2021-2024 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
Grisette.Core
Contents
- Organization of the module
- Note for the examples in the documentation
- Introduction to symbolic values in Grisette
- Solvable types
- Basic symbolic operations
- Unsolvable types and merging
- Pretty printing
- Symbolic Generation
- Error Handling
- Solver backend
- Substitutions for symbolic values given solver models
- Utilities
Description
Synopsis
- data Identifier where
- Identifier :: Text -> Identifier
- IdentifierWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => Identifier -> a -> Identifier
- data Symbol where
- SimpleSymbol :: Identifier -> Symbol
- IndexedSymbol :: Identifier -> Int -> Symbol
- identifier :: Text -> Identifier
- withInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => Identifier -> a -> Identifier
- withLoc :: Identifier -> SpliceQ Identifier
- uniqueIdentifier :: Text -> IO Identifier
- simple :: Identifier -> Symbol
- indexed :: Identifier -> Int -> Symbol
- symbolIdentifier :: Symbol -> Identifier
- modifyIdentifier :: (Identifier -> Identifier) -> Symbol -> Symbol
- class IsString t => Solvable c t | t -> c where
- con :: c -> t
- conView :: t -> Maybe c
- sym :: Symbol -> t
- ssym :: Identifier -> t
- isym :: Identifier -> Int -> t
- pattern Con :: Solvable c t => c -> t
- slocsym :: Solvable c s => Identifier -> SpliceQ s
- ilocsym :: Solvable c s => Identifier -> Int -> SpliceQ s
- class LogicalOp b where
- class ITEOp v where
- class SymEq a where
- class (forall a. SymEq a => SymEq (f a)) => SymEq1 f where
- symEq1 :: (SymEq a, SymEq1 f) => f a -> f a -> SymBool
- class (forall a. SymEq a => SymEq1 (f a)) => SymEq2 f where
- liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> f a c -> f b d -> SymBool
- symEq2 :: (SymEq a, SymEq b, SymEq2 f) => f a b -> f a b -> SymBool
- distinct :: Eq a => [a] -> Bool
- class SymEq a => SymOrd a where
- class (SymEq1 f, forall a. SymOrd a => SymOrd (f a)) => SymOrd1 f where
- liftSymCompare :: (a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
- symCompare1 :: (SymOrd1 f, SymOrd a) => f a -> f a -> Union Ordering
- class (SymEq2 f, forall a. SymOrd a => SymOrd1 (f a)) => SymOrd2 f where
- symCompare2 :: (SymOrd2 f, SymOrd a, SymOrd b) => f a b -> f a b -> Union Ordering
- symMax :: (SymOrd a, ITEOp a) => a -> a -> a
- symMin :: (SymOrd a, ITEOp a) => a -> a -> a
- mrgMax :: (SymOrd a, Mergeable a, SymBranching m, Applicative m) => a -> a -> m a
- mrgMin :: (SymOrd a, Mergeable a, SymBranching m, Applicative m) => a -> a -> m a
- class BV bv where
- bvExtract :: BV bv => Int -> Int -> bv -> bv
- class SizedBV bv where
- sizedBVConcat :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => bv l -> bv r -> bv (l + r)
- sizedBVZext :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> bv l -> bv r
- sizedBVSext :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> bv l -> bv r
- sizedBVExt :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> bv l -> bv r
- sizedBVSelect :: (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> bv n -> bv w
- sizedBVFromIntegral :: (Integral a, KnownNat n, 1 <= n) => a -> bv n
- sizedBVExtract :: forall p i q j n bv. (SizedBV bv, KnownNat n, KnownNat i, KnownNat j, 1 <= n, (i + 1) <= n, j <= i) => p i -> q j -> bv n -> bv ((i - j) + 1)
- class Bits a => SymShift a where
- symShift :: a -> a -> a
- symShiftNegated :: a -> a -> a
- class (MonadError e m, TryMerge m, Mergeable a) => SafeSymShift e a m where
- safeSymShiftL :: a -> a -> m a
- safeSymShiftR :: a -> a -> m a
- safeSymStrictShiftL :: a -> a -> m a
- safeSymStrictShiftR :: a -> a -> m a
- class Bits a => SymRotate a where
- symRotate :: a -> a -> a
- symRotateNegated :: a -> a -> a
- class (MonadError e m, TryMerge m, Mergeable a) => SafeSymRotate e a m where
- safeSymRotateL :: a -> a -> m a
- safeSymRotateR :: a -> a -> m a
- class SignConversion ubv sbv | ubv -> sbv, sbv -> ubv where
- toSigned :: ubv -> sbv
- toUnsigned :: sbv -> ubv
- class DivOr a where
- divOrZero :: (DivOr a, Num a) => a -> a -> a
- modOrDividend :: (DivOr a, Num a) => a -> a -> a
- quotOrZero :: (DivOr a, Num a) => a -> a -> a
- remOrDividend :: (DivOr a, Num a) => a -> a -> a
- divModOrZeroDividend :: (DivOr a, Num a) => a -> a -> (a, a)
- quotRemOrZeroDividend :: (DivOr a, Num a) => a -> a -> (a, a)
- class (MonadError e m, TryMerge m, Mergeable a, DivOr a) => SafeDiv e a m where
- safeDiv :: a -> a -> m a
- safeMod :: a -> a -> m a
- safeDivMod :: a -> a -> m (a, a)
- safeQuot :: a -> a -> m a
- safeRem :: a -> a -> m a
- safeQuotRem :: a -> a -> m (a, a)
- class (MonadError e m, TryMerge m, Mergeable a) => SafeLinearArith e a m where
- class FdivOr a where
- fdivOrZero :: (FdivOr a, Num a) => a -> a -> a
- recipOrZero :: (FdivOr a, Num a) => a -> a
- class (MonadError e m, TryMerge m, Mergeable a) => SafeFdiv e a m where
- class LogBaseOr a where
- logBaseOr :: a -> a -> a -> a
- logBaseOrZero :: (LogBaseOr a, Num a) => a -> a -> a
- class (MonadError e m, TryMerge m, Mergeable a) => SafeLogBase e a m where
- safeLogBase :: a -> a -> m a
- class Function f arg ret | f -> arg ret where
- (#) :: f -> arg -> ret
- class Apply uf where
- fpIsNaN :: RealFloat a => a -> Bool
- fpIsPositiveZero :: RealFloat a => a -> Bool
- fpIsNegativeZero :: RealFloat a => a -> Bool
- fpIsPositiveInfinite :: RealFloat a => a -> Bool
- fpIsNegativeInfinite :: RealFloat a => a -> Bool
- fpIsPositive :: RealFloat a => a -> Bool
- fpIsNegative :: RealFloat a => a -> Bool
- fpIsInfinite :: RealFloat a => a -> Bool
- fpIsZero :: RealFloat a => a -> Bool
- fpIsNormal :: RealFloat a => a -> Bool
- fpIsSubnormal :: RealFloat a => a -> Bool
- fpIsPoint :: RealFloat a => a -> Bool
- class SymIEEEFPTraits a where
- symFpIsNaN :: a -> SymBool
- symFpIsPositive :: a -> SymBool
- symFpIsNegative :: a -> SymBool
- symFpIsPositiveInfinite :: a -> SymBool
- symFpIsNegativeInfinite :: a -> SymBool
- symFpIsInfinite :: a -> SymBool
- symFpIsPositiveZero :: a -> SymBool
- symFpIsNegativeZero :: a -> SymBool
- symFpIsZero :: a -> SymBool
- symFpIsNormal :: a -> SymBool
- symFpIsSubnormal :: a -> SymBool
- symFpIsPoint :: a -> SymBool
- class IEEEFPConstants a where
- fpPositiveInfinite :: a
- fpNegativeInfinite :: a
- fpNaN :: a
- fpNegativeZero :: a
- fpPositiveZero :: a
- fpMinNormalized :: a
- fpMinSubnormal :: a
- fpMaxNormalized :: a
- fpMaxSubnormal :: a
- class IEEEFPRoundingMode mode where
- class IEEEFPOp a where
- fpAbs :: a -> a
- fpNeg :: a -> a
- fpRem :: a -> a -> a
- fpMinimum :: a -> a -> a
- fpMinimumNumber :: a -> a -> a
- fpMaximum :: a -> a -> a
- fpMaximumNumber :: a -> a -> a
- class IEEEFPRoundingMode mode => IEEEFPRoundingOp a mode | a -> mode where
- class IEEEFPConvertible a fp mode | fp -> mode where
- class (IEEEFPConvertible a fp mode, IEEEFPRoundingMode mode) => IEEEFPToAlgReal a fp mode | fp -> mode where
- fpToAlgReal :: a -> fp -> a
- class ToCon a b where
- class (forall a b. ToCon a b => ToCon (f1 a) (f2 b)) => ToCon1 f1 f2 where
- toCon1 :: (ToCon1 f1 f2, ToCon a b) => f1 a -> Maybe (f2 b)
- class (forall a b. ToCon a b => ToCon1 (f1 a) (f2 b)) => ToCon2 f1 f2 where
- liftToCon2 :: (a -> Maybe b) -> (c -> Maybe d) -> f1 a c -> Maybe (f2 b d)
- toCon2 :: (ToCon2 f1 f2, ToCon a b, ToCon c d) => f1 a c -> Maybe (f2 b d)
- class Mergeable b => ToSym a b where
- toSym :: a -> b
- class (forall a b. ToSym a b => ToSym (f1 a) (f2 b), Mergeable1 f2) => ToSym1 f1 f2 where
- toSym1 :: (ToSym1 f1 f2, ToSym a b) => f1 a -> f2 b
- class (forall a b. ToSym a b => ToSym1 (f1 a) (f2 b), Mergeable2 f2) => ToSym2 f1 f2 where
- liftToSym2 :: (a -> b) -> (c -> d) -> f1 a c -> f2 b d
- toSym2 :: (ToSym2 f1 f2, ToSym a b, ToSym c d) => f1 a c -> f2 b d
- class BitCast from to where
- bitCast :: from -> to
- class BitCastCanonical from to where
- bitCastCanonicalValue :: proxy from -> to
- class BitCastOr from to where
- bitCastOr :: to -> from -> to
- type BitCastOrCanonical a b = (BitCastCanonical a b, BitCastOr a b)
- bitCastOrCanonical :: BitCastOrCanonical from to => from -> to
- class (MonadError e m, TryMerge m, Mergeable b, BitCastOr a b) => SafeBitCast e a b m where
- safeBitCast :: a -> m b
- class SymFromIntegral from to where
- symFromIntegral :: from -> to
- data Union a
- class (Eq t, Ord t, Hashable t) => IsConcrete t
- unionUnaryOp :: (a -> a) -> Union a -> Union a
- unionBinOp :: (a -> a -> a) -> Union a -> Union a -> Union a
- liftUnion :: forall u a. (Mergeable a, SymBranching u, Applicative u) => Union a -> u a
- unionMergingStrategy :: Union a -> Maybe (MergingStrategy a)
- liftToMonadUnion :: (Mergeable a, MonadUnion u) => Union a -> u a
- unionSize :: Union a -> Int
- class Mergeable a where
- class (forall a. Mergeable a => Mergeable (u a)) => Mergeable1 (u :: Type -> Type) where
- liftRootStrategy :: MergingStrategy a -> MergingStrategy (u a)
- rootStrategy1 :: (Mergeable a, Mergeable1 u) => MergingStrategy (u a)
- class (forall a. Mergeable a => Mergeable1 (u a)) => Mergeable2 (u :: Type -> Type -> Type) where
- liftRootStrategy2 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b)
- rootStrategy2 :: (Mergeable a, Mergeable b, Mergeable2 u) => MergingStrategy (u a b)
- class (forall a. Mergeable a => Mergeable2 (u a)) => Mergeable3 (u :: Type -> Type -> Type -> Type) where
- liftRootStrategy3 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy c -> MergingStrategy (u a b c)
- rootStrategy3 :: (Mergeable a, Mergeable b, Mergeable c, Mergeable3 u) => MergingStrategy (u a b c)
- data MergingStrategy a where
- SimpleStrategy :: (SymBool -> a -> a -> a) -> MergingStrategy a
- SortedStrategy :: (Ord idx, Typeable idx, Show idx) => (a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
- NoStrategy :: MergingStrategy a
- wrapStrategy :: MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
- product2Strategy :: (a -> b -> r) -> (r -> (a, b)) -> MergingStrategy a -> MergingStrategy b -> MergingStrategy r
- data DynamicSortedIdx where
- DynamicSortedIdx :: forall idx. (Show idx, Ord idx, Typeable idx) => idx -> DynamicSortedIdx
- data StrategyList container where
- StrategyList :: forall a container. container [DynamicSortedIdx] -> container (MergingStrategy a) -> StrategyList container
- buildStrategyList :: forall a container. Functor container => MergingStrategy a -> container a -> StrategyList container
- resolveStrategy :: forall x. MergingStrategy x -> x -> ([DynamicSortedIdx], MergingStrategy x)
- resolveStrategy' :: forall x. x -> MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x)
- class Mergeable a => SimpleMergeable a where
- class (Mergeable1 u, forall a. SimpleMergeable a => SimpleMergeable (u a)) => SimpleMergeable1 u where
- liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> u a -> u a -> u a
- mrgIte1 :: (SimpleMergeable1 u, SimpleMergeable a) => SymBool -> u a -> u a -> u a
- class (Mergeable2 u, forall a. SimpleMergeable a => SimpleMergeable1 (u a)) => SimpleMergeable2 u where
- liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> u a b -> u a b -> u a b
- mrgIte2 :: (SimpleMergeable2 u, SimpleMergeable a, SimpleMergeable b) => SymBool -> u a b -> u a b -> u a b
- class (SimpleMergeable1 u, forall a. Mergeable a => SimpleMergeable (u a), TryMerge u) => SymBranching (u :: Type -> Type) where
- mrgIfWithStrategy :: MergingStrategy a -> SymBool -> u a -> u a -> u a
- mrgIfPropagatedStrategy :: SymBool -> u a -> u a -> u a
- mrgIf :: (SymBranching u, Mergeable a) => SymBool -> u a -> u a -> u a
- mergeWithStrategy :: SymBranching m => MergingStrategy a -> m a -> m a
- merge :: (SymBranching m, Mergeable a) => m a -> m a
- type MonadTryMerge f = (TryMerge f, Monad f)
- class TryMerge m where
- tryMergeWithStrategy :: MergingStrategy a -> m a -> m a
- mrgSingle :: (TryMerge m, Applicative m, Mergeable a) => a -> m a
- mrgSingleWithStrategy :: (TryMerge m, Applicative m) => MergingStrategy a -> a -> m a
- tryMerge :: (TryMerge m, Mergeable a) => m a -> m a
- class (Applicative u, SymBranching u) => PlainUnion (u :: Type -> Type) where
- singleView :: u a -> Maybe a
- ifView :: u a -> Maybe (SymBool, u a, u a)
- toGuardedList :: u a -> [(SymBool, a)]
- overestimateUnionValues :: Mergeable a => u a -> [a]
- pattern Single :: (PlainUnion u, Mergeable a) => a -> u a
- pattern If :: (PlainUnion u, Mergeable a) => SymBool -> u a -> u a -> u a
- simpleMerge :: forall u a. (SimpleMergeable a, PlainUnion u) => u a -> a
- (.#) :: (Function f a r, SimpleMergeable r, PlainUnion u) => f -> u a -> r
- onUnion :: forall u a r. (SimpleMergeable r, SymBranching u, PlainUnion u, Mergeable a) => (a -> r) -> u a -> r
- onUnion2 :: forall u a b r. (SimpleMergeable r, SymBranching u, PlainUnion u, Mergeable a, Mergeable b) => (a -> b -> r) -> u a -> u b -> r
- onUnion3 :: forall u a b c r. (SimpleMergeable r, SymBranching u, PlainUnion u, Mergeable a, Mergeable b, Mergeable c) => (a -> b -> c -> r) -> u a -> u b -> u c -> r
- onUnion4 :: forall u a b c d r. (SimpleMergeable r, SymBranching u, PlainUnion u, Mergeable a, Mergeable b, Mergeable c, Mergeable d) => (a -> b -> c -> d -> r) -> u a -> u b -> u c -> u d -> r
- type MonadUnion u = (SymBranching u, Monad u)
- class PPrint a where
- pformat :: a -> Doc ann
- pformatPrec :: Int -> a -> Doc ann
- pformatList :: [a] -> Doc ann
- docToTextWith :: LayoutOptions -> Doc ann -> Text
- docToTextWithWidth :: Int -> Doc ann -> Text
- docToText :: Doc ann -> Text
- pformatTextWith :: PPrint a => LayoutOptions -> a -> Text
- pformatTextWithWidth :: PPrint a => Int -> a -> Text
- pformatText :: PPrint a => a -> Text
- pprint :: PPrint a => a -> IO ()
- class (forall a. PPrint a => PPrint (f a)) => PPrint1 f where
- pformatPrec1 :: (PPrint1 f, PPrint a) => Int -> f a -> Doc ann
- pformatList1 :: (PPrint1 f, PPrint a) => [f a] -> Doc ann
- class (forall a. PPrint a => PPrint1 (f a), forall a b. (PPrint a, PPrint b) => PPrint (f a b)) => PPrint2 f where
- pformatPrec2 :: (PPrint2 f, PPrint a, PPrint b) => Int -> f a b -> Doc ann
- pformatList2 :: (PPrint2 f, PPrint a, PPrint b) => [f a b] -> Doc ann
- groupedEnclose :: Doc ann -> Doc ann -> Doc ann -> Doc ann
- condEnclose :: Bool -> Doc ann -> Doc ann -> Doc ann -> Doc ann
- pformatWithConstructor :: Int -> Doc ann -> [Doc ann] -> Doc ann
- pformatWithConstructorNoAlign :: Int -> Doc ann -> [Doc ann] -> Doc ann
- viaShowsPrec :: (Int -> a -> ShowS) -> Int -> a -> Doc ann
- module Prettyprinter
- newtype FreshIndex = FreshIndex Int
- class Monad m => MonadFresh m where
- getFreshIndex :: m FreshIndex
- setFreshIndex :: FreshIndex -> m ()
- getIdentifier :: m Identifier
- localIdentifier :: (Identifier -> Identifier) -> m a -> m a
- nextFreshIndex :: MonadFresh m => m FreshIndex
- liftFresh :: MonadFresh m => Fresh a -> m a
- type Fresh = FreshT Identity
- newtype FreshT m a = FreshT {
- runFreshTFromIndex :: Identifier -> FreshIndex -> m (a, FreshIndex)
- runFresh :: Fresh a -> Identifier -> a
- runFreshT :: Monad m => FreshT m a -> Identifier -> m a
- mrgRunFreshT :: (Monad m, TryMerge m, Mergeable a) => FreshT m a -> Identifier -> m a
- freshString :: (MonadFresh m, IsString s) => String -> m s
- class Mergeable a => GenSym spec a where
- fresh :: MonadFresh m => spec -> m (Union a)
- class GenSymSimple spec a where
- simpleFresh :: MonadFresh m => spec -> m a
- genSym :: GenSym spec a => spec -> Identifier -> Union a
- genSymSimple :: forall spec a. GenSymSimple spec a => spec -> Identifier -> a
- derivedNoSpecFresh :: forall a m. (Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) => () -> m (Union a)
- derivedNoSpecSimpleFresh :: forall a m. (Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) => () -> m a
- derivedSameShapeSimpleFresh :: forall a m. (Generic a, GenSymSameShape (Rep a), MonadFresh m) => a -> m a
- chooseFresh :: forall a m. (Mergeable a, MonadFresh m) => [a] -> m (Union a)
- chooseSimpleFresh :: forall a m. (SimpleMergeable a, MonadFresh m) => [a] -> m a
- chooseUnionFresh :: forall a m. (Mergeable a, MonadFresh m) => [Union a] -> m (Union a)
- choose :: forall a. Mergeable a => [a] -> Identifier -> Union a
- chooseSimple :: forall a. SimpleMergeable a => [a] -> Identifier -> a
- chooseUnion :: forall a. Mergeable a => [Union a] -> Identifier -> Union a
- data EnumGenBound a = EnumGenBound a a
- newtype EnumGenUpperBound a = EnumGenUpperBound a
- data ListSpec spec = ListSpec {
- genListMinLength :: Int
- genListMaxLength :: Int
- genListSubSpec :: spec
- data SimpleListSpec spec = SimpleListSpec {
- genSimpleListLength :: Int
- genSimpleListSubSpec :: spec
- data AssertionError = AssertionError
- data VerificationConditions
- class TransformError from to where
- transformError :: from -> to
- symAssert :: (TransformError AssertionError to, Mergeable to, MonadError to erm, MonadUnion erm) => SymBool -> erm ()
- symAssume :: (TransformError VerificationConditions to, Mergeable to, MonadError to erm, MonadUnion erm) => SymBool -> erm ()
- symAssertWith :: (Mergeable e, MonadError e erm, MonadUnion erm) => e -> SymBool -> erm ()
- symAssertTransformableError :: (Mergeable to, TransformError from to, MonadError to erm, MonadUnion erm) => from -> SymBool -> erm ()
- symThrowTransformableError :: (Mergeable to, Mergeable a, TransformError from to, MonadError to erm, MonadUnion erm) => from -> erm a
- newtype CBMCEither a b = CBMCEither {
- runCBMCEither :: Either a b
- newtype CBMCExceptT e m a = CBMCExceptT {
- runCBMCExceptT :: m (CBMCEither e a)
- cbmcExcept :: Monad m => Either e a -> CBMCExceptT e m a
- mapCBMCExceptT :: (m (Either e a) -> n (Either e' b)) -> CBMCExceptT e m a -> CBMCExceptT e' n b
- withCBMCExceptT :: Functor m => (e -> e') -> CBMCExceptT e m a -> CBMCExceptT e' m a
- data SolvingFailure
- class Monad m => MonadicSolver m where
- monadicSolverPush :: Int -> m ()
- monadicSolverPop :: Int -> m ()
- monadicSolverResetAssertions :: m ()
- monadicSolverAssert :: SymBool -> m ()
- monadicSolverCheckSat :: m (Either SolvingFailure Model)
- monadicSolverSolve :: MonadicSolver m => SymBool -> m (Either SolvingFailure Model)
- data SolverCommand
- class Solver handle => ConfigurableSolver config handle | config -> handle where
- class Solver handle where
- solverRunCommand :: (handle -> IO (Either SolvingFailure a)) -> handle -> SolverCommand -> IO (Either SolvingFailure a)
- solverAssert :: handle -> SymBool -> IO (Either SolvingFailure ())
- solverCheckSat :: handle -> IO (Either SolvingFailure Model)
- solverPush :: handle -> Int -> IO (Either SolvingFailure ())
- solverPop :: handle -> Int -> IO (Either SolvingFailure ())
- solverResetAssertions :: handle -> IO (Either SolvingFailure ())
- solverTerminate :: handle -> IO ()
- solverForceTerminate :: handle -> IO ()
- solverSolve :: Solver handle => handle -> SymBool -> IO (Either SolvingFailure Model)
- withSolver :: ConfigurableSolver config handle => config -> (handle -> IO a) -> IO a
- solve :: ConfigurableSolver config handle => config -> SymBool -> IO (Either SolvingFailure Model)
- solverSolveMulti :: Solver handle => handle -> Int -> SymBool -> IO ([Model], SolvingFailure)
- solveMulti :: ConfigurableSolver config handle => config -> Int -> SymBool -> IO ([Model], SolvingFailure)
- class UnionWithExcept t u e v | t -> u e v where
- extractUnionExcept :: t -> u (Either e v)
- solverSolveExcept :: (UnionWithExcept t u e v, PlainUnion u, Functor u, Solver handle) => handle -> (Either e v -> SymBool) -> t -> IO (Either SolvingFailure Model)
- solveExcept :: (UnionWithExcept t u e v, PlainUnion u, Functor u, ConfigurableSolver config handle) => config -> (Either e v -> SymBool) -> t -> IO (Either SolvingFailure Model)
- solverSolveMultiExcept :: (UnionWithExcept t u e v, PlainUnion u, Functor u, Solver handle) => handle -> Int -> (Either e v -> SymBool) -> t -> IO ([Model], SolvingFailure)
- solveMultiExcept :: (UnionWithExcept t u e v, PlainUnion u, Functor u, ConfigurableSolver config handle) => config -> Int -> (Either e v -> SymBool) -> t -> IO ([Model], SolvingFailure)
- data VerifierResult cex exception
- = CEGISVerifierFoundCex cex
- | CEGISVerifierNoCex
- | CEGISVerifierException exception
- type SynthesisConstraintFun cex = cex -> IO SymBool
- type VerifierFun cex exception = Model -> IO (VerifierResult cex exception)
- data CEGISResult exception
- = CEGISSuccess Model
- | CEGISVerifierFailure exception
- | CEGISSolverFailure SolvingFailure
- solverGenericCEGIS :: Solver handle => handle -> Bool -> SymBool -> SynthesisConstraintFun input -> [VerifierFun input exception] -> IO ([input], CEGISResult exception)
- solverGenericCEGISWithRefinement :: Solver handle => handle -> Bool -> SymBool -> SynthesisConstraintFun input -> Maybe RefinementConditionFun -> [VerifierFun input exception] -> IO ([input], CEGISResult exception)
- genericCEGIS :: ConfigurableSolver config handle => config -> Bool -> SymBool -> SynthesisConstraintFun input -> [VerifierFun input exception] -> IO ([input], CEGISResult exception)
- genericCEGISWithRefinement :: ConfigurableSolver config handle => config -> Bool -> SymBool -> SynthesisConstraintFun input -> Maybe RefinementConditionFun -> [VerifierFun input exception] -> IO ([input], CEGISResult exception)
- data CEGISCondition = CEGISCondition SymBool SymBool
- solverCegisMultiInputs :: (EvalSym input, ExtractSym input, Solver handle) => handle -> handle -> [input] -> (input -> CEGISCondition) -> IO ([input], CEGISResult SolvingFailure)
- solverCegis :: (Solver handle, EvalSym inputs, ExtractSym inputs, SymEq inputs) => handle -> handle -> inputs -> (inputs -> CEGISCondition) -> IO ([inputs], CEGISResult SolvingFailure)
- solverCegisExcept :: (UnionWithExcept t u e v, PlainUnion u, Functor u, EvalSym inputs, ExtractSym inputs, Solver handle, SymEq inputs) => handle -> handle -> inputs -> (Either e v -> CEGISCondition) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure)
- solverCegisExceptStdVC :: (UnionWithExcept t u VerificationConditions (), PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, Solver handle, SymEq inputs) => handle -> handle -> inputs -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure)
- solverCegisExceptVC :: (UnionWithExcept t u e v, PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, Solver handle, SymEq inputs) => handle -> handle -> inputs -> (Either e v -> u (Either VerificationConditions ())) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure)
- solverCegisExceptMultiInputs :: (Solver handle, EvalSym inputs, ExtractSym inputs, UnionWithExcept t u e v, PlainUnion u, Monad u) => handle -> handle -> [inputs] -> (Either e v -> CEGISCondition) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure)
- solverCegisExceptStdVCMultiInputs :: (Solver handle, EvalSym inputs, ExtractSym inputs, UnionWithExcept t u VerificationConditions (), PlainUnion u, Monad u) => handle -> handle -> [inputs] -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure)
- solverCegisExceptVCMultiInputs :: (Solver handle, EvalSym inputs, ExtractSym inputs, UnionWithExcept t u e v, PlainUnion u, Monad u) => handle -> handle -> [inputs] -> (Either e v -> u (Either VerificationConditions ())) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure)
- solverCegisForAll :: (ExtractSym forallInput, Solver handle) => handle -> handle -> forallInput -> CEGISCondition -> IO ([Model], CEGISResult SolvingFailure)
- solverCegisForAllExcept :: (UnionWithExcept t u e v, PlainUnion u, Functor u, EvalSym inputs, ExtractSym inputs, Solver handle, SymEq inputs) => handle -> handle -> inputs -> (Either e v -> CEGISCondition) -> t -> IO ([Model], CEGISResult SolvingFailure)
- solverCegisForAllExceptStdVC :: (UnionWithExcept t u VerificationConditions (), PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, Solver handle, SymEq inputs) => handle -> handle -> inputs -> t -> IO ([Model], CEGISResult SolvingFailure)
- solverCegisForAllExceptVC :: (UnionWithExcept t u e v, PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, Solver handle, SymEq inputs) => handle -> handle -> inputs -> (Either e v -> u (Either VerificationConditions ())) -> t -> IO ([Model], CEGISResult SolvingFailure)
- cegisPostCond :: SymBool -> CEGISCondition
- cegisPrePost :: SymBool -> SymBool -> CEGISCondition
- cegisMultiInputs :: (EvalSym input, ExtractSym input, ConfigurableSolver config handle) => config -> [input] -> (input -> CEGISCondition) -> IO ([input], CEGISResult SolvingFailure)
- cegis :: (ConfigurableSolver config handle, EvalSym inputs, ExtractSym inputs, SymEq inputs) => config -> inputs -> (inputs -> CEGISCondition) -> IO ([inputs], CEGISResult SolvingFailure)
- cegisExcept :: (UnionWithExcept t u e v, PlainUnion u, Functor u, EvalSym inputs, ExtractSym inputs, ConfigurableSolver config handle, SymEq inputs) => config -> inputs -> (Either e v -> CEGISCondition) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure)
- cegisExceptStdVC :: (UnionWithExcept t u VerificationConditions (), PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, ConfigurableSolver config handle, SymEq inputs) => config -> inputs -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure)
- cegisExceptVC :: (UnionWithExcept t u e v, PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, ConfigurableSolver config handle, SymEq inputs) => config -> inputs -> (Either e v -> u (Either VerificationConditions ())) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure)
- cegisExceptMultiInputs :: (ConfigurableSolver config handle, EvalSym inputs, ExtractSym inputs, UnionWithExcept t u e v, PlainUnion u, Monad u) => config -> [inputs] -> (Either e v -> CEGISCondition) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure)
- cegisExceptStdVCMultiInputs :: (ConfigurableSolver config handle, EvalSym inputs, ExtractSym inputs, UnionWithExcept t u VerificationConditions (), PlainUnion u, Monad u) => config -> [inputs] -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure)
- cegisExceptVCMultiInputs :: (ConfigurableSolver config handle, EvalSym inputs, ExtractSym inputs, UnionWithExcept t u e v, PlainUnion u, Monad u) => config -> [inputs] -> (Either e v -> u (Either VerificationConditions ())) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure)
- cegisForAll :: (ExtractSym forallInput, ConfigurableSolver config handle) => config -> forallInput -> CEGISCondition -> IO ([Model], CEGISResult SolvingFailure)
- cegisForAllExcept :: (UnionWithExcept t u e v, PlainUnion u, Functor u, EvalSym inputs, ExtractSym inputs, ConfigurableSolver config handle, SymEq inputs) => config -> inputs -> (Either e v -> CEGISCondition) -> t -> IO ([Model], CEGISResult SolvingFailure)
- cegisForAllExceptStdVC :: (UnionWithExcept t u VerificationConditions (), PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, ConfigurableSolver config handle, SymEq inputs) => config -> inputs -> t -> IO ([Model], CEGISResult SolvingFailure)
- cegisForAllExceptVC :: (UnionWithExcept t u e v, PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, ConfigurableSolver config handle, SymEq inputs) => config -> inputs -> (Either e v -> u (Either VerificationConditions ())) -> t -> IO ([Model], CEGISResult SolvingFailure)
- class Monoid symbolSet => SymbolSetOps symbolSet (typedSymbol :: Type -> Type) | symbolSet -> typedSymbol where
- emptySet :: symbolSet
- isEmptySet :: symbolSet -> Bool
- containsSymbol :: forall a. typedSymbol a -> symbolSet -> Bool
- insertSymbol :: forall a. typedSymbol a -> symbolSet -> symbolSet
- intersectionSet :: symbolSet -> symbolSet -> symbolSet
- unionSet :: symbolSet -> symbolSet -> symbolSet
- differenceSet :: symbolSet -> symbolSet -> symbolSet
- class SymbolSetOps symbolSet typedSymbol => SymbolSetRep rep symbolSet (typedSymbol :: Type -> Type) where
- buildSymbolSet :: rep -> symbolSet
- class ExtractSym a where
- extractSym :: a -> AnySymbolSet
- extractSymMaybe :: IsSymbolKind knd => a -> Maybe (SymbolSet knd)
- class (forall a. ExtractSym a => ExtractSym (f a)) => ExtractSym1 f where
- liftExtractSymMaybe :: IsSymbolKind knd => (a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
- extractSym1 :: (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) => f a -> SymbolSet knd
- extractSymMaybe1 :: (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) => f a -> Maybe (SymbolSet knd)
- class (forall a. ExtractSym a => ExtractSym1 (f a)) => ExtractSym2 f where
- liftExtractSymMaybe2 :: IsSymbolKind knd => (a -> Maybe (SymbolSet knd)) -> (b -> Maybe (SymbolSet knd)) -> f a b -> Maybe (SymbolSet knd)
- extractSym2 :: (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) => f a b -> SymbolSet knd
- extractSymMaybe2 :: (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) => f a b -> Maybe (SymbolSet knd)
- class SymbolSetOps symbolSet typedSymbol => ModelOps model symbolSet typedSymbol | model -> symbolSet typedSymbol where
- emptyModel :: model
- isEmptyModel :: model -> Bool
- modelContains :: typedSymbol a -> model -> Bool
- valueOf :: typedSymbol t -> model -> Maybe t
- insertValue :: typedSymbol t -> t -> model -> model
- exceptFor :: symbolSet -> model -> model
- exceptFor' :: typedSymbol t -> model -> model
- restrictTo :: symbolSet -> model -> model
- extendTo :: symbolSet -> model -> model
- exact :: symbolSet -> model -> model
- class ModelRep rep model | rep -> model where
- buildModel :: rep -> model
- class EvalSym a where
- evalSymToCon :: (ToCon a b, EvalSym a) => Model -> a -> b
- class (forall a. EvalSym a => EvalSym (f a)) => EvalSym1 f where
- liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
- evalSym1 :: (EvalSym1 f, EvalSym a) => Bool -> Model -> f a -> f a
- evalSymToCon1 :: (EvalSym1 f, EvalSym a, ToCon1 f g, ToCon a b) => Model -> f a -> g b
- class (forall a. EvalSym a => EvalSym1 (f a)) => EvalSym2 f where
- evalSym2 :: (EvalSym2 f, EvalSym a, EvalSym b) => Bool -> Model -> f a b -> f a b
- evalSymToCon2 :: (EvalSym2 f, EvalSym a, EvalSym c, ToCon2 f g, ToCon a b, ToCon c d) => Model -> f a c -> g b d
- class SubstSym a where
- substSym :: (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> a -> a
- class (forall a. SubstSym a => SubstSym (f a)) => SubstSym1 f where
- liftSubstSym :: (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> f a -> f a
- substSym1 :: (SubstSym1 f, SubstSym a, LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> f a -> f a
- class (forall a. SubstSym a => SubstSym1 (f a)) => SubstSym2 f where
- liftSubstSym2 :: (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> f a b -> f a b
- substSym2 :: (SubstSym2 f, SubstSym a, SubstSym b, LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> f a b -> f a b
- htmemo :: (Eq k, Hashable k) => (k -> a) -> k -> a
- htmemo2 :: (Eq k1, Hashable k1, Eq k2, Hashable k2) => (k1 -> k2 -> a) -> k1 -> k2 -> a
- htmemo3 :: (Eq k1, Hashable k1, Eq k2, Hashable k2, Eq k3, Hashable k3) => (k1 -> k2 -> k3 -> a) -> k1 -> k2 -> k3 -> a
- htmup :: (Eq k, Hashable k) => (b -> c) -> (k -> b) -> k -> c
- htmemoFix :: (Eq k, Hashable k) => ((k -> a) -> k -> a) -> k -> a
- newtype Default a = Default {
- unDefault :: a
- newtype Default1 (f :: Type -> Type) a = Default1 {
- unDefault1 :: f a
- data family SymEqArgs arity a b :: Type
- class GSymEq arity f where
- genericSymEq :: (Generic a, GSymEq Arity0 (Rep a)) => a -> a -> SymBool
- genericLiftSymEq :: (Generic1 f, GSymEq Arity1 (Rep1 f)) => (a -> b -> SymBool) -> f a -> f b -> SymBool
- data family SymOrdArgs arity a b :: Type
- class GSymOrd arity f where
- gsymCompare :: SymOrdArgs arity a b -> f a -> f b -> Union Ordering
- genericSymCompare :: (Generic a, GSymOrd Arity0 (Rep a)) => a -> a -> Union Ordering
- genericLiftSymCompare :: (Generic1 f, GSymOrd Arity1 (Rep1 f)) => (a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
- data family MergeableArgs arity a :: Type
- class GMergeable arity f where
- grootStrategy :: MergeableArgs arity a -> MergingStrategy (f a)
- genericRootStrategy :: (Generic a, GMergeable Arity0 (Rep a)) => MergingStrategy a
- genericLiftRootStrategy :: (Generic1 f, GMergeable Arity1 (Rep1 f)) => MergingStrategy a -> MergingStrategy (f a)
- data family SimpleMergeableArgs arity a :: Type
- class GSimpleMergeable arity f where
- gmrgIte :: SimpleMergeableArgs arity a -> SymBool -> f a -> f a -> f a
- genericMrgIte :: (Generic a, GSimpleMergeable Arity0 (Rep a)) => SymBool -> a -> a -> a
- genericLiftMrgIte :: (Generic1 f, GSimpleMergeable Arity1 (Rep1 f)) => (SymBool -> a -> a -> a) -> SymBool -> f a -> f a -> f a
- data family ToConArgs arity a b :: Type
- class GToCon arity f1 f2 where
- genericToCon :: (Generic a, Generic b, GToCon Arity0 (Rep a) (Rep b)) => a -> Maybe b
- genericLiftToCon :: (Generic1 f1, Generic1 f2, GToCon Arity1 (Rep1 f1) (Rep1 f2)) => (a -> Maybe b) -> f1 a -> Maybe (f2 b)
- data family ToSymArgs arity a b :: Type
- class GToSym arity f1 f2 where
- genericToSym :: (Generic a, Generic b, GToSym Arity0 (Rep a) (Rep b)) => a -> b
- genericLiftToSym :: (Generic1 f1, Generic1 f2, GToSym Arity1 (Rep1 f1) (Rep1 f2), Mergeable b) => (a -> b) -> f1 a -> f2 b
- data family EvalSymArgs arity a :: Type
- class GEvalSym arity f where
- gevalSym :: EvalSymArgs arity a -> Bool -> Model -> f a -> f a
- genericEvalSym :: (Generic a, GEvalSym Arity0 (Rep a)) => Bool -> Model -> a -> a
- genericLiftEvalSym :: (Generic1 f, GEvalSym Arity1 (Rep1 f)) => (Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
- data family ExtractSymArgs arity (knd :: SymbolKind) a :: Type
- class GExtractSym arity f where
- gextractSymMaybe :: IsSymbolKind knd => ExtractSymArgs arity knd a -> f a -> Maybe (SymbolSet knd)
- genericExtractSymMaybe :: (Generic a, GExtractSym Arity0 (Rep a), IsSymbolKind knd) => a -> Maybe (SymbolSet knd)
- genericLiftExtractSymMaybe :: (Generic1 f, GExtractSym Arity1 (Rep1 f), IsSymbolKind knd) => (a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
- data family SubstSymArgs arity (knd :: SymbolKind) a cb sb :: Type
- class GSubstSym arity f where
- gsubstSym :: (LinkedRep cb sb, IsSymbolKind knd) => SubstSymArgs arity knd a cb sb -> TypedSymbol knd cb -> sb -> f a -> f a
- genericSubstSym :: (Generic a, GSubstSym Arity0 (Rep a), LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> a -> a
- genericLiftSubstSym :: (Generic1 f, GSubstSym Arity1 (Rep1 f), LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> f a -> f a
- genericPFormatPrec :: (Generic a, GPPrint Arity0 (Rep a)) => Int -> a -> Doc ann
- genericLiftPFormatPrec :: (Generic1 f, GPPrint Arity1 (Rep1 f)) => (Int -> a -> Doc ann) -> ([a] -> Doc ann) -> Int -> f a -> Doc ann
- genericPFormatList :: (Generic a, GPPrint Arity0 (Rep a)) => [a] -> Doc ann
- genericLiftPFormatList :: (Generic1 f, GPPrint Arity1 (Rep1 f)) => (Int -> a -> Doc ann) -> ([a] -> Doc ann) -> [f a] -> Doc ann
- data family PPrintArgs arity a ann :: Type
- class GPPrint arity f where
- gpformatPrec :: PPrintArgs arity a ann -> PPrintType -> Int -> f a -> Doc ann
- gpformatList :: HasCallStack => PPrintArgs arity a ann -> [f a] -> Doc ann
- gisNullary :: HasCallStack => PPrintArgs arity a ann -> f a -> Bool
- data PPrintType
Organization of the module
The module is organized by first introducing symbolic values, which
includes solvable (primitive) types and
unsolvable (non-primitive) types.
Solvable types are those directly supported by the underlying solver.
Examples include symbolic Booleans (SymBool), integers
(SymInteger), and bit vectors
(SymWordN nUnion monadic container and Mergeable instances to be merged.
We will elaborate the internal details of the symbolic values in the documentation, but it is likely that you can skip them and directly go through the APIs and the operations to start using Grisette.
Various operations are provided for manipulating symbolic values, including solvable and unsolvable types. Apart from the basic operations for each type of symbolic values, we also provide generic operations for:
- Symbolic equality and comparison (
SymEq,SymOrd) - Conversion between concrete and symbolic values (
ToCon,ToSym) - Merging of symbolic values (
Mergeable,SimpleMergeable,TryMerge) - Symbolic branching (
SymBranching)
Additional tools for building symbolic evaluation based applications are also provided:
- Pretty printing (e.g.,
PPrint) - Symbolic generation, or generating fresh symbolic values (e.g.,
GenSym) - Error handling (e.g.,
symAssert) - Solver backend interface (e.g.,
solve,cegis) - Substitutions for symbolic values given the solving results (e.g.,
ExtractSym,EvalSym,SubstSym).
Finally some utilities, including helpers for deriving instances for the type classes are provided in this module.
Note for the examples in the documentation
The examples may assume a z3 solver
available in PATH.
Introduction to symbolic values in Grisette
Symbolic evaluation primer
Grisette is a tool for performing symbolic evaluation on programs. With Grisette, you can construct your own symbolic DSL, and get the symbolic evaluator for it without the need of manually implementing the symbolic evaluation algorithms.
Symbolic evaluation is a technique that allows us to analyze all possible runs of a program by representing inputs (or the program itself) as symbolic values and evaluating the program to produce symbolic constraints over these values. These constraints can then be used to find concrete assignments to the symbolic values that meet certain criteria, such as triggering a bug in a verification task or satisfying a specification in a synthesis task.
For example, in the following pseudo code, suppose that we want to know whether the assertion at the end of the code will hold for all possible inputs:
a = input()
b = 4
if (a < 5) {
b -= a
}
assert (b > 0)We can represent the input a as a symbolic integer, and do symbolic
evaluation for it. By exploring all possible program paths, we will
know that the result for the condition in the assertion would then be a
symbolic formula:
(ite (< a 5) (> (- 4 a) 0) (> 4 0)).
The original program violates the assertion when this formula is false.
We can use a solver to ask whether this could happen, and solver will
tell us that when a is 4, the assertion will not hold.
Our resulting formula captures the information about all possible program runs. One of the challenges of symbolic evaluation is the well-known path explosion problem, which occurs when traditional symbolic evaluation techniques evaluate and reason about the possible paths one-by-one. This can lead to exponential growth in the number of paths that need to be analyzed, making the process impractical for many tasks.
To address this issue, Grisette uses a technique called "path merging". In path merging, symbolic values are merged together in order to reduce the number of paths that need to be explored simultaneously. This can significantly improve the performance of symbolic evaluation, especially for tasks such as program synthesis that are prone to the path explosion problem. This path merging is done automatically by Grisette, with a set of symbolic values.
In Grisette, we make a distinction between two kinds of symbolic values: solvable types and unsolvable types. These two types of values are merged differently.
Solvable types (solver-primitive types)
Solvable types are types that are directly supported by the underlying solver and are represented as symbolic formulas. Examples include symbolic Booleans, integers and bit vectors. The values of solvable types can be fully merged into a single value, which can significantly reduce the number of paths that need to be explored.
For example, there are three symbolic Booleans a, b and c, in the
following code, and a symbolic Boolean x is defined to be the result of
a conditional expression:
x = if a then b else c -- pseudo code, not real Grisette code
The result would be a single symbolic integer formula:
>>>x = symIte "a" "b" "c" :: SymInteger -- real Grisette code>>>x(ite a b c)
If we further add 1 to x, we will not have to split to two paths,
but we can directly construct a formula with the merged value:
>>>x + 1(+ 1 (ite a b c))
Unsolvable types (non-solver-primitive types)
Unsolvable types, on the other hand, are types that are not
directly supported by the solver and cannot be fully merged into a
single formula. Examples include lists, algebraic data types, and
concrete Haskell integer types. To symbolically evaluate values with
unsolvable types, Grisette provides a symbolic union container (Union),
which is a set of values guarded by their path conditions.
The values of unsolvable types are partially merged in a symbolic
union, which is essentially an if-then-else tree.
For example, assume that the lists have the type
[.
In the following example, the result shows that SymBool][b] and [c] can be
merged together in the same symbolic union because they have the same
length:
x = if a then [b] else [c] -- pseudo code, not real Grisette code
Or, in real Grisette code:
>>>mrgIf "a" (return ["b"]) (return ["c"]) :: Union [SymBool]{[(ite a b c)]}
Note that we are using mrgIf instead of symIte for Unions.
The second example shows that [b] and [c,d] cannot be merged
together because they have different lengths:
if a then [b] else [c, d] -- pseudo code, not real Grisette code
In real Grisette code:
>>>mrgIf "a" (return ["b"]) (return ["c", "d"]) :: Union [SymBool]{If a [b] [c,d]}
The following example is more complicated. To make the merging efficient, Grisette would maintain a representation invariant of the symbolic unions. In this case, the lists with length 1 should be placed at the then branch, and the lists with length 2 should be placed at the else branch.
x = if a1 then [b] else if a2 then [c, d] else [f] -- pseudo code, not real Grisette code
In real Grisette code:
>>>x = mrgIf "a1" (return ["b"]) (mrgIf "a2" (return ["c", "d"]) (return ["f"])) :: Union [SymBool]>>>x{If (|| a1 (! a2)) [(ite a1 b f)] [c,d]}
When we further operate on this partially merged values,
we will need to split into multiple paths. For example, when we apply
head onto the last result, and we will distribute head among the
branches:
head x -- pseudo code, not real Grisette code -- intermediate result: If (|| a1 (! a2)) (Single (head [(ite a1 b f)])) (Single (head [c,d])) -- intermediate result: If (|| a1 (! a2)) (Single (ite a1 b f)) (Single c)
This "path splitting" is done with the monad instance of Union. The
result is then merged into a single formula, and further operation on it
won't have to split into multiple paths:
>>>x = mrgIf "a1" (return ["b"]) (mrgIf "a2" (return ["c", "d"]) (return ["f"])) :: Union [SymBool]>>>:{do v <- x -- Path splitted with the (>>=) mrgReturn $ head v -- mrgReturn helps with the merging :} {(ite (|| a1 (! a2)) (ite a1 b f) c)}
Generally, merging the possible branches in a symbolic union can reduce
the number of paths to be explored in the future, but can make the path
conditions larger and harder to solve. To have a good balance between
this, Grisette has built a hierarchical merging algorithm, which is
configurable via MergingStrategy. For algebraic data types, we have
prebuilt merging strategies via the derivation of the Mergeable type
class (Also see GMergeable for detail of derivation). You only need to
know the details of the merging algorithm if you are going to work with
complex non-algebraic data types, or you'd like to configure the merging
based on your domain knowledge to tweak the performance.
Solvable types
Grisette currently provides an implementation for the following solvable types:
SymBool(Bool, symbolic Booleans)SymInteger(Integer, symbolic unbounded integers)SymIntNnIntNnn)SymWordNnWordNnn)SymFPeb sbFPeb sbebexponent bits andsbsignificand bits)SymAlgReal(AlgReal), symbolic algebraic real numbers.SymBool=~>SymBoolBool=->BoolSymBool-~>SymBoolBool-->Bool
The bit-width of bit vector types and floating point types have their are checked at compile time.
Grisette also provides runtime-checked versions of bit-vectors, which
might be more convenient in many scenarios:
SomeSymIntN and SomeSymWordN.
Values of a solvable type can consist of concrete values, symbolic
constants (placeholders for concrete values that can be assigned by a
solver to satisfy a formula), and complex symbolic formulas with
symbolic operations. The Solvable type class provides a way to
construct concrete values and symbolic constants.
Examples:
>>>con True :: SymBool -- a concrete valuetrue>>>true :: SymBool -- via the LogicalOp instancetrue>>>1 :: SymInteger -- via the Num instance1>>>ssym "a" :: SymBool -- a symbolic constanta
With the OverloadedStrings GHC extension enabled, symbolic constants
can also be constructed from strings.
>>>"a" :: SymBoola
Symbolic operations are provided through a set of type classes,
such as SymEq, SymOrd, and Num. Please check out the documentation for
more details.
Examples:
>>>let a = "a" :: SymInteger>>>let b = "b" :: SymInteger>>>a .== b(= a b)
Identifiers and symbols
data Identifier where Source #
Identifier type used for GenSym
The constructor is hidden intentionally. You can construct an identifier by:
- a raw identifier
The following two expressions will refer to the same identifier (the solver won't distinguish them and would assign the same value to them). The user may need to use unique names to avoid unintentional identifier collision.
>>>identifier "a"a
>>>"a" :: Identifier -- available when OverloadedStrings is enableda
- bundle the identifier with some user provided information
Identifiers created with different name or different additional information will not be the same.
>>>withInfo "a" (1 :: Int)a:1
- bundle the calling file location with the identifier to ensure global uniqueness
Identifiers created at different locations will not be the same. The identifiers created at the same location will be the same.
>>>$$(withLoc "a") -- a sample result could be "a:<interactive>:18:4-18"a:<interactive>:...
Constructors
| Identifier :: Text -> Identifier | |
| IdentifierWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => Identifier -> a -> Identifier |
Instances
Symbol types for a symbolic variable.
The symbols can be indexed with an integer.
Constructors
| SimpleSymbol :: Identifier -> Symbol | |
| IndexedSymbol :: Identifier -> Int -> Symbol |
Instances
identifier :: Text -> Identifier Source #
Simple identifier. The same identifier refers to the same symbolic variable in the whole program.
The user may need to use unique identifiers to avoid unintentional identifier collision.
withInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => Identifier -> a -> Identifier Source #
Identifier with extra information.
The same identifier with the same information refers to the same symbolic variable in the whole program.
The user may need to use unique identifiers or additional information to avoid unintentional identifier collision.
withLoc :: Identifier -> SpliceQ Identifier Source #
Identifier with the current location as extra information.
>>>$$(withLoc "a") -- a sample result could be "a:<interactive>:18:4-18"a:<interactive>:...
The uniqueness is ensured for the call to identifier at different location.
uniqueIdentifier :: Text -> IO Identifier Source #
Get a globally unique identifier within the IO monad.
simple :: Identifier -> Symbol Source #
Create a simple symbol.
symbolIdentifier :: Symbol -> Identifier Source #
Get the identifier of a symbol.
modifyIdentifier :: (Identifier -> Identifier) -> Symbol -> Symbol Source #
Modify the identifier of a symbol.
Creation and extraction of solvable values
class IsString t => Solvable c t | t -> c where Source #
The class defines the creation and pattern matching of solvable type values.
Methods
Wrap a concrete value in a symbolic value.
>>>con True :: SymBooltrue
conView :: t -> Maybe c Source #
Extract the concrete value from a symbolic value.
>>>conView (con True :: SymBool)Just True
>>>conView (ssym "a" :: SymBool)Nothing
Generate symbolic constants.
Two symbolic constants with the same symbol are the same symbolic constant, and will always be assigned with the same value by the solver.
>>>sym "a" :: SymBoola>>>(sym "a" :: SymBool) == sym "a"True>>>(sym "a" :: SymBool) == sym "b"False>>>(sym "a" :: SymBool) .&& sym "a"a>>>(sym "a" :: SymBool) == isym "a" 1False
ssym :: Identifier -> t Source #
Generate simply-named symbolic constants.
Two symbolic constants with the same identifier are the same symbolic constant, and will always be assigned with the same value by the solver.
>>>ssym "a" :: SymBoola>>>(ssym "a" :: SymBool) == ssym "a"True>>>(ssym "a" :: SymBool) == ssym "b"False>>>(ssym "a" :: SymBool) .&& ssym "a"a
isym :: Identifier -> Int -> t Source #
Generate indexed symbolic constants.
Two symbolic constants with the same identifier but different indices are not the same symbolic constants.
>>>isym "a" 1 :: SymBoola@1
Instances
pattern Con :: Solvable c t => c -> t Source #
Extract the concrete value from a solvable value with conView.
>>>case con True :: SymBool of Con v -> vTrue
slocsym :: Solvable c s => Identifier -> SpliceQ s Source #
Generate simply-named symbolic variables. The file location will be attached to the identifier.
>>>$$(slocsym "a") :: SymBoola:<interactive>:...
Calling slocsym with the same name at different location will always
generate different symbolic constants. Calling slocsym at the same
location for multiple times will generate the same symbolic constants.
>>>($$(slocsym "a") :: SymBool) == $$(slocsym "a")False>>>let f _ = $$(slocsym "a") :: SymBool>>>f () == f ()True
ilocsym :: Solvable c s => Identifier -> Int -> SpliceQ s Source #
Generate indexed symbolic variables. The file location will be attached to the identifier.
>>>$$(ilocsym "a" 1) :: SymBoola:<interactive>:...@1
Calling ilocsym with the same name and index at different location will
always generate different symbolic constants. Calling slocsym at the same
location for multiple times will generate the same symbolic constants.
Basic symbolic operations
Basic logical operators
class LogicalOp b where Source #
Symbolic logical operators for symbolic booleans.
>>>let t = true :: SymBool>>>let f = false :: SymBool>>>let a = "a" :: SymBool>>>let b = "b" :: SymBool>>>t .|| ftrue>>>a .|| ttrue>>>a .|| fa>>>a .|| b(|| a b)>>>t .&& ffalse>>>a .&& ta>>>a .&& ffalse>>>a .&& b(&& a b)>>>symNot tfalse>>>symNot ftrue>>>symNot a(! a)>>>t `symXor` ftrue>>>t `symXor` tfalse>>>a `symXor` t(! a)>>>a `symXor` fa>>>a `symXor` b(|| (&& (! a) b) (&& a (! b)))
Methods
Constant true
Constant false
(.||) :: b -> b -> b infixr 2 Source #
Symbolic disjunction
(.&&) :: b -> b -> b infixr 3 Source #
Symbolic conjunction
Symbolic negation
symXor :: b -> b -> b Source #
Symbolic exclusive disjunction
symImplies :: b -> b -> b Source #
Symbolic implication
Instances
| LogicalOp SymBool Source # | |
Defined in Grisette.Internal.Core.Data.Class.LogicalOp | |
| LogicalOp Bool Source # | |
| LogicalOp a => LogicalOp (Identity a) Source # | |
Defined in Grisette.Internal.Core.Data.Class.LogicalOp | |
| (LogicalOp a, Mergeable a) => LogicalOp (Union a) Source # | |
Defined in Grisette.Internal.Core.Control.Monad.Union | |
ITE operator for solvable (see Grisette.Core)s, including symbolic boolean, integer, etc.
>>>let a = "a" :: SymBool>>>let b = "b" :: SymBool>>>let c = "c" :: SymBool>>>symIte a b c(ite a b c)
Instances
Symbolic equality
Symbolic equality. Note that we can't use Haskell's Eq class since
symbolic comparison won't necessarily return a concrete Bool value.
>>>let a = 1 :: SymInteger>>>let b = 2 :: SymInteger>>>a .== bfalse>>>a ./= btrue
>>>let a = "a" :: SymInteger>>>let b = "b" :: SymInteger>>>a .== b(= a b)>>>a ./= b(distinct a b)
Note: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving SymEq via (Default X)
Methods
(.==) :: a -> a -> SymBool infix 4 Source #
(./=) :: a -> a -> SymBool infix 4 Source #
symDistinct :: [a] -> SymBool Source #
Check if all elements in a list are distinct, under the symbolic equality semantics.
Instances
class (forall a. SymEq a => SymEq (f a)) => SymEq1 f where Source #
Lifting of the SymEq class to unary type constructors.
Any instance should be subject to the following law that canonicity is preserved:
liftSymEq (.==) should be equivalent to (.==), under the symbolic
semantics.
This class therefore represents the generalization of SymEq by decomposing
its main method into a canonical lifting on a canonical inner method, so that
the lifting can be reused for other arguments than the canonical one.
Methods
liftSymEq :: (a -> b -> SymBool) -> f a -> f b -> SymBool Source #
Lift a symbolic equality test through the type constructor.
The function will usually be applied to an symbolic equality function, but the more general type ensures that the implementation uses it to compare elements of the first container with elements of the second.
Instances
symEq1 :: (SymEq a, SymEq1 f) => f a -> f a -> SymBool Source #
Lift the standard ( function through the type constructor..==)
class (forall a. SymEq a => SymEq1 (f a)) => SymEq2 f where Source #
Lifting of the SymEq class to binary type constructors.
Methods
liftSymEq2 :: (a -> b -> SymBool) -> (c -> d -> SymBool) -> f a c -> f b d -> SymBool Source #
Lift symbolic equality tests through the type constructor.
The function will usually be applied to an symbolic equality function, but the more general type ensures that the implementation uses it to compare elements of the first container with elements of the second.
Instances
| SymEq2 Either Source # | |
Defined in Grisette.Internal.Core.Data.Class.SymEq | |
| SymEq2 (,) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SymEq | |
| SymEq a => SymEq2 ((,,) a) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SymEq | |
| (SymEq a, SymEq b) => SymEq2 ((,,,) a b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SymEq | |
symEq2 :: (SymEq a, SymEq b, SymEq2 f) => f a b -> f a b -> SymBool Source #
Lift the standard ( function through the type constructor..==)
Supplemental operation for Eq
distinct :: Eq a => [a] -> Bool Source #
Check if all elements in a list are distinct.
Note that empty or singleton lists are always distinct.
>>>distinct []True>>>distinct [1]True>>>distinct [1, 2, 3]True>>>distinct [1, 2, 2]False
Symbolic comparison
class SymEq a => SymOrd a where Source #
Symbolic total order. Note that we can't use Haskell's Ord class since
symbolic comparison won't necessarily return a concrete Bool or Ordering
value.
>>>let a = 1 :: SymInteger>>>let b = 2 :: SymInteger>>>a .< btrue>>>a .> bfalse
>>>let a = "a" :: SymInteger>>>let b = "b" :: SymInteger>>>a .< b(< a b)>>>a .<= b(<= a b)>>>a .> b(< b a)>>>a .>= b(<= b a)
For symCompare, Ordering is not a solvable type, and the result would
be wrapped in a union-like monad. See
Union and PlainUnion for more
information.
>>>a `symCompare` b :: Union Ordering{If (< a b) LT (If (= a b) EQ GT)}
Note: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving SymOrd via (Default X)
Minimal complete definition
Methods
(.<) :: a -> a -> SymBool infix 4 Source #
(.<=) :: a -> a -> SymBool infix 4 Source #
(.>) :: a -> a -> SymBool infix 4 Source #
(.>=) :: a -> a -> SymBool infix 4 Source #
symCompare :: a -> a -> Union Ordering Source #
Instances
class (SymEq1 f, forall a. SymOrd a => SymOrd (f a)) => SymOrd1 f where Source #
Lifting of the SymOrd class to unary type constructors.
Any instance should be subject to the following law that canonicity is preserved:
liftSymCompare symCompare should be equivalent to symCompare, under the
symbolic semantics.
This class therefore represents the generalization of SymOrd by decomposing
its main method into a canonical lifting on a canonical inner method, so that
the lifting can be reused for other arguments than the canonical one.
Methods
liftSymCompare :: (a -> b -> Union Ordering) -> f a -> f b -> Union Ordering Source #
Lift a symCompare function through the type constructor.
The function will usually be applied to an symbolic comparison function, but the more general type ensures that the implementation uses it to compare elements of the first container with elements of the second.
Instances
symCompare1 :: (SymOrd1 f, SymOrd a) => f a -> f a -> Union Ordering Source #
Lift the standard symCompare function to binary type constructors.
class (SymEq2 f, forall a. SymOrd a => SymOrd1 (f a)) => SymOrd2 f where Source #
Lifting of the SymOrd class to binary type constructors.
Methods
liftSymCompare2 :: (a -> b -> Union Ordering) -> (c -> d -> Union Ordering) -> f a c -> f b d -> Union Ordering Source #
Lift a symCompare function through the type constructor.
The function will usually be applied to an symbolic comparison function, but the more general type ensures that the implementation uses it to compare elements of the first container with elements of the second.
Instances
symCompare2 :: (SymOrd2 f, SymOrd a, SymOrd b) => f a b -> f a b -> Union Ordering Source #
Lift the standard symCompare function through the type constructors.
mrgMax :: (SymOrd a, Mergeable a, SymBranching m, Applicative m) => a -> a -> m a Source #
Symbolic maximum, with a union-like monad.
mrgMin :: (SymOrd a, Mergeable a, SymBranching m, Applicative m) => a -> a -> m a Source #
Symbolic minimum, with a union-like monad.
Bit-vectors
Bit vector operations. Including concatenation (bvConcat),
extension (bvZext, bvSext, bvExt), and selection
(bvSelect).
Methods
bvConcat :: bv -> bv -> bv Source #
Concatenation of two bit vectors.
>>>bvConcat (SomeSymWordN (0b101 :: SymWordN 3)) (SomeSymWordN (0b010 :: SymWordN 3))0b101010
Arguments
| :: Int | Desired output length |
| -> bv | Bit vector to extend |
| -> bv |
Zero extension of a bit vector.
>>>bvZext 6 (SomeSymWordN (0b101 :: SymWordN 3))0b000101
Arguments
| :: Int | Desired output length |
| -> bv | Bit vector to extend |
| -> bv |
Sign extension of a bit vector.
>>>bvSext 6 (SomeSymWordN (0b101 :: SymWordN 3))0b111101
Arguments
| :: Int | Desired output length |
| -> bv | Bit vector to extend |
| -> bv |
Extension of a bit vector. Signedness is determined by the input bit vector type.
>>>bvExt 6 (SomeSymIntN (0b101 :: SymIntN 3))0b111101>>>bvExt 6 (SomeSymIntN (0b001 :: SymIntN 3))0b000001>>>bvExt 6 (SomeSymWordN (0b101 :: SymWordN 3))0b000101>>>bvExt 6 (SomeSymWordN (0b001 :: SymWordN 3))0b000001
Arguments
| :: Int | Index of the least significant bit of the slice |
| -> Int | Desired output width, |
| -> bv | Bit vector to select from |
| -> bv |
Slicing out a smaller bit vector from a larger one,
selecting a slice with width w starting from index ix.
The least significant bit is indexed as 0.
>>>bvSelect 1 3 (SomeSymIntN (0b001010 :: SymIntN 6))0b101
Create a bit vector from an integer. The bit-width is the first argument, which should not be zero.
>>>bv 12 21 :: SomeSymIntN0x015
Instances
| SizedBV bv => BV (SomeBV bv) Source # | |
Defined in Grisette.Internal.SymPrim.SomeBV | |
Arguments
| :: BV bv | |
| => Int | The start position to extract from, |
| -> Int | The end position to extract from, |
| -> bv | Bit vector to extract from |
| -> bv |
Slicing out a smaller bit vector from a larger one, extract a slice from
bit i down to j.
The least significant bit is indexed as 0.
>>>bvExtract 4 2 (SomeSymIntN (0b010100 :: SymIntN 6))0b101
class SizedBV bv where Source #
Sized bit vector operations. Including concatenation (sizedBVConcat),
extension (sizedBVZext, sizedBVSext, sizedBVExt), and selection
(sizedBVSelect).
Minimal complete definition
sizedBVConcat, sizedBVZext, sizedBVSext, sizedBVExt, sizedBVSelect
Methods
sizedBVConcat :: (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => bv l -> bv r -> bv (l + r) Source #
Concatenation of two bit vectors.
>>>sizedBVConcat (0b101 :: SymIntN 3) (0b010 :: SymIntN 3)0b101010
Arguments
| :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) | |
| => proxy r | Desired output width |
| -> bv l | Bit vector to extend |
| -> bv r |
Zero extension of a bit vector.
>>>sizedBVZext (Proxy @6) (0b101 :: SymIntN 3)0b000101
Arguments
| :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) | |
| => proxy r | Desired output width |
| -> bv l | Bit vector to extend |
| -> bv r |
Signed extension of a bit vector.
>>>sizedBVSext (Proxy @6) (0b101 :: SymIntN 3)0b111101
Arguments
| :: (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) | |
| => proxy r | Desired output width |
| -> bv l | Bit vector to extend |
| -> bv r |
Extension of a bit vector. Signedness is determined by the input bit vector type.
>>>sizedBVExt (Proxy @6) (0b101 :: SymIntN 3)0b111101>>>sizedBVExt (Proxy @6) (0b001 :: SymIntN 3)0b000001>>>sizedBVExt (Proxy @6) (0b101 :: SymWordN 3)0b000101>>>sizedBVExt (Proxy @6) (0b001 :: SymWordN 3)0b000001
Arguments
| :: (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) | |
| => p ix | Index of the least significant bit of the slice |
| -> q w | Desired output width, |
| -> bv n | Bit vector to select from |
| -> bv w |
Slicing out a smaller bit vector from a larger one, selecting a slice with
width w starting from index ix.
The least significant bit is indexed as 0.
>>>sizedBVSelect (Proxy @2) (Proxy @3) (con 0b010100 :: SymIntN 6)0b101
sizedBVFromIntegral :: (Integral a, KnownNat n, 1 <= n) => a -> bv n Source #
Instances
| SizedBV IntN Source # | |
Defined in Grisette.Internal.SymPrim.BV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => IntN l -> IntN r -> IntN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> IntN n -> IntN w Source # sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> IntN n Source # | |
| SizedBV WordN Source # | |
Defined in Grisette.Internal.SymPrim.BV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> WordN n -> WordN w Source # sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> WordN n Source # | |
| SizedBV SymIntN Source # | |
Defined in Grisette.Internal.SymPrim.SymBV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => SymIntN l -> SymIntN r -> SymIntN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymIntN l -> SymIntN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> SymIntN n -> SymIntN w Source # sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> SymIntN n Source # | |
| SizedBV SymWordN Source # | |
Defined in Grisette.Internal.SymPrim.SymBV Methods sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => SymWordN l -> SymWordN r -> SymWordN (l + r) Source # sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> SymWordN l -> SymWordN r Source # sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => p ix -> q w -> SymWordN n -> SymWordN w Source # sizedBVFromIntegral :: forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> SymWordN n Source # | |
Arguments
| :: forall p i q j n bv. (SizedBV bv, KnownNat n, KnownNat i, KnownNat j, 1 <= n, (i + 1) <= n, j <= i) | |
| => p i | The start position to extract from, |
| -> q j | The end position to extract from, |
| -> bv n | Bit vector to extract from |
| -> bv ((i - j) + 1) |
Slicing out a smaller bit vector from a larger one, extract a slice from
bit i down to j.
The least significant bit is indexed as 0.
>>>sizedBVExtract (Proxy @4) (Proxy @2) (con 0b010100 :: SymIntN 6)0b101
class Bits a => SymShift a where Source #
A class for shifting operations.
The symShift function shifts the value to the left if the shift amount is
positive, and to the right if the shift amount is negative. If shifting
beyond the bit width of the value, the result is the same as shifting with
the bit width.
The symShiftNegated function shifts the value to the right if the shift
amount is positive, and to the left if the shift amount is negative. This
function is introduced to handle the asymmetry of the range of values.
Instances
| SymShift Int16 Source # | |
| SymShift Int32 Source # | |
| SymShift Int64 Source # | |
| SymShift Int8 Source # | |
| SymShift Word16 Source # | |
| SymShift Word32 Source # | |
| SymShift Word64 Source # | |
| SymShift Word8 Source # | |
| SymShift Int Source # | |
| SymShift Word Source # | |
| (Integral a, FiniteBits a) => SymShift (DefaultFiniteBitsSymShift a) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SymShift Methods symShift :: DefaultFiniteBitsSymShift a -> DefaultFiniteBitsSymShift a -> DefaultFiniteBitsSymShift a Source # symShiftNegated :: DefaultFiniteBitsSymShift a -> DefaultFiniteBitsSymShift a -> DefaultFiniteBitsSymShift a Source # | |
| (KnownNat n, 1 <= n) => SymShift (IntN n) Source # | |
| (KnownNat n, 1 <= n) => SymShift (WordN n) Source # | |
| (forall (n :: Nat). (KnownNat n, 1 <= n) => SymShift (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) => SymShift (SomeBV bv) Source # | |
| (KnownNat n, 1 <= n) => SymShift (SymIntN n) Source # | |
| (KnownNat n, 1 <= n) => SymShift (SymWordN n) Source # | |
class (MonadError e m, TryMerge m, Mergeable a) => SafeSymShift e a m where Source #
Safe version for shiftL or shiftR.
The safeSymShiftL and safeSymShiftR are defined for all non-negative
shift amounts.
- Shifting by negative shift amounts is an error.
- The result is defined to be 0 when shifting left by more than or equal to the bit size of the number.
- The result is defined to be 0 when shifting right by more than or equal to the bit size of the number and the number is unsigned or signed non-negative.
- The result is defined to be -1 when shifting right by more than or equal to the bit size of the number and the number is signed negative.
The safeSymStrictShiftL and safeSymStrictShiftR are defined for all
non-negative shift amounts that is less than the bit size. Shifting by more
than or equal to the bit size is an error, otherwise they are the same as the
non-strict versions.
Methods
safeSymShiftL :: a -> a -> m a Source #
safeSymShiftR :: a -> a -> m a Source #
safeSymStrictShiftL :: a -> a -> m a Source #
safeSymStrictShiftR :: a -> a -> m a Source #
Instances
class Bits a => SymRotate a where Source #
The symRotate is similar to rotate, but accepts the type itself instead
of Int for the rotate amount. The function works on all inputs, including
the rotate amounts that are beyond the bit width of the value.
The symRotateNegated function rotates to the opposite direction of
symRotate. This function is introduced to handle the asymmetry of the range
of values.
Instances
| SymRotate Int16 Source # | |
| SymRotate Int32 Source # | |
| SymRotate Int64 Source # | |
| SymRotate Int8 Source # | |
| SymRotate Word16 Source # | |
| SymRotate Word32 Source # | |
| SymRotate Word64 Source # | |
| SymRotate Word8 Source # | |
| SymRotate Int Source # | |
| SymRotate Word Source # | |
| (Integral a, FiniteBits a) => SymRotate (DefaultFiniteBitsSymRotate a) Source # | |
| (KnownNat n, 1 <= n) => SymRotate (IntN n) Source # | |
| (KnownNat n, 1 <= n) => SymRotate (WordN n) Source # | |
| (forall (n :: Nat). (KnownNat n, 1 <= n) => SymRotate (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) => SymRotate (SomeBV bv) Source # | |
| (KnownNat n, 1 <= n) => SymRotate (SymIntN n) Source # | |
| (KnownNat n, 1 <= n) => SymRotate (SymWordN n) Source # | |
class (MonadError e m, TryMerge m, Mergeable a) => SafeSymRotate e a m where Source #
Safe rotation operations. The operators will reject negative shift amounts.
Instances
class SignConversion ubv sbv | ubv -> sbv, sbv -> ubv where Source #
Convert values between signed and unsigned.
Methods
toSigned :: ubv -> sbv Source #
Convert unsigned value to the corresponding signed value.
toUnsigned :: sbv -> ubv Source #
Convert signed value to the corresponding unsigned value.
Instances
| SignConversion Word16 Int16 Source # | |
| SignConversion Word32 Int32 Source # | |
| SignConversion Word64 Int64 Source # | |
| SignConversion Word8 Int8 Source # | |
| SignConversion Word Int Source # | |
| (KnownNat n, 1 <= n) => SignConversion (WordN n) (IntN n) Source # | |
| (forall (n :: Nat). (KnownNat n, 1 <= n) => SignConversion (ubv n) (sbv n), SignConversion (ubv 1) (sbv 1)) => SignConversion (SomeBV ubv) (SomeBV sbv) Source # | |
| (KnownNat n, 1 <= n) => SignConversion (SymWordN n) (SymIntN n) Source # | |
Safe operation for Numbers
Safe division handling with default values returned on exception.
Methods
divOr :: a -> a -> a -> a Source #
Safe div with default value returned on exception.
>>>divOr "d" "a" "b" :: SymInteger(ite (= b 0) d (div a b))
modOr :: a -> a -> a -> a Source #
Safe mod with default value returned on exception.
>>>modOr "d" "a" "b" :: SymInteger(ite (= b 0) d (mod a b))
divModOr :: (a, a) -> a -> a -> (a, a) Source #
Safe divMod with default value returned on exception.
>>>divModOr ("d", "m") "a" "b" :: (SymInteger, SymInteger)((ite (= b 0) d (div a b)),(ite (= b 0) m (mod a b)))
quotOr :: a -> a -> a -> a Source #
Safe quot with default value returned on exception.
remOr :: a -> a -> a -> a Source #
Safe rem with default value returned on exception.
quotRemOr :: (a, a) -> a -> a -> (a, a) Source #
Safe quotRem with default value returned on exception.
Instances
modOrDividend :: (DivOr a, Num a) => a -> a -> a Source #
Safe mod with dividend returned on exception.
remOrDividend :: (DivOr a, Num a) => a -> a -> a Source #
Safe rem with dividend returned on exception.
divModOrZeroDividend :: (DivOr a, Num a) => a -> a -> (a, a) Source #
Safe divMod with 0 returned on exception.
quotRemOrZeroDividend :: (DivOr a, Num a) => a -> a -> (a, a) Source #
Safe quotRem with 0 returned on exception.
class (MonadError e m, TryMerge m, Mergeable a, DivOr a) => SafeDiv e a m where Source #
Safe division with monadic error handling in multi-path
execution. These procedures throw an exception when the
divisor is zero. The result should be able to handle errors with
MonadError.
Minimal complete definition
(safeDiv, safeMod | safeDivMod), (safeQuot, safeRem | safeQuotRem)
Methods
safeDiv :: a -> a -> m a Source #
Safe div with monadic error handling in multi-path execution.
>>>safeDiv "a" "b" :: ExceptT ArithException Union SymIntegerExceptT {If (= b 0) (Left divide by zero) (Right (div a b))}
safeMod :: a -> a -> m a Source #
Safe mod with monadic error handling in multi-path execution.
>>>safeMod "a" "b" :: ExceptT ArithException Union SymIntegerExceptT {If (= b 0) (Left divide by zero) (Right (mod a b))}
safeDivMod :: a -> a -> m (a, a) Source #
Safe divMod with monadic error handling in multi-path execution.
>>>safeDivMod "a" "b" :: ExceptT ArithException Union (SymInteger, SymInteger)ExceptT {If (= b 0) (Left divide by zero) (Right ((div a b),(mod a b)))}
safeQuot :: a -> a -> m a Source #
Safe quot with monadic error handling in multi-path execution.
safeRem :: a -> a -> m a Source #
Safe rem with monadic error handling in multi-path execution.
safeQuotRem :: a -> a -> m (a, a) Source #
Safe quotRem with monadic error handling in multi-path execution.
Instances
class (MonadError e m, TryMerge m, Mergeable a) => SafeLinearArith e a m where Source #
Safe division with monadic error handling in multi-path
execution. These procedures throw an exception when overflow or underflow happens.
The result should be able to handle errors with MonadError.
Methods
safeAdd :: a -> a -> m a Source #
Safe + with monadic error handling in multi-path execution.
Overflows or underflows are treated as errors.
>>>safeAdd (ssym "a") (ssym "b") :: ExceptT ArithException Union SymIntegerExceptT {Right (+ a b)}>>>safeAdd (ssym "a") (ssym "b") :: ExceptT ArithException Union (SymIntN 4)ExceptT {If (ite (< 0x0 a) (&& (< 0x0 b) (< (+ a b) 0x0)) (&& (< a 0x0) (&& (< b 0x0) (<= 0x0 (+ a b))))) (If (< 0x0 a) (Left arithmetic overflow) (Left arithmetic underflow)) (Right (+ a b))}
Safe negate with monadic error handling in multi-path execution.
Overflows or underflows are treated as errors.
>>>safeNeg (ssym "a") :: ExceptT ArithException Union SymIntegerExceptT {Right (- a)}>>>safeNeg (ssym "a") :: ExceptT ArithException Union (SymIntN 4)ExceptT {If (= a 0x8) (Left arithmetic overflow) (Right (- a))}
safeSub :: a -> a -> m a Source #
Safe - with monadic error handling in multi-path execution.
Overflows or underflows are treated as errors.
>>>safeSub (ssym "a") (ssym "b") :: ExceptT ArithException Union SymIntegerExceptT {Right (+ a (- b))}>>>safeSub (ssym "a") (ssym "b") :: ExceptT ArithException Union (SymIntN 4)ExceptT {If (ite (<= 0x0 a) (&& (< b 0x0) (< (+ a (- b)) 0x0)) (&& (< a 0x0) (&& (< 0x0 b) (< 0x0 (+ a (- b)))))) (If (<= 0x0 a) (Left arithmetic overflow) (Left arithmetic underflow)) (Right (+ a (- b)))}
Instances
Safe fractional with default values returned on exception.
Methods
fdivOr :: a -> a -> a -> a Source #
Safe / with default values returned on exception.
>>>fdivOr "d" "a" "b" :: SymAlgReal(ite (= b 0.0) d (fdiv a b))
recipOr :: a -> a -> a Source #
Safe recip with default values returned on exception.
>>>recipOr "d" "a" :: SymAlgReal(ite (= a 0.0) d (recip a))
Instances
| FdivOr AlgReal Source # | |
| FdivOr SymAlgReal Source # | |
Defined in Grisette.Internal.Core.Data.Class.SafeFdiv Methods fdivOr :: SymAlgReal -> SymAlgReal -> SymAlgReal -> SymAlgReal Source # recipOr :: SymAlgReal -> SymAlgReal -> SymAlgReal Source # | |
class (MonadError e m, TryMerge m, Mergeable a) => SafeFdiv e a m where Source #
Safe fractional division with monadic error handling in multi-path
execution. These procedures throw an exception when the denominator is zero.
The result should be able to handle errors with MonadError.
Minimal complete definition
Methods
safeFdiv :: a -> a -> m a Source #
Safe fractional division with monadic error handling in multi-path execution.
>>>safeFdiv "a" "b" :: ExceptT ArithException Union SymAlgRealExceptT {If (= b 0.0) (Left Ratio has zero denominator) (Right (fdiv a b))}
safeRecip :: a -> m a Source #
Safe fractional reciprocal with monadic error handling in multi-path execution.
>>>safeRecip "a" :: ExceptT ArithException Union SymAlgRealExceptT {If (= a 0.0) (Left Ratio has zero denominator) (Right (recip a))}
default safeRecip :: Fractional a => a -> m a Source #
Instances
| (MonadError ArithException m, TryMerge m) => SafeFdiv ArithException AlgReal m Source # | |
| (MonadError ArithException m, MonadUnion m) => SafeFdiv ArithException SymAlgReal m Source # | |
Defined in Grisette.Internal.Core.Data.Class.SafeFdiv Methods safeFdiv :: SymAlgReal -> SymAlgReal -> m SymAlgReal Source # safeRecip :: SymAlgReal -> m SymAlgReal Source # | |
class LogBaseOr a where Source #
Safe logBase with default values returned on exception.
Methods
logBaseOr :: a -> a -> a -> a Source #
Safe logBase with default values returned on exception.
>>>logBaseOr "d" "base" "val" :: SymAlgReal(ite (= base 1.0) d (fdiv (log val) (log base)))
Instances
| LogBaseOr SymAlgReal Source # | |
Defined in Grisette.Internal.Core.Data.Class.SafeLogBase Methods logBaseOr :: SymAlgReal -> SymAlgReal -> SymAlgReal -> SymAlgReal Source # | |
logBaseOrZero :: (LogBaseOr a, Num a) => a -> a -> a Source #
Safe logBase with 0 returned on exception.
class (MonadError e m, TryMerge m, Mergeable a) => SafeLogBase e a m where Source #
Safe logBase with monadic error handling in multi-path execution.
These procedures throw an exception when the base is 1.
The result should be able to handle errors with MonadError.
Minimal complete definition
Nothing
Methods
safeLogBase :: a -> a -> m a Source #
Safe logBase with monadic error handling in multi-path execution.
>>>safeLogBase (ssym "base") (ssym "val") :: ExceptT ArithException Union SymAlgRealExceptT {If (= base 1.0) (Left Ratio has zero denominator) (Right (fdiv (log val) (log base)))}
Instances
| (MonadError ArithException m, MonadUnion m) => SafeLogBase ArithException SymAlgReal m Source # | |
Defined in Grisette.Internal.Core.Data.Class.SafeLogBase Methods safeLogBase :: SymAlgReal -> SymAlgReal -> m SymAlgReal Source # | |
Functions
class Function f arg ret | f -> arg ret where Source #
Abstraction for function-like types.
Methods
(#) :: f -> arg -> ret infixl 9 Source #
Function application operator.
The operator is not right associated (like ($)). It is left associated,
and you can provide many arguments with this operator once at a time.
>>>(+1) # 23
>>>(+) # 2 # 35
Instances
| (Function f arg ret, Mergeable f, Mergeable ret) => Function (Union f) arg (Union ret) Source # | |
| (LinkedRep a sa, LinkedRep b sb) => Function (a --> b) sa sb Source # | |
Defined in Grisette.Internal.SymPrim.GeneralFun | |
| (SupportedNonFuncPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca --> cb)) => Function (sa -~> sb) sa sb Source # | |
Defined in Grisette.Internal.SymPrim.SymGeneralFun | |
| (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb, SupportedPrim (ca =-> cb)) => Function (sa =~> sb) sa sb Source # | |
Defined in Grisette.Internal.SymPrim.SymTabularFun | |
| Eq a => Function (a =-> b) a b Source # | |
Defined in Grisette.Internal.SymPrim.TabularFun | |
| Function (a -> b) a b Source # | |
Defined in Grisette.Internal.Core.Data.Class.Function | |
Applying an uninterpreted function.
>>>let f = "f" :: SymInteger =~> SymInteger =~> SymInteger>>>apply f "a" "b"(apply (apply f a) b)
Note that for implementation reasons, you can also use apply function on
a non-function symbolic value. In this case, the function is treated as an
id function.
Instances
IEEE Floating points
fpIsPositiveZero :: RealFloat a => a -> Bool Source #
Check if a floating-point number is positive zero.
fpIsNegativeZero :: RealFloat a => a -> Bool Source #
Check if a floating-point number is negative zero.
fpIsPositiveInfinite :: RealFloat a => a -> Bool Source #
Check if a floating-point number is positive infinite.
fpIsNegativeInfinite :: RealFloat a => a -> Bool Source #
Check if a floating-point number is negative infinite.
fpIsPositive :: RealFloat a => a -> Bool Source #
Check if a floating-point number is positive. +0, +inf are considered positive. nan, -0, -inf are not positive.
fpIsNegative :: RealFloat a => a -> Bool Source #
Check if a floating-point number is negative. -0, -inf are considered negative. nan, +0, +inf are not negative.
fpIsInfinite :: RealFloat a => a -> Bool Source #
Check if a floating-point number is infinite.
fpIsNormal :: RealFloat a => a -> Bool Source #
Check if a floating-point number is normal, i.e., not 0, not inf, not nan, and not denormalized.
fpIsSubnormal :: RealFloat a => a -> Bool Source #
Check if a floating-point number is subnormal, i.e., denormalized. 0, inf, or nan are not subnormal.
fpIsPoint :: RealFloat a => a -> Bool Source #
Check if a floating-point number is a point, i.e., not inf, not nan.
class SymIEEEFPTraits a where Source #
A class for symbolic traits of IEEE floating-point numbers.
Methods
symFpIsNaN :: a -> SymBool Source #
Check if a symbolic floating-point number is not-a-number.
symFpIsPositive :: a -> SymBool Source #
Check if a symbolic floating-point number is positive. +0, +inf are considered positive. nan, -0, -inf are not positive.
symFpIsNegative :: a -> SymBool Source #
Check if a symbolic floating-point number is negative. -0, -inf are considered negative. nan, +0, +inf are not negative.
symFpIsPositiveInfinite :: a -> SymBool Source #
Check if a symbolic floating-point number is positive infinite.
symFpIsNegativeInfinite :: a -> SymBool Source #
Check if a symbolic floating-point number is negative infinite.
symFpIsInfinite :: a -> SymBool Source #
Check if a symbolic floating-point number is infinite.
symFpIsPositiveZero :: a -> SymBool Source #
Check if a symbolic floating-point number is positive zero.
symFpIsNegativeZero :: a -> SymBool Source #
Check if a symbolic floating-point number is negative zero.
symFpIsZero :: a -> SymBool Source #
Check if a symbolic floating-point number is zero.
symFpIsNormal :: a -> SymBool Source #
Check if a symbolic floating-point number is normal, i.e., not 0, not inf, not nan, and not denormalized.
symFpIsSubnormal :: a -> SymBool Source #
Check if a symbolic floating-point number is subnormal, i.e., denormalized. 0, inf, or nan are not subnormal.
symFpIsPoint :: a -> SymBool Source #
Check if a symbolic floating-point number is a point, i.e., not inf, not nan.
Instances
class IEEEFPConstants a where Source #
Constants for IEEE floating-point numbers.
Methods
fpPositiveInfinite :: a Source #
Positive infinity.
fpNegativeInfinite :: a Source #
Negative infinity.
Not-a-number.
fpNegativeZero :: a Source #
Negative zero.
fpPositiveZero :: a Source #
Positive zero.
fpMinNormalized :: a Source #
Smallest positive normalized number.
fpMinSubnormal :: a Source #
Smallest positive subnormal number.
fpMaxNormalized :: a Source #
Largest positive normalized number.
fpMaxSubnormal :: a Source #
Largest positive subnormal number.
Instances
| ValidFP eb sb => IEEEFPConstants (FP eb sb) Source # | |
Defined in Grisette.Internal.SymPrim.FP Methods fpPositiveInfinite :: FP eb sb Source # fpNegativeInfinite :: FP eb sb Source # fpNegativeZero :: FP eb sb Source # fpPositiveZero :: FP eb sb Source # fpMinNormalized :: FP eb sb Source # fpMinSubnormal :: FP eb sb Source # fpMaxNormalized :: FP eb sb Source # fpMaxSubnormal :: FP eb sb Source # | |
| ValidFP eb sb => IEEEFPConstants (SymFP eb sb) Source # | |
Defined in Grisette.Internal.SymPrim.SymFP Methods fpPositiveInfinite :: SymFP eb sb Source # fpNegativeInfinite :: SymFP eb sb Source # fpNegativeZero :: SymFP eb sb Source # fpPositiveZero :: SymFP eb sb Source # fpMinNormalized :: SymFP eb sb Source # fpMinSubnormal :: SymFP eb sb Source # fpMaxNormalized :: SymFP eb sb Source # fpMaxSubnormal :: SymFP eb sb Source # | |
class IEEEFPRoundingMode mode where Source #
Rounding modes for floating-point operations.
Methods
Round to nearest, ties to even.
Round to nearest, ties to away from zero.
Round towards positive infinity.
Round towards negative infinity.
Round towards zero.
Instances
| IEEEFPRoundingMode FPRoundingMode Source # | |
Defined in Grisette.Internal.SymPrim.FP Methods rne :: FPRoundingMode Source # rna :: FPRoundingMode Source # rtp :: FPRoundingMode Source # rtn :: FPRoundingMode Source # rtz :: FPRoundingMode Source # | |
| IEEEFPRoundingMode SymFPRoundingMode Source # | |
Defined in Grisette.Internal.SymPrim.SymFP Methods rne :: SymFPRoundingMode Source # rna :: SymFPRoundingMode Source # rtp :: SymFPRoundingMode Source # | |
class IEEEFPOp a where Source #
Operations on IEEE floating-point numbers, without rounding mode.
Methods
IEEE754-2019 abs operation.
IEEE754-2019 negate operation.
IEEE754-2019 remainder operation.
fpMinimum :: a -> a -> a Source #
IEEE754-2019 minimum operation.
- The comparison for zeros follows -0 < 0
- Returns NaN if one operand is NaN.
fpMinimumNumber :: a -> a -> a Source #
IEEE754-2019 minimumNumber operation.
- The comparison for zeros follows -0 < 0
- Returns the other operand if one operand is NaN.
fpMaximum :: a -> a -> a Source #
IEEE754-2019 maximum operation.
- The comparison for zeros follows -0 < 0
- Returns NaN if one operand is NaN.
fpMaximumNumber :: a -> a -> a Source #
IEEE754-2019 maximumNumber operation.
- The comparison for zeros follows -0 < 0
- Returns the other operand if one operand is NaN.
Instances
| ValidFP eb sb => IEEEFPOp (FP eb sb) Source # | |
Defined in Grisette.Internal.SymPrim.FP Methods fpAbs :: FP eb sb -> FP eb sb Source # fpNeg :: FP eb sb -> FP eb sb Source # fpRem :: FP eb sb -> FP eb sb -> FP eb sb Source # fpMinimum :: FP eb sb -> FP eb sb -> FP eb sb Source # fpMinimumNumber :: FP eb sb -> FP eb sb -> FP eb sb Source # fpMaximum :: FP eb sb -> FP eb sb -> FP eb sb Source # fpMaximumNumber :: FP eb sb -> FP eb sb -> FP eb sb Source # | |
| ValidFP eb sb => IEEEFPOp (SymFP eb sb) Source # | |
Defined in Grisette.Internal.SymPrim.SymFP Methods fpAbs :: SymFP eb sb -> SymFP eb sb Source # fpNeg :: SymFP eb sb -> SymFP eb sb Source # fpRem :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # fpMinimum :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # fpMinimumNumber :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # fpMaximum :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # fpMaximumNumber :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # | |
class IEEEFPRoundingMode mode => IEEEFPRoundingOp a mode | a -> mode where Source #
Operations on IEEE floating-point numbers, with rounding mode.
Methods
fpAdd :: mode -> a -> a -> a Source #
fpSub :: mode -> a -> a -> a Source #
fpMul :: mode -> a -> a -> a Source #
fpDiv :: mode -> a -> a -> a Source #
fpFMA :: mode -> a -> a -> a -> a Source #
fpSqrt :: mode -> a -> a Source #
fpRoundToIntegral :: mode -> a -> a Source #
Instances
class IEEEFPConvertible a fp mode | fp -> mode where Source #
Conversion from and to FPs.
Methods
Arguments
| :: a | Default value when converting non-representable FPs. For example, when converting to non-FP types, the NaN and infinities are not representable. Additionally, when converting to bit-vectors, out-of-bound FPs are not representable. Note that out-of-bound means that the value after conversion is out of bound, not the value before conversion, meaning that converting from 3.5 to 2-bit unsigned bit-vector is out-of-bound when rounding to positive, but not when rounding to negative. |
| -> mode | Rounding mode. Ignored when converting to |
| -> fp | FP value. |
| -> a |
Instances
class (IEEEFPConvertible a fp mode, IEEEFPRoundingMode mode) => IEEEFPToAlgReal a fp mode | fp -> mode where Source #
Converting FP to real numbers.
Minimal complete definition
Nothing
Methods
fpToAlgReal :: a -> fp -> a Source #
Instances
| ValidFP eb sb => IEEEFPToAlgReal AlgReal (FP eb sb) FPRoundingMode Source # | |
Defined in Grisette.Internal.SymPrim.FP | |
| ValidFP eb sb => IEEEFPToAlgReal SymAlgReal (SymFP eb sb) SymFPRoundingMode Source # | |
Defined in Grisette.Internal.SymPrim.SymFP Methods fpToAlgReal :: SymAlgReal -> SymFP eb sb -> SymAlgReal Source # | |
Conversion between Concrete and Symbolic values
class ToCon a b where Source #
Convert a symbolic value to concrete value if possible.
Methods
toCon :: a -> Maybe b Source #
Convert a symbolic value to concrete value if possible.
If the symbolic value cannot be converted to concrete, the result will be Nothing.
>>>toCon (ssym "a" :: SymInteger) :: Maybe IntegerNothing
>>>toCon (con 1 :: SymInteger) :: Maybe IntegerJust 1
toCon works on complex types too.
>>>toCon ([con 1, con 2] :: [SymInteger]) :: Maybe [Integer]Just [1,2]
>>>toCon ([con 1, ssym "a"] :: [SymInteger]) :: Maybe [Integer]Nothing
Instances
| ToCon All All Source # | |
| ToCon Any Any Source # | |
| ToCon Int16 Int16 Source # | |
| ToCon Int32 Int32 Source # | |
| ToCon Int64 Int64 Source # | |
| ToCon Int8 Int8 Source # | |
| ToCon Word16 Word16 Source # | |
| ToCon Word32 Word32 Source # | |
| ToCon Word64 Word64 Source # | |
| ToCon Word8 Word8 Source # | |
| ToCon ByteString ByteString Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: ByteString -> Maybe ByteString Source # | |
| ToCon Ordering Ordering Source # | |
| ToCon AssertionError AssertionError Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon Methods | |
| ToCon VerificationConditions VerificationConditions Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: VerificationConditions -> Maybe VerificationConditions Source # | |
| ToCon FPRoundingMode FPRoundingMode Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon Methods | |
| ToCon NotRepresentableFPError NotRepresentableFPError Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: NotRepresentableFPError -> Maybe NotRepresentableFPError Source # | |
| ToCon SomeBVException SomeBVException Source # | |
Defined in Grisette.Internal.SymPrim.SomeBV Methods | |
| ToCon SymAlgReal AlgReal Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| ToCon SymAlgReal SymAlgReal Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymAlgReal -> Maybe SymAlgReal Source # | |
| ToCon SymBool SymBool Source # | |
| ToCon SymBool Bool Source # | |
| ToCon SymFP32 Float Source # | |
| ToCon SymFP64 Double Source # | |
| ToCon SymFPRoundingMode FPRoundingMode Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon Methods | |
| ToCon SymFPRoundingMode SymFPRoundingMode Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymFPRoundingMode -> Maybe SymFPRoundingMode Source # | |
| ToCon SymInteger SymInteger Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymInteger -> Maybe SymInteger Source # | |
| ToCon SymInteger Integer Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| ToCon Text Text Source # | |
| ToCon Integer Integer Source # | |
| ToCon () () Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| ToCon Bool Bool Source # | |
| ToCon Char Char Source # | |
| ToCon Double Double Source # | |
| ToCon Float Float Source # | |
| ToCon Int Int Source # | |
| ToCon Word Word Source # | |
| ToCon v v Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| ToCon a b => ToCon a (Identity b) Source # | |
| (Generic a, Generic b, GToCon Arity0 (Rep a) (Rep b)) => ToCon a (Default b) Source # | |
| ToCon a b => ToCon (Identity a) b Source # | |
| (ToCon a b, Mergeable a) => ToCon (Union a) b Source # | |
| ToCon (SymIntN 8) Int8 Source # | |
| ToCon (SymIntN 16) Int16 Source # | |
| ToCon (SymIntN 32) Int32 Source # | |
| ToCon (SymIntN 64) Int64 Source # | |
| ToCon (SymIntN 64) Int Source # | |
| ToCon (SymWordN 8) Word8 Source # | |
| ToCon (SymWordN 16) Word16 Source # | |
| ToCon (SymWordN 32) Word32 Source # | |
| ToCon (SymWordN 64) Word64 Source # | |
| ToCon (SymWordN 64) Word Source # | |
| ToCon a b => ToCon (Identity a) (Identity b) Source # | |
| ToCon a_1 a_2 => ToCon (First a_1) (First a_2) Source # | |
| ToCon a_1 a_2 => ToCon (Last a_1) (Last a_2) Source # | |
| ToCon a_1 a_2 => ToCon (Down a_1) (Down a_2) Source # | |
| ToCon a_1 a_2 => ToCon (Dual a_1) (Dual a_2) Source # | |
| ToCon a_1 a_2 => ToCon (Product a_1) (Product a_2) Source # | |
| ToCon a_1 a_2 => ToCon (Sum a_1) (Sum a_2) Source # | |
| ToCon p0 p => ToCon (Par1 p0) (Par1 p) Source # | |
| ToCon a b => ToCon (Union a) (Union b) Source # | |
| (KnownNat n, 1 <= n) => ToCon (IntN n) (IntN n) Source # | |
| (KnownNat n, 1 <= n) => ToCon (WordN n) (WordN n) Source # | |
| (forall (n :: Nat). (KnownNat n, 1 <= n) => ToCon (sbv n) (cbv n)) => ToCon (SomeBV sbv) (SomeBV cbv) Source # | |
| (KnownNat n, 1 <= n) => ToCon (SymIntN n) (IntN n) Source # | |
| (KnownNat n, 1 <= n) => ToCon (SymIntN n) (SymIntN n) Source # | |
| (KnownNat n, 1 <= n) => ToCon (SymWordN n) (WordN n) Source # | |
| (KnownNat n, 1 <= n) => ToCon (SymWordN n) (SymWordN n) Source # | |
| ToCon a_1 a_2 => ToCon (Maybe a_1) (Maybe a_2) Source # | |
| ToCon a_1 a_2 => ToCon [a_1] [a_2] Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| (Generic1 f1, Generic1 f2, GToCon Arity1 (Rep1 f1) (Rep1 f2), ToCon a b) => ToCon (f1 a) (Default1 f2 b) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2) => ToCon (Either a_1 b_1) (Either a_2 b_2) Source # | |
| (ToCon e1 e2, ToCon a1 a2) => ToCon (Either e1 a1) (CBMCEither e2 a2) Source # | |
| ToCon (U1 p0) (U1 p) Source # | |
| ToCon (V1 p0) (V1 p) Source # | |
| (ToCon e1 e2, ToCon a1 a2) => ToCon (CBMCEither e1 a1) (Either e2 a2) Source # | |
| (ToCon e1 e2, ToCon a1 a2) => ToCon (CBMCEither e1 a1) (CBMCEither e2 a2) Source # | |
Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods toCon :: CBMCEither e1 a1 -> Maybe (CBMCEither e2 a2) Source # | |
| ValidFP eb sb => ToCon (FP eb sb) (FP eb sb) Source # | |
| ValidFP eb sb => ToCon (SymFP eb sb) (FP eb sb) Source # | |
| ValidFP eb sb => ToCon (SymFP eb sb) (SymFP eb sb) Source # | |
| (SupportedPrim a, SupportedPrim b) => ToCon (a -~> b) (a -~> b) Source # | |
| (SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa -~> sb) (ca --> cb) Source # | |
| (SupportedPrim a, SupportedPrim b) => ToCon (a =~> b) (a =~> b) Source # | |
| (SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa =~> sb) (ca =-> cb) Source # | |
| (ToCon1 m1 m2, ToCon a b) => ToCon (MaybeT m1 a) (MaybeT m2 b) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2) => ToCon (a_1, b_1) (a_2, b_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| ToCon (m1 (CBMCEither e1 a)) (Either e2 b) => ToCon (CBMCExceptT e1 m1 a) (Either e2 b) Source # | |
| ToCon (m1 (Either e1 a)) (Either e2 b) => ToCon (ExceptT e1 m1 a) (Either e2 b) Source # | |
| ToCon a0 a => ToCon (Const a0 b0) (Const a b) Source # | |
| ToCon (f0 a0) (f a) => ToCon (Ap f0 a0) (Ap f a) Source # | |
| ToCon (f0 a0) (f a) => ToCon (Alt f0 a0) (Alt f a) Source # | |
| ToCon (f0 p0) (f p) => ToCon (Rec1 f0 p0) (Rec1 f p) Source # | |
| (ToCon1 m1 m2, ToCon e1 e2, ToCon a b) => ToCon (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b) Source # | |
Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods toCon :: CBMCExceptT e1 m1 a -> Maybe (CBMCExceptT e2 m2 b) Source # | |
| (ToCon1 m1 m2, ToCon e1 e2, ToCon a b) => ToCon (ExceptT e1 m1 a) (ExceptT e2 m2 b) Source # | |
| (ToCon1 m m1, ToCon a b) => ToCon (IdentityT m a) (IdentityT m1 b) Source # | |
| (ToCon1 m1 m2, ToCon a b, ToCon s1 s2) => ToCon (WriterT s1 m1 a) (WriterT s2 m2 b) Source # | |
| (ToCon1 m1 m2, ToCon a b, ToCon s1 s2) => ToCon (WriterT s1 m1 a) (WriterT s2 m2 b) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2) => ToCon (a_1, b_1, c_1) (a_2, b_2, c_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| (ToCon (l0 a0) (l a), ToCon (r0 a0) (r a)) => ToCon (Product l0 r0 a0) (Product l r a) Source # | |
| (ToCon (l0 a0) (l a), ToCon (r0 a0) (r a)) => ToCon (Sum l0 r0 a0) (Sum l r a) Source # | |
| (ToCon (f0 p0) (f p), ToCon (g0 p0) (g p)) => ToCon ((f0 :*: g0) p0) ((f :*: g) p) Source # | |
| (ToCon (f0 p0) (f p), ToCon (g0 p0) (g p)) => ToCon ((f0 :+: g0) p0) ((f :+: g) p) Source # | |
| ToCon c0 c => ToCon (K1 i0 c0 p0) (K1 i c p) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2) => ToCon (a_1, b_1, c_1, d_1) (a_2, b_2, c_2, d_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| ToCon (f0 (g0 a0)) (f (g a)) => ToCon (Compose f0 g0 a0) (Compose f g a) Source # | |
| ToCon (f0 (g0 p0)) (f (g p)) => ToCon ((f0 :.: g0) p0) ((f :.: g) p) Source # | |
| ToCon (f0 p0) (f p) => ToCon (M1 i0 c0 f0 p0) (M1 i c f p) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2) => ToCon (a_1, b_1, c_1, d_1, e_1) (a_2, b_2, c_2, d_2, e_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2) => ToCon (a_1, b_1, c_1, d_1, e_1, f_1) (a_2, b_2, c_2, d_2, e_2, f_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2) => ToCon (a_1, b_1, c_1, d_1, e_1, f_1, g_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2) => ToCon (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2, ToCon i_1 i_2) => ToCon (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1, i_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2, i_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2, ToCon i_1 i_2, ToCon j_1 j_2) => ToCon (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1, i_1, j_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2, i_2, j_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2, ToCon i_1 i_2, ToCon j_1 j_2, ToCon k_1 k_2) => ToCon (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1, i_1, j_1, k_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2, i_2, j_2, k_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2, ToCon i_1 i_2, ToCon j_1 j_2, ToCon k_1 k_2, ToCon l_1 l_2) => ToCon (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1, i_1, j_1, k_1, l_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2, i_2, j_2, k_2, l_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2, ToCon i_1 i_2, ToCon j_1 j_2, ToCon k_1 k_2, ToCon l_1 l_2, ToCon m_1 m_2) => ToCon (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1, i_1, j_1, k_1, l_1, m_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2, i_2, j_2, k_2, l_2, m_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2, ToCon i_1 i_2, ToCon j_1 j_2, ToCon k_1 k_2, ToCon l_1 l_2, ToCon m_1 m_2, ToCon n_1 n_2) => ToCon (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1, i_1, j_1, k_1, l_1, m_1, n_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2, i_2, j_2, k_2, l_2, m_2, n_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2, ToCon i_1 i_2, ToCon j_1 j_2, ToCon k_1 k_2, ToCon l_1 l_2, ToCon m_1 m_2, ToCon n_1 n_2, ToCon o_1 o_2) => ToCon (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1, i_1, j_1, k_1, l_1, m_1, n_1, o_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2, i_2, j_2, k_2, l_2, m_2, n_2, o_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
class (forall a b. ToCon a b => ToCon (f1 a) (f2 b)) => ToCon1 f1 f2 where Source #
Lifting of ToCon to unary type constructors.
Methods
liftToCon :: (a -> Maybe b) -> f1 a -> Maybe (f2 b) Source #
Lift a conversion to concrete function to unary type constructors.
Instances
| ToCon1 Identity Identity Source # | |
| ToCon1 First First Source # | |
| ToCon1 Last Last Source # | |
| ToCon1 Down Down Source # | |
| ToCon1 Dual Dual Source # | |
| ToCon1 Product Product Source # | |
| ToCon1 Sum Sum Source # | |
| ToCon1 Union Union Source # | |
| ToCon1 Maybe Maybe Source # | |
| ToCon1 List List Source # | |
| (Generic1 f1, Generic1 f2, GToCon Arity1 (Rep1 f1) (Rep1 f2)) => ToCon1 f1 (Default1 f2) Source # | |
| ToCon a_1 a_2 => ToCon1 (Either a_1) (Either a_2) Source # | |
| ToCon1 m1 m2 => ToCon1 (MaybeT m1) (MaybeT m2) Source # | |
| ToCon a_1 a_2 => ToCon1 ((,) a_1) ((,) a_2) Source # | |
| ToCon a0 a => ToCon1 (Const a0 :: Type -> Type) (Const a :: Type -> Type) Source # | |
| ToCon1 f0 f => ToCon1 (Ap f0) (Ap f) Source # | |
| ToCon1 f0 f => ToCon1 (Alt f0) (Alt f) Source # | |
| (ToCon1 m1 m2, ToCon e1 e2) => ToCon1 (ExceptT e1 m1) (ExceptT e2 m2) Source # | |
| ToCon1 m m1 => ToCon1 (IdentityT m) (IdentityT m1) Source # | |
| (ToCon1 m1 m2, ToCon s1 s2) => ToCon1 (WriterT s1 m1) (WriterT s2 m2) Source # | |
| (ToCon1 m1 m2, ToCon s1 s2) => ToCon1 (WriterT s1 m1) (WriterT s2 m2) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2) => ToCon1 ((,,) a_1 b_1) ((,,) a_2 b_2) Source # | |
| (ToCon1 l0 l, ToCon1 r0 r) => ToCon1 (Product l0 r0) (Product l r) Source # | |
| (ToCon1 l0 l, ToCon1 r0 r) => ToCon1 (Sum l0 r0) (Sum l r) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2) => ToCon1 ((,,,) a_1 b_1 c_1) ((,,,) a_2 b_2 c_2) Source # | |
| (ToCon1 f0 f, ToCon1 g0 g) => ToCon1 (Compose f0 g0) (Compose f g) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2) => ToCon1 ((,,,,) a_1 b_1 c_1 d_1) ((,,,,) a_2 b_2 c_2 d_2) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2) => ToCon1 ((,,,,,) a_1 b_1 c_1 d_1 e_1) ((,,,,,) a_2 b_2 c_2 d_2 e_2) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2) => ToCon1 ((,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1) ((,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2) => ToCon1 ((,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1) ((,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2) => ToCon1 ((,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1) ((,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2, ToCon i_1 i_2) => ToCon1 ((,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1) ((,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2, ToCon i_1 i_2, ToCon j_1 j_2) => ToCon1 ((,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1) ((,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2, ToCon i_1 i_2, ToCon j_1 j_2, ToCon k_1 k_2) => ToCon1 ((,,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1 k_1) ((,,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2 k_2) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2, ToCon i_1 i_2, ToCon j_1 j_2, ToCon k_1 k_2, ToCon l_1 l_2) => ToCon1 ((,,,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1 k_1 l_1) ((,,,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2 k_2 l_2) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2, ToCon i_1 i_2, ToCon j_1 j_2, ToCon k_1 k_2, ToCon l_1 l_2, ToCon m_1 m_2) => ToCon1 ((,,,,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1 k_1 l_1 m_1) ((,,,,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2 k_2 l_2 m_2) Source # | |
| (ToCon a_1 a_2, ToCon b_1 b_2, ToCon c_1 c_2, ToCon d_1 d_2, ToCon e_1 e_2, ToCon f_1 f_2, ToCon g_1 g_2, ToCon h_1 h_2, ToCon i_1 i_2, ToCon j_1 j_2, ToCon k_1 k_2, ToCon l_1 l_2, ToCon m_1 m_2, ToCon n_1 n_2) => ToCon1 ((,,,,,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1 k_1 l_1 m_1 n_1) ((,,,,,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2 k_2 l_2 m_2 n_2) Source # | |
toCon1 :: (ToCon1 f1 f2, ToCon a b) => f1 a -> Maybe (f2 b) Source #
Lift the standard toCon to unary type constructors.
class (forall a b. ToCon a b => ToCon1 (f1 a) (f2 b)) => ToCon2 f1 f2 where Source #
Lifting of ToCon to binary type constructors.
Methods
liftToCon2 :: (a -> Maybe b) -> (c -> Maybe d) -> f1 a c -> Maybe (f2 b d) Source #
Lift conversion to concrete functions to binary type constructors.
Instances
| ToCon2 Either Either Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| ToCon2 (,) (,) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| ToCon a b => ToCon2 ((,,) a) ((,,) b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| (ToCon a c, ToCon b d) => ToCon2 ((,,,) a b) ((,,,) c d) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
toCon2 :: (ToCon2 f1 f2, ToCon a b, ToCon c d) => f1 a c -> Maybe (f2 b d) Source #
Lift the standard toCon to binary type constructors.
class Mergeable b => ToSym a b where Source #
Convert a concrete value to symbolic value.
Methods
Convert a concrete value to symbolic value.
>>>toSym False :: SymBoolfalse
>>>toSym [False, True] :: [SymBool][false,true]
Instances
class (forall a b. ToSym a b => ToSym (f1 a) (f2 b), Mergeable1 f2) => ToSym1 f1 f2 where Source #
Lifting of ToSym to unary type constructors.
Methods
liftToSym :: Mergeable b => (a -> b) -> f1 a -> f2 b Source #
Lift a conversion to symbolic function to unary type constructors.
Instances
| ToSym1 Identity Identity Source # | |
| ToSym1 First First Source # | |
| ToSym1 Last Last Source # | |
| ToSym1 Down Down Source # | |
| ToSym1 Dual Dual Source # | |
| ToSym1 Product Product Source # | |
| ToSym1 Sum Sum Source # | |
| ToSym1 Union Union Source # | |
| ToSym1 Maybe Maybe Source # | |
| ToSym1 List List Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (Generic1 f1, Generic1 f2, GToSym Arity1 (Rep1 f1) (Rep1 f2), GMergeable Arity1 (Rep1 f2)) => ToSym1 f1 (Default1 f2) Source # | |
| ToSym a_1 a_2 => ToSym1 (Either a_1) (Either a_2) Source # | |
| ToSym1 m1 m2 => ToSym1 (MaybeT m1) (MaybeT m2) Source # | |
| ToSym a_1 a_2 => ToSym1 ((,) a_1) ((,) a_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| ToSym a0 a => ToSym1 (Const a0 :: Type -> Type) (Const a :: Type -> Type) Source # | |
| ToSym1 f0 f => ToSym1 (Ap f0) (Ap f) Source # | |
| ToSym1 f0 f => ToSym1 (Alt f0) (Alt f) Source # | |
| (ToSym1 m1 m2, ToSym e1 e2) => ToSym1 (ExceptT e1 m1) (ExceptT e2 m2) Source # | |
| ToSym1 m m1 => ToSym1 (IdentityT m) (IdentityT m1) Source # | |
| (ToSym s2 s1, ToSym1 m1 m2, Mergeable1 m2) => ToSym1 (ReaderT s1 m1) (ReaderT s2 m2) Source # | |
| (ToSym1 m1 m2, Mergeable s) => ToSym1 (StateT s m1) (StateT s m2) Source # | |
| (ToSym1 m1 m2, Mergeable s) => ToSym1 (StateT s m1) (StateT s m2) Source # | |
| (ToSym1 m1 m2, ToSym s1 s2) => ToSym1 (WriterT s1 m1) (WriterT s2 m2) Source # | |
| (ToSym1 m1 m2, ToSym s1 s2) => ToSym1 (WriterT s1 m1) (WriterT s2 m2) Source # | |
| (ToSym a_1 a_2, ToSym b_1 b_2) => ToSym1 ((,,) a_1 b_1) ((,,) a_2 b_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym1 l0 l, ToSym1 r0 r) => ToSym1 (Product l0 r0) (Product l r) Source # | |
| (ToSym1 l0 l, ToSym1 r0 r) => ToSym1 (Sum l0 r0) (Sum l r) Source # | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2) => ToSym1 ((,,,) a_1 b_1 c_1) ((,,,) a_2 b_2 c_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| ToSym c a => ToSym1 ((->) a) ((->) c) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym1 f0 f, ToSym1 g0 g) => ToSym1 (Compose f0 g0) (Compose f g) Source # | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2) => ToSym1 ((,,,,) a_1 b_1 c_1 d_1) ((,,,,) a_2 b_2 c_2 d_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2) => ToSym1 ((,,,,,) a_1 b_1 c_1 d_1 e_1) ((,,,,,) a_2 b_2 c_2 d_2 e_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2) => ToSym1 ((,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1) ((,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2) => ToSym1 ((,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1) ((,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2) => ToSym1 ((,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1) ((,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2) => ToSym1 ((,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1) ((,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2) => ToSym1 ((,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1) ((,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2, ToSym k_1 k_2) => ToSym1 ((,,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1 k_1) ((,,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2 k_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2, ToSym k_1 k_2, ToSym l_1 l_2) => ToSym1 ((,,,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1 k_1 l_1) ((,,,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2 k_2 l_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2, ToSym k_1 k_2, ToSym l_1 l_2, ToSym m_1 m_2) => ToSym1 ((,,,,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1 k_1 l_1 m_1) ((,,,,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2 k_2 l_2 m_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2, ToSym k_1 k_2, ToSym l_1 l_2, ToSym m_1 m_2, ToSym n_1 n_2) => ToSym1 ((,,,,,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1 k_1 l_1 m_1 n_1) ((,,,,,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2 k_2 l_2 m_2 n_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
toSym1 :: (ToSym1 f1 f2, ToSym a b) => f1 a -> f2 b Source #
Lift the standard toSym to unary type constructors.
class (forall a b. ToSym a b => ToSym1 (f1 a) (f2 b), Mergeable2 f2) => ToSym2 f1 f2 where Source #
Lifting of ToSym to binary type constructors.
Methods
liftToSym2 :: (a -> b) -> (c -> d) -> f1 a c -> f2 b d Source #
Lift conversion to symbolic functions to binary type constructors.
Instances
| ToSym2 Either Either Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods liftToSym2 :: (a -> b) -> (c -> d) -> Either a c -> Either b d Source # | |
| ToSym2 (,) (,) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods liftToSym2 :: (a -> b) -> (c -> d) -> (a, c) -> (b, d) Source # | |
| ToSym a b => ToSym2 ((,,) a) ((,,) b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods liftToSym2 :: (a0 -> b0) -> (c -> d) -> (a, a0, c) -> (b, b0, d) Source # | |
| (ToSym a c, ToSym b d) => ToSym2 ((,,,) a b) ((,,,) c d) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods liftToSym2 :: (a0 -> b0) -> (c0 -> d0) -> (a, b, a0, c0) -> (c, d, b0, d0) Source # | |
toSym2 :: (ToSym2 f1 f2, ToSym a b, ToSym c d) => f1 a c -> f2 b d Source #
Lift the standard toSym to binary type constructors.
Conversion between different symbolic types
class BitCast from to where Source #
Type class for bit-casting between types.
Special Considerations for Floating-Point Types:
Typically, bit-casting a value from type a to type b and then back to
type a should result in the original value. However, this is not always
true for floating-point values. In SMT-LIB2, there is only one NaN value with
multiple bit representations.
Given this, we do not provide BitCast for the FP type,
instead, we use the bitCastOrCanonical function to use a canonical
representation for the NaN values.
If your application requires distinguishing between different NaN values, it is recommended to define your own floating-point type using bit-vectors. This allows you to check for NaN values and perform operations by bitcasting back to the provided floating-point types when they are not NaN values.
Instances
class BitCastCanonical from to where Source #
The canonical value when the bitcast cannot be precisely performed.
For example, with SMT-LIB2, there is only one NaN for floating point numbers,
with multiple bit representations. Our underlying FP type
also follows this convention. This means that we cannot precisely bitcast a
FP to other types. So instead, we bitcast the NaN value
to a canonical representation, defined with this type class.
Methods
bitCastCanonicalValue :: proxy from -> to Source #
Instances
class BitCastOr from to where Source #
Bitcasting a value. If the value cannot be precisely bitcast, use the default value.
Instances
| BitCastOr FP16 Int16 Source # | |
| BitCastOr FP16 Word16 Source # | |
| BitCastOr FP32 Int32 Source # | |
| BitCastOr FP32 Word32 Source # | |
| BitCastOr FP32 Float Source # | |
| BitCastOr FP64 Int64 Source # | |
| BitCastOr FP64 Word64 Source # | |
| BitCastOr FP64 Double Source # | |
| (ValidFP eb sb, n ~ (eb + sb)) => BitCastOr (FP eb sb) (IntN n) Source # | |
| (ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (FP eb sb) (WordN r) Source # | |
| (ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (SymFP eb sb) (SymIntN r) Source # | |
| (ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (SymFP eb sb) (SymWordN r) Source # | |
type BitCastOrCanonical a b = (BitCastCanonical a b, BitCastOr a b) Source #
Constraint for bitcasting a value and when the value cannot be precisely bitcast, use the canonical value.
bitCastOrCanonical :: BitCastOrCanonical from to => from -> to Source #
Bitcasting a value and when the value cannot be precisely bitcast, use the canonical value.
class (MonadError e m, TryMerge m, Mergeable b, BitCastOr a b) => SafeBitCast e a b m where Source #
Bitcasting a value. If the value cannot be precisely bitcast, throw an error.
Methods
safeBitCast :: a -> m b Source #
Instances
class SymFromIntegral from to where Source #
Conversion from a symbolic integral type.
Methods
symFromIntegral :: from -> to Source #
Instances
Unsolvable types and merging
There are types that be directly represented as SMT formulas and therefore not directly supported by the SMT solvers. These types are referred to as unsolvable types. To symbolically evaluate such types, we represent them with symbolic unions. A symbolic union is a set of multiple values from different execution paths, each guarded with a corresponding path condition. The value of a union can be determined by an SMT solver based on the truth value of the path conditions.
Union basics
In Grisette, the symbolic union type is Union.
Two constructs are useful in constructing symbolic union values: mrgIf
and mrgSingle.
mrgSingle unconditionally wraps a value in a symbolic union container,
while mrgIf models branching control flow semantics with symbolic
conditions.
Here are some examples of using mrgSingle and mrgIf:
>>>mrgSingle ["a"] :: Union [SymInteger]{[a]}>>>mrgIf "a" (mrgSingle ["b"]) (mrgSingle ["c", "d"]) :: Union [SymInteger]{If a [b] [c,d]}
Union is a monad, and its bind operation is similar to tree
substitution.
This means you can then use monadic constructs to model sequential programs.
For example, the following pseudo code can be
modeled in Grisette with the combinators provided by Grisette, and the do-notation:
x = if a then [b] else [b,c] -- pseudo code, not Grisette code y = if d then [e] else [e,f] return (x ++ y :: [SymInteger])
>>>:{ret :: Union [SymInteger] ret = do x <- mrgIf "a" (return ["b"]) (return ["b","c"]) y <- mrgIf "d" (return ["e"]) (return ["e","f"]) -- we will explain mrgReturn later, but rule of thumb is to -- always use mrg* functions if provided by Grisette and if -- you don't understand what will happen with ordinary return. mrgReturn $ x ++ y :}
When this code is evaluated, the result would be as follows:
>>>ret{If (&& a d) [b,e] (If (|| a d) [b,(ite a e c),(ite a f e)] [b,c,e,f])}
In the result, we can see that the results are reorganized and the two lists with the same length are merged together. This is important for scaling symbolic evaluation to real-world problems.
The mrgReturn function is crucial for
ensuring that the results are merged. It resolves the Mergeable
constraint, and retrieves a merging strategy for the contained type from
the constraint.
The merging strategy is then cached in the Union container to
help merge the result of the entire do-block.
This is necessary due to
the constrained-monad problem,
as the return function from the Monad type class cannot resolve
extra constraints.
Our solution to this problem with merging strategy caching is inspired
by the knowledge propagation technique introduced in the
blog post by Oleg Kiselyov.
In addition to mrgReturn,
Grisette provides many combinators with the mrg prefix.
You should use these combinators and always have the result cache the merging strategy.
Consider the following code:
>>>return 1 :: Union Integer<1>>>>mrgReturn 1 :: Union Integer{1}>>>mrgIf "a" (return 1) (return 2) :: Union Integer{If a 1 2}
In the first example, using return instead of
mrgReturn results in a unmerged container
(printed as <...>), which means that no merging strategy is cached.
In the second and third example, using
mrgReturn or mrgIf results in a merged
container (printed as {...}) with a cached merging strategy.
When working with Union, it is important to always use the mrg
prefixed combinators to ensure that the merging strategy is properly
cached. This will enable Grisette to properly merge the results of the
entire do-block and scale symbolic evaluation to real-world problems.
Those functions that merges the results can also further propagate the
cached merging strategy, see how the result is merged:
>>>f x y = mrgIf "f" (return x) (return y) :: Union Integer>>>do; a <- mrgIf "a" (return 1) (return 2); f a (a + 1){If (&& a f) 1 (If (|| a f) 2 3)}
For more details on this, see the documentation for Union,
MergingStrategy, and the merging section in
this module.
Working with user-defined types
To make a type compatible with the symbolic evaluation and merging in
Grisette, you need to implement the Mergeable type class.
If you are only working with algebraic
data types, you can derive the Mergeable instance automatically
For example:
>>>import GHC.Generics>>>:{data X = X SymInteger Integer deriving (Generic, Show) deriving (Mergeable) via (Default X) :}
Grisette also provide deriveAll template haskell procedure to
derive all the instances for the classes that are relevant. This include
Generic, Show, Mergeable, etc. If you only want to
derive some of them, you can also use deriveAllExcept or
derive.
>>>:{data X = X SymInteger Integer deriveAllExcept ''X [''Ord] -- Ord is excluded because it is a symbolic type :}
Having the Mergeable instance allows you to use the Union type to
represent values of type X, and have them merged with the mrgIf
combinator:
>>>mrgIf "c1" (mrgSingle $ X "b" 1) (mrgIf "c2" (mrgSingle $ X "c" 2) (mrgSingle $ X "d" 1)) :: Union X{If (|| c1 (! c2)) (X (ite c1 b d) 1) (X c 2)}
Note that deriving all instances may need to enable many
extensions, see deriveAll for details.
Using monad transformers
It is also possible to apply monad transformers onto Union to extend
it with various mechanisms.
For example, by applying ExceptT,
you can symbolically evaluate a program with error handling.
To do this, you will need to define an error type and derive the Mergeable
instance for it. Then, you can use the combinators provided by
MonadError (and the mrg* variants of them in
Grisette.Lib.Control.Monad.Except) for error handling, and the mrgIf
combinator will also work with transformed Union containers.
Here's an example using the ExceptT transformer
to model error handling in Grisette:
>>>import Control.Monad.Except>>>:{data Error = Fail deriveAll ''Error :}
>>>mrgIf "a" (throwError Fail) (return "x") :: ExceptT Error Union SymIntegerExceptT {If a (Left Fail) (Right x)}
This will return a symbolic union value representing a program that
throws an error in the then branch and returns a value in the else
branch.
Details of the merging algorithm
The following is the details of the merging algorithm.
If you are not going to manually configure the system by writing a
MergingStrategy and will only use the derived strategies,
you can safely ignore the following contents in this section.
In Grisette, the symbolic union has the Ordered Guards (ORG) representation, which can be viewed as a nested if-then-else with some representation invariant.
For example, the following symbolic union represents a symbolic list of symbolic integers with length 1, 2 or 3. The values are kept sorted in the container: the list with length 1 is placed at the first place, the list with length 2 is placed at the second place, and so on.
\[ \left\{\begin{aligned}% &\texttt{[a]}&&\mathrm{if}&&\texttt{c1}\\% &\texttt{[b,b]}&&\mathrm{else~if}&&\texttt{c2}\\% &\texttt{[a,b,c]}&&\mathrm{otherwise}\end{aligned}\right. \]
In Haskell syntax, the container is represented as the following nested if-then-else tree
If c1 [a] (If c2 [b,b] [a,b,c])
The representations means that when c1 is true, then the value is a
list [a], or when c1 is false and c2 is true, the value is a list
[b,b], or otherwise the value is [a,b,c].
This representation allows you to use
the constructs that are not supported by the underlying solvers freely.
For example, when applying head on this structure, we can just
distribute the head function through the three branches, and get
\[ \left\{\begin{aligned}% &\texttt{head [a]}&&\mathrm{if}&&\texttt{c1}\\% &\texttt{head [b,b]}&&\mathrm{else~if}&&\texttt{c2}\\% &\texttt{head [a,b,c]}&&\mathrm{otherwise} \end{aligned}\right. \]
or, equivalently
\[ \left\{\begin{aligned}% &\texttt{a}&&\mathrm{if}&&\texttt{c1}\\% &\texttt{b}&&\mathrm{else~if}&&\texttt{c2}\\% &\texttt{a}&&\mathrm{otherwise}% \end{aligned}\right. \]
Further symbolic evaluation will also distribute computations over the branches in this result, and the identical branches will cause redundant computation. To mitigate this, Grisette would try to merge the branches, and the previous result would become
\[ \left\{\begin{aligned}% &\texttt{a}&&\mathrm{if}&&\texttt{c1}\vee\neg\texttt{c2}\\% &\texttt{b}&&\mathrm{otherwise}\\% \end{aligned}\right. \]
Note that if the contained type is symbolic Boolean, we may further merge the values into a single formula.
\[ \left\{\begin{aligned}&\texttt{(ite c1 a (ite c2 b a))}&&\mathrm{unconditional}\end{aligned}\right. \]
In Grisette, such merging happens in the mrgIf or
mrgIfPropagatedStrategy
functions, which model the symbolic conditional branching semantics.
To keep the merging efficient and generate small constraints, we enforce
that the symbolic union maintains the values in a sorted way, and merge
the unions with a mergesort-style merging algorithm. In the following
example, the two ORG containers passed to the mrgIf are sorted
with the natural ordering on the integers. In the result, the values are
also organized in a sorted way, and the path conditions are correctly
maintained.
\[ \texttt{mrgIf}\left[% \texttt{c},% \left\{\begin{aligned}% &\texttt{1}&&\mathrm{if}&&\texttt{c1}\\% &\texttt{3}&&\mathrm{else~if}&&\texttt{c2}\\% &\texttt{4}&&\mathrm{otherwise}% \end{aligned}\right.,% \left\{\begin{aligned}% &\texttt{1}&&\mathrm{if}&&\texttt{c3}\\% &\texttt{2}&&\mathrm{else~if}&&\texttt{c4}\\% &\texttt{4}&&\mathrm{otherwise}% \end{aligned}\right.% \right]% =\left\{\begin{aligned}% &\texttt{1}&&\mathrm{if}&&\texttt{(ite c c1 c3)}\\% &\texttt{2}&&\mathrm{else~if}&&\texttt{(&& (! c) c3)}\\% &\texttt{3}&&\mathrm{else~if}&&\texttt{(&& c c2)}\\% &\texttt{4}&&\mathrm{otherwise}% \end{aligned}\right. \]
So far, we have described ORG as a flat list of values. When the list is long, it is beneficial to partition the values and merge (some or all) partitions into nested ORG values. This hierarchical ORG representation is particularly useful for complex data types, such as tuples, which tend to yield long lists.
In the following example, v* are values, while t* are ORG containers.
The values in the containers are first partitioned into three groups:
{v11, v12, v13}, {v2}, and {v13}.
In each group, the values share some common features, (e.g., they are
constructed with the same data constructor).
The values in each group are organized in a subtree, e.g., the first group
is organized in the subtree t1.
The hierarchical representation also keeps a representation invariant:
at each level in the hierarchy, the values (or the subtrees) are also sorted
by some criteria. Here, in the first level, the values are sorted by the
constructor declaration order, and in the second level, the values are sorted
by the concrete field in the constructor A.
This criteria is given by the MergingStrategy in the Mergeable class,
called the root merging strategy of the type.
data X = A Integer SymInteger | B | C
\[ \left\{\begin{aligned}% &\texttt{t1}&&\mathrm{if}&&\texttt{c1}\\% &\texttt{B}&&\mathrm{else if}&&\texttt{c2}\\% &\texttt{C}&&\mathrm{otherwise}&&% \end{aligned}\right.% \hspace{2em}\mathrm{where}\hspace{2em}% \texttt{t1} = \left\{\begin{aligned}% &\texttt{A 1 a}&&\mathrm{if}&&\texttt{c11}\\% &\texttt{A 3 b}&&\mathrm{else if}&&\texttt{c12}\\% &\texttt{A 4 (&& x y)}&&\mathrm{otherwise}&&% \end{aligned}\right. \]
In Haskell syntax, it can be represented as follows:
If c1 (If c11 (A 1 a) (If c12 (A 3 b) (A 4 (&& x y))))
(If c2 B
C)All the symbolic unions in Grisette should maintain the hierarchical
sorted invariant, and are sorted in the same way, with respect to the same
merging strategy (the root merging strategy for the type).
We can then merge the containers with a hierarchical
merging algorithm: at each level, we align the values and subtrees, and merge
the aligned ones. In the following example, mrgIf resolves the root merging
strategy s, and calls the function mrgIf', which accepts the merging strategy
as an argument. The symbolic union operands to the mrgIf' function must be
sorted with the merging strategy passed to the function.
Here we use the name of the subtrees and values to indicate the order of them:
t1should be placed beforev3in thethenbranch,t1andv4can be aligned witht1'andv4', respectively.
The aligned subtrees will be merged recursively with mrgIf', with a
sub-strategy given by the merging strategy s for the subtrees.
For example, t1 and t1' will be merged with the sub-strategy s'.
The aligned values will be merged with a merging function, also given by
the merging strategy s. For example, v4 and v4' will be merged with
the merging function f'.
The ordering and the sub-strategies are abstracted with SortedStrategy,
and the merging functions will be wrapped in SimpleStrategy.
The merging algorithm can then be configured by implementing the merging
strategies for the types contained in a symbolic union. See the documentation
for MergingStrategy for details.
\[ \begin{aligned}% & \texttt{mrgIf}\left[% \texttt{c},% \left\{\begin{aligned}% &\texttt{t1}&&\mathrm{if}&&\texttt{c1}\\% &\texttt{v3}&&\mathrm{else~if}&&\texttt{c2}\\% &\texttt{v4}&&\mathrm{otherwise}% \end{aligned}\right.,% \left\{\begin{aligned}% &\texttt{t1'}&&\mathrm{if}&&\texttt{c3}\\% &\texttt{t2'}&&\mathrm{else~if}&&\texttt{c4}\\% &\texttt{v4'}&&\mathrm{otherwise}% \end{aligned}\right.% \right]\\% =~ & \texttt{mrgIf'}\left[% \texttt{s},% \texttt{c},% \left\{\begin{aligned}% &\texttt{t1}&&\mathrm{if}&&\texttt{c1}\\% &\texttt{v3}&&\mathrm{else~if}&&\texttt{c2}\\% &\texttt{v4}&&\mathrm{otherwise}% \end{aligned}\right.,% \left\{\begin{aligned}% &\texttt{t1'}&&\mathrm{if}&&\texttt{c3}\\% &\texttt{t2'}&&\mathrm{else~if}&&\texttt{c4}\\% &\texttt{v4'}&&\mathrm{otherwise}% \end{aligned}\right.% \right]\\% =~ & \left\{\begin{aligned}% &\texttt{mrgIf' s' c t1 t1'}&&\mathrm{if}&&\texttt{(ite c c1 c3)}\\% &\texttt{t2'}&&\mathrm{else~if}&&\texttt{(&& (! c) c4)}\\% &\texttt{v3}&&\mathrm{else~if}&&\texttt{(&& c c2)}\\% &\texttt{f' c v4 v4'}&&\mathrm{otherwise}% \end{aligned}\right. \end{aligned} \]
For more details of the algorithm, please refer to Grisette's paper.
Union Monad
Union is the UnionBase container (hidden) enhanced with
MergingStrategy
knowledge propagation.
The UnionBase models the underlying semantics evaluation semantics for
unsolvable types with the nested if-then-else tree semantics, and can be
viewed as the following structure:
data UnionBase a = UnionSingle a | UnionIf bool (Union a) (Union a)
The UnionSingle constructor is for a single value with the path condition
true, and the UnionIf constructor is the if operator in an if-then-else
tree.
For clarity, when printing a Union value, we will omit the UnionSingle
constructor. The following two representations has the same semantics.
If c1 (If c11 v11 (If c12 v12 v13))
(If c2 v2
v3)\[ \left\{\begin{aligned}&t_1&&\mathrm{if}&&c_1\\&v_2&&\mathrm{else if}&&c_2\\&v_3&&\mathrm{otherwise}&&\end{aligned}\right.\hspace{2em}\mathrm{where}\hspace{2em}t_1 = \left\{\begin{aligned}&v_{11}&&\mathrm{if}&&c_{11}\\&v_{12}&&\mathrm{else if}&&c_{12}\\&v_{13}&&\mathrm{otherwise}&&\end{aligned}\right. \]
To reduce the size of the if-then-else tree to reduce the number of paths to
execute, Grisette would merge the branches in a UnionBase container and
maintain a representation invariant for them. To perform this merging
procedure, Grisette relies on a type class called Mergeable and the
merging strategy defined by it.
UnionBase is a monad, so we can easily write code with the do-notation and
monadic combinators. However, the standard monadic operators cannot
resolve any extra constraints, including the Mergeable constraint (see
The constrained-monad
problem
by Sculthorpe et al.).
This prevents the standard do-notations to merge the results automatically,
and would result in bad performance or very verbose code.
To reduce this boilerplate, Grisette provide another monad, Union that
would try to cache the merging strategy.
The Union has two data constructors (hidden intentionally), UAny and
UMrg. The UAny data constructor (printed as <...>) wraps an
arbitrary (probably unmerged) UnionBase. It is constructed when no
Mergeable knowledge is available (for example, when constructed with
Haskell's return). The UMrg data constructor (printed as {...}) wraps
a merged UnionBase along with the Mergeable constraint. This constraint
can be propagated to the contexts without Mergeable knowledge, and helps
the system to merge the resulting UnionBase.
Examples:
return cannot resolve the Mergeable constraint.
>>>return 1 :: Union Integer<1>
mrgReturn can resolve the Mergeable constraint.
>>>import Grisette.Lib.Base>>>mrgReturn 1 :: Union Integer{1}
mrgIfPropagatedStrategy does not try to Mergeable constraint.
>>>mrgIfPropagatedStrategy "a" (return 1) (mrgIfPropagatedStrategy "b" (return 1) (return 2)) :: Union Integer<If a 1 (If b 1 2)>
But mrgIfPropagatedStrategy is able to merge the result if some of the
branches are merged and have a cached merging strategy:
>>>mrgIfPropagatedStrategy "a" (return 1) (mrgIfPropagatedStrategy "b" (mrgReturn 1) (return 2)) :: Union Integer{If (|| a b) 1 2}
The >>= operator uses mrgIfPropagatedStrategy internally. When the final
statement in a do-block merges the values, the system can then merge the
final result.
>>>:{do x <- mrgIfPropagatedStrategy (ssym "a") (return 1) (mrgIfPropagatedStrategy (ssym "b") (return 1) (return 2)) mrgSingle $ x + 1 :: Union Integer :} {If (|| a b) 2 3}
Calling a function that merges a result at the last line of a do-notation
will also merge the whole block. If you stick to these mrg* combinators and
all the functions will merge the results, the whole program can be
symbolically evaluated efficiently.
>>>f x y = mrgIf "c" x y :: Union Integer>>>:{do x <- mrgIfPropagatedStrategy (ssym "a") (return 1) (mrgIfPropagatedStrategy (ssym "b") (return 1) (return 2)) f x (x + 1) :} {If (&& c (|| a b)) 1 (If (|| a (|| b c)) 2 3)}
In Grisette.Lib.Base, Grisette.Lib.Mtl, we also provided more mrg*
variants of other combinators. You should stick to these combinators to
ensure efficient merging by Grisette.
Instances
class (Eq t, Ord t, Hashable t) => IsConcrete t Source #
Tag for concrete types. Useful for specifying the merge strategy for some parametrized types where we should have different merge strategy for symbolic and concrete ones.
Instances
unionBinOp :: (a -> a -> a) -> Union a -> Union a -> Union a Source #
Lift a binary operation to Union.
liftUnion :: forall u a. (Mergeable a, SymBranching u, Applicative u) => Union a -> u a Source #
Lift the Union to any Applicative SymBranching.
unionMergingStrategy :: Union a -> Maybe (MergingStrategy a) Source #
Get the (possibly empty) cached merging strategy.
liftToMonadUnion :: (Mergeable a, MonadUnion u) => Union a -> u a Source #
Alias for liftUnion, but for monads.
unionSize :: Union a -> Int Source #
The size of a union is defined as the number of branches. For example,
>>>unionSize (return True)1>>>unionSize (mrgIf "a" (return 1) (return 2) :: Union Integer)2>>>unionSize (choose [1..7] "a" :: Union Integer)7
Mergeable
class Mergeable a where Source #
Each type is associated with a root merge strategy given by rootStrategy.
The root merge strategy should be able to merge every value of the type.
Grisette will use the root merge strategy to merge the values of the type in
a union.
Note 1: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving Mergeable via (Default X)
Instances
class (forall a. Mergeable a => Mergeable (u a)) => Mergeable1 (u :: Type -> Type) where Source #
Lifting of the Mergeable class to unary type constructors.
Methods
liftRootStrategy :: MergingStrategy a -> MergingStrategy (u a) Source #
Lift merge strategy through the type constructor.
Instances
rootStrategy1 :: (Mergeable a, Mergeable1 u) => MergingStrategy (u a) Source #
Lift the root merge strategy through the unary type constructor.
class (forall a. Mergeable a => Mergeable1 (u a)) => Mergeable2 (u :: Type -> Type -> Type) where Source #
Lifting of the Mergeable class to binary type constructors.
Methods
liftRootStrategy2 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy (u a b) Source #
Lift merge strategy through the type constructor.
Instances
| Mergeable2 Either Source # | |
Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods liftRootStrategy2 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy (Either a b) Source # | |
| Mergeable2 (,) Source # | |
Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods liftRootStrategy2 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy (a, b) Source # | |
| Mergeable a => Mergeable2 ((,,) a) Source # | |
Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods liftRootStrategy2 :: MergingStrategy a0 -> MergingStrategy b -> MergingStrategy (a, a0, b) Source # | |
| (Mergeable a, Mergeable b) => Mergeable2 ((,,,) a b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods liftRootStrategy2 :: MergingStrategy a0 -> MergingStrategy b0 -> MergingStrategy (a, b, a0, b0) Source # | |
| Mergeable2 (->) Source # | |
Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods liftRootStrategy2 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy (a -> b) Source # | |
rootStrategy2 :: (Mergeable a, Mergeable b, Mergeable2 u) => MergingStrategy (u a b) Source #
Lift the root merge strategy through the binary type constructor.
class (forall a. Mergeable a => Mergeable2 (u a)) => Mergeable3 (u :: Type -> Type -> Type -> Type) where Source #
Lifting of the Mergeable class to ternary type constructors.
Methods
liftRootStrategy3 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy c -> MergingStrategy (u a b c) Source #
Lift merge strategy through the type constructor.
Instances
| Mergeable3 (,,) Source # | |
Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods liftRootStrategy3 :: MergingStrategy a -> MergingStrategy b -> MergingStrategy c -> MergingStrategy (a, b, c) Source # | |
| Mergeable a => Mergeable3 ((,,,) a) Source # | |
Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods liftRootStrategy3 :: MergingStrategy a0 -> MergingStrategy b -> MergingStrategy c -> MergingStrategy (a, a0, b, c) Source # | |
rootStrategy3 :: (Mergeable a, Mergeable b, Mergeable c, Mergeable3 u) => MergingStrategy (u a b c) Source #
Lift the root merge strategy through the binary type constructor.
Merging strategy
data MergingStrategy a where Source #
Merging strategies.
You probably do not need to know the details of this type if you are only going to use algebraic data types. You can get merging strategies for them with type derivation.
In Grisette, a merged union (if-then-else tree) follows the hierarchical sorted representation invariant with regards to some merging strategy.
A merging strategy encodes how to merge a subset of the values of a given type. We have three types of merging strategies:
- Simple strategy
- Sorted strategy
- No strategy
The SimpleStrategy merges values with a simple merge function.
For example,
- the symbolic boolean values can be directly merged with
symIte. - the set
{1}, which is a subset of the values of the typeInteger, can be simply merged as the set contains only a single value. - all the
Justvalues of the typeMaybe SymBoolcan be simply merged by merging the wrapped symbolic boolean withsymIte.
The SortedStrategy merges values by first grouping the values with an
indexing function, and the values with the same index will be organized as
a sub-tree in the if-then-else structure of
UnionBase. Each group (sub-tree) will be
further merged with a sub-strategy for the index.
The index type should be a totally ordered type (with the Ord
type class). Grisette will use the indexing function to partition the values
into sub-trees, and organize them in a sorted way. The sub-trees will further
be merged with the sub-strategies. For example,
- all the integers can be merged with
SortedStrategyby indexing with the identity function and use theSimpleStrategyshown before as the sub-strategies. - all the
Maybe SymBoolvalues can be merged withSortedStrategyby indexing withisJust, theNothingandJustvalues can then be merged with different simple strategies as sub-strategies.
The NoStrategy does not perform any merging.
For example, we cannot merge values with function types that returns concrete
lists.
For ADTs, we can automatically derive the Mergeable type class, which
provides a merging strategy.
If the derived version does not work for you, you should determine
if your type can be directly merged with a merging function. If so, you can
implement the merging strategy as a SimpleStrategy.
If the type cannot be directly merged with a merging function, but could be
partitioned into subsets of values that can be simply merged with a function,
you should implement the merging strategy as a SortedStrategy.
For easier building of the merging strategies, check out the combinators
like wrapStrategy.
For more details, please see the documents of the constructors, or refer to Grisette's paper.
Constructors
| SimpleStrategy | Simple mergeable strategy. For symbolic booleans, we can implement its merge strategy as follows: SimpleStrategy symIte :: MergingStrategy SymBool |
Fields
| |
| SortedStrategy | Sorted mergeable strategy. For Integers, we can implement its merge strategy as follows: SortedStrategy id (\_ -> SimpleStrategy $ \_ t _ -> t) For SortedStrategy
(\case; Nothing -> False; Just _ -> True)
(\idx ->
if idx
then SimpleStrategy $ \_ t _ -> t
else SimpleStrategy $ \cond (Just l) (Just r) -> Just $ symIte cond l r) |
Fields
| |
| NoStrategy :: MergingStrategy a | For preventing the merging intentionally. This could be useful for keeping some value concrete and may help generate more efficient formulas. See Grisette's paper for details. |
Manual merging strategy construction
Arguments
| :: MergingStrategy a | The merge strategy to be wrapped |
| -> (a -> b) | The wrap function |
| -> (b -> a) | The unwrap function, which does not have to be defined for every value |
| -> MergingStrategy b |
Useful utility function for building merge strategies manually.
For example, to build the merge strategy for the just branch of Maybe a,
one could write
wrapStrategy Just fromMaybe rootStrategy :: MergingStrategy (Maybe a)
Arguments
| :: (a -> b -> r) | The wrap function |
| -> (r -> (a, b)) | The unwrap function, which does not have to be defined for every value |
| -> MergingStrategy a | The first merge strategy to be wrapped |
| -> MergingStrategy b | The second merge strategy to be wrapped |
| -> MergingStrategy r |
Useful utility function for building merge strategies for product types manually.
For example, to build the merge strategy for the following product type, one could write
data X = X { x1 :: Int, x2 :: Bool }
product2Strategy X (\(X a b) -> (a, b)) rootStrategy rootStrategy
:: MergingStrategy Xdata DynamicSortedIdx where Source #
Helper type for combining arbitrary number of indices into one. Useful when trying to write efficient merge strategy for lists/vectors.
Constructors
| DynamicSortedIdx :: forall idx. (Show idx, Ord idx, Typeable idx) => idx -> DynamicSortedIdx |
Instances
| Show DynamicSortedIdx Source # | |
Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods showsPrec :: Int -> DynamicSortedIdx -> ShowS # show :: DynamicSortedIdx -> String # showList :: [DynamicSortedIdx] -> ShowS # | |
| Eq DynamicSortedIdx Source # | |
Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods (==) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # (/=) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # | |
| Ord DynamicSortedIdx Source # | |
Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods compare :: DynamicSortedIdx -> DynamicSortedIdx -> Ordering # (<) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # (<=) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # (>) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # (>=) :: DynamicSortedIdx -> DynamicSortedIdx -> Bool # max :: DynamicSortedIdx -> DynamicSortedIdx -> DynamicSortedIdx # min :: DynamicSortedIdx -> DynamicSortedIdx -> DynamicSortedIdx # | |
data StrategyList container where Source #
Helper type for building efficient merge strategy for list-like containers.
Constructors
| StrategyList :: forall a container. container [DynamicSortedIdx] -> container (MergingStrategy a) -> StrategyList container |
Instances
buildStrategyList :: forall a container. Functor container => MergingStrategy a -> container a -> StrategyList container Source #
Helper function for building efficient merge strategy for list-like containers.
resolveStrategy :: forall x. MergingStrategy x -> x -> ([DynamicSortedIdx], MergingStrategy x) Source #
Resolves the indices and the terminal merge strategy for a value of some
Mergeable type.
resolveStrategy' :: forall x. x -> MergingStrategy x -> ([DynamicSortedIdx], MergingStrategy x) Source #
Resolves the indices and the terminal merge strategy for a value given a merge strategy for its type.
Simple mergeable types
class Mergeable a => SimpleMergeable a where Source #
This class indicates that a type has a simple root merge strategy.
Note: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving (Mergeable, SimpleMergeable) via (Default X)
Methods
mrgIte :: SymBool -> a -> a -> a Source #
Performs if-then-else with the simple root merge strategy.
>>>mrgIte "a" "b" "c" :: SymInteger(ite a b c)
Instances
class (Mergeable1 u, forall a. SimpleMergeable a => SimpleMergeable (u a)) => SimpleMergeable1 u where Source #
Lifting of the SimpleMergeable class to unary type constructors.
Methods
liftMrgIte :: (SymBool -> a -> a -> a) -> SymBool -> u a -> u a -> u a Source #
Lift mrgIte through the type constructor.
>>>liftMrgIte mrgIte "a" (Identity "b") (Identity "c") :: Identity SymIntegerIdentity (ite a b c)
Instances
mrgIte1 :: (SimpleMergeable1 u, SimpleMergeable a) => SymBool -> u a -> u a -> u a Source #
Lift the standard mrgIte function through the type constructor.
>>>mrgIte1 "a" (Identity "b") (Identity "c") :: Identity SymIntegerIdentity (ite a b c)
class (Mergeable2 u, forall a. SimpleMergeable a => SimpleMergeable1 (u a)) => SimpleMergeable2 u where Source #
Lifting of the SimpleMergeable class to binary type constructors.
Methods
liftMrgIte2 :: (SymBool -> a -> a -> a) -> (SymBool -> b -> b -> b) -> SymBool -> u a b -> u a b -> u a b Source #
Lift mrgIte through the type constructor.
>>>liftMrgIte2 mrgIte mrgIte "a" ("b", "c") ("d", "e") :: (SymInteger, SymBool)((ite a b d),(ite a c e))
Instances
| SimpleMergeable2 (,) Source # | |
| SimpleMergeable a => SimpleMergeable2 ((,,) a) Source # | |
| (SimpleMergeable a, SimpleMergeable b) => SimpleMergeable2 ((,,,) a b) Source # | |
| SimpleMergeable2 (->) Source # | |
mrgIte2 :: (SimpleMergeable2 u, SimpleMergeable a, SimpleMergeable b) => SymBool -> u a b -> u a b -> u a b Source #
Lift the standard mrgIte function through the type constructor.
>>>mrgIte2 "a" ("b", "c") ("d", "e") :: (SymInteger, SymBool)((ite a b d),(ite a c e))
Symbolic branching
class (SimpleMergeable1 u, forall a. Mergeable a => SimpleMergeable (u a), TryMerge u) => SymBranching (u :: Type -> Type) where Source #
Special case of the Mergeable1 and SimpleMergeable1 class for type
constructors that are SimpleMergeable when applied to any Mergeable
types.
This type class is used to generalize the mrgIf function to other
containers, for example, monad transformer transformed Unions.
Methods
mrgIfWithStrategy :: MergingStrategy a -> SymBool -> u a -> u a -> u a Source #
Symbolic if control flow with the result merged with some merge
strategy.
>>>mrgIfWithStrategy rootStrategy "a" (mrgSingle "b") (return "c") :: Union SymInteger{(ite a b c)}
Note: Be careful to call this directly in your code. The supplied merge strategy should be consistent with the type's root merge strategy, or some internal invariants would be broken and the program can crash.
This function is to be called when the Mergeable constraint can not be
resolved, e.g., the merge strategy for the contained type is given with
Mergeable1. In other cases, mrgIf is usually a better alternative.
mrgIfPropagatedStrategy :: SymBool -> u a -> u a -> u a Source #
Symbolic if control flow with the result.
This function does not need a merging strategy, and it will merge the result only if any of the branches is merged.
Instances
mrgIf :: (SymBranching u, Mergeable a) => SymBool -> u a -> u a -> u a Source #
Symbolic if control flow with the result merged with the type's root
merge strategy.
Equivalent to mrgIfWithStrategy rootStrategy
>>>mrgIf "a" (return "b") (return "c") :: Union SymInteger{(ite a b c)}
mergeWithStrategy :: SymBranching m => MergingStrategy a -> m a -> m a Source #
Try to merge the container with a given merge strategy.
merge :: (SymBranching m, Mergeable a) => m a -> m a Source #
Try to merge the container with the root strategy.
TryMerge operations
class TryMerge m where Source #
A class for containers that may or may not be merged.
If the container is capable of multi-path execution, then the
tryMergeWithStrategy function should merge the paths according to the
supplied strategy.
If the container is not capable of multi-path execution, then the
tryMergeWithStrategy function should be equivalent to id.
Note that this will not necessarily do a recursive merge for the elements.
Methods
tryMergeWithStrategy :: MergingStrategy a -> m a -> m a Source #
Instances
mrgSingle :: (TryMerge m, Applicative m, Mergeable a) => a -> m a Source #
Wrap a value in the applicative functor and propagate the type's root merge strategy.
Equivalent to mrgSingleWithStrategy rootStrategy
>>>mrgSingle "a" :: Union SymInteger{a}
mrgSingleWithStrategy :: (TryMerge m, Applicative m) => MergingStrategy a -> a -> m a Source #
Wrap a value in the applicative functor and capture the Mergeable
knowledge.
>>>mrgSingleWithStrategy rootStrategy "a" :: Union SymInteger{a}
Note: Be careful to call this directly from your code. The supplied merge strategy should be consistent with the type's root merge strategy, or some internal invariants would be broken and the program can crash.
This function is to be called when the Mergeable constraint can not be
resolved, e.g., the merge strategy for the contained type is given with
Mergeable1. In other cases, mrgPure
is usually a better alternative.
tryMerge :: (TryMerge m, Mergeable a) => m a -> m a Source #
Try to merge the container with the root strategy.
PlainUnion operations
class (Applicative u, SymBranching u) => PlainUnion (u :: Type -> Type) where Source #
Plain union containers that can be projected back into single value or if-guarded values.
Minimal complete definition
Methods
singleView :: u a -> Maybe a Source #
Pattern match to extract single values.
>>>singleView (return 1 :: Union Integer)Just 1>>>singleView (mrgIfPropagatedStrategy "a" (return 1) (return 2) :: Union Integer)Nothing
ifView :: u a -> Maybe (SymBool, u a, u a) Source #
Pattern match to extract if values.
>>>ifView (return 1 :: Union Integer)Nothing>>>ifView (mrgIfPropagatedStrategy "a" (return 1) (return 2) :: Union Integer)Just (a,<1>,<2>)>>>ifView (mrgIf "a" (return 1) (return 2) :: Union Integer)Just (a,{1},{2})
toGuardedList :: u a -> [(SymBool, a)] Source #
Convert the union to a guarded list.
>>>toGuardedList (mrgIf "a" (return 1) (mrgIf "b" (return 2) (return 3)) :: Union Integer)[(a,1),((&& b (! a)),2),((! (|| b a)),3)]
overestimateUnionValues :: Mergeable a => u a -> [a] Source #
Return all possible values in the union. Drop the path conditions.
>>>overestimateUnionValues (return 1 :: Union Integer)[1]
>>>overestimateUnionValues (mrgIf "a" (return 1) (return 2) :: Union Integer)[1,2]
Instances
pattern Single :: (PlainUnion u, Mergeable a) => a -> u a Source #
Pattern match to extract single values with singleView.
>>>case (return 1 :: Union Integer) of Single v -> v1
pattern If :: (PlainUnion u, Mergeable a) => SymBool -> u a -> u a -> u a Source #
Pattern match to extract guard values with ifView
>>>case (mrgIfPropagatedStrategy "a" (return 1) (return 2) :: Union Integer) of If c t f -> (c,t,f)(a,<1>,<2>)
simpleMerge :: forall u a. (SimpleMergeable a, PlainUnion u) => u a -> a Source #
Merge the simply mergeable values in a union, and extract the merged value.
In the following example,
mrgIfPropagatedStrategy
will not merge the results, and simpleMerge will merge it and extract the
single merged value.
>>>mrgIfPropagatedStrategy (ssym "a") (return $ ssym "b") (return $ ssym "c") :: Union SymBool<If a b c>>>>simpleMerge $ (mrgIfPropagatedStrategy (ssym "a") (return $ ssym "b") (return $ ssym "c") :: Union SymBool)(ite a b c)
(.#) :: (Function f a r, SimpleMergeable r, PlainUnion u) => f -> u a -> r infixl 9 Source #
Helper for applying functions on PlainUnion and SimpleMergeable.
>>>let f :: Integer -> Union Integer = \x -> mrgIf (ssym "a") (mrgSingle $ x + 1) (mrgSingle $ x + 2)>>>f .# (mrgIf (ssym "b" :: SymBool) (mrgSingle 0) (mrgSingle 2) :: Union Integer){If (&& b a) 1 (If b 2 (If a 3 4))}
onUnion :: forall u a r. (SimpleMergeable r, SymBranching u, PlainUnion u, Mergeable a) => (a -> r) -> u a -> r Source #
Lift a function to work on union values.
>>>sumU = onUnion sum :: Union [SymInteger] -> SymInteger>>>sumU (mrgIfPropagatedStrategy "cond" (return ["a"]) (return ["b","c"]) :: Union [SymInteger])(ite cond a (+ b c))
onUnion2 :: forall u a b r. (SimpleMergeable r, SymBranching u, PlainUnion u, Mergeable a, Mergeable b) => (a -> b -> r) -> u a -> u b -> r Source #
Lift a function to work on union values.
onUnion3 :: forall u a b c r. (SimpleMergeable r, SymBranching u, PlainUnion u, Mergeable a, Mergeable b, Mergeable c) => (a -> b -> c -> r) -> u a -> u b -> u c -> r Source #
Lift a function to work on union values.
onUnion4 :: forall u a b c d r. (SimpleMergeable r, SymBranching u, PlainUnion u, Mergeable a, Mergeable b, Mergeable c, Mergeable d) => (a -> b -> c -> d -> r) -> u a -> u b -> u c -> u d -> r Source #
Lift a function to work on union values.
type MonadUnion u = (SymBranching u, Monad u) Source #
Class for monads that support union-like operations and
Mergeable knowledge propagation.
Pretty printing
Pretty printing of values.
This class is similar to the Pretty class from the Prettyprinter package,
but it also provides pretty printing with a given precedence level.
We are able to derive instances of this class for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving PPrint via (Default X)
The derived instance will pretty print the value with a format similar to the one used by ormolu.
Minimal complete definition
Methods
pformat :: a -> Doc ann Source #
pformatPrec :: Int -> a -> Doc ann Source #
pformatList :: [a] -> Doc ann Source #
Instances
docToTextWith :: LayoutOptions -> Doc ann -> Text Source #
Convenience function to layout and render a Doc to Text.
You can control the layout with LayoutOptions.
docToText :: Doc ann -> Text Source #
Convenience function to layout and render a Doc to Text.
The default layout options defaultLayoutOptions are used.
pformatTextWith :: PPrint a => LayoutOptions -> a -> Text Source #
Convenience function to format a value to Text.
You can control the layout with LayoutOptions.
pformatTextWithWidth :: PPrint a => Int -> a -> Text Source #
Convenience function to format a value to Text.
You can control the layout with a single number of the width limit.
pformatText :: PPrint a => a -> Text Source #
Convenience function to format a value to Text.
The default layout options defaultLayoutOptions are used.
class (forall a. PPrint a => PPrint (f a)) => PPrint1 f where Source #
Lifting of the PPrint class to unary type constructors.
Minimal complete definition
Methods
liftPFormatPrec :: (Int -> a -> Doc ann) -> ([a] -> Doc ann) -> Int -> f a -> Doc ann Source #
Lift a pretty-printer to a unary type constructor.
liftPFormatList :: (Int -> a -> Doc ann) -> ([a] -> Doc ann) -> [f a] -> Doc ann Source #
Lift a pretty-printer to list of values with unary type constructors.
Instances
pformatPrec1 :: (PPrint1 f, PPrint a) => Int -> f a -> Doc ann Source #
Lift the standard pretty-printer (pformatPrec, pformatList) to unary
type constructors.
pformatList1 :: (PPrint1 f, PPrint a) => [f a] -> Doc ann Source #
Lift the standard pretty-printer (pformatPrec, pformatList) to list of
values with unary type constructors.
class (forall a. PPrint a => PPrint1 (f a), forall a b. (PPrint a, PPrint b) => PPrint (f a b)) => PPrint2 f where Source #
Lifting of the PPrint class to binary type constructors.
Minimal complete definition
Methods
liftPFormatPrec2 :: (Int -> a -> Doc ann) -> ([a] -> Doc ann) -> (Int -> b -> Doc ann) -> ([b] -> Doc ann) -> Int -> f a b -> Doc ann Source #
Lift two pretty-printers to a binary type constructor.
liftPFormatList2 :: (Int -> a -> Doc ann) -> ([a] -> Doc ann) -> (Int -> b -> Doc ann) -> ([b] -> Doc ann) -> [f a b] -> Doc ann Source #
Lift two pretty-printers to list of values with binary type constructors.
Instances
| PPrint2 Either Source # | |
Defined in Grisette.Internal.Core.Data.Class.PPrint | |
| PPrint2 HashMap Source # | |
Defined in Grisette.Internal.Core.Data.Class.PPrint | |
| PPrint2 (,) Source # | |
Defined in Grisette.Internal.Core.Data.Class.PPrint | |
| PPrint a => PPrint2 ((,,) a) Source # | |
Defined in Grisette.Internal.Core.Data.Class.PPrint Methods liftPFormatPrec2 :: (Int -> a0 -> Doc ann) -> ([a0] -> Doc ann) -> (Int -> b -> Doc ann) -> ([b] -> Doc ann) -> Int -> (a, a0, b) -> Doc ann Source # liftPFormatList2 :: (Int -> a0 -> Doc ann) -> ([a0] -> Doc ann) -> (Int -> b -> Doc ann) -> ([b] -> Doc ann) -> [(a, a0, b)] -> Doc ann Source # | |
| (PPrint a, PPrint b) => PPrint2 ((,,,) a b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.PPrint Methods liftPFormatPrec2 :: (Int -> a0 -> Doc ann) -> ([a0] -> Doc ann) -> (Int -> b0 -> Doc ann) -> ([b0] -> Doc ann) -> Int -> (a, b, a0, b0) -> Doc ann Source # liftPFormatList2 :: (Int -> a0 -> Doc ann) -> ([a0] -> Doc ann) -> (Int -> b0 -> Doc ann) -> ([b0] -> Doc ann) -> [(a, b, a0, b0)] -> Doc ann Source # | |
pformatPrec2 :: (PPrint2 f, PPrint a, PPrint b) => Int -> f a b -> Doc ann Source #
Lift the standard pretty-printer (pformatPrec, pformatList) to binary
type constructors.
pformatList2 :: (PPrint2 f, PPrint a, PPrint b) => [f a b] -> Doc ann Source #
Lift the standard pretty-printer (pformatPrec, pformatList) to list of
values with binary type constructors.
Helpers for pretty printing
groupedEnclose :: Doc ann -> Doc ann -> Doc ann -> Doc ann Source #
Enclose a document with left and right documents.
The pretty printer will try to layout the document in a single line, but the right document may be split to a newline.
condEnclose :: Bool -> Doc ann -> Doc ann -> Doc ann -> Doc ann Source #
Conditionally enclose a document with left and right documents.
If the condition is True, then this function is equivalent to
groupedEnclose.
pformatWithConstructor :: Int -> Doc ann -> [Doc ann] -> Doc ann Source #
Pretty print a list of fields with a constructor.
Aligns the fields and nests them by 2 spaces.
pformatWithConstructorNoAlign :: Int -> Doc ann -> [Doc ann] -> Doc ann Source #
Pretty print a list of fields with a constructor without alignment.
viaShowsPrec :: (Int -> a -> ShowS) -> Int -> a -> Doc ann Source #
Pretty print a value using showsPrec.
Re-export Prettyprinter for convenience
module Prettyprinter
Symbolic Generation
It is usually useful to generate complex symbolic values. For example, in program synthesis task, we may want to generate symbolic programs to represent the search space given some specification.
To help with this, we provide a set of classes and functions. The core
of the symbolic generation is the Fresh monad, the GenSymSimple class,
and the GenSym class.
The Fresh monad is a combination of specialized state and reader
monads. It keeps an identifier, and an index. The generated symbolic
constants would be constructed with both the identifier and the index.
Each time a new symbolic constant is generated, the index would be
incremented. This keeps that the generated symbolic constants are unique.
The GenSymSimple class helps generate symbolic values that do not require
a symbolic union, for example, symbolic Booleans.
It provides the simpleFresh function, which accepts a specification
for the symbolic values to generate.
We do not need any specification to generate a symbolic Boolean, so we provide a unit value as the specification:
>>>runFresh (simpleFresh ()) "x" :: SymBoolx@0
We can generate a list of symbolic Booleans by specifying the length of the list, and the specification for the elements. The two elements in the generated list are unique as they have different indices.
>>>runFresh (simpleFresh (SimpleListSpec 2 ())) "x" :: [SymBool][x@0,x@1]>>>runFresh (simpleFresh (SimpleListSpec 2 (SimpleListSpec 1 ()))) "x" :: [[SymBool]][[x@0],[x@1]]
The GenSym class helps generate symbolic values that require a symbolic
union, for example, lists with different lengths.
It provides the fresh function, which accepts a specification
for the symbolic values to generate.
We can generate a list of length 0, 1, or 2 by specifying the minimum and maximum lengths, and the specification for the elements:
>>>runFresh (fresh (ListSpec 0 2 ())) "x" :: Union [SymBool]{If x@2 [] (If x@3 [x@1] [x@0,x@1])}
We can generate many symbolic values at once with the Fresh monad.
The symbolic constants are ensured to be unique:
>>>:{flip runFresh "x" $ do a :: SymBool <- simpleFresh () b :: Union [SymBool] <- fresh (ListSpec 0 2 ()) return (a, b) :} (x@0,{If x@3 [] (If x@4 [x@2] [x@1,x@2])})
When you are just generating a symbolic value, and do not need to compose
multiple simpleFresh or fresh calls, you can use the genSym and
genSymSimple functions instead.
>>>genSymSimple (SimpleListSpec 2 ()) "x" :: [SymBool][x@0,x@1]>>>genSym (ListSpec 0 2 ()) "x" :: Union [SymBool]{If x@2 [] (If x@3 [x@1] [x@0,x@1])}
Symbolic choices from a list of symbolic values is very useful.
With the chooseFresh function,
we can generate a symbolic value by choosing from a list of
alternative values.
Grisette would generate symbolic Boolean guards to perform the symbolic
choice.
>>>:{(flip runFresh "x" $ do a <- simpleFresh () b <- simpleFresh () chooseFresh [[a],[a,b],[a,a,b]]) :: Union [SymBool] :} {If x@2 [x@0] (If x@3 [x@0,x@1] [x@0,x@0,x@1])}
Symbolic Generation Context
newtype FreshIndex Source #
Index type used for GenSym.
To generate fresh variables, a monadic stateful context will be maintained. The index should be increased every time a new symbolic constant is generated.
Constructors
| FreshIndex Int |
Instances
Symbolic Generation Monad
class Monad m => MonadFresh m where Source #
Monad class for fresh symbolic value generation.
The monad should be a reader monad for the Identifier and a state monad for
the FreshIndex.
Methods
getFreshIndex :: m FreshIndex Source #
Get the current index for fresh variable generation.
setFreshIndex :: FreshIndex -> m () Source #
Set the current index for fresh variable generation.
getIdentifier :: m Identifier Source #
Get the identifier.
localIdentifier :: (Identifier -> Identifier) -> m a -> m a Source #
Change the identifier locally and use a new index from 0 locally.
Instances
nextFreshIndex :: MonadFresh m => m FreshIndex Source #
Get the next fresh index and increase the current index.
liftFresh :: MonadFresh m => Fresh a -> m a Source #
Lifts an Fresh aMonadFresh.
A symbolic generation monad transformer.
It is a reader monad transformer for an identifier and a state monad transformer for indices.
Each time a fresh symbolic variable is generated, the index should be increased.
Constructors
| FreshT | |
Fields
| |
Instances
runFresh :: Fresh a -> Identifier -> a Source #
Run the symbolic generation with the given identifier and 0 as the initial index.
runFreshT :: Monad m => FreshT m a -> Identifier -> m a Source #
Run the symbolic generation with the given identifier and 0 as the initial index.
mrgRunFreshT :: (Monad m, TryMerge m, Mergeable a) => FreshT m a -> Identifier -> m a Source #
Run the symbolic generation with the given identifier and 0 as the initial index, and try to merge the result.
freshString :: (MonadFresh m, IsString s) => String -> m s Source #
Generate a fresh string with the given postfix.
>>>runFresh (freshString "b") "a" :: String"a@0[b]"
Symbolic Generation Class
class Mergeable a => GenSym spec a where Source #
Class of types in which symbolic values can be generated with respect to some specification.
The result will be wrapped in a union-like monad. This ensures that we can generate those types with complex merging rules.
The uniqueness of symbolic constants is managed with the a monadic context.
Fresh and FreshT can be useful.
Minimal complete definition
Nothing
Methods
fresh :: MonadFresh m => spec -> m (Union a) Source #
Generate a symbolic value given some specification. Within a single
MonadFresh context, calls to fresh would generate unique symbolic
constants.
The following example generates a symbolic boolean. No specification is needed.
>>>runFresh (fresh ()) "a" :: Union SymBool{a@0}
The following example generates booleans, which cannot be merged into a
single value with type Bool. No specification is needed.
>>>runFresh (fresh ()) "a" :: Union Bool{If a@0 False True}
The following example generates Maybe Bools.
There are more than one symbolic constants introduced, and their uniqueness
is ensured. No specification is needed.
>>>runFresh (fresh ()) "a" :: Union (Maybe Bool){If a@0 Nothing (If a@1 (Just False) (Just True))}
The following example generates lists of symbolic booleans with length 1 to 2.
>>>runFresh (fresh (ListSpec 1 2 ())) "a" :: Union [SymBool]{If a@2 [a@1] [a@0,a@1]}
When multiple symbolic values are generated, there will not be any identifier collision
>>>runFresh (do; a <- fresh (); b <- fresh (); return (a, b)) "a" :: (Union SymBool, Union SymBool)({a@0},{a@1})
default fresh :: GenSymSimple spec a => MonadFresh m => spec -> m (Union a) Source #
Instances
class GenSymSimple spec a where Source #
Class of types in which symbolic values can be generated with respect to some specification.
The result will not be wrapped in a union-like monad.
The uniqueness of symbolic constants is managed with the a monadic context.
Fresh and FreshT can be useful.
Methods
simpleFresh :: MonadFresh m => spec -> m a Source #
Generate a symbolic value given some specification. The uniqueness is ensured.
The following example generates a symbolic boolean. No specification is needed.
>>>runFresh (simpleFresh ()) "a" :: SymBoola@0
The following code generates list of symbolic boolean with length 2. As the length is fixed, we don't have to wrap the result in unions.
>>>runFresh (simpleFresh (SimpleListSpec 2 ())) "a" :: [SymBool][a@0,a@1]
Instances
genSym :: GenSym spec a => spec -> Identifier -> Union a Source #
Generate a symbolic variable wrapped in a Union without the monadic context. A globally unique identifier should be supplied to ensure the uniqueness of symbolic constants in the generated symbolic values.
>>>genSym (ListSpec 1 2 ()) "a" :: Union [SymBool]{If a@2 [a@1] [a@0,a@1]}
genSymSimple :: forall spec a. GenSymSimple spec a => spec -> Identifier -> a Source #
Generate a simple symbolic variable wrapped in a Union without the monadic context. A globally unique identifier should be supplied to ensure the uniqueness of symbolic constants in the generated symbolic values.
>>>genSymSimple (SimpleListSpec 2 ()) "a" :: [SymBool][a@0,a@1]
Symbolic Generation Class Derivation
derivedNoSpecFresh :: forall a m. (Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) => () -> m (Union a) Source #
We cannot provide DerivingVia style derivation for GenSym, while you can
use this fresh implementation to implement GenSym for your own types.
This fresh implementation is for the types that does not need any specification.
It will generate product types by generating each fields with () as specification,
and generate all possible values for a sum type.
Note: Never use on recursive types.
derivedNoSpecSimpleFresh :: forall a m. (Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) => () -> m a Source #
We cannot provide DerivingVia style derivation for GenSymSimple, while
you can use this simpleFresh implementation to implement GenSymSimple fo
your own types.
This simpleFresh implementation is for the types that does not need any specification.
It will generate product types by generating each fields with () as specification.
It will not work on sum types.
Note: Never use on recursive types.
derivedSameShapeSimpleFresh :: forall a m. (Generic a, GenSymSameShape (Rep a), MonadFresh m) => a -> m a Source #
We cannot provide DerivingVia style derivation for GenSymSimple, while
you can use this simpleFresh implementation to implement GenSymSimple fo
your own types.
This simpleFresh implementation is for the types that can be generated with
a reference value of the same type.
For sum types, it will generate the result with the same data constructor. For product types, it will generate the result by generating each field with the corresponding reference value.
Note: Can be used on recursive types.
Symbolic choice
chooseFresh :: forall a m. (Mergeable a, MonadFresh m) => [a] -> m (Union a) Source #
Symbolically chooses one of the provided values.
The procedure creates n - 1 fresh symbolic boolean variables every time it
is evaluated, and use these variables to conditionally select one of the n
provided expressions.
The result will be wrapped in a union-like monad, and also a monad
maintaining the MonadFresh context.
>>>runFresh (chooseFresh [1,2,3]) "a" :: Union Integer{If a@0 1 (If a@1 2 3)}
chooseSimpleFresh :: forall a m. (SimpleMergeable a, MonadFresh m) => [a] -> m a Source #
Symbolically chooses one of the provided values.
The procedure creates n - 1 fresh symbolic boolean variables every time it is evaluated, and use
these variables to conditionally select one of the n provided expressions.
The result will not be wrapped in a union-like monad, but will be
wrapped in a monad maintaining the Fresh context.
>>>import Data.Proxy>>>runFresh (chooseSimpleFresh [ssym "b", ssym "c", ssym "d"]) "a" :: SymInteger(ite a@0 b (ite a@1 c d))
chooseUnionFresh :: forall a m. (Mergeable a, MonadFresh m) => [Union a] -> m (Union a) Source #
Symbolically chooses one of the provided values wrapped in union-like
monads. The procedure creates n - 1 fresh symbolic boolean variables every
time it is evaluated, and use these variables to conditionally select one of
the n provided expressions.
The result will be wrapped in a union-like monad, and also a monad
maintaining the Fresh context.
>>>let a = runFresh (chooseFresh [1, 2]) "a" :: Union Integer>>>let b = runFresh (chooseFresh [2, 3]) "b" :: Union Integer>>>runFresh (chooseUnionFresh [a, b]) "c" :: Union Integer{If (&& c@0 a@0) 1 (If (|| c@0 b@0) 2 3)}
choose :: forall a. Mergeable a => [a] -> Identifier -> Union a Source #
A wrapper for chooseFresh that executes the MonadFresh context.
A globally unique identifier should be supplied to ensure the uniqueness of
symbolic constants in the generated symbolic values.
chooseSimple :: forall a. SimpleMergeable a => [a] -> Identifier -> a Source #
A wrapper for chooseSimpleFresh that executes the MonadFresh context.
A globally unique identifier should be supplied to ensure the uniqueness of
symbolic constants in the generated symbolic values.
chooseUnion :: forall a. Mergeable a => [Union a] -> Identifier -> Union a Source #
A wrapper for chooseUnionFresh that executes the MonadFresh context.
A globally unique identifier should be supplied to ensure the uniqueness of
symbolic constants in the generated symbolic values.
Useful specifications
data EnumGenBound a Source #
Specification for numbers with lower bound (inclusive) and upper bound (exclusive)
>>>runFresh (fresh (EnumGenBound @Integer 0 4)) "c" :: Union Integer{If c@0 0 (If c@1 1 (If c@2 2 3))}
Constructors
| EnumGenBound a a |
Instances
| (Enum v, Mergeable v) => GenSym (EnumGenBound v) v Source # | |
Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => EnumGenBound v -> m (Union v) Source # | |
newtype EnumGenUpperBound a Source #
Specification for enum values with upper bound (exclusive). The result would chosen from [0 .. upperbound].
>>>runFresh (fresh (EnumGenUpperBound @Integer 4)) "c" :: Union Integer{If c@0 0 (If c@1 1 (If c@2 2 3))}
Constructors
| EnumGenUpperBound a |
Instances
| (Enum v, Mergeable v) => GenSym (EnumGenUpperBound v) v Source # | |
Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => EnumGenUpperBound v -> m (Union v) Source # | |
Specification for list generation.
>>>runFresh (fresh (ListSpec 0 2 ())) "c" :: Union [SymBool]{If c@2 [] (If c@3 [c@1] [c@0,c@1])}
>>>runFresh (fresh (ListSpec 0 2 (SimpleListSpec 1 ()))) "c" :: Union [[SymBool]]{If c@2 [] (If c@3 [[c@1]] [[c@0],[c@1]])}
Constructors
| ListSpec | |
Fields
| |
Instances
| Show spec => Show (ListSpec spec) Source # | |
| (GenSymConstrained spec a, Mergeable a) => GenSymConstrained (ListSpec spec) [a] Source # | |
Defined in Grisette.Experimental.GenSymConstrained Methods freshConstrained :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> ListSpec spec -> m (Union [a]) Source # | |
| (GenSym spec a, Mergeable a) => GenSym (ListSpec spec) [a] Source # | |
Defined in Grisette.Internal.Core.Data.Class.GenSym | |
data SimpleListSpec spec Source #
Specification for list generation of a specific length.
>>>runFresh (simpleFresh (SimpleListSpec 2 ())) "c" :: [SymBool][c@0,c@1]
Constructors
| SimpleListSpec | |
Fields
| |
Instances
Error Handling
Grisette supports using ExceptT to handle errors,
and provides the mrg* variants for the combinators in Grisette.Lib.Mtl,
for example, mrgThrowError.
>>>import Control.Monad.Except>>>import Grisette.Lib.Control.Monad.Except>>>mrgThrowError AssertionError :: ExceptT AssertionError Union ()ExceptT {Left AssertionError}
You can define your own error types, and reason about them with the solver APIs.
>>>import GHC.Generics>>>:{data Error = Error1 | Error2 | Error3 deriving (Show, Generic) deriving (Mergeable) via Default Error :}
>>>let [a,b,c] = ["a","b","c"] :: [SymBool]>>>res = mrgIf a (throwError Error1) (mrgIf b (return c) (throwError Error2)) :: ExceptT Error Union SymBool>>>resExceptT {If (|| a (! b)) (If a (Left Error1) (Left Error2)) (Right c)}>>>solveExcept z3 (\case Left _ -> con False; Right x -> x) resRight (Model {a -> False :: Bool, b -> True :: Bool, c -> True :: Bool})
The solver call in the above example means that we want the solver to find the conditions under which no error is thrown, and the result is true. For more details, please refer to the documentation of the solver APIs.
For those who prefer to encode errors as assertions and assumptions,
we provide the symAssert and symAssume functions. These functions
relies on the TransformError type class to transform the assertions
and assumptions to the user-defined error type.
See their documentation for details.
Predefined errors
data AssertionError Source #
Assertion error.
Constructors
| AssertionError |
Instances
data VerificationConditions Source #
Verification conditions. A crashed program path can terminate with either assertion violation errors or assumption violation errors.
Constructors
| AssertionViolation | |
| AssumptionViolation |
Instances
Error transformation
class TransformError from to where Source #
This class indicates that the error type to can always represent the
error type from.
This is useful in implementing generic procedures that may throw errors.
For example, we support symbolic division and modulo operations. These
operations should throw an error when the divisor is zero, and we use the
standard error type ArithException for this purpose.
However, the user may use other type to represent errors, so we need this
type class to transform the ArithException to the
user-defined types.
Another example of these generic procedures is the
symAssert and symAssume functions.
They can be used with any error types that are
compatible with the AssertionError and
VerificationConditions types, respectively.
Methods
transformError :: from -> to Source #
Transforms an error with type from to an error with type to.
Instances
symAssert :: (TransformError AssertionError to, Mergeable to, MonadError to erm, MonadUnion erm) => SymBool -> erm () Source #
Used within a monadic multi path computation to begin exception processing.
Checks the condition passed to the function. The current execution path will be terminated with assertion error if the condition is false.
If the condition is symbolic, Grisette will split the execution into two paths based on the condition. The symbolic execution will continue on the then-branch, where the condition is true. For the else branch, where the condition is false, the execution will be terminated.
The resulting monadic environment should be compatible with the AssertionError
error type. See TransformError type class for details.
Examples:
Terminates the execution if the condition is false.
Note that we may lose the Mergeable knowledge here if no possible execution
path is viable. This may affect the efficiency in theory, but in practice this
should not be a problem as all paths are terminated and no further evaluation
would be performed.
>>>symAssert (con False) :: ExceptT AssertionError Union ()ExceptT {Left AssertionError}>>>do; symAssert (con False); mrgReturn 1 :: ExceptT AssertionError Union IntegerExceptT <Left AssertionError>
No effect if the condition is true:
>>>symAssert (con True) :: ExceptT AssertionError Union ()ExceptT {Right ()}>>>do; symAssert (con True); mrgReturn 1 :: ExceptT AssertionError Union IntegerExceptT {Right 1}
Splitting the path and terminate one of them when the condition is symbolic.
>>>symAssert (ssym "a") :: ExceptT AssertionError Union ()ExceptT {If (! a) (Left AssertionError) (Right ())}>>>do; symAssert (ssym "a"); mrgReturn 1 :: ExceptT AssertionError Union IntegerExceptT {If (! a) (Left AssertionError) (Right 1)}
AssertionError is compatible with VerificationConditions:
>>>symAssert (ssym "a") :: ExceptT VerificationConditions Union ()ExceptT {If (! a) (Left AssertionViolation) (Right ())}
symAssume :: (TransformError VerificationConditions to, Mergeable to, MonadError to erm, MonadUnion erm) => SymBool -> erm () Source #
Used within a monadic multi path computation to begin exception processing.
Similar to symAssert, but terminates the execution path with AssumptionViolation error.
Examples:
>>>symAssume (ssym "a") :: ExceptT VerificationConditions Union ()ExceptT {If (! a) (Left AssumptionViolation) (Right ())}
symAssertWith :: (Mergeable e, MonadError e erm, MonadUnion erm) => e -> SymBool -> erm () Source #
Symbolic assertion with a custom error.
symAssertTransformableError :: (Mergeable to, TransformError from to, MonadError to erm, MonadUnion erm) => from -> SymBool -> erm () Source #
Used within a monadic multi path computation for exception processing.
Terminate the current execution path with the specified error if the condition does not hold. Compatible error can be transformed.
>>>let assert = symAssertTransformableError AssertionError :: SymBool -> ExceptT AssertionError Union ()>>>assert "a"ExceptT {If (! a) (Left AssertionError) (Right ())}
symThrowTransformableError :: (Mergeable to, Mergeable a, TransformError from to, MonadError to erm, MonadUnion erm) => from -> erm a Source #
Used within a monadic multi path computation to begin exception processing.
Terminate the current execution path with the specified error. Compatible errors can be transformed.
>>>symThrowTransformableError Overflow :: ExceptT AssertionError Union ()ExceptT {Left AssertionError}
Simulate CBMC error handling
newtype CBMCEither a b Source #
A wrapper type for Either. Uses different merging strategies.
Constructors
| CBMCEither | |
Fields
| |
Instances
newtype CBMCExceptT e m a Source #
Similar to ExceptT, but with different error
handling mechanism.
Constructors
| CBMCExceptT | |
Fields
| |
Instances
cbmcExcept :: Monad m => Either e a -> CBMCExceptT e m a Source #
Wrap an Either value in CBMCExceptT
mapCBMCExceptT :: (m (Either e a) -> n (Either e' b)) -> CBMCExceptT e m a -> CBMCExceptT e' n b Source #
Map the error and values in a CBMCExceptT
withCBMCExceptT :: Functor m => (e -> e') -> CBMCExceptT e m a -> CBMCExceptT e' m a Source #
Map the error in a CBMCExceptT
Solver backend
Grisette abstracts the solver backend with the Solver type class,
and the most basic solver call is the solve function.
In the following code, we will search for the integer solutions to two
equation systems.
The first equation system, as shown below, has the solution (x, y) = (13, -7).
[ left{ begin{aligned} x + y &= 6 -- x - y &= 20
Solver interfaces
data SolvingFailure Source #
The current failures that can be returned by the solver.
Constructors
| Unsat | Unsatisfiable: No model is available. |
| Unk | Unknown: The solver cannot determine whether the formula is satisfiable. |
| ResultNumLimitReached | The solver has reached the maximum number of models to return. |
| SolvingError SomeException | The solver has encountered an error. |
| Terminated | The solver has been terminated. |
Instances
| Show SolvingFailure Source # | |
Defined in Grisette.Internal.Core.Data.Class.Solver Methods showsPrec :: Int -> SolvingFailure -> ShowS # show :: SolvingFailure -> String # showList :: [SolvingFailure] -> ShowS # | |
class Monad m => MonadicSolver m where Source #
A monadic solver interface.
This interface abstract the monadic interface of a solver. All the operations
performed in the monad are using a single solver instance. The solver
instance is management by the monad's run function.
Methods
monadicSolverPush :: Int -> m () Source #
monadicSolverPop :: Int -> m () Source #
monadicSolverResetAssertions :: m () Source #
monadicSolverAssert :: SymBool -> m () Source #
monadicSolverCheckSat :: m (Either SolvingFailure Model) Source #
Instances
| MonadIO m => MonadicSolver (SBVIncrementalT m) Source # | |
Defined in Grisette.Internal.Backend.Solving Methods monadicSolverPush :: Int -> SBVIncrementalT m () Source # monadicSolverPop :: Int -> SBVIncrementalT m () Source # monadicSolverResetAssertions :: SBVIncrementalT m () Source # monadicSolverAssert :: SymBool -> SBVIncrementalT m () Source # monadicSolverCheckSat :: SBVIncrementalT m (Either SolvingFailure Model) Source # | |
monadicSolverSolve :: MonadicSolver m => SymBool -> m (Either SolvingFailure Model) Source #
Solve a single formula with a monadic solver. Find an assignment to it to make it true.
data SolverCommand Source #
The commands that can be sent to a solver.
class Solver handle => ConfigurableSolver config handle | config -> handle where Source #
A class that abstracts the creation of a solver instance based on a configuration.
The solver instance will need to be terminated by the user, with the solver interface.
Instances
| ConfigurableSolver GrisetteSMTConfig SBVSolverHandle Source # | |
Defined in Grisette.Internal.Backend.Solving Methods newSolver :: GrisetteSMTConfig -> IO SBVSolverHandle Source # | |
class Solver handle where Source #
A class that abstracts the solver interface.
Minimal complete definition
solverRunCommand, solverCheckSat, solverTerminate, solverForceTerminate
Methods
solverRunCommand :: (handle -> IO (Either SolvingFailure a)) -> handle -> SolverCommand -> IO (Either SolvingFailure a) Source #
Run a solver command.
solverAssert :: handle -> SymBool -> IO (Either SolvingFailure ()) Source #
Assert a formula.
solverCheckSat :: handle -> IO (Either SolvingFailure Model) Source #
Solve a formula.
solverPush :: handle -> Int -> IO (Either SolvingFailure ()) Source #
Push n levels.
solverPop :: handle -> Int -> IO (Either SolvingFailure ()) Source #
Pop n levels.
solverResetAssertions :: handle -> IO (Either SolvingFailure ()) Source #
Reset all assertions in the solver.
The solver keeps all the assertions used in the previous commands:
>>>solver <- newSolver z3>>>solverSolve solver "a"Right (Model {a -> True :: Bool})>>>solverSolve solver $ symNot "a"Left Unsat
You can clear the assertions using solverResetAssertions:
>>>solverResetAssertions solverRight ()>>>solverSolve solver $ symNot "a"Right (Model {a -> False :: Bool})
solverTerminate :: handle -> IO () Source #
Terminate the solver, wait until the last command is finished.
solverForceTerminate :: handle -> IO () Source #
Force terminate the solver, do not wait for the last command to finish.
Instances
| Solver SBVSolverHandle Source # | |
Defined in Grisette.Internal.Backend.Solving Methods solverRunCommand :: (SBVSolverHandle -> IO (Either SolvingFailure a)) -> SBVSolverHandle -> SolverCommand -> IO (Either SolvingFailure a) Source # solverAssert :: SBVSolverHandle -> SymBool -> IO (Either SolvingFailure ()) Source # solverCheckSat :: SBVSolverHandle -> IO (Either SolvingFailure Model) Source # solverPush :: SBVSolverHandle -> Int -> IO (Either SolvingFailure ()) Source # solverPop :: SBVSolverHandle -> Int -> IO (Either SolvingFailure ()) Source # solverResetAssertions :: SBVSolverHandle -> IO (Either SolvingFailure ()) Source # solverTerminate :: SBVSolverHandle -> IO () Source # solverForceTerminate :: SBVSolverHandle -> IO () Source # | |
solverSolve :: Solver handle => handle -> SymBool -> IO (Either SolvingFailure Model) Source #
Solve a single formula. Find an assignment to it to make it true.
withSolver :: ConfigurableSolver config handle => config -> (handle -> IO a) -> IO a Source #
Start a solver, run a computation with the solver, and terminate the solver after the computation finishes.
When an exception happens, this will forcibly terminate the solver.
Note: if Grisette is compiled with sbv < 10.10, the solver likely won't be really terminated until it has finished the last action, and this will result in long-running or zombie solver instances.
This was due to a bug in sbv, which is fixed in https://github.com/LeventErkok/sbv/pull/695.
Arguments
| :: ConfigurableSolver config handle | |
| => config | solver configuration |
| -> SymBool | formula to solve, the solver will try to make it true |
| -> IO (Either SolvingFailure Model) |
Solve a single formula. Find an assignment to it to make it true.
>>>solve z3 ("a" .&& ("b" :: SymInteger) .== 1)Right (Model {a -> True :: Bool, b -> 1 :: Integer})>>>solve z3 ("a" .&& symNot "a")Left Unsat
Arguments
| :: Solver handle | |
| => handle | solver handle |
| -> Int | maximum number of models to return |
| -> SymBool | formula to solve, the solver will try to make it true |
| -> IO ([Model], SolvingFailure) |
Solve a single formula while returning multiple models to make it true. The maximum number of desired models are given.
Arguments
| :: ConfigurableSolver config handle | |
| => config | solver configuration |
| -> Int | maximum number of models to return |
| -> SymBool | formula to solve, the solver will try to make it true |
| -> IO ([Model], SolvingFailure) |
Solve a single formula while returning multiple models to make it true. The maximum number of desired models are given.
>>> solveMulti z3 4 ("a" .|| "b")
[Model {a -> True :: Bool, b -> False :: Bool},Model {a -> False :: Bool, b -> True :: Bool},Model {a -> True :: Bool, b -> True :: Bool}]Union with exceptions
class UnionWithExcept t u e v | t -> u e v where Source #
A class that abstracts the union-like structures that contains exceptions.
Methods
extractUnionExcept :: t -> u (Either e v) Source #
Extract a union of exceptions and values from the structure.
Instances
| UnionWithExcept (Union (Either e v)) Union e v Source # | |
Defined in Grisette.Internal.Core.Control.Monad.Union | |
| UnionWithExcept (Union (CBMCEither e v)) Union e v Source # | |
Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods extractUnionExcept :: Union (CBMCEither e v) -> Union (Either e v) Source # | |
| (Monad u, TryMerge u, Mergeable e, Mergeable v) => UnionWithExcept (CBMCExceptT e u v) u e v Source # | |
Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods extractUnionExcept :: CBMCExceptT e u v -> u (Either e v) Source # | |
| UnionWithExcept (ExceptT e u v) u e v Source # | |
Defined in Grisette.Internal.Core.Data.Class.Solver Methods extractUnionExcept :: ExceptT e u v -> u (Either e v) Source # | |
Arguments
| :: (UnionWithExcept t u e v, PlainUnion u, Functor u, Solver handle) | |
| => handle | solver handle |
| -> (Either e v -> SymBool) | mapping the results to symbolic boolean formulas, the solver would try to find a model to make the formula true |
| -> t | the program to be solved, should be a union of exception and values |
| -> IO (Either SolvingFailure Model) |
Solver procedure for programs with error handling.
Arguments
| :: (UnionWithExcept t u e v, PlainUnion u, Functor u, ConfigurableSolver config handle) | |
| => config | solver configuration |
| -> (Either e v -> SymBool) | mapping the results to symbolic boolean formulas, the solver would try to find a model to make the formula true |
| -> t | the program to be solved, should be a union of exception and values |
| -> IO (Either SolvingFailure Model) |
Solver procedure for programs with error handling.
>>>import Control.Monad.Except>>>let x = "x" :: SymInteger>>>:{res :: ExceptT AssertionError Union () res = do symAssert $ x .> 0 -- constrain that x is positive symAssert $ x .< 2 -- constrain that x is less than 2 :}
>>>:{translate (Left _) = con False -- errors are not desirable translate _ = con True -- non-errors are desirable :}
>>>solveExcept z3 translate resRight (Model {x -> 1 :: Integer})
solverSolveMultiExcept Source #
Arguments
| :: (UnionWithExcept t u e v, PlainUnion u, Functor u, Solver handle) | |
| => handle | solver configuration |
| -> Int | maximum number of models to return |
| -> (Either e v -> SymBool) | mapping the results to symbolic boolean formulas, the solver would try to find a model to make the formula true |
| -> t | the program to be solved, should be a union of exception and values |
| -> IO ([Model], SolvingFailure) |
Solver procedure for programs with error handling. Would return multiple models if possible.
Arguments
| :: (UnionWithExcept t u e v, PlainUnion u, Functor u, ConfigurableSolver config handle) | |
| => config | solver configuration |
| -> Int | maximum number of models to return |
| -> (Either e v -> SymBool) | mapping the results to symbolic boolean formulas, the solver would try to find a model to make the formula true |
| -> t | the program to be solved, should be a union of exception and values |
| -> IO ([Model], SolvingFailure) |
Solver procedure for programs with error handling. Would return multiple models if possible.
Generic Counter-example Guided Inductive Synthesis (CEGIS) interface
data VerifierResult cex exception Source #
The response from a verifier.
Constructors
| CEGISVerifierFoundCex cex | |
| CEGISVerifierNoCex | |
| CEGISVerifierException exception |
type SynthesisConstraintFun cex = cex -> IO SymBool Source #
Build the synthesizer constraint from the verfication result. The first argument will be guaranteed to be distinct during each invocation of the function in the CEGIS algorithm, so it can be used to instantiate the identifiers for fresh variables.
type VerifierFun cex exception = Model -> IO (VerifierResult cex exception) Source #
The verifier.
data CEGISResult exception Source #
The result of the CEGIS procedure.
Constructors
| CEGISSuccess Model | |
| CEGISVerifierFailure exception | |
| CEGISSolverFailure SolvingFailure |
Instances
| Show exception => Show (CEGISResult exception) Source # | |
Defined in Grisette.Internal.Core.Data.Class.CEGISSolver Methods showsPrec :: Int -> CEGISResult exception -> ShowS # show :: CEGISResult exception -> String # showList :: [CEGISResult exception] -> ShowS # | |
Arguments
| :: Solver handle | |
| => handle | Configuration of the solver. |
| -> Bool | Whether we should rerun the passed verifiers if any other verifier found a counter-example. |
| -> SymBool | The initial synthesis constraint. |
| -> SynthesisConstraintFun input | Synthesis constraint from counter-examples |
| -> [VerifierFun input exception] | The verifier functions. |
| -> IO ([input], CEGISResult exception) |
Generic CEGIS procedure. See genericCEGIS for more details.
The difference from genericCEGIS is that this function accepts a solver
handle for the synthesizer, instead of a solver configuration.
solverGenericCEGISWithRefinement Source #
Arguments
| :: Solver handle | |
| => handle | Configuration of the solver. |
| -> Bool | Whether we should rerun the passed verifiers if any other verifier found a counter-example. |
| -> SymBool | The initial synthesis constraint. |
| -> SynthesisConstraintFun input | Synthesis constraint from counter-examples |
| -> Maybe RefinementConditionFun | Refinement condition generator. |
| -> [VerifierFun input exception] | The verifier functions. |
| -> IO ([input], CEGISResult exception) |
Generic CEGIS procedure with refinement. See genericCEGISWithRefinement
for more details.
The difference from genericCEGISWithRefinement is that this function
accepts a solver handle for the synthesizer, instead of a solver
configuration.
Arguments
| :: ConfigurableSolver config handle | |
| => config | Configuration of the solver. |
| -> Bool | Whether we should rerun the passed verifiers if any other verifier found a counter-example. |
| -> SymBool | The initial synthesis constraint. |
| -> SynthesisConstraintFun input | Synthesis constraint from counter-examples |
| -> [VerifierFun input exception] | The verifier functions. |
| -> IO ([input], CEGISResult exception) |
Generic CEGIS procedure.
The CEGIS procedure will try to find a model that satisfies the initial synthesis constraint, and satisfies all the inputs generated by the verifier.
genericCEGISWithRefinement Source #
Arguments
| :: ConfigurableSolver config handle | |
| => config | Configuration of the solver. |
| -> Bool | Whether we should rerun the passed verifiers if any other verifier found a counter-example. |
| -> SymBool | The initial synthesis constraint. |
| -> SynthesisConstraintFun input | Synthesis constraint from counter-examples |
| -> Maybe RefinementConditionFun | Refinement condition generator. |
| -> [VerifierFun input exception] | The verifier functions. |
| -> IO ([input], CEGISResult exception) |
Generic CEGIS procedure.
The CEGIS procedure will try to find a model that satisfies the initial synthesis constraint, and satisfies all the inputs generated by the verifier.
CEGIS interfaces with pre/post conditions
data CEGISCondition Source #
The condition for CEGIS to solve.
The first argument is the pre-condition, and the second argument is the post-condition.
The CEGIS procedures would try to find a model for the formula
\[ \forall P. (\exists I. \mathrm{pre}(P, I)) \wedge (\forall I. \mathrm{pre}(P, I)\implies \mathrm{post}(P, I)) \]
In program synthesis tasks, \(P\) is the symbolic constants in the symbolic program, and \(I\) is the input. The pre-condition is used to restrict the search space of the program. The procedure would only return programs that meets the pre-conditions on every possible inputs, and there are at least one possible input. The post-condition is used to specify the desired program behaviors.
Constructors
| CEGISCondition SymBool SymBool |
Instances
solverCegisMultiInputs Source #
Arguments
| :: (EvalSym input, ExtractSym input, Solver handle) | |
| => handle | |
| -> handle | |
| -> [input] | Initial symbolic inputs. The solver will try to find a
program that works on all the inputs representable by these inputs (see
|
| -> (input -> CEGISCondition) | The condition for the solver to solve. All the symbolic constants that are not in the inputs will be considered as part of the symbolic program. |
| -> IO ([input], CEGISResult SolvingFailure) | The counter-examples generated during the CEGIS loop, and the model found by the solver. |
CEGIS with multiple (possibly symbolic) inputs. See cegisMultiInputs for
more details.
The difference from cegisMultiInputs is that this function accepts two
solver handles, one for the synthesizer and one for the verifier.
The synthesizer solver will **not** be reset, while the verifier solver will be reset after each iteration.
Arguments
| :: (Solver handle, EvalSym inputs, ExtractSym inputs, SymEq inputs) | |
| => handle | The synthesizer solver handle |
| -> handle | The verifier solver handle |
| -> inputs | Initial symbolic inputs. The solver will try to find a
program that works on all the inputs representable by it (see
|
| -> (inputs -> CEGISCondition) | The condition for the solver to solve. All the symbolic constants that are not in the inputs will be considered as part of the symbolic program. |
| -> IO ([inputs], CEGISResult SolvingFailure) | The counter-examples generated during the CEGIS loop, and the model found by the solver. |
CEGIS with a single symbolic input to represent a set of inputs. See
cegis for more details.
The difference from cegis is that this function accepts two solver handles,
one for the synthesizer and one for the verifier.
The synthesizer solver will **not** be reset, while the verifier solver will be reset after each iteration.
solverCegisExcept :: (UnionWithExcept t u e v, PlainUnion u, Functor u, EvalSym inputs, ExtractSym inputs, Solver handle, SymEq inputs) => handle -> handle -> inputs -> (Either e v -> CEGISCondition) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, using a single symbolic
input to represent a set of inputs. See cegisExcept for more details.
The difference from cegisExcept is that this function accepts two solver
handles, one for the synthesizer and one for the verifier.
The synthesizer solver will **not** be reset, while the verifier solver will be reset after each iteration.
solverCegisExceptStdVC :: (UnionWithExcept t u VerificationConditions (), PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, Solver handle, SymEq inputs) => handle -> handle -> inputs -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, using a single symbolic
input to represent a set of inputs. See cegisExceptStdVC for more details.
The difference from cegisExceptStdVC is that this function accepts two
solver handles, one for the synthesizer and one for the verifier.
The synthesizer solver will **not** be reset, while the verifier solver will be reset after each iteration.
solverCegisExceptVC :: (UnionWithExcept t u e v, PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, Solver handle, SymEq inputs) => handle -> handle -> inputs -> (Either e v -> u (Either VerificationConditions ())) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, using a single symbolic input to represent a set of inputs.
The errors should be translated to assertion or assumption violations.
The difference from cegisExceptVC is that this function accepts two solver
handles, one for the synthesizer and one for the verifier.
The synthesizer solver will **not** be reset, while the verifier solver will be reset after each iteration.
solverCegisExceptMultiInputs :: (Solver handle, EvalSym inputs, ExtractSym inputs, UnionWithExcept t u e v, PlainUnion u, Monad u) => handle -> handle -> [inputs] -> (Either e v -> CEGISCondition) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, using multiple (possibly symbolic) inputs to represent a set of inputs.
The difference from cegisExceptMultiInputs is that this function accepts
two solver handles, one for the synthesizer and one for the verifier.
The synthesizer solver will **not** be reset, while the verifier solver will be reset after each iteration.
solverCegisExceptStdVCMultiInputs :: (Solver handle, EvalSym inputs, ExtractSym inputs, UnionWithExcept t u VerificationConditions (), PlainUnion u, Monad u) => handle -> handle -> [inputs] -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, using multiple (possibly
symbolic) inputs to represent a set of inputs. See
cegisExceptStdVCMultiInputs for more details.
The difference from cegisExceptStdVCMultiInputs is that this function
accepts two solver handles, one for the synthesizer and one for the verifier.
The synthesizer solver will **not** be reset, while the verifier solver will be reset after each iteration.
solverCegisExceptVCMultiInputs :: (Solver handle, EvalSym inputs, ExtractSym inputs, UnionWithExcept t u e v, PlainUnion u, Monad u) => handle -> handle -> [inputs] -> (Either e v -> u (Either VerificationConditions ())) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, using multiple (possibly symbolic) inputs to represent a set of inputs.
The errors should be translated to assertion or assumption violations.
The difference from cegisExceptVCMultiInputs is that this function accepts
two solver handles, one for the synthesizer and one for the verifier.
The synthesizer solver will **not** be reset, while the verifier solver will be reset after each iteration.
Arguments
| :: (ExtractSym forallInput, Solver handle) | |
| => handle | |
| -> handle | |
| -> forallInput | A symbolic value. All the symbolic constants in the value are treated as for-all variables. |
| -> CEGISCondition | |
| -> IO ([Model], CEGISResult SolvingFailure) | First output are the counter-examples for all the for-all variables, and the second output is the model for all other variables if CEGIS succeeds. |
CEGIS with a single symbolic input to represent a set of inputs. See
cegisForAll for more details.
The difference from cegisForAll is that this function accepts two solver
handles, one for the synthesizer and one for the verifier.
The synthesizer solver will **not** be reset, while the verifier solver will be reset after each iteration.
solverCegisForAllExcept :: (UnionWithExcept t u e v, PlainUnion u, Functor u, EvalSym inputs, ExtractSym inputs, Solver handle, SymEq inputs) => handle -> handle -> inputs -> (Either e v -> CEGISCondition) -> t -> IO ([Model], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, with a forall variable.
See cegisForAllExcept, cegisForAll and cegisExcept.
The difference from cegisForAllExcept is that this function accepts two
solver handles, one for the synthesizer and one for the verifier.
The synthesizer solver will **not** be reset, while the verifier solver will be reset after each iteration.
solverCegisForAllExceptStdVC :: (UnionWithExcept t u VerificationConditions (), PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, Solver handle, SymEq inputs) => handle -> handle -> inputs -> t -> IO ([Model], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, with a forall variable.
See cegisForAllExceptStdVC cegisForAll and cegisExceptStdVC.
The difference from cegisForAllExceptStdVC is that this function accepts
two solver handles, one for the synthesizer and one for the verifier.
The synthesizer solver will **not** be reset, while the verifier solver will be reset after each iteration.
solverCegisForAllExceptVC :: (UnionWithExcept t u e v, PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, Solver handle, SymEq inputs) => handle -> handle -> inputs -> (Either e v -> u (Either VerificationConditions ())) -> t -> IO ([Model], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, with a forall variable.
See cegisForAllExceptVC cegisForAll and cegisExceptVC.
The difference from cegisForAllExceptVC is that this function accepts two
solver handles, one for the synthesizer and one for the verifier.
The synthesizer solver will **not** be reset, while the verifier solver will be reset after each iteration.
cegisPostCond :: SymBool -> CEGISCondition Source #
Construct a CEGIS condition with only a post-condition. The pre-condition would be set to true, meaning that all programs in the program space are allowed.
cegisPrePost :: SymBool -> SymBool -> CEGISCondition Source #
Construct a CEGIS condition with both pre- and post-conditions.
Arguments
| :: (EvalSym input, ExtractSym input, ConfigurableSolver config handle) | |
| => config | The configuration of the solver |
| -> [input] | Initial symbolic inputs. The solver will try to find a
program that works on all the inputs representable by these inputs (see
|
| -> (input -> CEGISCondition) | The condition for the solver to solve. All the symbolic constants that are not in the inputs will be considered as part of the symbolic program. |
| -> IO ([input], CEGISResult SolvingFailure) | The counter-examples generated during the CEGIS loop, and the model found by the solver. |
CEGIS with multiple (possibly symbolic) inputs. Solves the following formula
(see CEGISCondition for details).
\[ \forall P. (\exists I\in\mathrm{inputs}. \mathrm{pre}(P, I)) \wedge (\forall I\in\mathrm{inputs}. \mathrm{pre}(P, I)\implies \mathrm{post}(P, I)) \]
For simpler queries, where the inputs are representable by a single
symbolic value, you may want to use cegis or cegisExcept instead.
We have an example for the cegis call.
Arguments
| :: (ConfigurableSolver config handle, EvalSym inputs, ExtractSym inputs, SymEq inputs) | |
| => config | The configuration of the solver |
| -> inputs | Initial symbolic inputs. The solver will try to find a
program that works on all the inputs representable by it (see
|
| -> (inputs -> CEGISCondition) | The condition for the solver to solve. All the symbolic constants that are not in the inputs will be considered as part of the symbolic program. |
| -> IO ([inputs], CEGISResult SolvingFailure) | The counter-examples generated during the CEGIS loop, and the model found by the solver. |
CEGIS with a single symbolic input to represent a set of inputs.
The following example tries to find the value of c such that for all
positive x, x * c && c -2. The c .> -2 clause is used to make
the solution unique.
>>>let [x,c] = ["x","c"] :: [SymInteger]>>>cegis z3 x (\x -> cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2))(...,CEGISSuccess (Model {c -> -1 :: Integer}))
cegisExcept :: (UnionWithExcept t u e v, PlainUnion u, Functor u, EvalSym inputs, ExtractSym inputs, ConfigurableSolver config handle, SymEq inputs) => config -> inputs -> (Either e v -> CEGISCondition) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, using a single symbolic input to represent a set of inputs.
cegisExcept is particularly useful when custom error types are used.
With cegisExcept, you define how the errors are interpreted to the
CEGIS conditions after the symbolic evaluation. This could increase the
readability and modularity of the code.
The following example tries to find the value of c such that for all
positive x, x * c && c -2. The c .> -2 assertion is used to make
the solution unique.
>>>let [x,c] = ["x","c"] :: [SymInteger]>>>import Control.Monad.Except>>>:{res :: SymInteger -> ExceptT VerificationConditions Union () res x = do symAssume $ x .> 0 symAssert $ x * c .< 0 symAssert $ c .> -2 :}
>>>:{translation (Left AssumptionViolation) = cegisPrePost (con False) (con True) translation (Left AssertionViolation) = cegisPostCond (con False) translation _ = cegisPostCond (con True) :}
>>>cegisExcept z3 x translation res([...],CEGISSuccess (Model {c -> -1 :: Integer}))
cegisExceptStdVC :: (UnionWithExcept t u VerificationConditions (), PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, ConfigurableSolver config handle, SymEq inputs) => config -> inputs -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, using a single symbolic
input to represent a set of inputs. This function saves the efforts to
implement the translation function for the standard error type
VerificationConditions, and the standard result type ().
This function translates assumption violations to failed pre-conditions,
and translates assertion violations to failed post-conditions.
The () result will not fail any conditions.
The following example tries to find the value of c such that for all
positive x, x * c && c -2. The c .> -2 assertion is used to make
the solution unique.
>>>let [x,c] = ["x","c"] :: [SymInteger]>>>import Control.Monad.Except>>>:{res :: SymInteger -> ExceptT VerificationConditions Union () res x = do symAssume $ x .> 0 symAssert $ x * c .< 0 symAssert $ c .> -2 :}
>>>cegisExceptStdVC z3 x res([...],CEGISSuccess (Model {c -> -1 :: Integer}))
cegisExceptVC :: (UnionWithExcept t u e v, PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, ConfigurableSolver config handle, SymEq inputs) => config -> inputs -> (Either e v -> u (Either VerificationConditions ())) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, using a single symbolic input to represent a set of inputs.
The errors should be translated to assertion or assumption violations.
cegisExceptMultiInputs :: (ConfigurableSolver config handle, EvalSym inputs, ExtractSym inputs, UnionWithExcept t u e v, PlainUnion u, Monad u) => config -> [inputs] -> (Either e v -> CEGISCondition) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, using multiple (possibly symbolic) inputs to represent a set of inputs.
cegisExceptStdVCMultiInputs :: (ConfigurableSolver config handle, EvalSym inputs, ExtractSym inputs, UnionWithExcept t u VerificationConditions (), PlainUnion u, Monad u) => config -> [inputs] -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, using multiple (possibly
symbolic) inputs to represent a set of inputs. This function saves the
efforts to implement the translation function for the standard error type
VerificationConditions, and the standard result type ().
This function translates assumption violations to failed pre-conditions,
and translates assertion violations to failed post-conditions.
The () result will not fail any conditions.
cegisExceptVCMultiInputs :: (ConfigurableSolver config handle, EvalSym inputs, ExtractSym inputs, UnionWithExcept t u e v, PlainUnion u, Monad u) => config -> [inputs] -> (Either e v -> u (Either VerificationConditions ())) -> (inputs -> t) -> IO ([inputs], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, using multiple (possibly symbolic) inputs to represent a set of inputs.
The errors should be translated to assertion or assumption violations.
Arguments
| :: (ExtractSym forallInput, ConfigurableSolver config handle) | |
| => config | |
| -> forallInput | A symbolic value. All the symbolic constants in the value are treated as for-all variables. |
| -> CEGISCondition | |
| -> IO ([Model], CEGISResult SolvingFailure) | First output are the counter-examples for all the for-all variables, and the second output is the model for all other variables if CEGIS succeeds. |
CEGIS with a single symbolic input to represent a set of inputs.
The following example tries to find the value of c such that for all
positive x, x * c && c -2. The c .> -2 clause is used to make
the solution unique.
>>>let [x,c] = ["x","c"] :: [SymInteger]>>>cegisForAll z3 x $ cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2)(...,CEGISSuccess (Model {c -> -1 :: Integer}))
cegisForAllExcept :: (UnionWithExcept t u e v, PlainUnion u, Functor u, EvalSym inputs, ExtractSym inputs, ConfigurableSolver config handle, SymEq inputs) => config -> inputs -> (Either e v -> CEGISCondition) -> t -> IO ([Model], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, with a forall variable.
See cegisForAll and cegisExcept.
cegisForAllExceptStdVC :: (UnionWithExcept t u VerificationConditions (), PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, ConfigurableSolver config handle, SymEq inputs) => config -> inputs -> t -> IO ([Model], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, with a forall variable.
See cegisForAll and cegisExceptStdVC.
cegisForAllExceptVC :: (UnionWithExcept t u e v, PlainUnion u, Monad u, EvalSym inputs, ExtractSym inputs, ConfigurableSolver config handle, SymEq inputs) => config -> inputs -> (Either e v -> u (Either VerificationConditions ())) -> t -> IO ([Model], CEGISResult SolvingFailure) Source #
CEGIS for symbolic programs with error handling, with a forall variable.
See cegisForAll and cegisExceptVC.
Substitutions for symbolic values given solver models
Symbolic constant extraction
class Monoid symbolSet => SymbolSetOps symbolSet (typedSymbol :: Type -> Type) | symbolSet -> typedSymbol where Source #
The operations on symbolic constant sets
Note that symbolic constants with different types are considered different.
>>>let aBool = "a" :: TypedAnySymbol Bool>>>let bBool = "b" :: TypedAnySymbol Bool>>>let cBool = "c" :: TypedAnySymbol Bool>>>let aInteger = "a" :: TypedAnySymbol Integer>>>emptySet :: AnySymbolSetSymbolSet {}>>>containsSymbol aBool (buildSymbolSet aBool :: AnySymbolSet)True>>>containsSymbol bBool (buildSymbolSet aBool :: AnySymbolSet)False>>>insertSymbol aBool (buildSymbolSet aBool :: AnySymbolSet)SymbolSet {a :: Bool}>>>insertSymbol aInteger (buildSymbolSet aBool :: AnySymbolSet)SymbolSet {a :: Bool, a :: Integer}>>>let abSet = buildSymbolSet (aBool, bBool) :: AnySymbolSet>>>let acSet = buildSymbolSet (aBool, cBool) :: AnySymbolSet>>>intersectionSet abSet acSetSymbolSet {a :: Bool}>>>unionSet abSet acSetSymbolSet {a :: Bool, b :: Bool, c :: Bool}>>>differenceSet abSet acSetSymbolSet {b :: Bool}
Methods
emptySet :: symbolSet Source #
Construct an empty set
isEmptySet :: symbolSet -> Bool Source #
Check if the set is empty
containsSymbol :: forall a. typedSymbol a -> symbolSet -> Bool Source #
Check if the set contains the given symbol
insertSymbol :: forall a. typedSymbol a -> symbolSet -> symbolSet Source #
Insert a symbol into the set
intersectionSet :: symbolSet -> symbolSet -> symbolSet Source #
Set intersection
unionSet :: symbolSet -> symbolSet -> symbolSet Source #
Set union
differenceSet :: symbolSet -> symbolSet -> symbolSet Source #
Set difference
Instances
| SymbolSetOps (SymbolSet knd) (TypedSymbol knd) Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Model Methods emptySet :: SymbolSet knd Source # isEmptySet :: SymbolSet knd -> Bool Source # containsSymbol :: TypedSymbol knd a -> SymbolSet knd -> Bool Source # insertSymbol :: TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd Source # intersectionSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd Source # unionSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd Source # differenceSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd Source # | |
class SymbolSetOps symbolSet typedSymbol => SymbolSetRep rep symbolSet (typedSymbol :: Type -> Type) where Source #
A type class for building a symbolic constant set manually from a symbolic constant set representation
>>>buildSymbolSet ("a" :: TypedAnySymbol Bool, "b" :: TypedAnySymbol Bool) :: AnySymbolSetSymbolSet {a :: Bool, b :: Bool}
Instances
class ExtractSym a where Source #
Extracts all the symbols (symbolic constants) that are transitively contained in the given value.
>>>extractSym ("a" :: SymBool)SymbolSet {a :: Bool}
>>>extractSym (mrgIf "a" (mrgReturn ["b"]) (mrgReturn ["c", "d"]) :: Union [SymBool])SymbolSet {a :: Bool, b :: Bool, c :: Bool, d :: Bool}
Note 1: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving ExtractSym via (Default X)
Minimal complete definition
Methods
extractSym :: a -> AnySymbolSet Source #
extractSymMaybe :: IsSymbolKind knd => a -> Maybe (SymbolSet knd) Source #
Instances
class (forall a. ExtractSym a => ExtractSym (f a)) => ExtractSym1 f where Source #
Lifting of ExtractSym to unary type constructors.
Methods
liftExtractSymMaybe :: IsSymbolKind knd => (a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd) Source #
Lifts the extractSymMaybe function to unary type constructors.
Instances
extractSym1 :: (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) => f a -> SymbolSet knd Source #
Lift the standard extractSym to unary type constructors.
extractSymMaybe1 :: (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) => f a -> Maybe (SymbolSet knd) Source #
Lift the standard extractSymMaybe to unary type constructors.
class (forall a. ExtractSym a => ExtractSym1 (f a)) => ExtractSym2 f where Source #
Lifting of ExtractSym to binary type constructors.
Methods
liftExtractSymMaybe2 :: IsSymbolKind knd => (a -> Maybe (SymbolSet knd)) -> (b -> Maybe (SymbolSet knd)) -> f a b -> Maybe (SymbolSet knd) Source #
Lifts the extractSymMaybe function to binary type constructors.
Instances
extractSym2 :: (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) => f a b -> SymbolSet knd Source #
Lift the standard extractSym to binary type constructors.
extractSymMaybe2 :: (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) => f a b -> Maybe (SymbolSet knd) Source #
Lift the standard extractSymMaybe to binary type constructors.
Evaluation with a model
When given a satisfiable formula, a solver can return a model that specifies the concrete assignments of the variables in the formula to make the formula true. We can use this model to evaluate some symbolic values by substituting the symbolic constants with the concrete assignments.
class SymbolSetOps symbolSet typedSymbol => ModelOps model symbolSet typedSymbol | model -> symbolSet typedSymbol where Source #
The operations on Models.
Note that symbolic constants with different types are considered different.
>>>let aBool = "a" :: TypedAnySymbol Bool>>>let bBool = "b" :: TypedAnySymbol Bool>>>let cBool = "c" :: TypedAnySymbol Bool>>>let aInteger = "a" :: TypedAnySymbol Integer>>>emptyModel :: ModelModel {}>>>valueOf aBool (buildModel (aBool ::= True) :: Model)Just True>>>valueOf bBool (buildModel (aBool ::= True) :: Model)Nothing>>>insertValue bBool False (buildModel (aBool ::= True) :: Model)Model {a -> True :: Bool, b -> False :: Bool}>>>let abModel = buildModel (aBool ::= True, bBool ::= False) :: Model>>>let acSet = buildSymbolSet (aBool, cBool) :: AnySymbolSet>>>exceptFor acSet abModelModel {b -> False :: Bool}>>>restrictTo acSet abModelModel {a -> True :: Bool}>>>extendTo acSet abModelModel {a -> True :: Bool, b -> False :: Bool, c -> False :: Bool}>>>exact acSet abModelModel {a -> True :: Bool, c -> False :: Bool}
Minimal complete definition
emptyModel, isEmptyModel, modelContains, valueOf, insertValue, exceptFor, exceptFor', restrictTo, extendTo
Methods
emptyModel :: model Source #
Construct an empty model
isEmptyModel :: model -> Bool Source #
Check if the model is empty
modelContains :: typedSymbol a -> model -> Bool Source #
Check if the model contains the given symbol
valueOf :: typedSymbol t -> model -> Maybe t Source #
Extract the assigned value for a given symbolic constant
insertValue :: typedSymbol t -> t -> model -> model Source #
Insert an assignment into the model
exceptFor :: symbolSet -> model -> model Source #
Returns a model that removed all the assignments for the symbolic constants in the set
exceptFor' :: typedSymbol t -> model -> model Source #
Returns a model that removed the assignments for the symbolic constants
restrictTo :: symbolSet -> model -> model Source #
Returns a model that only keeps the assignments for the symbolic constants in the set
extendTo :: symbolSet -> model -> model Source #
Returns a model that extends the assignments for the symbolic constants in the set by assigning default values to them
exact :: symbolSet -> model -> model Source #
Returns a model that contains the assignments for exactly the symbolic constants in the set by removing assignments for the symbolic constants that are not in the set and add assignments for the missing symbolic constants by assigning default values to them.
Instances
| ModelOps Model AnySymbolSet TypedAnySymbol Source # | |
Defined in Grisette.Internal.SymPrim.Prim.Model Methods emptyModel :: Model Source # isEmptyModel :: Model -> Bool Source # modelContains :: TypedAnySymbol a -> Model -> Bool Source # valueOf :: TypedAnySymbol t -> Model -> Maybe t Source # insertValue :: TypedAnySymbol t -> t -> Model -> Model Source # exceptFor :: AnySymbolSet -> Model -> Model Source # exceptFor' :: TypedAnySymbol t -> Model -> Model Source # restrictTo :: AnySymbolSet -> Model -> Model Source # | |
class ModelRep rep model | rep -> model where Source #
A type class for building a model manually from a model representation
Methods
buildModel :: rep -> model Source #
Build a model
>>>let aBool = "a" :: TypedAnySymbol Bool>>>let bBool = "b" :: TypedAnySymbol Bool>>>buildModel (aBool ::= True, bBool ::= False) :: ModelModel {a -> True :: Bool, b -> False :: Bool}
Instances
class EvalSym a where Source #
Evaluating symbolic values with some model. This would substitute the symbols (symbolic constants) with the values in the model.
>>>let model = insertValue "a" (1 :: Integer) emptyModel :: Model>>>evalSym False model ([ssym "a", ssym "b"] :: [SymInteger])[1,b]
If we set the first argument true, the missing symbols will be filled in with some default values:
>>>evalSym True model ([ssym "a", ssym "b"] :: [SymInteger])[1,0]
Note 1: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving EvalSym via (Default X)
Methods
evalSym :: Bool -> Model -> a -> a Source #
Evaluate a symbolic value with some model, possibly fill in values for the missing symbols.
Instances
evalSymToCon :: (ToCon a b, EvalSym a) => Model -> a -> b Source #
Evaluate a symbolic value with some model, fill in values for the missing symbols, and convert the result to a concrete value.
>>>let model = insertValue "a" (1 :: Integer) emptyModel :: Model>>>evalSymToCon model ([ssym "a", ssym "b"] :: [SymInteger]) :: [Integer][1,0]
class (forall a. EvalSym a => EvalSym (f a)) => EvalSym1 f where Source #
Lifting of EvalSym to unary type constructors.
Methods
liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a Source #
Lift the evalSym function to unary type constructors.
Instances
evalSym1 :: (EvalSym1 f, EvalSym a) => Bool -> Model -> f a -> f a Source #
Lifting the standard evalSym to unary type constructors.
evalSymToCon1 :: (EvalSym1 f, EvalSym a, ToCon1 f g, ToCon a b) => Model -> f a -> g b Source #
Evaluate and convert to concrete values with lifted standard evalSym for
unary type constructors. See evalSymToCon.
class (forall a. EvalSym a => EvalSym1 (f a)) => EvalSym2 f where Source #
Lifting of EvalSym1 to binary type constructors.
Methods
liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> f a b -> f a b Source #
Lift the evalSym function to binary type constructors.
Instances
| EvalSym2 Either Source # | |
| EvalSym2 (,) Source # | |
Defined in Grisette.Internal.Core.Data.Class.EvalSym | |
| EvalSym a => EvalSym2 ((,,) a) Source # | |
Defined in Grisette.Internal.Core.Data.Class.EvalSym | |
| (EvalSym a, EvalSym b) => EvalSym2 ((,,,) a b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.EvalSym | |
evalSym2 :: (EvalSym2 f, EvalSym a, EvalSym b) => Bool -> Model -> f a b -> f a b Source #
Lifting the standard evalSym to binary type constructors.
evalSymToCon2 :: (EvalSym2 f, EvalSym a, EvalSym c, ToCon2 f g, ToCon a b, ToCon c d) => Model -> f a c -> g b d Source #
Evaluate and convert to concrete values with lifted standard evalSym for
binary type constructors. See evalSymToCon.
Substitution of a symbol
class SubstSym a where Source #
Substitution of symbols (symbolic constants) to a symbolic value.
>>>a = "a" :: TypedAnySymbol Bool>>>v = "x" .&& "y" :: SymBool>>>substSym a v (["a" .&& "b", "a"] :: [SymBool])[(&& (&& x y) b),(&& x y)]
Note 1: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving SubstSym via (Default X)
Methods
substSym :: (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> a -> a Source #
Instances
class (forall a. SubstSym a => SubstSym (f a)) => SubstSym1 f where Source #
Lifting of SubstSym to unary type constructors.
Methods
liftSubstSym :: (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> f a -> f a Source #
Lift a symbol substitution function to unary type constructors.
Instances
| SubstSym1 Identity Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Identity a -> Identity a Source # | |
| SubstSym1 First Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> First a -> First a Source # | |
| SubstSym1 Last Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Last a -> Last a Source # | |
| SubstSym1 Down Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Down a -> Down a Source # | |
| SubstSym1 Dual Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Dual a -> Dual a Source # | |
| SubstSym1 Product Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Product a -> Product a Source # | |
| SubstSym1 Sum Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Sum a -> Sum a Source # | |
| SubstSym1 Union Source # | |
Defined in Grisette.Internal.Core.Control.Monad.Union Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Union a -> Union a Source # | |
| SubstSym1 Maybe Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Maybe a -> Maybe a Source # | |
| SubstSym1 List Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> [a] -> [a] Source # | |
| SubstSym a => SubstSym1 (Either a) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> Either a a0 -> Either a a0 Source # | |
| (Generic1 f, GSubstSym Arity1 (Rep1 f)) => SubstSym1 (Default1 f) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Default1 f a -> Default1 f a Source # | |
| SubstSym1 m => SubstSym1 (MaybeT m) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> MaybeT m a -> MaybeT m a Source # | |
| SubstSym a => SubstSym1 ((,) a) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, a0) -> (a, a0) Source # | |
| SubstSym a => SubstSym1 (Const a :: Type -> Type) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> Const a a0 -> Const a a0 Source # | |
| SubstSym1 f => SubstSym1 (Ap f) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Ap f a -> Ap f a Source # | |
| SubstSym1 f => SubstSym1 (Alt f) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Alt f a -> Alt f a Source # | |
| (SubstSym1 m, SubstSym e) => SubstSym1 (ExceptT e m) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> ExceptT e m a -> ExceptT e m a Source # | |
| SubstSym1 m => SubstSym1 (IdentityT m) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> IdentityT m a -> IdentityT m a Source # | |
| (SubstSym1 m, SubstSym s) => SubstSym1 (WriterT s m) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> WriterT s m a -> WriterT s m a Source # | |
| (SubstSym1 m, SubstSym s) => SubstSym1 (WriterT s m) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> WriterT s m a -> WriterT s m a Source # | |
| (SubstSym a, SubstSym b) => SubstSym1 ((,,) a b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, b, a0) -> (a, b, a0) Source # | |
| (SubstSym1 l, SubstSym1 r) => SubstSym1 (Product l r) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Product l r a -> Product l r a Source # | |
| (SubstSym1 l, SubstSym1 r) => SubstSym1 (Sum l r) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Sum l r a -> Sum l r a Source # | |
| (SubstSym a, SubstSym b, SubstSym c) => SubstSym1 ((,,,) a b c) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, b, c, a0) -> (a, b, c, a0) Source # | |
| (SubstSym1 f, SubstSym1 g) => SubstSym1 (Compose f g) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> Compose f g a -> Compose f g a Source # | |
| (SubstSym a, SubstSym b, SubstSym c, SubstSym d) => SubstSym1 ((,,,,) a b c d) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, b, c, d, a0) -> (a, b, c, d, a0) Source # | |
| (SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e) => SubstSym1 ((,,,,,) a b c d e) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, b, c, d, e, a0) -> (a, b, c, d, e, a0) Source # | |
| (SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f) => SubstSym1 ((,,,,,,) a b c d e f) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, b, c, d, e, f, a0) -> (a, b, c, d, e, f, a0) Source # | |
| (SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g) => SubstSym1 ((,,,,,,,) a b c d e f g) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, b, c, d, e, f, g, a0) -> (a, b, c, d, e, f, g, a0) Source # | |
| (SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h) => SubstSym1 ((,,,,,,,,) a b c d e f g h) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, b, c, d, e, f, g, h, a0) -> (a, b, c, d, e, f, g, h, a0) Source # | |
| (SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i) => SubstSym1 ((,,,,,,,,,) a b c d e f g h i) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, b, c, d, e, f, g, h, i, a0) -> (a, b, c, d, e, f, g, h, i, a0) Source # | |
| (SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j) => SubstSym1 ((,,,,,,,,,,) a b c d e f g h i j) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, b, c, d, e, f, g, h, i, j, a0) -> (a, b, c, d, e, f, g, h, i, j, a0) Source # | |
| (SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j, SubstSym k) => SubstSym1 ((,,,,,,,,,,,) a b c d e f g h i j k) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, b, c, d, e, f, g, h, i, j, k, a0) -> (a, b, c, d, e, f, g, h, i, j, k, a0) Source # | |
| (SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j, SubstSym k, SubstSym l) => SubstSym1 ((,,,,,,,,,,,,) a b c d e f g h i j k l) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, b, c, d, e, f, g, h, i, j, k, l, a0) -> (a, b, c, d, e, f, g, h, i, j, k, l, a0) Source # | |
| (SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j, SubstSym k, SubstSym l, SubstSym m) => SubstSym1 ((,,,,,,,,,,,,,) a b c d e f g h i j k l m) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, b, c, d, e, f, g, h, i, j, k, l, m, a0) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, a0) Source # | |
| (SubstSym a, SubstSym b, SubstSym c, SubstSym d, SubstSym e, SubstSym f, SubstSym g, SubstSym h, SubstSym i, SubstSym j, SubstSym k, SubstSym l, SubstSym m, SubstSym n) => SubstSym1 ((,,,,,,,,,,,,,,) a b c d e f g h i j k l m n) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym :: forall cb sb (knd :: SymbolKind) a0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> TypedSymbol knd cb -> sb -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n, a0) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n, a0) Source # | |
substSym1 :: (SubstSym1 f, SubstSym a, LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> f a -> f a Source #
Lifting the standard substSym to unary type constructors.
class (forall a. SubstSym a => SubstSym1 (f a)) => SubstSym2 f where Source #
Lifting of SubstSym to binary type constructors.
Methods
liftSubstSym2 :: (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> f a b -> f a b Source #
Lift a symbol substitution function to binary type constructors.
Instances
| SubstSym2 Either Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> Either a b -> Either a b Source # | |
| SubstSym2 (,) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a, b) -> (a, b) Source # | |
| SubstSym a => SubstSym2 ((,,) a) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a0 b. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> (TypedSymbol knd cb -> sb -> b -> b) -> TypedSymbol knd cb -> sb -> (a, a0, b) -> (a, a0, b) Source # | |
| (SubstSym a, SubstSym b) => SubstSym2 ((,,,) a b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym Methods liftSubstSym2 :: forall cb sb (knd :: SymbolKind) a0 b0. (LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a0 -> a0) -> (TypedSymbol knd cb -> sb -> b0 -> b0) -> TypedSymbol knd cb -> sb -> (a, b, a0, b0) -> (a, b, a0, b0) Source # | |
substSym2 :: (SubstSym2 f, SubstSym a, SubstSym b, LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> f a b -> f a b Source #
Lifting the standard substSym to binary type constructors.
Utilities
Memoization
htmemo :: (Eq k, Hashable k) => (k -> a) -> k -> a Source #
Function memoizer with mutable hash table.
htmemo2 :: (Eq k1, Hashable k1, Eq k2, Hashable k2) => (k1 -> k2 -> a) -> k1 -> k2 -> a Source #
Function memoizer with mutable hash table. Works on binary functions.
htmemo3 :: (Eq k1, Hashable k1, Eq k2, Hashable k2, Eq k3, Hashable k3) => (k1 -> k2 -> k3 -> a) -> k1 -> k2 -> k3 -> a Source #
Function memoizer with mutable hash table. Works on ternary functions.
htmup :: (Eq k, Hashable k) => (b -> c) -> (k -> b) -> k -> c Source #
Lift a memoizer to work with one more argument.
htmemoFix :: (Eq k, Hashable k) => ((k -> a) -> k -> a) -> k -> a Source #
Memoizing recursion. Use like fix.
Generic deriving of classes
Default wrappers
This newtype wrapper can be used to derive default instances for
classes taking an argument of kind Type.
Instances
newtype Default1 (f :: Type -> Type) a #
This newtype wrapper can be used to derive default instances for
classes taking an argument of kind Type -> Type
Constructors
| Default1 | |
Fields
| |
Instances
SymEq
data family SymEqArgs arity a b :: Type Source #
The arguments to the generic equality function.
Instances
| data SymEqArgs Arity0 _ _1 Source # | |
Defined in Grisette.Internal.Core.Data.Class.SymEq | |
| newtype SymEqArgs Arity1 a b Source # | |
Defined in Grisette.Internal.Core.Data.Class.SymEq | |
class GSymEq arity f where Source #
The class of types that can be generically compared for symbolic equality.
Instances
| GSymEq Arity1 Par1 Source # | |
| GSymEq arity (U1 :: Type -> Type) Source # | |
| GSymEq arity (V1 :: Type -> Type) Source # | |
| SymEq1 f => GSymEq Arity1 (Rec1 f) Source # | |
| (GSymEq arity a, GSymEq arity b) => GSymEq arity (a :*: b) Source # | |
| (GSymEq arity a, GSymEq arity b) => GSymEq arity (a :+: b) Source # | |
| SymEq a => GSymEq arity (K1 i a :: Type -> Type) Source # | |
| (SymEq1 f, GSymEq Arity1 g) => GSymEq Arity1 (f :.: g) Source # | |
| GSymEq arity a => GSymEq arity (M1 i c a) Source # | |
genericSymEq :: (Generic a, GSymEq Arity0 (Rep a)) => a -> a -> SymBool Source #
Generic ( function..==)
genericLiftSymEq :: (Generic1 f, GSymEq Arity1 (Rep1 f)) => (a -> b -> SymBool) -> f a -> f b -> SymBool Source #
Generic liftSymEq function.
SymOrd
data family SymOrdArgs arity a b :: Type Source #
The arguments to the generic comparison function.
Instances
| data SymOrdArgs Arity0 _ _1 Source # | |
Defined in Grisette.Internal.Core.Data.Class.SymOrd | |
| newtype SymOrdArgs Arity1 a b Source # | |
Defined in Grisette.Internal.Core.Data.Class.SymOrd | |
class GSymOrd arity f where Source #
The class of types that can be generically symbolically compared.
Methods
gsymCompare :: SymOrdArgs arity a b -> f a -> f b -> Union Ordering Source #
Instances
genericSymCompare :: (Generic a, GSymOrd Arity0 (Rep a)) => a -> a -> Union Ordering Source #
Generic symCompare function.
genericLiftSymCompare :: (Generic1 f, GSymOrd Arity1 (Rep1 f)) => (a -> b -> Union Ordering) -> f a -> f b -> Union Ordering Source #
Generic liftSymCompare function.
Mergeable
data family MergeableArgs arity a :: Type Source #
The arguments to the generic merging strategy function.
Instances
| data MergeableArgs Arity0 _ Source # | |
Defined in Grisette.Internal.Core.Data.Class.Mergeable | |
| newtype MergeableArgs Arity1 a Source # | |
Defined in Grisette.Internal.Core.Data.Class.Mergeable | |
class GMergeable arity f where Source #
The class of types that can be generically merged.
Methods
grootStrategy :: MergeableArgs arity a -> MergingStrategy (f a) Source #
Instances
genericRootStrategy :: (Generic a, GMergeable Arity0 (Rep a)) => MergingStrategy a Source #
Generic rootStrategy.
genericLiftRootStrategy :: (Generic1 f, GMergeable Arity1 (Rep1 f)) => MergingStrategy a -> MergingStrategy (f a) Source #
Generic liftRootStrategy.
SimpleMergeable
data family SimpleMergeableArgs arity a :: Type Source #
The arguments to the generic simple merging function.
Instances
| data SimpleMergeableArgs Arity0 _ Source # | |
| newtype SimpleMergeableArgs Arity1 a Source # | |
class GSimpleMergeable arity f where Source #
Generic SimpleMergeable class.
Methods
gmrgIte :: SimpleMergeableArgs arity a -> SymBool -> f a -> f a -> f a Source #
Instances
| GSimpleMergeable Arity1 Par1 Source # | |
| GSimpleMergeable arity (U1 :: Type -> Type) Source # | |
| GSimpleMergeable arity (V1 :: Type -> Type) Source # | |
| SimpleMergeable1 f => GSimpleMergeable Arity1 (Rec1 f) Source # | |
| (GSimpleMergeable arity a, GSimpleMergeable arity b) => GSimpleMergeable arity (a :*: b) Source # | |
| SimpleMergeable c => GSimpleMergeable arity (K1 i c :: Type -> Type) Source # | |
| (SimpleMergeable1 f, GSimpleMergeable Arity1 g) => GSimpleMergeable Arity1 (f :.: g) Source # | |
| GSimpleMergeable arity a => GSimpleMergeable arity (M1 i c a) Source # | |
genericMrgIte :: (Generic a, GSimpleMergeable Arity0 (Rep a)) => SymBool -> a -> a -> a Source #
Generic mrgIte function.
genericLiftMrgIte :: (Generic1 f, GSimpleMergeable Arity1 (Rep1 f)) => (SymBool -> a -> a -> a) -> SymBool -> f a -> f a -> f a Source #
Generic liftMrgIte function.
ToCon
data family ToConArgs arity a b :: Type Source #
The arguments to the generic toCon function.
Instances
| data ToConArgs Arity0 _ _1 Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
| newtype ToConArgs Arity1 a b Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToCon | |
class GToCon arity f1 f2 where Source #
The class of types that can be generically converted to concrete values.
Instances
| GToCon Arity1 Par1 Par1 Source # | |
| GToCon arity (U1 :: Type -> Type) (U1 :: Type -> Type) Source # | |
| GToCon arity (V1 :: Type -> Type) (V1 :: Type -> Type) Source # | |
| ToCon1 f1 f2 => GToCon Arity1 (Rec1 f1) (Rec1 f2) Source # | |
| (GToCon arity a b, GToCon arity c d) => GToCon arity (a :*: c) (b :*: d) Source # | |
| (GToCon arity a b, GToCon arity c d) => GToCon arity (a :+: c) (b :+: d) Source # | |
| ToCon a b => GToCon arity (K1 i a :: Type -> Type) (K1 i b :: Type -> Type) Source # | |
| (ToCon1 f1 f2, GToCon Arity1 g1 g2) => GToCon Arity1 (f1 :.: g1) (f2 :.: g2) Source # | |
| GToCon arity a b => GToCon arity (M1 i c1 a) (M1 i c2 b) Source # | |
genericToCon :: (Generic a, Generic b, GToCon Arity0 (Rep a) (Rep b)) => a -> Maybe b Source #
Generic toCon function.
genericLiftToCon :: (Generic1 f1, Generic1 f2, GToCon Arity1 (Rep1 f1) (Rep1 f2)) => (a -> Maybe b) -> f1 a -> Maybe (f2 b) Source #
Generic liftToCon function.
ToSym
data family ToSymArgs arity a b :: Type Source #
The arguments to the generic toSym function.
Instances
| data ToSymArgs Arity0 _ _1 Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| data ToSymArgs Arity1 _ _1 Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
class GToSym arity f1 f2 where Source #
The class of types that can be generically converted to symbolic values.
Instances
| GToSym Arity1 Par1 Par1 Source # | |
| GToSym arity (U1 :: Type -> Type) (U1 :: Type -> Type) Source # | |
| GToSym arity (V1 :: Type -> Type) (V1 :: Type -> Type) Source # | |
| ToSym1 f1 f2 => GToSym Arity1 (Rec1 f1) (Rec1 f2) Source # | |
| (GToSym arity a b, GToSym arity c d) => GToSym arity (a :*: c) (b :*: d) Source # | |
| (GToSym arity a b, GToSym arity c d) => GToSym arity (a :+: c) (b :+: d) Source # | |
| ToSym a b => GToSym arity (K1 i a :: Type -> Type) (K1 i b :: Type -> Type) Source # | |
| (ToSym1 f1 f2, GToSym Arity1 g1 g2, Mergeable1 g2) => GToSym Arity1 (f1 :.: g1) (f2 :.: g2) Source # | |
| GToSym arity f1 f2 => GToSym arity (M1 i c1 f1) (M1 i c2 f2) Source # | |
genericToSym :: (Generic a, Generic b, GToSym Arity0 (Rep a) (Rep b)) => a -> b Source #
Generic toSym function.
genericLiftToSym :: (Generic1 f1, Generic1 f2, GToSym Arity1 (Rep1 f1) (Rep1 f2), Mergeable b) => (a -> b) -> f1 a -> f2 b Source #
Generic liftToSym function.
EvalSym
data family EvalSymArgs arity a :: Type Source #
The arguments to the generic evalSym function.
Instances
| data EvalSymArgs Arity0 _ Source # | |
Defined in Grisette.Internal.Core.Data.Class.EvalSym | |
| newtype EvalSymArgs Arity1 a Source # | |
Defined in Grisette.Internal.Core.Data.Class.EvalSym | |
class GEvalSym arity f where Source #
The class of types that can be generically evaluated.
Instances
| GEvalSym Arity1 Par1 Source # | |
Defined in Grisette.Internal.Core.Data.Class.EvalSym | |
| GEvalSym arity (U1 :: Type -> Type) Source # | |
Defined in Grisette.Internal.Core.Data.Class.EvalSym | |
| GEvalSym arity (V1 :: Type -> Type) Source # | |
Defined in Grisette.Internal.Core.Data.Class.EvalSym | |
| EvalSym1 a => GEvalSym Arity1 (Rec1 a) Source # | |
Defined in Grisette.Internal.Core.Data.Class.EvalSym | |
| (GEvalSym arity a, GEvalSym arity b) => GEvalSym arity (a :*: b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.EvalSym | |
| (GEvalSym arity a, GEvalSym arity b) => GEvalSym arity (a :+: b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.EvalSym | |
| EvalSym a => GEvalSym arity (K1 i a :: Type -> Type) Source # | |
Defined in Grisette.Internal.Core.Data.Class.EvalSym | |
| (EvalSym1 f, GEvalSym Arity1 g) => GEvalSym Arity1 (f :.: g) Source # | |
Defined in Grisette.Internal.Core.Data.Class.EvalSym | |
| GEvalSym arity a => GEvalSym arity (M1 i c a) Source # | |
Defined in Grisette.Internal.Core.Data.Class.EvalSym | |
genericEvalSym :: (Generic a, GEvalSym Arity0 (Rep a)) => Bool -> Model -> a -> a Source #
Generic evalSym function.
genericLiftEvalSym :: (Generic1 f, GEvalSym Arity1 (Rep1 f)) => (Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a Source #
Generic liftEvalSym function.
ExtractSym
data family ExtractSymArgs arity (knd :: SymbolKind) a :: Type Source #
The arguments to the generic extractSym function.
Instances
| data ExtractSymArgs Arity0 _ _1 Source # | |
Defined in Grisette.Internal.Core.Data.Class.ExtractSym | |
| newtype ExtractSymArgs Arity1 knd a Source # | |
Defined in Grisette.Internal.Core.Data.Class.ExtractSym | |
class GExtractSym arity f where Source #
The class of types that can generically extract the symbols.
Methods
gextractSymMaybe :: IsSymbolKind knd => ExtractSymArgs arity knd a -> f a -> Maybe (SymbolSet knd) Source #
Instances
genericExtractSymMaybe :: (Generic a, GExtractSym Arity0 (Rep a), IsSymbolKind knd) => a -> Maybe (SymbolSet knd) Source #
Generic extractSym function.
genericLiftExtractSymMaybe :: (Generic1 f, GExtractSym Arity1 (Rep1 f), IsSymbolKind knd) => (a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd) Source #
Generic liftExtractSymMaybe function.
SubstSym
data family SubstSymArgs arity (knd :: SymbolKind) a cb sb :: Type Source #
The arguments to the generic substSym function.
Instances
| data SubstSymArgs Arity0 _ _1 _2 _3 Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym | |
| newtype SubstSymArgs Arity1 knd a cb sb Source # | |
Defined in Grisette.Internal.Core.Data.Class.SubstSym | |
class GSubstSym arity f where Source #
The class of types where we can generically substitute the symbols in a value.
Methods
gsubstSym :: (LinkedRep cb sb, IsSymbolKind knd) => SubstSymArgs arity knd a cb sb -> TypedSymbol knd cb -> sb -> f a -> f a Source #
Instances
genericSubstSym :: (Generic a, GSubstSym Arity0 (Rep a), LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> a -> a Source #
Generic substSym function.
genericLiftSubstSym :: (Generic1 f, GSubstSym Arity1 (Rep1 f), LinkedRep cb sb, IsSymbolKind knd) => (TypedSymbol knd cb -> sb -> a -> a) -> TypedSymbol knd cb -> sb -> f a -> f a Source #
Generic liftSubstSym function.
PPrint
genericPFormatPrec :: (Generic a, GPPrint Arity0 (Rep a)) => Int -> a -> Doc ann Source #
Generic pformatPrec function.
genericLiftPFormatPrec :: (Generic1 f, GPPrint Arity1 (Rep1 f)) => (Int -> a -> Doc ann) -> ([a] -> Doc ann) -> Int -> f a -> Doc ann Source #
Generic liftPFormatPrec function.
genericPFormatList :: (Generic a, GPPrint Arity0 (Rep a)) => [a] -> Doc ann Source #
Generic pformatList function.
genericLiftPFormatList :: (Generic1 f, GPPrint Arity1 (Rep1 f)) => (Int -> a -> Doc ann) -> ([a] -> Doc ann) -> [f a] -> Doc ann Source #
Generic liftPFormatList function.
data family PPrintArgs arity a ann :: Type Source #
The arguments to the generic PPrint class.
Instances
| data PPrintArgs Arity0 _ _1 Source # | |
Defined in Grisette.Internal.Core.Data.Class.PPrint | |
| data PPrintArgs Arity1 a ann Source # | |
Defined in Grisette.Internal.Core.Data.Class.PPrint | |
class GPPrint arity f where Source #
Generic PPrint class.
Minimal complete definition
Methods
gpformatPrec :: PPrintArgs arity a ann -> PPrintType -> Int -> f a -> Doc ann Source #
gpformatList :: HasCallStack => PPrintArgs arity a ann -> [f a] -> Doc ann Source #
gisNullary :: HasCallStack => PPrintArgs arity a ann -> f a -> Bool Source #
Instances
data PPrintType Source #
Controls how to pretty-print a generic representation.
Instances
| Show PPrintType Source # | |
Defined in Grisette.Internal.Core.Data.Class.PPrint Methods showsPrec :: Int -> PPrintType -> ShowS # show :: PPrintType -> String # showList :: [PPrintType] -> ShowS # | |
| Eq PPrintType Source # | |
Defined in Grisette.Internal.Core.Data.Class.PPrint | |