Grisette.Internal.SymPrim.AlgReal

Documentation

newtype AlgRealPoly

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

Generic AlgRealPoly

Defined in Grisette.Internal.SymPrim.AlgReal

Associated Types

type Rep AlgRealPoly :: Type -> Type

Methods

from :: AlgRealPoly -> Rep AlgRealPoly x

to :: Rep AlgRealPoly x -> AlgRealPoly

Binary AlgRealPoly

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

put :: AlgRealPoly -> Put

get :: Get AlgRealPoly

putList :: [AlgRealPoly] -> Put

Serial AlgRealPoly

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

deserialize :: MonadGet m => m AlgRealPoly

Serialize AlgRealPoly

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

put :: Putter AlgRealPoly

get :: Get AlgRealPoly

NFData AlgRealPoly

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

rnf :: AlgRealPoly -> ()

Eq AlgRealPoly

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

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

Mergeable AlgRealPoly

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

Methods

rootStrategy :: MergingStrategy AlgRealPoly

Hashable AlgRealPoly

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

hashWithSalt :: Int -> AlgRealPoly -> Int

hash :: AlgRealPoly -> Int

Lift AlgRealPoly

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

Defined in Grisette.Internal.SymPrim.AlgReal

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

data UnsupportedAlgRealOperation

Exception for unsupported operations on algebraic real numbers.

We only support operations on exact rationals.

Constructors

UnsupportedAlgRealOperation

Fields

• op :: String
• msg :: String

Instances

Exception UnsupportedAlgRealOperation

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

toException :: UnsupportedAlgRealOperation -> SomeException

fromException :: SomeException -> Maybe UnsupportedAlgRealOperation

displayException :: UnsupportedAlgRealOperation -> String

Show UnsupportedAlgRealOperation

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

showsPrec :: Int -> UnsupportedAlgRealOperation -> ShowS

show :: UnsupportedAlgRealOperation -> String

showList :: [UnsupportedAlgRealOperation] -> ShowS

toSBVAlgReal :: AlgReal -> AlgReal

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

fromSBVAlgReal :: AlgReal -> AlgReal

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

data RealPoint

Boundary point for real intervals.

Constructors

OpenPoint Rational

Open point.

ClosedPoint Rational

Closed point.

Instances

Generic RealPoint

Defined in Grisette.Internal.SymPrim.AlgReal

Associated Types

type Rep RealPoint :: Type -> Type

Methods

from :: RealPoint -> Rep RealPoint x

to :: Rep RealPoint x -> RealPoint

Binary RealPoint

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

put :: RealPoint -> Put

get :: Get RealPoint

putList :: [RealPoint] -> Put

Serial RealPoint

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

deserialize :: MonadGet m => m RealPoint

Serialize RealPoint

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

put :: Putter RealPoint

get :: Get RealPoint

NFData RealPoint

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

rnf :: RealPoint -> ()

Eq RealPoint

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

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

Mergeable RealPoint

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

Methods

rootStrategy :: MergingStrategy RealPoint

Hashable RealPoint

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

hashWithSalt :: Int -> RealPoint -> Int

hash :: RealPoint -> Int

Lift RealPoint

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

Defined in Grisette.Internal.SymPrim.AlgReal

