3 import ctypes
, ctypes
.util
5 from fractions
import Fraction
, gcd
7 from . import isl
, islhelper
10 libisl
= ctypes
.CDLL(ctypes
.util
.find_library('isl'))
12 libisl
.isl_printer_get_str
.restype
= ctypes
.c_char_p
16 'constant', 'symbol', 'symbols',
17 'eq', 'le', 'lt', 'ge', 'gt',
23 def symbolToInt(self):
24 make dictionary of key:value (letter:integer)
25 iterate through the dictionary to find matching symbol
26 return the given integer value
27 d = {'a': 1, 'b': 2, 'c': 3, 'd': 4, 'e': 5, 'f': 6, 'g': 7, 'h': 8, 'i': 6, 'j': 10, 'k': 11, 'l': 12, 'm': 13, 'n': 14,
28 'o': 15, 'p': 16, 'q': 17, 'r': 18, 's': 19, 't': 20, 'u': 21, 'v': 22, 'w': 23, 'x': 24, 'y': 25, 'z': 26}
45 def _polymorphic_method(func
):
46 @functools.wraps(func
)
48 if isinstance(b
, Expression
):
50 if isinstance(b
, numbers
.Rational
):
56 def _polymorphic_operator(func
):
57 # A polymorphic operator should call a polymorphic method, hence we just
58 # have to test the left operand.
59 @functools.wraps(func
)
61 if isinstance(a
, numbers
.Rational
):
64 elif isinstance(a
, Expression
):
66 raise TypeError('arguments must be linear expressions')
74 self
._ic
= libisl
.isl_ctx_alloc()
77 def _as_parameter_(self
):
80 #comment out so does not delete itself after being created
82 # libisl.isl_ctx_free(self)
84 def __eq__(self
, other
):
85 if not isinstance(other
, Context
):
87 return self
._ic
== other
._ic
94 This class implements linear expressions.
97 def __new__(cls
, coefficients
=None, constant
=0):
98 if isinstance(coefficients
, str):
100 raise TypeError('too many arguments')
101 return cls
.fromstring(coefficients
)
102 self
= super().__new
__(cls
)
103 self
._coefficients
= {}
104 if isinstance(coefficients
, dict):
105 coefficients
= coefficients
.items()
106 if coefficients
is not None:
107 for symbol
, coefficient
in coefficients
:
108 if isinstance(symbol
, Expression
) and symbol
.issymbol():
110 elif not isinstance(symbol
, str):
111 raise TypeError('symbols must be strings')
112 if not isinstance(coefficient
, numbers
.Rational
):
113 raise TypeError('coefficients must be rational numbers')
115 self
._coefficients
[symbol
] = coefficient
116 if not isinstance(constant
, numbers
.Rational
):
117 raise TypeError('constant must be a rational number')
118 self
._constant
= constant
123 yield from sorted(self
._coefficients
)
127 return len(list(self
.symbols()))
129 def coefficient(self
, symbol
):
130 if isinstance(symbol
, Expression
) and symbol
.issymbol():
132 elif not isinstance(symbol
, str):
133 raise TypeError('symbol must be a string')
135 return self
._coefficients
[symbol
]
139 __getitem__
= coefficient
141 def coefficients(self
):
142 for symbol
in self
.symbols():
143 yield symbol
, self
.coefficient(symbol
)
147 return self
._constant
149 def isconstant(self
):
150 return len(self
._coefficients
) == 0
153 for symbol
in self
.symbols():
154 yield self
.coefficient(symbol
)
157 def values_int(self
):
158 for symbol
in self
.symbols():
159 return self
.coefficient(symbol
)
160 return int(self
.constant
)
164 if not self
.issymbol():
165 raise ValueError('not a symbol: {}'.format(self
))
166 for symbol
in self
.symbols():
170 return len(self
._coefficients
) == 1 and self
._constant
== 0
173 return (not self
.isconstant()) or bool(self
.constant
)
182 def __add__(self
, other
):
183 coefficients
= dict(self
.coefficients())
184 for symbol
, coefficient
in other
.coefficients():
185 if symbol
in coefficients
:
186 coefficients
[symbol
] += coefficient
188 coefficients
[symbol
] = coefficient
189 constant
= self
.constant
+ other
.constant
190 return Expression(coefficients
, constant
)
195 def __sub__(self
, other
):
196 coefficients
= dict(self
.coefficients())
197 for symbol
, coefficient
in other
.coefficients():
198 if symbol
in coefficients
:
199 coefficients
[symbol
] -= coefficient
201 coefficients
[symbol
] = -coefficient
202 constant
= self
.constant
- other
.constant
203 return Expression(coefficients
, constant
)
205 def __rsub__(self
, other
):
206 return -(self
- other
)
209 def __mul__(self
, other
):
210 if other
.isconstant():
211 coefficients
= dict(self
.coefficients())
212 for symbol
in coefficients
:
213 coefficients
[symbol
] *= other
.constant
214 constant
= self
.constant
* other
.constant
215 return Expression(coefficients
, constant
)
216 if isinstance(other
, Expression
) and not self
.isconstant():
217 raise ValueError('non-linear expression: '
218 '{} * {}'.format(self
._parenstr
(), other
._parenstr
()))
219 return NotImplemented
224 def __truediv__(self
, other
):
225 if other
.isconstant():
226 coefficients
= dict(self
.coefficients())
227 for symbol
in coefficients
:
228 coefficients
[symbol
] = \
229 Fraction(coefficients
[symbol
], other
.constant
)
230 constant
= Fraction(self
.constant
, other
.constant
)
231 return Expression(coefficients
, constant
)
232 if isinstance(other
, Expression
):
233 raise ValueError('non-linear expression: '
234 '{} / {}'.format(self
._parenstr
(), other
._parenstr
()))
235 return NotImplemented
237 def __rtruediv__(self
, other
):
238 if isinstance(other
, self
):
239 if self
.isconstant():
240 constant
= Fraction(other
, self
.constant
)
241 return Expression(constant
=constant
)
243 raise ValueError('non-linear expression: '
244 '{} / {}'.format(other
._parenstr
(), self
._parenstr
()))
245 return NotImplemented
249 symbols
= sorted(self
.symbols())
251 for symbol
in symbols
:
252 coefficient
= self
[symbol
]
257 string
+= ' + {}'.format(symbol
)
258 elif coefficient
== -1:
260 string
+= '-{}'.format(symbol
)
262 string
+= ' - {}'.format(symbol
)
265 string
+= '{}*{}'.format(coefficient
, symbol
)
266 elif coefficient
> 0:
267 string
+= ' + {}*{}'.format(coefficient
, symbol
)
269 assert coefficient
< 0
271 string
+= ' - {}*{}'.format(coefficient
, symbol
)
273 constant
= self
.constant
274 if constant
!= 0 and i
== 0:
275 string
+= '{}'.format(constant
)
277 string
+= ' + {}'.format(constant
)
280 string
+= ' - {}'.format(constant
)
285 def _parenstr(self
, always
=False):
287 if not always
and (self
.isconstant() or self
.issymbol()):
290 return '({})'.format(string
)
293 string
= '{}({{'.format(self
.__class
__.__name
__)
294 for i
, (symbol
, coefficient
) in enumerate(self
.coefficients()):
297 string
+= '{!r}: {!r}'.format(symbol
, coefficient
)
298 string
+= '}}, {!r})'.format(self
.constant
)
302 def fromstring(cls
, string
):
303 raise NotImplementedError
306 def __eq__(self
, other
):
308 # see http://docs.sympy.org/dev/tutorial/gotchas.html#equals-signs
309 return isinstance(other
, Expression
) and \
310 self
._coefficients
== other
._coefficients
and \
311 self
.constant
== other
.constant
314 return hash((self
._coefficients
, self
._constant
))
317 lcm
= functools
.reduce(lambda a
, b
: a
*b
// gcd(a
, b
),
318 [value
.denominator
for value
in self
.values()])
322 def _eq(self
, other
):
323 return Polyhedron(equalities
=[(self
- other
)._canonify
()])
326 def __le__(self
, other
):
327 return Polyhedron(inequalities
=[(self
- other
)._canonify
()])
330 def __lt__(self
, other
):
331 return Polyhedron(inequalities
=[(self
- other
)._canonify
() + 1])
334 def __ge__(self
, other
):
335 return Polyhedron(inequalities
=[(other
- self
)._canonify
()])
338 def __gt__(self
, other
):
339 return Polyhedron(inequalities
=[(other
- self
)._canonify
() + 1])
342 def constant(numerator
=0, denominator
=None):
343 if denominator
is None and isinstance(numerator
, numbers
.Rational
):
344 return Expression(constant
=3)
346 return Expression(constant
=Fraction(numerator
, denominator
))
349 if not isinstance(name
, str):
350 raise TypeError('name must be a string')
351 return Expression(coefficients
={name
: 1})
354 if isinstance(names
, str):
355 names
= names
.replace(',', ' ').split()
356 return (symbol(name
) for name
in names
)
359 @_polymorphic_operator
363 @_polymorphic_operator
367 @_polymorphic_operator
371 @_polymorphic_operator
375 @_polymorphic_operator
382 This class implements polyhedrons.
385 def __new__(cls
, equalities
=None, inequalities
=None):
386 if isinstance(equalities
, str):
387 if inequalities
is not None:
388 raise TypeError('too many arguments')
389 return cls
.fromstring(equalities
)
390 self
= super().__new
__(cls
)
391 self
._equalities
= []
392 if equalities
is not None:
393 for constraint
in equalities
:
394 for value
in constraint
.values():
395 if value
.denominator
!= 1:
396 raise TypeError('non-integer constraint: '
397 '{} == 0'.format(constraint
))
398 self
._equalities
.append(constraint
)
399 self
._inequalities
= []
400 if inequalities
is not None:
401 for constraint
in inequalities
:
402 for value
in constraint
.values():
403 if value
.denominator
!= 1:
404 raise TypeError('non-integer constraint: '
405 '{} <= 0'.format(constraint
))
406 self
._inequalities
.append(constraint
)
407 self
._bset
= self
.to_isl()
409 #put this here just to test from isl method
410 #from_isl = self.from_isl(self._bset)
417 def equalities(self
):
418 yield from self
._equalities
421 def inequalities(self
):
422 yield from self
._inequalities
426 return self
._constant
428 def isconstant(self
):
429 return len(self
._coefficients
) == 0
433 return bool(libisl
.isl_basic_set_is_empty(self
._bset
))
435 def constraints(self
):
436 yield from self
.equalities
437 yield from self
.inequalities
442 for constraint
in self
.constraints():
443 s
.update(constraint
.symbols
)
448 return len(self
.symbols())
451 # return false if the polyhedron is empty, true otherwise
452 if self
._equalities
or self
._inequalities
:
458 def __contains__(self
, value
):
459 # is the value in the polyhedron?
460 raise NotImplementedError
462 def __eq__(self
, other
):
463 raise NotImplementedError
468 def isuniverse(self
):
469 return self
== universe
471 def isdisjoint(self
, other
):
472 # return true if the polyhedron has no elements in common with other
473 raise NotImplementedError
475 def issubset(self
, other
):
476 raise NotImplementedError
478 def __le__(self
, other
):
479 return self
.issubset(other
)
481 def __lt__(self
, other
):
482 raise NotImplementedError
484 def issuperset(self
, other
):
485 # test whether every element in other is in the polyhedron
487 if value
== self
.constraints():
491 raise NotImplementedError
493 def __ge__(self
, other
):
494 return self
.issuperset(other
)
496 def __gt__(self
, other
):
497 raise NotImplementedError
499 def union(self
, *others
):
500 # return a new polyhedron with elements from the polyhedron and all
501 # others (convex union)
502 raise NotImplementedError
504 def __or__(self
, other
):
505 return self
.union(other
)
507 def intersection(self
, *others
):
508 # return a new polyhedron with elements common to the polyhedron and all
510 # a poor man's implementation could be:
511 # equalities = list(self.equalities)
512 # inequalities = list(self.inequalities)
513 # for other in others:
514 # equalities.extend(other.equalities)
515 # inequalities.extend(other.inequalities)
516 # return self.__class__(equalities, inequalities)
517 raise NotImplementedError
519 def __and__(self
, other
):
520 return self
.intersection(other
)
522 def difference(self
, *others
):
523 # return a new polyhedron with elements in the polyhedron that are not
525 raise NotImplementedError
527 def __sub__(self
, other
):
528 return self
.difference(other
)
532 for constraint
in self
.equalities
:
533 constraints
.append('{} == 0'.format(constraint
))
534 for constraint
in self
.inequalities
:
535 constraints
.append('{} <= 0'.format(constraint
))
536 return '{{{}}}'.format(', '.join(constraints
))
539 equalities
= list(self
.equalities
)
540 inequalities
= list(self
.inequalities
)
541 return '{}(equalities={!r}, inequalities={!r})' \
542 ''.format(self
.__class
__.__name
__, equalities
, inequalities
)
545 def fromstring(cls
, string
):
546 raise NotImplementedError
549 #d = Expression().__dict__ #write expression values to dictionary in form {'_constant': value, '_coefficients': value}
550 d
= {'_constant': 2, '_coefficients': {'b':1}}
551 coeff
= d
.get('_coefficients')
552 num_coefficients
= len(coeff
)
553 space
= libisl
.isl_space_set_alloc(Context(), 0, num_coefficients
)
554 bset
= libisl
.isl_basic_set_empty(libisl
.isl_space_copy(space
))
555 ls
= libisl
.isl_local_space_from_space(libisl
.isl_space_copy(space
))
556 ceq
= libisl
.isl_equality_alloc(libisl
.isl_local_space_copy(ls
))
557 cin
= libisl
.isl_inequality_alloc(libisl
.isl_local_space_copy(ls
))
558 '''if there are equalities/inequalities, take each constant and coefficient and add as a constraint to the basic set
559 need to change the symbols method to a lookup table for the integer value for each letter that could be a symbol'''
562 value
= d
.get('_constant')
563 ceq
= libisl
.isl_constraint_set_constant_si(ceq
, value
)
564 if '_coefficients' in d
:
565 value_co
= d
.get('_coefficients')
567 num
= value_co
.get(co
)
568 ceq
= libisl
.isl_constraint_set_coefficient_si(ceq
, islhelper
.isl_dim_set
, get_ids(co
), num
)
569 bset
= libisl
.isl_set_add_constraint(bset
, ceq
)
571 if self
._inequalities
:
573 value
= d
.get('_constant')
574 cin
= libisl
.isl_constraint_set_constant_si(cin
, value
)
575 if '_coefficients' in d
:
576 value_co
= d
.get('_coefficients')
578 num
= value_co
.get(co
)
579 if value_co
: #if dictionary not empty add coefficient as to constraint
580 cin
= libisl
.isl_constraint_set_coefficient_si(cin
, islhelper
.isl_dim_set
, get_ids(co
), num
)
581 bset
= libisl
.isl_set_add_constraint(bset
, cin
)
582 ip
= libisl
.isl_printer_to_str(Context()) #create string printer
583 ip
= libisl
.isl_printer_print_set(ip
, bset
) #print set to printer
584 string
= libisl
.isl_printer_get_str(ip
) #get string from printer
590 def from_isl(self
, bset
):
591 '''takes basic set in isl form and puts back into python version of polyhedron
592 isl example code gives idl form as:
593 "{[i] : exists (a : i = 2a and i >= 10 and i <= 42)}");'''
601 universe
= Polyhedron()