clang-format for moved file

Author: Daniel Kroening

src/solvers/lowering/functions.cpp

@@ -8,36 +8,35 @@ Author: Daniel Kroening, [email protected]
 
 #include "functions.h"
 
-#include <util/std_types.h>
 #include <util/std_expr.h>
+#include <util/std_types.h>
 
-void functionst::record(
-  const function_application_exprt &function_application)
+void functionst::record(const function_application_exprt &function_application)
 {
-  function_map[function_application.function()].applications.
-    insert(function_application);
+  function_map[function_application.function()].applications.insert(
+    function_application);
 }
 
 void functionst::add_function_constraints()
 {
-  for(function_mapt::const_iterator it=
-      function_map.begin();
-      it!=function_map.end();
+  for(function_mapt::const_iterator it = function_map.begin();
+      it != function_map.end();
       it++)
     add_function_constraints(it->second);
 }
 
-exprt functionst::arguments_equal(const exprt::operandst &o1,
-                                  const exprt::operandst &o2)
+exprt functionst::arguments_equal(
+  const exprt::operandst &o1,
+  const exprt::operandst &o2)
 {
   PRECONDITION(o1.size() == o2.size());
 
   exprt::operandst conjuncts;
   conjuncts.reserve(o1.size());
 
-  for(std::size_t i=0; i<o1.size(); i++)
+  for(std::size_t i = 0; i < o1.size(); i++)
   {
-    exprt lhs=o1[i];
+    exprt lhs = o1[i];
     exprt rhs = typecast_exprt::conditional_cast(o2[i], o1[i].type());
     conjuncts.push_back(equal_exprt(lhs, rhs));
   }
@@ -50,21 +49,20 @@ void functionst::add_function_constraints(const function_infot &info)
   // Do Ackermann's function reduction.
   // This is quadratic, slow, and needs to be modernized.
 
-  for(std::set<function_application_exprt>::const_iterator
-      it1=info.applications.begin();
-      it1!=info.applications.end();
+  for(std::set<function_application_exprt>::const_iterator it1 =
+        info.applications.begin();
+      it1 != info.applications.end();
       it1++)
   {
-    for(std::set<function_application_exprt>::const_iterator
-        it2=info.applications.begin();
-        it2!=it1;
+    for(std::set<function_application_exprt>::const_iterator it2 =
+          info.applications.begin();
+        it2 != it1;
         it2++)
     {
-      exprt arguments_equal_expr=
+      exprt arguments_equal_expr =
         arguments_equal(it1->arguments(), it2->arguments());
 
-      implies_exprt implication(arguments_equal_expr,
-                                equal_exprt(*it1, *it2));
+      implies_exprt implication(arguments_equal_expr, equal_exprt(*it1, *it2));
 
       decision_procedure.set_to_true(implication);
     }

src/solvers/lowering/functions.h

@@ -31,8 +31,7 @@ class functionst
   {
   }
 
-  void record(
-    const function_application_exprt &function_application);
+  void record(const function_application_exprt &function_application);
 
   virtual void post_process()
   {
@@ -55,8 +54,7 @@ class functionst
   virtual void add_function_constraints();
   virtual void add_function_constraints(const function_infot &info);
 
-  exprt arguments_equal(const exprt::operandst &o1,
-                        const exprt::operandst &o2);
+  exprt arguments_equal(const exprt::operandst &o1, const exprt::operandst &o2);
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H