Add a floating-point support to c++ api.

src/api/c++/z3++.h

@@ -138,11 +138,22 @@ namespace z3 {
        \brief A Context manages all other Z3 objects, global configuration options, etc.
     */
     class context {
+    public:
+        enum class rounding_mode {
+            RNA,
+            RNE,
+            RTP,
+            RTN,
+            RTZ
+        };
+    private:
         bool       m_enable_exceptions;
+        rounding_mode m_rounding_mode;
         Z3_context m_ctx;
         void init(config & c) {
             m_ctx = Z3_mk_context_rc(c);
             m_enable_exceptions = true;
+            m_rounding_mode = rounding_mode::RNA;
             Z3_set_error_handler(m_ctx, 0);
             Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
         }
@@ -247,6 +258,26 @@ namespace z3 {
         */
         sort array_sort(sort d, sort r);
         sort array_sort(sort_vector const& d, sort r);
+        /**
+           \brief Return a floating point sort.
+           \c ebits is a number of exponent bits,
+           \c sbits	is a number of significand bits,
+           \pre where ebits must be larger than 1 and sbits must be larger than 2.
+         */
+        sort fpa_sort(unsigned ebits, unsigned sbits);
+        /**
+           \brief Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
+         */
+        template<size_t precision>
+        sort fpa_sort();
+        /**
+           \brief Return a RoundingMode sort.
+         */
+        sort fpa_rounding_mode();
+        /**
+           \breif Sets RoundingMode of FloatingPoints.
+         */
+        void set_rounding_mode(rounding_mode rm);
         /**
            \brief Return an enumeration sort: enum_names[0], ..., enum_names[n-1].
            \c cs and \c ts are output parameters. The method stores in \c cs the constants corresponding to the enumerated elements,
@@ -284,6 +315,10 @@ namespace z3 {
         expr int_const(char const * name);
         expr real_const(char const * name);
         expr bv_const(char const * name, unsigned sz);
+        expr fpa_const(char const * name, unsigned ebits, unsigned sbits);
+
+        template<size_t precision>
+        expr fpa_const(char const * name);
 
         expr bool_val(bool b);
 
@@ -307,6 +342,9 @@ namespace z3 {
         expr bv_val(char const * n, unsigned sz);
         expr bv_val(unsigned n, bool const* bits);
 
+        expr fpa_val(double n);
+        expr fpa_val(float n);
+
         expr string_val(char const* s);
         expr string_val(std::string const& s);
 
@@ -465,6 +503,7 @@ namespace z3 {
     public:
         sort(context & c):ast(c) {}
         sort(context & c, Z3_sort s):ast(c, reinterpret_cast<Z3_ast>(s)) {}
+        sort(context & c, Z3_ast a):ast(c, a) {}
         sort(sort const & s):ast(s) {}
         operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
         /**
@@ -523,6 +562,10 @@ namespace z3 {
             \brief Return true if this sort is a Finite domain sort.
         */
         bool is_finite_domain() const { return sort_kind() == Z3_FINITE_DOMAIN_SORT; }
+        /**
+            \brief Return true if this sort is a Floating point sort.
+        */
+        bool is_fpa() const { return sort_kind() == Z3_FLOATING_POINT_SORT; }
 
         /**
             \brief Return the size of this Bit-vector sort.
@@ -531,6 +574,9 @@ namespace z3 {
         */
         unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_error(); return r; }
 
+        unsigned fpa_ebits() const { assert(is_fpa()); unsigned r = Z3_fpa_get_ebits(ctx(), *this); check_error(); return r; }
+
+        unsigned fpa_sbits() const { assert(is_fpa()); unsigned r = Z3_fpa_get_sbits(ctx(), *this); check_error(); return r; }
         /**
             \brief Return the domain of this Array sort.
 
@@ -644,6 +690,10 @@ namespace z3 {
 
         */
         bool is_finite_domain() const { return get_sort().is_finite_domain(); }
+        /**
+            \brief Return true if this is a FloatingPoint expression. .
+        */
+        bool is_fpa() const { return get_sort().is_fpa(); }
 
         /**
            \brief Return true if this expression is a numeral.
@@ -803,6 +853,17 @@ namespace z3 {
 
         operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
 
+        /**
+           \brief Return a RoundingMode sort.
+         */
+        sort fpa_rounding_mode() {
+            assert(is_fpa());
+            Z3_sort s = ctx().fpa_rounding_mode();
+            check_error();
+            return sort(ctx(), s);
+        }
+
+
         /**
            \brief Return the declaration associated with this application.
            This method assumes the expression is an application.
@@ -992,15 +1053,26 @@ namespace z3 {
         friend expr nor(expr const& a, expr const& b);
         friend expr xnor(expr const& a, expr const& b);
 
+        friend expr min(expr const& a, expr const& b);
+        friend expr max(expr const& a, expr const& b);
+
         expr rotate_left(unsigned i) { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
         expr rotate_right(unsigned i) { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
         expr repeat(unsigned i) { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
 
+        friend expr abs(expr const & a);
+        friend expr sqrt(expr const & a, expr const & rm);
+
         friend expr operator~(expr const & a);
         expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
         unsigned lo() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }
         unsigned hi() const { assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
 
+        /**
+           \brief FloatingPoint fused multiply-add.
+          */
+        friend expr fma(expr const& a, expr const& b, expr const& c);
+
         /**
            \brief sequence and regular expression operations.
            + is overloaded as sequence concatenation and regular expression union.
@@ -1109,7 +1181,13 @@ namespace z3 {
     inline expr mod(expr const & a, int b) { return mod(a, a.ctx().num_val(b, a.get_sort())); }
     inline expr mod(int a, expr const & b) { return mod(b.ctx().num_val(a, b.get_sort()), b); }
 
-    inline expr rem(expr const& a, expr const& b) { _Z3_MK_BIN_(a, b, Z3_mk_rem);   }
+    inline expr rem(expr const& a, expr const& b) {
+        if (a.is_fpa() && b.is_fpa()) {
+            _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
+        } else {
+            _Z3_MK_BIN_(a, b, Z3_mk_rem);
+        }
+    }
     inline expr rem(expr const & a, int b) { return rem(a, a.ctx().num_val(b, a.get_sort())); }
     inline expr rem(int a, expr const & b) { return rem(b.ctx().num_val(a, b.get_sort()), b); }
 
@@ -1158,8 +1236,8 @@ namespace z3 {
         a.check_error();
         return expr(a.ctx(), r);
     }
-    inline expr operator==(expr const & a, int b) { assert(a.is_arith() || a.is_bv()); return a == a.ctx().num_val(b, a.get_sort()); }
+    inline expr operator==(expr const & a, int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a == a.ctx().num_val(b, a.get_sort()); }
-    inline expr operator==(int a, expr const & b) { assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) == b; }
+    inline expr operator==(int a, expr const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) == b; }
 
     inline expr operator!=(expr const & a, expr const & b) {
         check_context(a, b);
@@ -1168,8 +1246,8 @@ namespace z3 {
         a.check_error();
         return expr(a.ctx(), r);
     }
-    inline expr operator!=(expr const & a, int b) { assert(a.is_arith() || a.is_bv()); return a != a.ctx().num_val(b, a.get_sort()); }
+    inline expr operator!=(expr const & a, int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a != a.ctx().num_val(b, a.get_sort()); }
-    inline expr operator!=(int a, expr const & b) { assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) != b; }
+    inline expr operator!=(int a, expr const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) != b; }
 
     inline expr operator+(expr const & a, expr const & b) {
         check_context(a, b);
@@ -1188,6 +1266,9 @@ namespace z3 {
             Z3_ast _args[2] = { a, b };
             r = Z3_mk_re_union(a.ctx(), 2, _args);
         }
+        else if (a.is_fpa() && b.is_fpa()) {
+            r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
+        }
         else {
             // operator is not supported by given arguments.
             assert(false);
@@ -1208,6 +1289,9 @@ namespace z3 {
         else if (a.is_bv() && b.is_bv()) {
             r = Z3_mk_bvmul(a.ctx(), a, b);
         }
+        else if (a.is_fpa() && b.is_fpa()) {
+            r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
+        }
         else {
             // operator is not supported by given arguments.
             assert(false);
@@ -1245,6 +1329,9 @@ namespace z3 {
         else if (a.is_bv() && b.is_bv()) {
             r = Z3_mk_bvsdiv(a.ctx(), a, b);
         }
+        else if (a.is_fpa() && b.is_fpa()) {
+            r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
+        }
         else {
             // operator is not supported by given arguments.
             assert(false);
@@ -1263,6 +1350,9 @@ namespace z3 {
         else if (a.is_bv()) {
             r = Z3_mk_bvneg(a.ctx(), a);
         }
+        else if (a.is_fpa()) {
+            r = Z3_mk_fpa_neg(a.ctx(), a);
+        }
         else {
             // operator is not supported by given arguments.
             assert(false);
@@ -1281,6 +1371,9 @@ namespace z3 {
         else if (a.is_bv() && b.is_bv()) {
             r = Z3_mk_bvsub(a.ctx(), a, b);
         }
+        else if (a.is_fpa() && b.is_fpa()) {
+            r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
+        }
         else {
             // operator is not supported by given arguments.
             assert(false);
@@ -1300,6 +1393,9 @@ namespace z3 {
         else if (a.is_bv() && b.is_bv()) {
             r = Z3_mk_bvsle(a.ctx(), a, b);
         }
+        else if (a.is_fpa() && b.is_fpa()) {
+            r = Z3_mk_fpa_leq(a.ctx(), a, b);
+        }
         else {
             // operator is not supported by given arguments.
             assert(false);
@@ -1322,6 +1418,9 @@ namespace z3 {
         else if (a.is_bv() && b.is_bv()) {
             r = Z3_mk_bvslt(a.ctx(), a, b);
         }
+        else if (a.is_fpa() && b.is_fpa()) {
+            r = Z3_mk_fpa_lt(a.ctx(), a, b);
+        }
         else {
             // operator is not supported by given arguments.
             assert(false);
@@ -1341,6 +1440,9 @@ namespace z3 {
         else if (a.is_bv() && b.is_bv()) {
             r = Z3_mk_bvsgt(a.ctx(), a, b);
         }
+        else if (a.is_fpa() && b.is_fpa()) {
+            r = Z3_mk_fpa_gt(a.ctx(), a, b);
+        }
         else {
             // operator is not supported by given arguments.
             assert(false);
@@ -1366,17 +1468,30 @@ namespace z3 {
     inline expr nand(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }
     inline expr nor(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }
     inline expr xnor(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
-
+    inline expr min(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_fpa_min(a.ctx(), a, b); return expr(a.ctx(), r); }
+    inline expr max(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_fpa_max(a.ctx(), a, b); return expr(a.ctx(), r); }
+    inline expr abs(expr const & a) { Z3_ast r = Z3_mk_fpa_abs(a.ctx(), a); return expr(a.ctx(), r); }
+    inline expr sqrt(expr const & a, expr const& rm) {
+        check_context(a, rm);
+        assert(a.is_fpa());
+        Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
+        return expr(a.ctx(), r);
+    }
     inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
 
-
+    inline expr fma(expr const& a, expr const& b, expr const& c, expr const& rm) {
+        check_context(a, b); check_context(a, c); check_context(a, rm);
+        assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
+        Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
+        a.check_error();
+        return expr(a.ctx(), r);
+    }
 
     /**
        \brief Create the if-then-else expression <tt>ite(c, t, e)</tt>
 
        \pre c.is_bool()
     */
-
     inline expr ite(expr const & c, expr const & t, expr const & e) {
         check_context(c, t); check_context(c, e);
         assert(c.is_bool());
@@ -2562,6 +2677,31 @@ namespace z3 {
     inline sort context::string_sort() { Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }
     inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
     inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
+    inline sort context::fpa_sort(unsigned ebits, unsigned sbits) { Z3_sort s = Z3_mk_fpa_sort(m_ctx, ebits, sbits); check_error(); return sort(*this, s); }
+
+    template<>
+    inline sort context::fpa_sort<16>() { return fpa_sort(5, 11); }
+
+    template<>
+    inline sort context::fpa_sort<32>() { return fpa_sort(8, 24); }
+
+    template<>
+    inline sort context::fpa_sort<64>() { return fpa_sort(11, 53); }
+
+    template<>
+    inline sort context::fpa_sort<128>() { return fpa_sort(15, 113); }
+
+    inline sort context::fpa_rounding_mode() {
+        switch (m_rounding_mode) {
+            case rounding_mode::RNA: return sort(*this, Z3_mk_fpa_rna(m_ctx));
+            case rounding_mode::RNE: return sort(*this, Z3_mk_fpa_rne(m_ctx));
+            case rounding_mode::RTP: return sort(*this, Z3_mk_fpa_rtp(m_ctx));
+            case rounding_mode::RTN: return sort(*this, Z3_mk_fpa_rtn(m_ctx));
+            case rounding_mode::RTZ: return sort(*this, Z3_mk_fpa_rtz(m_ctx));
+        }
+    }
+
+    inline void context::set_rounding_mode(rounding_mode rm) { m_rounding_mode = rm; }
 
     inline sort context::array_sort(sort d, sort r) { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }
     inline sort context::array_sort(sort_vector const& d, sort r) {
@@ -2681,6 +2821,10 @@ namespace z3 {
     inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
     inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
     inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
+    inline expr context::fpa_const(char const * name, unsigned ebits, unsigned sbits) { return constant(name, fpa_sort(ebits, sbits)); }
+
+    template<size_t precision>
+    inline expr context::fpa_const(char const * name) { return constant(name, fpa_sort<precision>()); }
 
     inline expr context::bool_val(bool b) { return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }
 
@@ -2708,6 +2852,9 @@ namespace z3 {
         Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
     }
 
+    inline expr context::fpa_val(double n) { sort s = fpa_sort<64>(); Z3_ast r = Z3_mk_fpa_numeral_double(m_ctx, n, s); check_error(); return expr(*this, r); }
+    inline expr context::fpa_val(float n) { sort s = fpa_sort<32>(); Z3_ast r = Z3_mk_fpa_numeral_float(m_ctx, n, s); check_error(); return expr(*this, r); }
+
     inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }
     inline expr context::string_val(std::string const& s) { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }