mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

access polynomial expressions from algebraic numerals

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-23 15:08:11 -07:00
parent a6a041ec5d
commit e1d2b88a82
2 changed files with 12 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/api/api_algebraic.cpp
View file

@ -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);

6
src/api/python/z3/z3.py
View file

@ -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)