From d6a1ea82e1e5aab6d7752197ea2d7ade352f62e3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Dec 2012 16:47:37 -0800 Subject: [PATCH] exposed subresultants aka psc-chain procedure Signed-off-by: Leonardo de Moura --- scripts/mk_project.py | 4 +-- src/api/api_algebraic.cpp | 2 +- src/api/api_polynomial.cpp | 50 ++++++++++++++++++++++++++++++++ src/api/python/z3poly.py | 37 +++++++++++++++++++++++ src/api/z3.h | 1 + src/api/z3_polynomial.h | 45 ++++++++++++++++++++++++++++ src/math/polynomial/polynomial.h | 1 + 7 files changed, 137 insertions(+), 3 deletions(-) create mode 100644 src/api/python/z3poly.py create mode 100644 src/api/z3_polynomial.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 3405d8751..0ebcfe45d 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -58,11 +58,11 @@ def init_project_def(): add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('smtparser', ['portfolio'], 'parsers/smt') + API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h'] add_lib('api', ['portfolio', 'user_plugin', 'smtparser'], - includes2install=['z3.h', 'z3_api.h', 'z3_v1.h', 'z3_macros.h', 'z3_algebraic.h']) + includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3') add_exe('test', ['api', 'fuzzing'], exe_name='test-z3', install=False) - API_files = ['z3_api.h', 'z3_algebraic.h'] add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', reexports=['api'], dll_name='libz3', diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp index 3751c82ee..a3c6726f2 100644 --- a/src/api/api_algebraic.cpp +++ b/src/api/api_algebraic.cpp @@ -21,11 +21,11 @@ Notes: #include"z3.h" #include"api_log_macros.h" #include"api_context.h" +#include"api_ast_vector.h" #include"algebraic_numbers.h" #include"expr2polynomial.h" #include"cancel_eh.h" #include"scoped_timer.h" -#include"api_ast_vector.h" extern "C" { diff --git a/src/api/api_polynomial.cpp b/src/api/api_polynomial.cpp index af5803369..3148f972b 100644 --- a/src/api/api_polynomial.cpp +++ b/src/api/api_polynomial.cpp @@ -16,7 +16,16 @@ Author: Notes: --*/ +#include +#include"z3.h" +#include"api_log_macros.h" +#include"api_context.h" #include"api_polynomial.h" +#include"api_ast_vector.h" +#include"expr2polynomial.h" +#include"cancel_eh.h" +#include"scoped_timer.h" +#include"expr2var.h" namespace api { @@ -32,3 +41,44 @@ namespace api { } }; + +extern "C" { + + Z3_ast_vector Z3_API Z3_polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x) { + Z3_TRY; + LOG_Z3_polynomial_subresultants(c, p, q, x); + RESET_ERROR_CODE(); + polynomial::manager & pm = mk_c(c)->pm(); + polynomial_ref _p(pm), _q(pm); + polynomial::scoped_numeral d(pm.m()); + default_expr2polynomial converter(mk_c(c)->m(), pm); + if (!converter.to_polynomial(to_expr(p), _p, d) || + !converter.to_polynomial(to_expr(q), _q, d)) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } + Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, mk_c(c)->m()); + mk_c(c)->save_object(result); + if (converter.is_var(to_expr(x))) { + expr2var const & mapping = converter.get_mapping(); + unsigned v_x = mapping.to_var(to_expr(x)); + polynomial_ref_vector rs(pm); + polynomial_ref r(pm); + expr_ref _r(mk_c(c)->m()); + { + cancel_eh eh(pm); + api::context::set_interruptable(*(mk_c(c)), eh); + scoped_timer timer(mk_c(c)->params().m_timeout, &eh); + pm.psc_chain(_p, _q, v_x, rs); + } + for (unsigned i = 0; i < rs.size(); i++) { + r = rs.get(i); + converter.to_expr(r, true, _r); + result->m_ast_vector.push_back(_r); + } + } + RETURN_Z3(of_ast_vector(result)); + Z3_CATCH_RETURN(0); + } + +}; diff --git a/src/api/python/z3poly.py b/src/api/python/z3poly.py new file mode 100644 index 000000000..0b8bf9457 --- /dev/null +++ b/src/api/python/z3poly.py @@ -0,0 +1,37 @@ +############################################ +# Copyright (c) 2012 Microsoft Corporation +# +# Z3 Python interface for Z3 polynomials +# +# Author: Leonardo de Moura (leonardo) +############################################ +from z3 import * + +def subresultants(p, q, x): + """ + Return the non-constant subresultants of 'p' and 'q' with respect to the "variable" 'x'. + + 'p', 'q' and 'x' are Z3 expressions where 'p' and 'q' are arithmetic terms. + Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable. + Example: f(a) is a considered to be a variable b in the polynomial + + f(a)*f(a) + 2*f(a) + 1 + + >>> x, y = Reals('x y') + >>> subresultants(2*x + y, 3*x - 2*y + 2, x) + [-7*y + 4] + >>> r = subresultants(3*y*x**2 + y**3 + 1, 2*x**3 + y + 3, x) + >>> r[0] + 4*y**9 + 12*y**6 + 27*y**5 + 162*y**4 + 255*y**3 + 4 + >>> r[1] + -6*y**4 + -6*y + """ + return AstVector(Z3_polynomial_subresultants(p.ctx_ref(), p.as_ast(), q.as_ast(), x.as_ast()), p.ctx) + +if __name__ == "__main__": + import doctest + if doctest.testmod().failed: + exit(1) + + + diff --git a/src/api/z3.h b/src/api/z3.h index 15f0a5985..c3e38e3f1 100644 --- a/src/api/z3.h +++ b/src/api/z3.h @@ -25,6 +25,7 @@ Notes: #include"z3_macros.h" #include"z3_api.h" #include"z3_algebraic.h" +#include"z3_polynomial.h" #undef __in #undef __out diff --git a/src/api/z3_polynomial.h b/src/api/z3_polynomial.h new file mode 100644 index 000000000..614e654f9 --- /dev/null +++ b/src/api/z3_polynomial.h @@ -0,0 +1,45 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + z3_polynomial.h + +Abstract: + + Additional APIs for polynomials. + +Author: + + Leonardo de Moura (leonardo) 2012-12-09 + +Notes: + +--*/ + +#ifndef _Z3_POLYNOMIAL_H_ +#define _Z3_POLYNOMIAL_H_ + +#ifdef __cplusplus +extern "C" { +#endif // __cplusplus + + /** + \brief Return the nonzero subresultants of \c p and \c q with respect to the "variable" \c x. + + \pre \c p, \c q and \c x are Z3 expressions where \c p and \c q are arithmetic terms. + Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable. + Example: f(a) is a considered to be a variable in the polynomial + + f(a)*f(a) + 2*f(a) + 1 + + def_API('Z3_polynomial_subresultants', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + */ + Z3_ast_vector Z3_API Z3_polynomial_subresultants(__in Z3_context c, __in Z3_ast p, __in Z3_ast q, __in Z3_ast x); + + +#ifdef __cplusplus +}; +#endif // __cplusplus + +#endif diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h index 7cefe6f56..d17d2ac5a 100644 --- a/src/math/polynomial/polynomial.h +++ b/src/math/polynomial/polynomial.h @@ -219,6 +219,7 @@ namespace polynomial { void set_zp(uint64 p); void set_cancel(bool f); + void cancel() { set_cancel(true); } /** \brief Abstract event handler.