Merge pull request #3776 from tautschnig/deprecation-equal_exprt

Construct equal_exprt in a non-deprecated way

Author: tautschnig

src/analyses/invariant_set.cpp

@@ -752,9 +752,8 @@ void invariant_sett::nnf(exprt &expr, bool negate)
       typecast_expr.op().type().id() == ID_unsignedbv ||
       typecast_expr.op().type().id() == ID_signedbv)
     {
-      equal_exprt tmp;
-      tmp.lhs() = typecast_expr.op();
-      tmp.rhs() = from_integer(0, typecast_expr.op().type());
+      equal_exprt tmp(
+        typecast_expr.op(), from_integer(0, typecast_expr.op().type()));
       nnf(tmp, !negate);
       expr.swap(tmp);
     }
@@ -1053,9 +1052,7 @@ void invariant_sett::assignment(
   const exprt &lhs,
   const exprt &rhs)
 {
-  equal_exprt equality;
-  equality.lhs()=lhs;
-  equality.rhs()=rhs;
+  equal_exprt equality(lhs, rhs);
 
   // first evaluate RHS
   simplify(equality.rhs());

src/ansi-c/c_typecheck_expr.cpp

@@ -2540,8 +2540,8 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    equal_exprt equality_expr;
-    equality_expr.operands()=expr.arguments();
+    equal_exprt equality_expr(
+      expr.arguments().front(), expr.arguments().back());
     equality_expr.add_source_location()=source_location;
 
     if(!base_type_eq(equality_expr.lhs().type(),

src/goto-programs/goto_convert.cpp

@@ -1156,9 +1156,7 @@ exprt goto_convertt::case_guard(
 
     forall_expr(it, case_op)
     {
-      equal_exprt eq_expr;
-      eq_expr.lhs() = value;
-      eq_expr.rhs() = *it;
+      equal_exprt eq_expr(value, *it);
       dest.move_to_operands(eq_expr);
     }
     INVARIANT(

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -143,9 +143,6 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 
       // add implications
 
-      equal_exprt equality;
-      equality.lhs() = expr.offset(); // index operand
-
       // type of index operand
       const typet &constant_type = expr.offset().type();
 
@@ -154,8 +151,6 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 
       for(std::size_t i=0; i<bytes; i++)
       {
-        equality.rhs()=from_integer(i, constant_type);
-
         std::size_t offset=i*byte_width;
 
         for(std::size_t j=0; j<width; j++)
@@ -164,23 +159,20 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
           else
             equal_bv[j]=const_literal(true);
 
-        prop.l_set_to_true(
-          prop.limplies(convert(equality), prop.land(equal_bv)));
+        prop.l_set_to_true(prop.limplies(
+          convert(equal_exprt(expr.offset(), from_integer(i, constant_type))),
+          prop.land(equal_bv)));
       }
     }
     else
     {
-      equal_exprt equality;
-      equality.lhs() = expr.offset(); // index operand
-
       // type of index operand
       const typet &constant_type = expr.offset().type();
 
       for(std::size_t i=0; i<bytes; i++)
       {
-        equality.rhs()=from_integer(i, constant_type);
-
-        literalt e=convert(equality);
+        literalt e =
+          convert(equal_exprt(expr.offset(), from_integer(i, constant_type)));
 
         std::size_t offset=i*byte_width;
 

src/solvers/flattening/boolbv_byte_update.cpp

@@ -85,9 +85,8 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
   for(std::size_t offset=0; offset<bv.size(); offset+=byte_width)
   {
     // index condition
-    equal_exprt equality;
-    equality.lhs()=offset_expr;
-    equality.rhs()=from_integer(offset/byte_width, offset_expr.type());
+    equal_exprt equality(
+      offset_expr, from_integer(offset / byte_width, offset_expr.type()));
     literalt equal=convert(equality);
 
     bv_endianness_mapt map_op(op.type(), little_endian, ns, boolbv_width);

src/solvers/flattening/boolbv_extractbit.cpp

@@ -51,11 +51,8 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
       std::max(address_bits(src_bv_width), index_bv_width);
     unsignedbv_typet index_type(index_width);
 
-    equal_exprt equality;
-    equality.lhs() = expr.index();
-
-    if(index_type!=equality.lhs().type())
-      equality.lhs().make_typecast(index_type);
+    equal_exprt equality(
+      typecast_exprt::conditional_cast(expr.index(), index_type), exprt());
 
     if(prop.has_set_to())
     {

src/solvers/flattening/boolbv_index.cpp

@@ -144,12 +144,6 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
       // add implications
 
-      equal_exprt index_equality;
-      index_equality.lhs()=index; // index operand
-
-      equal_exprt value_equality;
-      value_equality.lhs()=result;
-
 #ifdef COMPACT_EQUAL_CONST
       bv_utils.equal_const_register(convert_bv(index));  // Definitely
       bv_utils.equal_const_register(convert_bv(result)); // Maybe
@@ -159,19 +153,15 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
       for(mp_integer i=0; i<array_size; i=i+1)
       {
-        index_equality.rhs()=from_integer(i, index_equality.lhs().type());
-        CHECK_RETURN(index_equality.rhs().is_not_nil());
-
         INVARIANT(
           it != array.operands().end(),
           "this loop iterates over the array, so `it` shouldn't be increased "
           "past the array's end");
 
-        value_equality.rhs()=*it++;
-
         // Cache comparisons and equalities
-        prop.l_set_to_true(convert(implies_exprt(index_equality,
-                                                 value_equality)));
+        prop.l_set_to_true(convert(implies_exprt(
+          equal_exprt(index, from_integer(i, index.type())),
+          equal_exprt(result, *it++))));
       }
 
       return bv;
@@ -203,9 +193,6 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
       // add implications
 
-      equal_exprt index_equality;
-      index_equality.lhs()=index; // index operand
-
 #ifdef COMPACT_EQUAL_CONST
       bv_utils.equal_const_register(convert_bv(index));  // Definitely
 #endif
@@ -215,26 +202,21 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
       for(mp_integer i=0; i<array_size; i=i+1)
       {
-        index_equality.rhs()=from_integer(i, index_equality.lhs().type());
-        CHECK_RETURN(index_equality.rhs().is_not_nil());
-
         mp_integer offset=i*width;
 
         for(std::size_t j=0; j<width; j++)
           equal_bv[j] = prop.lequal(
             bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
 
-        prop.l_set_to_true(
-          prop.limplies(convert(index_equality), prop.land(equal_bv)));
+        prop.l_set_to_true(prop.limplies(
+          convert(equal_exprt(index, from_integer(i, index.type()))),
+          prop.land(equal_bv)));
       }
     }
     else
     {
       bv.resize(width);
 
-      equal_exprt equality;
-      equality.lhs()=index; // index operand
-
 #ifdef COMPACT_EQUAL_CONST
       bv_utils.equal_const_register(convert_bv(index));  // Definitely
 #endif
@@ -247,9 +229,8 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
       for(mp_integer i=0; i<array_size; i=i+1)
       {
-        equality.op1()=from_integer(i, constant_type);
-
-        literalt e=convert(equality);
+        literalt e =
+          convert(equal_exprt(index, from_integer(i, constant_type)));
 
         mp_integer offset=i*width;