From 7ea0cb19b356e863f342f2424d7c5befc8b3f313 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 26 Nov 2015 22:29:24 +0100
Subject: [PATCH] added some new functions to sylvan. isolated new code to make
 it easier to update sylvan to newer versions later

Former-commit-id: 6b489993a50ea680fe928e9305d950a7caf04415
---
 resources/3rdparty/sylvan/src/sylvan_mtbdd.c  | 302 +-----------
 resources/3rdparty/sylvan/src/sylvan_mtbdd.h  |  65 +--
 resources/3rdparty/sylvan/src/sylvan_obj.cpp  |  43 ++
 resources/3rdparty/sylvan/src/sylvan_obj.hpp  |  14 +
 .../3rdparty/sylvan/src/sylvan_storm_custom.c | 464 ++++++++++++++++++
 .../3rdparty/sylvan/src/sylvan_storm_custom.h |  95 ++++
 src/storage/dd/sylvan/InternalSylvanAdd.cpp   |  20 +-
 test/functional/storage/SylvanDdTest.cpp      |  20 +-
 8 files changed, 643 insertions(+), 380 deletions(-)
 create mode 100644 resources/3rdparty/sylvan/src/sylvan_storm_custom.c
 create mode 100644 resources/3rdparty/sylvan/src/sylvan_storm_custom.h

diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c
index 311bb9a3d..d7cf736f8 100644
--- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c
+++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c
@@ -1191,81 +1191,6 @@ TASK_IMPL_2(MTBDD, mtbdd_op_times, MTBDD*, pa, MTBDD*, pb)
     return mtbdd_invalid;
 }
 
-/**
- * Binary operation Times (for MTBDDs of same type)
- * Only for MTBDDs where either all leaves are Integer or Double.
- * If either operand is mtbdd_false (not defined),
- * then the result is mtbdd_false (i.e. not defined).
- */
-TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb)
-{
-    MTBDD a = *pa, b = *pb;
-    if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false;
-    
-    // Do not handle Boolean MTBDDs...
-    
-    mtbddnode_t na = GETNODE(a);
-    mtbddnode_t nb = GETNODE(b);
-    
-    if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
-        uint64_t val_a = mtbddnode_getvalue(na);
-        uint64_t val_b = mtbddnode_getvalue(nb);
-        if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // both uint64_t
-            if (val_a == 0) return a;
-            else if (val_b == 0) return b;
-            else {
-                MTBDD result;
-                if (val_a == 1) result = b;
-                else if (val_b == 1) result = a;
-                else result = mtbdd_uint64(val_a*val_b);
-                int nega = mtbdd_isnegated(a);
-                int negb = mtbdd_isnegated(b);
-                if (nega ^ negb) return mtbdd_negate(result);
-                else return result;
-            }
-        } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
-            // both double
-            double vval_a = *(double*)&val_a;
-            double vval_b = *(double*)&val_b;
-            if (vval_a == 0.0) return a;
-            else if (vval_b == 0.0) return b;
-            else {
-                MTBDD result;
-                if (vval_a == 0.0 || vval_b == 1.0) result = a;
-
-                int nega = mtbdd_isnegated(a);
-                int negb = mtbdd_isnegated(b);
-                result = mtbdd_double(a / b);
-                if (nega ^ negb) return mtbdd_negate(result);
-                else return result;
-            }
-        }
-        else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
-            // both fraction
-            uint64_t nom_a = val_a>>32;
-            uint64_t nom_b = val_b>>32;
-            uint64_t denom_a = val_a&0xffffffff;
-            uint64_t denom_b = val_b&0xffffffff;
-            // multiply!
-            uint32_t c = gcd(denom_b, denom_a);
-            uint32_t d = gcd(nom_a, nom_b);
-            nom_a /= d;
-            denom_a /= c;
-            nom_a *= (denom_b/c);
-            denom_a *= (nom_b/d);
-            // compute result
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            MTBDD result = mtbdd_fraction(nom_a, denom_a);
-            if (nega ^ negb) return mtbdd_negate(result);
-            else return result;
-        }
-    }
-    
-    return mtbdd_invalid;
-}
-
 /**
  * Binary operation Minimum (for MTBDDs of same type)
  * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
@@ -1422,188 +1347,6 @@ TASK_IMPL_2(MTBDD, mtbdd_op_max, MTBDD*, pa, MTBDD*, pb)
     return mtbdd_invalid;
 }
 
-/**
- * Binary operation Equals (for MTBDDs of same type)
- * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
- * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
- * then the result is mtbdd_false (i.e. not defined).
- */
-TASK_IMPL_2(MTBDD, mtbdd_op_equals, MTBDD*, pa, MTBDD*, pb)
-{
-    MTBDD a = *pa, b = *pb;
-    if (a == mtbdd_false && b == mtbdd_false) return mtbdd_true;
-    if (a == mtbdd_true && b == mtbdd_true) return mtbdd_true;
-    
-    mtbddnode_t na = GETNODE(a);
-    mtbddnode_t nb = GETNODE(b);
-    
-    if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
-        uint64_t val_a = mtbddnode_getvalue(na);
-        uint64_t val_b = mtbddnode_getvalue(nb);
-        if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // both uint64_t
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (val_a == val_b && !(nega ^ negb)) return mtbdd_true;
-            return mtbdd_false;
-        } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
-            // both double
-            double vval_a = *(double*)&val_a;
-            double vval_b = *(double*)&val_b;
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (vval_a == vval_b && !(nega ^ negb)) return mtbdd_true;
-            return mtbdd_false;
-        } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
-            // both fraction
-            uint64_t nom_a = val_a>>32;
-            uint64_t nom_b = val_b>>32;
-            uint64_t denom_a = val_a&0xffffffff;
-            uint64_t denom_b = val_b&0xffffffff;
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nom_a == nom_b && denom_a == denom_b && !(nega ^ negb)) return mtbdd_true;
-            return mtbdd_false;
-        }
-    }
-    
-    if (a < b) {
-        *pa = b;
-        *pb = a;
-    }
-    
-    return mtbdd_invalid;
-}
-
-/**
- * Binary operation Equals (for MTBDDs of same type)
- * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
- * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
- * then the result is mtbdd_false (i.e. not defined).
- */
-TASK_IMPL_2(MTBDD, mtbdd_op_less, MTBDD*, pa, MTBDD*, pb)
-{
-    MTBDD a = *pa, b = *pb;
-    if (a == mtbdd_false && b == mtbdd_false) return mtbdd_true;
-    if (a == mtbdd_true && b == mtbdd_true) return mtbdd_true;
-    
-    mtbddnode_t na = GETNODE(a);
-    mtbddnode_t nb = GETNODE(b);
-    
-    if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
-        uint64_t val_a = mtbddnode_getvalue(na);
-        uint64_t val_b = mtbddnode_getvalue(nb);
-        if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // both uint64_t
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nega && !negb) return mtbdd_true;
-            if (!nega && negb) return mtbdd_false;
-            if (nega && negb && val_a < val_b) return mtbdd_false;
-            return mtbdd_true;
-        } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
-            // both double
-            double vval_a = *(double*)&val_a;
-            double vval_b = *(double*)&val_b;
-            int nega = mtbdd_isnegated(a);
-            if (nega) vval_a = -vval_a;
-            int negb = mtbdd_isnegated(b);
-            if (negb) vval_b = -vval_b;
-            if (vval_a < vval_b) return mtbdd_true;
-            return mtbdd_false;
-        } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
-            // both fraction
-            uint64_t nom_a = val_a>>32;
-            uint64_t nom_b = val_b>>32;
-            uint64_t denom_a = val_a&0xffffffff;
-            uint64_t denom_b = val_b&0xffffffff;
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nega && !negb) return mtbdd_true;
-            if (!nega && negb) return mtbdd_false;
-            return nom_a * denom_b < nom_b * denom_a ? mtbdd_true : mtbdd_false;
-        }
-    }
-    
-    return mtbdd_invalid;
-}
-
-/**
- * Binary operation Equals (for MTBDDs of same type)
- * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
- * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
- * then the result is mtbdd_false (i.e. not defined).
- */
-TASK_IMPL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, pa, MTBDD*, pb)
-{
-    MTBDD a = *pa, b = *pb;
-    if (a == mtbdd_false && b == mtbdd_false) return mtbdd_true;
-    if (a == mtbdd_true && b == mtbdd_true) return mtbdd_true;
-    
-    mtbddnode_t na = GETNODE(a);
-    mtbddnode_t nb = GETNODE(b);
-    
-    if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
-        uint64_t val_a = mtbddnode_getvalue(na);
-        uint64_t val_b = mtbddnode_getvalue(nb);
-        if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
-            // both uint64_t
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            if (nega && !negb) {
-                if (val_a != 0) return mtbdd_true;
-                if (val_b != 0) return mtbdd_true;
-                return mtbdd_false;
-            }
-            if (!nega && negb) {
-                if (val_b != 0) return mtbdd_false;
-                if (val_a != 0) return mtbdd_false;
-                return mtbdd_true;
-            }
-            if (nega && negb) {
-                return val_a >= val_b ? mtbdd_true : mtbdd_false;
-            }
-            return val_a <= val_b ? mtbdd_true : mtbdd_false;
-        } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
-            // both double
-            double vval_a = *(double*)&val_a;
-            double vval_b = *(double*)&val_b;
-            int nega = mtbdd_isnegated(a);
-            if (nega) vval_a = -vval_a;
-            int negb = mtbdd_isnegated(b);
-            if (negb) vval_b = -vval_b;
-            if (vval_a <= vval_b) return mtbdd_true;
-            return mtbdd_false;
-        } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
-            // both fraction
-            uint64_t nom_a = val_a>>32;
-            uint64_t nom_b = val_b>>32;
-            uint64_t denom_a = val_a&0xffffffff;
-            uint64_t denom_b = val_b&0xffffffff;
-            int nega = mtbdd_isnegated(a);
-            int negb = mtbdd_isnegated(b);
-            nom_a *= denom_b;
-            nom_b *= denom_a;
-            if (nega && !negb) {
-                if (nom_a != 0) return mtbdd_true;
-                if (nom_b != 0) return mtbdd_true;
-                return mtbdd_false;
-            }
-            if (!nega && negb) {
-                if (nom_a != 0) return mtbdd_false;
-                if (nom_b != 0) return mtbdd_false;
-                return mtbdd_true;
-            }
-            if (nega && negb) {
-                return nom_a >= nom_b ? mtbdd_true : mtbdd_false;
-            }
-            return val_a <= val_b ? mtbdd_true : mtbdd_false;
-        }
-    }
-    
-    return mtbdd_invalid;
-}
-
 /**
  * Compute IF <f> THEN <g> ELSE <h>.
  * <f> must be a Boolean MTBDD (or standard BDD).
@@ -1712,39 +1455,6 @@ TASK_IMPL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, a, size_t, svalue)
     return mtbdd_invalid;
 }
 
-TASK_IMPL_2(MTBDD, mtbdd_op_not_zero, MTBDD, a, size_t, v)
-{
-    /* We only expect "double" terminals, or false */
-    if (a == mtbdd_false) return mtbdd_false;
-    if (a == mtbdd_true) return mtbdd_invalid;
-    
-    // a != constant
-    mtbddnode_t na = GETNODE(a);
-    
-    if (mtbddnode_isleaf(na)) {
-        if (mtbddnode_gettype(na) == 0) {
-            return mtbdd_getuint64(a) != 0 ? mtbdd_true : mtbdd_false;
-        } else if (mtbddnode_gettype(na) == 1) {
-            return mtbdd_getdouble(a) != 0.0 ? mtbdd_true : mtbdd_false;
-        } else if (mtbddnode_gettype(na) == 2) {
-            return mtbdd_getnumer(a) != 0 ? mtbdd_true : mtbdd_false;
-        }
-    }
-    
-    // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
-    return v > 0 ? mtbdd_invalid : mtbdd_invalid;
-}
-
-TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, a, size_t, v)
-{
-    /* We only expect "double" terminals, or false */
-    if (a == mtbdd_false) return mtbdd_double(0);
-    if (a == mtbdd_true) return mtbdd_double(1.0);
-    
-    // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
-    return v > 0 ? mtbdd_invalid : mtbdd_invalid;
-}
-
 TASK_IMPL_2(MTBDD, mtbdd_threshold_double, MTBDD, dd, double, d)
 {
     return mtbdd_uapply(dd, TASK(mtbdd_op_threshold_double), *(size_t*)&d);
@@ -1755,16 +1465,6 @@ TASK_IMPL_2(MTBDD, mtbdd_strict_threshold_double, MTBDD, dd, double, d)
     return mtbdd_uapply(dd, TASK(mtbdd_op_strict_threshold_double), *(size_t*)&d);
 }
 
