From 6168af3c99a906b77a7bbd94199c3edbdf2a9963 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 23 Aug 2016 13:53:07 +0200
Subject: [PATCH] intermediate commit in an attempt to have proper cudd support
 for some operations

Former-commit-id: 0bb840ecff463dee6ef78dbdc47567be8c330fa5
---
 .../3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc  | 26 +++++++++----------
 resources/3rdparty/cudd-3.0.0/cudd/cudd.h     |  6 +++++
 src/builder/DdPrismModelBuilder.cpp           |  3 +++
 3 files changed, 22 insertions(+), 13 deletions(-)

diff --git a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc
index fd2622c2a..1666f3970 100644
--- a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc
+++ b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc
@@ -566,7 +566,7 @@ BDD::operator+(
   const BDD& other) const
 {
     DdManager *mgr = checkSameManager(other);
-    DdNode *result = Cudd_bddOr(mgr,node,other.node);
+    DdNode *result = 	(mgr,node,other.node);
     checkReturnValue(result);
     return BDD(p, result);
 
@@ -3154,63 +3154,63 @@ ADD::GreaterThanOrEqual(const ADD& g) const
         
 } // ADD::GreaterThanOrEqual
 
-ADD
+BDD
 ADD::EqualsBdd(const ADD& g) const
 {
     DdManager *mgr = checkSameManager(g);
     DdNode *result = Cudd_addApply(mgr, Cudd_addToBddEquals, node, g.node);
     checkReturnValue(result);
-    return ADD(p, result);
+    return BDD(p, result);
         
 } // ADD::EqualsBdd
     
-ADD
+BDD
 ADD::NotEqualsBdd(const ADD& g) const
 {
     DdManager *mgr = checkSameManager(g);
     DdNode *result = Cudd_addApply(mgr, Cudd_addToBddNotEquals, node, g.node);
     checkReturnValue(result);
-    return ADD(p, result);
+    return BDD(p, result);
     
 } // ADD::NotEqualsBdd
     
-ADD
+BDD
 ADD::LessThanBdd(const ADD& g) const
 {
     DdManager *mgr = checkSameManager(g);
     DdNode *result = Cudd_addApply(mgr, Cudd_addToBddLessThan, node, g.node);
     checkReturnValue(result);
-    return ADD(p, result);
+    return BDD(p, result);
         
 } // ADD::LessThanBdd
     
-ADD
+BDD
 ADD::LessThanOrEqualBdd(const ADD& g) const
 {
     DdManager *mgr = checkSameManager(g);
     DdNode *result = Cudd_addApply(mgr, Cudd_addToBddLessThanEquals, node, g.node);
     checkReturnValue(result);
-    return ADD(p, result);
+    return BDD(p, result);
         
 } // ADD::LessThanOrEqualBdd
     
-ADD
+BDD
 ADD::GreaterThanBdd(const ADD& g) const
 {
     DdManager *mgr = checkSameManager(g);
     DdNode *result = Cudd_addApply(mgr, Cudd_addToBddGreaterThan, node, g.node);
     checkReturnValue(result);
-    return ADD(p, result);
+    return BDD(p, result);
         
 } // ADD::GreaterThanBdd
     
-ADD
+BDD
 ADD::GreaterThanOrEqualBdd(const ADD& g) const
 {
     DdManager *mgr = checkSameManager(g);
     DdNode *result = Cudd_addApply(mgr, Cudd_addToBddGreaterThanEquals, node, g.node);
     checkReturnValue(result);
-    return ADD(p, result);
+    return BDD(p, result);
         
 } // ADD::GreaterThanOrEqualBdd
     
diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cudd.h b/resources/3rdparty/cudd-3.0.0/cudd/cudd.h
index e7bdbf0c1..711f59bc9 100644
--- a/resources/3rdparty/cudd-3.0.0/cudd/cudd.h
+++ b/resources/3rdparty/cudd-3.0.0/cudd/cudd.h
@@ -693,6 +693,12 @@ extern DdNode * Cudd_addGreaterThan (DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addGreaterThanEquals (DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addLessThan (DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addLessThanEquals (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addToBddEquals (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addToBddNotEquals (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addToBddGreaterThan (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addToBddGreaterThanEquals (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addToBddLessThan (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addToBddLessThanEquals (DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addPow (DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addMod (DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addLogXY (DdManager *dd, DdNode **f, DdNode **g);
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index a397b0de0..498a48a64 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -178,6 +178,9 @@ namespace storm {
                         variableToColumnMetaVariableMap->emplace(booleanVariable.getExpressionVariable(), variablePair.second);
                         
                         storm::dd::Bdd<Type> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second);
+                        std::cout << "got here " << variableIdentity.isOne() << variableIdentity.isZero() << std::endl;
+                        variableIdentity.exportToDot("id_bdd.dot");
+                        variableIdentity.template toAdd<ValueType>().exportToDot("id_add.dot");
                         variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
                         moduleIdentity &= variableIdentity;
                         moduleRange &= manager->getRange(variablePair.first);