40   if(_stack.isEmpty()) {  in hasNext()
43   if(!_used && _stack.top()->isVar()) {  in hasNext()
46   while(!_stack.isEmpty()) {  in hasNext()
47     const TermList* t=_stack.pop();  in hasNext()
57       _stack.push(t);  in hasNext()
60     _stack.push(t->next());  in hasNext()
64       _stack.push(trm->args());  in hasNext()
81   if(_stack->isEmpty()) {  in hasNext()
88   const TermList* t=_stack->pop();  in hasNext()
93   return !_stack->isEmpty();  in hasNext()
105   ASS(_stack->isNonEmpty());  in right()
109   const TermList* t=_stack->pop();  in right()
125   if(_stack.isEmpty()) {  in hasNext()
132   const TermList* t=_stack.pop();  in hasNext()
134   return !_stack.isEmpty();  in hasNext()
146   Term* t = _stack.pop();  in next()
151       _stack.push(const_cast<Term*>(ts->term()));  in next()
169     _stack.pop();  in right()
235   ASS(_stack.size()%2==0);  in hasNext()
240   if(_stack.isEmpty()) {  in hasNext()
245   while(!_stack.isEmpty()) {  in hasNext()
246     tt=_stack.pop();  in hasNext()
247     ss=_stack.pop();  in hasNext()
249       _stack.push(ss->next());  in hasNext()
250       _stack.push(tt->next());  in hasNext()
260 	_stack.push(ss->term()->args());  in hasNext()
261 	_stack.push(tt->term()->args());  in hasNext()
280   : _stack(64)  in TermFunIterator()
286   _stack.push(t->args());  in TermFunIterator()
302   while (_stack.isNonEmpty()) {  in hasNext()
303     const TermList* ts = _stack.pop();  in hasNext()
307     _stack.push(ts->next());  in hasNext()
314     _stack.push(t->args());  in hasNext()
342   : _stack(64)  in TermVarIterator()
346   _stack.push(t->args());  in TermVarIterator()
355   : _stack(64)  in TermVarIterator()
358   _stack.push(ts);  in TermVarIterator()
371   while (_stack.isNonEmpty()) {  in hasNext()
372     const TermList* ts = _stack.pop();  in hasNext()
376     _stack.push(ts->next());  in hasNext()
381     _stack.push(ts->term()->args());  in hasNext()