Simplify ID_and, ID_or, ID_xor via BDDs - disabled

At present, this breaks several cbmc/Quantifier* regression tests as
it seemingly yields expressions of a shape not expected by that code.

Author: tautschnig

src/util/simplify_expr_boolean.cpp

@@ -11,8 +11,11 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 #include <unordered_set>
 
+#include <solvers/prop/bdd_expr.h>
+
 #include "expr.h"
 #include "namespace.h"
+#include "simplify_utils.h"
 #include "std_expr.h"
 
 bool simplify_exprt::simplify_boolean(exprt &expr)
@@ -79,6 +82,21 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
     if(operands.empty())
       return true;
 
+    #if 0
+    bdd_exprt t(ns);
+    t.from_expr(expr);
+    exprt tmp=t.as_expr();
+    sort_and_join(tmp);
+
+    if(tmp!=expr)
+    {
+      expr.swap(tmp);
+      return false;
+    }
+
+    return true;
+    #else
+
     bool result=true;
 
     exprt::operandst::const_iterator last;
@@ -183,6 +201,7 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
     }
 
     return result;
+    #endif
   }
 
   return true;