17package com.microsoft.z3;
30 Native.IntPtr res =
new Native.IntPtr();
31 if (!Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res))
32 throw new Z3Exception(
"Sign is not a Boolean value");
33 return res.value != 0;
42 return new BitVecExpr(getContext(), Native.fpaGetNumeralSignBv(getContext().nCtx(), getNativeObject()));
52 return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
64 Native.LongPtr res =
new Native.LongPtr();
65 if (!Native.fpaGetNumeralSignificandUint64(getContext().nCtx(), getNativeObject(), res))
66 throw new Z3Exception(
"Significand is not a 64 bit unsigned integer");
76 return new BitVecExpr(getContext(), Native.fpaGetNumeralSignificandBv(getContext().nCtx(), getNativeObject()));
85 return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject(), biased);
94 Native.LongPtr res =
new Native.LongPtr();
95 if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res, biased))
96 throw new Z3Exception(
"Exponent is not a 64 bit integer");
106 return new BitVecExpr(getContext(), Native.fpaGetNumeralExponentBv(getContext().nCtx(), getNativeObject(), biased));
117 return Native.fpaIsNumeralNan(getContext().nCtx(), getNativeObject());
127 return Native.fpaIsNumeralInf(getContext().nCtx(), getNativeObject());
137 return Native.fpaIsNumeralZero(getContext().nCtx(), getNativeObject());
147 return Native.fpaIsNumeralNormal(getContext().nCtx(), getNativeObject());
157 return Native.fpaIsNumeralSubnormal(getContext().nCtx(), getNativeObject());
167 return Native.fpaIsNumeralPositive(getContext().nCtx(), getNativeObject());
177 return Native.fpaIsNumeralNegative(getContext().nCtx(), getNativeObject());
191 return Native.getNumeralString(getContext().nCtx(), getNativeObject());
BitVecExpr getExponentBV(boolean biased)
String getExponent(boolean biased)
long getExponentInt64(boolean biased)
BitVecExpr getSignificandBV()
FPNum(Context ctx, long obj)
long getSignificandUInt64()
def String(name, ctx=None)