Merge pull request #3786 from tautschnig/deprecation-and_exprt

Construct and_exprt in a non-deprecated way

Author: tautschnig

src/solvers/flattening/functions.cpp

@@ -32,21 +32,17 @@ exprt functionst::arguments_equal(const exprt::operandst &o1,
 {
   PRECONDITION(o1.size() == o2.size());
 
-  if(o1.empty())
-    return true_exprt();
-
-  and_exprt and_expr;
-  and_exprt::operandst &conjuncts=and_expr.operands();
-  conjuncts.resize(o1.size());
+  exprt::operandst conjuncts;
+  conjuncts.reserve(o1.size());
 
   for(std::size_t i=0; i<o1.size(); i++)
   {
     exprt lhs=o1[i];
     exprt rhs = typecast_exprt::conditional_cast(o2[i], o1[i].type());
-    conjuncts[i]=equal_exprt(lhs, rhs);
+    conjuncts.push_back(equal_exprt(lhs, rhs));
   }
 
-  return std::move(and_expr);
+  return conjunction(conjuncts);
 }
 
 void functionst::add_function_constraints(const function_infot &info)

src/solvers/floatbv/float_bv.cpp

@@ -777,13 +777,11 @@ exprt float_bvt::relation(
 
     if(rel==relt::LT)
     {
-      and_exprt and_bv;
-      and_bv.reserve_operands(4);
-      and_bv.copy_to_operands(less_than3);
-      // for the case of two negative numbers
-      and_bv.copy_to_operands(not_exprt(bitwise_equal));
-      and_bv.copy_to_operands(not_exprt(both_zero));
-      and_bv.copy_to_operands(not_exprt(nan));
+      and_exprt and_bv{{less_than3,
+                        // for the case of two negative numbers
+                        not_exprt(bitwise_equal),
+                        not_exprt(both_zero),
+                        not_exprt(nan)}};
 
       return std::move(and_bv);
     }

src/util/guard.cpp

@@ -52,8 +52,7 @@ void guardt::add(const exprt &expr)
   }
   else if(id()!=ID_and)
   {
-    and_exprt a;
-    a.add_to_operands(*this);
+    and_exprt a({*this});
     *this=a;
   }
 

src/util/std_expr.cpp

@@ -53,9 +53,7 @@ exprt conjunction(const exprt::operandst &op)
     return op.front();
   else
   {
-    and_exprt result;
-    result.operands()=op;
-    return std::move(result);
+    return and_exprt(exprt::operandst(op));
   }
 }
 

src/util/std_expr.h

@@ -2467,6 +2467,11 @@ class and_exprt:public multi_ary_exprt
     : multi_ary_exprt(ID_and, {op0, op1, op2, op3}, bool_typet())
   {
   }
+
+  explicit and_exprt(exprt::operandst &&_operands)
+    : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
+  {
+  }
 };
 
 /// 1) generates a conjunction for two or more operands