+ if self.isempty():
+ return 'Empty'
+ elif self.isuniverse():
+ return 'Universe'
+ else:
+ equalities = list(self.equalities)
+ inequalities = list(self.inequalities)
+ return '{}(equalities={!r}, inequalities={!r})' \
+ ''.format(self.__class__.__name__, equalities, inequalities)
+
+ @classmethod
+ def _fromsympy(cls, expr):
+ import sympy
+ equalities = []
+ inequalities = []
+ if expr.func == sympy.And:
+ for arg in expr.args:
+ arg_eqs, arg_ins = cls._fromsympy(arg)
+ equalities.extend(arg_eqs)
+ inequalities.extend(arg_ins)
+ elif expr.func == sympy.Eq:
+ expr = Expression.fromsympy(expr.args[0] - expr.args[1])
+ equalities.append(expr)
+ else:
+ if expr.func == sympy.Lt:
+ expr = Expression.fromsympy(expr.args[1] - expr.args[0] - 1)
+ elif expr.func == sympy.Le:
+ expr = Expression.fromsympy(expr.args[1] - expr.args[0])
+ elif expr.func == sympy.Ge:
+ expr = Expression.fromsympy(expr.args[0] - expr.args[1])
+ elif expr.func == sympy.Gt:
+ expr = Expression.fromsympy(expr.args[0] - expr.args[1] - 1)
+ else:
+ raise ValueError('non-polyhedral expression: {!r}'.format(expr))
+ inequalities.append(expr)
+ return equalities, inequalities
+
+ @classmethod
+ def fromsympy(cls, expr):
+ import sympy
+ equalities, inequalities = cls._fromsympy(expr)
+ return cls(equalities, inequalities)
+
+ def tosympy(self):
+ import sympy
+ constraints = []
+ for equality in self.equalities:
+ constraints.append(sympy.Eq(equality.tosympy(), 0))
+ for inequality in self.inequalities:
+ constraints.append(sympy.Ge(inequality.tosympy(), 0))
+ return sympy.And(*constraints)