GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/booleans/type_enumerator.h Lines: 19 19 100.0 %
Date: 2021-03-22 Branches: 14 35 40.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_enumerator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Tim King, Mathias Preiner
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief An enumerator for Booleans
13
 **
14
 ** An enumerator for Booleans.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H
20
#define CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H
21
22
#include "theory/type_enumerator.h"
23
#include "expr/type_node.h"
24
#include "expr/kind.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace booleans {
29
30
4430
class BooleanEnumerator : public TypeEnumeratorBase<BooleanEnumerator> {
31
  enum { FALSE, TRUE, DONE } d_value;
32
33
 public:
34
1879
  BooleanEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
35
1879
      : TypeEnumeratorBase<BooleanEnumerator>(type), d_value(FALSE)
36
  {
37
1879
    Assert(type.getKind() == kind::TYPE_CONSTANT
38
           && type.getConst<TypeConstant>() == BOOLEAN_TYPE);
39
1879
  }
40
41
4368
  Node operator*() override {
42
4368
    switch(d_value) {
43
4041
    case FALSE:
44
4041
      return NodeManager::currentNM()->mkConst(false);
45
244
    case TRUE:
46
244
      return NodeManager::currentNM()->mkConst(true);
47
83
    default:
48
83
      throw NoMoreValuesException(getType());
49
    }
50
  }
51
52
259
  BooleanEnumerator& operator++() override
53
  {
54
    // sequence is FALSE, TRUE
55
259
    if(d_value == FALSE) {
56
185
      d_value = TRUE;
57
    } else {
58
74
      d_value = DONE;
59
    }
60
259
    return *this;
61
  }
62
63
4684
  bool isFinished() override { return d_value == DONE; }
64
};/* class BooleanEnumerator */
65
66
}/* CVC4::theory::booleans namespace */
67
}/* CVC4::theory namespace */
68
}/* CVC4 namespace */
69
70
#endif /* CVC4__THEORY__BOOLEANS__TYPE_ENUMERATOR_H */