From 96fb4cafb9aa43d0f7b380bd1c5a95af73757bd9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 22 Jun 2018 13:35:42 +0100 Subject: [PATCH 1/2] Rewrite format_number_range The previous code contained an unreachable instruction "next=true;" As I could not figure out where it belongs I ended up rewriting it, now using a lot less nesting and putting all the state into the iterator and a single start_number variable instead of several Booleans. --- src/util/format_number_range.cpp | 131 ++++++++++--------------------- src/util/format_number_range.h | 2 +- 2 files changed, 44 insertions(+), 89 deletions(-) diff --git a/src/util/format_number_range.cpp b/src/util/format_number_range.cpp index 2a88d94f2ff..2c4c54d1da3 100644 --- a/src/util/format_number_range.cpp +++ b/src/util/format_number_range.cpp @@ -10,107 +10,62 @@ Author: Daniel Kroening, kroening@kroening.com /// Format vector of numbers into a compressed range #include -#include +#include #include +#include "invariant.h" + #include "format_number_range.h" /// create shorter representation for output -/// \param parameters: vector of numbers +/// \param input_numbers: vector of numbers /// \return string of compressed number range representation -std::string format_number_range(std::vector &numbers) +std::string format_number_range(const std::vector &input_numbers) { - std::string number_range; + PRECONDITION(!input_numbers.empty()); + + std::vector numbers(input_numbers); std::sort(numbers.begin(), numbers.end()); unsigned end_number=numbers.back(); if(numbers.front()==end_number) - number_range=std::to_string(end_number); // only single number - else + return std::to_string(end_number); // only single number + + std::stringstream number_range; + + auto start_number = numbers.front(); + + for(std::vector::const_iterator it = numbers.begin(); + it != numbers.end(); + ++it) { - bool next=true; - bool first=true; - bool range=false; - unsigned start_number=numbers.front(); - unsigned last_number=start_number; + const auto number = *it; + const auto next = std::next(it); + + // advance one forward + if(next != numbers.end() && *next <= number + 1) + continue; + + // end this block range + if(start_number != numbers.front()) + number_range << ','; - for(const auto &number : numbers) + if(number == start_number) { - if(next) - { - next=false; - start_number=number; - last_number=number; - } - // advance one forward - else - { - if(number==last_number+1 && !(number==end_number)) - { - last_number++; - if(last_number>start_number+1) - range=true; - } - // end this block range - else - { - if(first) - first=false; - else - number_range+=","; - if(last_number>start_number) - { - if(range) - { - if(number==end_number && number==last_number+1) - number_range+= - std::to_string(start_number)+"-"+std::to_string(end_number); - else if(number==end_number) - number_range+= - std::to_string(start_number)+"-"+std::to_string(last_number)+ - ","+std::to_string(end_number); - else - number_range+= - std::to_string(start_number)+"-"+std::to_string(last_number); - } - else - { - if(number!=end_number) - number_range+= - std::to_string(start_number)+","+std::to_string(last_number); - else - { - if(start_number+1==last_number && last_number+1==number) - number_range+= - std::to_string(start_number)+"-"+std::to_string(end_number); - else - number_range+= - std::to_string(start_number)+ - ","+std::to_string(last_number)+ - ","+std::to_string(end_number); - } - } - start_number=number; - last_number=number; - range=false; - continue; - } - else - { - if(number!=end_number) - number_range+=std::to_string(start_number); - else - number_range+=std::to_string(start_number)+","+ - std::to_string(end_number); - start_number=number; - last_number=number; - range=false; - continue; // already set next start number - } - next=true; - } - } + number_range << number; } + else if(number == start_number + 1) + { + number_range << start_number << ',' << number; + } + else + { + number_range << start_number << '-' << number; + } + + if(next != numbers.end()) + start_number = *next; } - assert(!number_range.empty()); - return number_range; + + CHECK_RETURN(!number_range.str().empty()); + return number_range.str(); } diff --git a/src/util/format_number_range.h b/src/util/format_number_range.h index 98c54d9a533..4188afee8ea 100644 --- a/src/util/format_number_range.h +++ b/src/util/format_number_range.h @@ -15,6 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -std::string format_number_range(std::vector &); +std::string format_number_range(const std::vector &); #endif // CPROVER_UTIL_FORMAT_NUMBER_RANGE_H From 70d1a85804ad3016838887e1bf66f4934505b63b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 24 Sep 2018 13:18:25 +0000 Subject: [PATCH 2/2] Unit test for format_number_range format_number_range was not being tested in isolation before. --- unit/Makefile | 1 + unit/util/format_number_range.cpp | 37 +++++++++++++++++++++++++++++++ 2 files changed, 38 insertions(+) create mode 100644 unit/util/format_number_range.cpp diff --git a/unit/Makefile b/unit/Makefile index bc9800d85a9..bcd06e218c8 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -32,6 +32,7 @@ SRC += analyses/ai/ai.cpp \ util/expr_cast/expr_cast.cpp \ util/expr.cpp \ util/file_util.cpp \ + util/format_number_range.cpp \ util/get_base_name.cpp \ util/graph.cpp \ util/irep.cpp \ diff --git a/unit/util/format_number_range.cpp b/unit/util/format_number_range.cpp new file mode 100644 index 00000000000..487d64a06a0 --- /dev/null +++ b/unit/util/format_number_range.cpp @@ -0,0 +1,37 @@ +/*******************************************************************\ + + Module: format_number_range unit tests + + Author: Michael Tautschnig + +\*******************************************************************/ + +#include + +#include + +TEST_CASE( + "Format a range of unsigned numbers", + "[core][util][format_number_range]") +{ + const std::vector singleton = {1u}; + REQUIRE(format_number_range(singleton) == "1"); + + const std::vector r1 = {0u, 42u}; + REQUIRE(format_number_range(r1) == "0,42"); + + const std::vector r2 = {0u, 1u}; + REQUIRE(format_number_range(r2) == "0,1"); + + const std::vector r3 = {1u, 2u, 3u}; + REQUIRE(format_number_range(r3) == "1-3"); + + const std::vector r4 = {1u, 3u, 4u, 5u}; + REQUIRE(format_number_range(r4) == "1,3-5"); + + const std::vector r5 = {1u, 10u, 11u, 12u, 42u}; + REQUIRE(format_number_range(r5) == "1,10-12,42"); + + const std::vector r6 = {1u, 10u, 11u, 12u, 42u, 43u, 44u}; + REQUIRE(format_number_range(r6) == "1,10-12,42-44"); +}