Extract defining components of algebraic number via C and C++ API (#3321)

* First steps toward adding Julia bindings

* Simplifications

* Streamlining

* Friends of tactic and probe

* Add missing functions

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Changes for CxxWrap v0.9.0

* Wrap enumeration and tuple sort

* Wrap z3::fixedpoint

* Wrap z3::optimize

* Wrap missing functions

* Fix aux types

* Add some missing functions

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit 5aab9f9240.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit cfccd7ca2c.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit f24740c595.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit 592499eaa0.

* Checkout current version of pipeline

* Build Julia bindings on macOS

* Extract components of algebraic number

* Add type to C API function name

* Remove blank line

* Typo in doc

* Return Z3_ast_vector containing coefficients

src/api/api_algebraic.cpp

@@ -418,4 +418,36 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_algebraic_get_poly(c, a);
+        RESET_ERROR_CODE();
+        CHECK_IS_ALGEBRAIC(a, 0);
+        algebraic_numbers::manager & _am = am(c);
+        algebraic_numbers::anum const & av = get_irrational(c, a);
+        scoped_mpz_vector coeffs(_am.qm());
+        _am.get_polynomial(av, coeffs);
+        api::context * _c = mk_c(c);
+        sort * s = _c->m().mk_sort(_c->get_arith_fid(), REAL_SORT);
+        Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, *_c, _c->m());
+        mk_c(c)->save_object(result);
+        for (unsigned i = 0; i < coeffs.size(); i++) {
+            rational r(coeffs[i]);
+            expr * a = _c->mk_numeral_core(r, s);
+            result->m_ast_vector.push_back(a);
+        }
+        RETURN_Z3(of_ast_vector(result));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a) {
+        Z3_TRY;
+        LOG_Z3_algebraic_get_i(c, a);
+        RESET_ERROR_CODE();
+        CHECK_IS_ALGEBRAIC(a, 0);
+        algebraic_numbers::manager & _am = am(c);
+        algebraic_numbers::anum const & av = get_irrational(c, a);
+        return _am.get_i(av);
+        Z3_CATCH_RETURN(0);
+    }
 };

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

@@ -66,6 +66,7 @@ namespace z3 {
     class func_entry;
     class statistics;
     class apply_result;
+    template<typename T> class cast_ast;
     template<typename T> class ast_vector_tpl;
     typedef ast_vector_tpl<ast>       ast_vector;
     typedef ast_vector_tpl<expr>      expr_vector;
@@ -511,6 +512,74 @@ namespace z3 {
 
     inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b); }
 
+    template<typename T>
+    class ast_vector_tpl : public object {
+        Z3_ast_vector m_vector;
+        void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
+    public:
+        ast_vector_tpl(context & c):object(c) { init(Z3_mk_ast_vector(c)); }
+        ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
+        ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
+        ast_vector_tpl(context& c, ast_vector_tpl const& src): object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); }
+
+        ~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); }
+        operator Z3_ast_vector() const { return m_vector; }
+        unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
+        T operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
+        void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
+        void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
+        T back() const { return operator[](size() - 1); }
+        void pop_back() { assert(size() > 0); resize(size() - 1); }
+        bool empty() const { return size() == 0; }
+        ast_vector_tpl & operator=(ast_vector_tpl const & s) {
+            Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
+            Z3_ast_vector_dec_ref(ctx(), m_vector);
+            m_ctx = s.m_ctx;
+            m_vector = s.m_vector;
+            return *this;
+        }
+        ast_vector_tpl& set(unsigned idx, ast& a) {
+            Z3_ast_vector_set(ctx(), m_vector, idx, a);
+            return *this;
+        }
+        /*
+          Disabled pending C++98 build upgrade
+        bool contains(T const& x) const {
+            for (T y : *this) if (eq(x, y)) return true;
+            return false;
+        }
+        */
+
+        class iterator {
+            ast_vector_tpl const* m_vector;
+            unsigned m_index;
+        public:
+            iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {}
+            iterator(iterator const& other): m_vector(other.m_vector), m_index(other.m_index) {}
+            iterator operator=(iterator const& other) { m_vector = other.m_vector; m_index = other.m_index; return *this; }
+
+            bool operator==(iterator const& other) const {
+                return other.m_index == m_index;
+            };
+            bool operator!=(iterator const& other) const {
+                return other.m_index != m_index;
+            };
+            iterator& operator++() {
+                ++m_index;
+                return *this;
+            }
+            void set(T& arg) {
+                Z3_ast_vector_set(m_vector->ctx(), *m_vector, m_index, arg);
+            }
+            iterator operator++(int) { iterator tmp = *this; ++m_index; return tmp; }
+            T * operator->() const { return &(operator*()); }
+            T operator*() const { return (*m_vector)[m_index]; }
+        };
+        iterator begin() const { return iterator(this, 0); }
+        iterator end() const { return iterator(this, size()); }
+        friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
+    };
+
 
     /**
        \brief A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
@@ -665,7 +734,6 @@ namespace z3 {
        \brief A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean.
        Every expression has a sort.
     */
