From 5a0c54034ebd36114da4d505b5cce20a16f1e7db Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 30 Nov 2015 15:40:08 +0100
Subject: [PATCH] committed missing files

Former-commit-id: c72bc0b44db01878f92ad7b49ea1bc79314d2a7c
---
 .../sylvan/src/sylvan_obj_bdd_storm.hpp       |   1 +
 .../sylvan/src/sylvan_obj_mtbdd_storm.hpp     |  42 +++++++
 .../3rdparty/sylvan/src/sylvan_obj_storm.cpp  | 112 ++++++++++++++++++
 3 files changed, 155 insertions(+)
 create mode 100644 resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp
 create mode 100644 resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp
 create mode 100644 resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp

diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp
new file mode 100644
index 000000000..c5020144b
--- /dev/null
+++ b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp
@@ -0,0 +1 @@
+    Mtbdd toDoubleMtbdd() const;
diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp
new file mode 100644
index 000000000..90f62ffa3
--- /dev/null
+++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp
@@ -0,0 +1,42 @@
+    /**
+     * @brief Computes f - g
+     */
+    Mtbdd Minus(const Mtbdd &other) const;
+
+    /**
+     * @brief Computes f / g
+     */
+    Mtbdd Divide(const Mtbdd &other) const;
+    
+    Bdd NotZero() const;
+    
+    Bdd Equals(const Mtbdd& other) const;
+    
+    Bdd Less(const Mtbdd& other) const;
+
+    Bdd LessOrEqual(const Mtbdd& other) const;
+    
+    double getDoubleMax() const;
+
+    double getDoubleMin() const;
+    
+    bool EqualNorm(const Mtbdd& other, double epsilon) const;
+
+    bool EqualNormRel(const Mtbdd& other, double epsilon) const;
+    
+    Mtbdd Floor() const;
+
+    Mtbdd Ceil() const;
+    
+    Mtbdd Pow(const Mtbdd& other) const;
+
+    Mtbdd Mod(const Mtbdd& other) const;
+
+    Mtbdd Logxy(const Mtbdd& other) const;
+    
+    size_t CountLeaves() const;
+
+    /**
+     * @brief Compute the number of non-zero variable assignments, using variables in cube.
+     */
+    double NonZeroCount(size_t variableCount) const;
\ No newline at end of file
diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp
new file mode 100644
index 000000000..a080e5698
--- /dev/null
+++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp
@@ -0,0 +1,112 @@
+Mtbdd
+Bdd::toDoubleMtbdd() const {
+    LACE_ME;
+    return mtbdd_bool_to_double(bdd);
+}
+
+Mtbdd
+Mtbdd::Minus(const Mtbdd &other) const
+{
+    LACE_ME;
+    return mtbdd_minus(mtbdd, other.mtbdd);
+}
+
+Mtbdd
+Mtbdd::Divide(const Mtbdd &other) const
+{
+    LACE_ME;
+    return mtbdd_divide(mtbdd, other.mtbdd);
+}
+
+Bdd
+Mtbdd::NotZero() const
+{
+    LACE_ME;
+    return mtbdd_not_zero(mtbdd);
+}
+
+Bdd
+Mtbdd::Equals(const Mtbdd& other) const {
+    LACE_ME;
+    return mtbdd_equals(mtbdd, other.mtbdd);
+}
+
+Bdd
+Mtbdd::Less(const Mtbdd& other) const {
+    LACE_ME;
+    return mtbdd_less_as_bdd(mtbdd, other.mtbdd);
+}
+
+Bdd
+Mtbdd::LessOrEqual(const Mtbdd& other) const {
+    LACE_ME;
+    return mtbdd_less_or_equal_as_bdd(mtbdd, other.mtbdd);
+}
+
+double
+Mtbdd::getDoubleMax() const {
+    LACE_ME;
+    MTBDD maxNode = mtbdd_maximum(mtbdd);
+    return mtbdd_getdouble(maxNode);
+}
+
+double
+Mtbdd::getDoubleMin() const {
+    LACE_ME;
+    MTBDD minNode = mtbdd_minimum(mtbdd);
+    return mtbdd_getdouble(minNode);
+}
+
+bool
+Mtbdd::EqualNorm(const Mtbdd& other, double epsilon) const {
+    LACE_ME;
+    return mtbdd_equal_norm_d(mtbdd, other.mtbdd, epsilon);
+}
+
+bool
+Mtbdd::EqualNormRel(const Mtbdd& other, double epsilon) const {
+    LACE_ME;
+    return mtbdd_equal_norm_rel_d(mtbdd, other.mtbdd, epsilon);
+}
+
+Mtbdd
+Mtbdd::Floor() const {
+    LACE_ME;
+    return mtbdd_floor(mtbdd);
+}
+
+Mtbdd
+Mtbdd::Ceil() const {
+    LACE_ME;
+    return mtbdd_ceil(mtbdd);
+}
+
+Mtbdd
+Mtbdd::Pow(const Mtbdd& other) const {
+    LACE_ME;
+    return mtbdd_pow(mtbdd, other.mtbdd);
+}
+
+Mtbdd
+Mtbdd::Mod(const Mtbdd& other) const {
+    LACE_ME;
+    return mtbdd_mod(mtbdd, other.mtbdd);
+}
+
+Mtbdd
+Mtbdd::Logxy(const Mtbdd& other) const {
+    LACE_ME;
+    return mtbdd_logxy(mtbdd, other.mtbdd);
+}
+
+size_t
+Mtbdd::CountLeaves() const {
+    LACE_ME;
+    return mtbdd_leafcount(mtbdd);
+}
+
+double
+Mtbdd::NonZeroCount(size_t variableCount) const {
+    LACE_ME;
+    return mtbdd_non_zero_count(mtbdd, variableCount);
+}