| 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 SExpr
- showsSExprWithParens :: Char -> Char -> SExpr -> ShowS
- fileLocation :: SpliceQ SExpr
- data Identifier = Identifier {}
- data Symbol where
- SimpleSymbol :: Identifier -> Symbol
- IndexedSymbol :: Identifier -> Int -> Symbol
- identifier :: Text -> Identifier
- withMetadata :: Text -> SExpr -> Identifier
- mapMetadata :: (SExpr -> SExpr) -> Identifier -> Identifier
- withLocation :: Text -> SpliceQ Identifier
- uniqueIdentifier :: Text -> IO Identifier
- simple :: Identifier -> Symbol
- indexed :: Identifier -> Int -> Symbol
- symbolIdentifier :: Symbol -> Identifier
- mapIdentifier :: (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 => Text -> SpliceQ s
- ilocsym :: Solvable c s => Text -> 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 Bool
- | 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
- stableMemo :: (a -> b) -> a -> b
- stableMemo2 :: (a -> b -> c) -> a -> b -> c
- stableMemo3 :: (a -> b -> c -> d) -> a -> b -> c -> d
- stableMup :: (b -> c) -> (a -> b) -> a -> c
- stableMemoFix :: ((a -> b) -> a -> b) -> a -> b
- weakStableMemo :: (a -> b) -> a -> b
- weakStableMemo2 :: (a -> b -> c) -> a -> b -> c
- weakStableMemo3 :: (a -> b -> c -> d) -> a -> b -> c -> d
- weakStableMup :: (b -> c) -> (a -> b) -> a -> c
- weakStableMemoFix :: ((a -> b) -> a -> b) -> 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
- htmemoFix :: (Eq k, Hashable k) => ((k -> a) -> k -> a) -> k -> a
- htmup :: (Eq k, Hashable k) => (b -> c) -> (k -> b) -> k -> c
- 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
S-expression data type. Used for symbol metadata.
Instances
showsSExprWithParens :: Char -> Char -> SExpr -> ShowS Source #
Show an S-expression with specific parentheses.
fileLocation :: SpliceQ SExpr Source #
Get the file location of the splice.
data Identifier 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 metadata
Identifiers created with different name or different additional information will not be the same.
>>>withMetadata "a" (NumberAtom 1)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.
>>>$$(withLocation "a") -- a sample result could be "a:[grisette-file-location <interactive> 18 (4 18)]"a:[grisette-file-location <interactive>...]
Constructors
| 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.
withMetadata :: Text -> SExpr -> Identifier Source #
Identifier with extra metadata.
The same identifier with the same metadata refers to the same symbolic variable in the whole program.
The user may need to use unique identifiers or additional metadata to avoid unintentional identifier collision.
mapMetadata :: (SExpr -> SExpr) -> Identifier -> Identifier Source #
Modify the metadata of an identifier.
withLocation :: Text -> SpliceQ Identifier Source #
Identifier with the file 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.
mapIdentifier :: (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 => Text -> SpliceQ s Source #
Generate simply-named symbolic variables. The file location will be attached to the identifier.
>>>$$(slocsym "a") :: SymBoola:[grisette-file-location <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 => Text -> Int -> SpliceQ s Source #
Generate indexed symbolic variables. The file location will be attached to the identifier.
>>>$$(ilocsym "a" 1) :: SymBoola:[grisette-file-location <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
| ITEOp SymAlgReal Source # | |
Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymAlgReal -> SymAlgReal -> SymAlgReal Source # | |
| ITEOp SymBool Source # | |
| ITEOp SymFPRoundingMode Source # | |
Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymFPRoundingMode -> SymFPRoundingMode -> SymFPRoundingMode Source # | |
| ITEOp SymInteger Source # | |
Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymInteger -> SymInteger -> SymInteger Source # | |
| ITEOp v => ITEOp (Identity v) Source # | |
| (ITEOp a, Mergeable a) => ITEOp (Union a) Source # | |
| (forall (n :: Nat). (KnownNat n, 1 <= n) => ITEOp (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) => ITEOp (SomeBV bv) Source # | |
| (KnownNat n, 1 <= n) => ITEOp (SymIntN n) Source # | |
| (KnownNat n, 1 <= n) => ITEOp (SymWordN n) Source # | |
| ITEOp (a --> b) Source # | |
| ValidFP eb sb => ITEOp (SymFP eb sb) Source # | |
| ITEOp (sa -~> sb) Source # | |
| ITEOp (sa =~> sb) Source # | |
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.