From e643f8481f88ab46bd237edeeeb0db4e0944040e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 8 Apr 2019 13:00:24 +0100 Subject: [PATCH 1/3] functionst is a lowering, not a flattening No bit-flattening is happening in this reduction. --- src/solvers/Makefile | 2 +- src/solvers/flattening/boolbv.h | 3 ++- src/solvers/{flattening => lowering}/functions.cpp | 0 src/solvers/{flattening => lowering}/functions.h | 6 +++--- src/solvers/lowering/module_dependencies.txt | 1 + 5 files changed, 7 insertions(+), 5 deletions(-) rename src/solvers/{flattening => lowering}/functions.cpp (100%) rename src/solvers/{flattening => lowering}/functions.h (88%) diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 81a435735cb..b183a6d99f2 100644 --- a/src/solvers/Makefile +++ b/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 \ diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 67995bc80c7..b2c87f2b881 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -19,11 +19,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "bv_utils.h" #include "boolbv_width.h" #include "boolbv_map.h" #include "arrays.h" -#include "functions.h" class extractbit_exprt; class extractbits_exprt; diff --git a/src/solvers/flattening/functions.cpp b/src/solvers/lowering/functions.cpp similarity index 100% rename from src/solvers/flattening/functions.cpp rename to src/solvers/lowering/functions.cpp diff --git a/src/solvers/flattening/functions.h b/src/solvers/lowering/functions.h similarity index 88% rename from src/solvers/flattening/functions.h rename to src/solvers/lowering/functions.h index 54f1dab54ea..70c9ccdf7f5 100644 --- a/src/solvers/flattening/functions.h +++ b/src/solvers/lowering/functions.h @@ -9,8 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com /// \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 #include @@ -57,4 +57,4 @@ class functionst const exprt::operandst &o2); }; -#endif // CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H +#endif // CPROVER_SOLVERS_LOWERING_FUNCTIONS_H diff --git a/src/solvers/lowering/module_dependencies.txt b/src/solvers/lowering/module_dependencies.txt index c770b3922e1..7e2ec6e2404 100644 --- a/src/solvers/lowering/module_dependencies.txt +++ b/src/solvers/lowering/module_dependencies.txt @@ -1,2 +1,3 @@ +solvers solvers/lowering util From e50fe09349c69cee0901cef8009e7448c1dfbc8b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 10 Apr 2019 13:32:22 -0700 Subject: [PATCH 2/3] clang format the moved files --- src/solvers/lowering/functions.cpp | 40 ++++++++++++++---------------- src/solvers/lowering/functions.h | 11 ++++---- 2 files changed, 24 insertions(+), 27 deletions(-) diff --git a/src/solvers/lowering/functions.cpp b/src/solvers/lowering/functions.cpp index 2588275b14f..48f1bfc0e6b 100644 --- a/src/solvers/lowering/functions.cpp +++ b/src/solvers/lowering/functions.cpp @@ -8,36 +8,35 @@ Author: Daniel Kroening, kroening@kroening.com #include "functions.h" -#include #include +#include -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::const_iterator - it1=info.applications.begin(); - it1!=info.applications.end(); + for(std::set::const_iterator it1 = + info.applications.begin(); + it1 != info.applications.end(); it1++) { - for(std::set::const_iterator - it2=info.applications.begin(); - it2!=it1; + for(std::set::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); } diff --git a/src/solvers/lowering/functions.h b/src/solvers/lowering/functions.h index 70c9ccdf7f5..89fb760ea94 100644 --- a/src/solvers/lowering/functions.h +++ b/src/solvers/lowering/functions.h @@ -22,15 +22,15 @@ Author: Daniel Kroening, kroening@kroening.com 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_LOWERING_FUNCTIONS_H From f3b2587497d3fe93c1a75b61434c4cbc0ea49e67 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 10 Apr 2019 13:54:50 -0700 Subject: [PATCH 3/3] introduce a ranged for --- src/solvers/lowering/functions.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/solvers/lowering/functions.cpp b/src/solvers/lowering/functions.cpp index 48f1bfc0e6b..8b2f160cf16 100644 --- a/src/solvers/lowering/functions.cpp +++ b/src/solvers/lowering/functions.cpp @@ -19,10 +19,8 @@ void functionst::record(const function_application_exprt &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(