CBMC
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 
19 #include "format_number_range.h"
20 
24 std::string format_number_range(const std::vector<mp_integer> &input_numbers)
25 {
26  PRECONDITION(!input_numbers.empty());
27 
28  std::vector<mp_integer> numbers(input_numbers);
29  std::sort(numbers.begin(), numbers.end());
30  if(numbers.front() == numbers.back())
31  return integer2string(numbers.back()); // only single number
32 
33  std::stringstream number_range;
34 
35  auto start_number = numbers.front();
36 
37  for(std::vector<mp_integer>::const_iterator it = numbers.begin();
38  it != numbers.end();
39  ++it)
40  {
41  const auto number = *it;
42  const auto next = std::next(it);
43 
44  // advance one forward
45  if(next != numbers.end() && *next <= number + 1)
46  continue;
47 
48  // end this block range
49  if(start_number != numbers.front())
50  number_range << ',';
51 
52  if(number == start_number)
53  {
54  number_range << number;
55  }
56  else if(number == start_number + 1)
57  {
58  number_range << start_number << ',' << number;
59  }
60  else
61  {
62  number_range << start_number << '-' << number;
63  }
64 
65  if(next != numbers.end())
66  start_number = *next;
67  }
68 
69  POSTCONDITION(!number_range.str().empty());
70  return number_range.str();
71 }
72 
74 static void append_numbers(
75  const std::string &number_range,
76  std::vector<mp_integer> &numbers,
77  bool last_number_is_set,
78  bool is_range)
79 {
80  if(!last_number_is_set && is_range)
81  {
83  "unterminated number range '" + integer2string(*(++numbers.rbegin())) +
84  "-'");
85  }
86 
87  if(!last_number_is_set)
88  {
90  "invalid number range '" + number_range + "'");
91  }
92 
93  if(is_range)
94  {
95  mp_integer end_range = numbers.back();
96  numbers.pop_back();
97  mp_integer begin_range = numbers.back();
98  numbers.pop_back();
99  if(begin_range > end_range)
100  {
102  "lower bound must not be larger than upper bound '" +
103  integer2string(begin_range) + "-" + integer2string(end_range) + "'");
104  }
105  for(mp_integer i = begin_range; i < end_range; ++i)
106  numbers.push_back(i);
107  // add upper bound separately to avoid
108  // potential overflow issues in the loop above
109  numbers.push_back(end_range);
110  }
111 }
112 
113 std::vector<mp_integer> parse_number_range(const std::string &number_range)
114 {
115  std::vector<mp_integer> numbers(1, 0);
116  bool last_number_is_set = false;
117  bool is_range = false;
118 
119  for(char c : number_range)
120  {
121  if('0' <= c && c <= '9')
122  {
123  numbers.back() *= 10;
124  numbers.back() += c - '0';
125  last_number_is_set = true;
126  }
127  else if(c == ',')
128  {
129  append_numbers(number_range, numbers, last_number_is_set, is_range);
130 
131  numbers.push_back(0);
132  last_number_is_set = false;
133  is_range = false;
134  }
135  else if(c == '-')
136  {
137  if(!last_number_is_set)
138  {
140  "lower bound missing in number range '" + number_range + "'");
141  }
142  numbers.push_back(0);
143  last_number_is_set = false;
144  is_range = true;
145  }
146  else
147  {
149  std::string("character '") + c + "' not allowed in number range");
150  }
151  }
152  append_numbers(number_range, numbers, last_number_is_set, is_range);
153 
154  return numbers;
155 }
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< mp_integer > &input_numbers)
create shorter representation for output
std::vector< mp_integer > 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< mp_integer > &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.
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
BigInt mp_integer
Definition: smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define POSTCONDITION(CONDITION)
Definition: invariant.h:479