Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng

src/api/api_ast.cpp

@@ -648,6 +648,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 == FLOATING_POINT_SORT) {
+            return Z3_FLOATING_POINT_SORT;
+        }
+        else if (fid == mk_c(c)->get_fpa_fid() && k == ROUNDING_MODE_SORT) {
+            return Z3_ROUNDING_MODE_SORT;
+        }
         else {
             return Z3_UNKNOWN_SORT;
         }
@@ -1113,6 +1119,62 @@ extern "C" {
                 return Z3_OP_UNINTERPRETED;
             }
         }
+        
+        if (mk_c(c)->get_fpa_fid() == _d->get_family_id()) {
+            switch (_d->get_decl_kind()) {
+            case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN;
+            case OP_FPA_RM_NEAREST_TIES_TO_AWAY: return Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY;
+            case OP_FPA_RM_TOWARD_POSITIVE: return Z3_OP_FPA_RM_TOWARD_POSITIVE;
+            case OP_FPA_RM_TOWARD_NEGATIVE: return Z3_OP_FPA_RM_TOWARD_NEGATIVE;
+            case OP_FPA_RM_TOWARD_ZERO: return Z3_OP_FPA_RM_TOWARD_ZERO;
+            case OP_FPA_NUM: return Z3_OP_FPA_NUM;
+            case OP_FPA_PLUS_INF: return Z3_OP_FPA_PLUS_INF;
+            case OP_FPA_MINUS_INF: return Z3_OP_FPA_MINUS_INF;
+            case OP_FPA_NAN: return Z3_OP_FPA_NAN;
+            case OP_FPA_MINUS_ZERO: return Z3_OP_FPA_MINUS_ZERO;
+            case OP_FPA_PLUS_ZERO: return Z3_OP_FPA_PLUS_ZERO;
+            case OP_FPA_ADD: return Z3_OP_FPA_ADD;
+            case OP_FPA_SUB: return Z3_OP_FPA_SUB;
+            case OP_FPA_NEG: return Z3_OP_FPA_NEG;
+            case OP_FPA_MUL: return Z3_OP_FPA_MUL;
+            case OP_FPA_DIV: return Z3_OP_FPA_DIV;
+            case OP_FPA_REM: return Z3_OP_FPA_REM;
+            case OP_FPA_ABS: return Z3_OP_FPA_ABS;
+            case OP_FPA_MIN: return Z3_OP_FPA_MIN;
+            case OP_FPA_MAX: return Z3_OP_FPA_MAX;
+            case OP_FPA_FMA: return Z3_OP_FPA_FMA;
+            case OP_FPA_SQRT: return Z3_OP_FPA_SQRT;
+            case OP_FPA_EQ: return Z3_OP_FPA_EQ;
+            case OP_FPA_ROUND_TO_INTEGRAL: return Z3_OP_FPA_ROUND_TO_INTEGRAL;
+            case OP_FPA_LT: return Z3_OP_FPA_LT;
+            case OP_FPA_GT: return Z3_OP_FPA_GT;
+            case OP_FPA_LE: return Z3_OP_FPA_LE;
+            case OP_FPA_GE: return Z3_OP_FPA_GE;
+            case OP_FPA_IS_NAN: return Z3_OP_FPA_IS_NAN;
+            case OP_FPA_IS_INF: return Z3_OP_FPA_IS_INF;
+            case OP_FPA_IS_ZERO: return Z3_OP_FPA_IS_ZERO;
+            case OP_FPA_IS_NORMAL: return Z3_OP_FPA_IS_NORMAL;
+            case OP_FPA_IS_SUBNORMAL: return Z3_OP_FPA_IS_SUBNORMAL;
+            case OP_FPA_IS_NEGATIVE: return Z3_OP_FPA_IS_NEGATIVE;
+            case OP_FPA_IS_POSITIVE: return Z3_OP_FPA_IS_POSITIVE;
+            case OP_FPA_FP: return Z3_OP_FPA_FP;
+            case OP_FPA_TO_FP: return Z3_OP_FPA_TO_FP;
+            case OP_FPA_TO_FP_UNSIGNED: return Z3_OP_FPA_TO_FP_UNSIGNED;
+            case OP_FPA_TO_UBV: return Z3_OP_FPA_TO_UBV;
+            case OP_FPA_TO_SBV: return Z3_OP_FPA_TO_SBV;
+            case OP_FPA_TO_REAL: return Z3_OP_FPA_TO_REAL;
+            case OP_FPA_TO_IEEE_BV: return Z3_OP_FPA_TO_IEEE_BV;
+            case OP_FPA_INTERNAL_BVWRAP:
+            case OP_FPA_INTERNAL_BVUNWRAP:
+            case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED:
+            case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED:
+            case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED:
+                return Z3_OP_UNINTERPRETED;
+            default:
+                UNREACHABLE();
+                return Z3_OP_UNINTERPRETED;
+            }
+        }
 
         if (mk_c(c)->m().get_label_family_id() == _d->get_family_id()) {
             switch(_d->get_decl_kind()) {

src/api/api_context.cpp

@@ -88,6 +88,7 @@ namespace api {
         m_arith_util(m()),
         m_bv_util(m()),
         m_datalog_util(m()),
+        m_fpa_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("fpa");
         m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
 
         if (!m_user_ref_count) {

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"fpa_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;
+        fpa_util                   m_fpa_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; }
+        fpa_util & fpautil() { return m_fpa_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; }

src/api/api_fpa.cpp

@@ -0,0 +1,794 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    api_fpa.cpp
+
+Abstract:
+
+    Additional APIs for floating-point arithmetic (FP).
+
+Author:
+
+    Christoph M. Wintersteiger (cwinter) 2013-06-05
+
+Notes:
+    
+--*/
+#include<iostream>
+#include"z3.h"
+#include"api_log_macros.h"
+#include"api_context.h"
+#include"fpa_decl_plugin.h"
+
+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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    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(); 
+        api::context * ctx = mk_c(c);
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_even());
+        RETURN_Z3(r);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    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(); 
+        api::context * ctx = mk_c(c);
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_nearest_ties_to_away());
+        RETURN_Z3(r);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    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(); 
+        api::context * ctx = mk_c(c);
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_positive());
+        RETURN_Z3(r);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    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(); 
+        api::context * ctx = mk_c(c);
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_negative());
+        RETURN_Z3(r);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    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(); 
+        api::context * ctx = mk_c(c);
+        Z3_ast r = of_ast(ctx->fpautil().mk_round_toward_zero());
+        RETURN_Z3(r);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+
+    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(); 
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_sort Z3_API Z3_mk_fpa_sort_half(Z3_context c) {
+        return Z3_mk_fpa_sort(c, 5, 11);
+    }
+
+    Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c) {
+        return Z3_mk_fpa_sort(c, 5, 11);
+    }
+
+    Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c) {
+        return Z3_mk_fpa_sort(c, 8, 24);
+    }
+
+    Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c) {
+        return Z3_mk_fpa_sort(c, 8, 24);
+    }
+
+    Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c) {
+        return Z3_mk_fpa_sort(c, 11, 53);
+    }
+
+    Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c) {
+        return Z3_mk_fpa_sort(c, 11, 53);
+    }
+
+    Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(Z3_context c) {
+        return Z3_mk_fpa_sort(c, 15, 113);
+    }
+
+    Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c) {
+        return Z3_mk_fpa_sort(c, 15, 113);
+    }
+
+    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();         
+        api::context * ctx = mk_c(c);
+        Z3_ast r = of_ast(ctx->fpautil().mk_nan(to_sort(s)));
+        RETURN_Z3(r);
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_zero(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_nzero(to_sort(s)) : 
+                                          ctx->fpautil().mk_pzero(to_sort(s)));
+        RETURN_Z3(r);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_numeral_float(Z3_context c, float v, Z3_sort ty) {
+        Z3_TRY;
+        LOG_Z3_mk_fpa_numeral_float(c, v, ty);
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty) {
+        Z3_TRY;
+        LOG_Z3_mk_fpa_numeral_double(c, v, ty);
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_numeral_int(Z3_context c, signed v, Z3_sort ty) {
+        Z3_TRY;
+        LOG_Z3_mk_fpa_numeral_int(c, v, ty);
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_numeral_uint_int(Z3_context c, Z3_bool sgn, unsigned sig, signed exp, Z3_sort ty) {
+        Z3_TRY;
+        LOG_Z3_mk_fpa_numeral_uint64_int64(c, sgn, sig, exp, ty);
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_numeral_uint64_int64(Z3_context c, Z3_bool sgn, __uint64 sig, __int64 exp, Z3_sort ty) {
+        Z3_TRY;
+        LOG_Z3_mk_fpa_numeral_uint64_int64(c, sgn, sig, exp, ty);
+        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);
+        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);
+        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);
+        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);
+        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);
+        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);
+        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);
+        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);
+        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);
+        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);
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2) {
+        Z3_TRY;
+        LOG_Z3_mk_fpa_max(c, t1, t2);
+        RESET_ERROR_CODE();
+        api::context * ctx = mk_c(c);
+        Z3_ast r = of_ast(ctx->fpautil().mk_max(to_expr(t1), to_expr(t2)));
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2) {
+        Z3_TRY;
+        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);
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2) {
+        Z3_TRY;
+        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);
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_is_negative(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_is_positive(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+
+    Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_mk_fpa_to_fp_bv(c, bv, s);
+        RESET_ERROR_CODE();
+        api::context * ctx = mk_c(c);
+        fpa_util & fu = ctx->fpautil();
+        if (!ctx->bvutil().is_bv(to_expr(bv)) ||
+            !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(bv)));
+        RETURN_Z3(r);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_mk_fpa_to_fp_float(c, rm, t, s);
+        RESET_ERROR_CODE();
+        api::context * ctx = mk_c(c);
+        fpa_util & fu = ctx->fpautil();
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_mk_fpa_to_fp_real(c, rm, t, s);
+        RESET_ERROR_CODE();
+        api::context * ctx = mk_c(c);
+        fpa_util & fu = ctx->fpautil();
+        if (!fu.is_rm(to_expr(rm)) ||
+            !ctx->autil().is_real(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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_mk_fpa_to_fp_signed(c, rm, t, s);
+        RESET_ERROR_CODE();
+        api::context * ctx = mk_c(c);
+        fpa_util & fu = ctx->fpautil();
+        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(to_sort(s), to_expr(rm), to_expr(t)));
+        RETURN_Z3(r);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_mk_fpa_to_fp_unsigned(c, rm, t, s);
+        RESET_ERROR_CODE();
+        api::context * ctx = mk_c(c);
+        fpa_util & fu = ctx->fpautil();
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_to_real(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        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);
+        Z3_CATCH_RETURN(0);
+    }
+
+    unsigned Z3_API Z3_fpa_get_ebits(Z3_context c, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_fpa_get_ebits(c, s);
+        RESET_ERROR_CODE();
+        CHECK_NON_NULL(s, 0);
+        return mk_c(c)->fpautil().get_ebits(to_sort(s));
+        Z3_CATCH_RETURN(0);
+    }
+
+    unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_fpa_get_ebits(c, s);
+        RESET_ERROR_CODE();
+        CHECK_NON_NULL(s, 0);
+        return mk_c(c)->fpautil().get_sbits(to_sort(s));
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int * sgn) {
+        Z3_TRY;
+        LOG_Z3_fpa_get_numeral_sign(c, t, sgn);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        mpf_manager & mpfm = mk_c(c)->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);
+        if (!r || mpfm.is_nan(val)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        *sgn = (mpfm.is_nan(val)) ? 0 : mpfm.sgn(val);
+        return r;
+        Z3_CATCH_RETURN(0);
+    }
+    
+    Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t) {
+        Z3_TRY;
+        LOG_Z3_fpa_get_numeral_significand_string(c, t);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
+        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)) {            
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return "";
+        }
+        else if (!mpfm.is_regular(val)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG)
+            return "";
+        }
+        unsigned sbits = val.get().get_sbits();
+        scoped_mpq q(mpqm);
+        scoped_mpz sn(mpzm);
+        mpfm.sig_normalized(val, sn);
+        mpqm.set(q, sn);
+        mpqm.div(q, mpfm.m_powers2(sbits - 1), q);
+        std::stringstream ss;
+        mpqm.display_decimal(ss, q, sbits);
+        return mk_c(c)->mk_external_string(ss.str());
+        Z3_CATCH_RETURN("");
+
+    }
+
+    Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t) {
+        Z3_TRY;
+        LOG_Z3_fpa_get_numeral_exponent_string(c, t);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        mpf_manager & mpfm = mk_c(c)->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);
+        if (!r) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return "";
+        }
+        else if (!mpfm.is_normal(val) && !mpfm.is_denormal(val)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG)
+                return "";
+        }
+        mpf_exp_t exp = mpfm.exp_normalized(val);        
+        std::stringstream ss;
+        ss << exp;
+        return mk_c(c)->mk_external_string(ss.str());
+        Z3_CATCH_RETURN("");
+    }
+
+    Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(__in Z3_context c, __in Z3_ast t, __out __int64 * n) {
+        Z3_TRY;
+        LOG_Z3_fpa_get_numeral_exponent_string(c, t);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        mpf_manager & mpfm = mk_c(c)->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);        
+        if (!r) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        *n = mpfm.exp(val);
+        return 1;
+        Z3_CATCH_RETURN(0);
+    }
+
+    Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        LOG_Z3_mk_fpa_to_ieee_bv(c, t);
+        RESET_ERROR_CODE();
+        api::context * ctx = mk_c(c);
+        Z3_ast r = of_ast(ctx->fpautil().mk_float_to_ieee_bv(to_expr(t)));
+        RETURN_Z3(r);
+        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_TRY;
+        LOG_Z3_mk_fpa_to_fp_real_int(c, rm, sig, exp, s);
+        RESET_ERROR_CODE();
+        api::context * ctx = mk_c(c);
+        fpa_util & fu = ctx->fpautil();
+        if (!fu.is_rm(to_expr(rm)) ||
+            !ctx->autil().is_real(to_expr(sig)) ||
+            !ctx->autil().is_int(to_expr(exp)) ||
+            !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(sig), to_expr(exp)));
+        RETURN_Z3(r);
+        Z3_CATCH_RETURN(0);
+    }
+
+};

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"fpa_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;
@@ -48,7 +50,7 @@ extern "C" {
     Z3_ast Z3_API Z3_mk_numeral(Z3_context c, const char* n, Z3_sort ty) {
         Z3_TRY;
         LOG_Z3_mk_numeral(c, n, ty);
-        RESET_ERROR_CODE();          
+        RESET_ERROR_CODE();
         if (!check_numeral_sort(c, ty)) {
             RETURN_Z3(0);
         }
@@ -56,40 +58,42 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
+        sort * _ty = to_sort(ty);
+        bool is_float = mk_c(c)->fpautil().is_float(_ty);
         std::string fixed_num;
         char const* m = n;
         while (*m) {
             if (!(('0' <= *m && *m <= '9') ||
-                  ('/' == *m) || ('-' == *m) ||
-                  (' ' == *m) || ('\n' == *m) ||
-                  ('.' == *m) || ('e' == *m) ||
-                  ('E' == *m))) {
+                ('/' == *m) || ('-' == *m) ||
+                (' ' == *m) || ('\n' == *m) ||
+                ('.' == *m) || ('e' == *m) ||
+                ('E' == *m) ||
+                ('p' == *m && is_float) ||
+                ('P' == *m && is_float))) {
                 SET_ERROR_CODE(Z3_PARSER_ERROR);
                 return 0;
             }
             ++m;
         }
-        ast * a = mk_c(c)->mk_numeral_core(rational(n), to_sort(ty));
+        ast * a = 0;
+        if (_ty->get_family_id() == mk_c(c)->get_fpa_fid()) {
+            // avoid expanding floats into huge rationals.
+            fpa_util & fu = mk_c(c)->fpautil();
+            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);
     }
-    
+
     Z3_ast Z3_API Z3_mk_int(Z3_context c, int value, Z3_sort ty) {
         Z3_TRY;
         LOG_Z3_mk_int(c, value, ty);
-        RESET_ERROR_CODE();  
-        if (!check_numeral_sort(c, ty)) {
-            RETURN_Z3(0);
-        }
-        ast * a = mk_c(c)->mk_numeral_core(rational(value), to_sort(ty));
-        RETURN_Z3(of_ast(a)); 
-        Z3_CATCH_RETURN(0);
-    }
-    
-    Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned value, Z3_sort ty) {
-        Z3_TRY;
-        LOG_Z3_mk_unsigned_int(c, value, ty);
-        RESET_ERROR_CODE();   
+        RESET_ERROR_CODE();
         if (!check_numeral_sort(c, ty)) {
             RETURN_Z3(0);
         }
@@ -97,11 +101,23 @@ extern "C" {
         RETURN_Z3(of_ast(a));
         Z3_CATCH_RETURN(0);
     }
-    
+
+    Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned value, Z3_sort ty) {
+        Z3_TRY;
+        LOG_Z3_mk_unsigned_int(c, value, ty);
+        RESET_ERROR_CODE();
+        if (!check_numeral_sort(c, ty)) {
+            RETURN_Z3(0);
+        }
+        ast * a = mk_c(c)->mk_numeral_core(rational(value), to_sort(ty));
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_ast Z3_API Z3_mk_int64(Z3_context c, long long value, Z3_sort ty) {
         Z3_TRY;
         LOG_Z3_mk_int64(c, value, ty);
-        RESET_ERROR_CODE();  
+        RESET_ERROR_CODE();
         if (!check_numeral_sort(c, ty)) {
             RETURN_Z3(0);
         }
@@ -110,11 +126,11 @@ extern "C" {
         RETURN_Z3(of_ast(a));
         Z3_CATCH_RETURN(0);
     }
-    
+
     Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, unsigned long long value, Z3_sort ty) {
         Z3_TRY;
         LOG_Z3_mk_unsigned_int64(c, value, ty);
-        RESET_ERROR_CODE(); 
+        RESET_ERROR_CODE();
         if (!check_numeral_sort(c, ty)) {
             RETURN_Z3(0);
         }
@@ -129,9 +145,11 @@ extern "C" {
         LOG_Z3_is_numeral_ast(c, a);
         RESET_ERROR_CODE();
         expr* e = to_expr(a);
-        return 
+        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)->fpautil().is_numeral(e) ||
+            mk_c(c)->fpautil().is_rm_numeral(e);
         Z3_CATCH_RETURN(Z3_FALSE);
     }
 
@@ -172,8 +190,37 @@ 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.
+            fpa_util & fu = mk_c(c)->fpautil();
+            scoped_mpf tmp(fu.fm());
+            mpf_rounding_mode rm;
+            if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm)) {
+                switch (rm) {
+                case OP_FPA_RM_NEAREST_TIES_TO_EVEN: 
+                    return mk_c(c)->mk_external_string("roundNearestTiesToEven"); 
+                    break;
+                case OP_FPA_RM_NEAREST_TIES_TO_AWAY:
+                    return mk_c(c)->mk_external_string("roundNearestTiesToAway"); 
+                    break;
+                case OP_FPA_RM_TOWARD_POSITIVE:
+                    return mk_c(c)->mk_external_string("roundTowardPositive");
+                    break;
+                case OP_FPA_RM_TOWARD_NEGATIVE:
+                    return mk_c(c)->mk_external_string("roundTowardNegative");
+                    break;
+                case OP_FPA_RM_TOWARD_ZERO:
+                default:
+                    return mk_c(c)->mk_external_string("roundTowardZero");
+                    break;
+                }                
+            }
+            else if (mk_c(c)->fpautil().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("");
     }

