-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathTLFormulaSet.h
157 lines (112 loc) · 6.43 KB
/
TLFormulaSet.h
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
/* File: TLFormulaSet.h
Author: Marc Diefenbruch, Axel Hirche
Project: QUEST
Date: (C) 1997, 1998 University of Essen, Germany
*/
#ifndef _TL_FORMULASET_H_
#define _TL_FORMULASET_H_
#include "TL.h"
#include "SCL/SCList.h"
#include "TLFormula.h"
class TLFormulaSet : public SCList<TLFormula>
{
friend class SCStream& operator<< (class SCStream& out, const TLFormulaSet& set);
public:
TLFormulaSet (void); // Create empty set.
TLFormulaSet (const TLFormulaSet*);
// Create a copy.
TLFormulaSet (const TLFormula* phi);
// Create set with phi as sole
// element.
~TLFormulaSet (void);
class
SCStream& Display (class SCStream&) const;
// Have to do redefine this
// to avoid clashes with
// SCList...
TLFormulaSet& operator= (const TLFormulaSet&);
// assignment from set.
TLFormulaSet& operator= (const TLFormula*); // assignment from formula.
TLFormulaSet& operator+= (const TLFormulaSet&);
// union
TLFormulaSet& operator-= (const TLFormulaSet&);
// difference
TLFormulaSet& operator*= (const TLFormulaSet&);
// intersection
TLFormulaSet& operator+= (const TLFormula*);
// union assignment
TLFormulaSet& operator-= (const TLFormula*);
// difference assignment
SCBoolean Insert (const TLFormula*); // true, if phi actually was inserted,
// false otherwise.
SCBoolean IsSubset (const TLFormulaSet&);
// subset test
SCBoolean IsElem (const TLFormula*) const;
// element test
TLFormula* FindMatch (const TLFormula* toMatch) const;
// Return the element with
// TLFormula::operator== (*FindMatch(toMatch), *toMatch)
// equal to true.
// FindMatch(toMatch) == toMatch
// is normally NOT true!!!
SCBoolean operator== (const TLFormulaSet&) const;
// Equality test.
SCBoolean operator!= (const TLFormulaSet&) const;
// Inequality test.
SCNatural NumOfElems (void) const; // number of elements in set.
SCNatural NumOfAtomics (void) const; // number of atomic
// propositions in set.
TLFormula* ExtractAny (void); // Extract some formula from
// the set.
TLFormula* ExtractAtomic (void); // Extract some atomic formula
// from the set.
TLFormulaSet* GetAllAtomics (void) const; // Get subset with all
// atomic propositions.
SCBoolean IsEmpty (void) const; // Test emptyness of set.
SCBoolean IsValid (void) const; // Check if all atomic
// props evaluate to TRUE.
void RemoveAllElements (void);
static
void Initialize (SCBoolean trueEquivEmpty,
SCBoolean nowIsPureAtomic,
SCBoolean extendedAutomaton);
static
TLFormula* GetTRUEPhi (void);
static
TLFormula* GetFALSEPhi (void); // Formula sets only store
// references, i.e. do not
// dispose of their elements.
// If we have to create a TRUE
// or FALSE on the fly during
// expansion, we use a
// reference to a global static
// object to avoid memory leaks.
#if _TL_DEBUG_ > 4
void CheckMe (void) const; // Do some internal error
// checkig and bail out
// if any are found.
#endif
protected:
void InsertBefore (const TLFormula* toInsert,
class SCListCons<TLFormula>* where = NULL);
void InsertAfter (const TLFormula* toInsert,
class SCListCons<TLFormula>* where = NULL);
TLFormula* Remove (const TLFormula* toKill);
#if _TL_DEBUG_ > 4
SCBoolean deleted; // destructor sets this to true.
#endif
SCNatural numOfAtomics; // Number of Atomic
// propositions in a formula
// set.
static SCBoolean trueEquivEmpty;
static SCBoolean nowIsPureAtomic;
static SCBoolean extendedAutomaton;
static class TLFormulaTRUE truePhi;
static class TLFormulaFALSE falsePhi;
};
class SCStream& operator<< (class SCStream& out, const TLFormulaSet& set);
class SCStream& operator<< (class SCStream& out, const TLFormulaSet* set);
#if _TL_INLINING_
#include "TLFormulaSet.inl.h"
#endif // _TL_INLINING_
#endif // _TL_FORMULASET_H_