Implement standard widening

[linpy.git] / pypol / polyhedra.py

diff --git a/pypol/polyhedra.py b/pypol/polyhedra.py
index f8d413e..ccb1a8c 100644 (file)
--- a/pypol/polyhedra.py
+++ b/pypol/polyhedra.py
@@ -112,6 +112,31 @@ class Polyhedron(Domain):
             for inequality in self.inequalities]
         return Polyhedron(equalities, inequalities)
 
+    def _asinequalities(self):
+        inequalities = list(self.equalities)
+        inequalities.extend([-expression for expression in self.equalities])
+        inequalities.extend(self.inequalities)
+        return inequalities
+
+    def widen(self, other):
+        if not isinstance(other, Polyhedron):
+            raise ValueError('argument must be a Polyhedron instance')
+        inequalities1 = self._asinequalities()
+        inequalities2 = other._asinequalities()
+        inequalities = []
+        for inequality1 in inequalities1:
+            if other <= Polyhedron(inequalities=[inequality1]):
+                inequalities.append(inequality1)
+        for inequality2 in inequalities2:
+            for i in range(len(inequalities1)):
+                inequalities3 = inequalities1[:i] + inequalities[i + 1:]
+                inequalities3.append(inequality2)
+                polyhedron3 = Polyhedron(inequalities=inequalities3)
+                if self == polyhedron3:
+                    inequalities.append(inequality2)
+                    break
+        return Polyhedron(inequalities=inequalities)
+
     @classmethod
     def _fromislbasicset(cls, islbset, symbols):
         if libisl.isl_basic_set_is_empty(islbset):
@@ -236,6 +261,11 @@ class EmptyType(Polyhedron):
         self._dimension = 0
         return self
 
+    def widen(self, other):
+        if not isinstance(other, Polyhedron):
+            raise ValueError('argument must be a Polyhedron instance')
+        return other
+
     def __repr__(self):
         return 'Empty'