Browse Source
Started adding stuff to src/storage/dd/sylvan/InternalSylvanDdManager.
Started adding stuff to src/storage/dd/sylvan/InternalSylvanDdManager.
Former-commit-id: cf8adfc43f
main
PBerger
9 years ago
3 changed files with 309 additions and 271 deletions
-
273src/storage/dd/sylvan/InternalSylvanDdManager.cpp
-
278src/storage/dd/sylvan/InternalSylvanDdManager.h
-
29src/utility/sylvan.h
@ -1,127 +1,148 @@ |
|||||
#include "src/storage/dd/sylvan/InternalSylvanDdManager.h"
|
|
||||
|
|
||||
#include <cmath>
|
|
||||
|
|
||||
#include "src/settings/SettingsManager.h"
|
|
||||
#include "src/settings/modules/SylvanSettings.h"
|
|
||||
|
|
||||
#include "src/utility/constants.h"
|
|
||||
#include "src/utility/macros.h"
|
|
||||
#include "src/exceptions/NotSupportedException.h"
|
|
||||
|
|
||||
namespace storm { |
|
||||
namespace dd { |
|
||||
uint_fast64_t InternalDdManager<DdType::Sylvan>::numberOfInstances = 0; |
|
||||
|
|
||||
// It is important that the variable pairs start at an even offset, because sylvan assumes this to be true for
|
|
||||
// some operations.
|
|
||||
uint_fast64_t InternalDdManager<DdType::Sylvan>::nextFreeVariableIndex = 0; |
|
||||
|
|
||||
uint_fast64_t findLargestPowerOfTwoFitting(uint_fast64_t number) { |
|
||||
for (uint_fast64_t index = 0; index < 64; ++index) { |
|
||||
if ((number & (1ull << (63 - index))) != 0) { |
|
||||
return 63 - index; |
|
||||
} |
|
||||
} |
|
||||
return 0; |
|
||||
} |
|
||||
|
|
||||
InternalDdManager<DdType::Sylvan>::InternalDdManager() { |
|
||||
if (numberOfInstances == 0) { |
|
||||
// Initialize lace: auto-detect number of workers.
|
|
||||
lace_init(storm::settings::getModule<storm::settings::modules::SylvanSettings>().getNumberOfThreads(), 1000000); |
|
||||
lace_startup(0, 0, 0); |
|
||||
|
|
||||
// Each node takes 24 bytes and the maximal memory is specified in megabytes.
|
|
||||
uint_fast64_t totalNodesToStore = storm::settings::getModule<storm::settings::modules::SylvanSettings>().getMaximalMemory() * 1024 * 1024 / 24; |
|
||||
|
|
||||
// Compute the power of two that still fits within the total numbers to store.
|
|
||||
uint_fast64_t powerOfTwo = findLargestPowerOfTwoFitting(totalNodesToStore); |
|
||||
|
|
||||
sylvan::Sylvan::initPackage(1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 8 : 0ull), 1ull << (powerOfTwo - 1), 1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 12 : 0ull), 1ull << (powerOfTwo - 1)); |
|
||||
sylvan::Sylvan::initBdd(1); |
|
||||
sylvan::Sylvan::initMtbdd(); |
|
||||
} |
|
||||
++numberOfInstances; |
|
||||
} |
|
||||
|
|
||||
InternalDdManager<DdType::Sylvan>::~InternalDdManager() { |
|
||||
--numberOfInstances; |
|
||||
if (numberOfInstances == 0) { |
|
||||
// Enable this to print the sylvan statistics to a file.
|
|
||||
// FILE* filePointer = fopen("sylvan.stats", "w");
|
|
||||
// sylvan_stats_report(filePointer, 0);
|
|
||||
// fclose(filePointer);
|
|
||||
|
|
||||
sylvan::Sylvan::quitPackage(); |
|
||||
lace_exit(); |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddOne() const { |
|
||||
return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddOne()); |
|
||||
} |
|
||||
|
|
||||
template<> |
|
||||
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const { |
|
||||
return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(storm::utility::one<double>())); |
|
||||
} |
|
||||
|
|
||||
template<> |
|
||||
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const { |
|
||||
return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(storm::utility::one<uint_fast64_t>())); |
|
||||
} |
|
||||
|
|
||||
InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddZero() const { |
|
||||
return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddZero()); |
|
||||
} |
|
||||
|
|
||||
template<> |
|
||||
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const { |
|
||||
return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(storm::utility::zero<double>())); |
|
||||
} |
|
||||
|
|
||||
template<> |
|
||||
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const { |
|
||||
return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(storm::utility::zero<uint_fast64_t>())); |
|
||||
} |
|
||||
|
|
||||
template<> |
|
||||
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const { |
|
||||
return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(value)); |
|
||||
} |
|
||||
|
|
||||
template<> |
|
||||
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const { |
|
||||
return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(value)); |
|
||||
} |
|
||||
|
|
||||
std::pair<InternalBdd<DdType::Sylvan>, InternalBdd<DdType::Sylvan>> InternalDdManager<DdType::Sylvan>::createNewDdVariablePair() { |
|
||||
InternalBdd<DdType::Sylvan> first = InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddVar(nextFreeVariableIndex)); |
|
||||
InternalBdd<DdType::Sylvan> second = InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddVar(nextFreeVariableIndex + 1)); |
|
||||
nextFreeVariableIndex += 2; |
|
||||
return std::make_pair(first, second); |
|
||||
} |
|
||||
|
|
||||
void InternalDdManager<DdType::Sylvan>::allowDynamicReordering(bool value) { |
|
||||
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); |
|
||||
} |
|
||||
|
|
||||
bool InternalDdManager<DdType::Sylvan>::isDynamicReorderingAllowed() const { |
|
||||
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); |
|
||||
} |
|
||||
|
|
||||
void InternalDdManager<DdType::Sylvan>::triggerReordering() { |
|
||||
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); |
|
||||
} |
|
||||
|
|
||||
template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const; |
|
||||
template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const; |
|
||||
|
|
||||
template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const; |
|
||||
template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const; |
|
||||
|
|
||||
template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const; |
|
||||
template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const; |
|
||||
} |
|
||||
|
#include "src/storage/dd/sylvan/InternalSylvanDdManager.h"
|
||||
|
|
||||
|
#include <cmath>
|
||||
|
|
||||
|
#include "src/settings/SettingsManager.h"
|
||||
|
#include "src/settings/modules/SylvanSettings.h"
|
||||
|
|
||||
|
#include "src/utility/constants.h"
|
||||
|
#include "src/utility/macros.h"
|
||||
|
#include "src/exceptions/NotSupportedException.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace dd { |
||||
|
uint_fast64_t InternalDdManager<DdType::Sylvan>::numberOfInstances = 0; |
||||
|
|
||||
|
// It is important that the variable pairs start at an even offset, because sylvan assumes this to be true for
|
||||
|
// some operations.
|
||||
|
uint_fast64_t InternalDdManager<DdType::Sylvan>::nextFreeVariableIndex = 0; |
||||
|
|
||||
|
uint_fast64_t findLargestPowerOfTwoFitting(uint_fast64_t number) { |
||||
|
for (uint_fast64_t index = 0; index < 64; ++index) { |
||||
|
if ((number & (1ull << (63 - index))) != 0) { |
||||
|
return 63 - index; |
||||
|
} |
||||
|
} |
||||
|
return 0; |
||||
|
} |
||||
|
|
||||
|
InternalDdManager<DdType::Sylvan>::InternalDdManager() { |
||||
|
if (numberOfInstances == 0) { |
||||
|
// Initialize lace: auto-detect number of workers.
|
||||
|
lace_init(storm::settings::getModule<storm::settings::modules::SylvanSettings>().getNumberOfThreads(), 1000000); |
||||
|
lace_startup(0, 0, 0); |
||||
|
|
||||
|
// Each node takes 24 bytes and the maximal memory is specified in megabytes.
|
||||
|
uint_fast64_t totalNodesToStore = storm::settings::getModule<storm::settings::modules::SylvanSettings>().getMaximalMemory() * 1024 * 1024 / 24; |
||||
|
|
||||
|
// Compute the power of two that still fits within the total numbers to store.
|
||||
|
uint_fast64_t powerOfTwo = findLargestPowerOfTwoFitting(totalNodesToStore); |
||||
|
|
||||
|
sylvan::Sylvan::initPackage(1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 8 : 0ull), 1ull << (powerOfTwo - 1), 1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 12 : 0ull), 1ull << (powerOfTwo - 1)); |
||||
|
sylvan::Sylvan::initBdd(1); |
||||
|
sylvan::Sylvan::initMtbdd(); |
||||
|
} |
||||
|
++numberOfInstances; |
||||
|
} |
||||
|
|
||||
|
InternalDdManager<DdType::Sylvan>::~InternalDdManager() { |
||||
|
--numberOfInstances; |
||||
|
if (numberOfInstances == 0) { |
||||
|
// Enable this to print the sylvan statistics to a file.
|
||||
|
// FILE* filePointer = fopen("sylvan.stats", "w");
|
||||
|
// sylvan_stats_report(filePointer, 0);
|
||||
|
// fclose(filePointer);
|
||||
|
|
||||
|
sylvan::Sylvan::quitPackage(); |
||||
|
lace_exit(); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddOne() const { |
||||
|
return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddOne()); |
||||
|
} |
||||
|
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const { |
||||
|
return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(storm::utility::one<double>())); |
||||
|
} |
||||
|
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const { |
||||
|
return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(storm::utility::one<uint_fast64_t>())); |
||||
|
} |
||||
|
|
||||
|
#ifdef STORM_HAVE_CARL
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddOne() const { |
||||
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), storm::utility::one<storm::RationalFunction>())); |
||||
|
} |
||||
|
#endif
|
||||
|
|
||||
|
InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddZero() const { |
||||
|
return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddZero()); |
||||
|
} |
||||
|
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const { |
||||
|
return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(storm::utility::zero<double>())); |
||||
|
} |
||||
|
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const { |
||||
|
return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(storm::utility::zero<uint_fast64_t>())); |
||||
|
} |
||||
|
|
||||
|
#ifdef STORM_HAVE_CARL
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddZero() const { |
||||
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), storm::utility::zero<storm::RationalFunction>())); |
||||
|
} |
||||
|
#endif
|
||||
|
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const { |
||||
|
return InternalAdd<DdType::Sylvan, double>(this, sylvan::Mtbdd::doubleTerminal(value)); |
||||
|
} |
||||
|
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const { |
||||
|
return InternalAdd<DdType::Sylvan, uint_fast64_t>(this, sylvan::Mtbdd::int64Terminal(value)); |
||||
|
} |
||||
|
|
||||
|
#ifdef STORM_HAVE_CARL
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getConstant(storm::RationalFunction const& value) const { |
||||
|
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), storm::utility::zero<storm::RationalFunction>())); |
||||
|
} |
||||
|
#endif
|
||||
|
|
||||
|
std::pair<InternalBdd<DdType::Sylvan>, InternalBdd<DdType::Sylvan>> InternalDdManager<DdType::Sylvan>::createNewDdVariablePair() { |
||||
|
InternalBdd<DdType::Sylvan> first = InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddVar(nextFreeVariableIndex)); |
||||
|
InternalBdd<DdType::Sylvan> second = InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddVar(nextFreeVariableIndex + 1)); |
||||
|
nextFreeVariableIndex += 2; |
||||
|
return std::make_pair(first, second); |
||||
|
} |
||||
|
|
||||
|
void InternalDdManager<DdType::Sylvan>::allowDynamicReordering(bool value) { |
||||
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); |
||||
|
} |
||||
|
|
||||
|
bool InternalDdManager<DdType::Sylvan>::isDynamicReorderingAllowed() const { |
||||
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); |
||||
|
} |
||||
|
|
||||
|
void InternalDdManager<DdType::Sylvan>::triggerReordering() { |
||||
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); |
||||
|
} |
||||
|
|
||||
|
template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const; |
||||
|
template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const; |
||||
|
|
||||
|
template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const; |
||||
|
template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const; |
||||
|
|
||||
|
template InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const; |
||||
|
template InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const; |
||||
|
} |
||||
} |
} |
||||
@ -1,132 +1,148 @@ |
|||||
#ifndef STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ |
|
||||
#define STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ |
|
||||
|
|
||||
#include "src/storage/dd/DdType.h" |
|
||||
#include "src/storage/dd/InternalDdManager.h" |
|
||||
|
|
||||
#include "src/storage/dd/sylvan/InternalSylvanBdd.h" |
|
||||
#include "src/storage/dd/sylvan/InternalSylvanAdd.h" |
|
||||
|
|
||||
namespace storm { |
|
||||
namespace dd { |
|
||||
template<DdType LibraryType, typename ValueType> |
|
||||
class InternalAdd; |
|
||||
|
|
||||
template<DdType LibraryType> |
|
||||
class InternalBdd; |
|
||||
|
|
||||
template<> |
|
||||
class InternalDdManager<DdType::Sylvan> { |
|
||||
public: |
|
||||
friend class InternalBdd<DdType::Sylvan>; |
|
||||
|
|
||||
template<DdType LibraryType, typename ValueType> |
|
||||
friend class InternalAdd; |
|
||||
|
|
||||
/*! |
|
||||
* Creates a new internal manager for Sylvan DDs. |
|
||||
*/ |
|
||||
InternalDdManager(); |
|
||||
|
|
||||
/*! |
|
||||
* Destroys the internal manager. |
|
||||
*/ |
|
||||
~InternalDdManager(); |
|
||||
|
|
||||
/*! |
|
||||
* Retrieves a BDD representing the constant one function. |
|
||||
* |
|
||||
* @return A BDD representing the constant one function. |
|
||||
*/ |
|
||||
InternalBdd<DdType::Sylvan> getBddOne() const; |
|
||||
|
|
||||
/*! |
|
||||
* Retrieves an ADD representing the constant one function. |
|
||||
* |
|
||||
* @return An ADD representing the constant one function. |
|
||||
*/ |
|
||||
template<typename ValueType> |
|
||||
InternalAdd<DdType::Sylvan, ValueType> getAddOne() const; |
|
||||
|
|
||||
/*! |
|
||||
* Retrieves a BDD representing the constant zero function. |
|
||||
* |
|
||||
* @return A BDD representing the constant zero function. |
|
||||
*/ |
|
||||
InternalBdd<DdType::Sylvan> getBddZero() const; |
|
||||
|
|
||||
/*! |
|
||||
* Retrieves an ADD representing the constant zero function. |
|
||||
* |
|
||||
* @return An ADD representing the constant zero function. |
|
||||
*/ |
|
||||
template<typename ValueType> |
|
||||
InternalAdd<DdType::Sylvan, ValueType> getAddZero() const; |
|
||||
|
|
||||
/*! |
|
||||
* Retrieves an ADD representing the constant function with the given value. |
|
||||
* |
|
||||
* @return An ADD representing the constant function with the given value. |
|
||||
*/ |
|
||||
template<typename ValueType> |
|
||||
InternalAdd<DdType::Sylvan, ValueType> getConstant(ValueType const& value) const; |
|
||||
|
|
||||
/*! |
|
||||
* Creates a new pair of DD variables and returns the two cubes as a result. |
|
||||
* |
|
||||
* @return The two cubes belonging to the DD variables. |
|
||||
*/ |
|
||||
std::pair<InternalBdd<DdType::Sylvan>, InternalBdd<DdType::Sylvan>> createNewDdVariablePair(); |
|
||||
|
|
||||
/*! |
|
||||
* Sets whether or not dynamic reordering is allowed for the DDs managed by this manager. |
|
||||
* |
|
||||
* @param value If set to true, dynamic reordering is allowed and forbidden otherwise. |
|
||||
*/ |
|
||||
void allowDynamicReordering(bool value); |
|
||||
|
|
||||
/*! |
|
||||
* Retrieves whether dynamic reordering is currently allowed. |
|
||||
* |
|
||||
* @return True iff dynamic reordering is currently allowed. |
|
||||
*/ |
|
||||
bool isDynamicReorderingAllowed() const; |
|
||||
|
|
||||
/*! |
|
||||
* Triggers a reordering of the DDs managed by this manager. |
|
||||
*/ |
|
||||
void triggerReordering(); |
|
||||
|
|
||||
private: |
|
||||
// A counter for the number of instances of this class. This is used to determine when to initialize and |
|
||||
// quit the sylvan. This is because Sylvan does not know the concept of managers but implicitly has a |
|
||||
// 'global' manager. |
|
||||
static uint_fast64_t numberOfInstances; |
|
||||
|
|
||||
// The index of the next free variable index. This needs to be shared across all instances since the sylvan |
|
||||
// manager is implicitly 'global'. |
|
||||
static uint_fast64_t nextFreeVariableIndex; |
|
||||
}; |
|
||||
|
|
||||
template<> |
|
||||
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const; |
|
||||
|
|
||||
template<> |
|
||||
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const; |
|
||||
|
|
||||
template<> |
|
||||
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const; |
|
||||
|
|
||||
template<> |
|
||||
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const; |
|
||||
|
|
||||
template<> |
|
||||
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const; |
|
||||
|
|
||||
template<> |
|
||||
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const; |
|
||||
|
|
||||
} |
|
||||
} |
|
||||
|
|
||||
|
#ifndef STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ |
||||
|
#define STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ |
||||
|
|
||||
|
#include "src/storage/dd/DdType.h" |
||||
|
#include "src/storage/dd/InternalDdManager.h" |
||||
|
|
||||
|
#include "src/storage/dd/sylvan/InternalSylvanBdd.h" |
||||
|
#include "src/storage/dd/sylvan/InternalSylvanAdd.h" |
||||
|
|
||||
|
#include "src/adapters/CarlAdapter.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace dd { |
||||
|
template<DdType LibraryType, typename ValueType> |
||||
|
class InternalAdd; |
||||
|
|
||||
|
template<DdType LibraryType> |
||||
|
class InternalBdd; |
||||
|
|
||||
|
template<> |
||||
|
class InternalDdManager<DdType::Sylvan> { |
||||
|
public: |
||||
|
friend class InternalBdd<DdType::Sylvan>; |
||||
|
|
||||
|
template<DdType LibraryType, typename ValueType> |
||||
|
friend class InternalAdd; |
||||
|
|
||||
|
/*! |
||||
|
* Creates a new internal manager for Sylvan DDs. |
||||
|
*/ |
||||
|
InternalDdManager(); |
||||
|
|
||||
|
/*! |
||||
|
* Destroys the internal manager. |
||||
|
*/ |
||||
|
~InternalDdManager(); |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves a BDD representing the constant one function. |
||||
|
* |
||||
|
* @return A BDD representing the constant one function. |
||||
|
*/ |
||||
|
InternalBdd<DdType::Sylvan> getBddOne() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves an ADD representing the constant one function. |
||||
|
* |
||||
|
* @return An ADD representing the constant one function. |
||||
|
*/ |
||||
|
template<typename ValueType> |
||||
|
InternalAdd<DdType::Sylvan, ValueType> getAddOne() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves a BDD representing the constant zero function. |
||||
|
* |
||||
|
* @return A BDD representing the constant zero function. |
||||
|
*/ |
||||
|
InternalBdd<DdType::Sylvan> getBddZero() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves an ADD representing the constant zero function. |
||||
|
* |
||||
|
* @return An ADD representing the constant zero function. |
||||
|
*/ |
||||
|
template<typename ValueType> |
||||
|
InternalAdd<DdType::Sylvan, ValueType> getAddZero() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves an ADD representing the constant function with the given value. |
||||
|
* |
||||
|
* @return An ADD representing the constant function with the given value. |
||||
|
*/ |
||||
|
template<typename ValueType> |
||||
|
InternalAdd<DdType::Sylvan, ValueType> getConstant(ValueType const& value) const; |
||||
|
|
||||
|
/*! |
||||
|
* Creates a new pair of DD variables and returns the two cubes as a result. |
||||
|
* |
||||
|
* @return The two cubes belonging to the DD variables. |
||||
|
*/ |
||||
|
std::pair<InternalBdd<DdType::Sylvan>, InternalBdd<DdType::Sylvan>> createNewDdVariablePair(); |
||||
|
|
||||
|
/*! |
||||
|
* Sets whether or not dynamic reordering is allowed for the DDs managed by this manager. |
||||
|
* |
||||
|
* @param value If set to true, dynamic reordering is allowed and forbidden otherwise. |
||||
|
*/ |
||||
|
void allowDynamicReordering(bool value); |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether dynamic reordering is currently allowed. |
||||
|
* |
||||
|
* @return True iff dynamic reordering is currently allowed. |
||||
|
*/ |
||||
|
bool isDynamicReorderingAllowed() const; |
||||
|
|
||||
|
/*! |
||||
|
* Triggers a reordering of the DDs managed by this manager. |
||||
|
*/ |
||||
|
void triggerReordering(); |
||||
|
|
||||
|
private: |
||||
|
// A counter for the number of instances of this class. This is used to determine when to initialize and |
||||
|
// quit the sylvan. This is because Sylvan does not know the concept of managers but implicitly has a |
||||
|
// 'global' manager. |
||||
|
static uint_fast64_t numberOfInstances; |
||||
|
|
||||
|
// The index of the next free variable index. This needs to be shared across all instances since the sylvan |
||||
|
// manager is implicitly 'global'. |
||||
|
static uint_fast64_t nextFreeVariableIndex; |
||||
|
}; |
||||
|
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddOne() const; |
||||
|
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddOne() const; |
||||
|
|
||||
|
#ifdef STORM_HAVE_CARL |
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddOne() const; |
||||
|
#endif |
||||
|
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getAddZero() const; |
||||
|
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getAddZero() const; |
||||
|
|
||||
|
#ifdef STORM_HAVE_CARL |
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddZero() const; |
||||
|
#endif |
||||
|
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, double> InternalDdManager<DdType::Sylvan>::getConstant(double const& value) const; |
||||
|
|
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, uint_fast64_t> InternalDdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const; |
||||
|
|
||||
|
#ifdef STORM_HAVE_CARL |
||||
|
template<> |
||||
|
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getConstant(storm::RationalNumber const& value) const; |
||||
|
#endif |
||||
|
} |
||||
|
} |
||||
|
|
||||
#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ */ |
#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ */ |
||||
@ -1,15 +1,16 @@ |
|||||
#ifndef STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ |
|
||||
#define STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ |
|
||||
|
|
||||
#pragma clang diagnostic push |
|
||||
#pragma clang diagnostic ignored "-Wextra-semi" |
|
||||
#pragma clang diagnostic ignored "-Wzero-length-array" |
|
||||
#pragma clang diagnostic ignored "-Wgnu-zero-variadic-macro-arguments" |
|
||||
#pragma clang diagnostic ignored "-Wdeprecated-register" |
|
||||
#pragma clang diagnostic ignored "-Wc99-extensions" |
|
||||
|
|
||||
#include "sylvan_obj.hpp" |
|
||||
|
|
||||
#pragma clang diagnostic pop |
|
||||
|
|
||||
|
#ifndef STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ |
||||
|
#define STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ |
||||
|
|
||||
|
#pragma clang diagnostic push |
||||
|
#pragma clang diagnostic ignored "-Wextra-semi" |
||||
|
#pragma clang diagnostic ignored "-Wzero-length-array" |
||||
|
#pragma clang diagnostic ignored "-Wgnu-zero-variadic-macro-arguments" |
||||
|
#pragma clang diagnostic ignored "-Wdeprecated-register" |
||||
|
#pragma clang diagnostic ignored "-Wc99-extensions" |
||||
|
|
||||
|
#include "sylvan_obj.hpp" |
||||
|
#include "sylvan_storm_rational_function.h" |
||||
|
|
||||
|
#pragma clang diagnostic pop |
||||
|
|
||||
#endif /* STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ */ |
#endif /* STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ */ |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue