1 2 /* 3 * File SubformulaIterator.hpp. 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 SubformulaIterator.hpp 21 * Defines a class SubformulaIterator that iterates 22 * over subformulas in formula lists and formulas. 23 * 24 * @since 06/01/2004, Manchester 25 */ 26 27 #ifndef __SubformulaIterator__ 28 #define __SubformulaIterator__ 29 30 #include "Lib/VirtualIterator.hpp" 31 32 #include "Formula.hpp" 33 34 namespace Kernel { 35 36 /** 37 * Implements an iterator over subformulas of a formula or formula list. 38 */ 39 class SubformulaIterator 40 : public IteratorCore<Formula*> 41 { 42 public: 43 SubformulaIterator (Formula*); 44 SubformulaIterator (FormulaList*); 45 ~SubformulaIterator (); 46 47 bool hasNext (); 48 Formula* next (); 49 Formula* next (int& polarity); 50 private: 51 class Element; 52 Formula* _current; 53 int _currentPolarity; 54 Element* _reserve; 55 }; // class SubformulaIterator 56 57 } 58 59 #endif // __SubformulaIterator__ 60 61 62