Apply clang-format suggestions

No function change.
The change have been generated automatically by clang-format.

Author: romainbrenguier

src/solvers/smt2/smt2_ast.cpp

@@ -101,12 +101,11 @@ static std::function<smt2_astt(smt2_astt)> make_function(smt2_astt f)
 std::function<smt2_astt(smt2_astt)>
 smt2_extract(const mp_integer &width, const mp_integer &offset)
 {
-  return make_function(
-    smt2_astt::make(
-      "_",
-      smt2_astt("extract"),
-      smt2_astt::integer(width),
-      smt2_astt::integer(offset)));
+  return make_function(smt2_astt::make(
+    "_",
+    smt2_astt("extract"),
+    smt2_astt::integer(width),
+    smt2_astt::integer(offset)));
 }
 
 smt2_astt smt2_eq(smt2_astt left, smt2_astt right)

src/solvers/smt2/smt2_conv.cpp

@@ -871,12 +871,11 @@ smt2_astt smt2_convt::convert_expr(const exprt &expr)
         // do bitnot component-by-component
         for(mp_integer i=0; i!=size; ++i)
         {
-          bvnot_node.add_child(
+          bvnot_node.add_child(smt2_astt::make(
+            "bvnot",
             smt2_astt::make(
-              "bvnot",
-              smt2_astt::make(
-                smt_typename + "." + std::to_string((size - i - 1).to_long()),
-                smt2_astt("?vectorop"))));
+              smt_typename + "." + std::to_string((size - i - 1).to_long()),
+              smt2_astt("?vectorop"))));
         }
 
         return smt2_let(
@@ -932,12 +931,11 @@ smt2_astt smt2_convt::convert_expr(const exprt &expr)
         // negate component-by-component
         for(mp_integer i=0; i!=size; ++i)
         {
-          bvneg_node.add_child(
+          bvneg_node.add_child(smt2_astt::make(
+            "bvneg",
             smt2_astt::make(
-              "bvneg",
-              smt2_astt::make(
-                smt_typename + "." + std::to_string((size - i - 1).to_long()),
-                smt2_astt("?vectorop"))));
+              smt_typename + "." + std::to_string((size - i - 1).to_long()),
+              smt2_astt("?vectorop"))));
         }
 
         return smt2_let(
@@ -1319,9 +1317,8 @@ smt2_astt smt2_convt::convert_expr(const exprt &expr)
     {
       typecast_exprt tmp(extractbit_expr.index(), extractbit_expr.src().type());
       return smt2_eq(
-        smt2_extract(0, 0)(
-          smt2_astt::make(
-            "bvlshr", flatten2bv(extractbit_expr.src()), convert_expr(tmp))),
+        smt2_extract(0, 0)(smt2_astt::make(
+          "bvlshr", flatten2bv(extractbit_expr.src()), convert_expr(tmp))),
         smt2_astt("bin1"));
     }
   }
@@ -1538,21 +1535,19 @@ smt2_astt smt2_convt::convert_expr(const exprt &expr)
               convert_expr(expr.op0())),
             smt2_sign_extend(smt2_astt::integer(mp_integer(1)))(
               convert_expr(expr.op1()))))},
-        smt2_not(
-          smt2_eq(
-            smt2_extract(width, width)(smt2_astt("?sum")),
-            smt2_extract(width - 1, width - 1)(smt2_astt("?sum")))));
+        smt2_not(smt2_eq(
+          smt2_extract(width, width)(smt2_astt("?sum")),
+          smt2_extract(width - 1, width - 1)(smt2_astt("?sum")))));
     }
     else if(op_type.id()==ID_unsignedbv ||
             op_type.id()==ID_pointer)
     {
       // overflow is simply carry-out
       return smt2_eq(
-        smt2_extract(width, width)(
-          smt2_astt::make(
-            (subtract ? "bvsub" : "bvadd"),
-            smt2_zero_extend(1)(convert_expr(expr.op0())),
-            smt2_zero_extend(1)(convert_expr(expr.op1())))),
+        smt2_extract(width, width)(smt2_astt::make(
+          (subtract ? "bvsub" : "bvadd"),
+          smt2_zero_extend(1)(convert_expr(expr.op0())),
+          smt2_zero_extend(1)(convert_expr(expr.op1())))),
         smt2_astt("#b1"));
     }
     else
