From 325d8c5cd2951d6ed459cdb7a30e9a6233c56753 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 12 Nov 2015 21:19:37 +0000
Subject: [PATCH] Fixes to handling of constants in CUDD - factor out pre-hash
 truncation in to a separate function and make sure truncation is also carrued
 oit when *re*hashing the table. [from Joachim Klein]

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10872 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 cudd/cudd/cuddTable.c | 35 ++++++++++++++++++++++++-----------
 1 file changed, 24 insertions(+), 11 deletions(-)

diff --git a/cudd/cudd/cuddTable.c b/cudd/cudd/cuddTable.c
index 2b31990f..8ee039c6 100644
--- a/cudd/cudd/cuddTable.c
+++ b/cudd/cudd/cuddTable.c
@@ -1463,6 +1463,28 @@ cuddUniqueInterZdd(
 } /* end of cuddUniqueInterZdd */
 
 
+/**
+ * Truncate a double value to 10^-10 precision.
+ */
+static double truncateDoubleConstant(double value)
+{
+	double trunc, m, n;
+
+	// (round off before doing hash function to ensure
+	//  close valued constants are in the same table)
+	if (finite(value)) {
+		trunc = 10000000000.0; // 10^10
+		m = value * trunc;
+		n = floor(m);
+		if (m-n >= 0.5)
+			n = n + 1;
+		n = n / trunc;
+		return n;
+	} else {
+		return value;
+	}
+}
+
 /**Function********************************************************************
 
   Synopsis    [Checks the unique table for the existence of a constant node.]
@@ -1511,17 +1533,7 @@ cuddUniqueConst(
     // this is the new version...
     // (round off before doing hash function to ensure
     //  close valued constants are in the same table)
-    if (finite(value)) {
-		trunc = 10000000000.0; // 10^10
-		m = value * trunc;
-		n = floor(m);
-		if (m-n >= 0.5) 
-			n = n + 1;
-		n = n / trunc;
-		split.value = n;
-	} else {
-	    split.value = value;
-	}
+    split.value = truncateDoubleConstant(value);
 
     pos = ddHash(split.bits[0], split.bits[1], unique->constants.shift);
     nodelist = unique->constants.nodelist;
@@ -1710,6 +1722,7 @@ cuddRehash(
 	    while (node != NULL) {
 		next = node->next;
 		split.value = cuddV(node);
+		split.value = truncateDoubleConstant(split.value);
 		pos = ddHash(split.bits[0], split.bits[1], shift);
 		node->next = nodelist[pos];
 		nodelist[pos] = node;