1 /********************* */
2 /*! \file dagification_visitor.cpp
3 ** \verbatim
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
11 **
12 ** \brief Implementation of a dagifier for CVC4 expressions
13 **
14 ** Implementation of a dagifier for CVC4 expressions.
15 **/
16
17 #include "printer/dagification_visitor.h"
18
19 #include "context/context.h"
20 #include "theory/substitutions.h"
21
22 #include <sstream>
23
24 namespace CVC4 {
25 namespace printer {
26
DagificationVisitor(unsigned threshold,std::string letVarPrefix)27 DagificationVisitor::DagificationVisitor(unsigned threshold, std::string letVarPrefix) :
28 d_threshold(threshold),
29 d_letVarPrefix(letVarPrefix),
30 d_nodeCount(),
31 d_top(),
32 d_context(new context::Context()),
33 d_substitutions(new theory::SubstitutionMap(d_context)),
34 d_letVar(0),
35 d_done(false),
36 d_uniqueParent(),
37 d_substNodes() {
38
39 // 0 doesn't make sense
40 AlwaysAssertArgument(threshold > 0, threshold);
41 }
42
~DagificationVisitor()43 DagificationVisitor::~DagificationVisitor() {
44 delete d_substitutions;
45 delete d_context;
46 }
47
alreadyVisited(TNode current,TNode parent)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)
52 {
53 // for quantifiers, we visit them but we don't recurse on them
54 visit(current, parent);
55 return true;
56 }
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;
68 }
69
visit(TNode current,TNode parent)70 void DagificationVisitor::visit(TNode current, TNode parent) {
71
72 #ifdef CVC4_TRACING
73 # ifdef CVC4_DEBUG
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 */
80
81 if(d_uniqueParent.find(current) != d_uniqueParent.end()) {
82 // we've seen this expr before
83
84 TNode& uniqueParent = d_uniqueParent[current];
85
86 if(!uniqueParent.isNull() && uniqueParent != parent) {
87 // there is not a unique parent for this expr, mark it
88 uniqueParent = TNode::null();
89 }
90
91 // increase the count
92 const unsigned count = ++d_nodeCount[current];
93
94 if(count > d_threshold) {
95 // candidate for a let binder
96 d_substNodes.push_back(current);
97 }
98 } else {
99 // we haven't seen this expr before
100 Assert(d_nodeCount[current] == 0);
101 d_nodeCount[current] = 1;
102 d_uniqueParent[current] = parent;
103 }
104 }
105
start(TNode node)106 void DagificationVisitor::start(TNode node) {
107 AlwaysAssert(!d_done, "DagificationVisitor cannot be re-used");
108 d_top = node;
109 }
110
done(TNode node)111 void DagificationVisitor::done(TNode node) {
112 AlwaysAssert(!d_done);
113
114 d_done = true;
115
116 #ifdef CVC4_TRACING
117 # ifdef CVC4_DEBUG
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 */
124
125 // letify subexprs before parents (cascading LETs)
126 std::sort(d_substNodes.begin(), d_substNodes.end());
127
128 for(std::vector<TNode>::iterator i = d_substNodes.begin();
129 i != d_substNodes.end();
130 ++i) {
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
136 continue;
137 }
138
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);
143
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);
148 }
149 }
150
getLets()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;
154 }
155
getDagifiedBody()156 Node DagificationVisitor::getDagifiedBody() {
157 AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
158
159 #ifdef CVC4_TRACING
160 # ifdef CVC4_DEBUG
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 */
167
168 return d_substitutions->apply(d_top);
169 }
170
171 }/* CVC4::printer namespace */
172 }/* CVC4 namespace */
173