functionst is a lowering, not a flattening

No bit-flattening is happening in this reduction.

Author: Daniel Kroening

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

@@ -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>
@@ -57,4 +57,4 @@ class functionst
                         const exprt::operandst &o2);
 };
 
-#endif // CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H
+#endif // CPROVER_SOLVERS_LOWERING_FUNCTIONS_H

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

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