Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api

src/ast/float_decl_plugin.cpp

@@ -256,6 +256,9 @@ func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_param
     case OP_FLOAT_IS_NZERO: name = "isNZero";   break;
     case OP_FLOAT_IS_PZERO: name = "isPZero";   break;        
     case OP_FLOAT_IS_SIGN_MINUS: name = "isSignMinus";  break;
+    case OP_FLOAT_IS_INF: name = "isInfinite";  break;
+    case OP_FLOAT_IS_NORMAL: name = "isNormal";  break;
+    case OP_FLOAT_IS_SUBNORMAL: name = "isSubnormal";  break;
     default:
         UNREACHABLE();
         break;
@@ -415,6 +418,9 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
     case OP_FLOAT_IS_NZERO:
     case OP_FLOAT_IS_PZERO:
     case OP_FLOAT_IS_SIGN_MINUS: 
+    case OP_FLOAT_IS_INF:
+    case OP_FLOAT_IS_NORMAL:
+    case OP_FLOAT_IS_SUBNORMAL:
         return mk_unary_rel_decl(k, num_parameters, parameters, arity, domain, range);
     case OP_FLOAT_ABS: 
     case OP_FLOAT_UMINUS:
@@ -473,9 +479,12 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
     op_names.push_back(builtin_name("<=", OP_FLOAT_LE));
     op_names.push_back(builtin_name(">=", OP_FLOAT_GE));
 
+    op_names.push_back(builtin_name("isInfinite", OP_FLOAT_IS_INF));
     op_names.push_back(builtin_name("isZero", OP_FLOAT_IS_ZERO));
     op_names.push_back(builtin_name("isNZero", OP_FLOAT_IS_NZERO));
     op_names.push_back(builtin_name("isPZero", OP_FLOAT_IS_PZERO));
+    op_names.push_back(builtin_name("isNormal", OP_FLOAT_IS_NORMAL));
+    op_names.push_back(builtin_name("isSubnormal", OP_FLOAT_IS_SUBNORMAL));
     op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_SIGN_MINUS));
 
     op_names.push_back(builtin_name("min", OP_FLOAT_MIN));

src/ast/float_decl_plugin.h

@@ -61,9 +61,12 @@ enum float_op_kind {
     OP_FLOAT_GT,
     OP_FLOAT_LE,
     OP_FLOAT_GE,
+    OP_FLOAT_IS_INF,
     OP_FLOAT_IS_ZERO,
-    OP_FLOAT_IS_NZERO,
+    OP_FLOAT_IS_NORMAL,
+    OP_FLOAT_IS_SUBNORMAL,    
     OP_FLOAT_IS_PZERO,
+    OP_FLOAT_IS_NZERO,
     OP_FLOAT_IS_SIGN_MINUS,
 
     OP_TO_FLOAT,
@@ -237,7 +240,10 @@ public:
     app * mk_le(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_LE, arg1, arg2); }
     app * mk_ge(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_GE, arg1, arg2); }
 
+    app * mk_is_inf(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_INF, arg1); }
     app * mk_is_zero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_ZERO, arg1); }
+    app * mk_is_normal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NORMAL, arg1); }
+    app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SUBNORMAL, arg1); }
     app * mk_is_nzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NZERO, arg1); }
     app * mk_is_pzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_PZERO, arg1); }
     app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SIGN_MINUS, arg1); }

src/ast/rewriter/float_rewriter.cpp

@@ -58,6 +58,9 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
     case OP_FLOAT_IS_ZERO:   SASSERT(num_args == 1); st = mk_is_zero(args[0], result); break;
     case OP_FLOAT_IS_NZERO:  SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break;
     case OP_FLOAT_IS_PZERO:  SASSERT(num_args == 1); st = mk_is_pzero(args[0], result); break;
+    case OP_FLOAT_IS_INF:    SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break;
+    case OP_FLOAT_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break;
+    case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break;
     case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break;
     case OP_TO_IEEE_BV:      SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break;
     }
@@ -428,6 +431,36 @@ br_status float_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) {
     return BR_FAILED;
 }
 
+br_status float_rewriter::mk_is_inf(expr * arg1, expr_ref & result) {
+    scoped_mpf v(m_util.fm());
+    if (m_util.is_value(arg1, v)) {
+        result = (m_util.fm().is_inf(v)) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_is_normal(expr * arg1, expr_ref & result) {
+    scoped_mpf v(m_util.fm());
+    if (m_util.is_value(arg1, v)) {
+        result = (m_util.fm().is_normal(v)) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) {
+    scoped_mpf v(m_util.fm());
+    if (m_util.is_value(arg1, v)) {
+        result = (m_util.fm().is_denormal(v)) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
 br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) {
     scoped_mpf v(m_util.fm());
     if (m_util.is_value(arg1, v)) {

src/ast/rewriter/float_rewriter.h

@@ -66,6 +66,9 @@ public:
     br_status mk_is_zero(expr * arg1, expr_ref & result);
     br_status mk_is_nzero(expr * arg1, expr_ref & result);
     br_status mk_is_pzero(expr * arg1, expr_ref & result);
+    br_status mk_is_inf(expr * arg1, expr_ref & result);
+    br_status mk_is_normal(expr * arg1, expr_ref & result);
+    br_status mk_is_subnormal(expr * arg1, expr_ref & result);
     br_status mk_is_sign_minus(expr * arg1, expr_ref & result);
 
     br_status mk_to_ieee_bv(expr * arg1, expr_ref & result);

src/tactic/fpa/fpa2bv_converter.cpp

@@ -1621,6 +1621,21 @@ void fpa2bv_converter::mk_is_pzero(func_decl * f, unsigned num, expr * const * a
     m_simp.mk_and(a0_is_pos, a0_is_zero, result);
 }
 
+void fpa2bv_converter::mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 1);
+    mk_is_inf(args[0], result);
+}
+
+void fpa2bv_converter::mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 1);
+    mk_is_normal(args[0], result);
+}
+
+void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 1);
+    mk_is_denormal(args[0], result);
+}
+
 void fpa2bv_converter::mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 1);
     mk_is_neg(args[0], result);

src/tactic/fpa/fpa2bv_converter.h

@@ -116,6 +116,9 @@ public:
     void mk_is_nzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_is_pzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
 
     void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);    

src/tactic/fpa/fpa2bv_rewriter.h

@@ -132,6 +132,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
             case OP_FLOAT_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
             case OP_FLOAT_IS_NZERO: m_conv.mk_is_nzero(f, num, args, result); return BR_DONE;
             case OP_FLOAT_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE;
             case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE;
             case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE;
             case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;