From: Danielle Bolan Date: Thu, 3 Jul 2014 15:17:45 +0000 (+0200) Subject: Add methods may be useful for larger polys, change format of printing X-Git-Tag: 1.0~155 X-Git-Url: https://scm.cri.ensmp.fr/git/linpy.git/commitdiff_plain/fb070deb31a82b789e1be4ffc5dfa64b4b7a9e36?ds=inline;hp=90d7f21ee1486524f499f66ef546a24331b2009c Add methods may be useful for larger polys, change format of printing --- diff --git a/examples/squares.py b/examples/squares.py index 6bc352a..0df8b4b 100755 --- a/examples/squares.py +++ b/examples/squares.py @@ -11,22 +11,23 @@ sq4 = Le(1, x) & Le(x, 2) & Le(1, y) & Le(y, 2) sq5 = Le(1, x) & Le(x, 2) & Le(1, y) sq6 = Le(1, x) & Le(x, 2) & Le(1, y) & Eq(y, 3) sq7 = Le(0, x) & Le(x, 2) & Le(0, y) & Eq(z, 2) & Le(a, 3) -u = Polyhedron([]) -x = sq1 - sq2 +universe = Polyhedron([]) +q = sq1 - sq2 +e = Empty print('sq1 =', sq1) #print correct square print('sq2 =', sq2) #print correct square print('sq3 =', sq3) #print correct square print('sq4 =', sq4) #print correct square -print('u =', u) #print correct square +print('universe =', universe) #print correct square print() print('¬sq1 =', ~sq1) #test complement print() print('sq1 + sq1 =', sq1 + sq2) #test addition print('sq1 + sq2 =', Polyhedron(sq1 + sq2)) #test addition print() -print('u + u =', u + u)#test addition -print('u - u =', u - u) #test subtraction +print('universe + universe =', universe + universe)#test addition +print('universe - universe =', universe - universe) #test subtraction print() print('sq2 - sq1 =', sq2 - sq1) #test subtraction print('sq2 - sq1 =', Polyhedron(sq2 - sq1)) #test subtraction @@ -43,7 +44,7 @@ print('sq1 disjoint:', sq1.disjoint()) #make disjoint print('sq2 disjoint:', sq2.disjoint()) #make disjoint print() print('is square 1 universe?:', sq1.isuniverse()) #test if square is universe -print('is u universe?:', u.isuniverse()) #test if square is universe +print('is u universe?:', universe.isuniverse()) #test if square is universe print() print('is sq1 a subset of sq2?:', sq1.issubset(sq2)) #test issubset() print('is sq4 less than sq3?:', sq4.__lt__(sq3)) # test lt(), must be a strict subset @@ -54,8 +55,7 @@ print() print('lexographic min of sq2:', sq2.lexmin()) #test lexmax() print('lexographic max of sq2:', sq2.lexmax()) #test lexmax() print() -print('Polyhedral hull of sq1 + sq2 is:', x.polyhedral_hull()) #test polyhedral hull, returns same - #value as Polyhedron(sq1 + sq2) +print('Polyhedral hull of sq1 + sq2 is:', q.polyhedral_hull()) #test polyhedral hull print() print('is sq1 bounded?', sq1.isbounded()) #unbounded should return True print('is sq5 bounded?', sq5.isbounded()) #unbounded should return False @@ -63,5 +63,9 @@ print() print('sq6:', sq6) print('sq6 simplified:', sq6.sample()) print() -#print(u.drop_dims(' ')) -print('sq7 with out constraints involving y and a', sq7.project_out([y, a])) #drops dims that are passed +print(universe.project_out([x])) +print('sq7 with out constraints involving y and a', sq7.project_out([a, z, x, y])) #drops dims that are passed +print() +print('sq1 has {} parameters'.format(sq1.num_parameters())) +print() +print('does sq1 constraints involve x?', sq1.involves_dims([x])) diff --git a/pypol/domains.py b/pypol/domains.py index 224ac5f..a2650e4 100644 --- a/pypol/domains.py +++ b/pypol/domains.py @@ -152,20 +152,20 @@ class Domain: islbset = libisl.isl_set_polyhedral_hull(islset) return Polyhedron._fromislbasicset(islbset, self.symbols) - def project_out(self, symbols): + def project_out(self, dims): # use to remove certain variables islset = self._toislset(self.polyhedra, self.symbols) n = 0 for index, symbol in reversed(list(enumerate(self.symbols))): - if symbol in symbols: + if symbol in dims: n += 1 elif n > 0: islset = libisl.isl_set_project_out(islset, libisl.isl_dim_set, index + 1, n) n = 0 if n > 0: islset = libisl.isl_set_project_out(islset, libisl.isl_dim_set, 0, n) - symbols = [symbol for symbol in self.symbols if symbol not in symbols] - return Domain._fromislset(islset, symbols) + dims = [symbol for symbol in self.symbols if symbol not in dims] + return Domain._fromislset(islset, dims) def sample(self): from .polyhedra import Polyhedron @@ -221,6 +221,31 @@ class Domain: islset = self._toislset(self.polyhedra, self.symbols) islset = libisl.isl_set_lexmax(islset) return self._fromislset(islset, self.symbols) + + def num_parameters(self): + #could be useful with large, complicated polyhedrons + islbset = self._toislbasicset(self.equalities, self.inequalities, self.symbols) + num = libisl.isl_basic_set_dim(islbset, libisl.isl_dim_set) + return num + + def involves_dims(self, dims): + #could be useful with large, complicated polyhedrons + islset = self._toislset(self.polyhedra, self.symbols) + dims = sorted(dims) + symbols = sorted(list(self.symbols)) + n = 0 + if len(dims)>0: + for dim in dims: + if dim in symbols: + first = symbols.index(dims[0]) + n +=1 + else: + first = 0 + else: + return False + value = bool(libisl.isl_set_involves_dims(islset, libisl.isl_dim_set, first, n)) + libisl.isl_set_free(islset) + return value @classmethod def _fromislset(cls, islset, symbols): diff --git a/pypol/polyhedra.py b/pypol/polyhedra.py index 6b44bdc..7181565 100644 --- a/pypol/polyhedra.py +++ b/pypol/polyhedra.py @@ -84,7 +84,7 @@ class Polyhedron(Domain): def polyhedral_hull(self): return self - + @classmethod def _fromislbasicset(cls, islbset, symbols): islconstraints = islhelper.isl_basic_set_constraints(islbset) @@ -164,9 +164,9 @@ class Polyhedron(Domain): else: strings = [] for equality in self.equalities: - strings.append('Eq({}, 0)'.format(equality)) + strings.append('0 == {}'.format(equality)) for inequality in self.inequalities: - strings.append('Ge({}, 0)'.format(inequality)) + strings.append('0 <= {}'.format(inequality)) if len(strings) == 1: return strings[0] else: diff --git a/pypol/tests/test_domains.py b/pypol/tests/test_domains.py index df7b01c..4d38075 100644 --- a/pypol/tests/test_domains.py +++ b/pypol/tests/test_domains.py @@ -38,10 +38,13 @@ class TestDomain(unittest.TestCase): def test_disjoint(self): self.assertEqual(self.square1.disjoint(), self.disjoint) + self.assertEqual(self.empty.disjoint(), Empty) + self.assertEqual(self.universe.disjoint(), self.universe) def test_isempty(self): self.assertFalse(self.square1.isempty()) self.assertTrue(self.empty.isempty()) + self.assertFalse(self.universe.isempty()) def test_isuniverse(self): self.assertFalse(self.square1.isuniverse()) @@ -54,6 +57,7 @@ class TestDomain(unittest.TestCase): def test_eq(self): self.assertTrue(self.square1 == self.square1) self.assertFalse(self.square1 == self.square2) + self.assertFalse(self.empty == self.universe) def test_isdisjoint(self): self.assertFalse(self.square1.isdisjoint(self.square2)) @@ -147,3 +151,13 @@ class TestDomain(unittest.TestCase): self.assertEqual(self.square1.lexmax(), self.lexmax) self.assertEqual(self.universe.lexmax(), self.universe) self.assertEqual(self.empty.lexmax(), Empty) + + def test_num_parameters(self): + self.assertEqual(self.square1.num_parameters(), 2) + self.assertEqual(self.empty.num_parameters(), 0) + self.assertEqual(self.universe.num_parameters(), 0) + + def test_involves_dims(self): + self.assertTrue(self.square1.involves_dims(symbols('x y'))) + self.assertFalse(self.empty.involves_dims(symbols('x'))) + self.assertFalse(self.universe.involves_dims(symbols('x'))) diff --git a/pypol/tests/test_polyhedra.py b/pypol/tests/test_polyhedra.py index cb2015f..7b8e033 100644 --- a/pypol/tests/test_polyhedra.py +++ b/pypol/tests/test_polyhedra.py @@ -20,11 +20,11 @@ class TestPolyhedron(unittest.TestCase): def test_str(self): self.assertEqual(str(self.square), - 'And(Ge(x, 0), Ge(-x + 1, 0), Ge(y, 0), Ge(-y + 1, 0))') + 'And(0 <= x, 0 <= -x + 1, 0 <= y, 0 <= -y + 1)') def test_repr(self): self.assertEqual(repr(self.square), - "And(Ge(x, 0), Ge(-x + 1, 0), Ge(y, 0), Ge(-y + 1, 0))") + "And(0 <= x, 0 <= -x + 1, 0 <= y, 0 <= -y + 1)") def test_fromstring(self): self.assertEqual(Polyhedron.fromstring('{x >= 0, -x + 1 >= 0, '