From: Vivien Maisonneuve Date: Thu, 17 Jul 2014 16:12:32 +0000 (+0200) Subject: Implement standard widening X-Git-Tag: 1.0~97 X-Git-Url: https://scm.cri.mines-paristech.fr/git/linpy.git/commitdiff_plain/82e100a9d5e7db532fda649849dc784148e55069?ds=inline;hp=c8a857e117e2f99120b450f8fd08e20c9da78ec8 Implement standard widening --- 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'