Upgrading epd and mtr packages to be compatible with the latest release of CUDD 2.4.2

5 files changed, 337 insertions, 337 deletions

diff --git a/src/bdd/epd/epd.c b/src/bdd/epd/epd.c
index 9f362f1b..3f92af94 100644
--- a/src/bdd/epd/epd.c
+++ b/src/bdd/epd/epd.c
@@ -52,7 +52,7 @@
 #include <stdlib.h>
 #include <string.h>
 #include <math.h>
-#include "util.h"
+#include "util_hack.h"
 #include "epd.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -71,9 +71,9 @@ ABC_NAMESPACE_IMPL_START
 EpDouble *
 EpdAlloc(void)
 {
-  EpDouble    *epd;
+  EpDouble      *epd;
 
-  epd = ALLOC(EpDouble, 1);
+  epd = ABC_ALLOC(EpDouble, 1);
   return(epd);
 }
 
@@ -116,7 +116,7 @@ EpdCmp(const char *key1, const char *key2)
 void
 EpdFree(EpDouble *epd)
 {
-  FREE(epd);
+  ABC_FREE(epd);
 }
 
 
@@ -134,9 +134,9 @@ EpdFree(EpDouble *epd)
 void
 EpdGetString(EpDouble *epd, char *str)
 {
-  double    value;
-  int        exponent;
-  char        *pos;
+  double        value;
+  int           exponent;
+  char          *pos;
 
   if (IsNanDouble(epd->type.value)) {
     sprintf(str, "NaN");
@@ -150,7 +150,7 @@ EpdGetString(EpDouble *epd, char *str)
   }
 
   assert(epd->type.bits.exponent == EPD_MAX_BIN ||
-     epd->type.bits.exponent == 0);
+         epd->type.bits.exponent == 0);
 
   EpdGetValueAndDecimalExponent(epd, &value, &exponent);
   sprintf(str, "%e", value);
