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

Description

 
Synopsis

Documentation

newtype SymAlgReal Source #

Symbolic representation of algebraic real numbers.

Constructors

SymAlgReal (Term AlgReal) 

Instances

Instances details
Binary SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

put :: SymAlgReal -> Put #

get :: Get SymAlgReal #

putList :: [SymAlgReal] -> Put #

Serial SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

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

deserialize :: MonadGet m => m SymAlgReal #

Serialize SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

put :: Putter SymAlgReal #

get :: Get SymAlgReal #

NFData SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

rnf :: SymAlgReal -> () #

IsString SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

fromString :: String -> SymAlgReal #

Floating SymAlgReal Source #

The functions are total and will not throw errors. The result for logBase is considered undefined if the base is 1.

It is the responsibility of the caller to ensure that the base is not 1 with the symbolic constraints, or use the LogBaseOr or SafeLogBase classes.

Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

pi :: SymAlgReal #

exp :: SymAlgReal -> SymAlgReal #

log :: SymAlgReal -> SymAlgReal #

sqrt :: SymAlgReal -> SymAlgReal #

(**) :: SymAlgReal -> SymAlgReal -> SymAlgReal #

logBase :: SymAlgReal -> SymAlgReal -> SymAlgReal #

sin :: SymAlgReal -> SymAlgReal #

cos :: SymAlgReal -> SymAlgReal #

tan :: SymAlgReal -> SymAlgReal #

asin :: SymAlgReal -> SymAlgReal #

acos :: SymAlgReal -> SymAlgReal #

atan :: SymAlgReal -> SymAlgReal #

sinh :: SymAlgReal -> SymAlgReal #

cosh :: SymAlgReal -> SymAlgReal #

tanh :: SymAlgReal -> SymAlgReal #

asinh :: SymAlgReal -> SymAlgReal #

acosh :: SymAlgReal -> SymAlgReal #

atanh :: SymAlgReal -> SymAlgReal #

log1p :: SymAlgReal -> SymAlgReal #

expm1 :: SymAlgReal -> SymAlgReal #

log1pexp :: SymAlgReal -> SymAlgReal #

log1mexp :: SymAlgReal -> SymAlgReal #

Generic SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Associated Types

type Rep SymAlgReal 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

