GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/type_enumerator.h Lines: 51 55 92.7 %
Date: 2021-03-22 Branches: 41 164 25.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_enumerator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Tim King, Andrew Reynolds
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 Enumerators for types
13
 **
14
 ** Enumerators for types.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__TYPE_ENUMERATOR_H
20
#define CVC4__THEORY__TYPE_ENUMERATOR_H
21
22
#include "base/check.h"
23
#include "base/exception.h"
24
#include "expr/node.h"
25
#include "expr/type_node.h"
26
27
namespace CVC4 {
28
namespace theory {
29
30
3038
class NoMoreValuesException : public Exception {
31
 public:
32
3038
  NoMoreValuesException(TypeNode n)
33
3038
      : Exception("No more values for type `" + n.toString() + "'")
34
  {
35
3038
  }
36
};/* class NoMoreValuesException */
37
38
6452
class TypeEnumeratorInterface {
39
 public:
40
191135
  TypeEnumeratorInterface(TypeNode type) : d_type(type) {}
41
42
197587
  virtual ~TypeEnumeratorInterface() {}
43
44
  /** Is this enumerator out of constants to enumerate? */
45
  virtual bool isFinished() = 0;
46
47
  /**
48
   * Get the current constant of this type.
49
   *
50
   * @throws NoMoreValuesException if no such constant exists.
51
   */
52
  virtual Node operator*() = 0;
53
54
  /** Increment the pointer to the next available constant. */
55
  virtual TypeEnumeratorInterface& operator++() = 0;
56
57
  /** Clone this enumerator. */
58
  virtual TypeEnumeratorInterface* clone() const = 0;
59
60
  /** Get the type from which we're enumerating constants. */
61
32153
  TypeNode getType() const { return d_type; }
62
63
 private:
64
  const TypeNode d_type;
65
}; /* class TypeEnumeratorInterface */
66
67
// AJR: This class stores particular information that is relevant to type enumeration.
68
//      For finite model finding, we set d_fixed_usort=true,
69
//      and store the finite cardinality bounds for each uninterpreted sort encountered in the model.
70
18942
class TypeEnumeratorProperties
71
{
72
public:
73
18942
  TypeEnumeratorProperties() : d_fixed_usort_card(false){}
74
  Integer getFixedCardinality( TypeNode tn ) { return d_fixed_card[tn]; }
75
  bool d_fixed_usort_card;
76
  std::map< TypeNode, Integer > d_fixed_card;
77
};
78
79
template <class T>
80
204039
class TypeEnumeratorBase : public TypeEnumeratorInterface {
81
public:
82
83
191135
  TypeEnumeratorBase(TypeNode type) :
84
191135
    TypeEnumeratorInterface(type) {
85
191135
  }
86
87
16937
  TypeEnumeratorInterface* clone() const override
88
  {
89
16937
    return new T(static_cast<const T&>(*this));
90
  }
91
92
};/* class TypeEnumeratorBase */
93
94
/** Type enumerator class.
95
 * Enumerates values for a type.
96
 * Its constructor takes the type to enumerate and a pointer to a
97
 * TypeEnumeratorProperties class, which this type enumerator does not own.
98
 */
99
class TypeEnumerator {
100
  TypeEnumeratorInterface* d_te;
101
102
  static TypeEnumeratorInterface* mkTypeEnumerator(
103
      TypeNode type, TypeEnumeratorProperties* tep);
104
105
 public:
106
180554
  TypeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
107
180554
      : d_te(mkTypeEnumerator(type, tep))
108
  {
109
180554
  }
110
111
16935
  TypeEnumerator(const TypeEnumerator& te) :
112
16935
    d_te(te.d_te->clone()) {
113
16935
  }
114
74
  TypeEnumerator(TypeEnumeratorInterface* te) : d_te(te){
115
74
  }
116
2
  TypeEnumerator& operator=(const TypeEnumerator& te) {
117
2
    delete d_te;
118
2
    d_te = te.d_te->clone();
119
2
    return *this;
120
  }
121
122
197563
  ~TypeEnumerator() { delete d_te; }
123
299856
  bool isFinished()
124
  {
125
// On Mac clang, there appears to be a code generation bug in an exception
126
// block here.  For now, there doesn't appear a good workaround; just disable
127
// assertions on that setup.
128
#if defined(CVC4_ASSERTIONS) && !(defined(__clang__))
129
299856
    if(d_te->isFinished()) {
130
      try {
131
3002
        **d_te;
132
        Assert(false) << "expected an NoMoreValuesException to be thrown";
133
3002
      } catch(NoMoreValuesException&) {
134
        // ignore the exception, we're just asserting that it would be thrown
135
        //
136
        // This block can crash on clang 3.0 on Mac OS, perhaps related to
137
        // bug:  http://llvm.org/bugs/show_bug.cgi?id=13359
138
        //
139
        // Hence the #if !(defined(__APPLE__) && defined(__clang__)) above
140
      }
141
    } else {
142
      try {
143
296854
        **d_te;
144
      } catch(NoMoreValuesException&) {
145
        Assert(false) << "didn't expect a NoMoreValuesException to be thrown";
146
      }
147
    }
148
#endif /* CVC4_ASSERTIONS && !(APPLE || clang) */
149
299856
    return d_te->isFinished();
150
  }
151
239204
  Node operator*()
152
  {
153
// On Mac clang, there appears to be a code generation bug in an exception
154
// block above (and perhaps here, too).  For now, there doesn't appear a
155
// good workaround; just disable assertions on that setup.
156
#if defined(CVC4_ASSERTIONS) && !(defined(__APPLE__) && defined(__clang__))
157
    try {
158
478390
      Node n = **d_te;
159
239186
      Assert(n.isConst()) << "Term " << n
160
                          << " from type enumerator is not constant";
161
239186
      Assert(!isFinished());
162
478372
      return n;
163
36
    } catch(NoMoreValuesException&) {
164
18
      Assert(isFinished());
165
18
      throw;
166
    }
167
#else /* CVC4_ASSERTIONS && !(APPLE || clang) */
168
    return **d_te;
169
#endif /* CVC4_ASSERTIONS && !(APPLE || clang) */
170
  }
171
58386
  TypeEnumerator& operator++()
172
  {
173
58386
    ++*d_te;
174
58386
    return *this;
175
  }
176
2040
  TypeEnumerator operator++(int)
177
  {
178
2040
    TypeEnumerator te = *this;
179
2040
    ++*d_te;
180
2040
    return te;
181
  }
182
183
2082
  TypeNode getType() const { return d_te->getType(); }
184
};/* class TypeEnumerator */
185
186
}/* CVC4::theory namespace */
187
}/* CVC4 namespace */
188
189
#endif /* CVC4__THEORY__TYPE_ENUMERATOR_H */