grisette-0.11.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.AlgReal

Description

 
Synopsis

Documentation

newtype AlgRealPoly Source #

A univariate polynomial with integer coefficients.

For instance, 5x^3+2x-5 is represented as AlgRealPoly [(5, 3), (2, 1), (-5, 0)].

Constructors

AlgRealPoly [(Integer, Integer)] 

Instances

Instances details
Binary AlgRealPoly Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

put :: AlgRealPoly -> Put #

get :: Get AlgRealPoly #

putList :: [AlgRealPoly] -> Put #

Serial AlgRealPoly Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

deserialize :: MonadGet m => m AlgRealPoly #

Serialize AlgRealPoly Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

put :: Putter AlgRealPoly #

get :: Get AlgRealPoly #

NFData AlgRealPoly Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

rnf :: AlgRealPoly -> () #

Generic AlgRealPoly Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Associated Types

type Rep AlgRealPoly 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

type Rep AlgRealPoly = D1 ('MetaData "AlgRealPoly" "Grisette.Internal.SymPrim.AlgReal" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "AlgRealPoly" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Integer, Integer)])))

Methods

from :: AlgRealPoly -> Rep AlgRealPoly x #

to :: Rep AlgRealPoly x -> AlgRealPoly #

Eq AlgRealPoly Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

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

Mergeable AlgRealPoly Source # 
Instance details

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

Methods

rootStrategy :: MergingStrategy AlgRealPoly Source #

sortIndices :: AlgRealPoly -> [DynamicSortedIdx] Source #

Hashable AlgRealPoly Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

hashWithSalt :: Int -> AlgRealPoly -> Int #

hash :: AlgRealPoly -> Int #

Lift AlgRealPoly Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

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

type Rep AlgRealPoly Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

type Rep AlgRealPoly = D1 ('MetaData "AlgRealPoly" "Grisette.Internal.SymPrim.AlgReal" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'True) (C1 ('MetaCons "AlgRealPoly" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Integer, Integer)])))

data UnsupportedAlgRealOperation Source #

Exception for unsupported operations on algebraic real numbers.

We only support operations on exact rationals.

Constructors

UnsupportedAlgRealOperation 

Fields

Instances

Instances details
Exception UnsupportedAlgRealOperation Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

toException :: UnsupportedAlgRealOperation -> SomeException #

fromException :: SomeException -> Maybe UnsupportedAlgRealOperation #

displayException :: UnsupportedAlgRealOperation -> String #

backtraceDesired :: UnsupportedAlgRealOperation -> Bool #

Show UnsupportedAlgRealOperation Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

showsPrec :: Int -> UnsupportedAlgRealOperation -> ShowS #

show :: UnsupportedAlgRealOperation -> String #

showList :: [UnsupportedAlgRealOperation] -> ShowS #

toSBVAlgReal :: AlgReal -> AlgReal Source #

Convert algebraic real numbers to SBV's algebraic real numbers.

fromSBVAlgReal :: AlgReal -> AlgReal Source #

Convert SBV's algebraic real numbers to algebraic real numbers.

data RealPoint Source #

Boundary point for real intervals.

Constructors

OpenPoint Rational

Open point.

ClosedPoint Rational

Closed point.

Instances

Instances details
Binary RealPoint Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

put :: RealPoint -> Put #

get :: Get RealPoint #

putList :: [RealPoint] -> Put #

Serial RealPoint Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

deserialize :: MonadGet m => m RealPoint #

Serialize RealPoint Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

put :: Putter RealPoint #

get :: Get RealPoint #

NFData RealPoint Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

rnf :: RealPoint -> () #

Generic RealPoint Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Associated Types

type Rep RealPoint 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

type Rep RealPoint = D1 ('MetaData "RealPoint" "Grisette.Internal.SymPrim.AlgReal" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "OpenPoint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Rational)) :+: C1 ('MetaCons "ClosedPoint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Rational)))

Methods

from :: RealPoint -> Rep RealPoint x #

to :: Rep RealPoint x -> RealPoint #

Eq RealPoint Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

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

Mergeable RealPoint Source # 
Instance details

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

Methods

rootStrategy :: MergingStrategy RealPoint Source #

sortIndices :: RealPoint -> [DynamicSortedIdx] Source #

Hashable RealPoint Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

hashWithSalt :: Int -> RealPoint -> Int #

hash :: RealPoint -> Int #

Lift RealPoint Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

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

type Rep RealPoint Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

type Rep RealPoint = D1 ('MetaData "RealPoint" "Grisette.Internal.SymPrim.AlgReal" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "OpenPoint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Rational)) :+: C1 ('MetaCons "ClosedPoint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Rational)))

data AlgReal where Source #

Algebraic real numbers. The representation can be abstract for roots-of-polynomials or intervals.

Constructors

AlgExactRational :: Rational -> AlgReal

Exact rational number.

AlgInexactRational :: Rational -> AlgReal

Inexact rational numbers. SMT-solver return it with ? at the end.

AlgPolyRoot

Algebraic real number as a root of a polynomial.

Fields

AlgInterval

Interval with low and high bounds.

Fields

Instances

Instances details
Arbitrary AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

arbitrary :: Gen AlgReal #

shrink :: AlgReal -> [AlgReal] #

Binary AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

put :: AlgReal -> Put #

get :: Get AlgReal #

putList :: [AlgReal] -> Put #

Serial AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

deserialize :: MonadGet m => m AlgReal #

Serialize AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

put :: Putter AlgReal #

get :: Get AlgReal #

NFData AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

rnf :: AlgReal -> () #

Generic AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Associated Types

type Rep AlgReal 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

type Rep AlgReal = D1 ('MetaData "AlgReal" "Grisette.Internal.SymPrim.AlgReal" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) ((C1 ('MetaCons "AlgExactRational" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Rational)) :+: C1 ('MetaCons "AlgInexactRational" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Rational))) :+: (C1 ('MetaCons "AlgPolyRoot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AlgRealPoly) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))) :+: C1 ('MetaCons "AlgInterval" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RealPoint) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RealPoint))))

Methods

from :: AlgReal -> Rep AlgReal x #

to :: Rep AlgReal x -> AlgReal #

Num AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

(+) :: AlgReal -> AlgReal -> AlgReal #

(-) :: AlgReal -> AlgReal -> AlgReal #

(*) :: AlgReal -> AlgReal -> AlgReal #

negate :: AlgReal -> AlgReal #

abs :: AlgReal -> AlgReal #

signum :: AlgReal -> AlgReal #

fromInteger :: Integer -> AlgReal #

Fractional AlgReal Source #

Unlike sbv, we throw the error when divided by zero happens

Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

(/) :: AlgReal -> AlgReal -> AlgReal #

recip :: AlgReal -> AlgReal #

fromRational :: Rational -> AlgReal #

Real AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

toRational :: AlgReal -> Rational #

Show AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

showsPrec :: Int -> AlgReal -> ShowS #

show :: AlgReal -> String #

showList :: [AlgReal] -> ShowS #

Eq AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

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

Ord AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

compare :: AlgReal -> AlgReal -> Ordering #

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

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

(>) :: AlgReal -> AlgReal -> Bool #

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

max :: AlgReal -> AlgReal -> AlgReal #

min :: AlgReal -> AlgReal -> AlgReal #

Apply AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Associated Types

type FunType AlgReal 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

type FunType AlgReal = AlgReal

Methods

apply :: AlgReal -> FunType AlgReal Source #

FdivOr AlgReal Source # 
Instance details

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

Methods

fdivOr :: AlgReal -> AlgReal -> AlgReal -> AlgReal Source #

recipOr :: AlgReal -> AlgReal -> AlgReal Source #

EvalSym AlgReal Source # 
Instance details

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

Methods

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

ExtractSym AlgReal Source # 
Instance details

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

Methods

extractSym :: AlgReal -> AnySymbolSet Source #

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

Mergeable AlgReal Source # 
Instance details

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

Methods

rootStrategy :: MergingStrategy AlgReal Source #

sortIndices :: AlgReal -> [DynamicSortedIdx] Source #

PPrint AlgReal Source # 
Instance details

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

Methods

pformat :: AlgReal -> Doc ann Source #

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

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

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

SymEq AlgReal Source # 
Instance details

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

Methods

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

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

symDistinct :: [AlgReal] -> SymBool Source #

SymOrd AlgReal Source # 
Instance details

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

Methods

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

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

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

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

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

AllSyms AlgReal Source # 
Instance details

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

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

allSyms :: AlgReal -> [SomeSym] Source #

NonFuncSBVRep AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type NonFuncSBVBaseType AlgReal 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type NonFuncSBVBaseType AlgReal = AlgReal
PEvalFloatingTerm AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFloatingTerm

Methods

pevalFloatingUnaryTerm :: FloatingUnaryOp -> Term AlgReal -> Term AlgReal Source #

pevalPowerTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal Source #

withSbvFloatingTermConstraint :: (Floating (SBVType AlgReal) => r) -> r Source #

sbvPowerTerm :: SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal Source #

sbvFloatingUnaryTerm :: FloatingUnaryOp -> SBVType AlgReal -> SBVType AlgReal Source #

PEvalFractionalTerm AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFractionalTerm

Methods

pevalFdivTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal Source #

pevalRecipTerm :: Term AlgReal -> Term AlgReal Source #

withSbvFractionalTermConstraint :: (Fractional (SBVType AlgReal) => r) -> r Source #

sbvFdivTerm :: SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal Source #

sbvRecipTerm :: SBVType AlgReal -> SBVType AlgReal Source #

PEvalIEEEFPConvertibleTerm AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm

Methods

pevalFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term AlgReal -> Term FPRoundingMode -> Term (FP eb sb) -> Term AlgReal Source #

pevalToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term AlgReal -> Term (FP eb sb) Source #

sbvFromFPOrTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType AlgReal -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType AlgReal Source #

sbvToFPTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType AlgReal -> SBVType (FP eb sb) Source #

PEvalNumTerm AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm

Methods

pevalAddNumTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal Source #

pevalNegNumTerm :: Term AlgReal -> Term AlgReal Source #

pevalMulNumTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal Source #

pevalAbsNumTerm :: Term AlgReal -> Term AlgReal Source #

pevalSignumNumTerm :: Term AlgReal -> Term AlgReal Source #

withSbvNumTermConstraint :: (Num (SBVType AlgReal) => r) -> r Source #

sbvAddNumTerm :: SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal Source #

sbvNegNumTerm :: SBVType AlgReal -> SBVType AlgReal Source #

sbvMulNumTerm :: SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal Source #

sbvAbsNumTerm :: SBVType AlgReal -> SBVType AlgReal Source #

sbvSignumNumTerm :: SBVType AlgReal -> SBVType AlgReal Source #

PEvalOrdTerm AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm

Methods

pevalLtOrdTerm :: Term AlgReal -> Term AlgReal -> Term Bool Source #

pevalLeOrdTerm :: Term AlgReal -> Term AlgReal -> Term Bool Source #

withSbvOrdTermConstraint :: (OrdSymbolic (SBVType AlgReal) => r) -> r Source #

sbvLtOrdTerm :: SBVType AlgReal -> SBVType AlgReal -> SBV Bool Source #

sbvLeOrdTerm :: SBVType AlgReal -> SBVType AlgReal -> SBV Bool Source #

SBVRep AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type SBVType AlgReal 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type SBVType AlgReal = SBV AlgReal
SupportedNonFuncPrim AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

conNonFuncSBVTerm :: AlgReal -> SBV (NonFuncSBVBaseType AlgReal) Source #

symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType AlgReal)) Source #

withNonFuncPrim :: (NonFuncPrimConstraint AlgReal => r) -> r Source #

SupportedPrim AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

primTypeRep :: TypeRep AlgReal Source #

sameCon :: AlgReal -> AlgReal -> Bool Source #

hashConWithSalt :: Int -> AlgReal -> Int Source #

pformatCon :: AlgReal -> String Source #

defaultValue :: AlgReal Source #

pevalITETerm :: Term Bool -> Term AlgReal -> Term AlgReal -> Term AlgReal Source #

pevalEqTerm :: Term AlgReal -> Term AlgReal -> Term Bool Source #

pevalDistinctTerm :: NonEmpty (Term AlgReal) -> Term Bool Source #

conSBVTerm :: AlgReal -> SBVType AlgReal Source #

symSBVName :: TypedSymbol 'AnyKind AlgReal -> Int -> String Source #

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType AlgReal) Source #

withPrim :: ((PrimConstraint AlgReal, SMTDefinable (SBVType AlgReal), Mergeable (SBVType AlgReal), Typeable (SBVType AlgReal)) => a) -> a Source #

sbvIte :: SBV Bool -> SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal Source #

sbvEq :: SBVType AlgReal -> SBVType AlgReal -> SBV Bool Source #

sbvDistinct :: NonEmpty (SBVType AlgReal) -> SBV Bool Source #

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> AlgReal Source #

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd AlgReal -> Maybe (TypedSymbol knd' AlgReal) Source #

funcDummyConstraint :: SBVType AlgReal -> SBV Bool Source #

SupportedPrimConstraint AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type PrimConstraint AlgReal 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type PrimConstraint AlgReal = ()
SymRep AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

Associated Types

type SymType AlgReal 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

type SymType AlgReal = SymAlgReal
UnifiedConRep AlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type ConType AlgReal 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type ConType AlgReal = AlgReal
UnifiedSymRep AlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type SymType AlgReal 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type SymType AlgReal = SymAlgReal
Hashable AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

hashWithSalt :: Int -> AlgReal -> Int #

hash :: AlgReal -> Int #

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 #

ToCon SymAlgReal AlgReal Source # 
Instance details

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

Methods

toCon :: SymAlgReal -> Maybe AlgReal Source #

ToSym AlgReal SymAlgReal Source # 
Instance details

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

Methods

toSym :: AlgReal -> 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 #

PEvalFromIntegralTerm Integer AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term Integer -> Term AlgReal Source #

sbvFromIntegralTerm :: SBVType Integer -> SBVType AlgReal Source #

Lift AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

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

(MonadError ArithException m, TryMerge m) => SafeFdiv ArithException AlgReal m Source # 
Instance details

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

Methods

safeFdiv :: AlgReal -> AlgReal -> m AlgReal Source #

safeRecip :: AlgReal -> m AlgReal Source #

UnifiedFromIntegral 'C Integer AlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral Integer, Num AlgReal) (SymFromIntegral Integer AlgReal) => r) -> r Source #

UnifiedSolvable 'C AlgReal AlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSolvable

Methods

withBaseSolvable :: (If (IsConMode 'C) (AlgReal ~ AlgReal) (Solvable AlgReal AlgReal) => 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 mode m) => UnifiedSafeFdiv mode ArithException AlgReal m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFdiv

Methods

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

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb) => UnifiedSafeFromFP mode NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m Source # 
Instance details

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

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m AlgReal Source #

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'C (IntN n') AlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral (IntN n'), Num AlgReal) (SymFromIntegral (IntN n') AlgReal) => r) -> r Source #

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'C (WordN n') AlgReal Source # 
Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral (WordN n'), Num AlgReal) (SymFromIntegral (WordN n') AlgReal) => r) -> r Source #

