]
-_iscc_debug = False
+def _strsymbol(symbol):
+ if isinstance(symbol, str):
+ return symbol
+ elif isinstance(symbol, Expression) and symbol.issymbol():
+ return str(symbol)
+ else:
+ raise TypeError('symbol must be a string or a symbol')
+
+def _strsymbols(symbols):
+ if isinstance(symbols, str):
+ return symbols.replace(',', ' ').split()
+ else:
+ return [_strsymbol(symbol) for symbol in symbols]
+
+
+class _ISCC:
+
+ command =['iscc']
+ debug = False
+
+ @classmethod
+ def eval(cls, input):
+ if not input.endswith(';'):
+ input += ';'
+ proc = subprocess.Popen(cls.command,
+ stdin=subprocess.PIPE, stdout=subprocess.PIPE,
+ universal_newlines=True)
+ output, error = proc.communicate(input=input)
+ output = output.strip()
+ if cls.debug:
+ print('iscc: {!r} -> {!r}'.format(input, output))
+ return output
+
+ @classmethod
+ def symbols(cls, symbols):
+ symbols = _strsymbols(symbols)
+ return '[{}]'.format(', '.join(symbols))
+
+ @classmethod
+ def constraints(cls, equalities, inequalities):
+ strings = []
+ for equality in equalities:
+ strings.append('{} = 0'.format(equality))
+ for inequality in inequalities:
+ strings.append('{} <= 0'.format(inequality))
+ return ' and '.join(strings)
+
+ @classmethod
+ def set(cls, symbols, equalities, inequalities):
+ return '{{ {} : {} }}'.format(cls.symbols(symbols),
+ cls.constraints(equalities, inequalities))
+
+ @classmethod
+ def map(cls, lsymbols, rsymbols, equalities, inequalities):
+ return '{{ {} -> {} : {} }}'.format(
+ cls.symbols(lsymbols), cls.symbols(rsymbols),
+ cls.constraints(equalities, inequalities))
-def _iscc(input):
- if not input.endswith(';'):
- input += ';'
- proc = subprocess.Popen(['iscc'],
- stdin=subprocess.PIPE, stdout=subprocess.PIPE,
- universal_newlines=True)
- output, error = proc.communicate(input=input)
- output = output.strip()
- if _iscc_debug:
- print('ISCC({!r}) = {!r}'.format(input, output))
- return output
+_iscc = _ISCC()
def _polymorphic_method(func):
coefficients = coefficients.items()
if coefficients is not None:
for symbol, coefficient in coefficients:
- if isinstance(symbol, Expression) and symbol.issymbol():
- symbol = str(symbol)
- elif not isinstance(symbol, str):
- raise TypeError('symbols must be strings')
+ symbol = _strsymbol(symbol)
if not isinstance(coefficient, numbers.Rational):
raise TypeError('coefficients must be rational numbers')
if coefficient != 0:
@classmethod
def _fromiscc(cls, symbols, string):
+ symbols = _strsymbols(symbols)
string = re.sub(r'(\d+)\s*([a-zA-Z_]\w*)',
lambda m: '{}*{}'.format(m.group(1), m.group(2)),
string)
context[symbol] = Symbol(symbol)
return eval(string, context)
+ @property
def symbols(self):
- yield from sorted(self._coefficients)
+ return tuple(sorted(self._coefficients))
@property
def dimension(self):
- return len(list(self.symbols()))
+ return len(list(self.symbols))
def coefficient(self, symbol):
- if isinstance(symbol, Expression) and symbol.issymbol():
- symbol = str(symbol)
- elif not isinstance(symbol, str):
- raise TypeError('symbol must be a string')
+ symbol = _strsymbol(symbol)
try:
return self._coefficients[symbol]
except KeyError:
__getitem__ = coefficient
def coefficients(self):
- for symbol in self.symbols():
+ for symbol in self.symbols:
yield symbol, self.coefficient(symbol)
@property
return len(self._coefficients) == 0
def values(self):
- for symbol in self.symbols():
+ for symbol in self.symbols:
yield self.coefficient(symbol)
yield self.constant
def symbol(self):
if not self.issymbol():
raise ValueError('not a symbol: {}'.format(self))
- for symbol in self.symbols():
+ for symbol in self.symbols:
return symbol
def issymbol(self):
def __repr__(self):
string = ''
- symbols = sorted(self.symbols())
+ symbols = self.symbols
i = 0
for symbol in symbols:
coefficient = self[symbol]
return Expression(constant=Fraction(numerator, denominator))
def Symbol(name):
- if not isinstance(name, str):
- raise TypeError('name must be a string')
+ name = _strsymbol(name)
return Expression(coefficients={name: 1})
def symbols(names):
- if isinstance(names, str):
- names = names.replace(',', ' ').split()
+ names = _strsymbols(names)
return (Symbol(name) for name in names)
inequalities = []
symbols = set()
for equality in equalities:
- symbols.update(equality.symbols())
+ symbols.update(equality.symbols)
for inequality in inequalities:
- symbols.update(inequality.symbols())
- symbols = sorted(symbols)
- string = cls._isccpoly(symbols, equalities, inequalities)
- string = _iscc(string)
+ symbols.update(inequality.symbols)
+ symbols = list(symbols)
+ string = _iscc.set(symbols, equalities, inequalities)
+ string = _iscc.eval(string)
return cls._fromiscc(symbols, string)
- @classmethod
- def _isccpoly(cls, symbols, equalities, inequalities):
- strings = []
- for equality in equalities:
- strings.append('{} = 0'.format(equality))
- for inequality in inequalities:
- strings.append('{} <= 0'.format(inequality))
- string = '{{ [{}] : {} }}'.format(', '.join(symbols), ' and '.join(strings))
- return string
-
def _toiscc(self, symbols):
- return self._isccpoly(symbols, self.equalities, self.inequalities)
+ return _iscc.set(symbols, self.equalities, self.inequalities)
@classmethod
def _fromiscc(cls, symbols, string):
if re.match(r'^\s*\{\s*\}\s*$', string):
return empty
self = super().__new__(cls)
- self._symbols = symbols
+ self._symbols = sorted(_strsymbols(symbols))
self._equalities = []
self._inequalities = []
string = re.sub(r'^\s*\{\s*(.*?)\s*\}\s*$', lambda m: m.group(1), string)
yield from self.equalities
yield from self.inequalities
+ @property
def symbols(self):
- yield from self._symbols
+ return tuple(self._symbols)
@property
def dimension(self):
- return len(self.symbols())
+ return len(self.symbols)
def __bool__(self):
# return false if the polyhedron is empty, true otherwise
raise not self.isempty()
+ def _symbolunion(self, *others):
+ symbols = set(self.symbols)
+ for other in others:
+ symbols.update(other.symbols)
+ return sorted(symbols)
+
def __eq__(self, other):
- symbols = set(self.symbols()) | set(other.symbols())
+ symbols = self._symbolunion(other)
string = '{} = {}'.format(self._toiscc(symbols), other._toiscc(symbols))
- string = _iscc(string)
+ string = _iscc.eval(string)
return string == 'True'
def isempty(self):
return (self & other).isempty()
def issubset(self, other):
- symbols = set(self.symbols()) | set(other.symbols())
+ symbols = self._symbolunion(other)
string = '{} <= {}'.format(self._toiscc(symbols), other._toiscc(symbols))
- string = _iscc(string)
+ string = _iscc.eval(string)
return string == 'True'
def __le__(self, other):
return self.issubset(other)
def __lt__(self, other):
- symbols = set(self.symbols()) | set(other.symbols())
+ symbols = self._symbolunion(other)
string = '{} < {}'.format(self._toiscc(symbols), other._toiscc(symbols))
- string = _iscc(string)
+ string = _iscc.eval(string)
return string == 'True'
def issuperset(self, other):
# test whether every element in other is in the polyhedron
- symbols = set(self.symbols()) | set(other.symbols())
+ symbols = self._symbolunion(other)
string = '{} >= {}'.format(self._toiscc(symbols), other._toiscc(symbols))
- string = _iscc(string)
+ string = _iscc.eval(string)
return string == 'True'
def __ge__(self, other):
return self.issuperset(other)
def __gt__(self, other):
- symbols = set(self.symbols() + other.symbols())
+ symbols = self._symbolunion(other)
string = '{} > {}'.format(self._toiscc(symbols), other._toiscc(symbols))
- string = _iscc(string)
+ string = _iscc.eval(string)
return string == 'True'
def union(self, *others):
# return a new polyhedron with elements from the polyhedron and all
# others (convex union)
- symbols = set(self.symbols())
- for other in others:
- symbols.update(other.symbols())
- symbols = sorted(symbols)
+ symbols = self._symbolunion(*others)
strings = [self._toiscc(symbols)]
for other in others:
strings.append(other._toiscc(symbols))
string = ' + '.join(strings)
- string = _iscc('poly ({})'.format(string))
+ string = _iscc.eval('poly ({})'.format(string))
return Polyhedron._fromiscc(symbols, string)
def __or__(self, other):
return self.union(other)
def intersection(self, *others):
- symbols = set(self.symbols())
- for other in others:
- symbols.update(other.symbols())
- symbols = sorted(symbols)
+ symbols = self._symbolunion(*others)
strings = [self._toiscc(symbols)]
for other in others:
strings.append(other._toiscc(symbols))
string = ' * '.join(strings)
- string = _iscc('poly ({})'.format(string))
+ string = _iscc.eval('poly ({})'.format(string))
return Polyhedron._fromiscc(symbols, string)
def __and__(self, other):
def difference(self, *others):
# return a new polyhedron with elements in the polyhedron that are not
# in the others
- symbols = set(self.symbols())
- for other in others:
- symbols.update(other.symbols())
- symbols = sorted(symbols)
+ symbols = self._symbolunion(*others)
strings = [self._toiscc(symbols)]
for other in others:
strings.append(other._toiscc(symbols))
string = ' - '.join(strings)
- string = _iscc('poly ({})'.format(string))
+ string = _iscc.eval('poly ({})'.format(string))
return Polyhedron._fromiscc(symbols, string)
def __sub__(self, other):
return self.difference(other)
+ def projection(self, symbols):
+ symbols = _strsymbols(symbols)
+ string = _iscc.map(symbols, self.symbols,
+ self.equalities, self.inequalities)
+ string = _iscc.eval('poly (dom ({}))'.format(string))
+ return Polyhedron._fromiscc(symbols, string)
+
+ def __getitem__(self, symbol):
+ return self.projection([symbol])
+
def __repr__(self):
constraints = []
for constraint in self.equalities:
empty = Eq(1, 0)
universe = Polyhedron()
+
+
+if __name__ == '__main__':
+ x, y, z = symbols('x y z')
+ sq0 = (0 <= x) & (x <= 1) & (0 <= y) & (y <= 1)
+ sq1 = (1 <= x) & (x <= 2) & (1 <= y) & (y <= 2)
+ print('sq0 ∪ sq1 =', sq0 | sq1)
+ print('sq0 ∩ sq1 =', sq0 & sq1)
+ print('sq0[x] =', sq0[x])