From 82e100a9d5e7db532fda649849dc784148e55069 Mon Sep 17 00:00:00 2001
From: Vivien Maisonneuve <v.maisonneuve@gmail.com>
Date: Thu, 17 Jul 2014 18:12:32 +0200
Subject: [PATCH] Implement standard widening
---
pypol/polyhedra.py | 30 ++++++++++++++++++++++++++++++
1 file changed, 30 insertions(+)
diff --git a/pypol/polyhedra.py b/pypol/polyhedra.py
index f8d413e..ccb1a8c 100644
--- 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'
--
2.20.1