diff options
author | 2021-08-26 22:48:28 +0900 | |
---|---|---|
committer | 2021-08-26 22:58:27 +0900 | |
commit | 44a3da18a257cc46aa0dbfd01947deeb377ab049 (patch) | |
tree | 854c7a5f1e1d671ddcccc7f1f60e55080e50ec43 /rba.tool.editor.endpoint/lib/linux/z3/include/z3_polynomial.h | |
parent | 6166bddbc4c94c4e0da3c884e1a592dfa1faa4ad (diff) |
include dependent packagelamprey_12.0.1lamprey/12.0.1koi_11.0.4koi/11.0.412.0.111.0.4
Signed-off-by: Kenji Hosokawa <khosokawa@jp.adit-jv.com>
Diffstat (limited to 'rba.tool.editor.endpoint/lib/linux/z3/include/z3_polynomial.h')
-rw-r--r-- | rba.tool.editor.endpoint/lib/linux/z3/include/z3_polynomial.h | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/rba.tool.editor.endpoint/lib/linux/z3/include/z3_polynomial.h b/rba.tool.editor.endpoint/lib/linux/z3/include/z3_polynomial.h new file mode 100644 index 0000000..5f4815d --- /dev/null +++ b/rba.tool.editor.endpoint/lib/linux/z3/include/z3_polynomial.h @@ -0,0 +1,54 @@ +/*++ +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 + + /** \defgroup capi C API */ + /*@{*/ + + + /** @name Polynomials */ + /*@{*/ + + /** + \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: \ccode{f(a)} is a considered to be a variable in the polynomial \ccode{ + 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(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x); + + + /*@}*/ + /*@}*/ + +#ifdef __cplusplus +} +#endif // __cplusplus + +#endif |