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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
/********************* */
/*! \file dagification_visitor.cpp
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Paul Meng, Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Implementation of a dagifier for CVC4 expressions
**
** Implementation of a dagifier for CVC4 expressions.
**/
#include "printer/dagification_visitor.h"
#include "context/context.h"
#include "theory/substitutions.h"
#include <sstream>
namespace CVC4 {
namespace printer {
DagificationVisitor::DagificationVisitor(unsigned threshold, std::string letVarPrefix) :
d_threshold(threshold),
d_letVarPrefix(letVarPrefix),
d_nodeCount(),
d_top(),
d_context(new context::Context()),
d_substitutions(new theory::SubstitutionMap(d_context)),
d_letVar(0),
d_done(false),
d_uniqueParent(),
d_substNodes() {
// 0 doesn't make sense
AlwaysAssertArgument(threshold > 0, threshold);
}
DagificationVisitor::~DagificationVisitor() {
delete d_substitutions;
delete d_context;
}
bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) {
// don't visit variables, constants, or those exprs that we've
// already seen more than the threshold: if we've increased
// the count beyond the threshold already, we've done the same
// for all subexpressions, so it isn't useful to traverse and
// increment again (they'll be dagified anyway).
return current.isVar() ||
current.getMetaKind() == kind::metakind::CONSTANT ||
current.getNumChildren()==0 ||
( ( current.getKind() == kind::NOT ||
current.getKind() == kind::UMINUS ) &&
( current[0].isVar() ||
current[0].getMetaKind() == kind::metakind::CONSTANT ) ) ||
current.getKind() == kind::SORT_TYPE ||
d_nodeCount[current] > d_threshold;
}
void DagificationVisitor::visit(TNode current, TNode parent) {
#ifdef CVC4_TRACING
# ifdef CVC4_DEBUG
// turn off dagification for Debug stream while we're doing this work
Node::dag::Scope scopeDebug(Debug.getStream(), false);
# endif /* CVC4_DEBUG */
// turn off dagification for Trace stream while we're doing this work
Node::dag::Scope scopeTrace(Trace.getStream(), false);
#endif /* CVC4_TRACING */
if(d_uniqueParent.find(current) != d_uniqueParent.end()) {
// we've seen this expr before
TNode& uniqueParent = d_uniqueParent[current];
if(!uniqueParent.isNull() && uniqueParent != parent) {
// there is not a unique parent for this expr, mark it
uniqueParent = TNode::null();
}
// increase the count
const unsigned count = ++d_nodeCount[current];
if(count > d_threshold) {
// candidate for a let binder
d_substNodes.push_back(current);
}
} else {
// we haven't seen this expr before
Assert(d_nodeCount[current] == 0);
d_nodeCount[current] = 1;
d_uniqueParent[current] = parent;
}
}
void DagificationVisitor::start(TNode node) {
AlwaysAssert(!d_done, "DagificationVisitor cannot be re-used");
d_top = node;
}
void DagificationVisitor::done(TNode node) {
AlwaysAssert(!d_done);
d_done = true;
#ifdef CVC4_TRACING
# ifdef CVC4_DEBUG
// turn off dagification for Debug stream while we're doing this work
Node::dag::Scope scopeDebug(Debug.getStream(), false);
# endif /* CVC4_DEBUG */
// turn off dagification for Trace stream while we're doing this work
Node::dag::Scope scopeTrace(Trace.getStream(), false);
#endif /* CVC4_TRACING */
// letify subexprs before parents (cascading LETs)
std::sort(d_substNodes.begin(), d_substNodes.end());
for(std::vector<TNode>::iterator i = d_substNodes.begin();
i != d_substNodes.end();
++i) {
Assert(d_nodeCount[*i] > d_threshold);
TNode parent = d_uniqueParent[*i];
if(!parent.isNull() && d_nodeCount[parent] > d_threshold) {
// no need to letify this expr, because it only occurs in
// a single super-expression, and that one will be letified
continue;
}
// construct the let binder
std::stringstream ss;
ss << d_letVarPrefix << d_letVar++;
Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY | NodeManager::SKOLEM_EXACT_NAME);
// apply previous substitutions to the rhs, enabling cascading LETs
Node n = d_substitutions->apply(*i);
Assert(! d_substitutions->hasSubstitution(n));
d_substitutions->addSubstitution(n, letvar);
}
}
const theory::SubstitutionMap& DagificationVisitor::getLets() {
AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
return *d_substitutions;
}
Node DagificationVisitor::getDagifiedBody() {
AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
#ifdef CVC4_TRACING
# ifdef CVC4_DEBUG
// turn off dagification for Debug stream while we're doing this work
Node::dag::Scope scopeDebug(Debug.getStream(), false);
# endif /* CVC4_DEBUG */
// turn off dagification for Trace stream while we're doing this work
Node::dag::Scope scopeTrace(Trace.getStream(), false);
#endif /* CVC4_TRACING */
return d_substitutions->apply(d_top);
}
}/* CVC4::printer namespace */
}/* CVC4 namespace */
|
