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
/*
* 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 FormulaUnit.hpp
* Defines class FormulaUnit for units consisting of formulas.
*
* @since 09/05/2007 Manchester
*/
#ifndef __FormulaUnit__
#define __FormulaUnit__
#include "Lib/Allocator.hpp"
#include "Unit.hpp"
using namespace Lib;
namespace Kernel {
class Formula;
/**
* Class to represent units of inference deriving formulas.
* @since 09/05/2007 Manchester
*/
class FormulaUnit
: public Unit
{
public:
/** New unit of a given kind */
FormulaUnit(Formula* f,const Inference& inf)
: Unit(FORMULA,inf),
_formula(f), _cachedColor(COLOR_INVALID), _cachedWeight(0)
{ doUnitTracing(); }
void destroy();
std::string toString() const;
unsigned varCnt();
/** Return the formula of this unit */
const Formula* formula() const
{ return _formula; }
/** Return the formula of this unit */
Formula* formula()
{ return _formula; }
Color getColor();
unsigned weight();
USE_ALLOCATOR(FormulaUnit);
protected:
/** Formula of this unit */
Formula* _formula;
Color _cachedColor;
unsigned _cachedWeight;
}; // class FormulaUnit
}
#endif