1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Morgan Deters, Andres Noetzli, Abdalrhman Mohamed |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Dump utility classes and functions. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__DUMP_H |
19 |
|
#define CVC5__DUMP_H |
20 |
|
|
21 |
|
#include "base/output.h" |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
|
25 |
|
class Command; |
26 |
|
class NodeCommand; |
27 |
|
|
28 |
|
#if defined(CVC5_DUMPING) && !defined(CVC5_MUZZLE) |
29 |
|
|
30 |
|
class CVC5dumpstream |
31 |
|
{ |
32 |
|
public: |
33 |
737 |
CVC5dumpstream() : d_os(nullptr) {} |
34 |
10 |
CVC5dumpstream(std::ostream& os) : d_os(&os) {} |
35 |
|
|
36 |
|
CVC5dumpstream& operator<<(const Command& c); |
37 |
|
|
38 |
|
/** A convenience function for dumping internal commands. |
39 |
|
* |
40 |
|
* Since Commands are now part of the public API, internal code should use |
41 |
|
* NodeCommands and this function (instead of the one above) to dump them. |
42 |
|
*/ |
43 |
|
CVC5dumpstream& operator<<(const NodeCommand& nc); |
44 |
|
|
45 |
|
private: |
46 |
|
std::ostream* d_os; |
47 |
|
}; /* class CVC5dumpstream */ |
48 |
|
|
49 |
|
#else |
50 |
|
|
51 |
|
/** |
52 |
|
* Dummy implementation of the dump stream when dumping is disabled or the |
53 |
|
* build is muzzled. |
54 |
|
*/ |
55 |
|
class CVC5dumpstream |
56 |
|
{ |
57 |
|
public: |
58 |
|
CVC5dumpstream() {} |
59 |
|
CVC5dumpstream(std::ostream& os) {} |
60 |
|
CVC5dumpstream& operator<<(const Command& c); |
61 |
|
CVC5dumpstream& operator<<(const NodeCommand& nc); |
62 |
|
}; /* class CVC5dumpstream */ |
63 |
|
|
64 |
|
#endif /* CVC5_DUMPING && !CVC5_MUZZLE */ |
65 |
|
|
66 |
|
/** The dump class */ |
67 |
18794 |
class DumpC |
68 |
|
{ |
69 |
|
public: |
70 |
747 |
CVC5dumpstream operator()(const char* tag) |
71 |
|
{ |
72 |
747 |
if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { |
73 |
10 |
return CVC5dumpstream(getStream()); |
74 |
|
} else { |
75 |
737 |
return CVC5dumpstream(); |
76 |
|
} |
77 |
|
} |
78 |
|
|
79 |
|
CVC5dumpstream operator()(std::string tag) |
80 |
|
{ |
81 |
|
if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { |
82 |
|
return CVC5dumpstream(getStream()); |
83 |
|
} else { |
84 |
|
return CVC5dumpstream(); |
85 |
|
} |
86 |
|
} |
87 |
|
|
88 |
8 |
bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; } |
89 |
|
bool on (std::string tag) { d_tags.insert(tag); return true; } |
90 |
|
bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } |
91 |
|
bool off(std::string tag) { d_tags.erase (tag); return false; } |
92 |
|
bool off() { d_tags.clear(); return false; } |
93 |
|
|
94 |
17503391 |
bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } |
95 |
27 |
bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } |
96 |
|
|
97 |
|
std::ostream& setStream(std::ostream* os); |
98 |
|
std::ostream& getStream(); |
99 |
|
std::ostream* getStreamPointer(); |
100 |
|
|
101 |
|
void setDumpFromString(const std::string& optarg); |
102 |
|
|
103 |
|
private: |
104 |
|
/** Set of dumping tags that are currently active. */ |
105 |
|
std::set<std::string> d_tags; |
106 |
|
|
107 |
|
/** The message printed on `--dump help`. */ |
108 |
|
static const std::string s_dumpHelp; |
109 |
|
};/* class DumpC */ |
110 |
|
|
111 |
|
/** The dump singleton */ |
112 |
|
extern DumpC DumpChannel; |
113 |
|
|
114 |
|
#define Dump ::cvc5::DumpChannel |
115 |
|
|
116 |
|
} // namespace cvc5 |
117 |
|
|
118 |
|
#endif /* CVC5__DUMP_H */ |