From 4819fdabee81326bb57b6346c498ac7a49a74037 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 12 Jan 2019 18:22:15 +0000
Subject: [PATCH] Construct and_exprt in a non-deprecated way

The default constructor is deprecated. To facilitate construction with an
arbitrary number of operands a new constructor taking a initializer list is
added.
---
 src/solvers/flattening/functions.cpp | 12 ++++--------
 src/solvers/floatbv/float_bv.cpp     | 12 +++++-------
 src/util/guard.cpp                   |  3 +--
 src/util/std_expr.cpp                |  4 +---
 src/util/std_expr.h                  |  5 +++++
 5 files changed, 16 insertions(+), 20 deletions(-)

diff --git a/src/solvers/flattening/functions.cpp b/src/solvers/flattening/functions.cpp
index 9b14b16acf7..2588275b14f 100644
--- a/src/solvers/flattening/functions.cpp
+++ b/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)
diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp
index 10a65a64e00..eddb67a13ca 100644
--- a/src/solvers/floatbv/float_bv.cpp
+++ b/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);
     }
diff --git a/src/util/guard.cpp b/src/util/guard.cpp
index 6e501f3f558..3e99bba4d1a 100644
--- a/src/util/guard.cpp
+++ b/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;
   }
 
diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp
index 39f8c578f06..6e0d47456cb 100644
--- a/src/util/std_expr.cpp
+++ b/src/util/std_expr.cpp
@@ -55,9 +55,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));
   }
 }
 
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index b94f17931bd..eeda6344d20 100644
--- a/src/util/std_expr.h
+++ b/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