Replace guardt by exprt::operandst in rw_set

This was not making really use of guardt, since no guardt specific
operations where performed, but instead just represents a conjunction.
We replace that by a list of expressions and do the conjunction when
needed.
This avoids dependencies on guardt.

Author: romainbrenguier

src/goto-instrument/rw_set.cpp

@@ -79,14 +79,15 @@ void _rw_set_loct::compute()
 void _rw_set_loct::assign(const exprt &lhs, const exprt &rhs)
 {
   read(rhs);
-  read_write_rec(lhs, false, true, "", guardt(true_exprt()));
+  read_write_rec(lhs, false, true, "", exprt::operandst());
 }
 
 void _rw_set_loct::read_write_rec(
   const exprt &expr,
-  bool r, bool w,
+  bool r,
+  bool w,
   const std::string &suffix,
-  const guardt &guard)
+  const exprt::operandst &guard)
 {
   if(expr.id()==ID_symbol)
   {
@@ -96,16 +97,16 @@ void _rw_set_loct::read_write_rec(
 
     if(r)
     {
-      const auto &entry =
-        r_entries.emplace(object, entryt(symbol_expr, object, guard.as_expr()));
+      const auto &entry = r_entries.emplace(
+        object, entryt(symbol_expr, object, conjunction(guard)));
 
       track_deref(entry.first->second, true);
     }
 
     if(w)
     {
-      const auto &entry =
-        w_entries.emplace(object, entryt(symbol_expr, object, guard.as_expr()));
+      const auto &entry = w_entries.emplace(
+        object, entryt(symbol_expr, object, conjunction(guard)));
 
       track_deref(entry.first->second, false);
     }
@@ -176,12 +177,12 @@ void _rw_set_loct::read_write_rec(
     assert(expr.operands().size()==3);
     read(expr.op0(), guard);
 
-    guardt true_guard(guard);
-    true_guard.add(expr.op0());
+    exprt::operandst true_guard = guard;
+    true_guard.push_back(expr.op0());
     read_write_rec(expr.op1(), r, w, suffix, true_guard);
 
-    guardt false_guard(guard);
-    false_guard.add(not_exprt(expr.op0()));
+    exprt::operandst false_guard = guard;
+    false_guard.push_back(not_exprt(expr.op0()));
     read_write_rec(expr.op2(), r, w, suffix, false_guard);
   }
   else

src/goto-instrument/rw_set.h

@@ -18,7 +18,6 @@ Date: February 2006
 #include <vector>
 #include <set>
 
-#include <util/guard.h>
 #include <util/std_expr.h>
 
 #include <goto-programs/goto_model.h>
@@ -158,17 +157,17 @@ class _rw_set_loct:public rw_set_baset
 
   void read(const exprt &expr)
   {
-    read_write_rec(expr, true, false, "", guardt(true_exprt()));
+    read_write_rec(expr, true, false, "", exprt::operandst());
   }
 
-  void read(const exprt &expr, const guardt &guard)
+  void read(const exprt &expr, const exprt::operandst &guard)
   {
     read_write_rec(expr, true, false, "", guard);
   }
 
   void write(const exprt &expr)
   {
-    read_write_rec(expr, false, true, "", guardt(true_exprt()));
+    read_write_rec(expr, false, true, "", exprt::operandst());
   }
 
   void compute();
@@ -177,9 +176,10 @@ class _rw_set_loct:public rw_set_baset
 
   void read_write_rec(
     const exprt &expr,
-    bool r, bool w,
+    bool r,
+    bool w,
     const std::string &suffix,
-    const guardt &guard);
+    const exprt::operandst &guard);
 };
 
 class rw_set_loct:public _rw_set_loct