GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node_self_iterator.h Lines: 40 43 93.0 %
Date: 2021-05-22 Branches: 23 94 24.5 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Morgan Deters, Mathias Preiner, Andres Noetzli
4
 *
5
 * This file is part of the cvc5 project.
6
 *
7
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 * in the top-level source directory and their institutional affiliations.
9
 * All rights reserved.  See the file COPYING in the top-level source
10
 * directory for licensing information.
11
 * ****************************************************************************
12
 *
13
 * Iterator supporting Node "self-iteration."
14
 */
15
16
#include "cvc5_private.h"
17
18
#ifndef CVC5__EXPR__NODE_SELF_ITERATOR_H
19
#define CVC5__EXPR__NODE_SELF_ITERATOR_H
20
21
#include <iterator>
22
23
#include "base/check.h"
24
#include "expr/node.h"
25
26
namespace cvc5 {
27
namespace expr {
28
29
4502960132
class NodeSelfIterator : public std::iterator<std::input_iterator_tag, Node> {
30
  Node d_node;
31
  Node::const_iterator d_child;
32
33
public:
34
  static NodeSelfIterator self(TNode n);
35
  static NodeSelfIterator selfEnd(TNode n);
36
37
  NodeSelfIterator();
38
  NodeSelfIterator(Node n);
39
  NodeSelfIterator(TNode n);
40
  NodeSelfIterator(const NodeSelfIterator& i);
41
42
  NodeSelfIterator(Node::const_iterator i);
43
  NodeSelfIterator(TNode::const_iterator i);
44
45
  Node operator*() const;
46
  NodeSelfIterator& operator++();
47
  NodeSelfIterator operator++(int);
48
49
  bool operator==(NodeSelfIterator i) const;
50
  bool operator!=(NodeSelfIterator i) const;
51
52
};/* class NodeSelfIterator */
53
54
268590882
inline NodeSelfIterator NodeSelfIterator::self(TNode n) {
55
268590882
  Assert(!n.isNull()) << "Self-iteration over null nodes not permitted.";
56
268590882
  return NodeSelfIterator(n);
57
}
58
59
241402247
inline NodeSelfIterator NodeSelfIterator::selfEnd(TNode n) {
60
241402247
  Assert(!n.isNull()) << "Self-iteration over null nodes not permitted.";
61
241402247
  return NodeSelfIterator(n.end());
62
}
63
64
inline NodeSelfIterator::NodeSelfIterator() :
65
  d_node(),
66
  d_child() {
67
}
68
69
2
inline NodeSelfIterator::NodeSelfIterator(Node node) :
70
  d_node(node),
71
2
  d_child() {
72
2
  Assert(!node.isNull()) << "Self-iteration over null nodes not permitted.";
73
2
}
74
75
268590882
inline NodeSelfIterator::NodeSelfIterator(TNode node) :
76
  d_node(node),
77
268590882
  d_child() {
78
268590882
  Assert(!node.isNull()) << "Self-iteration over null nodes not permitted.";
79
268590882
}
80
81
3854491149
inline NodeSelfIterator::NodeSelfIterator(const NodeSelfIterator& i) :
82
  d_node(i.d_node),
83
3854491149
  d_child(i.d_child) {
84
3854491149
}
85
86
123632491
inline NodeSelfIterator::NodeSelfIterator(Node::const_iterator i) :
87
  d_node(),
88
123632491
  d_child(i) {
89
123632491
}
90
91
241402247
inline NodeSelfIterator::NodeSelfIterator(TNode::const_iterator i) :
92
  d_node(),
93
241402247
  d_child(i) {
94
241402247
}
95
96
240945821
inline Node NodeSelfIterator::operator*() const {
97
240945821
  return d_node.isNull() ? *d_child : d_node;
98
}
99
100
317865671
inline NodeSelfIterator& NodeSelfIterator::operator++() {
101
317865671
  if(d_node.isNull()) {
102
88326718
    ++d_child;
103
  } else {
104
229538953
    d_child = d_node.end();
105
229538953
    d_node = Node::null();
106
  }
107
317865671
  return *this;
108
}
109
110
4
inline NodeSelfIterator NodeSelfIterator::operator++(int) {
111
4
  NodeSelfIterator i = *this;
112
4
  ++*this;
113
4
  return i;
114
}
115
116
797871174
inline bool NodeSelfIterator::operator==(NodeSelfIterator i) const {
117
797871174
  return d_node == i.d_node && d_child == i.d_child;
118
}
119
120
443449635
inline bool NodeSelfIterator::operator!=(NodeSelfIterator i) const {
121
443449635
  return !(*this == i);
122
}
123
124
}  // namespace expr
125
}  // namespace cvc5
126
127
#endif /* CVC5__EXPR__NODE_SELF_ITERATOR_H */