Merge pull request #4511 from diffblue/functions-is-a-lowering

functionst is a lowering, not a flattening

Author: tautschnig

src/solvers/Makefile

@@ -134,12 +134,12 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/bv_utils.cpp \
       flattening/c_bit_field_replacement_type.cpp \
       flattening/equality.cpp \
-      flattening/functions.cpp \
       flattening/pointer_logic.cpp \
       floatbv/float_bv.cpp \
       floatbv/float_utils.cpp \
       floatbv/float_approximation.cpp \
       lowering/byte_operators.cpp \
+      lowering/functions.cpp \
       lowering/popcount.cpp \
       bdd/miniBDD/miniBDD.cpp \
       prop/bdd_expr.cpp \

src/solvers/flattening/boolbv.h

@@ -19,11 +19,12 @@ Author: Daniel Kroening, [email protected]
 #include <util/mp_arith.h>
 #include <util/optional.h>
 
+#include <solvers/lowering/functions.h>
+
 #include "bv_utils.h"
 #include "boolbv_width.h"
 #include "boolbv_map.h"
 #include "arrays.h"
-#include "functions.h"
 
 class extractbit_exprt;
 class extractbits_exprt;

src/solvers/flattening/functions.cpp renamed to src/solvers/lowering/functions.cpp

@@ -8,36 +8,33 @@ 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();
-      it++)
-    add_function_constraints(it->second);
+  for(const auto &function : function_map)
+    add_function_constraints(function.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 +47,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));
 
       prop_conv.set_to_true(implication);
     }

src/solvers/flattening/functions.h renamed to src/solvers/lowering/functions.h

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Uninterpreted Functions
 
-#ifndef CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H
-#define CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H
+#ifndef CPROVER_SOLVERS_LOWERING_FUNCTIONS_H
+#define CPROVER_SOLVERS_LOWERING_FUNCTIONS_H
 
 #include <map>
 #include <set>
@@ -22,15 +22,15 @@ Author: Daniel Kroening, [email protected]
 class functionst
 {
 public:
-  explicit functionst(prop_convt &_prop_conv):
-    prop_conv(_prop_conv) { }
+  explicit functionst(prop_convt &_prop_conv) : prop_conv(_prop_conv)
+  {
+  }
 
   virtual ~functionst()
   {
   }
 
-  void record(
-    const function_application_exprt &function_application);
+  void record(const function_application_exprt &function_application);
 
   virtual void post_process()
   {
@@ -53,8 +53,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
+#endif // CPROVER_SOLVERS_LOWERING_FUNCTIONS_H

src/solvers/lowering/module_dependencies.txt

@@ -1,2 +1,3 @@
+solvers
 solvers/lowering
 util