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 : : * This pre-processing pass implementes the normalizer in the FMCAD 2025 paper.
11 : : */
12 : :
13 : : #include "preprocessing/passes/normalize.h"
14 : :
15 : : #include <unordered_map>
16 : :
17 : : #include "expr/cardinality_constraint.h"
18 : : #include "expr/normalize_sort_converter.h"
19 : : #include "expr/skolem_manager.h"
20 : : #include "preprocessing/assertion_pipeline.h"
21 : : #include "preprocessing/preprocessing_pass_context.h"
22 : : #include "util/statistics_registry.h"
23 : :
24 : : using namespace cvc5::internal::kind;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace preprocessing {
28 : : namespace passes {
29 : :
30 : : /**
31 : : * Compute (and cache) the superpattern for a given symbol (used in Step 5).
32 : : *
33 : : * A superpattern has one segment per equivalence class. Each segment begins
34 : : * with the count of -1 values (the number of members of the class where the
35 : : * symbol does not occur) followed by the sorted list of non-negative role
36 : : * indices where the symbol does occur.
37 : : *
38 : : * @param symbol The symbol whose superpattern is requested.
39 : : * @param eqClasses The equivalence classes of assertions (NodeInfo*).
40 : : * @param symbolOccurrences Map from symbol to the assertions in which it
41 : : * occurs.
42 : : * @param patternCache Cache mapping symbols to their computed superpatterns.
43 : : * @return A const reference to the cached superpattern for the symbol.
44 : : */
45 : 4 : static const std::vector<std::vector<int32_t>>& getOrComputeSuperpattern(
46 : : const std::string& symbol,
47 : : const std::vector<std::vector<NodeInfo*>>& eqClasses,
48 : : const std::unordered_map<std::string,
49 : : std::vector<std::shared_ptr<NodeInfo>>>&
50 : : symbolOccurrences,
51 : : std::unordered_map<std::string, std::vector<std::vector<int32_t>>>&
52 : : patternCache)
53 : : {
54 : 4 : auto it = patternCache.find(symbol);
55 [ - + ]: 4 : if (it != patternCache.end())
56 : : {
57 : 0 : return it->second;
58 : : }
59 : :
60 : : // Initialize the superpattern with empty vectors for each segment
61 : 4 : std::vector<std::vector<int32_t>> superpattern(eqClasses.size());
62 : 4 : auto symbolIt = symbolOccurrences.find(symbol);
63 [ - + ][ - + ]: 4 : Assert(symbolIt != symbolOccurrences.end());
[ - - ]
64 : :
65 : : // Iterate over all occurrences of the symbol
66 [ + + ]: 10 : for (const auto& nodeInfo : symbolIt->second)
67 : : {
68 : 6 : auto roleIt = nodeInfo->role.find(symbol);
69 [ - + ][ - + ]: 6 : Assert(roleIt != nodeInfo->role.end());
[ - - ]
70 : :
71 : : // Get the equivalence class ID for this node
72 : 6 : size_t eqClassId = nodeInfo->id;
73 : :
74 : : // Push the non-negative value to the corresponding segment in the
75 : : // superpattern
76 : 6 : superpattern[eqClassId].push_back(roleIt->second);
77 : : }
78 : :
79 : : // Sort each segment in the superpattern and compute the -1 count
80 [ + + ]: 8 : for (size_t i = 0; i < superpattern.size(); ++i)
81 : : {
82 : 4 : std::sort(superpattern[i].begin(), superpattern[i].end());
83 : : // The count of -1s is the size of the equivalence class minus
84 : : // the number of non-negative values
85 : 8 : superpattern[i].insert(superpattern[i].begin(),
86 : 4 : eqClasses[i].size() - superpattern[i].size());
87 : : }
88 : :
89 : 4 : auto& ret = patternCache[symbol];
90 : 4 : ret = std::move(superpattern);
91 : 4 : return ret;
92 : 4 : }
93 : :
94 : : /**
95 : : * Comparator for NodeInfo* based on their superpatterns (used in Step 5).
96 : : *
97 : : * Comparison proceeds segment-by-segment:
98 : : * - Compare the leading -1 count for the segment.
99 : : * - Then compare the occurrence positions lexicographically.
100 : : * - If one segment has more positions, it is considered greater.
101 : : *
102 : : * Superpatterns are computed on demand and cached in patternCache.
103 : : *
104 : : * @param a First NodeInfo.
105 : : * @param b Second NodeInfo.
106 : : * @param eqClasses Equivalence classes (for segment sizing).
107 : : * @param patternCache Cache of computed superpatterns.
108 : : * @param symbolOccurrences Occurrence lists per symbol.
109 : : * @return True if a should come before b.
110 : : */
111 : 2 : static bool compareBySuperpattern(
112 : : NodeInfo* a,
113 : : NodeInfo* b,
114 : : const std::vector<std::vector<NodeInfo*>>& eqClasses,
115 : : std::unordered_map<std::string, std::vector<std::vector<int32_t>>>&
116 : : patternCache,
117 : : const std::unordered_map<std::string,
118 : : std::vector<std::shared_ptr<NodeInfo>>>&
119 : : symbolOccurrences)
120 : : {
121 : 2 : auto itA = a->varNames.begin();
122 : 2 : auto itB = b->varNames.begin();
123 : :
124 [ + - ][ + - ]: 2 : while (itA != a->varNames.end() && itB != b->varNames.end())
[ + - ]
125 : : {
126 : 2 : const std::string& symbolA = itA->first;
127 : 2 : const std::string& symbolB = itB->first;
128 : :
129 [ - + ]: 2 : if (symbolA == symbolB)
130 : : {
131 : 0 : ++itA;
132 : 0 : ++itB;
133 : 0 : continue;
134 : : }
135 : :
136 : 2 : const auto& superpatternA = getOrComputeSuperpattern(
137 : : symbolA, eqClasses, symbolOccurrences, patternCache);
138 : 2 : const auto& superpatternB = getOrComputeSuperpattern(
139 : : symbolB, eqClasses, symbolOccurrences, patternCache);
140 : :
141 : : // Compare superpatterns segment by segment
142 [ + - ]: 2 : for (size_t i = 0; i < superpatternA.size(); ++i)
143 : : {
144 : 2 : const auto& patA = superpatternA[i];
145 : 2 : const auto& patB = superpatternB[i];
146 : :
147 : : // Compare the count of -1s in the segment
148 [ + - ]: 2 : if (patA[0] != patB[0])
149 : : {
150 : 2 : return patA[0] < patB[0];
151 : : }
152 : :
153 : : // Compare the non-negative values in the segment
154 [ - - ][ - - ]: 0 : for (size_t j = 1; j < patA.size() && j < patB.size(); ++j)
[ - - ]
155 : : {
156 [ - - ]: 0 : if (patA[j] != patB[j])
157 : : {
158 : 0 : return patA[j] < patB[j];
159 : : }
160 : : }
161 : :
162 : : // If one segment has more non-negative values, it is considered greater
163 [ - - ]: 0 : if (patA.size() != patB.size())
164 : : {
165 : 0 : return patA.size() < patB.size();
166 : : }
167 : : }
168 : :
169 : 0 : ++itA;
170 : 0 : ++itB;
171 : : }
172 : :
173 : : // Handle cases where one iterator reaches the end before the other
174 [ - - ]: 0 : if (itA != a->varNames.end()) return true;
175 [ - - ]: 0 : if (itB != b->varNames.end()) return false;
176 : :
177 : 0 : return false;
178 : : }
179 : :
180 : : /**
181 : : * Comparator for NodeInfo* based on normalized variable names (used in Step 8).
182 : : *
183 : : * @param a First NodeInfo.
184 : : * @param b Second NodeInfo.
185 : : * @param normalizedName Map from original symbol to normalized name.
186 : : * @return True if a should come before b.
187 : : */
188 : 4 : static bool compareByNormalizedNames(
189 : : NodeInfo* a,
190 : : NodeInfo* b,
191 : : std::unordered_map<std::string, std::string>& normalizedName)
192 : : {
193 : 4 : size_t sz = std::min(a->varNames.size(), b->varNames.size());
194 [ + - ]: 4 : for (size_t i = 0; i < sz; ++i)
195 : : {
196 : 4 : const std::string& symbolA = a->varNames[i].first;
197 : 4 : const std::string& symbolB = b->varNames[i].first;
198 : 4 : const std::string& normNameA = normalizedName[symbolA];
199 : 4 : const std::string& normNameB = normalizedName[symbolB];
200 [ + - ]: 4 : if (normNameA != normNameB)
201 : : {
202 : 4 : return normNameA < normNameB;
203 : : }
204 : : }
205 : 0 : return false;
206 : : }
207 : :
208 : : /**
209 : : * Constructor for the Normalize preprocessing pass.
210 : : *
211 : : * @param preprocContext The preprocessing pass context.
212 : : */
213 : 52018 : Normalize::Normalize(PreprocessingPassContext* preprocContext)
214 : : : PreprocessingPass(preprocContext, "normalize"),
215 : 52018 : d_statistics(statisticsRegistry()) {};
216 : :
217 : : /**
218 : : * Generates a compressed encoding (also known as a pattern) of the given node's
219 : : * DAG structure. Additionally, calculates the role map, which is used later for
220 : : * super-pattern comparison.
221 : : *
222 : : * @param root The node itself
223 : : * @param encoding The resulting compressed encoding string.
224 : : * @param role A map tracking the first occurrence index of each symbol (used in
225 : : * super-patterns).
226 : : */
227 : 4 : void generateEncoding(const Node& root,
228 : : std::string& encoding,
229 : : std::unordered_map<std::string, int32_t>& role)
230 : : {
231 : 4 : std::vector<std::pair<Node, Node>> stack; // Pair of node, parent
232 : 4 : std::unordered_map<Node, bool> visited;
233 : 4 : std::unordered_map<Node, size_t> subtreeIdMap;
234 : 4 : std::unordered_map<std::string, size_t> symbolMap;
235 : 4 : size_t varIdCounter = 1;
236 : 4 : size_t subtreeIdCounter = 1;
237 : 4 : int32_t cnt = 0;
238 : :
239 : 4 : std::vector<std::string> nodeEncodings;
240 : :
241 : 4 : stack.push_back({root, root});
242 : :
243 [ + + ]: 44 : while (!stack.empty())
244 : : {
245 : : // Get current node and its parent
246 : 40 : auto [n, parent] = stack.back();
247 : :
248 : 40 : auto [it, inserted] = visited.emplace(n, false);
249 [ + + ]: 40 : if (inserted)
250 : : {
251 : : // First time seeing this node
252 [ + + ][ + + ]: 28 : if (!n.isVar() && !n.isConst())
[ + + ]
253 : : {
254 : : // Operator node
255 [ + + ]: 36 : for (const Node& child : n)
256 : : {
257 [ + - ]: 24 : if (visited.find(child) == visited.end())
258 : : {
259 : : // Push child with current node n as its parent
260 : 24 : stack.push_back({child, n});
261 : : }
262 : 24 : }
263 : : }
264 : : else
265 : : {
266 : : // For variables and constants, update role map and mark as processed
267 : : // immediately
268 [ + + ]: 16 : if (n.isVar())
269 : : {
270 : 8 : std::string symbol = std::to_string(n.getId());
271 : :
272 : 8 : if (role.find(symbol) == role.end()
273 [ + - ][ + - ]: 8 : && parent.getKind()
[ + - ]
274 : : != cvc5::internal::Kind::
275 : : INST_ATTRIBUTE) // Ignore variables in INST_ATTRIBUTE
276 : : // (qid)
277 : : {
278 : 8 : role[symbol] = cnt;
279 : : }
280 : 8 : cnt++; // Increment cnt whether variable is new or not
281 : 8 : }
282 : :
283 : 16 : it->second = true;
284 : 16 : stack.pop_back();
285 : : }
286 : : }
287 [ + - ]: 12 : else if (!it->second)
288 : : {
289 : : // Second time seeing this node, process it
290 : :
291 [ - + ]: 12 : if (n.isVar())
292 : : {
293 : : // Variables are processed when included in operator nodes
294 : 0 : stack.pop_back();
295 : : }
296 [ - + ]: 12 : else if (n.isConst())
297 : : {
298 : : // Constants are processed when included in operator nodes
299 : 0 : stack.pop_back();
300 : : }
301 : : else
302 : : {
303 [ + - ]: 12 : if (n.hasOperator())
304 : : {
305 : 12 : Node opNode = n.getOperator();
306 [ - + ]: 12 : if (opNode.isVar())
307 : : {
308 : 0 : std::string symbol = std::to_string(opNode.getId());
309 : :
310 : 0 : if (role.find(symbol) == role.end()
311 : 0 : && n.getKind() != cvc5::internal::Kind::INST_ATTRIBUTE)
312 : : {
313 : 0 : role[symbol] = cnt;
314 : : }
315 : 0 : cnt++; // Increment cnt whether variable is new or not
316 : 0 : }
317 : 12 : }
318 : :
319 : : // Assign an ID to this node
320 : 12 : size_t id = subtreeIdCounter++;
321 : 12 : subtreeIdMap[n] = id;
322 : :
323 : : // Build the encoding string
324 : 12 : std::string nodeEncoding = std::to_string(id) + ":";
325 : :
326 : : // Include operator kind
327 : 12 : cvc5::internal::Kind k = static_cast<cvc5::internal::Kind>(n.getKind());
328 : 12 : std::string opKind = cvc5::internal::kind::toString(k);
329 : 12 : nodeEncoding += opKind + ",";
330 : :
331 : : // For each child, include appropriate encoding
332 [ + + ]: 36 : for (size_t i = n.getNumChildren(); i-- > 0;)
333 : : {
334 : 24 : Node child = n[i];
335 [ + + ]: 24 : if (child.isConst())
336 : : {
337 : : // Include '^' followed by the constant value and '^'
338 : 8 : std::string value = std::to_string(child.getId());
339 : 8 : nodeEncoding += "^" + value + "^,";
340 : 8 : }
341 [ + + ]: 16 : else if (child.isVar())
342 : : {
343 : : // Update role map
344 : 8 : std::string symbol = std::to_string(child.getId());
345 : :
346 : 8 : if (role.find(symbol) == role.end()
347 [ - + ][ - - ]: 8 : && n.getKind() != cvc5::internal::Kind::INST_ATTRIBUTE)
[ - + ]
348 : : {
349 : 0 : role[symbol] = cnt;
350 : : }
351 : 8 : cnt++; // Increment cnt whether variable is new or not
352 : :
353 : : // Assign ID to variable if not already assigned
354 [ + - ]: 8 : if (symbolMap.find(symbol) == symbolMap.end())
355 : : {
356 : 8 : symbolMap[symbol] = varIdCounter++;
357 : : }
358 : :
359 : : // Include variable ID
360 : 8 : size_t varId = symbolMap[symbol];
361 : 8 : nodeEncoding += std::to_string(varId) + ",";
362 : 8 : }
363 : : else
364 : : {
365 : : // Subtree: Include '|' followed by its ID and '|'
366 : 8 : size_t childId = subtreeIdMap[child];
367 : 8 : nodeEncoding += "|" + std::to_string(childId) + "|,";
368 : : }
369 : 24 : }
370 : :
371 : : // Remove the last comma
372 [ + - ]: 12 : if (n.getNumChildren() > 0)
373 : : {
374 : 12 : nodeEncoding.pop_back();
375 : : }
376 : :
377 : 12 : nodeEncoding += ";";
378 : :
379 : : // Collect the encoding instead of concatenating
380 : 12 : nodeEncodings.push_back(nodeEncoding);
381 : :
382 : : // Mark as processed and pop
383 : 12 : it->second = true;
384 : 12 : stack.pop_back();
385 : 12 : }
386 : : }
387 : : else
388 : : {
389 : : // Node has already been processed
390 : 0 : stack.pop_back();
391 : : }
392 : 40 : }
393 : :
394 : : // Concatenate the node encodings in reverse order
395 [ + + ]: 16 : for (auto it = nodeEncodings.rbegin(); it != nodeEncodings.rend(); ++it)
396 : : {
397 : 12 : encoding += *it;
398 : : }
399 : 4 : }
400 : :
401 : : /**
402 : : * Retrieves information about a node, including its encoding and role map.
403 : : *
404 : : * @param node The node to analyze.
405 : : * @return A unique pointer to the NodeInfo structure containing the node's
406 : : * details.
407 : : */
408 : 4 : std::unique_ptr<NodeInfo> Normalize::getNodeInfo(const Node& node)
409 : : {
410 : 4 : std::string encoding;
411 : 4 : std::unordered_map<std::string, int32_t> role;
412 : 4 : generateEncoding(node, encoding, role);
413 : :
414 : : std::vector<std::pair<std::string, int32_t>> varNames(role.begin(),
415 : 4 : role.end());
416 : 4 : std::sort(varNames.begin(),
417 : : varNames.end(),
418 : 8 : [](const std::pair<std::string, int32_t>& A,
419 : : const std::pair<std::string, int32_t>& B) {
420 : 8 : return A.second > B.second;
421 : : });
422 : :
423 : 8 : return std::make_unique<NodeInfo>(node, encoding, 0, role, varNames);
424 : 4 : }
425 : :
426 : : /**
427 : : * Calculates the number of digits in a given non-negative integer.
428 : : *
429 : : * @param n The non-negative integer to analyze.
430 : : * @return The number of digits in the non-negative integer.
431 : : */
432 : 6 : size_t numDigits(size_t n)
433 : : {
434 [ + + ]: 6 : if (n == 0)
435 : : {
436 : 2 : return 1;
437 : : }
438 : 4 : int count = 0;
439 [ + + ]: 8 : while (n > 0)
440 : : {
441 : 4 : n = n / 10;
442 : 4 : count++;
443 : : }
444 : 4 : return count;
445 : : }
446 : :
447 : : /**
448 : : * Renames variables in a node to ensure consistent naming.
449 : : *
450 : : * @param n The node to rename.
451 : : * @param freeVar2node Map for free variable substitutions.
452 : : * @param boundVar2node Map for bound variable substitutions.
453 : : * @param normalizedName Map for storing normalized variable names.
454 : : * @param nodeManager The node manager for creating new nodes.
455 : : * @param d_preprocContext The preprocessing pass context.
456 : : * @param sortNormalizer The sort normalizer for type conversion.
457 : : * @param hasQID Flag indicating if quantifier IDs are present.
458 : : * @return The renamed node.
459 : : */
460 : 4 : Node rename(const Node& n,
461 : : std::unordered_map<Node, Node>& freeVar2node,
462 : : std::unordered_map<Node, Node>& boundVar2node,
463 : : std::unordered_map<std::string, std::string>& normalizedName,
464 : : NodeManager* nodeManager,
465 : : PreprocessingPassContext* d_preprocContext,
466 : : NormalizeSortNodeConverter& sortNormalizer,
467 : : bool& hasQID)
468 : : {
469 : : // Map to cache normalized nodes
470 : 4 : std::unordered_map<Node, Node> normalized;
471 : :
472 : : // Stack for iterative traversal
473 : 4 : std::vector<Node> stack;
474 : :
475 : : // Map to keep track of visited nodes
476 : 4 : std::unordered_map<Node, bool> visited;
477 : :
478 : : // Initialize a global variable counter for variable renaming
479 : : static size_t globalVarCounter = 0;
480 : :
481 : : // Initialize a variable counter for bound variables
482 : 4 : size_t boundVarCounter = 0;
483 : 4 : boundVar2node.clear();
484 : :
485 : : // Push the root node onto the stack
486 : 4 : stack.push_back(n);
487 : :
488 [ + + ]: 44 : while (!stack.empty())
489 : : {
490 : 40 : Node current = stack.back();
491 : :
492 : 40 : auto [it, inserted] = visited.emplace(current, false);
493 [ + + ]: 40 : if (inserted)
494 : : {
495 : : // First time seeing this node
496 : :
497 [ + + ][ + + ]: 28 : if (current.isConst() || current.isVar())
[ + + ]
498 : : {
499 : : // For constants and variables, process immediately
500 [ + + ]: 16 : if (current.isVar())
501 : : {
502 [ - + ]: 8 : if (current.getKind() == cvc5::internal::Kind::BOUND_VARIABLE)
503 : : {
504 : 0 : auto it_bv = boundVar2node.find(current);
505 [ - - ]: 0 : if (it_bv != boundVar2node.end())
506 : : {
507 : 0 : normalized[current] = it_bv->second;
508 : : }
509 : : else
510 : : {
511 : 0 : size_t id = boundVarCounter++;
512 : : std::string new_var_name = "u"
513 : 0 : + std::string(8 - numDigits(id), '0')
514 : 0 : + std::to_string(id);
515 : : Node ret = nodeManager->mkBoundVar(
516 : 0 : new_var_name, sortNormalizer.convertType(current.getType()));
517 : :
518 : 0 : boundVar2node[current] = ret;
519 : 0 : normalized[current] = ret;
520 : 0 : normalizedName[std::to_string(current.getId())] = new_var_name;
521 : 0 : }
522 : : }
523 : : else
524 : : {
525 : 8 : auto it_fv = freeVar2node.find(current);
526 [ + + ]: 8 : if (it_fv != freeVar2node.end())
527 : : {
528 : 2 : normalized[current] = it_fv->second;
529 : : }
530 : : else
531 : : {
532 : 6 : std::vector<Node> cnodes;
533 : 6 : size_t id = globalVarCounter++;
534 : : std::string new_var_name = "v"
535 : 12 : + std::string(8 - numDigits(id), '0')
536 : 12 : + std::to_string(id);
537 : : // Create substitution variable with original type for
538 : : // substitution
539 : : Node substVar = nodeManager->getSkolemManager()->mkDummySkolem(
540 : : new_var_name,
541 : 6 : current.getType(),
542 : 12 : SkolemFlags::SKOLEM_EXACT_NAME);
543 : :
544 : : // Create normalized variable with normalized type for the final
545 : : // result
546 : : Node ret = nodeManager->getSkolemManager()->mkDummySkolem(
547 : : new_var_name,
548 : 12 : sortNormalizer.convertType(current.getType()),
549 : 12 : SkolemFlags::SKOLEM_EXACT_NAME);
550 : :
551 : 6 : freeVar2node[current] = ret;
552 : 6 : normalized[current] = ret;
553 : 6 : d_preprocContext->addSubstitution(current, substVar);
554 : 6 : normalizedName[std::to_string(current.getId())] = new_var_name;
555 : 6 : }
556 : : }
557 : : }
558 : : else
559 : : {
560 : : // Constants are unchanged
561 : 8 : normalized[current] = current;
562 : : }
563 : :
564 : : // Mark as processed and pop from the stack
565 : 16 : it->second = true;
566 : 16 : stack.pop_back();
567 : : }
568 : : else
569 : : {
570 : : // Non-const, non-var node
571 : :
572 : 24 : if (!hasQID
573 [ + - ][ - + ]: 12 : && current.getKind() == cvc5::internal::Kind::INST_ATTRIBUTE)
[ - + ]
574 : : {
575 [ - - ]: 0 : for (const Node& child : current)
576 : : {
577 [ - - ]: 0 : if (child.isVar())
578 : : {
579 : 0 : hasQID = true;
580 : 0 : break; // Found at least one qid, no need to check further
581 : : }
582 [ - - ]: 0 : }
583 : : }
584 : :
585 : : // For quantifiers, process bound variables immediately
586 : 12 : if (current.getKind() == cvc5::internal::Kind::FORALL
587 [ + - ][ - + ]: 12 : || current.getKind() == cvc5::internal::Kind::EXISTS)
[ - + ]
588 : : {
589 : 0 : Node bound_vars = current[0];
590 : :
591 : : // Normalize bound variables and update boundVar2node
592 : 0 : std::vector<Node> normalizedBoundVars;
593 [ - - ]: 0 : for (const Node& bv : bound_vars)
594 : : {
595 : 0 : auto it_bv = boundVar2node.find(bv);
596 [ - - ]: 0 : if (it_bv != boundVar2node.end())
597 : : {
598 : 0 : normalized[bv] = it_bv->second;
599 : : }
600 : : else
601 : : {
602 : 0 : size_t id = boundVarCounter++;
603 : : std::string new_var_name = "u"
604 : 0 : + std::string(8 - numDigits(id), '0')
605 : 0 : + std::to_string(id);
606 : :
607 : : Node ret = nodeManager->mkBoundVar(
608 : 0 : new_var_name, sortNormalizer.convertType(bv.getType()));
609 : 0 : boundVar2node[bv] = ret;
610 : 0 : normalized[bv] = ret;
611 : 0 : }
612 : 0 : normalizedBoundVars.push_back(normalized[bv]);
613 : 0 : }
614 : :
615 : : Node normalizedBoundVarList = nodeManager->mkNode(
616 : 0 : cvc5::internal::Kind::BOUND_VAR_LIST, normalizedBoundVars);
617 : 0 : normalized[bound_vars] = normalizedBoundVarList;
618 : 0 : }
619 : :
620 : : // Push unvisited children onto the stack
621 [ + + ]: 36 : for (int i = current.getNumChildren() - 1; i >= 0; --i)
622 : : {
623 : 24 : const Node& child = current[i];
624 [ + - ]: 24 : if (visited.find(child) == visited.end())
625 : : {
626 : 24 : stack.push_back(child);
627 : : }
628 : 24 : }
629 : :
630 : : // For APPLY_UF nodes, push the operator
631 [ - + ]: 12 : if (current.getKind() == cvc5::internal::Kind::APPLY_UF)
632 : : {
633 : 0 : Node op = current.getOperator();
634 [ - - ]: 0 : if (visited.find(op) == visited.end())
635 : : {
636 : 0 : stack.push_back(op);
637 : : }
638 : 0 : }
639 : :
640 : : // Leave 'it->second' as false; we'll process this node later
641 : : }
642 : : }
643 [ + - ]: 12 : else if (!it->second)
644 : : {
645 : : // Second time seeing this node, process it after its children
646 : :
647 : 12 : std::vector<Node> children;
648 : :
649 [ - + ]: 12 : if (current.getKind() == cvc5::internal::Kind::APPLY_UF)
650 : : {
651 : : // Handle operator for APPLY_UF nodes
652 : 0 : auto opIt = normalized.find(current.getOperator());
653 : 0 : Assert(opIt != normalized.end());
654 : 0 : children.push_back(opIt->second);
655 : : }
656 [ - + ]: 12 : else if (current.getMetaKind() == metakind::PARAMETERIZED)
657 : : {
658 : : // For parameterized nodes, include the operator
659 : 0 : children.push_back(current.getOperator());
660 : : }
661 : :
662 [ + + ]: 36 : for (const Node& child : current)
663 : : {
664 : 24 : auto childIt = normalized.find(child);
665 [ - + ][ - + ]: 24 : Assert(childIt != normalized.end());
[ - - ]
666 : 24 : children.push_back(childIt->second);
667 : 24 : }
668 : :
669 : 12 : Node ret = nodeManager->mkNode(current.getKind(), children);
670 : 12 : normalized[current] = ret;
671 : :
672 : : // Mark as processed and pop from the stack
673 : 12 : it->second = true;
674 : 12 : stack.pop_back();
675 : 12 : }
676 : : else
677 : : {
678 : : // Node has already been processed
679 : 0 : stack.pop_back();
680 : : }
681 : 40 : }
682 : :
683 : 8 : return normalized[n];
684 : 4 : }
685 : :
686 : : /**
687 : : * Checks if a node represents a trivial equality (e.g., x = x).
688 : : *
689 : : * @param n The node to check.
690 : : * @return True if the node is a trivial equality, false otherwise.
691 : : */
692 : 6 : bool isTrivialEquality(const Node& n)
693 : : {
694 [ - + ]: 6 : if (n.getKind() == cvc5::internal::Kind::EQUAL)
695 : : {
696 : 0 : const auto &lhs = n[0], rhs = n[1];
697 [ - - ]: 0 : if (lhs == rhs)
698 : : {
699 : 0 : return true;
700 : : }
701 [ - - ][ - - ]: 0 : }
702 : 6 : return false;
703 : : }
704 : :
705 : : /**
706 : : * Checks if a node represents the constant true.
707 : : *
708 : : * @param n The node to check.
709 : : * @return True if the node is the constant true, false otherwise.
710 : : */
711 : 6 : bool isTrue(const Node& n)
712 : : {
713 [ + + ][ + - ]: 6 : if (n.isConst() && n.getType().isBoolean())
[ + + ][ + + ]
[ - - ]
714 : : {
715 : 2 : return n.getConst<bool>();
716 : : }
717 : 4 : return false;
718 : : }
719 : :
720 : : /**
721 : : * Collects all unique types present in a node's subtree.
722 : : *
723 : : * @param n The root node of the subtree.
724 : : * @param types Vector to store the collected types.
725 : : * @param visited Set to track visited nodes.
726 : : * @param mark Set to track collected types.
727 : : */
728 : 4 : void collectTypes(TNode n,
729 : : std::vector<TypeNode>& types,
730 : : std::unordered_set<TNode>& visited,
731 : : std::unordered_set<TypeNode>& mark)
732 : : {
733 : 4 : std::unordered_set<TNode>::iterator it;
734 : 4 : std::vector<TNode> visit;
735 : 4 : TNode cur;
736 : 4 : visit.push_back(n);
737 : : do
738 : : {
739 : 28 : cur = visit.back();
740 : 28 : visit.pop_back();
741 : 28 : it = visited.find(cur);
742 [ + + ]: 28 : if (it == visited.end())
743 : : {
744 : 22 : visited.insert(cur);
745 : :
746 [ + + ]: 22 : if (mark.find(cur.getType()) == mark.end())
747 : : {
748 : 4 : mark.insert(cur.getType());
749 : 4 : types.push_back(cur.getType());
750 : : }
751 : :
752 : : // special cases where the type is not part of the AST
753 [ - + ]: 22 : if (cur.getKind() == Kind::CARDINALITY_CONSTRAINT)
754 : : {
755 : 0 : if (mark.find(
756 : 0 : cur.getOperator().getConst<CardinalityConstraint>().getType())
757 [ - - ]: 0 : == mark.end())
758 : : {
759 : 0 : mark.insert(
760 : 0 : cur.getOperator().getConst<CardinalityConstraint>().getType());
761 : 0 : types.push_back(
762 : 0 : cur.getOperator().getConst<CardinalityConstraint>().getType());
763 : : }
764 : : }
765 : 22 : visit.insert(visit.end(), cur.begin(), cur.end());
766 : : }
767 [ + + ]: 28 : } while (!visit.empty());
768 : 4 : }
769 : :
770 : : /**
771 : : * Renames quantifier IDs (QIDs) in a node to ensure consistent naming.
772 : : *
773 : : * @param n The node to rename.
774 : : * @param qidRenamed Map for storing renamed QIDs.
775 : : * @param normalizedName Map for storing normalized QID names.
776 : : * @param nodeManager The node manager for creating new nodes.
777 : : * @return The renamed node.
778 : : */
779 : 0 : Node renameQid(const Node& n,
780 : : std::unordered_map<Node, Node>& qidRenamed,
781 : : std::unordered_map<std::string, std::string>& normalizedName,
782 : : NodeManager* nodeManager)
783 : : {
784 : : // Map to cache normalized nodes.
785 : 0 : std::unordered_map<Node, Node> normalized;
786 : : // Map to track visited nodes (false: first visit; true: processed).
787 : 0 : std::unordered_map<Node, bool> visited;
788 : : // Stack for iterative traversal.
789 : : // Each element is a pair: (current node, its parent).
790 : 0 : std::vector<std::pair<Node, Node>> stack;
791 : : // Global counter for qid renaming (starting at 1).
792 : : static size_t qidCounter = 1;
793 : :
794 : : // Push the root node with a null parent.
795 : 0 : stack.push_back({n, Node()});
796 : :
797 [ - - ]: 0 : while (!stack.empty())
798 : : {
799 : : // Get current node and its parent.
800 : 0 : auto [current, parent] = stack.back();
801 : :
802 : : // Try inserting current node into visited.
803 : 0 : auto [it, inserted] = visited.emplace(current, false);
804 [ - - ]: 0 : if (inserted)
805 : : {
806 : : // First time seeing this node.
807 : 0 : if (current.isConst() || current.isVar())
808 : : {
809 : : // Check if current is a variable and qualifies as a qid.
810 : : // A qid is defined as a variable whose parent has kind INST_ATTRIBUTE.
811 : 0 : if (current.isVar()
812 : 0 : && (!parent.isNull()
813 [ - - ]: 0 : && parent.getKind() == cvc5::internal::Kind::INST_ATTRIBUTE))
814 : : {
815 : : // If we already renamed this variable, use that renaming.
816 : 0 : auto it_qid = qidRenamed.find(current);
817 [ - - ]: 0 : if (it_qid != qidRenamed.end())
818 : : {
819 : 0 : normalized[current] = it_qid->second;
820 : : }
821 : : else
822 : : {
823 : : // Otherwise, generate a new name "q00000001", "q00000002", etc.
824 : : std::string new_var_name =
825 : 0 : "q" + std::string(8 - numDigits(qidCounter), '0')
826 : 0 : + std::to_string(qidCounter);
827 : 0 : qidCounter++;
828 : :
829 : : // Create a new dummy skolem (or qid variable) with the new name.
830 : : Node ret = nodeManager->getSkolemManager()->mkDummySkolem(
831 : : new_var_name,
832 : 0 : current.getType(),
833 : 0 : SkolemFlags::SKOLEM_EXACT_NAME);
834 : 0 : qidRenamed[current] = ret;
835 : 0 : normalized[current] = ret;
836 : 0 : normalizedName[std::to_string(current.getId())] = new_var_name;
837 : 0 : }
838 : : }
839 : : else
840 : : {
841 : : // Otherwise, leave the node unchanged.
842 : 0 : normalized[current] = current;
843 : : }
844 : : // Mark this node as processed.
845 : 0 : visited[current] = true;
846 : 0 : stack.pop_back();
847 : : }
848 : : else
849 : : {
850 : : // For non-const and non-var nodes, push their children (with current as
851 : : // parent) in reverse order to preserve left-to-right traversal.
852 [ - - ]: 0 : for (int i = current.getNumChildren() - 1; i >= 0; --i)
853 : : {
854 : 0 : Node child = current[i];
855 : 0 : stack.push_back({child, current});
856 : 0 : }
857 : : // For APPLY_UF nodes, push the operator.
858 [ - - ]: 0 : if (current.getKind() == cvc5::internal::Kind::APPLY_UF)
859 : : {
860 : 0 : Node op = current.getOperator();
861 : 0 : stack.push_back({op, current});
862 : 0 : }
863 : : // Leave the node for a second visit.
864 : : }
865 : : }
866 [ - - ]: 0 : else if (!it->second)
867 : : {
868 : : // Second time visiting the node: all its children have been processed.
869 : 0 : std::vector<Node> children;
870 [ - - ]: 0 : if (current.getKind() == cvc5::internal::Kind::APPLY_UF)
871 : : {
872 : : // Add the normalized operator.
873 : 0 : auto opIt = normalized.find(current.getOperator());
874 : 0 : Assert(opIt != normalized.end());
875 : 0 : children.push_back(opIt->second);
876 : : }
877 [ - - ]: 0 : else if (current.getMetaKind() == metakind::PARAMETERIZED)
878 : : {
879 : : // For parameterized nodes, include the operator.
880 : 0 : children.push_back(current.getOperator());
881 : : }
882 : : // Add normalized children.
883 [ - - ]: 0 : for (const Node& child : current)
884 : : {
885 : 0 : auto childIt = normalized.find(child);
886 : 0 : Assert(childIt != normalized.end());
887 : 0 : children.push_back(childIt->second);
888 : 0 : }
889 : : // Reconstruct the node with its normalized children.
890 : 0 : Node ret = nodeManager->mkNode(current.getKind(), children);
891 : 0 : normalized[current] = ret;
892 : 0 : visited[current] = true;
893 : 0 : stack.pop_back();
894 : 0 : }
895 : : else
896 : : {
897 : : // Node already processed.
898 : 0 : stack.pop_back();
899 : : }
900 : 0 : }
901 : :
902 : 0 : return normalized[n];
903 : 0 : }
904 : :
905 : 2 : PreprocessingPassResult Normalize::applyInternal(
906 : : AssertionPipeline* assertionsToPreprocess)
907 : : {
908 : 2 : TimerStat::CodeTimer codeTimer(d_statistics.d_passTime);
909 : :
910 : : // ----------------------------------------
911 : : // Step 1: Collect NodeInfo for all assertions
912 : : // ----------------------------------------
913 : 2 : std::vector<std::shared_ptr<NodeInfo>> nodeInfos;
914 [ + + ]: 8 : for (const Node& assertion : assertionsToPreprocess->ref())
915 : : {
916 [ + - ][ + + ]: 6 : if (isTrivialEquality(assertion) || isTrue(assertion))
[ + + ]
917 : : {
918 : 2 : continue;
919 : : }
920 : 4 : auto ni = getNodeInfo(assertion);
921 : 4 : nodeInfos.push_back(std::move(ni));
922 : 4 : }
923 : :
924 : : // ----------------------------------------
925 : : // Step 2: Store symbol occurrences for super-pattern computation
926 : : // ----------------------------------------
927 : : std::unordered_map<std::string, std::vector<std::shared_ptr<NodeInfo>>>
928 : 2 : symbolOccurrences;
929 [ + + ]: 6 : for (const auto& nodeInfo : nodeInfos)
930 : : {
931 [ + + ]: 12 : for (const auto& varName : nodeInfo->varNames)
932 : : {
933 : 8 : symbolOccurrences[varName.first].push_back(nodeInfo);
934 : : }
935 : : }
936 : :
937 : : // ----------------------------------------
938 : : // Step 3: Classify assertions into equivalence classes
939 : : // ----------------------------------------
940 : 2 : std::vector<std::vector<NodeInfo*>> eqClasses;
941 : 2 : std::unordered_map<std::string, size_t> seenEncodings;
942 [ + + ]: 6 : for (auto& niPtr : nodeInfos)
943 : : {
944 : 4 : NodeInfo* current = niPtr.get();
945 : 4 : auto it = seenEncodings.find(current->encoding);
946 [ + + ]: 4 : if (it != seenEncodings.end())
947 : : {
948 : 2 : eqClasses[it->second].push_back(current);
949 : : }
950 : : else
951 : : {
952 : 2 : seenEncodings[current->encoding] = eqClasses.size();
953 : 2 : std::vector<NodeInfo*> newClass;
954 : 2 : newClass.push_back(current);
955 : 2 : eqClasses.push_back(std::move(newClass));
956 : 2 : }
957 : : }
958 : :
959 : : // ----------------------------------------
960 : : // Step 4: Sort equivalence classes based on encodings
961 : : // ----------------------------------------
962 : 2 : std::sort(
963 : : eqClasses.begin(),
964 : : eqClasses.end(),
965 : 0 : [](const std::vector<NodeInfo*>& a, const std::vector<NodeInfo*>& b) {
966 : : // Silence false positive:
967 : : // https://github.com/llvm/llvm-project/issues/78132
968 : : // NOLINTNEXTLINE(clang-analyzer-cplusplus.Move)
969 : 0 : return a[0]->encoding > b[0]->encoding;
970 : : });
971 : :
972 : : // Assign IDs to equivalence classes for super-pattern computation
973 : 2 : size_t idCnt = 0;
974 [ + + ]: 4 : for (const auto& eqClass : eqClasses)
975 : : {
976 [ + + ]: 6 : for (const auto& ni : eqClass)
977 : : {
978 : 4 : ni->setId(idCnt);
979 : : }
980 : 2 : idCnt++;
981 : : }
982 : : // ----------------------------------------
983 : : // Step 5: Sort within equivalence classes
984 : : // ----------------------------------------
985 : : std::unordered_map<std::string, std::vector<std::vector<int32_t>>>
986 : 2 : patternCache;
987 [ + + ]: 4 : for (auto& eqClass : eqClasses)
988 : : {
989 : 2 : std::sort(eqClass.begin(), eqClass.end(), [&](NodeInfo* a, NodeInfo* b) {
990 : 4 : return compareBySuperpattern(
991 : 2 : a, b, eqClasses, patternCache, symbolOccurrences);
992 : : });
993 : : }
994 : :
995 : : // ----------------------------------------
996 : : // Step 6: Collect and normalize types
997 : : // ----------------------------------------
998 : 2 : std::vector<TypeNode> types;
999 : 2 : std::unordered_set<TNode> visited;
1000 : 2 : std::unordered_set<TypeNode> mark;
1001 [ + + ]: 4 : for (const std::vector<NodeInfo*>& eqClass : eqClasses)
1002 : : {
1003 [ + + ]: 6 : for (NodeInfo* nodeInfo : eqClass)
1004 : : {
1005 : 4 : collectTypes(nodeInfo->node, types, visited, mark);
1006 : : }
1007 : : }
1008 : :
1009 : 2 : std::unordered_map<TypeNode, TypeNode> normalizedSorts;
1010 : 2 : int sortCounter = 0;
1011 [ + + ]: 6 : for (const TypeNode& ctn : types)
1012 : : {
1013 [ - + ][ - - ]: 4 : if (ctn.isUninterpretedSort() && ctn.getNumChildren() == 0)
[ - + ]
1014 : : {
1015 : : std::string new_sort_name = "S"
1016 : 0 : + std::string(8 - numDigits(sortCounter), '0')
1017 : 0 : + std::to_string(sortCounter);
1018 : 0 : sortCounter++;
1019 : 0 : TypeNode new_sort = nodeManager()->mkSort(new_sort_name);
1020 : 0 : normalizedSorts[ctn] = new_sort;
1021 : 0 : }
1022 : : }
1023 : :
1024 : 2 : NormalizeSortNodeConverter sortNormalizer(normalizedSorts, nodeManager());
1025 : :
1026 : : // ----------------------------------------
1027 : : // Step 7: Normalize nodes based on sorted order
1028 : : // ----------------------------------------
1029 : 2 : std::unordered_map<Node, Node> freeVar2node;
1030 : 2 : std::unordered_map<Node, Node> boundVar2node;
1031 : 2 : std::unordered_map<std::string, std::string> normalizedName;
1032 : :
1033 : 2 : bool hasQID = false;
1034 [ + + ]: 4 : for (const auto& eqClass : eqClasses)
1035 : : {
1036 [ + + ]: 6 : for (const auto& ni : eqClass)
1037 : : {
1038 : 4 : Node renamed = rename(ni->node,
1039 : : freeVar2node,
1040 : : boundVar2node,
1041 : : normalizedName,
1042 : : nodeManager(),
1043 : : d_preprocContext,
1044 : : sortNormalizer,
1045 : 4 : hasQID);
1046 : 4 : ni->node = renamed;
1047 : 4 : }
1048 : : }
1049 : :
1050 : : // ----------------------------------------
1051 : : // Step 8: Sort nodes within equivalence classes based on normalized names
1052 : : // ----------------------------------------
1053 [ + + ]: 4 : for (auto& eqClass : eqClasses)
1054 : : {
1055 : 2 : std::sort(eqClass.begin(), eqClass.end(), [&](NodeInfo* a, NodeInfo* b) {
1056 : 4 : return compareByNormalizedNames(a, b, normalizedName);
1057 : : });
1058 : : }
1059 : :
1060 : : // ----------------------------------------
1061 : : // Step 9: Reassign qid top to bottom
1062 : : // ----------------------------------------
1063 : 2 : std::unordered_map<Node, Node> qidRenamed;
1064 [ - + ]: 2 : if (hasQID)
1065 : : {
1066 [ - - ]: 0 : for (const auto& eqClass : eqClasses)
1067 : : {
1068 [ - - ]: 0 : for (const auto& ni : eqClass)
1069 : : {
1070 : : Node renamed =
1071 : 0 : renameQid(ni->node, qidRenamed, normalizedName, nodeManager());
1072 : 0 : ni->node = renamed;
1073 : 0 : }
1074 : : }
1075 : : }
1076 : :
1077 : : // ----------------------------------------
1078 : : // Step 10: Replace assertions with normalized versions
1079 : : // ----------------------------------------
1080 : 2 : size_t idx = 0;
1081 [ + + ]: 4 : for (const auto& eqClass : eqClasses)
1082 : : {
1083 [ + + ]: 6 : for (const auto& ni : eqClass)
1084 : : {
1085 : 4 : assertionsToPreprocess->replace(idx++, ni->node);
1086 : : }
1087 : : }
1088 : 2 : assertionsToPreprocess->resize(idx);
1089 : :
1090 : 2 : return PreprocessingPassResult::NO_CONFLICT;
1091 : 2 : }
1092 : :
1093 : 52018 : Normalize::Statistics::Statistics(StatisticsRegistry& reg)
1094 : 52018 : : d_passTime(reg.registerTimer("Normalize::pass_time"))
1095 : : {
1096 : 52018 : }
1097 : :
1098 : : } // namespace passes
1099 : : } // namespace preprocessing
1100 : : } // namespace cvc5::internal
|
