Merge pull request #5005 from romainbrenguier/bugfix/bdd-cache

Fix a bug with the cache in the BDD to exprt conversion

Author: romainbrenguier

src/solvers/prop/bdd_expr.cpp

@@ -105,17 +105,14 @@ static exprt make_or(exprt a, exprt b)
 
 /// Helper function for \c bddt to \c exprt conversion
 /// \param r: node to convert
-/// \param complement: whether we want the negation of the expression
-///        represented by r
 /// \param cache: map of already computed values
 exprt bdd_exprt::as_expr(
   const bdd_nodet &r,
-  bool complement,
   std::unordered_map<bdd_nodet::idt, exprt> &cache) const
 {
   if(r.is_constant())
   {
-    if(complement)
+    if(r.is_complement())
       return false_exprt();
     else
       return true_exprt();
@@ -129,63 +126,46 @@ exprt bdd_exprt::as_expr(
   auto insert_result = cache.emplace(r.id(), nil_exprt());
   if(insert_result.second)
   {
-    insert_result.first->second = [&]() -> exprt {
+    auto result_ignoring_complementation = [&]() -> exprt {
       if(r.else_branch().is_constant())
       {
         if(r.then_branch().is_constant())
         {
-          if(r.else_branch().is_complement() != complement)
+          if(r.else_branch().is_complement()) // else is false
             return n_expr;
-          return not_exprt(n_expr);
+          return not_exprt(n_expr); // else is true
         }
         else
         {
-          if(r.else_branch().is_complement() != complement)
+          if(r.else_branch().is_complement()) // else is false
           {
-            return make_and(
-              n_expr,
-              as_expr(
-                r.then_branch(),
-                complement != r.then_branch().is_complement(),
-                cache));
+            exprt then_case = as_expr(r.then_branch(), cache);
+            return make_and(n_expr, then_case);
           }
-          return make_or(
-            not_exprt(n_expr),
-            as_expr(
-              r.then_branch(),
-              complement != r.then_branch().is_complement(),
-              cache));
+          exprt then_case = as_expr(r.then_branch(), cache);
+          return make_or(not_exprt(n_expr), then_case);
         }
       }
       else if(r.then_branch().is_constant())
       {
-        if(r.then_branch().is_complement() != complement)
+        if(r.then_branch().is_complement()) // then is false
         {
-          return make_and(
-            not_exprt(n_expr),
-            as_expr(
-              r.else_branch(),
-              complement != r.else_branch().is_complement(),
-              cache));
+          exprt else_case = as_expr(r.else_branch(), cache);
+          return make_and(not_exprt(n_expr), else_case);
         }
-        return make_or(
-          n_expr,
-          as_expr(
-            r.else_branch(),
-            complement != r.else_branch().is_complement(),
-            cache));
+        exprt else_case = as_expr(r.else_branch(), cache);
+        return make_or(n_expr, else_case);
       }
-      return if_exprt(
-        n_expr,
-        as_expr(
-          r.then_branch(),
-          r.then_branch().is_complement() != complement,
-          cache),
-        as_expr(
-          r.else_branch(),
-          r.else_branch().is_complement() != complement,
-          cache));
+
+      exprt then_branch = as_expr(r.then_branch(), cache);
+      exprt else_branch = as_expr(r.else_branch(), cache);
+      return if_exprt(n_expr, then_branch, else_branch);
     }();
+
+    insert_result.first->second =
+      r.is_complement()
+        ? boolean_negate(std::move(result_ignoring_complementation))
+        : result_ignoring_complementation;
   }
   return insert_result.first->second;
 }
@@ -194,5 +174,5 @@ exprt bdd_exprt::as_expr(const bddt &root) const
 {
   std::unordered_map<bdd_nodet::idt, exprt> cache;
   bdd_nodet node = bdd_mgr.bdd_node(root);
-  return as_expr(node, node.is_complement(), cache);
+  return as_expr(node, cache);
 }

src/solvers/prop/bdd_expr.h

@@ -50,7 +50,6 @@ class bdd_exprt
   bddt from_expr_rec(const exprt &expr);
   exprt as_expr(
     const bdd_nodet &r,
-    bool complement,
     std::unordered_map<bdd_nodet::idt, exprt> &cache) const;
 };
 

unit/solvers/prop/bdd_expr.cpp

@@ -56,13 +56,54 @@ SCENARIO("bdd_expr", "[core][solver][prop][bdd_expr]")
     WHEN("It is converted to an exprt")
     {
       const exprt result = bdd_expr_converter.as_expr(bdd);
-      THEN("It is equal to the expression (a & !b) or (!b & a)")
+      THEN("It is equivalent to the expression !(!a || b)")
       {
-        REQUIRE(result.id() == ID_and);
-        REQUIRE(result.operands().size() == 2);
-        REQUIRE((result.op0() == a || result.op1() == a));
-        REQUIRE((result.op0() == not_exprt(b) || result.op1() == not_exprt(b)));
+        const bddt to_compare =
+          bdd_expr_converter.from_expr(not_exprt{or_exprt{not_exprt{a}, b}});
+        REQUIRE(bdd.bdd_xor(to_compare).is_false());
+        REQUIRE(bdd.bdd_xor(to_compare.bdd_not()).is_true());
       }
     }
   }
+
+  GIVEN("(!a | b) xor (a => b) ")
+  {
+    const symbol_exprt a("a", bool_typet());
+    const symbol_exprt b("b", bool_typet());
+    const bddt bdd = bdd_expr_converter.from_expr(
+      xor_exprt{or_exprt{not_exprt{a}, b}, implies_exprt{a, b}});
+    THEN("It reduces to false")
+    {
+      REQUIRE(bdd.is_false());
+    }
+  }
+
+  GIVEN("e = (a | b) xor (c | d)")
+  {
+    const symbol_exprt a("a", bool_typet());
+    const symbol_exprt b("b", bool_typet());
+    const symbol_exprt c("c", bool_typet());
+    const symbol_exprt d("d", bool_typet());
+
+    const xor_exprt expr{or_exprt{a, b}, or_exprt{c, d}};
+    const bddt bdd = bdd_expr_converter.from_expr(expr);
+
+    THEN("e xor e is false")
+    {
+      REQUIRE(bdd.bdd_xor(bdd_expr_converter.from_expr(expr)).is_false());
+    }
+
+    THEN("e xor !e is true")
+    {
+      REQUIRE(
+        bdd.bdd_xor(bdd_expr_converter.from_expr(not_exprt{expr})).is_true());
+    }
+
+    THEN("Converting to expr and back to BDD gives the same BDD")
+    {
+      const exprt expr_of_bdd = bdd_expr_converter.as_expr(bdd);
+      const bddt bdd_of_expr = bdd_expr_converter.from_expr(expr_of_bdd);
+      REQUIRE(bdd_of_expr.equals(bdd));
+    }
+  }
 }