From a9840b291f2ce960910b7fec6209e74a8b02d665 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 10 Jun 2013 19:06:45 +0100
Subject: [PATCH] FPA API: Tied into rest of the API; added numeral/value
handling through existing functions; added trivial .NET example.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
examples/dotnet/Program.cs | 12 ++++++
src/api/api_ast.cpp | 6 +++
src/api/api_context.cpp | 2 +
src/api/api_context.h | 5 +++
src/api/api_fpa.cpp | 78 ++++++++++++++++++-------------------
src/api/api_numeral.cpp | 35 ++++++++++++++---
src/api/dotnet/Expr.cs | 8 +++-
src/api/z3_api.h | 2 +
src/ast/float_decl_plugin.h | 8 ++--
9 files changed, 104 insertions(+), 52 deletions(-)
diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs
index 2085de296..c75553e7b 100644
--- a/examples/dotnet/Program.cs
+++ b/examples/dotnet/Program.cs
@@ -2022,6 +2022,17 @@ namespace test_mapi
// Console.WriteLine("{0}", ctx.MkEq(s1, t1));
}
+ public static void FloatingPointExample(Context ctx)
+ {
+ Console.WriteLine("FloatingPointExample");
+
+ FPSort s = ctx.MkFPSort(11, 53);
+ Console.WriteLine("Sort: {0}", s);
+
+ FPNum n = (FPNum) ctx.MkNumeral("0.125", s);
+ Console.WriteLine("Numeral: {0}", n.ToString());
+ }
+
static void Main(string[] args)
{
try
@@ -2063,6 +2074,7 @@ namespace test_mapi
FindSmallModelExample(ctx);
SimplifierExample(ctx);
FiniteDomainExample(ctx);
+ FloatingPointExample(ctx);
}
// These examples need proof generation turned on.
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 6855f6209..ccc2cbf88 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -647,6 +647,12 @@ extern "C" {
else if (fid == mk_c(c)->get_datalog_fid() && k == datalog::DL_FINITE_SORT) {
return Z3_FINITE_DOMAIN_SORT;
}
+ else if (fid == mk_c(c)->get_fpa_fid() && k == FLOAT_SORT) {
+ return Z3_FLOATING_POINT_SORT;
+ }
+ else if (fid == mk_c(c)->get_fpa_fid() && k == ROUNDING_MODE_SORT) {
+ return Z3_FLOATING_POINT_ROUNDING_MODE_SORT;
+ }
else {
return Z3_UNKNOWN_SORT;
}
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index cf179332a..f4314dcca 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -88,6 +88,7 @@ namespace api {
m_arith_util(m()),
m_bv_util(m()),
m_datalog_util(m()),
+ m_float_util(m()),
m_last_result(m()),
m_ast_trail(m()),
m_replay_stack() {
@@ -112,6 +113,7 @@ namespace api {
m_array_fid = m().mk_family_id("array");
m_dt_fid = m().mk_family_id("datatype");
m_datalog_fid = m().mk_family_id("datalog_relation");
+ m_fpa_fid = m().mk_family_id("float");
m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
if (!m_user_ref_count) {
diff --git a/src/api/api_context.h b/src/api/api_context.h
index e0c95b07b..f409a4ece 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -27,6 +27,7 @@ Revision History:
#include"bv_decl_plugin.h"
#include"datatype_decl_plugin.h"
#include"dl_decl_plugin.h"
+#include"float_decl_plugin.h"
#include"smt_kernel.h"
#include"smt_params.h"
#include"event_handler.h"
@@ -56,6 +57,7 @@ namespace api {
arith_util m_arith_util;
bv_util m_bv_util;
datalog::dl_decl_util m_datalog_util;
+ float_util m_float_util;
// Support for old solver API
smt_params m_fparams;
@@ -75,6 +77,7 @@ namespace api {
family_id m_bv_fid;
family_id m_dt_fid;
family_id m_datalog_fid;
+ family_id m_fpa_fid;
datatype_decl_plugin * m_dt_plugin;
std::string m_string_buffer; // temporary buffer used to cache strings sent to the "external" world.
@@ -115,12 +118,14 @@ namespace api {
arith_util & autil() { return m_arith_util; }
bv_util & bvutil() { return m_bv_util; }
datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
+ float_util & float_util() { return m_float_util; }
family_id get_basic_fid() const { return m_basic_fid; }
family_id get_array_fid() const { return m_array_fid; }
family_id get_arith_fid() const { return m_arith_fid; }
family_id get_bv_fid() const { return m_bv_fid; }
family_id get_dt_fid() const { return m_dt_fid; }
family_id get_datalog_fid() const { return m_datalog_fid; }
+ family_id get_fpa_fid() const { return m_fpa_fid; }
datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; }
Z3_error_code get_error_code() const { return m_error_code; }
diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index cfb5a2624..278a0556a 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -28,7 +28,7 @@ extern "C" {
LOG_Z3_mk_fpa_rounding_mode_sort(c);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_sort r = of_sort(float_util(ctx->m()).mk_rm_sort());
+ Z3_sort r = of_sort(ctx->float_util().mk_rm_sort());
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -39,7 +39,7 @@ extern "C" {
LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_round_nearest_ties_to_even());
+ Z3_ast r = of_ast(ctx->float_util().mk_round_nearest_ties_to_even());
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -50,7 +50,7 @@ extern "C" {
LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_round_nearest_ties_to_away());
+ Z3_ast r = of_ast(ctx->float_util().mk_round_nearest_ties_to_away());
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -61,7 +61,7 @@ extern "C" {
LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_round_toward_positive());
+ Z3_ast r = of_ast(ctx->float_util().mk_round_toward_positive());
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -72,7 +72,7 @@ extern "C" {
LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_round_toward_negative());
+ Z3_ast r = of_ast(ctx->float_util().mk_round_toward_negative());
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -83,7 +83,7 @@ extern "C" {
LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_round_toward_zero());
+ Z3_ast r = of_ast(ctx->float_util().mk_round_toward_zero());
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -95,9 +95,8 @@ extern "C" {
if (ebits < 2 || sbits < 3) {
SET_ERROR_CODE(Z3_INVALID_ARG);
}
- api::context * ctx = mk_c(c);
- float_util fu(ctx->m());
- Z3_sort r = of_sort(fu.mk_float_sort(ebits, sbits));
+ api::context * ctx = mk_c(c);
+ Z3_sort r = of_sort(ctx->float_util().mk_float_sort(ebits, sbits));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -107,7 +106,7 @@ extern "C" {
LOG_Z3_mk_fpa_nan(c, s);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_nan(to_sort(s)));
+ Z3_ast r = of_ast(ctx->float_util().mk_nan(to_sort(s)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -117,8 +116,7 @@ extern "C" {
LOG_Z3_mk_fpa_inf(c, s, negative);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- float_util fu(ctx->m());
- Z3_ast r = of_ast(negative != 0 ? fu.mk_minus_inf(to_sort(s)) : fu.mk_plus_inf(to_sort(s)));
+ Z3_ast r = of_ast(negative != 0 ? ctx->float_util().mk_minus_inf(to_sort(s)) : ctx->float_util().mk_plus_inf(to_sort(s)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -128,10 +126,9 @@ extern "C" {
LOG_Z3_mk_double(c, v, ty);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- float_util fu(ctx->m());
- mpf tmp;
- fu.fm().set(tmp, fu.get_ebits(to_sort(ty)), fu.get_sbits(to_sort(ty)), v);
- Z3_ast r = of_ast(fu.mk_value(tmp));
+ scoped_mpf tmp(ctx->float_util().fm());
+ ctx->float_util().fm().set(tmp, ctx->float_util().get_ebits(to_sort(ty)), ctx->float_util().get_sbits(to_sort(ty)), v);
+ Z3_ast r = of_ast(ctx->float_util().mk_value(tmp));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -141,7 +138,7 @@ extern "C" {
LOG_Z3_mk_fpa_abs(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_abs(to_expr(t)));
+ Z3_ast r = of_ast(ctx->float_util().mk_abs(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -151,7 +148,7 @@ extern "C" {
LOG_Z3_mk_fpa_neg(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_uminus(to_expr(t)));
+ Z3_ast r = of_ast(ctx->float_util().mk_uminus(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -161,7 +158,7 @@ extern "C" {
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_add(to_expr(rm), to_expr(t1), to_expr(t2)));
+ Z3_ast r = of_ast(ctx->float_util().mk_add(to_expr(rm), to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -171,7 +168,7 @@ extern "C" {
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_sub(to_expr(rm), to_expr(t1), to_expr(t2)));
+ Z3_ast r = of_ast(ctx->float_util().mk_sub(to_expr(rm), to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -181,7 +178,7 @@ extern "C" {
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_mul(to_expr(rm), to_expr(t1), to_expr(t2)));
+ Z3_ast r = of_ast(ctx->float_util().mk_mul(to_expr(rm), to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -191,7 +188,7 @@ extern "C" {
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_div(to_expr(rm), to_expr(t1), to_expr(t2)));
+ Z3_ast r = of_ast(ctx->float_util().mk_div(to_expr(rm), to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -201,7 +198,7 @@ extern "C" {
LOG_Z3_mk_fpa_fma(c, rm, t1, t2, t3);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_fused_ma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3)));
+ Z3_ast r = of_ast(ctx->float_util().mk_fused_ma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -211,7 +208,7 @@ extern "C" {
LOG_Z3_mk_fpa_sqrt(c, rm, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_sqrt(to_expr(rm), to_expr(t)));
+ Z3_ast r = of_ast(ctx->float_util().mk_sqrt(to_expr(rm), to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -221,7 +218,7 @@ extern "C" {
LOG_Z3_mk_fpa_rem(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_rem(to_expr(t1), to_expr(t2)));
+ Z3_ast r = of_ast(ctx->float_util().mk_rem(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -231,7 +228,7 @@ extern "C" {
LOG_Z3_mk_fpa_eq(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_float_eq(to_expr(t1), to_expr(t2)));
+ Z3_ast r = of_ast(ctx->float_util().mk_float_eq(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -241,7 +238,7 @@ extern "C" {
LOG_Z3_mk_fpa_le(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_le(to_expr(t1), to_expr(t2)));
+ Z3_ast r = of_ast(ctx->float_util().mk_le(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -251,7 +248,7 @@ extern "C" {
LOG_Z3_mk_fpa_lt(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_lt(to_expr(t1), to_expr(t2)));
+ Z3_ast r = of_ast(ctx->float_util().mk_lt(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -261,7 +258,7 @@ extern "C" {
LOG_Z3_mk_fpa_ge(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_ge(to_expr(t1), to_expr(t2)));
+ Z3_ast r = of_ast(ctx->float_util().mk_ge(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -271,7 +268,7 @@ extern "C" {
LOG_Z3_mk_fpa_gt(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_gt(to_expr(t1), to_expr(t2)));
+ Z3_ast r = of_ast(ctx->float_util().mk_gt(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -281,7 +278,7 @@ extern "C" {
LOG_Z3_mk_fpa_is_normal(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_is_normal(to_expr(t)));
+ Z3_ast r = of_ast(ctx->float_util().mk_is_normal(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -291,7 +288,7 @@ extern "C" {
LOG_Z3_mk_fpa_is_subnormal(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_is_subnormal(to_expr(t)));
+ Z3_ast r = of_ast(ctx->float_util().mk_is_subnormal(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -301,7 +298,7 @@ extern "C" {
LOG_Z3_mk_fpa_is_zero(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_is_zero(to_expr(t)));
+ Z3_ast r = of_ast(ctx->float_util().mk_is_zero(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -311,7 +308,7 @@ extern "C" {
LOG_Z3_mk_fpa_is_inf(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_is_inf(to_expr(t)));
+ Z3_ast r = of_ast(ctx->float_util().mk_is_inf(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -321,7 +318,7 @@ extern "C" {
LOG_Z3_mk_fpa_is_nan(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_is_nan(to_expr(t)));
+ Z3_ast r = of_ast(ctx->float_util().mk_is_nan(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -331,7 +328,7 @@ extern "C" {
LOG_Z3_mk_fpa_min(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_min(to_expr(t1), to_expr(t2)));
+ Z3_ast r = of_ast(ctx->float_util().mk_min(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -341,7 +338,7 @@ extern "C" {
LOG_Z3_mk_fpa_max(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_max(to_expr(t1), to_expr(t2)));
+ Z3_ast r = of_ast(ctx->float_util().mk_max(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
@@ -350,10 +347,9 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_fpa_convert(c, s, rm, t);
RESET_ERROR_CODE();
- api::context * ctx = mk_c(c);
- float_util fu(ctx->m());
+ api::context * ctx = mk_c(c);
expr * args [2] = { to_expr(rm), to_expr(t) };
- Z3_ast r = of_ast(ctx->m().mk_app(fu.get_family_id(), OP_TO_FLOAT,
+ Z3_ast r = of_ast(ctx->m().mk_app(ctx->float_util().get_family_id(), OP_TO_FLOAT,
to_sort(s)->get_num_parameters(), to_sort(s)->get_parameters(),
2, args));
RETURN_Z3(r);
@@ -365,7 +361,7 @@ extern "C" {
LOG_Z3_mk_fpa_to_ieee_bv(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
- Z3_ast r = of_ast(float_util(ctx->m()).mk_to_ieee_bv(to_expr(t)));
+ Z3_ast r = of_ast(ctx->float_util().mk_to_ieee_bv(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp
index d4a6587bc..6924afff3 100644
--- a/src/api/api_numeral.cpp
+++ b/src/api/api_numeral.cpp
@@ -23,13 +23,15 @@ Revision History:
#include"arith_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"algebraic_numbers.h"
+#include"float_decl_plugin.h"
bool is_numeral_sort(Z3_context c, Z3_sort ty) {
sort * _ty = to_sort(ty);
family_id fid = _ty->get_family_id();
if (fid != mk_c(c)->get_arith_fid() &&
fid != mk_c(c)->get_bv_fid() &&
- fid != mk_c(c)->get_datalog_fid()) {
+ fid != mk_c(c)->get_datalog_fid() &&
+ fid != mk_c(c)->get_fpa_fid()) {
return false;
}
return true;
@@ -69,7 +71,19 @@ extern "C" {
}
++m;
}
- ast * a = mk_c(c)->mk_numeral_core(rational(n), to_sort(ty));
+ ast * a = 0;
+ sort * _ty = to_sort(ty);
+ if (_ty->get_family_id() == mk_c(c)->get_fpa_fid())
+ {
+ // avoid expanding floats into huge rationals.
+ float_util & fu = mk_c(c)->float_util();
+ scoped_mpf t(fu.fm());
+ fu.fm().set(t, fu.get_ebits(_ty), fu.get_sbits(_ty), MPF_ROUND_TOWARD_ZERO, n);
+ a = fu.mk_value(t);
+ mk_c(c)->save_ast_trail(a);
+ }
+ else
+ a = mk_c(c)->mk_numeral_core(rational(n), _ty);
RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0);
}
@@ -131,7 +145,8 @@ extern "C" {
expr* e = to_expr(a);
return
mk_c(c)->autil().is_numeral(e) ||
- mk_c(c)->bvutil().is_numeral(e);
+ mk_c(c)->bvutil().is_numeral(e) ||
+ mk_c(c)->float_util().is_value(e);
Z3_CATCH_RETURN(Z3_FALSE);
}
@@ -155,7 +170,7 @@ extern "C" {
if (mk_c(c)->datalog_util().is_numeral(e, v)) {
r = rational(v, rational::ui64());
return Z3_TRUE;
- }
+ }
return Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
}
@@ -172,8 +187,16 @@ extern "C" {
return mk_c(c)->mk_external_string(r.to_string());
}
else {
- SET_ERROR_CODE(Z3_INVALID_ARG);
- return "";
+ // floats are separated from all others to avoid huge rationals.
+ float_util & fu = mk_c(c)->float_util();
+ scoped_mpf tmp(fu.fm());
+ if (mk_c(c)->float_util().is_numeral(to_expr(a), tmp)) {
+ return mk_c(c)->mk_external_string(fu.fm().to_string(tmp));
+ }
+ else {
+ SET_ERROR_CODE(Z3_INVALID_ARG);
+ return "";
+ }
}
Z3_CATCH_RETURN("");
}
diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index b2927e2c3..367e62666 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -1532,7 +1532,9 @@ namespace Microsoft.Z3
{
case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj);
case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj);
- case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
+ case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
+ case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPNum(ctx, obj);
+ case Z3_sort_kind.Z3_FLOATING_POINT_ROUNDING_MODE_SORT: return new FPRMNum(ctx, obj);
}
}
@@ -1543,7 +1545,9 @@ namespace Microsoft.Z3
case Z3_sort_kind.Z3_REAL_SORT: return new RealExpr(ctx, obj);
case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj);
case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj);
- case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);
+ case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);
+ case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPExpr(ctx, obj);
+ case Z3_sort_kind.Z3_FLOATING_POINT_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj);
}
return new Expr(ctx, obj);
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 6d59cf650..a761c89eb 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -194,6 +194,8 @@ typedef enum
Z3_DATATYPE_SORT,
Z3_RELATION_SORT,
Z3_FINITE_DOMAIN_SORT,
+ Z3_FLOATING_POINT_SORT,
+ Z3_FLOATING_POINT_ROUNDING_MODE_SORT,
Z3_UNKNOWN_SORT = 1000
} Z3_sort_kind;
diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h
index deda7e045..0b8349793 100644
--- a/src/ast/float_decl_plugin.h
+++ b/src/ast/float_decl_plugin.h
@@ -201,9 +201,11 @@ public:
app * mk_minus_inf(sort * s) { return mk_minus_inf(get_ebits(s), get_sbits(s)); }
app * mk_value(mpf const & v) { return m_plugin->mk_value(v); }
- bool is_value(expr * n) { return m_plugin->is_value(n); }
- bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); }
- bool is_rm(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm(n, v); }
+ bool is_value(expr * n) const { return m_plugin->is_value(n); }
+ bool is_numeral(expr * n) const { return is_value(n); }
+ bool is_value(expr * n, mpf & v) const { return m_plugin->is_value(n, v); }
+ bool is_numeral(expr * n, mpf & v) const { return is_value(n, v); }
+ bool is_rm(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm(n, v); }
app * mk_pzero(unsigned ebits, unsigned sbits);
app * mk_nzero(unsigned ebits, unsigned sbits);