mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
Resolved merge conflicts. Added FPA API input validity checks.
This commit is contained in:
commit
9053e6eba6
|
@ -909,14 +909,16 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_sign(c, t, sgn);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(t, 0);
|
||||
CHECK_VALID_AST(t, 0);
|
||||
if (sgn == 0) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
|
||||
family_id fid = mk_c(c)->get_fpa_fid();
|
||||
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
|
||||
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);
|
||||
|
@ -933,6 +935,71 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_fpa_get_numeral_sign_bv(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_sign_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();
|
||||
family_id fid = mk_c(c)->get_fpa_fid();
|
||||
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
|
||||
api::context * ctx = mk_c(c);
|
||||
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(to_expr(t), val);
|
||||
if (!r || mpfm.is_nan(val)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
app * a;
|
||||
if (mpfm.is_pos(val))
|
||||
a = ctx->bvutil().mk_numeral(0, 1);
|
||||
else
|
||||
a = ctx->bvutil().mk_numeral(1, 1);
|
||||
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);
|
||||
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);
|
||||
SASSERT(plugin != 0);
|
||||
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 sbits = val.get().get_sbits();
|
||||
scoped_mpq q(mpqm);
|
||||
mpqm.set(q, mpfm.sig(val));
|
||||
if (mpfm.is_inf(val)) mpqm.set(q, 0);
|
||||
app * a = mk_c(c)->bvutil().mk_numeral(q.get(), sbits-1);
|
||||
mk_c(c)->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_significand_string(c, t);
|
||||
|
@ -952,8 +1019,8 @@ extern "C" {
|
|||
}
|
||||
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))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG)
|
||||
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 "";
|
||||
}
|
||||
unsigned sbits = val.get().get_sbits();
|
||||
|
@ -972,6 +1039,8 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_significand_uint64(c, t, n);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(t, 0);
|
||||
CHECK_VALID_AST(t, 0);
|
||||
if (n == 0) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
|
@ -992,7 +1061,7 @@ extern "C" {
|
|||
bool r = plugin->is_numeral(e, val);
|
||||
const mpz & z = mpfm.sig(val);
|
||||
if (!r ||
|
||||
!(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val)) ||
|
||||
!(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val)) ||
|
||||
!mpzm.is_uint64(z)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
*n = 0;
|
||||
|
@ -1003,10 +1072,12 @@ 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();
|
||||
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();
|
||||
family_id fid = mk_c(c)->get_fpa_fid();
|
||||
|
@ -1019,23 +1090,35 @@ extern "C" {
|
|||
}
|
||||
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))) {
|
||||
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 "";
|
||||
}
|
||||
mpf_exp_t exp = mpfm.is_zero(val) ? 0 :
|
||||
mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) :
|
||||
mpfm.exp(val);
|
||||
unsigned ebits = val.get().get_ebits();
|
||||
mpf_exp_t exp;
|
||||
if (biased) {
|
||||
exp = mpfm.is_zero(val) ? 0 :
|
||||
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
|
||||
mpfm.bias_exp(ebits, mpfm.exp(val));
|
||||
}
|
||||
else {
|
||||
exp = mpfm.is_zero(val) ? 0 :
|
||||
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
|
||||
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
|
||||
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(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();
|
||||
CHECK_NON_NULL(t, 0);
|
||||
CHECK_VALID_AST(t, 0);
|
||||
if (n == 0) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
|
@ -1053,22 +1136,73 @@ extern "C" {
|
|||
}
|
||||
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))) {
|
||||
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
*n = 0;
|
||||
return 0;
|
||||
}
|
||||
*n = mpfm.is_zero(val) ? 0 :
|
||||
mpfm.is_denormal(val) ? mpfm.mk_min_exp(val.get().get_ebits()) :
|
||||
mpfm.exp(val);
|
||||
unsigned ebits = val.get().get_ebits();
|
||||
if (biased) {
|
||||
*n = mpfm.is_zero(val) ? 0 :
|
||||
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
|
||||
mpfm.bias_exp(ebits, mpfm.exp(val));
|
||||
}
|
||||
else {
|
||||
*n = mpfm.is_zero(val) ? 0 :
|
||||
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
|
||||
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
|
||||
mpfm.exp(val);
|
||||
}
|
||||
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();
|
||||
family_id fid = mk_c(c)->get_fpa_fid();
|
||||
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid);
|
||||
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;
|
||||
if (biased) {
|
||||
exp = mpfm.is_zero(val) ? 0 :
|
||||
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
|
||||
mpfm.bias_exp(ebits, mpfm.exp(val));
|
||||
}
|
||||
else {
|
||||
exp = mpfm.is_zero(val) ? 0 :
|
||||
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
|
||||
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
|
||||
mpfm.exp(val);
|
||||
}
|
||||
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);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(t, 0);
|
||||
CHECK_VALID_AST(t, 0);
|
||||
if (!is_fp(c, t)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
RETURN_Z3(0);
|
||||
|
@ -1098,4 +1232,102 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_is_numeral_nan(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
return fu.is_nan(to_expr(t));
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_is_numeral_inf(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
return fu.is_inf(to_expr(t));
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_is_numeral_zero(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
return fu.is_zero(to_expr(t));
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_is_numeral_normal(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
return fu.is_normal(to_expr(t));
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_is_numeral_subnormal(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
return fu.is_subnormal(to_expr(t));
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_is_numeral_positive(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
return fu.is_positive(to_expr(t));
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_is_numeral_negative(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
return fu.is_negative(to_expr(t));
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
@ -14,7 +14,7 @@ Author:
|
|||
Christoph Wintersteiger (cwinter) 2013-06-10
|
||||
|
||||
Notes:
|
||||
|
||||
|
||||
--*/
|
||||
using System;
|
||||
using System.Diagnostics.Contracts;
|
||||
|
@ -27,6 +27,20 @@ namespace Microsoft.Z3
|
|||
[ContractVerification(true)]
|
||||
public class FPNum : FPExpr
|
||||
{
|
||||
/// <summary>
|
||||
/// The sign of a floating-point numeral as a bit-vector expression
|
||||
/// </summary>
|
||||
/// <remarks>
|
||||
/// NaN's do not have a bit-vector sign, so they are invalid arguments.
|
||||
/// </remarks>
|
||||
public BitVecExpr SignBV
|
||||
{
|
||||
get
|
||||
{
|
||||
return new BitVecExpr(Context, Native.Z3_fpa_get_numeral_sign_bv(Context.nCtx, NativeObject));
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Retrieves the sign of a floating-point literal
|
||||
/// </summary>
|
||||
|
@ -38,7 +52,7 @@ namespace Microsoft.Z3
|
|||
get
|
||||
{
|
||||
int res = 0;
|
||||
if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref 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;
|
||||
}
|
||||
|
@ -63,7 +77,7 @@ namespace Microsoft.Z3
|
|||
/// The significand value of a floating-point numeral as a UInt64
|
||||
/// </summary>
|
||||
/// <remarks>
|
||||
/// This function extracts the significand bits, without the
|
||||
/// This function extracts the significand bits, without the
|
||||
/// hidden bit or normalization. Throws an exception if the
|
||||
/// significand does not fit into a UInt64.
|
||||
/// </remarks>
|
||||
|
@ -73,36 +87,90 @@ namespace Microsoft.Z3
|
|||
{
|
||||
UInt64 result = 0;
|
||||
if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0)
|
||||
throw new Z3Exception("Significand is not a 64 bit unsigned integer");
|
||||
throw new Z3Exception("Significand is not a 64 bit unsigned integer");
|
||||
return result;
|
||||
}
|
||||
}
|
||||
|
||||
/// <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));
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Indicates whether the numeral is a NaN.
|
||||
/// </summary>
|
||||
public bool IsNaN { get { return Native.Z3_fpa_is_numeral_nan(Context.nCtx, NativeObject) != 0; } }
|
||||
|
||||
/// <summary>
|
||||
/// Indicates whether the numeral is a +oo or -oo.
|
||||
/// </summary>
|
||||
public bool IsInf { get { return Native.Z3_fpa_is_numeral_inf(Context.nCtx, NativeObject) != 0; } }
|
||||
|
||||
/// <summary>
|
||||
/// Indicates whether the numeral is +zero or -zero.
|
||||
/// </summary>
|
||||
public bool IsZero{ get { return Native.Z3_fpa_is_numeral_zero(Context.nCtx, NativeObject) != 0; } }
|
||||
|
||||
/// <summary>
|
||||
/// Indicates whether the numeral is normal.
|
||||
/// </summary>
|
||||
public bool IsNormal { get { return Native.Z3_fpa_is_numeral_normal(Context.nCtx, NativeObject) != 0; } }
|
||||
|
||||
/// <summary>
|
||||
/// Indicates whether the numeral is subnormal.
|
||||
/// </summary>
|
||||
public bool IsSubnormal { get { return Native.Z3_fpa_is_numeral_subnormal(Context.nCtx, NativeObject) != 0; } }
|
||||
|
||||
/// <summary>
|
||||
/// Indicates whether the numeral is positive.
|
||||
/// </summary>
|
||||
public bool IsPositive { get { return Native.Z3_fpa_is_numeral_positive(Context.nCtx, NativeObject) != 0; } }
|
||||
|
||||
/// <summary>
|
||||
/// Indicates whether the numeral is negative.
|
||||
/// </summary>
|
||||
public bool IsNegative { get { return Native.Z3_fpa_is_numeral_negative(Context.nCtx, NativeObject) != 0; } }
|
||||
|
||||
#region Internal
|
||||
internal FPNum(Context ctx, IntPtr obj)
|
||||
: base(ctx, obj)
|
||||
|
@ -113,7 +181,7 @@ namespace Microsoft.Z3
|
|||
|
||||
/// <summary>
|
||||
/// Returns a string representation of the numeral.
|
||||
/// </summary>
|
||||
/// </summary>
|
||||
public override string ToString()
|
||||
{
|
||||
return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
|
||||
|
|
|
@ -20,7 +20,7 @@ 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
|
||||
|
@ -33,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
|
||||
|
@ -57,25 +66,117 @@ 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));
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* Indicates whether the numeral is a NaN.
|
||||
* @throws Z3Exception on error
|
||||
* @return a boolean
|
||||
**/
|
||||
public boolean isNaN()
|
||||
{
|
||||
return Native.fpaIsNumeralNan(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
* Indicates whether the numeral is a +oo or -oo.
|
||||
* @throws Z3Exception on error
|
||||
* @return a boolean
|
||||
**/
|
||||
public boolean isInf()
|
||||
{
|
||||
return Native.fpaIsNumeralInf(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
* Indicates whether the numeral is +zero or -zero.
|
||||
* @throws Z3Exception on error
|
||||
* @return a boolean
|
||||
**/
|
||||
public boolean isZero()
|
||||
{
|
||||
return Native.fpaIsNumeralZero(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
* Indicates whether the numeral is normal.
|
||||
* @throws Z3Exception on error
|
||||
* @return a boolean
|
||||
**/
|
||||
public boolean isNormal()
|
||||
{
|
||||
return Native.fpaIsNumeralNormal(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
* Indicates whether the numeral is subnormal.
|
||||
* @throws Z3Exception on error
|
||||
* @return a boolean
|
||||
**/
|
||||
public boolean isSubnormal()
|
||||
{
|
||||
return Native.fpaIsNumeralSubnormal(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
* Indicates whether the numeral is positive.
|
||||
* @throws Z3Exception on error
|
||||
* @return a boolean
|
||||
**/
|
||||
public boolean isPositive()
|
||||
{
|
||||
return Native.fpaIsNumeralPositive(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
* Indicates whether the numeral is negative.
|
||||
* @throws Z3Exception on error
|
||||
* @return a boolean
|
||||
**/
|
||||
public boolean isNegative()
|
||||
{
|
||||
return Native.fpaIsNumeralNegative(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
|
||||
public FPNum(Context ctx, long obj)
|
||||
{
|
||||
|
@ -88,6 +189,5 @@ public class FPNum extends FPExpr
|
|||
public String toString()
|
||||
{
|
||||
return Native.getNumeralString(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
|
|
|
@ -1325,10 +1325,20 @@ struct
|
|||
let get_ebits = Z3native.fpa_get_ebits
|
||||
let get_sbits = Z3native.fpa_get_sbits
|
||||
let get_numeral_sign = Z3native.fpa_get_numeral_sign
|
||||
let get_numeral_significand_string = Z3native.fpa_get_numeral_significand_string
|
||||
let get_numeral_significand_uint = Z3native.fpa_get_numeral_significand_uint64
|
||||
let get_numeral_sign_bv = Z3native.fpa_get_numeral_sign_bv
|
||||
let get_numeral_exponent_string = Z3native.fpa_get_numeral_exponent_string
|
||||
let get_numeral_exponent_int = Z3native.fpa_get_numeral_exponent_int64
|
||||
let get_numeral_exponent_bv = Z3native.fpa_get_numeral_exponent_bv
|
||||
let get_numeral_significand_string = Z3native.fpa_get_numeral_significand_string
|
||||
let get_numeral_significand_uint = Z3native.fpa_get_numeral_significand_uint64
|
||||
let get_numeral_significand_bv = Z3native.fpa_get_numeral_significand_bv
|
||||
let is_numeral_nan = Z3native.fpa_is_numeral_nan
|
||||
let is_numeral_inf = Z3native.fpa_is_numeral_inf
|
||||
let is_numeral_zero = Z3native.fpa_is_numeral_zero
|
||||
let is_numeral_normal = Z3native.fpa_is_numeral_normal
|
||||
let is_numeral_subnormal = Z3native.fpa_is_numeral_subnormal
|
||||
let is_numeral_positive = Z3native.fpa_is_numeral_positive
|
||||
let is_numeral_negative = Z3native.fpa_is_numeral_negative
|
||||
let mk_to_ieee_bv = Z3native.mk_fpa_to_ieee_bv
|
||||
let mk_to_fp_int_real = Z3native.mk_fpa_to_fp_int_real
|
||||
let numeral_to_string x = Z3native.get_numeral_string (Expr.gc x) x
|
||||
|
|
|
@ -2141,21 +2141,54 @@ sig
|
|||
(** Retrieves the sign of a floating-point literal. *)
|
||||
val get_numeral_sign : context -> Expr.expr -> bool * int
|
||||
|
||||
(** Return 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. *)
|
||||
val get_numeral_sign_bv : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Return the exponent value of a floating-point numeral as a string *)
|
||||
val get_numeral_exponent_string : context -> Expr.expr -> bool -> string
|
||||
|
||||
(** Return the exponent value of a floating-point numeral as a signed integer *)
|
||||
val get_numeral_exponent_int : context -> Expr.expr -> bool -> bool * int
|
||||
|
||||
(** Return the exponent of a floating-point numeral as a bit-vector expression.
|
||||
Remark: NaN's do not have a bit-vector exponent, so they are invalid arguments. *)
|
||||
val get_numeral_exponent_bv : context -> Expr.expr -> bool -> Expr.expr
|
||||
|
||||
(** Return the significand value of a floating-point numeral as a bit-vector expression.
|
||||
Remark: NaN's do not have a bit-vector significand, so they are invalid arguments. *)
|
||||
val get_numeral_significand_bv : context -> Expr.expr -> Expr.expr
|
||||
|
||||
(** Return the significand value of a floating-point numeral as a string. *)
|
||||
val get_numeral_significand_string : context -> Expr.expr -> string
|
||||
|
||||
(** Return the significand value of a floating-point numeral as a uint64.
|
||||
Remark: This function extracts the significand bits, without the
|
||||
hidden bit or normalization. Throws an exception if the
|
||||
significand does not fit into a uint64. *)
|
||||
significand does not fit into an int. *)
|
||||
val get_numeral_significand_uint : context -> Expr.expr -> bool * int
|
||||
|
||||
(** Return the exponent value of a floating-point numeral as a string *)
|
||||
val get_numeral_exponent_string : context -> Expr.expr -> string
|
||||
(** Indicates whether a floating-point numeral is a NaN. *)
|
||||
val is_numeral_nan : context -> Expr.expr -> bool
|
||||
|
||||
(** Return the exponent value of a floating-point numeral as a signed integer *)
|
||||
val get_numeral_exponent_int : context -> Expr.expr -> bool * int
|
||||
(** Indicates whether a floating-point numeral is +oo or -oo. *)
|
||||
val is_numeral_inf : context -> Expr.expr -> bool
|
||||
|
||||
(** Indicates whether a floating-point numeral is +zero or -zero. *)
|
||||
val is_numeral_zero : context -> Expr.expr -> bool
|
||||
|
||||
(** Indicates whether a floating-point numeral is normal. *)
|
||||
val is_numeral_normal : context -> Expr.expr -> bool
|
||||
|
||||
(** Indicates whether a floating-point numeral is subnormal. *)
|
||||
val is_numeral_subnormal : context -> Expr.expr -> bool
|
||||
|
||||
(** Indicates whether a floating-point numeral is positive. *)
|
||||
val is_numeral_positive : context -> Expr.expr -> bool
|
||||
|
||||
(** Indicates whether a floating-point numeral is negative. *)
|
||||
val is_numeral_negative : context -> Expr.expr -> bool
|
||||
|
||||
(** Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. *)
|
||||
val mk_to_ieee_bv : context -> Expr.expr -> Expr.expr
|
||||
|
||||
|
@ -3023,29 +3056,22 @@ sig
|
|||
(** Assert a constraint (or multiple) into the solver. *)
|
||||
val add : solver -> Expr.expr list -> unit
|
||||
|
||||
(** * Assert multiple constraints (cs) into the solver, and track them (in the
|
||||
* unsat) core
|
||||
* using the Boolean constants in ps.
|
||||
*
|
||||
* This API is an alternative to {!check} with assumptions for
|
||||
* extracting unsat cores.
|
||||
* Both APIs can be used in the same solver. The unsat core will contain a
|
||||
* combination
|
||||
* of the Boolean variables provided using {!assert_and_track}
|
||||
* and the Boolean literals
|
||||
* provided using {!check} with assumptions. *)
|
||||
(** Assert multiple constraints (cs) into the solver, and track them (in the
|
||||
unsat) core using the Boolean constants in ps.
|
||||
|
||||
This API is an alternative to {!check} with assumptions for extracting unsat cores.
|
||||
Both APIs can be used in the same solver. The unsat core will contain a combination
|
||||
of the Boolean variables provided using {!assert_and_track} and the Boolean literals
|
||||
provided using {!check} with assumptions. *)
|
||||
val assert_and_track_l : solver -> Expr.expr list -> Expr.expr list -> unit
|
||||
|
||||
(** * Assert a constraint (c) into the solver, and track it (in the unsat) core
|
||||
* using the Boolean constant p.
|
||||
*
|
||||
* This API is an alternative to {!check} with assumptions for
|
||||
* extracting unsat cores.
|
||||
* Both APIs can be used in the same solver. The unsat core will contain a
|
||||
* combination
|
||||
* of the Boolean variables provided using {!assert_and_track}
|
||||
* and the Boolean literals
|
||||
* provided using {!check} with assumptions. *)
|
||||
(** Assert a constraint (c) into the solver, and track it (in the unsat) core
|
||||
using the Boolean constant p.
|
||||
|
||||
This API is an alternative to {!check} with assumptions for extracting unsat cores.
|
||||
Both APIs can be used in the same solver. The unsat core will contain a combination
|
||||
of the Boolean variables provided using {!assert_and_track} and the Boolean literals
|
||||
provided using {!check} with assumptions. *)
|
||||
val assert_and_track : solver -> Expr.expr -> Expr.expr -> unit
|
||||
|
||||
(** The number of assertions in the solver. *)
|
||||
|
|
|
@ -8452,27 +8452,13 @@ def is_fprm_value(a):
|
|||
|
||||
### FP Numerals
|
||||
|
||||
class FPNumRef(FPRef):
|
||||
def isNaN(self):
|
||||
return self.decl().kind() == Z3_OP_FPA_NAN
|
||||
class FPNumRef(FPRef):
|
||||
"""The sign of the numeral.
|
||||
|
||||
def isInf(self):
|
||||
return self.decl().kind() == Z3_OP_FPA_PLUS_INF or self.decl().kind() == Z3_OP_FPA_MINUS_INF
|
||||
|
||||
def isZero(self):
|
||||
return self.decl().kind() == Z3_OP_FPA_PLUS_ZERO or self.decl().kind() == Z3_OP_FPA_MINUS_ZERO
|
||||
|
||||
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 the numeral.
|
||||
|
||||
>>> x = FPNumRef(+1.0, FPSort(8, 24))
|
||||
>>> x = FPVal(+1.0, FPSort(8, 24))
|
||||
>>> x.sign()
|
||||
False
|
||||
>>> x = FPNumRef(-1.0, FPSort(8, 24))
|
||||
>>> x = FPVal(-1.0, FPSort(8, 24))
|
||||
>>> x.sign()
|
||||
True
|
||||
"""
|
||||
|
@ -8482,48 +8468,103 @@ 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.
|
||||
"""
|
||||
The significand of the numeral.
|
||||
def sign_as_bv(self):
|
||||
return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx)
|
||||
|
||||
>>> x = FPNumRef(2.5, FPSort(8, 24))
|
||||
"""The significand of the numeral.
|
||||
|
||||
>>> x = FPVal(2.5, FPSort(8, 24))
|
||||
>>> x.significand()
|
||||
1.25
|
||||
"""
|
||||
def significand(self):
|
||||
return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast())
|
||||
|
||||
"""
|
||||
The exponent of the numeral.
|
||||
"""The significand of the numeral as a long.
|
||||
|
||||
>>> x = FPNumRef(2.5, FPSort(8, 24))
|
||||
>>> x = FPVal(2.5, FPSort(8, 24))
|
||||
>>> x.significand_as_long()
|
||||
1.25
|
||||
"""
|
||||
def significand_as_long(self):
|
||||
return Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast())
|
||||
|
||||
"""The significand of the 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.
|
||||
|
||||
>>> x = FPVal(2.5, FPSort(8, 24))
|
||||
>>> 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.
|
||||
"""The exponent of the numeral as a long.
|
||||
|
||||
>>> x = FPNumRef(2.5, FPSort(8, 24))
|
||||
>>> x = FPVal(2.5, FPSort(8, 24))
|
||||
>>> 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 the 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)
|
||||
|
||||
"""Indicates whether the numeral is a NaN."""
|
||||
def isNaN(self):
|
||||
return Z3_fpa_is_numeral_nan(self.ctx.ref(), self.as_ast())
|
||||
|
||||
"""Indicates whether the numeral is +oo or -oo."""
|
||||
def isInf(self):
|
||||
return Z3_fpa_is_numeral_inf(self.ctx.ref(), self.as_ast())
|
||||
|
||||
"""Indicates whether the numeral is +zero or -zero."""
|
||||
def isZero(self):
|
||||
return Z3_fpa_is_numeral_zero(self.ctx.ref(), self.as_ast())
|
||||
|
||||
"""Indicates whether the numeral is normal."""
|
||||
def isNormal(self):
|
||||
return Z3_fpa_is_numeral_normal(self.ctx.ref(), self.as_ast())
|
||||
|
||||
"""Indicates whether the numeral is subnormal."""
|
||||
def isSubnormal(self):
|
||||
return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast())
|
||||
|
||||
"""Indicates whether the numeral is postitive."""
|
||||
def isPositive(self):
|
||||
return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast())
|
||||
|
||||
"""Indicates whether the numeral is negative."""
|
||||
def isNegative(self):
|
||||
return Z3_fpa_is_numeral_negative(self.ctx.ref(), self.as_ast())
|
||||
|
||||
"""
|
||||
The string representation of the numeral.
|
||||
|
||||
>>> x = FPNumRef(20, FPSort(8, 24))
|
||||
>>> x = FPVal(20, FPSort(8, 24))
|
||||
>>> x.as_string()
|
||||
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):
|
||||
|
@ -8676,7 +8717,7 @@ def FPVal(sig, exp=None, fps=None, ctx=None):
|
|||
>>> v = FPVal(20.0, FPSort(8, 24))
|
||||
>>> v
|
||||
1.25*(2**4)
|
||||
>>> print("0x%.8x" % v.exponent_as_long())
|
||||
>>> print("0x%.8x" % v.exponent_as_long(False))
|
||||
0x00000004
|
||||
>>> v = FPVal(2.25, FPSort(8, 24))
|
||||
>>> v
|
||||
|
|
|
@ -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))
|
||||
|
|
128
src/api/z3_fpa.h
128
src/api/z3_fpa.h
|
@ -253,9 +253,9 @@ extern "C" {
|
|||
|
||||
This is the operator named `fp' in the SMT FP theory definition.
|
||||
Note that \c sign is required to be a bit-vector of size 1. Significand and exponent
|
||||
are required to be greater than 1 and 2 respectively. The FloatingPoint sort
|
||||
are required to be longer than 1 and 2 respectively. The FloatingPoint sort
|
||||
of the resulting expression is automatically determined from the bit-vector sizes
|
||||
of the arguments.
|
||||
of the arguments. The exponent is assumed to be in IEEE-754 biased representation.
|
||||
|
||||
\param c logical context
|
||||
\param sgn sign
|
||||
|
@ -822,6 +822,100 @@ extern "C" {
|
|||
*/
|
||||
unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s);
|
||||
|
||||
/**
|
||||
\brief Checks whether a given floating-point numeral is a NaN.
|
||||
|
||||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
def_API('Z3_fpa_is_numeral_nan', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Checks whether a given floating-point numeral is a +oo or -oo.
|
||||
|
||||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
def_API('Z3_fpa_is_numeral_inf', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Checks whether a given floating-point numeral is +zero or -zero.
|
||||
|
||||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
def_API('Z3_fpa_is_numeral_zero', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Checks whether a given floating-point numeral is normal.
|
||||
|
||||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
def_API('Z3_fpa_is_numeral_normal', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Checks whether a given floating-point numeral is subnormal.
|
||||
|
||||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
def_API('Z3_fpa_is_numeral_subnormal', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Checks whether a given floating-point numeral is positive.
|
||||
|
||||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
def_API('Z3_fpa_is_numeral_positive', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Checks whether a given floating-point numeral is negative.
|
||||
|
||||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
def_API('Z3_fpa_is_numeral_negative', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Retrieves the sign of a floating-point literal as a bit-vector expression.
|
||||
|
||||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
Remarks: NaN is an invalid argument.
|
||||
|
||||
def_API('Z3_fpa_get_numeral_sign_bv', AST, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_fpa_get_numeral_sign_bv(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Retrieves the significand of a floating-point literal as a bit-vector expression.
|
||||
|
||||
\param c logical context
|
||||
\param t a floating-point numeral
|
||||
|
||||
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 sign of a floating-point literal.
|
||||
|
||||
|
@ -858,23 +952,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
|
||||
|
@ -882,12 +978,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.
|
||||
|
|
|
@ -288,11 +288,16 @@ public:
|
|||
app * mk_nzero(sort * s) { return mk_nzero(get_ebits(s), get_sbits(s)); }
|
||||
|
||||
bool is_nan(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nan(v); }
|
||||
bool is_inf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_inf(v); }
|
||||
bool is_pinf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pinf(v); }
|
||||
bool is_ninf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_ninf(v); }
|
||||
bool is_zero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_zero(v); }
|
||||
bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pzero(v); }
|
||||
bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nzero(v); }
|
||||
bool is_normal(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_normal(v); }
|
||||
bool is_subnormal(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_denormal(v); }
|
||||
bool is_positive(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pos(v); }
|
||||
bool is_negative(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_neg(v); }
|
||||
|
||||
app * mk_fp(expr * sgn, expr * exp, expr * sig) {
|
||||
SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1);
|
||||
|
|
|
@ -22,13 +22,13 @@ Revision History:
|
|||
#include"ast_ll_pp.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
||||
// ---------------------------
|
||||
//
|
||||
// Base class
|
||||
//
|
||||
// ---------------------------
|
||||
|
||||
|
||||
conflict_resolution::conflict_resolution(ast_manager & m,
|
||||
context & ctx,
|
||||
dyn_ack_manager & dyn_ack_manager,
|
||||
|
@ -42,7 +42,7 @@ namespace smt {
|
|||
m_dyn_ack_manager(dyn_ack_manager),
|
||||
m_assigned_literals(assigned_literals),
|
||||
m_lemma_atoms(m),
|
||||
m_todo_js_qhead(0),
|
||||
m_todo_js_qhead(0),
|
||||
m_antecedents(0),
|
||||
m_watches(watches),
|
||||
m_new_proofs(m),
|
||||
|
@ -67,7 +67,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
/**
|
||||
\brief Find a common ancestor (anc) of n1 and n2 in the 'proof' tree.
|
||||
\brief Find a common ancestor (anc) of n1 and n2 in the 'proof' tree.
|
||||
The common ancestor is used to produce irredundant transitivity proofs.
|
||||
|
||||
n1 = a1 = ... = ai = ANC = ... = root
|
||||
|
@ -100,7 +100,7 @@ namespace smt {
|
|||
*/
|
||||
void conflict_resolution::eq_justification2literals(enode * lhs, enode * rhs, eq_justification js) {
|
||||
SASSERT(m_antecedents);
|
||||
TRACE("conflict_detail",
|
||||
TRACE("conflict_detail",
|
||||
ast_manager& m = get_manager();
|
||||
tout << mk_pp(lhs->get_owner(), m) << " = " << mk_pp(rhs->get_owner(), m);
|
||||
switch (js.get_kind()) {
|
||||
|
@ -133,7 +133,7 @@ namespace smt {
|
|||
mark_eq(lhs->get_arg(1), rhs->get_arg(0));
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < num_args; i++)
|
||||
for (unsigned i = 0; i < num_args; i++)
|
||||
mark_eq(lhs->get_arg(i), rhs->get_arg(i));
|
||||
}
|
||||
break;
|
||||
|
@ -146,9 +146,9 @@ namespace smt {
|
|||
/**
|
||||
\brief Process the transitivity 'proof' from n1 and n2, where
|
||||
n1 and n2 are in the same branch
|
||||
|
||||
|
||||
n1 -> ... -> n2
|
||||
|
||||
|
||||
This method may update m_antecedents, m_todo_js and m_todo_eqs.
|
||||
|
||||
The resultant set of literals is stored in m_antecedents.
|
||||
|
@ -163,7 +163,7 @@ namespace smt {
|
|||
|
||||
/**
|
||||
\brief Process the justification of n1 = n2.
|
||||
|
||||
|
||||
This method may update m_antecedents, m_todo_js and m_todo_eqs.
|
||||
|
||||
The resultant set of literals is stored in m_antecedents.
|
||||
|
@ -180,8 +180,8 @@ namespace smt {
|
|||
|
||||
The result is stored in result.
|
||||
|
||||
\remark This method does not reset the vectors m_antecedents, m_todo_js, m_todo_eqs, nor reset the
|
||||
marks in the justification objects.
|
||||
\remark This method does not reset the vectors m_antecedents, m_todo_js, m_todo_eqs, nor reset the
|
||||
marks in the justification objects.
|
||||
*/
|
||||
void conflict_resolution::justification2literals_core(justification * js, literal_vector & result) {
|
||||
SASSERT(m_todo_js_qhead <= m_todo_js.size());
|
||||
|
@ -294,13 +294,13 @@ namespace smt {
|
|||
if (js)
|
||||
r = std::max(r, get_justification_max_lvl(js));
|
||||
break;
|
||||
}
|
||||
}
|
||||
case b_justification::BIN_CLAUSE:
|
||||
r = std::max(r, m_ctx.get_assign_level(js.get_literal()));
|
||||
break;
|
||||
case b_justification::AXIOM:
|
||||
break;
|
||||
case b_justification::JUSTIFICATION:
|
||||
case b_justification::JUSTIFICATION:
|
||||
r = std::max(r, get_justification_max_lvl(js.get_justification()));
|
||||
break;
|
||||
default:
|
||||
|
@ -313,8 +313,8 @@ namespace smt {
|
|||
bool_var var = antecedent.var();
|
||||
unsigned lvl = m_ctx.get_assign_level(var);
|
||||
SASSERT(var < static_cast<int>(m_ctx.get_num_bool_vars()));
|
||||
TRACE("conflict", tout << "processing antecedent (level " << lvl << "):";
|
||||
m_ctx.display_literal(tout, antecedent);
|
||||
TRACE("conflict", tout << "processing antecedent (level " << lvl << "):";
|
||||
m_ctx.display_literal(tout, antecedent);
|
||||
m_ctx.display_detailed_literal(tout << " ", antecedent); tout << "\n";);
|
||||
|
||||
if (!m_ctx.is_marked(var) && lvl > m_ctx.get_base_level()) {
|
||||
|
@ -386,17 +386,17 @@ namespace smt {
|
|||
consequent = false_literal;
|
||||
if (not_l != null_literal)
|
||||
consequent = ~not_l;
|
||||
|
||||
|
||||
m_conflict_lvl = get_max_lvl(consequent, js);
|
||||
|
||||
TRACE("conflict_bug",
|
||||
tout << "conflict_lvl: " << m_conflict_lvl << " scope_lvl: " << m_ctx.get_scope_level() << " base_lvl: " << m_ctx.get_base_level()
|
||||
TRACE("conflict_bug",
|
||||
tout << "conflict_lvl: " << m_conflict_lvl << " scope_lvl: " << m_ctx.get_scope_level() << " base_lvl: " << m_ctx.get_base_level()
|
||||
<< " search_lvl: " << m_ctx.get_search_level() << "\n";
|
||||
tout << "js.kind: " << js.get_kind() << "\n";
|
||||
tout << "consequent: " << consequent << ": ";
|
||||
m_ctx.display_literal_verbose(tout, consequent); tout << "\n";
|
||||
m_ctx.display(tout, js); tout << "\n";
|
||||
);
|
||||
);
|
||||
|
||||
// m_conflict_lvl can be smaller than m_ctx.get_search_level() when:
|
||||
// there are user level scopes created using the Z3 API, and
|
||||
|
@ -413,7 +413,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
TRACE("conflict", tout << "conflict_lvl: " << m_conflict_lvl << "\n";);
|
||||
|
||||
|
||||
SASSERT(!m_assigned_literals.empty());
|
||||
|
||||
SASSERT(m_todo_js.empty());
|
||||
|
@ -425,32 +425,32 @@ namespace smt {
|
|||
/**
|
||||
\brief Cleanup datastructures used during resolve(), minimize lemma (when minimization is enabled),
|
||||
compute m_new_scope_lvl and m_lemma_iscope_lvl, generate proof if needed.
|
||||
|
||||
|
||||
This method assumes that the lemma is stored in m_lemma (and the associated atoms in m_lemma_atoms).
|
||||
|
||||
|
||||
\warning This method assumes the literals in m_lemma[1] ... m_lemma[m_lemma.size() - 1] are marked.
|
||||
*/
|
||||
void conflict_resolution::finalize_resolve(b_justification conflict, literal not_l) {
|
||||
unmark_justifications(0);
|
||||
|
||||
|
||||
TRACE("conflict",
|
||||
tout << "before minimization:\n";
|
||||
m_ctx.display_literals(tout, m_lemma);
|
||||
tout << "\n";);
|
||||
|
||||
|
||||
TRACE("conflict_verbose",
|
||||
tout << "before minimization:\n";
|
||||
m_ctx.display_literals_verbose(tout, m_lemma);
|
||||
tout << "\n";);
|
||||
|
||||
|
||||
if (m_params.m_minimize_lemmas)
|
||||
minimize_lemma();
|
||||
|
||||
|
||||
TRACE("conflict",
|
||||
tout << "after minimization:\n";
|
||||
m_ctx.display_literals(tout, m_lemma);
|
||||
tout << "\n";);
|
||||
|
||||
|
||||
TRACE("conflict_verbose",
|
||||
tout << "after minimization:\n";
|
||||
m_ctx.display_literals_verbose(tout, m_lemma);
|
||||
|
@ -459,7 +459,7 @@ namespace smt {
|
|||
TRACE("conflict_bug",
|
||||
m_ctx.display_literals_verbose(tout, m_lemma);
|
||||
tout << "\n";);
|
||||
|
||||
|
||||
literal_vector::iterator it = m_lemma.begin();
|
||||
literal_vector::iterator end = m_lemma.end();
|
||||
m_new_scope_lvl = m_ctx.get_search_level();
|
||||
|
@ -478,11 +478,11 @@ namespace smt {
|
|||
m_lemma_iscope_lvl = lvl;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
TRACE("conflict",
|
||||
tout << "new scope level: " << m_new_scope_lvl << "\n";
|
||||
tout << "intern. scope level: " << m_lemma_iscope_lvl << "\n";);
|
||||
|
||||
|
||||
if (m_manager.proofs_enabled())
|
||||
mk_conflict_proof(conflict, not_l);
|
||||
}
|
||||
|
@ -505,7 +505,7 @@ namespace smt {
|
|||
TRACE("conflict", tout << "not_l: "; m_ctx.display_literal(tout, not_l); tout << "\n";);
|
||||
process_antecedent(not_l, num_marks);
|
||||
}
|
||||
|
||||
|
||||
do {
|
||||
|
||||
if (get_manager().has_trace_stream()) {
|
||||
|
@ -542,7 +542,7 @@ namespace smt {
|
|||
process_antecedent(~l, num_marks);
|
||||
}
|
||||
justification * js = cls->get_justification();
|
||||
if (js)
|
||||
if (js)
|
||||
process_justification(js, num_marks);
|
||||
break;
|
||||
}
|
||||
|
@ -558,13 +558,13 @@ namespace smt {
|
|||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
||||
|
||||
while (true) {
|
||||
literal l = m_assigned_literals[idx];
|
||||
if (m_ctx.is_marked(l.var()))
|
||||
if (m_ctx.is_marked(l.var()))
|
||||
break;
|
||||
CTRACE("conflict", m_ctx.get_assign_level(l) != m_conflict_lvl && m_ctx.get_assign_level(l) != m_ctx.get_base_level(),
|
||||
tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal(tout, l);
|
||||
tout << "assign_level(l): " << m_ctx.get_assign_level(l) << ", conflict_lvl: " << m_conflict_lvl << ", l: "; m_ctx.display_literal(tout, l);
|
||||
tout << "\n";);
|
||||
SASSERT(m_ctx.get_assign_level(l) == m_conflict_lvl ||
|
||||
// it may also be an (out-of-order) asserted literal
|
||||
|
@ -580,7 +580,7 @@ namespace smt {
|
|||
idx--;
|
||||
num_marks--;
|
||||
m_ctx.unset_mark(c_var);
|
||||
}
|
||||
}
|
||||
while (num_marks > 0);
|
||||
|
||||
TRACE("conflict", tout << "FUIP: "; m_ctx.display_literal(tout, consequent); tout << "\n";);
|
||||
|
@ -589,8 +589,8 @@ namespace smt {
|
|||
m_lemma_atoms.set(0, m_ctx.bool_var2expr(consequent.var()));
|
||||
|
||||
// TODO:
|
||||
//
|
||||
// equality optimization should go here.
|
||||
//
|
||||
// equality optimization should go here.
|
||||
//
|
||||
|
||||
finalize_resolve(conflict, not_l);
|
||||
|
@ -600,7 +600,7 @@ namespace smt {
|
|||
|
||||
/**
|
||||
\brief Return an approximation for the set of scope levels where the literals in m_lemma
|
||||
were assigned.
|
||||
were assigned.
|
||||
*/
|
||||
level_approx_set conflict_resolution::get_lemma_approx_level_set() {
|
||||
level_approx_set result;
|
||||
|
@ -640,7 +640,7 @@ namespace smt {
|
|||
unsigned lvl = m_ctx.get_assign_level(var);
|
||||
if (!m_ctx.is_marked(var) && lvl > m_ctx.get_base_level()) {
|
||||
if (m_lvl_set.may_contain(lvl)) {
|
||||
m_ctx.set_mark(var);
|
||||
m_ctx.set_mark(var);
|
||||
m_unmark.push_back(var);
|
||||
m_lemma_min_stack.push_back(var);
|
||||
}
|
||||
|
@ -667,18 +667,18 @@ namespace smt {
|
|||
}
|
||||
|
||||
/**
|
||||
\brief Return true if lit is implied by other marked literals
|
||||
and/or literals assigned at the base level.
|
||||
The set lvl_set is used as an optimization.
|
||||
\brief Return true if lit is implied by other marked literals
|
||||
and/or literals assigned at the base level.
|
||||
The set lvl_set is used as an optimization.
|
||||
The idea is to stop the recursive search with a failure
|
||||
as soon as we find a literal assigned in a level that is not in lvl_set.
|
||||
as soon as we find a literal assigned in a level that is not in lvl_set.
|
||||
*/
|
||||
bool conflict_resolution::implied_by_marked(literal lit) {
|
||||
m_lemma_min_stack.reset(); // avoid recursive function
|
||||
m_lemma_min_stack.push_back(lit.var());
|
||||
unsigned old_size = m_unmark.size();
|
||||
unsigned old_js_qhead = m_todo_js_qhead;
|
||||
|
||||
|
||||
while (!m_lemma_min_stack.empty()) {
|
||||
bool_var var = m_lemma_min_stack.back();
|
||||
m_lemma_min_stack.pop_back();
|
||||
|
@ -739,7 +739,7 @@ namespace smt {
|
|||
m_unmark.reset();
|
||||
|
||||
m_lvl_set = get_lemma_approx_level_set();
|
||||
|
||||
|
||||
unsigned sz = m_lemma.size();
|
||||
unsigned i = 1; // the first literal is the FUIP
|
||||
unsigned j = 1;
|
||||
|
@ -756,7 +756,7 @@ namespace smt {
|
|||
j++;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
reset_unmark_and_justifications(0, 0);
|
||||
m_lemma .shrink(j);
|
||||
m_lemma_atoms.shrink(j);
|
||||
|
@ -810,7 +810,7 @@ namespace smt {
|
|||
}
|
||||
if (m_manager.coarse_grain_proofs())
|
||||
return pr;
|
||||
TRACE("norm_eq_proof",
|
||||
TRACE("norm_eq_proof",
|
||||
tout << "#" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";
|
||||
tout << mk_ll_pp(pr, m_manager, true, false););
|
||||
SASSERT(m_manager.is_eq(fact) || m_manager.is_iff(fact));
|
||||
|
@ -906,7 +906,7 @@ namespace smt {
|
|||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
\brief Return the proof object associated with the given literal if it already
|
||||
exists. Otherwise, return 0 and add l to the todo-list.
|
||||
|
@ -939,13 +939,13 @@ namespace smt {
|
|||
// p1: is a proof of "A"
|
||||
// p2: is a proof of "not A"
|
||||
// [unit-resolution p1 p2]: false
|
||||
//
|
||||
//
|
||||
// Let us assume that "A" was assigned first during propagation.
|
||||
// Then, the "resolve" method will never select "not A" as a hypothesis.
|
||||
// "not_A" will be the not_l argument in this method.
|
||||
// "not_A" will be the not_l argument in this method.
|
||||
// Since we are assuming that "A" was assigned first", m_ctx.get_justification("A") will be
|
||||
// p1.
|
||||
//
|
||||
//
|
||||
// So, the test "m_ctx.get_justification(l.var()) == js" is used to check
|
||||
// if l was assigned before ~l.
|
||||
if ((m_ctx.is_marked(l.var()) && m_ctx.get_justification(l.var()) == js) || (js.get_kind() == b_justification::AXIOM)) {
|
||||
|
@ -1022,11 +1022,11 @@ namespace smt {
|
|||
tout << mk_pp(m_manager.get_fact(prs[i]), m_manager) << "\n";
|
||||
}
|
||||
tout << "consequent:\n" << mk_pp(l_exr, m_manager) << "\n";);
|
||||
TRACE("get_proof",
|
||||
TRACE("get_proof",
|
||||
tout << l.index() << " " << true_literal.index() << " " << false_literal.index() << " ";
|
||||
m_ctx.display_literal(tout, l); tout << " --->\n";
|
||||
tout << mk_ll_pp(l_exr, m_manager););
|
||||
CTRACE("get_proof_bug_after",
|
||||
CTRACE("get_proof_bug_after",
|
||||
invocation_counter >= DUMP_AFTER_NUM_INVOCATIONS,
|
||||
tout << l.index() << " " << true_literal.index() << " " << false_literal.index() << " ";
|
||||
m_ctx.display_literal(tout, l); tout << " --->\n";
|
||||
|
@ -1040,7 +1040,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
\brief Return the proof object associated with the given justification
|
||||
if it already exists. Otherwise, return 0 and add js to the todo-list.
|
||||
|
@ -1094,7 +1094,7 @@ namespace smt {
|
|||
i = 2;
|
||||
}
|
||||
}
|
||||
for (; i < num_lits; i++)
|
||||
for (; i < num_lits; i++)
|
||||
if (get_proof(~cls->get_literal(i)) == 0)
|
||||
visited = false;
|
||||
return visited;
|
||||
|
@ -1109,7 +1109,7 @@ namespace smt {
|
|||
SASSERT(pr);
|
||||
TRACE("proof_gen_bug", tout << "lit2pr_saved: #" << l << "\n";);
|
||||
m_lit2proof.insert(l, pr);
|
||||
TRACE("mk_proof",
|
||||
TRACE("mk_proof",
|
||||
tout << mk_bounded_pp(m_ctx.bool_var2expr(l.var()), m_manager, 10) << "\n";
|
||||
tout << "storing proof for: "; m_ctx.display_literal(tout, l); tout << "\n";
|
||||
tout << mk_ll_pp(pr, m_manager););
|
||||
|
@ -1118,7 +1118,7 @@ namespace smt {
|
|||
/**
|
||||
\brief Given that lhs = ... = rhs, and lhs reaches rhs in the 'proof' tree branch.
|
||||
Then, return true if all proof objects needed to create the proof steps are already
|
||||
available. Otherwise return false and update m_todo_pr with info about the proof
|
||||
available. Otherwise return false and update m_todo_pr with info about the proof
|
||||
objects that need to be created.
|
||||
*/
|
||||
bool conflict_resolution::visit_trans_proof(enode * lhs, enode * rhs) {
|
||||
|
@ -1174,7 +1174,7 @@ namespace smt {
|
|||
|
||||
/**
|
||||
\brief Return true if all proof objects that are used to build the proof that lhs = rhs were
|
||||
already built. If the result is false, then m_todo_pr is updated with info about the proof
|
||||
already built. If the result is false, then m_todo_pr is updated with info about the proof
|
||||
objects that need to be created.
|
||||
*/
|
||||
bool conflict_resolution::visit_eq_justications(enode * lhs, enode * rhs) {
|
||||
|
@ -1226,7 +1226,7 @@ namespace smt {
|
|||
if (prs1.size() == 1)
|
||||
pr = prs1[0];
|
||||
else {
|
||||
TRACE("mk_transitivity",
|
||||
TRACE("mk_transitivity",
|
||||
unsigned sz = prs1.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
tout << mk_ll_pp(prs1[i], m_manager) << "\n";
|
||||
|
@ -1288,7 +1288,7 @@ namespace smt {
|
|||
}
|
||||
case tp_elem::LITERAL: {
|
||||
literal l = to_literal(elem.m_lidx);
|
||||
if (m_lit2proof.contains(l))
|
||||
if (m_lit2proof.contains(l))
|
||||
m_todo_pr.pop_back();
|
||||
else {
|
||||
b_justification js = m_ctx.get_justification(l.var());
|
||||
|
@ -1342,11 +1342,11 @@ namespace smt {
|
|||
|
||||
void conflict_resolution::process_antecedent_for_unsat_core(literal antecedent) {
|
||||
bool_var var = antecedent.var();
|
||||
TRACE("conflict", tout << "processing antecedent: ";
|
||||
m_ctx.display_literal_info(tout << antecedent << " ", antecedent);
|
||||
tout << (m_ctx.is_marked(var)?"marked":"not marked");
|
||||
tout << "\n";);
|
||||
|
||||
TRACE("conflict", tout << "processing antecedent: ";
|
||||
m_ctx.display_literal_info(tout << antecedent << " ", antecedent);
|
||||
tout << (m_ctx.is_marked(var)?"marked":"not marked");
|
||||
tout << "\n";);
|
||||
|
||||
if (!m_ctx.is_marked(var)) {
|
||||
m_ctx.set_mark(var);
|
||||
m_unmark.push_back(var);
|
||||
|
@ -1355,7 +1355,7 @@ namespace smt {
|
|||
m_assumptions.push_back(antecedent);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void conflict_resolution::process_justification_for_unsat_core(justification * js) {
|
||||
literal_vector & antecedents = m_tmp_literal_vector;
|
||||
antecedents.reset();
|
||||
|
@ -1370,7 +1370,7 @@ namespace smt {
|
|||
SASSERT(m_ctx.tracking_assumptions());
|
||||
m_assumptions.reset();
|
||||
m_unmark.reset();
|
||||
|
||||
|
||||
SASSERT(m_conflict_lvl <= m_ctx.get_search_level());
|
||||
unsigned search_lvl = m_ctx.get_search_level();
|
||||
|
||||
|
@ -1378,17 +1378,17 @@ namespace smt {
|
|||
literal consequent = false_literal;
|
||||
if (not_l != null_literal) {
|
||||
consequent = ~not_l;
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
int idx = skip_literals_above_conflict_level();
|
||||
|
||||
|
||||
if (not_l != null_literal)
|
||||
process_antecedent_for_unsat_core(consequent);
|
||||
|
||||
|
||||
if (m_assigned_literals.empty()) {
|
||||
goto end_unsat_core;
|
||||
}
|
||||
|
||||
|
||||
while (true) {
|
||||
TRACE("unsat_core_bug", tout << consequent << " js.get_kind(): " << js.get_kind() << ", idx: " << idx << "\n";);
|
||||
switch (js.get_kind()) {
|
||||
|
@ -1411,7 +1411,7 @@ namespace smt {
|
|||
process_antecedent_for_unsat_core(~l);
|
||||
}
|
||||
justification * js = cls->get_justification();
|
||||
if (js)
|
||||
if (js)
|
||||
process_justification_for_unsat_core(js);
|
||||
break;
|
||||
}
|
||||
|
@ -1430,17 +1430,17 @@ namespace smt {
|
|||
|
||||
if (m_ctx.is_assumption(consequent.var())) {
|
||||
m_assumptions.push_back(consequent);
|
||||
}
|
||||
}
|
||||
while (idx >= 0) {
|
||||
literal l = m_assigned_literals[idx];
|
||||
TRACE("unsat_core_bug", tout << "l: " << l << ", get_assign_level(l): " << m_ctx.get_assign_level(l) << ", is_marked(l): " << m_ctx.is_marked(l.var()) << "\n";);
|
||||
if (m_ctx.get_assign_level(l) < search_lvl)
|
||||
goto end_unsat_core;
|
||||
if (m_ctx.is_marked(l.var()))
|
||||
if (m_ctx.get_assign_level(l) < search_lvl)
|
||||
goto end_unsat_core;
|
||||
if (m_ctx.is_marked(l.var()))
|
||||
break;
|
||||
idx--;
|
||||
}
|
||||
if (idx < 0) {
|
||||
if (idx < 0) {
|
||||
goto end_unsat_core;
|
||||
}
|
||||
|
||||
|
@ -1456,12 +1456,12 @@ namespace smt {
|
|||
TRACE("unsat_core", tout << "assumptions:\n"; m_ctx.display_literals(tout, m_assumptions); tout << "\n";);
|
||||
reset_unmark_and_justifications(0, 0);
|
||||
}
|
||||
|
||||
conflict_resolution * mk_conflict_resolution(ast_manager & m,
|
||||
|
||||
conflict_resolution * mk_conflict_resolution(ast_manager & m,
|
||||
context & ctx,
|
||||
dyn_ack_manager & dack_manager,
|
||||
smt_params const & params,
|
||||
literal_vector const & assigned_literals,
|
||||
literal_vector const & assigned_literals,
|
||||
vector<watch_list> & watches) {
|
||||
return alloc(conflict_resolution, m, ctx, dack_manager, params, assigned_literals, watches);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue