1 /*
2 * TdZdd: a Top-down/Breadth-first Decision Diagram Manipulation Framework
3 * by Hiroaki Iwashita <iwashita@erato.ist.hokudai.ac.jp>
4 * Copyright (c) 2014 ERATO MINATO Project
5 *
6 * Permission is hereby granted, free of charge, to any person obtaining a
7 * copy of this software and associated documentation files (the "Software"),
8 * to deal in the Software without restriction, including without limitation
9 * the rights to use, copy, modify, merge, publish, distribute, sublicense,
10 * and/or sell copies of the Software, and to permit persons to whom the
11 * Software is furnished to do so, subject to the following conditions:
12 *
13 * The above copyright notice and this permission notice shall be included in
14 * all copies or substantial portions of the Software.
15 *
16 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
21 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
22 * DEALINGS IN THE SOFTWARE.
23 */
24
25 #pragma once
26
27 #include <cstdio>
28 #include <ctime>
29 #include <iostream>
30 #include <streambuf>
31 #include <string>
32
33 #include "ResourceUsage.hpp"
34
35 namespace tdzdd {
36
capitalize(std::string const & s)37 inline std::string capitalize(std::string const& s) {
38 std::string t = s;
39 if (t.size() >= 1) {
40 t[0] = toupper(s[0]);
41 }
42 return t;
43 }
44
45 template<typename T>
to_string(T const & o)46 inline std::string to_string(T const& o) {
47 std::ostringstream oss;
48 oss << o;
49 return oss.str();
50 }
51
52 template<std::ostream& os>
53 class MessageHandler_: public std::ostream {
54 class Buf: public std::streambuf {
55 MessageHandler_& mh;
56
57 public:
Buf(MessageHandler_ & mh)58 Buf(MessageHandler_& mh)
59 : mh(mh) {
60 }
61
62 protected:
imbue(std::locale const & loc)63 virtual void imbue(std::locale const& loc) {
64 os.imbue(loc);
65 }
66
overflow(int c)67 virtual int overflow(int c) {
68 if (!enabled) return c;
69
70 if (lastUser != this) {
71 if (column != 0) {
72 os.put('\n');
73 ++lineno;
74 column = 0;
75 }
76 lastUser = this;
77 }
78
79 if (c == EOF) return EOF;
80
81 if (column == 0) {
82 if (isspace(c)) return c;
83 for (int i = mh.indent; i > 0; --i) {
84 os.put(' ');
85 ++column;
86 }
87 }
88
89 os.put(c);
90
91 if (c == '\n') {
92 ++lineno;
93 column = 0;
94 }
95 else {
96 ++column;
97 }
98
99 return c;
100 }
101 };
102
103 static int const INDENT_SIZE = 2;
104 static bool enabled;
105 static int indentLevel;
106 static int lineno;
107 static int column;
108 static Buf* lastUser;
109
110 Buf buf;
111 std::string name;
112 int indent;
113 int beginLine;
114 ResourceUsage initialUsage;
115 ResourceUsage prevUsage;
116 int totalSteps;
117 int stepCount;
118 int dotCount;
119 time_t dotTime;
120 bool stepping;
121
122 public:
MessageHandler_()123 MessageHandler_()
124 : std::ostream(&buf), buf(*this), indent(indentLevel * INDENT_SIZE),
125 beginLine(0), totalSteps(0), stepCount(0),
126 dotCount(0), dotTime(0), stepping(false) {
127 flags(os.flags());
128 precision(os.precision());
129 width(os.width());
130 }
131
~MessageHandler_()132 virtual ~MessageHandler_() {
133 if (!name.empty()) end("aborted");
134 }
135
showMessages(bool flag=true)136 static bool showMessages(bool flag = true) {
137 bool prev = enabled;
138 enabled = flag;
139 return prev;
140 }
141
begin(std::string const & s)142 MessageHandler_& begin(std::string const& s) {
143 if (!enabled) return *this;
144 if (!name.empty()) end("aborted");
145 name = s.empty() ? "level-" + indentLevel : s;
146 indent = indentLevel * INDENT_SIZE;
147 *this << "\n" << capitalize(name);
148 indent = ++indentLevel * INDENT_SIZE;
149 beginLine = lineno;
150 initialUsage.update();
151 prevUsage = initialUsage;
152 setSteps(10);
153 return *this;
154 }
155
setSteps(int steps)156 MessageHandler_& setSteps(int steps) {
157 if (!enabled) return *this;
158 totalSteps = steps;
159 stepCount = 0;
160 dotCount = 0;
161 dotTime = std::time(0);
162 stepping = false;
163 return *this;
164 }
165
step(char dot='-')166 MessageHandler_& step(char dot = '-') {
167 if (!enabled) return *this;
168
169 if (!stepping && dotTime + 4 < std::time(0)) {
170 *this << '\n';
171 stepping = true;
172 }
173
174 if (stepping) {
175 if (stepCount % 50 != column - indent) {
176 *this << '\n';
177 for (int i = stepCount % 50; i > 0; --i) {
178 *this << '-';
179 }
180 }
181 *this << dot;
182 ++stepCount;
183 if (column - indent >= 50) {
184 ResourceUsage usage;
185 ResourceUsage diff = usage - prevUsage;
186 *this << std::setw(3) << std::right
187 << (stepCount * 100 / totalSteps);
188 *this << "% (" << diff.elapsedTime() << ", " << diff.memory()
189 << ")\n";
190 prevUsage = usage;
191 }
192 }
193 else {
194 ++stepCount;
195 while (dotCount * totalSteps < stepCount * 10) {
196 if (dotCount == 0) *this << ' ';
197 *this << '.';
198 ++dotCount;
199 dotTime = std::time(0);
200 }
201 }
202
203 return *this;
204 }
205
end(std::string const & msg="",std::string const & info="")206 MessageHandler_& end(std::string const& msg = "", std::string const& info =
207 "") {
208 if (!enabled) return *this;
209 if (name.empty()) return *this;
210
211 ResourceUsage rusage = ResourceUsage() - initialUsage;
212
213 if (beginLine == lineno) {
214 if (!info.empty()) {
215 *this << " " << info;
216 }
217 else if (msg.empty()) {
218 *this << " done";
219 }
220 else {
221 *this << " " << msg;
222 }
223 *this << " in " << rusage << ".\n";
224
225 indent = --indentLevel * INDENT_SIZE;
226 }
227 else {
228 indent = --indentLevel * INDENT_SIZE;
229
230 if (msg.empty()) {
231 *this << "\nDone " << name;
232 }
233 else {
234 *this << "\n" << capitalize(msg);
235 }
236 if (!info.empty()) *this << " " << info;
237 *this << " in " << rusage << ".\n";
238 }
239
240 name = "";
241 return *this;
242 }
243
end(size_t n)244 MessageHandler_& end(size_t n) {
245 if (!enabled) return *this;
246 return end("", "<" + to_string(n) + ">");
247 }
248
col() const249 int col() const {
250 return column;
251 }
252 };
253
254 template<std::ostream& os>
255 bool MessageHandler_<os>::enabled = false;
256
257 template<std::ostream& os>
258 int MessageHandler_<os>::indentLevel = 0;
259
260 template<std::ostream& os>
261 int MessageHandler_<os>::lineno = 1;
262
263 template<std::ostream& os>
264 int MessageHandler_<os>::column = 0;
265
266 template<std::ostream& os>
267 typename MessageHandler_<os>::Buf* MessageHandler_<os>::lastUser = 0;
268
269 typedef MessageHandler_<std::cerr> MessageHandler;
270
271 } // namespace tdzdd
272