CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
19#include "format_number_range.h"
20
24std::string format_number_range(const std::vector<mp_integer> &input_numbers)
25{
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
74static void append_numbers(
75 const std::string &number_range,
76 std::vector<mp_integer> &numbers,
78 bool is_range)
79{
81 {
83 "unterminated number range '" + integer2string(*(++numbers.rbegin())) +
84 "-'");
85 }
86
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();
100 {
102 "lower bound must not be larger than upper bound '" +
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
113std::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 {
130
131 numbers.push_back(0);
132 last_number_is_set = false;
133 is_range = false;
134 }
135 else if(c == '-')
136 {
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 }
153
154 return numbers;
155}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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