Commenting to document recent changes to CUDD constant hashing/truncation. [from Joachim Klein]

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

cudd/cudd/cuddTable.c

@@ -1464,7 +1464,12 @@ cuddUniqueInterZdd(
 
 
 /**
- * Truncate a double value to 10^-10 precision.
+ * Helper function: Truncate a double value to approximately
+ * 10^-10 precision (with rounding).
+ *
+ * This is used in cuddUnqiueConstant and cuddRehash to generate a
+ * canonical double value for the hash lookup, ensuring that values that
+ * are close will be hashed to the same bucket.
  */
 static double truncateDoubleConstant(double value)
 {
@@ -1524,15 +1529,42 @@ cuddUniqueConst(
 
     cuddAdjust(value); /* for the case of crippled infinities */
 
+
     if (ddAbs(value) < unique->epsilon) {
-	value = 0.0;
-    }
-    /* this is the old version:
-    split.value = value;
-    */
-    // this is the new version...
-    // (round off before doing hash function to ensure
-    //  close valued constants are in the same table)
+        value = 0.0;
+    }
+
+    /* PRISM-specific behaviour:
+     * To keep the number of distinct constants with very close double value low,
+     * we would like to identify constants where
+     *   ddEqualVal(value, existing_constant, unique->epsilon)
+     * is true, i.e., where the values differ by less than the CUDD epsilon parameter.
+     *
+     * However, as the lookup in the unique table is performed via a hashtable, we have
+     * to ensure that all constants that are close are hashed into the same bucket
+     * in the hash table.
+     *
+     * This is achieved by performing the hashtable lookup not on the value itself, but
+     * on a truncated/rounded version, i.e., where the precision has been reduced such
+     * that it is ensured that all constants within the epsilon range are hashed to
+     * the same value.
+     *
+     * The procedure is then:
+     *  1) Lookup the bucket (pos) using the truncated value (split.value)
+     *  2) In the linked list of the bucket, search for an exact match
+     *     or a close match
+     *  3) If there is no match, insert the value.
+     *
+     * To ensure that the uniqueness for the constants is not violated, during
+     * rehashing of the unique table for the constants, the truncation has to be
+     * applied as well (see cuddRehash, case for i == CUDD_CONST_INDEX).
+     */
+
+    // this is the original, CUDD version (without truncation):
+    // split.value = value;
+
+    // PRISM version:
+    // use truncated value for hash lookup
     split.value = truncateDoubleConstant(value);
 
     pos = ddHash(split.bits[0], split.bits[1], unique->constants.shift);
@@ -1721,8 +1753,14 @@ cuddRehash(
 	    node = oldnodelist[j];
 	    while (node != NULL) {
 		next = node->next;
-		split.value = cuddV(node);
-		split.value = truncateDoubleConstant(split.value);
+
+		// original CUDD version:
+		// split.value = cuddV(node);
+
+		// PRISM version: we have to truncate the value for the hash lookup
+		// (see corresponding comment in cuddUniqueConstant)
+		split.value = truncateDoubleConstant(cuddV(node));
+
 		pos = ddHash(split.bits[0], split.bits[1], shift);
 		node->next = nodelist[pos];
 		nodelist[pos] = node;