Added log(x,b) function to CUDD.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@570 bbc10eb1-c90d-0410-af57-cb519fbb1720

cudd/cudd/cudd.h

@@ -750,6 +750,7 @@ 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_addMonadicApply (DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
 extern DdNode * Cudd_addLog (DdManager * dd, DdNode * f);
 extern DdNode * Cudd_addFloor (DdManager * dd, DdNode * f);

cudd/cudd/cuddAddApply.c

@@ -1062,6 +1062,49 @@ Cudd_addMod(
 } /* 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 = (0.0/0.0);
+	// If arg is <0 or NaN, then result is NaN
+	else if (cuddV(F) < 0 || cuddV(F) != cuddV(F)) value = (0.0/0.0);
+	// 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                                          */
 /*---------------------------------------------------------------------------*/

cudd/modified/README

@@ -68,6 +68,7 @@ Details
   Cudd_addLessThanEquals() - f op g = 1 if f<=g else 0
   Cudd_addPow() - power
   Cudd_addMod() - modulo
+  Cudd_addLogXY() - log x base y
   
 * Added the following functions to be used with Cudd_addMonadicApply()
   Cudd_addFloor() - floor
@@ -119,6 +120,7 @@ Details
   Cudd_addLessThanEquals()
   Cudd_addPow()
   Cudd_addMod()
+  Cudd_addLogXY()
   Cudd_addFloor()
   Cudd_addCeil()
   Cudd_EqualSupNormRel()