Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
InternalCuddDdManager.cpp
Go to the documentation of this file.
1#include "storm/storage/dd/cudd/InternalCuddDdManager.h"
2
3#include "storm/exceptions/MissingLibraryException.h"
4#include "storm/exceptions/NotSupportedException.h"
5#include "storm/settings/SettingsManager.h"
6#include "storm/settings/modules/CuddSettings.h"
7#include "storm/utility/macros.h"
8
9namespace storm {
10namespace dd {
11
12#ifdef STORM_HAVE_CUDD
13InternalDdManager<DdType::CUDD>::InternalDdManager() : cuddManager(), reorderingTechnique(CUDD_REORDER_NONE), numberOfDdVariables(0) {
14 this->cuddManager.SetMaxMemory(
15 static_cast<unsigned long>(storm::settings::getModule<storm::settings::modules::CuddSettings>().getMaximalMemory() * 1024ul * 1024ul));
16
17 auto const& settings = storm::settings::getModule<storm::settings::modules::CuddSettings>();
18 this->cuddManager.SetEpsilon(settings.getConstantPrecision());
19
20 // Now set the selected reordering technique.
21 storm::settings::modules::CuddSettings::ReorderingTechnique reorderingTechniqueAsSetting = settings.getReorderingTechnique();
22 switch (reorderingTechniqueAsSetting) {
23 case storm::settings::modules::CuddSettings::ReorderingTechnique::None:
24 this->reorderingTechnique = CUDD_REORDER_NONE;
25 break;
26 case storm::settings::modules::CuddSettings::ReorderingTechnique::Random:
27 this->reorderingTechnique = CUDD_REORDER_RANDOM;
28 break;
29 case storm::settings::modules::CuddSettings::ReorderingTechnique::RandomPivot:
30 this->reorderingTechnique = CUDD_REORDER_RANDOM_PIVOT;
31 break;
32 case storm::settings::modules::CuddSettings::ReorderingTechnique::Sift:
33 this->reorderingTechnique = CUDD_REORDER_SIFT;
34 break;
35 case storm::settings::modules::CuddSettings::ReorderingTechnique::SiftConv:
36 this->reorderingTechnique = CUDD_REORDER_SIFT_CONVERGE;
37 break;
38 case storm::settings::modules::CuddSettings::ReorderingTechnique::SymmetricSift:
39 this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT;
40 break;
41 case storm::settings::modules::CuddSettings::ReorderingTechnique::SymmetricSiftConv:
42 this->reorderingTechnique = CUDD_REORDER_SYMM_SIFT_CONV;
43 break;
44 case storm::settings::modules::CuddSettings::ReorderingTechnique::GroupSift:
45 this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT;
46 break;
47 case storm::settings::modules::CuddSettings::ReorderingTechnique::GroupSiftConv:
48 this->reorderingTechnique = CUDD_REORDER_GROUP_SIFT_CONV;
49 break;
50 case storm::settings::modules::CuddSettings::ReorderingTechnique::Win2:
51 this->reorderingTechnique = CUDD_REORDER_WINDOW2;
52 break;
53 case storm::settings::modules::CuddSettings::ReorderingTechnique::Win2Conv:
54 this->reorderingTechnique = CUDD_REORDER_WINDOW2_CONV;
55 break;
56 case storm::settings::modules::CuddSettings::ReorderingTechnique::Win3:
57 this->reorderingTechnique = CUDD_REORDER_WINDOW3;
58 break;
59 case storm::settings::modules::CuddSettings::ReorderingTechnique::Win3Conv:
60 this->reorderingTechnique = CUDD_REORDER_WINDOW3_CONV;
61 break;
62 case storm::settings::modules::CuddSettings::ReorderingTechnique::Win4:
63 this->reorderingTechnique = CUDD_REORDER_WINDOW4;
64 break;
65 case storm::settings::modules::CuddSettings::ReorderingTechnique::Win4Conv:
66 this->reorderingTechnique = CUDD_REORDER_WINDOW4_CONV;
67 break;
68 case storm::settings::modules::CuddSettings::ReorderingTechnique::Annealing:
69 this->reorderingTechnique = CUDD_REORDER_ANNEALING;
70 break;
71 case storm::settings::modules::CuddSettings::ReorderingTechnique::Genetic:
72 this->reorderingTechnique = CUDD_REORDER_GENETIC;
73 break;
74 case storm::settings::modules::CuddSettings::ReorderingTechnique::Exact:
75 this->reorderingTechnique = CUDD_REORDER_EXACT;
76 break;
77 }
78
79 this->allowDynamicReordering(settings.isReorderingEnabled());
80}
81
82InternalDdManager<DdType::CUDD>::~InternalDdManager() {
83 // Intentionally left empty.
84}
85
86InternalBdd<DdType::CUDD> InternalDdManager<DdType::CUDD>::getBddOne() const {
87 return InternalBdd<DdType::CUDD>(this, cuddManager.bddOne());
88}
89
90template<typename ValueType>
91InternalAdd<DdType::CUDD, ValueType> InternalDdManager<DdType::CUDD>::getAddOne() const {
92 return InternalAdd<DdType::CUDD, ValueType>(this, cuddManager.addOne());
93}
94
95InternalBdd<DdType::CUDD> InternalDdManager<DdType::CUDD>::getBddZero() const {
96 return InternalBdd<DdType::CUDD>(this, cuddManager.bddZero());
97}
98
99InternalBdd<DdType::CUDD> InternalDdManager<DdType::CUDD>::getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd<DdType::CUDD> const& cube,
100 uint64_t numberOfDdVariables) const {
101 return InternalBdd<DdType::CUDD>(this, cudd::BDD(cuddManager, this->getBddEncodingLessOrEqualThanRec(0, (1ull << numberOfDdVariables) - 1, bound,
102 cube.getCuddDdNode(), numberOfDdVariables)));
103}
104
105DdNodePtr InternalDdManager<DdType::CUDD>::getBddEncodingLessOrEqualThanRec(uint64_t minimalValue, uint64_t maximalValue, uint64_t bound, DdNodePtr cube,
106 uint64_t remainingDdVariables) const {
107 if (maximalValue <= bound) {
108 return Cudd_ReadOne(cuddManager.getManager());
109 } else if (minimalValue > bound) {
110 return Cudd_ReadLogicZero(cuddManager.getManager());
111 }
112
113 STORM_LOG_ASSERT(remainingDdVariables > 0, "Expected more remaining DD variables.");
114 STORM_LOG_ASSERT(!Cudd_IsConstant(cube), "Expected non-constant cube.");
115 uint64_t newRemainingDdVariables = remainingDdVariables - 1;
116 DdNodePtr elseResult =
117 getBddEncodingLessOrEqualThanRec(minimalValue, maximalValue & ~(1ull << newRemainingDdVariables), bound, Cudd_T(cube), newRemainingDdVariables);
118 Cudd_Ref(elseResult);
119 DdNodePtr thenResult =
120 getBddEncodingLessOrEqualThanRec(minimalValue | (1ull << newRemainingDdVariables), maximalValue, bound, Cudd_T(cube), newRemainingDdVariables);
121 Cudd_Ref(thenResult);
122 STORM_LOG_ASSERT(thenResult != elseResult, "Expected different results.");
123
124 bool complemented = Cudd_IsComplement(thenResult);
125 DdNodePtr result =
126 cuddUniqueInter(cuddManager.getManager(), Cudd_NodeReadIndex(cube), Cudd_Regular(thenResult), complemented ? Cudd_Not(elseResult) : elseResult);
127 if (complemented) {
128 result = Cudd_Not(result);
129 }
130 Cudd_Deref(thenResult);
131 Cudd_Deref(elseResult);
132 return result;
133}
134
135template<typename ValueType>
136InternalAdd<DdType::CUDD, ValueType> InternalDdManager<DdType::CUDD>::getAddZero() const {
137 return InternalAdd<DdType::CUDD, ValueType>(this, cuddManager.addZero());
138}
139
140template<typename ValueType>
141InternalAdd<DdType::CUDD, ValueType> InternalDdManager<DdType::CUDD>::getAddUndefined() const {
142 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Undefined values are not supported by CUDD.");
143}
144
145template<typename ValueType>
146InternalAdd<DdType::CUDD, ValueType> InternalDdManager<DdType::CUDD>::getConstant(ValueType const& value) const {
147 return InternalAdd<DdType::CUDD, ValueType>(this, cuddManager.constant(value));
148}
149
150template<>
151InternalAdd<DdType::CUDD, storm::RationalNumber> InternalDdManager<DdType::CUDD>::getConstant(storm::RationalNumber const& value) const {
152 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported.");
153}
154
155std::vector<InternalBdd<DdType::CUDD>> InternalDdManager<DdType::CUDD>::createDdVariables(uint64_t numberOfLayers,
156 boost::optional<uint_fast64_t> const& position) {
157 std::vector<InternalBdd<DdType::CUDD>> result;
158
159 if (position) {
160 for (uint64_t layer = 0; layer < numberOfLayers; ++layer) {
161 result.emplace_back(InternalBdd<DdType::CUDD>(this, cuddManager.bddNewVarAtLevel(position.get() + layer)));
162 }
163 } else {
164 for (uint64_t layer = 0; layer < numberOfLayers; ++layer) {
165 result.emplace_back(InternalBdd<DdType::CUDD>(this, cuddManager.bddVar()));
166 }
167 }
168
169 // Connect the variables so they are not 'torn apart' by dynamic reordering.
170 // Note that MTR_FIXED preserves the order of the layers. While this is not always necessary to preserve,
171 // (for example) the hybrid engine relies on this connection, so we choose MTR_FIXED instead of MTR_DEFAULT.
172 cuddManager.MakeTreeNode(result.front().getIndex(), numberOfLayers, MTR_FIXED);
173
174 // Keep track of the number of variables.
175 numberOfDdVariables += numberOfLayers;
176
177 return result;
178}
179
180bool InternalDdManager<DdType::CUDD>::supportsOrderedInsertion() const {
181 return true;
182}
183
184void InternalDdManager<DdType::CUDD>::allowDynamicReordering(bool value) {
185 if (value) {
186 this->getCuddManager().AutodynEnable(this->reorderingTechnique);
187 } else {
188 this->getCuddManager().AutodynDisable();
189 }
190}
191
192bool InternalDdManager<DdType::CUDD>::isDynamicReorderingAllowed() const {
193 Cudd_ReorderingType type;
194 return this->getCuddManager().ReorderingStatus(&type);
195}
196
197void InternalDdManager<DdType::CUDD>::triggerReordering() {
198 this->getCuddManager().ReduceHeap(this->reorderingTechnique, 0);
199}
200
201void InternalDdManager<DdType::CUDD>::debugCheck() const {
202 this->getCuddManager().CheckKeys();
203 this->getCuddManager().DebugCheck();
204}
205
206void InternalDdManager<DdType::CUDD>::execute(std::function<void()> const& f) const {
207 f();
208}
209
210cudd::Cudd& InternalDdManager<DdType::CUDD>::getCuddManager() {
211 return cuddManager;
212}
213
214cudd::Cudd const& InternalDdManager<DdType::CUDD>::getCuddManager() const {
215 return cuddManager;
216}
217
218uint_fast64_t InternalDdManager<DdType::CUDD>::getNumberOfDdVariables() const {
219 return numberOfDdVariables;
220}
221
222#else
223
224InternalDdManager<DdType::CUDD>::InternalDdManager() {
225 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
226 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
227 "of Storm with CUDD support.");
228}
229
230InternalDdManager<DdType::CUDD>::~InternalDdManager() {
231 // Intentionally left empty.
232}
233
234InternalBdd<DdType::CUDD> InternalDdManager<DdType::CUDD>::getBddOne() const {
235 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
236 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
237 "of Storm with CUDD support.");
238}
239
240template<typename ValueType>
241InternalAdd<DdType::CUDD, ValueType> InternalDdManager<DdType::CUDD>::getAddOne() const {
242 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
243 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
244 "of Storm with CUDD support.");
245}
246
247InternalBdd<DdType::CUDD> InternalDdManager<DdType::CUDD>::getBddZero() const {
248 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
249 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
250 "of Storm with CUDD support.");
251}
252
253InternalBdd<DdType::CUDD> InternalDdManager<DdType::CUDD>::getBddEncodingLessOrEqualThan(uint64_t bound, InternalBdd<DdType::CUDD> const& cube,
254 uint64_t numberOfDdVariables) const {
255 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
256 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
257 "of Storm with CUDD support.");
258}
259
260template<typename ValueType>
261InternalAdd<DdType::CUDD, ValueType> InternalDdManager<DdType::CUDD>::getAddZero() const {
262 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
263 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
264 "of Storm with CUDD support.");
265}
266
267template<typename ValueType>
268InternalAdd<DdType::CUDD, ValueType> InternalDdManager<DdType::CUDD>::getAddUndefined() const {
269 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
270 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
271 "of Storm with CUDD support.");
272}
273
274template<typename ValueType>
275InternalAdd<DdType::CUDD, ValueType> InternalDdManager<DdType::CUDD>::getConstant(ValueType const& value) const {
276 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
277 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
278 "of Storm with CUDD support.");
279}
280
281template<>
282InternalAdd<DdType::CUDD, storm::RationalNumber> InternalDdManager<DdType::CUDD>::getConstant(storm::RationalNumber const& value) const {
283 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
284 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
285 "of Storm with CUDD support.");
286}
287
288std::vector<InternalBdd<DdType::CUDD>> InternalDdManager<DdType::CUDD>::createDdVariables(uint64_t numberOfLayers,
289 boost::optional<uint_fast64_t> const& position) {
290 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
291 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
292 "of Storm with CUDD support.");
293}
294
295bool InternalDdManager<DdType::CUDD>::supportsOrderedInsertion() const {
296 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
297 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
298 "of Storm with CUDD support.");
299}
300
301void InternalDdManager<DdType::CUDD>::allowDynamicReordering(bool value) {
302 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
303 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
304 "of Storm with CUDD support.");
305}
306
307bool InternalDdManager<DdType::CUDD>::isDynamicReorderingAllowed() const {
308 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
309 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
310 "of Storm with CUDD support.");
311}
312
313void InternalDdManager<DdType::CUDD>::triggerReordering() {
314 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
315 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
316 "of Storm with CUDD support.");
317}
318
319void InternalDdManager<DdType::CUDD>::debugCheck() const {
320 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
321 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
322 "of Storm with CUDD support.");
323}
324
325void InternalDdManager<DdType::CUDD>::execute(std::function<void()> const& f) const {
326 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
327 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
328 "of Storm with CUDD support.");
329}
330
331uint_fast64_t InternalDdManager<DdType::CUDD>::getNumberOfDdVariables() const {
332 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
333 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
334 "of Storm with CUDD support.");
335}
336#endif
337
338template InternalAdd<DdType::CUDD, double> InternalDdManager<DdType::CUDD>::getAddOne() const;
339template InternalAdd<DdType::CUDD, uint_fast64_t> InternalDdManager<DdType::CUDD>::getAddOne() const;
340template InternalAdd<DdType::CUDD, storm::RationalNumber> InternalDdManager<DdType::CUDD>::getAddOne() const;
341
342template InternalAdd<DdType::CUDD, double> InternalDdManager<DdType::CUDD>::getAddZero() const;
343template InternalAdd<DdType::CUDD, uint_fast64_t> InternalDdManager<DdType::CUDD>::getAddZero() const;
344template InternalAdd<DdType::CUDD, storm::RationalNumber> InternalDdManager<DdType::CUDD>::getAddZero() const;
345
346template InternalAdd<DdType::CUDD, double> InternalDdManager<DdType::CUDD>::getConstant(double const& value) const;
347template InternalAdd<DdType::CUDD, uint_fast64_t> InternalDdManager<DdType::CUDD>::getConstant(uint_fast64_t const& value) const;
348} // namespace dd
349} // namespace storm
STORM_LOG_ASSERT
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
STORM_LOG_THROW
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30