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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
/*
* 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 Unit.hpp
* Defines class Unit for all kinds of proof units
*
* @since 08/05/2007 Manchester
*/
#ifndef __Unit__
#define __Unit__
#include "Forwards.hpp"
#include "Lib/List.hpp"
#include "Lib/Output.hpp"
#include "Kernel/Inference.hpp"
namespace Kernel {
using namespace Lib;
/**
* Class to represent units of inference (such as clauses and formulas).
* @since 08/05/2007 Manchester
*/
class Unit
{
protected:
~Unit() {}
public:
/** Kind of unit. The integers should not be changed, they are used in
* Compare.
*/
enum Kind {
/** Clause unit */
CLAUSE = 0,
/** Formula unit */
FORMULA = 1
};
void destroy();
std::string toString() const;
unsigned varCnt();
std::string inferenceAsString() const;
/** True if a clause unit */
bool isClause() const
{ return _kind == CLAUSE; }
Clause* asClause();
/** Return the number of this unit */
unsigned number() const { return _number; }
/** Forcefully change the unit's number - use with care! - numbers should be unique across the whole board! */
void overwriteNumber(unsigned newNumber) { _number = newNumber; }
/** Return the inference of this unit */
Inference& inference() { return _inference; }
const Inference& inference() const { return _inference; }
/** return the input type of the unit */
UnitInputType inputType() const { return _inference.inputType(); }
/** set the input type of the unit */
void setInputType(UnitInputType it) { _inference.setInputType(it); }
/** return true if inputType relates to a goal **/
bool derivedFromGoal() const { return _inference.derivedFromGoal(); }
/** see isPureTheoryDescendant in Inference.cpp */
bool isPureTheoryDescendant() const { return _inference.isPureTheoryDescendant(); }
/** see isTheoryAxiom in Inference.cpp */
bool isTheoryAxiom() const { return _inference.isTheoryAxiom(); }
unsigned char getSineLevel() const { return _inference.getSineLevel(); }
/** true if the unit is read from a TPTP included file */
bool included() const { return _inference.included(); }
/** This is just a more convenient (but also less efficient) way
* for accessing the unit's parents than using its inferefence's iterator. */
UnitIterator getParents() const;
/**
* Recursive minimization of ancestors for sat-based inferences (AVATAR_REFUTATION, GLOBAL_SUMSUPTION) triggered here.
*
* (Note that with minimizeSatProofs set to off, it's already too late to do this as we did not collect the necessary info,
* however, it pays off to call this anyway, to correctly set any required stats in the inference objects.)
*
* Could be extended further if more stats provided by the inference tree should be found
* to require some final touches before proof printing. Currently, we care about the InputType, the induction stats, and _isPureTheoryDescendant.
*
* returns true if the minimized tree traversal observed an INPUT inference (to facilitate a certain sanity check later).
*/
bool minimizeAncestorsAndUpdateSelectedStats();
/** Return the inherited color of the unit or COLOR_INVALID
* if there isn't an inherited color.
*
* Inherited color is set by parser constructs left_formula,
* right_formula and end_formula.
*/
inline Color inheritedColor() const
{
return static_cast<Color>(_inheritedColor);
}
void setInheritedColor(Color color)
{
ASS_NEQ(color,COLOR_INVALID);
_inheritedColor = color;
} // setInheritedColor
void invalidateInheritedColor() { _inheritedColor = COLOR_INVALID; }
Color getColor();
unsigned getWeight();
Formula* getFormula();
/**
* Increase the number of references to the unit.
*
* Only clauses are reference-counted, for FormulaUnits nothing
* is done.
*/
void incRefCnt();
/**
* Decrease the number of references to the unit.
*
* Only clauses are reference-counted, for FormulaUnits nothing
* is done.
*/
void decRefCnt();
/** Return true iff unit was created during preprocessing
* (and not during the run of the saturation algorithm) */
inline bool isFromPreprocessing()
{ return !_firstNonPreprocessingNumber || _number<_firstNonPreprocessingNumber; }
void assertValid();
static void onPreprocessingEnd();
static void resetPreprocessingEnd() { _firstNonPreprocessingNumber = 0; }
static void onParsingEnd(){ _lastParsingNumber = _lastNumber;}
static unsigned getLastParsingNumber(){ return _lastParsingNumber;}
protected:
/** Number of this unit, used for printing and statistics */
unsigned _number;
/** Kind */
unsigned _kind : 1;
/** used in interpolation to denote parents of what color have been used */
unsigned _inheritedColor : 2;
/** inference used to obtain the unit */
Inference _inference;
Unit(Kind kind, Inference inf);
/** Used to enumerate units */
static unsigned _lastNumber;
/** Used to determine which clauses come from preprocessing
*
* 0 means preprocessing is not over yet.*/
static unsigned _firstNonPreprocessingNumber;
static unsigned _lastParsingNumber;
/** outputs this unit and its parents depending on vampire's clause tracing options */
void doUnitTracing();
private:
template<class Pre, class Post>
void _traverseParents(Unit& self, unsigned& depth, Pre& pre, Post& post) {
pre(unsigned(depth), &self);
depth++;
auto infit = self.inference().iterator();
while (self.inference().hasNext(infit)) {
auto parent = self.inference().next(infit);
_traverseParents(*parent, depth, pre, post);
}
depth--;
post(unsigned(depth), &self);
}
protected:
template<class Pre, class Post>
void traverseParents(Pre pre, Post post) {
unsigned depth = 0;
_traverseParents(*this, depth, pre, post);
}
template<class Pre>
void traverseParentsPre (Pre pre ) { traverseParents(pre , [](auto...) {}); }
template<class Post>
void traverseParentsPost(Post post) { traverseParents([](auto...) {}, post); }
}; // class Unit
std::ostream& operator<< (std::ostream& out, const Unit& u );
}
#endif