type Rep SymAlgReal = D1 ('MetaData "SymAlgReal" "Grisette.Internal.SymPrim.SymAlgReal" "grisette-0.12.0.0-2G8wsM3ZzbCKYYnSn6PeBx" 'True) (C1 ('MetaCons "SymAlgReal" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingAlgRealTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term AlgReal))))

Methods

from :: SymAlgReal -> Rep SymAlgReal x #

to :: Rep SymAlgReal x -> SymAlgReal #

Num SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

(+) :: SymAlgReal -> SymAlgReal -> SymAlgReal #

(-) :: SymAlgReal -> SymAlgReal -> SymAlgReal #

(*) :: SymAlgReal -> SymAlgReal -> SymAlgReal #

negate :: SymAlgReal -> SymAlgReal #

abs :: SymAlgReal -> SymAlgReal #

signum :: SymAlgReal -> SymAlgReal #

fromInteger :: Integer -> SymAlgReal #

Fractional SymAlgReal Source #

The function is 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 FdivOr or SafeFdiv classes.

Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

(/) :: SymAlgReal -> SymAlgReal -> SymAlgReal #

recip :: SymAlgReal -> SymAlgReal #

fromRational :: Rational -> SymAlgReal #

Real SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

toRational :: SymAlgReal -> Rational #

Show SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

showsPrec :: Int -> SymAlgReal -> ShowS #

show :: SymAlgReal -> String #

showList :: [SymAlgReal] -> ShowS #

Eq SymAlgReal Source #

This will crash the program.

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

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

Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

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

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

Ord SymAlgReal Source #

This will crash the program.

SymAlgReal cannot be compared concretely.

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

Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

compare :: SymAlgReal -> SymAlgReal -> Ordering #

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

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

(>) :: SymAlgReal -> SymAlgReal -> Bool #

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

max :: SymAlgReal -> SymAlgReal -> SymAlgReal #

min :: SymAlgReal -> SymAlgReal -> SymAlgReal #

KeyEq SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

keyEq :: SymAlgReal -> SymAlgReal -> Bool Source #

KeyHashable SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

keyHashWithSalt :: Int -> SymAlgReal -> Int Source #

Apply SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Associated Types

type FunType SymAlgReal 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

type FunType SymAlgReal = SymAlgReal

Methods

apply :: SymAlgReal -> FunType SymAlgReal Source #

ITEOp SymAlgReal Source # 
Instance details

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

Methods

symIte :: SymBool -> SymAlgReal -> SymAlgReal -> SymAlgReal Source #

FdivOr SymAlgReal Source # 
Instance details

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

Methods

fdivOr :: SymAlgReal -> SymAlgReal -> SymAlgReal -> SymAlgReal Source #

recipOr :: SymAlgReal -> SymAlgReal -> SymAlgReal Source #

LogBaseOr SymAlgReal Source # 
Instance details

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

Methods

logBaseOr :: SymAlgReal -> SymAlgReal -> SymAlgReal -> SymAlgReal Source #

EvalSym SymAlgReal Source # 
Instance details

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

Methods

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

ExtractSym SymAlgReal Source # 
Instance details

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

Methods

extractSym :: SymAlgReal -> AnySymbolSet Source #

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

Mergeable SymAlgReal Source # 
Instance details

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

Methods

rootStrategy :: MergingStrategy SymAlgReal Source #

sortIndices :: SymAlgReal -> [DynamicSortedIdx] Source #

PPrint SymAlgReal Source # 
Instance details

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

Methods

pformat :: SymAlgReal -> Doc ann Source #

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

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

SimpleMergeable SymAlgReal Source # 
Instance details

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

Methods

mrgIte :: SymBool -> SymAlgReal -> SymAlgReal -> SymAlgReal Source #

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

SymEq SymAlgReal Source # 
Instance details

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

Methods

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

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

symDistinct :: [SymAlgReal] -> SymBool Source #

SymOrd SymAlgReal Source # 
Instance details

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

Methods

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

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

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

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

symCompare :: SymAlgReal -> SymAlgReal -> Union Ordering Source #

AllSyms SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

allSymsS :: SymAlgReal -> [SomeSym] -> [SomeSym] Source #

allSyms :: SymAlgReal -> [SomeSym] Source #

ConRep SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Associated Types

type ConType SymAlgReal 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

type ConType SymAlgReal = AlgReal
UnifiedConRep SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type ConType SymAlgReal 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type ConType SymAlgReal = AlgReal
UnifiedSymRep SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type SymType SymAlgReal 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type SymType SymAlgReal = SymAlgReal
GenSym SymAlgReal SymAlgReal Source # 
Instance details

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

Methods

fresh :: MonadFresh m => SymAlgReal -> m (Union SymAlgReal) Source #

GenSym () SymAlgReal Source # 
Instance details

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

Methods

fresh :: MonadFresh m => () -> m (Union SymAlgReal) Source #

GenSymSimple SymAlgReal SymAlgReal Source # 
Instance details

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

Methods

simpleFresh :: MonadFresh m => SymAlgReal -> m SymAlgReal Source #

GenSymSimple () SymAlgReal Source # 
Instance details

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

Methods

simpleFresh :: MonadFresh m => () -> m SymAlgReal Source #

Solvable AlgReal SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

con :: AlgReal -> SymAlgReal Source #

conView :: SymAlgReal -> Maybe AlgReal Source #

sym :: Symbol -> SymAlgReal Source #

ssym :: Identifier -> SymAlgReal Source #

isym :: Identifier -> Int -> SymAlgReal Source #

SymFromIntegral SymInteger SymAlgReal Source # 
Instance details

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

Methods

symFromIntegral :: SymInteger -> SymAlgReal Source #

ToCon SymAlgReal Rational Source # 
Instance details

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

Methods

toCon :: SymAlgReal -> Maybe Rational Source #

ToCon SymAlgReal AlgReal Source # 
Instance details

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

Methods

toCon :: SymAlgReal -> Maybe AlgReal Source #

ToCon SymAlgReal SymAlgReal Source # 
Instance details

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

Methods

toCon :: SymAlgReal -> Maybe SymAlgReal Source #

ToSym Rational SymAlgReal Source # 
Instance details

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

Methods

toSym :: Rational -> SymAlgReal Source #

ToSym AlgReal SymAlgReal Source # 
Instance details

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

Methods

toSym :: AlgReal -> SymAlgReal Source #

ToSym SymAlgReal SymAlgReal Source # 
Instance details

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

Methods

toSym :: SymAlgReal -> SymAlgReal Source #

LinkedRep AlgReal SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

underlyingTerm :: SymAlgReal -> Term AlgReal Source #

wrapTerm :: Term AlgReal -> SymAlgReal Source #

Lift SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

lift :: Quote m => SymAlgReal -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => SymAlgReal -> Code m SymAlgReal #

(MonadError ArithException m, MonadUnion m) => SafeFdiv ArithException SymAlgReal m Source # 
Instance details

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

Methods

safeFdiv :: SymAlgReal -> SymAlgReal -> m SymAlgReal Source #

safeRecip :: SymAlgReal -> m SymAlgReal Source #

(MonadError ArithException m, MonadUnion m) => SafeLogBase ArithException SymAlgReal m Source # 
Instance details

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

Methods

safeLogBase :: SymAlgReal -> SymAlgReal -> m SymAlgReal 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 #

UnifiedSolvable 'S SymAlgReal AlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSolvable

Methods

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

(MonadError ArithException m, UnifiedBranching 'S m) => UnifiedSafeFdiv 'S ArithException SymAlgReal m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFdiv

Methods

withBaseUnifiedSafeFdiv :: (SafeFdiv ArithException SymAlgReal m => r) -> r Source #

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

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

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

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

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

Methods

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

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymIntN n') SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'S (SymWordN n') SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

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

ValidFP eb sb => IEEEFPConvertible SymAlgReal (SymFP eb sb) SymFPRoundingMode Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

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

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

ValidFP eb sb => IEEEFPToAlgReal SymAlgReal (SymFP eb sb) SymFPRoundingMode Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fpToAlgReal :: SymAlgReal -> SymFP eb sb -> SymAlgReal Source #

(KnownNat n, 1 <= n) => SymFromIntegral (SymIntN n) SymAlgReal Source # 
Instance details

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

Methods

symFromIntegral :: SymIntN n -> SymAlgReal Source #

(KnownNat n, 1 <= n) => SymFromIntegral (SymWordN n) SymAlgReal Source # 
Instance details

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

Methods

symFromIntegral :: SymWordN n -> SymAlgReal Source #

type Rep SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

type Rep SymAlgReal = D1 ('MetaData "SymAlgReal" "Grisette.Internal.SymPrim.SymAlgReal" "grisette-0.12.0.0-2G8wsM3ZzbCKYYnSn6PeBx" 'True) (C1 ('MetaCons "SymAlgReal" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingAlgRealTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term AlgReal))))
type FunType SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

type FunType SymAlgReal = SymAlgReal
type ConType SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

type ConType SymAlgReal = AlgReal
type ConType SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type ConType SymAlgReal = AlgReal
type SymType SymAlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type SymType SymAlgReal = SymAlgReal

type SymAlgRealKey = AsKey SymAlgReal Source #

SymAlgReal type with identity equality.

Orphan instances

SymRep AlgReal Source # 
Instance details

Associated Types

type SymType AlgReal 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

type SymType AlgReal = SymAlgReal
LinkedRep AlgReal SymAlgReal Source # 
Instance details

Methods

underlyingTerm :: SymAlgReal -> Term AlgReal Source #

wrapTerm :: Term AlgReal -> SymAlgReal Source #