added polynomial evaluation at algebraic point

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

src/api/api_algebraic.cpp

@@ -22,6 +22,9 @@ Notes:
 #include"api_log_macros.h"
 #include"api_context.h"
 #include"algebraic_numbers.h"
+#include"expr2polynomial.h"
+#include"cancel_eh.h"
+#include"scoped_timer.h"
 
 extern "C" {
 
@@ -318,6 +321,34 @@ extern "C" {
         return !Z3_algebraic_eq(c, a, b);
     }
 
+    static bool to_anum_vector(Z3_context c, unsigned n, Z3_ast a[], scoped_anum_vector & as) {
+        algebraic_numbers::manager & _am = am(c);
+        scoped_anum tmp(_am);
+        for (unsigned i = 0; i < n; i++) {
+            if (is_rational(c, a[i])) {
+                _am.set(tmp, get_rational(c, a[i]).to_mpq());       
+                as.push_back(tmp);
+            }
+            else if (is_irrational(c, a[i])) {
+                as.push_back(get_irrational(c, a[i]));
+            }
+            else {
+                return false;
+            }
+        }
+        return true;
+    }
+
+    class vector_var2anum : public polynomial::var2anum {
+        scoped_anum_vector const & m_as;
+    public:
+        vector_var2anum(scoped_anum_vector & as):m_as(as) {}
+        virtual ~vector_var2anum() {}
+        virtual algebraic_numbers::manager & m() const { return m_as.m(); }
+        virtual bool contains(polynomial::var x) const { return static_cast<unsigned>(x) < m_as.size(); }
+        virtual algebraic_numbers::anum const & operator()(polynomial::var x) const { return m_as.get(x); }
+    };
+
     Z3_ast_vector Z3_API Z3_algebraic_roots(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]) {
         Z3_TRY;
         LOG_Z3_algebraic_roots(c, p, n, a);
@@ -331,8 +362,30 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_algebraic_eval(c, p, n, a);
         RESET_ERROR_CODE();
-        // TODO
+        polynomial::manager & pm = mk_c(c)->pm();
-        return 0;
+        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)) {
+            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;
+        }
+        {
+            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);
+            int r = _am.eval_sign_at(_p, v2a);
+            if (r > 0) return 1;
+            else if (r < 0) return -1;
+            else return 0;
+        }
         Z3_CATCH_RETURN(0);
     }
 

src/api/api_context.h

@@ -32,6 +32,7 @@ Revision History:
 #include"event_handler.h"
 #include"tactic_manager.h"
 #include"context_params.h"
