intermediate commit in an attempt to have proper cudd support for some operations

Former-commit-id: 0bb840ecff

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
     

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);

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);