Grisette.Internal.SymPrim.SymInteger

Documentation

newtype SymInteger

Symbolic (unbounded, mathematical) integer type.

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

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

Constructors

SymInteger (Term Integer)

Instances

IsString SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

fromString :: String -> SymInteger

Generic SymInteger

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

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

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

showsPrec :: Int -> SymInteger -> ShowS

show :: SymInteger -> String

showList :: [SymInteger] -> ShowS

NFData SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

rnf :: SymInteger -> ()

Eq SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

(==) :: SymInteger -> SymInteger -> Bool

(/=) :: SymInteger -> SymInteger -> Bool

EvalSym SymInteger

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

Methods

evalSym :: Bool -> Model -> SymInteger -> SymInteger

ExtractSym SymInteger

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

Methods

extractSym :: SymInteger -> AnySymbolSet

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => SymInteger -> Maybe (SymbolSet knd)

Apply SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Associated Types

type FunType SymInteger

Methods

apply :: SymInteger -> FunType SymInteger

ITEOp SymInteger

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

Methods

symIte :: SymBool -> SymInteger -> SymInteger -> SymInteger

Mergeable SymInteger

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

Methods

rootStrategy :: MergingStrategy SymInteger

PPrint SymInteger

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

Methods

pformat :: SymInteger -> Doc ann

pformatPrec :: Int -> SymInteger -> Doc ann

pformatList :: [SymInteger] -> Doc ann

DivOr SymInteger

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

Methods

divOr :: SymInteger -> SymInteger -> SymInteger -> SymInteger

modOr :: SymInteger -> SymInteger -> SymInteger -> SymInteger

divModOr :: (SymInteger, SymInteger) -> SymInteger -> SymInteger -> (SymInteger, SymInteger)

quotOr :: SymInteger -> SymInteger -> SymInteger -> SymInteger

remOr :: SymInteger -> SymInteger -> SymInteger -> SymInteger

quotRemOr :: (SymInteger, SymInteger) -> SymInteger -> SymInteger -> (SymInteger, SymInteger)

SimpleMergeable SymInteger

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

Methods

mrgIte :: SymBool -> SymInteger -> SymInteger -> SymInteger

SubstSym SymInteger

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

Methods

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

SymEq SymInteger

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

Methods

(.==) :: SymInteger -> SymInteger -> SymBool

(./=) :: SymInteger -> SymInteger -> SymBool

symDistinct :: [SymInteger] -> SymBool

SymOrd SymInteger

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

Methods

(.<) :: SymInteger -> SymInteger -> SymBool

(.<=) :: SymInteger -> SymInteger -> SymBool

(.>) :: SymInteger -> SymInteger -> SymBool

(.>=) :: SymInteger -> SymInteger -> SymBool

symCompare :: SymInteger -> SymInteger -> Union Ordering

AllSyms SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

allSymsS :: SymInteger -> [SomeSym] -> [SomeSym]

allSyms :: SymInteger -> [SomeSym]

ConRep SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Associated Types

type ConType SymInteger

Hashable SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

hashWithSalt :: Int -> SymInteger -> Int

hash :: SymInteger -> Int

GenSym SymInteger SymInteger

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

Methods

fresh :: MonadFresh m => SymInteger -> m (Union SymInteger)

GenSym () SymInteger

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

Methods

fresh :: MonadFresh m => () -> m (Union SymInteger)

GenSymSimple SymInteger SymInteger

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

Methods

simpleFresh :: MonadFresh m => SymInteger -> m SymInteger

GenSymSimple () SymInteger

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

Methods

simpleFresh :: MonadFresh m => () -> m SymInteger

Solvable Integer SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

con :: Integer -> SymInteger

conView :: SymInteger -> Maybe Integer

sym :: Symbol -> SymInteger

ssym :: Identifier -> SymInteger

isym :: Identifier -> Int -> SymInteger

SymFromIntegral SymInteger SymAlgReal

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

Methods

symFromIntegral :: SymInteger -> SymAlgReal

SymFromIntegral SymInteger SymInteger

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

Methods

symFromIntegral :: SymInteger -> SymInteger

ToCon SymInteger SymInteger

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

Methods

toCon :: SymInteger -> Maybe SymInteger

ToCon SymInteger Integer

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

Methods

toCon :: SymInteger -> Maybe Integer

ToSym SymInteger SymInteger

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

Methods

toSym :: SymInteger -> SymInteger

ToSym Integer SymInteger

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

Methods

toSym :: Integer -> SymInteger

LinkedRep Integer SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

underlyingTerm :: SymInteger -> Term Integer

wrapTerm :: Term Integer -> SymInteger

Lift SymInteger

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) => SafeDiv ArithException SymInteger m

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

Methods

safeDiv :: SymInteger -> SymInteger -> m SymInteger