+#include"api_polynomial.h"
 
 namespace smtlib {
     class parser;
@@ -81,6 +82,8 @@ namespace api {
         Z3_ast_print_mode          m_print_mode;
 
         event_handler *            m_interruptable; // Reference to an object that can be interrupted by Z3_interrupt
+
+        pmanager                   m_pmanager;
     public:
         // Scoped obj for setting m_interruptable
         class set_interruptable {
@@ -167,6 +170,13 @@ namespace api {
 
         void check_sorts(ast * n);
 
+        // ------------------------
+        //
+        // Polynomial manager & caches
+        //
+        // -----------------------
+        polynomial::manager & pm() { return m_pmanager.pm(); }
+
         // ------------------------
         //
         // Solver interface for backward compatibility 

src/api/api_polynomial.cpp

@@ -0,0 +1,34 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    api_polynomial.cpp
+
+Abstract:
+
+    Polynomial manager and caches for the external API.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-12-08
+
+Notes:
+    
+--*/
+#include"api_polynomial.h"
+
+namespace api {
+
+    pmanager::pmanager():
+        m_pm(m_nm) {
+    }
+
+    pmanager::~pmanager() {
+    }
+    
+    void pmanager::set_cancel(bool f) {
+        m_pm.set_cancel(f);
+    }
+
+};

src/api/api_polynomial.h

@@ -0,0 +1,39 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    api_polynomial.h
+
+Abstract:
+
+    Polynomial manager and caches for the external API.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-12-08
+
+Notes:
+    
+--*/
+#ifndef _API_POLYNOMIAL_H_
+#define _API_POLYNOMIAL_H_
+
+#include"polynomial.h"
+
+namespace api {
+    
+    class pmanager {
+        unsynch_mpz_manager m_nm;
+        polynomial::manager m_pm;
+        // TODO: add support for caching expressions -> polynomial and back
+    public:
+        pmanager();
+        virtual ~pmanager();
+        polynomial::manager & pm() { return m_pm; }
+        void set_cancel(bool f);
+    };
+
+};
+
+#endif

src/api/python/z3.py

@@ -1126,6 +1126,27 @@ def Var(idx, s):
         _z3_assert(is_sort(s), "Z3 sort expected")
     return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
 
+def RealVar(idx, ctx=None):
+    """
+    Create a real free variable. Free variables are used to create quantified formulas.
+    They are also used to create polynomials.
+    
+    >>> RealVar(0)
+    Var(0)
+    """
+    return Var(idx, RealSort(ctx))
+
+def RealVarVector(n, ctx=None):
+    """
+    Create a list of Real free variables.
+    The variables have ids: 0, 1, ..., n-1
+    
+    >>> x0, x1, x2, x3 = RealVarVector(4)
+    >>> x2
+    Var(2)
+    """
+    return [ RealVar(i, ctx) for i in range(n) ]
+
 #########################################
 #
 # Booleans

src/api/python/z3num.py

@@ -481,6 +481,30 @@ class Numeral:
 
     def ctx_ref(self):
         return self.ctx.ref()
+
+def eval_sign_at(p, vs):
+    """ 
+    Evaluate the sign of the polynomial `p` at `vs`.  `p` is a Z3
+    Expression containing arithmetic operators: +, -, *, ^k where k is
+    an integer; and free variables x that is_var(x) is True. Moreover,
+    all variables must be real.
+    
+    The result is 1 if the polynomial is positive at the given point,
+    -1 if negative, and 0 if zero.
+
+    >>> x0, x1, x2 = RealVarVector(3)
+    >>> eval_sign_at(x0**2 + x1*x2 + 1, (Numeral(0), Numeral(1), Numeral(2)))
+    1
+    >>> eval_sign_at(x0**2 - 2, [ Numeral(Sqrt(2)) ])
+    0
+    >>> eval_sign_at((x0 + x1)*(x0 + x2), (Numeral(0), Numeral(Sqrt(2)), Numeral(Sqrt(3))))
+    1
+    """
+    num = len(vs)
+    _vs = (Ast * num)()
+    for i in range(num):
+        _vs[i] = vs[i].ast
+    return Z3_algebraic_eval(p.ctx_ref(), p.as_ast(), num, _vs)
         
 if __name__ == "__main__":
     import doctest

src/ast/expr2polynomial.cpp

@@ -49,21 +49,24 @@ struct expr2polynomial::imp {
     polynomial::polynomial_ref_vector  m_presult_stack;
     polynomial::scoped_numeral_vector  m_dresult_stack;
 
+    bool                               m_use_var_idxs;
+
     volatile bool                      m_cancel;
     
-    imp(expr2polynomial & w, ast_manager & am, polynomial::manager & pm, expr2var * e2v):
+    imp(expr2polynomial & w, ast_manager & am, polynomial::manager & pm, expr2var * e2v, bool use_var_idxs):
         m_wrapper(w),
         m_am(am),
         m_autil(am),
         m_pm(pm),
-        m_expr2var(e2v == 0 ? alloc(expr2var, am) : e2v),
+        m_expr2var(e2v == 0 && !use_var_idxs ? alloc(expr2var, am) : e2v),
-        m_expr2var_owner(e2v == 0),
+        m_expr2var_owner(e2v == 0 && !use_var_idxs),
         m_var2expr(am),
         m_cached_domain(am),
         m_cached_polynomials(pm),
         m_cached_denominators(pm.m()),
         m_presult_stack(pm),
         m_dresult_stack(pm.m()),
+        m_use_var_idxs(use_var_idxs),
         m_cancel(false) {
     }
 
@@ -95,6 +98,14 @@ struct expr2polynomial::imp {
         cooperate("expr2polynomial");
     }
 
+    void throw_not_polynomial() {
+        throw default_exception("the given expression is not a polynomial");
+    }
+
+    void throw_no_int_var() {
+        throw default_exception("integer variables are not allowed in the given polynomial");
+    }
+
     void push_frame(app * t) {
         m_frame_stack.push_back(frame(t));
     }
@@ -127,14 +138,26 @@ struct expr2polynomial::imp {
     }
 
     void store_var_poly(expr * t) {
-        polynomial::var x = m_expr2var->to_var(t);
+        polynomial::var x;
-        if (x == UINT_MAX) {
+        if (m_use_var_idxs) {
-            bool is_int = m_autil.is_int(t);
+            SASSERT(::is_var(t));
-            x = m_wrapper.mk_var(is_int);
+            if (m_autil.is_int(t))
-            m_expr2var->insert(t, x);
+                throw_no_int_var();
-            if (x >= m_var2expr.size())
+            unsigned idx = to_var(t)->get_idx();
-                m_var2expr.resize(x+1, 0);
+            while (idx >= m_pm.num_vars())
-            m_var2expr.set(x, t);
+                m_pm.mk_var();
+            x = static_cast<polynomial::var>(idx);
+        }
+        else {
+            x = m_expr2var->to_var(t);
+            if (x == UINT_MAX) {
+                bool is_int = m_autil.is_int(t);
+                x = m_wrapper.mk_var(is_int);
+                m_expr2var->insert(t, x);
+                if (x >= m_var2expr.size())
+                    m_var2expr.resize(x+1, 0);
+                m_var2expr.set(x, t);
+            }
         }
         polynomial::numeral one(1);
         store_result(t, pm().mk_polynomial(x), one);
@@ -160,7 +183,10 @@ struct expr2polynomial::imp {
             rational k;
             SASSERT(t->get_num_args() == 2);
             if (!m_autil.is_numeral(t->get_arg(1), k) || !k.is_int() || !k.is_unsigned()) {
-                store_var_poly(t);
+                if (m_use_var_idxs)
+                    throw_not_polynomial();
+                else
+                    store_var_poly(t);
                 return true;
             }
             push_frame(t);
@@ -168,6 +194,8 @@ struct expr2polynomial::imp {
         }
         default:
             // can't handle operator
+            if (m_use_var_idxs)
+                throw_not_polynomial();
             store_var_poly(t);
             return true;
         }
@@ -190,6 +218,8 @@ struct expr2polynomial::imp {
         
         SASSERT(is_app(t));
         if (!m_autil.is_arith_expr(t)) {
+            if (m_use_var_idxs)
+                throw_not_polynomial();
             store_var_poly(t);
             return true;
         }
@@ -378,19 +408,25 @@ struct expr2polynomial::imp {
 
         for (unsigned i = 0; i < sz; i++) {
             margs.reset();
-            polynomial::monomial * m = pm().get_monomial(p, i);
+            polynomial::monomial * _m = pm().get_monomial(p, i);
             polynomial::numeral const & a = pm().coeff(p, i);
             if (!nm().is_one(a)) {
                 margs.push_back(m_autil.mk_numeral(rational(a), is_int));
             }
-            unsigned msz = pm().size(m);
+            unsigned msz = pm().size(_m);
             for (unsigned j = 0; j < msz; j++) {
-                polynomial::var x = pm().get_var(m, j);
+                polynomial::var x = pm().get_var(_m, j);
-                expr * t = m_var2expr.get(x);
+                expr * t;
-                if (m_wrapper.is_int(x) && !is_int) {
+                if (m_use_var_idxs) {
-                    t = m_autil.mk_to_real(t);
+                    t = m().mk_var(x, m_autil.mk_real());
                 }
-                unsigned d = pm().degree(m, j);
+                else {
+                    t = m_var2expr.get(x);
+                    if (m_wrapper.is_int(x) && !is_int) {
+                        t = m_autil.mk_to_real(t);
+                    }
+                }
+                unsigned d = pm().degree(_m, j);
                 if (use_power && d > 1) {
                     margs.push_back(m_autil.mk_power(t, m_autil.mk_numeral(rational(d), is_int)));
                 }
@@ -426,8 +462,8 @@ struct expr2polynomial::imp {
     }
 };
 
-expr2polynomial::expr2polynomial(ast_manager & am, polynomial::manager & pm, expr2var * e2v) {
+expr2polynomial::expr2polynomial(ast_manager & am, polynomial::manager & pm, expr2var * e2v, bool use_var_idxs) {
-    m_imp = alloc(imp, *this, am, pm, e2v);
+    m_imp = alloc(imp, *this, am, pm, e2v, use_var_idxs);
 }
 
 expr2polynomial::~expr2polynomial() {
@@ -451,10 +487,12 @@ void expr2polynomial::to_expr(polynomial::polynomial_ref const & p, bool use_pow
 }
 
 bool expr2polynomial::is_var(expr * t) const { 
+    SASSERT(!m_imp->m_use_var_idxs);
     return m_imp->m_expr2var->is_var(t); 
 }
     
 expr2var const & expr2polynomial::get_mapping() const { 
+    SASSERT(!m_imp->m_use_var_idxs);
     return *(m_imp->m_expr2var); 
 }
 

src/ast/expr2polynomial.h

@@ -29,7 +29,24 @@ class expr2polynomial {
     struct imp;
     imp * m_imp;
 public:
-    expr2polynomial(ast_manager & am, polynomial::manager & pm, expr2var * e2v);
+    expr2polynomial(ast_manager & am, 
+                    polynomial::manager & pm, 
+                    expr2var * e2v,
+                    /*
+                      If true, the expressions converted into 
+                      polynomials should only contain Z3 free variables.
+                      A Z3 variable x, with idx i, is converted into
+                      the variable i of the polynomial manager pm.
+                      
+                      An exception is thrown if there is a mismatch between
+                      the sorts x and the variable in the polynomial manager.
+
+                      The argument e2v is ignored when use_var_idxs is true.
+
+                      Moreover, only real variables are allowed.
+                    */
+                    bool use_var_idxs = false
+                    );
     virtual ~expr2polynomial();
 
     ast_manager & m() const;
@@ -63,6 +80,8 @@ public:
     
     /**
        \brief Return the mapping from expressions to variables
+    
+       \pre the object was created using use_var_idxs = false.
     */
     expr2var const & get_mapping() const;
 
@@ -74,10 +93,10 @@ public:
     /**
        \brief Return true if the variable is associated with an expression of integer sort.
     */
-    virtual bool is_int(polynomial::var x) const = 0;
+    virtual bool is_int(polynomial::var x) const { UNREACHABLE(); return false; }
 
 protected:
-    virtual polynomial::var mk_var(bool is_int) = 0;
+    virtual polynomial::var mk_var(bool is_int) { UNREACHABLE(); return polynomial::null_var; }
 };
 
 class default_expr2polynomial : public expr2polynomial {

src/math/polynomial/algebraic_numbers.h

@@ -64,6 +64,8 @@ namespace algebraic_numbers {
         static void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
 
         void set_cancel(bool f);
+        
+        void cancel() { set_cancel(true); }
 
         void updt_params(params_ref const & p);