From: Vivien Maisonneuve <v.maisonneuve@gmail.com>
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)