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