diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp index 7d08ade35..d31622b3e 100644 --- a/src/api/api_algebraic.cpp +++ b/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); + } }; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 00a647474..b3c670846 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -66,6 +66,7 @@ namespace z3 { class func_entry; class statistics; class apply_result; + template class cast_ast; template class ast_vector_tpl; typedef ast_vector_tpl ast_vector; typedef ast_vector_tpl 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 + 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()(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 class cast_ast; - template<> class cast_ast { public: ast operator()(context & c, Z3_ast a) { return ast(c, a); } @@ -1882,75 +1967,6 @@ namespace z3 { } }; - template - 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()(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 template array::array(ast_vector_tpl const & v) { diff --git a/src/api/julia/z3jl.cpp b/src/api/julia/z3jl.cpp index 923349179..0877cc3cd 100644 --- a/src/api/julia/z3jl.cpp +++ b/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) diff --git a/src/api/z3_algebraic.h b/src/api/z3_algebraic.h index 1ebc1ad8f..bb419d218 100644 --- a/src/api/z3_algebraic.h +++ b/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); + /*@}*/ /*@}*/ diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 8e61d7ebb..b984ce2c0 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/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()); diff --git a/src/math/polynomial/algebraic_numbers.h b/src/math/polynomial/algebraic_numbers.h index 2822f0042..e1f37b718 100644 --- a/src/math/polynomial/algebraic_numbers.h +++ b/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 & 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);