1
2 /*
3 * File SubformulaIterator.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 SubformulaIterator.cpp
21 * Implements a class SubformulaIterator that iterates
22 * over subformulas in formula lists, and formulas.
23 *
24 * @since 06/01/2004 Manchester
25 * @since 02/06/2007 Manchester changed to new datastructures
26 * @since 06/05/2015 Gothenburg in order to support FOOL, we need to search for formulas inside terms as well
27 */
28
29 #include "Debug/Tracer.hpp"
30
31 #include "SubformulaIterator.hpp"
32
33 namespace Kernel {
34
35 /**
36 * Elements strong information, used internally in subformula iterators.
37 */
38 class SubformulaIterator::Element {
39 public:
Element(FormulaList * list,int polarity,Element * rest)40 Element (FormulaList* list, int polarity, Element* rest)
41 : _tag(FORMULA_LIST),
42 _formulaList(list),
43 _polarity(polarity),
44 _rest(rest)
45 {}
Element(Formula * f,int polarity,Element * rest)46 Element (Formula* f, int polarity, Element* rest)
47 : _tag(FORMULA),
48 _formula(f),
49 _polarity(polarity),
50 _rest(rest)
51 {}
Element(TermList * ts,int polarity,Element * rest)52 Element (TermList* ts, int polarity, Element* rest)
53 : _tag(TERM_LIST),
54 _termList(ts),
55 _polarity(polarity),
56 _rest(rest)
57 {}
Element(Term * t,int polarity,Element * rest)58 Element (Term* t, int polarity, Element* rest)
59 : _tag(TERM),
60 _term(t),
61 _polarity(polarity),
62 _rest(rest)
63 {}
64 enum Tag {
65 FORMULA_LIST,
66 FORMULA,
67 TERM_LIST,
68 TERM
69 };
70 Tag _tag;
71 union{
72 FormulaList* _formulaList;
73 Formula* _formula;
74 TermList* _termList;
75 Term* _term;
76 };
77 int _polarity;
78 Element* _rest;
79
80 CLASS_NAME(SubformulaIterator::Element);
81 USE_ALLOCATOR(SubformulaIterator::Element);
82 };
83
84
85 /**
86 * Build an iterator over t.
87 * @since 06/01/2004 Manchester
88 */
SubformulaIterator(Formula * f)89 SubformulaIterator::SubformulaIterator (Formula* f)
90 : _current(f),
91 _currentPolarity(1),
92 _reserve(0)
93 {
94 } // SubformulaIterator::SubformulaIterator
95
96
97 /**
98 * Build an iterator over of ts.
99 * @since 06/01/2004 Manchester
100 */
SubformulaIterator(FormulaList * ts)101 SubformulaIterator::SubformulaIterator (FormulaList* ts)
102 : _current(0),
103 _reserve(new Element(ts,1,0))
104 {
105 } // SubformulaIterator::SubformulaIterator
106
107
108 /**
109 * True if there the next subformula.
110 * @since 06/01/2004 Manchester
111 * @since 22/08/2004 Torrevieja, a bug fixed causing reserve formulas
112 * to be ignored
113 * @since 06/05/2015 Gothenburg look inside terms in search for formulas, used by FOOL
114 */
hasNext()115 bool SubformulaIterator::hasNext ()
116 {
117 CALL("SubformulaIterator::hasNext");
118
119 if (_current) {
120 return true;
121 }
122
123 // try to set _current
124 while (_reserve) {
125 switch (_reserve->_tag) {
126 case Element::Tag::FORMULA_LIST: {
127 FormulaList *first = _reserve->_formulaList;
128 if (FormulaList::isEmpty(first)) {
129 Element *rest = _reserve->_rest;
130 delete _reserve;
131 _reserve = rest;
132 break;
133 } else { // first is non-empty
134 _current = first->head();
135 _currentPolarity = _reserve->_polarity;
136 _reserve->_formulaList = first->tail();
137 return true;
138 }
139 }
140
141 case Element::Tag::FORMULA: {
142 _current = _reserve->_formula;
143 _currentPolarity = _reserve->_polarity;
144 Element *rest = _reserve->_rest;
145 delete _reserve;
146 _reserve = rest;
147 return true;
148 }
149
150 case Element::Tag::TERM_LIST: {
151 TermList* first = _reserve->_termList;
152 if (!first->isTerm()) {
153 Element *rest = _reserve->_rest;
154 delete _reserve;
155 _reserve = rest;
156 } else { // first is non-empty
157 _reserve->_termList = first->next();
158 _reserve = new Element(first->term(), _reserve->_polarity, _reserve);
159 }
160 break;
161 }
162
163 case Element::Tag::TERM: {
164 Term* term = _reserve->_term;
165 int polarity = _reserve->_polarity;
166 Element* rest = new Element(term->args(), polarity, _reserve->_rest);
167 if (!term->isSpecial()) {
168 delete _reserve;
169 _reserve = rest;
170 break;
171 }
172
173 switch (term->functor()) {
174 case Term::SF_ITE: {
175 _current = term->getSpecialData()->getCondition();
176 _currentPolarity = polarity;
177 delete _reserve;
178 _reserve = rest;
179 return true;
180 }
181 case Term::SF_LET: {
182 delete _reserve;
183 TermList binding = term->getSpecialData()->getBinding();
184 if (!binding.isTerm()) {
185 _reserve = rest;
186 } else {
187 // TODO: should be 1 instead of polarity?
188 _reserve = new Element(binding.term(), polarity, rest);
189 }
190 break;
191 }
192 case Term::SF_LET_TUPLE: {
193 delete _reserve;
194 TermList binding = term->getSpecialData()->getBinding();
195 if (!binding.isTerm()) {
196 _reserve = rest;
197 } else {
198 // TODO: should be 1 instead of polarity?
199 _reserve = new Element(binding.term(), polarity, rest);
200 }
201 break;
202 }
203 case Term::SF_FORMULA: {
204 _current = term->getSpecialData()->getFormula();
205 _currentPolarity = polarity;
206 delete _reserve;
207 _reserve = rest;
208 return true;
209 }
210 case Term::SF_TUPLE: {
211 delete _reserve;
212 Term* tupleTerm = term->getSpecialData()->getTupleTerm();
213 // TODO: should be 1 instead of polarity?
214 _reserve = new Element(tupleTerm, polarity, rest);
215 break;
216 }
217 #if VDEBUG
218 default:
219 ASSERTION_VIOLATION;
220 #endif
221 }
222 break;
223 }
224
225 #if VDEBUG
226 default:
227 ASSERTION_VIOLATION;
228 #endif
229 }
230 }
231 // _reserve is empty
232 return false;
233 } // SubformulaIterator::hasNext
234
235
236 /**
237 * Return the next subformula.
238 */
next()239 Formula* SubformulaIterator::next ()
240 {
241 CALL("SubformulaIterator::next/0");
242
243 int dummy;
244 return next(dummy);
245 }
246
247 /**
248 * Return the next subformula, into @c resultPolarity assign the polarity
249 * of the returned subformula in the iterated formula.
250 *
251 * @since 06/01/2004 Manchester
252 * @since 11/12/2004 Manchester, true and false added
253 * @since 06/05/2015 Gothenburg look inside terms in search for formulas, used by FOOL
254 */
next(int & resultPolarity)255 Formula* SubformulaIterator::next (int& resultPolarity)
256 {
257 CALL("SubformulaIterator::next/1");
258
259 Formula* result = _current;
260 resultPolarity = _currentPolarity;
261
262 switch (result->connective()) {
263 case LITERAL:
264 _reserve = new Element(result->literal()->args(), resultPolarity, _reserve);
265 _current = 0;
266 break;
267
268 case TRUE:
269 case FALSE:
270 case NAME:
271 _current = 0;
272 break;
273
274 case AND:
275 case OR:
276 _reserve = new Element(result->args(), resultPolarity, _reserve);
277 _current = 0;
278 break;
279
280 case IMP:
281 _current = result->left();
282 _currentPolarity = -resultPolarity;
283 _reserve = new Element(result->right(), resultPolarity, _reserve);
284 break;
285
286 case IFF:
287 case XOR:
288 _current = result->left();
289 _currentPolarity = 0;
290 _reserve = new Element(result->right(), 0, _reserve);
291 break;
292
293 case NOT:
294 _current = result->uarg();
295 _currentPolarity = -resultPolarity;
296 break;
297
298 case FORALL:
299 case EXISTS:
300 _current = result->qarg();
301 _currentPolarity = resultPolarity;
302 break;
303
304 case BOOL_TERM: {
305 _current = 0;
306 TermList ts = result->getBooleanTerm();
307 if (!ts.isVar()) {
308 // here we rely on the fact that TermList can only be either a variable, a $ite or a $let
309 _reserve = new Element(ts.term(), resultPolarity, _reserve);
310 }
311 break;
312 }
313
314 #if VDEBUG
315 default:
316 ASSERTION_VIOLATION;
317 #endif
318 }
319
320 return result;
321 } // SubformulaIterator::next
322
323
324 /**
325 * Destroy the iterator.
326 */
~SubformulaIterator()327 SubformulaIterator::~SubformulaIterator ()
328 {
329 while (_reserve) {
330 Element* next = _reserve->_rest;
331 delete _reserve;
332 _reserve = next;
333 }
334 } // SubformulaIterator::~SubformulaIterator
335
336 }
337