cudd3 now working, but tests segfaulting

Former-commit-id: 9742e4e75e

resources/3rdparty/CMakeLists.txt

@@ -48,8 +48,8 @@ add_dependencies(resources cudd3)
 ExternalProject_Get_Property(cudd3 binary_dir)
 set(CUDD3_INCLUDE_DIR ${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0/include PARENT_SCOPE)
 
-set(CUDD3_SHARED_LIBRARIES ${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0/libcudd${DYNAMIC_EXT} PARENT_SCOPE)
-set(CUDD3_STATIC_LIBRARIES ${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0/libcudd${STATIC_EXT} PARENT_SCOPE)
+set(CUDD3_SHARED_LIBRARIES ${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0/lib/libcudd${DYNAMIC_EXT} PARENT_SCOPE)
+set(CUDD3_STATIC_LIBRARIES ${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0/liblibcudd${STATIC_EXT} PARENT_SCOPE)
 
 ExternalProject_Add(
         googletest

resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc

@@ -2640,6 +2640,23 @@ ADD::OrAbstract(
 
 } // ADD::OrAbstract
 
+ADD
+ADD::MinAbstract(const ADD& cube) const
+{
+    DdManager *mgr = checkSameManager(cube);
+    DdNode *result = Cudd_addMinAbstract(mgr, node, cube.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+} // ADD::MinAbstract
+    
+ADD
+ADD::MaxAbstract(const ADD& cube) const
+{
+    DdManager *mgr = checkSameManager(cube);
+    DdNode *result = Cudd_addMaxAbstract(mgr, node, cube.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+} // ADD::MaxAbstract
 
 ADD
 ADD::Plus(
@@ -2832,7 +2849,39 @@ ADD::Xnor(
 
 } // ADD::Xnor
 
-
+ADD
+ADD::Pow(
+  const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addPow, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::Pow
+    
+ADD
+ADD::Mod(
+  const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addMod, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::Mod
+    
+ADD
+ADD::LogXY(
+  const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addLogXY, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::LogXY
+    
 ADD
 ADD::Log() const
 {
@@ -2840,9 +2889,28 @@ ADD::Log() const
     DdNode *result = Cudd_addMonadicApply(mgr, Cudd_addLog, node);
     checkReturnValue(result);
     return ADD(p, result);
-
+        
 } // ADD::Log
-
+    
+ADD
+ADD::Floor() const
+{
+    DdManager *mgr = p->manager;
+    DdNode *result = Cudd_addMonadicApply(mgr, Cudd_addFloor, node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::Floor
+    
+ADD
+ADD::Ceil() const
+{
+    DdManager *mgr = p->manager;
+    DdNode *result = Cudd_addMonadicApply(mgr, Cudd_addCeil, node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::Ceil
 
 ADD
 ADD::FindMax() const
@@ -3008,6 +3076,65 @@ Cudd::addResidue(
 
 } // Cudd::addResidue
 
+ADD
+ADD::Equals(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addEquals, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::Equals
+    
+ADD
+ADD::NotEquals(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addNotEquals, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::NotEquals
+
+ADD
+ADD::LessThan(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addLessThan, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::LessThan
+    
+ADD
+ADD::LessThanOrEqual(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addLessThanEquals, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::LessThanOrEqual
+    
+ADD
+ADD::GreaterThan(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addGreaterThan, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::GreaterThan
+    
+ADD
+ADD::GreaterThanOrEqual(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addGreaterThanEquals, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::GreaterThanOrEqual
 
 BDD
 BDD::AndAbstract(
@@ -5130,6 +5257,16 @@ ADD::EqualSupNorm(
 
 } // ADD::EqualSupNorm
 
+bool
+ADD::EqualSupNormRel(
+  const ADD& g,
+  CUDD_VALUE_TYPE tolerance,
+  int pr) const
+{
+    DdManager *mgr = checkSameManager(g);
+    return Cudd_EqualSupNormRel(mgr, node, g.node, tolerance, pr) != 0;
+        
+} // ADD::EqualSupNormRel
 
 BDD
 BDD::MakePrime(

resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh

@@ -332,6 +332,8 @@ public:
     ADD ExistAbstract(const ADD& cube) const;
     ADD UnivAbstract(const ADD& cube) const;
     ADD OrAbstract(const ADD& cube) const;
+    ADD MinAbstract(const ADD& cube) const;
+    ADD MaxAbstract(const ADD& cube) const;
     ADD Plus(const ADD& g) const;
     ADD Times(const ADD& g) const;
     ADD Threshold(const ADD& g) const;
@@ -348,7 +350,12 @@ public:
     ADD Nor(const ADD& g) const;
     ADD Xor(const ADD& g) const;
     ADD Xnor(const ADD& g) const;
+    ADD Pow(const ADD& g) const;
+    ADD Mod(const ADD& g) const;
+    ADD LogXY(const ADD& g) const;
     ADD Log() const;
+    ADD Floor() const;
+    ADD Ceil() const;
     ADD FindMax() const;
     ADD FindMin() const;
     ADD IthBit(int bit) const;
@@ -360,6 +367,12 @@ public:
     ADD Cmpl() const;
     ADD Negate() const;
     ADD RoundOff(int N) const;
+    ADD Equals(const ADD& g) const;
+    ADD NotEquals(const ADD& g) const;
+    ADD LessThan(const ADD& g) const;
+    ADD LessThanOrEqual(const ADD& g) const;
+    ADD GreaterThan(const ADD& g) const;
+    ADD GreaterThanOrEqual(const ADD& g) const;
     BDD BddThreshold(CUDD_VALUE_TYPE value) const;
     BDD BddStrictThreshold(CUDD_VALUE_TYPE value) const;
     BDD BddInterval(CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper) const;
@@ -377,8 +390,8 @@ public:
     ADD TimesPlus(const ADD& B, std::vector<ADD> z) const;
     ADD Triangle(const ADD& g, std::vector<ADD> z) const;
     ADD Eval(int * inputs) const;
-    bool EqualSupNorm(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr) const;
-
+    bool EqualSupNorm(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr = 0) const;
+    bool EqualSupNormRel(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr = 0) const;
 }; // ADD
 
 

resources/3rdparty/cudd-3.0.0/cudd/cudd.h

@@ -665,6 +665,8 @@ extern int Cudd_bddVarIsBound(DdManager *dd, int index);
 extern DdNode * Cudd_addExistAbstract(DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * Cudd_addUnivAbstract(DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * Cudd_addOrAbstract(DdManager *manager, DdNode *f, DdNode *cube);
+extern DdNode * Cudd_addMinAbstract(DdManager * manager, DdNode * f, DdNode * cube);
+extern DdNode * Cudd_addMaxAbstract(DdManager * manager, DdNode * f, DdNode * cube);
 extern DdNode * Cudd_addApply(DdManager *dd, DD_AOP op, DdNode *f, DdNode *g);
 extern DdNode * Cudd_addPlus(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addTimes(DdManager *dd, DdNode **f, DdNode **g);
@@ -682,6 +684,17 @@ extern DdNode * Cudd_addNand(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addNor(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addXor(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addXnor(DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addEquals (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addNotEquals (DdManager *dd, DdNode **f, DdNode **g);
+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_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);
+extern DdNode * Cudd_addFloor (DdManager * dd, DdNode * f);
+extern DdNode * Cudd_addCeil (DdManager * dd, DdNode * f);
 extern DdNode * Cudd_addMonadicApply(DdManager * dd, DD_MAOP op, DdNode * f);
 extern DdNode * Cudd_addLog(DdManager * dd, DdNode * f);
 extern DdNode * Cudd_addFindMax(DdManager *dd, DdNode *f);
@@ -852,6 +865,7 @@ extern DdNode * Cudd_Increasing(DdManager *dd, DdNode *f, int i);
 extern int Cudd_EquivDC(DdManager *dd, DdNode *F, DdNode *G, DdNode *D);
 extern int Cudd_bddLeqUnless(DdManager *dd, DdNode *f, DdNode *g, DdNode *D);
 extern int Cudd_EqualSupNorm(DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr);
+extern int Cudd_EqualSupNormRel (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr);
 extern DdNode * Cudd_bddMakePrime(DdManager *dd, DdNode *cube, DdNode *f);
 extern DdNode * Cudd_bddMaximallyExpand(DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f);
 extern DdNode * Cudd_bddLargestPrimeUnate(DdManager *dd , DdNode *f, DdNode *phaseBdd);

resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c

@@ -204,6 +204,82 @@ Cudd_addOrAbstract(
 
 } /* end of Cudd_addOrAbstract */
 
+/**Function********************************************************************
+ 
+ Synopsis    [Abstracts all the variables in cube from the
+ ADD f by taking the minimum.]
+ 
+ Description [Abstracts all the variables in cube from the ADD f
+ by taking the minimum over all possible values taken by the
+ variables.  Returns the abstracted ADD if successful; NULL
+ otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addUnivAbstract Cudd_addExistAbstract]
+ 
+ Note: Added by Dave Parker 14/6/99
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addMinAbstract(
+                    DdManager * manager,
+                    DdNode * f,
+                    DdNode * cube)
+{
+    DdNode *res;
+    
+    if (addCheckPositiveCube(manager, cube) == 0) {
+        (void) fprintf(manager->err,"Error: Can only abstract cubes");
+        return(NULL);
+    }
+    
+    do {
+        manager->reordered = 0;
+        res = cuddAddMinAbstractRecur(manager, f, cube);
+    } while (manager->reordered == 1);
+    return(res);
+    
+} /* end of Cudd_addMinAbstract */
+
+
+/**Function********************************************************************
+ 
+ Synopsis    [Abstracts all the variables in cube from the
+ ADD f by taking the maximum.]
+ 
+ Description [Abstracts all the variables in cube from the ADD f
+ by taking the maximum over all possible values taken by the
+ variables.  Returns the abstracted ADD if successful; NULL
+ otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addUnivAbstract Cudd_addExistAbstract]
+ 
+ Note: Added by Dave Parker 14/6/99
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addMaxAbstract(
+                    DdManager * manager,
+                    DdNode * f,
+                    DdNode * cube)
+{
+    DdNode *res;
+    
+    if (addCheckPositiveCube(manager, cube) == 0) {
+        (void) fprintf(manager->err,"Error: Can only abstract cubes");
+        return(NULL);
+    }
+    
+    do {
+        manager->reordered = 0;
+        res = cuddAddMaxAbstractRecur(manager, f, cube);
+    } while (manager->reordered == 1);
+    return(res);
+    
+} /* end of Cudd_addMaxAbstract */
 
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
@@ -511,7 +587,188 @@ cuddAddOrAbstractRecur(
 
 } /* end of cuddAddOrAbstractRecur */
 
-
+/**Function********************************************************************
+ 
+ Synopsis    [Performs the recursive step of Cudd_addMinAbstract.]
+ 
+ Description [Performs the recursive step of Cudd_addMinAbstract.
+ Returns the ADD obtained by abstracting the variables of cube from f,
+ if successful; NULL otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     []
+ 
+ ******************************************************************************/
+DdNode *
+cuddAddMinAbstractRecur(
+                        DdManager * manager,
+                        DdNode * f,
+                        DdNode * cube)
+{
+    DdNode	*T, *E, *res, *res1, *res2, *zero;
+    
+    zero = DD_ZERO(manager);
+    
+    /* Cube is guaranteed to be a cube at this point. */
+    if (f == zero || cuddIsConstant(cube)) {
+        return(f);
+    }
+    
+    /* Abstract a variable that does not appear in f. */
+    if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
+        res = cuddAddMinAbstractRecur(manager, f, cuddT(cube));
+       	return(res);
+    }
+    
+    if ((res = cuddCacheLookup2(manager, Cudd_addMinAbstract, f, cube)) != NULL) {
+        return(res);
+    }
+    
+    
+    T = cuddT(f);
+    E = cuddE(f);
+    
+    /* If the two indices are the same, so are their levels. */
+    if (f->index == cube->index) {
+        res1 = cuddAddMinAbstractRecur(manager, T, cuddT(cube));
+        if (res1 == NULL) return(NULL);
+        cuddRef(res1);
+        res2 = cuddAddMinAbstractRecur(manager, E, cuddT(cube));
+        if (res2 == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            return(NULL);
+        }
+        cuddRef(res2);
+        res = cuddAddApplyRecur(manager, Cudd_addMinimum, res1, res2);
+        if (res == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            Cudd_RecursiveDeref(manager,res2);
+            return(NULL);
+        }
+        cuddRef(res);
+        Cudd_RecursiveDeref(manager,res1);
+        Cudd_RecursiveDeref(manager,res2);
+        cuddCacheInsert2(manager, Cudd_addMinAbstract, f, cube, res);
+        cuddDeref(res);
+        return(res);
+    }
+    else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
+        res1 = cuddAddMinAbstractRecur(manager, T, cube);
+        if (res1 == NULL) return(NULL);
+        cuddRef(res1);
+        res2 = cuddAddMinAbstractRecur(manager, E, cube);
+        if (res2 == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            return(NULL);
+        }
+        cuddRef(res2);
+        res = (res1 == res2) ? res1 :
+        cuddUniqueInter(manager, (int) f->index, res1, res2);
+        if (res == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            Cudd_RecursiveDeref(manager,res2);
+            return(NULL);
+        }
+        cuddDeref(res1);
+        cuddDeref(res2);
+        cuddCacheInsert2(manager, Cudd_addMinAbstract, f, cube, res);
+        return(res);
+    }
+    
+} /* end of cuddAddMinAbstractRecur */
+
+
+/**Function********************************************************************
+ 
+ Synopsis    [Performs the recursive step of Cudd_addMaxAbstract.]
+ 
+ Description [Performs the recursive step of Cudd_addMaxAbstract.
+ Returns the ADD obtained by abstracting the variables of cube from f,
+ if successful; NULL otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     []
+ 
+ ******************************************************************************/
+DdNode *
+cuddAddMaxAbstractRecur(
+                        DdManager * manager,
+                        DdNode * f,
+                        DdNode * cube)
+{
+    DdNode	*T, *E, *res, *res1, *res2, *zero;
+    
+    zero = DD_ZERO(manager);
+    
+    /* Cube is guaranteed to be a cube at this point. */
+    if (f == zero || cuddIsConstant(cube)) {
+        return(f);
+    }
+    
+    /* Abstract a variable that does not appear in f. */
+    if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
+        res = cuddAddMaxAbstractRecur(manager, f, cuddT(cube));
+       	return(res);
+    }
+    
+    if ((res = cuddCacheLookup2(manager, Cudd_addMaxAbstract, f, cube)) != NULL) {
+        return(res);
+    }
+    
+    
+    T = cuddT(f);
+    E = cuddE(f);
+    
+    /* If the two indices are the same, so are their levels. */
+    if (f->index == cube->index) {
+        res1 = cuddAddMaxAbstractRecur(manager, T, cuddT(cube));
+        if (res1 == NULL) return(NULL);
+        cuddRef(res1);
+        res2 = cuddAddMaxAbstractRecur(manager, E, cuddT(cube));
+        if (res2 == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            return(NULL);
+        }
+        cuddRef(res2);
+        res = cuddAddApplyRecur(manager, Cudd_addMaximum, res1, res2);
+        if (res == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            Cudd_RecursiveDeref(manager,res2);
+            return(NULL);
+        }
+        cuddRef(res);
+        Cudd_RecursiveDeref(manager,res1);
+        Cudd_RecursiveDeref(manager,res2);
+        cuddCacheInsert2(manager, Cudd_addMaxAbstract, f, cube, res);
+        cuddDeref(res);
+        return(res);
+    }
+    else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
+        res1 = cuddAddMaxAbstractRecur(manager, T, cube);
+        if (res1 == NULL) return(NULL);
+        cuddRef(res1);
+        res2 = cuddAddMaxAbstractRecur(manager, E, cube);
+        if (res2 == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            return(NULL);
+        }
+        cuddRef(res2);
+        res = (res1 == res2) ? res1 :
+        cuddUniqueInter(manager, (int) f->index, res1, res2);
+        if (res == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            Cudd_RecursiveDeref(manager,res2);
+            return(NULL);
+        }
+        cuddDeref(res1);
+        cuddDeref(res2);
+        cuddCacheInsert2(manager, Cudd_addMaxAbstract, f, cube, res);
+        return(res);
+    }	    
+    
+} /* end of cuddAddMaxAbstractRecur */
 
 /*---------------------------------------------------------------------------*/
 /* Definition of static functions                                            */

resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c

@@ -733,6 +733,358 @@ Cudd_addLog(
 
 } /* end of Cudd_addLog */
 
+/**Function********************************************************************
+ 
+ Synopsis    [Floor of an ADD.]
+ 
+ Description [Floor of an ADD. Returns NULL
+ if not a terminal case; floor(f) otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addMonadicApply]
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addFloor(
+              DdManager * dd,
+              DdNode * f)
+{
+    if (cuddIsConstant(f)) {
+        CUDD_VALUE_TYPE value = floor(cuddV(f));
+        DdNode *res = cuddUniqueConst(dd,value);
+        return(res);
+    }
+    return(NULL);
+    
+} /* end of Cudd_addFloor */
+
+
+/**Function********************************************************************
+ 
+ Synopsis    [Ceiling of an ADD.]
+ 
+ Description [Ceiling of an ADD. Returns NULL
+ if not a terminal case; ceil(f) otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addMonadicApply]
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addCeil(
+             DdManager * dd,
+             DdNode * f)
+{
+    if (cuddIsConstant(f)) {
+        CUDD_VALUE_TYPE value = ceil(cuddV(f));
+        DdNode *res = cuddUniqueConst(dd,value);
+        return(res);
+    }
+    return(NULL);
+    
+} /* end of Cudd_addCeiling */
+
+/**Function********************************************************************
+ 
+ Synopsis    [1 if f==g; 0 otherwise.]
+ 
+ Description [Returns NULL if not a terminal case; f op g otherwise,
+ where f op g is 1 if f==g; 0 otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addApply]
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addEquals(
+               DdManager * dd,
+               DdNode ** f,
+               DdNode ** g)
+{
+    DdNode *F, *G;
+    
+    F = *f; G = *g;
+    if (F == G) return(DD_ONE(dd));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
+    if (F > G) { /* swap f and g */
+        *f = G;
+        *g = F;
+    }
+    return(NULL);
+    
+} /* end of Cudd_addEquals */
+
+
+/**Function********************************************************************
+ 
+ Synopsis    [1 if f!=g; 0 otherwise.]
+ 
+ Description [Returns NULL if not a terminal case; f op g otherwise,
+ where f op g is 1 if f!=g; 0 otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addApply]
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addNotEquals(
+                  DdManager * dd,
+                  DdNode ** f,
+                  DdNode ** g)
+{
+    DdNode *F, *G;
+    
+    F = *f; G = *g;
+    if (F == G) return(DD_ZERO(dd));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd));
+    if (F > G) { /* swap f and g */
+        *f = G;
+        *g = F;
+    }
+    return(NULL);
+    
+} /* end of Cudd_addNotEquals */
+
+/**Function********************************************************************
+ 
+ Synopsis    [1 if f>g; 0 otherwise.]
+ 
+ Description [Returns NULL if not a terminal case; f op g otherwise,
+ where f op g is 1 if f>g; 0 otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addApply]
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addGreaterThan(
+                    DdManager * dd,
+                    DdNode ** f,
+                    DdNode ** g)
+{
+    DdNode *F, *G;
+    
+    F = *f; G = *g;
+    if (F == G) return(DD_ZERO(dd));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) {
+        if (cuddV(F)>cuddV(G)) return (DD_ONE(dd)); else return (DD_ZERO(dd));
+    }
+    return(NULL);
+    
+} /* end of Cudd_addGreaterThan */
+
+
+/**Function********************************************************************
+ 
+ Synopsis    [1 if f>=g; 0 otherwise.]
+ 
+ Description [Returns NULL if not a terminal case; f op g otherwise,
+ where f op g is 1 if f>=g; 0 otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addApply]
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addGreaterThanEquals(
+                          DdManager * dd,
+                          DdNode ** f,
+                          DdNode ** g)
+{
+    DdNode *F, *G;
+    
+    F = *f; G = *g;
+    if (F == G) return(DD_ONE(dd));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) {
+        if (cuddV(F)>=cuddV(G)) return (DD_ONE(dd)); else return (DD_ZERO(dd));
+    }
+    return(NULL);
+    
+} /* end of Cudd_addGreaterThanEquals */
+
+
+/**Function********************************************************************
+ 
+ Synopsis    [1 if f<g; 0 otherwise.]
+ 
+ Description [Returns NULL if not a terminal case; f op g otherwise,
+ where f op g is 1 if f<g; 0 otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addApply]
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addLessThan(
+                 DdManager * dd,
+                 DdNode ** f,
+                 DdNode ** g)
+{
+    DdNode *F, *G;
+    
+    F = *f; G = *g;
+    if (F == G) return(DD_ZERO(dd));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) {
+        if (cuddV(F)<cuddV(G)) return (DD_ONE(dd)); else return (DD_ZERO(dd));
+    }
+    return(NULL);
+    
+} /* end of Cudd_addLessThan */
+
+
+/**Function********************************************************************
+ 
+ Synopsis    [1 if f<=g; 0 otherwise.]
+ 
+ Description [Returns NULL if not a terminal case; f op g otherwise,
+ where f op g is 1 if f<=g; 0 otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addApply]
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addLessThanEquals(
+                       DdManager * dd,
+                       DdNode ** f,
+                       DdNode ** g)
+{
+    DdNode *F, *G;
+    
+    F = *f; G = *g;
+    if (F == G) return(DD_ONE(dd));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) {
+        if (cuddV(F)<=cuddV(G)) return (DD_ONE(dd)); else return (DD_ZERO(dd));
+    }
+    return(NULL);
+    
+} /* end of Cudd_addLessThanEquals */
+
+/**Function********************************************************************
+ 
+ Synopsis    [f to the power of g.]
+ 
+ Description [Returns NULL if not a terminal case; f op g otherwise,
+ where f op g is f to the power of g.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addApply]
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addPow(
+            DdManager * dd,
+            DdNode ** f,
+            DdNode ** g)
+{
+    DdNode *res;
+    DdNode *F, *G;
+    CUDD_VALUE_TYPE value;
+    
+    F = *f; G = *g;
+    if (G == DD_ZERO(dd)) return(DD_ONE(dd));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) {
+        value = pow(cuddV(F), cuddV(G));
+        res = cuddUniqueConst(dd,value);
+        return(res);
+    }
+    return(NULL);
+    
+} /* end of Cudd_addPow */
+
+
+/**Function********************************************************************
+ 
+ Synopsis    [f modulo g.]
+ 
+ Description [Returns NULL if not a terminal case; f op g otherwise,
+ where f op g is f modulo g.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addApply]
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addMod(
+            DdManager * dd,
+            DdNode ** f,
+            DdNode ** g)
+{
+    DdNode *res;
+    DdNode *F, *G;
+    int rem;
+    CUDD_VALUE_TYPE value;
+    
+    F = *f; G = *g;
+    if (cuddIsConstant(F) && cuddIsConstant(G)) {
+        // If g is <=0, then result is NaN
+        if (cuddV(G) <= 0) value = (NAN);
+        // Take care of negative case (% is remainder, not modulo)
+        else {
+            rem = ((int)cuddV(F) % (int)cuddV(G));
+            if (rem < 0) rem += (int)cuddV(G);
+            value = rem;
+        }
+        // Create/return result
+        res = cuddUniqueConst(dd,value);
+        return(res);
+    }
+    return(NULL);
+    
+} /* end of Cudd_addMod */
+
+
+/**Function********************************************************************
+ 
+ Synopsis    [log f base g.]
+ 
+ Description [Returns NULL if not a terminal case; f op g otherwise,
+ where f op g is log f base g.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addApply]
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addLogXY(
+              DdManager * dd,
+              DdNode ** f,
+              DdNode ** g)
+{
+    DdNode *res;
+    DdNode *F, *G;
+    CUDD_VALUE_TYPE value;
+    
+    F = *f; G = *g;
+    if (cuddIsConstant(F) && cuddIsConstant(G)) {
+        // If base is <=0 or ==1 (or +Inf/NaN), then result is NaN
+        if (cuddV(G) <= 0 || cuddV(G) == 1.0 || G==DD_PLUS_INFINITY(dd) || cuddV(G) != cuddV(G)) value = (NAN);
+        // If arg is <0 or NaN, then result is NaN
+        else if (cuddV(F) < 0 || cuddV(F) != cuddV(F)) value = (NAN);
+        // If arg is +Inf, then result is +Inf
+        else if (F==DD_PLUS_INFINITY(dd)) return DD_PLUS_INFINITY(dd);
+        // If arg is (positive/negative) 0, then result is -Inf
+        else if (cuddV(F) == 0.0 || cuddV(F) == -0.0) return DD_MINUS_INFINITY(dd);
+        // Default case: normal log
+        else value = log(cuddV(F)) / log(cuddV(G));
+        // Create/return result
+        res = cuddUniqueConst(dd,value);
+        return(res);
+    }
+    return(NULL);
+    
+} /* end of Cudd_addLogXY */
 
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */

resources/3rdparty/cudd-3.0.0/cudd/cuddInt.h

@@ -1061,6 +1061,8 @@ extern "C" {
 extern DdNode * cuddAddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * cuddAddUnivAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * cuddAddOrAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube);
+extern DdNode * cuddAddMinAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
+extern DdNode * cuddAddMaxAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * cuddAddApplyRecur(DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g);
 extern DdNode * cuddAddMonadicApplyRecur(DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
 extern DdNode * cuddAddScalarInverseRecur(DdManager *dd, DdNode *f, DdNode *epsilon);

resources/3rdparty/cudd-3.0.0/cudd/cuddSat.c

@@ -816,6 +816,71 @@ Cudd_EqualSupNorm(
 
 } /* end of Cudd_EqualSupNorm */
 
+/**Function********************************************************************
+ 
+ Synopsis    [Compares two ADDs for equality within tolerance.]
+ 
+ Description [Same as Cudd_EqualSupNorm but tests for max _relative_ difference
+ i.e. (f-g/f)<e instead of (f-g)<e ]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     []
+ 
+ ******************************************************************************/
+int
+Cudd_EqualSupNormRel(
+                     DdManager * dd /* manager */,
+                     DdNode * f /* first ADD */,
+                     DdNode * g /* second ADD */,
+                     CUDD_VALUE_TYPE  tolerance /* maximum allowed difference */,
+                     int  pr /* verbosity level */)
+{
+    DdNode *fv, *fvn, *gv, *gvn, *r;
+    unsigned int topf, topg;
+    
+    statLine(dd);
+    /* Check terminal cases. */
+    if (f == g) return(1);
+    if (Cudd_IsConstant(f) && Cudd_IsConstant(g)) {
+        if (ddAbs((cuddV(f) - cuddV(g))/cuddV(f)) < tolerance) {
+            return(1);
+        } else {
+            if (pr>0) {
+                (void) fprintf(dd->out,"Offending nodes:\n");
+                (void) fprintf(dd->out,
+                               "f: address = %p\t value = %40.30f\n",
+                               (void *) f, cuddV(f));
+                (void) fprintf(dd->out,
+                               "g: address = %p\t value = %40.30f\n",
+                               (void *) g, cuddV(g));
+            }
+            return(0);
+        }
+    }
+    
+    /* We only insert the result in the cache if the comparison is
+     ** successful. Therefore, if we hit we return 1. */
+    r = cuddCacheLookup2(dd,(DD_CTFP)Cudd_EqualSupNormRel,f,g);
+    if (r != NULL) {
+        return(1);
+    }
+    
+    /* Compute the cofactors and solve the recursive subproblems. */
+    topf = cuddI(dd,f->index);
+    topg = cuddI(dd,g->index);
+    
+    if (topf <= topg) {fv = cuddT(f); fvn = cuddE(f);} else {fv = fvn = f;}
+    if (topg <= topf) {gv = cuddT(g); gvn = cuddE(g);} else {gv = gvn = g;}
+    
+    if (!Cudd_EqualSupNormRel(dd,fv,gv,tolerance,pr)) return(0);
+    if (!Cudd_EqualSupNormRel(dd,fvn,gvn,tolerance,pr)) return(0);
+    
+    cuddCacheInsert2(dd,(DD_CTFP)Cudd_EqualSupNormRel,f,g,DD_ONE(dd));
+    
+    return(1);
+    
+} /* end of Cudd_EqualSupNormRel */
 
 /**
   @brief Expands cube to a prime implicant of f.

src/storage/dd/cudd/InternalCuddAdd.cpp

@@ -434,7 +434,7 @@ namespace storm {
             
             if (currentLevel == maxLevel) {
                 groups.push_back(InternalAdd<DdType::CUDD, ValueType>(ddManager, cudd::ADD(ddManager->getCuddManager(), dd)));
-            } else if (ddGroupVariableIndices[currentLevel] < dd->index) {
+            } else if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
                 splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
                 splitIntoGroupsRec(dd, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
             } else {
@@ -459,15 +459,15 @@ namespace storm {
             
             if (currentLevel == maxLevel) {
                 groups.push_back(std::make_pair(InternalAdd<DdType::CUDD, ValueType>(ddManager, cudd::ADD(ddManager->getCuddManager(), dd1)), InternalAdd<DdType::CUDD, ValueType>(ddManager, cudd::ADD(ddManager->getCuddManager(), dd2))));
-            } else if (ddGroupVariableIndices[currentLevel] < dd1->index) {
-                if (ddGroupVariableIndices[currentLevel] < dd2->index) {
+            } else if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd1)) {
+                if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd2)) {
                     splitIntoGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
                     splitIntoGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
                 } else {
                     splitIntoGroupsRec(dd1, Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
                     splitIntoGroupsRec(dd1, Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
                 }
-            } else if (ddGroupVariableIndices[currentLevel] < dd2->index) {
+            } else if (ddGroupVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd2)) {
                 splitIntoGroupsRec(Cudd_T(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
                 splitIntoGroupsRec(Cudd_E(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel);
             } else {
@@ -500,26 +500,26 @@ namespace storm {
                 DdNode const* thenElse;
                 DdNode const* thenThen;
                 
-                if (ddColumnVariableIndices[currentColumnLevel] < dd->index) {
+                if (ddColumnVariableIndices[currentColumnLevel] < Cudd_NodeReadIndex(dd)) {
                     elseElse = elseThen = thenElse = thenThen = dd;
-                } else if (ddRowVariableIndices[currentColumnLevel] < dd->index) {
-                    elseElse = thenElse = Cudd_E(dd);
-                    elseThen = thenThen = Cudd_T(dd);
+                } else if (ddRowVariableIndices[currentColumnLevel] < Cudd_NodeReadIndex(dd)) {
+                    elseElse = thenElse = Cudd_E_const(dd);
+                    elseThen = thenThen = Cudd_T_const(dd);
                 } else {
-                    DdNode const* elseNode = Cudd_E(dd);
-                    if (ddColumnVariableIndices[currentColumnLevel] < elseNode->index) {
+                    DdNode const* elseNode = Cudd_E_const(dd);
+                    if (ddColumnVariableIndices[currentColumnLevel] < Cudd_NodeReadIndex(elseNode)) {
                         elseElse = elseThen = elseNode;
                     } else {
-                        elseElse = Cudd_E(elseNode);
-                        elseThen = Cudd_T(elseNode);
+                        elseElse = Cudd_E_const(elseNode);
+                        elseThen = Cudd_T_const(elseNode);
                     }
                     
-                    DdNode const* thenNode = Cudd_T(dd);
-                    if (ddColumnVariableIndices[currentColumnLevel] < thenNode->index) {
+                    DdNode const* thenNode = Cudd_T_const(dd);
+                    if (ddColumnVariableIndices[currentColumnLevel] < Cudd_NodeReadIndex(thenNode)) {
                         thenElse = thenThen = thenNode;
                     } else {
-                        thenElse = Cudd_E(thenNode);
-                        thenThen = Cudd_T(thenNode);
+                        thenElse = Cudd_E_const(thenNode);
+                        thenThen = Cudd_T_const(thenNode);
                     }
                 }