Merge pull request #3547 from diffblue/smt2_concat

smt2: concat

Author: kroening

scripts/delete_failing_smt2_solver_tests

@@ -87,8 +87,6 @@ rm equality_through_struct_containing_arrays2/test.desc
 rm equality_through_union1/test.desc
 rm equality_through_union2/test.desc
 rm equality_through_union3/test.desc
-rm gcc_bswap1/test.desc
-rm gcc_vector1/test.desc
 rm graphml_witness1/test.desc
 rm integer-assignments1/test.desc
 rm memory_allocation1/test.desc

src/solvers/smt2/smt2_parser.cpp

@@ -11,6 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "smt2_format.h"
 
 #include <util/arith_tools.h>
+#include <util/range.h>
+
+#include <numeric>
 
 smt2_parsert::tokent smt2_parsert::next_token()
 {
@@ -612,15 +615,17 @@ exprt smt2_parsert::function_application()
       }
       else if(id=="concat")
       {
-        if(op.size()!=2)
-          throw error("concat takes two operands");
+        // add the widths
+        auto op_width = make_range(op).map([](const exprt &o) {
+          return to_unsignedbv_type(o.type()).get_width();
+        });
 
-        auto width0=to_unsignedbv_type(op[0].type()).get_width();
-        auto width1=to_unsignedbv_type(op[1].type()).get_width();
+        const std::size_t total_width =
+          std::accumulate(op_width.begin(), op_width.end(), 0);
 
-        unsignedbv_typet t(width0+width1);
+        const unsignedbv_typet t(total_width);
 
-        return binary_exprt(op[0], ID_concatenation, op[1], t);
+        return concatenation_exprt(std::move(op), t);
       }
       else if(id=="distinct")
       {

src/util/std_expr.h

@@ -973,22 +973,32 @@ template<> inline bool can_cast_expr<binary_relation_exprt>(const exprt &base)
 class multi_ary_exprt:public exprt
 {
 public:
-  DEPRECATED("use multi_ary_exprt(id, type) instead")
+  DEPRECATED("use multi_ary_exprt(id, op, type) instead")
   multi_ary_exprt()
   {
   }
 
-  DEPRECATED("use multi_ary_exprt(id, type) instead")
+  DEPRECATED("use multi_ary_exprt(id, op, type) instead")
   explicit multi_ary_exprt(const irep_idt &_id):exprt(_id)
   {
   }
 
+  DEPRECATED("use multi_ary_exprt(id, op, type) instead")
   multi_ary_exprt(
     const irep_idt &_id,
     const typet &_type):exprt(_id, _type)
   {
   }
 
+  multi_ary_exprt(
+    const irep_idt &_id,
+    operandst &&_operands,
+    const typet &_type)
+    : exprt(_id, _type)
+  {
+    operands() = std::move(_operands);
+  }
+
   multi_ary_exprt(
     const exprt &_lhs,
     const irep_idt &_id,
@@ -4531,31 +4541,33 @@ inline void validate_expr(const function_application_exprt &value)
   validate_operands(value, 2, "Function application must have two operands");
 }
 
-
 /// \brief Concatenation of bit-vector operands
 ///
 /// This expression takes any number of operands
-/// (a restriction to make this binary will happen in the future).
-/// The ordering of the operands is the same as in the _new_ SMT 1.x standard,
+/// The ordering of the operands is the same as in the SMT-LIB 2 standard,
 /// i.e., most-significant operands come first.
-class concatenation_exprt:public exprt
+class concatenation_exprt : public multi_ary_exprt
 {
 public:
-  DEPRECATED("use concatenation_exprt(op0, op1, type) instead")
-  concatenation_exprt():exprt(ID_concatenation)
+  DEPRECATED("use concatenation_exprt(op, type) instead")
+  concatenation_exprt() : multi_ary_exprt(ID_concatenation)
   {
   }
 
-  DEPRECATED("use concatenation_exprt(op0, op1, type) instead")
-  explicit concatenation_exprt(const typet &_type):
-    exprt(ID_concatenation, _type)
+  DEPRECATED("use concatenation_exprt(op, type) instead")
+  explicit concatenation_exprt(const typet &_type)
+    : multi_ary_exprt(ID_concatenation, _type)
   {
   }
 
   concatenation_exprt(const exprt &_op0, const exprt &_op1, const typet &_type)
-    : exprt(ID_concatenation, _type)
+    : multi_ary_exprt(_op0, ID_concatenation, _op1, _type)
+  {
+  }
+
+  concatenation_exprt(operandst &&_operands, const typet &_type)
+    : multi_ary_exprt(ID_concatenation, std::move(_operands), _type)
   {
-    add_to_operands(_op0, _op1);
   }
 };