mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-08 15:13:23 +00:00
Code Activity

FPA API: numerals, .NET and Java

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-10 17:28:07 +00:00
parent 3391c9c44c
commit ee0ec7fe3a
16 changed files with 770 additions and 175 deletions
Download patch file Download diff file Expand all files Collapse all files

89
src/api/api_fpa.cpp
View file

@ -200,7 +200,8 @@ extern "C" {
LOG_Z3_mk_fpa_inf(c, s, negative); LOG_Z3_mk_fpa_inf(c, s, negative);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(negative != 0 ? ctx->fpa_util().mk_ninf(to_sort(s)) : ctx->fpa_util().mk_pinf(to_sort(s))); Z3_ast r = of_ast(negative != 0 ? ctx->fpa_util().mk_ninf(to_sort(s)) :
ctx->fpa_util().mk_pinf(to_sort(s)));
RETURN_Z3(r); RETURN_Z3(r);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -210,7 +211,8 @@ extern "C" {
LOG_Z3_mk_fpa_inf(c, s, negative); LOG_Z3_mk_fpa_inf(c, s, negative);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
Z3_ast r = of_ast(negative != 0 ? ctx->fpa_util().mk_nzero(to_sort(s)) : ctx->fpa_util().mk_pzero(to_sort(s))); Z3_ast r = of_ast(negative != 0 ? ctx->fpa_util().mk_nzero(to_sort(s)) :
ctx->fpa_util().mk_pzero(to_sort(s)));
RETURN_Z3(r); RETURN_Z3(r);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -231,7 +233,10 @@ extern "C" {
RESET_ERROR_CODE(); RESET_ERROR_CODE();
api::context * ctx = mk_c(c); api::context * ctx = mk_c(c);
scoped_mpf tmp(ctx->fpa_util().fm()); scoped_mpf tmp(ctx->fpa_util().fm());
ctx->fpa_util().fm().set(tmp, ctx->fpa_util().get_ebits(to_sort(ty)), ctx->fpa_util().get_sbits(to_sort(ty)), v); ctx->fpa_util().fm().set(tmp,
ctx->fpa_util().get_ebits(to_sort(ty)),
ctx->fpa_util().get_sbits(to_sort(ty)),
v);
Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp)); Z3_ast r = of_ast(ctx->fpa_util().mk_value(tmp));
RETURN_Z3(r); RETURN_Z3(r);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
@ -667,6 +672,84 @@ extern "C" {
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
Z3_bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int * sgn) {
Z3_TRY;
LOG_Z3_fpa_get_numeral_sign(c, t, sgn);
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
scoped_mpf val(mpfm);
bool r = plugin->is_numeral(to_expr(t), val);
*sgn = (mpfm.is_nan(val)) ? 0 : mpfm.sgn(val);
return r;
Z3_CATCH_RETURN(0);
}
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_get_numeral_significand_string(c, t);
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
scoped_mpf val(mpfm);
if (!plugin->is_numeral(to_expr(t), val)) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return "";
}
unsigned sbits = val.get().get_sbits();
scoped_mpq q(mpqm);
mpqm.set(q, mpfm.sig(val));
mpqm.div(q, mpfm.m_powers2(sbits - 1), q);
std::stringstream ss;
mpqm.display_decimal(ss, q, sbits);
return mk_c(c)->mk_external_string(ss.str());
Z3_CATCH_RETURN("");
}
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_get_numeral_exponent_string(c, t);
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
scoped_mpf val(mpfm);
bool r = plugin->is_numeral(to_expr(t), val);
if (!r) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return "";
}
const mpf_exp_t exp = mpfm.exp(val);
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(__in Z3_context c, __in Z3_ast t, __out __int64 * n) {
Z3_TRY;
LOG_Z3_fpa_get_numeral_exponent_string(c, t);
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
scoped_mpf val(mpfm);
bool r = plugin->is_numeral(to_expr(t), val);
if (!r) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
*n = mpfm.exp(val);
return 1;
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t) { Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t) {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_fpa_to_ieee_bv(c, t); LOG_Z3_mk_fpa_to_ieee_bv(c, t);

29
src/api/api_numeral.cpp
View file

@ -76,8 +76,7 @@ extern "C" {
++m; ++m;
} }
ast * a = 0; ast * a = 0;
if (_ty->get_family_id() == mk_c(c)->get_fpa_fid()) if (_ty->get_family_id() == mk_c(c)->get_fpa_fid()) {
{
// avoid expanding floats into huge rationals. // avoid expanding floats into huge rationals.
fpa_util & fu = mk_c(c)->fpa_util(); fpa_util & fu = mk_c(c)->fpa_util();
scoped_mpf t(fu.fm()); scoped_mpf t(fu.fm());
@ -149,7 +148,8 @@ extern "C" {
return return
mk_c(c)->autil().is_numeral(e) || mk_c(c)->autil().is_numeral(e) ||
mk_c(c)->bvutil().is_numeral(e) || mk_c(c)->bvutil().is_numeral(e) ||
mk_c(c)->fpa_util().is_numeral(e); mk_c(c)->fpa_util().is_numeral(e) ||
mk_c(c)->fpa_util().is_rm_numeral(e);
Z3_CATCH_RETURN(Z3_FALSE); Z3_CATCH_RETURN(Z3_FALSE);
} }
@ -193,7 +193,28 @@ extern "C" {
// floats are separated from all others to avoid huge rationals. // floats are separated from all others to avoid huge rationals.
fpa_util & fu = mk_c(c)->fpa_util(); fpa_util & fu = mk_c(c)->fpa_util();
scoped_mpf tmp(fu.fm()); scoped_mpf tmp(fu.fm());
if (mk_c(c)->fpa_util().is_numeral(to_expr(a), tmp)) { mpf_rounding_mode rm;
if (mk_c(c)->fpa_util().is_rm_numeral(to_expr(a), rm)) {
switch (rm) {
case OP_FPA_RM_NEAREST_TIES_TO_EVEN:
return mk_c(c)->mk_external_string("roundNearestTiesToEven");
break;
case OP_FPA_RM_NEAREST_TIES_TO_AWAY:
return mk_c(c)->mk_external_string("roundNearestTiesToAway");
break;
case OP_FPA_RM_TOWARD_POSITIVE:
return mk_c(c)->mk_external_string("roundTowardPositive");
break;
case OP_FPA_RM_TOWARD_NEGATIVE:
return mk_c(c)->mk_external_string("roundTowardNegative");
break;
case OP_FPA_RM_TOWARD_ZERO:
default:
return mk_c(c)->mk_external_string("roundTowardZero");
break;
}
}
else if (mk_c(c)->fpa_util().is_numeral(to_expr(a), tmp)) {
return mk_c(c)->mk_external_string(fu.fm().to_string(tmp)); return mk_c(c)->mk_external_string(fu.fm().to_string(tmp));
} }
else { else {

36
src/api/dotnet/Context.cs
View file

@ -3465,82 +3465,82 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. /// Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
/// </summary> /// </summary>
public FPRMExpr MkFPRNE() public FPRMNum MkFPRNE()
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return new FPRMExpr(this, Native.Z3_mk_fpa_rne(nCtx)); return new FPRMNum(this, Native.Z3_mk_fpa_rne(nCtx));
} }
/// <summary> /// <summary>
/// Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. /// Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
/// </summary> /// </summary>
public FPRMExpr MkFPRoundNearestTiesToAway() public FPRMNum MkFPRoundNearestTiesToAway()
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx)); return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
} }
/// <summary> /// <summary>
/// Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. /// Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
/// </summary> /// </summary>
public FPRMExpr MkFPRNA() public FPRMNum MkFPRNA()
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return new FPRMExpr(this, Native.Z3_mk_fpa_rna(nCtx)); return new FPRMNum(this, Native.Z3_mk_fpa_rna(nCtx));
} }
/// <summary> /// <summary>
/// Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. /// Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
/// </summary> /// </summary>
public FPRMExpr MkFPRoundTowardPositive() public FPRMNum MkFPRoundTowardPositive()
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return new FPRMExpr(this, Native.Z3_mk_fpa_round_toward_positive(nCtx)); return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
} }
/// <summary> /// <summary>
/// Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. /// Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
/// </summary> /// </summary>
public FPRMExpr MkFPRTP() public FPRMNum MkFPRTP()
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return new FPRMExpr(this, Native.Z3_mk_fpa_rtp(nCtx)); return new FPRMNum(this, Native.Z3_mk_fpa_rtp(nCtx));
} }
/// <summary> /// <summary>
/// Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. /// Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
/// </summary> /// </summary>
public FPRMExpr MkFPRoundTowardNegative() public FPRMNum MkFPRoundTowardNegative()
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return new FPRMExpr(this, Native.Z3_mk_fpa_round_toward_negative(nCtx)); return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
} }
/// <summary> /// <summary>
/// Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. /// Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
/// </summary> /// </summary>
public FPRMExpr MkFPRTN() public FPRMNum MkFPRTN()
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return new FPRMExpr(this, Native.Z3_mk_fpa_rtn(nCtx)); return new FPRMNum(this, Native.Z3_mk_fpa_rtn(nCtx));
} }
/// <summary> /// <summary>
/// Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. /// Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
/// </summary> /// </summary>
public FPRMExpr MkFPRoundTowardZero() public FPRMNum MkFPRoundTowardZero()
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return new FPRMExpr(this, Native.Z3_mk_fpa_round_toward_zero(nCtx)); return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
} }
/// <summary> /// <summary>
/// Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. /// Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
/// </summary> /// </summary>
public FPRMExpr MkFPRTZ() public FPRMNum MkFPRTZ()
{ {
Contract.Ensures(Contract.Result<FPRMExpr>() != null); Contract.Ensures(Contract.Result<FPRMExpr>() != null);
return new FPRMExpr(this, Native.Z3_mk_fpa_rtz(nCtx)); return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx));
} }
#endregion #endregion
#endregion #endregion