@@ -204,15 +204,15 @@ EpdConvert(double value, EpDouble *epd)
 void
 EpdMultiply(EpDouble *epd1, double value)
 {
-  EpDouble    epd2;
-  double    tmp;
-  int        exponent;
+  EpDouble      epd2;
+  double        tmp;
+  int           exponent;
 
   if (EpdIsNan(epd1) || IsNanDouble(value)) {
     EpdMakeNan(epd1);
     return;
   } else if (EpdIsInf(epd1) || IsInfDouble(value)) {
-    int    sign;
+    int sign;
 
     EpdConvert(value, &epd2);
     sign = epd1->type.bits.sign ^ epd2.type.bits.sign;
@@ -245,14 +245,14 @@ EpdMultiply(EpDouble *epd1, double value)
 void
 EpdMultiply2(EpDouble *epd1, EpDouble *epd2)
 {
-  double    value;
-  int        exponent;
+  double        value;
+  int           exponent;
 
   if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
     EpdMakeNan(epd1);
     return;
   } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
-    int    sign;
+    int sign;
 
     sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
     EpdMakeInf(epd1, sign);
@@ -284,14 +284,14 @@ EpdMultiply2(EpDouble *epd1, EpDouble *epd2)
 void
 EpdMultiply2Decimal(EpDouble *epd1, EpDouble *epd2)
 {
-  double    value;
-  int        exponent;
+  double        value;
+  int           exponent;
 
   if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
     EpdMakeNan(epd1);
     return;
   } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
-    int    sign;
+    int sign;
 
     sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
     EpdMakeInf(epd1, sign);
@@ -324,7 +324,7 @@ EpdMultiply3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
     EpdMakeNan(epd1);
     return;
   } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
-    int    sign;
+    int sign;
 
     sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
     EpdMakeInf(epd3, sign);
@@ -358,7 +358,7 @@ EpdMultiply3Decimal(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
     EpdMakeNan(epd1);
     return;
   } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
-    int    sign;
+    int sign;
 
     sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
     EpdMakeInf(epd3, sign);
@@ -385,15 +385,15 @@ EpdMultiply3Decimal(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
 void
 EpdDivide(EpDouble *epd1, double value)
 {
-  EpDouble    epd2;
-  double    tmp;
-  int        exponent;
+  EpDouble      epd2;
+  double        tmp;
+  int           exponent;
 
   if (EpdIsNan(epd1) || IsNanDouble(value)) {
     EpdMakeNan(epd1);
     return;
   } else if (EpdIsInf(epd1) || IsInfDouble(value)) {
-    int    sign;
+    int sign;
 
     EpdConvert(value, &epd2);
     if (EpdIsInf(epd1) && IsInfDouble(value)) {
@@ -438,14 +438,14 @@ EpdDivide(EpDouble *epd1, double value)
 void
 EpdDivide2(EpDouble *epd1, EpDouble *epd2)
 {
-  double    value;
-  int        exponent;
+  double        value;
+  int           exponent;
 
   if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
     EpdMakeNan(epd1);
     return;
   } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
-    int    sign;
+    int sign;
 
     if (EpdIsInf(epd1) && EpdIsInf(epd2)) {
       EpdMakeNan(epd1);
@@ -493,7 +493,7 @@ EpdDivide3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
     EpdMakeNan(epd3);
     return;
   } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
-    int    sign;
+    int sign;
 
     if (EpdIsInf(epd1) && EpdIsInf(epd2)) {
       EpdMakeNan(epd3);
@@ -535,21 +535,21 @@ EpdDivide3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
 void
 EpdAdd(EpDouble *epd1, double value)
 {
-  EpDouble    epd2;
-  double    tmp;
-  int        exponent, diff;
+  EpDouble      epd2;
+  double        tmp;
+  int           exponent, diff;
 
   if (EpdIsNan(epd1) || IsNanDouble(value)) {
     EpdMakeNan(epd1);
     return;
   } else if (EpdIsInf(epd1) || IsInfDouble(value)) {
-    int    sign;
+    int sign;
 
     EpdConvert(value, &epd2);
     if (EpdIsInf(epd1) && IsInfDouble(value)) {
       sign = epd1->type.bits.sign ^ epd2.type.bits.sign;
       if (sign == 1)
-    EpdMakeNan(epd1);
+        EpdMakeNan(epd1);
     } else if (EpdIsInf(&epd2)) {
       EpdCopy(&epd2, epd1);
     }
@@ -597,19 +597,19 @@ EpdAdd(EpDouble *epd1, double value)
 void
 EpdAdd2(EpDouble *epd1, EpDouble *epd2)
 {
-  double    value;
-  int        exponent, diff;
+  double        value;
+  int           exponent, diff;
 
   if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
     EpdMakeNan(epd1);
     return;
   } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
-    int    sign;
+    int sign;
 
     if (EpdIsInf(epd1) && EpdIsInf(epd2)) {
       sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
       if (sign == 1)
-    EpdMakeNan(epd1);
+        EpdMakeNan(epd1);
     } else if (EpdIsInf(epd2)) {
       EpdCopy(epd2, epd1);
     }
@@ -623,7 +623,7 @@ EpdAdd2(EpDouble *epd1, EpDouble *epd2)
     diff = epd1->exponent - epd2->exponent;
     if (diff <= EPD_MAX_BIN) {
       value = epd1->type.value +
-        epd2->type.value / pow((double)2.0, (double)diff);
+                epd2->type.value / pow((double)2.0, (double)diff);
     } else
       value = epd1->type.value;
     exponent = epd1->exponent;
@@ -631,7 +631,7 @@ EpdAdd2(EpDouble *epd1, EpDouble *epd2)
     diff = epd2->exponent - epd1->exponent;
     if (diff <= EPD_MAX_BIN) {
       value = epd1->type.value / pow((double)2.0, (double)diff) +
-        epd2->type.value;
+                epd2->type.value;
     } else
       value = epd2->type.value;
     exponent = epd2->exponent;
@@ -659,21 +659,21 @@ EpdAdd2(EpDouble *epd1, EpDouble *epd2)
 void
 EpdAdd3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
 {
-  double    value;
-  int        exponent, diff;
+  double        value;
+  int           exponent, diff;
 
   if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
     EpdMakeNan(epd3);
     return;
   } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
-    int    sign;
+    int sign;
 
     if (EpdIsInf(epd1) && EpdIsInf(epd2)) {
       sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
       if (sign == 1)
-    EpdMakeNan(epd3);
+        EpdMakeNan(epd3);
       else
-    EpdCopy(epd1, epd3);
+        EpdCopy(epd1, epd3);
     } else if (EpdIsInf(epd1)) {
       EpdCopy(epd1, epd3);
     } else {
@@ -689,7 +689,7 @@ EpdAdd3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
     diff = epd1->exponent - epd2->exponent;
     if (diff <= EPD_MAX_BIN) {
       value = epd1->type.value +
-        epd2->type.value / pow((double)2.0, (double)diff);
+                epd2->type.value / pow((double)2.0, (double)diff);
     } else
       value = epd1->type.value;
     exponent = epd1->exponent;
@@ -697,7 +697,7 @@ EpdAdd3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
     diff = epd2->exponent - epd1->exponent;
     if (diff <= EPD_MAX_BIN) {
       value = epd1->type.value / pow((double)2.0, (double)diff) +
-        epd2->type.value;
+                epd2->type.value;
     } else
       value = epd2->type.value;
     exponent = epd2->exponent;
@@ -725,21 +725,21 @@ EpdAdd3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
 void
 EpdSubtract(EpDouble *epd1, double value)
 {
-  EpDouble    epd2;
-  double    tmp;
-  int        exponent, diff;
+  EpDouble      epd2;
+  double        tmp;
+  int           exponent, diff;
 
   if (EpdIsNan(epd1) || IsNanDouble(value)) {
     EpdMakeNan(epd1);
     return;
   } else if (EpdIsInf(epd1) || IsInfDouble(value)) {
-    int    sign;
+    int sign;
 
     EpdConvert(value, &epd2);
     if (EpdIsInf(epd1) && IsInfDouble(value)) {
       sign = epd1->type.bits.sign ^ epd2.type.bits.sign;
       if (sign == 0)
-    EpdMakeNan(epd1);
+        EpdMakeNan(epd1);
     } else if (EpdIsInf(&epd2)) {
       EpdCopy(&epd2, epd1);
     }
@@ -787,19 +787,19 @@ EpdSubtract(EpDouble *epd1, double value)
 void
 EpdSubtract2(EpDouble *epd1, EpDouble *epd2)
 {
-  double    value;
-  int        exponent, diff;
+  double        value;
+  int           exponent, diff;
 
   if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
     EpdMakeNan(epd1);
     return;
   } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
-    int    sign;
+    int sign;
 
     if (EpdIsInf(epd1) && EpdIsInf(epd2)) {
       sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
       if (sign == 0)
-    EpdMakeNan(epd1);
+        EpdMakeNan(epd1);
     } else if (EpdIsInf(epd2)) {
       EpdCopy(epd2, epd1);
     }
@@ -813,7 +813,7 @@ EpdSubtract2(EpDouble *epd1, EpDouble *epd2)
     diff = epd1->exponent - epd2->exponent;
     if (diff <= EPD_MAX_BIN) {
       value = epd1->type.value -
-        epd2->type.value / pow((double)2.0, (double)diff);
+                epd2->type.value / pow((double)2.0, (double)diff);
     } else
       value = epd1->type.value;
     exponent = epd1->exponent;
@@ -821,7 +821,7 @@ EpdSubtract2(EpDouble *epd1, EpDouble *epd2)
     diff = epd2->exponent - epd1->exponent;
     if (diff <= EPD_MAX_BIN) {
       value = epd1->type.value / pow((double)2.0, (double)diff) -
-        epd2->type.value;
+                epd2->type.value;
     } else
       value = epd2->type.value * (double)(-1.0);
     exponent = epd2->exponent;
@@ -849,21 +849,21 @@ EpdSubtract2(EpDouble *epd1, EpDouble *epd2)
 void
 EpdSubtract3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
 {
-  double    value;
-  int        exponent, diff;
+  double        value;
+  int           exponent, diff;
 
   if (EpdIsNan(epd1) || EpdIsNan(epd2)) {
     EpdMakeNan(epd3);
     return;
   } else if (EpdIsInf(epd1) || EpdIsInf(epd2)) {
-    int    sign;
+    int sign;
 
     if (EpdIsInf(epd1) && EpdIsInf(epd2)) {
       sign = epd1->type.bits.sign ^ epd2->type.bits.sign;
       if (sign == 0)
-    EpdCopy(epd1, epd3);
+        EpdCopy(epd1, epd3);
       else
-    EpdMakeNan(epd3);
+        EpdMakeNan(epd3);
     } else if (EpdIsInf(epd1)) {
       EpdCopy(epd1, epd1);
     } else {
@@ -880,7 +880,7 @@ EpdSubtract3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
     diff = epd1->exponent - epd2->exponent;
     if (diff <= EPD_MAX_BIN) {
       value = epd1->type.value -
-        epd2->type.value / pow((double)2.0, (double)diff);
+                epd2->type.value / pow((double)2.0, (double)diff);
     } else
       value = epd1->type.value;
     exponent = epd1->exponent;
@@ -888,7 +888,7 @@ EpdSubtract3(EpDouble *epd1, EpDouble *epd2, EpDouble *epd3)
     diff = epd2->exponent - epd1->exponent;
     if (diff <= EPD_MAX_BIN) {
       value = epd1->type.value / pow((double)2.0, (double)diff) -
-        epd2->type.value;
+                epd2->type.value;
     } else
       value = epd2->type.value * (double)(-1.0);
     exponent = epd2->exponent;
@@ -920,7 +920,7 @@ EpdPow2(int n, EpDouble *epd)
     EpdConvert(pow((double)2.0, (double)n), epd);
   } else {
     EpDouble    epd1, epd2;
-    int        n1, n2;
+    int         n1, n2;
 
     n1 = n / 2;
     n2 = n - n1;
@@ -951,7 +951,7 @@ EpdPow2Decimal(int n, EpDouble *epd)
     EpdNormalizeDecimal(epd);
   } else {
     EpDouble    epd1, epd2;
-    int        n1, n2;
+    int         n1, n2;
 
     n1 = n / 2;
     n2 = n - n1;
@@ -976,7 +976,7 @@ EpdPow2Decimal(int n, EpDouble *epd)
 void
 EpdNormalize(EpDouble *epd)
 {
-  int        exponent;
+  int           exponent;
 
   if (IsNanOrInfDouble(epd->type.value)) {
     epd->exponent = 0;
@@ -1006,7 +1006,7 @@ EpdNormalize(EpDouble *epd)
 void
 EpdNormalizeDecimal(EpDouble *epd)
 {
-  int        exponent;
+  int           exponent;
 
   if (IsNanOrInfDouble(epd->type.value)) {
     epd->exponent = 0;
@@ -1033,7 +1033,7 @@ EpdNormalizeDecimal(EpDouble *epd)
 void
 EpdGetValueAndDecimalExponent(EpDouble *epd, double *value, int *exponent)
 {
-  EpDouble    epd1, epd2;
+  EpDouble      epd1, epd2;
 
   if (EpdIsNanOrInf(epd))
     return;
@@ -1067,8 +1067,8 @@ EpdGetValueAndDecimalExponent(EpDouble *epd, double *value, int *exponent)
 int
 EpdGetExponent(double value)
 {
-  int        exponent;
-  EpDouble    epd;
+  int           exponent;
+  EpDouble      epd;
 
   epd.type.value = value;
   exponent = epd.type.bits.exponent;
@@ -1090,8 +1090,8 @@ EpdGetExponent(double value)
 int
 EpdGetExponentDecimal(double value)
 {
-  char    *pos, str[24];
-  int    exponent;
+  char  *pos, str[24];
+  int   exponent;
 
   sprintf(str, "%E", value);
   pos = strstr(str, "E");
@@ -1304,7 +1304,7 @@ IsInfDouble(double value)
 int
 IsNanDouble(double value)
 {
-  EpType    val;
+  EpType        val;
   
   val.value = value;
   if (val.nan.exponent == EPD_EXP_INF &&
@@ -1332,7 +1332,7 @@ IsNanDouble(double value)
 int
 IsNanOrInfDouble(double value)
 {
-  EpType    val;
+  EpType        val;
 
   val.value = value;
   if (val.nan.exponent == EPD_EXP_INF &&
diff --git a/src/bdd/epd/epd.h b/src/bdd/epd/epd.h
index f19f2830..1ca033d2 100644
--- a/src/bdd/epd/epd.h
+++ b/src/bdd/epd/epd.h
@@ -57,9 +57,9 @@ ABC_NAMESPACE_HEADER_START
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
 
-#define    EPD_MAX_BIN    1023
-#define    EPD_MAX_DEC    308
-#define    EPD_EXP_INF    0x7ff
+#define EPD_MAX_BIN     1023
+#define EPD_MAX_DEC     308
+#define EPD_EXP_INF     0x7ff
 
 /*---------------------------------------------------------------------------*/
 /* Structure declarations                                                    */
@@ -74,15 +74,15 @@ ABC_NAMESPACE_HEADER_START
   SeeAlso     []
 
 ******************************************************************************/
-#ifdef    EPD_BIG_ENDIAN
-struct IeeeDoubleStruct {    /* BIG_ENDIAN */
+#ifdef  EPD_BIG_ENDIAN
+struct IeeeDoubleStruct {       /* BIG_ENDIAN */
   unsigned int sign: 1;
   unsigned int exponent: 11;
   unsigned int mantissa0: 20;
   unsigned int mantissa1: 32;
 };
 #else
-struct IeeeDoubleStruct {    /* LITTLE_ENDIAN */
+struct IeeeDoubleStruct {       /* LITTLE_ENDIAN */
   unsigned int mantissa1: 32;
   unsigned int mantissa0: 20;
   unsigned int exponent: 11;
@@ -99,8 +99,8 @@ struct IeeeDoubleStruct {    /* LITTLE_ENDIAN */
   SeeAlso     []
 
 ******************************************************************************/
-#ifdef    EPD_BIG_ENDIAN
-struct IeeeNanStruct {    /* BIG_ENDIAN */
+#ifdef  EPD_BIG_ENDIAN
+struct IeeeNanStruct {  /* BIG_ENDIAN */
   unsigned int sign: 1;
   unsigned int exponent: 11;
   unsigned int quiet_bit: 1;
@@ -108,7 +108,7 @@ struct IeeeNanStruct {    /* BIG_ENDIAN */
   unsigned int mantissa1: 32;
 };
 #else
-struct IeeeNanStruct {    /* LITTLE_ENDIAN */
+struct IeeeNanStruct {  /* LITTLE_ENDIAN */
   unsigned int mantissa1: 32;
   unsigned int mantissa0: 19;
   unsigned int quiet_bit: 1;
@@ -127,14 +127,14 @@ struct IeeeNanStruct {    /* LITTLE_ENDIAN */
 
 ******************************************************************************/
 union EpTypeUnion {
-  double            value;
-  struct IeeeDoubleStruct    bits;
-  struct IeeeNanStruct        nan;
+  double                        value;
+  struct IeeeDoubleStruct       bits;
+  struct IeeeNanStruct          nan;
 };
 
 struct EpDoubleStruct {
-  union EpTypeUnion        type;
-  int                exponent;
+  union EpTypeUnion             type;
+  int                           exponent;
 };
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/mtr/mtr.h b/src/bdd/mtr/mtr.h
index d3b703b8..5ac35313 100644
--- a/src/bdd/mtr/mtr.h
+++ b/src/bdd/mtr/mtr.h
@@ -96,20 +96,20 @@ ABC_NAMESPACE_HEADER_START
 #endif
 
 /* Flag definitions */
-#define MTR_DEFAULT    0x00000000
+#define MTR_DEFAULT     0x00000000
 #define MTR_TERMINAL    0x00000001
-#define MTR_SOFT    0x00000002
-#define MTR_FIXED    0x00000004
-#define MTR_NEWNODE    0x00000008
+#define MTR_SOFT        0x00000002
+#define MTR_FIXED       0x00000004
+#define MTR_NEWNODE     0x00000008
 
 /* MTR_MAXHIGH is defined in such a way that on 32-bit and 64-bit
 ** machines one can cast a value to (int) without generating a negative
 ** number.
 */
 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
-#define MTR_MAXHIGH    (((MtrHalfWord) ~0) >> 1)
+#define MTR_MAXHIGH     (((MtrHalfWord) ~0) >> 1)
 #else
-#define MTR_MAXHIGH    ((MtrHalfWord) ~0)
+#define MTR_MAXHIGH     ((MtrHalfWord) ~0)
 #endif
 
 
@@ -150,8 +150,8 @@ typedef struct MtrNode {
 /*---------------------------------------------------------------------------*/
 
 /* Flag manipulation macros */
-#define MTR_SET(node, flag)        (node->flags |= (flag))
-#define MTR_RESET(node, flag)    (node->flags &= ~ (flag))
+#define MTR_SET(node, flag)             (node->flags |= (flag))
+#define MTR_RESET(node, flag)   (node->flags &= ~ (flag))
 #define MTR_TEST(node, flag)    (node->flags & (flag))
 
 
diff --git a/src/bdd/mtr/mtrBasic.c b/src/bdd/mtr/mtrBasic.c
index e06317d5..a2420d4a 100644
--- a/src/bdd/mtr/mtrBasic.c
+++ b/src/bdd/mtr/mtrBasic.c
@@ -7,20 +7,20 @@
   Synopsis    [Basic manipulation of multiway branching trees.]
 
   Description [External procedures included in this module:
-        <ul>
-        <li> Mtr_AllocNode()
-        <li> Mtr_DeallocNode()
-        <li> Mtr_InitTree()
-        <li> Mtr_FreeTree()
-        <li> Mtr_CopyTree()
-        <li> Mtr_MakeFirstChild()
-        <li> Mtr_MakeLastChild()
-        <li> Mtr_CreateFirstChild()
-        <li> Mtr_CreateLastChild()
-        <li> Mtr_MakeNextSibling()
-        <li> Mtr_PrintTree()
-        </ul>
-        ]
+            <ul>
+            <li> Mtr_AllocNode()
+            <li> Mtr_DeallocNode()
+            <li> Mtr_InitTree()
+            <li> Mtr_FreeTree()
+            <li> Mtr_CopyTree()
+            <li> Mtr_MakeFirstChild()
+            <li> Mtr_MakeLastChild()
+            <li> Mtr_CreateFirstChild()
+            <li> Mtr_CreateLastChild()
+            <li> Mtr_MakeNextSibling()
+            <li> Mtr_PrintTree()
+            </ul>
+            ]
 
   SeeAlso     [cudd package]
 
@@ -60,7 +60,7 @@
 
 ******************************************************************************/
 
-#include "util.h"
+#include "util_hack.h"
 #include "mtrInt.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -119,7 +119,7 @@ Mtr_AllocNode(void)
 {
     MtrNode *node;
 
-    node = ALLOC(MtrNode,1);
+    node = ABC_ALLOC(MtrNode,1);
     return node;
 
 } /* Mtr_AllocNode */
@@ -140,7 +140,7 @@ void
 Mtr_DeallocNode(
   MtrNode * node /* node to be deallocated */)
 {
-    FREE(node);
+    ABC_FREE(node);
     return;
 
 } /* end of Mtr_DeallocNode */
@@ -224,18 +224,18 @@ Mtr_CopyTree(
     if (copy == NULL) return(NULL);
     copy->parent = copy->elder = copy->child = copy->younger = NULL;
     if (node->child != NULL) {
-    copy->child = Mtr_CopyTree(node->child, expansion);
-    if (copy->child == NULL) {
-        Mtr_DeallocNode(copy);
-        return(NULL);
-    }
+        copy->child = Mtr_CopyTree(node->child, expansion);
+        if (copy->child == NULL) {
+            Mtr_DeallocNode(copy);
+            return(NULL);
+        }
     }
     if (node->younger != NULL) {
-    copy->younger = Mtr_CopyTree(node->younger, expansion);
-    if (copy->younger == NULL) {
-        Mtr_FreeTree(copy);
-        return(NULL);
-    }
+        copy->younger = Mtr_CopyTree(node->younger, expansion);
+        if (copy->younger == NULL) {
+            Mtr_FreeTree(copy);
+            return(NULL);
+        }
     }
     copy->flags = node->flags;
     copy->low = node->low * expansion;
@@ -243,11 +243,11 @@ Mtr_CopyTree(
     copy->index = node->index * expansion;
     if (copy->younger) copy->younger->elder = copy;
     if (copy->child) {
-    MtrNode *auxnode = copy->child;
-    while (auxnode != NULL) {
-        auxnode->parent = copy;
-        auxnode = auxnode->younger;
-    }
+        MtrNode *auxnode = copy->child;
+        while (auxnode != NULL) {
+            auxnode->parent = copy;
+            auxnode = auxnode->younger;
+        }
     }
     return(copy);
 
@@ -275,9 +275,9 @@ Mtr_MakeFirstChild(
     child->elder = NULL;
     if (parent->child != NULL) {
 #ifdef MTR_DEBUG
-    assert(parent->child->elder == NULL);
+        assert(parent->child->elder == NULL);
 #endif
-    parent->child->elder = child;
+        parent->child->elder = child;
     }
     parent->child = child;
     return;
@@ -306,14 +306,14 @@ Mtr_MakeLastChild(
     child->younger = NULL;
 
     if (parent->child == NULL) {
-    parent->child = child;
-    child->elder = NULL;
+        parent->child = child;
+        child->elder = NULL;
     } else {
-    for (node = parent->child;
-         node->younger != NULL;
-         node = node->younger);
-    node->younger = child;
-    child->elder = node;
+        for (node = parent->child;
+             node->younger != NULL;
+             node = node->younger);
+        node->younger = child;
+        child->elder = node;
     }
     child->parent = parent;
     return;
@@ -398,7 +398,7 @@ Mtr_MakeNextSibling(
 {
     second->younger = first->younger;
     if (first->younger != NULL) {
-    first->younger->elder = second;
+        first->younger->elder = second;
     }
     second->parent = first->parent;
     first->younger = second;
diff --git a/src/bdd/mtr/mtrGroup.c b/src/bdd/mtr/mtrGroup.c
index afc7bfdf..280108c9 100644
--- a/src/bdd/mtr/mtrGroup.c
+++ b/src/bdd/mtr/mtrGroup.c
@@ -7,20 +7,20 @@
   Synopsis    [Functions to support group specification for reordering.]
 
   Description [External procedures included in this module:
-        <ul>
-        <li> Mtr_InitGroupTree()
-        <li> Mtr_MakeGroup()
-        <li> Mtr_DissolveGroup()
-        <li> Mtr_FindGroup()
-        <li> Mtr_SwapGroups()
-        <li> Mtr_PrintGroups()
-        <li> Mtr_ReadGroups()
-        </ul>
-    Static procedures included in this module:
-        <ul>
-        <li> mtrShiftHL
-        </ul>
-        ]
+            <ul>
+            <li> Mtr_InitGroupTree()
+            <li> Mtr_MakeGroup()
+            <li> Mtr_DissolveGroup()
+            <li> Mtr_FindGroup()
+            <li> Mtr_SwapGroups()
+            <li> Mtr_PrintGroups()
+            <li> Mtr_ReadGroups()
+            </ul>
+        Static procedures included in this module:
+            <ul>
+            <li> mtrShiftHL
+            </ul>
+            ]
 
   SeeAlso     [cudd package]
 
@@ -60,7 +60,7 @@
 
 ******************************************************************************/
 
-#include "util.h"
+#include "util_hack.h"
 #include "mtrInt.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -162,27 +162,27 @@ Mtr_MakeGroup(
   unsigned int  flags /* flags for the new group */)
 {
     MtrNode *node,
-        *first,
-        *last,
-        *previous,
-        *newn;
+            *first,
+            *last,
+            *previous,
+            *newn;
 
     /* Sanity check. */
     if (size == 0)
-    return(NULL);
+        return(NULL);
 
     /* Check whether current group includes new group.  This check is
     ** necessary at the top-level call.  In the subsequent calls it is
     ** redundant. */
     if (low < (unsigned int) root->low ||
-    low + size > (unsigned int) (root->low + root->size))
-    return(NULL);
+        low + size > (unsigned int) (root->low + root->size))
+        return(NULL);
 
     /* Trying to create an existing group has the effect of updating
     ** the flags. */
     if (root->size == size && root->low == low) {
-    root->flags = flags;
-    return(root);
+        root->flags = flags;
+        return(root);
     }
 
     /* At this point we know that the new group is properly contained
@@ -191,15 +191,15 @@ Mtr_MakeGroup(
 
     /* Root has no children: create a new group. */
     if (root->child == NULL) {
-    newn = Mtr_AllocNode();
-    if (newn == NULL) return(NULL);    /* out of memory */
-    newn->low = low;
-    newn->size = size;
-    newn->flags = flags;
-    newn->parent = root;
-    newn->elder = newn->younger = newn->child = NULL;
-    root->child = newn;
-    return(newn);
+        newn = Mtr_AllocNode();
+        if (newn == NULL) return(NULL); /* out of memory */
+        newn->low = low;
+        newn->size = size;
+        newn->flags = flags;
+        newn->parent = root;
+        newn->elder = newn->younger = newn->child = NULL;
+        root->child = newn;
+        return(newn);
     }
 
     /* Root has children: Find all chidren of root that are included
@@ -208,58 +208,58 @@ Mtr_MakeGroup(
     previous = NULL;
     first = root->child; /* guaranteed to be non-NULL */
     while (first != NULL && low >= (unsigned int) (first->low + first->size)) {
-    previous = first;
-    first = first->younger;
+        previous = first;
+        first = first->younger;
     }
     if (first == NULL) {
-    /* We have scanned the entire list and we need to append a new
-    ** child at the end of it.  Previous points to the last child
-    ** of root. */
-    newn = Mtr_AllocNode();
-    if (newn == NULL) return(NULL);    /* out of memory */
-    newn->low = low;
-    newn->size = size;
-    newn->flags = flags;
-    newn->parent = root;
-    newn->elder = previous;
-    previous->younger = newn;
-    newn->younger = newn->child = NULL;
-    return(newn);
+        /* We have scanned the entire list and we need to append a new
+        ** child at the end of it.  Previous points to the last child
+        ** of root. */
+        newn = Mtr_AllocNode();
+        if (newn == NULL) return(NULL); /* out of memory */
+        newn->low = low;
+        newn->size = size;
+        newn->flags = flags;
+        newn->parent = root;
+        newn->elder = previous;
+        previous->younger = newn;
+        newn->younger = newn->child = NULL;
+        return(newn);
     }
     /* Here first is non-NULL and low < first->low + first->size. */
     if (low >= (unsigned int) first->low &&
-    low + size <= (unsigned int) (first->low + first->size)) {
-    /* The new group is contained in the group of first. */
-    newn = Mtr_MakeGroup(first, low, size, flags);
-    return(newn);
+        low + size <= (unsigned int) (first->low + first->size)) {
+        /* The new group is contained in the group of first. */
+        newn = Mtr_MakeGroup(first, low, size, flags);
+        return(newn);
     } else if (low + size <= first->low) {
-    /* The new group is entirely contained in the gap between
-    ** previous and first. */
-    newn = Mtr_AllocNode();
-    if (newn == NULL) return(NULL);    /* out of memory */
-    newn->low = low;
-    newn->size = size;
-    newn->flags = flags;
-    newn->child = NULL;
-    newn->parent = root;
-    newn->elder = previous;
-    newn->younger = first;
-    first->elder = newn;
-    if (previous != NULL) {
-        previous->younger = newn;
-    } else {
-        root->child = newn;
-    }
-    return(newn);
+        /* The new group is entirely contained in the gap between
+        ** previous and first. */
+        newn = Mtr_AllocNode();
+        if (newn == NULL) return(NULL); /* out of memory */
+        newn->low = low;
+        newn->size = size;
+        newn->flags = flags;
+        newn->child = NULL;
+        newn->parent = root;
+        newn->elder = previous;
+        newn->younger = first;
+        first->elder = newn;
+        if (previous != NULL) {
+            previous->younger = newn;
+        } else {
+            root->child = newn;
+        }
+        return(newn);
     } else if (low < (unsigned int) first->low &&
-           low + size < (unsigned int) (first->low + first->size)) {
-    /* Trying to cut an existing group: not allowed. */
-    return(NULL);
+               low + size < (unsigned int) (first->low + first->size)) {
+        /* Trying to cut an existing group: not allowed. */
+        return(NULL);
     } else if (low > first->low) {
-    /* The new group neither is contained in the group of first
-    ** (this was tested above) nor contains it. It is therefore
-    ** trying to cut an existing group: not allowed. */
-    return(NULL);
+        /* The new group neither is contained in the group of first
+        ** (this was tested above) nor contains it. It is therefore
+        ** trying to cut an existing group: not allowed. */
+        return(NULL);
     }
 
     /* First holds the pointer to the first child contained in the new
@@ -267,40 +267,40 @@ Mtr_MakeGroup(
     ** first->size.  One of the two inequalities is strict. */
     last = first->younger;
     while (last != NULL &&
-       (unsigned int) (last->low + last->size) < low + size) {
-    last = last->younger;
-    }
-    if (last == NULL) {
-    /* All the chilren of root from first onward become children
-    ** of the new group. */
-    newn = Mtr_AllocNode();
-    if (newn == NULL) return(NULL);    /* out of memory */
-    newn->low = low;
-    newn->size = size;
-    newn->flags = flags;
-    newn->child = first;
-    newn->parent = root;
-    newn->elder = previous;
-    newn->younger = NULL;
-    first->elder = NULL;
-    if (previous != NULL) {
-        previous->younger = newn;
-    } else {
-        root->child = newn;
-    }
-    last = first;
-    while (last != NULL) {
-        last->parent = newn;
+           (unsigned int) (last->low + last->size) < low + size) {
         last = last->younger;
     }
-    return(newn);
+    if (last == NULL) {
+        /* All the chilren of root from first onward become children
+        ** of the new group. */
+        newn = Mtr_AllocNode();
+        if (newn == NULL) return(NULL); /* out of memory */
+        newn->low = low;
+        newn->size = size;
+        newn->flags = flags;
+        newn->child = first;
+        newn->parent = root;
+        newn->elder = previous;
+        newn->younger = NULL;
+        first->elder = NULL;
+        if (previous != NULL) {
+            previous->younger = newn;
+        } else {
+            root->child = newn;
+        }
+        last = first;
+        while (last != NULL) {
+            last->parent = newn;
+            last = last->younger;
+        }
+        return(newn);
     }
 
     /* Here last != NULL and low + size <= last->low + last->size. */
     if (low + size - 1 >= (unsigned int) last->low &&
-    low + size < (unsigned int) (last->low + last->size)) {
-    /* Trying to cut an existing group: not allowed. */
-    return(NULL);
+        low + size < (unsigned int) (last->low + last->size)) {
+        /* Trying to cut an existing group: not allowed. */
+        return(NULL);
     }
 
     /* First and last point to the first and last of the children of
@@ -310,26 +310,26 @@ Mtr_MakeGroup(
     ** preceeding first. If it is NULL, then first is the first child
     ** of root. */
     newn = Mtr_AllocNode();
-    if (newn == NULL) return(NULL);    /* out of memory */
+    if (newn == NULL) return(NULL);     /* out of memory */
     newn->low = low;
     newn->size = size;
     newn->flags = flags;
     newn->child = first;
     newn->parent = root;
     if (previous == NULL) {
-    root->child = newn;
+        root->child = newn;
     } else {
-    previous->younger = newn;
+        previous->younger = newn;
     }
     newn->elder = previous;
     newn->younger = last->younger;
     if (last->younger != NULL) {
-    last->younger->elder = newn;
+        last->younger->elder = newn;
     }
     last->younger = NULL;
     first->elder = NULL;
     for (node = first; node != NULL; node = node->younger) {
-    node->parent = newn;
+        node->parent = newn;
     }
 
     return(newn);
@@ -368,20 +368,20 @@ Mtr_DissolveGroup(
     /* Make all children of group children of its parent, and make
     ** last point to the last child of group. */
     for (last = group->child; last->younger != NULL; last = last->younger) {
-    last->parent = parent;
+        last->parent = parent;
     }
     last->parent = parent;
 
     last->younger = group->younger;
     if (group->younger != NULL) {
-    group->younger->elder = last;
+        group->younger->elder = last;
     }
 
     group->child->elder = group->elder;
     if (group == parent->child) {
-    parent->child = group->child;
+        parent->child = group->child;
     } else {
-    group->elder->younger = group->child;
+        group->elder->younger = group->child;
     }
 
     Mtr_DeallocNode(group);
@@ -425,28 +425,28 @@ Mtr_FindGroup(
     ** check is necessary at the top-level call.  In the subsequent
     ** calls it is redundant. */
     if (low < (unsigned int) root->low ||
-    low + size > (unsigned int) (root->low + root->size))
-    return(NULL);
+        low + size > (unsigned int) (root->low + root->size))
+        return(NULL);
 
     if (root->size == size && root->low == low)
-    return(root);
+        return(root);
 
     if (root->child == NULL)
-    return(NULL);
+        return(NULL);
 
     /* Find all chidren of root that are included in the new group. If
     ** the group of any child entirely contains the new group, call
     ** Mtr_MakeGroup recursively.  */
     node = root->child;
     while (low >= (unsigned int) (node->low + node->size)) {
-    node = node->younger;
+        node = node->younger;
     }
     if (low + size <= (unsigned int) (node->low + node->size)) {
-    /* The group is contained in the group of node. */
-    node = Mtr_FindGroup(node, low, size);
-    return(node);
+        /* The group is contained in the group of node. */
+        node = Mtr_FindGroup(node, low, size);
+        return(node);
     } else {
-    return(NULL);
+        return(NULL);
     }
 
 } /* end of Mtr_FindGroup */
@@ -477,11 +477,11 @@ Mtr_SwapGroups(
     int sizeSecond;
 
     if (second->younger == first) { /* make first first */
-    node = first;
-    first = second;
-    second = node;
+        node = first;
+        first = second;
+        second = node;
     } else if (first->younger != second) { /* non-adjacent */
-    return(0);
+        return(0);
     }
 
     sizeFirst = first->size;
@@ -491,12 +491,12 @@ Mtr_SwapGroups(
     parent = first->parent;
     if (parent == NULL || second->parent != parent) return(0);
     if (parent->child == first) {
-    parent->child = second;
+        parent->child = second;
     } else { /* first->elder != NULL */
-    first->elder->younger = second;
+        first->elder->younger = second;
     }
     if (second->younger != NULL) {
-    second->younger->elder = first;
+        second->younger->elder = first;
     }
     first->younger = second->younger;
     second->elder = first->elder;
@@ -549,30 +549,30 @@ Mtr_PrintGroups(
     if (!silent) (void) printf("(%hu",root->low);
 #endif
     if (MTR_TEST(root,MTR_TERMINAL) || root->child == NULL) {
-    if (!silent) (void) printf(",");
+        if (!silent) (void) printf(",");
     } else {
-    node = root->child;
-    while (node != NULL) {
-        assert(node->low >= root->low && (int) (node->low + node->size) <= (int) (root->low + root->size));
-        assert(node->parent == root);
-        Mtr_PrintGroups(node,silent);
-        node = node->younger;
-    }
+        node = root->child;
+        while (node != NULL) {
+            assert(node->low >= root->low && (int) (node->low + node->size) <= (int) (root->low + root->size));
+            assert(node->parent == root);
+            Mtr_PrintGroups(node,silent);
+            node = node->younger;
+        }
     }
     if (!silent) {
 #if SIZEOF_VOID_P == 8
-    (void) printf("%u", root->low + root->size - 1);
+        (void) printf("%u", root->low + root->size - 1);
 #else
-    (void) printf("%hu", root->low + root->size - 1);
+        (void) printf("%hu", root->low + root->size - 1);
 #endif
-    if (root->flags != MTR_DEFAULT) {
-        (void) printf("|");
-        if (MTR_TEST(root,MTR_FIXED)) (void) printf("F");
-        if (MTR_TEST(root,MTR_NEWNODE)) (void) printf("N");
-        if (MTR_TEST(root,MTR_SOFT)) (void) printf("S");
-    }
-    (void) printf(")");
-    if (root->parent == NULL) (void) printf("\n");
+        if (root->flags != MTR_DEFAULT) {
+            (void) printf("|");
+            if (MTR_TEST(root,MTR_FIXED)) (void) printf("F");
+            if (MTR_TEST(root,MTR_NEWNODE)) (void) printf("N");
+            if (MTR_TEST(root,MTR_SOFT)) (void) printf("S");
+        }
+        (void) printf(")");
+        if (root->parent == NULL) (void) printf("\n");
     }
     assert((root->flags &~(MTR_TERMINAL | MTR_SOFT | MTR_FIXED | MTR_NEWNODE)) == 0);
     return;
@@ -625,53 +625,53 @@ Mtr_ReadGroups(
     if (root == NULL) return NULL;
 
     while (! feof(fp)) {
-    /* Read a triple and check for consistency. */
-    err = fscanf(fp, "%d %d %s", &low, &size, attrib);
-    if (err == EOF) {
-        break;
-    } else if (err != 3) {
-        Mtr_FreeTree(root);
-        return(NULL);
-    } else if (low < 0 || low+size > nleaves || size < 1) {
-        Mtr_FreeTree(root);
-        return(NULL);
-    } else if (strlen(attrib) > 8 * sizeof(MtrHalfWord)) {
-        /* Not enough bits in the flags word to store these many
-        ** attributes. */
-        Mtr_FreeTree(root);
-        return(NULL);
-    }
+        /* Read a triple and check for consistency. */
+        err = fscanf(fp, "%d %d %s", &low, &size, attrib);
+        if (err == EOF) {
+            break;
+        } else if (err != 3) {
+            Mtr_FreeTree(root);
+            return(NULL);
+        } else if (low < 0 || low+size > nleaves || size < 1) {
+            Mtr_FreeTree(root);
+            return(NULL);
+        } else if (strlen(attrib) > 8 * sizeof(MtrHalfWord)) {
+            /* Not enough bits in the flags word to store these many
+            ** attributes. */
+            Mtr_FreeTree(root);
+            return(NULL);
+        }
 
-    /* Parse the flag string. Currently all flags are permitted,
-    ** to make debugging easier. Normally, specifying NEWNODE
-    ** wouldn't be allowed. */
-    flags = MTR_DEFAULT;
-    for (c=attrib; *c != 0; c++) {
-        switch (*c) {
-        case 'D':
-        break;
-        case 'F':
-        flags |= MTR_FIXED;
-        break;
-        case 'N':
-        flags |= MTR_NEWNODE;
-        break;
-        case 'S':
-        flags |= MTR_SOFT;
-        break;
-        case 'T':
-        flags |= MTR_TERMINAL;
-        break;
-        default:
-        return NULL;
+        /* Parse the flag string. Currently all flags are permitted,
+        ** to make debugging easier. Normally, specifying NEWNODE
+        ** wouldn't be allowed. */
+        flags = MTR_DEFAULT;
+        for (c=attrib; *c != 0; c++) {
+            switch (*c) {
+            case 'D':
+                break;
+            case 'F':
+                flags |= MTR_FIXED;
+                break;
+            case 'N':
+                flags |= MTR_NEWNODE;
+                break;
+            case 'S':
+                flags |= MTR_SOFT;
+                break;
+            case 'T':
+                flags |= MTR_TERMINAL;
+                break;
+            default:
+                return NULL;
+            }
+        }
+        node = Mtr_MakeGroup(root, (MtrHalfWord) low, (MtrHalfWord) size,
+                             flags);
+        if (node == NULL) {
+            Mtr_FreeTree(root);
+            return(NULL);
         }
-    }
-    node = Mtr_MakeGroup(root, (MtrHalfWord) low, (MtrHalfWord) size,
-                 flags);
-    if (node == NULL) {
-        Mtr_FreeTree(root);
-        return(NULL);
-    }
     }
 
     return(root);
@@ -720,11 +720,11 @@ mtrShiftHL(
     node->low = (MtrHalfWord) low;
 
     if (!MTR_TEST(node,MTR_TERMINAL) && node->child != NULL) {
-    auxnode = node->child;
-    do {
-        if (!mtrShiftHL(auxnode,shift)) return(0);
-        auxnode = auxnode->younger;
-    } while (auxnode != NULL);
+        auxnode = node->child;
+        do {
+            if (!mtrShiftHL(auxnode,shift)) return(0);
+            auxnode = auxnode->younger;
+        } while (auxnode != NULL);
     }
 
     return(1);