cprover
format_number_range.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Format vector of numbers into a compressed range
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include <algorithm>
13#include <sstream>
14#include <string>
15
16#include "exception_utils.h"
17#include "invariant.h"
18#include "optional.h"
19
20#include "format_number_range.h"
21
25std::string format_number_range(const std::vector<unsigned> &input_numbers)
26{
27 PRECONDITION(!input_numbers.empty());
28
29 std::vector<unsigned> numbers(input_numbers);
30 std::sort(numbers.begin(), numbers.end());
31 unsigned end_number=numbers.back();
32 if(numbers.front()==end_number)
33 return std::to_string(end_number); // only single number
34
35 std::stringstream number_range;
36
37 auto start_number = numbers.front();
38
39 for(std::vector<unsigned>::const_iterator it = numbers.begin();
40 it != numbers.end();
41 ++it)
42 {
43 const auto number = *it;
44 const auto next = std::next(it);
45
46 // advance one forward
47 if(next != numbers.end() && *next <= number + 1)
48 continue;
49
50 // end this block range
51 if(start_number != numbers.front())
52 number_range << ',';
53
54 if(number == start_number)
55 {
56 number_range << number;
57 }
58 else if(number == start_number + 1)
59 {
60 number_range << start_number << ',' << number;
61 }
62 else
63 {
64 number_range << start_number << '-' << number;
65 }
66
67 if(next != numbers.end())
68 start_number = *next;
69 }
70
71 POSTCONDITION(!number_range.str().empty());
72 return number_range.str();
73}
74
76static void append_numbers(
77 const std::string &number_range,
78 std::vector<unsigned> &numbers,
79 bool last_number_is_set,
80 bool is_range)
81{
82 if(!last_number_is_set && is_range)
83 {
85 "unterminated number range '" + std::to_string(*(++numbers.rbegin())) +
86 "-'");
87 }
88
89 if(!last_number_is_set)
90 {
92 "invalid number range '" + number_range + "'");
93 }
94
95 if(is_range)
96 {
97 unsigned end_range = numbers.back();
98 numbers.pop_back();
99 unsigned begin_range = numbers.back();
100 numbers.pop_back();
101 if(begin_range > end_range)
102 {
104 "lower bound must not be larger than upper bound '" +
105 std::to_string(begin_range) + "-" + std::to_string(end_range) + "'");
106 }
107 for(unsigned i = begin_range; i < end_range; ++i)
108 numbers.push_back(i);
109 // add upper bound separately to avoid
110 // potential overflow issues in the loop above
111 numbers.push_back(end_range);
112 }
113}
114
115std::vector<unsigned> parse_number_range(const std::string &number_range)
116{
117 std::vector<unsigned> numbers(1, 0);
118 bool last_number_is_set = false;
119 bool is_range = false;
120
121 for(char c : number_range)
122 {
123 if('0' <= c && c <= '9')
124 {
125 numbers.back() *= 10;
126 numbers.back() += c - '0';
127 last_number_is_set = true;
128 }
129 else if(c == ',')
130 {
131 append_numbers(number_range, numbers, last_number_is_set, is_range);
132
133 numbers.push_back(0);
134 last_number_is_set = false;
135 is_range = false;
136 }
137 else if(c == '-')
138 {
139 if(!last_number_is_set)
140 {
142 "lower bound missing in number range '" + number_range + "'");
143 }
144 numbers.push_back(0);
145 last_number_is_set = false;
146 is_range = true;
147 }
148 else
149 {
151 std::string("character '") + c + "' not allowed in number range");
152 }
153 }
154 append_numbers(number_range, numbers, last_number_is_set, is_range);
155
156 return numbers;
157}
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
std::string format_number_range(const std::vector< unsigned > &input_numbers)
create shorter representation for output
std::vector< unsigned > parse_number_range(const std::string &number_range)
Parse a compressed range into a vector of numbers, e.g.
static void append_numbers(const std::string &number_range, std::vector< unsigned > &numbers, bool last_number_is_set, bool is_range)
Appends number resp. numbers begin_range ... number to numbers.
Format vector of numbers into a compressed range.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define POSTCONDITION(CONDITION)
Definition: invariant.h:479
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.