From: Vivien Maisonneuve Date: Thu, 3 Jul 2014 09:43:04 +0000 (+0200) Subject: Better implementation of NSAD'10 example X-Git-Tag: 1.0~156 X-Git-Url: https://scm.cri.ensmp.fr/git/linpy.git/commitdiff_plain/90d7f21ee1486524f499f66ef546a24331b2009c Better implementation of NSAD'10 example --- diff --git a/examples/nsad2010.py b/examples/nsad2010.py index 1bf97d8..8194618 100755 --- a/examples/nsad2010.py +++ b/examples/nsad2010.py @@ -2,47 +2,45 @@ from pypol import * -def affine_derivative_closure(T, x0s, xs): - - dxs = [x0.asdummy() for x0 in x0s] - k = Dummy('k') - - for x in T.symbols: - assert x in x0s + xs - - T0 = T - - T1 = T0 - for i, x0 in enumerate(x0s): - x, dx = xs[i], dxs[i] - T1 &= Eq(dx, x - x0) - - T2 = T1.project_out(T0.symbols) - - T3_eqs = [] - T3_ins = [] - for T2_eq in T2.equalities: - c = T2_eq.constant - T3_eq = T2_eq + (k - 1) * c - T3_eqs.append(T3_eq) - for T2_in in T2.inequalities: - c = T2_in.constant - T3_in = T2_in + (k - 1) * c - T3_ins.append(T3_in) - T3 = Polyhedron(T3_eqs, T3_ins) - T3 &= Ge(k, 0) - - T4 = T3.project_out([k]) - for i, dx in enumerate(dxs): - x0, x = x0s[i], xs[i] - T4 &= Eq(dx, x - x0) - T4 = T4.project_out(dxs) - - return T4 - -i0, j0, i, j = symbols(['i', 'j', "i'", "j'"]) -T = Eq(i, i0 + 2) & Eq(j, j0 + 1) - -print('T =', T) -Tstar = affine_derivative_closure(T, [i0, j0], [i, j]) -print('T* =', Tstar) + +class Transformer: + + def __new__(cls, polyhedron, range_symbols, domain_symbols): + self = object().__new__(cls) + self.polyhedron = polyhedron + self.range_symbols = range_symbols + self.domain_symbols = domain_symbols + return self + + @property + def symbols(self): + return self.range_symbols + self.domain_symbols + + def star(self): + delta_symbols = [symbol.asdummy() for symbol in self.range_symbols] + k = Dummy('k') + polyhedron = self.polyhedron + for x, xprime, dx in zip(self.range_symbols, self.domain_symbols, delta_symbols): + polyhedron &= Eq(dx, xprime - x) + polyhedron = polyhedron.project_out(self.symbols) + equalities, inequalities = [], [] + for equality in polyhedron.equalities: + equality += (k-1) * equality.constant + equalities.append(equality) + for inequality in polyhedron.inequalities: + inequality += (k-1) * inequality.constant + inequalities.append(inequality) + polyhedron = Polyhedron(equalities, inequalities) & Ge(k, 0) + polyhedron = polyhedron.project_out([k]) + for x, xprime, dx in zip(self.range_symbols, self.domain_symbols, delta_symbols): + polyhedron &= Eq(dx, xprime - x) + polyhedron = polyhedron.project_out(delta_symbols) + return Transformer(polyhedron, self.range_symbols, self.domain_symbols) + + +if __name__ == '__main__': + i, iprime, j, jprime = symbols("i i' j j'") + transformer = Transformer(Eq(iprime, i + 2) & Eq(jprime, j + 1), + [i, j], [iprime, jprime]) + print('T =', transformer.polyhedron) + print('T* =', transformer.star().polyhedron)