src/api/dotnet/AST.cs

@@ -227,10 +227,8 @@ namespace Microsoft.Z3
         internal override void IncRef(IntPtr o)
         {            
             // Console.WriteLine("AST IncRef()");
-            if (Context == null)
-                throw new Z3Exception("inc() called on null context");
-            if (o == IntPtr.Zero)
-                throw new Z3Exception("inc() called on null AST");
+            if (Context == null || o == IntPtr.Zero)
+                return;
             Context.AST_DRQ.IncAndClear(Context, o);
             base.IncRef(o);
         }
@@ -238,10 +236,8 @@ namespace Microsoft.Z3
         internal override void DecRef(IntPtr o)
         {
             // Console.WriteLine("AST DecRef()");
-            if (Context == null)
-                throw new Z3Exception("dec() called on null context");
-            if (o == IntPtr.Zero)
-                throw new Z3Exception("dec() called on null AST");
+            if (Context == null || o == IntPtr.Zero)
+                return;
             Context.AST_DRQ.Add(o);
             base.DecRef(o);
         }

src/api/dotnet/ArithExpr.cs

@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for ArithExpr </summary>
-        internal protected ArithExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal ArithExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {

src/api/dotnet/ArrayExpr.cs

@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for ArrayExpr </summary>
-        internal protected ArrayExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal ArrayExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {

src/api/dotnet/BitVecExpr.cs

@@ -41,7 +41,6 @@ namespace Microsoft.Z3
 
         #region Internal
         /// <summary> Constructor for BitVecExpr </summary>
-        internal protected BitVecExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
         internal BitVecExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
         #endregion
     }

src/api/dotnet/BoolExpr.cs

@@ -32,8 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for BoolExpr </summary>
-        internal protected BoolExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
-        /// <summary> Constructor for BoolExpr </summary>
         internal BoolExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
         #endregion
     }

src/api/dotnet/Context.cs

@@ -3438,6 +3438,805 @@ namespace Microsoft.Z3
         }
         #endregion
 
+        #region Floating-Point Arithmetic
+
+        #region Rounding Modes
+        #region RoundingMode Sort
+        /// <summary>
+        /// Create the floating-point RoundingMode sort.
+        /// </summary>    
+        public FPRMSort MkFPRoundingModeSort()
+        {
+            Contract.Ensures(Contract.Result<FPRMSort>() != null);
+            return new FPRMSort(this);
+        }
+        #endregion
+        
+        #region Numerals
+        /// <summary>
+        /// Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
+        /// </summary>
+        public FPRMExpr MkFPRoundNearestTiesToEven()
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx));
+        }
+
+        /// <summary>
+        /// Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
+        /// </summary>
+        public FPRMNum MkFPRNE()
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPRMNum(this, Native.Z3_mk_fpa_rne(nCtx));
+        }
+
+        /// <summary>
+        /// Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
+        /// </summary>
+        public FPRMNum MkFPRoundNearestTiesToAway()
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx));
+        }
+
+        /// <summary>
+        /// Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
+        /// </summary>
+        public FPRMNum MkFPRNA()
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPRMNum(this, Native.Z3_mk_fpa_rna(nCtx));
+        }
+
+        /// <summary>
+        /// Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
+        /// </summary>
+        public FPRMNum MkFPRoundTowardPositive()
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx));
+        }
+
+        /// <summary>
+        /// Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
+        /// </summary>
+        public FPRMNum MkFPRTP()
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPRMNum(this, Native.Z3_mk_fpa_rtp(nCtx));
+        }
+
+        /// <summary>
+        /// Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
+        /// </summary>
+        public FPRMNum MkFPRoundTowardNegative()
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx));
+        }
+
+        /// <summary>
+        /// Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
+        /// </summary>
+        public FPRMNum MkFPRTN()
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPRMNum(this, Native.Z3_mk_fpa_rtn(nCtx));
+        }
+
+        /// <summary>
+        /// Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
+        /// </summary>
+        public FPRMNum MkFPRoundTowardZero()
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx));
+        }
+
+        /// <summary>
+        /// Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
+        /// </summary>
+        public FPRMNum MkFPRTZ()
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx));
+        }        
+        #endregion
+        #endregion
+
+        #region FloatingPoint Sorts
+        /// <summary>
+        /// Create a FloatingPoint sort.
+        /// </summary>
+        /// <param name="ebits">exponent bits in the FloatingPoint sort.</param>
+        /// <param name="sbits">significand bits in the FloatingPoint sort.</param>
+        public FPSort MkFPSort(uint ebits, uint sbits)
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, ebits, sbits);
+        }
+
+        /// <summary>
+        /// Create the half-precision (16-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSortHalf()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_half(nCtx));
+        }
+
+        /// <summary>
+        /// Create the half-precision (16-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSort16()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_16(nCtx));
+        }
+
+        /// <summary>
+        /// Create the single-precision (32-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSortSingle()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_single(nCtx));
+        }
+
+        /// <summary>
+        /// Create the single-precision (32-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSort32()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_32(nCtx));
+        }
+
+        /// <summary>
+        /// Create the double-precision (64-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSortDouble()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_double(nCtx));
+        }
+
+        /// <summary>
+        /// Create the double-precision (64-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSort64()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_64(nCtx));
+        }
+
+        /// <summary>
+        /// Create the quadruple-precision (128-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSortQuadruple()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_quadruple(nCtx));
+        }
+
+        /// <summary>
+        /// Create the quadruple-precision (128-bit) FloatingPoint sort.
+        /// </summary>
+        public FPSort MkFPSort128()
+        {
+            Contract.Ensures(Contract.Result<FPSort>() != null);
+            return new FPSort(this, Native.Z3_mk_fpa_sort_128(nCtx));
+        }
+        #endregion
+        
+        #region Numerals
+        /// <summary>
+        /// Create a NaN of sort s.
+        /// </summary>        
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFPNaN(FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a floating-point infinity of sort s.
+        /// </summary>        
+        /// <param name="s">FloatingPoint sort.</param>   
+        /// <param name="negative">indicates whether the result should be negative.</param>
+        public FPNum MkFPInf(FPSort s, bool negative)
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative ? 1 : 0));
+        }
+
+        /// <summary>
+        /// Create a floating-point zero of sort s.
+        /// </summary>        
+        /// <param name="s">FloatingPoint sort.</param>   
+        /// <param name="negative">indicates whether the result should be negative.</param>
+        public FPNum MkFPZero(FPSort s, bool negative)
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, negative ? 1 : 0));
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a float.
+        /// </summary>        
+        /// <param name="v">numeral value.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFPNumeral(float v, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a float.
+        /// </summary>        
+        /// <param name="v">numeral value.</param>
+        /// <param name="s">FloatingPoint sort.</param>
+        public FPNum MkFPNumeral(double v, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from an int.
+        /// </summary>        
+        /// <param name="v">numeral value.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFPNumeral(int v, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a sign bit and two integers.
+        /// </summary>        
+        /// <param name="sgn">the sign.</param>
+        /// <param name="sig">the significand.</param>
+        /// <param name="exp">the exponent.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPNum(this, Native.Z3_mk_fpa_numeral_uint_int(nCtx, sgn ? 1 : 0, sig, exp, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
+        /// </summary>        
+        /// <param name="sgn">the sign.</param>
+        /// <param name="sig">the significand.</param>
+        /// <param name="exp">the exponent.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFPNumeral(bool sgn, UInt64 sig, Int64 exp, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return new FPNum(this, Native.Z3_mk_fpa_numeral_uint64_int64(nCtx, sgn ? 1 : 0, sig, exp, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a float.
+        /// </summary>        
+        /// <param name="v">numeral value.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFP(float v, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return MkFPNumeral(v, s);
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a float.
+        /// </summary>        
+        /// <param name="v">numeral value.</param>
+        /// <param name="s">FloatingPoint sort.</param>
+        public FPNum MkFP(double v, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return MkFPNumeral(v, s);
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from an int.
+        /// </summary>        
+        /// <param name="v">numeral value.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFP(int v, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return MkFPNumeral(v, s);
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a sign bit and two integers.
+        /// </summary>        
+        /// <param name="sgn">the sign.</param>        
+        /// <param name="exp">the exponent.</param>
+        /// <param name="sig">the significand.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFP(bool sgn, int exp, uint sig, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return MkFPNumeral(sgn, sig, exp, s);
+        }
+
+        /// <summary>
+        /// Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
+        /// </summary>        
+        /// <param name="sgn">the sign.</param>        
+        /// <param name="exp">the exponent.</param>
+        /// <param name="sig">the significand.</param>
+        /// <param name="s">FloatingPoint sort.</param>        
+        public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPRMExpr>() != null);
+            return MkFPNumeral(sgn, sig, exp, s);
+        }
+
+        #endregion
+
+        #region Operators
+        /// <summary>
+        /// Floating-point absolute value
+        /// </summary>
+        /// <param name="t">floating-point term</param>
+        public FPExpr MkFPAbs(FPExpr t) 
+        {
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject));
+        }
+   
+        /// <summary>
+        /// Floating-point negation
+        /// </summary>
+        /// <param name="t">floating-point term</param>
+        public FPExpr MkFPNeg(FPExpr t) 
+        {
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject));
+        }
+
+        /// <summary>
+        /// Floating-point addition
+        /// </summary>
+        /// <param name="rm">rounding mode term</param>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2) 
+        {
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_add(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
+        }
+
+        /// <summary>
+        /// Floating-point subtraction
+        /// </summary>
+        /// <param name="rm">rounding mode term</param>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2) 
+        {
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
+        }
+    
+        /// <summary>
+        /// Floating-point multiplication
+        /// </summary>
+        /// <param name="rm">rounding mode term</param>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2) 
+        {
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_mul(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
+        }
+   
+        /// <summary>
+        /// Floating-point division
+        /// </summary>
+        /// <param name="rm">rounding mode term</param>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2) 
+        {
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_div(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject));
+        }
+   
+        /// <summary>
+        /// Floating-point fused multiply-add
+        /// </summary>
+        /// <remarks>
+        /// The result is round((t1 * t2) + t3)
+        /// </remarks>
+        /// <param name="rm">rounding mode term</param>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        /// <param name="t3">floating-point term</param>
+        public FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3) 
+        {
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_fma(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject));
+        }
+   
+        /// <summary>
+        /// Floating-point square root
+        /// </summary>        
+        /// <param name="rm">rounding mode term</param>        
+        /// <param name="t">floating-point term</param>        
+        public FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t) 
+        {
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_sqrt(this.nCtx, rm.NativeObject, t.NativeObject));
+        }
+   
+        /// <summary>
+        /// Floating-point remainder
+        /// </summary>        
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public FPExpr MkFPRem(FPExpr t1, FPExpr t2) 
+        {
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject));
+        }
+
+        /// <summary>
+        /// Floating-point roundToIntegral. Rounds a floating-point number to 
+        /// the closest integer, again represented as a floating-point number.
+        /// </summary>        
+        /// <param name="rm">term of RoundingMode sort</param>
+        /// <param name="t">floating-point term</param>
+        public FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t)
+        {            
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject));
+        }
+
+        /// <summary>
+        /// Minimum of floating-point numbers.
+        /// </summary>        
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public FPExpr MkFPMin(FPExpr t1, FPExpr t2)
+        {
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject));
+        }
+
+        /// <summary>
+        /// Maximum of floating-point numbers.
+        /// </summary>        
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public FPExpr MkFPMax(FPExpr t1, FPExpr t2)
+        {
+            Contract.Ensures(Contract.Result<FPNum>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject));
+        }   
+        
+        /// <summary>
+        /// Floating-point less than or equal.
+        /// </summary>        
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public BoolExpr MkFPLEq(FPExpr t1, FPExpr t2) 
+        {            
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject));
+        }
+
+        /// <summary>
+        /// Floating-point less than.
+        /// </summary>        
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public BoolExpr MkFPLt(FPExpr t1, FPExpr t2) 
+        {            
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject));
+        }
+    
+        /// <summary>
+        /// Floating-point greater than or equal.
+        /// </summary>        
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public BoolExpr MkFPGEq(FPExpr t1, FPExpr t2) 
+        {            
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject));
+        }
+
+        /// <summary>
+        /// Floating-point greater than.
+        /// </summary>        
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public BoolExpr MkFPGt(FPExpr t1, FPExpr t2) 
+        {            
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_gt(this.nCtx, t1.NativeObject, t2.NativeObject));
+        }
+
+        /// <summary>
+        /// Floating-point equality.
+        /// </summary>
+        /// <remarks>
+        /// Note that this is IEEE 754 equality (as opposed to standard =).
+        /// </remarks>
+        /// <param name="t1">floating-point term</param>
+        /// <param name="t2">floating-point term</param>
+        public BoolExpr MkFPEq(FPExpr t1, FPExpr t2)
+        {
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject));
+        }
+
+        /// <summary>
+        /// Predicate indicating whether t is a normal floating-point number.
+        /// </summary>        
+        /// <param name="t">floating-point term</param>        
+        public BoolExpr MkFPIsNormal(FPExpr t) 
+        {            
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject));
+        }
+   
+        /// <summary>
+        /// Predicate indicating whether t is a subnormal floating-point number.
+        /// </summary>        
+        /// <param name="t">floating-point term</param>        
+        public BoolExpr MkFPIsSubnormal(FPExpr t) 
+        {            
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject));
+        }
+
+        /// <summary>
+        /// Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0.
+        /// </summary>        
+        /// <param name="t">floating-point term</param>        
+        public BoolExpr MkFPIsZero(FPExpr t)
+        {
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject));
+        }
+
+        /// <summary>
+        /// Predicate indicating whether t is a floating-point number representing +oo or -oo.
+        /// </summary>        
+        /// <param name="t">floating-point term</param>        
+        public BoolExpr MkFPIsInfinite(FPExpr t)
+        {
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject));
+        }
+
+        /// <summary>
+        /// Predicate indicating whether t is a NaN.
+        /// </summary>        
+        /// <param name="t">floating-point term</param>        
+        public BoolExpr MkFPIsNaN(FPExpr t) 
+        {            
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject));
+        }
+
+        /// <summary>
+        /// Predicate indicating whether t is a negative floating-point number.
+        /// </summary>        
+        /// <param name="t">floating-point term</param>        
+        public BoolExpr MkFPIsNegative(FPExpr t)
+        {
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_is_negative(this.nCtx, t.NativeObject));
+        }
+
+        /// <summary>
+        /// Predicate indicating whether t is a positive floating-point number.
+        /// </summary>        
+        /// <param name="t">floating-point term</param>        
+        public BoolExpr MkFPIsPositive(FPExpr t)
+        {
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject));
+        }        
+        #endregion
+
+        #region Conversions to FloatingPoint terms
+        /// <summary>
+        /// Create an expression of FloatingPoint sort from three bit-vector expressions.
+        /// </summary>
+        /// <remarks>
+        /// This is the operator named `fp' in the SMT FP theory definition. 
+        /// Note that sgn 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 
+        /// of the resulting expression is automatically determined from the bit-vector sizes
+        /// of the arguments.
+        /// </remarks>
+        /// <param name="sgn">bit-vector term (of size 1) representing the sign.</param>
+        /// <param name="sig">bit-vector term representing the significand.</param>
+        /// <param name="exp">bit-vector term representing the exponent.</param>
+        public FPExpr MkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp)
+        {
+            Contract.Ensures(Contract.Result<FPExpr>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_fp(this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObject));
+        }
+
+        /// <summary>
+        /// Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of a bit-vector term bv to a 
+        /// floating-point term of sort s. The bit-vector size of bv (m) must be equal 
+        /// to ebits+sbits of s. The format of the bit-vector is as defined by the 
+        /// IEEE 754-2008 interchange format.
+        /// </remarks>
+        /// <param name="bv">bit-vector value (of size m).</param>
+        /// <param name="s">FloatingPoint sort (ebits+sbits == m)</param>
+        public FPExpr MkFPToFP(BitVecExpr bv, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPExpr>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_to_fp_bv(this.nCtx, bv.NativeObject, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of a floating-point term t to a
+        /// floating-point term of sort s. If necessary, the result will be rounded according
+        /// to rounding mode rm.
+        /// </remarks>
+        /// <param name="rm">RoundingMode term.</param>
+        /// <param name="t">FloatingPoint term.</param>
+        /// <param name="s">FloatingPoint sort.</param>
+        public FPExpr MkFPToFP(FPRMExpr rm, FPExpr t, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPExpr>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Conversion of a term of real sort into a term of FloatingPoint sort.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of term t of real sort into a
+        /// floating-point term of sort s. If necessary, the result will be rounded according
+        /// to rounding mode rm.
+        /// </remarks>
+        /// <param name="rm">RoundingMode term.</param>
+        /// <param name="t">term of Real sort.</param>
+        /// <param name="s">FloatingPoint sort.</param>
+        public FPExpr MkFPToFP(FPRMExpr rm, RealExpr t, FPSort s)
+        {
+            Contract.Ensures(Contract.Result<FPExpr>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_to_fp_real(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of the bit-vector term t into a
+        /// floating-point term of sort s. The bit-vector t is taken to be in signed 
+        /// 2's complement format (when signed==true, otherwise unsigned). If necessary, the 
+        /// result will be rounded according to rounding mode rm.
+        /// </remarks>
+        /// <param name="rm">RoundingMode term.</param>
+        /// <param name="t">term of bit-vector sort.</param>
+        /// <param name="s">FloatingPoint sort.</param>
+        /// <param name="signed">flag indicating whether t is interpreted as signed or unsigned bit-vector.</param>
+        public FPExpr MkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, bool signed)
+        {
+            Contract.Ensures(Contract.Result<FPExpr>() != null);
+            if (signed)
+                return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
+            else
+                return new FPExpr(this, Native.Z3_mk_fpa_to_fp_unsigned(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject));
+        }
+
+        /// <summary>
+        /// Conversion of a floating-point number to another FloatingPoint sort s.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of a floating-point term t to a different
+        /// FloatingPoint sort s. If necessary, rounding according to rm is applied. 
+        /// </remarks>
+        /// <param name="s">FloatingPoint sort</param>
+        /// <param name="rm">floating-point rounding mode term</param>
+        /// <param name="t">floating-point term</param>
+        public FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t)
+        {
+            Contract.Ensures(Contract.Result<FPExpr>() != null);
+            return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
+        }
+        #endregion
+
+        #region Conversions from FloatingPoint terms
+        /// <summary>
+        /// Conversion of a floating-point term into a bit-vector.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of the floating-poiunt term t into a
+        /// bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, 
+        /// the result will be rounded according to rounding mode rm.
+        /// </remarks>        
+        /// <param name="rm">RoundingMode term.</param>
+        /// <param name="t">FloatingPoint term</param>
+        /// <param name="sz">Size of the resulting bit-vector.</param>
+        /// <param name="signed">Indicates whether the result is a signed or unsigned bit-vector.</param>
+        public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool signed)
+        {
+            Contract.Ensures(Contract.Result<BitVecExpr>() != null);
+            if (signed)
+                return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
+            else
+                return new BitVecExpr(this, Native.Z3_mk_fpa_to_ubv(this.nCtx, rm.NativeObject, t.NativeObject, sz));
+        }
+
+        /// <summary>
+        /// Conversion of a floating-point term into a real-numbered term.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of the floating-poiunt term t into a
+        /// real number. Note that this type of conversion will often result in non-linear 
+        /// constraints over real terms.
+        /// </remarks>        
+        /// <param name="t">FloatingPoint term</param>
+        public RealExpr MkFPToReal(FPExpr t)
+        {
+            Contract.Ensures(Contract.Result<RealExpr>() != null);
+            return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject));
+        }
+        #endregion
+
+        #region Z3-specific extensions
+        /// <summary>
+        /// Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
+        /// </summary>
+        /// <remarks>
+        /// The size of the resulting bit-vector is automatically determined. Note that 
+        /// IEEE 754-2008 allows multiple different representations of NaN. This conversion 
+        /// knows only one NaN and it will always produce the same bit-vector represenatation of 
+        /// that NaN. 
+        /// </remarks>
+        /// <param name="t">FloatingPoint term.</param>
+        public BitVecExpr MkFPToIEEEBV(FPExpr t)
+        {
+            Contract.Ensures(Contract.Result<BitVecExpr>() != null);
+            return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
+        }
+
+        /// <summary>
+        /// Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
+        /// </summary>
+        /// <remarks>
+        /// Produces a term that represents the conversion of sig * 2^exp into a 
+        /// floating-point term of sort s. If necessary, the result will be rounded
+        /// 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="s">FloatingPoint sort.</param>
+        public BitVecExpr MkFPToFP(FPRMExpr rm, RealExpr sig, IntExpr exp, 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));
+        }
+        #endregion
+        #endregion // Floating-point Arithmetic
 
         #region Miscellaneous
         /// <summary>

