5dfddfe5ddbc47d884775a2d17e9db23a70379cf
4 import ctypes
, ctypes
.util
7 from fractions
import Fraction
, gcd
9 libisl
= ctypes
.CDLL(ctypes
.util
.find_library('isl'))
11 libisl
.isl_printer_get_str
.restype
= ctypes
.c_char_p
15 'constant', 'symbol', 'symbols',
16 'eq', 'le', 'lt', 'ge', 'gt',
22 def symbolToInt(self):
23 make dictionary of key:value (letter:integer)
24 iterate through the dictionary to find matching symbol
25 return the given integer value
26 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,
27 'o': 15, 'p': 16, 'q': 17, 'r': 18, 's': 19, 't': 20, 'u': 21, 'v': 22, 'w': 23, 'x': 24, 'y': 25, 'z': 26}
44 def _polymorphic_method(func
):
45 @functools.wraps(func
)
47 if isinstance(b
, Expression
):
49 if isinstance(b
, numbers
.Rational
):
55 def _polymorphic_operator(func
):
56 # A polymorphic operator should call a polymorphic method, hence we just
57 # have to test the left operand.
58 @functools.wraps(func
)
60 if isinstance(a
, numbers
.Rational
):
63 elif isinstance(a
, Expression
):
65 raise TypeError('arguments must be linear expressions')
73 self
._ic
= libisl
.isl_ctx_alloc()
76 def _as_parameter_(self
):
79 #comment out so does not delete itself after being created
81 # libisl.isl_ctx_free(self)
83 def __eq__(self
, other
):
84 if not isinstance(other
, Context
):
86 return self
._ic
== other
._ic
93 This class implements linear expressions.
96 def __new__(cls
, coefficients
=None, constant
=0):
97 if isinstance(coefficients
, str):
99 raise TypeError('too many arguments')
100 return cls
.fromstring(coefficients
)
101 self
= super().__new
__(cls
)
102 self
._coefficients
= {}
103 if isinstance(coefficients
, dict):
104 coefficients
= coefficients
.items()
105 if coefficients
is not None:
106 for symbol
, coefficient
in coefficients
:
107 if isinstance(symbol
, Expression
) and symbol
.issymbol():
109 elif not isinstance(symbol
, str):
110 raise TypeError('symbols must be strings')
111 if not isinstance(coefficient
, numbers
.Rational
):
112 raise TypeError('coefficients must be rational numbers')
114 self
._coefficients
[symbol
] = coefficient
115 if not isinstance(constant
, numbers
.Rational
):
116 raise TypeError('constant must be a rational number')
117 self
._constant
= constant
122 yield from sorted(self
._coefficients
)
126 return len(list(self
.symbols()))
128 def coefficient(self
, symbol
):
129 if isinstance(symbol
, Expression
) and symbol
.issymbol():
131 elif not isinstance(symbol
, str):
132 raise TypeError('symbol must be a string')
134 return self
._coefficients
[symbol
]
138 __getitem__
= coefficient
140 def coefficients(self
):
141 for symbol
in self
.symbols():
142 yield symbol
, self
.coefficient(symbol
)
146 return self
._constant
148 def isconstant(self
):
149 return len(self
._coefficients
) == 0
152 for symbol
in self
.symbols():
153 yield self
.coefficient(symbol
)
156 def values_int(self
):
157 for symbol
in self
.symbols():
158 return self
.coefficient(symbol
)
159 return int(self
.constant
)
163 if not self
.issymbol():
164 raise ValueError('not a symbol: {}'.format(self
))
165 for symbol
in self
.symbols():
169 return len(self
._coefficients
) == 1 and self
._constant
== 0
172 return (not self
.isconstant()) or bool(self
.constant
)
181 def __add__(self
, other
):
182 coefficients
= dict(self
.coefficients())
183 for symbol
, coefficient
in other
.coefficients():
184 if symbol
in coefficients
:
185 coefficients
[symbol
] += coefficient
187 coefficients
[symbol
] = coefficient
188 constant
= self
.constant
+ other
.constant
189 return Expression(coefficients
, constant
)
194 def __sub__(self
, other
):
195 coefficients
= dict(self
.coefficients())
196 for symbol
, coefficient
in other
.coefficients():
197 if symbol
in coefficients
:
198 coefficients
[symbol
] -= coefficient
200 coefficients
[symbol
] = -coefficient
201 constant
= self
.constant
- other
.constant
202 return Expression(coefficients
, constant
)
204 def __rsub__(self
, other
):
205 return -(self
- other
)
208 def __mul__(self
, other
):
209 if other
.isconstant():
210 coefficients
= dict(self
.coefficients())
211 for symbol
in coefficients
:
212 coefficients
[symbol
] *= other
.constant
213 constant
= self
.constant
* other
.constant
214 return Expression(coefficients
, constant
)
215 if isinstance(other
, Expression
) and not self
.isconstant():
216 raise ValueError('non-linear expression: '
217 '{} * {}'.format(self
._parenstr
(), other
._parenstr
()))
218 return NotImplemented
223 def __truediv__(self
, other
):
224 if other
.isconstant():
225 coefficients
= dict(self
.coefficients())
226 for symbol
in coefficients
:
227 coefficients
[symbol
] = \
228 Fraction(coefficients
[symbol
], other
.constant
)
229 constant
= Fraction(self
.constant
, other
.constant
)
230 return Expression(coefficients
, constant
)
231 if isinstance(other
, Expression
):
232 raise ValueError('non-linear expression: '
233 '{} / {}'.format(self
._parenstr
(), other
._parenstr
()))
234 return NotImplemented
236 def __rtruediv__(self
, other
):
237 if isinstance(other
, self
):
238 if self
.isconstant():
239 constant
= Fraction(other
, self
.constant
)
240 return Expression(constant
=constant
)
242 raise ValueError('non-linear expression: '
243 '{} / {}'.format(other
._parenstr
(), self
._parenstr
()))
244 return NotImplemented
248 symbols
= sorted(self
.symbols())
250 for symbol
in symbols
:
251 coefficient
= self
[symbol
]
256 string
+= ' + {}'.format(symbol
)
257 elif coefficient
== -1:
259 string
+= '-{}'.format(symbol
)
261 string
+= ' - {}'.format(symbol
)
264 string
+= '{}*{}'.format(coefficient
, symbol
)
265 elif coefficient
> 0:
266 string
+= ' + {}*{}'.format(coefficient
, symbol
)
268 assert coefficient
< 0
270 string
+= ' - {}*{}'.format(coefficient
, symbol
)
272 constant
= self
.constant
273 if constant
!= 0 and i
== 0:
274 string
+= '{}'.format(constant
)
276 string
+= ' + {}'.format(constant
)
279 string
+= ' - {}'.format(constant
)
284 def _parenstr(self
, always
=False):
286 if not always
and (self
.isconstant() or self
.issymbol()):
289 return '({})'.format(string
)
292 string
= '{}({{'.format(self
.__class
__.__name
__)
293 for i
, (symbol
, coefficient
) in enumerate(self
.coefficients()):
296 string
+= '{!r}: {!r}'.format(symbol
, coefficient
)
297 string
+= '}}, {!r})'.format(self
.constant
)
301 def fromstring(cls
, string
):
302 raise NotImplementedError
305 def __eq__(self
, other
):
307 # see http://docs.sympy.org/dev/tutorial/gotchas.html#equals-signs
308 return isinstance(other
, Expression
) and \
309 self
._coefficients
== other
._coefficients
and \
310 self
.constant
== other
.constant
313 return hash((self
._coefficients
, self
._constant
))
316 lcm
= functools
.reduce(lambda a
, b
: a
*b
// gcd(a
, b
),
317 [value
.denominator
for value
in self
.values()])
321 def _eq(self
, other
):
322 return Polyhedron(equalities
=[(self
- other
)._canonify
()])
325 def __le__(self
, other
):
326 return Polyhedron(inequalities
=[(self
- other
)._canonify
()])
329 def __lt__(self
, other
):
330 return Polyhedron(inequalities
=[(self
- other
)._canonify
() + 1])
333 def __ge__(self
, other
):
334 return Polyhedron(inequalities
=[(other
- self
)._canonify
()])
337 def __gt__(self
, other
):
338 return Polyhedron(inequalities
=[(other
- self
)._canonify
() + 1])
341 def constant(numerator
=0, denominator
=None):
342 if denominator
is None and isinstance(numerator
, numbers
.Rational
):
343 return Expression(constant
=3)
345 return Expression(constant
=Fraction(numerator
, denominator
))
348 if not isinstance(name
, str):
349 raise TypeError('name must be a string')
350 return Expression(coefficients
={name
: 1})
353 if isinstance(names
, str):
354 names
= names
.replace(',', ' ').split()
355 return (symbol(name
) for name
in names
)
358 @_polymorphic_operator
362 @_polymorphic_operator
366 @_polymorphic_operator
370 @_polymorphic_operator
374 @_polymorphic_operator
381 This class implements polyhedrons.
384 def __new__(cls
, equalities
=None, inequalities
=None):
385 if isinstance(equalities
, str):
386 if inequalities
is not None:
387 raise TypeError('too many arguments')
388 return cls
.fromstring(equalities
)
389 self
= super().__new
__(cls
)
390 self
._equalities
= []
391 if equalities
is not None:
392 for constraint
in equalities
:
393 for value
in constraint
.values():
394 if value
.denominator
!= 1:
395 raise TypeError('non-integer constraint: '
396 '{} == 0'.format(constraint
))
397 self
._equalities
.append(constraint
)
398 self
._inequalities
= []
399 if inequalities
is not None:
400 for constraint
in inequalities
:
401 for value
in constraint
.values():
402 if value
.denominator
!= 1:
403 raise TypeError('non-integer constraint: '
404 '{} <= 0'.format(constraint
))
405 self
._inequalities
.append(constraint
)
406 self
._bset
= self
.to_isl()
408 #put this here just to test from isl method
409 #from_isl = self.from_isl(self._bset)
416 def equalities(self
):
417 yield from self
._equalities
420 def inequalities(self
):
421 yield from self
._inequalities
425 return self
._constant
427 def isconstant(self
):
428 return len(self
._coefficients
) == 0
432 return bool(libisl
.isl_basic_set_is_empty(self
._bset
))
434 def constraints(self
):
435 yield from self
.equalities
436 yield from self
.inequalities
441 for constraint
in self
.constraints():
442 s
.update(constraint
.symbols
)
447 return len(self
.symbols())
450 # return false if the polyhedron is empty, true otherwise
451 if self
._equalities
or self
._inequalities
:
457 def __contains__(self
, value
):
458 # is the value in the polyhedron?
459 raise NotImplementedError
461 def __eq__(self
, other
):
462 raise NotImplementedError
467 def isuniverse(self
):
468 return self
== universe
470 def isdisjoint(self
, other
):
471 # return true if the polyhedron has no elements in common with other
472 raise NotImplementedError
474 def issubset(self
, other
):
475 raise NotImplementedError
477 def __le__(self
, other
):
478 return self
.issubset(other
)
480 def __lt__(self
, other
):
481 raise NotImplementedError
483 def issuperset(self
, other
):
484 # test whether every element in other is in the polyhedron
486 if value
== self
.constraints():
490 raise NotImplementedError
492 def __ge__(self
, other
):
493 return self
.issuperset(other
)
495 def __gt__(self
, other
):
496 raise NotImplementedError
498 def union(self
, *others
):
499 # return a new polyhedron with elements from the polyhedron and all
500 # others (convex union)
501 raise NotImplementedError
503 def __or__(self
, other
):
504 return self
.union(other
)
506 def intersection(self
, *others
):
507 # return a new polyhedron with elements common to the polyhedron and all
509 # a poor man's implementation could be:
510 # equalities = list(self.equalities)
511 # inequalities = list(self.inequalities)
512 # for other in others:
513 # equalities.extend(other.equalities)
514 # inequalities.extend(other.inequalities)
515 # return self.__class__(equalities, inequalities)
516 raise NotImplementedError
518 def __and__(self
, other
):
519 return self
.intersection(other
)
521 def difference(self
, *others
):
522 # return a new polyhedron with elements in the polyhedron that are not
524 raise NotImplementedError
526 def __sub__(self
, other
):
527 return self
.difference(other
)
531 for constraint
in self
.equalities
:
532 constraints
.append('{} == 0'.format(constraint
))
533 for constraint
in self
.inequalities
:
534 constraints
.append('{} <= 0'.format(constraint
))
535 return '{{{}}}'.format(', '.join(constraints
))
538 equalities
= list(self
.equalities
)
539 inequalities
= list(self
.inequalities
)
540 return '{}(equalities={!r}, inequalities={!r})' \
541 ''.format(self
.__class
__.__name
__, equalities
, inequalities
)
544 def fromstring(cls
, string
):
545 raise NotImplementedError
548 #d = Expression().__dict__ #write expression values to dictionary in form {'_constant': value, '_coefficients': value}
549 d
= {'_constant': 2, '_coefficients': {'b':1}}
550 coeff
= d
.get('_coefficients')
551 num_coefficients
= len(coeff
)
552 space
= libisl
.isl_space_set_alloc(Context(), 0, num_coefficients
)
553 bset
= libisl
.isl_basic_set_empty(libisl
.isl_space_copy(space
))
554 ls
= libisl
.isl_local_space_from_space(libisl
.isl_space_copy(space
))
555 ceq
= libisl
.isl_equality_alloc(libisl
.isl_local_space_copy(ls
))
556 cin
= libisl
.isl_inequality_alloc(libisl
.isl_local_space_copy(ls
))
557 '''if there are equalities/inequalities, take each constant and coefficient and add as a constraint to the basic set
558 need to change the symbols method to a lookup table for the integer value for each letter that could be a symbol'''
561 value
= d
.get('_constant')
562 ceq
= libisl
.isl_constraint_set_constant_si(ceq
, value
)
563 if '_coefficients' in d
:
564 value_co
= d
.get('_coefficients')
566 num
= value_co
.get(co
)
567 ceq
= libisl
.isl_constraint_set_coefficient_si(ceq
, 3, get_ids(co
), num
) #use 3 for type isl_dim_set
568 bset
= libisl
.isl_set_add_constraint(bset
, ceq
)
570 if self
._inequalities
:
572 value
= d
.get('_constant')
573 cin
= libisl
.isl_constraint_set_constant_si(cin
, value
)
574 if '_coefficients' in d
:
575 value_co
= d
.get('_coefficients')
577 num
= value_co
.get(co
)
578 if value_co
: #if dictionary not empty add coefficient as to constraint
579 cin
= libisl
.isl_constraint_set_coefficient_si(cin
, 3, get_ids(co
), num
) #use 3 for type isl_dim_set
580 bset
= libisl
.isl_set_add_constraint(bset
, cin
)
581 ip
= libisl
.isl_printer_to_str(Context()) #create string printer
582 ip
= libisl
.isl_printer_print_set(ip
, bset
) #print set to printer
583 string
= libisl
.isl_printer_get_str(ip
) #get string from printer
589 def from_isl(self
, bset
):
590 '''takes basic set in isl form and puts back into python version of polyhedron
591 isl example code gives idl form as:
592 "{[i] : exists (a : i = 2a and i >= 10 and i <= 42)}");'''
600 universe
= Polyhedron()