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