Implementation using iscc

[linpy.git] / polyp.py

diff --git a/pypol/linear.py b/polyp.py
similarity index 58%
rename from pypol/linear.py
rename to polyp.py
index a5f55fa..b73814e 100644 (file)
--- a/pypol/linear.py
+++ b/polyp.py
@@ -1,26 +1,43 @@
 
 import functools
 import numbers
 
 import functools
 import numbers

+import re
+import subprocess

 
 from fractions import Fraction, gcd
 
 
 __all__ = [
     'Expression',
 
 from fractions import Fraction, gcd
 
 
 __all__ = [
     'Expression',

-    'constant', 'symbol', 'symbols',
-    'eq', 'le', 'lt', 'ge', 'gt',
+    'Constant', 'Symbol', 'symbols',
+    'Eq', 'Le', 'Lt', 'Ge', 'Gt',

     'Polyhedron',
     'empty', 'universe'
 ]
 
 
     'Polyhedron',
     'empty', 'universe'
 ]
 
 

+_iscc_debug = False
+
+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
+
+

 def _polymorphic_method(func):
     @functools.wraps(func)
     def wrapper(a, b):
         if isinstance(b, Expression):
             return func(a, b)
         if isinstance(b, numbers.Rational):
 def _polymorphic_method(func):
     @functools.wraps(func)
     def wrapper(a, b):
         if isinstance(b, Expression):
             return func(a, b)
         if isinstance(b, numbers.Rational):

-            b = constant(b)
+            b = Constant(b)

             return func(a, b)
         return NotImplemented
     return wrapper
             return func(a, b)
         return NotImplemented
     return wrapper


@@ -31,7 +48,7 @@ def _polymorphic_operator(func):
     @functools.wraps(func)
     def wrapper(a, b):
         if isinstance(a, numbers.Rational):
     @functools.wraps(func)
     def wrapper(a, b):
         if isinstance(a, numbers.Rational):

-            a = constant(a)
+            a = Constant(a)

             return func(a, b)
         elif isinstance(a, Expression):
             return func(a, b)
             return func(a, b)
         elif isinstance(a, Expression):
             return func(a, b)


@@ -45,10 +62,6 @@ class Expression:
     """
 
     def __new__(cls, coefficients=None, constant=0):
     """
 
     def __new__(cls, coefficients=None, constant=0):

-        if isinstance(coefficients, str):
-            if constant:
-                raise TypeError('too many arguments')
-            return cls.fromstring(coefficients)

         self = super().__new__(cls)
         self._coefficients = {}
         if isinstance(coefficients, dict):
         self = super().__new__(cls)
         self._coefficients = {}
         if isinstance(coefficients, dict):


@@ -68,6 +81,16 @@ class Expression:
         self._constant = constant
         return self
 
         self._constant = constant
         return self
 

+    @classmethod
+    def _fromiscc(cls, symbols, string):
+        string = re.sub(r'(\d+)\s*([a-zA-Z_]\w*)',
+                lambda m: '{}*{}'.format(m.group(1), m.group(2)),
+                string)
+        context = {}
+        for symbol in symbols:
+            context[symbol] = Symbol(symbol)
+        return eval(string, context)
+

     def symbols(self):
         yield from sorted(self._coefficients)
 
     def symbols(self):
         yield from sorted(self._coefficients)
 


@@ -145,7 +168,8 @@ class Expression:
         constant = self.constant - other.constant
         return Expression(coefficients, constant)
 
         constant = self.constant - other.constant
         return Expression(coefficients, constant)
 

-    __rsub__ = __sub__
+    def __rsub__(self, other):
+        return -(self - other)

 
     @_polymorphic_method
     def __mul__(self, other):
 
     @_polymorphic_method
     def __mul__(self, other):


@@ -157,36 +181,12 @@ class Expression:
             return Expression(coefficients, constant)
         if isinstance(other, Expression) and not self.isconstant():
             raise ValueError('non-linear expression: '
             return Expression(coefficients, constant)
         if isinstance(other, Expression) and not self.isconstant():
             raise ValueError('non-linear expression: '

-                    '{} * {}'.format(self._parenstr(), other._parenstr()))
+                    '{} * {}'.format(self._prepr(), other._prepr()))

         return NotImplemented
 
     __rmul__ = __mul__
 
         return NotImplemented
 
     __rmul__ = __mul__
 