ValidFP eb sb => IEEEFPConvertible AlgReal (FP eb sb) FPRoundingMode Source # 
Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fromFPOr :: AlgReal -> FPRoundingMode -> FP eb sb -> AlgReal Source #

toFP :: FPRoundingMode -> AlgReal -> FP eb sb Source #

ValidFP eb sb => IEEEFPToAlgReal AlgReal (FP eb sb) FPRoundingMode Source # 
Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fpToAlgReal :: AlgReal -> FP eb sb -> AlgReal Source #

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (IntN n) AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (IntN n) -> Term AlgReal Source #

sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType AlgReal Source #

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (WordN n) AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (WordN n) -> Term AlgReal Source #

sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType AlgReal Source #

type Rep AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

type Rep AlgReal = D1 ('MetaData "AlgReal" "Grisette.Internal.SymPrim.AlgReal" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) ((C1 ('MetaCons "AlgExactRational" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Rational)) :+: C1 ('MetaCons "AlgInexactRational" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Rational))) :+: (C1 ('MetaCons "AlgPolyRoot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AlgRealPoly) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))) :+: C1 ('MetaCons "AlgInterval" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RealPoint) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RealPoint))))
type FunType AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.AlgReal

type FunType AlgReal = AlgReal
type NonFuncSBVBaseType AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type NonFuncSBVBaseType AlgReal = AlgReal
type PrimConstraint AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type PrimConstraint AlgReal = ()
type SBVType AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type SBVType AlgReal = SBV AlgReal
type SymType AlgReal Source # 
Instance details

Defined in Grisette.Internal.SymPrim.SymAlgReal

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

Defined in Grisette.Internal.Unified.Class.UnifiedRep

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

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type SymType AlgReal = SymAlgReal