avoid access to exprt::opX()

This commit replaces exprt::opX by named access methods; this will
eventually enable us to protect exprt::opX().

Author: Daniel Kroening

src/solvers/flattening/arrays.cpp

@@ -546,7 +546,7 @@ void arrayst::add_array_constraints_with(
       {
         const typet &subtype = expr.type().subtype();
         index_exprt index_expr1(expr, other_index, subtype);
-        index_exprt index_expr2(expr.op0(), other_index, subtype);
+        index_exprt index_expr2(expr.old(), other_index, subtype);
 
         equal_exprt equality_expr(index_expr1, index_expr2);
 
@@ -646,12 +646,12 @@ void arrayst::add_array_constraints_array_of(
     index_exprt index_expr(expr, index, subtype);
 
     DATA_INVARIANT(
-      base_type_eq(index_expr.type(), expr.op0().type(), ns),
+      base_type_eq(index_expr.type(), expr.what().type(), ns),
       "array_of operand type should match array element type");
 
     // add constraint
     lazy_constraintt lazy(
-      lazy_typet::ARRAY_OF, equal_exprt(index_expr, expr.op0()));
+      lazy_typet::ARRAY_OF, equal_exprt(index_expr, expr.what()));
     add_array_constraint(lazy, false); // added immediately
   }
 }

src/solvers/flattening/boolbv_array_of.cpp

@@ -42,7 +42,7 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
   if(to_integer(array_size, size))
     return conversion_failed(expr);
 
-  const bvt &tmp=convert_bv(expr.op0());
+  const bvt &tmp = convert_bv(expr.what());
 
   INVARIANT(
     size * tmp.size() == width,

src/solvers/smt2/smt2_conv.cpp

@@ -3361,11 +3361,11 @@ void smt2_convt::convert_floatbv_div(const ieee_float_op_exprt &expr)
   if(use_FPA_theory)
   {
     out << "(fp.div ";
-    convert_rounding_mode_FPA(expr.op2());
+    convert_rounding_mode_FPA(expr.rounding_mode());
     out << " ";
-    convert_expr(expr.op0());
+    convert_expr(expr.lhs());
     out << " ";
-    convert_expr(expr.op1());
+    convert_expr(expr.rhs());
     out << ")";
   }
   else
@@ -3555,8 +3555,8 @@ void smt2_convt::convert_with(const with_exprt &expr)
   {
     const struct_typet &struct_type = to_struct_type(ns.follow(expr_type));
 
-    const exprt &index=expr.op1();
-    const exprt &value=expr.op2();
+    const exprt &index = expr.where();
+    const exprt &value = expr.new_value();
 
     const irep_idt &component_name=index.get(ID_component_name);
 
@@ -3569,7 +3569,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
       const std::string &smt_typename = datatype_map.at(expr_type);
 
       out << "(update-" << smt_typename << "." << component_name << " ";
-      convert_expr(expr.op0());
+      convert_expr(expr.old());
       out << " ";
       convert_expr(value);
       out << ")";
@@ -3583,7 +3583,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
         boolbv_width.get_member(struct_type, component_name);
 
       out << "(let ((?withop ";
-      convert_expr(expr.op0());
+      convert_expr(expr.old());
       out << ")) ";
 
       if(m.width==struct_width)
@@ -3626,7 +3626,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
   {
     const union_typet &union_type = to_union_type(ns.follow(expr_type));
 
-    const exprt &value=expr.op2();
+    const exprt &value = expr.new_value();
 
     std::size_t total_width=boolbv_width(union_type);
     CHECK_RETURN_WITH_DIAGNOSTICS(
@@ -3651,7 +3651,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
       out << "((_ extract "
           << (total_width-1)
           << " " << member_width << ") ";
-      convert_expr(expr.op0());
+      convert_expr(expr.old());
       out << ") ";
       flatten2bv(value);
       out << ")";

src/util/simplify_expr.cpp

@@ -1889,7 +1889,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
             exprt compo_offset = from_integer(*i, offset.type());
             plus_exprt new_offset(offset, compo_offset);
             simplify_node(new_offset);
-            exprt new_value(with.op2());
+            exprt new_value(with.new_value());
             expr.op1().swap(new_offset);
             expr.op2().swap(new_value);
             simplify_byte_update(expr); // do this recursively
@@ -1916,7 +1916,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
 
           plus_exprt new_offset(offset, index_offset);
           simplify_node(new_offset);
-          exprt new_value(with.op2());
+          exprt new_value(with.new_value());
           expr.op1().swap(new_offset);
           expr.op2().swap(new_value);
           simplify_byte_update(expr); // do this recursively