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
|
/********************* */
/*! \file node_self_iterator.h
** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Iterator supporting Node "self-iteration"
**
** Iterator supporting Node "self-iteration."
**/
#include "cvc4_private.h"
#ifndef __CVC4__EXPR__NODE_SELF_ITERATOR_H
#define __CVC4__EXPR__NODE_SELF_ITERATOR_H
#include <iterator>
#include "util/cvc4_assert.h"
#include "expr/node.h"
namespace CVC4 {
namespace expr {
class NodeSelfIterator : std::iterator<std::input_iterator_tag, Node> {
Node d_node;
Node::const_iterator d_child;
public:
static NodeSelfIterator self(TNode n);
static NodeSelfIterator selfEnd(TNode n);
NodeSelfIterator();
NodeSelfIterator(Node n);
NodeSelfIterator(TNode n);
NodeSelfIterator(const NodeSelfIterator& i);
NodeSelfIterator(Node::const_iterator i);
NodeSelfIterator(TNode::const_iterator i);
Node operator*() const;
NodeSelfIterator& operator++();
NodeSelfIterator operator++(int);
bool operator==(NodeSelfIterator i) const;
bool operator!=(NodeSelfIterator i) const;
};/* class NodeSelfIterator */
inline NodeSelfIterator NodeSelfIterator::self(TNode n) {
Assert(!n.isNull(), "Self-iteration over null nodes not permitted.");
return NodeSelfIterator(n);
}
inline NodeSelfIterator NodeSelfIterator::selfEnd(TNode n) {
Assert(!n.isNull(), "Self-iteration over null nodes not permitted.");
return NodeSelfIterator(n.end());
}
inline NodeSelfIterator::NodeSelfIterator() :
d_node(),
d_child() {
}
inline NodeSelfIterator::NodeSelfIterator(Node node) :
d_node(node),
d_child() {
Assert(!node.isNull(), "Self-iteration over null nodes not permitted.");
}
inline NodeSelfIterator::NodeSelfIterator(TNode node) :
d_node(node),
d_child() {
Assert(!node.isNull(), "Self-iteration over null nodes not permitted.");
}
inline NodeSelfIterator::NodeSelfIterator(const NodeSelfIterator& i) :
d_node(i.d_node),
d_child(i.d_child) {
}
inline NodeSelfIterator::NodeSelfIterator(Node::const_iterator i) :
d_node(),
d_child(i) {
}
inline NodeSelfIterator::NodeSelfIterator(TNode::const_iterator i) :
d_node(),
d_child(i) {
}
inline Node NodeSelfIterator::operator*() const {
return d_node.isNull() ? *d_child : d_node;
}
inline NodeSelfIterator& NodeSelfIterator::operator++() {
if(d_node.isNull()) {
++d_child;
} else {
d_child = d_node.end();
d_node = Node::null();
}
return *this;
}
inline NodeSelfIterator NodeSelfIterator::operator++(int) {
NodeSelfIterator i = *this;
++*this;
return i;
}
inline bool NodeSelfIterator::operator==(NodeSelfIterator i) const {
return d_node == i.d_node && d_child == i.d_child;
}
inline bool NodeSelfIterator::operator!=(NodeSelfIterator i) const {
return !(*this == i);
}
}/* CVC4::expr namespace */
}/* CVC4 namespace */
#endif /* __CVC4__EXPR__NODE_SELF_ITERATOR_H */
|
