Merge pull request #8 from costas-basdekis/frozenset-dis

Use `frozenset` for `Cnf.dis`

satispy/cnf.py

@@ -1,3 +1,5 @@
+from itertools import product
+
 cnfClass = None
 
 class Variable(object):
@@ -45,13 +47,13 @@ def __cmp__(self, other):
 
 class NaiveCnf(object):
     def __init__(self):
-        self.dis = []
+        self.dis = frozenset()
 
     @classmethod
     def create_from(cls, x):
         if isinstance(x, Variable):
             cnf = NaiveCnf()
-            cnf.dis = [frozenset([x])]
+            cnf.dis = frozenset([frozenset([x])])
             return cnf
         elif isinstance(x, cls):
             return x
@@ -61,18 +63,18 @@ def create_from(cls, x):
     def __and__(self, other):
         other = NaiveCnf.create_from(other)
         result = NaiveCnf()
-        result.dis = self.dis + other.dis
+        result.dis = self.dis | other.dis
         return result
 
     def __or__(self, other):
         other = NaiveCnf.create_from(other)
 
-        if len(self.dis) > 0 and len(other.dis) > 0:
-            new_dis = []
-            for d1, d2 in [(d1,d2) for d1 in self.dis for d2 in other.dis]:
-                d3 = d1 | d2
-                new_dis.append(d3)
-        elif len(self.dis) == 0:
+        if self.dis and other.dis:
+            new_dis = frozenset(
+                d1 | d2
+                for d1, d2 in product(self.dis, other.dis)
+            )
+        elif other.dis:
             new_dis = other.dis
         else:
             new_dis = self.dis
@@ -89,8 +91,10 @@ def __neg__(self):
 
         for d in self.dis:
             c = NaiveCnf()
-            for v in d:
-                c.dis.append(frozenset([-v]))
+            c.dis = frozenset(
+                frozenset([-v])
+                for v in d
+            )
             cnfs.append(c)
 
         ret = NaiveCnf()
@@ -141,19 +145,19 @@ def reduceCnf(cnf):
         if dont_add: continue
         # TODO: Is this necessary anymore? Probably not. Do statistical analysis.
         if x not in output.dis:
-            output.dis.append(x)
+            output.dis |= frozenset([x])
     return output
 #end def reduceCnf(cnf)
 
 class Cnf(object):
     def __init__(self):
-        self.dis = []
+        self.dis = frozenset()
 
     @classmethod
     def create_from(cls, x):
         if isinstance(x, Variable):
             cnf = Cnf()
-            cnf.dis = [frozenset([x])]
+            cnf.dis = frozenset([frozenset([x])])
             return cnf
         elif isinstance(x, cls):
             return x
@@ -163,19 +167,18 @@ def create_from(cls, x):
     def __and__(self, other):
         other = Cnf.create_from(other)
         result = Cnf()
-        result.dis = self.dis + other.dis
+        result.dis = self.dis | other.dis
         return result
 
     def __or__(self, other):
         other = Cnf.create_from(other)
 
-        if len(self.dis) > 0 and len(other.dis) > 0:
-            new_dis = []
-            for d1, d2 in [(d1,d2) for d1 in self.dis for d2 in other.dis]:
-                d3 = d1 | d2
-                if d3 not in new_dis:
-                    new_dis.append(d3)
-        elif len(self.dis) == 0:
+        if self.dis and other.dis:
+            new_dis = frozenset(
+                d1 | d2
+                for d1, d2 in product(self.dis, other.dis)
+            )
+        elif other.dis:
             new_dis = other.dis
         else:
             new_dis = self.dis
@@ -192,8 +195,10 @@ def __neg__(self):
 
         for d in self.dis:
             c = Cnf()
-            for v in d:
-                c.dis.append(frozenset([-v]))
+            c.dis = frozenset(
+                frozenset([-v])
+                for v in d
+            )
             x = reduceCnf(c)
             if x not in cnfs:
                 cnfs.append(x)

satispy/io/dimacs_cnf.py

@@ -64,8 +64,10 @@ def fromstring(self, s):
         c = Cnf()
 
         lines = new_lines[1:]
-        for line in lines:
-            c.dis.append(frozenset(map(lambda vn: Variable("v"+vn.strip(" \t\r\n-"), vn[0] == '-'), line.split(" ")[:-1])))
+        c.dis = frozenset(
+            frozenset(map(lambda vn: Variable("v"+vn.strip(" \t\r\n-"), vn[0] == '-'), line.split(" ")[:-1]))
+            for line in lines
+        )
 
         for i in xrange(1,varz+1):
             stri = str(i)

tests/run_tests.py

@@ -2,6 +2,7 @@
 
 import os
 import sys
+from itertools import permutations
 
 sys.path.insert(0, os.path.dirname(os.path.dirname(os.path.realpath(__file__))))
 
@@ -28,6 +29,47 @@ def testEqualits(self):
 
         self.assertNotEqual(v1,-v1)
 
