Simplify RCF C API. Add Z3_rcf_mk_roots (C API) and MkRoots (Python API). Implement basic root isolation support.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/api/api_rcf.cpp

@@ -23,29 +23,10 @@ Notes:
 #include"z3.h"
 #include"api_log_macros.h"
 #include"api_context.h"
-#include"api_rcf.h"
+#include"realclosure.h"
 
 extern "C" {
 
-    void Z3_API Z3_rcf_inc_ref(Z3_context c, Z3_rcf_num a) {
-        Z3_TRY;
-        LOG_Z3_rcf_inc_ref(c, a);
-        RESET_ERROR_CODE();
-        to_rcf_num(a)->inc_ref();
-        Z3_CATCH;
-    }
-
-    void Z3_API Z3_rcf_dec_ref(Z3_context c, Z3_rcf_num a) {
-        Z3_TRY;
-        LOG_Z3_rcf_dec_ref(c, a);
-        RESET_ERROR_CODE();
-        if (to_rcf_num(a)->ref_count() == 1) {
-            mk_c(c)->rcfm().del(to_rcnumeral(a));
-        }
-        to_rcf_num(a)->dec_ref();
-        Z3_CATCH;
-    }
-
     static rcmanager & rcfm(Z3_context c) {
         return mk_c(c)->rcfm();
     }
@@ -53,14 +34,24 @@ extern "C" {
     static void reset_rcf_cancel(Z3_context c) {
         rcfm(c).reset_cancel();
     }
-    
+
-    static Z3_rcf_num mk_rcf_num(Z3_context c, rcnumeral & a) {
+    static rcnumeral to_rcnumeral(Z3_rcf_num a) { 
-        Z3_rcf_num_ref * r = alloc(Z3_rcf_num_ref);
+        return rcnumeral::mk(a); 
-        rcfm(c).swap(r->m_num, a);
-        mk_c(c)->save_object(r);
-        return of_rcf_num(r);
     }
-    
+
+    static Z3_rcf_num from_rcnumeral(rcnumeral a) { 
+        return reinterpret_cast<Z3_rcf_num>(a.c_ptr()); 
+    }
+
+    void Z3_API Z3_rcf_del(Z3_context c, Z3_rcf_num a) {
+        Z3_TRY;
+        LOG_Z3_rcf_del(c, a);
+        RESET_ERROR_CODE();
+        rcnumeral _a = to_rcnumeral(a);
+        rcfm(c).del(_a);
+        Z3_CATCH;
+    }
+
     Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val) {
         Z3_TRY;
         LOG_Z3_rcf_mk_rational(c, val);
@@ -68,9 +59,9 @@ extern "C" {
         reset_rcf_cancel(c);
         scoped_mpq q(rcfm(c).qm());
         rcfm(c).qm().set(q, val);
-        scoped_rcnumeral r(rcfm(c));
+        rcnumeral r;
         rcfm(c).set(r, q);
-        RETURN_Z3(mk_rcf_num(c, r));
+        RETURN_Z3(from_rcnumeral(r));
         Z3_CATCH_RETURN(0);
     }
 
@@ -79,9 +70,9 @@ extern "C" {
         LOG_Z3_rcf_mk_small_int(c, val);
         RESET_ERROR_CODE();
         reset_rcf_cancel(c);
-        scoped_rcnumeral r(rcfm(c));
+        rcnumeral r;
         rcfm(c).set(r, val);
-        RETURN_Z3(mk_rcf_num(c, r));
+        RETURN_Z3(from_rcnumeral(r));
         Z3_CATCH_RETURN(0);
     }
 
@@ -90,9 +81,9 @@ extern "C" {
         LOG_Z3_rcf_mk_pi(c);
         RESET_ERROR_CODE();
         reset_rcf_cancel(c);
-        scoped_rcnumeral r(rcfm(c));
+        rcnumeral r;
         rcfm(c).mk_pi(r);
-        RETURN_Z3(mk_rcf_num(c, r));
+        RETURN_Z3(from_rcnumeral(r));
         Z3_CATCH_RETURN(0);
     }
 
@@ -101,9 +92,9 @@ extern "C" {
         LOG_Z3_rcf_mk_e(c);
         RESET_ERROR_CODE();
         reset_rcf_cancel(c);
-        scoped_rcnumeral r(rcfm(c));
+        rcnumeral r;
         rcfm(c).mk_e(r);
-        RETURN_Z3(mk_rcf_num(c, r));
+        RETURN_Z3(from_rcnumeral(r));
         Z3_CATCH_RETURN(0);
     }
 
@@ -112,9 +103,37 @@ extern "C" {
         LOG_Z3_rcf_mk_infinitesimal(c, name);
         RESET_ERROR_CODE();
         reset_rcf_cancel(c);
-        scoped_rcnumeral r(rcfm(c));
+        rcnumeral r;
         rcfm(c).mk_infinitesimal(name, r);
-        RETURN_Z3(mk_rcf_num(c, r));
+        RETURN_Z3(from_rcnumeral(r));
+        Z3_CATCH_RETURN(0);
+    }
+
+    unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]) {
+        Z3_TRY;
+        LOG_Z3_rcf_mk_roots(c, n, a, roots);
+        RESET_ERROR_CODE();
+        reset_rcf_cancel(c);
+        rcnumeral_vector av;
+        unsigned rz = 0;
+        for (unsigned i = 0; i < n; i++) {
+            if (!rcfm(c).is_zero(to_rcnumeral(a[i])))
+                rz = i + 1;
+            av.push_back(to_rcnumeral(a[i]));
+        }
+        if (rz == 0) {
+            // it is the zero polynomial
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        av.shrink(rz);
+        rcnumeral_vector rs;
+        rcfm(c).isolate_roots(av.size(), av.c_ptr(), rs);
+        unsigned num_roots = rs.size();
+        for (unsigned i = 0; i < num_roots; i++) {
+            roots[i] = from_rcnumeral(rs[i]);
+        }
+        return num_roots;
         Z3_CATCH_RETURN(0);
     }
 
@@ -123,9 +142,9 @@ extern "C" {
         LOG_Z3_rcf_add(c, a, b);
         RESET_ERROR_CODE();
         reset_rcf_cancel(c);
-        scoped_rcnumeral r(rcfm(c));
+        rcnumeral r;
         rcfm(c).add(to_rcnumeral(a), to_rcnumeral(b), r);
-        RETURN_Z3(mk_rcf_num(c, r));
+        RETURN_Z3(from_rcnumeral(r));
         Z3_CATCH_RETURN(0);
     }
 
@@ -134,9 +153,9 @@ extern "C" {
         LOG_Z3_rcf_sub(c, a, b);
         RESET_ERROR_CODE();
         reset_rcf_cancel(c);
-        scoped_rcnumeral r(rcfm(c));
+        rcnumeral r;
         rcfm(c).sub(to_rcnumeral(a), to_rcnumeral(b), r);
-        RETURN_Z3(mk_rcf_num(c, r));
+        RETURN_Z3(from_rcnumeral(r));
         Z3_CATCH_RETURN(0);
     }
 
@@ -145,9 +164,9 @@ extern "C" {
         LOG_Z3_rcf_mul(c, a, b);
         RESET_ERROR_CODE();
         reset_rcf_cancel(c);
-        scoped_rcnumeral r(rcfm(c));
+        rcnumeral r;
         rcfm(c).mul(to_rcnumeral(a), to_rcnumeral(b), r);
-        RETURN_Z3(mk_rcf_num(c, r));
+        RETURN_Z3(from_rcnumeral(r));
         Z3_CATCH_RETURN(0);
     }
 
@@ -156,9 +175,9 @@ extern "C" {
         LOG_Z3_rcf_div(c, a, b);
         RESET_ERROR_CODE();
         reset_rcf_cancel(c);
-        scoped_rcnumeral r(rcfm(c));
+        rcnumeral r;
         rcfm(c).div(to_rcnumeral(a), to_rcnumeral(b), r);
-        RETURN_Z3(mk_rcf_num(c, r));
+        RETURN_Z3(from_rcnumeral(r));
         Z3_CATCH_RETURN(0);
     }
     
@@ -167,9 +186,9 @@ extern "C" {
         LOG_Z3_rcf_neg(c, a);
         RESET_ERROR_CODE();
         reset_rcf_cancel(c);
-        scoped_rcnumeral r(rcfm(c));
+        rcnumeral r;
         rcfm(c).neg(to_rcnumeral(a), r);
-        RETURN_Z3(mk_rcf_num(c, r));
+        RETURN_Z3(from_rcnumeral(r));
         Z3_CATCH_RETURN(0);
     }
 
@@ -178,9 +197,9 @@ extern "C" {
         LOG_Z3_rcf_inv(c, a);
         RESET_ERROR_CODE();
         reset_rcf_cancel(c);
-        scoped_rcnumeral r(rcfm(c));
+        rcnumeral r;
         rcfm(c).inv(to_rcnumeral(a), r);
-        RETURN_Z3(mk_rcf_num(c, r));
+        RETURN_Z3(from_rcnumeral(r));
         Z3_CATCH_RETURN(0);
     }
 

src/api/api_rcf.h

@@ -1,38 +0,0 @@
-/*++
-Copyright (c) 2013 Microsoft Corporation
-
-Module Name:
-
-    api_rcf.h
-
-Abstract:
-
-    Additional APIs for handling elements of the Z3 real closed field that contains:
-       - transcendental extensions
-       - infinitesimal extensions
-       - algebraic extensions
-
-Author:
-
-    Leonardo de Moura (leonardo) 2012-01-05
-
-Notes:
-    
---*/
-#ifndef _API_RCF_H_
-#define _API_RCF_H_
-
-#include"api_util.h"
-#include"realclosure.h"
-
-struct Z3_rcf_num_ref : public api::object {
-    rcnumeral m_num;
-    virtual ~Z3_rcf_num_ref() {}
-};
-
-
-inline Z3_rcf_num_ref * to_rcf_num(Z3_rcf_num n) { return reinterpret_cast<Z3_rcf_num_ref *>(n); }
-inline Z3_rcf_num of_rcf_num(Z3_rcf_num_ref * n) { return reinterpret_cast<Z3_rcf_num>(n); }
-inline rcnumeral & to_rcnumeral(Z3_rcf_num n) { SASSERT(n != 0); return to_rcf_num(n)->m_num; }
-
-#endif

src/api/python/z3rcf.py

@@ -32,6 +32,22 @@ def MkInfinitesimal(name="eps", ctx=None):
     ctx = z3._get_ctx(ctx)
     return RCFNum(Z3_rcf_mk_infinitesimal(ctx.ref(), name), ctx)
 
+def MkRoots(p, ctx=None):
+    ctx = z3._get_ctx(ctx)
+    num = len(p)
+    _tmp = [] 
+    _as  = (RCFNumObj * num)()
+    _rs  = (RCFNumObj * num)() 
+    for i in range(num):
+        _a = _to_rcfnum(p[i], ctx)
+        _tmp.append(_a) # prevent GC
+        _as[i] = _a.num
+    nr = Z3_rcf_mk_roots(ctx.ref(), num, _as, _rs)
+    r  = []
+    for i in range(nr):
+        r.append(RCFNum(_rs[i], ctx))
+    return r
+
 class RCFNum:
     def __init__(self, num, ctx=None):
         # TODO: add support for converting AST numeral values into RCFNum
@@ -41,10 +57,9 @@ class RCFNum:
         else:
             self.ctx = z3._get_ctx(ctx)
             self.num = Z3_rcf_mk_rational(self.ctx_ref(), str(num))
-        Z3_rcf_inc_ref(self.ctx_ref(), self.num)
 
     def __del__(self):
-        Z3_rcf_dec_ref(self.ctx_ref(), self.num)
+        Z3_rcf_del(self.ctx_ref(), self.num)
 
     def ctx_ref(self):
         return self.ctx.ref()
@@ -53,28 +68,36 @@ class RCFNum:
         return Z3_rcf_num_to_string(self.ctx_ref(), self.num)
 
     def __add__(self, other):
-        return RCFNum(Z3_rcf_add(self.ctx_ref(), self.num, _to_rcfnum(other, self.ctx).num), self.ctx)
+        v = _to_rcfnum(other, self.ctx)
+        return RCFNum(Z3_rcf_add(self.ctx_ref(), self.num, v.num), self.ctx)
 
     def __radd__(self, other):
-        return RCFNum(Z3_rcf_add(self.ctx_ref(), _to_rcfnum(other, self.ctx).num, self.num), self.ctx)
+        v = _to_rcfnum(other, self.ctx)
+        return RCFNum(Z3_rcf_add(self.ctx_ref(), v.num, self.num), self.ctx)
 
     def __mul__(self, other):
-        return RCFNum(Z3_rcf_mul(self.ctx_ref(), self.num, _to_rcfnum(other, self.ctx).num), self.ctx)
+        v = _to_rcfnum(other, self.ctx)
+        return RCFNum(Z3_rcf_mul(self.ctx_ref(), self.num, v.num), self.ctx)
 
     def __rmul__(self, other):
-        return RCFNum(Z3_rcf_mul(self.ctx_ref(), _to_rcfnum(other, self.ctx).num, self.num), self.ctx)
+        v = _to_rcfnum(other, self.ctx)
+        return RCFNum(Z3_rcf_mul(self.ctx_ref(), v.num, self.num), self.ctx)
 
     def __sub__(self, other):
-        return RCFNum(Z3_rcf_sub(self.ctx_ref(), self.num, _to_rcfnum(other, self.ctx).num), self.ctx)
+        v = _to_rcfnum(other, self.ctx)
+        return RCFNum(Z3_rcf_sub(self.ctx_ref(), self.num, v.num), self.ctx)
 
     def __rsub__(self, other):
-        return RCFNum(Z3_rcf_sub(self.ctx_ref(), _to_rcfnum(other, self.ctx).num, self.num), self.ctx)
+        v = _to_rcfnum(other, self.ctx)
+        return RCFNum(Z3_rcf_sub(self.ctx_ref(), v.num, self.num), self.ctx)
 
     def __div__(self, other):
-        return RCFNum(Z3_rcf_div(self.ctx_ref(), self.num, _to_rcfnum(other, self.ctx).num), self.ctx)
+        v = _to_rcfnum(other, self.ctx)
+        return RCFNum(Z3_rcf_div(self.ctx_ref(), self.num, v.num), self.ctx)
 
     def __rdiv__(self, other):
-        return RCFNum(Z3_rcf_div(self.ctx_ref(), _to_rcfnum(other, self.ctx).num, self.num), self.ctx)
+        v = _to_rcfnum(other, self.ctx)
+        return RCFNum(Z3_rcf_div(self.ctx_ref(), v.num, self.num), self.ctx)
 
     def __neg__(self):
         return self.__rsub__(0)
@@ -83,32 +106,42 @@ class RCFNum:
         return Z3_rcf_num_to_decimal_string(self.ctx_ref(), self.num, prec)
     
     def __lt__(self, other):
-        return Z3_rcf_lt(self.ctx_ref(), self.num, _to_rcfnum(other, self.ctx).num)
+        v = _to_rcfnum(other, self.ctx)
+        return Z3_rcf_lt(self.ctx_ref(), self.num, v.num)
 
     def __rlt__(self, other):
-        return Z3_rcf_lt(self.ctx_ref(), _to_rcfnum(other, self.ctx).num, self.num)
+        v = _to_rcfnum(other, self.ctx)
+        return Z3_rcf_lt(self.ctx_ref(), v.num, self.num)
 
     def __gt__(self, other):
-        return Z3_rcf_gt(self.ctx_ref(), self.num, _to_rcfnum(other, self.ctx).num)
+        v = _to_rcfnum(other, self.ctx)
+        return Z3_rcf_gt(self.ctx_ref(), self.num, v.num)
 
     def __rgt__(self, other):
-        return Z3_rcf_gt(self.ctx_ref(), _to_rcfnum(other, self.ctx).num, self.num)
+        v = _to_rcfnum(other, self.ctx)
+        return Z3_rcf_gt(self.ctx_ref(), v.num, self.num)
 
     def __le__(self, other):
-        return Z3_rcf_le(self.ctx_ref(), self.num, _to_rcfnum(other, self.ctx).num)
+        v = _to_rcfnum(other, self.ctx)
+        return Z3_rcf_le(self.ctx_ref(), self.num, v.num)
 
     def __rle__(self, other):
-        return Z3_rcf_le(self.ctx_ref(), _to_rcfnum(other, self.ctx).num, self.num)
+        v = _to_rcfnum(other, self.ctx)
+        return Z3_rcf_le(self.ctx_ref(), v.num, self.num)
 
     def __ge__(self, other):
-        return Z3_rcf_ge(self.ctx_ref(), self.num, _to_rcfnum(other, self.ctx).num)
+        v = _to_rcfnum(other, self.ctx)
+        return Z3_rcf_ge(self.ctx_ref(), self.num, v.num)
 
     def __rge__(self, other):
-        return Z3_rcf_ge(self.ctx_ref(), _to_rcfnum(other, self.ctx).num, self.num)
+        v = _to_rcfnum(other, self.ctx)
+        return Z3_rcf_ge(self.ctx_ref(), v.num, self.num)
 
     def __eq__(self, other):
-        return Z3_rcf_eq(self.ctx_ref(), self.num, _to_rcfnum(other, self.ctx).num)
+        v = _to_rcfnum(other, self.ctx)
+        return Z3_rcf_eq(self.ctx_ref(), self.num, v.num)
 
     def __ne__(self, other):
-        return Z3_rcf_neq(self.ctx_ref(), self.num, _to_rcfnum(other, self.ctx).num)
+        v = _to_rcfnum(other, self.ctx)
+        return Z3_rcf_neq(self.ctx_ref(), self.num, v.num)
 

src/api/z3_rcf.h

@@ -27,18 +27,11 @@ extern "C" {
 #endif // __cplusplus
 
     /**
-       \brief Increment the reference counter of a RCF numeral.
+       \brief Delete a RCF numeral created using the RCF API.
-    
-       def_API('Z3_rcf_inc_ref', VOID, (_in(CONTEXT), _in(RCF_NUM)))
-    */
-    void Z3_API Z3_rcf_inc_ref(__in Z3_context c, __in Z3_rcf_num a);
 
-    /**
+       def_API('Z3_rcf_del', VOID, (_in(CONTEXT), _in(RCF_NUM)))
-       \brief Decrement the reference counter of a RCF numeral.
-
-       def_API('Z3_rcf_dec_ref', VOID, (_in(CONTEXT), _in(RCF_NUM)))
     */
-    void Z3_API Z3_rcf_dec_ref(__in Z3_context c, __in Z3_rcf_num a);
+    void Z3_API Z3_rcf_del(__in Z3_context c, __in Z3_rcf_num a);
 
     /**
        \brief Return a RCF rational using the given string.
@@ -75,6 +68,17 @@ extern "C" {
     */
     Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(__in Z3_context c, __in Z3_string name);
 
+    /**
+       \brief Store in roots the roots of the polynomial <tt>a[n-1]*x^{n-1} + ... + a[0]</tt>.
+       The output vector \c roots must have size \c n. 
+       It returns the number of roots of the polynomial.
+
+       \pre The input polynomial is not the zero polynomial. 
+
+       def_API('Z3_rcf_mk_roots', UINT, (_in(CONTEXT), _in(UINT), _in_array(1, RCF_NUM), _out_array(1, RCF_NUM)))
+    */
+    unsigned Z3_API Z3_rcf_mk_roots(__in Z3_context c, __in unsigned n, __in_ecount(n) Z3_rcf_num const a[], __out_ecount(n) Z3_rcf_num roots[]);
+
     /**
        \brief Return the value a + b. 
 

src/math/realclosure/realclosure.cpp

@@ -1082,10 +1082,86 @@ namespace realclosure {
             }
         }
 
-        void isolate_roots(unsigned n, numeral const * as, numeral_vector & roots) {
+        /**
+           \brief Root isolation for polynomials that are
+                   - nonlinear (degree > 2)
+                   - zero is not a root
+                   - square free
+                   - nonconstant
+        */
+        void nl_nz_sqf_isolate_roots(unsigned n, value * const * as, numeral_vector & roots) {
+            SASSERT(n > 2);
+            SASSERT(!is_zero(as[0])); 
+            SASSERT(!is_zero(as[n-1]));
             // TODO
         }
 
+        /**
+           \brief Root isolation for polynomials that are
+                   - zero is not a root
+                   - square free
+                   - nonconstant
+        */
+        void nz_sqf_isolate_roots(unsigned n, value * const * as, numeral_vector & roots) {
+            SASSERT(n > 1);
+            SASSERT(!is_zero(as[0])); 
+            SASSERT(!is_zero(as[n-1]));
+            if (n == 2) {
+                // we don't need a field extension for linear polynomials.
+                numeral r;
+                value_ref neg_as_0(*this);
+                neg_as_0 = neg(as[0]);
+                set(r, div(neg_as_0, as[1]));
+                roots.push_back(r);
+            }
+            else {
+                nl_nz_sqf_isolate_roots(n, as, roots); 
+            }
+        }
+        
+        /**
+           \brief Root isolation for polynomials where 0 is not a root.
+        */
+        void nz_isolate_roots(unsigned n, value * const * as, numeral_vector & roots) {
+            SASSERT(n > 0);
+            SASSERT(!is_zero(as[0])); 
+            SASSERT(!is_zero(as[n-1]));
+            if (n == 1) {
+                // constant polynomial
+                return; 
+            }
+            value_ref_buffer sqf(*this);
+            square_free(n, as, sqf);
+            nz_sqf_isolate_roots(sqf.size(), sqf.c_ptr(), roots);
+        }
+
+        /**
+           \brief Root isolation entry point.
+        */
+        void isolate_roots(unsigned n, numeral const * as, numeral_vector & roots) {
+            SASSERT(n > 0);
+            SASSERT(!is_zero(as[n-1]));
+            if (n == 1) {
+                // constant polynomial
+                return; 
+            }
+            unsigned i = 0;
+            for (; i < n; i++) {
+                if (!is_zero(as[i]))
+                    break;
+            }
+            SASSERT(i < n);
+            SASSERT(!is_zero(as[i]));
+            ptr_buffer<value> as_values;
+            for (; i < n; i++)
+                as_values.push_back(as[i].m_value);
+            nz_isolate_roots(as_values.size(), as_values.c_ptr(), roots);
+            if (as_values.size() < n) {
+                // zero is a root
+                roots.push_back(numeral());
+            }
+        }
+
         void reset(numeral & a) {
             del(a);
             SASSERT(is_zero(a));

src/math/realclosure/realclosure.h

@@ -278,6 +278,10 @@ namespace realclosure {
         value * m_value;
     public:
         num():m_value(0) {}
+
+        // Low level functions for implementing the C API
+        void * c_ptr() { return m_value; }
+        static num mk(void * ptr) { num r; r.m_value = reinterpret_cast<value*>(ptr); return r; }
     };
 };