Floating point over nullables, sort-erased

One lifted constructor per liftable operator, <id>?, each answering none unless every argument is some.

A rounding-mode argument becomes nullable along with the rest: fpAdd? takes a rounding mode of sort (Nullable RoundingMode), as every argument of a lifted operator is nullable.

def Cvc.Untyped.Term.fpRem? [Ω] (lft rgt : Term) : Env Term

fpRem lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.fpRem? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_REM #[lft, rgt]

def Cvc.Untyped.Term.fpOfBits? [Ω] (sign exponent significand : Term) : Env Term

fpOfBits lifted over nullables, strictly: none unless every argument is some.

Equations

• sign.fpOfBits? exponent significand = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_FP #[sign, exponent, significand]

def Cvc.Untyped.Term.fpMax? [Ω] (lft rgt : Term) : Env Term

fpMax lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.fpMax? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_MAX #[lft, rgt]

def Cvc.Untyped.Term.fpIsSubnormal? [Ω] (fp : Term) : Env Term

fpIsSubnormal lifted over nullables, strictly: none unless every argument is some.

Equations

• fp.fpIsSubnormal? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_IS_SUBNORMAL #[fp]

def Cvc.Untyped.Term.fpDiv? [Ω] (rm lft rgt : Term) : Env Term

fpDiv lifted over nullables, strictly: none unless every argument is some.

Equations

• rm.fpDiv? lft rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_DIV #[rm, lft, rgt]

def Cvc.Untyped.Term.fpSqrt? [Ω] (rm fp : Term) : Env Term

fpSqrt lifted over nullables, strictly: none unless every argument is some.

Equations

• rm.fpSqrt? fp = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_SQRT #[rm, fp]

def Cvc.Untyped.Term.fpGt? [Ω] (lft rgt : Term) : Env Term

fpGt lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.fpGt? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_GT #[lft, rgt]

def Cvc.Untyped.Term.fpIsNan? [Ω] (fp : Term) : Env Term

fpIsNan lifted over nullables, strictly: none unless every argument is some.

Equations

• fp.fpIsNan? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_IS_NAN #[fp]

def Cvc.Untyped.Term.fpFma? [Ω] (rm a b c : Term) : Env Term

fpFma lifted over nullables, strictly: none unless every argument is some.

Equations

• rm.fpFma? a b c = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_FMA #[rm, a, b, c]

def Cvc.Untyped.Term.fpLe? [Ω] (lft rgt : Term) : Env Term

fpLe lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.fpLe? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_LEQ #[lft, rgt]

def Cvc.Untyped.Term.fpToReal? [Ω] (fp : Term) : Env Term

fpToReal lifted over nullables, strictly: none unless every argument is some.

Equations

• fp.fpToReal? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_TO_REAL #[fp]

def Cvc.Untyped.Term.fpRti? [Ω] (rm fp : Term) : Env Term

fpRti lifted over nullables, strictly: none unless every argument is some.

Equations

• rm.fpRti? fp = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_RTI #[rm, fp]

def Cvc.Untyped.Term.fpGe? [Ω] (lft rgt : Term) : Env Term

fpGe lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.fpGe? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_GEQ #[lft, rgt]

def Cvc.Untyped.Term.fpAbs? [Ω] (fp : Term) : Env Term

fpAbs lifted over nullables, strictly: none unless every argument is some.

Equations

• fp.fpAbs? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_ABS #[fp]

def Cvc.Untyped.Term.fpEq? [Ω] (lft rgt : Term) : Env Term

fpEq lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.fpEq? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_EQ #[lft, rgt]

def Cvc.Untyped.Term.fpSub? [Ω] (rm lft rgt : Term) : Env Term

fpSub lifted over nullables, strictly: none unless every argument is some.

Equations

• rm.fpSub? lft rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_SUB #[rm, lft, rgt]

def Cvc.Untyped.Term.fpIsNeg? [Ω] (fp : Term) : Env Term

fpIsNeg lifted over nullables, strictly: none unless every argument is some.

Equations

• fp.fpIsNeg? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_IS_NEG #[fp]

def Cvc.Untyped.Term.fpMul? [Ω] (rm lft rgt : Term) : Env Term

fpMul lifted over nullables, strictly: none unless every argument is some.

Equations

• rm.fpMul? lft rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_MULT #[rm, lft, rgt]

def Cvc.Untyped.Term.fpIsPos? [Ω] (fp : Term) : Env Term

fpIsPos lifted over nullables, strictly: none unless every argument is some.

Equations

• fp.fpIsPos? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_IS_POS #[fp]

def Cvc.Untyped.Term.fpNeg? [Ω] (fp : Term) : Env Term

fpNeg lifted over nullables, strictly: none unless every argument is some.

Equations

• fp.fpNeg? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_NEG #[fp]

def Cvc.Untyped.Term.fpMin? [Ω] (lft rgt : Term) : Env Term

fpMin lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.fpMin? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_MIN #[lft, rgt]

def Cvc.Untyped.Term.fpIsZero? [Ω] (fp : Term) : Env Term

fpIsZero lifted over nullables, strictly: none unless every argument is some.

Equations

• fp.fpIsZero? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_IS_ZERO #[fp]

def Cvc.Untyped.Term.fpLt? [Ω] (lft rgt : Term) : Env Term

fpLt lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.fpLt? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_LT #[lft, rgt]

def Cvc.Untyped.Term.fpAdd? [Ω] (rm lft rgt : Term) : Env Term

fpAdd lifted over nullables, strictly: none unless every argument is some.

Equations

• rm.fpAdd? lft rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_ADD #[rm, lft, rgt]

def Cvc.Untyped.Term.fpIsNormal? [Ω] (fp : Term) : Env Term

fpIsNormal lifted over nullables, strictly: none unless every argument is some.

Equations

• fp.fpIsNormal? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_IS_NORMAL #[fp]

def Cvc.Untyped.Term.fpIsInf? [Ω] (fp : Term) : Env Term

fpIsInf lifted over nullables, strictly: none unless every argument is some.

Equations

• fp.fpIsInf? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.FLOATINGPOINT_IS_INF #[fp]