From 10808766a204fcc854ae30fe471ada80bab1f60f Mon Sep 17 00:00:00 2001
From: Vivien Maisonneuve <v.maisonneuve@gmail.com>
Date: Wed, 2 Jul 2014 10:31:27 +0200
Subject: [PATCH] New example: basic implementation of ACI'10

---
 examples/nsad2010.py | 53 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)
 create mode 100755 examples/nsad2010.py

diff --git a/examples/nsad2010.py b/examples/nsad2010.py
new file mode 100755
index 0000000..14c984c
--- /dev/null
+++ b/examples/nsad2010.py
@@ -0,0 +1,53 @@
+#!/usr/bin/env python3
+
+from pypol import *
+
+def affine_derivative_closure(T, x0s):
+
+    xs = [Symbol("{}'".format(x0.name)) for x0 in x0s]
+    dxs = [Symbol('d{}'.format(x0.name)) for x0 in x0s]
+    k = Symbol('k')
+
+    for x in T.symbols:
+        x = Symbol(x)
+        assert x in x0s + xs
+    for dx in dxs:
+        assert dx.name not in T.symbols
+    assert k.name not in T.symbols
+
+    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])
+print('T* =', Tstar)
-- 
2.20.1