grisette-0.12.0.0: Symbolic evaluation as a library

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

Grisette.Internal.SymPrim.SymBool

Contents

Orphan instances

Description

Synopsis

newtype SymBool = SymBool (Term Bool)
type SymBoolKey = AsKey SymBool

Documentation

newtype SymBool Source #

Symbolic Boolean type.

>>> "a" :: SymBool
a
>>> "a" .&& "b" :: SymBool
(&& a b)

More operations are available. Please refer to Grisette.Core for more information.

Constructors

SymBool (Term Bool)

Instances

Instances details

Binary SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Methods

put :: SymBool -> Put #

get :: Get SymBool #

putList :: [SymBool] -> Put #

Serial SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Methods

serialize :: MonadPut m => SymBool -> m () #

deserialize :: MonadGet m => m SymBool #

Serialize SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Methods

put :: Putter SymBool #

get :: Get SymBool #

NFData SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Methods

rnf :: SymBool -> () #

IsString SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Methods

fromString :: String -> SymBool #

Generic SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Associated Types

type Rep SymBool
Instance details Defined in Grisette.Internal.SymPrim.SymBool type Rep SymBool = D1 ('MetaData "SymBool" "Grisette.Internal.SymPrim.SymBool" "grisette-0.12.0.0-2G8wsM3ZzbCKYYnSn6PeBx" 'True) (C1 ('MetaCons "SymBool" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingBoolTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term Bool))))

Methods

from :: SymBool -> Rep SymBool x #

to :: Rep SymBool x -> SymBool #

Show SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Methods

showsPrec :: Int -> SymBool -> ShowS #

show :: SymBool -> String #

showList :: [SymBool] -> ShowS #

Eq SymBool Source #

This will crash the program.

SymBool cannot be compared concretely.

If you want to use the type as keys in hash maps based on term equality, say memo table, you should use AsKey SymBool instead.

If you want symbolic version of the equality operator, use SymEq instead.

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Methods

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

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

KeyEq SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Methods

keyEq :: SymBool -> SymBool -> Bool Source #

KeyHashable SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Methods

keyHashWithSalt :: Int -> SymBool -> Int Source #

Apply SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Associated Types

type FunType SymBool
Instance details Defined in Grisette.Internal.SymPrim.SymBool type FunType SymBool = SymBool

Methods

apply :: SymBool -> FunType SymBool Source #

ITEOp SymBool Source #

Instance details

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

Methods

symIte :: SymBool -> SymBool -> SymBool -> SymBool Source #

LogicalOp SymBool Source #

Instance details

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

Methods

true :: SymBool Source #

false :: SymBool Source #

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

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

symNot :: SymBool -> SymBool Source #

symXor :: SymBool -> SymBool -> SymBool Source #

symImplies :: SymBool -> SymBool -> SymBool Source #

EvalSym SymBool Source #

Instance details

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

Methods

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

ExtractSym SymBool Source #

Instance details

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

Methods

extractSym :: SymBool -> AnySymbolSet Source #

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

Mergeable SymBool Source #

Instance details

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

Methods

rootStrategy :: MergingStrategy SymBool Source #

sortIndices :: SymBool -> [DynamicSortedIdx] Source #

PPrint SymBool Source #

Instance details

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

Methods

pformat :: SymBool -> Doc ann Source #

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

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

SimpleMergeable SymBool Source #

Instance details

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

Methods

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

SubstSym SymBool 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 -> SymBool -> SymBool Source #

SymEq SymBool Source #

Instance details

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

Methods

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

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

symDistinct :: [SymBool] -> SymBool Source #

SymOrd SymBool Source #

Instance details

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

Methods

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

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

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

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

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

AllSyms SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Methods

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

allSyms :: SymBool -> [SomeSym] Source #

ConRep SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Associated Types

type ConType SymBool
Instance details Defined in Grisette.Internal.SymPrim.SymBool type ConType SymBool = Bool

UnifiedConRep SymBool Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type ConType SymBool
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type ConType SymBool = Bool

UnifiedSymRep SymBool Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type SymType SymBool
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type SymType SymBool = SymBool

GenSym SymBool SymBool Source #

Instance details

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

Methods

fresh :: MonadFresh m => SymBool -> m (Union SymBool) Source #

GenSym () SymBool Source #

Instance details

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

Methods

fresh :: MonadFresh m => () -> m (Union SymBool) Source #

GenSymSimple SymBool SymBool Source #

Instance details

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

Methods

simpleFresh :: MonadFresh m => SymBool -> m SymBool Source #

GenSymSimple () SymBool Source #

Instance details

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

Methods

simpleFresh :: MonadFresh m => () -> m SymBool Source #

Solvable Bool SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Methods

con :: Bool -> SymBool Source #

conView :: SymBool -> Maybe Bool Source #

sym :: Symbol -> SymBool Source #

ssym :: Identifier -> SymBool Source #

isym :: Identifier -> Int -> SymBool Source #

ToCon SymBool SymBool Source #

Instance details

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

Methods

toCon :: SymBool -> Maybe SymBool Source #

ToCon SymBool Bool Source #

Instance details

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

Methods

toCon :: SymBool -> Maybe Bool Source #

ToSym SymBool SymBool Source #

Instance details

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

Methods

toSym :: SymBool -> SymBool Source #

ToSym Bool SymBool Source #

Instance details

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

Methods

toSym :: Bool -> SymBool Source #

LinkedRep Bool SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Methods

underlyingTerm :: SymBool -> Term Bool Source #

wrapTerm :: Term Bool -> SymBool Source #

Lift SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

Methods

lift :: Quote m => SymBool -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => SymBool -> Code m SymBool #

UnifiedSolvable 'S SymBool Bool Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSolvable

Methods

withBaseSolvable :: (If (IsConMode 'S) (SymBool ~ Bool) (Solvable Bool SymBool) => r) -> r Source #

BitCast SymBool (SymIntN 1) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

bitCast :: SymBool -> SymIntN 1 Source #

BitCast SymBool (SymWordN 1) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

bitCast :: SymBool -> SymWordN 1 Source #

BitCast (SymIntN 1) SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

bitCast :: SymIntN 1 -> SymBool Source #

BitCast (SymWordN 1) SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBV

Methods

bitCast :: SymWordN 1 -> SymBool Source #

ToSym (Union Bool) SymBool Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union

Methods

toSym :: Union Bool -> SymBool Source #

type Rep SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

type Rep SymBool = D1 ('MetaData "SymBool" "Grisette.Internal.SymPrim.SymBool" "grisette-0.12.0.0-2G8wsM3ZzbCKYYnSn6PeBx" 'True) (C1 ('MetaCons "SymBool" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingBoolTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term Bool))))

type FunType SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

type FunType SymBool = SymBool

type ConType SymBool Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymBool

type ConType SymBool = Bool

type ConType SymBool Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type ConType SymBool = Bool

type SymType SymBool Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type SymType SymBool = SymBool

type SymBoolKey = AsKey SymBool Source #

SymBool type with identity equality.

Orphan instances

SymRep Bool Source #

Instance details

Associated Types

type SymType Bool
Instance details Defined in Grisette.Internal.SymPrim.SymBool type SymType Bool = SymBool

LinkedRep Bool SymBool Source #

Instance details

Methods

underlyingTerm :: SymBool -> Term Bool Source #

wrapTerm :: Term Bool -> SymBool Source #