-    @_polymorphic_method
-    def __truediv__(self, other):
-        if other.isconstant():
-            coefficients = dict(self.coefficients())
-            for symbol in coefficients:
-                coefficients[symbol] = \
-                        Fraction(coefficients[symbol], other.constant)
-            constant = Fraction(self.constant, other.constant)
-            return Expression(coefficients, constant)
-        if isinstance(other, Expression):
-            raise ValueError('non-linear expression: '
-                '{} / {}'.format(self._parenstr(), other._parenstr()))
-        return NotImplemented
-
-    def __rtruediv__(self, other):
-        if isinstance(other, Rational):
-            if self.isconstant():
-                constant = Fraction(other, self.constant)
-                return Expression(constant=constant)
-            else:
-                raise ValueError('non-linear expression: '
-                        '{} / {}'.format(other._parenstr(), self._parenstr()))
-        return NotImplemented
-
-    def __str__(self):
+    def __repr__(self):

         string = ''
         symbols = sorted(self.symbols())
         i = 0
         string = ''
         symbols = sorted(self.symbols())
         i = 0


@@ -224,26 +224,13 @@ class Expression:
             string = '0'
         return string
 
             string = '0'
         return string
 

-    def _parenstr(self, always=False):
+    def _prepr(self, always=False):

         string = str(self)
         if not always and (self.isconstant() or self.issymbol()):
             return string
         else:
             return '({})'.format(string)
 
         string = str(self)
         if not always and (self.isconstant() or self.issymbol()):
             return string
         else:
             return '({})'.format(string)
 

-    def __repr__(self):
-        string = '{}({{'.format(self.__class__.__name__)
-        for i, (symbol, coefficient) in enumerate(self.coefficients()):
-            if i != 0:
-                string += ', '
-            string += '{!r}: {!r}'.format(symbol, coefficient)
-        string += '}}, {!r})'.format(self.constant)
-        return string
-
-    @classmethod
-    def fromstring(cls, string):
-        raise NotImplementedError
-

     @_polymorphic_method
     def __eq__(self, other):
         # "normal" equality
     @_polymorphic_method
     def __eq__(self, other):
         # "normal" equality


@@ -253,41 +240,36 @@ class Expression:
                 self.constant == other.constant
 
     def __hash__(self):
                 self.constant == other.constant
 
     def __hash__(self):

-        return hash((self._coefficients, self._constant))
-
-    def _canonify(self):
-        lcm = functools.reduce(lambda a, b: a*b // gcd(a, b),
-                [value.denominator for value in self.values()])
-        return self * lcm
+        return hash((tuple(self._coefficients), self._constant))

 
     @_polymorphic_method
     def _eq(self, other):
 
     @_polymorphic_method
     def _eq(self, other):

-        return Polyhedron(equalities=[(self - other)._canonify()])
+        return Polyhedron(equalities=[self - other])

 
     @_polymorphic_method
     def __le__(self, other):
 
     @_polymorphic_method
     def __le__(self, other):

-        return Polyhedron(inequalities=[(self - other)._canonify()])
+        return Polyhedron(inequalities=[self - other])

 
     @_polymorphic_method
     def __lt__(self, other):
 
     @_polymorphic_method
     def __lt__(self, other):

-        return Polyhedron(inequalities=[(self - other)._canonify() + 1])
+        return Polyhedron(inequalities=[self - other + 1])

 
     @_polymorphic_method
     def __ge__(self, other):
 
     @_polymorphic_method
     def __ge__(self, other):

-        return Polyhedron(inequalities=[(other - self)._canonify()])
+        return Polyhedron(inequalities=[other - self])

 
     @_polymorphic_method
     def __gt__(self, other):
 
     @_polymorphic_method
     def __gt__(self, other):

