/usr/lib/python2.7/dist-packages/z3poly.py is in python-z3 4.4.1-0.3build4.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 | ############################################
# 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)
|