blob: 3820924743fd8f565adace6461c93c537af475e6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
|
/********************* */
/*! \file dump.h
** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Dump utility classes and functions
**
** Dump utility classes and functions.
**/
#include "cvc4_public.h"
#ifndef __CVC4__DUMP_H
#define __CVC4__DUMP_H
#include "util/output.h"
#include "expr/command.h"
namespace CVC4 {
class CVC4_PUBLIC CVC4dumpstream {
#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
std::ostream* d_os;
#endif /* CVC4_DUMPING && !CVC4_MUZZLE */
#ifdef CVC4_PORTFOLIO
CommandSequence* d_commands;
#endif /* CVC4_PORTFOLIO */
public:
CVC4dumpstream() throw()
#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO)
: d_os(NULL), d_commands(NULL)
#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
: d_os(NULL)
#elif defined(CVC4_PORTFOLIO)
: d_commands(NULL)
#endif /* CVC4_PORTFOLIO */
{ }
CVC4dumpstream(std::ostream& os, CommandSequence& commands) throw()
#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO)
: d_os(&os), d_commands(&commands)
#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
: d_os(&os)
#elif defined(CVC4_PORTFOLIO)
: d_commands(&commands)
#endif /* CVC4_PORTFOLIO */
{ }
CVC4dumpstream& operator<<(const Command& c) {
#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
if(d_os != NULL) {
(*d_os) << c << std::endl;
}
#endif
#if defined(CVC4_PORTFOLIO)
if(d_commands != NULL) {
d_commands->addCommand(c.clone());
}
#endif
return *this;
}
};/* class CVC4dumpstream */
/** The dump class */
class CVC4_PUBLIC DumpC {
std::set<std::string> d_tags;
CommandSequence d_commands;
public:
CVC4dumpstream operator()(const char* tag) {
if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
return CVC4dumpstream(getStream(), d_commands);
} else {
return CVC4dumpstream();
}
}
CVC4dumpstream operator()(std::string tag) {
if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
return CVC4dumpstream(getStream(), d_commands);
} else {
return CVC4dumpstream();
}
}
void clear() { d_commands.clear(); }
const CommandSequence& getCommands() const { return d_commands; }
void declareVar(Expr e, std::string comment) {
if(isOn("declarations")) {
std::stringstream ss;
ss << Expr::setlanguage(Expr::setlanguage::getLanguage(getStream())) << e;
std::string s = ss.str();
CVC4dumpstream(getStream(), d_commands)
<< CommentCommand(s + " is " + comment)
<< DeclareFunctionCommand(s, e, e.getType());
}
}
bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
bool on (std::string tag) { d_tags.insert(tag); return true; }
bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
bool off(std::string tag) { d_tags.erase (tag); return false; }
bool off() { d_tags.clear(); return false; }
bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
std::ostream& setStream(std::ostream& os) { DumpOut.setStream(os); return os; }
std::ostream& getStream() { return DumpOut.getStream(); }
};/* class DumpC */
/** The dump singleton */
extern DumpC DumpChannel CVC4_PUBLIC;
#define Dump ::CVC4::DumpChannel
}/* CVC4 namespace */
#endif /* __CVC4__DUMP_H */
|
