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