1 /********************* */
2 /*! \file dagification_visitor.cpp
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
12 ** \brief Implementation of a dagifier for CVC4 expressions
14 ** Implementation of a dagifier for CVC4 expressions.
17 #include "printer/dagification_visitor.h"
19 #include "context/context.h"
20 #include "expr/node_algorithm.h"
21 #include "expr/node_manager_attributes.h"
22 #include "theory/substitutions.h"
29 DagificationVisitor::DagificationVisitor(unsigned threshold
,
30 std::string letVarPrefix
)
31 : d_threshold(threshold
),
32 d_letVarPrefix(letVarPrefix
),
36 d_context(new context::Context()),
37 d_substitutions(new theory::SubstitutionMap(d_context
)),
43 // 0 doesn't make sense
44 AlwaysAssertArgument(threshold
> 0, threshold
);
47 DagificationVisitor::~DagificationVisitor() {
48 delete d_substitutions
;
52 bool DagificationVisitor::alreadyVisited(TNode current
, TNode parent
) {
53 Kind ck
= current
.getKind();
54 if (current
.isClosure())
56 // for quantifiers, we visit them but we don't recurse on them
57 visit(current
, parent
);
59 // search for variables that start with the let prefix
60 std::unordered_set
<TNode
, TNodeHashFunction
> vs
;
61 expr::getVariables(current
, vs
);
62 for (const TNode v
: vs
)
64 const std::string name
= v
.getAttribute(expr::VarNameAttr());
65 if (name
.compare(0, d_letVarPrefix
.size(), d_letVarPrefix
) == 0)
67 d_reservedLetNames
.insert(name
);
72 else if (current
.isVar())
74 const std::string name
= current
.getAttribute(expr::VarNameAttr());
75 if (name
.compare(0, d_letVarPrefix
.size(), d_letVarPrefix
) == 0)
77 d_reservedLetNames
.insert(name
);
80 // don't visit variables, constants, or those exprs that we've
81 // already seen more than the threshold: if we've increased
82 // the count beyond the threshold already, we've done the same
83 // for all subexpressions, so it isn't useful to traverse and
84 // increment again (they'll be dagified anyway).
85 return current
.isVar() || current
.getMetaKind() == kind::metakind::CONSTANT
86 || current
.getNumChildren() == 0
87 || ((ck
== kind::NOT
|| ck
== kind::UMINUS
)
88 && (current
[0].isVar()
89 || current
[0].getMetaKind() == kind::metakind::CONSTANT
))
90 || ck
== kind::SORT_TYPE
|| d_nodeCount
[current
] > d_threshold
;
93 void DagificationVisitor::visit(TNode current
, TNode parent
) {
97 // turn off dagification for Debug stream while we're doing this work
98 Node::dag::Scope
scopeDebug(Debug
.getStream(), false);
99 # endif /* CVC4_DEBUG */
100 // turn off dagification for Trace stream while we're doing this work
101 Node::dag::Scope
scopeTrace(Trace
.getStream(), false);
102 #endif /* CVC4_TRACING */
104 if(d_uniqueParent
.find(current
) != d_uniqueParent
.end()) {
105 // we've seen this expr before
107 TNode
& uniqueParent
= d_uniqueParent
[current
];
109 // We restrict this optimization to nodes with arity 1 since otherwise we
110 // may run into issues with tree traverals. Without this restriction
111 // dumping regress3/pp-regfile increases the file size by a factor of 5000.
112 if (!uniqueParent
.isNull()
113 && (uniqueParent
!= parent
|| parent
.getNumChildren() > 1))
115 // there is not a unique parent for this expr, mark it
116 uniqueParent
= TNode::null();
119 // increase the count
120 const unsigned count
= ++d_nodeCount
[current
];
122 if(count
> d_threshold
) {
123 // candidate for a let binder
124 d_substNodes
.push_back(current
);
127 // we haven't seen this expr before
128 Assert(d_nodeCount
[current
] == 0);
129 d_nodeCount
[current
] = 1;
130 d_uniqueParent
[current
] = parent
;
134 void DagificationVisitor::start(TNode node
) {
135 AlwaysAssert(!d_done
) << "DagificationVisitor cannot be re-used";
139 void DagificationVisitor::done(TNode node
) {
140 AlwaysAssert(!d_done
);
146 // turn off dagification for Debug stream while we're doing this work
147 Node::dag::Scope
scopeDebug(Debug
.getStream(), false);
148 # endif /* CVC4_DEBUG */
149 // turn off dagification for Trace stream while we're doing this work
150 Node::dag::Scope
scopeTrace(Trace
.getStream(), false);
151 #endif /* CVC4_TRACING */
153 // letify subexprs before parents (cascading LETs)
154 std::sort(d_substNodes
.begin(), d_substNodes
.end());
156 for(std::vector
<TNode
>::iterator i
= d_substNodes
.begin();
157 i
!= d_substNodes
.end();
159 Assert(d_nodeCount
[*i
] > d_threshold
);
160 TNode parent
= d_uniqueParent
[*i
];
161 if(!parent
.isNull() && d_nodeCount
[parent
] > d_threshold
) {
162 // no need to letify this expr, because it only occurs in
163 // a single super-expression, and that one will be letified
167 // construct the let binder
168 std::stringstream ss
;
172 ss
<< d_letVarPrefix
<< d_letVar
++;
173 } while (d_reservedLetNames
.find(ss
.str()) != d_reservedLetNames
.end());
174 Node letvar
= NodeManager::currentNM()->mkSkolem(ss
.str(), (*i
).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY
| NodeManager::SKOLEM_EXACT_NAME
);
176 // apply previous substitutions to the rhs, enabling cascading LETs
177 Node n
= d_substitutions
->apply(*i
);
178 Assert(!d_substitutions
->hasSubstitution(n
));
179 d_substitutions
->addSubstitution(n
, letvar
);
183 const theory::SubstitutionMap
& DagificationVisitor::getLets() {
185 << "DagificationVisitor must be used as a visitor before "
186 "getting the dagified version out!";
187 return *d_substitutions
;
190 Node
DagificationVisitor::getDagifiedBody() {
192 << "DagificationVisitor must be used as a visitor before "
193 "getting the dagified version out!";
197 // turn off dagification for Debug stream while we're doing this work
198 Node::dag::Scope
scopeDebug(Debug
.getStream(), false);
199 # endif /* CVC4_DEBUG */
200 // turn off dagification for Trace stream while we're doing this work
201 Node::dag::Scope
scopeTrace(Trace
.getStream(), false);
202 #endif /* CVC4_TRACING */
204 return d_substitutions
->apply(d_top
);
207 }/* CVC4::printer namespace */
208 }/* CVC4 namespace */