added sylvan settings. made sylvan available from the cli

Former-commit-id: 3d2403de90

src/cli/entrypoints.h

@@ -110,17 +110,17 @@ namespace storm {
         } \
     }
     
-        template<typename ValueType>
+        template<typename ValueType, storm::dd::DdType LibraryType>
         void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
-            std::shared_ptr<storm::models::ModelBase> model = buildSymbolicModel<ValueType>(program, formulas);
+            std::shared_ptr<storm::models::ModelBase> model = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
             STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
-
+            
             // Preprocess the model if needed.
-            BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulas);
-
+            BRANCH_ON_MODELTYPE(model, model, ValueType, LibraryType, preprocessModel, formulas);
+            
             // Print some information about the model.
             model->printModelInformationToStream(std::cout);
-
+            
             // Verify the model, if a formula was given.
             if (!formulas.empty()) {
                 if (model->isSparseModel()) {
@@ -134,15 +134,24 @@ namespace storm {
                     }
                 } else if (model->isSymbolicModel()) {
                     if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
-                        verifySymbolicModelWithHybridEngine(model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formulas);
+                        verifySymbolicModelWithHybridEngine(model->as<storm::models::symbolic::Model<LibraryType>>(), formulas);
                     } else {
-                        verifySymbolicModelWithSymbolicEngine(model->as<storm::models::symbolic::Model<storm::dd::DdType::CUDD>>(), formulas);
+                        verifySymbolicModelWithSymbolicEngine(model->as<storm::models::symbolic::Model<LibraryType>>(), formulas);
                     }
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
                 }
             }
         }
