From 161d0ced692386a866e55aea673d991e2e95f753 Mon Sep 17 00:00:00 2001
From: Vivien Maisonneuve <v.maisonneuve@gmail.com>
Date: Thu, 3 Jul 2014 10:19:39 +0200
Subject: [PATCH] Support for dummy symbols

---
 examples/nsad2010.py         | 12 ++++--------
 pypol/__init__.py            |  4 ++--
 pypol/linexprs.py            | 38 +++++++++++++++++++++++++++++++++---
 pypol/tests/test_linexprs.py | 17 ++++++++++++++++
 4 files changed, 58 insertions(+), 13 deletions(-)

diff --git a/examples/nsad2010.py b/examples/nsad2010.py
index e2cacc7..1bf97d8 100755
--- a/examples/nsad2010.py
+++ b/examples/nsad2010.py
@@ -2,17 +2,13 @@
 
 from pypol import *
 
-def affine_derivative_closure(T, x0s):
+def affine_derivative_closure(T, x0s, xs):
 
-    xs = [Symbol("{}'".format(x0.name)) for x0 in x0s]
-    dxs = [Symbol('d{}'.format(x0.name)) for x0 in x0s]
-    k = Symbol('k')
+    dxs = [x0.asdummy() for x0 in x0s]
+    k = Dummy('k')
 
     for x in T.symbols:
         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
 
@@ -48,5 +44,5 @@ 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])
+Tstar = affine_derivative_closure(T, [i0, j0], [i, j])
 print('T* =', Tstar)
diff --git a/pypol/__init__.py b/pypol/__init__.py
index 89f80fc..c81cb25 100644
--- a/pypol/__init__.py
+++ b/pypol/__init__.py
@@ -2,13 +2,13 @@
 A polyhedral library based on ISL.
 """
 
-from .linexprs import Expression, Symbol, symbols, Rational
+from .linexprs import Expression, Symbol, symbols, Dummy, Rational
 from .polyhedra import Polyhedron, Eq, Ne, Le, Lt, Ge, Gt, Ne, Empty, Universe
 from .domains import Domain, And, Or, Not
 
 
 __all__ = [
-    'Expression', 'Symbol', 'symbols', 'Rational',
+    'Expression', 'Symbol', 'symbols', 'Dummy', 'Rational',
     'Polyhedron', 'Eq', 'Ne', 'Le', 'Lt', 'Ge', 'Gt', 'Empty', 'Universe',
     'Domain', 'And', 'Or', 'Not',
 ]
diff --git a/pypol/linexprs.py b/pypol/linexprs.py
index 73c6b0e..f3cff23 100644
--- a/pypol/linexprs.py
+++ b/pypol/linexprs.py
@@ -9,7 +9,7 @@ from fractions import Fraction, gcd
 
 __all__ = [
     'Expression',
-    'Symbol', 'symbols',
+    'Symbol', 'symbols', 'Dummy',
     'Rational',
 ]
 
@@ -355,7 +355,7 @@ class Symbol(Expression):
         return self._name
 
     def __hash__(self):
-        return hash(self._name)
+        return hash(self.sortkey())
 
     def coefficient(self, symbol):
         if not isinstance(symbol, Symbol):
@@ -390,7 +390,11 @@ class Symbol(Expression):
         yield 1
 
     def __eq__(self, other):
-        return isinstance(other, Symbol) and self.name == other.name
+        return not isinstance(other, Dummy) and isinstance(other, Symbol) \
+            and self.name == other.name
+
+    def asdummy(self):
+        return Dummy(self.name)
 
     @classmethod
     def _fromast(cls, node):
@@ -417,6 +421,34 @@ def symbols(names):
     return tuple(Symbol(name) for name in names)
 
 
+class Dummy(Symbol):
+
+    __slots__ = (
+        '_name',
+        '_index',
+    )
+
+    _count = 0
+
+    def __new__(cls, name=None):
+        if name is None:
+            name = 'Dummy_{}'.format(Dummy._count)
+        self = object().__new__(cls)
+        self._name = name.strip()
+        self._index = Dummy._count
+        Dummy._count += 1
+        return self
+
+    def __hash__(self):
+        return hash(self.sortkey())
+
+    def sortkey(self):
+        return self._name, self._index
+
+    def __eq__(self, other):
+        return isinstance(other, Dummy) and self._index == other._index
+
+
 class Rational(Expression):
 
     __slots__ = (
diff --git a/pypol/tests/test_linexprs.py b/pypol/tests/test_linexprs.py
index adfec7d..508c57b 100644
--- a/pypol/tests/test_linexprs.py
+++ b/pypol/tests/test_linexprs.py
@@ -231,6 +231,23 @@ class TestSymbol(unittest.TestCase):
         self.assertListEqual(list(symbols(['x', 'y'])), [self.x, self.y])
 
 
+class TestDummy(unittest.TestCase):
+
+    def setUp(self):
+        self.x = Dummy('x')
+
+    def test_new(self):
+        self.assertEqual(self.x.name, 'x')
+        self.assertTrue(Dummy().name.startswith('Dummy'))
+
+    def test_eq(self):
+        self.assertEqual(self.x, self.x)
+        self.assertNotEqual(self.x, Symbol('x'))
+        self.assertNotEqual(Symbol('x'), self.x)
+        self.assertNotEqual(self.x, Dummy('x'))
+        self.assertNotEqual(Dummy(), Dummy())
+
+
 class TestRational(unittest.TestCase):
 
     def setUp(self):
-- 
2.20.1