1 2 /* 3 * File InterpolantsNew.cpp. 4 * 5 * This file is part of the source code of the software program 6 * Vampire. It is protected by applicable 7 * copyright laws. 8 * 9 * This source code is distributed under the licence found here 10 * https://vprover.github.io/license.html 11 * and in the source directory 12 * 13 * In summary, you are allowed to use Vampire for non-commercial 14 * purposes but not allowed to distribute, modify, copy, create derivatives, 15 * or use in competitions. 16 * For other uses of Vampire please contact developers for a different 17 * licence, which we will make an effort to provide. 18 */ 19 /** 20 * @file InterpolantsNew.cpp 21 * Implements class InterpolantsNew. 22 * @author Bernhard Gleiss 23 */ 24 25 #include "InterpolantsNew.hpp" 26 27 #include <unordered_set> 28 29 #include "Kernel/Unit.hpp" 30 #include "Kernel/FormulaUnit.hpp" 31 #include "Kernel/Formula.hpp" 32 #include "Kernel/Connective.hpp" 33 #include "Kernel/InferenceStore.hpp" 34 35 #include "Shell/Flattening.hpp" 36 #include "SimplifyFalseTrue.hpp" 37 #include "Shell/NNF.hpp" 38 39 #include "Debug/Assertion.hpp" 40 41 /* 42 * note that formulas are implemented as both formulas (usual formulas) and 43 * clauses (vectors of literals) for efficiency. If we don't care about the 44 * difference (as in this class), we use the class Unit, which wraps around 45 * formulas and clauses, abstracting away the differences. 46 * ======================================================================== 47 * We conceptually think of proofs as DAGS, where the nodes are inferences: 48 * Each such inference i has some premises (n_i=#premises, n_i>=0), a conclusion 49 * and n_i parent inferences. 50 * 51 * Due to performance reasons, a proof nonetheless consists not of inferences, 52 * but of the conclusions of those inferences (and these 53 * conclusions are not formulas but more generally units). 54 * Each such conclusion c (conceptually of an inference inf_c) points to the 55 * conclusions of each parent inference of inf_c. 56 * ======================================================================== 57 * Additionally to the proof-information, we use coloring information, 58 * which is created during parsing: 59 * 1) For each symbol, we can use getColor() to query if that symbol is A-local, 60 * B-local or global (COLOR_LEFT, COLOR_RIGHT or COLOR_TRANSPARENT). 61 * getColor() is also extended in the obvious way to formulas and clauses. 62 * 2) For each input formula, we can use inheritedColor() to query if that 63 * formula is part of the A-formula, part of the B-formula or part of the 64 * theory axioms (COLOR_LEFT, COLOR_RIGHT or COLOR_TRANSPARENT). 65 * For all other formulas, inheritedColor() is set to COLOR_INVALID 66 * ======================================================================== 67 * Note that the word 'splitting' is used with two different meanings in 68 * this class: 1) splitting a proof into an A- and a B- part as described 69 * in the thesis 70 * 2) splitting the proof for Avatar 71 */ 72 73 namespace Shell 74 { 75 using namespace Kernel; 76 77 78 //preprocessing proof 79 removeTheoryInferences(Unit * refutation)80 void InterpolantsNew::removeTheoryInferences(Unit* refutation) 81 { 82 BYPASSING_ALLOCATOR; 83 CALL("InterpolantsNew::removeTheoryInferences"); 84 85 ProofIteratorPostOrder it(refutation); 86 while (it.hasNext()) // traverse the proof in depth-first post order 87 { 88 Unit* current = it.next(); 89 90 // sanity check 91 ASS((!InferenceStore::instance()->getParents(current).hasNext() && ( current->inheritedColor() == COLOR_LEFT 92 || current->inheritedColor() == COLOR_RIGHT 93 || current->inheritedColor() == COLOR_TRANSPARENT 94 )) 95 || (InferenceStore::instance()->getParents(current).hasNext() && current->inheritedColor() == COLOR_INVALID)); 96 97 // compute whether inference has grey and non-grey parent inferences 98 bool hasGreyParents = false; 99 bool hasNonGreyParents = false; 100 101 VirtualIterator<Unit*> parents = InferenceStore::instance()->getParents(current); 102 while (parents.hasNext()) 103 { 104 Unit* premise = parents.next(); 105 if (premise->inheritedColor() == COLOR_TRANSPARENT) 106 { 107 hasGreyParents = true; 108 } 109 else 110 { 111 hasNonGreyParents = true; 112 } 113 } 114 115 // whenever a non-input-inference has only grey parents, color it grey too (needed to compute which inferences are derived only from theory axioms) 116 if (current->inheritedColor() == COLOR_INVALID && !hasNonGreyParents) 117 { 118 current->setInheritedColor(COLOR_TRANSPARENT); 119 } 120 121 // whenever an inference has both grey parents and non-grey parents, remove the grey parents 122 if (hasGreyParents && hasNonGreyParents) 123 { 124 UnitList* premises = UnitList::empty(); 125 126 VirtualIterator<Unit*> parents = InferenceStore::instance()->getParents(current); 127 while (parents.hasNext()) 128 { 129 Unit* premise = parents.next(); 130 if (premise->inheritedColor() != COLOR_TRANSPARENT) 131 { 132 UnitList::push(premise, premises); 133 } 134 else 135 { 136 premise->decRefCnt(); 137 } 138 } 139 140 current->inference() = NonspecificInferenceMany(current->inference().rule(), premises); 141 } 142 } 143 } 144 145 146 //main method 147 148 /* 149 * main method 150 * cf. Definition 3.1.2 of the thesis 151 */ getInterpolant(Unit * refutation,UnitWeight weightFunction)152 Formula* InterpolantsNew::getInterpolant(Unit *refutation, UnitWeight weightFunction) 153 { 154 BYPASSING_ALLOCATOR; 155 CALL("InterpolantsNew::getInterpolant"); 156 157 /* 158 * compute coloring for the inferences, i.e. compute splitting function in the words of the thesis 159 */ 160 const SplittingFunction splittingFunction = computeSplittingFunction(refutation, weightFunction); 161 162 /* 163 * compute A-subproofs 164 */ 165 const SubproofsUnionFind unitsToRepresentative = computeSubproofs(refutation, splittingFunction); 166 167 /* 168 * collect all boundaries of the subproofs 169 */ 170 const Boundary boundary = computeBoundary(refutation, splittingFunction); 171 172 /* 173 * generate the interpolant (i.e. the splitting formula in the words of the thesis, cf. Definition 3.1.2. of the thesis) 174 */ 175 const auto interpolant = generateInterpolant(refutation, boundary, splittingFunction, unitsToRepresentative); 176 177 return interpolant; 178 } 179 180 181 //main helper methods 182 183 /* 184 * compute the maximal A-subproofs of the proofs using standard union-find ideas as described in the thesis 185 * Note: can't just use depth-first-search, since edge information is only saved in one direction in the nodes 186 * Note: We represent each subproof by the conclusion of one of its inferences (the so called representative unit) 187 */ computeSubproofs(Unit * refutation,const SplittingFunction & splittingFunction)188 InterpolantsNew::SubproofsUnionFind InterpolantsNew::computeSubproofs(Unit* refutation, const SplittingFunction& splittingFunction) 189 { 190 CALL("InterpolantsNew::computeSubproofs"); 191 192 std::unordered_map<Unit*, Unit*> unitsToRepresentative; // maps each unit u1 (belonging to a red subproof) to the representative unit u2 of that subproof 193 std::unordered_map<Unit*, int> unitsToSize; // needed for weighted quick-union: for each unit, counts number of elements rooted in that unit 194 195 ProofIteratorBFSPreOrder it(refutation); // traverse the proof in breadth-first pre-order 196 while (it.hasNext()) 197 { 198 Unit* current = it.next(); 199 200 // standard union-find: if current inference is assigned to A-part of the proof, 201 if (splittingFunction.at(current) == COLOR_LEFT) 202 { 203 // then for each parent inference, 204 VirtualIterator<Unit*> parents = InferenceStore::instance()->getParents(current); 205 while (parents.hasNext()) 206 { 207 Unit* premise = parents.next(); 208 209 // the parent may be from the B-part, this is to induce connectedness over a common parent 210 // (Even then we want to merge, so that this parent appears only once in the final interpolant.) 211 { 212 // merge the subproof of the current inference with the subproof of the parent inference 213 merge(unitsToRepresentative, unitsToSize, current, premise); 214 } 215 } 216 } 217 } 218 219 return unitsToRepresentative; 220 } 221 222 223 /* 224 * computes the boundaries of the A-subproofs using Breadth-first search (BFS) 225 * Using idea from the thesis: a unit occurs as boundary of a subproof, if it has a different color than of its parents/ one of its children. 226 */ computeBoundary(Unit * refutation,const SplittingFunction & splittingFunction)227 InterpolantsNew::Boundary InterpolantsNew::computeBoundary(Unit* refutation,const SplittingFunction& splittingFunction) 228 { 229 CALL("InterpolantsNew::computeBoundary"); 230 231 std::unordered_set<Kernel::Unit*> inputNodes; // input is a blue premise of a red inference 232 std::unordered_set<Kernel::Unit*> outputNodes; // output is a red premise of a blue inference or a red refutation 233 234 ProofIteratorBFSPreOrder it(refutation); // traverse the proof in breadth-first pre-order 235 while (it.hasNext()) 236 { 237 Unit* current = it.next(); 238 239 // if current inference is assigned to A-part 240 ASS(splittingFunction.at(current) == COLOR_LEFT || splittingFunction.at(current) == COLOR_RIGHT); 241 if (splittingFunction.at(current) == COLOR_LEFT) 242 { 243 // then for each parent inference, 244 VirtualIterator<Unit*> parents = InferenceStore::instance()->getParents(current); 245 while (parents.hasNext()) 246 { 247 Unit* premise = parents.next(); 248 249 // if it is assigned to the B-part 250 ASS(splittingFunction.at(premise) == COLOR_LEFT || splittingFunction.at(premise) == COLOR_RIGHT); 251 if (splittingFunction.at(premise) != COLOR_LEFT) 252 { 253 inputNodes.insert(premise); 254 } 255 } 256 } 257 258 // if current inference is assigned to B-part 259 else 260 { 261 // then for each parent inference, 262 VirtualIterator<Unit*> parents = InferenceStore::instance()->getParents(current); 263 while (parents.hasNext()) 264 { 265 Unit* premise = parents.next(); 266 267 // if it is assigned to the A-part 268 ASS(splittingFunction.at(premise) == COLOR_LEFT || splittingFunction.at(premise) == COLOR_RIGHT); 269 if (splittingFunction.at(premise) == COLOR_LEFT) 270 { 271 outputNodes.insert(premise); 272 } 273 } 274 } 275 } 276 277 // we finally have to check for the empty clause, if it appears as boundary of an A-subproof 278 if (splittingFunction.at(refutation) == COLOR_LEFT) 279 { 280 outputNodes.insert(refutation); 281 } 282 283 return make_pair(std::move(inputNodes), std::move(outputNodes)); 284 } 285 286 /* 287 * generate the interpolant from the boundary 288 * Note: we already have collected all relevant information before calling this function, 289 * we now just need to build (and simplify) a formula out of the information. 290 */ generateInterpolant(Kernel::Unit * refutation,const Boundary & boundary,const SplittingFunction & splittingFunction,const SubproofsUnionFind & unitsToRepresentative)291 Formula* InterpolantsNew::generateInterpolant(Kernel::Unit* refutation, const Boundary& boundary, 292 const SplittingFunction& splittingFunction, const SubproofsUnionFind& unitsToRepresentative) 293 { 294 CALL("InterpolantsNew::generateInterpolant"); 295 296 const std::unordered_set<Unit*>& inputNodes = boundary.first; 297 const std::unordered_set<Unit*>& outputNodes = boundary.second; 298 299 struct InterpolantBuilder { 300 int implCnt; // for statistics only 301 302 Kernel::Color lastCol; 303 FormulaList* conjuncts; 304 Formula* aside; 305 InterpolantBuilder() : implCnt(0), lastCol(COLOR_LEFT), conjuncts(FormulaList::empty()), aside(nullptr) {} 306 307 Formula* finiliseLeft() { 308 CALL("InterpolantsNew::InterpolantBuilder::finiliseLeft"); 309 return JunctionFormula::generalJunction(Connective::AND, conjuncts); 310 } 311 312 Formula* finiliseRight() { 313 CALL("InterpolantsNew::InterpolantBuilder::finiliseRight"); 314 Formula* antecedent = JunctionFormula::generalJunction(Connective::AND, conjuncts); 315 316 implCnt++; 317 318 return new BinaryFormula(IMP,antecedent,aside); 319 } 320 321 Formula* finalise() { 322 CALL("InterpolantsNew::InterpolantBuilder::finalise"); 323 if (lastCol == COLOR_LEFT) { 324 return finiliseLeft(); 325 } else { 326 return finiliseRight(); 327 } 328 } 329 330 void addLeft(Unit* u) { 331 CALL("InterpolantsNew::InterpolantBuilder::addLeft"); 332 // cout << "addLeft " << u->toString() << endl; 333 334 if (lastCol != COLOR_LEFT) { 335 Formula* f = finiliseRight(); 336 conjuncts = FormulaList::empty(); 337 FormulaList::push(f,conjuncts); 338 } 339 FormulaList::push(u->getFormula(),conjuncts); 340 341 lastCol = COLOR_LEFT; 342 } 343 344 void addRight(Unit* u) { 345 CALL("InterpolantsNew::InterpolantBuilder::addRight"); 346 // cout << "addRight " << u->toString() << endl; 347 348 if (lastCol != COLOR_RIGHT) { 349 aside = finiliseLeft(); 350 conjuncts = FormulaList::empty(); 351 } 352 FormulaList::push(u->getFormula(),conjuncts); 353 354 lastCol = COLOR_RIGHT; 355 } 356 }; 357 358 // one nested implication for each connected A-part 359 // std::unordered_map<Unit*, InterpolantBuilder> contributions; 360 InterpolantBuilder justOneNoodle; 361 362 // do dfs on the derivation and present results in the reversed order (using stack for it) 363 ProofIteratorPostOrder pipo(refutation); 364 static UnitStack buffer; 365 buffer.reset(); 366 buffer.loadFromIterator(pipo); 367 368 UnitStack::Iterator it(buffer); 369 while (it.hasNext()) { 370 Unit* u = it.next(); 371 372 // cout << "Next " << u->toString() << endl; 373 374 if (outputNodes.find(u) != outputNodes.end()) { 375 ASS_EQ(splittingFunction.at(u),COLOR_LEFT); 376 377 /* 378 Unit* uRoot = root(unitsToRepresentative, u); 379 contributions[uRoot].addLeft(u); 380 */ 381 justOneNoodle.addLeft(u); 382 383 } else if (inputNodes.find(u) != inputNodes.end()) { 384 ASS_EQ(splittingFunction.at(u),COLOR_RIGHT); 385 386 /* 387 Unit* uRoot = root(unitsToRepresentative, u); 388 contributions[uRoot].addRight(u); 389 */ 390 justOneNoodle.addRight(u); 391 } 392 } 393 394 /* 395 FormulaList* outerConjunction = FormulaList::empty(); 396 397 // statistics only 398 vstring nestednesses; 399 400 for (auto& rootBuilderPair : contributions) { 401 InterpolantBuilder& builder = rootBuilderPair.second; 402 403 FormulaList::push(builder.finalise(),outerConjunction); 404 405 nestednesses += Int::toString(builder.implCnt) + ","; 406 } 407 */ 408 409 // finally conjoin all generated implications and return the simplified result, which is the interpolant 410 //Formula* interpolant = JunctionFormula::generalJunction(Connective::AND, outerConjunction); 411 Formula* interpolant = justOneNoodle.finalise(); 412 413 // print number of pieces 414 // print the depth of each ... 415 416 // cout << "Number of red components: " << contributions.size() << endl; 417 cout << "Nestedness: " << justOneNoodle.implCnt << endl; 418 cout << "Before simplification: " << interpolant->toString() << endl; 419 cout << "Weight before simplification: " << interpolant->weight() << endl; 420 421 return Flattening::flatten(NNF::ennf(Flattening::flatten(SimplifyFalseTrue::simplify(interpolant)),true)); 422 } 423 424 425 // splitting function 426 427 /* 428 * implements local splitting function from the thesis (improved version of approach #2, cf. section 3.3) 429 */ computeSplittingFunction(Kernel::Unit * refutation,UnitWeight weightFunction)430 std::unordered_map<Kernel::Unit*, Kernel::Color> InterpolantsNew::computeSplittingFunction(Kernel::Unit* refutation, UnitWeight weightFunction) 431 { 432 CALL("InterpolantsNew::computeSplittingFunction"); 433 434 std::unordered_map<Kernel::Unit*, Kernel::Color> splittingFunction; 435 436 ProofIteratorPostOrder it(refutation); 437 while (it.hasNext()) // traverse the proof in depth-first post order 438 { 439 Unit* current = it.next(); 440 ASS((!InferenceStore::instance()->getParents(current).hasNext() && (current->inheritedColor() == COLOR_LEFT || current->inheritedColor() == COLOR_RIGHT)) || (InferenceStore::instance()->getParents(current).hasNext() && current->inheritedColor() == COLOR_INVALID)); 441 442 // if the inference is an axiom, assign it to the corresponding partition 443 if (!InferenceStore::instance()->getParents(current).hasNext()) 444 { 445 splittingFunction[current] = current->inheritedColor(); 446 continue; 447 } 448 449 // if the inference contains a colored symbol, assign it to the corresponding partition (this 450 // ensures requirement of a LOCAL splitting function in the words of the thesis): 451 // - this is the case if either the conclusion contains a colored symbol 452 if (current->getColor() == COLOR_LEFT || current->getColor() == COLOR_RIGHT) 453 { 454 splittingFunction[current] = current->getColor(); 455 continue; 456 } 457 458 // - or if any premise contains a colored symbol 459 Color containedColor = COLOR_TRANSPARENT; 460 VirtualIterator<Unit*> parents = InferenceStore::instance()->getParents(current); 461 while (parents.hasNext()) 462 { 463 Unit* premise= parents.next(); 464 465 if (premise->getColor() == COLOR_LEFT || premise->getColor() == COLOR_RIGHT) 466 { 467 containedColor = premise->getColor(); 468 break; 469 } 470 } 471 if (containedColor != COLOR_TRANSPARENT) 472 { 473 splittingFunction[current] = containedColor; 474 continue; 475 } 476 477 /* otherwise we choose the following heuristic 478 * if the weighted sum of the conclusions of all parent inferences assigned 479 * to the red partition is greater than the weighted sum of the conclusions 480 * of all parent inferences assigned to the blue partition, then 481 * assign the inference to red, otherwise to blue 482 */ 483 parents = InferenceStore::instance()->getParents(current); 484 485 double difference = 0; 486 while (parents.hasNext()) 487 { 488 Unit* premise= parents.next(); 489 490 ASS(splittingFunction.at(premise) == COLOR_LEFT || splittingFunction.at(premise) == COLOR_RIGHT); 491 if (splittingFunction.at(premise) == COLOR_LEFT) 492 { 493 difference += weightForUnit(premise, weightFunction); 494 } 495 else 496 { 497 difference -= weightForUnit(premise, weightFunction); 498 } 499 } 500 splittingFunction[current] = difference > 0 ? COLOR_LEFT : COLOR_RIGHT; 501 } 502 503 return splittingFunction; 504 } 505 506 // helper method for unit weight 507 weightForUnit(Kernel::Unit * unit,UnitWeight weightFunction)508 double InterpolantsNew::weightForUnit(Kernel::Unit* unit, UnitWeight weightFunction) 509 { 510 CALL("InterpolantsNew::weightForUnit"); 511 512 if (weightFunction == UnitWeight::VAMPIRE) 513 { 514 return unit->getWeight(); 515 } 516 else 517 { 518 ASS_EQ(weightFunction, UnitWeight::QUANTIFIED_VARS); 519 return unit->varCnt(); 520 } 521 } 522 523 524 // union find helper methods 525 526 /* 527 * standard implementation of union-find following 528 * https://www.cs.princeton.edu/~rs/AlgsDS07/01UnionFind.pdf 529 * Note: we keep the invariant that we omit from the map the units which map to themselves 530 * Note: we don't apply path compression. That would possibly be a little 531 * bit faster, but then we couldn't make the unitsToRepresentative-argument 532 * of the root-function const. 533 */ 534 root(const UnionFindMap & unitsToRepresentative,Unit * unit)535 Kernel::Unit* InterpolantsNew::root(const UnionFindMap& unitsToRepresentative, Unit* unit) 536 { 537 CALL("InterpolantsNew::root"); 538 539 Unit* root = unit; 540 while (unitsToRepresentative.find(root) != unitsToRepresentative.end()) 541 { 542 ASS_NEQ(unitsToRepresentative.at(root), root); 543 root = unitsToRepresentative.at(root); 544 } 545 546 return root; 547 } 548 find(UnionFindMap & unitsToRepresentative,Unit * unit1,Unit * unit2)549 bool InterpolantsNew::find(UnionFindMap& unitsToRepresentative, Unit* unit1, Unit* unit2) 550 { 551 CALL("InterpolantsNew::find"); 552 553 return root(unitsToRepresentative, unit1) == root(unitsToRepresentative, unit2); 554 } 555 merge(UnionFindMap & unitsToRepresentative,std::unordered_map<Unit *,int> unitsToSize,Unit * unit1,Unit * unit2)556 void InterpolantsNew::merge(UnionFindMap& unitsToRepresentative, 557 std::unordered_map<Unit*, int> unitsToSize, 558 Unit* unit1, 559 Unit* unit2) 560 { 561 CALL("InterpolantsNew::merge"); 562 563 ASS_NEQ(unit1, unit2); 564 Unit* root1 = root(unitsToRepresentative, unit1); 565 Unit* root2 = root(unitsToRepresentative, unit2); 566 567 if (root1 != root2) 568 { 569 if (unitsToSize[root1] < unitsToSize[root2]) // weighted version 570 { 571 unitsToRepresentative[root1] = root2; 572 unitsToSize[root2] += unitsToSize[root1]; 573 } 574 else 575 { 576 unitsToRepresentative[root2] = root1; 577 unitsToSize[root1] += unitsToSize[root2]; 578 } 579 } 580 } 581 ProofIteratorBFSPreOrder(Unit * refutation)582 ProofIteratorBFSPreOrder::ProofIteratorBFSPreOrder(Unit* refutation) 583 { 584 CALL("ProofIteratorBFSPreOrder::ProofIteratorBFSPreOrder"); 585 586 todo.push(refutation); 587 } 588 hasNext()589 bool ProofIteratorBFSPreOrder::hasNext() 590 { 591 CALL("ProofIteratorBFSPreOrder::hasNext"); 592 593 while (!todo.empty()) 594 { 595 if (visited.find(todo.front()) == visited.end()) 596 { 597 return true; 598 } 599 else 600 { 601 todo.pop(); 602 } 603 } 604 605 return false; 606 } 607 608 /* 609 * iterative Breadth-first search (BFS) through the proof DAG 610 */ next()611 Unit* ProofIteratorBFSPreOrder::next() 612 { 613 CALL("ProofIteratorBFSPreOrder::next"); 614 615 while (!todo.empty()) 616 { 617 Unit* current = todo.front(); 618 todo.pop(); 619 620 if (visited.find(current) == visited.end()) 621 { 622 // add unprocessed premises to queue for BFS: 623 VirtualIterator<Unit*> parents = InferenceStore::instance()->getParents(current); 624 625 while (parents.hasNext()) 626 { 627 Unit* premise= parents.next(); 628 todo.push(premise); 629 } 630 631 // remember that we have visited current 632 visited.insert(current); 633 634 return current; 635 } 636 637 } 638 639 // we have already iterated through all inferences 640 return nullptr; 641 } 642 643 ProofIteratorPostOrder(Unit * refutation)644 ProofIteratorPostOrder::ProofIteratorPostOrder(Unit* refutation) 645 { 646 CALL("ProofIteratorPostOrder::ProofIteratorPostOrder"); 647 todo.push(refutation); 648 } 649 hasNext()650 bool ProofIteratorPostOrder::hasNext() 651 { 652 CALL("ProofIteratorPostOrder::hasNext"); 653 return !todo.empty(); 654 } 655 656 /* 657 * iterative post-order depth-first search (DFS) through the proof DAG 658 * following the usual ideas, e.g. 659 * https://pythonme.wordpress.com/2013/08/05/algorithm-iterative-dfs-depth-first-search-with-postorder-and-preorder/ 660 */ next()661 Unit* ProofIteratorPostOrder::next() 662 { 663 CALL("ProofIteratorPostOrder::next"); 664 while (!todo.empty()) 665 { 666 Unit* currentUnit = todo.top(); 667 668 // if we haven't already visited the current unit 669 if (visited.find(currentUnit) == visited.end()) 670 { 671 bool existsUnvisitedParent = false; 672 673 // add unprocessed premises to stack for DFS. If there is at least one unprocessed premise, don't compute the result 674 // for currentUnit now, but wait until those unprocessed premises are processed. 675 VirtualIterator<Unit*> parents = InferenceStore::instance()->getParents(currentUnit); 676 while (parents.hasNext()) 677 { 678 Unit* premise= parents.next(); 679 680 // if we haven't visited the current premise yet 681 if (visited.find(premise) == visited.end()) 682 { 683 // add it to the stack 684 todo.push(premise); 685 existsUnvisitedParent = true; 686 } 687 } 688 689 // if we already visited all parent-inferences, we can visit the inference too 690 if (!existsUnvisitedParent) 691 { 692 visited.insert(currentUnit); 693 todo.pop(); 694 return currentUnit; 695 } 696 } 697 else 698 { 699 todo.pop(); 700 } 701 } 702 703 // we have already iterated through all inferences 704 return nullptr; 705 } 706 707 708 } 709