1 #!/usr/bin/env python3
3 from pypol import *
5 def affine_derivative_closure(T, x0s):
7 xs = [Symbol("{}'".format(x0.name)) for x0 in x0s]
8 dxs = [Symbol('d{}'.format(x0.name)) for x0 in x0s]
9 k = Symbol('k')
11 for x in T.symbols:
12 assert x in x0s + xs
13 for dx in dxs:
14 assert dx.name not in T.symbols
15 assert k.name not in T.symbols
17 T0 = T
19 T1 = T0
20 for i, x0 in enumerate(x0s):
21 x, dx = xs[i], dxs[i]
22 T1 &= Eq(dx, x - x0)
24 T2 = T1.project_out(T0.symbols)
26 T3_eqs = []
27 T3_ins = []
28 for T2_eq in T2.equalities:
29 c = T2_eq.constant
30 T3_eq = T2_eq + (k - 1) * c
31 T3_eqs.append(T3_eq)
32 for T2_in in T2.inequalities:
33 c = T2_in.constant
34 T3_in = T2_in + (k - 1) * c
35 T3_ins.append(T3_in)
36 T3 = Polyhedron(T3_eqs, T3_ins)
37 T3 &= Ge(k, 0)
39 T4 = T3.project_out([k])
40 for i, dx in enumerate(dxs):
41 x0, x = x0s[i], xs[i]
42 T4 &= Eq(dx, x - x0)
43 T4 = T4.project_out(dxs)
45 return T4
47 i0, j0, i, j = symbols(['i', 'j', "i'", "j'"])
48 T = Eq(i, i0 + 2) & Eq(j, j0 + 1)
50 print('T =', T)
51 Tstar = affine_derivative_closure(T, [i0, j0])
52 print('T* =', Tstar)