From 82e100a9d5e7db532fda649849dc784148e55069 Mon Sep 17 00:00:00 2001 From: Vivien Maisonneuve 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