-        return Polyhedron(inequalities=[(other - self)._canonify() + 1])
+        return Polyhedron(inequalities=[other - self + 1])

 
 
 
 

-def constant(numerator=0, denominator=None):
+def Constant(numerator=0, denominator=None):

     if denominator is None and isinstance(numerator, numbers.Rational):
         return Expression(constant=numerator)
     else:
         return Expression(constant=Fraction(numerator, denominator))
 
     if denominator is None and isinstance(numerator, numbers.Rational):
         return Expression(constant=numerator)
     else:
         return Expression(constant=Fraction(numerator, denominator))
 

-def symbol(name):
+def Symbol(name):

     if not isinstance(name, str):
         raise TypeError('name must be a string')
     return Expression(coefficients={name: 1})
     if not isinstance(name, str):
         raise TypeError('name must be a string')
     return Expression(coefficients={name: 1})


@@ -295,27 +277,27 @@ def symbol(name):
 def symbols(names):
     if isinstance(names, str):
         names = names.replace(',', ' ').split()
 def symbols(names):
     if isinstance(names, str):
         names = names.replace(',', ' ').split()

-    return (symbol(name) for name in names)
+    return (Symbol(name) for name in names)

 
 
 @_polymorphic_operator
 
 
 @_polymorphic_operator

-def eq(a, b):
+def Eq(a, b):

     return a._eq(b)
 
 @_polymorphic_operator
     return a._eq(b)
 
 @_polymorphic_operator

-def le(a, b):
+def Le(a, b):

     return a <= b
 
 @_polymorphic_operator
     return a <= b
 
 @_polymorphic_operator

-def lt(a, b):
+def Lt(a, b):

     return a < b
 
 @_polymorphic_operator
     return a < b
 
 @_polymorphic_operator

-def ge(a, b):
+def Ge(a, b):

     return a >= b
 
 @_polymorphic_operator
     return a >= b
 
 @_polymorphic_operator

-def gt(a, b):
+def Gt(a, b):

     return a > b
 
 
     return a > b
 
 


@@ -325,27 +307,70 @@ class Polyhedron:
     """
 
     def __new__(cls, equalities=None, inequalities=None):
     """
 
     def __new__(cls, equalities=None, inequalities=None):

-        if isinstance(equalities, str):
-            if inequalities is not None:
-                raise TypeError('too many arguments')
-            return cls.fromstring(equalities)
+        if equalities is None:
+            equalities = []
+        if inequalities is None:
+            inequalities = []
+        symbols = set()
+        for equality in equalities:
+            symbols.update(equality.symbols())
+        for inequality in inequalities:
+            symbols.update(inequality.symbols())
+        symbols = sorted(symbols)
+        string = cls._isccpoly(symbols, equalities, inequalities)
+        string = _iscc(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)
+
+    @classmethod
+    def _fromiscc(cls, symbols, string):
+        if re.match(r'^\s*\{\s*\}\s*$', string):
+            return empty

         self = super().__new__(cls)
         self = super().__new__(cls)

+        self._symbols = symbols

         self._equalities = []
         self._equalities = []

-        if equalities is not None:
-            for constraint in equalities:
-                for value in constraint.values():
-                    if value.denominator != 1:
-                        raise TypeError('non-integer constraint: '
-                                '{} == 0'.format(constraint))
-                self._equalities.append(constraint)

         self._inequalities = []
         self._inequalities = []