src/api/dotnet/DatatypeExpr.cs

@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for DatatypeExpr </summary>
-        internal protected DatatypeExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal DatatypeExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {

src/api/dotnet/EnumSort.cs

@@ -78,7 +78,7 @@ namespace Microsoft.Z3
 
         #region Internal
         internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(name != null);

src/api/dotnet/Expr.cs

@@ -1448,6 +1448,281 @@ namespace Microsoft.Z3
         /// Indicates whether the term is a less than predicate over a finite domain.
         /// </summary>
         public bool IsFiniteDomainLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } }
+        #endregion
+
+        #region Floating-point terms
+        /// <summary>
+        ///  Indicates whether the terms is of floating-point sort.
+        /// </summary>
+        public bool IsFP
+        {
+            get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FLOATING_POINT_SORT; }
+        }
+
+        /// <summary>
+        ///  Indicates whether the terms is of floating-point rounding mode sort.
+        /// </summary>
+        public bool IsFPRM
+        {
+            get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_ROUNDING_MODE_SORT; }
+        }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point numeral
+        /// </summary>
+        public bool IsFPNumeral { get { return IsFP && IsNumeral; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point rounding mode numeral
+        /// </summary>
+        public bool IsFPRMNumeral { get { return IsFPRM && IsNumeral; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
+        /// </summary>
+        public bool IsFPRMRoundNearestTiesToEven{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
+        
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
+        /// </summary>
+        public bool IsFPRMRoundNearestTiesToAway{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }        
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundTowardNegative
+        /// </summary>
+        public bool IsFPRMRoundTowardNegative{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundTowardPositive
+        /// </summary>
+        public bool IsFPRMRoundTowardPositive{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundTowardZero
+        /// </summary>
+        public bool IsFPRMRoundTowardZero{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
+        /// </summary>
+        public bool IsFPRMExprRNE{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
+        
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
+        /// </summary>
+        public bool IsFPRMExprRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }        
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundTowardNegative
+        /// </summary>
+        public bool IsFPRMExprRTN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundTowardPositive
+        /// </summary>
+        public bool IsFPRMExprRTP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
+
+        /// <summary>
+        /// Indicates whether the term is the floating-point rounding numeral roundTowardZero
+        /// </summary>
+        public bool IsFPRMExprRTZ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point rounding mode numeral
+        /// </summary>
+        public bool IsFPRMExpr { 
+            get { 
+                return IsApp && 
+                       (FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY||
+                       FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN ||
+                       FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE ||
+                       FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE ||
+                       FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO);
+            }
+        }
+        
+        /// <summary>
+        /// Indicates whether the term is a floating-point +oo
+        /// </summary>
+        public bool IsFPPlusInfinity{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_PLUS_INF; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point -oo
+        /// </summary>
+        public bool IsFPMinusInfinity{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MINUS_INF; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point NaN
+        /// </summary>
+        public bool IsFPNaN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_NAN; } }
+
+                /// <summary>
+        /// Indicates whether the term is a floating-point +zero
+        /// </summary>
+        public bool IsFPPlusZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point -zero
+        /// </summary>
+        public bool IsFPMinusZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point addition term
+        /// </summary>
+        public bool IsFPAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ADD; } }
+
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point subtraction term
+        /// </summary>
+        public bool IsFPSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_SUB; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point negation term
+        /// </summary>
+        public bool IsFPNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_NEG; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point multiplication term
+        /// </summary>
+        public bool IsFPMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MUL; } }
+                    
+        /// <summary>
+        /// Indicates whether the term is a floating-point divison term
+        /// </summary>
+        public bool IsFPDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_DIV; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point remainder term
+        /// </summary>
+        public bool IsFPRem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_REM; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point term absolute value term
+        /// </summary>
+        public bool IsFPAbs { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ABS; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point minimum term
+        /// </summary>
+        public bool IsFPMin { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MIN; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point maximum term
+        /// </summary>
+        public bool IsFPMax { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MAX; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point fused multiply-add term
+        /// </summary>
+        public bool IsFPFMA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_FMA; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point square root term
+        /// </summary>
+        public bool IsFPSqrt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_SQRT; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point roundToIntegral term
+        /// </summary>
+        public bool IsFPRoundToIntegral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ROUND_TO_INTEGRAL; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point equality term
+        /// </summary>
+        public bool IsFPEq { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_EQ; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point less-than term
+        /// </summary>
+        public bool IsFPLt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LT; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point greater-than term
+        /// </summary>
+        public bool IsFPGt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GT; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point less-than or equal term
+        /// </summary>
+        public bool IsFPLe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LE; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point greater-than or erqual term
+        /// </summary>
+        public bool IsFPGe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GE; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point isNaN predicate term
+        /// </summary>
+        public bool IsFPisNaN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NAN; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point isInf predicate term
+        /// </summary>
+        public bool IsFPisInf { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_INF; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point isZero predicate term
+        /// </summary>
+        public bool IsFPisZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_ZERO; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point isNormal term
+        /// </summary>
+        public bool IsFPisNormal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NORMAL; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point isSubnormal predicate term
+        /// </summary>
+        public bool IsFPisSubnormal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_SUBNORMAL; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point isNegative predicate term
+        /// </summary>
+        public bool IsFPisNegative { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; } }    
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point isPositive predicate term
+        /// </summary>
+        public bool IsFPisPositive { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; } }    
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point constructor term
+        /// </summary>
+        public bool IsFPFP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_FP; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point conversion term
+        /// </summary>
+        public bool IsFPToFp { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_FP; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point conversion from unsigned bit-vector term
+        /// </summary>
+        public bool IsFPToFpUnsigned { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_FP_UNSIGNED; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point conversion to unsigned bit-vector term
+        /// </summary>
+        public bool IsFPToUBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_UBV; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point conversion to signed bit-vector term
+        /// </summary>
+        public bool IsFPToSBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_SBV; } }
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point conversion to real term
+        /// </summary>
+        public bool IsFPToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_REAL; } }    
+
+
+        /// <summary>
+        /// Indicates whether the term is a floating-point conversion to IEEE-754 bit-vector term
+        /// </summary>
+        public bool IsFPToIEEEBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_IEEE_BV; } }
+
         #endregion
         #endregion
 
@@ -1489,10 +1764,6 @@ namespace Microsoft.Z3
         /// <summary> 
         /// Constructor for Expr 
         /// </summary>
-        internal protected Expr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
-        /// <summary> 
-        /// Constructor for Expr 
-        /// </summary>
         internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 
 #if DEBUG
@@ -1541,7 +1812,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_ROUNDING_MODE_SORT: return new FPRMNum(ctx, obj);
                 }
             }
 
@@ -1552,7 +1825,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_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj);
             }
 
             return new Expr(ctx, obj);

src/api/dotnet/FPExpr.cs

