17package com.microsoft.z3;
32 throw new Z3Exception(
"Sign is not a Boolean value");
33 return res.value != 0;
66 throw new Z3Exception(
"Significand is not a 64 bit unsigned integer");
96 throw new Z3Exception(
"Exponent is not a 64 bit integer");
BitVecExpr getExponentBV(boolean biased)
String getExponent(boolean biased)
long getExponentInt64(boolean biased)
BitVecExpr getSignificandBV()
FPNum(Context ctx, long obj)
long getSignificandUInt64()
static boolean fpaIsNumeralZero(long a0, long a1)
static boolean fpaGetNumeralSign(long a0, long a1, IntPtr a2)
static String fpaGetNumeralSignificandString(long a0, long a1)
static long fpaGetNumeralSignificandBv(long a0, long a1)
static boolean fpaIsNumeralNan(long a0, long a1)
static boolean fpaGetNumeralSignificandUint64(long a0, long a1, LongPtr a2)
static boolean fpaIsNumeralSubnormal(long a0, long a1)
static boolean fpaIsNumeralNormal(long a0, long a1)
static long fpaGetNumeralSignBv(long a0, long a1)
static boolean fpaGetNumeralExponentInt64(long a0, long a1, LongPtr a2, boolean a3)
static String getNumeralString(long a0, long a1)
static boolean fpaIsNumeralPositive(long a0, long a1)
static boolean fpaIsNumeralNegative(long a0, long a1)
static boolean fpaIsNumeralInf(long a0, long a1)
static String fpaGetNumeralExponentString(long a0, long a1, boolean a2)
static long fpaGetNumeralExponentBv(long a0, long a1, boolean a2)
def String(name, ctx=None)