Integrated a few more functions to CUDD which are necessary (PRISM adds them as well).

resources/3rdparty/cudd-2.5.0/Makefile

@@ -201,7 +201,7 @@ IDIR	= $(DDWDIR)/include
 INCLUDE = -I$(IDIR)
 
 BDIRS	= cudd dddmp mtr st util epd obj
-DIRS	= $(BDIRS) nanotrav
+DIRS	= $(BDIRS)
 
 #------------------------------------------------------------------------
 

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

@@ -786,6 +786,12 @@ extern DdNode * Cudd_addXor (DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addXnor (DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addMonadicApply (DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
 extern DdNode * Cudd_addLog (DdManager * dd, DdNode * f);
+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_addFindMax (DdManager *dd, DdNode *f);
 extern DdNode * Cudd_addFindMin (DdManager *dd, DdNode *f);
 extern DdNode * Cudd_addIthBit (DdManager *dd, DdNode *f, int bit);

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

@@ -783,7 +783,187 @@ Cudd_addLog(
 
 } /* end of Cudd_addLog */
 
+/**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 */
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
 /*---------------------------------------------------------------------------*/