-
     class expr : public ast {
     public:
         expr(context & c):ast(c) {}
@@ -815,6 +883,25 @@ namespace z3 {
             return expr(ctx(), r);
         }
         
+        /**
+           \brief Return coefficients for p of an algebraic number (root-obj p i)
+         */
+        expr_vector algebraic_poly() const {
+            assert(is_algebraic());
+            Z3_ast_vector r = Z3_algebraic_get_poly(ctx(), m_ast);
+            check_error();
+            return expr_vector(ctx(), r);
+        }
+
+        /**
+           \brief Return i of an algebraic number (root-obj p i)
+         */
+        unsigned algebraic_i() const {
+            assert(is_algebraic());
+            unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
+            check_error();
+            return i;
+        }
 
         /**
            \brief retrieve unique identifier for expression.
@@ -1848,8 +1935,6 @@ namespace z3 {
         return to_func_decl(a.ctx(), Z3_mk_tree_order(a.ctx(), a, index));
     }
 
-    template<typename T> class cast_ast;
-
     template<> class cast_ast<ast> {
     public:
         ast operator()(context & c, Z3_ast a) { return ast(c, a); }
@@ -1882,75 +1967,6 @@ namespace z3 {
         }
     };
 
-    template<typename T>
-    class ast_vector_tpl : public object {
-        Z3_ast_vector m_vector;
-        void init(Z3_ast_vector v) { Z3_ast_vector_inc_ref(ctx(), v); m_vector = v; }
-    public:
-        ast_vector_tpl(context & c):object(c) { init(Z3_mk_ast_vector(c)); }
-        ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
-        ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
-        ast_vector_tpl(context& c, ast_vector_tpl const& src): object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); }
-
-        ~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); }
-        operator Z3_ast_vector() const { return m_vector; }
-        unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
-        T operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
-        void push_back(T const & e) { Z3_ast_vector_push(ctx(), m_vector, e); check_error(); }
-        void resize(unsigned sz) { Z3_ast_vector_resize(ctx(), m_vector, sz); check_error(); }
-        T back() const { return operator[](size() - 1); }
-        void pop_back() { assert(size() > 0); resize(size() - 1); }
-        bool empty() const { return size() == 0; }
-        ast_vector_tpl & operator=(ast_vector_tpl const & s) {
-            Z3_ast_vector_inc_ref(s.ctx(), s.m_vector);
-            Z3_ast_vector_dec_ref(ctx(), m_vector);
-            m_ctx = s.m_ctx;
-            m_vector = s.m_vector;
-            return *this;
-        }
-        ast_vector_tpl& set(unsigned idx, ast& a) {
-            Z3_ast_vector_set(ctx(), m_vector, idx, a);
-            return *this;
-        }
-        /*
-          Disabled pending C++98 build upgrade
-        bool contains(T const& x) const {
-            for (T y : *this) if (eq(x, y)) return true;
-            return false;
-        }
-        */
-
-        class iterator {
-            ast_vector_tpl const* m_vector;
-            unsigned m_index;
-        public:
-            iterator(ast_vector_tpl const* v, unsigned i): m_vector(v), m_index(i) {}
-            iterator(iterator const& other): m_vector(other.m_vector), m_index(other.m_index) {}
-            iterator operator=(iterator const& other) { m_vector = other.m_vector; m_index = other.m_index; return *this; }
-
-            bool operator==(iterator const& other) const {
-                return other.m_index == m_index;
-            };
-            bool operator!=(iterator const& other) const {
-                return other.m_index != m_index;
-            };
-            iterator& operator++() {
-                ++m_index;
-                return *this;
-            }
-            void set(T& arg) {
-                Z3_ast_vector_set(m_vector->ctx(), *m_vector, m_index, arg);
-            }
-            iterator operator++(int) { iterator tmp = *this; ++m_index; return tmp; }
-            T * operator->() const { return &(operator*()); }
-            T operator*() const { return (*m_vector)[m_index]; }
-        };
-        iterator begin() const { return iterator(this, 0); }
-        iterator end() const { return iterator(this, size()); }
-        friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
-    };
-
-
     template<typename T>
     template<typename T2>
     array<T>::array(ast_vector_tpl<T2> const & v) {

src/api/julia/z3jl.cpp

@@ -203,6 +203,10 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
         .MM(expr, is_well_sorted)
         .MM(expr, get_decimal_string)
         .MM(expr, id)
+        .MM(expr, algebraic_lower)
+        .MM(expr, algebraic_upper)
+        .MM(expr, algebraic_poly)
+        .MM(expr, algebraic_i)
         .MM(expr, get_numeral_int)
         .MM(expr, get_numeral_uint)
         .MM(expr, get_numeral_int64)

src/api/z3_algebraic.h

@@ -223,6 +223,24 @@ extern "C" {
     */
     int Z3_API Z3_algebraic_eval(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]);
 
+    /**
+       \brief Return the coefficients of the defining polynomial.
+
+       \pre Z3_algebraic_is_value(c, a)
+
+       def_API('Z3_algebraic_get_poly', AST_VECTOR, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a);
+
+    /**
+       \brief Return which root of the polynomial the algebraic number represents.
+
+       \pre Z3_algebraic_is_value(c, a)
+
+       def_API('Z3_algebraic_get_i', UINT, (_in(CONTEXT), _in(AST)))
+    */
+    unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a);
+
     /*@}*/
     /*@}*/
 

