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 "theory/substitutions.h"
27 DagificationVisitor::DagificationVisitor(unsigned threshold
, std::string letVarPrefix
) :
28 d_threshold(threshold
),
29 d_letVarPrefix(letVarPrefix
),
32 d_context(new context::Context()),
33 d_substitutions(new theory::SubstitutionMap(d_context
)),
39 // 0 doesn't make sense
40 AlwaysAssertArgument(threshold
> 0, threshold
);
43 DagificationVisitor::~DagificationVisitor() {
44 delete d_substitutions
;
48 bool DagificationVisitor::alreadyVisited(TNode current
, TNode parent
) {
49 Kind ck
= current
.getKind();
50 if (ck
== kind::FORALL
|| ck
== kind::EXISTS
|| ck
== kind::LAMBDA
51 || ck
== kind::CHOICE
)
53 // for quantifiers, we visit them but we don't recurse on them
54 visit(current
, parent
);
57 // don't visit variables, constants, or those exprs that we've
58 // already seen more than the threshold: if we've increased
59 // the count beyond the threshold already, we've done the same
60 // for all subexpressions, so it isn't useful to traverse and
61 // increment again (they'll be dagified anyway).
62 return current
.isVar() || current
.getMetaKind() == kind::metakind::CONSTANT
63 || current
.getNumChildren() == 0
64 || ((ck
== kind::NOT
|| ck
== kind::UMINUS
)
65 && (current
[0].isVar()
66 || current
[0].getMetaKind() == kind::metakind::CONSTANT
))
67 || ck
== kind::SORT_TYPE
|| d_nodeCount
[current
] > d_threshold
;
70 void DagificationVisitor::visit(TNode current
, TNode parent
) {
74 // turn off dagification for Debug stream while we're doing this work
75 Node::dag::Scope
scopeDebug(Debug
.getStream(), false);
76 # endif /* CVC4_DEBUG */
77 // turn off dagification for Trace stream while we're doing this work
78 Node::dag::Scope
scopeTrace(Trace
.getStream(), false);
79 #endif /* CVC4_TRACING */
81 if(d_uniqueParent
.find(current
) != d_uniqueParent
.end()) {
82 // we've seen this expr before
84 TNode
& uniqueParent
= d_uniqueParent
[current
];
86 if(!uniqueParent
.isNull() && uniqueParent
!= parent
) {
87 // there is not a unique parent for this expr, mark it
88 uniqueParent
= TNode::null();
92 const unsigned count
= ++d_nodeCount
[current
];
94 if(count
> d_threshold
) {
95 // candidate for a let binder
96 d_substNodes
.push_back(current
);
99 // we haven't seen this expr before
100 Assert(d_nodeCount
[current
] == 0);
101 d_nodeCount
[current
] = 1;
102 d_uniqueParent
[current
] = parent
;
106 void DagificationVisitor::start(TNode node
) {
107 AlwaysAssert(!d_done
, "DagificationVisitor cannot be re-used");
111 void DagificationVisitor::done(TNode node
) {
112 AlwaysAssert(!d_done
);
118 // turn off dagification for Debug stream while we're doing this work
119 Node::dag::Scope
scopeDebug(Debug
.getStream(), false);
120 # endif /* CVC4_DEBUG */
121 // turn off dagification for Trace stream while we're doing this work
122 Node::dag::Scope
scopeTrace(Trace
.getStream(), false);
123 #endif /* CVC4_TRACING */
125 // letify subexprs before parents (cascading LETs)
126 std::sort(d_substNodes
.begin(), d_substNodes
.end());
128 for(std::vector
<TNode
>::iterator i
= d_substNodes
.begin();
129 i
!= d_substNodes
.end();
131 Assert(d_nodeCount
[*i
] > d_threshold
);
132 TNode parent
= d_uniqueParent
[*i
];
133 if(!parent
.isNull() && d_nodeCount
[parent
] > d_threshold
) {
134 // no need to letify this expr, because it only occurs in
135 // a single super-expression, and that one will be letified
139 // construct the let binder
140 std::stringstream ss
;
141 ss
<< d_letVarPrefix
<< d_letVar
++;
142 Node letvar
= NodeManager::currentNM()->mkSkolem(ss
.str(), (*i
).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY
| NodeManager::SKOLEM_EXACT_NAME
);
144 // apply previous substitutions to the rhs, enabling cascading LETs
145 Node n
= d_substitutions
->apply(*i
);
146 Assert(! d_substitutions
->hasSubstitution(n
));
147 d_substitutions
->addSubstitution(n
, letvar
);
151 const theory::SubstitutionMap
& DagificationVisitor::getLets() {
152 AlwaysAssert(d_done
, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
153 return *d_substitutions
;
156 Node
DagificationVisitor::getDagifiedBody() {
157 AlwaysAssert(d_done
, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
161 // turn off dagification for Debug stream while we're doing this work
162 Node::dag::Scope
scopeDebug(Debug
.getStream(), false);
163 # endif /* CVC4_DEBUG */
164 // turn off dagification for Trace stream while we're doing this work
165 Node::dag::Scope
scopeTrace(Trace
.getStream(), false);
166 #endif /* CVC4_TRACING */
168 return d_substitutions
->apply(d_top
);
171 }/* CVC4::printer namespace */
172 }/* CVC4 namespace */