diff options
author | Kenji Hosokawa <khosokawa@jp.adit-jv.com> | 2021-09-27 17:23:10 +0900 |
---|---|---|
committer | Kenji Hosokawa <khosokawa@jp.adit-jv.com> | 2021-09-27 17:23:10 +0900 |
commit | 05417f782cb2377a4105969f910d2ed0416a8c47 (patch) | |
tree | 245300cbb1d501035de708ab93f174e7093c2f4c /tool_bin/lib/linux/z3/include/z3_polynomial.h | |
parent | 44a3da18a257cc46aa0dbfd01947deeb377ab049 (diff) |
push pre-built toolneedlefish_13.93.0needlefish/13.93.0marlin_12.93.0marlin_12.92.0marlin_12.91.0marlin_12.90.1marlin/12.93.0marlin/12.92.0marlin/12.91.0marlin/12.90.1lamprey_12.1.6lamprey_12.1.5lamprey_12.1.4lamprey_12.1.3lamprey_12.1.2lamprey_12.1.1lamprey_12.1.0lamprey/12.1.6lamprey/12.1.5lamprey/12.1.4lamprey/12.1.3lamprey/12.1.2lamprey/12.1.1lamprey/12.1.0koi_11.0.5koi/11.0.513.93.012.93.012.92.012.91.012.90.112.1.612.1.512.1.412.1.312.1.212.1.112.1.011.0.5
Signed-off-by: Kenji Hosokawa <khosokawa@jp.adit-jv.com>
Diffstat (limited to 'tool_bin/lib/linux/z3/include/z3_polynomial.h')
-rw-r--r-- | tool_bin/lib/linux/z3/include/z3_polynomial.h | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/tool_bin/lib/linux/z3/include/z3_polynomial.h b/tool_bin/lib/linux/z3/include/z3_polynomial.h new file mode 100644 index 0000000..5f4815d --- /dev/null +++ b/tool_bin/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 |