X-Git-Url: https://scm.cri.mines-paristech.fr/git/linpy.git/blobdiff_plain/096532c477811ce4fe26f2e6a82cb0b795bdeca2..bb2fe6868c69f2d478da3ecbf4efeeef21c6eae2:/polyp.py diff --git a/polyp.py b/polyp.py index b73814e..ca32493 100644 --- a/polyp.py +++ b/polyp.py @@ -16,19 +16,65 @@ __all__ = [ ] -_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): @@ -68,10 +114,7 @@ class Expression: 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: @@ -83,6 +126,7 @@ class Expression: @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) @@ -99,10 +143,7 @@ class Expression: 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: @@ -270,13 +311,11 @@ def Constant(numerator=0, denominator=None): 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) @@ -317,29 +356,19 @@ class Polyhedron: for inequality in inequalities: symbols.update(inequality.symbols()) symbols = sorted(symbols) - string = cls._isccpoly(symbols, equalities, inequalities) - string = _iscc(string) + 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 = _strsymbols(symbols) self._equalities = [] self._inequalities = [] string = re.sub(r'^\s*\{\s*(.*?)\s*\}\s*$', lambda m: m.group(1), string) @@ -396,10 +425,16 @@ class Polyhedron: # 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): @@ -413,63 +448,58 @@ class Polyhedron: 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 = self._symbolunion(*others) symbols = sorted(symbols) 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): @@ -478,20 +508,28 @@ class Polyhedron: 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 = self._symbolunion(*others) symbols = sorted(symbols) 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: @@ -510,3 +548,12 @@ class Polyhedron: 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])