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
168
169
170
171
172
173
174
175
176
177
178
|
/********************* */
/*! \file dagification_visitor.h
** \verbatim
** Top contributors (to current version):
** Morgan Deters, Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 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 A dagifier for CVC4 expressions
**
** A dagifier for CVC4 expressions.
**/
#include "cvc4_private.h"
#ifndef __CVC4__PRINTER__DAGIFICATION_VISITOR_H
#define __CVC4__PRINTER__DAGIFICATION_VISITOR_H
#include <string>
#include <unordered_map>
#include <vector>
#include "expr/node.h"
#include "util/hash.h"
namespace CVC4 {
namespace context {
class Context;
}/* CVC4::context namespace */
namespace theory {
class SubstitutionMap;
}/* CVC4::theory namespace */
namespace printer {
/**
* This is a visitor class (intended to be used with CVC4's NodeVisitor)
* that visits an expression looking for common subexpressions that appear
* more than N times, where N is a configurable threshold. Afterward,
* let bindings can be extracted from this visitor and applied to the
* expression.
*
* This dagifier never introduces let bindings for variables, constants,
* unary-minus exprs over variables or constants, or NOT exprs over
* variables or constants. This dagifier never introduces let bindings
* for types.
*/
class DagificationVisitor {
/**
* The threshold for dagification. Subexprs occurring more than this
* number of times are dagified.
*/
const unsigned d_threshold;
/**
* The prefix for introduced let bindings.
*/
const std::string d_letVarPrefix;
/**
* A map of subexprs to their occurrence count.
*/
std::unordered_map<TNode, unsigned, TNodeHashFunction> d_nodeCount;
/**
* The top-most node we are visiting.
*/
TNode d_top;
/**
* This class doesn't operate in a context-dependent fashion, but
* SubstitutionMap does, so we need a context.
*/
context::Context* d_context;
/**
* A map of subexprs to their newly-introduced let bindings.
*/
theory::SubstitutionMap* d_substitutions;
/**
* The current count of let bindings. Used to build unique names
* for the bindings.
*/
unsigned d_letVar;
/**
* Keep track of whether we are done yet (for assertions---this visitor
* can only be used one time).
*/
bool d_done;
/**
* If a subexpr occurs uniquely in one parent expr, this map points to
* it. An expr not occurring as a key in this map means we haven't
* seen it yet (and its occurrence count should be zero). If an expr
* points to the null expr in this map, it means we've seen more than
* one parent, so the subexpr doesn't have a unique parent.
*
* This information is kept because if a subexpr occurs more than the
* threshold, it is normally subject to dagification. But if it occurs
* only in one unique parent expression, and the parent meets the
* threshold too, then the parent will be dagified and there's no point
* in independently dagifying the child. (If it is beyond the threshold
* and occurs in more than one parent, we'll independently dagify.)
*/
std::unordered_map<TNode, TNode, TNodeHashFunction> d_uniqueParent;
/**
* A list of all nodes that meet the occurrence threshold and therefore
* *may* be subject to dagification, except for the unique-parent rule
* mentioned above.
*/
std::vector<TNode> d_substNodes;
public:
/** Our visitor doesn't return anything. */
typedef void return_type;
/**
* Construct a dagification visitor with the given threshold and let
* binding prefix.
*
* @param threshold the threshold to apply for dagification (must be > 0)
* @param letVarPrefix prefix for let bindings (by default, "_let_")
*/
DagificationVisitor(unsigned threshold, std::string letVarPrefix = "_let_");
/**
* Simple destructor, clean up memory.
*/
~DagificationVisitor();
/**
* Returns true if "current" has already been visited a sufficient
* number of times to make it a candidate for dagification, or if
* it cannot ever be subject to dagification.
*/
bool alreadyVisited(TNode current, TNode parent);
/**
* Visit the expr "current", it might be a candidate for a let binder.
*/
void visit(TNode current, TNode parent);
/**
* Marks the node as the starting literal.
*/
void start(TNode node);
/**
* Called when we're done with all visitation. Does postprocessing.
*/
void done(TNode node);
/**
* Get the let substitutions.
*/
const theory::SubstitutionMap& getLets();
/**
* Return the let-substituted expression.
*/
Node getDagifiedBody();
};/* class DagificationVisitor */
}/* CVC4::printer namespace */
}/* CVC4 namespace */
#endif /* __CVC4__PRINTER__DAGIFICATION_VISITOR_H */
|
