Re-added option to export DFTs to smtlib2 SMT files

src/storm-dft-cli/storm-dft.cpp

@@ -51,6 +51,12 @@ void processOptions() {
         return;
     }
 
+    if (dftIOSettings.isExportToSmt()) {
+        // Export to json
+        storm::api::exportDFTToSMT<ValueType>(*dft, dftIOSettings.getExportSmtFilename());
+        return;
+    }
+
     // Check well-formedness of DFT
     std::stringstream stream;
     if (!dft->checkWellFormedness(stream)) {

src/storm-dft/api/storm-dft.cpp

@@ -50,6 +50,7 @@ namespace storm {
             std::vector<storm::solver::SmtSolver::CheckResult> results = smtChecker.toSolver();
 
             if (printOutput) {
+                // TODO add suitable output function, maybe add query descriptions for better readability
                 for (size_t i = 0; i < results.size(); ++i) {
                     std::string tmp = "unknonwn";
                     if (results.at(i) == storm::solver::SmtSolver::CheckResult::Sat) {

src/storm-dft/modelchecker/dft/DFTASFChecker.cpp

@@ -456,6 +456,8 @@ namespace storm {
             // Set backtracking marker to check several properties without reconstructing DFT encoding
             solver->push();
 
+            //TODO put different queries in separate functions for further modularization
+
             // Constraint that toplevel element will not fail (part of constraint 13)
             std::shared_ptr<SmtConstraint> tleNeverFailedConstr = std::make_shared<IsConstantValue>(
                     timePointVariables.at(dft.getTopLevelIndex()), notFailed);

src/storm-dft/modelchecker/dft/SmtConstraint.h

@@ -8,8 +8,19 @@ namespace storm {
             virtual ~SmtConstraint() {
             }
 
+            /** Generate a string describing the constraint in Smtlib2 format
+             *
+             * @param varNames vector of variable names
+             * @return Smtlib2 format string
+             */
             virtual std::string toSmtlib2(std::vector<std::string> const &varNames) const = 0;
 
+            /** Generate an expression describing the constraint in Storm format
+             *
+             * @param varNames vector of variable names
+             * @param manager the expression manager used to handle the expressions
+             * @return the expression
+             */
             virtual storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
                                                                 std::shared_ptr<storm::expressions::ExpressionManager> manager) const = 0;
 

src/storm-dft/settings/modules/DftIOSettings.cpp

@@ -25,6 +25,7 @@ namespace storm {
             const std::string DftIOSettings::minValueOptionName = "min";
             const std::string DftIOSettings::maxValueOptionName = "max";
             const std::string DftIOSettings::exportToJsonOptionName = "export-json";
+            const std::string DftIOSettings::exportToSmtOptionName = "export-smt";
             const std::string DftIOSettings::displayStatsOptionName = "show-dft-stats";
 
 
@@ -56,6 +57,11 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.")
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build())
                                         .build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportToSmtOptionName, false,
+                                                               "Export the model as SMT encoding to the smtlib2 format.")
+                                        .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename",
+                                                                                                            "The name of the smtlib2 file to export to.").build())
+                                        .build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, displayStatsOptionName, false, "Print stats to stdout").build());
             }
 
@@ -122,6 +128,14 @@ namespace storm {
                 return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString();
             }
 
+            bool DftIOSettings::isExportToSmt() const {
+                return this->getOption(exportToSmtOptionName).getHasOptionBeenSet();
+            }
+
+            std::string DftIOSettings::getExportSmtFilename() const {
+                return this->getOption(exportToSmtOptionName).getArgumentByName("filename").getValueAsString();
+            }
+
             bool DftIOSettings::isDisplayStatsSet() const {
                 return this->getOption(displayStatsOptionName).getHasOptionBeenSet();
             }

src/storm-dft/settings/modules/DftIOSettings.h

@@ -108,6 +108,13 @@ namespace storm {
                  */
                 bool isExportToJson() const;
 
+                /*!
+                 * Retrieves whether the export to smtlib2 file option was set.
+                 *
+                 * @return True if the export to smtlib2 file option was set.
+                 */
+                bool isExportToSmt() const;
+
                 /*!
                  * Retrieves the name of the json file to export to.
                  *
@@ -115,6 +122,13 @@ namespace storm {
                  */
                 std::string getExportJsonFilename() const;
 
+                /*!
+                 * Retrieves the name of the smtlib2 file to export to.
+                 *
+                 * @return The name of the smtlib2 file to export to.
+                 */
+                std::string getExportSmtFilename() const;
+
                 /*!
                  * Retrieves whether statistics for the DFT should be displayed.
                  *
@@ -142,6 +156,7 @@ namespace storm {
                 static const std::string minValueOptionName;
                 static const std::string maxValueOptionName;
                 static const std::string exportToJsonOptionName;
+                static const std::string exportToSmtOptionName;
                 static const std::string displayStatsOptionName;
 
             };

src/storm/solver/SmtSolver.h

@@ -50,7 +50,7 @@ namespace storm {
                 storm::expressions::ExpressionManager const& getManager() const;
                 
             private:
-                // The expression manager responsible for the variableswhose value can be requested via this model
+                // The expression manager responsible for the variables whose value can be requested via this model
                 // reference.
                 storm::expressions::ExpressionManager const& manager;
 			};