+    def testOrderOfOperationsDontMatter(self):
+        v1 = Variable("v1")
+        v2 = Variable("v2")
+        v3 = Variable("v3")
+
+        variables = [v1, v2, v3]
+
+        two_variables_permutations = list(permutations(variables[:2]))
+        different_and_variables = {
+            va & vb
+            for va, vb in two_variables_permutations
+        }
+        self.assertEqual(len(different_and_variables), 1)
+        different_or_variables = {
+            va | vb
+            for va, vb in two_variables_permutations
+        }
+        self.assertEqual(len(different_or_variables), 1)
+        different_xor_variables = {
+            va ^ vb
+            for va, vb in two_variables_permutations
+        }
+        self.assertEqual(len(different_xor_variables), 1)
+
+        three_variables_permutations = list(permutations(variables[:3]))
+        different_and_variables = {
+            va & vb & vc
+            for va, vb, vc in three_variables_permutations
+        }
+        self.assertEqual(len(different_and_variables), 1)
+        different_or_variables = {
+            va | vb | vc
+            for va, vb, vc in three_variables_permutations
+        }
+        self.assertEqual(len(different_or_variables), 1)
+        different_xor_variables = {
+            va ^ vb ^ vc
+            for va, vb, vc in three_variables_permutations
+        }
+        self.assertEqual(len(different_xor_variables), 1)
+
     def testHash(self):
         v1 = Variable("v1")
         v2 = Variable("v1")
@@ -86,7 +128,7 @@ def testAnd(self):
         v1 = Variable("v1")
         v2 = Variable("v2")
         cnf = v1 & v2
-        self.assertEqual(set([frozenset([v1]),frozenset([v2])]), set(cnf.dis))
+        self.assertEqual(frozenset([frozenset([v1]), frozenset([v2])]), cnf.dis)
 
     def testOr(self):
         v1 = Variable("v1")
@@ -96,21 +138,21 @@ def testOr(self):
 
         cnf1 = v1 | v2
 
-        self.assertEqual(set([frozenset([v1,v2])]), set(cnf1.dis))
+        self.assertEqual(frozenset([frozenset([v1,v2])]), cnf1.dis)
 
         cnf2 = cnf1 | v3
 
-        self.assertEqual(set([frozenset([v1,v2,v3])]), set(cnf2.dis))
+        self.assertEqual(frozenset([frozenset([v1,v2,v3])]), cnf2.dis)
 
         # Test empty CNF or
         cnf = Cnf()
         cnf |= v1
 
-        self.assertEqual(set([frozenset([v1])]), set(cnf.dis))
+        self.assertEqual(frozenset([frozenset([v1])]), cnf.dis)
 
     def testCreateFrom(self):
         v1 = Variable("v1")
-        self.assertEqual(set([frozenset([v1])]), set(Cnf.create_from(v1).dis))
+        self.assertEqual(frozenset([frozenset([v1])]), Cnf.create_from(v1).dis)
 
     def testMixed(self):
         v1 = Variable("v1")
@@ -119,31 +161,31 @@ def testMixed(self):
         v4 = Variable("v4")
 
         self.assertEqual(
-            set([
+            frozenset([
                 frozenset([v1,v2]),
                 frozenset([v3])
             ]),
-            set(((v1 | v2) & v3).dis)
+            ((v1 | v2) & v3).dis
         )
 
         # Distribution
         self.assertEqual(
-            set([
+            frozenset([
                 frozenset([v1,v3]),
                 frozenset([v2,v3])
             ]),
-            set(((v1 & v2) | v3).dis)
+            ((v1 & v2) | v3).dis
         )
 
         # Double distribution
         self.assertEqual(
-            set([
+            frozenset([
                 frozenset([v1,v3]),
                 frozenset([v1,v4]),
                 frozenset([v2,v3]),
                 frozenset([v2,v4])
             ]),
-            set(((v1 & v2) | (v3 & v4)).dis)
+            ((v1 & v2) | (v3 & v4)).dis
         )
 
     def testNegation(self):
@@ -152,8 +194,8 @@ def testNegation(self):
         v3 = Variable("v3")
 
         self.assertEqual(
-            set([frozenset([-v1])]),
-            set((-Cnf.create_from(v1)).dis)
+            frozenset([frozenset([-v1])]),
+            (-Cnf.create_from(v1)).dis
         )
 
     def testXor(self):
@@ -163,20 +205,20 @@ def testXor(self):
         cnf = v1 ^ v2
 
         self.assertEqual(
-            set([
+            frozenset([
                 frozenset([v1,v2]),
                 frozenset([-v1,-v2])
             ]),
-            set(cnf.dis)
+            cnf.dis
         )
 
     def testImplication(self):
         v1 = Variable("v1")
         v2 = Variable("v2")
 
         self.assertEqual(
-            set([frozenset([-v1,v2])]),
-            set((v1 >> v2).dis)
+            frozenset([frozenset([-v1,v2])]),
+            (v1 >> v2).dis
         )
 
 class DimacsTest(unittest.TestCase):