BDDs require a namespace - pass one to guardt's or operator

Author: tautschnig

src/goto-symex/goto_symex_state.cpp

@@ -679,7 +679,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
           // that implies the current one
           return false;
 
-        write_guard|=*it;
+        write_guard.logical_or(*it, ns);
       }
     }
 
@@ -704,7 +704,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
         // that implies the current one
         return false;
 
-      read_guard|=*it;
+      read_guard.logical_or(*it, ns);
     }
 
     exprt cond=read_guard.as_expr();

src/goto-symex/symex_atomic_section.cpp

@@ -76,7 +76,7 @@ void goto_symext::symex_atomic_end(statet &state)
         it=++(r_it->second.second.begin());
         it!=r_it->second.second.end();
         ++it)
-      read_guard|=*it;
+      read_guard.logical_or(*it, ns);
     exprt read_guard_expr=read_guard.as_expr();
     do_simplify(read_guard_expr);
 
@@ -102,7 +102,7 @@ void goto_symext::symex_atomic_end(statet &state)
         it=++(w_it->second.begin());
         it!=w_it->second.end();
         ++it)
-      write_guard|=*it;
+      write_guard.logical_or(*it, ns);
     exprt write_guard_expr=write_guard.as_expr();
     do_simplify(write_guard_expr);
 

src/goto-symex/symex_goto.cpp

@@ -244,7 +244,7 @@ void goto_symext::merge_gotos(statet &state)
     merge_value_sets(goto_state, state);
 
     // adjust guard
-    state.guard|=goto_state.guard;
+    state.guard.logical_or(goto_state.guard, ns);
 
     // adjust depth
     state.depth=std::min(state.depth, goto_state.depth);

src/util/guard.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "std_expr.h"
 #include "simplify_utils.h"
-#include "symbol_table.h"
 #include "namespace.h"
 #include "guard.h"
 
@@ -169,7 +168,7 @@ guardt &operator -= (guardt &g1, const guardt &g2)
 
 /*******************************************************************\
 
-Function: operator |=
+Function: guardt::logical_or
 
   Inputs:
 
@@ -179,8 +178,10 @@ Function: operator |=
 
 \*******************************************************************/
 
-guardt &operator |= (guardt &g1, const guardt &g2)
+guardt& guardt::logical_or(const guardt &g2, const namespacet &ns)
 {
+  guardt &g1=*this;
+
   if(g2.is_false() || g1.is_true()) return g1;
   if(g1.is_false() || g2.is_true()) { g1=g2; return g1; }
 
@@ -194,8 +195,6 @@ guardt &operator |= (guardt &g1, const guardt &g2)
     else
       g1=or_exprt(g1, g2);
 
-    symbol_tablet symbol_table;
-    namespacet ns(symbol_table);
     bdd_exprt t(ns);
     t.from_expr(g1);
     g1=t.as_expr();
@@ -257,8 +256,6 @@ guardt &operator |= (guardt &g1, const guardt &g2)
     {
       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();

src/util/guard.h

@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "expr.h"
 
+class namespacet;
+
 class guardt:public exprt
 {
 public:
@@ -58,7 +60,7 @@ class guardt:public exprt
 #endif
 
   friend guardt &operator -= (guardt &g1, const guardt &g2);
-  friend guardt &operator |= (guardt &g1, const guardt &g2);
+  guardt& logical_or(const guardt &g2, const namespacet &ns);
 
 #if 0
   void swap(guardt &g)