grisette-0.12.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2024
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellNone
LanguageHaskell2010

Grisette.Internal.SymPrim.SymInteger

Description

 
Synopsis

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 #

Enum SymInteger Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

succ :: SymInteger -> SymInteger #

pred :: SymInteger -> SymInteger #

toEnum :: Int -> SymInteger #

fromEnum :: SymInteger -> Int #

enumFrom :: SymInteger -> [SymInteger] #

enumFromThen :: SymInteger -> SymInteger -> [SymInteger] #

enumFromTo :: SymInteger -> SymInteger -> [SymInteger] #

enumFromThenTo :: SymInteger -> SymInteger -> SymInteger -> [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.12.0.0-2G8wsM3ZzbCKYYnSn6PeBx" '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 #

Integral SymInteger Source #

The functions are total and will not throw errors. The result is considered undefined if the divisor is 0.

It is the responsibility of the caller to ensure that the divisor is not zero with the symbolic constraints, or use the DivOr or SafeDiv classes.

Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

quot :: SymInteger -> SymInteger -> SymInteger #

rem :: SymInteger -> SymInteger -> SymInteger #

div :: SymInteger -> SymInteger -> SymInteger #

mod :: SymInteger -> SymInteger -> SymInteger #

quotRem :: SymInteger -> SymInteger -> (SymInteger, SymInteger) #

divMod :: SymInteger -> SymInteger -> (SymInteger, SymInteger) #

toInteger :: SymInteger -> Integer #

Real SymInteger Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

toRational :: SymInteger -> Rational #

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 #

This will crash the program.

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

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

Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

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

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

Ord SymInteger Source #

Except for max and min, the other functions will crash the program.

SymInteger cannot be compared concretely.

If you want symbolic version of the comparison operators, use SymOrd instead.

Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

compare :: SymInteger -> SymInteger -> Ordering #

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

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

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

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

max :: SymInteger -> SymInteger -> SymInteger #

min :: SymInteger -> SymInteger -> SymInteger #

KeyEq SymInteger Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

keyEq :: SymInteger -> SymInteger -> Bool Source #

KeyHashable SymInteger Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymInteger

Methods

keyHashWithSalt :: Int -> SymInteger -> Int Source #

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
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.12.0.0-2G8wsM3ZzbCKYYnSn6PeBx" '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

type SymIntegerKey = AsKey SymInteger Source #

SymInteger type with identity equality.

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 #