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