Upsampling BVDDs works, needs more testing

Author: ckirsch

tools/bvdd.py

@@ -287,54 +287,58 @@ def swap(self):
                     for i in pt])
         return new_bvdd.link(swap2right_bvdd, return_tuples)
 
-    def unapply(self, a_rt_inv, rt = None, rt_inv = None, index = 0):
+    def unapply(self, b_rt_inv, rt = None, rt_inv = None, index = 0):
         new_bvdd = type(self)({})
-        a_rt_inv = a_rt_inv if a_rt_inv is not None else {}
+        b_rt_inv = b_rt_inv if b_rt_inv is not None else {}
         rt = rt if rt is not None else {}
         rt_inv = rt_inv if rt_inv is not None else {}
         s2o = self.get_s2o()
         for inputs in s2o:
             output = s2o[inputs]
             if isinstance(output, BVDD):
-                output, a_rt_inv, rt, rt_inv = output.unapply(a_rt_inv, rt, rt_inv, index + 1)
+                output, b_rt_inv, rt, rt_inv = output.unapply(b_rt_inv, rt, rt_inv, index + 1)
                 new_bvdd.set(inputs, output)
             else:
                 if output not in rt_inv:
                     rt_inv[output] = len(rt_inv) + 1
-                    if output not in a_rt_inv:
-                        a_rt_inv[output] = len(a_rt_inv) + 1
-                    rt[rt_inv[output]] = a_rt_inv[output]
+                    if output not in b_rt_inv:
+                        b_rt_inv[output] = len(b_rt_inv) + 1
+                    rt[rt_inv[output]] = b_rt_inv[output]
                 new_bvdd.set(inputs, rt_inv[output])
-        return new_bvdd.reduce_SBDD().reduce_BVDD(index), a_rt_inv, rt, rt_inv
+        return new_bvdd.reduce_SBDD().reduce_BVDD(index), b_rt_inv, rt, rt_inv
 
-    def upsample(self, level, a_rt_inv = None, b_cs = None, b_rts = None, index = 0):
+    def upsample(self, level, a_rt_inv = None, b_rt_inv = None, b_cs = None, b_rts = None, index = 0):
         assert level > 0
         a_c = type(self)({})
         a_rt_inv = a_rt_inv if a_rt_inv is not None else {}
+        b_rt_inv = b_rt_inv if b_rt_inv is not None else {}
         b_cs = b_cs if b_cs is not None else {}
         b_rts = b_rts if b_rts is not None else {}
         s2o = self.get_s2o()
         for inputs in s2o:
             output = s2o[inputs]
             if isinstance(output, BVDD):
                 if index < 2**(level - 1) - 1:
-                    output, a_rt_inv, b_cs, b_rts = output.upsample(level,
-                        a_rt_inv, b_cs, b_rts, index + 1)
+                    output, a_rt_inv, b_rt_inv, b_cs, b_rts = output.upsample(level,
+                        a_rt_inv, b_rt_inv, b_cs, b_rts, index + 1)
                     a_c.set(inputs, output)
                 else:
-                    output, a_rt_inv, rt, rt_inv = output.unapply(a_rt_inv)
-                    if output not in a_rt_inv:
-                        a_rt_inv[output] = len(a_rt_inv) + 1
-                        b_cs[a_rt_inv[output]] = output
-                        b_rts[a_rt_inv[output]] = rt
-                    a_c.set(inputs, a_rt_inv[output])
+                    output, b_rt_inv, rt, rt_inv = output.unapply(b_rt_inv)
+                    key = (output, tuple(rt.values()))
+                    if key not in a_rt_inv:
+                        a_rt_inv[key] = len(a_rt_inv) + 1
+                        b_cs[a_rt_inv[key]] = output
+                        b_rts[a_rt_inv[key]] = rt
+                    a_c.set(inputs, a_rt_inv[key])
             else:
                 if output not in a_rt_inv:
                     a_rt_inv[output] = len(a_rt_inv) + 1
+                    if output not in b_rt_inv:
+                        b_rt_inv[output] = len(b_rt_inv) + 1
                     b_cs[a_rt_inv[output]] = BVDD.constant(1)
-                    b_rts[a_rt_inv[output]] = {1:a_rt_inv[output]}
+                    b_rts[a_rt_inv[output]] = {1:b_rt_inv[output]}
                 a_c.set(inputs, a_rt_inv[output])
-        return a_c.reduce_SBDD().reduce_BVDD(index), a_rt_inv, b_cs, b_rts
+        return a_c.reduce_SBDD().reduce_BVDD(index), a_rt_inv, b_rt_inv, b_cs, b_rts
 
     def downsample(self, bvdds, return_tuples):
         # apply to bvdds may reduce to constants

tools/cflobvdd.py

@@ -382,11 +382,12 @@ def upsample(self):
         if self.is_upsample_cached():
             return self.get_cached_upsample()
 
-        g_a_bvdd, _, g_b_bvdds, g_b_return_tuples = self.bvdd.upsample(self.level)
+        g_a_bvdd, g_a_rt_inv, g_b_rt_inv, g_b_bvdds, g_b_return_tuples = self.bvdd.upsample(self.level)
+
+        assert g_a_bvdd.number_of_exits() == len(g_a_rt_inv)
 
         # TODO: enable different input orderings
-        g = BV_Internal_Grouping(self.level, self.swap_level, self.fork_level, True,
-            len(g_b_return_tuples))
+        g = BV_Internal_Grouping(self.level, self.swap_level, self.fork_level, True, len(g_b_rt_inv))
 
         if g_a_bvdd.is_constant():
             g.a_connection = BV_No_Distinction_Proto.representative(self.level - 1,
@@ -414,9 +415,6 @@ def upsample(self):
 
         g.b_return_tuples = g_b_return_tuples
 
-        if g.a_connection.is_no_distinction_proto():
-            print(self)
-
         if (g.a_connection.is_no_distinction_proto() and
             g.number_of_b_connections == 1 and
             g.b_connections[1].is_no_distinction_proto()):
@@ -521,8 +519,6 @@ def reduce(self, reduction_tuple):
 
             bvdd = self.bvdd.reduce(reduction_tuple)
 
-            assert self.level == self.fork_level
-
             if bvdd.is_constant():
                 g = No_Distinction_Proto.representative(self.level,
                     self.swap_level, self.fork_level)