Browse Source

Fixed template specialization.

Re-Implemented terminal generation.


Former-commit-id: 253f95b673
tempestpy_adaptions
PBerger 8 years ago
parent
commit
dbbae87962
  1. 3
      src/storage/dd/DdManager.cpp
  2. 7
      src/storage/dd/sylvan/InternalSylvanDdManager.cpp

3
src/storage/dd/DdManager.cpp

@ -108,13 +108,14 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template<>
template<>
Add<DdType::Sylvan, storm::RationalFunction> DdManager<DdType::Sylvan>::getIdentity(storm::expressions::Variable const& variable) const {
storm::dd::DdMetaVariable<DdType::Sylvan> const& metaVariable = this->getMetaVariable(variable);
Add<DdType::Sylvan, storm::RationalFunction> result = this->getAddZero<storm::RationalFunction>();
for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
storm::RationalFunction constantFunction(value);
result += this->getEncoding(variable, value).template toAdd<ValueType>() * this->getConstant(constantFunction);
result += this->getEncoding(variable, value).template toAdd<storm::RationalFunction>() * this->getConstant(constantFunction);
}
return result;
}

7
src/storage/dd/sylvan/InternalSylvanDdManager.cpp

@ -131,12 +131,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template<>
InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getConstant(storm::RationalFunction const& value) const {
storm::RationalFunction rationalFunction = value;
storm_rational_function_ptr_struct helperStruct;
helperStruct.storm_rational_function = (void*)(&rationalFunction);
uint64_t terminalValue = (uint64_t)&helperStruct;
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), terminalValue));
return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this, sylvan::Mtbdd::stormRationalFunctionTerminal(value));
}
#endif

Loading…
Cancel
Save