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

Author: tautschnig

src/goto-symex/goto_symex_state.cpp

@@ -575,7 +575,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);
       }
     }
 
@@ -600,7 +600,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

@@ -57,7 +57,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);
 
@@ -83,7 +83,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

@@ -235,17 +235,19 @@ void goto_symext::merge_goto(
   const statet::goto_statet &goto_state,
   statet &state)
 {
+  statet::goto_statet &goto_state=*list_it;
+
   // check atomic section
   if(state.atomic_section_id!=goto_state.atomic_section_id)
-    throw "atomic sections differ across branches";
+    throw "Atomic sections differ across branches";
 
   // do SSA phi functions
   phi_function(goto_state, 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

@@ -123,15 +123,12 @@ guardt &operator -= (guardt &g1, const guardt &g2)
   return g1;
 }
 
-guardt &operator |= (guardt &g1, const guardt &g2)
+guardt& guardt::logical_or(const guardt &g2, const namespacet &ns)
 {
-  if(g2.is_false() || g1.is_true())
-    return g1;
-  if(g1.is_false() || g2.is_true())
-  {
-    g1=g2;
-    return g1;
-  }
+  guardt &g1=*this;
+
+  if(g2.is_false() || g1.is_true()) return g1;
+  if(g1.is_false() || g2.is_true()) { g1=g2; return g1; }
 
   if(g1.id()!=ID_and || g2.id()!=ID_and)
   {
@@ -143,8 +140,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();
@@ -207,8 +202,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

@@ -16,6 +16,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "expr.h"
 
+class namespacet;
+
 class guardt:public exprt
 {
 public:
@@ -61,7 +63,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)