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

@@ -9,9 +9,12 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 #include <unordered_set>
 
+#include <solvers/prop/bdd_expr.h>
+
 #include "simplify_expr_class.h"
 #include "expr.h"
 #include "namespace.h"
+#include "simplify_utils.h"
 #include "std_expr.h"
 
 /*******************************************************************\
@@ -87,6 +90,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;
@@ -188,6 +206,7 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
     }
 
     return result;
+    #endif
   }
 
   return true;