Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
InternalCuddAdd.cpp
Go to the documentation of this file.
1#include "storm/storage/dd/cudd/InternalCuddAdd.h"
2
3#include "storm/exceptions/MissingLibraryException.h"
4#include "storm/exceptions/NotSupportedException.h"
5#include "storm/storage/BitVector.h"
6#include "storm/storage/SparseMatrix.h"
7#include "storm/storage/dd/Odd.h"
8#include "storm/storage/dd/cudd/CuddAddIterator.h"
9#include "storm/storage/dd/cudd/InternalCuddBdd.h"
10#include "storm/storage/dd/cudd/InternalCuddDdManager.h"
11#include "storm/utility/constants.h"
12#include "storm/utility/macros.h"
13
14namespace storm {
15namespace dd {
16
17#ifdef STORM_HAVE_CUDD
18template<typename ValueType>
19InternalAdd<DdType::CUDD, ValueType>::InternalAdd(InternalDdManager<DdType::CUDD> const* ddManager, cudd::ADD cuddAdd)
20 : ddManager(ddManager), cuddAdd(cuddAdd) {
21 // Intentionally left empty.
22}
23
24template<typename ValueType>
25bool InternalAdd<DdType::CUDD, ValueType>::operator==(InternalAdd<DdType::CUDD, ValueType> const& other) const {
26 return this->getCuddAdd() == other.getCuddAdd();
27}
28
29template<typename ValueType>
30bool InternalAdd<DdType::CUDD, ValueType>::operator!=(InternalAdd<DdType::CUDD, ValueType> const& other) const {
31 return !(*this == other);
32}
33
34template<typename ValueType>
35InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator+(InternalAdd<DdType::CUDD, ValueType> const& other) const {
36 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd() + other.getCuddAdd());
37}
38
39template<typename ValueType>
40InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator+=(InternalAdd<DdType::CUDD, ValueType> const& other) {
41 this->cuddAdd = this->getCuddAdd() + other.getCuddAdd();
42 return *this;
43}
44
45template<typename ValueType>
46InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator*(InternalAdd<DdType::CUDD, ValueType> const& other) const {
47 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd() * other.getCuddAdd());
48}
49
50template<typename ValueType>
51InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator*=(InternalAdd<DdType::CUDD, ValueType> const& other) {
52 this->cuddAdd = this->getCuddAdd() * other.getCuddAdd();
53 return *this;
54}
55
56template<typename ValueType>
57InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator-(InternalAdd<DdType::CUDD, ValueType> const& other) const {
58 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd() - other.getCuddAdd());
59}
60
61template<typename ValueType>
62InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator-=(InternalAdd<DdType::CUDD, ValueType> const& other) {
63 this->cuddAdd = this->getCuddAdd() - other.getCuddAdd();
64 return *this;
65}
66
67template<typename ValueType>
68InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator/(InternalAdd<DdType::CUDD, ValueType> const& other) const {
69 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Divide(other.getCuddAdd()));
70}
71
72template<typename ValueType>
73InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator/=(InternalAdd<DdType::CUDD, ValueType> const& other) {
74 this->cuddAdd = this->getCuddAdd().Divide(other.getCuddAdd());
75 return *this;
76}
77
78template<typename ValueType>
79InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::equals(InternalAdd<DdType::CUDD, ValueType> const& other) const {
80 return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().EqualsBdd(other.getCuddAdd()));
81}
82
83template<typename ValueType>
84InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::notEquals(InternalAdd<DdType::CUDD, ValueType> const& other) const {
85 return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().NotEqualsBdd(other.getCuddAdd()));
86}
87
88template<typename ValueType>
89InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::less(InternalAdd<DdType::CUDD, ValueType> const& other) const {
90 return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().LessThanBdd(other.getCuddAdd()));
91}
92
93template<typename ValueType>
94InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::lessOrEqual(InternalAdd<DdType::CUDD, ValueType> const& other) const {
95 return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().LessThanOrEqualBdd(other.getCuddAdd()));
96}
97
98template<typename ValueType>
99InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greater(InternalAdd<DdType::CUDD, ValueType> const& other) const {
100 return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().GreaterThanBdd(other.getCuddAdd()));
101}
102
103template<typename ValueType>
104InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greaterOrEqual(InternalAdd<DdType::CUDD, ValueType> const& other) const {
105 return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().GreaterThanOrEqualBdd(other.getCuddAdd()));
106}
107
108template<typename ValueType>
109InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::pow(InternalAdd<DdType::CUDD, ValueType> const& other) const {
110 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Pow(other.getCuddAdd()));
111}
112
113template<typename ValueType>
114InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::mod(InternalAdd<DdType::CUDD, ValueType> const& other) const {
115 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Mod(other.getCuddAdd()));
116}
117
118template<typename ValueType>
119InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::logxy(InternalAdd<DdType::CUDD, ValueType> const& other) const {
120 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().LogXY(other.getCuddAdd()));
121}
122
123template<typename ValueType>
124InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::floor() const {
125 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Floor());
126}
127
128template<typename ValueType>
129InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::ceil() const {
130 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Ceil());
131}
132
133template<typename ValueType>
134InternalAdd<DdType::CUDD, storm::RationalNumber> InternalAdd<DdType::CUDD, ValueType>::sharpenKwekMehlhorn(size_t /*precision*/) const {
135 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported");
136}
137
138template<typename ValueType>
139InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::minimum(InternalAdd<DdType::CUDD, ValueType> const& other) const {
140 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Minimum(other.getCuddAdd()));
141}
142
143template<typename ValueType>
144InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::maximum(InternalAdd<DdType::CUDD, ValueType> const& other) const {
145 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Maximum(other.getCuddAdd()));
146}
147
148template<typename ValueType>
149template<typename TargetValueType>
150typename std::enable_if<std::is_same<ValueType, TargetValueType>::value, InternalAdd<DdType::CUDD, TargetValueType>>
151
152 ::type InternalAdd<DdType::CUDD, ValueType>::toValueType() const {
153 return *this;
154}
155
156template<typename ValueType>
157template<typename TargetValueType>
158typename std::enable_if<!std::is_same<ValueType, TargetValueType>::value, InternalAdd<DdType::CUDD, TargetValueType>>
159
160 ::type InternalAdd<DdType::CUDD, ValueType>::toValueType() const {
161 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported");
162}
163
164template<typename ValueType>
165InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::sumAbstract(InternalBdd<DdType::CUDD> const& cube) const {
166 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().ExistAbstract(cube.toAdd<ValueType>().getCuddAdd()));
167}
168
169template<typename ValueType>
170InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::minAbstract(InternalBdd<DdType::CUDD> const& cube) const {
171 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MinAbstract(cube.toAdd<ValueType>().getCuddAdd()));
172}
173
174template<typename ValueType>
175InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::minAbstractRepresentative(InternalBdd<DdType::CUDD> const& cube) const {
176 return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd<ValueType>().getCuddAdd()));
177}
178
179template<typename ValueType>
180InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::maxAbstract(InternalBdd<DdType::CUDD> const& cube) const {
181 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MaxAbstract(cube.toAdd<ValueType>().getCuddAdd()));
182}
183
184template<typename ValueType>
185InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::maxAbstractRepresentative(InternalBdd<DdType::CUDD> const& cube) const {
186 return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().MaxAbstractRepresentative(cube.toAdd<ValueType>().getCuddAdd()));
187}
188
189template<typename ValueType>
190bool InternalAdd<DdType::CUDD, ValueType>::equalModuloPrecision(InternalAdd<DdType::CUDD, ValueType> const& other, ValueType const& precision,
191 bool relative) const {
192 if (relative) {
193 return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision);
194 } else {
195 return this->getCuddAdd().EqualSupNorm(other.getCuddAdd(), precision);
196 }
197}
198
199template<>
200bool InternalAdd<DdType::CUDD, storm::RationalNumber>::equalModuloPrecision(InternalAdd<DdType::CUDD, storm::RationalNumber> const& /*other*/,
201 storm::RationalNumber const& /*precision*/, bool /*relative*/) const {
202 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported.");
203}
204
205template<typename ValueType>
206InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::swapVariables(std::vector<InternalBdd<DdType::CUDD>> const& from,
207 std::vector<InternalBdd<DdType::CUDD>> const& to) const {
208 std::vector<cudd::ADD> fromAdd;
209 std::vector<cudd::ADD> toAdd;
210 STORM_LOG_ASSERT(fromAdd.size() == toAdd.size(), "Sizes of vectors do not match.");
211 for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) {
212 fromAdd.push_back(it1->getCuddBdd().Add());
213 toAdd.push_back(it2->getCuddBdd().Add());
214 }
215 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().SwapVariables(fromAdd, toAdd));
216}
217
218template<typename ValueType>
219InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::permuteVariables(std::vector<InternalBdd<DdType::CUDD>> const& from,
220 std::vector<InternalBdd<DdType::CUDD>> const& to) const {
221 // Build the full permutation.
222 uint64_t numberOfVariables = ddManager->getCuddManager().ReadSize();
223 int* permutation = new int[numberOfVariables];
224 for (uint64_t variable = 0; variable < numberOfVariables; ++variable) {
225 permutation[variable] = variable;
226 }
227
228 for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) {
229 permutation[it1->getIndex()] = it2->getIndex();
230 }
231 InternalAdd<DdType::CUDD, ValueType> result(ddManager, this->getCuddAdd().Permute(permutation));
232
233 delete[] permutation;
234 return result;
235}
236
237template<typename ValueType>
238InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::multiplyMatrix(
239 InternalAdd<DdType::CUDD, ValueType> const& otherMatrix, std::vector<InternalBdd<DdType::CUDD>> const& summationDdVariables) const {
240 // Create the CUDD summation variables.
241 std::vector<cudd::ADD> summationAdds;
242 for (auto const& ddVariable : summationDdVariables) {
243 summationAdds.push_back(ddVariable.toAdd<ValueType>().getCuddAdd());
244 }
245
246 // return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().TimesPlus(otherMatrix.getCuddAdd(), summationAdds));
247 // return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Triangle(otherMatrix.getCuddAdd(), summationAdds));
248 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationAdds));
249}
250
251template<typename ValueType>
252InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::multiplyMatrix(
253 InternalBdd<DdType::CUDD> const& otherMatrix, std::vector<InternalBdd<DdType::CUDD>> const& summationDdVariables) const {
254 return this->multiplyMatrix(otherMatrix.template toAdd<ValueType>(), summationDdVariables);
255}
256
257template<typename ValueType>
258InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greater(ValueType const& value) const {
259 return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().BddStrictThreshold(value));
260}
261
262template<>
263InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, storm::RationalNumber>::greater(storm::RationalNumber const& value) const {
264 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported.");
265}
266
267template<typename ValueType>
268InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greaterOrEqual(ValueType const& value) const {
269 return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().BddThreshold(value));
270}
271
272template<>
273InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, storm::RationalNumber>::greaterOrEqual(storm::RationalNumber const& value) const {
274 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported.");
275}
276
277template<typename ValueType>
278InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::less(ValueType const& value) const {
279 return InternalBdd<DdType::CUDD>(ddManager, ~this->getCuddAdd().BddThreshold(value));
280}
281
282template<>
283InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, storm::RationalNumber>::less(storm::RationalNumber const& value) const {
284 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported.");
285}
286
287template<typename ValueType>
288InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::lessOrEqual(ValueType const& value) const {
289 return InternalBdd<DdType::CUDD>(ddManager, ~this->getCuddAdd().BddStrictThreshold(value));
290}
291
292template<>
293InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, storm::RationalNumber>::lessOrEqual(storm::RationalNumber const& value) const {
294 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported.");
295}
296
297template<typename ValueType>
298InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::notZero() const {
299 return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().BddPattern());
300}
301
302template<typename ValueType>
303InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::constrain(InternalAdd<DdType::CUDD, ValueType> const& constraint) const {
304 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Constrain(constraint.getCuddAdd()));
305}
306
307template<typename ValueType>
308InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::restrict(InternalAdd<DdType::CUDD, ValueType> const& constraint) const {
309 return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Restrict(constraint.getCuddAdd()));
310}
311
312template<typename ValueType>
313InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::getSupport() const {
314 return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().Support());
315}
316
317template<typename ValueType>
318uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getNonZeroCount(uint_fast64_t numberOfDdVariables) const {
319 // If the number of DD variables is zero, CUDD returns a number greater 0 for constant nodes different from
320 // zero, which is not the behaviour we expect.
321 if (numberOfDdVariables == 0) {
322 return 0;
323 }
324 return static_cast<uint_fast64_t>(this->getCuddAdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
325}
326
327template<typename ValueType>
328uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getLeafCount() const {
329 return static_cast<uint_fast64_t>(this->getCuddAdd().CountLeaves());
330}
331
332template<typename ValueType>
333uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getNodeCount() const {
334 return static_cast<uint_fast64_t>(this->getCuddAdd().nodeCount());
335}
336
337template<typename ValueType>
338ValueType InternalAdd<DdType::CUDD, ValueType>::getMin() const {
339 cudd::ADD constantMinAdd = this->getCuddAdd().FindMin();
340 return storm::utility::convertNumber<ValueType>(Cudd_V(constantMinAdd.getNode()));
341}
342
343template<typename ValueType>
344ValueType InternalAdd<DdType::CUDD, ValueType>::getMax() const {
345 cudd::ADD constantMaxAdd = this->getCuddAdd().FindMax();
346 return storm::utility::convertNumber<ValueType>(Cudd_V(constantMaxAdd.getNode()));
347}
348
349template<typename ValueType>
350ValueType InternalAdd<DdType::CUDD, ValueType>::getValue() const {
351 return storm::utility::convertNumber<ValueType>(Cudd_V(this->getCuddAdd().getNode()));
352}
353
354template<typename ValueType>
355bool InternalAdd<DdType::CUDD, ValueType>::isOne() const {
356 return this->getCuddAdd().IsOne();
357}
358
359template<typename ValueType>
360bool InternalAdd<DdType::CUDD, ValueType>::isZero() const {
361 return this->getCuddAdd().IsZero();
362}
363
364template<typename ValueType>
365bool InternalAdd<DdType::CUDD, ValueType>::isConstant() const {
366 return Cudd_IsConstant(this->getCuddAdd().getNode());
367}
368
369template<typename ValueType>
370uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getIndex() const {
371 return static_cast<uint_fast64_t>(this->getCuddAdd().NodeReadIndex());
372}
373
374template<typename ValueType>
375uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getLevel() const {
376 return static_cast<uint_fast64_t>(ddManager->getCuddManager().ReadPerm(this->getIndex()));
377}
378
379template<typename ValueType>
380void InternalAdd<DdType::CUDD, ValueType>::exportToDot(std::string const& filename, std::vector<std::string> const& ddVariableNamesAsStrings,
381 bool showVariablesIfPossible) const {
382 // Build the name input of the DD.
383 std::vector<char*> ddNames;
384 std::string ddName("f");
385 ddNames.push_back(new char[ddName.size() + 1]);
386 std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back());
387
388 // Now build the variables names.
389 std::vector<char*> ddVariableNames;
390 for (auto const& element : ddVariableNamesAsStrings) {
391 ddVariableNames.push_back(new char[element.size() + 1]);
392 std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back());
393 }
394
395 // Open the file, dump the DD and close it again.
396 FILE* filePointer = fopen(filename.c_str(), "w");
397 std::vector<cudd::ADD> cuddAddVector = {this->getCuddAdd()};
398 if (showVariablesIfPossible) {
399 ddManager->getCuddManager().DumpDot(cuddAddVector, ddVariableNames.data(), &ddNames[0], filePointer);
400 } else {
401 ddManager->getCuddManager().DumpDot(cuddAddVector, nullptr, &ddNames[0], filePointer);
402 }
403 fclose(filePointer);
404
405 // Finally, delete the names.
406 for (char* element : ddNames) {
407 delete[] element;
408 }
409 for (char* element : ddVariableNames) {
410 delete[] element;
411 }
412}
413
414template<typename ValueType>
415void InternalAdd<DdType::CUDD, ValueType>::exportToText(std::string const&) const {
416 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported");
417}
418
419template<typename ValueType>
420AddIterator<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::begin(DdManager<DdType::CUDD> const& fullDdManager, InternalBdd<DdType::CUDD> const&,
421 uint_fast64_t, std::set<storm::expressions::Variable> const& metaVariables,
422 bool enumerateDontCareMetaVariables) const {
423 int* cube;
424 double value;
425 DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value);
426 return AddIterator<DdType::CUDD, ValueType>(fullDdManager, generator, cube, storm::utility::convertNumber<ValueType>(value),
427 (Cudd_IsGenEmpty(generator) != 0), &metaVariables, enumerateDontCareMetaVariables);
428}
429
430template<typename ValueType>
431AddIterator<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::end(DdManager<DdType::CUDD> const& fullDdManager) const {
432 return AddIterator<DdType::CUDD, ValueType>(fullDdManager, nullptr, nullptr, 0, true, nullptr, false);
433}
434
435template<typename ValueType>
436cudd::ADD InternalAdd<DdType::CUDD, ValueType>::getCuddAdd() const {
437 return this->cuddAdd;
438}
439
440template<typename ValueType>
441DdNode* InternalAdd<DdType::CUDD, ValueType>::getCuddDdNode() const {
442 return this->getCuddAdd().getNode();
443}
444
445template<typename ValueType>
446std::string InternalAdd<DdType::CUDD, ValueType>::getStringId() const {
447 std::stringstream ss;
448 ss << this->getCuddDdNode();
449 return ss.str();
450}
451
452template<typename ValueType>
453Odd InternalAdd<DdType::CUDD, ValueType>::createOdd(std::vector<uint_fast64_t> const& ddVariableIndices) const {
454 // Prepare a unique table for each level that keeps the constructed ODD nodes unique.
455 std::vector<std::unordered_map<DdNode*, std::shared_ptr<Odd>>> uniqueTableForLevels(ddVariableIndices.size() + 1);
456
457 // Now construct the ODD structure from the ADD.
458 std::shared_ptr<Odd> rootOdd =
459 createOddRec(this->getCuddDdNode(), ddManager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
460
461 // Return a copy of the root node to remove the shared_ptr encapsulation.
462 return Odd(*rootOdd);
463}
464
465template<typename ValueType>
466std::shared_ptr<Odd> InternalAdd<DdType::CUDD, ValueType>::createOddRec(DdNode* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel,
467 uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices,
468 std::vector<std::unordered_map<DdNode*, std::shared_ptr<Odd>>>& uniqueTableForLevels) {
469 // Check whether the ODD for this node has already been computed (for this level) and if so, return this instead.
470 auto const& iterator = uniqueTableForLevels[currentLevel].find(dd);
471 if (iterator != uniqueTableForLevels[currentLevel].end()) {
472 return iterator->second;
473 } else {
474 // Otherwise, we need to recursively compute the ODD.
475
476 // If we are already past the maximal level that is to be considered, we can simply create an Odd without
477 // successors
478 if (currentLevel == maxLevel) {
479 uint_fast64_t elseOffset = 0;
480 uint_fast64_t thenOffset = 0;
481
482 // If the DD is not the zero leaf, then the then-offset is 1.
483 if (dd != Cudd_ReadZero(manager.getManager())) {
484 thenOffset = 1;
485 }
486
487 auto oddNode = std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
488 uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
489 return oddNode;
490 } else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
491 // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
492 // node for the then-successor as well.
493 std::shared_ptr<Odd> elseNode = createOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
494 std::shared_ptr<Odd> thenNode = elseNode;
495 auto oddNode = std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode,
496 thenNode->getElseOffset() + thenNode->getThenOffset());
497 uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
498 return oddNode;
499 } else {
500 // Otherwise, we compute the ODDs for both the then- and else successors.
501 std::shared_ptr<Odd> elseNode = createOddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
502 std::shared_ptr<Odd> thenNode = createOddRec(Cudd_T(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
503
504 uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
505 uint_fast64_t totalThenOffset = thenNode->getElseOffset() + thenNode->getThenOffset();
506
507 auto oddNode = std::make_shared<Odd>(elseNode, totalElseOffset, thenNode, totalThenOffset);
508 uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
509 return oddNode;
510 }
511 }
512}
513
514template<typename ValueType>
515InternalDdManager<DdType::CUDD> const& InternalAdd<DdType::CUDD, ValueType>::getInternalDdManager() const {
516 return *ddManager;
517}
518
519template<typename ValueType>
520void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices,
521 std::vector<ValueType>& targetVector,
522 std::function<ValueType(ValueType const&, ValueType const&)> const& function) const {
523 forEachRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices,
524 [&function, &targetVector](uint64_t const& offset, ValueType const& value) { targetVector[offset] = function(targetVector[offset], value); });
525}
526
527template<typename ValueType>
528void InternalAdd<DdType::CUDD, ValueType>::forEach(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices,
529 std::function<void(uint64_t const&, ValueType const&)> const& function) const {
530 forEachRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, function);
531}
532
533template<typename ValueType>
534void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices,
535 std::vector<uint_fast64_t> const& offsets, std::vector<ValueType>& targetVector,
536 std::function<ValueType(ValueType const&, ValueType const&)> const& function) const {
537 forEachRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices,
538 [&function, &targetVector, &offsets](uint64_t const& offset, ValueType const& value) {
539 ValueType& targetValue = targetVector[offsets[offset]];
540 targetValue = function(targetValue, value);
541 });
542}
543
544template<typename ValueType>
545void InternalAdd<DdType::CUDD, ValueType>::forEachRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset,
546 Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices,
547 std::function<void(uint64_t const&, ValueType const&)> const& function) const {
548 // For the empty DD, we do not need to add any entries.
549 if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
550 return;
551 }
552
553 // If we are at the maximal level, the value to be set is stored as a constant in the DD.
554 if (currentLevel == maxLevel) {
555 function(currentOffset, storm::utility::convertNumber<ValueType>(Cudd_V(dd)));
556 } else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
557 // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set
558 // and for the one in which it is not set.
559 forEachRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, function);
560 forEachRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, function);
561 } else {
562 // Otherwise, we simply recursively call the function for both (different) cases.
563 forEachRec(Cudd_E_const(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, function);
564 forEachRec(Cudd_T_const(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, function);
565 }
566}
567
568template<typename ValueType>
569std::vector<uint64_t> InternalAdd<DdType::CUDD, ValueType>::decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices,
570 storm::storage::BitVector const& ddLabelVariableIndices) const {
571 std::vector<uint64_t> result;
572 decodeGroupLabelsRec(this->getCuddDdNode(), result, ddGroupVariableIndices, ddLabelVariableIndices, 0, ddGroupVariableIndices.size(), 0);
573 return result;
574}
575
576template<typename ValueType>
577void InternalAdd<DdType::CUDD, ValueType>::decodeGroupLabelsRec(DdNode* dd, std::vector<uint64_t>& labels,
578 std::vector<uint_fast64_t> const& ddGroupVariableIndices,
579 storm::storage::BitVector const& ddLabelVariableIndices, uint_fast64_t currentLevel,
580 uint_fast64_t maxLevel, uint64_t label) const {
581 // For the empty DD, we do not need to create a group.
582 if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
583 return;
584 }
585
586 if (currentLevel == maxLevel) {
587 labels.push_back(label);
588 } else {
589 uint64_t elseLabel = label;
590 uint64_t thenLabel = label;
591
592 if (ddLabelVariableIndices.get(currentLevel)) {
593 elseLabel <<= 1;
594 thenLabel = (thenLabel << 1) | 1;
595 }
596
597 if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
598 decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, elseLabel);
599 decodeGroupLabelsRec(dd, labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, thenLabel);
600 } else {
601 decodeGroupLabelsRec(Cudd_E(dd), labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, elseLabel);
602 decodeGroupLabelsRec(Cudd_T(dd), labels, ddGroupVariableIndices, ddLabelVariableIndices, currentLevel + 1, maxLevel, thenLabel);
603 }
604 }
605}
606
607template<typename ValueType>
608std::vector<InternalAdd<DdType::CUDD, ValueType>> InternalAdd<DdType::CUDD, ValueType>::splitIntoGroups(
609 std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
610 std::vector<InternalAdd<DdType::CUDD, ValueType>> result;
611 splitIntoGroupsRec(this->getCuddDdNode(), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size());
612 return result;
613}
614
615template<typename ValueType>
616void InternalAdd<DdType::CUDD, ValueType>::splitIntoGroupsRec(DdNode* dd, std::vector<InternalAdd<DdType::CUDD, ValueType>>& groups,
617 std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel,
618 uint_fast64_t maxLevel) const {
619 // For the empty DD, we do not need to create a group.
620 if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
621 return;
622 }
623
624 if (currentLevel == maxLevel) {
625 groups.push_back(InternalAdd<DdType::CUDD, ValueType>(ddManager, cudd::ADD(ddManager->getCuddManager(), dd)));
626 } else if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
627 splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
628 splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
629 } else {
630 // FIXME: We first traverse the else successor (unlike other variants of this method).
631 // Otherwise, the GameBasedMdpModelCheckerTest would not terminate. See github issue #64
632 splitIntoGroupsRec(Cudd_E(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
633 splitIntoGroupsRec(Cudd_T(dd), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
634 }
635}
636
637template<typename ValueType>
638std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>> InternalAdd<DdType::CUDD, ValueType>::splitIntoGroups(
639 InternalAdd<DdType::CUDD, ValueType> vector, std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
640 std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>> result;
641 splitIntoGroupsRec(this->getCuddDdNode(), vector.getCuddDdNode(), result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size());
642 return result;
643}
644
645template<typename ValueType>
646void InternalAdd<DdType::CUDD, ValueType>::splitIntoGroupsRec(
647 DdNode* dd1, DdNode* dd2, std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>>& groups,
648 std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel) const {
649 // For the empty DD, we do not need to create a group.
650 if (dd1 == Cudd_ReadZero(ddManager->getCuddManager().getManager()) && dd2 == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
651 return;
652 }
653
654 if (currentLevel == maxLevel) {
655 groups.push_back(std::make_pair(InternalAdd<DdType::CUDD, ValueType>(ddManager, cudd::ADD(ddManager->getCuddManager(), dd1)),
656 InternalAdd<DdType::CUDD, ValueType>(ddManager, cudd::ADD(ddManager->getCuddManager(), dd2))));
657 } else if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd1)) {
658 if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd2)) {
659 splitIntoGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
660 splitIntoGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
661 } else {
662 splitIntoGroupsRec(dd1, Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
663 splitIntoGroupsRec(dd1, Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
664 }
665 } else if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd2)) {
666 splitIntoGroupsRec(Cudd_T(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
667 splitIntoGroupsRec(Cudd_E(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
668 } else {
669 splitIntoGroupsRec(Cudd_T(dd1), Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
670 splitIntoGroupsRec(Cudd_E(dd1), Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
671 }
672}
673
674template<typename ValueType>
675std::vector<std::vector<InternalAdd<DdType::CUDD, ValueType>>> InternalAdd<DdType::CUDD, ValueType>::splitIntoGroups(
676 std::vector<InternalAdd<DdType::CUDD, ValueType>> const& vectors, std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
677 std::vector<std::vector<InternalAdd<DdType::CUDD, ValueType>>> result;
678 std::vector<DdNode*> dds;
679 for (auto const& vector : vectors) {
680 dds.push_back(vector.getCuddDdNode());
681 }
682 dds.push_back(this->getCuddDdNode());
683
684 splitIntoGroupsRec(dds, result, ddGroupVariableIndices, 0, ddGroupVariableIndices.size());
685 return result;
686}
687
688template<typename ValueType>
689void InternalAdd<DdType::CUDD, ValueType>::splitIntoGroupsRec(std::vector<DdNode*> const& dds,
690 std::vector<std::vector<InternalAdd<DdType::CUDD, ValueType>>>& groups,
691 std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel,
692 uint_fast64_t maxLevel) const {
693 // For the empty DD, we do not need to create a group.
694 {
695 bool emptyDd = true;
696 for (auto const& dd : dds) {
697 if (dd != Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
698 emptyDd = false;
699 break;
700 }
701 }
702 if (emptyDd) {
703 return;
704 }
705 }
706
707 if (currentLevel == maxLevel) {
708 std::vector<InternalAdd<DdType::CUDD, ValueType>> newGroup;
709 for (auto dd : dds) {
710 newGroup.emplace_back(ddManager, cudd::ADD(ddManager->getCuddManager(), dd));
711 }
712 groups.push_back(std::move(newGroup));
713 } else {
714 std::vector<DdNode*> thenSubDds(dds), elseSubDds(dds);
715 for (uint64_t ddIndex = 0; ddIndex < dds.size(); ++ddIndex) {
716 auto const& dd = dds[ddIndex];
717 if (ddGroupVariableIndices[currentLevel] == Cudd_NodeReadIndex(dd)) {
718 thenSubDds[ddIndex] = Cudd_T(dd);
719 elseSubDds[ddIndex] = Cudd_E(dd);
720 }
721 }
722 splitIntoGroupsRec(thenSubDds, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
723 splitIntoGroupsRec(elseSubDds, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
724 }
725}
726
727template<typename ValueType>
728void InternalAdd<DdType::CUDD, ValueType>::toMatrixComponents(std::vector<uint_fast64_t> const& rowGroupIndices, std::vector<uint_fast64_t>& rowIndications,
729 std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues,
730 Odd const& rowOdd, Odd const& columnOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices,
731 std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool writeValues) const {
732 return toMatrixComponentsRec(this->getCuddDdNode(), rowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, 0, 0,
733 ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices,
734 writeValues);
735}
736
737template<typename ValueType>
738void InternalAdd<DdType::CUDD, ValueType>::toMatrixComponentsRec(DdNode const* dd, std::vector<uint_fast64_t> const& rowGroupOffsets,
739 std::vector<uint_fast64_t>& rowIndications,
740 std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues,
741 Odd const& rowOdd, Odd const& columnOdd, uint_fast64_t currentRowLevel,
742 uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset,
743 uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices,
744 std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues) const {
745 // For the empty DD, we do not need to add any entries.
746 if (dd == Cudd_ReadZero(ddManager->getCuddManager().getManager())) {
747 return;
748 }
749
750 // If we are at the maximal level, the value to be set is stored as a constant in the DD.
751 if (currentRowLevel + currentColumnLevel == maxLevel) {
752 if (generateValues) {
753 columnsAndValues[rowIndications[rowGroupOffsets[currentRowOffset]]] =
754 storm::storage::MatrixEntry<uint_fast64_t, ValueType>(currentColumnOffset, storm::utility::convertNumber<ValueType>(Cudd_V(dd)));
755 }
756 ++rowIndications[rowGroupOffsets[currentRowOffset]];
757 } else {
758 DdNode const* elseElse;
759 DdNode const* elseThen;
760 DdNode const* thenElse;
761 DdNode const* thenThen;
762
763 if (ddColumnVariableIndices[currentColumnLevel] < Cudd_NodeReadIndex(dd)) {
764 elseElse = elseThen = thenElse = thenThen = dd;
765 } else if (ddRowVariableIndices[currentColumnLevel] < Cudd_NodeReadIndex(dd)) {
766 elseElse = thenElse = Cudd_E_const(dd);
767 elseThen = thenThen = Cudd_T_const(dd);
768 } else {
769 DdNode const* elseNode = Cudd_E_const(dd);
770 if (ddColumnVariableIndices[currentColumnLevel] < Cudd_NodeReadIndex(elseNode)) {
771 elseElse = elseThen = elseNode;
772 } else {
773 elseElse = Cudd_E_const(elseNode);
774 elseThen = Cudd_T_const(elseNode);
775 }
776
777 DdNode const* thenNode = Cudd_T_const(dd);
778 if (ddColumnVariableIndices[currentColumnLevel] < Cudd_NodeReadIndex(thenNode)) {
779 thenElse = thenThen = thenNode;
780 } else {
781 thenElse = Cudd_E_const(thenNode);
782 thenThen = Cudd_T_const(thenNode);
783 }
784 }
785
786 // Visit else-else.
787 toMatrixComponentsRec(elseElse, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getElseSuccessor(),
788 currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset, ddRowVariableIndices,
789 ddColumnVariableIndices, generateValues);
790 // Visit else-then.
791 toMatrixComponentsRec(elseThen, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getElseSuccessor(), columnOdd.getThenSuccessor(),
792 currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset, currentColumnOffset + columnOdd.getElseOffset(),
793 ddRowVariableIndices, ddColumnVariableIndices, generateValues);
794 // Visit then-else.
795 toMatrixComponentsRec(thenElse, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getThenSuccessor(), columnOdd.getElseSuccessor(),
796 currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), currentColumnOffset,
797 ddRowVariableIndices, ddColumnVariableIndices, generateValues);
798 // Visit then-then.
799 toMatrixComponentsRec(thenThen, rowGroupOffsets, rowIndications, columnsAndValues, rowOdd.getThenSuccessor(), columnOdd.getThenSuccessor(),
800 currentRowLevel + 1, currentColumnLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(),
801 currentColumnOffset + columnOdd.getElseOffset(), ddRowVariableIndices, ddColumnVariableIndices, generateValues);
802 }
803}
804
805template<typename ValueType>
806InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::fromVector(InternalDdManager<DdType::CUDD> const* ddManager,
807 std::vector<ValueType> const& values, storm::dd::Odd const& odd,
808 std::vector<uint_fast64_t> const& ddVariableIndices) {
809 uint_fast64_t offset = 0;
810 return InternalAdd<DdType::CUDD, ValueType>(
811 ddManager, cudd::ADD(ddManager->getCuddManager(),
812 fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices)));
813}
814
815template<typename ValueType>
816DdNode* InternalAdd<DdType::CUDD, ValueType>::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel,
817 uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd const& odd,
818 std::vector<uint_fast64_t> const& ddVariableIndices) {
819 if (currentLevel == maxLevel) {
820 // If we are in a terminal node of the ODD, we need to check whether the then-offset of the ODD is one
821 // (meaning the encoding is a valid one) or zero (meaning the encoding is not valid). Consequently, we
822 // need to copy the next value of the vector iff the then-offset is greater than zero.
823 if (odd.getThenOffset() > 0) {
824 return Cudd_addConst(manager, values[currentOffset++]);
825 } else {
826 return Cudd_ReadZero(manager);
827 }
828 } else {
829 // If the total offset is zero, we can just return the constant zero DD.
830 if (odd.getThenOffset() + odd.getElseOffset() == 0) {
831 return Cudd_ReadZero(manager);
832 }
833
834 // Determine the new else-successor.
835 DdNode* elseSuccessor = nullptr;
836 if (odd.getElseOffset() > 0) {
837 elseSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getElseSuccessor(), ddVariableIndices);
838 } else {
839 elseSuccessor = Cudd_ReadZero(manager);
840 }
841 Cudd_Ref(elseSuccessor);
842
843 // Determine the new then-successor.
844 DdNode* thenSuccessor = nullptr;
845 if (odd.getThenOffset() > 0) {
846 thenSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getThenSuccessor(), ddVariableIndices);
847 } else {
848 thenSuccessor = Cudd_ReadZero(manager);
849 }
850 Cudd_Ref(thenSuccessor);
851
852 // Create a node representing ITE(currentVar, thenSuccessor, elseSuccessor);
853 DdNode* result = Cudd_addIthVar(manager, static_cast<int>(ddVariableIndices[currentLevel]));
854 Cudd_Ref(result);
855 DdNode* newResult = Cudd_addIte(manager, result, thenSuccessor, elseSuccessor);
856 Cudd_Ref(newResult);
857
858 // Dispose of the intermediate results
859 Cudd_RecursiveDeref(manager, result);
860 Cudd_RecursiveDeref(manager, thenSuccessor);
861 Cudd_RecursiveDeref(manager, elseSuccessor);
862
863 // Before returning, we remove the protection imposed by the previous call to Cudd_Ref.
864 Cudd_Deref(newResult);
865
866 return newResult;
867 }
868}
869
870template<>
871DdNode* InternalAdd<DdType::CUDD, storm::RationalNumber>::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel,
872 uint_fast64_t maxLevel, std::vector<storm::RationalNumber> const& values,
873 Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices) {
874 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported");
875}
876
877#else
878template<typename ValueType>
879bool InternalAdd<DdType::CUDD, ValueType>::operator==(InternalAdd<DdType::CUDD, ValueType> const& other) const {
880 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
881 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
882 "of Storm with CUDD support.");
883}
884
885template<typename ValueType>
886bool InternalAdd<DdType::CUDD, ValueType>::operator!=(InternalAdd<DdType::CUDD, ValueType> const& other) const {
887 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
888 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
889 "of Storm with CUDD support.");
890}
891
892template<typename ValueType>
893InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator+(InternalAdd<DdType::CUDD, ValueType> const& other) const {
894 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
895 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
896 "of Storm with CUDD support.");
897}
898
899template<typename ValueType>
900InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator+=(InternalAdd<DdType::CUDD, ValueType> const& other) {
901 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
902 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
903 "of Storm with CUDD support.");
904}
905
906template<typename ValueType>
907InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator*(InternalAdd<DdType::CUDD, ValueType> const& other) const {
908 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
909 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
910 "of Storm with CUDD support.");
911}
912
913template<typename ValueType>
914InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator*=(InternalAdd<DdType::CUDD, ValueType> const& other) {
915 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
916 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
917 "of Storm with CUDD support.");
918}
919
920template<typename ValueType>
921InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator-(InternalAdd<DdType::CUDD, ValueType> const& other) const {
922 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
923 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
924 "of Storm with CUDD support.");
925}
926
927template<typename ValueType>
928InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator-=(InternalAdd<DdType::CUDD, ValueType> const& other) {
929 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
930 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
931 "of Storm with CUDD support.");
932}
933
934template<typename ValueType>
935InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::operator/(InternalAdd<DdType::CUDD, ValueType> const& other) const {
936 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
937 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
938 "of Storm with CUDD support.");
939}
940
941template<typename ValueType>
942InternalAdd<DdType::CUDD, ValueType>& InternalAdd<DdType::CUDD, ValueType>::operator/=(InternalAdd<DdType::CUDD, ValueType> const& other) {
943 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
944 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
945 "of Storm with CUDD support.");
946}
947
948template<typename ValueType>
949InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::equals(InternalAdd<DdType::CUDD, ValueType> const& other) const {
950 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
951 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
952 "of Storm with CUDD support.");
953}
954
955template<typename ValueType>
956InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::notEquals(InternalAdd<DdType::CUDD, ValueType> const& other) const {
957 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
958 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
959 "of Storm with CUDD support.");
960}
961
962template<typename ValueType>
963InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::less(InternalAdd<DdType::CUDD, ValueType> const& other) const {
964 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
965 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
966 "of Storm with CUDD support.");
967}
968
969template<typename ValueType>
970InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::lessOrEqual(InternalAdd<DdType::CUDD, ValueType> const& other) const {
971 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
972 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
973 "of Storm with CUDD support.");
974}
975
976template<typename ValueType>
977InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greater(InternalAdd<DdType::CUDD, ValueType> const& other) const {
978 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
979 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
980 "of Storm with CUDD support.");
981}
982
983template<typename ValueType>
984InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greaterOrEqual(InternalAdd<DdType::CUDD, ValueType> const& other) const {
985 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
986 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
987 "of Storm with CUDD support.");
988}
989
990template<typename ValueType>
991InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::pow(InternalAdd<DdType::CUDD, ValueType> const& other) const {
992 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
993 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
994 "of Storm with CUDD support.");
995}
996
997template<typename ValueType>
998InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::mod(InternalAdd<DdType::CUDD, ValueType> const& other) const {
999 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1000 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1001 "of Storm with CUDD support.");
1002}
1003
1004template<typename ValueType>
1005InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::logxy(InternalAdd<DdType::CUDD, ValueType> const& other) const {
1006 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1007 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1008 "of Storm with CUDD support.");
1009}
1010
1011template<typename ValueType>
1012InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::floor() const {
1013 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1014 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1015 "of Storm with CUDD support.");
1016}
1017
1018template<typename ValueType>
1019InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::ceil() const {
1020 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1021 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1022 "of Storm with CUDD support.");
1023}
1024
1025template<typename ValueType>
1026InternalAdd<DdType::CUDD, storm::RationalNumber> InternalAdd<DdType::CUDD, ValueType>::sharpenKwekMehlhorn(size_t /*precision*/) const {
1027 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1028 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1029 "of Storm with CUDD support.");
1030}
1031
1032template<typename ValueType>
1033InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::minimum(InternalAdd<DdType::CUDD, ValueType> const& other) const {
1034 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1035 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1036 "of Storm with CUDD support.");
1037}
1038
1039template<typename ValueType>
1040InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::maximum(InternalAdd<DdType::CUDD, ValueType> const& other) const {
1041 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1042 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1043 "of Storm with CUDD support.");
1044}
1045
1046template<typename ValueType>
1047template<typename TargetValueType>
1048typename std::enable_if<std::is_same<ValueType, TargetValueType>::value, InternalAdd<DdType::CUDD, TargetValueType>>::type
1049InternalAdd<DdType::CUDD, ValueType>::toValueType() const {
1050 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1051 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1052 "of Storm with CUDD support.");
1053}
1054
1055template<typename ValueType>
1056template<typename TargetValueType>
1057typename std::enable_if<!std::is_same<ValueType, TargetValueType>::value, InternalAdd<DdType::CUDD, TargetValueType>>::type
1058InternalAdd<DdType::CUDD, ValueType>::toValueType() const {
1059 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1060 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1061 "of Storm with CUDD support.");
1062}
1063
1064template<typename ValueType>
1065InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::sumAbstract(InternalBdd<DdType::CUDD> const& cube) const {
1066 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1067 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1068 "of Storm with CUDD support.");
1069}
1070
1071template<typename ValueType>
1072InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::minAbstract(InternalBdd<DdType::CUDD> const& cube) const {
1073 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1074 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1075 "of Storm with CUDD support.");
1076}
1077
1078template<typename ValueType>
1079InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::minAbstractRepresentative(InternalBdd<DdType::CUDD> const& cube) const {
1080 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1081 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1082 "of Storm with CUDD support.");
1083}
1084
1085template<typename ValueType>
1086InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::maxAbstract(InternalBdd<DdType::CUDD> const& cube) const {
1087 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1088 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1089 "of Storm with CUDD support.");
1090}
1091
1092template<typename ValueType>
1093InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::maxAbstractRepresentative(InternalBdd<DdType::CUDD> const& cube) const {
1094 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1095 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1096 "of Storm with CUDD support.");
1097}
1098
1099template<typename ValueType>
1100bool InternalAdd<DdType::CUDD, ValueType>::equalModuloPrecision(InternalAdd<DdType::CUDD, ValueType> const& other, ValueType const& precision,
1101 bool relative) const {
1102 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1103 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1104 "of Storm with CUDD support.");
1105}
1106
1107template<>
1108bool InternalAdd<DdType::CUDD, storm::RationalNumber>::equalModuloPrecision(InternalAdd<DdType::CUDD, storm::RationalNumber> const& /*other*/,
1109 storm::RationalNumber const& /*precision*/, bool /*relative*/) const {
1110 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1111 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1112 "of Storm with CUDD support.");
1113}
1114
1115template<typename ValueType>
1116InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::swapVariables(std::vector<InternalBdd<DdType::CUDD>> const& from,
1117 std::vector<InternalBdd<DdType::CUDD>> const& to) const {
1118 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1119 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1120 "of Storm with CUDD support.");
1121}
1122
1123template<typename ValueType>
1124InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::permuteVariables(std::vector<InternalBdd<DdType::CUDD>> const& from,
1125 std::vector<InternalBdd<DdType::CUDD>> const& to) const {
1126 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1127 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1128 "of Storm with CUDD support.");
1129}
1130
1131template<typename ValueType>
1132InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::multiplyMatrix(
1133 InternalAdd<DdType::CUDD, ValueType> const& otherMatrix, std::vector<InternalBdd<DdType::CUDD>> const& summationDdVariables) const {
1134 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1135 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1136 "of Storm with CUDD support.");
1137}
1138
1139template<typename ValueType>
1140InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::multiplyMatrix(
1141 InternalBdd<DdType::CUDD> const& otherMatrix, std::vector<InternalBdd<DdType::CUDD>> const& summationDdVariables) const {
1142 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1143 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1144 "of Storm with CUDD support.");
1145}
1146
1147template<typename ValueType>
1148InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greater(ValueType const& value) const {
1149 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1150 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1151 "of Storm with CUDD support.");
1152}
1153
1154template<>
1155InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, storm::RationalNumber>::greater(storm::RationalNumber const& value) const {
1156 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1157 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1158 "of Storm with CUDD support.");
1159}
1160
1161template<typename ValueType>
1162InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greaterOrEqual(ValueType const& value) const {
1163 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1164 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1165 "of Storm with CUDD support.");
1166}
1167
1168template<>
1169InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, storm::RationalNumber>::greaterOrEqual(storm::RationalNumber const& value) const {
1170 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1171 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1172 "of Storm with CUDD support.");
1173}
1174
1175template<typename ValueType>
1176InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::less(ValueType const& value) const {
1177 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1178 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1179 "of Storm with CUDD support.");
1180}
1181
1182template<>
1183InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, storm::RationalNumber>::less(storm::RationalNumber const& value) const {
1184 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1185 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1186 "of Storm with CUDD support.");
1187}
1188
1189template<typename ValueType>
1190InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::lessOrEqual(ValueType const& value) const {
1191 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1192 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1193 "of Storm with CUDD support.");
1194}
1195
1196template<>
1197InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, storm::RationalNumber>::lessOrEqual(storm::RationalNumber const& value) const {
1198 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1199 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1200 "of Storm with CUDD support.");
1201}
1202
1203template<typename ValueType>
1204InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::notZero() const {
1205 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1206 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1207 "of Storm with CUDD support.");
1208}
1209
1210template<typename ValueType>
1211InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::constrain(InternalAdd<DdType::CUDD, ValueType> const& constraint) const {
1212 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1213 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1214 "of Storm with CUDD support.");
1215}
1216
1217template<typename ValueType>
1218InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::restrict(InternalAdd<DdType::CUDD, ValueType> const& constraint) const {
1219 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1220 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1221 "of Storm with CUDD support.");
1222}
1223
1224template<typename ValueType>
1225InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::getSupport() const {
1226 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1227 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1228 "of Storm with CUDD support.");
1229}
1230
1231template<typename ValueType>
1232uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getNonZeroCount(uint_fast64_t numberOfDdVariables) const {
1233 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1234 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1235 "of Storm with CUDD support.");
1236}
1237
1238template<typename ValueType>
1239uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getLeafCount() const {
1240 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1241 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1242 "of Storm with CUDD support.");
1243}
1244
1245template<typename ValueType>
1246uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getNodeCount() const {
1247 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1248 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1249 "of Storm with CUDD support.");
1250}
1251
1252template<typename ValueType>
1253ValueType InternalAdd<DdType::CUDD, ValueType>::getMin() const {
1254 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1255 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1256 "of Storm with CUDD support.");
1257}
1258
1259template<typename ValueType>
1260ValueType InternalAdd<DdType::CUDD, ValueType>::getMax() const {
1261 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1262 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1263 "of Storm with CUDD support.");
1264}
1265
1266template<typename ValueType>
1267ValueType InternalAdd<DdType::CUDD, ValueType>::getValue() const {
1268 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1269 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1270 "of Storm with CUDD support.");
1271}
1272
1273template<typename ValueType>
1274bool InternalAdd<DdType::CUDD, ValueType>::isOne() const {
1275 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1276 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1277 "of Storm with CUDD support.");
1278}
1279
1280template<typename ValueType>
1281bool InternalAdd<DdType::CUDD, ValueType>::isZero() const {
1282 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1283 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1284 "of Storm with CUDD support.");
1285}
1286
1287template<typename ValueType>
1288bool InternalAdd<DdType::CUDD, ValueType>::isConstant() const {
1289 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1290 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1291 "of Storm with CUDD support.");
1292}
1293
1294template<typename ValueType>
1295uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getIndex() const {
1296 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1297 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1298 "of Storm with CUDD support.");
1299}
1300
1301template<typename ValueType>
1302uint_fast64_t InternalAdd<DdType::CUDD, ValueType>::getLevel() const {
1303 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1304 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1305 "of Storm with CUDD support.");
1306}
1307
1308template<typename ValueType>
1309void InternalAdd<DdType::CUDD, ValueType>::exportToDot(std::string const& filename, std::vector<std::string> const& ddVariableNamesAsStrings,
1310 bool showVariablesIfPossible) const {
1311 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1312 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1313 "of Storm with CUDD support.");
1314}
1315
1316template<typename ValueType>
1317void InternalAdd<DdType::CUDD, ValueType>::exportToText(std::string const&) const {
1318 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1319 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1320 "of Storm with CUDD support.");
1321}
1322
1323template<typename ValueType>
1324AddIterator<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::begin(DdManager<DdType::CUDD> const& fullDdManager, InternalBdd<DdType::CUDD> const&,
1325 uint_fast64_t, std::set<storm::expressions::Variable> const& metaVariables,
1326 bool enumerateDontCareMetaVariables) const {
1327 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1328 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1329 "of Storm with CUDD support.");
1330}
1331
1332template<typename ValueType>
1333AddIterator<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::end(DdManager<DdType::CUDD> const& fullDdManager) const {
1334 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1335 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1336 "of Storm with CUDD support.");
1337}
1338
1339template<typename ValueType>
1340std::string InternalAdd<DdType::CUDD, ValueType>::getStringId() const {
1341 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1342 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1343 "of Storm with CUDD support.");
1344}
1345
1346template<typename ValueType>
1347Odd InternalAdd<DdType::CUDD, ValueType>::createOdd(std::vector<uint_fast64_t> const& ddVariableIndices) const {
1348 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1349 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1350 "of Storm with CUDD support.");
1351}
1352
1353template<typename ValueType>
1354InternalDdManager<DdType::CUDD> const& InternalAdd<DdType::CUDD, ValueType>::getInternalDdManager() const {
1355 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1356 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1357 "of Storm with CUDD support.");
1358}
1359
1360template<typename ValueType>
1361void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices,
1362 std::vector<ValueType>& targetVector,
1363 std::function<ValueType(ValueType const&, ValueType const&)> const& function) const {
1364 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1365 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1366 "of Storm with CUDD support.");
1367}
1368
1369template<typename ValueType>
1370void InternalAdd<DdType::CUDD, ValueType>::forEach(Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices,
1371 std::function<void(uint64_t const&, ValueType const&)> const& function) const {
1372 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1373 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1374 "of Storm with CUDD support.");
1375}
1376
1377template<typename ValueType>
1378void InternalAdd<DdType::CUDD, ValueType>::composeWithExplicitVector(storm::dd::Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices,
1379 std::vector<uint_fast64_t> const& offsets, std::vector<ValueType>& targetVector,
1380 std::function<ValueType(ValueType const&, ValueType const&)> const& function) const {
1381 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1382 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1383 "of Storm with CUDD support.");
1384}
1385
1386template<typename ValueType>
1387std::vector<uint64_t> InternalAdd<DdType::CUDD, ValueType>::decodeGroupLabels(std::vector<uint_fast64_t> const& ddGroupVariableIndices,
1388 storm::storage::BitVector const& ddLabelVariableIndices) const {
1389 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1390 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1391 "of Storm with CUDD support.");
1392}
1393
1394template<typename ValueType>
1395std::vector<InternalAdd<DdType::CUDD, ValueType>> InternalAdd<DdType::CUDD, ValueType>::splitIntoGroups(
1396 std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
1397 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1398 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1399 "of Storm with CUDD support.");
1400}
1401
1402template<typename ValueType>
1403std::vector<std::pair<InternalAdd<DdType::CUDD, ValueType>, InternalAdd<DdType::CUDD, ValueType>>> InternalAdd<DdType::CUDD, ValueType>::splitIntoGroups(
1404 InternalAdd<DdType::CUDD, ValueType> vector, std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
1405 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1406 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1407 "of Storm with CUDD support.");
1408}
1409
1410template<typename ValueType>
1411std::vector<std::vector<InternalAdd<DdType::CUDD, ValueType>>> InternalAdd<DdType::CUDD, ValueType>::splitIntoGroups(
1412 std::vector<InternalAdd<DdType::CUDD, ValueType>> const& vectors, std::vector<uint_fast64_t> const& ddGroupVariableIndices) const {
1413 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1414 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1415 "of Storm with CUDD support.");
1416}
1417
1418template<typename ValueType>
1419void InternalAdd<DdType::CUDD, ValueType>::toMatrixComponents(std::vector<uint_fast64_t> const& rowGroupIndices, std::vector<uint_fast64_t>& rowIndications,
1420 std::vector<storm::storage::MatrixEntry<uint_fast64_t, ValueType>>& columnsAndValues,
1421 Odd const& rowOdd, Odd const& columnOdd, std::vector<uint_fast64_t> const& ddRowVariableIndices,
1422 std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool writeValues) const {
1423 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1424 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1425 "of Storm with CUDD support.");
1426}
1427
1428template<typename ValueType>
1429InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::fromVector(InternalDdManager<DdType::CUDD> const* ddManager,
1430 std::vector<ValueType> const& values, storm::dd::Odd const& odd,
1431 std::vector<uint_fast64_t> const& ddVariableIndices) {
1432 STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
1433 "This version of Storm was compiled without support for CUDD. Yet, a method was called that requires this support. Please choose a version "
1434 "of Storm with CUDD support.");
1435}
1436
1437#endif
1438
1439template class InternalAdd<DdType::CUDD, double>;
1440template InternalAdd<DdType::CUDD, double> InternalAdd<DdType::CUDD, double>::toValueType<double>() const;
1441template class InternalAdd<DdType::CUDD, uint_fast64_t>;
1442template InternalAdd<DdType::CUDD, uint_fast64_t> InternalAdd<DdType::CUDD, uint_fast64_t>::toValueType<uint_fast64_t>() const;
1443
1444template class InternalAdd<DdType::CUDD, storm::RationalNumber>;
1445template InternalAdd<DdType::CUDD, storm::RationalNumber> InternalAdd<DdType::CUDD, storm::RationalNumber>::toValueType<storm::RationalNumber>() const;
1446template InternalAdd<DdType::CUDD, storm::RationalNumber> InternalAdd<DdType::CUDD, double>::toValueType<storm::RationalNumber>() const;
1447template InternalAdd<DdType::CUDD, double> InternalAdd<DdType::CUDD, storm::RationalNumber>::toValueType<double>() const;
1448} // namespace dd
1449} // namespace storm
storm::storage::BitVector
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
storm::storage::BitVector::get
bool get(uint64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
Definition BitVector.cpp:267
storm::storage::MatrixEntry
Definition SparseMatrix.h:39
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
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:12
storm::settings::manager
SettingsManager const & manager()
Retrieves the settings manager.
Definition SettingsManager.cpp:662
storm::utility::Minimum
Extremum< storm::OptimizationDirection::Minimize, ValueType > Minimum
Definition Extremum.h:129
storm::utility::Maximum
Extremum< storm::OptimizationDirection::Maximize, ValueType > Maximum
Definition Extremum.h:127