diff --git a/.gitignore b/.gitignore index bf8c019..1b0bb09 100644 --- a/.gitignore +++ b/.gitignore @@ -3,3 +3,4 @@ catch.hpp __pycache__ tags *.bak +*.pyc diff --git a/symbsat-py/symbsat/poly.py b/symbsat-py/symbsat/poly.py index f3dd5f5..603f56d 100644 --- a/symbsat-py/symbsat/poly.py +++ b/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 == [] diff --git a/symbsat-py/symbsat/poly_new/__init__.py b/symbsat-py/symbsat/poly_new/__init__.py new file mode 100644 index 0000000..4379cdc --- /dev/null +++ b/symbsat-py/symbsat/poly_new/__init__.py @@ -0,0 +1,2 @@ +from .list import PolyList # noqa +from .zdd import PolyZDD # noqa diff --git a/symbsat-py/symbsat/poly_new/base.py b/symbsat-py/symbsat/poly_new/base.py new file mode 100644 index 0000000..cf2d07a --- /dev/null +++ b/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 diff --git a/symbsat-py/symbsat/poly_new/list.py b/symbsat-py/symbsat/poly_new/list.py new file mode 100644 index 0000000..8f4fb50 --- /dev/null +++ b/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 diff --git a/symbsat-py/symbsat/poly_new/zdd.py b/symbsat-py/symbsat/poly_new/zdd.py new file mode 100644 index 0000000..155ee98 --- /dev/null +++ b/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 diff --git a/symbsat-py/symbsat/zdd_new/__init__.py b/symbsat-py/symbsat/zdd_new/__init__.py new file mode 100644 index 0000000..a64682f --- /dev/null +++ b/symbsat-py/symbsat/zdd_new/__init__.py @@ -0,0 +1 @@ +from .zdd import ZDD diff --git a/symbsat-py/symbsat/zdd_new/node.py b/symbsat-py/symbsat/zdd_new/node.py new file mode 100644 index 0000000..1a20dfb --- /dev/null +++ b/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) diff --git a/symbsat-py/symbsat/zdd_new/zdd.py b/symbsat-py/symbsat/zdd_new/zdd.py new file mode 100644 index 0000000..4409bbe --- /dev/null +++ b/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 + diff --git a/symbsat-py/tests/poly/test_poly_list.py b/symbsat-py/tests/poly/test_poly_list.py new file mode 100644 index 0000000..25ccddf --- /dev/null +++ b/symbsat-py/tests/poly/test_poly_list.py @@ -0,0 +1,72 @@ +import unittest + +from symbsat.monom import Monom4 as Monom +from symbsat.poly_new import PolyList, PolyZDD + + +class BaseTest(unittest.TestCase): + + def setUp(self): + # Added this because of the pylint warning + self.poly_cls = object + + def test_init_not_implemented(self): + with self.assertRaises(NotImplementedError): + self.poly_cls() + + def test_init_from_var(self): + self.poly_cls(var=0) + + def test_init_from_monom(self): + + monom_zero = Monom.zero() + self.poly_cls(monom=monom_zero) + + monom_one = Monom.one() + self.poly_cls(monom=monom_one) + + monom_a = Monom(vars=[1]) + self.poly_cls(monom=monom_a) + + monom_ab = Monom(vars=[1, 2]) + self.poly_cls(monom=monom_ab) + + def test_init_from_monoms(self): + monom_a = Monom(vars=[1]) + monom_b = Monom(vars=[2]) + self.poly_cls(monoms=[monom_a, monom_b]) + + +class TestPolyList(BaseTest): + + def setUp(self): + self.poly_cls = PolyList + + @unittest.skip('Not implemented') + def test_init_from_var(self): + pass + + +class TestPolyZDD(BaseTest): + + def setUp(self): + self.poly_cls = PolyZDD + + # @unittest.skip('Not implemented') + # def test_init_from_monom(self): + # pass + + @unittest.skip('Not implemented') + def test_init_from_monoms(self): + pass + + +def load_tests(loader, tests, pattern): + test_cases = (TestPolyList, TestPolyZDD) + + suite = unittest.TestSuite() + for test_case in test_cases: + tests = loader.loadTestsFromTestCase(test_case) + suite.addTests(tests) + + return suite