Make exprt a field of guard instead of inheriting

Guardt does not override virtual methods or access private fields so we
can remove inheritance and use a field instead.

Author: romainbrenguier

src/analyses/goto_rw.h

@@ -370,7 +370,7 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
     get_modet mode,
     const exprt &expr) override
   {
-    guard = true_exprt();
+    guard = guardt();
 
     rw_range_set_value_sett::get_objects_rec(_function, _target, mode, expr);
   }

src/goto-symex/symex_goto.cpp

@@ -225,7 +225,7 @@ void goto_symext::symex_goto(statet &state)
   // adjust guards
   if(new_guard.is_true())
   {
-    state.guard = false_exprt();
+    state.guard = guardt(false_exprt());
   }
   else
   {

src/util/guard.cpp

@@ -46,17 +46,17 @@ void guardt::add(const exprt &expr)
     return;
   else if(is_true() || expr.is_false())
   {
-    *this=expr;
+    this->expr = expr;
 
     return;
   }
-  else if(id()!=ID_and)
+  else if(this->expr.id() != ID_and)
   {
-    and_exprt a({*this});
-    *this=a;
+    and_exprt a({this->expr});
+    this->expr = a;
   }
 
-  operandst &op=operands();
+  exprt::operandst &op = this->expr.operands();
 
   if(expr.id()==ID_and)
     op.insert(op.end(),
@@ -68,14 +68,14 @@ void guardt::add(const exprt &expr)
 
 guardt &operator -= (guardt &g1, const guardt &g2)
 {
-  if(g1.id()!=ID_and || g2.id()!=ID_and)
+  if(g1.expr.id() != ID_and || g2.expr.id() != ID_and)
     return g1;
 
-  sort_and_join(g1);
-  guardt g2_sorted=g2;
+  sort_and_join(g1.expr);
+  exprt g2_sorted = g2.as_expr();
   sort_and_join(g2_sorted);
 
-  exprt::operandst &op1=g1.operands();
+  exprt::operandst &op1 = g1.expr.operands();
   const exprt::operandst &op2=g2_sorted.operands();
 
   exprt::operandst::iterator it1=op1.begin();
@@ -90,7 +90,7 @@ guardt &operator -= (guardt &g1, const guardt &g2)
       it1=op1.erase(it1);
   }
 
-  g1=conjunction(op1);
+  g1.expr = conjunction(op1);
 
   return g1;
 }
@@ -101,30 +101,30 @@ guardt &operator |= (guardt &g1, const guardt &g2)
     return g1;
   if(g1.is_false() || g2.is_true())
   {
-    g1=g2;
+    g1.expr = g2.expr;
     return g1;
   }
 
-  if(g1.id()!=ID_and || g2.id()!=ID_and)
+  if(g1.expr.id() != ID_and || g2.expr.id() != ID_and)
   {
-    exprt tmp(boolean_negate(g2));
+    exprt tmp(boolean_negate(g2.as_expr()));
 
-    if(tmp==g1)
-      g1 = true_exprt();
+    if(tmp == g1.as_expr())
+      g1.expr = true_exprt();
     else
-      g1=or_exprt(g1, g2);
+      g1.expr = or_exprt(g1.as_expr(), g2.as_expr());
 
     // TODO: make simplify more capable and apply here
 
     return g1;
   }
 
   // find common prefix
-  sort_and_join(g1);
-  guardt g2_sorted=g2;
+  sort_and_join(g1.expr);
+  exprt g2_sorted = g2.as_expr();
   sort_and_join(g2_sorted);
 
-  exprt::operandst &op1=g1.operands();
+  exprt::operandst &op1 = g1.expr.operands();
   const exprt::operandst &op2=g2_sorted.operands();
 
   exprt::operandst n_op1, n_op2;
@@ -160,7 +160,7 @@ guardt &operator |= (guardt &g1, const guardt &g2)
   exprt and_expr1=conjunction(n_op1);
   exprt and_expr2=conjunction(n_op2);
 
-  g1=conjunction(op1);
+  g1.expr = conjunction(op1);
 
   exprt tmp(boolean_negate(and_expr2));
 

src/util/guard.h

@@ -16,47 +16,46 @@ Author: Daniel Kroening, [email protected]
 
 #include "std_expr.h"
 
-class guardt : private exprt
+class guardt
 {
 public:
-  guardt()
+  guardt() : expr(true_exprt())
   {
-    *this = true_exprt();
   }
 
-  guardt &operator=(const exprt &e)
+  explicit guardt(const exprt &e) : expr(e)
   {
-    *this=static_cast<const guardt&>(e);
-
-    return *this;
   }
 
   void add(const exprt &expr);
 
   void append(const guardt &guard)
   {
-    add(guard);
+    add(guard.as_expr());
   }
 
   exprt as_expr() const
   {
-    return *this;
+    return expr;
   }
 
   void guard_expr(exprt &dest) const;
 
   bool is_true() const
   {
-    return exprt::is_true();
+    return expr.is_true();
   }
 
   bool is_false() const
   {
-    return exprt::is_false();
+    return expr.is_false();
   }
 
   friend guardt &operator -= (guardt &g1, const guardt &g2);
   friend guardt &operator |= (guardt &g1, const guardt &g2);
+
+private:
+  exprt expr;
 };
 
 #endif // CPROVER_UTIL_GUARD_H