Use BDDs to simplify guard expressions

Author: tautschnig

src/util/guard.cpp

@@ -13,8 +13,12 @@ Author: Daniel Kroening, [email protected]
 
 #include <ostream>
 
+#include <solvers/prop/bdd_expr.h>
+
+#include "namespace.h"
 #include "std_expr.h"
 #include "simplify_utils.h"
+#include "symbol_table.h"
 
 void guardt::guard_expr(exprt &dest) const
 {
@@ -139,7 +143,11 @@ guardt &operator |= (guardt &g1, const guardt &g2)
     else
       g1=or_exprt(g1, g2);
 
-    // TODO: make simplify more capable and apply here
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+    bdd_exprt t(ns);
+    t.from_expr(g1);
+    g1=t.as_expr();
 
     return g1;
   }
@@ -196,8 +204,15 @@ guardt &operator |= (guardt &g1, const guardt &g2)
     {
     }
     else
-      // TODO: make simplify more capable and apply here
+    {
       g1.add(or_exprt(and_expr1, and_expr2));
+
+      symbol_tablet symbol_table;
+      namespacet ns(symbol_table);
+      bdd_exprt t(ns);
+      t.from_expr(g1);
+      g1=t.as_expr();
+    }
   }
 
   return g1;