From dc7c7f2817ae094fb15101ad7c141869b1b321ff Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 26 Feb 2008 15:03:48 +0000
Subject: [PATCH] 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         |  1 +
 cudd/cudd/cuddAddApply.c | 43 ++++++++++++++++++++++++++++++++++++++++
 cudd/modified/README     |  2 ++
 3 files changed, 46 insertions(+)

diff --git a/cudd/cudd/cudd.h b/cudd/cudd/cudd.h
index ea3d7ab7..9ac4e0cf 100644
--- a/cudd/cudd/cudd.h
+++ b/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);
diff --git a/cudd/cudd/cuddAddApply.c b/cudd/cudd/cuddAddApply.c
index 25246fdd..0dd6f80f 100644
--- a/cudd/cudd/cuddAddApply.c
+++ b/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                                          */
 /*---------------------------------------------------------------------------*/
diff --git a/cudd/modified/README b/cudd/modified/README
index 099e2225..ab31b11e 100644
--- a/cudd/modified/README
+++ b/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()