17#include "storm-config.h"
23#pragma clang diagnostic push
24#pragma clang diagnostic ignored "-Wzero-length-array"
25#pragma clang diagnostic ignored "-Wc99-extensions"
38VOID_TASK_2(execute_sylvan, std::function<
void()>
const*, f, std::exception_ptr*, e) {
41 }
catch (std::exception& exception) {
42 *e = std::current_exception();
47#pragma clang diagnostic pop
50uint_fast64_t InternalDdManager<DdType::Sylvan>::numberOfInstances = 0;
51bool InternalDdManager<DdType::Sylvan>::suspended =
false;
55uint_fast64_t InternalDdManager<DdType::Sylvan>::nextFreeVariableIndex = 0;
58 for (uint_fast64_t index = 0; index < 64; ++index) {
59 if ((number & (1ull << (63 - index))) != 0) {
67 if (numberOfInstances == 0) {
69 size_t const task_deque_size = 1024 * 1024;
71 lace_set_stacksize(1024 * 1024 * 16);
76 sylvan_init_package();
78 sylvan::Sylvan::initBdd();
79 sylvan::Sylvan::initMtbdd();
80 sylvan::Sylvan::initCustomMtbdd();
83 sylvan_gc_hook_pregc(TASK(gc_start));
84 sylvan_gc_hook_postgc(TASK(gc_end));
95 if (numberOfInstances == 0) {
101 sylvan::Sylvan::quitPackage();
128 sylvan::Mtbdd::stormRationalFunctionTerminal(storm::utility::one<storm::RationalFunction>()));
136 uint64_t numberOfDdVariables)
const {
137 return InternalBdd<DdType::Sylvan>(
this, sylvan::Bdd(this->getBddEncodingLessOrEqualThanRec(0, (1ull << numberOfDdVariables) - 1, bound,
138 cube.getSylvanBdd().GetBDD(), numberOfDdVariables)));
142 uint64_t remainingDdVariables)
const {
143 if (maximalValue <= bound) {
145 }
else if (minimalValue > bound) {
149 STORM_LOG_ASSERT(remainingDdVariables > 0,
"Expected more remaining DD variables.");
150 uint64_t newRemainingDdVariables = remainingDdVariables - 1;
152 getBddEncodingLessOrEqualThanRec(minimalValue, maximalValue & ~(1ull << newRemainingDdVariables), bound, sylvan_high(cube), newRemainingDdVariables);
153 bdd_refs_push(elseResult);
155 getBddEncodingLessOrEqualThanRec(minimalValue | (1ull << newRemainingDdVariables), maximalValue, bound, sylvan_high(cube), newRemainingDdVariables);
156 bdd_refs_push(elseResult);
157 BDD result = sylvan_makenode(sylvan_var(cube), elseResult, thenResult);
177#ifdef STORM_HAVE_CARL
181 sylvan::Mtbdd::stormRationalFunctionTerminal(storm::utility::zero<storm::RationalFunction>()));
185template<
typename ValueType>
205#ifdef STORM_HAVE_CARL
213 boost::optional<uint_fast64_t>
const& position) {
214 STORM_LOG_THROW(!position, storm::exceptions::NotSupportedException,
"The manager does not support ordered insertion.");
216 std::vector<InternalBdd<DdType::Sylvan>> result;
218 for (uint64_t layer = 0; layer < numberOfLayers; ++layer) {
220 ++nextFreeVariableIndex;
231 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Operation is not supported by sylvan.");
235 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Operation is not supported by sylvan.");
239 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Operation is not supported by sylvan.");
243 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Operation is not supported by sylvan.");
248 std::exception_ptr e =
nullptr;
252 RUN(execute_sylvan, &f, &e);
257 RUN(execute_sylvan, &f, &e);
260 std::rethrow_exception(e);
265 return nextFreeVariableIndex;
273#ifdef STORM_HAVE_CARL
This class represents the settings for Sylvan.
uint_fast64_t getNumberOfThreads() const
Retrieves the amount of threads available to Sylvan.
#define STORM_LOG_TRACE(message)
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
VOID_TASK_2(execute_sylvan, std::function< void()> const *, f, std::exception_ptr *, e)
uint_fast64_t findLargestPowerOfTwoFitting(uint_fast64_t number)
SettingsType const & getModule()
Get module.