@@ -0,0 +1,52 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    FPExpr.cs
+
+Abstract:
+
+    Z3 Managed API: Floating Point Expressions
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2013-06-10
+
+Notes:
+    
+--*/
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{    
+    /// <summary>
+    /// FloatingPoint Expressions
+    /// </summary>
+    public class FPExpr : Expr
+    {
+        /// <summary>
+        /// The number of exponent bits.
+        /// </summary>
+        public uint EBits { get { return ((FPSort)Sort).EBits; } }
+
+        /// <summary>
+        /// The number of significand bits.
+        /// </summary>
+        public uint SBits { get { return ((FPSort)Sort).EBits; } }
+
+        #region Internal
+        /// <summary> Constructor for FPExpr </summary>
+        internal FPExpr(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/FPNum.cs

@@ -0,0 +1,103 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    FPNum.cs
+
+Abstract:
+
+    Z3 Managed API: Floating Point Numerals
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2013-06-10
+
+Notes:
+    
+--*/
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// FloatiungPoint Numerals
+    /// </summary>
+    [ContractVerification(true)]
+    public class FPNum : FPExpr
+    {
+        /// <summary>
+        /// Retrieves the sign of a floating-point literal
+        /// </summary>
+        /// <remarks>
+        /// Remarks: returns true if the numeral is negative
+        /// </remarks>
+        public bool Sign
+        {
+            get
+            {
+                int res = 0;
+                if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0)                
+                    throw new Z3Exception("Sign is not a Boolean value");
+                return res != 0;
+            }
+        }
+
+        /// <summary>
+        /// The significand value of a floating-point numeral as a string
+        /// </summary>
+        /// <remarks>
+        /// The significand s is always 0 &lt; s &lt; 2.0; the resulting string is long
+        /// enough to represent the real significand precisely.
+        /// </remarks>
+        public string Significand
+        {
+            get
+            {
+                return Native.Z3_fpa_get_numeral_significand_string(Context.nCtx, NativeObject);
+            }
+        }
+
+        /// <summary>
+        /// Return the exponent value of a floating-point numeral as a string
+        /// </summary>
+        public string Exponent
+        {
+            get
+            {
+                return Native.Z3_fpa_get_numeral_exponent_string(Context.nCtx, NativeObject);
+            }
+        }
+
+        /// <summary>
+        /// Return the exponent value of a floating-point numeral as a signed 64-bit integer
+        /// </summary>
+        public Int64 ExponentInt64
+        {
+            get
+            {
+                Int64 result = 0;
+                if (Native.Z3_fpa_get_numeral_exponent_int64(Context.nCtx, NativeObject, ref result) == 0)
+                    throw new Z3Exception("Exponent is not a 64 bit integer");
+                return result;
+            }
+        }
+
+        #region Internal
+        internal FPNum(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+
+        /// <summary>
+        /// Returns a string representation of the numeral.
+        /// </summary>        
+        public override string ToString()
+        {
+            return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
+        }
+    }
+}

src/api/dotnet/FPRMExpr.cs

@@ -0,0 +1,42 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    FPRMExpr.cs
+
+Abstract:
+
+    Z3 Managed API: Floating Point Expressions over Rounding Modes
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2013-06-10
+
+Notes:
+    
+--*/
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// FloatingPoint RoundingMode Expressions
+    /// </summary>
+    public class FPRMExpr : Expr
+    {
+        #region Internal
+        /// <summary> Constructor for FPRMExpr </summary>
+        internal FPRMExpr(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/FPRMNum.cs

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

src/api/dotnet/FPRMSort.cs

@@ -0,0 +1,43 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    FPRMSort.cs
+
+Abstract:
+
+    Z3 Managed API: Rounding Mode Sort
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2013-06-10
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// The FloatingPoint RoundingMode sort
+    /// </summary>
+    public class FPRMSort : Sort
+    {
+        #region Internal
+        internal FPRMSort(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal FPRMSort(Context ctx)
+            : base(ctx, Native.Z3_mk_fpa_rounding_mode_sort(ctx.nCtx))
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/FPSort.cs

@@ -0,0 +1,52 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    FPSort.cs
+
+Abstract:
+
+    Z3 Managed API: Floating Point Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2013-06-10
+
+Notes:
+    
+--*/
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// FloatingPoint sort
+    /// </summary>
+    public class FPSort : Sort
+    {
+        /// <summary>
+        /// The number of exponent bits.
+        /// </summary>
+        public uint EBits { get { return Native.Z3_fpa_get_ebits(Context.nCtx, NativeObject); } }
+
+        /// <summary>
+        /// The number of significand bits.
+        /// </summary>
+        public uint SBits { get { return Native.Z3_fpa_get_sbits(Context.nCtx, NativeObject); } }
+
+        #region Internal
+        internal FPSort(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal FPSort(Context ctx, uint ebits, uint sbits)
+            : base(ctx, Native.Z3_mk_fpa_sort(ctx.nCtx, ebits, sbits))
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }    
+}

src/api/dotnet/IntExpr.cs

@@ -1,5 +1,5 @@
 /*++
-Copyright (<c>) 2012 Microsoft Corporation
+Copyright (c) 2012 Microsoft Corporation
 
 Module Name:
 
@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for IntExpr </summary>
-        internal protected IntExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal IntExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {

src/api/dotnet/ListSort.cs

@@ -113,9 +113,9 @@ namespace Microsoft.Z3
             }
         }
 
-        #region Internal        
+        #region Internal
         internal ListSort(Context ctx, Symbol name, Sort elemSort)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(name != null);

src/api/dotnet/Microsoft.Z3.csproj

@@ -342,6 +342,12 @@
     <Compile Include="ConstructorList.cs" />
     <Compile Include="DatatypeExpr.cs" />
     <Compile Include="DatatypeSort.cs" />
+    <Compile Include="FPExpr.cs" />
+    <Compile Include="FPNum.cs" />
+    <Compile Include="FPRMExpr.cs" />
+    <Compile Include="FPRMNum.cs" />
+    <Compile Include="FPRMSort.cs" />
+    <Compile Include="FPSort.cs" />
     <Compile Include="Global.cs" />
     <Compile Include="IDecRefQueue.cs" />
     <Compile Include="Enumerations.cs" />

src/api/dotnet/Quantifier.cs

@@ -160,7 +160,7 @@ namespace Microsoft.Z3
         #region Internal
         [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
         internal Quantifier(Context ctx, bool isForall, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(sorts != null);
@@ -203,7 +203,7 @@ namespace Microsoft.Z3
 
         [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
         internal Quantifier(Context ctx, bool isForall, Expr[] bound, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(body != null);

src/api/dotnet/RealExpr.cs

@@ -32,11 +32,6 @@ namespace Microsoft.Z3
     {
         #region Internal
         /// <summary> Constructor for RealExpr </summary>
-        internal protected RealExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
         internal RealExpr(Context ctx, IntPtr obj)
             : base(ctx, obj)
         {

src/api/dotnet/Sort.cs

@@ -116,8 +116,7 @@ namespace Microsoft.Z3
         #region Internal
         /// <summary>
         /// Sort constructor
-        /// </summary>
-        internal protected Sort(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
+        /// </summary>        
         internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 
 #if DEBUG
@@ -146,6 +145,8 @@ namespace Microsoft.Z3
                 case Z3_sort_kind.Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj);
                 case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj);
                 case Z3_sort_kind.Z3_RELATION_SORT: return new RelationSort(ctx, obj);
+                case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPSort(ctx, obj);
+                case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMSort(ctx, obj);
                 default:
                     throw new Z3Exception("Unknown sort kind");
             }

src/api/dotnet/TupleSort.cs

@@ -68,7 +68,7 @@ namespace Microsoft.Z3
 
         #region Internal
         internal TupleSort(Context ctx, Symbol name, uint numFields, Symbol[] fieldNames, Sort[] fieldSorts)
-            : base(ctx)
+            : base(ctx, IntPtr.Zero)
         {
             Contract.Requires(ctx != null);
             Contract.Requires(name != null);

src/api/java/AST.java

@@ -227,10 +227,8 @@ public class AST extends Z3Object
     void incRef(long o) throws Z3Exception
     {
         // Console.WriteLine("AST IncRef()");
-        if (getContext() == null)
-            throw new Z3Exception("inc() called on null context");
-        if (o == 0)
-            throw new Z3Exception("inc() called on null AST");
+        if (getContext() == null || o == 0)
+			return;
         getContext().ast_DRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
@@ -238,10 +236,8 @@ public class AST extends Z3Object
     void decRef(long o) throws Z3Exception
     {
         // Console.WriteLine("AST DecRef()");
-        if (getContext() == null)
-            throw new Z3Exception("dec() called on null context");
-        if (o == 0)
-            throw new Z3Exception("dec() called on null AST");
+        if (getContext() == null || o == 0)
+			return;
         getContext().ast_DRQ().add(o);
         super.decRef(o);
     }

src/api/java/ArithExpr.java

@@ -25,11 +25,6 @@ public class ArithExpr extends Expr
 	/**
 	 * Constructor for ArithExpr
 	 **/
-	protected ArithExpr(Context ctx)
-	{
-		super(ctx);
-	}
-
 	ArithExpr(Context ctx, long obj) throws Z3Exception
 	{
 		super(ctx, obj);

src/api/java/ArrayExpr.java

@@ -26,11 +26,6 @@ public class ArrayExpr extends Expr
 	/**
 	 * Constructor for ArrayExpr
 	 **/
-	protected ArrayExpr(Context ctx)
-	{
-		super(ctx);
-	}
-
 	ArrayExpr(Context ctx, long obj) throws Z3Exception
 	{
 		super(ctx, obj);

src/api/java/BitVecExpr.java

@@ -37,11 +37,6 @@ public class BitVecExpr extends Expr
 	/**
 	 * Constructor for BitVecExpr
 	 **/
-	BitVecExpr(Context ctx)
-	{
-		super(ctx);
-	}
-
 	BitVecExpr(Context ctx, long obj) throws Z3Exception
 	{
 		super(ctx, obj);

src/api/java/Context.java

@@ -85,7 +85,7 @@ public class Context extends IDisposable
     /**
      * Create an array of symbols.
      **/
-    Symbol[] MkSymbols(String[] names) throws Z3Exception
+    Symbol[] mkSymbols(String[] names) throws Z3Exception
     {
         if (names == null)
             return null;
@@ -218,7 +218,7 @@ public class Context extends IDisposable
     public EnumSort mkEnumSort(String name, String... enumNames)
             throws Z3Exception
     {
-        return new EnumSort(this, mkSymbol(name), MkSymbols(enumNames));
+        return new EnumSort(this, mkSymbol(name), mkSymbols(enumNames));
     }
 
     /**
@@ -295,7 +295,7 @@ public class Context extends IDisposable
     {
 
         return new Constructor(this, mkSymbol(name), mkSymbol(recognizer),
-                MkSymbols(fieldNames), sorts, sortRefs);
+                mkSymbols(fieldNames), sorts, sortRefs);
     }
 
     /**
@@ -358,7 +358,7 @@ public class Context extends IDisposable
     public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
             throws Z3Exception
     {
-        return mkDatatypeSorts(MkSymbols(names), c);
+        return mkDatatypeSorts(mkSymbols(names), c);
     }
 
     /**
@@ -2000,25 +2000,22 @@ public class Context extends IDisposable
 
     /**
      * Create a universal Quantifier.
+	 * @param sorts the sorts of the bound variables. 
+	 * @param names names of the bound variables 
+	 * @param body the body of the quantifier. 
+	 * @param weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
+     * @param patterns array containing the patterns created using {@code MkPattern}. 
+	 * @param noPatterns array containing the anti-patterns created using {@code MkPattern}. 
+	 * @param quantifierID optional symbol to track quantifier. 
+	 * @param skolemID optional symbol to track skolem constants.
+	 * 
 	 * Remarks:  Creates a forall formula, where
      * {@code weight"/> is the weight, <paramref name="patterns} is
      * an array of patterns, {@code sorts} is an array with the sorts
      * of the bound variables, {@code names} is an array with the
      * 'names' of the bound variables, and {@code body} is the body
      * of the quantifier. Quantifiers are associated with weights indicating the
-     * importance of using the quantifier during instantiation. 
-     * 
-	 * @param sorts the sorts of the bound variables. 
-	 * @param names names of the bound variables 
-	 * @param body the body of the quantifier. 
-	 * @param weight quantifiers are
-     * associated with weights indicating the importance of using the quantifier
-     * during instantiation. By default, pass the weight 0.
-     * @param patterns array containing the patterns created using
-     * {@code MkPattern}. 
-	 * @param noPatterns array containing the anti-patterns created using {@code MkPattern}. 
-	 * @param quantifierID optional symbol to track quantifier. 
-	 * @param skolemID optional symbol to track skolem constants.
+     * importance of using the quantifier during instantiation.
      **/
     public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
             int weight, Pattern[] patterns, Expr[] noPatterns,
@@ -2789,6 +2786,778 @@ public class Context extends IDisposable
         return new Fixedpoint(this);
     }
 
+    
+    /**
+     * Create the floating-point RoundingMode sort.
+     * @throws Z3Exception 
+     **/    
+    public FPRMSort mkFPRoundingModeSort() throws Z3Exception
+    {
+        return new FPRMSort(this);
+    }
+
+    /**
+     * Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
+     * @throws Z3Exception 
+     **/
+    public FPRMExpr mkFPRoundNearestTiesToEven() throws Z3Exception
+    {
+        return new FPRMExpr(this, Native.mkFpaRoundNearestTiesToEven(nCtx()));
+    }
+
+    /**
+     * Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
+     * @throws Z3Exception 
+     **/
+    public FPRMNum mkFPRNE() throws Z3Exception
+    {
+        return new FPRMNum(this, Native.mkFpaRne(nCtx()));
+    }
+
+    /**
+     * Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
+     * @throws Z3Exception 
+     **/
+    public FPRMNum mkFPRoundNearestTiesToAway() throws Z3Exception
+    {
+        return new FPRMNum(this, Native.mkFpaRoundNearestTiesToAway(nCtx()));
+    }
+
+    /**
+     * Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
+     * @throws Z3Exception 
+     **/
+    public FPRMNum mkFPRNA() throws Z3Exception
+    {
+        return new FPRMNum(this, Native.mkFpaRna(nCtx()));
+    }
+
+    /**
+     * Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
+     * @throws Z3Exception 
+     **/
+    public FPRMNum mkFPRoundTowardPositive() throws Z3Exception
+    {
+        return new FPRMNum(this, Native.mkFpaRoundTowardPositive(nCtx()));
+    }
+
+    /**
+     * Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
+     * @throws Z3Exception 
+     **/
+    public FPRMNum mkFPRTP() throws Z3Exception
+    {
+        return new FPRMNum(this, Native.mkFpaRtp(nCtx()));
+    }
+
+    /**
+     * Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
+     * @throws Z3Exception 
+     **/
+    public FPRMNum mkFPRoundTowardNegative() throws Z3Exception
+    {
+        return new FPRMNum(this, Native.mkFpaRoundTowardNegative(nCtx()));
+    }
+
+    /**
+     * Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
+     * @throws Z3Exception 
+     **/
+    public FPRMNum mkFPRTN() throws Z3Exception
+    {
+        return new FPRMNum(this, Native.mkFpaRtn(nCtx()));
+    }
+
+    /**
+     * Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
+     * @throws Z3Exception 
+     **/
+    public FPRMNum mkFPRoundTowardZero() throws Z3Exception
+    {
+        return new FPRMNum(this, Native.mkFpaRoundTowardZero(nCtx()));
+    }
+
+    /**
+     * Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
+     * @throws Z3Exception 
+     **/
+    public FPRMNum mkFPRTZ() throws Z3Exception
+    {
+        return new FPRMNum(this, Native.mkFpaRtz(nCtx()));
+    }        
+
+    /**
+     * Create a FloatingPoint sort.
+     * @param ebits exponent bits in the FloatingPoint sort.
+     * @param sbits significand bits in the FloatingPoint sort.
+     * @throws Z3Exception 
+     **/     
+    public FPSort mkFPSort(int ebits, int sbits) throws Z3Exception
+    {
+        return new FPSort(this, ebits, sbits);
+    }
+
+    /**
+     * Create the half-precision (16-bit) FloatingPoint sort.
+     * @throws Z3Exception 
+     **/
+    public FPSort mkFPSortHalf() throws Z3Exception
+    {
+        return new FPSort(this, Native.mkFpaSortHalf(nCtx()));
+    }
+
+    /**
+     * Create the half-precision (16-bit) FloatingPoint sort.
+     * @throws Z3Exception 
+     **/
+    public FPSort mkFPSort16() throws Z3Exception
+    {
+        return new FPSort(this, Native.mkFpaSort16(nCtx()));
+    }
+
+    /**
+     * Create the single-precision (32-bit) FloatingPoint sort.
+     * @throws Z3Exception 
+     **/
+    public FPSort mkFPSortSingle() throws Z3Exception
+    {
+        return new FPSort(this, Native.mkFpaSortSingle(nCtx()));
+    }
+
+    /**
+     * Create the single-precision (32-bit) FloatingPoint sort.
+     * @throws Z3Exception 
+     **/
+    public FPSort mkFPSort32() throws Z3Exception
+    {
+        return new FPSort(this, Native.mkFpaSort32(nCtx()));
+    }
+
+    /**
+     * Create the double-precision (64-bit) FloatingPoint sort.
+     * @throws Z3Exception 
+     **/
+    public FPSort mkFPSortDouble() throws Z3Exception
+    {
+        return new FPSort(this, Native.mkFpaSortDouble(nCtx()));
+    }
+
+    /**
+     * Create the double-precision (64-bit) FloatingPoint sort.
+     * @throws Z3Exception 
+     **/
+    public FPSort mkFPSort64() throws Z3Exception
+    {
+        return new FPSort(this, Native.mkFpaSort64(nCtx()));
+    }
+
+    /**
+     * Create the quadruple-precision (128-bit) FloatingPoint sort.
+     * @throws Z3Exception 
+     **/
+    public FPSort mkFPSortQuadruple() throws Z3Exception
+    {        
+        return new FPSort(this, Native.mkFpaSortQuadruple(nCtx()));
+    }
+
+    /**
+     * Create the quadruple-precision (128-bit) FloatingPoint sort.
+     * @throws Z3Exception 
+     **/
+    public FPSort mkFPSort128() throws Z3Exception
+    {
+        return new FPSort(this, Native.mkFpaSort128(nCtx()));
+    }
+
+
+    /**
+     * Create a NaN of sort s.
+     * @param s FloatingPoint sort.     
+     * @throws Z3Exception 
+     **/               
+    public FPNum mkFPNaN(FPSort s) throws Z3Exception
+    {
+        return new FPNum(this, Native.mkFpaNan(nCtx(), s.getNativeObject()));
+    }
+
+    /**
+     * Create a floating-point infinity of sort s.
+     * @param s FloatingPoint sort.   
+     * @param negative indicates whether the result should be negative.
+     * @throws Z3Exception 
+     **/             
+    public FPNum mkFPInf(FPSort s, boolean negative) throws Z3Exception
+    {
+        return new FPNum(this, Native.mkFpaInf(nCtx(), s.getNativeObject(), negative));
+    }
+
+    /**
+     * Create a floating-point zero of sort s.
+     * @param s FloatingPoint sort.   
+     * @param negative indicates whether the result should be negative.
+     * @throws Z3Exception 
+     **/             
+    public FPNum mkFPZero(FPSort s, boolean negative) throws Z3Exception
+    {
+        return new FPNum(this, Native.mkFpaZero(nCtx(), s.getNativeObject(), negative));
+    }
+
+    /**
+     * Create a numeral of FloatingPoint sort from a float.
+     * @param v numeral value.
+     * @param s FloatingPoint sort.
+     * @throws Z3Exception 
+     **/        
+    public FPNum mkFPNumeral(float v, FPSort s) throws Z3Exception
+    {
+        return new FPNum(this, Native.mkFpaNumeralFloat(nCtx(), v, s.getNativeObject()));
+    }
+
+    /**
+     * Create a numeral of FloatingPoint sort from a float.
+     * @param v numeral value.
+     * @param s FloatingPoint sort.
+     * @throws Z3Exception 
+     **/        
+    public FPNum mkFPNumeral(double v, FPSort s) throws Z3Exception
+    {
+        return new FPNum(this, Native.mkFpaNumeralDouble(nCtx(), v, s.getNativeObject()));
+    }
+
+    /**
+     * Create a numeral of FloatingPoint sort from an int.
+     * * @param v numeral value.
+     * @param s FloatingPoint sort.
+     * @throws Z3Exception 
+     **/                    
+    public FPNum mkFPNumeral(int v, FPSort s) throws Z3Exception
+    {
+        return new FPNum(this, Native.mkFpaNumeralInt(nCtx(), v, s.getNativeObject()));
+    }
+
+    /**
+     * Create a numeral of FloatingPoint sort from a sign bit and two integers.
+     * @param sgn the sign.
+     * @param sig the significand.
+     * @param exp the exponent.
+     * @param s FloatingPoint sort.
+     * @throws Z3Exception 
+     **/            
+    public FPNum mkFPNumeral(boolean sgn, int sig, int exp, FPSort s) throws Z3Exception
+    {
+        return new FPNum(this, Native.mkFpaNumeralUintInt(nCtx(), sgn, sig, exp, s.getNativeObject()));    
+    }
+
+    /**
+     * Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
+     * @param sgn the sign.
+     * @param sig the significand.
+     * @param exp the exponent.
+     * @param s FloatingPoint sort.
+     * @throws Z3Exception 
+     **/
+    public FPNum mkFPNumeral(boolean sgn, long sig, long exp, FPSort s) throws Z3Exception
+    {
+        return new FPNum(this, Native.mkFpaNumeralUint64Int64(nCtx(), sgn, sig, exp, s.getNativeObject()));
+    }
+
+    /**
+     * Create a numeral of FloatingPoint sort from a float.
+     * @param v numeral value.
+     * @param s FloatingPoint sort.
+     * @throws Z3Exception 
+     **/        
+    public FPNum mkFP(float v, FPSort s) throws Z3Exception
+    {
+        return mkFPNumeral(v, s);
+    }
+
+    /**
+     * Create a numeral of FloatingPoint sort from a float.
+     * @param v numeral value.
+     * @param s FloatingPoint sort.
+     * @throws Z3Exception 
+     **/             
+    public FPNum mkFP(double v, FPSort s) throws Z3Exception
+    {
+        return mkFPNumeral(v, s);
+    }
+
+    /**
+     * Create a numeral of FloatingPoint sort from an int.
+     * @param v numeral value.
+     * @param s FloatingPoint sort.
+     * @throws Z3Exception 
+     **/        
+            
+    public FPNum mkFP(int v, FPSort s) throws Z3Exception
+    {
+        return mkFPNumeral(v, s);
+    }
+
+    /**
+     * Create a numeral of FloatingPoint sort from a sign bit and two integers.
+     * @param sgn the sign.        
+     * @param exp the exponent.
+     * @param sig the significand.
+     * @param s FloatingPoint sort.
+     * @throws Z3Exception 
+     **/                     
+    public FPNum mkFP(boolean sgn, int exp, int sig, FPSort s) throws Z3Exception
+    {
+        return mkFPNumeral(sgn, sig, exp, s);
+    }
+
+    /**
+     * Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
+     * @param sgn the sign.        
+     * @param exp the exponent.
+     * @param sig the significand.
+     * @param s FloatingPoint sort.
+     * @throws Z3Exception 
+     **/                     
+    public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s) throws Z3Exception
+    {
+        return mkFPNumeral(sgn, sig, exp, s);
+    }
+
+
+    /**
+     * Floating-point absolute value
+     * @param t floating-point term
+     * @throws Z3Exception 
+     **/     
+    public FPExpr mkFPAbs(FPExpr t) throws Z3Exception 
+    {
+        return new FPExpr(this, Native.mkFpaAbs(nCtx(), t.getNativeObject()));
+    }
+
+    /**
+     * Floating-point negation
+     * @param t floating-point term
+     * @throws Z3Exception 
+     **/     
+    public FPExpr mkFPNeg(FPExpr t) throws Z3Exception 
+    {
+        return new FPExpr(this, Native.mkFpaNeg(nCtx(), t.getNativeObject()));
+    }
+
+    /**
+     * Floating-point addition
+     * @param rm rounding mode term
+     * @param t1 floating-point term
+     * @param t2 floating-point term     
+     * @throws Z3Exception 
+     **/     
+    public FPExpr mkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2) throws Z3Exception 
+    {
+        return new FPExpr(this, Native.mkFpaAdd(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
+    }
+
+    /**
+     * Floating-point subtraction
+     * @param rm rounding mode term
+     * @param t1 floating-point term
+     * @param t2 floating-point term
+     * @throws Z3Exception 
+     **/     
+    public FPExpr mkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2) throws Z3Exception 
+    {
+        return new FPExpr(this, Native.mkFpaSub(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
+    }
+
+    /**
+     * Floating-point multiplication
+     * @param rm rounding mode term
+     * @param t1 floating-point term
+     * @param t2 floating-point term
+     * @throws Z3Exception 
+     **/     
+    public FPExpr mkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2) throws Z3Exception 
+    {
+        return new FPExpr(this, Native.mkFpaMul(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
+    }
+
+    /**
+     * Floating-point division
+     * @param rm rounding mode term
+     * @param t1 floating-point term
+     * @param t2 floating-point term
+     * @throws Z3Exception 
+     **/     
+    public FPExpr mkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2) throws Z3Exception 
+    {
+        return new FPExpr(this, Native.mkFpaDiv(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject()));
+    }
+
+    /**
+     * Floating-point fused multiply-add
+     * @param rm rounding mode term
+     * @param t1 floating-point term
+     * @param t2 floating-point term
+     * @param t3">floating-point term
+     * Remarks:
+     * The result is round((t1 * t2) + t3)
+     * @throws Z3Exception 
+     **/
+    public FPExpr mkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3) throws Z3Exception 
+    {
+        return new FPExpr(this, Native.mkFpaFma(nCtx(), rm.getNativeObject(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject()));
+    }
+
+    /**
+     * Floating-point square root
+     * @param rm rounding mode term        
+     * @param t floating-point term
+     * @throws Z3Exception 
+     **/        
+    public FPExpr mkFPSqrt(FPRMExpr rm, FPExpr t) throws Z3Exception 
+    {
+        return new FPExpr(this, Native.mkFpaSqrt(nCtx(), rm.getNativeObject(), t.getNativeObject()));
+    }
+
+    /**
+     * Floating-point remainder
+     * @param t1 floating-point term
+     * @param t2 floating-point term
+     * @throws Z3Exception 
+     **/             
+    public FPExpr mkFPRem(FPExpr t1, FPExpr t2) throws Z3Exception 
+    {
+        return new FPExpr(this, Native.mkFpaRem(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
+    }
+
+    /**
+     * Floating-point roundToIntegral. Rounds a floating-point number to 
+     * the closest integer, again represented as a floating-point number.
+     * @param rm">term of RoundingMode sort
+     * @param t floating-point term
+     * @throws Z3Exception 
+     **/             
+    public FPExpr mkFPRoundToIntegral(FPRMExpr rm, FPExpr t) throws Z3Exception
+    {            
+        return new FPExpr(this, Native.mkFpaRoundToIntegral(nCtx(), rm.getNativeObject(), t.getNativeObject()));
+    }
+
+    /**
+     * Minimum of floating-point numbers.
+     * @param t1 floating-point term
+     * @param t2 floating-point term
+     * @throws Z3Exception 
+     **/
+    public FPExpr mkFPMin(FPExpr t1, FPExpr t2) throws Z3Exception
+    {
+        return new FPExpr(this, Native.mkFpaMin(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
+    }
+
+    /**
+     * Maximum of floating-point numbers.
+     * @param t1 floating-point term
+     * @param t2 floating-point term
+     * @throws Z3Exception 
+     **/             
+    public FPExpr mkFPMax(FPExpr t1, FPExpr t2) throws Z3Exception
+    {
+        return new FPExpr(this, Native.mkFpaMax(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
+    }   
+    
+    /**
+     * Floating-point less than or equal.
+     * @param t1 floating-point term
+     * @param t2 floating-point term
+     * @throws Z3Exception 
+     **/             
+    public BoolExpr mkFPLEq(FPExpr t1, FPExpr t2) throws Z3Exception 
+    {            
+        return new BoolExpr(this, Native.mkFpaLeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
+    }
+
+    /**
+     * Floating-point less than.
+     * @param t1 floating-point term
+     * @param t2 floating-point term
+     * @throws Z3Exception 
+     **/             
+    public BoolExpr mkFPLt(FPExpr t1, FPExpr t2) throws Z3Exception 
+    {                    
+        return new BoolExpr(this, Native.mkFpaLt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
+    }
+
+    /**
+     * Floating-point greater than or equal.
+     * @param t1 floating-point term
+     * @param t2 floating-point term
+     * @throws Z3Exception 
+     **/             
+    public BoolExpr mkFPGEq(FPExpr t1, FPExpr t2) throws Z3Exception 
+    {                    
+        return new BoolExpr(this, Native.mkFpaGeq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
+    }
+
+    /**
+     * Floating-point greater than.
+     * @param t1 floating-point term
+     * @param t2 floating-point term
+     * @throws Z3Exception 
+     **/             
+    public BoolExpr mkFPGt(FPExpr t1, FPExpr t2) throws Z3Exception 
+    {            
+        return new BoolExpr(this, Native.mkFpaGt(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
+    }
+
+    /**
+     * Floating-point equality.
+     * @param t1 floating-point term
+     * @param t2 floating-point term
+     * Remarks:
+     * Note that this is IEEE 754 equality (as opposed to standard =).
+     * @throws Z3Exception 
+     **/
+    public BoolExpr mkFPEq(FPExpr t1, FPExpr t2) throws Z3Exception
+    {
+        return new BoolExpr(this, Native.mkFpaEq(nCtx(), t1.getNativeObject(), t2.getNativeObject()));
+    }
+
+    /**
+     * Predicate indicating whether t is a normal floating-point number.\
+     * @param t floating-point term
+     * @throws Z3Exception 
+     **/
+    public BoolExpr mkFPIsNormal(FPExpr t) throws Z3Exception 
+    {
+        return new BoolExpr(this, Native.mkFpaIsNormal(nCtx(), t.getNativeObject()));
+    }
+
+    /**
+     * Predicate indicating whether t is a subnormal floating-point number.\
+     * @param t floating-point term
+     * @throws Z3Exception 
+     **/        
+    public BoolExpr mkFPIsSubnormal(FPExpr t) throws Z3Exception 
+    {                   
+        return new BoolExpr(this, Native.mkFpaIsSubnormal(nCtx(), t.getNativeObject()));
+    }
+
+    /**
+     * Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0.
+     * @param t floating-point term
+     * @throws Z3Exception 
+     **/        
+    public BoolExpr mkFPIsZero(FPExpr t) throws Z3Exception
+    {
+        return new BoolExpr(this, Native.mkFpaIsZero(nCtx(), t.getNativeObject()));
+    }
+
+    /**
+     * Predicate indicating whether t is a floating-point number representing +oo or -oo.
+     * @param t floating-point term
+     * @throws Z3Exception 
+     **/        
+    public BoolExpr mkFPIsInfinite(FPExpr t) throws Z3Exception
+    {    
+        return new BoolExpr(this, Native.mkFpaIsInfinite(nCtx(), t.getNativeObject()));
+    }
+
+    /**
+     * Predicate indicating whether t is a NaN.
+     * @param t floating-point term
+     * @throws Z3Exception 
+     **/             
+    public BoolExpr mkFPIsNaN(FPExpr t) throws Z3Exception 
+    {                   
+        return new BoolExpr(this, Native.mkFpaIsNan(nCtx(), t.getNativeObject()));
+    }
+
+    /**
+     * Predicate indicating whether t is a negative floating-point number.
+     * @param t floating-point term
+     * @throws Z3Exception 
+     **/        
+    public BoolExpr mkFPIsNegative(FPExpr t) throws Z3Exception
+    {     
+        return new BoolExpr(this, Native.mkFpaIsNegative(nCtx(), t.getNativeObject()));
+    }
+
+    /**
+     * Predicate indicating whether t is a positive floating-point number.
+     * @param t floating-point term
+     * @throws Z3Exception 
+     **/        
+    public BoolExpr mkFPIsPositive(FPExpr t) throws Z3Exception
+    {
+        return new BoolExpr(this, Native.mkFpaIsPositive(nCtx(), t.getNativeObject()));
+    }        
+
+    /**
+     * Create an expression of FloatingPoint sort from three bit-vector expressions.     
+     * @param sgn bit-vector term (of size 1) representing the sign.
+     * @param sig bit-vector term representing the significand.
+     * @param exp bit-vector term representing the exponent.
+     * Remarks:
+     * This is the operator named `fp' in the SMT FP theory definition. 
+     * Note that sgn 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 
+     * of the resulting expression is automatically determined from the bit-vector sizes
+     * of the arguments.
+     * @throws Z3Exception 
+     **/
+    public FPExpr mkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp) throws Z3Exception
+    {
+        return new FPExpr(this, Native.mkFpaFp(nCtx(), sgn.getNativeObject(), sig.getNativeObject(), exp.getNativeObject()));
+    }
+
+    /**
+     * Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
+     * @param bv">bit-vector value (of size m).
+     * @param s FloatingPoint sort (ebits+sbits == m)
+     * Remarks:
+     * Produces a term that represents the conversion of a bit-vector term bv to a 
+     * floating-point term of sort s. The bit-vector size of bv (m) must be equal 
+     * to ebits+sbits of s. The format of the bit-vector is as defined by the 
+     * IEEE 754-2008 interchange format.
+     * @throws Z3Exception 
+     **/
+    public FPExpr mkFPToFP(BitVecExpr bv, FPSort s) throws Z3Exception
+    {
+        return new FPExpr(this, Native.mkFpaToFpBv(nCtx(), bv.getNativeObject(), s.getNativeObject()));
+    }
+
+    /**
+     * Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
+     * @param rm RoundingMode term.
+     * @param t FloatingPoint term.
+     * @param s FloatingPoint sort.
+     * Remarks:
+     * Produces a term that represents the conversion of a floating-point term t to a
+     * floating-point term of sort s. If necessary, the result will be rounded according
+     * to rounding mode rm.
+     * @throws Z3Exception 
+     **/
+    public FPExpr mkFPToFP(FPRMExpr rm, FPExpr t, FPSort s) throws Z3Exception
+    {
+        return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
+    }
+
+    /**
+     * Conversion of a term of real sort into a term of FloatingPoint sort.
+     * @param rm RoundingMode term.
+     * @param t term of Real sort.
+     * @param s FloatingPoint sort.
+     * Remarks:
+     * Produces a term that represents the conversion of term t of real sort into a
+     * floating-point term of sort s. If necessary, the result will be rounded according
+     * to rounding mode rm.
+     * @throws Z3Exception 
+     **/
+    public FPExpr mkFPToFP(FPRMExpr rm, RealExpr t, FPSort s) throws Z3Exception
+    {
+        return new FPExpr(this, Native.mkFpaToFpReal(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
+    }
+
+    /**
+     * Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
+     * @param rm RoundingMode term.
+     * @param t term of bit-vector sort.
+     * @param s FloatingPoint sort.
+     * @param signed flag indicating whether t is interpreted as signed or unsigned bit-vector.
+     * Remarks:
+     * Produces a term that represents the conversion of the bit-vector term t into a
+     * floating-point term of sort s. The bit-vector t is taken to be in signed 
+     * 2's complement format (when signed==true, otherwise unsigned). If necessary, the 
+     * result will be rounded according to rounding mode rm.
+     * @throws Z3Exception 
+     **/
+    public FPExpr mkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed) throws Z3Exception
+    {
+        if (signed)
+            return new FPExpr(this, Native.mkFpaToFpSigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
+        else
+            return new FPExpr(this, Native.mkFpaToFpUnsigned(nCtx(), rm.getNativeObject(), t.getNativeObject(), s.getNativeObject()));
+    }
+
+    /**
+     * Conversion of a floating-point number to another FloatingPoint sort s.
+     * @param s FloatingPoint sort
+     * @param rm floating-point rounding mode term
+     * @param t floating-point term
+     * Remarks:
+     * Produces a term that represents the conversion of a floating-point term t to a different
+     * FloatingPoint sort s. If necessary, rounding according to rm is applied. 
+     * @throws Z3Exception 
+     **/
+    public FPExpr mkFPToFP(FPSort s, FPRMExpr rm, FPExpr t) throws Z3Exception
+    {
+        return new FPExpr(this, Native.mkFpaToFpFloat(nCtx(), s.getNativeObject(), rm.getNativeObject(), t.getNativeObject()));
+    }
+
+    /**
+     * Conversion of a floating-point term into a bit-vector.
+     * @param rm RoundingMode term.
+     * @param t FloatingPoint term
+     * @param sz Size of the resulting bit-vector.
+     * @param signed Indicates whether the result is a signed or unsigned bit-vector.
+     * Remarks:
+     * Produces a term that represents the conversion of the floating-poiunt term t into a
+     * bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, 
+     * the result will be rounded according to rounding mode rm.        
+     * @throws Z3Exception 
+     **/
+    public BitVecExpr mkFPToBV(FPRMExpr rm, FPExpr t, int sz, boolean signed) throws Z3Exception
+    {
+        if (signed)
+            return new BitVecExpr(this, Native.mkFpaToSbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
+        else
+            return new BitVecExpr(this, Native.mkFpaToUbv(nCtx(), rm.getNativeObject(), t.getNativeObject(), sz));
+    }
+
+    /**
+     * Conversion of a floating-point term into a real-numbered term.
+     * @param t FloatingPoint term
+     * Remarks:
+     * Produces a term that represents the conversion of the floating-poiunt term t into a
+     * real number. Note that this type of conversion will often result in non-linear 
+     * constraints over real terms.
+     * @throws Z3Exception 
+     **/
+    public RealExpr mkFPToReal(FPExpr t) throws Z3Exception
+    {
+        return new RealExpr(this, Native.mkFpaToReal(nCtx(), t.getNativeObject()));
+    }
+
+    /**
+     * Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
+     * @param t FloatingPoint term.
+     * Remarks:
+     * The size of the resulting bit-vector is automatically determined. Note that 
+     * IEEE 754-2008 allows multiple different representations of NaN. This conversion 
+     * knows only one NaN and it will always produce the same bit-vector represenatation of 
+     * that NaN. 
+     * @throws Z3Exception 
+     **/
+    public BitVecExpr mkFPToIEEEBV(FPExpr t) throws Z3Exception
+    {
+        return new BitVecExpr(this, Native.mkFpaToIeeeBv(nCtx(), t.getNativeObject()));
+    }
+
+    /**
+     * 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 s FloatingPoint sort.
+     * Remarks:
+     * Produces a term that represents the conversion of sig * 2^exp into a 
+     * floating-point term of sort s. If necessary, the result will be rounded
+     * according to rounding mode rm.
+     * @throws Z3Exception 
+     **/
+         
+    public BitVecExpr mkFPToFP(FPRMExpr rm, RealExpr sig, IntExpr exp, FPSort s) throws Z3Exception
+    {
+        return new BitVecExpr(this, Native.mkFpaToFpRealInt(nCtx(), rm.getNativeObject(), sig.getNativeObject(), exp.getNativeObject(), s.getNativeObject()));
+    }
+    
+    
     /**
      * Wraps an AST.
 	 * Remarks: This function is used for transitions between

src/api/java/DatatypeExpr.java

@@ -25,11 +25,6 @@ public class DatatypeExpr extends Expr
 	/**
 	 * Constructor for DatatypeExpr
 	 **/
-	protected DatatypeExpr(Context ctx)
-	{
-		super(ctx);
-	}
-
 	DatatypeExpr(Context ctx, long obj) throws Z3Exception
 	{
 		super(ctx, obj);

src/api/java/EnumSort.java

@@ -64,7 +64,7 @@ public class EnumSort extends Sort
 
 	EnumSort(Context ctx, Symbol name, Symbol[] enumNames) throws Z3Exception
 	{
-		super(ctx);
+		super(ctx, 0);
 
 		int n = enumNames.length;
 		long[] n_constdecls = new long[n];

src/api/java/Expr.java

@@ -2161,6 +2161,10 @@ public class Expr extends AST
 				return new RatNum(ctx, obj);
 			case Z3_BV_SORT:
 				return new BitVecNum(ctx, obj);
+			case Z3_FLOATING_POINT_SORT:
+				return new FPNum(ctx, obj);
+			case Z3_ROUNDING_MODE_SORT:
+				return new FPRMNum(ctx, obj);
 			default: ;
 			}
 		}
@@ -2179,6 +2183,10 @@ public class Expr extends AST
 			return new ArrayExpr(ctx, obj);
 		case Z3_DATATYPE_SORT:
 			return new DatatypeExpr(ctx, obj);
+		case Z3_FLOATING_POINT_SORT:
+			return new FPExpr(ctx, obj);
+		case Z3_ROUNDING_MODE_SORT:
+			return new FPRMExpr(ctx, obj);
 		default: ;
 		}
 

src/api/java/FPExpr.java

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

src/api/java/FPNum.java

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

src/api/java/FPRMExpr.java

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

src/api/java/FPRMNum.java

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

src/api/java/FPRMSort.java

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

src/api/java/FPSort.java

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

src/api/java/Fixedpoint.java

@@ -173,7 +173,7 @@ public class Fixedpoint extends Z3Object
 
     /**
      * Backtrack one backtracking point.
-	 * Remarks: Note that an exception is thrown if {#code pop} 
+	 * Remarks: Note that an exception is thrown if {@code pop} 
 	 * is called without a corresponding {@code push}
      *  
 	 * @see push

src/api/java/IntExpr.java

@@ -26,11 +26,6 @@ public class IntExpr extends ArithExpr
 	 * Constructor for IntExpr
 	 * @throws Z3Exception on error
 	 **/
-	protected IntExpr(Context ctx) throws Z3Exception
-	{
-		super(ctx);
-	}
-
 	IntExpr(Context ctx, long obj) throws Z3Exception
 	{
 		super(ctx, obj);

src/api/java/ListSort.java

@@ -88,7 +88,7 @@ public class ListSort extends Sort
 
     ListSort(Context ctx, Symbol name, Sort elemSort) throws Z3Exception
     {
-        super(ctx);
+        super(ctx, 0);
 
         Native.LongPtr inil = new Native.LongPtr(), iisnil = new Native.LongPtr();
         Native.LongPtr icons = new Native.LongPtr(), iiscons = new Native.LongPtr();

src/api/java/Quantifier.java

@@ -149,7 +149,7 @@ public class Quantifier extends BoolExpr
             Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
             Symbol quantifierID, Symbol skolemID) throws Z3Exception
     {
-        super(ctx);
+        super(ctx, 0);
 
         getContext().checkContextMatch(patterns);
         getContext().checkContextMatch(noPatterns);
@@ -185,7 +185,7 @@ public class Quantifier extends BoolExpr
             int weight, Pattern[] patterns, Expr[] noPatterns,
             Symbol quantifierID, Symbol skolemID) throws Z3Exception
     {
-        super(ctx);
+        super(ctx, 0);
 
         getContext().checkContextMatch(noPatterns);
         getContext().checkContextMatch(patterns);

src/api/java/RealExpr.java

@@ -25,11 +25,6 @@ public class RealExpr extends ArithExpr
     /**
      * Constructor for RealExpr
      **/
-    protected RealExpr(Context ctx)
-    {
-        super(ctx);
-    }
-
     RealExpr(Context ctx, long obj) throws Z3Exception
     {
         super(ctx, obj);

src/api/java/Sort.java

@@ -98,18 +98,9 @@ public class Sort extends AST
     /**
      * Sort constructor
      **/
-    protected Sort(Context ctx) throws Z3Exception
-    {
-        super(ctx);
-        {
-        }
-    }
-
     Sort(Context ctx, long obj) throws Z3Exception
     {
         super(ctx, obj);
-        {
-        }
     }
 
     void checkNativeObject(long obj) throws Z3Exception
@@ -143,6 +134,10 @@ public class Sort extends AST
             return new FiniteDomainSort(ctx, obj);
         case Z3_RELATION_SORT:
             return new RelationSort(ctx, obj);
+        case Z3_FLOATING_POINT_SORT:
+        	return new FPSort(ctx, obj);
+        case Z3_ROUNDING_MODE_SORT:
+    		return new FPRMSort(ctx, obj);
         default:
             throw new Z3Exception("Unknown sort kind");
         }

src/api/java/TupleSort.java

@@ -59,7 +59,7 @@ public class TupleSort extends Sort
     TupleSort(Context ctx, Symbol name, int numFields, Symbol[] fieldNames,
             Sort[] fieldSorts) throws Z3Exception
     {
-        super(ctx);
+        super(ctx, 0);
 
         Native.LongPtr t = new Native.LongPtr();
         setNativeObject(Native.mkTupleSort(ctx.nCtx(), name.getNativeObject(),

src/api/python/z3printer.py

@@ -8,6 +8,7 @@
 import sys, io, z3
 from z3consts import *
 from z3core import *
+from ctypes import *
 
 ##############################
 #
@@ -30,7 +31,7 @@ _z3_op_to_str = {
     Z3_OP_BASHR : '>>', Z3_OP_BSHL : '<<', Z3_OP_BLSHR : 'LShR', 
     Z3_OP_CONCAT : 'Concat', Z3_OP_EXTRACT : 'Extract', Z3_OP_BV2INT : 'BV2Int',
     Z3_OP_ARRAY_MAP : 'Map', Z3_OP_SELECT : 'Select', Z3_OP_STORE : 'Store', 
-    Z3_OP_CONST_ARRAY : 'K' 
+    Z3_OP_CONST_ARRAY : 'K'
     }
 
 # List of infix operators
@@ -45,17 +46,64 @@ _z3_unary = [ Z3_OP_UMINUS, Z3_OP_BNOT, Z3_OP_BNEG ]
 # Precedence
 _z3_precedence = {
     Z3_OP_POWER : 0,
-    Z3_OP_UMINUS : 1, Z3_OP_BNEG : 1, Z3_OP_BNOT : 1,
+    Z3_OP_UMINUS : 1, Z3_OP_BNEG : 1, Z3_OP_BNOT : 1, 
     Z3_OP_MUL : 2, Z3_OP_DIV : 2, Z3_OP_IDIV : 2, Z3_OP_MOD : 2, Z3_OP_BMUL : 2, Z3_OP_BSDIV : 2, Z3_OP_BSMOD : 2,
-    Z3_OP_ADD : 3, Z3_OP_SUB : 3, Z3_OP_BADD : 3, Z3_OP_BSUB : 3,
+    Z3_OP_ADD : 3, Z3_OP_SUB : 3, Z3_OP_BADD : 3, Z3_OP_BSUB : 3,    
     Z3_OP_BASHR : 4, Z3_OP_BSHL : 4,
     Z3_OP_BAND : 5,
     Z3_OP_BXOR : 6,
     Z3_OP_BOR : 7,
     Z3_OP_LE : 8, Z3_OP_LT : 8, Z3_OP_GE : 8, Z3_OP_GT : 8, Z3_OP_EQ : 8, Z3_OP_SLEQ : 8, Z3_OP_SLT : 8, Z3_OP_SGEQ : 8, Z3_OP_SGT : 8,
-    Z3_OP_IFF : 8
+    Z3_OP_IFF : 8,
+    
+    Z3_OP_FPA_NEG : 1,
+    Z3_OP_FPA_MUL : 2, Z3_OP_FPA_DIV : 2, Z3_OP_FPA_REM : 2, Z3_OP_FPA_FMA : 2,
+    Z3_OP_FPA_ADD: 3, Z3_OP_FPA_SUB : 3,
+    Z3_OP_FPA_LE : 8, Z3_OP_FPA_LT : 8, Z3_OP_FPA_GE : 8, Z3_OP_FPA_GT : 8, Z3_OP_FPA_EQ : 8
     }
 
+# FPA operators 
+_z3_op_to_fpa_normal_str = {
+    Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN : 'RoundNearestTiesToEven()', Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY : 'RoundNearestTiesToAway()',
+    Z3_OP_FPA_RM_TOWARD_POSITIVE : 'RoundTowardPositive()', Z3_OP_FPA_RM_TOWARD_NEGATIVE : 'RoundTowardNegative()',
+    Z3_OP_FPA_RM_TOWARD_ZERO : 'RoundTowardZero()',
+    Z3_OP_FPA_PLUS_INF : '+oo', Z3_OP_FPA_MINUS_INF : '-oo',
+    Z3_OP_FPA_NAN : 'NaN', Z3_OP_FPA_PLUS_ZERO : 'PZero', Z3_OP_FPA_MINUS_ZERO : 'NZero',
+    Z3_OP_FPA_ADD : 'fpAdd', Z3_OP_FPA_SUB : 'fpSub', Z3_OP_FPA_NEG : 'fpNeg', Z3_OP_FPA_MUL : 'fpMul',
+    Z3_OP_FPA_DIV : 'fpDiv', Z3_OP_FPA_REM : 'fpRem', Z3_OP_FPA_ABS : 'fpAbs',
+    Z3_OP_FPA_MIN : 'fpMin', Z3_OP_FPA_MAX : 'fpMax',
+    Z3_OP_FPA_FMA : 'fpFMA', Z3_OP_FPA_SQRT : 'fpSqrt', Z3_OP_FPA_ROUND_TO_INTEGRAL : 'fpRoundToIntegral',
+
+    Z3_OP_FPA_EQ : 'fpEQ', Z3_OP_FPA_LT : 'fpLT', Z3_OP_FPA_GT : 'fpGT', Z3_OP_FPA_LE : 'fpLEQ',
+    Z3_OP_FPA_GE : 'fpGEQ',
+
+    Z3_OP_FPA_IS_NAN : 'fpIsNaN', Z3_OP_FPA_IS_INF : 'fpIsInf', Z3_OP_FPA_IS_ZERO : 'fpIsZero',
+    Z3_OP_FPA_IS_NORMAL : 'fpIsNormal', Z3_OP_FPA_IS_SUBNORMAL : 'fpIsSubnormal',
+    Z3_OP_FPA_IS_NEGATIVE : 'fpIsNegative', Z3_OP_FPA_IS_POSITIVE : 'fpIsPositive',
+    
+    Z3_OP_FPA_FP : 'fpFP', Z3_OP_FPA_TO_FP : 'fpToFP', Z3_OP_FPA_TO_FP_UNSIGNED: 'fpToFPUnsigned',
+    Z3_OP_FPA_TO_UBV : 'fpToUBV', Z3_OP_FPA_TO_SBV : 'fpToSBV', Z3_OP_FPA_TO_REAL: 'fpToReal',
+    Z3_OP_FPA_TO_IEEE_BV : 'fpToIEEEBV'
+    }
+
+_z3_op_to_fpa_pretty_str = {    
+    Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN : 'RNE()', Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY : 'RNA()',
+    Z3_OP_FPA_RM_TOWARD_POSITIVE : 'RTP()', Z3_OP_FPA_RM_TOWARD_NEGATIVE : 'RTN()',
+    Z3_OP_FPA_RM_TOWARD_ZERO : 'RTZ()',
+    Z3_OP_FPA_PLUS_INF : '+oo', Z3_OP_FPA_MINUS_INF : '-oo',
+    Z3_OP_FPA_NAN : 'NaN', Z3_OP_FPA_PLUS_ZERO : '+0.0', Z3_OP_FPA_MINUS_ZERO : '-0.0',
+    
+    Z3_OP_FPA_ADD : '+', Z3_OP_FPA_SUB : '-', Z3_OP_FPA_MUL : '*', Z3_OP_FPA_DIV : '/', 
+    Z3_OP_FPA_REM : '%', Z3_OP_FPA_NEG : '-',
+    
+    Z3_OP_FPA_EQ : 'fpEQ', Z3_OP_FPA_LT : '<', Z3_OP_FPA_GT : '>', Z3_OP_FPA_LE : '<=', Z3_OP_FPA_GE : '>='
+}
+    
+_z3_fpa_infix = [
+    Z3_OP_FPA_ADD, Z3_OP_FPA_SUB, Z3_OP_FPA_MUL, Z3_OP_FPA_DIV, Z3_OP_FPA_REM,
+    Z3_OP_FPA_LT, Z3_OP_FPA_GT, Z3_OP_FPA_LE, Z3_OP_FPA_GE
+]
+
 def _is_assoc(k):
     return k == Z3_OP_BOR or k == Z3_OP_BXOR or k == Z3_OP_BAND or k == Z3_OP_ADD or k == Z3_OP_BADD or k == Z3_OP_MUL or k == Z3_OP_BMUL
 
@@ -138,6 +186,7 @@ for _k in _z3_infix:
     _infix_map[_k] = True
 for _k in _z3_unary:
     _unary_map[_k] = True
+    
 for _k in _z3_infix_compact:
     _infix_compact_map[_k] = True
 
@@ -463,6 +512,7 @@ class Formatter:
         self.precision           = 10
         self.ellipses            = to_format(_ellipses)
         self.max_visited         = 10000
+        self.fpa_pretty          = True
     
     def pp_ellipses(self):
         return self.ellipses
@@ -499,6 +549,8 @@ class Formatter:
             return seq1('Array', (self.pp_sort(s.domain()), self.pp_sort(s.range())))
         elif isinstance(s, z3.BitVecSortRef):
             return seq1('BitVec', (to_format(s.size()), ))
+        elif isinstance(s, z3.FPSortRef):
+            return seq1('FPSort', (to_format(s.ebits()), to_format(s.sbits())))
         else:
             return to_format(s.name())
 
@@ -520,6 +572,123 @@ class Formatter:
     def pp_bv(self, a):
         return to_format(a.as_string())
 
+    def pp_fprm_value(self, a):
+        z3._z3_assert(z3.is_fprm_value(a), 'expected FPRMNumRef')
+        if self.fpa_pretty and (a.decl().kind() in _z3_op_to_fpa_pretty_str):
+            return to_format(_z3_op_to_fpa_pretty_str.get(a.decl().kind()))
+        else:
+            return to_format(_z3_op_to_fpa_normal_str.get(a.decl().kind()))
+
+    def pp_fp_value(self, a):
+        z3._z3_assert(isinstance(a, z3.FPNumRef), 'type mismatch')
+        if not self.fpa_pretty:            
+            if (a.isNaN()):
+                return to_format('NaN')
+            elif (a.isInf()):
+                if (a.isNegative()):
+                    return to_format('-oo')
+                else:
+                    return to_format('+oo')
+            elif (a.isZero()):
+                if (a.isNegative()):
+                    return to_format('-zero')
+                else:
+                    return to_format('+zero')
+            else:
+                z3._z3_assert(z3.is_fp_value(a), 'expecting FP num ast')
+                r = []
+                sgn = c_int(0)
+                sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn))
+                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('-'))
+                r.append(to_format(sig))
+                r.append(to_format('*(2**'))
+                r.append(to_format(exp))
+                r.append(to_format(', '))
+                r.append(to_format(a.sort()))
+                r.append(to_format('))'))
+                return compose(r)
+        else:
+            if (a.isNaN()):
+                return to_format(_z3_op_to_fpa_pretty_str[Z3_OP_FPA_NAN])
+            elif (a.isInf()):
+                if (a.isNegative()):
+                    return to_format(_z3_op_to_fpa_pretty_str[Z3_OP_FPA_MINUS_INF])
+                else:
+                    return to_format(_z3_op_to_fpa_pretty_str[Z3_OP_FPA_PLUS_INF])
+            elif (a.isZero()):
+                if (a.isNegative()):
+                    return to_format(_z3_op_to_fpa_pretty_str[Z3_OP_FPA_MINUS_ZERO])
+                else:
+                    return to_format(_z3_op_to_fpa_pretty_str[Z3_OP_FPA_PLUS_ZERO])
+            else:
+                z3._z3_assert(z3.is_fp_value(a), 'expecting FP num ast')
+                r = []
+                sgn = c_long(0)
+                sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn))
+                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))
+                if (exp != '0'):
+                    r.append(to_format('*(2**'))
+                    r.append(to_format(exp))
+                    r.append(to_format(')'))                
+                return compose(r)
+
+
+    def pp_fp(self, a, d, xs):
+        z3._z3_assert(isinstance(a, z3.FPRef), "type mismatch")
+        k = a.decl().kind()
+        op = '?'
+        if (self.fpa_pretty and k in _z3_op_to_fpa_pretty_str):
+            op = _z3_op_to_fpa_pretty_str[k]
+        elif k in _z3_op_to_fpa_normal_str:
+            op = _z3_op_to_fpa_normal_str[k]
+        elif k in _z3_op_to_str:
+            op = _z3_op_to_str[k]        
+
+        n = a.num_args()
+
+        if self.fpa_pretty:
+            if self.is_infix(k) and n >= 3:            
+                rm = a.arg(0)
+                if z3.is_fprm_value(rm) and z3._dflt_rm(a.ctx).eq(rm):
+                    arg1 = to_format(self.pp_expr(a.arg(1), d+1, xs))
+                    arg2 = to_format(self.pp_expr(a.arg(2), d+1, xs))
+                    r = []
+                    r.append(arg1)
+                    r.append(to_format(' '))
+                    r.append(to_format(op))
+                    r.append(to_format(' '))
+                    r.append(arg2)
+                    return compose(r)
+            elif k == Z3_OP_FPA_NEG:
+                return compose([to_format('-') , to_format(self.pp_expr(a.arg(0), d+1, xs))])
+
+        if k in _z3_op_to_fpa_normal_str:
+            op = _z3_op_to_fpa_normal_str[k]
+        
+        r = []        
+        r.append(to_format(op))
+        if not z3.is_const(a):
+            r.append(to_format('('))                        
+            first = True
+            for c in a.children():                
+                if first:
+                    first = False
+                else:
+                    r.append(to_format(', '))
+                r.append(self.pp_expr(c, d+1, xs))
+            r.append(to_format(')'))
+            return compose(r)
+        else:
+            return to_format(a.as_string())
+
     def pp_prefix(self, a, d, xs):
         r  = []
         sz = 0
@@ -678,9 +847,15 @@ class Formatter:
         elif z3.is_rational_value(a):
             return self.pp_rational(a)
         elif z3.is_algebraic_value(a):
-            return self.pp_algebraic(a)
+            return self.pp_algebraic(a)        
         elif z3.is_bv_value(a):
             return self.pp_bv(a)
+        elif z3.is_fprm_value(a):
+            return self.pp_fprm_value(a)
+        elif z3.is_fp_value(a):
+            return self.pp_fp_value(a)
+        elif z3.is_fp(a):
+            return self.pp_fp(a, d, xs)
         elif z3.is_const(a):
             return self.pp_const(a)
         else:
@@ -939,6 +1114,12 @@ def set_pp_option(k, v):
         else:
             set_html_mode(False)
         return True
+    if k == 'fpa_pretty':
+        if v:
+            set_fpa_pretty(True)
+        else:
+            set_fpa_pretty(False)
+        return True
     val = getattr(_PP, k, None)
     if val != None:
         z3._z3_assert(type(v) == type(val), "Invalid pretty print option value")
@@ -965,6 +1146,23 @@ def set_html_mode(flag=True):
     else:
         _Formatter = Formatter()
 
+def set_fpa_pretty(flag=True):
+    global _Formatter
+    global _z3_op_to_str
+    _Formatter.fpa_pretty = flag
+    if flag:
+        for (_k,_v) in _z3_op_to_fpa_pretty_str.items():
+            _z3_op_to_str[_k] = _v
+        for _k in _z3_fpa_infix:
+            _infix_map[_k] = True
+    else:
+        for (_k,_v) in _z3_op_to_fpa_normal_str.items():
+            _z3_op_to_str[_k] = _v
+        for _k in _z3_fpa_infix:
+            _infix_map[_k] = False
+
+set_fpa_pretty(True)
+
 def in_html_mode():
     return isinstance(_Formatter, HTMLFormatter)
 

src/api/z3.h

@@ -28,6 +28,7 @@ Notes:
 #include"z3_polynomial.h"
 #include"z3_rcf.h"
 #include"z3_interp.h"
+#include"z3_fpa.h"
 
 #undef __in
 #undef __out

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_ROUNDING_MODE_SORT,
     Z3_UNKNOWN_SORT = 1000
 } Z3_sort_kind;
 
@@ -767,7 +769,7 @@ typedef enum
          - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.
 
 
-      - Z3_OP_PR_HYPER_RESOLVE: Hyper-resolution rule.
+    - Z3_OP_PR_HYPER_RESOLVE: Hyper-resolution rule.
 
         The premises of the rules is a sequence of clauses.
         The first clause argument is the main clause of the rule.
@@ -875,6 +877,90 @@ typedef enum
 
       - Z3_OP_DT_ACCESSOR: datatype accessor.
 
+      - Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: Floating-point rounding mode RNE
+      
+      - Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: Floating-point rounding mode RNA
+      
+      - Z3_OP_FPA_RM_TOWARD_POSITIVE: Floating-point rounding mode RTP
+      
+      - Z3_OP_FPA_RM_TOWARD_NEGATIVE: Floating-point rounding mode RTN
+      
+      - Z3_OP_FPA_RM_TOWARD_ZERO: Floating-point rounding mode RTZ
+
+      - Z3_OP_FPA_NUM: Floating-point value
+      
+      - Z3_OP_FPA_PLUS_INF: Floating-point +oo
+      
+      - Z3_OP_FPA_MINUS_INF: Floating-point -oo
+      
+      - Z3_OP_FPA_NAN: Floating-point NaN
+      
+      - Z3_OP_FPA_PLUS_ZERO: Floating-point +zero
+      
+      - Z3_OP_FPA_MINUS_ZERO: Floating-point -zero
+
+      - Z3_OP_FPA_ADD: Floating-point addition
+      
+      - Z3_OP_FPA_SUB: Floating-point subtraction
+      
+      - Z3_OP_FPA_NEG: Floating-point negation
+
+      - Z3_OP_FPA_MUL: Floating-point multiplication
+      
+      - Z3_OP_FPA_DIV: Floating-point division
+      
+      - Z3_OP_FPA_REM: Floating-point remainder
+      
+      - Z3_OP_FPA_ABS: Floating-point absolute value
+      
+      - Z3_OP_FPA_MIN: Floating-point minimum
+
+      - Z3_OP_FPA_MAX: Floating-point maximum
+
+      - Z3_OP_FPA_FMA: Floating-point fused multiply-add
+      
+      - Z3_OP_FPA_SQRT: Floating-point square root
+      
+      - Z3_OP_FPA_ROUND_TO_INTEGRAL: Floating-point round to integral
+
+      - Z3_OP_FPA_EQ: Floating-point equality 
+
+      - Z3_OP_FPA_LT: Floating-point less than
+      
+      - Z3_OP_FPA_GT: Floating-point greater than
+      
+      - Z3_OP_FPA_LE: Floating-point less than or equal
+      
+      - Z3_OP_FPA_GE: Floating-point greater than or equal
+
+      - Z3_OP_FPA_IS_NAN: Floating-point isNaN
+      
+      - Z3_OP_FPA_IS_INF: Floating-point isInfinite
+
+      - Z3_OP_FPA_IS_ZERO: Floating-point isZero
+
+      - Z3_OP_FPA_IS_NORMAL: Floating-point isNormal
+
+      - Z3_OP_FPA_IS_SUBNORMAL: Floating-point isSubnormal      
+
+      - Z3_OP_FPA_IS_NEGATIVE: Floating-point isNegative
+
+      - Z3_OP_FPA_IS_POSITIVE: Floating-point isPositive
+
+      - Z3_OP_FPA_FP: Floating-point constructor from 3 bit-vectors
+
+      - Z3_OP_FPA_TO_FP: Floating-point conversion (various)
+
+      - Z3_OP_FPA_TO_FP_UNSIGNED: Floating-point conversion from unsigend bit-vector
+      
+      - Z3_OP_FPA_TO_UBV: Floating-point conversion to unsigned bit-vector
+
+      - Z3_OP_FPA_TO_SBV: Floating-point conversion to signed bit-vector
+      
+      - Z3_OP_FPA_TO_REAL: Floating-point conversion to real number
+
+      - Z3_OP_FPA_TO_IEEE_BV: Floating-point conversion to IEEE-754 bit-vector
+      
       - Z3_OP_UNINTERPRETED: kind used for uninterpreted symbols.
 */
 typedef enum {
@@ -1056,6 +1142,55 @@ typedef enum {
     Z3_OP_DT_RECOGNISER,
     Z3_OP_DT_ACCESSOR,
 
+    // Floating-Point Arithmetic
+    Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN,
+    Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY,
+    Z3_OP_FPA_RM_TOWARD_POSITIVE,
+    Z3_OP_FPA_RM_TOWARD_NEGATIVE,
+    Z3_OP_FPA_RM_TOWARD_ZERO,
+
+    Z3_OP_FPA_NUM,
+    Z3_OP_FPA_PLUS_INF,
+    Z3_OP_FPA_MINUS_INF,
+    Z3_OP_FPA_NAN,
+    Z3_OP_FPA_PLUS_ZERO,
+    Z3_OP_FPA_MINUS_ZERO,
+
+    Z3_OP_FPA_ADD,
+    Z3_OP_FPA_SUB,
+    Z3_OP_FPA_NEG,
+    Z3_OP_FPA_MUL,
+    Z3_OP_FPA_DIV,
+    Z3_OP_FPA_REM,
+    Z3_OP_FPA_ABS,
+    Z3_OP_FPA_MIN,
+    Z3_OP_FPA_MAX,
+    Z3_OP_FPA_FMA,
+    Z3_OP_FPA_SQRT,
+    Z3_OP_FPA_ROUND_TO_INTEGRAL,
+
+    Z3_OP_FPA_EQ,
+    Z3_OP_FPA_LT,
+    Z3_OP_FPA_GT,
+    Z3_OP_FPA_LE,
+    Z3_OP_FPA_GE,
+    Z3_OP_FPA_IS_NAN,
+    Z3_OP_FPA_IS_INF,
+    Z3_OP_FPA_IS_ZERO,
+    Z3_OP_FPA_IS_NORMAL,
+    Z3_OP_FPA_IS_SUBNORMAL,
+    Z3_OP_FPA_IS_NEGATIVE,
+    Z3_OP_FPA_IS_POSITIVE,
+
+    Z3_OP_FPA_FP,
+    Z3_OP_FPA_TO_FP,
+    Z3_OP_FPA_TO_FP_UNSIGNED,
+    Z3_OP_FPA_TO_UBV,
+    Z3_OP_FPA_TO_SBV,
+    Z3_OP_FPA_TO_REAL,
+
+    Z3_OP_FPA_TO_IEEE_BV,
+
     Z3_OP_UNINTERPRETED         
 } Z3_decl_kind;
 
@@ -1698,8 +1833,7 @@ extern "C" {
     /**
        \brief Create the real type. 
 
-       This type is not a floating point number.
-       Z3 does not have support for floating point numbers yet.
+       Note that this type is not a floating point number.
 
        def_API('Z3_mk_real_sort', SORT, (_in(CONTEXT), ))
     */

src/api/z3_fpa.h

@@ -0,0 +1,927 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    z3_fpa.h
+
+Abstract:
+
+    Additional APIs for floating-point arithmetic (FP).
+
+Author:
+
+    Christoph M. Wintersteiger (cwinter) 2013-06-05
+
+Notes:
+    
+--*/
+#ifndef _Z3_FPA_H_
+#define _Z3_FPA_H_
+
+#ifdef __cplusplus
+extern "C" {
+#endif // __cplusplus
+
+    /**
+    \defgroup capi C API
+
+    */
+
+    /*@{*/
+
+    /**
+        @name Floating-Point API
+        */
+    /*@{*/
+
+    /**
+        \brief Create the RoundingMode sort.
+
+        \param c logical context
+     
+        def_API('Z3_mk_fpa_rounding_mode_sort', SORT, (_in(CONTEXT),))
+    */
+    Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(__in Z3_context c);
+
+    /**
+        \brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
+
+        \param c logical context
+     
+        def_API('Z3_mk_fpa_round_nearest_ties_to_even', AST, (_in(CONTEXT),))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(__in Z3_context c);
+
+    /**
+        \brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
+
+        \param c logical context
+
+        def_API('Z3_mk_fpa_rne', AST, (_in(CONTEXT),))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_rne(__in Z3_context c);
+
+    /**
+        \brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
+
+        \param c logical context
+     
+        def_API('Z3_mk_fpa_round_nearest_ties_to_away', AST, (_in(CONTEXT),))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(__in Z3_context c);
+
+    /**
+        \brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
+
+        \param c logical context
+
+        def_API('Z3_mk_fpa_rna', AST, (_in(CONTEXT),))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_rna(__in Z3_context c);
+
+    /**
+        \brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
+
+        \param c logical context
+     
+        def_API('Z3_mk_fpa_round_toward_positive', AST, (_in(CONTEXT),))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(__in Z3_context c);
+
+    /**
+        \brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
+
+        \param c logical context
+
+        def_API('Z3_mk_fpa_rtp', AST, (_in(CONTEXT),))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_rtp(__in Z3_context c);
+
+    /**
+        \brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
+     
+        \param c logical context
+
+        def_API('Z3_mk_fpa_round_toward_negative', AST, (_in(CONTEXT),))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(__in Z3_context c);
+
+    /**
+        \brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
+
+        \param c logical context
+
+        def_API('Z3_mk_fpa_rtn', AST, (_in(CONTEXT),))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_rtn(__in Z3_context c);
+
+    /**
+        \brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
+
+        \param c logical context
+     
+        def_API('Z3_mk_fpa_round_toward_zero', AST, (_in(CONTEXT),))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(__in Z3_context c);
+
+    /**
+        \brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
+
+        \param c logical context
+
+        def_API('Z3_mk_fpa_rtz', AST, (_in(CONTEXT),))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_rtz(__in Z3_context c);
+
+    /**
+        \brief Create a FloatingPoint sort.
+
+        \param c logical context
+        \param ebits number of exponent bits
+        \param sbits number of significand bits
+
+        \remark ebits must be larger than 1 and sbits must be larger than 2.
+     
+        def_API('Z3_mk_fpa_sort', SORT, (_in(CONTEXT), _in(UINT), _in(UINT)))        
+    */
+    Z3_sort Z3_API Z3_mk_fpa_sort(__in Z3_context c, __in unsigned ebits, __in unsigned sbits);
+
+    /**
+        \brief Create the half-precision (16-bit) FloatingPoint sort.
+
+        \param c logical context
+
+        def_API('Z3_mk_fpa_sort_half', SORT, (_in(CONTEXT),))
+    */
+    Z3_sort Z3_API Z3_mk_fpa_sort_half(__in Z3_context c);
+
+    /**
+        \brief Create the half-precision (16-bit) FloatingPoint sort.
+
+        \param c logical context
+
+        def_API('Z3_mk_fpa_sort_16', SORT, (_in(CONTEXT),))
+    */
+    Z3_sort Z3_API Z3_mk_fpa_sort_16(__in Z3_context c);
+
+    /**
+        \brief Create the single-precision (32-bit) FloatingPoint sort.
+
+        \param c logical context.       
+
+        def_API('Z3_mk_fpa_sort_single', SORT, (_in(CONTEXT),))
+    */
+    Z3_sort Z3_API Z3_mk_fpa_sort_single(__in Z3_context c);
+
+    /**
+        \brief Create the single-precision (32-bit) FloatingPoint sort.
+
+        \param c logical context
+
+        def_API('Z3_mk_fpa_sort_32', SORT, (_in(CONTEXT),))
+    */
+    Z3_sort Z3_API Z3_mk_fpa_sort_32(__in Z3_context c);
+
+    /**
+        \brief Create the double-precision (64-bit) FloatingPoint sort.
+
+        \param c logical context
+
+        def_API('Z3_mk_fpa_sort_double', SORT, (_in(CONTEXT),))
+    */
+    Z3_sort Z3_API Z3_mk_fpa_sort_double(__in Z3_context c);
+
+    /**
+        \brief Create the double-precision (64-bit) FloatingPoint sort.
+
+        \param c logical context
+
+        def_API('Z3_mk_fpa_sort_64', SORT, (_in(CONTEXT),))
+    */
+    Z3_sort Z3_API Z3_mk_fpa_sort_64(__in Z3_context c);
+
+    /**
+        \brief Create the quadruple-precision (128-bit) FloatingPoint sort.
+
+        \param c logical context
+
+        def_API('Z3_mk_fpa_sort_quadruple', SORT, (_in(CONTEXT),))
+    */
+    Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(__in Z3_context c);
+
+    /**
+        \brief Create the quadruple-precision (128-bit) FloatingPoint sort.
+
+        \param c logical context
+
+        def_API('Z3_mk_fpa_sort_128', SORT, (_in(CONTEXT),))
+    */
+    Z3_sort Z3_API Z3_mk_fpa_sort_128(__in Z3_context c);
+
+    /**
+        \brief Create a floating-point NaN of sort s.
+
+        \param c logical context
+        \param s target sort 
+     
+        def_API('Z3_mk_fpa_nan', AST, (_in(CONTEXT),_in(SORT)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_nan(__in Z3_context c, __in Z3_sort s);
+
+    /**
+        \brief Create a floating-point infinity of sort s.
+
+        \param c logical context
+        \param s target sort 
+        \param negative indicates whether the result should be negative
+     
+        When \c negative is true, -oo will be generated instead of +oo.
+
+        def_API('Z3_mk_fpa_inf', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_inf(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative);
+
+    /**
+        \brief Create a floating-point zero of sort s.
+
+        \param c logical context
+        \param s target sort
+        \param negative indicates whether the result should be negative
+
+        When \c negative is true, -zero will be generated instead of +zero.
+
+        def_API('Z3_mk_fpa_zero', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_zero(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative);
+
+    /**
+        \brief Create an expression of FloatingPoint sort from three bit-vector expressions.
+
+	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 
+        of the resulting expression is automatically determined from the bit-vector sizes
+        of the arguments.
+
+        \param c logical context
+        \param sgn sign         
+        \param exp exponent
+        \param sig significand
+
+        def_API('Z3_mk_fpa_fp', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
+    */
+    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.
+
+        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.
+
+        \param c logical context
+        \param v value
+        \param ty sort
+
+        ty must be a FloatingPoint sort
+
+        \sa Z3_mk_numeral
+
+        def_API('Z3_mk_fpa_numeral_float', AST, (_in(CONTEXT), _in(FLOAT), _in(SORT)))
+    */
+    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. 
+       
+       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
+
+       ty must be a FloatingPoint sort
+
+       \sa Z3_mk_numeral
+
+       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);
+
+    /**
+        \brief Create a numeral of FloatingPoint sort from a signed integer.
+
+        \param c logical context
+        \param v value
+        \param ty result sort
+
+        ty must be a FloatingPoint sort
+
+        \sa Z3_mk_numeral
+
+        def_API('Z3_mk_fpa_numeral_int', AST, (_in(CONTEXT), _in(INT), _in(SORT)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_numeral_int(__in Z3_context c, __in signed v, Z3_sort ty);
+
+    /**
+        \brief Create a numeral of FloatingPoint sort from a sign bit and two integers.
+
+        \param c logical context
+        \param sgn sign bit (true == negative)
+        \param sig significand
+        \param exp exponent
+        \param ty result sort
+
+        ty must be a FloatingPoint sort
+
+        \sa Z3_mk_numeral
+
+        def_API('Z3_mk_fpa_numeral_uint_int', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(INT), _in(SORT)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_numeral_uint_int(__in Z3_context c, __in Z3_bool sgn, __in unsigned sig, __in signed exp, Z3_sort ty);
+
+    /**
+        \brief Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
+
+        \param c logical context
+        \param sgn sign bit (true == negative)
+        \param sig significand
+        \param exp exponent
+        \param ty result sort
+
+        ty must be a FloatingPoint sort
+
+        \sa Z3_mk_numeral
+
+        def_API('Z3_mk_fpa_numeral_uint64_int64', AST, (_in(CONTEXT), _in(BOOL), _in(UINT64), _in(INT64), _in(SORT)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_numeral_uint64_int64(__in Z3_context c, __in Z3_bool sgn, __in __uint64 sig, __in __int64 exp, Z3_sort ty);
+
+    /**
+        \brief Floating-point absolute value
+
+        \param c logical context
+        \param t term of FloatingPoint sort
+     
+        def_API('Z3_mk_fpa_abs', AST, (_in(CONTEXT),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_abs(__in Z3_context c, __in Z3_ast t);
+   
+    /**
+        \brief Floating-point negation
+
+        \param c logical context
+        \param t term of FloatingPoint sort
+     
+        def_API('Z3_mk_fpa_neg', AST, (_in(CONTEXT),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_neg(__in Z3_context c, __in Z3_ast t);
+   
+    /**
+        \brief Floating-point addition
+
+        \param c logical context
+        \param rm term of RoundingMode sort
+        \param t1 term of FloatingPoint sort
+        \param t2 term of FloatingPoint sort
+
+        rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_add', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_add(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);
+   
+    /**
+        \brief Floating-point subtraction
+
+        \param c logical context
+        \param rm term of RoundingMode sort
+        \param t1 term of FloatingPoint sort
+        \param t2 term of FloatingPoint sort
+
+        rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_sub', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_sub(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);   
+   
+    /**
+        \brief Floating-point multiplication
+
+        \param c logical context
+        \param rm term of RoundingMode sort
+        \param t1 term of FloatingPoint sort
+        \param t2 term of FloatingPoint sort
+
+        rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_mul', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_mul(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);   
+   
+    /**
+        \brief Floating-point division
+
+        \param c logical context
+        \param rm term of RoundingMode sort
+        \param t1 term of FloatingPoint sort.
+        \param t2 term of FloatingPoint sort
+
+        The nodes rm must be of RoundingMode sort t1 and t2 must have the same FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_div', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_div(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);    
+   
+    /**
+        \brief Floating-point fused multiply-add.
+
+        \param c logical context
+        \param rm term of RoundingMode sort
+        \param t1 term of FloatingPoint sort
+        \param t2 term of FloatingPoint sor
+        \param t3 term of FloatingPoint sort
+
+        The result is round((t1 * t2) + t3)
+
+        rm must be of RoundingMode sort, t1, t2, and t3 must have the same FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_fma', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_fma(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2, __in Z3_ast t3);
+   
+    /**
+        \brief Floating-point square root
+
+        \param c logical context
+        \param rm term of RoundingMode sort
+        \param t term of FloatingPoint sort
+
+        rm must be of RoundingMode sort, t must have FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_sqrt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_sqrt(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t);
+   
+    /**
+        \brief Floating-point remainder
+
+        \param c logical context
+        \param t1 term of FloatingPoint sort
+        \param t2 term of FloatingPoint sort
+
+        t1 and t2 must have the same FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_rem', AST, (_in(CONTEXT),_in(AST),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_rem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
+
+    /**
+        \brief Floating-point roundToIntegral. Rounds a floating-point number to 
+        the closest integer, again represented as a floating-point number.
+
+        \param c logical context
+        \param rm term of RoundingMode sort
+        \param t term of FloatingPoint sort
+
+        t must be of FloatingPoint sort.
+
+        def_API('Z3_mk_fpa_round_to_integral', AST, (_in(CONTEXT),_in(AST),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_round_to_integral(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t);
+
+    /**
+        \brief Minimum of floating-point numbers.
+
+        \param c logical context
+        \param t1 term of FloatingPoint sort
+        \param t2 term of FloatingPoint sort
+
+        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);
+
+        /**
+        \brief Maximum of floating-point numbers.
+
+        \param c logical context
+        \param t1 term of FloatingPoint sort
+        \param t2 term of FloatingPoint sort
+
+        t1, t2 must have the same FloatingPoint sort.
+
+        def_API('Z3_mk_fpa_max', AST, (_in(CONTEXT),_in(AST),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_max(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
+   
+     /**
+        \brief Floating-point less than or equal.
+
+        \param c logical context
+        \param t1 term of FloatingPoint sort
+        \param t2 term of FloatingPoint sort
+
+        t1 and t2 must have the same FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_leq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
+    */      
+    Z3_ast Z3_API Z3_mk_fpa_leq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
+
+     /**
+        \brief Floating-point less than.
+
+        \param c logical context
+        \param t1 term of FloatingPoint sort
+        \param t2 term of FloatingPoint sort
+
+        t1 and t2 must have the same FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_lt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
+    */      
+    Z3_ast Z3_API Z3_mk_fpa_lt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
+        
+    /**
+        \brief Floating-point greater than or equal.
+
+        \param c logical context
+        \param t1 term of FloatingPoint sort
+        \param t2 term of FloatingPoint sort
+
+        t1 and t2 must have the same FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_geq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
+    */      
+    Z3_ast Z3_API Z3_mk_fpa_geq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
+
+    /**
+        \brief Floating-point greater than.
+
+        \param c logical context
+        \param t1 term of FloatingPoint sort
+        \param t2 term of FloatingPoint sort
+
+        t1 and t2 must have the same FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_gt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
+    */      
+    Z3_ast Z3_API Z3_mk_fpa_gt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
+
+    /**
+        \brief Floating-point equality.
+
+        \param c logical context
+        \param t1 term of FloatingPoint sort
+        \param t2 term of FloatingPoint sort
+
+        Note that this is IEEE 754 equality (as opposed to SMT-LIB =).
+
+        t1 and t2 must have the same FloatingPoint sort.
+
+        def_API('Z3_mk_fpa_eq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_eq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
+   
+    /**
+        \brief Predicate indicating whether t is a normal floating-point number.
+
+        \param c logical context
+        \param t term of FloatingPoint sort
+
+        t must have FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_is_normal', AST, (_in(CONTEXT),_in(AST)))
+    */      
+    Z3_ast Z3_API Z3_mk_fpa_is_normal(__in Z3_context c, __in Z3_ast t);
+
+    /**
+        \brief Predicate indicating whether t is a subnormal floating-point number.
+
+        \param c logical context
+        \param t term of FloatingPoint sort
+
+        t must have FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_is_subnormal', AST, (_in(CONTEXT),_in(AST)))
+    */      
+    Z3_ast Z3_API Z3_mk_fpa_is_subnormal(__in Z3_context c, __in Z3_ast t);
+
+    /**
+        \brief Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.
+
+        \param c logical context
+        \param t term of FloatingPoint sort
+
+        t must have FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_is_zero', AST, (_in(CONTEXT),_in(AST)))
+    */      
+    Z3_ast Z3_API Z3_mk_fpa_is_zero(__in Z3_context c, __in Z3_ast t);
+
+   /**
+        \brief Predicate indicating whether t is a floating-point number representing +oo or -oo.
+
+        \param c logical context
+        \param t term of FloatingPoint sort
+
+        t must have FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_is_infinite', AST, (_in(CONTEXT),_in(AST)))
+    */      
+    Z3_ast Z3_API Z3_mk_fpa_is_infinite(__in Z3_context c, __in Z3_ast t);
+
+    /**
+        \brief Predicate indicating whether t is a NaN.
+
+        \param c logical context
+        \param t term of FloatingPoint sort
+
+        t must have FloatingPoint sort.
+     
+        def_API('Z3_mk_fpa_is_nan', AST, (_in(CONTEXT),_in(AST)))
+    */      
+    Z3_ast Z3_API Z3_mk_fpa_is_nan(__in Z3_context c, __in Z3_ast t);
+
+    /**
+        \brief Predicate indicating whether t is a negative floating-point number.
+
+        \param c logical context
+        \param t term of FloatingPoint sort
+
+        t must have FloatingPoint sort.
+
+        def_API('Z3_mk_fpa_is_negative', AST, (_in(CONTEXT),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_is_negative(__in Z3_context c, __in Z3_ast t);
+
+    /**
+        \brief Predicate indicating whether t is a positive floating-point number.
+
+        \param c logical context
+        \param t term of FloatingPoint sort
+
+        t must have FloatingPoint sort.
+
+        def_API('Z3_mk_fpa_is_positive', AST, (_in(CONTEXT),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_is_positive(__in Z3_context c, __in Z3_ast t);
+
+    /**
+        \brief Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
+
+        Produces a term that represents the conversion of a bit-vector term bv to a 
+        floating-point term of sort s.
+
+        \param c logical context
+        \param bv a bit-vector term
+        \param s floating-point sort
+
+        s must be a FloatingPoint sort, t must be of bit-vector sort, and the bit-vector 
+        size of bv must be equal to ebits+sbits of s. The format of the bit-vector is 
+        as defined by the IEEE 754-2008 interchange format.
+     
+        def_API('Z3_mk_fpa_to_fp_bv', AST, (_in(CONTEXT),_in(AST),_in(SORT)))
+    */      
+    Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(__in Z3_context c, __in Z3_ast bv, __in Z3_sort s);
+
+    /**
+        \brief Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
+        
+        Produces a term that represents the conversion of a floating-point term t to a
+        floating-point term of sort s. If necessary, the result will be rounded according
+        to rounding mode rm.
+
+        \param c logical context    
+        \param rm term of RoundingMode sort
+        \param t term of FloatingPoint sort
+        \param s floating-point sort
+
+        s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of floating-point sort.
+
+        def_API('Z3_mk_fpa_to_fp_float', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_to_fp_float(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s);
+
+    /**
+        \brief Conversion of a term of real sort into a term of FloatingPoint sort.
+
+        Produces a term that represents the conversion of term t of real sort into a
+        floating-point term of sort s. If necessary, the result will be rounded according
+        to rounding mode rm.
+
+        \param c logical context    
+        \param rm term of RoundingMode sort
+        \param t term of Real sort
+        \param s floating-point sort
+
+        s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of real sort.
+
+        def_API('Z3_mk_fpa_to_fp_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_to_fp_real(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s);
+
+    /**
+        \brief Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
+
+        Produces a term that represents the conversion of the bit-vector term t into a
+        floating-point term of sort s. The bit-vector t is taken to be in signed 
+        2's complement format. If necessary, the result will be rounded according
+        to rounding mode rm.
+
+        \param c logical context
+        \param rm term of RoundingMode sort
+        \param t term of bit-vector sort
+        \param s floating-point sort
+
+        s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of bit-vector sort.
+
+        def_API('Z3_mk_fpa_to_fp_signed', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s);
+
+    /**
+        \brief Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
+
+        Produces a term that represents the conversion of the bit-vector term t into a
+        floating-point term of sort s. The bit-vector t is taken to be in unsigned
+        2's complement format. If necessary, the result will be rounded according
+        to rounding mode rm.
+
+        \param c logical context
+        \param rm term of RoundingMode sort
+        \param t term of bit-vector sort
+        \param s floating-point sort
+
+        s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of bit-vector sort.
+
+        def_API('Z3_mk_fpa_to_fp_unsigned', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s);
+
+    /**
+        \brief Conversion of a floating-point term into an unsigned bit-vector.
+
+        Produces a term that represents the conversion of the floating-poiunt term t into a
+        bit-vector term of size sz in unsigned 2's complement format. If necessary, the result 
+		will be rounded according to rounding mode rm.
+
+        \param c logical context
+        \param rm term of RoundingMode sort
+        \param t term of FloatingPoint sort
+        \param sz size of the resulting bit-vector
+
+        def_API('Z3_mk_fpa_to_ubv', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(UINT)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_to_ubv(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in unsigned sz);
+
+    /**
+        \brief Conversion of a floating-point term into a signed bit-vector.
+
+        Produces a term that represents the conversion of the floating-poiunt term t into a
+        bit-vector term of size sz in signed 2's complement format. If necessary, the result 
+		will be rounded according to rounding mode rm.
+
+        \param c logical context
+        \param rm term of RoundingMode sort
+        \param t term of FloatingPoint sort
+        \param sz size of the resulting bit-vector
+
+        def_API('Z3_mk_fpa_to_sbv', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(UINT)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_to_sbv(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in unsigned sz);
+
+    /**
+        \brief Conversion of a floating-point term into a real-numbered term.
+
+        Produces a term that represents the conversion of the floating-poiunt term t into a
+        real number. Note that this type of conversion will often result in non-linear 
+        constraints over real terms.
+
+        \param c logical context        
+        \param t term of FloatingPoint sort
+
+        def_API('Z3_mk_fpa_to_real', AST, (_in(CONTEXT),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_to_real(__in Z3_context c, __in Z3_ast t);
+
+
+    /**
+        @name Z3-specific floating-point extensions
+    */
+    /*@{*/
+
+    /**
+        \brief Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.
+
+		\param c logical context
+        \param s FloatingPoint sort
+
+        def_API('Z3_fpa_get_ebits', UINT, (_in(CONTEXT),_in(SORT)))
+    */
+    unsigned Z3_API Z3_fpa_get_ebits(__in Z3_context c, __in Z3_sort s);
+
+    /**
+        \brief Retrieves the number of bits reserved for the significand in a FloatingPoint sort.
+
+		\param c logical context
+        \param s FloatingPoint sort
+
+        def_API('Z3_fpa_get_sbits', UINT, (_in(CONTEXT),_in(SORT)))
+    */
+    unsigned Z3_API Z3_fpa_get_sbits(__in Z3_context c, __in Z3_sort s);
+
+    /**
+        \brief Retrieves the sign of a floating-point literal.
+
+		\param c logical context
+        \param t a floating-point numeral
+		\param sgn sign
+
+        Remarks: sets \c sgn to 0 if the literal is NaN or positive and to 1 otherwise.
+
+        def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(INT)))
+    */
+    Z3_bool Z3_API Z3_fpa_get_numeral_sign(__in Z3_context c, __in Z3_ast t, __out int * sgn);
+
+    /**
+        \brief Return the significand value of a floating-point numeral as a string.
+
+		\param c logical context
+        \param t a floating-point numeral
+
+        Remarks: The significand s is always 0 < s < 2.0; the resulting string is long
+        enough to represent the real significand precisely.
+
+        def_API('Z3_fpa_get_numeral_significand_string', STRING, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t);
+
+    /**
+        \brief Return the exponent value of a floating-point numeral as a string
+
+		\param c logical context
+        \param t a floating-point numeral
+
+        def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t);
+
+    /**
+        \brief Return the exponent value of a floating-point numeral as a signed 64-bit integer
+
+        \param c logical context
+        \param t a floating-point numeral
+		\param n exponent
+
+        def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64)))
+    */
+    Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(__in Z3_context c, __in Z3_ast t, __out __int64 * n);
+
+    /**
+        \brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
+
+        \param c logical context
+        \param t term of FloatingPoint sort
+
+        t must have FloatingPoint sort. The size of the resulting bit-vector is automatically 
+        determined. 
+        
+        Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion 
+        knows only one NaN and it will always produce the same bit-vector represenatation of 
+        that NaN. 
+
+        def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(__in Z3_context c, __in Z3_ast t);
+
+    /**
+        \brief Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
+
+        Produces a term that represents the conversion of sig * 2^exp into a 
+        floating-point term of sort s. If necessary, the result will be rounded
+        according to rounding mode rm.
+
+        \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 s FloatingPoint sort
+
+        s must be a FloatingPoint sort, rm must be of RoundingMode sort, t 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)))
+    */
+    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);
+
+    /*@}*/
+
+    /*@}*/
+    /*@}*/
+
+#ifdef __cplusplus
+};
+#endif // __cplusplus
+
+#endif

src/api/z3_replayer.cpp

@@ -40,11 +40,12 @@ struct z3_replayer::imp {
     __int64                  m_int64;
     __uint64                 m_uint64;
     double                   m_double;
+    float                    m_float;
     size_t                   m_ptr;
     size_t_map<void *>       m_heap;
     svector<z3_replayer_cmd> m_cmds;
 
-    enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY };
+    enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY, FLOAT };
 
     struct value { 
         value_kind m_kind;
@@ -54,6 +55,7 @@ struct z3_replayer::imp {
             double       m_double;
             char const * m_str;
             void *       m_obj;
+            float        m_float;
         };
         value():m_kind(OBJECT), m_int(0) {}
         value(void * obj):m_kind(OBJECT), m_obj(obj) {}
@@ -61,6 +63,7 @@ struct z3_replayer::imp {
         value(value_kind k, __uint64 u):m_kind(k), m_uint(u) {}
         value(value_kind k, __int64 i):m_kind(k), m_int(i) {}
         value(value_kind k, double d):m_kind(k), m_double(d) {}
+        value(value_kind k, float f):m_kind(k), m_float(f) {}
     };
 
     svector<value>              m_args;
@@ -85,9 +88,12 @@ struct z3_replayer::imp {
         case UINT64:
             out << v.m_uint;
             break;
+        case FLOAT:
+            out << v.m_float;
+            break;
         case DOUBLE:
             out << v.m_double;
-            break;
+            break;        
         case STRING:
             out << v.m_str;
             break;
@@ -219,6 +225,26 @@ struct z3_replayer::imp {
         return curr() == '-' || curr() == '.' || ('0' <= curr() && curr() <= '9') || curr() == 'e' || curr() == 'E'; 
     }
 
+#if (!defined(strtof))
+    float strtof(const char * str, char ** end_ptr) {
+        // Note: This may introduce a double-rounding problem.
+        return (float)strtod(str, end_ptr);
+    }
+#endif
+
+    void read_float() {
+        m_string.reset();
+        while (is_double_char()) {
+            m_string.push_back(curr());
+            next();
+        }
+        if (m_string.empty())
+            throw z3_replayer_exception("invalid float");
+        m_string.push_back(0);
+        char * ptr;
+        m_float = strtof(m_string.begin(), &ptr);
+    }
+
     void read_double() {
         m_string.reset();
         while (is_double_char()) {
@@ -407,12 +433,18 @@ struct z3_replayer::imp {
                 TRACE("z3_replayer", tout << "[" << m_line << "] " << "U " << m_uint64 << "\n";);
                 m_args.push_back(value(UINT64, m_uint64));
                 break;
+            case 'F':
+                // push float
+                next(); skip_blank(); read_float();
+                TRACE("z3_replayer", tout << "[" << m_line << "] " << "F " << m_float << "\n";);
+                m_args.push_back(value(FLOAT, m_float));
+                break;
             case 'D':
                 // push double
                 next(); skip_blank(); read_double();
                 TRACE("z3_replayer", tout << "[" << m_line << "] " << "D " << m_double << "\n";);
                 m_args.push_back(value(DOUBLE, m_double));
-                break;
+                break;            
             case 'p':
             case 's':
             case 'u':
@@ -516,6 +548,12 @@ struct z3_replayer::imp {
         return m_args[pos].m_uint;
     }
 
+    float get_float(unsigned pos) const {
+        if (pos >= m_args.size() || m_args[pos].m_kind != FLOAT)
+            throw_invalid_reference();
+        return m_args[pos].m_float;
+    }
+
     double get_double(unsigned pos) const {
         if (pos >= m_args.size() || m_args[pos].m_kind != DOUBLE)
             throw_invalid_reference();
@@ -653,6 +691,10 @@ __uint64 z3_replayer::get_uint64(unsigned pos) const {
     return m_imp->get_uint64(pos);
 }
 
+float z3_replayer::get_float(unsigned pos) const {
+    return m_imp->get_float(pos);
+}
+
 double z3_replayer::get_double(unsigned pos) const {
     return m_imp->get_double(pos);
 }

src/api/z3_replayer.h

@@ -42,6 +42,7 @@ public:
     unsigned get_uint(unsigned pos) const;
     __int64 get_int64(unsigned pos) const;
     __uint64 get_uint64(unsigned pos) const;
+    float get_float(unsigned pos) const;
     double get_double(unsigned pos) const;
     bool get_bool(unsigned pos) const;
     Z3_string get_str(unsigned pos) const;