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
/*
* 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 ClauseQueue.hpp
* Defines class ClauseQueue.
*
* @since 30/12/2007 Manchester
*/
#ifndef __ClauseQueue__
#define __ClauseQueue__
#if VDEBUG
#include <ostream>
#endif
#include "Debug/Assertion.hpp"
#include "Lib/Reflection.hpp"
namespace Kernel {
class Clause;
/**
* A clause queue organised as a skip list. The comparison of elements
* is made using the virtual function compare.
* @since 30/12/2007 Manchester
*/
class ClauseQueue
{
public:
ClauseQueue();
virtual ~ClauseQueue();
void insert(Clause*);
bool remove(Clause*);
void removeAll();
Clause* pop();
/** True if the queue is empty */
bool isEmpty() const
{ return _left->nodes[0] == 0; }
void output(std::ostream&) const;
friend class Iterator;
protected:
/** comparison of clauses */
virtual bool lessThan(Clause*,Clause*) = 0;
/** Nodes in the skip list */
class Node {
public:
/** Clause at this node */
Clause* clause;
/** Links to other nodes on the right, can be of any length */
Node* nodes[1];
};
/** Height of the leftmost node minus 1 */
unsigned _height;
/** the leftmost node with the dummy key and value */
Node* _left;
public:
/** Iterator over the queue
* @since 04/01/2008 flight Manchester-Murcia
*/
class Iterator {
public:
DECL_ELEMENT_TYPE(Clause*);
/** Create a new iterator */
inline explicit Iterator(ClauseQueue& queue)
: _current(queue._left)
{}
/** true if there is a next clause */
inline bool hasNext() const
{ return _current->nodes[0]; }
/** return the next clause */
inline Clause* next()
{
_current = _current->nodes[0];
ASS(_current);
return _current->clause;
}
private:
/** Current node */
Node* _current;
}; // class ClauseQueue::Iterator
// class DelIterator {
// public:
// explicit DelIterator(ClauseQueue& queue)
// { }
//
// bool hasNext()
// { }
//
// Clause* next()
// { }
//
// void del()
// { }
// private:
// };
}; // class ClauseQueue
} // namespace Kernel
#endif