1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
/*
* This file is part of the source code of the software program
* Vampire. It is protected by applicable
* copyright laws.
*
* This source code is distributed under the licence found here
* https://vprover.github.io/license.html
* and in the source directory
*/
/**
* @file FormulaVarIterator.hpp
* Defines a class FormulaVarIterator that iterates
* over free variables in a formula or a term.
*
* @since 06/01/2004, Manchester
* @since 02/09/2009 Redmond, reimplemented to work with non-rectified
* formulas and return each variable only once
* @since 15/05/2015 Gothenburg, FOOL support added
*/
#ifndef __FormulaVarIterator__
#define __FormulaVarIterator__
#include "Lib/Stack.hpp"
#include "Kernel/Term.hpp"
#include "Kernel/Formula.hpp"
using namespace Lib;
namespace Kernel {
/**
* Implements an iterator over free variables of a
* formula, a term or a list of terms.
*
* Any argument may contain $let and $ite expressions.
*
* @since 06/01/2004, Manchester
* @since 02/09/2009 Redmond, reimplemented to work with non-rectified
* formulas and return each variable only once
* @since 15/05/2015 Gothenburg, FOOL support added
*/
class FormulaVarIterator
{
public:
DECL_ELEMENT_TYPE(unsigned);
explicit FormulaVarIterator(const Formula*);
explicit FormulaVarIterator(const Term*);
explicit FormulaVarIterator(const TermList);
bool hasNext();
unsigned next();
private:
/** instruction of what to process next */
enum Instruction {
/** process formula */
FVI_FORMULA,
/** process term */
FVI_TERM,
/** process term list */
FVI_TERM_LIST,
/** bind variables bound by quantifier or $let */
FVI_BIND,
/** unbind variables bound by quantifier or $let */
FVI_UNBIND,
};
/** If true then _nextVar contains the next variable */
bool _found;
/** The variable to be returned by next() */
unsigned _nextVar;
/** Counter used to store bound variables, together with the number of times they are bound */
ZIArray<unsigned> _bound;
/** To store previously found free variables */
ZIArray<bool> _free;
/** Stack of formulas to be processed */
Stack<const Formula*> _formulas;
/** Stack of terms to process */
Stack<const Term*> _terms;
/** Stack of term lists to process */
Stack<TermList> _termLists;
/** Stack of instructions telling what to do next */
Stack<Instruction> _instructions;
/** Stack of lists of variables to process */
Stack<const VList*> _vars;
}; // class FormulaVarIterator
template<typename T> // a template to work with Term*, TermList*, and Formula*
bool isFreeVariableOf(T thing, unsigned var)
{
FormulaVarIterator fvi(thing);
while (fvi.hasNext()) {
if (var == fvi.next()) {
return true;
}
}
return false;
}
/**
* Return the list of all free variables of the term.
* The result is only non-empty when there are quantified
* formulas or $let-terms inside the term.
* Each variable in the term is returned just once.
*
* NOTE: don't use this function, if you don't actually need a List
* (FormulaVarIterator is a better choice)
*
* NOTE: remember to free the list when done with it
* (otherwise we leak memory!)
*
* @since 07/05/2015 Gothenburg
*/
template<typename T> // a template to work with Term*, TermList*, and Formula*
VList* freeVariables(T thing)
{
FormulaVarIterator fvi(thing);
VList::FIFO result;
while (fvi.hasNext()) {
result.pushBack(fvi.next());
}
return result.list();
} // Term::freeVariables
}
#endif // __FormulaVarIterator__