@@ -1732,12 +1727,11 @@ smt2_astt smt2_convt::convert_expr(const exprt &expr)
 
           for(std::size_t byte = 0; byte < bytes; byte++)
           {
-            bindings.push_back(
-              std::make_pair(
-                smt2_astt("bswap_byte_" + byte),
-                smt2_extract(
-                  (byte * bits_per_byte + (bits_per_byte - 1)),
-                  (byte * bits_per_byte))(smt2_astt("bswap_op"))));
+            bindings.push_back(std::make_pair(
+              smt2_astt("bswap_byte_" + byte),
+              smt2_extract(
+                (byte * bits_per_byte + (bits_per_byte - 1)),
+                (byte * bits_per_byte))(smt2_astt("bswap_op"))));
           }
 
           auto concat_node = smt2_astt::make("concat");
@@ -1872,9 +1866,8 @@ smt2_astt smt2_convt::convert_typecast(const typecast_exprt &expr)
             if(to_width > from_integer_bits)
             {
               return smt2_sign_extend(
-                smt2_astt::integer(to_width - from_integer_bits))(
-                smt2_extract(from_width - 1, from_fraction_bits)(
-                  convert_expr(src)));
+                smt2_astt::integer(to_width - from_integer_bits))(smt2_extract(
+                from_width - 1, from_fraction_bits)(convert_expr(src)));
             }
             else
             {
@@ -1885,10 +1878,9 @@ smt2_astt smt2_convt::convert_typecast(const typecast_exprt &expr)
           }(),
           smt2_ite(
             smt2_and(
-              smt2_not(
-                smt2_eq(
-                  smt2_extract(from_fraction_bits - 1, 0)(smt2_astt("?tcop")),
-                  smt2_bv(0, from_fraction_bits))),
+              smt2_not(smt2_eq(
+                smt2_extract(from_fraction_bits - 1, 0)(smt2_astt("?tcop")),
+                smt2_bv(0, from_fraction_bits))),
               smt2_eq(
                 smt2_extract(from_width - 1, from_width - 1)(
                   smt2_astt("?tcop")),
@@ -2061,9 +2053,8 @@ smt2_astt smt2_convt::convert_typecast(const typecast_exprt &expr)
             }
             else
             {
-              return smt2_sign_extend(
-                smt2_astt::integer(to_integer_bits - from_width))(
-                convert_expr(src));
+              return smt2_sign_extend(smt2_astt::integer(
+                to_integer_bits - from_width))(convert_expr(src));
             }
           }
         }(),
@@ -2690,10 +2681,8 @@ smt2_astt smt2_convt::convert_is_dynamic_object(const exprt &expr)
       auto node = smt2_astt::make("or");
       for(const auto &object : dynamic_objects)
       {
-        node.add_child(
-          smt2_eq(
-            smt2_bv(object, config.bv_encoding.object_bits),
-            smt2_astt("?obj")));
+        node.add_child(smt2_eq(
+          smt2_bv(object, config.bv_encoding.object_bits), smt2_astt("?obj")));
       }
       return node;
     }());
@@ -3099,12 +3088,11 @@ smt2_astt smt2_convt::convert_div(const div_exprt &expr)
     fixedbv_spect spec(to_fixedbv_type(expr.type()));
     std::size_t fraction_bits=spec.get_fraction_bits();
 
-    return smt2_extract(spec.width - 1, 0)(
+    return smt2_extract(spec.width - 1, 0)(smt2_astt::make(
+      "bvsdiv",
       smt2_astt::make(
-        "bvsdiv",
-        smt2_astt::make(
-          "concat", convert_expr(expr.op0()), smt2_bv(0, fraction_bits)),
-        smt2_sign_extend(fraction_bits)(convert_expr(expr.op1()))));
+        "concat", convert_expr(expr.op0()), smt2_bv(0, fraction_bits)),
+      smt2_sign_extend(fraction_bits)(convert_expr(expr.op1()))));
   }
   else if(expr.type().id()==ID_floatbv)
   {
@@ -3498,24 +3486,22 @@ smt2_astt smt2_convt::convert_index(const index_exprt &expr)
       std::size_t sub_width=boolbv_width(array_type.subtype());
       std::size_t index_width=boolbv_width(expr.index().type());
 
-      auto node = smt2_extract(sub_width - 1, 0)(
-        smt2_astt::make(
-          "bvlshr",
-          convert_expr(expr.array()),
-          smt2_astt::make("bvmul", smt2_bv(sub_width, array_width), [&] {
-            // SMT2 says that the shift distance must be the same as
-            // the width of what we shift.
-            if(array_width > index_width)
-            {
-              return smt2_zero_extend(array_width - index_width)(
-                convert_expr(expr.index()));
-            }
-            else
-            {
-              return smt2_extract(array_width - 1, 0)(
-                convert_expr(expr.index()));
-            }
-          }())));
+      auto node = smt2_extract(sub_width - 1, 0)(smt2_astt::make(
+        "bvlshr",
+        convert_expr(expr.array()),
+        smt2_astt::make("bvmul", smt2_bv(sub_width, array_width), [&] {
+          // SMT2 says that the shift distance must be the same as
+          // the width of what we shift.
+          if(array_width > index_width)
+          {
+            return smt2_zero_extend(array_width - index_width)(
+              convert_expr(expr.index()));
+          }
+          else
+          {
+            return smt2_extract(array_width - 1, 0)(convert_expr(expr.index()));
+          }
+        }())));
 
       return unflatten(array_type.subtype(), std::move(node));
     }
