From 7a31c6bc743cfa0fc5ffa1c76e506e15c07427c5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 8 Dec 2012 21:07:17 -0800
Subject: [PATCH] exposed root isolation algorithm in the API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/api/api_algebraic.cpp | 35 ++++++++++++++++++++++++++++++++---
 src/api/python/z3num.py   | 28 ++++++++++++++++++++++++++++
 2 files changed, 60 insertions(+), 3 deletions(-)

diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp
index f5a52a6ea..3751c82ee 100644
--- a/src/api/api_algebraic.cpp
+++ b/src/api/api_algebraic.cpp
@@ -25,6 +25,7 @@ Notes:
 #include"expr2polynomial.h"
 #include"cancel_eh.h"
 #include"scoped_timer.h"
+#include"api_ast_vector.h"
 
 extern "C" {
 
@@ -353,8 +354,35 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_algebraic_roots(c, p, n, a);
         RESET_ERROR_CODE();
-        // TODO
-        return 0;
+        polynomial::manager & pm = mk_c(c)->pm();
+        polynomial_ref _p(pm);
+        polynomial::scoped_numeral d(pm.m());
+        expr2polynomial converter(mk_c(c)->m(), pm, 0, true);
+        if (!converter.to_polynomial(to_expr(p), _p, d) ||
+            static_cast<unsigned>(max_var(_p)) >= n + 1) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        algebraic_numbers::manager & _am = am(c);
+        scoped_anum_vector as(_am);
+        if (!to_anum_vector(c, n, a, as)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        scoped_anum_vector roots(_am);
+        {
+            cancel_eh<algebraic_numbers::manager> eh(_am);
+            api::context::set_interruptable(*(mk_c(c)), eh);
+            scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
+            vector_var2anum v2a(as);
+            _am.isolate_roots(_p, v2a, roots);
+        }
+        Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+        mk_c(c)->save_object(result);
+        for (unsigned i = 0; i < roots.size(); i++) {
+            result->m_ast_vector.push_back(au(c).mk_numeral(roots.get(i), false));
+        }
+        RETURN_Z3(of_ast_vector(result));
         Z3_CATCH_RETURN(0);
     }
 
@@ -366,7 +394,8 @@ extern "C" {
         polynomial_ref _p(pm);
         polynomial::scoped_numeral d(pm.m());
         expr2polynomial converter(mk_c(c)->m(), pm, 0, true);
-        if (!converter.to_polynomial(to_expr(p), _p, d)) {
+        if (!converter.to_polynomial(to_expr(p), _p, d) ||
+            static_cast<unsigned>(max_var(_p)) >= n) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
diff --git a/src/api/python/z3num.py b/src/api/python/z3num.py
index de30e9e7a..99f336050 100644
--- a/src/api/python/z3num.py
+++ b/src/api/python/z3num.py
@@ -505,6 +505,34 @@ def eval_sign_at(p, vs):
     for i in range(num):
         _vs[i] = vs[i].ast
     return Z3_algebraic_eval(p.ctx_ref(), p.as_ast(), num, _vs)
+
+def isolate_roots(p, vs=[]):
+    """
+    Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the 
+    roots of the univariate polynomial p(vs[0], ..., vs[len(vs)-1], x_n).
+       
+    Remarks:
+    * p is a Z3 expression that contains only arithmetic terms and free variables.
+    * forall i in [0, n) vs is a numeral.
+    
+    The result is a list of numerals
+
+    >>> x0 = RealVar(0)
+    >>> isolate_roots(x0**5 - x0 - 1)
+    [1.1673039782?]
+    >>> x1 = RealVar(1)
+    >>> isolate_roots(x0**2 - x1**4 - 1, [ Numeral(Sqrt(3)) ])
+    [-1.1892071150?, 1.1892071150?]
+    >>> x2 = RealVar(2)
+    >>> isolate_roots(x2**2 + x0 - x1, [ Numeral(Sqrt(3)), Numeral(Sqrt(2)) ])
+    []
+    """
+    num = len(vs)
+    _vs = (Ast * num)()
+    for i in range(num):
+        _vs[i] = vs[i].ast
+    _roots = AstVector(Z3_algebraic_roots(p.ctx_ref(), p.as_ast(), num, _vs), p.ctx)
+    return [ Numeral(r) for r in _roots ]
         
 if __name__ == "__main__":
     import doctest