1 /********************* */
2 /*! \file dagification_visitor.cpp
4 ** Original author: mdeters
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011, 2012 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Implementation of a dagifier for CVC4 expressions
16 ** Implementation of a dagifier for CVC4 expressions.
19 #include "printer/dagification_visitor.h"
21 #include "context/context.h"
22 #include "theory/substitutions.h"
29 DagificationVisitor::DagificationVisitor(unsigned threshold
, std::string letVarPrefix
) :
30 d_threshold(threshold
),
31 d_letVarPrefix(letVarPrefix
),
34 d_context(new context::Context()),
35 d_substitutions(new theory::SubstitutionMap(d_context
)),
41 // 0 doesn't make sense
42 CheckArgument(threshold
> 0, threshold
);
45 DagificationVisitor::~DagificationVisitor() {
46 delete d_substitutions
;
50 bool DagificationVisitor::alreadyVisited(TNode current
, TNode parent
) {
51 // don't visit variables, constants, or those exprs that we've
52 // already seen more than the threshold: if we've increased
53 // the count beyond the threshold already, we've done the same
54 // for all subexpressions, so it isn't useful to traverse and
55 // increment again (they'll be dagified anyway).
56 return current
.getMetaKind() == kind::metakind::VARIABLE
||
57 current
.getMetaKind() == kind::metakind::CONSTANT
||
58 ( ( current
.getKind() == kind::NOT
||
59 current
.getKind() == kind::UMINUS
) &&
60 ( current
[0].getMetaKind() == kind::metakind::VARIABLE
||
61 current
[0].getMetaKind() == kind::metakind::CONSTANT
) ) ||
62 current
.getKind() == kind::SORT_TYPE
||
63 d_nodeCount
[current
] > d_threshold
;
66 void DagificationVisitor::visit(TNode current
, TNode parent
) {
70 // turn off dagification for Debug stream while we're doing this work
71 Node::dag::Scope
scopeDebug(Debug
.getStream(), false);
72 # endif /* CVC4_DEBUG */
73 // turn off dagification for Trace stream while we're doing this work
74 Node::dag::Scope
scopeTrace(Trace
.getStream(), false);
75 #endif /* CVC4_TRACING */
77 if(d_uniqueParent
.find(current
) != d_uniqueParent
.end()) {
78 // we've seen this expr before
80 TNode
& uniqueParent
= d_uniqueParent
[current
];
82 if(!uniqueParent
.isNull() && uniqueParent
!= parent
) {
83 // there is not a unique parent for this expr, mark it
84 uniqueParent
= TNode::null();
88 const unsigned count
= ++d_nodeCount
[current
];
90 if(count
> d_threshold
) {
91 // candidate for a let binder
92 d_substNodes
.push_back(current
);
95 // we haven't seen this expr before
96 Assert(d_nodeCount
[current
] == 0);
97 d_nodeCount
[current
] = 1;
98 d_uniqueParent
[current
] = parent
;
102 void DagificationVisitor::start(TNode node
) {
103 AlwaysAssert(!d_done
, "DagificationVisitor cannot be re-used");
107 void DagificationVisitor::done(TNode node
) {
108 AlwaysAssert(!d_done
);
114 // turn off dagification for Debug stream while we're doing this work
115 Node::dag::Scope
scopeDebug(Debug
.getStream(), false);
116 # endif /* CVC4_DEBUG */
117 // turn off dagification for Trace stream while we're doing this work
118 Node::dag::Scope
scopeTrace(Trace
.getStream(), false);
119 #endif /* CVC4_TRACING */
121 // letify subexprs before parents (cascading LETs)
122 std::sort(d_substNodes
.begin(), d_substNodes
.end());
124 for(std::vector
<TNode
>::iterator i
= d_substNodes
.begin();
125 i
!= d_substNodes
.end();
127 Assert(d_nodeCount
[*i
] > d_threshold
);
128 TNode parent
= d_uniqueParent
[*i
];
129 if(!parent
.isNull() && d_nodeCount
[parent
] > d_threshold
) {
130 // no need to letify this expr, because it only occurs in
131 // a single super-expression, and that one will be letified
135 // construct the let binder
136 std::stringstream ss
;
137 ss
<< d_letVarPrefix
<< d_letVar
++;
138 Node letvar
= NodeManager::currentNM()->mkVar(ss
.str(), (*i
).getType());
140 // apply previous substitutions to the rhs, enabling cascading LETs
141 Node n
= d_substitutions
->apply(*i
);
142 Assert(! d_substitutions
->hasSubstitution(n
));
143 d_substitutions
->addSubstitution(n
, letvar
);
147 const theory::SubstitutionMap
& DagificationVisitor::getLets() {
148 AlwaysAssert(d_done
, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
149 return *d_substitutions
;
152 Node
DagificationVisitor::getDagifiedBody() {
153 AlwaysAssert(d_done
, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
157 // turn off dagification for Debug stream while we're doing this work
158 Node::dag::Scope
scopeDebug(Debug
.getStream(), false);
159 # endif /* CVC4_DEBUG */
160 // turn off dagification for Trace stream while we're doing this work
161 Node::dag::Scope
scopeTrace(Trace
.getStream(), false);
162 #endif /* CVC4_TRACING */
164 return d_substitutions
->apply(d_top
);
167 }/* CVC4::printer namespace */
168 }/* CVC4 namespace */