WIP: [py] Make single interface for polynomials

.gitignore

@@ -3,3 +3,4 @@ catch.hpp
 __pycache__
 tags
 *.bak
+*.pyc

symbsat-py/symbsat/poly.py

@@ -53,13 +53,13 @@ def __str__(self):
     def copy(self):
         return Poly(self)
 
-    @classmethod
-    def zero(cls):
-        return cls([])
+    def zero(self):
+        class_ = type(self)
+        return class_([])
 
-    @classmethod
-    def one(cls):
-        return cls([Monom.one()])
+    def one(self):
+        class_ = type(self)
+        return class_([Monom.one()])
 
     def is_zero(self):
         return self == []

symbsat-py/symbsat/poly_new/__init__.py

@@ -0,0 +1,2 @@
+from .list import PolyList  # noqa
+from .zdd import PolyZDD  # noqa

symbsat-py/symbsat/poly_new/base.py

@@ -0,0 +1,71 @@
+import abc
+
+
+class Poly(metaclass=abc.ABCMeta):
+    """Base class for boolean polynomials."""
+
+    def __init__(self, *, monoms=None, var=None, monom=None):
+        is_monoms = monoms is not None
+        is_var = var is not None
+        is_monom = monom is not None
+
+        # We want zero or one parameter
+        if [is_monoms, is_var, is_monom].count(True) > 1:
+            raise RuntimeError("Only one initialization parameter is allowed")
+
+        if is_monoms:
+            self._init_monoms(monoms)
+        elif is_var:
+            self._init_var(var)
+        elif is_monom:
+            self._init_monom(monom)
+        else:
+            raise NotImplementedError
+
+    @abc.abstractclassmethod
+    def make_zero(cls):
+        raise NotImplementedError
+
+    @abc.abstractclassmethod
+    def make_one(cls):
+        raise NotImplementedError
+
+    @abc.abstractmethod
+    def _init_monoms(self, monoms):
+        raise NotImplementedError
+
+    @abc.abstractmethod
+    def _init_var(self, var):
+        raise NotImplementedError
+
+    @abc.abstractmethod
+    def _init_monom(self, monom):
+        raise NotImplementedError
+
+    @abc.abstractmethod
+    def __add__(self, other):
+        raise NotImplementedError
+
+    @abc.abstractmethod
+    def __mul__(self, other):
+        raise NotImplementedError
+
+    @abc.abstractmethod
+    def __str__(self):
+        raise NotImplementedError
+
+    @abc.abstractmethod
+    def copy(self):
+        raise NotImplementedError
+
+    @abc.abstractmethod
+    def is_zero(self):
+        raise NotImplementedError
+
+    @abc.abstractmethod
+    def is_one(self):
+        raise NotImplementedError
+
+    @abc.abstractmethod
+    def lm(self):
+        raise NotImplementedError

symbsat-py/symbsat/poly_new/list.py

@@ -0,0 +1,68 @@
+import collections
+import itertools
+import operator
+
+from symbsat.monom import Monom
+
+from .base import Poly
+
+
+class PolyList(Poly):
+
+    def _init_monoms(self, monoms):
+        self._list = sorted(monoms, reverse=True)
+
+    def _init_var(self, var):
+        self._list = [Monom(vars=[var])]
+
+    def _init_monom(self, monom):
+        self._list = [monom]
+
+    @classmethod
+    def make_zero(cls):
+        raise NotImplementedError
+
+    @classmethod
+    def make_one(cls):
+        raise NotImplementedError
+
+    def __add__(self, other):
+        # symmetric difference
+        if isinstance(other, Monom):
+            return PolyList(monoms=list(set(self) ^ set([other])))
+        if isinstance(other, PolyList):
+            return PolyList(monoms=list(set(self) ^ set(other)))
+        return NotImplemented
+
+    def __mul__(self, other):
+        if isinstance(other, Monom):
+            if self.is_zero() or other.is_zero():
+                return PolyList.make_zero()
+            monoms = map(lambda m: m*other, self)
+        elif isinstance(other, PolyList):
+            if self.is_zero() or other.is_zero():
+                return PolyList.make_zero()
+            monoms = itertools.starmap(
+                operator.mul,
+                (itertools.product(self, other))
+            )
+        else:
+            return NotImplemented
+
+        counter = collections.Counter(monoms)
+        return PolyList(monoms={m for m, c in counter.items() if c % 2 != 0})
+
+    def __str__(self):
+        raise NotImplementedError
+
+    def copy(self):
+        raise NotImplementedError
+
+    def is_zero(self):
+        raise NotImplementedError
+
+    def is_one(self):
+        raise NotImplementedError
+
+    def lm(self):
+        raise NotImplementedError

symbsat-py/symbsat/poly_new/zdd.py

