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

exposed root isolation algorithm in the API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-08 21:07:17 -08:00
parent 0d230375be
commit 7a31c6bc74
2 changed files with 60 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/api/api_algebraic.cpp
View file

@ -25,6 +25,7 @@ Notes:
#include"expr2polynomial.h"
#include"cancel_eh.h"
#include"scoped_timer.h"
#include"api_ast_vector.h"
extern "C" {
@ -353,8 +354,35 @@ extern "C" {
Z3_TRY;
LOG_Z3_algebraic_roots(c, p, n, a);
RESET_ERROR_CODE();
// TODO
return 0;
polynomial::manager & pm = mk_c(c)->pm();
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) ||
static_cast<unsigned>(max_var(_p)) >= n + 1) {
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;
}
scoped_anum_vector roots(_am);
{
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);
_am.isolate_roots(_p, v2a, roots);
}
Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, mk_c(c)->m());
mk_c(c)->save_object(result);
for (unsigned i = 0; i < roots.size(); i++) {
result->m_ast_vector.push_back(au(c).mk_numeral(roots.get(i), false));
}
RETURN_Z3(of_ast_vector(result));
Z3_CATCH_RETURN(0);
}
@ -366,7 +394,8 @@ extern "C" {
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)) {
if (!converter.to_polynomial(to_expr(p), _p, d) ||
static_cast<unsigned>(max_var(_p)) >= n) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}

28
src/api/python/z3num.py
View file

@ -505,6 +505,34 @@ def eval_sign_at(p, vs):
for i in range(num):
_vs[i] = vs[i].ast
return Z3_algebraic_eval(p.ctx_ref(), p.as_ast(), num, _vs)
def isolate_roots(p, vs=[]):
"""
Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the
roots of the univariate polynomial p(vs[0], ..., vs[len(vs)-1], x_n).
Remarks:
* p is a Z3 expression that contains only arithmetic terms and free variables.
* forall i in [0, n) vs is a numeral.
The result is a list of numerals
>>> x0 = RealVar(0)
>>> isolate_roots(x0**5 - x0 - 1)
[1.1673039782?]
>>> x1 = RealVar(1)
>>> isolate_roots(x0**2 - x1**4 - 1, [ Numeral(Sqrt(3)) ])
[-1.1892071150?, 1.1892071150?]
>>> x2 = RealVar(2)
>>> isolate_roots(x2**2 + x0 - x1, [ Numeral(Sqrt(3)), Numeral(Sqrt(2)) ])
[]
"""
num = len(vs)
_vs = (Ast * num)()
for i in range(num):
_vs[i] = vs[i].ast
_roots = AstVector(Z3_algebraic_roots(p.ctx_ref(), p.as_ast(), num, _vs), p.ctx)
return [ Numeral(r) for r in _roots ]
if __name__ == "__main__":
import doctest