src/math/polynomial/algebraic_numbers.cpp

@@ -1951,6 +1951,19 @@ namespace algebraic_numbers {
             }
         }
 
+        unsigned get_i(numeral const & a) {
+            if (a.is_basic()) {
+                if (is_zero(a)) {
+                    return 0;
+                }
+                return 1;
+            }
+            else {
+                algebraic_cell * c = a.to_algebraic();
+                return c->m_i;
+            }
+        }
+
         /**
            \brief "Optimistic" mapping: it assumes all variables are mapped to
            basic_values (rationals). Throws an exception if that is not the case.
@@ -3000,6 +3013,10 @@ namespace algebraic_numbers {
         m_imp->get_polynomial(a, r);
     }
 
+    unsigned manager::get_i(numeral const & a) {
+        return m_imp->get_i(a);
+    }
+
     void manager::get_lower(numeral const & a, mpbq & l) {
         SASSERT(!is_rational(a));
         bqm().set(l, a.to_algebraic()->m_interval.lower());

src/math/polynomial/algebraic_numbers.h

@@ -307,6 +307,7 @@ namespace algebraic_numbers {
         sign eval_sign_at(polynomial_ref const & p, polynomial::var2anum const & x2v);
 
         void get_polynomial(numeral const & a, svector<mpz> & r);
+        unsigned get_i(numeral const & a);
         
         // Procedures for getting lower and upper bounds for irrational numbers
         void get_lower(numeral const & a, mpbq & l);