1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Morgan Deters, Tim King, Andrew Reynolds |
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 |
|
* Enumerators for types. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__TYPE_ENUMERATOR_H |
19 |
|
#define CVC5__THEORY__TYPE_ENUMERATOR_H |
20 |
|
|
21 |
|
#include "base/check.h" |
22 |
|
#include "base/exception.h" |
23 |
|
#include "expr/node.h" |
24 |
|
#include "expr/type_node.h" |
25 |
|
#include "util/integer.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace theory { |
29 |
|
|
30 |
1810 |
class NoMoreValuesException : public Exception { |
31 |
|
public: |
32 |
1810 |
NoMoreValuesException(TypeNode n) |
33 |
1810 |
: Exception("No more values for type `" + n.toString() + "'") |
34 |
|
{ |
35 |
1810 |
} |
36 |
|
};/* class NoMoreValuesException */ |
37 |
|
|
38 |
5218 |
class TypeEnumeratorInterface { |
39 |
|
public: |
40 |
126706 |
TypeEnumeratorInterface(TypeNode type) : d_type(type) {} |
41 |
|
|
42 |
131924 |
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 |
19329 |
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 |
12862 |
class TypeEnumeratorProperties |
71 |
|
{ |
72 |
|
public: |
73 |
12862 |
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 |
137142 |
class TypeEnumeratorBase : public TypeEnumeratorInterface { |
81 |
|
public: |
82 |
|
|
83 |
126706 |
TypeEnumeratorBase(TypeNode type) : |
84 |
126706 |
TypeEnumeratorInterface(type) { |
85 |
126706 |
} |
86 |
|
|
87 |
10499 |
TypeEnumeratorInterface* clone() const override |
88 |
|
{ |
89 |
10499 |
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 |
121339 |
TypeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) |
107 |
121339 |
: d_te(mkTypeEnumerator(type, tep)) |
108 |
|
{ |
109 |
121339 |
} |
110 |
|
|
111 |
10497 |
TypeEnumerator(const TypeEnumerator& te) : |
112 |
10497 |
d_te(te.d_te->clone()) { |
113 |
10497 |
} |
114 |
62 |
TypeEnumerator(TypeEnumeratorInterface* te) : d_te(te){ |
115 |
62 |
} |
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 |
131898 |
~TypeEnumerator() { delete d_te; } |
123 |
176074 |
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(CVC5_ASSERTIONS) && !(defined(__clang__)) |
129 |
176074 |
if(d_te->isFinished()) { |
130 |
|
try { |
131 |
1774 |
**d_te; |
132 |
|
Assert(false) << "expected an NoMoreValuesException to be thrown"; |
133 |
1774 |
} 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 |
174300 |
**d_te; |
144 |
|
} catch(NoMoreValuesException&) { |
145 |
|
Assert(false) << "didn't expect a NoMoreValuesException to be thrown"; |
146 |
|
} |
147 |
|
} |
148 |
|
#endif /* CVC5_ASSERTIONS && !(APPLE || clang) */ |
149 |
176074 |
return d_te->isFinished(); |
150 |
|
} |
151 |
150661 |
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(CVC5_ASSERTIONS) && !(defined(__APPLE__) && defined(__clang__)) |
157 |
|
try { |
158 |
301304 |
Node n = **d_te; |
159 |
150643 |
Assert(n.isConst()) << "Term " << n |
160 |
|
<< " from type enumerator is not constant"; |
161 |
150643 |
Assert(!isFinished()); |
162 |
301286 |
return n; |
163 |
36 |
} catch(NoMoreValuesException&) { |
164 |
18 |
Assert(isFinished()); |
165 |
18 |
throw; |
166 |
|
} |
167 |
|
#else /* CVC5_ASSERTIONS && !(APPLE || clang) */ |
168 |
|
return **d_te; |
169 |
|
#endif /* CVC5_ASSERTIONS && !(APPLE || clang) */ |
170 |
|
} |
171 |
23324 |
TypeEnumerator& operator++() |
172 |
|
{ |
173 |
23324 |
++*d_te; |
174 |
23324 |
return *this; |
175 |
|
} |
176 |
2037 |
TypeEnumerator operator++(int) |
177 |
|
{ |
178 |
2037 |
TypeEnumerator te = *this; |
179 |
2037 |
++*d_te; |
180 |
2037 |
return te; |
181 |
|
} |
182 |
|
|
183 |
2079 |
TypeNode getType() const { return d_te->getType(); } |
184 |
|
};/* class TypeEnumerator */ |
185 |
|
|
186 |
|
} // namespace theory |
187 |
|
} // namespace cvc5 |
188 |
|
|
189 |
|
#endif /* CVC5__THEORY__TYPE_ENUMERATOR_H */ |