Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Dejan Jovanovic, Clark Barrett
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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.
11 : : * ****************************************************************************
12 : : *
13 : : * A substitution mapping for theory simplification.
14 : : */
15 : :
16 : : #include "theory/substitutions.h"
17 : : #include "expr/node_algorithm.h"
18 : : #include "theory/rewriter.h"
19 : :
20 : : using namespace std;
21 : :
22 : : namespace cvc5::internal {
23 : : namespace theory {
24 : :
25 : 467997 : SubstitutionMap::SubstitutionMap(context::Context* context, bool compress)
26 : : : d_context(),
27 : : d_substitutions(context ? context : &d_context),
28 : : d_substitutionCache(),
29 : : d_cacheInvalidated(false),
30 : : d_compress(compress),
31 [ + + ][ + + ]: 467997 : d_cacheInvalidator(context ? context : &d_context, d_cacheInvalidated)
32 : : {
33 : 467997 : }
34 : :
35 : 39326 : std::unordered_map<Node, Node> SubstitutionMap::getSubstitutions() const
36 : : {
37 : 39326 : std::unordered_map<Node, Node> subs;
38 [ + + ]: 96445 : for (const auto& sub : d_substitutions)
39 : : {
40 : 57119 : subs.emplace(sub.first, sub.second);
41 : : }
42 : 39326 : return subs;
43 : : }
44 : :
45 : 3 : Node SubstitutionMap::toFormula(NodeManager* nm) const
46 : : {
47 : 6 : std::vector<Node> conj;
48 [ + + ]: 13 : for (const auto& sub : d_substitutions)
49 : : {
50 : 10 : conj.emplace_back(nm->mkNode(Kind::EQUAL, sub.first, sub.second));
51 : : }
52 : 6 : return nm->mkAnd(conj);
53 : : }
54 : :
55 : : struct substitution_stack_element {
56 : : TNode d_node;
57 : : bool d_children_added;
58 : 6538470 : substitution_stack_element(TNode node) : d_node(node), d_children_added(false)
59 : : {
60 : 6538470 : }
61 : : };/* struct substitution_stack_element */
62 : :
63 : 4230720 : Node SubstitutionMap::internalSubstitute(TNode t,
64 : : NodeCache& cache,
65 : : std::set<TNode>* tracker,
66 : : const ShouldTraverseCallback* stc)
67 : : {
68 [ + - ]: 4230720 : Trace("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << endl;
69 : :
70 [ + + ]: 4230720 : if (d_substitutions.empty()) {
71 : 2670940 : return t;
72 : : }
73 : :
74 : : // Do a topological sort of the subexpressions and substitute them
75 : 1559780 : vector<substitution_stack_element> toVisit;
76 : 1559780 : toVisit.push_back((TNode) t);
77 : :
78 [ + + ]: 12296200 : while (!toVisit.empty())
79 : : {
80 : : // The current node we are processing
81 : 10736400 : substitution_stack_element& stackHead = toVisit.back();
82 : 10736400 : TNode current = stackHead.d_node;
83 : :
84 [ + - ]: 10736400 : Trace("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << endl;
85 : :
86 : : // If node already in the cache we're done, pop from the stack
87 : 10736400 : NodeCache::iterator find = cache.find(current);
88 [ + + ]: 10736400 : if (find != cache.end()) {
89 : 876040 : toVisit.pop_back();
90 : 876040 : continue;
91 : : }
92 : :
93 : 9860380 : NodeMap::iterator find2 = d_substitutions.find(current);
94 [ + + ]: 9860380 : if (find2 != d_substitutions.end()) {
95 : 545813 : Node rhs = (*find2).second;
96 : : // if the substitution changes the current term
97 [ + - ]: 545813 : if (rhs != current)
98 : : {
99 : 545813 : find = cache.find(rhs);
100 [ + + ]: 545813 : if (find == cache.end())
101 : : {
102 : : // visit the RHS
103 : 200124 : toVisit.push_back((TNode)rhs);
104 : 200124 : continue;
105 : : }
106 : : // update the substitution map if using compression
107 [ + + ][ + + ]: 345689 : if (tracker == nullptr && d_compress)
108 : : {
109 : 343495 : d_substitutions[current] = cache[rhs];
110 : : }
111 : 345689 : cache[current] = cache[rhs];
112 : 345689 : toVisit.pop_back();
113 [ + + ]: 345689 : if (tracker != nullptr)
114 : : {
115 : 2170 : tracker->insert(current);
116 : : }
117 : 345689 : continue;
118 : : }
119 : : }
120 : :
121 : : // Not yet substituted, so process
122 [ + + ]: 9314570 : if (stackHead.d_children_added)
123 : : {
124 : : // Children have been processed, so substitute
125 : 3997830 : NodeBuilder builder(current.getNodeManager(), current.getKind());
126 [ + + ]: 3997830 : if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
127 : : {
128 : 650095 : builder << Node(cache[current.getOperator()]);
129 : : }
130 [ + + ]: 12391800 : for (const Node& nc : current)
131 : : {
132 [ - + ][ - + ]: 8394000 : Assert(cache.find(nc) != cache.end());
[ - - ]
133 : 8394000 : builder << Node(cache[nc]);
134 : : }
135 : : // Mark the substitution and continue
136 : 3997830 : Node result = builder;
137 [ + + ]: 3997830 : if (result != current) {
138 : 1226630 : find = cache.find(result);
139 [ + + ]: 1226630 : if (find != cache.end()) {
140 : 17648 : result = find->second;
141 : : }
142 : : else {
143 : 1208980 : find2 = d_substitutions.find(result);
144 [ - + ]: 1208980 : if (find2 != d_substitutions.end()) {
145 : 0 : Node rhs = (*find2).second;
146 [ - - ]: 0 : if (rhs != result)
147 : : {
148 : 0 : find = cache.find(rhs);
149 [ - - ]: 0 : if (find == cache.end())
150 : : {
151 : : // visit the RHS
152 : 0 : toVisit.push_back((TNode)rhs);
153 : 0 : continue;
154 : : }
155 : : // update the substitution map if using compression
156 [ - - ]: 0 : if (d_compress)
157 : : {
158 : 0 : d_substitutions[result] = cache[rhs];
159 : : }
160 : 0 : cache[result] = cache[rhs];
161 [ - - ]: 0 : if (tracker != nullptr)
162 : : {
163 : 0 : tracker->insert(result);
164 : : }
165 : 0 : result = cache[rhs];
166 : : }
167 : : }
168 : : }
169 : : }
170 [ + - ]: 3997830 : Trace("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << endl;
171 : 3997830 : cache[current] = result;
172 : 3997830 : toVisit.pop_back();
173 : : }
174 : : else
175 : : {
176 : : // Mark that we have added the children if any
177 [ + + ][ + + ]: 5316740 : bool recurse = (stc == nullptr || (*stc)(current));
[ + + ][ - - ]
178 : 5316740 : if (recurse
179 [ + + ][ + + ]: 6637440 : && (current.getNumChildren() > 0
[ + + ]
180 [ + + ]: 1320700 : || current.getMetaKind() == kind::metakind::PARAMETERIZED))
181 : : {
182 : 3997830 : stackHead.d_children_added = true;
183 : : // We need to add the operator, if any
184 [ + + ]: 3997830 : if(current.getMetaKind() == kind::metakind::PARAMETERIZED) {
185 : 1300190 : TNode opNode = current.getOperator();
186 : 650095 : NodeCache::iterator opFind = cache.find(opNode);
187 [ + + ]: 650095 : if (opFind == cache.end()) {
188 : 205703 : toVisit.push_back(opNode);
189 : : }
190 : : }
191 : : // We need to add the children
192 [ + + ]: 12391800 : for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
193 : 16788000 : TNode childNode = *child_it;
194 : 8394000 : NodeCache::iterator childFind = cache.find(childNode);
195 [ + + ]: 8394000 : if (childFind == cache.end()) {
196 : 4572860 : toVisit.push_back(childNode);
197 : : }
198 : : }
199 : : }
200 : : else
201 : : {
202 : : // No children, so we're done
203 [ + - ]: 1318910 : Trace("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << endl;
204 : 1318910 : cache[current] = current;
205 : 1318910 : toVisit.pop_back();
206 : : }
207 : : }
208 : : }
209 : :
210 : : // Return the substituted version
211 : 1559780 : return cache[t];
212 : : } /* SubstitutionMap::internalSubstitute() */
213 : :
214 : 6911050 : void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache)
215 : : {
216 : : // don't check type equal here, since this utility may be used in conversions
217 : : // that change the types of terms
218 [ + - ]: 6911050 : Trace("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << endl;
219 : : // Shouldn't use compression if replacing a current substitution, or otherwise
220 : : // the range of other d_substitutions can be out of sync.
221 : : // For example, if we have substitution { y -> f(x) } and then later add
222 : : // { x -> a } the substitution may be updated to { y -> f(a), x -> a }. If
223 : : // we later erase x, then we'd have { y -> f(a) }, but x no longer maps to a.
224 : 6911050 : Assert(d_substitutions.find(x) == d_substitutions.end() || !d_compress);
225 : :
226 : : // this causes a later assert-fail (the rhs != current one, above) anyway
227 : : // putting it here is easier to diagnose
228 [ - + ][ - + ]: 6911050 : Assert(x != t) << "cannot substitute a term for itself";
[ - - ]
229 : :
230 : 6911050 : d_substitutions[x] = t;
231 : :
232 : : // Also invalidate the cache if necessary
233 [ + + ]: 6911050 : if (invalidateCache) {
234 : 6910920 : d_cacheInvalidated = true;
235 : : }
236 : : else {
237 : 125 : d_substitutionCache[x] = d_substitutions[x];
238 : : }
239 : 6911050 : }
240 : :
241 : :
242 : 21495 : void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateCache)
243 : : {
244 : 21495 : NodeMap::const_iterator it = subMap.begin();
245 : 21495 : NodeMap::const_iterator it_end = subMap.end();
246 [ + + ]: 44808 : for (; it != it_end; ++ it) {
247 [ - + ][ - + ]: 23313 : Assert(d_substitutions.find((*it).first) == d_substitutions.end());
[ - - ]
248 : 23313 : d_substitutions[(*it).first] = (*it).second;
249 [ - + ]: 23313 : if (!invalidateCache) {
250 : 0 : d_substitutionCache[(*it).first] = d_substitutions[(*it).first];
251 : : }
252 : : }
253 [ + - ]: 21495 : if (invalidateCache) {
254 : 21495 : d_cacheInvalidated = true;
255 : : }
256 : 21495 : }
257 : :
258 : 0 : void SubstitutionMap::eraseSubstitution(TNode x, bool invalidateCache)
259 : : {
260 : : // shouldn't use compression
261 : 0 : Assert(!d_compress);
262 : 0 : Assert(d_substitutions.find(x) != d_substitutions.end());
263 : 0 : d_substitutions[x] = x;
264 [ - - ]: 0 : if (invalidateCache)
265 : : {
266 : 0 : d_cacheInvalidated = true;
267 : : }
268 : 0 : }
269 : :
270 : 4230720 : Node SubstitutionMap::apply(TNode t,
271 : : Rewriter* r,
272 : : std::set<TNode>* tracker,
273 : : const ShouldTraverseCallback* stc)
274 : : {
275 [ + - ]: 4230720 : Trace("substitution") << "SubstitutionMap::apply(" << t << ")" << endl;
276 : :
277 : : // Setup the cache
278 [ + + ]: 4230720 : if (d_cacheInvalidated) {
279 : 170413 : d_substitutionCache.clear();
280 : 170413 : d_cacheInvalidated = false;
281 [ + - ]: 170413 : Trace("substitution") << "-- reset the cache" << endl;
282 : : }
283 : :
284 : : // Perform the substitution
285 : 4230720 : Node result = internalSubstitute(t, d_substitutionCache, tracker, stc);
286 [ + - ]: 4230720 : Trace("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << endl;
287 : :
288 [ + + ]: 4230720 : if (r != nullptr)
289 : : {
290 : 2497560 : Node orig = result;
291 : 2497560 : result = r->rewrite(result);
292 : 4995110 : Assert(r->rewrite(result) == result)
293 : 2497560 : << "Non-idempotent rewrite: " << orig << " --> " << result << " --> "
294 : 2497560 : << r->rewrite(result);
295 : : }
296 : :
297 : 4230710 : return result;
298 : : }
299 : :
300 : 0 : void SubstitutionMap::print(ostream& out) const {
301 : 0 : NodeMap::const_iterator it = d_substitutions.begin();
302 : 0 : NodeMap::const_iterator it_end = d_substitutions.end();
303 [ - - ]: 0 : for (; it != it_end; ++ it) {
304 : 0 : out << (*it).first << " -> " << (*it).second << endl;
305 : : }
306 : 0 : }
307 : :
308 : 0 : std::string SubstitutionMap::toString() const
309 : : {
310 : 0 : std::stringstream ss;
311 : 0 : print(ss);
312 : 0 : return ss.str();
313 : : }
314 : :
315 : : } // namespace theory
316 : :
317 : 0 : std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i) {
318 : 0 : return out << "[CDMap-iterator]";
319 : : }
320 : :
321 : : } // namespace cvc5::internal
|