9
src/api/dotnet/Expr.cs
View file

@ -1470,7 +1470,12 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Indicates whether the term is a floating-point numeral /// Indicates whether the term is a floating-point numeral
/// </summary> /// </summary>
public bool IsFPNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_NUM; } } public bool IsFPNumeral { get { return IsFP && IsNumeral; } }
/// <summary>
/// Indicates whether the term is a floating-point rounding mode numeral
/// </summary>
public bool IsFPRMNumeral { get { return IsFPRM && IsNumeral; } }
/// <summary> /// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
@ -1809,7 +1814,7 @@ namespace Microsoft.Z3
case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj); case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj);
case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj); case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPNum(ctx, obj); case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPNum(ctx, obj);
case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj); case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMNum(ctx, obj);
} }
} }

57
src/api/dotnet/FPNum.cs
View file

@ -27,6 +27,63 @@ namespace Microsoft.Z3
[ContractVerification(true)] [ContractVerification(true)]
public class FPNum : FPExpr public class FPNum : FPExpr
{ {
/// <summary>
/// Retrieves the sign of a floating-point literal
/// </summary>
/// <remarks>
/// Remarks: returns true if the numeral is negative
/// </remarks>
public bool Sign
{
get
{
int res = 0;
if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Sign is not a Boolean value");
return res != 0;
}
}
/// <summary>
/// The significand value of a floating-point numeral as a string
/// </summary>
/// <remarks>
/// The significand s is always 0 &lt; s &lt; 2.0; the resulting string is long
/// enough to represent the real significand precisely.
/// </remarks>
public string Significand
{
get
{
return Native.Z3_fpa_get_numeral_significand_string(Context.nCtx, NativeObject);
}
}
/// <summary>
/// Return the exponent value of a floating-point numeral as a string
/// </summary>
public string Exponent
{
get
{
return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject);
}
}
/// <summary>
/// Return the exponent value of a floating-point numeral as a signed 64-bit integer
/// </summary>
public Int64 ExponentInt64
{
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;
}
}
#region Internal #region Internal
internal FPNum(Context ctx, IntPtr obj) internal FPNum(Context ctx, IntPtr obj)
: base(ctx, obj) : base(ctx, obj)