@@ -3537,11 +3523,10 @@ smt2_astt smt2_convt::convert_index(const index_exprt &expr)
       }
       else
       {
-        return smt2_astt(
-          std::vector<smt2_astt>{smt2_index(
-                                   smt2_astt(smt_typename),
-                                   smt2_astt::integer(index_int->to_long())),
-                                 convert_expr(expr.array())});
+        return smt2_astt(std::vector<smt2_astt>{
+          smt2_index(
+            smt2_astt(smt_typename), smt2_astt::integer(index_int->to_long())),
+          convert_expr(expr.array())});
       }
     }
     else
@@ -3628,11 +3613,9 @@ smt2_astt smt2_convt::flatten2bv(const exprt &expr)
       auto concat_node = smt2_astt::make("concat");
       for(mp_integer i=0; i!=size; ++i)
       {
-        concat_node.add_child(
-          smt2_astt(
-            std::vector<smt2_astt>{
-              smt2_index(smt2_astt(smt_typename), smt2_astt::integer(i)),
-              smt2_astt("?vflop")}));
+        concat_node.add_child(smt2_astt(std::vector<smt2_astt>{
+          smt2_index(smt2_astt(smt_typename), smt2_astt::integer(i)),
+          smt2_astt("?vflop")}));
       }
       return smt2_let(
         {std::make_pair(smt2_astt("?vflop"), convert_expr(expr))},
@@ -3656,22 +3639,20 @@ smt2_astt smt2_convt::flatten2bv(const exprt &expr)
       const struct_typet::componentst &components=
         struct_type.components();
 
-      auto concat_node = smt2_astt(
-        std::vector<smt2_astt>{
-          smt2_index(
-            smt2_astt(smt_typename),
-            smt2_astt(id2string(components[0].get_name()))),
-          smt2_astt("?sflop")});
+      auto concat_node = smt2_astt(std::vector<smt2_astt>{
+        smt2_index(
+          smt2_astt(smt_typename),
+          smt2_astt(id2string(components[0].get_name()))),
+        smt2_astt("?sflop")});
 
       // SMT-LIB 2 concat is binary only
       for(std::size_t i = 0; i < components.size(); ++i)
       {
         concat_node = smt2_concat(
-          smt2_astt(
-            std::vector<smt2_astt>{smt2_index(
-                                     smt2_astt(smt_typename),
-                                     smt2_astt(components[i - 1].get_name())),
-                                   smt2_astt("?sflop")}),
+          smt2_astt(std::vector<smt2_astt>{
+            smt2_index(
+              smt2_astt(smt_typename), smt2_astt(components[i - 1].get_name())),
+            smt2_astt("?sflop")}),
           std::move(concat_node));
       }
 
@@ -3729,9 +3710,8 @@ smt2_convt::unflatten(const typet &type, smt2_astt ast, unsigned nesting)
           auto extract_node = smt2_extract(offset + subtype_width - 1, offset)(
             smt2_astt("?ufop"));
           extract_node.add_child(smt2_astt::integer(nesting));
-          mk_node.add_child(
-            unflatten(
-              vector_type.subtype(), std::move(extract_node), nesting + 1));
+          mk_node.add_child(unflatten(
+            vector_type.subtype(), std::move(extract_node), nesting + 1));
         }
         return mk_node;
       }());
@@ -3745,8 +3725,7 @@ smt2_convt::unflatten(const typet &type, smt2_astt ast, unsigned nesting)
     }
 
     return smt2_let(
-      {std::make_pair(smt2_astt("?ufop"), smt2_astt::integer(nesting))},
-      [&]() {
+      {std::make_pair(smt2_astt("?ufop"), smt2_astt::integer(nesting))}, [&]() {
         // TODO ast is missing from here!!!
 
         // extract members