Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Trustworthy
Language	Haskell2010

Grisette.Internal.Core.Control.Exception

Contents

Predefined exceptions

Description

Synopsis

data AssertionError = AssertionError
data VerificationConditions
- = AssertionViolation
- | AssumptionViolation

Predefined exceptions

data AssertionError Source #

Assertion error.

Constructors

AssertionError

Instances

Instances details

NFData AssertionError Source #

Instance details

Defined in Grisette.Internal.Core.Control.Exception

Methods

rnf :: AssertionError -> () #

Generic AssertionError Source #

Instance details

Defined in Grisette.Internal.Core.Control.Exception

Associated Types

type Rep AssertionError
Instance details Defined in Grisette.Internal.Core.Control.Exception type Rep AssertionError = D1 ('MetaData "AssertionError" "Grisette.Internal.Core.Control.Exception" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "AssertionError" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: AssertionError -> Rep AssertionError x #

to :: Rep AssertionError x -> AssertionError #

Show AssertionError Source #

Instance details

Defined in Grisette.Internal.Core.Control.Exception

Methods

showsPrec :: Int -> AssertionError -> ShowS #

show :: AssertionError -> String #

showList :: [AssertionError] -> ShowS #

Eq AssertionError Source #

Instance details

Defined in Grisette.Internal.Core.Control.Exception

Methods

(==) :: AssertionError -> AssertionError -> Bool #

(/=) :: AssertionError -> AssertionError -> Bool #

Ord AssertionError Source #

Instance details

Defined in Grisette.Internal.Core.Control.Exception

Methods

compare :: AssertionError -> AssertionError -> Ordering #

(<) :: AssertionError -> AssertionError -> Bool #

(<=) :: AssertionError -> AssertionError -> Bool #

(>) :: AssertionError -> AssertionError -> Bool #

(>=) :: AssertionError -> AssertionError -> Bool #

max :: AssertionError -> AssertionError -> AssertionError #

min :: AssertionError -> AssertionError -> AssertionError #

EvalSym AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> AssertionError -> AssertionError Source #

ExtractSym AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym

Methods

extractSym :: AssertionError -> AnySymbolSet Source #

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => AssertionError -> Maybe (SymbolSet knd) Source #

Mergeable AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy AssertionError Source #

sortIndices :: AssertionError -> [DynamicSortedIdx] Source #

PPrint AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint

Methods

pformat :: AssertionError -> Doc ann Source #

pformatPrec :: Int -> AssertionError -> Doc ann Source #

pformatList :: [AssertionError] -> Doc ann Source #

SimpleMergeable AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> AssertionError -> AssertionError -> AssertionError Source #

SubstSym AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym

Methods

substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> AssertionError -> AssertionError Source #

SymEq AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq

Methods

(.==) :: AssertionError -> AssertionError -> SymBool Source #

(./=) :: AssertionError -> AssertionError -> SymBool Source #

symDistinct :: [AssertionError] -> SymBool Source #

SymOrd AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd

Methods

(.<) :: AssertionError -> AssertionError -> SymBool Source #

(.<=) :: AssertionError -> AssertionError -> SymBool Source #

(.>) :: AssertionError -> AssertionError -> SymBool Source #

(.>=) :: AssertionError -> AssertionError -> SymBool Source #

symCompare :: AssertionError -> AssertionError -> Union Ordering Source #

AllSyms AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: AssertionError -> [SomeSym] -> [SomeSym] Source #

allSyms :: AssertionError -> [SomeSym] Source #

TransformError ArithException AssertionError Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.Error

Methods

transformError :: ArithException -> AssertionError Source #

TransformError ArrayException AssertionError Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.Error

Methods

transformError :: ArrayException -> AssertionError Source #

TransformError AssertionError AssertionError Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.Error

Methods

transformError :: AssertionError -> AssertionError Source #

TransformError AssertionError VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.Error

Methods

transformError :: AssertionError -> VerificationConditions Source #

ToCon AssertionError AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: AssertionError -> Maybe AssertionError Source #

ToSym AssertionError AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: AssertionError -> AssertionError Source #

DecideEvalMode mode => UnifiedSimpleMergeable mode AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSimpleMergeable

Methods

withBaseSimpleMergeable :: (If (IsConMode mode) () (SimpleMergeable AssertionError) => r) -> r Source #

DecideEvalMode mode => UnifiedSymEq mode AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymEq

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq AssertionError) (SymEq AssertionError) => r) -> r Source #

DecideEvalMode mode => UnifiedSymOrd mode AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymOrd

Methods

withBaseSymOrd :: (If (IsConMode mode) (Ord AssertionError) (SymOrd AssertionError) => r) -> r Source #

ToSym AssertionError (Union AssertionError) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: AssertionError -> Union AssertionError Source #

ToCon (Union AssertionError) AssertionError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: Union AssertionError -> Maybe AssertionError Source #