-TASK_IMPL_1(MTBDD, mtbdd_not_zero, MTBDD, dd)
-{
-    return mtbdd_uapply(dd, TASK(mtbdd_op_not_zero), 0);
-}
-
-TASK_IMPL_1(MTBDD, mtbdd_bool_to_double, MTBDD, dd)
-{
-    return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_double), 0);
-}
-
 /**
  * Compare two Double MTBDDs, returns Boolean True if they are equal within some value epsilon
  */
@@ -2881,3 +2581,5 @@ mtbdd_map_removeall(MTBDDMAP map, MTBDD variables)
         return mtbdd_map_removeall(node_getlow(map, n1), node_gethigh(variables, n2));
     }
 }
+
+#include "sylvan_storm_custom.c"
diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h
index c3fddc9ac..a6c6ebf62 100644
--- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h
+++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h
@@ -223,14 +223,6 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_plus, MTBDD, MTBDD, int);
  */
 TASK_DECL_2(MTBDD, mtbdd_op_times, MTBDD*, MTBDD*);
 TASK_DECL_3(MTBDD, mtbdd_abstract_op_times, MTBDD, MTBDD, int);
-
-/**
- * Binary operation Divide (for MTBDDs of same type)
- * Only for MTBDDs where all leaves are Integer or Double.
- * If either operand is mtbdd_false (not defined),
- * then the result is mtbdd_false (i.e. not defined).
- */
-TASK_DECL_2(MTBDD, mtbdd_op_divide, MTBDD*, MTBDD*);
     
 /**
  * Binary operation Minimum (for MTBDDs of same type)
@@ -249,35 +241,6 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_min, MTBDD, MTBDD, int);
  */
 TASK_DECL_2(MTBDD, mtbdd_op_max, MTBDD*, MTBDD*);
 TASK_DECL_3(MTBDD, mtbdd_abstract_op_max, MTBDD, MTBDD, int);
-
-/**
- * Binary operation equals (for MTBDDs of same type)
- * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
- * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
- * then the result is the other operand.
- */
-TASK_DECL_2(MTBDD, mtbdd_op_equals, MTBDD*, MTBDD*);
-
-/**
- * Binary operation Less (for MTBDDs of same type)
- * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
- * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
- * then the result is the other operand.
- */
-TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*);
-
-/**
- * Binary operation Less (for MTBDDs of same type)
- * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
- * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
- * then the result is the other operand.
- */
-TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*);
-    
-/**
- * Compute a == b
- */
-#define mtbdd_equals(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_equals))
     
 /**
  * Compute a + b
@@ -287,17 +250,12 @@ TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*);
 /**
  * Compute a - b
  */
-#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(b))
+//#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(b))
 
 /**
  * Compute a * b
  */
 #define mtbdd_times(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_times))
-
-/**
- * Compute a / b
- */
-#define mtbdd_divide(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_divide))
     
 /**
  * Compute min(a, b)
@@ -308,9 +266,6 @@ TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*);
  * Compute max(a, b)
  */
 #define mtbdd_max(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_max))