-        if inequalities is not None:
-            for constraint in inequalities:
-                for value in constraint.values():
-                    if value.denominator != 1:
-                        raise TypeError('non-integer constraint: '
-                                '{} <= 0'.format(constraint))
-                self._inequalities.append(constraint)
+        string = re.sub(r'^\s*\{\s*(.*?)\s*\}\s*$', lambda m: m.group(1), string)
+        if ':' not in string:
+            string = string + ':'
+        vstr, cstr = re.split(r'\s*:\s*', string)
+        assert vstr != ''
+        vstr = re.sub(r'^\s*\[\s*(.*?)\s*\]\s*$', lambda m: m.group(1), vstr)
+        toks = list(filter(None, re.split(r'\s*,\s*', vstr)))
+        assert len(toks) == len(symbols)
+        for i in range(len(symbols)):
+            symbol = symbols[i]
+            if toks[i] != symbol:
+                expr = Expression._fromiscc(symbols, toks[i])
+                self._equalities.append(Symbol(symbol) - expr)
+        if cstr != '':
+            cstrs = re.split(r'\s*and\s*', cstr)
+            for cstr in cstrs:
+                lhs, op, rhs = re.split(r'\s*(<=|>=|<|>|=)\s*', cstr)
+                lhs = Expression._fromiscc(symbols, lhs)
+                rhs = Expression._fromiscc(symbols, rhs)
+                if op == '=':
+                    self._equalities.append(lhs - rhs)
+                elif op == '<=':
+                    self._inequalities.append(lhs - rhs)
+                elif op == '>=':
+                    self._inequalities.append(rhs - lhs)
+                elif op == '<':
+                    self._inequalities.append(lhs - rhs + 1)
+                elif op == '>':
+                    self._inequalities.append(rhs - lhs + 1)

         return self
 
     @property
         return self
 
     @property


@@ -361,10 +386,7 @@ class Polyhedron:
         yield from self.inequalities
 
     def symbols(self):
         yield from self.inequalities
 
     def symbols(self):

-        s = set()
-        for constraint in self.constraints():
-            s.update(constraint.symbols)
-        yield from sorted(s)
+        yield from self._symbols

 
     @property
     def dimension(self):
 
     @property
     def dimension(self):


@@ -372,14 +394,13 @@ class Polyhedron:
 
     def __bool__(self):
         # return false if the polyhedron is empty, true otherwise
 
     def __bool__(self):
         # return false if the polyhedron is empty, true otherwise

-        raise NotImplementedError
-
-    def __contains__(self, value):
-        # is the value in the polyhedron?
-        raise NotImplementedError
+        raise not self.isempty()

 
     def __eq__(self, other):
 
     def __eq__(self, other):

-        raise NotImplementedError
+        symbols = set(self.symbols()) | set(other.symbols())
+        string = '{} = {}'.format(self._toiscc(symbols), other._toiscc(symbols))
+        string = _iscc(string)
+        return string == 'True'

 
     def isempty(self):
         return self == empty
 
     def isempty(self):
         return self == empty


@@ -389,46 +410,67 @@ class Polyhedron:
 
     def isdisjoint(self, other):
         # return true if the polyhedron has no elements in common with other
 
     def isdisjoint(self, other):
         # return true if the polyhedron has no elements in common with other

-        raise NotImplementedError
+        return (self & other).isempty()

 
     def issubset(self, other):
 
     def issubset(self, other):

-        raise NotImplementedError
+        symbols = set(self.symbols()) | set(other.symbols())
+        string = '{} <= {}'.format(self._toiscc(symbols), other._toiscc(symbols))
+        string = _iscc(string)
+        return string == 'True'

 
     def __le__(self, other):
         return self.issubset(other)
 
     def __lt__(self, other):
 
     def __le__(self, other):
         return self.issubset(other)
 
     def __lt__(self, other):

-        raise NotImplementedError
+        symbols = set(self.symbols()) | set(other.symbols())
+        string = '{} < {}'.format(self._toiscc(symbols), other._toiscc(symbols))
+        string = _iscc(string)
+        return string == 'True'

 
     def issuperset(self, other):
         # test whether every element in other is in the polyhedron
 
     def issuperset(self, other):
         # test whether every element in other is in the polyhedron

-        raise NotImplementedError
+        symbols = set(self.symbols()) | set(other.symbols())
+        string = '{} >= {}'.format(self._toiscc(symbols), other._toiscc(symbols))
+        string = _iscc(string)
+        return string == 'True'

 
     def __ge__(self, other):
         return self.issuperset(other)
 
     def __gt__(self, other):
 
     def __ge__(self, other):
         return self.issuperset(other)
 
     def __gt__(self, other):

