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	Safe-Inferred
Language	Haskell2010

Grisette.Internal.SymPrim.SymBool

Contents

Orphan instances

Description

Synopsis

newtype SymBool = SymBool (Term Bool)

Documentation

newtype SymBool Source #

Symbolic Boolean type.

>>> :set -XOverloadedStrings
>>> "a" :: SymBool
a
>>> "a" .&& "b" :: SymBool
(&& a b)

More symbolic operations are available. Please refer to the documentation for the type class instances.

Constructors

SymBool (Term Bool)

Instances

Instances details

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 :: Type -> Type # 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 #
NFData SymBool Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBool Methods rnf :: SymBool -> () #
Eq SymBool Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBool Methods (==) :: SymBool -> SymBool -> Bool # (/=) :: SymBool -> SymBool -> Bool #
EvaluateSym SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.EvaluateSym Methods evaluateSym :: Bool -> Model -> SymBool -> SymBool Source #
ExtractSymbolics SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: SymBool -> SymbolSet Source #
Apply SymBool Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBool Associated Types type FunType SymBool Source # Methods apply :: SymBool -> FunType SymBool Source #
GPretty SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GPretty Methods gpretty :: SymBool -> Doc ann Source # gprettyPrec :: Int -> SymBool -> Doc ann Source # gprettyList :: [SymBool] -> Doc ann 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 (.\|\|) :: SymBool -> SymBool -> SymBool Source # (.&&) :: SymBool -> SymBool -> SymBool Source # symNot :: SymBool -> SymBool Source # symXor :: SymBool -> SymBool -> SymBool Source # symImplies :: SymBool -> SymBool -> SymBool Source #
Mergeable SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy SymBool Source #
SEq SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: SymBool -> SymBool -> SymBool Source # (./=) :: SymBool -> SymBool -> SymBool Source #
SOrd SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: SymBool -> SymBool -> SymBool Source # (.<=) :: SymBool -> SymBool -> SymBool Source # (.>) :: SymBool -> SymBool -> SymBool Source # (.>=) :: SymBool -> SymBool -> SymBool Source # symCompare :: SymBool -> SymBool -> UnionM Ordering Source #
SimpleMergeable SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> SymBool -> SymBool -> SymBool Source #
SubstituteSym SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymBool -> SymBool 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 Source #
Hashable SymBool Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBool Methods hashWithSalt :: Int -> SymBool -> Int # hash :: SymBool -> Int #
GenSym SymBool SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => SymBool -> m (UnionM SymBool) Source #
GenSym () SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => () -> m (UnionM 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.Core.Data.Class.ToCon Methods toCon :: SymBool -> Maybe SymBool Source #
ToCon SymBool Bool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymBool -> Maybe Bool Source #
ToSym SymBool SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: SymBool -> SymBool Source #
ToSym Bool SymBool Source #
Instance details Defined in Grisette.Internal.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 #
ToSym (UnionM Bool) SymBool Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.UnionM Methods toSym :: UnionM 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.5.0.1-IKpKourvCOdG0l1QW5fLHa" '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

Orphan instances

SymRep Bool Source #
Instance details Associated Types type SymType Bool Source #
LinkedRep Bool SymBool Source #
Instance details Methods underlyingTerm :: SymBool -> Term Bool Source # wrapTerm :: Term Bool -> SymBool Source #