-    
-#define mtbdd_less_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less))
-#define mtbdd_less_or_equal_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less_or_equal))
 
 /**
  * Abstract the variables in <v> from <a> by taking the sum of all values
@@ -355,16 +310,6 @@ TASK_DECL_2(MTBDD, mtbdd_op_threshold_double, MTBDD, size_t)
  * Monad that converts double to a Boolean MTBDD, translate terminals > value to 1 and to 0 otherwise;
  */
 TASK_DECL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, size_t)
-
-/**
- * Monad that converts double to a Boolean MTBDD, translate terminals != 0 to 1 and to 0 otherwise;
- */
-TASK_DECL_2(MTBDD, mtbdd_op_not_zero, MTBDD, size_t)
-    
-/**
- * Monad that converts Boolean to a Double MTBDD, translate terminals true to 1 and to 0 otherwise;
- */
-TASK_DECL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, size_t)
     
 /**
  * Convert double to a Boolean MTBDD, translate terminals >= value to 1 and to 0 otherwise;
@@ -377,12 +322,6 @@ TASK_DECL_2(MTBDD, mtbdd_threshold_double, MTBDD, double);
  */
 TASK_DECL_2(MTBDD, mtbdd_strict_threshold_double, MTBDD, double);
 #define mtbdd_strict_threshold_double(dd, value) CALL(mtbdd_strict_threshold_double, dd, value)
-
-TASK_DECL_1(MTBDD, mtbdd_not_zero, MTBDD)
-#define mtbdd_not_zero(dd) CALL(mtbdd_not_zero, dd)
-    
-TASK_DECL_1(MTBDD, mtbdd_bool_to_double, MTBDD)
-#define mtbdd_bool_to_double(dd) CALL(mtbdd_bool_to_double, dd)
     
 /**
  * For two Double MTBDDs, calculate whether they are equal module some value epsilon
@@ -612,6 +551,8 @@ mtbdd_refs_sync(MTBDD result)
     return result;
 }
 
+#include "sylvan_storm_custom.h"
+    
 #ifdef __cplusplus
 }
 #endif /* __cplusplus */
diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp
index f62acd795..2eadee308 100644
--- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp
+++ b/resources/3rdparty/sylvan/src/sylvan_obj.cpp
@@ -944,6 +944,49 @@ Mtbdd::getDoubleMin() const {
     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);