-        raise NotImplementedError
+        symbols = set(self.symbols() + other.symbols())
+        string = '{} > {}'.format(self._toiscc(symbols), other._toiscc(symbols))
+        string = _iscc(string)
+        return string == 'True'

 
     def union(self, *others):
         # return a new polyhedron with elements from the polyhedron and all
         # others (convex union)
 
     def union(self, *others):
         # return a new polyhedron with elements from the polyhedron and all
         # others (convex union)

-        raise NotImplementedError
+        symbols = set(self.symbols())
+        for other in others:
+            symbols.update(other.symbols())
+        symbols = sorted(symbols)
+        strings = [self._toiscc(symbols)]
+        for other in others:
+            strings.append(other._toiscc(symbols))
+        string = ' + '.join(strings)
+        string = _iscc('poly ({})'.format(string))
+        return Polyhedron._fromiscc(symbols, string)

 
     def __or__(self, other):
         return self.union(other)
 
     def intersection(self, *others):
 
     def __or__(self, other):
         return self.union(other)
 
     def intersection(self, *others):

-        # return a new polyhedron with elements common to the polyhedron and all
-        # others
-        # a poor man's implementation could be:
-        # equalities = list(self.equalities)
-        # inequalities = list(self.inequalities)
-        # for other in others:
-        #     equalities.extend(other.equalities)
-        #     inequalities.extend(other.inequalities)
-        # return self.__class__(equalities, inequalities)
-        raise NotImplementedError
+        symbols = set(self.symbols())
+        for other in others:
+            symbols.update(other.symbols())
+        symbols = sorted(symbols)
+        strings = [self._toiscc(symbols)]
+        for other in others:
+            strings.append(other._toiscc(symbols))
+        string = ' * '.join(strings)
+        string = _iscc('poly ({})'.format(string))
+        return Polyhedron._fromiscc(symbols, string)

 
     def __and__(self, other):
         return self.intersection(other)
 
     def __and__(self, other):
         return self.intersection(other)


@@ -436,30 +478,35 @@ class Polyhedron:
     def difference(self, *others):
         # return a new polyhedron with elements in the polyhedron that are not
         # in the others
     def difference(self, *others):
         # return a new polyhedron with elements in the polyhedron that are not
         # in the others

-        raise NotImplementedError
+        symbols = set(self.symbols())
+        for other in others:
+            symbols.update(other.symbols())
+        symbols = sorted(symbols)
+        strings = [self._toiscc(symbols)]
+        for other in others:
+            strings.append(other._toiscc(symbols))
+        string = ' - '.join(strings)
+        string = _iscc('poly ({})'.format(string))
+        return Polyhedron._fromiscc(symbols, string)

 
     def __sub__(self, other):
         return self.difference(other)
 
 
     def __sub__(self, other):
         return self.difference(other)
 

-    def __str__(self):
+    def __repr__(self):

         constraints = []
         for constraint in self.equalities:
             constraints.append('{} == 0'.format(constraint))
         for constraint in self.inequalities:
             constraints.append('{} <= 0'.format(constraint))
         constraints = []
         for constraint in self.equalities:
             constraints.append('{} == 0'.format(constraint))
         for constraint in self.inequalities:
             constraints.append('{} <= 0'.format(constraint))

-        return '{{{}}}'.format(', '.join(constraints))
-
-    def __repr__(self):
-        equalities = list(self.equalities)
-        inequalities = list(self.inequalities)
-        return '{}(equalities={!r}, inequalities={!r})' \
-                ''.format(self.__class__.__name__, equalities, inequalities)
-
-    @classmethod
-    def fromstring(cls, string):
-        raise NotImplementedError
-
+        if len(constraints) == 0:
+            return 'universe'
+        elif len(constraints) == 1:
+            string = constraints[0]
+            return 'empty' if string == '1 == 0' else string
+        else:
+            strings = ['({})'.format(constraint) for constraint in constraints]
+            return ' & '.join(strings)

 
 

-empty = le(1, 0)
+empty = Eq(1, 0)

 
 universe = Polyhedron()
 
 universe = Polyhedron()