Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * A let binding utility.
11 : : */
12 : :
13 : : #include "printer/let_binding.h"
14 : :
15 : : #include <sstream>
16 : :
17 : : #include "expr/skolem_manager.h"
18 : :
19 : : namespace cvc5::internal {
20 : :
21 : 5170099 : LetBinding::LetBinding(const std::string& prefix,
22 : : uint32_t thresh,
23 : : bool traverseBinders,
24 : 5170099 : bool traverseSkolems)
25 : 5170099 : : d_prefix(prefix),
26 : 5170099 : d_thresh(thresh),
27 : 5170099 : d_traverseBinders(traverseBinders),
28 : 5170099 : d_traverseSkolems(traverseSkolems),
29 : 5170099 : d_context(),
30 : 5170099 : d_visitList(&d_context),
31 : 5170099 : d_count(&d_context),
32 : 5170099 : d_letList(&d_context),
33 : 5170099 : d_letMap(&d_context)
34 : : {
35 : 5170099 : }
36 : :
37 : 0 : uint32_t LetBinding::getThreshold() const { return d_thresh; }
38 : :
39 : 21545000 : void LetBinding::process(Node n)
40 : : {
41 [ + + ][ - + ]: 21545000 : if (n.isNull() || d_thresh == 0)
[ + + ]
42 : : {
43 : : // value of 0 means do not introduce let
44 : 13 : return;
45 : : }
46 : : // update the count of occurrences
47 : 21544987 : updateCounts(n);
48 : : }
49 : :
50 : 5162670 : void LetBinding::letify(Node n, std::vector<Node>& letList)
51 : : {
52 : : // first, push the context
53 : 5162670 : pushScope();
54 : : // process the node
55 : 5162670 : process(n);
56 : : // now, letify
57 : 5162670 : letify(letList);
58 : 5162670 : }
59 : :
60 : 5168370 : void LetBinding::letify(std::vector<Node>& letList)
61 : : {
62 : 5168370 : size_t prevSize = d_letList.size();
63 : : // populate the d_letList and d_letMap
64 : 5168370 : convertCountToLet();
65 : : // add the new entries to the letList
66 : 5168370 : letList.insert(letList.end(), d_letList.begin() + prevSize, d_letList.end());
67 : 5168370 : }
68 : :
69 : 5162670 : void LetBinding::pushScope() { d_context.push(); }
70 : :
71 : 5162670 : void LetBinding::popScope() { d_context.pop(); }
72 : :
73 : 71516051 : uint32_t LetBinding::getId(Node n) const
74 : : {
75 : 71516051 : NodeIdMap::const_iterator it = d_letMap.find(n);
76 [ + + ]: 71516051 : if (it == d_letMap.end())
77 : : {
78 : 40627627 : return 0;
79 : : }
80 : 30888424 : return (*it).second;
81 : : }
82 : :
83 : 8813589 : Node LetBinding::convert(Node n, bool letTop) const
84 : : {
85 [ + + ]: 8813589 : if (d_letMap.empty())
86 : : {
87 : 4174027 : return n;
88 : : }
89 : 4639562 : NodeManager* nm = n.getNodeManager();
90 : 4639562 : std::unordered_map<TNode, Node> visited;
91 : 4639562 : std::unordered_map<TNode, Node>::iterator it;
92 : 4639562 : std::vector<TNode> visit;
93 : 4639562 : TNode cur;
94 : 4639562 : visit.push_back(n);
95 : : do
96 : : {
97 : 11709549 : cur = visit.back();
98 : 11709549 : visit.pop_back();
99 : 11709549 : it = visited.find(cur);
100 : :
101 [ + + ]: 11709549 : if (it == visited.end())
102 : : {
103 : 7466252 : uint32_t id = getId(cur);
104 : : // do not letify id 0, or n itself if letTop is false
105 [ + + ][ + + ]: 7466252 : if (id > 0 && (cur != n || letTop))
[ + + ][ + + ]
106 : : {
107 : : // make the let variable
108 : 3377207 : std::stringstream ss;
109 : 3377207 : ss << d_prefix << id;
110 : 3377207 : visited[cur] = NodeManager::mkBoundVar(ss.str(), cur.getType());
111 : 3377207 : }
112 [ - + ]: 4089045 : else if (cur.isClosure())
113 : : {
114 : : // do not convert beneath quantifiers
115 : 0 : visited[cur] = cur;
116 : : }
117 : : else
118 : : {
119 : 4089045 : visited[cur] = Node::null();
120 : 4089045 : visit.push_back(cur);
121 : 4089045 : visit.insert(visit.end(), cur.begin(), cur.end());
122 : : }
123 : : }
124 [ + + ]: 4243297 : else if (it->second.isNull())
125 : : {
126 : 4089045 : Node ret = cur;
127 : 4089045 : bool childChanged = false;
128 : 4089045 : std::vector<Node> children;
129 [ + + ]: 4089045 : if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
130 : : {
131 : 394737 : children.push_back(cur.getOperator());
132 : : }
133 [ + + ]: 7069987 : for (const Node& cn : cur)
134 : : {
135 : 2980942 : it = visited.find(cn);
136 [ - + ][ - + ]: 2980942 : Assert(it != visited.end());
[ - - ]
137 [ - + ][ - + ]: 2980942 : Assert(!it->second.isNull());
[ - - ]
138 [ + + ][ + + ]: 2980942 : childChanged = childChanged || cn != it->second;
139 : 2980942 : children.push_back(it->second);
140 : 2980942 : }
141 [ + + ]: 4089045 : if (childChanged)
142 : : {
143 : 1473445 : ret = nm->mkNode(cur.getKind(), children);
144 : : }
145 : 4089045 : visited[cur] = ret;
146 : 4089045 : }
147 [ + + ]: 11709549 : } while (!visit.empty());
148 [ - + ][ - + ]: 4639562 : Assert(visited.find(n) != visited.end());
[ - - ]
149 [ - + ][ - + ]: 4639562 : Assert(!visited.find(n)->second.isNull());
[ - - ]
150 : 4639562 : return visited[n];
151 : 4639562 : }
152 : :
153 : 21544987 : void LetBinding::updateCounts(Node n)
154 : : {
155 : 21544987 : NodeIdMap::iterator it;
156 : 21544987 : std::vector<Node> visit;
157 : 21544987 : TNode cur;
158 : 21544987 : visit.push_back(n);
159 : : do
160 : : {
161 : 61651279 : cur = visit.back();
162 : 61651279 : it = d_count.find(cur);
163 [ + + ][ + + ]: 61651279 : bool isSkolem = (d_traverseSkolems && cur.getKind() == Kind::SKOLEM);
164 : : // do not traverse beneath quantifiers if d_traverseBinders is false.
165 [ + + ]: 61594232 : if ((!isSkolem && cur.getNumChildren() == 0)
166 [ + + ]: 35390947 : || cur.getKind() == Kind::BOUND_VAR_LIST
167 [ + + ][ + + ]: 123302558 : || (!d_traverseBinders && cur.isClosure()))
[ + + ][ + + ]
168 : : {
169 : 26308662 : visit.pop_back();
170 : 26308662 : continue;
171 : : }
172 [ + + ]: 35342617 : if (it == d_count.end())
173 : : {
174 : 8726571 : d_count[cur] = 0;
175 [ + + ]: 8726571 : if (isSkolem)
176 : : {
177 : : SkolemId skid;
178 : 3838 : Node cacheVal;
179 [ + + ][ - - ]: 3838 : if (SkolemManager::isSkolemFunction(cur, skid, cacheVal)
180 [ + - ][ + + ]: 3838 : && !cacheVal.isNull())
[ + - ]
181 : : {
182 [ + + ]: 3706 : if (cacheVal.getKind() == Kind::SEXPR)
183 : : {
184 : 170 : visit.insert(visit.end(), cacheVal.begin(), cacheVal.end());
185 : : }
186 : : else
187 : : {
188 : 3536 : visit.push_back(cacheVal);
189 : : }
190 : : }
191 : 3838 : }
192 : : else
193 : : {
194 [ + - ]: 8722733 : if (cur.hasOperator())
195 : : {
196 : 8722733 : visit.push_back(cur.getOperator());
197 : : }
198 : 8722733 : visit.insert(visit.end(), cur.begin(), cur.end());
199 : : }
200 : : }
201 : : else
202 : : {
203 [ + + ]: 26616046 : if ((*it).second == 0)
204 : : {
205 : 8726571 : d_visitList.push_back(cur);
206 : : }
207 : 26616046 : d_count[cur] = (*it).second + 1;
208 : 26616046 : visit.pop_back();
209 : : }
210 [ + + ]: 61651279 : } while (!visit.empty());
211 : 21544987 : }
212 : :
213 : 5168370 : void LetBinding::convertCountToLet()
214 : : {
215 [ - + ][ - + ]: 5168370 : Assert(d_thresh > 0);
[ - - ]
216 : : // Assign ids for those whose d_count is >= d_thresh, traverse in d_visitList
217 : : // in order so that deeper nodes are assigned lower identifiers, which
218 : : // ensures the let list can be printed.
219 : 5168370 : NodeIdMap::const_iterator itc;
220 [ + + ]: 13894941 : for (const Node& n : d_visitList)
221 : : {
222 [ - + ]: 8726571 : if (d_letMap.find(n) != d_letMap.end())
223 : : {
224 : : // already letified, perhaps at a lower context
225 : 0 : continue;
226 : : }
227 : 8726571 : itc = d_count.find(n);
228 [ - + ][ - + ]: 8726571 : Assert(itc != d_count.end());
[ - - ]
229 [ + + ]: 8726571 : if ((*itc).second >= d_thresh)
230 : : {
231 : 2503071 : d_letList.push_back(n);
232 : : // start with id 1
233 : 2503071 : size_t id = d_letMap.size() + 1;
234 : 2503071 : d_letMap[n] = id;
235 : : }
236 : : }
237 : 5168370 : }
238 : :
239 : : } // namespace cvc5::internal
|