type Rep AssertionError Source #

Instance details

Defined in Grisette.Internal.Core.Control.Exception

type Rep AssertionError = D1 ('MetaData "AssertionError" "Grisette.Internal.Core.Control.Exception" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "AssertionError" 'PrefixI 'False) (U1 :: Type -> Type))

data VerificationConditions Source #

Verification conditions. A crashed program path can terminate with either assertion violation errors or assumption violation errors.

Constructors

AssertionViolation
AssumptionViolation

Instances

Instances details

NFData VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Core.Control.Exception

Methods

rnf :: VerificationConditions -> () #

Generic VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Core.Control.Exception

Associated Types

type Rep VerificationConditions
Instance details Defined in Grisette.Internal.Core.Control.Exception type Rep VerificationConditions = D1 ('MetaData "VerificationConditions" "Grisette.Internal.Core.Control.Exception" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "AssertionViolation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AssumptionViolation" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: VerificationConditions -> Rep VerificationConditions x #

to :: Rep VerificationConditions x -> VerificationConditions #

Show VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Core.Control.Exception

Methods

showsPrec :: Int -> VerificationConditions -> ShowS #

show :: VerificationConditions -> String #

showList :: [VerificationConditions] -> ShowS #

Eq VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Core.Control.Exception

Methods

(==) :: VerificationConditions -> VerificationConditions -> Bool #

(/=) :: VerificationConditions -> VerificationConditions -> Bool #

Ord VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Core.Control.Exception

Methods

compare :: VerificationConditions -> VerificationConditions -> Ordering #

(<) :: VerificationConditions -> VerificationConditions -> Bool #

(<=) :: VerificationConditions -> VerificationConditions -> Bool #

(>) :: VerificationConditions -> VerificationConditions -> Bool #

(>=) :: VerificationConditions -> VerificationConditions -> Bool #

max :: VerificationConditions -> VerificationConditions -> VerificationConditions #

min :: VerificationConditions -> VerificationConditions -> VerificationConditions #

EvalSym VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> VerificationConditions -> VerificationConditions Source #

ExtractSym VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym

Methods

extractSym :: VerificationConditions -> AnySymbolSet Source #

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => VerificationConditions -> Maybe (SymbolSet knd) Source #

Mergeable VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy VerificationConditions Source #

sortIndices :: VerificationConditions -> [DynamicSortedIdx] Source #

PPrint VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint

Methods

pformat :: VerificationConditions -> Doc ann Source #

pformatPrec :: Int -> VerificationConditions -> Doc ann Source #

pformatList :: [VerificationConditions] -> Doc ann Source #

SubstSym VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym

Methods

substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> VerificationConditions -> VerificationConditions Source #

SymEq VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq

Methods

(.==) :: VerificationConditions -> VerificationConditions -> SymBool Source #

(./=) :: VerificationConditions -> VerificationConditions -> SymBool Source #

symDistinct :: [VerificationConditions] -> SymBool Source #

SymOrd VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd

Methods

(.<) :: VerificationConditions -> VerificationConditions -> SymBool Source #

(.<=) :: VerificationConditions -> VerificationConditions -> SymBool Source #

(.>) :: VerificationConditions -> VerificationConditions -> SymBool Source #

(.>=) :: VerificationConditions -> VerificationConditions -> SymBool Source #

symCompare :: VerificationConditions -> VerificationConditions -> Union Ordering Source #

AllSyms VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: VerificationConditions -> [SomeSym] -> [SomeSym] Source #

allSyms :: VerificationConditions -> [SomeSym] Source #

TransformError AssertionError VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.Error

Methods

transformError :: AssertionError -> VerificationConditions Source #

TransformError VerificationConditions VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.Error

Methods

transformError :: VerificationConditions -> VerificationConditions Source #

ToCon VerificationConditions VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: VerificationConditions -> Maybe VerificationConditions Source #

ToSym VerificationConditions VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: VerificationConditions -> VerificationConditions Source #

DecideEvalMode mode => UnifiedSymEq mode VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymEq

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq VerificationConditions) (SymEq VerificationConditions) => r) -> r Source #

DecideEvalMode mode => UnifiedSymOrd mode VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymOrd

Methods

withBaseSymOrd :: (If (IsConMode mode) (Ord VerificationConditions) (SymOrd VerificationConditions) => r) -> r Source #

ToSym VerificationConditions (Union VerificationConditions) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: VerificationConditions -> Union VerificationConditions Source #

ToCon (Union VerificationConditions) VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: Union VerificationConditions -> Maybe VerificationConditions Source #

type Rep VerificationConditions Source #

Instance details

Defined in Grisette.Internal.Core.Control.Exception

type Rep VerificationConditions = D1 ('MetaData "VerificationConditions" "Grisette.Internal.Core.Control.Exception" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "AssertionViolation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AssumptionViolation" 'PrefixI 'False) (U1 :: Type -> Type))