@@ -0,0 +1,53 @@
+from symbsat.zdd_new import ZDD
+from .base import Poly
+
+
+class PolyZDD(Poly):
+
+    @classmethod
+    def make_zero(cls):
+        raise NotImplementedError
+
+    @classmethod
+    def make_one(cls):
+        raise NotImplementedError
+
+    def _init_var(self, var: int):
+        self._zdd = ZDD(var)
+
+    def _init_monom(self, monom):
+        if monom.is_zero():
+            self._zdd = ZDD.zero()
+        elif monom.is_one():
+            self._zdd = ZDD.one()
+        else:
+            self._zdd = ZDD(monom.vars[0])
+            for var in monom.vars[1:]:
+                self._zdd *= ZDD(var)
+
+    def _init_monoms(self, monoms):
+        raise NotImplementedError
+
+    def __add__(self, other):
+        raise NotImplementedError
+
+    def __mul__(self, other):
+        raise NotImplementedError
+
+    def __imul__(self, other):
+        raise NotImplementedError
+
+    def __str__(self):
+        raise NotImplementedError
+
+    def copy(self):
+        raise NotImplementedError
+
+    def is_zero(self):
+        raise NotImplementedError
+
+    def is_one(self):
+        raise NotImplementedError
+
+    def lm(self):
+        raise NotImplementedError

symbsat-py/symbsat/zdd_new/__init__.py

@@ -0,0 +1 @@
+from .zdd import ZDD

symbsat-py/symbsat/zdd_new/node.py

@@ -0,0 +1,48 @@
+class Node:
+
+    __slots__ = ('var', 'mul', 'add')
+
+    def __init__(self, var, m, a):
+        if m and m.is_zero():
+            raise TypeError('Multiply branch cannot be zero')
+
+        self.var = var
+        self.mul = m  # and
+        self.add = a  # xor
+
+    @classmethod
+    def zero(cls):
+        return cls(-2, None, None)
+
+    @classmethod
+    def one(cls):
+        return cls(-1, None, None)
+
+    def copy(self):
+        if self.var < 0:
+            return self
+        return Node(
+            self.var,
+            self.mul.copy(),
+            self.add.copy()
+        )
+
+    def is_zero(self):
+        return self.var == -2
+
+    def is_one(self):
+        return self.var == -1
+
+    def __str__(self):
+        if self.is_one():
+            return "_one"
+        if self.is_zero():
+            return "_zero"
+
+        return (
+            '%s -> {%s} {%s}' %
+            (self.var, self.mul, self.add)
+        )
+
+    def __eq__(self, other):
+        return id(self) == id(other)

symbsat-py/symbsat/zdd_new/zdd.py

@@ -0,0 +1,108 @@
+from .node import Node
+
+
+class ZDD:
+
+    def __init__(self, var=-1):
+        if var < 0:
+            self.root = Node.zero()
+        else:
+            self.root = self.create_node(
+                var, Node.one(), Node.zero()
+            )
+
+    def create_node(self, var: int, m: Node, a: Node):
+        return Node(var, m, a)
+
+    @classmethod
+    def zero(cls):
+        return cls()
+
+    @classmethod
+    def one(cls):
+        zdd = cls()
+        zdd.root = Node.one()
+        return zdd
+
+    def _add(self, i, j):
+
+        if i.is_zero():
+            return j
+        if j.is_zero():
+            return i
+        if i == j:
+            return self.zero()
+
+        if i.is_one():
+            r = self.create_node(
+                j.var, j.mul, self._add(j.add, Node.one())
+            )
+        elif j.is_one():
+            r = self.create_node(
+                i.var, i.mul, self._add(i.add, Node.one())
+            )
+        else:
+            if i.var < j.var:
+                r = self.create_node(i.var, i.mul, self._add(i.add, j))
+            elif i.var > j.var:
+                r = self.create_node(j.var, j.mul, self._add(i, j.add))
+            else:
+                m = self._add(i.mul, j.mul)
+                a = self._add(i.add, j.add)
+
+                if m.is_zero():
+                    return a
+
+                r = self.create_node(i.var, m, a)
+        return r
+
+    def _mul(self, i, j):
+
+        if i.is_one():
+            return j
+        if i.is_zero() or j.is_zero():
+            return Node.zero()
+        if j.is_one() or i == j:
+            return i
+
+        r = None
+        if i.var < j.var:
+            m = self._mul(i.mul, j)
+            a = self._mul(i.add, j)
+
+            if m.is_zero():
+                return a
+
+            r = self.create_node(i.var, m, a)
+        elif i.var > j.var:
+            m = self._mul(j.mul, i)
+            a = self._mul(j.add, i)
+
+            if m.is_zero():
+                return a
+
+            r = self.create_node(j.var, m, a)
+        else:
+            m1 = self._mul(i.add, j.mul)
+            m2 = self._mul(i.mul, j.mul)
+            m3 = self._mul(i.mul, j.add)
+            ms_sum = self._add(m1, self._add(m2, m3))
+
+            if ms_sum.is_zero():
+                return self._mul(i.add, j.add)
+
+            r = self.create_node(i.var, ms_sum, self._mul(i.add, j.add))
+        return r
+
+    def __mul__(self, other):
+        self_cls = type(self)
+        zdd = self_cls()
+        zdd.root = zdd._mul(self.root, other.root)
+        return zdd
+
+    def __add__(self, other):
+        self_cls = type(self)
+        zdd = self_cls()
+        zdd.root = zdd._add(self.root, other.root)
+        return zdd
+