From: Vivien Maisonneuve Date: Sun, 8 Jun 2014 20:47:46 +0000 (+0200) Subject: ISCC wrapper and projection X-Git-Url: https://svn.cri.ensmp.fr/git/linpy.git/commitdiff_plain/a87eb293f1d72496c2645e8b90d40d896982520e?ds=inline ISCC wrapper and projection --- diff --git a/polyp.py b/polyp.py index b73814e..9058c08 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) -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 + @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)) + +_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) @@ -399,7 +428,7 @@ class Polyhedron: def __eq__(self, other): symbols = set(self.symbols()) | set(other.symbols()) string = '{} = {}'.format(self._toiscc(symbols), other._toiscc(symbols)) - string = _iscc(string) + string = _iscc.eval(string) return string == 'True' def isempty(self): @@ -415,7 +444,7 @@ class Polyhedron: def issubset(self, other): symbols = set(self.symbols()) | set(other.symbols()) string = '{} <= {}'.format(self._toiscc(symbols), other._toiscc(symbols)) - string = _iscc(string) + string = _iscc.eval(string) return string == 'True' def __le__(self, other): @@ -424,14 +453,14 @@ class Polyhedron: def __lt__(self, other): symbols = set(self.symbols()) | set(other.symbols()) 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()) string = '{} >= {}'.format(self._toiscc(symbols), other._toiscc(symbols)) - string = _iscc(string) + string = _iscc.eval(string) return string == 'True' def __ge__(self, other): @@ -440,7 +469,7 @@ class Polyhedron: def __gt__(self, other): symbols = set(self.symbols() + other.symbols()) string = '{} > {}'.format(self._toiscc(symbols), other._toiscc(symbols)) - string = _iscc(string) + string = _iscc.eval(string) return string == 'True' def union(self, *others): @@ -454,7 +483,7 @@ class Polyhedron: 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): @@ -469,7 +498,7 @@ class Polyhedron: 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): @@ -486,12 +515,22 @@ class Polyhedron: 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 +549,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])