1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 z3_polynomial.h 7 8 Abstract: 9 10 Additional APIs for polynomials. 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2012-12-09 15 16 Notes: 17 18 --*/ 19 20 #pragma once 21 22 #ifdef __cplusplus 23 extern "C" { 24 #endif // __cplusplus 25 26 /** \defgroup capi C API */ 27 /*@{*/ 28 29 30 /** @name Polynomials */ 31 /*@{*/ 32 33 /** 34 \brief Return the nonzero subresultants of \c p and \c q with respect to the "variable" \c x. 35 36 \pre \c p, \c q and \c x are Z3 expressions where \c p and \c q are arithmetic terms. 37 Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable. 38 Example: \ccode{f(a)} is a considered to be a variable in the polynomial \ccode{ 39 f(a)*f(a) + 2*f(a) + 1} 40 41 def_API('Z3_polynomial_subresultants', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(AST))) 42 */ 43 Z3_ast_vector Z3_API Z3_polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x); 44 45 46 /*@}*/ 47 /*@}*/ 48 49 #ifdef __cplusplus 50 } 51 #endif // __cplusplus 52 53