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