diff options
author | Kenji Hosokawa <khosokawa@jp.adit-jv.com> | 2021-08-26 22:48:28 +0900 |
---|---|---|
committer | Kenji Hosokawa <khosokawa@jp.adit-jv.com> | 2021-08-26 22:58:27 +0900 |
commit | 44a3da18a257cc46aa0dbfd01947deeb377ab049 (patch) | |
tree | 854c7a5f1e1d671ddcccc7f1f60e55080e50ec43 /rba.tool.editor.endpoint/lib/linux/z3/bin/python/z3/z3poly.py | |
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/bin/python/z3/z3poly.py')
-rw-r--r-- | rba.tool.editor.endpoint/lib/linux/z3/bin/python/z3/z3poly.py | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/rba.tool.editor.endpoint/lib/linux/z3/bin/python/z3/z3poly.py b/rba.tool.editor.endpoint/lib/linux/z3/bin/python/z3/z3poly.py new file mode 100644 index 0000000..189310f --- /dev/null +++ b/rba.tool.editor.endpoint/lib/linux/z3/bin/python/z3/z3poly.py @@ -0,0 +1,35 @@ +############################################
+# 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)
|