From bb18af75b6fa4bc4b8f0bfdb798078b0763f168d Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Tue, 7 Jul 2020 20:04:43 -0700
Subject: [PATCH] add initial support for dds

---
 src/core/result.cpp |  1 +
 src/mod_storage.cpp |  2 ++
 src/storage/dd.cpp  | 27 +++++++++++++++++++++++++++
 src/storage/dd.h    |  7 +++++++
 4 files changed, 37 insertions(+)
 create mode 100644 src/storage/dd.cpp
 create mode 100644 src/storage/dd.h

diff --git a/src/core/result.cpp b/src/core/result.cpp
index 70babdc..24ed729 100644
--- a/src/core/result.cpp
+++ b/src/core/result.cpp
@@ -70,6 +70,7 @@ void define_result(py::module& m) {
         .def("get_truth_values", &storm::modelchecker::ExplicitQualitativeCheckResult::getTruthValuesVector, "Get BitVector representing the truth values")
     ;
     py::class_<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>, std::shared_ptr<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>>>(m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result", qualitativeCheckResult)
+            .def("get_truth_values", &storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>::getTruthValuesVector, "Get Dd representing the truth values")
     ;
 
     // QuantitativeCheckResult
diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp
index 7576b25..552168c 100644
--- a/src/mod_storage.cpp
+++ b/src/mod_storage.cpp
@@ -1,6 +1,7 @@
 #include "common.h"
 
 #include "storage/bitvector.h"
+#include "storage/dd.h"
 #include "storage/model.h"
 #include "storage/matrix.h"
 #include "storage/distribution.h"
@@ -24,6 +25,7 @@ PYBIND11_MODULE(storage, m) {
 #endif
 
     define_bitvector(m);
+    define_dd<storm::dd::DdType::Sylvan>(m, "Sylvan");
     define_model(m);
     define_statevaluation(m);
     define_sparse_model(m);
diff --git a/src/storage/dd.cpp b/src/storage/dd.cpp
new file mode 100644
index 0000000..09b5a39
--- /dev/null
+++ b/src/storage/dd.cpp
@@ -0,0 +1,27 @@
+#include "dd.h"
+#include "storm/storage/dd/DdManager.h"
+#include "storm/storage/dd/Dd.h"
+#include "storm/storage/dd/Bdd.h"
+#include "src/helpers.h"
+
+template<storm::dd::DdType DdType>
+void define_dd(py::module& m, std::string const& libstring) {
+    py::class_<storm::dd::DdMetaVariable<DdType>> ddMetaVariable(m, (std::string("DdMetaVariable_") + libstring).c_str());
+    ddMetaVariable.def("compute_indices", &storm::dd::DdMetaVariable<DdType>::getIndices, py::arg("sorted")=true);
+    ddMetaVariable.def_property_readonly("name", &storm::dd::DdMetaVariable<DdType>::getName);
+
+    py::class_<storm::dd::DdManager<DdType>, std::shared_ptr<storm::dd::DdManager<DdType>>> ddManager(m, (std::string("DdManager_") + libstring).c_str());
+    //ddManager.def("get_meta_variable", &storm::dd::DdManager<DdType>::getMetaVariable, py::arg("expression_variable"));
+
+    py::class_<storm::dd::Dd<DdType>> dd(m, (std::string("Dd_") + libstring).c_str(), "Dd");
+    dd.def_property_readonly("node_count", &storm::dd::Dd<DdType>::getNodeCount, "get node count");
+    dd.def_property_readonly("dd_manager", &storm::dd::Dd<DdType>::getDdManager, "get the manager");
+    dd.def_property_readonly("meta_variables", [](storm::dd::Dd<DdType> const& dd) {return dd.getContainedMetaVariables();}, "the contained meta variables");
+
+
+    py::class_<storm::dd::Bdd<DdType>> bdd(m, (std::string("Bdd_") + libstring).c_str(), "Bdd", dd);
+    bdd.def("to_expression", &storm::dd::Bdd<DdType>::toExpression, py::arg("expression_manager"));
+}
+
+
+template void define_dd<storm::dd::DdType::Sylvan>(py::module& m, std::string const& libstring);
\ No newline at end of file
diff --git a/src/storage/dd.h b/src/storage/dd.h
new file mode 100644
index 0000000..9d9df2a
--- /dev/null
+++ b/src/storage/dd.h
@@ -0,0 +1,7 @@
+#pragma once
+
+#include "common.h"
+#include "storm/storage/dd/DdType.h"
+
+template<storm::dd::DdType DdType>
+void define_dd(py::module& m, std::string const& libname);