mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng
Conflicts: scripts/mk_util.py
This commit is contained in:
commit
1c9051016a
|
@ -2665,10 +2665,10 @@ void fpa_example() {
|
|||
c2 = Z3_mk_fpa_to_fp_bv(ctx,
|
||||
Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)),
|
||||
Z3_mk_fpa_sort(ctx, 11, 53));
|
||||
c3 = Z3_mk_fpa_to_fp_real_int(ctx,
|
||||
c3 = Z3_mk_fpa_to_fp_int_real(ctx,
|
||||
Z3_mk_fpa_rtz(ctx),
|
||||
Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)),
|
||||
Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)),
|
||||
Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)),
|
||||
Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)),
|
||||
Z3_mk_fpa_sort(ctx, 11, 53));
|
||||
c4 = Z3_mk_fpa_to_fp_real(ctx,
|
||||
Z3_mk_fpa_rtz(ctx),
|
||||
|
|
|
@ -64,6 +64,7 @@ VERBOSE=True
|
|||
DEBUG_MODE=False
|
||||
SHOW_CPPS = True
|
||||
VS_X64 = False
|
||||
LINUX_X64 = True
|
||||
ONLY_MAKEFILES = False
|
||||
Z3PY_SRC_DIR=None
|
||||
VS_PROJ = False
|
||||
|
@ -389,7 +390,8 @@ def find_ml_lib():
|
|||
return
|
||||
|
||||
def is64():
|
||||
return sys.maxsize >= 2**32
|
||||
global LINUX_X64
|
||||
return LINUX_X64 and sys.maxsize >= 2**32
|
||||
|
||||
def check_ar():
|
||||
if is_verbose():
|
||||
|
@ -505,6 +507,8 @@ def display_help(exit_code):
|
|||
print(" -t, --trace enable tracing in release mode.")
|
||||
if IS_WINDOWS:
|
||||
print(" -x, --x64 create 64 binary when using Visual Studio.")
|
||||
else:
|
||||
print(" --x86 force 32-bit x86 build on x64 systems.")
|
||||
print(" -m, --makefiles generate only makefiles.")
|
||||
if IS_WINDOWS:
|
||||
print(" -v, --vsproj generate Visual Studio Project Files.")
|
||||
|
@ -536,12 +540,13 @@ def display_help(exit_code):
|
|||
def parse_options():
|
||||
global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
|
||||
global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
|
||||
global LINUX_X64
|
||||
try:
|
||||
options, remainder = getopt.gnu_getopt(sys.argv[1:],
|
||||
'b:df:sxhmcvtnp:gj',
|
||||
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
|
||||
'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
|
||||
'githash=', 'ml'])
|
||||
'githash=', 'x86'])
|
||||
except:
|
||||
print("ERROR: Invalid command line option")
|
||||
display_help(1)
|
||||
|
@ -560,6 +565,8 @@ def parse_options():
|
|||
if not IS_WINDOWS:
|
||||
raise MKException('x64 compilation mode can only be specified when using Visual Studio')
|
||||
VS_X64 = True
|
||||
elif opt in ('--x86'):
|
||||
LINUX_X64=False
|
||||
elif opt in ('-h', '--help'):
|
||||
display_help(0)
|
||||
elif opt in ('-m', '--onlymakefiles'):
|
||||
|
@ -1823,6 +1830,10 @@ def mk_config():
|
|||
CPPFLAGS = '%s -D_AMD64_' % CPPFLAGS
|
||||
if sysname == 'Linux':
|
||||
CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS
|
||||
elif not LINUX_X64:
|
||||
CXXFLAGS = '%s -m32' % CXXFLAGS
|
||||
LDFLAGS = '%s -m32' % LDFLAGS
|
||||
SLIBFLAGS = '%s -m32' % SLIBFLAGS
|
||||
if DEBUG_MODE:
|
||||
CPPFLAGS = '%s -DZ3DEBUG' % CPPFLAGS
|
||||
if TRACE or DEBUG_MODE:
|
||||
|
|
|
@ -14,7 +14,7 @@ Author:
|
|||
Christoph M. Wintersteiger (cwinter) 2013-06-05
|
||||
|
||||
Notes:
|
||||
|
||||
|
||||
--*/
|
||||
#include<iostream>
|
||||
#include"z3.h"
|
||||
|
@ -27,21 +27,22 @@ extern "C" {
|
|||
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_rounding_mode_sort(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_sort r = of_sort(ctx->fpautil().mk_rm_sort());
|
||||
RETURN_Z3(r);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
sort * s = ctx->fpautil().mk_rm_sort();
|
||||
mk_c(c)->save_ast_trail(s);
|
||||
RETURN_Z3(of_sort(s));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c)
|
||||
{
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
|
||||
RESET_ERROR_CODE();
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_even());
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_round_nearest_ties_to_even();
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -50,19 +51,20 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_rne(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_even());
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_round_nearest_ties_to_even();
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c)
|
||||
{
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_round_nearest_ties_to_away(c);
|
||||
RESET_ERROR_CODE();
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_away());
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_round_nearest_ties_to_away();
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -71,19 +73,20 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_rna(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_away());
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_round_nearest_ties_to_away();
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c)
|
||||
{
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_round_toward_positive(c);
|
||||
RESET_ERROR_CODE();
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_positive());
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_round_toward_positive();
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -92,19 +95,20 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_rtp(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_positive());
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_round_toward_positive();
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c)
|
||||
{
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_round_toward_negative(c);
|
||||
RESET_ERROR_CODE();
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_negative());
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_round_toward_negative();
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -113,19 +117,20 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_rtn(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_negative());
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_round_toward_negative();
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c)
|
||||
{
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_round_toward_zero(c);
|
||||
RESET_ERROR_CODE();
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_zero());
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_round_toward_zero();
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -134,8 +139,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_rtz(c);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_zero());
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_round_toward_zero();
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -143,13 +149,14 @@ extern "C" {
|
|||
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_sort(c, ebits, sbits);
|
||||
RESET_ERROR_CODE();
|
||||
RESET_ERROR_CODE();
|
||||
if (ebits < 2 || sbits < 3) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
}
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_sort r = of_sort(ctx->fpautil().mk_float_sort(ebits, sbits));
|
||||
RETURN_Z3(r);
|
||||
}
|
||||
api::context * ctx = mk_c(c);
|
||||
sort * s = ctx->fpautil().mk_float_sort(ebits, sbits);
|
||||
ctx->save_ast_trail(s);
|
||||
RETURN_Z3(of_sort(s));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -188,21 +195,23 @@ extern "C" {
|
|||
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_nan(c, s);
|
||||
RESET_ERROR_CODE();
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_nan(to_sort(s)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_nan(to_sort(s));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, Z3_bool negative) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_inf(c, s, negative);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(negative != 0 ? ctx->fpautil().mk_ninf(to_sort(s)) :
|
||||
ctx->fpautil().mk_pinf(to_sort(s)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = negative != 0 ? ctx->fpautil().mk_ninf(to_sort(s)) :
|
||||
ctx->fpautil().mk_pinf(to_sort(s));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -211,9 +220,10 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_inf(c, s, negative);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(negative != 0 ? ctx->fpautil().mk_nzero(to_sort(s)) :
|
||||
ctx->fpautil().mk_pzero(to_sort(s)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = negative != 0 ? ctx->fpautil().mk_nzero(to_sort(s)) :
|
||||
ctx->fpautil().mk_pzero(to_sort(s));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -222,8 +232,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_fp(c, sgn, sig, exp);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_fp(to_expr(sgn), to_expr(sig), to_expr(exp));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -233,12 +244,13 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
scoped_mpf tmp(ctx->fpautil().fm());
|
||||
ctx->fpautil().fm().set(tmp,
|
||||
ctx->fpautil().get_ebits(to_sort(ty)),
|
||||
ctx->fpautil().get_sbits(to_sort(ty)),
|
||||
v);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
|
||||
RETURN_Z3(r);
|
||||
ctx->fpautil().fm().set(tmp,
|
||||
ctx->fpautil().get_ebits(to_sort(ty)),
|
||||
ctx->fpautil().get_sbits(to_sort(ty)),
|
||||
v);
|
||||
expr * a = ctx->fpautil().mk_value(tmp);
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -249,8 +261,9 @@ extern "C" {
|
|||
api::context * ctx = mk_c(c);
|
||||
scoped_mpf tmp(ctx->fpautil().fm());
|
||||
ctx->fpautil().fm().set(tmp, ctx->fpautil().get_ebits(to_sort(ty)), ctx->fpautil().get_sbits(to_sort(ty)), v);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_value(tmp);
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -261,11 +274,12 @@ extern "C" {
|
|||
api::context * ctx = mk_c(c);
|
||||
scoped_mpf tmp(ctx->fpautil().fm());
|
||||
ctx->fpautil().fm().set(tmp,
|
||||
ctx->fpautil().get_ebits(to_sort(ty)),
|
||||
ctx->fpautil().get_sbits(to_sort(ty)),
|
||||
v);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
|
||||
RETURN_Z3(r);
|
||||
ctx->fpautil().get_ebits(to_sort(ty)),
|
||||
ctx->fpautil().get_sbits(to_sort(ty)),
|
||||
v);
|
||||
expr * a = ctx->fpautil().mk_value(tmp);
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -275,12 +289,13 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
scoped_mpf tmp(ctx->fpautil().fm());
|
||||
ctx->fpautil().fm().set(tmp,
|
||||
ctx->fpautil().get_ebits(to_sort(ty)),
|
||||
ctx->fpautil().get_sbits(to_sort(ty)),
|
||||
sgn != 0, sig, exp);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
|
||||
RETURN_Z3(r);
|
||||
ctx->fpautil().fm().set(tmp,
|
||||
ctx->fpautil().get_ebits(to_sort(ty)),
|
||||
ctx->fpautil().get_sbits(to_sort(ty)),
|
||||
sgn != 0, sig, exp);
|
||||
expr * a = ctx->fpautil().mk_value(tmp);
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -291,111 +306,122 @@ extern "C" {
|
|||
api::context * ctx = mk_c(c);
|
||||
scoped_mpf tmp(ctx->fpautil().fm());
|
||||
ctx->fpautil().fm().set(tmp,
|
||||
ctx->fpautil().get_ebits(to_sort(ty)),
|
||||
ctx->fpautil().get_sbits(to_sort(ty)),
|
||||
sgn != 0, sig, exp);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_value(tmp));
|
||||
RETURN_Z3(r);
|
||||
ctx->fpautil().get_ebits(to_sort(ty)),
|
||||
ctx->fpautil().get_sbits(to_sort(ty)),
|
||||
sgn != 0, sig, exp);
|
||||
expr * a = ctx->fpautil().mk_value(tmp);
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_abs(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_abs(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_abs(to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_neg(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_neg(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_neg(to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_add(to_expr(rm), to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_add(to_expr(rm), to_expr(t1), to_expr(t2));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_div(to_expr(rm), to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_div(to_expr(rm), to_expr(t1), to_expr(t2));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_fma(c, rm, t1, t2, t3);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_fma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_sqrt(c, rm, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_sqrt(to_expr(rm), to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_sqrt(to_expr(rm), to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_rem(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_rem(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_rem(to_expr(t1), to_expr(t2));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_round_to_integral(c, rm, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_round_to_integral(to_expr(rm), to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_round_to_integral(to_expr(rm), to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -404,8 +430,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_min(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_min(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_min(to_expr(t1), to_expr(t2));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -418,14 +445,15 @@ extern "C" {
|
|||
RETURN_Z3(r);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_leq(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_le(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_le(to_expr(t1), to_expr(t2));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -434,18 +462,20 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_lt(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_lt(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_lt(to_expr(t1), to_expr(t2));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_geq(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_ge(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_ge(to_expr(t1), to_expr(t2));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -454,8 +484,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_gt(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_gt(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_gt(to_expr(t1), to_expr(t2));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -464,18 +495,20 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_eq(c, t1, t2);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_float_eq(to_expr(t1), to_expr(t2)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_float_eq(to_expr(t1), to_expr(t2));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_is_normal(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_is_normal(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_is_normal(to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -484,8 +517,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_is_subnormal(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_is_subnormal(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_is_subnormal(to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -494,8 +528,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_is_zero(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_is_zero(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_is_zero(to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -504,8 +539,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_is_infinite(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_is_inf(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_is_inf(to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -514,8 +550,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_is_nan(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_is_nan(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_is_nan(to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -524,8 +561,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_is_negative(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_is_negative(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_is_negative(to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -534,8 +572,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_is_positive(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_is_positive(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_is_positive(to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -551,8 +590,9 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(bv)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = fu.mk_to_fp(to_sort(s), to_expr(bv));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -562,14 +602,15 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
if (!fu.is_rm(to_expr(rm)) ||
|
||||
if (!fu.is_rm(to_expr(rm)) ||
|
||||
!fu.is_float(to_expr(t)) ||
|
||||
!fu.is_float(to_sort(s))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -585,8 +626,9 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -602,8 +644,9 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -613,14 +656,15 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
if (!fu.is_rm(to_expr(rm)) ||
|
||||
if (!fu.is_rm(to_expr(rm)) ||
|
||||
!ctx->bvutil().is_bv(to_expr(t)) ||
|
||||
!fu.is_float(to_sort(s))) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
Z3_ast r = of_ast(fu.mk_to_fp_unsigned(to_sort(s), to_expr(rm), to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = fu.mk_to_fp_unsigned(to_sort(s), to_expr(rm), to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -629,8 +673,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_to_ubv(c, rm, t, sz);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_to_ubv(to_expr(rm), to_expr(t), sz));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_to_ubv(to_expr(rm), to_expr(t), sz);
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -639,8 +684,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_to_sbv(c, rm, t, sz);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_to_sbv(to_expr(rm), to_expr(t), sz));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_to_sbv(to_expr(rm), to_expr(t), sz);
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -649,8 +695,9 @@ extern "C" {
|
|||
LOG_Z3_mk_fpa_to_real(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
Z3_ast r = of_ast(ctx->fpautil().mk_to_real(to_expr(t)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = ctx->fpautil().mk_to_real(to_expr(t));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
@ -689,7 +736,7 @@ extern "C" {
|
|||
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);
|
||||
|
@ -699,14 +746,14 @@ extern "C" {
|
|||
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
|
||||
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)) {
|
||||
scoped_mpf val(mpfm);
|
||||
if (!plugin->is_numeral(to_expr(t), val)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return "";
|
||||
}
|
||||
else if (!mpfm.is_regular(val)) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG)
|
||||
return "";
|
||||
return "";
|
||||
}
|
||||
unsigned sbits = val.get().get_sbits();
|
||||
scoped_mpq q(mpqm);
|
||||
|
@ -726,7 +773,7 @@ extern "C" {
|
|||
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)->fpautil().fm();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().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);
|
||||
|
@ -738,7 +785,7 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_INVALID_ARG)
|
||||
return "";
|
||||
}
|
||||
mpf_exp_t exp = mpfm.exp_normalized(val);
|
||||
mpf_exp_t exp = mpfm.exp_normalized(val);
|
||||
std::stringstream ss;
|
||||
ss << exp;
|
||||
return mk_c(c)->mk_external_string(ss.str());
|
||||
|
@ -753,7 +800,7 @@ extern "C" {
|
|||
mpf_manager & mpfm = mk_c(c)->fpautil().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);
|
||||
bool r = plugin->is_numeral(to_expr(t), val);
|
||||
if (!r) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
|
@ -773,9 +820,9 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_real_int(Z3_context c, Z3_ast rm, Z3_ast sig, Z3_ast exp, Z3_sort s) {
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_fpa_to_fp_real_int(c, rm, sig, exp, s);
|
||||
LOG_Z3_mk_fpa_to_fp_int_real(c, rm, sig, exp, s);
|
||||
RESET_ERROR_CODE();
|
||||
api::context * ctx = mk_c(c);
|
||||
fpa_util & fu = ctx->fpautil();
|
||||
|
@ -786,8 +833,9 @@ extern "C" {
|
|||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
Z3_ast r = of_ast(fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(sig), to_expr(exp)));
|
||||
RETURN_Z3(r);
|
||||
expr * a = fu.mk_to_fp(to_sort(s), to_expr(rm), to_expr(sig), to_expr(exp));
|
||||
ctx->save_ast_trail(a);
|
||||
RETURN_Z3(of_expr(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
|
|
|
@ -4227,13 +4227,13 @@ namespace Microsoft.Z3
|
|||
/// according to rounding mode rm.
|
||||
/// </remarks>
|
||||
/// <param name="rm">RoundingMode term.</param>
|
||||
/// <param name="sig">Significand term of Real sort.</param>
|
||||
/// <param name="exp">Exponent term of Int sort.</param>
|
||||
/// <param name="sig">Significand term of Real sort.</param>
|
||||
/// <param name="s">FloatingPoint sort.</param>
|
||||
public BitVecExpr MkFPToFP(FPRMExpr rm, RealExpr sig, IntExpr exp, FPSort s)
|
||||
public BitVecExpr MkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s)
|
||||
{
|
||||
Contract.Ensures(Contract.Result<BitVecExpr>() != null);
|
||||
return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_real_int(this.nCtx, rm.NativeObject, sig.NativeObject, exp.NativeObject, s.NativeObject));
|
||||
return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_int_real(this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.NativeObject));
|
||||
}
|
||||
#endregion
|
||||
#endregion // Floating-point Arithmetic
|
||||
|
|
|
@ -3542,8 +3542,8 @@ public class Context extends IDisposable
|
|||
/**
|
||||
* Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
|
||||
* @param rm RoundingMode term.
|
||||
* @param sig Significand term of Real sort.
|
||||
* @param exp Exponent term of Int sort.
|
||||
* @param sig Significand term of Real sort.
|
||||
* @param s FloatingPoint sort.
|
||||
* Remarks:
|
||||
* Produces a term that represents the conversion of sig * 2^exp into a
|
||||
|
@ -3552,9 +3552,9 @@ public class Context extends IDisposable
|
|||
* @throws Z3Exception
|
||||
**/
|
||||
|
||||
public BitVecExpr mkFPToFP(FPRMExpr rm, RealExpr sig, IntExpr exp, FPSort s) throws Z3Exception
|
||||
public BitVecExpr mkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s) throws Z3Exception
|
||||
{
|
||||
return new BitVecExpr(this, Native.mkFpaToFpRealInt(nCtx(), rm.getNativeObject(), sig.getNativeObject(), exp.getNativeObject(), s.getNativeObject()));
|
||||
return new BitVecExpr(this, Native.mkFpaToFpIntReal(nCtx(), rm.getNativeObject(), exp.getNativeObject(), sig.getNativeObject(), s.getNativeObject()));
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -274,7 +274,7 @@ extern "C" {
|
|||
Z3_ast Z3_API Z3_mk_fpa_fp(__in Z3_context c, __in Z3_ast sgn, __in Z3_ast exp, __in Z3_ast sig);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of FloatingPoint sort from a float.
|
||||
\brief Create a numeral of FloatingPoint sort from a float.
|
||||
|
||||
This function is used to create numerals that fit in a float value.
|
||||
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
|
||||
|
@ -292,20 +292,20 @@ extern "C" {
|
|||
Z3_ast Z3_API Z3_mk_fpa_numeral_float(__in Z3_context c, __in float v, __in Z3_sort ty);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of FloatingPoint sort from a double.
|
||||
\brief Create a numeral of FloatingPoint sort from a double.
|
||||
|
||||
This function is used to create numerals that fit in a double value.
|
||||
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
|
||||
This function is used to create numerals that fit in a double value.
|
||||
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
|
||||
|
||||
\param c logical context
|
||||
\param v value
|
||||
\param ty sort
|
||||
\param c logical context
|
||||
\param v value
|
||||
\param ty sort
|
||||
|
||||
ty must be a FloatingPoint sort
|
||||
ty must be a FloatingPoint sort
|
||||
|
||||
\sa Z3_mk_numeral
|
||||
\sa Z3_mk_numeral
|
||||
|
||||
def_API('Z3_mk_fpa_numeral_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT)))
|
||||
def_API('Z3_mk_fpa_numeral_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_numeral_double(__in Z3_context c, __in double v, __in Z3_sort ty);
|
||||
|
||||
|
@ -501,10 +501,10 @@ extern "C" {
|
|||
t1, t2 must have the same FloatingPoint sort.
|
||||
|
||||
def_API('Z3_mk_fpa_min', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_min(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_min(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
|
||||
|
||||
/**
|
||||
/**
|
||||
\brief Maximum of floating-point numbers.
|
||||
|
||||
\param c logical context
|
||||
|
@ -905,15 +905,15 @@ extern "C" {
|
|||
|
||||
\param c logical context
|
||||
\param rm term of RoundingMode sort
|
||||
\param sig significand term of Real sort
|
||||
\param exp exponent term of Int sort
|
||||
\param sig significand term of Real sort
|
||||
\param s FloatingPoint sort
|
||||
|
||||
s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of real sort.
|
||||
s must be a FloatingPoint sort, rm must be of RoundingMode sort, exp must be of int sort, sig must be of real sort.
|
||||
|
||||
def_API('Z3_mk_fpa_to_fp_real_int', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(SORT)))
|
||||
def_API('Z3_mk_fpa_to_fp_int_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_real_int(__in Z3_context c, __in Z3_ast rm, __in Z3_ast sig, __in Z3_ast exp, __in Z3_sort s);
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(__in Z3_context c, __in Z3_ast rm, __in Z3_ast exp, __in Z3_ast sig, __in Z3_sort s);
|
||||
|
||||
/*@}*/
|
||||
|
||||
|
|
Loading…
Reference in a new issue