mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Refactored FPA numeral accessors.
This commit is contained in:
parent
0a11e8f3c0
commit
abcb6040d4
|
@ -946,7 +946,7 @@ extern "C" {
|
|||
fpa_util & fu = mk_c(c)->fpautil();
|
||||
api::context * ctx = mk_c(c);
|
||||
expr * e = to_expr(t);
|
||||
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) {
|
||||
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
|
@ -956,6 +956,7 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
std::cout << "val=" << mpfm.to_string(val) << std::endl;
|
||||
app * a;
|
||||
if (mpfm.is_pos(val))
|
||||
a = ctx->bvutil().mk_numeral(0, 1);
|
||||
|
@ -966,44 +967,6 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_exponent_bv(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(t, 0);
|
||||
CHECK_VALID_AST(t, 0);
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
|
||||
family_id fid = mk_c(c)->get_fpa_fid();
|
||||
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
|
||||
fpa_util & fu = mk_c(c)->fpautil();
|
||||
expr * e = to_expr(t);
|
||||
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
scoped_mpf val(mpfm);
|
||||
bool r = plugin->is_numeral(e, val);
|
||||
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
unsigned ebits = val.get().get_ebits();
|
||||
mpf_exp_t q = mpfm.exp(val);
|
||||
mpf_exp_t q_biassed = mpfm.bias_exp(ebits, q);
|
||||
app * a;
|
||||
if (mpfm.is_inf(val))
|
||||
a = mk_c(c)->bvutil().mk_numeral(-1, ebits);
|
||||
else if (mpfm.is_zero(val) || mpfm.is_denormal(val))
|
||||
a = mk_c(c)->bvutil().mk_numeral(0, ebits);
|
||||
else
|
||||
a = mk_c(c)->bvutil().mk_numeral(q_biassed, ebits);
|
||||
mk_c(c)->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_significand_bv(c, t);
|
||||
|
@ -1018,7 +981,7 @@ extern "C" {
|
|||
SASSERT(plugin != 0);
|
||||
fpa_util & fu = mk_c(c)->fpautil();
|
||||
expr * e = to_expr(t);
|
||||
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !fu.is_fp(e)) {
|
||||
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
|
@ -1106,9 +1069,9 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t) {
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, Z3_bool biased) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_exponent_string(c, t);
|
||||
LOG_Z3_fpa_get_numeral_exponent_string(c, t, biased);
|
||||
RESET_ERROR_CODE();
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
|
@ -1127,19 +1090,21 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return "";
|
||||
}
|
||||
unsigned ebits = val.get().get_ebits();
|
||||
mpf_exp_t exp = mpfm.is_zero(val) ? 0 :
|
||||
mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) :
|
||||
mpfm.is_inf(val) ? mpfm.mk_top_exp(val.get().get_ebits()) :
|
||||
mpfm.exp(val);
|
||||
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
|
||||
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
|
||||
mpfm.bias_exp(ebits, mpfm.exp(val));
|
||||
if (!biased) mpfm.unbias_exp(ebits, exp);
|
||||
std::stringstream ss;
|
||||
ss << exp;
|
||||
return mk_c(c)->mk_external_string(ss.str());
|
||||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n) {
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n, Z3_bool biased) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n);
|
||||
LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n, biased);
|
||||
RESET_ERROR_CODE();
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
|
@ -1160,14 +1125,51 @@ extern "C" {
|
|||
*n = 0;
|
||||
return 0;
|
||||
}
|
||||
unsigned ebits = val.get().get_ebits();
|
||||
*n = mpfm.is_zero(val) ? 0 :
|
||||
mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) :
|
||||
mpfm.is_inf(val) ? mpfm.mk_top_exp(val.get().get_ebits()) :
|
||||
mpfm.exp(val);
|
||||
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
|
||||
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
|
||||
mpfm.bias_exp(ebits, mpfm.exp(val));
|
||||
if (!biased) *n = mpfm.unbias_exp(ebits, *n);
|
||||
return 1;
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, Z3_bool biased) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_exponent_bv(c, t, biased);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(t, 0);
|
||||
CHECK_VALID_AST(t, 0);
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
|
||||
family_id fid = mk_c(c)->get_fpa_fid();
|
||||
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
|
||||
fpa_util & fu = mk_c(c)->fpautil();
|
||||
expr * e = to_expr(t);
|
||||
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
scoped_mpf val(mpfm);
|
||||
bool r = plugin->is_numeral(e, val);
|
||||
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
unsigned ebits = val.get().get_ebits();
|
||||
mpf_exp_t exp = mpfm.is_zero(val) ? 0 :
|
||||
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
|
||||
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
|
||||
mpfm.bias_exp(ebits, mpfm.exp(val));
|
||||
if (!biased) exp = mpfm.unbias_exp(ebits, exp);
|
||||
app * a = mk_c(c)->bvutil().mk_numeral(exp, ebits);
|
||||
mk_c(c)->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_to_ieee_bv(c, t);
|
||||
|
|
|
@ -33,7 +33,7 @@ namespace Microsoft.Z3
|
|||
/// <remarks>
|
||||
/// NaN's do not have a bit-vector sign, so they are invalid arguments.
|
||||
/// </remarks>
|
||||
public BitVecExpr BVSign
|
||||
public BitVecExpr SignBV
|
||||
{
|
||||
get
|
||||
{
|
||||
|
@ -41,34 +41,6 @@ namespace Microsoft.Z3
|
|||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// The exponent of a floating-point numeral as a bit-vector expression
|
||||
/// </summary>
|
||||
/// <remarks>
|
||||
/// +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments.
|
||||
/// </remarks>
|
||||
public BitVecExpr BVExponent
|
||||
{
|
||||
get
|
||||
{
|
||||
return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject));
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// The significand of a floating-point numeral as a bit-vector expression
|
||||
/// </summary>
|
||||
/// <remarks>
|
||||
/// +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments.
|
||||
/// </remarks>
|
||||
public BitVecExpr BVSignificand
|
||||
{
|
||||
get
|
||||
{
|
||||
return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_significand_bv(Context.nCtx, NativeObject));
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Retrieves the sign of a floating-point literal
|
||||
/// </summary>
|
||||
|
@ -121,28 +93,47 @@ namespace Microsoft.Z3
|
|||
}
|
||||
|
||||
/// <summary>
|
||||
/// Return the exponent value of a floating-point numeral as a string
|
||||
/// The significand of a floating-point numeral as a bit-vector expression
|
||||
/// </summary>
|
||||
public string Exponent
|
||||
/// <remarks>
|
||||
/// +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments.
|
||||
/// </remarks>
|
||||
public BitVecExpr SignificandBV
|
||||
{
|
||||
get
|
||||
{
|
||||
return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject);
|
||||
return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_significand_bv(Context.nCtx, NativeObject));
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Return the (biased) exponent value of a floating-point numeral as a string
|
||||
/// </summary>
|
||||
public string Exponent(bool biased = true)
|
||||
{
|
||||
return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject, biased ? 1 : 0);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Return the exponent value of a floating-point numeral as a signed 64-bit integer
|
||||
/// </summary>
|
||||
public Int64 ExponentInt64
|
||||
public Int64 ExponentInt64(bool biased = true)
|
||||
{
|
||||
get
|
||||
{
|
||||
Int64 result = 0;
|
||||
if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result) == 0)
|
||||
throw new Z3Exception("Exponent is not a 64 bit integer");
|
||||
return result;
|
||||
}
|
||||
Int64 result = 0;
|
||||
if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result, biased ? 1 : 0) == 0)
|
||||
throw new Z3Exception("Exponent is not a 64 bit integer");
|
||||
return result;
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// The exponent of a floating-point numeral as a bit-vector expression
|
||||
/// </summary>
|
||||
/// <remarks>
|
||||
/// +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments.
|
||||
/// </remarks>
|
||||
public BitVecExpr ExponentBV(bool biased = true)
|
||||
{
|
||||
return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_exponent_bv(Context.nCtx, NativeObject, biased ? 1 : 0));
|
||||
}
|
||||
|
||||
#region Internal
|
||||
|
|
|
@ -20,34 +20,7 @@ package com.microsoft.z3;
|
|||
* FloatingPoint Numerals
|
||||
*/
|
||||
public class FPNum extends FPExpr
|
||||
{
|
||||
/**
|
||||
* The sign of a floating-point numeral as a bit-vector expression
|
||||
* Remarks: NaN's do not have a bit-vector sign, so they are invalid arguments.
|
||||
* @throws Z3Exception
|
||||
*/
|
||||
public BitVecExpr getBVSign() {
|
||||
return new BitVecExpr(getContext(), Native.fpaGetNumeralSignBv(getContext().nCtx(), getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
* The exponent of a floating-point numeral as a bit-vector expression
|
||||
* Remarks: +oo, -oo, and NaN's do not have a bit-vector exponent, so they are invalid arguments.
|
||||
* @throws Z3Exception
|
||||
*/
|
||||
public BitVecExpr getBVExponent() {
|
||||
return new BitVecExpr(getContext(), Native.fpaGetNumeralExponentBv(getContext().nCtx(), getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
* The significand of a floating-point numeral as a bit-vector expression
|
||||
* Remarks: +oo, -oo, and NaN's do not have a bit-vector significand, so they are invalid arguments.
|
||||
* @throws Z3Exception
|
||||
*/
|
||||
public BitVecExpr getBVSignificand() {
|
||||
return new BitVecExpr(getContext(), Native.fpaGetNumeralSignificandBv(getContext().nCtx(), getNativeObject()));
|
||||
}
|
||||
|
||||
{
|
||||
/**
|
||||
* Retrieves the sign of a floating-point literal
|
||||
* Remarks: returns true if the numeral is negative
|
||||
|
@ -60,6 +33,15 @@ public class FPNum extends FPExpr
|
|||
return res.value != 0;
|
||||
}
|
||||
|
||||
/**
|
||||
* The sign of a floating-point numeral as a bit-vector expression
|
||||
* Remarks: NaN's do not have a bit-vector sign, so they are invalid arguments.
|
||||
* @throws Z3Exception
|
||||
*/
|
||||
public BitVecExpr getSignBV() {
|
||||
return new BitVecExpr(getContext(), Native.fpaGetNumeralSignBv(getContext().nCtx(), getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
* The significand value of a floating-point numeral as a string
|
||||
* Remarks: The significand s is always 0 < s < 2.0; the resulting string is long
|
||||
|
@ -84,25 +66,45 @@ public class FPNum extends FPExpr
|
|||
throw new Z3Exception("Significand is not a 64 bit unsigned integer");
|
||||
return res.value;
|
||||
}
|
||||
|
||||
/**
|
||||
* The significand of a floating-point numeral as a bit-vector expression
|
||||
* Remarks: NaN is an invalid argument.
|
||||
* @throws Z3Exception
|
||||
*/
|
||||
public BitVecExpr getSignificandBV() {
|
||||
return new BitVecExpr(getContext(), Native.fpaGetNumeralSignificandBv(getContext().nCtx(), getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
* Return the exponent value of a floating-point numeral as a string
|
||||
* Remarks: NaN is an invalid argument.
|
||||
* @throws Z3Exception
|
||||
*/
|
||||
public String getExponent() {
|
||||
return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject());
|
||||
public String getExponent(boolean biased) {
|
||||
return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject(), biased);
|
||||
}
|
||||
|
||||
/**
|
||||
* Return the exponent value of a floating-point numeral as a signed 64-bit integer
|
||||
* Remarks: NaN is an invalid argument.
|
||||
* @throws Z3Exception
|
||||
*/
|
||||
public long getExponentInt64() {
|
||||
public long getExponentInt64(boolean biased) {
|
||||
Native.LongPtr res = new Native.LongPtr();
|
||||
if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res))
|
||||
if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res, biased))
|
||||
throw new Z3Exception("Exponent is not a 64 bit integer");
|
||||
return res.value;
|
||||
}
|
||||
|
||||
/**
|
||||
* The exponent of a floating-point numeral as a bit-vector expression
|
||||
* Remarks: NaN is an invalid argument.
|
||||
* @throws Z3Exception
|
||||
*/
|
||||
public BitVecExpr getExponentBV(boolean biased) {
|
||||
return new BitVecExpr(getContext(), Native.fpaGetNumeralExponentBv(getContext().nCtx(), getNativeObject(), biased));
|
||||
}
|
||||
|
||||
public FPNum(Context ctx, long obj)
|
||||
{
|
||||
|
|
|
@ -8445,31 +8445,7 @@ class FPNumRef(FPRef):
|
|||
def isNegative(self):
|
||||
k = self.decl().kind()
|
||||
return (self.num_args() == 0 and (k == Z3_OP_FPA_MINUS_INF or k == Z3_OP_FPA_MINUS_ZERO)) or (self.sign() == True)
|
||||
|
||||
"""
|
||||
The sign of a floating-point numeral as a bit-vector expression
|
||||
|
||||
Remark: NaN's do not have a bit-vector sign, so they are invalid arguments.
|
||||
"""
|
||||
def BVSign(self):
|
||||
return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), ctx)
|
||||
|
||||
"""
|
||||
The exponent of a floating-point numeral as a bit-vector expression
|
||||
|
||||
Remark: +oo, -oo and NaN's do not have a bit-vector exponent, so they are invalid arguments.
|
||||
"""
|
||||
def BVExponent(self):
|
||||
return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast()), ctx)
|
||||
|
||||
"""
|
||||
The sign of a floating-point numeral as a bit-vector expression
|
||||
|
||||
Remark: +oo, -oo and NaN's do not have a bit-vector significand, so they are invalid arguments.
|
||||
"""
|
||||
def BVSignificand(self):
|
||||
return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), ctx)
|
||||
|
||||
"""
|
||||
The sign of the numeral.
|
||||
|
||||
|
@ -8486,6 +8462,15 @@ class FPNumRef(FPRef):
|
|||
raise Z3Exception("error retrieving the sign of a numeral.")
|
||||
return l.value != 0
|
||||
|
||||
"""
|
||||
The sign of a floating-point numeral as a bit-vector expression
|
||||
|
||||
Remark: NaN's are invalid arguments.
|
||||
"""
|
||||
def sign_as_bv(self):
|
||||
return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx)
|
||||
|
||||
|
||||
"""
|
||||
The significand of the numeral.
|
||||
|
||||
|
@ -8495,6 +8480,14 @@ class FPNumRef(FPRef):
|
|||
"""
|
||||
def significand(self):
|
||||
return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast())
|
||||
|
||||
"""
|
||||
The significand of a floating-point numeral as a bit-vector expression
|
||||
|
||||
Remark: NaN are invalid arguments.
|
||||
"""
|
||||
def significand_as_bv(self):
|
||||
return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx)
|
||||
|
||||
"""
|
||||
The exponent of the numeral.
|
||||
|
@ -8503,8 +8496,8 @@ class FPNumRef(FPRef):
|
|||
>>> x.exponent()
|
||||
1
|
||||
"""
|
||||
def exponent(self):
|
||||
return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast())
|
||||
def exponent(self, biased=True):
|
||||
return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased)
|
||||
|
||||
"""
|
||||
The exponent of the numeral as a long.
|
||||
|
@ -8513,12 +8506,21 @@ class FPNumRef(FPRef):
|
|||
>>> x.exponent_as_long()
|
||||
1
|
||||
"""
|
||||
def exponent_as_long(self):
|
||||
def exponent_as_long(self, biased=True):
|
||||
ptr = (ctypes.c_longlong * 1)()
|
||||
if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr):
|
||||
if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr, biased):
|
||||
raise Z3Exception("error retrieving the exponent of a numeral.")
|
||||
return ptr[0]
|
||||
|
||||
"""
|
||||
The exponent of a floating-point numeral as a bit-vector expression
|
||||
|
||||
Remark: NaNs are invalid arguments.
|
||||
"""
|
||||
def exponent_as_bv(self, biased=True):
|
||||
return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx)
|
||||
|
||||
|
||||
"""
|
||||
The string representation of the numeral.
|
||||
|
||||
|
@ -8527,7 +8529,7 @@ class FPNumRef(FPRef):
|
|||
1.25*(2**4)
|
||||
"""
|
||||
def as_string(self):
|
||||
s = Z3_fpa_get_numeral_string(self.ctx.ref(), self.as_ast())
|
||||
s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast())
|
||||
return ("FPVal(%s, %s)" % (s, self.sort()))
|
||||
|
||||
def is_fp(a):
|
||||
|
|
|
@ -620,8 +620,8 @@ class Formatter:
|
|||
r = []
|
||||
sgn = c_int(0)
|
||||
sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn))
|
||||
exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast, False)
|
||||
sig = Z3_fpa_get_numeral_significand_string(a.ctx_ref(), a.ast)
|
||||
exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast)
|
||||
r.append(to_format('FPVal('))
|
||||
if sgnb and sgn.value != 0:
|
||||
r.append(to_format('-'))
|
||||
|
@ -650,8 +650,8 @@ class Formatter:
|
|||
r = []
|
||||
sgn = (ctypes.c_int)(0)
|
||||
sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn))
|
||||
exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast, False)
|
||||
sig = Z3_fpa_get_numeral_significand_string(a.ctx_ref(), a.ast)
|
||||
exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast)
|
||||
if sgnb and sgn.value != 0:
|
||||
r.append(to_format('-'))
|
||||
r.append(to_format(sig))
|
||||
|
|
|
@ -900,24 +900,12 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
Remarks: +oo, -oo and NaN are invalid arguments.
|
||||
Remarks: NaN is an invalid argument.
|
||||
|
||||
def_API('Z3_fpa_get_numeral_significand_bv', AST, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Retrieves the exponent of a floating-point literal as a bit-vector expression.
|
||||
|
||||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
Remarks: +oo, -oo and NaN are invalid arguments.
|
||||
|
||||
def_API('Z3_fpa_get_numeral_exponent_bv', AST, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Retrieves the sign of a floating-point literal.
|
||||
|
||||
|
@ -954,23 +942,25 @@ extern "C" {
|
|||
|
||||
Remarks: This function extracts the significand bits in `t`, without the
|
||||
hidden bit or normalization. Sets the Z3_INVALID_ARG error code if the
|
||||
significand does not fit into a uint64.
|
||||
significand does not fit into a uint64. NaN is an invalid argument.
|
||||
|
||||
def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, __uint64 * n);
|
||||
|
||||
/**
|
||||
\brief Return the exponent value of a floating-point numeral as a string
|
||||
\brief Return the exponent value of a floating-point numeral as a string.
|
||||
|
||||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
\param biased flag to indicate whether the result is in biased representation
|
||||
|
||||
Remarks: This function extracts the exponent in `t`, without normalization.
|
||||
NaN is an invalid argument.
|
||||
|
||||
def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST)))
|
||||
def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST), _in(BOOL)))
|
||||
*/
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t);
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, Z3_bool biased);
|
||||
|
||||
/**
|
||||
\brief Return the exponent value of a floating-point numeral as a signed 64-bit integer
|
||||
|
@ -978,12 +968,28 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
\param n exponent
|
||||
\param biased flag to indicate whether the result is in biased representation
|
||||
|
||||
Remarks: This function extracts the exponent in `t`, without normalization.
|
||||
NaN is an invalid argument.
|
||||
|
||||
def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64)))
|
||||
def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64), _in(BOOL)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n);
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n, Z3_bool biased);
|
||||
|
||||
/**
|
||||
\brief Retrieves the exponent of a floating-point literal as a bit-vector expression.
|
||||
|
||||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
\param biased flag to indicate whether the result is in biased representation
|
||||
|
||||
Remarks: This function extracts the exponent in `t`, without normalization.
|
||||
NaN is an invalid arguments.
|
||||
|
||||
def_API('Z3_fpa_get_numeral_exponent_bv', AST, (_in(CONTEXT), _in(AST), _in(BOOL)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, Z3_bool biased);
|
||||
|
||||
/**
|
||||
\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
|
||||
|
|
Loading…
Reference in a new issue