type Rep RealPoint = D1 ('MetaData "RealPoint" "Grisette.Internal.SymPrim.AlgReal" "grisette-0.9.0.0-8b30m8DmEAJELhVBobm0Vc" '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

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

• :: Integer

  Which root is it?

• -> AlgRealPoly

  Polynomial defining equation.

• -> Maybe String

  Approximate decimal representation.

• -> AlgReal

AlgInterval

Interval with low and high bounds.

Fields

• :: RealPoint

  Lower bound.

• -> RealPoint

  Upper bound.

• -> AlgReal

Instances

Arbitrary AlgReal

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

arbitrary :: Gen AlgReal

shrink :: AlgReal -> [AlgReal]

Generic AlgReal

Defined in Grisette.Internal.SymPrim.AlgReal

Associated Types

type Rep AlgReal :: Type -> Type

Methods

from :: AlgReal -> Rep AlgReal x

to :: Rep AlgReal x -> AlgReal

Num AlgReal

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

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

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

recip :: AlgReal -> AlgReal

fromRational :: Rational -> AlgReal

Real AlgReal

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

toRational :: AlgReal -> Rational

Show AlgReal

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

showsPrec :: Int -> AlgReal -> ShowS

show :: AlgReal -> String

showList :: [AlgReal] -> ShowS

Binary AlgReal

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

put :: AlgReal -> Put

get :: Get AlgReal

putList :: [AlgReal] -> Put

Serial AlgReal

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

deserialize :: MonadGet m => m AlgReal

Serialize AlgReal

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

put :: Putter AlgReal

get :: Get AlgReal

NFData AlgReal

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

rnf :: AlgReal -> ()

Eq AlgReal

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

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

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

Ord AlgReal

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

EvalSym AlgReal

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

Methods

evalSym :: Bool -> Model -> AlgReal -> AlgReal

ExtractSym AlgReal

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

Methods

extractSym :: AlgReal -> AnySymbolSet

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

Apply AlgReal

Defined in Grisette.Internal.SymPrim.AlgReal

Associated Types

type FunType AlgReal

Methods

apply :: AlgReal -> FunType AlgReal

Mergeable AlgReal

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

Methods

rootStrategy :: MergingStrategy AlgReal

PPrint AlgReal

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

Methods

pformat :: AlgReal -> Doc ann

pformatPrec :: Int -> AlgReal -> Doc ann

pformatList :: [AlgReal] -> Doc ann

FdivOr AlgReal

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

Methods

fdivOr :: AlgReal -> AlgReal -> AlgReal -> AlgReal

recipOr :: AlgReal -> AlgReal -> AlgReal

SubstSym AlgReal

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

Methods

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

SymEq AlgReal

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

Methods

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

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

symDistinct :: [AlgReal] -> SymBool

SymOrd AlgReal

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

Methods

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

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

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

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

symCompare :: AlgReal -> AlgReal -> Union Ordering

AllSyms AlgReal

Defined in Grisette.Internal.SymPrim.AllSyms

Methods

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

allSyms :: AlgReal -> [SomeSym]

NonFuncSBVRep AlgReal

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

Associated Types

type NonFuncSBVBaseType AlgReal

PEvalFloatingTerm AlgReal

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

Methods

pevalFloatingUnaryTerm :: FloatingUnaryOp -> Term AlgReal -> Term AlgReal

pevalPowerTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal

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

sbvPowerTerm :: SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal

sbvFloatingUnaryTerm :: FloatingUnaryOp -> SBVType AlgReal -> SBVType AlgReal

PEvalFractionalTerm AlgReal

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

Methods

pevalFdivTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal

pevalRecipTerm :: Term AlgReal -> Term AlgReal

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

sbvFdivTerm :: SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal

sbvRecipTerm :: SBVType AlgReal -> SBVType AlgReal

PEvalIEEEFPConvertibleTerm AlgReal

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

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

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

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

PEvalNumTerm AlgReal

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

Methods

pevalAddNumTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal

pevalNegNumTerm :: Term AlgReal -> Term AlgReal

pevalMulNumTerm :: Term AlgReal -> Term AlgReal -> Term AlgReal

pevalAbsNumTerm :: Term AlgReal -> Term AlgReal

pevalSignumNumTerm :: Term AlgReal -> Term AlgReal

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

sbvAddNumTerm :: SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal

sbvNegNumTerm :: SBVType AlgReal -> SBVType AlgReal

sbvMulNumTerm :: SBVType AlgReal -> SBVType AlgReal -> SBVType AlgReal

sbvAbsNumTerm :: SBVType AlgReal -> SBVType AlgReal

sbvSignumNumTerm :: SBVType AlgReal -> SBVType AlgReal

PEvalOrdTerm AlgReal

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

Methods

pevalLtOrdTerm :: Term AlgReal -> Term AlgReal -> Term Bool

pevalLeOrdTerm :: Term AlgReal -> Term AlgReal -> Term Bool

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

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

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

SBVRep AlgReal

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

Associated Types

type SBVType AlgReal

SupportedNonFuncPrim AlgReal

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

Methods

conNonFuncSBVTerm :: AlgReal -> SBV (NonFuncSBVBaseType AlgReal)

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

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

SupportedPrim AlgReal

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

Methods

primTypeRep :: TypeRep AlgReal

sameCon :: AlgReal -> AlgReal -> Bool

hashConWithSalt :: Int -> AlgReal -> Int

pformatCon :: AlgReal -> String

defaultValue :: AlgReal

pevalITETerm :: Term Bool -> Term AlgReal -> Term AlgReal -> Term AlgReal

pevalEqTerm :: Term AlgReal -> Term AlgReal -> Term Bool

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

conSBVTerm :: AlgReal -> SBVType AlgReal

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

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

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

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

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

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

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

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

funcDummyConstraint :: SBVType AlgReal -> SBV Bool

SupportedPrimConstraint AlgReal

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

Associated Types

type PrimConstraint AlgReal

SymRep AlgReal

Defined in Grisette.Internal.SymPrim.SymAlgReal

Associated Types

type SymType AlgReal

Hashable AlgReal

Defined in Grisette.Internal.SymPrim.AlgReal

Methods

hashWithSalt :: Int -> AlgReal -> Int

hash :: AlgReal -> Int

Solvable AlgReal SymAlgReal

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

con :: AlgReal -> SymAlgReal

conView :: SymAlgReal -> Maybe AlgReal

sym :: Symbol -> SymAlgReal

ssym :: Identifier -> SymAlgReal

isym :: Identifier -> Int -> SymAlgReal

ToCon SymAlgReal AlgReal

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

Methods

toCon :: SymAlgReal -> Maybe AlgReal

ToSym AlgReal SymAlgReal

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

Methods

toSym :: AlgReal -> SymAlgReal

LinkedRep AlgReal SymAlgReal

Defined in Grisette.Internal.SymPrim.SymAlgReal

Methods

underlyingTerm :: SymAlgReal -> Term AlgReal

wrapTerm :: Term AlgReal -> SymAlgReal

PEvalFromIntegralTerm Integer AlgReal

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

Methods

pevalFromIntegralTerm :: Term Integer -> Term AlgReal

sbvFromIntegralTerm :: SBVType Integer -> SBVType AlgReal

Lift AlgReal

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

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

Methods

safeFdiv :: AlgReal -> AlgReal -> m AlgReal

safeRecip :: AlgReal -> m AlgReal

UnifiedFromIntegral 'Con Integer AlgReal

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

(Typeable mode, MonadError ArithException m, UnifiedBranching mode m) => UnifiedSafeFdiv mode ArithException AlgReal m

Defined in Grisette.Unified.Internal.Class.UnifiedSafeFdiv

Methods

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

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

Defined in Grisette.Unified.Internal.Class.UnifiedSafeFromFP

Methods

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

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

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

Methods

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

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Con (IntN n') AlgReal

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

(KnownNat n', 1 <= n') => UnifiedFromIntegral 'Con (WordN n') AlgReal

Defined in Grisette.Unified.Internal.Class.UnifiedFromIntegral

Methods

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

ValidFP eb sb => IEEEFPConvertible AlgReal (FP eb sb) FPRoundingMode

Defined in Grisette.Internal.SymPrim.FP

Methods

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

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

ValidFP eb sb => IEEEFPToAlgReal AlgReal (FP eb sb) FPRoundingMode

Defined in Grisette.Internal.SymPrim.FP

Methods

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

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (IntN n) AlgReal

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

Methods

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

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

(KnownNat n, 1 <= n) => PEvalFromIntegralTerm (WordN n) AlgReal

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

Methods

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

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

type Rep AlgReal

Defined in Grisette.Internal.SymPrim.AlgReal

type Rep AlgReal = D1 ('MetaData "AlgReal" "Grisette.Internal.SymPrim.AlgReal" "grisette-0.9.0.0-8b30m8DmEAJELhVBobm0Vc" '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

Defined in Grisette.Internal.SymPrim.AlgReal

type FunType AlgReal = AlgReal

type NonFuncSBVBaseType AlgReal

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

type NonFuncSBVBaseType AlgReal = AlgReal

type PrimConstraint AlgReal

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

type PrimConstraint AlgReal = ()

type SBVType AlgReal

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

type SBVType AlgReal = SBV AlgReal

type SymType AlgReal

Defined in Grisette.Internal.SymPrim.SymAlgReal

type SymType AlgReal = SymAlgReal