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.SymInteger

Contents

Orphan instances

Description

Synopsis

newtype SymInteger = SymInteger (Term Integer)

Documentation

newtype SymInteger Source #

Symbolic (unbounded, mathematical) integer type.

>>> "a" + 1 :: SymInteger
(+ 1 a)

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

Constructors

SymInteger (Term Integer)

Instances

Instances details

IsString SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods fromString :: String -> SymInteger #
Generic SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Associated Types type Rep SymInteger :: Type -> Type # Methods from :: SymInteger -> Rep SymInteger x # to :: Rep SymInteger x -> SymInteger #
Num SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods (+) :: SymInteger -> SymInteger -> SymInteger # (-) :: SymInteger -> SymInteger -> SymInteger # (*) :: SymInteger -> SymInteger -> SymInteger # negate :: SymInteger -> SymInteger # abs :: SymInteger -> SymInteger # signum :: SymInteger -> SymInteger # fromInteger :: Integer -> SymInteger #
Show SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods showsPrec :: Int -> SymInteger -> ShowS # show :: SymInteger -> String # showList :: [SymInteger] -> ShowS #
NFData SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods rnf :: SymInteger -> () #
Eq SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods (==) :: SymInteger -> SymInteger -> Bool # (/=) :: SymInteger -> SymInteger -> Bool #
EvaluateSym SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.EvaluateSym Methods evaluateSym :: Bool -> Model -> SymInteger -> SymInteger Source #
ExtractSymbolics SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ExtractSymbolics Methods extractSymbolics :: SymInteger -> SymbolSet Source #
Apply SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Associated Types type FunType SymInteger Source # Methods apply :: SymInteger -> FunType SymInteger Source #
GPretty SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GPretty Methods gpretty :: SymInteger -> Doc ann Source # gprettyPrec :: Int -> SymInteger -> Doc ann Source # gprettyList :: [SymInteger] -> Doc ann Source #
ITEOp SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ITEOp Methods symIte :: SymBool -> SymInteger -> SymInteger -> SymInteger Source #
Mergeable SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy SymInteger Source #
SEq SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SEq Methods (.==) :: SymInteger -> SymInteger -> SymBool Source # (./=) :: SymInteger -> SymInteger -> SymBool Source #
SOrd SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SOrd Methods (.<) :: SymInteger -> SymInteger -> SymBool Source # (.<=) :: SymInteger -> SymInteger -> SymBool Source # (.>) :: SymInteger -> SymInteger -> SymBool Source # (.>=) :: SymInteger -> SymInteger -> SymBool Source # symCompare :: SymInteger -> SymInteger -> UnionM Ordering Source #
SimpleMergeable SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SimpleMergeable Methods mrgIte :: SymBool -> SymInteger -> SymInteger -> SymInteger Source #
SubstituteSym SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymInteger -> SymInteger Source #
AllSyms SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods allSymsS :: SymInteger -> [SomeSym] -> [SomeSym] Source # allSyms :: SymInteger -> [SomeSym] Source #
ConRep SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Associated Types type ConType SymInteger Source #
Hashable SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods hashWithSalt :: Int -> SymInteger -> Int # hash :: SymInteger -> Int #
GenSym SymInteger SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => SymInteger -> m (UnionM SymInteger) Source #
GenSym () SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => () -> m (UnionM SymInteger) Source #
GenSymSimple SymInteger SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => SymInteger -> m SymInteger Source #
GenSymSimple () SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => () -> m SymInteger Source #
Solvable Integer SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods con :: Integer -> SymInteger Source # conView :: SymInteger -> Maybe Integer Source # sym :: Symbol -> SymInteger Source # ssym :: Identifier -> SymInteger Source # isym :: Identifier -> Int -> SymInteger Source #
ToCon SymInteger SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymInteger -> Maybe SymInteger Source #
ToCon SymInteger Integer Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToCon Methods toCon :: SymInteger -> Maybe Integer Source #
ToSym SymInteger SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: SymInteger -> SymInteger Source #
ToSym Integer SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Integer -> SymInteger Source #
LinkedRep Integer SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods underlyingTerm :: SymInteger -> Term Integer Source # wrapTerm :: Term Integer -> SymInteger Source #
Lift SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods lift :: Quote m => SymInteger -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => SymInteger -> Code m SymInteger #
(MonadUnion m, MonadError ArithException m) => SafeDivision ArithException SymInteger m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: SymInteger -> SymInteger -> m SymInteger Source # safeMod :: SymInteger -> SymInteger -> m SymInteger Source # safeDivMod :: SymInteger -> SymInteger -> m (SymInteger, SymInteger) Source # safeQuot :: SymInteger -> SymInteger -> m SymInteger Source # safeRem :: SymInteger -> SymInteger -> m SymInteger Source # safeQuotRem :: SymInteger -> SymInteger -> m (SymInteger, SymInteger) Source #
(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException SymInteger m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: SymInteger -> SymInteger -> m SymInteger Source # safeNeg :: SymInteger -> m SymInteger Source # safeSub :: SymInteger -> SymInteger -> m SymInteger Source #
ToSym (UnionM Integer) SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.UnionM Methods toSym :: UnionM Integer -> SymInteger Source #
type Rep SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger type Rep SymInteger = D1 ('MetaData "SymInteger" "Grisette.Internal.SymPrim.SymInteger" "grisette-0.5.0.0-2ZDAuzWdzg48yPrBcRstUR" 'True) (C1 ('MetaCons "SymInteger" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingIntegerTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term Integer))))
type FunType SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger type FunType SymInteger = SymInteger
type ConType SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger type ConType SymInteger = Integer

Orphan instances

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