+        
+        template<typename ValueType>
+        void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
+            if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::CUDD) {
+                buildAndCheckSymbolicModel<ValueType, storm::dd::DdType::CUDD>(program, formulas);
+            } else if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::Sylvan) {
+                buildAndCheckSymbolicModel<ValueType, storm::dd::DdType::Sylvan>(program, formulas);
+            }
+        }
 
         template<typename ValueType>
         void buildAndCheckExplicitModel(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {

src/settings/SettingsManager.cpp

@@ -17,6 +17,7 @@
 #include "src/settings/modules/DebugSettings.h"
 #include "src/settings/modules/CounterexampleGeneratorSettings.h"
 #include "src/settings/modules/CuddSettings.h"
+#include "src/settings/modules/SylvanSettings.h"
 #include "src/settings/modules/GmmxxEquationSolverSettings.h"
 #include "src/settings/modules/NativeEquationSolverSettings.h"
 #include "src/settings/modules/BisimulationSettings.h"
@@ -38,6 +39,7 @@ namespace storm {
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::DebugSettings(*this)));
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::CounterexampleGeneratorSettings(*this)));
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::CuddSettings(*this)));
+            this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::SylvanSettings(*this)));
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GmmxxEquationSolverSettings(*this)));
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::NativeEquationSolverSettings(*this)));
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::BisimulationSettings(*this)));
@@ -509,6 +511,10 @@ namespace storm {
         storm::settings::modules::CuddSettings const& cuddSettings() {
             return dynamic_cast<storm::settings::modules::CuddSettings const&>(manager().getModule(storm::settings::modules::CuddSettings::moduleName));
         }
+
+        storm::settings::modules::SylvanSettings const& sylvanSettings() {
+            return dynamic_cast<storm::settings::modules::SylvanSettings const&>(manager().getModule(storm::settings::modules::SylvanSettings::moduleName));
+        }
         
         storm::settings::modules::GmmxxEquationSolverSettings const& gmmxxEquationSolverSettings() {
             return dynamic_cast<storm::settings::modules::GmmxxEquationSolverSettings const&>(manager().getModule(storm::settings::modules::GmmxxEquationSolverSettings::moduleName));

src/settings/SettingsManager.h

@@ -16,6 +16,7 @@ namespace storm {
             class DebugSettings;
             class CounterexampleGeneratorSettings;
             class CuddSettings;
+            class SylvanSettings;
             class GmmxxEquationSolverSettings;
             class NativeEquationSolverSettings;
             class BisimulationSettings;
@@ -267,6 +268,13 @@ namespace storm {
          * @return An object that allows accessing the CUDD settings.
          */
         storm::settings::modules::CuddSettings const& cuddSettings();
+
+        /*!
+         * Retrieves the Sylvan settings.
+         *
+         * @return An object that allows accessing the Sylvan settings.
+         */
+        storm::settings::modules::SylvanSettings const& sylvanSettings();
         
         /*!
          * Retrieves the settings of the gmm++-based equation solver.

src/settings/modules/CuddSettings.cpp

@@ -19,7 +19,7 @@ namespace storm {
             CuddSettings::CuddSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(2048).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(4096).build()).build());
                 
                 std::vector<std::string> reorderingTechniques;
                 reorderingTechniques.push_back("none");

src/settings/modules/GeneralSettings.cpp

@@ -8,6 +8,8 @@
 #include "src/settings/Argument.h"
 #include "src/solver/SolverSelectionOptions.h"
 
+#include "src/storage/dd/DdType.h"
+
 #include "src/exceptions/InvalidSettingsException.h"
 
 namespace storm {
@@ -51,6 +53,7 @@ namespace storm {
             const std::string GeneralSettings::bisimulationOptionShortName = "bisim";
             const std::string GeneralSettings::engineOptionName = "engine";
             const std::string GeneralSettings::engineOptionShortName = "e";
+            const std::string GeneralSettings::ddLibraryOptionName = "ddlib";
             const std::string GeneralSettings::cudaOptionName = "cuda";
             const std::string GeneralSettings::prismCompatibilityOptionName = "prismcompat";
             const std::string GeneralSettings::prismCompatibilityOptionShortName = "pc";
@@ -100,6 +103,10 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setShortName(timeoutOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "The number of seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build());
                 
+                std::vector<std::string> ddLibraries = {"cudd", "sylvan"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, ddLibraryOptionName, false, "Sets which library is preferred for decision-diagram operations.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer. Available are: cudd and sylvan.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(ddLibraries)).setDefaultValueString("cudd").build()).build());
+                
                 std::vector<std::string> lpSolvers = {"gurobi", "glpk"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build());
@@ -270,6 +277,15 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown SMT solver '" << smtSolverName << "'.");
             }
             
+            storm::dd::DdType GeneralSettings::getDdLibraryType() const {
+                std::string ddLibraryAsString = this->getOption(ddLibraryOptionName).getArgumentByName("name").getValueAsString();
+                if (ddLibraryAsString == "sylvan") {
+                    return storm::dd::DdType::Sylvan;
+                } else {
+                    return storm::dd::DdType::CUDD;
+                }
+            }
+            
             bool GeneralSettings::isConstantsSet() const {
                 return this->getOption(constantsOptionName).getHasOptionBeenSet();
             }

src/settings/modules/GeneralSettings.h

@@ -11,6 +11,10 @@ namespace storm {
         enum class MinMaxTechnique;
         enum class SmtSolverType;
     }
+    
+    namespace dd {
+        enum class DdType;
+    }
 
     namespace settings {
         namespace modules {
@@ -276,6 +280,13 @@ namespace storm {
                  */
                 storm::solver::SmtSolverType getSmtSolver() const;
                 
+                /*!
+                 * Retrieves the selected library for DD-related operations.
+                 *
+                 * @return The selected library.
+                 */
+                storm::dd::DdType getDdLibraryType() const;
+                
                 /*!
                  * Retrieves whether the export-to-dot option was set.
                  *
@@ -399,6 +410,7 @@ namespace storm {
                 static const std::string bisimulationOptionShortName;
                 static const std::string engineOptionName;
                 static const std::string engineOptionShortName;
+                static const std::string ddLibraryOptionName;
                 static const std::string cudaOptionName;
                 static const std::string prismCompatibilityOptionName;
                 static const std::string prismCompatibilityOptionShortName;

src/settings/modules/SylvanSettings.cpp

@@ -0,0 +1,33 @@
+#include "src/settings/modules/SylvanSettings.h"
+
+#include "src/settings/SettingsManager.h"
+
+#include "src/settings/Option.h"
+#include "src/settings/OptionBuilder.h"
+#include "src/settings/ArgumentBuilder.h"
+#include "src/settings/Argument.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string SylvanSettings::moduleName = "sylvan";
+            const std::string SylvanSettings::maximalMemoryOptionName = "maxmem";
+            const std::string SylvanSettings::threadCountOptionName = "threads";
+            
+            SylvanSettings::SylvanSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Sylvan in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Sylvan.").setDefaultValueUnsignedInteger(4096).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, threadCountOptionName, true, "Sets the number of threads used by Sylvan.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The number of threads available to Sylvan (0 means 'auto-detect').").setDefaultValueUnsignedInteger(0).build()).build());
+            }
+            
+            uint_fast64_t SylvanSettings::getMaximalMemory() const {
+                return this->getOption(maximalMemoryOptionName).getArgumentByName("value").getValueAsUnsignedInteger();
+            }
+            
+            uint_fast64_t SylvanSettings::getNumberOfThreads() const {
+                return this->getOption(threadCountOptionName).getArgumentByName("value").getValueAsUnsignedInteger();
+            }
+            
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/settings/modules/SylvanSettings.h

@@ -0,0 +1,50 @@
+#ifndef STORM_SETTINGS_MODULES_SYLVANSETTINGS_H_
+#define STORM_SETTINGS_MODULES_SYLVANSETTINGS_H_
+
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            /*!
+             * This class represents the settings for Sylvan.
+             */
+            class SylvanSettings : public ModuleSettings {
+            public:
+                /*!
+                 * Creates a new set of CUDD settings that is managed by the given manager.
+                 *
+                 * @param settingsManager The responsible manager.
+                 */
+                SylvanSettings(storm::settings::SettingsManager& settingsManager);
+                
+                /*!
+                 * Retrieves the maximal amount of memory (in megabytes) that Sylvan can occupy.
+                 *
+                 * @return The maximal amount of memory to use.
+                 */
+                uint_fast64_t getMaximalMemory() const;
+                
+                /*!
+                 * Retrieves the amount of threads available to Sylvan. Note that a value of zero means that the number
+                 * of threads is auto-detected to fit the current machine.
+                 *
+                 * @rreturn The number of threads.
+                 */
+                uint_fast64_t getNumberOfThreads() const;
+                
+                // The name of the module.
+                static const std::string moduleName;
+                
+            private:
+                // Define the string names of the options as constants.
+                static const std::string maximalMemoryOptionName;
+                static const std::string threadCountOptionName;
+            };
+            
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
+
+#endif /* STORM_SETTINGS_MODULES_SYLVANSETTINGS_H_ */

src/storage/dd/sylvan/InternalSylvanDdManager.cpp

@@ -1,8 +1,12 @@
 #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/NotImplementedException.h"
 #include "src/exceptions/NotSupportedException.h"
 
 #include <iostream>
@@ -15,13 +19,27 @@ namespace storm {
         // 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;
+                }
+            }
+        }
+        
         InternalDdManager<DdType::Sylvan>::InternalDdManager() {
             if (numberOfInstances == 0) {
                 // Initialize lace: auto-detect number of workers.
-                lace_init(0, 1000000);
+                lace_init(storm::settings::sylvanSettings().getNumberOfThreads(), 1000000);
                 lace_startup(0, 0, 0);
                 
-                sylvan::Sylvan::initPackage(1ull << 16, 1ull << 28, 1ul << 16, 1ull << 25);
+                // Each node takes 24 bytes and the maximal memory is specified in megabytes.
+                uint_fast64_t totalNodesToStore = storm::settings::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 : 0), 1ull << (powerOfTwo - 1), 1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 12 : 0), 1ull << (powerOfTwo - 1));
                 sylvan::Sylvan::initBdd(1);
                 sylvan::Sylvan::initMtbdd();
             }

src/utility/storm.cpp

@@ -29,7 +29,7 @@ namespace storm {
         }
     }
 
-    std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString)    {
+    std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString) {
         storm::parser::FormulaParser formulaParser;
         return parseFormulas(formulaParser, inputString);
     }

src/utility/storm.h

@@ -82,7 +82,7 @@ namespace storm {
     std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString);
     std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
             
-    template<typename ValueType>
+    template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
     std::shared_ptr<storm::models::ModelBase> buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
         std::shared_ptr<storm::models::ModelBase> result(nullptr);
 
@@ -104,11 +104,11 @@ namespace storm {
 
             result = storm::builder::ExplicitPrismModelBuilder<ValueType>().translateProgram(program, options);
         } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
-            typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
-            options = typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options(formulas);
+            typename storm::builder::DdPrismModelBuilder<LibraryType>::Options options;
+            options = typename storm::builder::DdPrismModelBuilder<LibraryType>::Options(formulas);
             options.addConstantDefinitionsFromString(program, constants);
 
-            result = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+            result = storm::builder::DdPrismModelBuilder<LibraryType>::translateProgram(program, options);
         }
 
         return result;