50
src/api/dotnet/FPRMExpr.cs
View file

@ -30,56 +30,6 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public class FPRMExpr : Expr public class FPRMExpr : Expr
{ {
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
/// </summary>
public bool isRoundNearestTiesToEven { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
/// </summary>
public bool isRNE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
/// </summary>
public bool isRoundNearestTiesToAway { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
/// </summary>
public bool isRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundTowardPositive
/// </summary>
public bool isRoundTowardPositive { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundTowardPositive
/// </summary>
public bool isRTP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundTowardNegative
/// </summary>
public bool isRoundTowardNegative { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundTowardNegative
/// </summary>
public bool isRTN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundTowardZero
/// </summary>
public bool isRoundTowardZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundTowardZero
/// </summary>
public bool isRTZ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
#region Internal #region Internal
/// <summary> Constructor for FPRMExpr </summary> /// <summary> Constructor for FPRMExpr </summary>
internal FPRMExpr(Context ctx, IntPtr obj) internal FPRMExpr(Context ctx, IntPtr obj)

100
src/api/dotnet/FPRMNum.cs Normal file
View file

@ -0,0 +1,100 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
FPRMExpr.cs
Abstract:
Z3 Managed API: Floating Point Rounding Mode Numerals
Author:
Christoph Wintersteiger (cwinter) 2013-06-10
Notes:
--*/
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Floating-point rounding mode numerals
/// </summary>
public class FPRMNum : FPRMExpr
{
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
/// </summary>
public bool isRoundNearestTiesToEven { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
/// </summary>
public bool isRNE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
/// </summary>
public bool isRoundNearestTiesToAway { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
/// </summary>
public bool isRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundTowardPositive
/// </summary>
public bool isRoundTowardPositive { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundTowardPositive
/// </summary>
public bool isRTP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundTowardNegative
/// </summary>
public bool isRoundTowardNegative { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundTowardNegative
/// </summary>
public bool isRTN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundTowardZero
/// </summary>
public bool isRoundTowardZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
/// <summary>
/// Indicates whether the term is the floating-point rounding numeral roundTowardZero
/// </summary>
public bool isRTZ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
/// <summary>
/// Returns a string representation of the numeral.
/// </summary>
public override string ToString()
{
return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
}
#region Internal
/// <summary> Constructor for FPRMNum </summary>
internal FPRMNum(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
}

40
src/api/java/Context.java
View file

@ -2865,90 +2865,90 @@ public class Context extends IDisposable
* Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. * Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
* @throws Z3Exception on error * @throws Z3Exception on error
**/ **/
public FPRMExpr mkFPRoundNearestTiesToEven() throws Z3Exception public FPRMNum mkFPRoundNearestTiesToEven() throws Z3Exception
{ {
return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx())); return new FPRMNum(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
} }
/** /**
* Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. * Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
* @throws Z3Exception * @throws Z3Exception
**/ **/
public FPRMExpr mkFPRNE() throws Z3Exception public FPRMNum mkFPRNE() throws Z3Exception
{ {
return new FPRMExpr(this, Native.mkFpaRne(nCtx())); return new FPRMNum(this, Native.mkFpaRne(nCtx()));
} }
/** /**
* Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. * Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
* @throws Z3Exception * @throws Z3Exception
**/ **/
public FPRMExpr mkFPRoundNearestTiesToAway() throws Z3Exception public FPRMNum mkFPRoundNearestTiesToAway() throws Z3Exception
{ {
return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToAway(nCtx())); return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
} }
/** /**
* Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. * Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
* @throws Z3Exception * @throws Z3Exception
**/ **/
public FPRMExpr mkFPRNA() throws Z3Exception public FPRMNum mkFPRNA() throws Z3Exception
{ {
return new FPRMExpr(this, Native.mkFpaRna(nCtx())); return new FPRMNum(this, Native.mkFpaRna(nCtx()));
} }
/** /**
* Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. * Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
* @throws Z3Exception * @throws Z3Exception
**/ **/
public FPRMExpr mkFPRoundTowardPositive() throws Z3Exception public FPRMNum mkFPRoundTowardPositive() throws Z3Exception
{ {
return new FPRMExpr(this, Native.mkFpaRoundTowardPositive(nCtx())); return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
} }
/** /**
* Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode. * Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
* @throws Z3Exception * @throws Z3Exception
**/ **/
public FPRMExpr mkFPRTP() throws Z3Exception public FPRMNum mkFPRTP() throws Z3Exception
{ {
return new FPRMExpr(this, Native.mkFpaRtp(nCtx())); return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
} }
/** /**
* Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. * Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
* @throws Z3Exception * @throws Z3Exception
**/ **/
public FPRMExpr mkFPRoundTowardNegative() throws Z3Exception public FPRMNum mkFPRoundTowardNegative() throws Z3Exception
{ {
return new FPRMExpr(this, Native.mkFpaRoundTowardNegative(nCtx())); return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
} }
/** /**
* Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode. * Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
* @throws Z3Exception * @throws Z3Exception
**/ **/
public FPRMExpr mkFPRTN() throws Z3Exception public FPRMNum mkFPRTN() throws Z3Exception
{ {
return new FPRMExpr(this, Native.mkFpaRtn(nCtx())); return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
} }
/** /**
* Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. * Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
* @throws Z3Exception * @throws Z3Exception
**/ **/
public FPRMExpr mkFPRoundTowardZero() throws Z3Exception public FPRMNum mkFPRoundTowardZero() throws Z3Exception
{ {
return new FPRMExpr(this, Native.mkFpaRoundTowardZero(nCtx())); return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
} }
/** /**
* Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode. * Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
* @throws Z3Exception * @throws Z3Exception
**/ **/
public FPRMExpr mkFPRTZ() throws Z3Exception public FPRMNum mkFPRTZ() throws Z3Exception
{ {
return new FPRMExpr(this, Native.mkFpaRtz(nCtx())); return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
} }
/** FloatingPoint Sorts **/ /** FloatingPoint Sorts **/

230
src/api/java/Expr.java
View file

@ -1714,98 +1714,105 @@ public class Expr extends AST
* Indicates whether the terms is of floating-point sort. * Indicates whether the terms is of floating-point sort.
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFP() throws Z3Exception { return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_FLOATING_POINT_SORT; } public boolean isFP() throws Z3Exception { return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_FLOATING_POINT_SORT; }
/** /**
* Indicates whether the terms is of floating-point rounding mode sort. * Indicates whether the terms is of floating-point rounding mode sort.
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPRM() throws Z3Exception { return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ROUNDING_MODE_SORT; } public boolean isFPRM() throws Z3Exception { return Z3_sort_kind.fromInt(Native.getSortKind(getContext().nCtx(), Native.getSort(getContext().nCtx(), getNativeObject()))) == Z3_sort_kind.Z3_ROUNDING_MODE_SORT; }
/** /**
* Indicates whether the term is a floating-point numeral * Indicates whether the term is a floating-point numeral
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPNumeral() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_NUM; } public boolean isFPNumeral() throws Z3Exception { return isFP() && isNumeral(); }
/**
* Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
* @return
* @throws Z3Exception
*/
public boolean IsFPRMNumRoundNearestTiesToEven() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
/**
* Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
* @return
* @throws Z3Exception
*/
public boolean IsFPRMNumRoundNearestTiesToAway() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardNegative
* @return
* @throws Z3Exception
*/
public boolean IsFPRMNumRoundTowardNegative() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardPositive
* @return
* @throws Z3Exception
*/
public boolean IsFPRMNumRoundTowardPositive() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardZero
* @return
* @throws Z3Exception
*/
public boolean IsFPRMNumRoundTowardZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
/**
* Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
* @return
* @throws Z3Exception
*/
public boolean IsFPRMNumRNE() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
/**
* Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
* @return
* @throws Z3Exception
*/
public boolean IsFPRMNumRNA() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardNegative
* @return
* @throws Z3Exception
*/
public boolean IsFPRMNumRTN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardPositive
* @return
* @throws Z3Exception
*/
public boolean IsFPRMNumRTP() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardZero
* @return
* @throws Z3Exception
*/
public boolean IsFPRMNumRTZ() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
/** /**
* Indicates whether the term is a floating-point rounding mode numeral * Indicates whether the term is a floating-point rounding mode numeral
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPRMNum() throws Z3Exception { public boolean isFPRMNumeral() throws Z3Exception { return isFPRM() && isNumeral(); }
/**
* Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
* @return
* @throws Z3Exception
*/
public boolean isFPRMNumRoundNearestTiesToEven() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
/**
* Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
* @return
* @throws Z3Exception
*/
public boolean isFPRMNumRoundNearestTiesToAway() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardNegative
* @return
* @throws Z3Exception
*/
public boolean isFPRMNumRoundTowardNegative() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardPositive
* @return
* @throws Z3Exception
*/
public boolean isFPRMNumRoundTowardPositive() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardZero
* @return
* @throws Z3Exception
*/
public boolean isFPRMNumRoundTowardZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
/**
* Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
* @return
* @throws Z3Exception
*/
public boolean isFPRMNumRNE() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
/**
* Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
* @return
* @throws Z3Exception
*/
public boolean isFPRMNumRNA() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardNegative
* @return
* @throws Z3Exception
*/
public boolean isFPRMNumRTN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardPositive
* @return
* @throws Z3Exception
*/
public boolean isFPRMNumRTP() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardZero
* @return
* @throws Z3Exception
*/
public boolean isFPRMNumRTZ() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
/**
* Indicates whether the term is a floating-point rounding mode numeral
* @return
* @throws Z3Exception
*/
public boolean isFPRMNum() throws Z3Exception {
return isApp() && return isApp() &&
(getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY || (getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY ||
getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN || getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN ||
@ -1819,42 +1826,42 @@ public class Expr extends AST
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPPlusInfinity() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_PLUS_INF; } public boolean isFPPlusInfinity() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_PLUS_INF; }
/** /**
* Indicates whether the term is a floating-point -oo * Indicates whether the term is a floating-point -oo
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPMinusInfinity() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MINUS_INF; } public boolean isFPMinusInfinity() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MINUS_INF; }
/** /**
* Indicates whether the term is a floating-point NaN * Indicates whether the term is a floating-point NaN
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPNaN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_NAN; } public boolean isFPNaN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_NAN; }
/** /**
* Indicates whether the term is a floating-point +zero * Indicates whether the term is a floating-point +zero
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPPlusZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO; } public boolean isFPPlusZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO; }
/** /**
* Indicates whether the term is a floating-point -zero * Indicates whether the term is a floating-point -zero
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPMinusZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO; } public boolean isFPMinusZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO; }
/** /**
* Indicates whether the term is a floating-point addition term * Indicates whether the term is a floating-point addition term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPAdd() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ADD; } public boolean isFPAdd() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ADD; }
/** /**
@ -1862,211 +1869,210 @@ public class Expr extends AST
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPSub() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_SUB; } public boolean isFPSub() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_SUB; }
/** /**
* Indicates whether the term is a floating-point negation term * Indicates whether the term is a floating-point negation term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPNeg() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_NEG; } public boolean isFPNeg() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_NEG; }
/** /**
* Indicates whether the term is a floating-point multiplication term * Indicates whether the term is a floating-point multiplication term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPMul() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MUL; } public boolean isFPMul() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MUL; }
/** /**
* Indicates whether the term is a floating-point divison term * Indicates whether the term is a floating-point divison term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPDiv() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_DIV; } public boolean isFPDiv() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_DIV; }
/** /**
* Indicates whether the term is a floating-point remainder term * Indicates whether the term is a floating-point remainder term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPRem() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_REM; } public boolean isFPRem() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_REM; }
/** /**
* Indicates whether the term is a floating-point term absolute value term * Indicates whether the term is a floating-point term absolute value term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPAbs() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ABS; } public boolean isFPAbs() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ABS; }
/** /**
* Indicates whether the term is a floating-point minimum term * Indicates whether the term is a floating-point minimum term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPMin() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MIN; } public boolean isFPMin() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MIN; }
/** /**
* Indicates whether the term is a floating-point maximum term * Indicates whether the term is a floating-point maximum term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPMax() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MAX; } public boolean isFPMax() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_MAX; }
/** /**
* Indicates whether the term is a floating-point fused multiply-add term * Indicates whether the term is a floating-point fused multiply-add term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPFMA() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_FMA; } public boolean isFPFMA() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_FMA; }
/** /**
* Indicates whether the term is a floating-point square root term * Indicates whether the term is a floating-point square root term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPSqrt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_SQRT; } public boolean isFPSqrt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_SQRT; }
/** /**
* Indicates whether the term is a floating-point roundToIntegral term * Indicates whether the term is a floating-point roundToIntegral term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPRoundToIntegral() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ROUND_TO_INTEGRAL; } public boolean isFPRoundToIntegral() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_ROUND_TO_INTEGRAL; }
/** /**
* Indicates whether the term is a floating-point equality term * Indicates whether the term is a floating-point equality term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPEq() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_EQ; } public boolean isFPEq() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_EQ; }
/** /**
* Indicates whether the term is a floating-point less-than term * Indicates whether the term is a floating-point less-than term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPLt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_LT; } public boolean isFPLt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_LT; }
/** /**
* Indicates whether the term is a floating-point greater-than term * Indicates whether the term is a floating-point greater-than term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPGt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_GT; } public boolean isFPGt() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_GT; }
/** /**
* Indicates whether the term is a floating-point less-than or equal term * Indicates whether the term is a floating-point less-than or equal term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPLe() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_LE; } public boolean isFPLe() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_LE; }
/** /**
* Indicates whether the term is a floating-point greater-than or erqual term * Indicates whether the term is a floating-point greater-than or erqual term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPGe() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_GE; } public boolean isFPGe() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_GE; }
/** /**
* Indicates whether the term is a floating-point isNaN predicate term * Indicates whether the term is a floating-point isNaN predicate term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPisNaN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NAN; } public boolean isFPisNaN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NAN; }
/** /**
* Indicates whether the term is a floating-point isInf predicate term * Indicates whether the term is a floating-point isInf predicate term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPisInf() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_INF; } public boolean isFPisInf() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_INF; }
/** /**
* Indicates whether the term is a floating-point isZero predicate term * Indicates whether the term is a floating-point isZero predicate term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPisZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_ZERO; } public boolean isFPisZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_ZERO; }
/** /**
* Indicates whether the term is a floating-point isNormal term * Indicates whether the term is a floating-point isNormal term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPisNormal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NORMAL; } public boolean isFPisNormal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NORMAL; }
/** /**
* Indicates whether the term is a floating-point isSubnormal predicate term * Indicates whether the term is a floating-point isSubnormal predicate term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPisSubnormal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_SUBNORMAL; } public boolean isFPisSubnormal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_SUBNORMAL; }
/** /**
* Indicates whether the term is a floating-point isNegative predicate term * Indicates whether the term is a floating-point isNegative predicate term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPisNegative() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; } public boolean isFPisNegative() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; }
/** /**
* Indicates whether the term is a floating-point isPositive predicate term * Indicates whether the term is a floating-point isPositive predicate term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPisPositive() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; } public boolean isFPisPositive() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; }
/** /**
* Indicates whether the term is a floating-point constructor term * Indicates whether the term is a floating-point constructor term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPFP() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_FP; } public boolean isFPFP() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_FP; }
/** /**
* Indicates whether the term is a floating-point conversion term * Indicates whether the term is a floating-point conversion term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPToFp() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_FP; } public boolean isFPToFp() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_FP; }
/** /**
* Indicates whether the term is a floating-point conversion from unsigned bit-vector term * Indicates whether the term is a floating-point conversion from unsigned bit-vector term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPToFpUnsigned() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_FP_UNSIGNED; } public boolean isFPToFpUnsigned() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_FP_UNSIGNED; }
/** /**
* Indicates whether the term is a floating-point conversion to unsigned bit-vector term * Indicates whether the term is a floating-point conversion to unsigned bit-vector term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPToUBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_UBV; } public boolean isFPToUBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_UBV; }
/** /**
* Indicates whether the term is a floating-point conversion to signed bit-vector term * Indicates whether the term is a floating-point conversion to signed bit-vector term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPToSBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_SBV; } public boolean isFPToSBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_SBV; }
/** /**
* Indicates whether the term is a floating-point conversion to real term * Indicates whether the term is a floating-point conversion to real term
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPToReal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_REAL; } public boolean isFPToReal() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_REAL; }
/** /**
* Indicates whether the term is a floating-point conversion to IEEE-754 bit-vector term1 * Indicates whether the term is a floating-point conversion to IEEE-754 bit-vector term1
* @return * @return
* @throws Z3Exception * @throws Z3Exception
*/ */
public boolean IsFPToIEEEBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_IEEE_BV; } public boolean isFPToIEEEBV() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_TO_IEEE_BV; }
/** /**
@ -2140,6 +2146,8 @@ public class Expr extends AST
return new BitVecNum(ctx, obj); return new BitVecNum(ctx, obj);
case Z3_FLOATING_POINT_SORT: case Z3_FLOATING_POINT_SORT:
return new FPNum(ctx, obj); return new FPNum(ctx, obj);
case Z3_ROUNDING_MODE_SORT:
return new FPRMNum(ctx, obj);
default: ; default: ;
} }
} }

41
src/api/java/FPExpr.java Normal file
View file

@ -0,0 +1,41 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
FPExpr.java
Abstract:
Author:
Christoph Wintersteiger (cwinter) 2013-06-10
Notes:
--*/
package com.microsoft.z3;
/**
* FloatingPoint Expressions
*/
public class FPExpr extends Expr
{
/**
* The number of exponent bits.
* @throws Z3Exception
*/
public int getEBits() throws Z3Exception { return ((FPSort)getSort()).getEBits(); }
/**
* The number of significand bits.
* @throws Z3Exception
*/
public int getSBits() throws Z3Exception { return ((FPSort)getSort()).getSBits(); }
public FPExpr(Context ctx, long obj) throws Z3Exception
{
super(ctx, obj);
}
}

86
src/api/java/FPNum.java Normal file
View file

@ -0,0 +1,86 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
FPNum.java
Abstract:
Author:
Christoph Wintersteiger (cwinter) 2013-06-10
Notes:
--*/
package com.microsoft.z3;
/**
* FloatingPoint Numerals
*/
public class FPNum extends FPExpr
{
/**
* Retrieves the sign of a floating-point literal
* Remarks: returns true if the numeral is negative
* @throws Z3Exception
*/
public boolean getSign() throws Z3Exception {
Native.IntPtr res = new Native.IntPtr();
if (Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res) ^ true)
throw new Z3Exception("Sign is not a Boolean value");
return res.value != 0;
}
/**
* The significand value of a floating-point numeral as a string
* Remarks: The significand s is always 0 &lt; s &lt; 2.0; the resulting string is long
* enough to represent the real significand precisely.
* @throws Z3Exception
**/
public String getSignificand() throws Z3Exception {
return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
}
/**
* Return the exponent value of a floating-point numeral as a string
* @throws Z3Exception
*/
public String getExponent() throws Z3Exception {
return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject());
}
/**
* Return the exponent value of a floating-point numeral as a signed 64-bit integer
* @throws Z3Exception
*/
public long getExponentInt64() throws Z3Exception {
Native.LongPtr res = new Native.LongPtr();
if (Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
throw new Z3Exception("Exponent is not a 64 bit integer");
return res.value;
}
public FPNum(Context ctx, long obj) throws Z3Exception
{
super(ctx, obj);
}
/**
* Returns a string representation of the numeral.
*/
public String toString()
{
try
{
return Native.getNumeralString(getContext().nCtx(), getNativeObject());
} catch (Z3Exception e)
{
return "Z3Exception: " + e.getMessage();
}
}
}

29
src/api/java/FPRMExpr.java Normal file
View file

@ -0,0 +1,29 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
FPRMExpr.java
Abstract:
Author:
Christoph Wintersteiger (cwinter) 2013-06-10
Notes:
--*/
package com.microsoft.z3;
/**
* FloatingPoint RoundingMode Expressions
*/
public class FPRMExpr extends Expr
{
public FPRMExpr(Context ctx, long obj) throws Z3Exception
{
super(ctx, obj);
}
}

90
src/api/java/FPRMNum.java Normal file
View file

@ -0,0 +1,90 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
FPRMNum.java
Abstract:
Author:
Christoph Wintersteiger (cwinter) 2013-06-10
Notes:
--*/
package com.microsoft.z3;
import com.microsoft.z3.enumerations.Z3_decl_kind;
/**
* FloatingPoint RoundingMode Numerals
*/
public class FPRMNum extends FPRMExpr {
/**
* Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
* @throws Z3Exception
* **/
public boolean isRoundNearestTiesToEven() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
/**
* Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
* @throws Z3Exception
*/
public boolean isRNE() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }
/**
* Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
* @throws Z3Exception
*/
public boolean isRoundNearestTiesToAway() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }
/**
* Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
* @throws Z3Exception
*/
public boolean isRNA() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardPositive
* @throws Z3Exception
*/
public boolean isRoundTowardPositive() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardPositive
* @throws Z3Exception
*/
public boolean isRTP() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardNegative
* @throws Z3Exception
*/
public boolean isRoundTowardNegative() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardNegative
* @throws Z3Exception
*/
public boolean isRTN() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardZero
* @throws Z3Exception
*/
public boolean isRoundTowardZero() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
/**
* Indicates whether the term is the floating-point rounding numeral roundTowardZero
* @throws Z3Exception
*/
public boolean isRTZ() throws Z3Exception { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
public FPRMNum(Context ctx, long obj) throws Z3Exception {
super(ctx, obj);
}
}

35
src/api/java/FPRMSort.java Normal file
View file

@ -0,0 +1,35 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
FPRMExpr.java
Abstract:
Author:
Christoph Wintersteiger (cwinter) 2013-06-10
Notes:
--*/
package com.microsoft.z3;
/**
* The FloatingPoint RoundingMode sort
**/
public class FPRMSort extends Sort
{
public FPRMSort(Context ctx) throws Z3Exception
{
super(ctx, Native.mkFpaRoundingModeSort(ctx.nCtx()));
}
public FPRMSort(Context ctx, long obj) throws Z3Exception
{
super(ctx, obj);
}
}

49
src/api/java/FPSort.java Normal file
View file

@ -0,0 +1,49 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
FPSort.java
Abstract:
Author:
Christoph Wintersteiger (cwinter) 2013-06-10
Notes:
--*/
package com.microsoft.z3;
/**
* A FloatingPoint sort
**/
public class FPSort extends Sort
{
public FPSort(Context ctx, long obj) throws Z3Exception
{
super(ctx, obj);
}
public FPSort(Context ctx, int ebits, int sbits) throws Z3Exception
{
super(ctx, Native.mkFpaSort(ctx.nCtx(), ebits, sbits));
}
/**
* The number of exponent bits.
*/
public int getEBits() throws Z3Exception {
return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());
}
/**
* The number of significand bits.
*/
public int getSBits() throws Z3Exception {
return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());
}
}

41
src/api/z3_fpa.h
View file

@ -834,6 +834,47 @@ extern "C" {
*/ */
unsigned Z3_API Z3_fpa_get_sbits(__in Z3_context c, __in Z3_sort s); unsigned Z3_API Z3_fpa_get_sbits(__in Z3_context c, __in Z3_sort s);
/**
\brief Retrieves the sign of a floating-point literal
Remarks: sets \c sgn to 0 if the literal is NaN or positive and to 1 otherwise.
\param t a floating-point numeral.
def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(INT)))
*/
Z3_bool Z3_API Z3_fpa_get_numeral_sign(__in Z3_context c, __in Z3_ast t, __out int * sgn);
/**
\brief Return 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
enough to represent the real significand precisely.
\param t a floating-point numeral.
def_API('Z3_fpa_get_numeral_significand_string', STRING, (_in(CONTEXT), _in(AST)))
*/
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t);
/**
\brief Return the exponent value of a floating-point numeral as a string
\param t a floating-point numeral.
def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST)))
*/
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t);
/**
\brief Return the exponent value of a floating-point numeral as a signed 64-bit integer
\param t a floating-point numeral.
def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64)))
*/
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(__in Z3_context c, __in Z3_ast t, __out __int64 * n);
/** /**
\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. \brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.