From e1d2b88a82e150ae2f4edda3fd5546de6d251e4f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Jul 2020 15:08:11 -0700 Subject: [PATCH] access polynomial expressions from algebraic numerals Signed-off-by: Nikolaj Bjorner --- src/api/api_algebraic.cpp | 14 ++++++-------- src/api/python/z3/z3.py | 6 ++++++ 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp index d31622b3e..90e8f4daf 100644 --- a/src/api/api_algebraic.cpp +++ b/src/api/api_algebraic.cpp @@ -427,14 +427,12 @@ extern "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); + 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()); + _c.save_object(result); + for (auto const& c : coeffs) { + result->m_ast_vector.push_back(_c.mk_numeral_core(c, s)); } RETURN_Z3(of_ast_vector(result)); Z3_CATCH_RETURN(nullptr); diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 61214dcc9..bbf072155 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -2921,6 +2921,12 @@ class AlgebraicNumRef(ArithRef): """ return Z3_get_numeral_decimal_string(self.ctx_ref(), self.as_ast(), prec) + def poly(self): + return AstVector(Z3_algebraic_get_poly(self.ctx_ref(), self.as_ast()), self.ctx) + + def index(self): + return Z3_algebraic_get_i(self.ctx_ref(), self.as_ast()) + def _py2expr(a, ctx=None): if isinstance(a, bool): return BoolVal(a, ctx)