grisette-0.11.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.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 operations are available. Please refer to Grisette.Core for more information.

Constructors

SymInteger (Term Integer)

Instances

Instances details

Binary SymInteger Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

put :: SymInteger -> Put #

get :: Get SymInteger #

putList :: [SymInteger] -> Put #

Serial SymInteger Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

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

deserialize :: MonadGet m => m SymInteger #

Serialize SymInteger Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

put :: Putter SymInteger #

get :: Get SymInteger #

NFData SymInteger Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

rnf :: SymInteger -> () #

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
Instance details Defined in Grisette.Internal.SymPrim.SymInteger type Rep SymInteger = D1 ('MetaData "SymInteger" "Grisette.Internal.SymPrim.SymInteger" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "SymInteger" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingIntegerTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term Integer))))

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 #

Eq SymInteger Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

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

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

Apply SymInteger Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Associated Types

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

Methods

apply :: SymInteger -> FunType SymInteger Source #

ITEOp SymInteger Source #

Instance details

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

Methods

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

EvalSym SymInteger Source #

Instance details

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

Methods

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

ExtractSym SymInteger Source #

Instance details

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

Methods

extractSym :: SymInteger -> AnySymbolSet Source #

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

Mergeable SymInteger Source #

Instance details

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

Methods

rootStrategy :: MergingStrategy SymInteger Source #

sortIndices :: SymInteger -> [DynamicSortedIdx] Source #

PPrint SymInteger Source #

Instance details

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

Methods

pformat :: SymInteger -> Doc ann Source #

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

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

DivOr SymInteger Source #

Instance details

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

Methods

divOr :: SymInteger -> SymInteger -> SymInteger -> SymInteger Source #

modOr :: SymInteger -> SymInteger -> SymInteger -> SymInteger Source #

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

quotOr :: SymInteger -> SymInteger -> SymInteger -> SymInteger Source #

remOr :: SymInteger -> SymInteger -> SymInteger -> SymInteger Source #

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

SimpleMergeable SymInteger Source #

Instance details

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

Methods

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

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

SymEq SymInteger Source #

Instance details

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

Methods

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

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

symDistinct :: [SymInteger] -> SymBool Source #

SymOrd SymInteger Source #

Instance details

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

Methods

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

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

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

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

symCompare :: SymInteger -> SymInteger -> Union Ordering 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
Instance details Defined in Grisette.Internal.SymPrim.SymInteger type ConType SymInteger = Integer

UnifiedConRep SymInteger Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type ConType SymInteger
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type ConType SymInteger = Integer

UnifiedSymRep SymInteger Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

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

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 (Union SymInteger) Source #

GenSym () SymInteger Source #

Instance details

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

Methods

fresh :: MonadFresh m => () -> m (Union 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 #

SymFromIntegral SymInteger SymAlgReal Source #

Instance details

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

Methods

symFromIntegral :: SymInteger -> SymAlgReal Source #

SymFromIntegral SymInteger SymInteger Source #

Instance details

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

Methods

symFromIntegral :: SymInteger -> SymInteger Source #

ToCon SymInteger SymInteger Source #

Instance details

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

Methods

toCon :: SymInteger -> Maybe SymInteger Source #

ToCon SymInteger Integer Source #

Instance details

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

Methods

toCon :: SymInteger -> Maybe Integer Source #

ToSym SymInteger SymInteger Source #

Instance details

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

Methods

toSym :: SymInteger -> SymInteger Source #

ToSym Integer SymInteger Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.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 #

(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 #

(MonadUnion m, MonadError ArithException m) => SafeDiv ArithException SymInteger m Source #

Instance details

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

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 #

UnifiedFromIntegral 'S SymInteger SymAlgReal Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

UnifiedFromIntegral 'S SymInteger SymInteger Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

UnifiedSolvable 'S SymInteger Integer Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSolvable

Methods

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

(MonadError ArithException m, UnifiedBranching 'S m) => UnifiedSafeDiv 'S ArithException SymInteger m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeDiv

Methods

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

(MonadError ArithException m, UnifiedBranching 'S m) => UnifiedSafeLinearArith 'S ArithException SymInteger m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeLinearArith

Methods

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

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

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

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

(KnownNat n, 1 <= n) => UnifiedFromIntegral 'S SymInteger (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

(KnownNat n, 1 <= n) => UnifiedFromIntegral 'S SymInteger (SymWordN n) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

ValidFP eb sb => UnifiedFromIntegral 'S SymInteger (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

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

Methods

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

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

Instance details

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

Methods

symFromIntegral :: SymInteger -> SymIntN n Source #

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

Instance details

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

Methods

symFromIntegral :: SymInteger -> SymWordN n Source #

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymIntN n') SymInteger Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymWordN n') SymInteger Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

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

Instance details

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

Methods

symFromIntegral :: SymInteger -> SymFP eb sb Source #

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

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

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

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

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

Instance details

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

Methods

symFromIntegral :: SymIntN n -> SymInteger Source #

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

Instance details

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

Methods

symFromIntegral :: SymWordN n -> SymInteger Source #

ToSym (Union Integer) SymInteger Source #

Instance details

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

Methods

toSym :: Union 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.11.0.0-HndeEPlDvvDHSETLw6O8c" '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

type ConType SymInteger Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type ConType SymInteger = Integer

type SymType SymInteger Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type SymType SymInteger = SymInteger

Orphan instances

SymRep Integer Source #

Instance details

Associated Types

type SymType Integer
Instance details Defined in Grisette.Internal.SymPrim.SymInteger type SymType Integer = SymInteger

LinkedRep Integer SymInteger Source #

Instance details

Methods

underlyingTerm :: SymInteger -> Term Integer Source #

wrapTerm :: Term Integer -> SymInteger Source #