1
2 /*
3 * File TermIterators.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 TermIterators.cpp
21 * Implements several iteratorn over terms.
22 */
23
24
25 #include "Debug/Tracer.hpp"
26
27 #include "Term.hpp"
28
29 #include "TermIterators.hpp"
30
31 namespace Kernel
32 {
33
34 /**
35 * True if there exists next variable
36 */
hasNext()37 bool VariableIterator::hasNext()
38 {
39 CALL("VariableIterator::hasNext");
40 if(_stack.isEmpty()) {
41 return false;
42 }
43 if(!_used && _stack.top()->isVar()) {
44 return true;
45 }
46 while(!_stack.isEmpty()) {
47 const TermList* t=_stack.pop();
48 if(_used && t->isVar()) {
49 _used=false;
50 t=t->next();
51 }
52 if(t->isEmpty()) {
53 continue;
54 }
55 if(t->isVar()) {
56 ASS(!_used);
57 _stack.push(t);
58 return true;
59 }
60 _stack.push(t->next());
61 ASS(t->isTerm());
62 const Term* trm=t->term();
63 if(!trm->shared() || !trm->ground()) {
64 _stack.push(trm->args());
65 }
66 }
67 return false;
68 }
69
70
71 ///////////////////////////////////////////
72
73
74 /**
75 * True if there exists next subterm
76 */
hasNext()77 bool SubtermIterator::hasNext()
78 {
79 CALL("SubtermIterator::hasNext");
80
81 if(_stack->isEmpty()) {
82 return false;
83 }
84 if(!_used) {
85 return true;
86 }
87 _used=false;
88 const TermList* t=_stack->pop();
89 pushNext(t->next());
90 if(t->isTerm()) {
91 pushNext(t->term()->args());
92 }
93 return !_stack->isEmpty();
94 }
95
96 /**
97 * Skip subterms of the term just returned by the @b next function
98 *
99 * Must be called after the @b next function before the @b hasNext
100 * function is called again.
101 */
right()102 void SubtermIterator::right()
103 {
104 CALL("SubtermIterator::right");
105 ASS(_stack->isNonEmpty());
106 ASS(_used);
107
108 _used=false;
109 const TermList* t=_stack->pop();
110 pushNext(t->next());
111
112 //we did here the same as in the hasNext function, we only didn't call
113 //the pushNext function on arguments of t
114 }
115
116 ///////////////////////////////////////////
117
118 /**
119 * True if there exists next subterm
120 */
hasNext()121 bool PolishSubtermIterator::hasNext()
122 {
123 CALL("PolishSubtermIterator::hasNext");
124
125 if(_stack.isEmpty()) {
126 return false;
127 }
128 if(!_used) {
129 return true;
130 }
131 _used=false;
132 const TermList* t=_stack.pop();
133 pushNext(t->next());
134 return !_stack.isEmpty();
135 }
136
137 /**
138 * Return the next non-variable subterm.
139 * @since 04/05/2013 Manchester
140 * @author Andrei Voronkov
141 */
next()142 TermList NonVariableIterator::next()
143 {
144 CALL("NonVariableIterator::next");
145
146 Term* t = _stack.pop();
147 _added = 0;
148 Term::Iterator ts(t);
149 for (const TermList* ts = t->args();!ts->isEmpty();ts = ts->next()) {
150 if (ts->isTerm()) {
151 _stack.push(const_cast<Term*>(ts->term()));
152 _added++;
153 }
154 }
155 return TermList(t);
156 } // NonVariableIterator::next
157
158 /**
159 * Skip all subterms of the terms returned by the last call to next()
160 * @since 04/05/2013 Manchester
161 * @author Andrei Voronkov
162 */
right()163 void NonVariableIterator::right()
164 {
165 CALL("NonVariableIterator::right");
166
167 while (_added > 0) {
168 _added--;
169 _stack.pop();
170 }
171 } // NonVariableIterator::right
172
173 /**
174 * True if there exists next non-variable subterm
175 */
176 // bool NonVariableIterator::hasNext()
177 // {
178 // CALL("NonVariableIterator::hasNext");
179
180 // if(_stack.isEmpty()) {
181 // return false;
182 // }
183 // ASS(_stack.top()->isTerm());
184 // if(!_used) {
185 // return true;
186 // }
187 // _used=false;
188 // const TermList* t=_stack.pop();
189 // pushNextNonVar(t->next());
190 // pushNextNonVar(t->term()->args());
191 // return !_stack.isEmpty();
192 // }
193
194 // /**
195 // * Skip subterms of the term just returned by the @b next function
196 // *
197 // * Must be called after the @b next function before the @b hasNext
198 // * function is called again.
199 // */
200 // void NonVariableIterator::right()
201 // {
202 // CALL("NonVariableIterator::right");
203 // ASS(_stack.isNonEmpty());
204 // ASS(_used);
205
206 // _used=false;
207 // const TermList* t=_stack.pop();
208 // pushNextNonVar(t->next());
209
210 // //we did here the same as in the hasNext function, we only didn't call
211 // //the pushNextNonVar function on arguments of t
212 // }
213
214 // void NonVariableIterator::pushNextNonVar(const TermList* t)
215 // {
216 // while(t->isVar()) {
217 // t=t->next();
218 // }
219 // if(!t->isEmpty()) {
220 // ASS(t->isTerm());
221 // _stack.push(t);
222 // }
223 // }
224
225
226 ///////////////////////////////////////////
227
228 /**
229 * True if there exists another disagreement between the two
230 * terms specified in the constructor.
231 */
hasNext()232 bool DisagreementSetIterator::hasNext()
233 {
234 CALL("DisagreementSetIterator::hasNext");
235 ASS(_stack.size()%2==0);
236
237 if(!_arg1.isEmpty()) {
238 return true;
239 }
240 if(_stack.isEmpty()) {
241 return false;
242 }
243 TermList* ss; //t1 subterms
244 TermList* tt; //t2 subterms
245 while(!_stack.isEmpty()) {
246 tt=_stack.pop();
247 ss=_stack.pop();
248 if(!ss->next()->isEmpty()) {
249 _stack.push(ss->next());
250 _stack.push(tt->next());
251 }
252 if(!_disjunctVariables && ss->sameContent(tt)) {
253 //if content is the same, neighter weightDiff nor varDiffs would change
254 continue;
255 }
256 if(TermList::sameTopFunctor(*ss,*tt)) {
257 ASS(ss->isTerm());
258 ASS(tt->isTerm());
259 if(ss->term()->arity()) {
260 _stack.push(ss->term()->args());
261 _stack.push(tt->term()->args());
262 }
263 } else {
264 _arg1=*ss;
265 _arg2=*tt;
266 return true;
267 }
268 }
269 return false;
270 }
271
272
273 ///////////////////////////////////////////
274
275 /**
276 * Build an iterator over symbols of t.
277 * @since 26/05/2007 Manchester
278 */
TermFunIterator(const Term * t)279 TermFunIterator::TermFunIterator (const Term* t)
280 : _stack(64)
281 {
282 CALL("TermFunIterator::TermFunIterator");
283
284 _hasNext = true;
285 _next = t->functor();
286 _stack.push(t->args());
287 } // TermFunIterator::TermFunIterator
288
289
290 /**
291 * True if there the next function.
292 * @since 26/05/2007 Manchester
293 */
hasNext()294 bool TermFunIterator::hasNext ()
295 {
296 CALL("TermFunIterator::hasNext");
297
298 if (_hasNext) {
299 return true;
300 }
301
302 while (_stack.isNonEmpty()) {
303 const TermList* ts = _stack.pop();
304 if (ts->isEmpty()) {
305 continue;
306 }
307 _stack.push(ts->next());
308 if (ts->isVar()) {
309 continue;
310 }
311 _hasNext = true;
312 const Term* t = ts->term();
313 _next = t->functor();
314 _stack.push(t->args());
315 return true;
316 }
317 return false;
318 } // TermFunIterator::hasNext
319
320
321 /**
322 * Return the next symbol.
323 * @since 26/05/2007 Manchester
324 */
next()325 unsigned TermFunIterator::next ()
326 {
327 CALL("TermFunIterator::hasNext");
328
329 ASS(_hasNext);
330
331 _hasNext = false;
332 return _next;
333 } // TermFunIterator::next
334
335
336 ///////////////////////////////////////////
337
338 /**
339 * Build an iterator over variables of t.
340 */
TermVarIterator(const Term * t)341 TermVarIterator::TermVarIterator (const Term* t)
342 : _stack(64)
343 {
344 CALL("TermVarIterator::TermVarIterator");
345
346 _stack.push(t->args());
347 } // TermVarIterator::TermVarIterator
348
349 /**
350 * Build an iterator over variables of t.
351 * @since 06/01/2004 Manchester
352 * @since 26/05/2007 Manchester, reimplemented
353 */
TermVarIterator(const TermList * ts)354 TermVarIterator::TermVarIterator (const TermList* ts)
355 : _stack(64)
356 {
357 CALL("TermVarIterator::TermVarIterator");
358 _stack.push(ts);
359 } // TermVarIterator::TermVarIterator
360
361
362 /**
363 * True if there the next variable.
364 * @since 06/01/2004 Manchester
365 * @since 26/05/2007 Manchester, reimplemented for new datastructures
366 */
hasNext()367 bool TermVarIterator::hasNext ()
368 {
369 CALL("TermVarIterator::hasNext");
370
371 while (_stack.isNonEmpty()) {
372 const TermList* ts = _stack.pop();
373 if (ts->isEmpty()) {
374 continue;
375 }
376 _stack.push(ts->next());
377 if (ts->isVar()) {
378 _next = ts->var();
379 return true;
380 }
381 _stack.push(ts->term()->args());
382 }
383 return false;
384 } // TermVarIterator::hasNext
385
386
387 /**
388 * Return the next variable.
389 * @since 06/01/2004 Manchester
390 * @since 26/05/2007 Manchester, reimplemented for new datastructures
391 */
next()392 unsigned TermVarIterator::next ()
393 {
394 CALL("TermVarIterator::next");
395 return _next;
396 } // TermVarIterator::next
397
398
399 ///////////////////////////////////////////
400
401
402
403 }
404