cprover
format_number_range.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Format vector of numbers into a compressed range
4 
5 Author: 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 
25 std::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 
77  const std::string &number_range,
78  std::vector<unsigned> &numbers,
79  optionalt<unsigned> &begin_range,
80  optionalt<unsigned> &number)
81 {
82  if(!number.has_value() && begin_range.has_value())
83  {
85  "unterminated number range '" + std::to_string(*begin_range) + "-'");
86  }
87 
88  if(!number.has_value())
89  {
91  "invalid number range '" + number_range + "'");
92  }
93 
94  if(number.has_value() && begin_range.has_value())
95  {
96  if(*begin_range > *number)
97  {
99  "lower bound must not be larger than upper bound '" +
100  std::to_string(*begin_range) + "-" + std::to_string(*number) + "'");
101  }
102  for(unsigned i = *begin_range; i < *number; ++i)
103  numbers.push_back(i);
104  // add upper bound separately to avoid
105  // potential overflow issues in the loop above
106  numbers.push_back(*number);
107  begin_range = {};
108  number = {};
109  }
110  else if(number.has_value() && !begin_range.has_value())
111  {
112  numbers.push_back(*number);
113  number = {};
114  }
115 }
116 
117 std::vector<unsigned> parse_number_range(const std::string &number_range)
118 {
119  std::vector<unsigned> numbers;
120 
121  optionalt<unsigned> begin_range;
122  optionalt<unsigned> number;
123  for(char c : number_range)
124  {
125  if('0' <= c && c <= '9')
126  {
127  if(!number.has_value())
128  number = 0;
129  *number = 10 * *number + (c - '0');
130  }
131  else if(c == ',')
132  {
133  append_numbers_and_reset(number_range, numbers, begin_range, number);
134  }
135  else if(c == '-')
136  {
137  if(!number.has_value())
138  {
140  "lower bound missing in number range '" + number_range + "'");
141  }
142  begin_range = number;
143  number = {};
144  }
145  else
146  {
148  std::string("character '") + c + "' not allowed in number range");
149  }
150  }
151  append_numbers_and_reset(number_range, numbers, begin_range, number);
152 
153  return numbers;
154 }
exception_utils.h
optional.h
parse_number_range
std::vector< unsigned > parse_number_range(const std::string &number_range)
Parse a compressed range into a vector of numbers, e.g.
Definition: format_number_range.cpp:117
deserialization_exceptiont
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Definition: exception_utils.h:73
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
format_number_range
std::string format_number_range(const std::vector< unsigned > &input_numbers)
create shorter representation for output
Definition: format_number_range.cpp:25
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
POSTCONDITION
#define POSTCONDITION(CONDITION)
Definition: invariant.h:480
invariant.h
format_number_range.h
Format vector of numbers into a compressed range.
append_numbers_and_reset
static void append_numbers_and_reset(const std::string &number_range, std::vector< unsigned > &numbers, optionalt< unsigned > &begin_range, optionalt< unsigned > &number)
Appends number resp. numbers begin_range ... number to numbers.
Definition: format_number_range.cpp:76