safeMod :: SymInteger -> SymInteger -> m SymInteger

safeDivMod :: SymInteger -> SymInteger -> m (SymInteger, SymInteger)

safeQuot :: SymInteger -> SymInteger -> m SymInteger

safeRem :: SymInteger -> SymInteger -> m SymInteger

safeQuotRem :: SymInteger -> SymInteger -> m (SymInteger, SymInteger)

(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException SymInteger m

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

Methods

safeAdd :: SymInteger -> SymInteger -> m SymInteger

safeNeg :: SymInteger -> m SymInteger

safeSub :: SymInteger -> SymInteger -> m SymInteger

UnifiedFromIntegral 'Sym SymInteger SymAlgReal

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral SymInteger, Num SymAlgReal) (SymFromIntegral SymInteger SymAlgReal) => r) -> r

UnifiedFromIntegral 'Sym SymInteger SymInteger

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral SymInteger, Num SymInteger) (SymFromIntegral SymInteger SymInteger) => r) -> r

(MonadError ArithException m, UnifiedBranching 'Sym m) => UnifiedSafeDiv 'Sym ArithException SymInteger m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeDiv

Methods

withBaseSafeDiv :: (SafeDiv ArithException SymInteger m => r) -> r

(MonadError ArithException m, UnifiedBranching 'Sym m) => UnifiedSafeLinearArith 'Sym ArithException SymInteger m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeLinearArith

Methods

withBaseSafeLinearArith :: (SafeLinearArith ArithException SymInteger m => r) -> r

(MonadError NotRepresentableFPError m, UnifiedBranching 'Sym m, ValidFP eb sb) => UnifiedSafeFromFP 'Sym NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m => r) -> r

(KnownNat n, 1 <= n) => UnifiedFromIntegral 'Sym SymInteger (SymIntN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral SymInteger, Num (SymIntN n)) (SymFromIntegral SymInteger (SymIntN n)) => r) -> r

(KnownNat n, 1 <= n) => UnifiedFromIntegral 'Sym SymInteger (SymWordN n)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral SymInteger, Num (SymWordN n)) (SymFromIntegral SymInteger (SymWordN n)) => r) -> r

ValidFP eb sb => UnifiedFromIntegral 'Sym SymInteger (SymFP eb sb)

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral SymInteger, Num (SymFP eb sb)) (SymFromIntegral SymInteger (SymFP eb sb)) => r) -> r

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m

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

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m SymInteger

(KnownNat n, 1 <= n) => SymFromIntegral SymInteger (SymIntN n)

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

Methods

symFromIntegral :: SymInteger -> SymIntN n

(KnownNat n, 1 <= n) => SymFromIntegral SymInteger (SymWordN n)

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

Methods

symFromIntegral :: SymInteger -> SymWordN n

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Sym (SymIntN n') SymInteger

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral (SymIntN n'), Num SymInteger) (SymFromIntegral (SymIntN n') SymInteger) => r) -> r

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Sym (SymWordN n') SymInteger

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'Sym) (Integral (SymWordN n'), Num SymInteger) (SymFromIntegral (SymWordN n') SymInteger) => r) -> r

ValidFP eb sb => SymFromIntegral SymInteger (SymFP eb sb)

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

Methods

symFromIntegral :: SymInteger -> SymFP eb sb

ValidFP eb sb => IEEEFPConvertible SymInteger (SymFP eb sb) SymFPRoundingMode

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymInteger -> SymFPRoundingMode -> SymFP eb sb -> SymInteger

toFP :: SymFPRoundingMode -> SymInteger -> SymFP eb sb

(KnownNat n, 1 <= n) => SymFromIntegral (SymIntN n) SymInteger

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

Methods

symFromIntegral :: SymIntN n -> SymInteger

(KnownNat n, 1 <= n) => SymFromIntegral (SymWordN n) SymInteger

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

Methods

symFromIntegral :: SymWordN n -> SymInteger

ToSym (Union Integer) SymInteger

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

Methods

toSym :: Union Integer -> SymInteger

type Rep SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

type Rep SymInteger = D1 ('MetaData "SymInteger" "Grisette.Internal.SymPrim.SymInteger" "grisette-0.8.0.0-9ziui23pS5H4p62qxsVv1c" 'True) (C1 ('MetaCons "SymInteger" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingIntegerTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term Integer))))

type FunType SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

type FunType SymInteger = SymInteger

type ConType SymInteger

Defined in Grisette.Internal.SymPrim.SymInteger

type ConType SymInteger = Integer

Orphan instances

SymRep Integer

Associated Types

type SymType Integer

LinkedRep Integer SymInteger

Methods

underlyingTerm :: SymInteger -> Term Integer

wrapTerm :: Term Integer -> SymInteger