+}
+
+
 Mtbdd
 Mtbdd::Support() const
 {
diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp
index bee74053b..907a22c38 100644
--- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp
+++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp
@@ -604,6 +604,20 @@ public:
 
     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;
+
     /**
      * @brief Computes the support of a Mtbdd.
      */
diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_custom.c b/resources/3rdparty/sylvan/src/sylvan_storm_custom.c
new file mode 100644
index 000000000..6cf7178d6
--- /dev/null
+++ b/resources/3rdparty/sylvan/src/sylvan_storm_custom.c
@@ -0,0 +1,464 @@
+/**
+ * Binary operation Times (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Integer or Double.
+ * If either operand is mtbdd_false (not defined),
+ * then the result is mtbdd_false (i.e. not defined).
+ */
+TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb)
+{
+    MTBDD a = *pa, b = *pb;
+    if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false;
+    
+    // Do not handle Boolean MTBDDs...
+    
+    mtbddnode_t na = GETNODE(a);
+    mtbddnode_t nb = GETNODE(b);
+    
+    if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
+        uint64_t val_a = mtbddnode_getvalue(na);
+        uint64_t val_b = mtbddnode_getvalue(nb);
+        if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
+            // both uint64_t
+            if (val_a == 0) return a;
+            else if (val_b == 0) return b;
+            else {
+                MTBDD result;
+                if (val_a == 1) result = b;
+                else if (val_b == 1) result = a;
+                else result = mtbdd_uint64(val_a*val_b);
+                int nega = mtbdd_isnegated(a);
+                int negb = mtbdd_isnegated(b);
+                if (nega ^ negb) return mtbdd_negate(result);
+                else return result;
+            }
+        } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
+            // both double
+            double vval_a = *(double*)&val_a;
+            double vval_b = *(double*)&val_b;
+            if (vval_a == 0.0) return a;
+            else if (vval_b == 0.0) return b;
+            else {
+                MTBDD result;
+                if (vval_a == 0.0 || vval_b == 1.0) result = a;
+                
+                int nega = mtbdd_isnegated(a);
+                int negb = mtbdd_isnegated(b);
+                result = mtbdd_double(a / b);
+                if (nega ^ negb) return mtbdd_negate(result);
+                else return result;
+            }
+        }
+        else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
+            // both fraction
+            uint64_t nom_a = val_a>>32;
+            uint64_t nom_b = val_b>>32;
+            uint64_t denom_a = val_a&0xffffffff;
+            uint64_t denom_b = val_b&0xffffffff;
+            // multiply!
+            uint32_t c = gcd(denom_b, denom_a);
+            uint32_t d = gcd(nom_a, nom_b);
+            nom_a /= d;
+            denom_a /= c;
+            nom_a *= (denom_b/c);
+            denom_a *= (nom_b/d);
+            // compute result
+            int nega = mtbdd_isnegated(a);
+            int negb = mtbdd_isnegated(b);
+            MTBDD result = mtbdd_fraction(nom_a, denom_a);
+            if (nega ^ negb) return mtbdd_negate(result);
+            else return result;
+        }
+    }
+    
+    return mtbdd_invalid;
+}
+
+/**
+ * Binary operation Equals (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
+ * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
+ * then the result is mtbdd_false (i.e. not defined).
+ */
+TASK_IMPL_2(MTBDD, mtbdd_op_equals, MTBDD*, pa, MTBDD*, pb)
+{
+    MTBDD a = *pa, b = *pb;
+    if (a == mtbdd_false && b == mtbdd_false) return mtbdd_true;
+    if (a == mtbdd_true && b == mtbdd_true) return mtbdd_true;
+    
+    mtbddnode_t na = GETNODE(a);
+    mtbddnode_t nb = GETNODE(b);
+    
+    if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
+        uint64_t val_a = mtbddnode_getvalue(na);
+        uint64_t val_b = mtbddnode_getvalue(nb);
+        if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
+            // both uint64_t
+            int nega = mtbdd_isnegated(a);
+            int negb = mtbdd_isnegated(b);
+            if (val_a == val_b && !(nega ^ negb)) return mtbdd_true;
+            return mtbdd_false;
+        } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
+            // both double
+            double vval_a = *(double*)&val_a;
+            double vval_b = *(double*)&val_b;
+            int nega = mtbdd_isnegated(a);
+            int negb = mtbdd_isnegated(b);
+            if (vval_a == vval_b && !(nega ^ negb)) return mtbdd_true;
+            return mtbdd_false;
+        } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
+            // both fraction
+            uint64_t nom_a = val_a>>32;
+            uint64_t nom_b = val_b>>32;
+            uint64_t denom_a = val_a&0xffffffff;
+            uint64_t denom_b = val_b&0xffffffff;
+            int nega = mtbdd_isnegated(a);
+            int negb = mtbdd_isnegated(b);
+            if (nom_a == nom_b && denom_a == denom_b && !(nega ^ negb)) return mtbdd_true;
+            return mtbdd_false;
+        }
+    }
+    
+    if (a < b) {
+        *pa = b;
+        *pb = a;
+    }
+    
+    return mtbdd_invalid;
+}
+
+/**
+ * Binary operation Equals (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
+ * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
+ * then the result is mtbdd_false (i.e. not defined).
+ */
+TASK_IMPL_2(MTBDD, mtbdd_op_less, MTBDD*, pa, MTBDD*, pb)
+{
+    MTBDD a = *pa, b = *pb;
+    if (a == mtbdd_false && b == mtbdd_false) return mtbdd_true;
+    if (a == mtbdd_true && b == mtbdd_true) return mtbdd_true;
+    
+    mtbddnode_t na = GETNODE(a);
+    mtbddnode_t nb = GETNODE(b);
+    
+    if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
+        uint64_t val_a = mtbddnode_getvalue(na);
+        uint64_t val_b = mtbddnode_getvalue(nb);
+        if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
+            // both uint64_t
+            int nega = mtbdd_isnegated(a);
+            int negb = mtbdd_isnegated(b);
+            if (nega && !negb) return mtbdd_true;
+            if (!nega && negb) return mtbdd_false;
+            if (nega && negb && val_a < val_b) return mtbdd_false;
+            return mtbdd_true;
+        } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
+            // both double
+            double vval_a = *(double*)&val_a;
+            double vval_b = *(double*)&val_b;
+            int nega = mtbdd_isnegated(a);
+            if (nega) vval_a = -vval_a;
+            int negb = mtbdd_isnegated(b);
+            if (negb) vval_b = -vval_b;
+            if (vval_a < vval_b) return mtbdd_true;
+            return mtbdd_false;
+        } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
+            // both fraction
+            uint64_t nom_a = val_a>>32;
+            uint64_t nom_b = val_b>>32;
+            uint64_t denom_a = val_a&0xffffffff;
+            uint64_t denom_b = val_b&0xffffffff;
+            int nega = mtbdd_isnegated(a);
+            int negb = mtbdd_isnegated(b);
+            if (nega && !negb) return mtbdd_true;
+            if (!nega && negb) return mtbdd_false;
+            return nom_a * denom_b < nom_b * denom_a ? mtbdd_true : mtbdd_false;
+        }
+    }
+    
+    return mtbdd_invalid;
+}
+
+/**
+ * Binary operation Equals (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
+ * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
+ * then the result is mtbdd_false (i.e. not defined).
+ */
+TASK_IMPL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, pa, MTBDD*, pb)
+{
+    MTBDD a = *pa, b = *pb;
+    if (a == mtbdd_false && b == mtbdd_false) return mtbdd_true;
+    if (a == mtbdd_true && b == mtbdd_true) return mtbdd_true;
+    
+    mtbddnode_t na = GETNODE(a);
+    mtbddnode_t nb = GETNODE(b);
+    
+    if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
+        uint64_t val_a = mtbddnode_getvalue(na);
+        uint64_t val_b = mtbddnode_getvalue(nb);
+        if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
+            // both uint64_t
+            int nega = mtbdd_isnegated(a);
+            int negb = mtbdd_isnegated(b);
+            if (nega && !negb) {
+                if (val_a != 0) return mtbdd_true;
+                if (val_b != 0) return mtbdd_true;
+                return mtbdd_false;
+            }
+            if (!nega && negb) {
+                if (val_b != 0) return mtbdd_false;
+                if (val_a != 0) return mtbdd_false;
+                return mtbdd_true;
+            }
+            if (nega && negb) {
+                return val_a >= val_b ? mtbdd_true : mtbdd_false;
+            }
+            return val_a <= val_b ? mtbdd_true : mtbdd_false;
+        } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
+            // both double
+            double vval_a = *(double*)&val_a;
+            double vval_b = *(double*)&val_b;
+            int nega = mtbdd_isnegated(a);
+            if (nega) vval_a = -vval_a;
+            int negb = mtbdd_isnegated(b);
+            if (negb) vval_b = -vval_b;
+            if (vval_a <= vval_b) return mtbdd_true;
+            return mtbdd_false;
+        } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
+            // both fraction
+            uint64_t nom_a = val_a>>32;
+            uint64_t nom_b = val_b>>32;
+            uint64_t denom_a = val_a&0xffffffff;
+            uint64_t denom_b = val_b&0xffffffff;
+            int nega = mtbdd_isnegated(a);
+            int negb = mtbdd_isnegated(b);
+            nom_a *= denom_b;
+            nom_b *= denom_a;
+            if (nega && !negb) {
+                if (nom_a != 0) return mtbdd_true;
+                if (nom_b != 0) return mtbdd_true;
+                return mtbdd_false;
+            }
+            if (!nega && negb) {
+                if (nom_a != 0) return mtbdd_false;
+                if (nom_b != 0) return mtbdd_false;
+                return mtbdd_true;
+            }
+            if (nega && negb) {
+                return nom_a >= nom_b ? mtbdd_true : mtbdd_false;
+            }
+            return val_a <= val_b ? mtbdd_true : mtbdd_false;
+        }
+    }
+    
+    return mtbdd_invalid;
+}
+
+/**
+ * Binary operation Pow (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Double.
+ * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
+ * then the result is mtbdd_false (i.e. not defined).
+ */
+TASK_IMPL_2(MTBDD, mtbdd_op_pow, MTBDD*, pa, MTBDD*, pb)
+{
+    MTBDD a = *pa, b = *pb;
+    
+    mtbddnode_t na = GETNODE(a);
+    mtbddnode_t nb = GETNODE(b);
+    
+    if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
+        uint64_t val_a = mtbddnode_getvalue(na);
+        uint64_t val_b = mtbddnode_getvalue(nb);
+        if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
+            assert(0);
+        } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
+            // both double
+            double vval_a = *(double*)&val_a;
+            double vval_b = *(double*)&val_b;
+            int nega = mtbdd_isnegated(a);
+            if (nega) vval_a = -vval_a;
+            int negb = mtbdd_isnegated(b);
+            if (negb) vval_b = -vval_b;
+            return mtbdd_double(pow(vval_a, vval_b));
+        } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
+            assert(0);
+        }
+    }
+    
+    return mtbdd_invalid;
+}
+
+/**
+ * Binary operation Mod (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Double.
+ * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
+ * then the result is mtbdd_false (i.e. not defined).
+ */
+TASK_IMPL_2(MTBDD, mtbdd_op_mod, MTBDD*, pa, MTBDD*, pb)
+{
+    MTBDD a = *pa, b = *pb;
+    
+    mtbddnode_t na = GETNODE(a);
+    mtbddnode_t nb = GETNODE(b);
+    
+    if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
+        uint64_t val_a = mtbddnode_getvalue(na);
+        uint64_t val_b = mtbddnode_getvalue(nb);
+        if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
+            assert(0);
+        } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
+            // both double
+            double vval_a = *(double*)&val_a;
+            double vval_b = *(double*)&val_b;
+            int nega = mtbdd_isnegated(a);
+            if (nega) vval_a = -vval_a;
+            int negb = mtbdd_isnegated(b);
+            if (negb) vval_b = -vval_b;
+            return mtbdd_double(fmod(vval_a, vval_b));
+        } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
+            assert(0);
+        }
+    }
+    
+    return mtbdd_invalid;
+}
+
+/**
+ * Binary operation Log (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Double.
+ * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
+ * then the result is mtbdd_false (i.e. not defined).
+ */
+TASK_IMPL_2(MTBDD, mtbdd_op_logxy, MTBDD*, pa, MTBDD*, pb)
+{
+    MTBDD a = *pa, b = *pb;
+    
+    mtbddnode_t na = GETNODE(a);
+    mtbddnode_t nb = GETNODE(b);
+    
+    if (mtbddnode_isleaf(na) && mtbddnode_isleaf(nb)) {
+        uint64_t val_a = mtbddnode_getvalue(na);
+        uint64_t val_b = mtbddnode_getvalue(nb);
+        if (mtbddnode_gettype(na) == 0 && mtbddnode_gettype(nb) == 0) {
+            assert(0);
+        } else if (mtbddnode_gettype(na) == 1 && mtbddnode_gettype(nb) == 1) {
+            // both double
+            double vval_a = *(double*)&val_a;
+            double vval_b = *(double*)&val_b;
+            int nega = mtbdd_isnegated(a);
+            if (nega) vval_a = -vval_a;
+            int negb = mtbdd_isnegated(b);
+            if (negb) vval_b = -vval_b;
+            return mtbdd_double(log(vval_a) / log(vval_b));
+        } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
+            assert(0);
+        }
+    }
+    
+    return mtbdd_invalid;
+}
+
+TASK_IMPL_2(MTBDD, mtbdd_op_not_zero, MTBDD, a, size_t, v)
+{
+    /* We only expect "double" terminals, or false */
+    if (a == mtbdd_false) return mtbdd_false;
+    if (a == mtbdd_true) return mtbdd_true;
+    
+    // a != constant
+    mtbddnode_t na = GETNODE(a);
+    
+    if (mtbddnode_isleaf(na)) {
+        if (mtbddnode_gettype(na) == 0) {
+            return mtbdd_getuint64(a) != 0 ? mtbdd_true : mtbdd_false;
+        } else if (mtbddnode_gettype(na) == 1) {
+            return mtbdd_getdouble(a) != 0.0 ? mtbdd_true : mtbdd_false;
+        } else if (mtbddnode_gettype(na) == 2) {
+            return mtbdd_getnumer(a) != 0 ? mtbdd_true : mtbdd_false;
+        }
+    }
+    
+    // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
+    return v > 0 ? mtbdd_invalid : mtbdd_invalid;
+}
+
+TASK_IMPL_1(MTBDD, mtbdd_not_zero, MTBDD, dd)
+{
+    return mtbdd_uapply(dd, TASK(mtbdd_op_not_zero), 0);
+}
+
+TASK_IMPL_2(MTBDD, mtbdd_op_floor, MTBDD, a, size_t, v)
+{
+    /* We only expect "double" terminals, or false */
+    if (a == mtbdd_false) return mtbdd_false;
+    if (a == mtbdd_true) return mtbdd_true;
+    
+    // a != constant
+    mtbddnode_t na = GETNODE(a);
+    
+    if (mtbddnode_isleaf(na)) {
+        if (mtbddnode_gettype(na) == 0) {
+            return a;
+        } else if (mtbddnode_gettype(na) == 1) {
+            MTBDD result = mtbdd_double(floor(mtbdd_getdouble(a)));
+            return mtbdd_isnegated(a) ? mtbdd_negate(result) : result;
+        } else if (mtbddnode_gettype(na) == 2) {
+            MTBDD result = mtbdd_fraction(mtbdd_getnumer(a) / mtbdd_getdenom(a), 1);
+            return mtbdd_isnegated(a) ? mtbdd_negate(result) : result;
+        }
+    }
+    
+    // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
+    return v > 0 ? mtbdd_invalid : mtbdd_invalid;
+}
+
+TASK_IMPL_1(MTBDD, mtbdd_floor, MTBDD, dd)
+{
+    return mtbdd_uapply(dd, TASK(mtbdd_op_floor), 0);
+}
+
+TASK_IMPL_2(MTBDD, mtbdd_op_ceil, MTBDD, a, size_t, v)
+{
+    /* We only expect "double" terminals, or false */
+    if (a == mtbdd_false) return mtbdd_false;
+    if (a == mtbdd_true) return mtbdd_true;
+    
+    // a != constant
+    mtbddnode_t na = GETNODE(a);
+    
+    if (mtbddnode_isleaf(na)) {
+        if (mtbddnode_gettype(na) == 0) {
+            return a;
+        } else if (mtbddnode_gettype(na) == 1) {
+            MTBDD result = mtbdd_double(ceil(mtbdd_getdouble(a)));
+            return mtbdd_isnegated(a) ? mtbdd_negate(result) : result;
+        } else if (mtbddnode_gettype(na) == 2) {
+            MTBDD result = mtbdd_fraction(mtbdd_getnumer(a) / mtbdd_getdenom(a) + 1, 1);
+            return mtbdd_isnegated(a) ? mtbdd_negate(result) : result;
+        }
+    }
+    
+    // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
+    return v > 0 ? mtbdd_invalid : mtbdd_invalid;
+}
+
+TASK_IMPL_1(MTBDD, mtbdd_ceil, MTBDD, dd)
+{
+    return mtbdd_uapply(dd, TASK(mtbdd_op_ceil), 0);
+}
+
+TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, a, size_t, v)
+{
+    /* We only expect "double" terminals, or false */
+    if (a == mtbdd_false) return mtbdd_double(0);
+    if (a == mtbdd_true) return mtbdd_double(1.0);
+    
+    // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter).
+    return v > 0 ? mtbdd_invalid : mtbdd_invalid;
+}
+
+TASK_IMPL_1(MTBDD, mtbdd_bool_to_double, MTBDD, dd)
+{
+    return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_double), 0);
+}
diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_custom.h b/resources/3rdparty/sylvan/src/sylvan_storm_custom.h
new file mode 100644
index 000000000..0e6f736d6
--- /dev/null
+++ b/resources/3rdparty/sylvan/src/sylvan_storm_custom.h
@@ -0,0 +1,95 @@
+/**
+ * Compute a - b
+ */
+#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(b))
+
+/**
+ * Binary operation Divide (for MTBDDs of same type)
+ * Only for MTBDDs where all leaves are Integer or Double.
+ * If either operand is mtbdd_false (not defined),
+ * then the result is mtbdd_false (i.e. not defined).
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_divide, MTBDD*, MTBDD*);
+#define mtbdd_divide(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_divide))
+
+/**
+ * Binary operation equals (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
+ * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
+ * then the result is the other operand.
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_equals, MTBDD*, MTBDD*);
+#define mtbdd_equals(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_equals))
+
+/**
+ * Binary operation Less (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
+ * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
+ * then the result is the other operand.
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*);
+#define mtbdd_less_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less))
+
+/**
+ * Binary operation Less (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double.
+ * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
+ * then the result is the other operand.
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*);
+#define mtbdd_less_or_equal_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less_or_equal))
+
+/**
+ * Binary operation Pow (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Integer, Double or a Fraction.
+ * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
+ * then the result is the other operand.
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_pow, MTBDD*, MTBDD*);
+#define mtbdd_pow(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_pow))
+
+/**
+ * Binary operation Mod (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Integer, Double or a Fraction.
+ * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
+ * then the result is the other operand.
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_mod, MTBDD*, MTBDD*);
+#define mtbdd_mod(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_mod))
+
+/**
+ * Binary operation Log (for MTBDDs of same type)
+ * Only for MTBDDs where either all leaves are Double or a Fraction.
+ * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined),
+ * then the result is the other operand.
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_logxy, MTBDD*, MTBDD*);
+#define mtbdd_logxy(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_logxy))
+
+/**
+ * Monad that converts double to a Boolean MTBDD, translate terminals != 0 to 1 and to 0 otherwise;
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_not_zero, MTBDD, size_t)
+TASK_DECL_1(MTBDD, mtbdd_not_zero, MTBDD)
+#define mtbdd_not_zero(dd) CALL(mtbdd_not_zero, dd)
+
+/**
+ * Monad that floors all values Double and Fraction values.
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_floor, MTBDD, size_t)
+TASK_DECL_1(MTBDD, mtbdd_floor, MTBDD)
+#define mtbdd_floor(dd) CALL(mtbdd_floor, dd)
+
+/**
+ * Monad that ceils all values Double and Fraction values.
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_ceil, MTBDD, size_t)
+TASK_DECL_1(MTBDD, mtbdd_ceil, MTBDD)
+#define mtbdd_ceil(dd) CALL(mtbdd_ceil, dd)
+
+/**
+ * Monad that converts Boolean to a Double MTBDD, translate terminals true to 1 and to 0 otherwise;
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, size_t)
+TASK_DECL_1(MTBDD, mtbdd_bool_to_double, MTBDD)
+#define mtbdd_bool_to_double(dd) CALL(mtbdd_bool_to_double, dd)
diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp
index 766da0bac..993ec6925 100644
--- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp
+++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp
@@ -103,27 +103,27 @@ namespace storm {
         
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::pow(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Pow(other.sylvanMtbdd));
         }
         
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::mod(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Mod(other.sylvanMtbdd));
         }
         
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::logxy(InternalAdd<DdType::Sylvan, ValueType> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Logxy(other.sylvanMtbdd));
         }
         
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::floor() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Floor());
         }
         
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::ceil() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Ceil());
         }
         
         template<typename ValueType>
@@ -153,7 +153,11 @@ namespace storm {
         
         template<typename ValueType>
         bool InternalAdd<DdType::Sylvan, ValueType>::equalModuloPrecision(InternalAdd<DdType::Sylvan, ValueType> const& other, double precision, bool relative) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            if (relative) {
+                return this->sylvanMtbdd.EqualNormRel(other.sylvanMtbdd, precision);
+            } else {
+                return this->sylvanMtbdd.EqualNorm(other.sylvanMtbdd, precision);
+            }
         }
         
         template<typename ValueType>
@@ -227,12 +231,12 @@ namespace storm {
         
         template<typename ValueType>
         ValueType InternalAdd<DdType::Sylvan, ValueType>::getMin() const {
-            return static_cast<ValueType>(this-sylvanMtbdd.getDoubleMin());
+            return static_cast<ValueType>(this->sylvanMtbdd.getDoubleMin());
         }
         
         template<typename ValueType>
         ValueType InternalAdd<DdType::Sylvan, ValueType>::getMax() const {
-            return static_cast<ValueType>(this-sylvanMtbdd.getDoubleMax());
+            return static_cast<ValueType>(this->sylvanMtbdd.getDoubleMax());
         }
         
         template<typename ValueType>
diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp
index 3aa6eb036..eab221a35 100644
--- a/test/functional/storage/SylvanDdTest.cpp
+++ b/test/functional/storage/SylvanDdTest.cpp
@@ -173,16 +173,16 @@ TEST(SylvanDd, OperatorTest) {
     dd4 *= manager->getEncoding(x.first, 2).template toAdd<double>();
     dd4 = dd4.sumAbstract({x.first});
     EXPECT_EQ(2, dd4.getValue());
-//
-//    dd4 = dd3.maximum(dd1);
-//    dd4 *= manager->getEncoding(x.first, 2).template toAdd<double>();
-//    dd4 = dd4.sumAbstract({x.first});
-//    EXPECT_EQ(5, dd4.getValue());
-//    
-//    dd1 = manager->template getConstant<double>(0.01);
-//    dd2 = manager->template getConstant<double>(0.01 + 1e-6);
-//    EXPECT_TRUE(dd1.equalModuloPrecision(dd2, 1e-6, false));
-//    EXPECT_FALSE(dd1.equalModuloPrecision(dd2, 1e-6));
+
+    dd4 = dd3.maximum(dd1);
+    dd4 *= manager->getEncoding(x.first, 2).template toAdd<double>();
+    dd4 = dd4.sumAbstract({x.first});
+    EXPECT_EQ(5, dd4.getValue());
+    
+    dd1 = manager->template getConstant<double>(0.01);
+    dd2 = manager->template getConstant<double>(0.01 + 1e-6);
+    EXPECT_TRUE(dd1.equalModuloPrecision(dd2, 1e-6, false));
+    EXPECT_FALSE(dd1.equalModuloPrecision(dd2, 1e-6));
 }
 
 //TEST(SylvanDd, AbstractionTest) {