Considering None in BVDD expressions

Author: ckirsch

tools/bitme.py

@@ -185,7 +185,9 @@ def get_input_expression(var_line, inputs):
             return [comparison_line]
 
     def get_bvdd_node_expression(sid_line, bvdd, sbdd, index = 0):
-        if isinstance(bvdd, bool) or isinstance(bvdd, int):
+        if bvdd is None:
+            return None
+        elif isinstance(bvdd, bool) or isinstance(bvdd, int):
             return Constd(btor2.Parser.next_nid(), sid_line, int(bvdd),
                 "domain-propagated value", 0)
         elif bvdd.is_dont_care():
@@ -205,9 +207,12 @@ def get_bvdd_node_expression(sid_line, bvdd, sbdd, index = 0):
                     if sbdd:
                         assert 0 <= inputs < 256
                         inputs = 2**inputs
+                    output_line = Values.get_bvdd_node_expression(sid_line, output, sbdd, index + 1)
+                    if output_line is None:
+                        continue
                     exp_line = Ite(btor2.Parser.next_nid(), sid_line,
                         Values.get_input_expression(var_line, inputs)[0],
-                        Values.get_bvdd_node_expression(sid_line, output, sbdd, index + 1),
+                        output_line,
                         exp_line,
                         var_line.comment, var_line.line_no)
         return exp_line

tools/bvdd.py

@@ -221,6 +221,9 @@ def intersection(self, bvdd2, bvdd3 = None):
     def is_not_empty(self):
         return not (self.is_constant() and self.get_dont_care_output() is None)
 
+    def is_not_full(self):
+        return not (self.is_constant() and self.get_dont_care_output() is not None)
+
     # for CFLOBVDDs
 
     def projection_proto(index):

tools/pdd.py

@@ -30,7 +30,7 @@ def is_consistent(self):
         for output1_value in self.o2s:
             inputs1 = self.o2s[output1_value]
             if len(self.o2s) == 1:
-                if not inputs1.is_constant() or inputs1.get_dont_care_output() is None:
+                if inputs1.is_not_full():
                     return False
             for output2_value in self.o2s:
                 if output1_value != output2_value: