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 : : * PartitionGenerator for creating partitions.
11 : : */
12 : :
13 : : #include "theory/partition_generator.h"
14 : :
15 : : #include <math.h>
16 : :
17 : : #include <algorithm>
18 : : #include <random>
19 : :
20 : : #include "expr/node_algorithm.h"
21 : : #include "expr/node_builder.h"
22 : : #include "options/parallel_options.h"
23 : : #include "prop/prop_engine.h"
24 : : #include "prop/theory_proxy.h"
25 : : #include "prop/zero_level_learner.h"
26 : : #include "theory/theory_engine.h"
27 : : #include "theory/theory_id.h"
28 : : #include "theory/theory_traits.h"
29 : :
30 : : using namespace std;
31 : :
32 : : namespace cvc5::internal {
33 : :
34 : : namespace theory {
35 : 0 : PartitionGenerator::PartitionGenerator(Env& env,
36 : : TheoryEngine* theoryEngine,
37 : 0 : prop::PropEngine* propEngine)
38 : : : TheoryEngineModule(env, theoryEngine, "PartitionGenerator"),
39 : 0 : d_numPartitions(options().parallel.computePartitions),
40 : 0 : d_numChecks(0),
41 : 0 : d_betweenChecks(0),
42 : 0 : d_numPartitionsSoFar(0),
43 : 0 : d_createdAnyPartitions(false),
44 : 0 : d_emittedAllPartitions(false)
45 : : {
46 : 0 : d_startTime = std::chrono::steady_clock::now();
47 : 0 : d_startTimeOfPreviousPartition = std::chrono::steady_clock::now();
48 : 0 : d_valuation = std::make_unique<Valuation>(theoryEngine);
49 : 0 : d_propEngine = propEngine;
50 : :
51 : 0 : d_conflictSize = options().parallel.partitionConflictSize;
52 [ - - ]: 0 : if (!d_conflictSize)
53 : : {
54 : 0 : d_conflictSize = static_cast<uint64_t>(log2(d_numPartitions));
55 : : }
56 : 0 : }
57 : :
58 : 0 : void PartitionGenerator::incrementOrInsertLemmaAtom(Node& node)
59 : : {
60 [ - - ]: 0 : if (d_lemmaMap.count(node) == 0)
61 : : {
62 : 0 : d_lemmaMap.insert({node, 1});
63 : 0 : d_lemmaLiterals.insert(node);
64 : : }
65 : : else
66 : : {
67 : 0 : int new_count = d_lemmaMap[node] + 1;
68 : 0 : d_lemmaMap.erase(node);
69 : 0 : d_lemmaMap.insert({node, new_count});
70 : : }
71 : 0 : }
72 : :
73 : 0 : void PartitionGenerator::notifyLemma(
74 : : TNode n,
75 : : CVC5_UNUSED InferenceId id,
76 : : CVC5_UNUSED LemmaProperty p,
77 : : CVC5_UNUSED const std::vector<Node>& skAsserts,
78 : : CVC5_UNUSED const std::vector<Node>& sks)
79 : : {
80 : 0 : if (options().parallel.partitionStrategy == options::PartitionMode::LEMMA_CUBE
81 [ - - ][ - - ]: 0 : || options().parallel.partitionStrategy
[ - - ]
82 : : == options::PartitionMode::LEMMA_SCATTER)
83 : : {
84 : 0 : std::vector<Node> toVisit;
85 : 0 : toVisit.push_back(n);
86 : :
87 [ - - ]: 0 : for (unsigned i = 0; i < toVisit.size(); ++i)
88 : : {
89 : 0 : Node current = toVisit[i];
90 : : // If current node is theory bool, visit the children.
91 [ - - ]: 0 : if (Theory::theoryOf(current) == THEORY_BOOL)
92 : : {
93 : 0 : for (unsigned child = 0, childEnd = current.getNumChildren();
94 [ - - ]: 0 : child < childEnd;
95 : : ++child)
96 : : {
97 : 0 : auto childNode = current[child];
98 : : // If we haven't seen the child, we should visit it.
99 [ - - ]: 0 : if (d_lemmaMap.count(childNode) == 0)
100 : : {
101 : 0 : toVisit.push_back(childNode);
102 : : }
103 : : else
104 : : {
105 : : // If we have already seen this chld node, then it is not theory
106 : : // bool, so we update its entry. No need to visit again.
107 : 0 : incrementOrInsertLemmaAtom(childNode);
108 : : }
109 : 0 : }
110 : : }
111 : : else
112 : : {
113 : 0 : incrementOrInsertLemmaAtom(current);
114 : : }
115 : 0 : }
116 : 0 : }
117 : 0 : }
118 : :
119 : : // Some of this function may be redundant, but I was trying to be
120 : : // complete.
121 : 0 : bool PartitionGenerator::isUnusable(Node n)
122 : : {
123 : : const std::unordered_set<Kind, kind::KindHashFunction> unusableKinds = {
124 : 0 : Kind::INST_CONSTANT, Kind::SKOLEM};
125 : :
126 : : // Check if n is constant or contains unusable kinds.
127 [ - - ]: 0 : if (n.isConst())
128 : : {
129 : 0 : return true;
130 : : }
131 : :
132 : : // Check if original has unusable kinds or contains skolems.
133 : 0 : Node originalN = SkolemManager::getOriginalForm(n);
134 [ - - ]: 0 : if (expr::hasSubtermKinds(unusableKinds, originalN))
135 : : {
136 : 0 : return true;
137 : : }
138 : :
139 : : // Get non negated versions before testing for bool expr.
140 : : Node nonNegatedOriginal =
141 [ - - ]: 0 : originalN.getKind() == Kind::NOT ? originalN[0] : originalN;
142 : :
143 : : // Check if this is a boolean expression
144 [ - - ]: 0 : if (Theory::theoryOf(nonNegatedOriginal) == THEORY_BOOL)
145 : : {
146 : 0 : return true;
147 : : }
148 : :
149 : 0 : return false;
150 : 0 : }
151 : :
152 : 0 : std::vector<Node> PartitionGenerator::collectLiterals(LiteralListType litType)
153 : : {
154 : 0 : std::vector<Node> filteredLiterals;
155 : 0 : std::vector<Node> unfilteredLiterals;
156 : :
157 [ - - ][ - - ]: 0 : switch (litType)
[ - ]
158 : : {
159 : 0 : case DECISION:
160 : : {
161 : 0 : unfilteredLiterals = d_propEngine->getPropDecisions();
162 : 0 : break;
163 : : }
164 : 0 : case HEAP:
165 : : {
166 : 0 : unfilteredLiterals = d_propEngine->getPropOrderHeap();
167 : 0 : break;
168 : : }
169 : 0 : case LEMMA:
170 : : {
171 : : std::vector<Node> lemmaNodes(d_lemmaLiterals.begin(),
172 : 0 : d_lemmaLiterals.end());
173 : 0 : unfilteredLiterals = lemmaNodes;
174 : 0 : break;
175 : 0 : }
176 : 0 : case ZLL:
177 : : {
178 : 0 : unfilteredLiterals = d_propEngine->getLearnedZeroLevelLiterals(
179 : 0 : modes::LearnedLitType::INPUT);
180 : 0 : break;
181 : : }
182 : 0 : default: return filteredLiterals;
183 : : }
184 : :
185 [ - - ]: 0 : if (litType == LEMMA)
186 : : {
187 : : // Sort by frequency of the literal.
188 : 0 : std::sort(unfilteredLiterals.begin(),
189 : : unfilteredLiterals.end(),
190 : 0 : [this](Node a, Node b) -> bool {
191 : 0 : return d_lemmaMap[a] > d_lemmaMap[b];
192 : : });
193 : : }
194 : :
195 : : // These checks may be unnecessary for ZLL.
196 [ - - ]: 0 : for (const Node& n : unfilteredLiterals)
197 : : {
198 [ - - ][ - - ]: 0 : if (isUnusable(n)
199 : 0 : || (litType == LEMMA && d_usedLemmaLiterals.count(n) != 0))
200 : : {
201 : 0 : continue;
202 : : }
203 : 0 : filteredLiterals.push_back(SkolemManager::getOriginalForm(n));
204 : : }
205 : :
206 : 0 : return filteredLiterals;
207 : 0 : }
208 : :
209 : 0 : void PartitionGenerator::emitPartition(Node toEmit)
210 : : {
211 : 0 : *options().parallel.partitionsOut << toEmit << std::endl;
212 : 0 : ++d_numPartitionsSoFar;
213 : 0 : d_createdAnyPartitions = true;
214 : 0 : }
215 : :
216 : 0 : Node PartitionGenerator::blockPath(TNode toBlock)
217 : : {
218 : : // Now block the path in the search.
219 : 0 : Node lemma = toBlock.notNode();
220 : 0 : d_assertedLemmas.push_back(lemma);
221 : 0 : return lemma;
222 : 0 : }
223 : :
224 : : // Send lemma that is the negation of all previously asserted lemmas.
225 : 0 : Node PartitionGenerator::stopPartitioning()
226 : : {
227 : 0 : d_emittedAllPartitions = true;
228 : 0 : return nodeManager()->mkConst(false);
229 : : }
230 : :
231 : : // For the scatter strategy, we make the following kinds of partitions:
232 : : // P1 = C1 = l1_{1} & ... & l1_{d_conflictSize}
233 : : // P2 = !C1 & C2 = l2_{1} & ... & l2_{d_conflictSize}
234 : : // P3 = !C1 & !C2 & C3 = l3_{1} & ... & l3_{d_conflictSize}
235 : : // P4 = !C1 & !C2 & !C3
236 : : // Note that we want to simply collect the partitions until we get to the
237 : : // timeout or total number of requested partitions.
238 : : // Once we reach that point, we dump all the partitions.
239 : 0 : Node PartitionGenerator::makeScatterPartitions(LiteralListType litType,
240 : : bool timedOut,
241 : : bool randomize)
242 : : {
243 : : // If we're not at the last cube
244 [ - - ]: 0 : if (d_numPartitionsSoFar < d_numPartitions - 1)
245 : : {
246 : 0 : std::vector<Node> literals = collectLiterals(litType);
247 : :
248 : : // Make sure we have enough literals.
249 : : // Conflict size can be set through options, but the default is log base
250 : : // 2 of the requested number of partitions.
251 [ - - ]: 0 : if (literals.size() < d_conflictSize)
252 : : {
253 : 0 : return Node::null();
254 : : }
255 : :
256 [ - - ]: 0 : if (randomize)
257 : : {
258 : 0 : std::shuffle(literals.begin(),
259 : : literals.end(),
260 : 0 : std::mt19937(std::random_device()()));
261 : : }
262 : :
263 : 0 : literals.resize(d_conflictSize);
264 : :
265 : : // Add literals to the seen list if we are using lemmas
266 [ - - ]: 0 : if (litType == LEMMA)
267 : : {
268 [ - - ]: 0 : for (auto l : literals)
269 : : {
270 : 0 : d_usedLemmaLiterals.insert(l);
271 : 0 : }
272 : : }
273 : :
274 : : // Make a cube from the literals
275 : 0 : Node conj = nodeManager()->mkAnd(literals);
276 : :
277 : : // For the scatter strategy, partitions look like the following:
278 : : // P1 = C1 = l1_{1} & .... & l1_{d_conflictSize}
279 : : // P2 = !C1 & C2 = l2_{1} & .... & l2_{d_conflictSize}
280 : : // P3 = !C1 & !C2 & C3 = l3_{1} & .... & l3_{d_conflictSize}
281 : : // P4 = !C1 & !C2 & !C3
282 : 0 : vector<Node> toEmit;
283 : :
284 : : // Collect negation of the previously used cubes.
285 [ - - ]: 0 : for (const Node& c : d_cubes)
286 : : {
287 : 0 : toEmit.push_back(c.notNode());
288 : : }
289 : :
290 : : // Add the conjunction to the list of cubesThis needs to happen after
291 : : // collecting the negations of the previously used cubes.
292 : 0 : d_cubes.push_back(conj);
293 : :
294 : : // Add the current cube.
295 : 0 : toEmit.push_back(conj);
296 : :
297 : : // Now make the scatter partition and add it to the list of partitions.
298 : 0 : Node scatterPartition = nodeManager()->mkAnd(toEmit);
299 : 0 : d_scatterPartitions.push_back(scatterPartition);
300 : :
301 : : // Just increment and don't actually output the partition yet
302 : 0 : d_numPartitionsSoFar++;
303 : :
304 : : // Track that we have created at least one partition
305 : 0 : d_createdAnyPartitions = true;
306 : :
307 [ - - ]: 0 : if (timedOut)
308 : : {
309 : 0 : emitRemainingPartitions(/*solved=*/false);
310 : 0 : return stopPartitioning();
311 : : }
312 : :
313 : 0 : return blockPath(conj);
314 : 0 : }
315 : :
316 : : // Otherwise, we are at the last partition, and we should emit all
317 : : // partitions now.
318 : 0 : emitRemainingPartitions(/*solved=*/false);
319 : 0 : return stopPartitioning();
320 : : }
321 : :
322 : 0 : Node PartitionGenerator::makeCubePartitions(LiteralListType litType,
323 : : bool emitZLL,
324 : : bool randomize)
325 : : {
326 : 0 : std::vector<Node> literals = collectLiterals(litType);
327 : 0 : uint64_t numVar = static_cast<uint64_t>(log2(d_numPartitions));
328 [ - - ]: 0 : if (literals.size() >= numVar)
329 : : {
330 [ - - ]: 0 : if (randomize)
331 : : {
332 : 0 : std::shuffle(literals.begin(),
333 : : literals.end(),
334 : 0 : std::mt19937(std::random_device()()));
335 : : }
336 : 0 : literals.resize(numVar);
337 : :
338 : : // This complicated thing is basically making a truth table
339 : : // of with 2^numVar variable so that each row can be emitted as a
340 : : // partition later. Each entry in resultNodeLists is a row corresponding
341 : : // to a cube: resultNodeLists = {
342 : : // { l1, l2}
343 : : // { l1, !l2}
344 : : // {!l1, l2}
345 : : // {!l1, !l2} }
346 : :
347 : : // total number of cubes/rows
348 : 0 : size_t total = pow(2, numVar);
349 : :
350 : : // resultNodeLists is built column by column.
351 : 0 : std::vector<std::vector<Node> > resultNodeLists(total);
352 : :
353 : : // t is used to determine whether to push the node or its not_node.
354 : 0 : bool t = false;
355 : :
356 : : // numConsecutiveTF tracks how many times the node should be
357 : : // consectuively true or false in a column.
358 : : // clang-format off
359 : : // For example, if numVar=3:
360 : : // x y z
361 : : // T T T
362 : : // T T F
363 : : // T F T
364 : : // T F F
365 : : // F T T
366 : : // F T F
367 : : // F F T
368 : : // F F F
369 : : // clang-format on
370 : : // For the first column, numConsecutiveTF = 4, then 2 for the
371 : : // second column, and 1 for the third column.
372 : 0 : size_t numConsecutiveTF = total / 2;
373 [ - - ]: 0 : for (Node n : literals)
374 : : {
375 : 0 : Node not_n = n.notNode();
376 : :
377 : : // loc tracks which row/cube we're on
378 : 0 : size_t loc = 0;
379 [ - - ]: 0 : for (size_t z = 0; z < total / numConsecutiveTF; ++z)
380 : : {
381 : 0 : t = !t;
382 [ - - ]: 0 : for (size_t j = 0; j < numConsecutiveTF; ++j)
383 : : {
384 [ - - ]: 0 : resultNodeLists[loc].push_back(t ? n : not_n);
385 : 0 : ++loc;
386 : : }
387 : : }
388 : :
389 : 0 : numConsecutiveTF = numConsecutiveTF / 2;
390 : 0 : }
391 [ - - ]: 0 : for (const std::vector<Node>& row : resultNodeLists)
392 : : {
393 : 0 : Node conj = nodeManager()->mkAnd(row);
394 [ - - ]: 0 : if (emitZLL)
395 : : {
396 : 0 : std::vector<Node> zllLiterals = collectLiterals(ZLL);
397 : 0 : zllLiterals.push_back(conj);
398 : 0 : Node zllConj = nodeManager()->mkAnd(zllLiterals);
399 : 0 : emitPartition(zllConj);
400 : 0 : }
401 : : else
402 : : {
403 : 0 : emitPartition(conj);
404 : : }
405 : 0 : }
406 : 0 : return stopPartitioning();
407 : 0 : }
408 : 0 : return Node::null();
409 : 0 : }
410 : :
411 : 0 : void PartitionGenerator::emitRemainingPartitions(bool solved)
412 : : {
413 [ - - ]: 0 : if (d_emittedAllPartitions)
414 : : {
415 : 0 : return;
416 : : }
417 : :
418 : 0 : bool emitZLL = options().parallel.appendLearnedLiteralsToCubes;
419 : 0 : std::vector<Node> zllLiterals;
420 : :
421 [ - - ]: 0 : if (emitZLL)
422 : : {
423 : : zllLiterals =
424 : 0 : d_propEngine->getLearnedZeroLevelLiterals(modes::LearnedLitType::INPUT);
425 : : }
426 : :
427 [ - - ]: 0 : for (const auto& partition : d_scatterPartitions)
428 : : {
429 : 0 : Node lemma = partition;
430 : :
431 [ - - ]: 0 : if (emitZLL)
432 : : {
433 : 0 : zllLiterals.push_back(partition);
434 : 0 : lemma = nodeManager()->mkAnd(zllLiterals);
435 : 0 : zllLiterals.pop_back();
436 : : }
437 : :
438 : 0 : emitPartition(lemma);
439 : 0 : }
440 : :
441 : : // If the problem has been solved, then there is no need to emit
442 : : // the final partition because it was solved by the partitioning solver.
443 : : // However, if the problem has not been solved by this solver, then
444 : : // we must emit the final partition.
445 [ - - ]: 0 : if (!solved)
446 : : {
447 : 0 : std::vector<Node> nots;
448 [ - - ]: 0 : for (const Node& cube : d_cubes)
449 : : {
450 : 0 : nots.push_back(cube.notNode());
451 : : }
452 : :
453 : 0 : Node finalPartition = nodeManager()->mkAnd(nots);
454 : :
455 [ - - ]: 0 : if (emitZLL)
456 : : {
457 : 0 : zllLiterals.push_back(finalPartition);
458 : 0 : finalPartition = nodeManager()->mkAnd(zllLiterals);
459 : : }
460 : :
461 : 0 : emitPartition(finalPartition);
462 : 0 : }
463 : 0 : }
464 : :
465 : 0 : void PartitionGenerator::check(Theory::Effort e)
466 : : {
467 : 0 : if ((options().parallel.partitionCheck == options::CheckMode::FULL
468 [ - - ]: 0 : && !Theory::fullEffort(e))
469 : 0 : || (options().parallel.computePartitions < 2))
470 : : {
471 : 0 : return;
472 : : }
473 : :
474 : : // This timing handles when the partitionTimeLimit is set. By default, it is
475 : : // set to 60 seconds. The partitionTimeLimit is used to force the partition
476 : : // generator to finish within a certain number of seconds.
477 : 0 : auto now = std::chrono::steady_clock::now();
478 : 0 : std::chrono::duration<double> totalElapsedTime = now - d_startTime;
479 : : bool timeOutExceeded =
480 : 0 : totalElapsedTime.count() >= options().parallel.partitionTimeLimit;
481 : :
482 : : // This timing code handles the partition timing when the partition-when flag
483 : : // is used to specify that, for example, the first partition should be made
484 : : // after 3 seconds (partition-start-time=3) while the subsequent partitions
485 : : // should be made at 1 second intervals (partition-time-interval=1.0).
486 [ - - ]: 0 : if (options().parallel.partitionWhen == options::PartitionWhenMode::TLIMIT)
487 : : {
488 : : std::chrono::duration<double> interElapsedTime =
489 : 0 : now - d_startTimeOfPreviousPartition;
490 : : bool startTimeExceeded =
491 : 0 : totalElapsedTime.count() >= options().parallel.partitionStartTime;
492 : : bool interTimeExceeded =
493 : 0 : interElapsedTime.count() >= options().parallel.partitionTimeInterval;
494 : :
495 : : // When using time limits, we partition if the partition start time is
496 : : // exceeded and no partitions have been made, or when at least one partition
497 : : // has been created and the inter-partition time limit has been exceeded
498 : 0 : bool timeLimitExceeded =
499 [ - - ]: 0 : ((d_createdAnyPartitions && interTimeExceeded)
500 [ - - ][ - - ]: 0 : || (!d_createdAnyPartitions && startTimeExceeded));
[ - - ]
501 : :
502 [ - - ]: 0 : if (!timeLimitExceeded)
503 : : {
504 : 0 : return;
505 : : }
506 : : // Reset start time of previous partition
507 : 0 : d_startTimeOfPreviousPartition = std::chrono::steady_clock::now();
508 : : }
509 : : else
510 : : {
511 : 0 : d_numChecks = d_numChecks + 1;
512 : 0 : d_betweenChecks = d_betweenChecks + 1;
513 : :
514 : : bool checkLimitExceeded =
515 : 0 : ((d_createdAnyPartitions
516 [ - - ]: 0 : && d_betweenChecks >= options().parallel.checksBetweenPartitions)
517 [ - - ][ - - ]: 0 : || (!d_createdAnyPartitions
518 [ - - ]: 0 : && d_numChecks >= options().parallel.checksBeforePartitioning));
519 [ - - ]: 0 : if (!checkLimitExceeded)
520 : : {
521 : 0 : return;
522 : : }
523 : : // Reset betweenChecks
524 : 0 : d_betweenChecks = 0;
525 : : }
526 : :
527 : 0 : Node lem;
528 : 0 : bool emitZLL = options().parallel.appendLearnedLiteralsToCubes;
529 : 0 : bool randomize = options().parallel.randomPartitioning;
530 : 0 : switch (options().parallel.partitionStrategy)
531 : : {
532 : 0 : case options::PartitionMode::HEAP_CUBE:
533 : 0 : lem = makeCubePartitions(/*litType=*/HEAP, emitZLL, randomize);
534 : 0 : break;
535 : 0 : case options::PartitionMode::DECISION_CUBE:
536 : 0 : lem = makeCubePartitions(/*litType=*/DECISION, emitZLL, randomize);
537 : 0 : break;
538 : 0 : case options::PartitionMode::LEMMA_CUBE:
539 : 0 : lem = makeCubePartitions(/*litType=*/LEMMA, emitZLL, randomize);
540 : 0 : break;
541 : 0 : case options::PartitionMode::HEAP_SCATTER:
542 : 0 : lem = makeScatterPartitions(
543 : 0 : /*litType=*/HEAP, timeOutExceeded, randomize);
544 : 0 : break;
545 : 0 : case options::PartitionMode::DECISION_SCATTER:
546 : 0 : lem = makeScatterPartitions(
547 : 0 : /*litType=*/DECISION, timeOutExceeded, randomize);
548 : 0 : break;
549 : 0 : case options::PartitionMode::LEMMA_SCATTER:
550 : 0 : lem = makeScatterPartitions(
551 : 0 : /*litType=*/LEMMA, timeOutExceeded, randomize);
552 : 0 : break;
553 : 0 : default: return;
554 : : }
555 : : // send the lemma if it exists
556 [ - - ]: 0 : if (!lem.isNull())
557 : : {
558 : 0 : d_out.lemma(lem, InferenceId::PARTITION_GENERATOR_PARTITION);
559 : : }
560 [ - - ]: 0 : }
561 : :
562 : 0 : void PartitionGenerator::postsolve(prop::SatValue result)
563 : : {
564 : : // Handle emitting pending partitions.
565 : : // This can be triggered by a scatter strategy that produces
566 : : // fewer than the requested number of partitions before solving
567 : : // the remainder of the problem.
568 [ - - ]: 0 : if (result != prop::SatValue::SAT_VALUE_TRUE)
569 : : {
570 : 0 : emitRemainingPartitions(/*solved=*/true);
571 : : }
572 : 0 : }
573 : :
574 : : } // namespace theory
575 : : } // namespace cvc5::internal
|
