From dd0813b8c4dcd3260cc7d23614660ecb57ef1ca3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 17 Feb 2016 21:40:48 +0100 Subject: [PATCH] cudd3 now working, but tests segfaulting Former-commit-id: 9742e4e75eee5a6cc1979afe0ac1898430c1548a --- resources/3rdparty/CMakeLists.txt | 4 +- .../3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc | 143 ++++++- .../3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh | 17 +- resources/3rdparty/cudd-3.0.0/cudd/cudd.h | 14 + .../3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c | 259 ++++++++++++- .../3rdparty/cudd-3.0.0/cudd/cuddAddApply.c | 352 ++++++++++++++++++ resources/3rdparty/cudd-3.0.0/cudd/cuddInt.h | 2 + resources/3rdparty/cudd-3.0.0/cudd/cuddSat.c | 65 ++++ src/storage/dd/cudd/InternalCuddAdd.cpp | 32 +- 9 files changed, 864 insertions(+), 24 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 049b2a4ac..1eae19497 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/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 diff --git a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc index 6aa67b516..e1c9807d8 100644 --- a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc +++ b/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( diff --git a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh index e71bc486c..f180320bd 100644 --- a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh +++ b/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 z) const; ADD Triangle(const ADD& g, std::vector 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 diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cudd.h b/resources/3rdparty/cudd-3.0.0/cudd/cudd.h index 9c140fd5d..e2447c878 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cudd.h +++ b/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); diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c index 33c578083..db284f7b4 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c +++ b/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 */ diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c index 3800638dc..d7a3c71cc 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c +++ b/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 f0) { + (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. diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 564a521e9..0925b4f58 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -434,7 +434,7 @@ namespace storm { if (currentLevel == maxLevel) { groups.push_back(InternalAdd(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(ddManager, cudd::ADD(ddManager->getCuddManager(), dd1)), InternalAdd(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); } }