Version abc71001

5 files changed, 1356 insertions, 0 deletions

diff --git a/src/bdd/mtr/module.make b/src/bdd/mtr/module.make
new file mode 100644
index 00000000..d7fa63d9
--- /dev/null
+++ b/src/bdd/mtr/module.make
@@ -0,0 +1,2 @@
+SRC +=  src/bdd/mtr/mtrBasic.c \
+    src/bdd/mtr/mtrGroup.c
diff --git a/src/bdd/mtr/mtr.h b/src/bdd/mtr/mtr.h
new file mode 100644
index 00000000..201329ae
--- /dev/null
+++ b/src/bdd/mtr/mtr.h
@@ -0,0 +1,173 @@
+/**CHeaderFile*****************************************************************
+
+  FileName    [mtr.h]
+
+  PackageName [mtr]
+
+  Synopsis    [Multiway-branch tree manipulation]
+
+  Description [This package provides two layers of functions. Functions
+  of the lower level manipulate multiway-branch trees, implemented
+  according to the classical scheme whereby each node points to its
+  first child and its previous and next siblings. These functions are
+  collected in mtrBasic.c.<p>
+  Functions of the upper layer deal with group trees, that is the trees
+  used by group sifting to represent the grouping of variables. These
+  functions are collected in mtrGroup.c.]
+
+  SeeAlso     [The CUDD package documentation; specifically on group
+  sifting.]
+
+  Author      [Fabio Somenzi]
+
+  Copyright   [This file was created at the University of Colorado at
+  Boulder.  The University of Colorado at Boulder makes no warranty
+  about the suitability of this software for any purpose.  It is
+  presented on an AS IS basis.]
+
+  Revision    [$Id: mtr.h,v 1.1.1.1 2003/02/24 22:24:02 wjiang Exp $]
+
+******************************************************************************/
+
+#ifndef __MTR
+#define __MTR
+
+/*---------------------------------------------------------------------------*/
+/* Nested includes                                                           */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+#ifndef SIZEOF_VOID_P
+#define SIZEOF_VOID_P 4
+#endif
+#ifndef SIZEOF_INT
+#define SIZEOF_INT 4
+#endif
+
+#undef CONST
+#if defined(__STDC__) || defined(__cplusplus)
+#define CONST           const
+#else /* !(__STDC__ || __cplusplus) */
+#define CONST
+#endif /* !(__STDC__ || __cplusplus) */
+
+/* These are potential duplicates. */
+#ifndef EXTERN
+#   ifdef __cplusplus
+#    define EXTERN extern "C"
+#   else
+#    define EXTERN extern
+#   endif
+#endif
+#ifndef ARGS
+#   if defined(__STDC__) || defined(__cplusplus)
+#    define ARGS(protos)    protos          /* ANSI C */
+#   else /* !(__STDC__ || __cplusplus) */
+#    define ARGS(protos)    ()              /* K&R C */
+#   endif /* !(__STDC__ || __cplusplus) */
+#endif
+
+#if defined(__GNUC__)
+#define MTR_INLINE __inline__
+# if (__GNUC__ >2 || __GNUC_MINOR__ >=7)
+#   define MTR_UNUSED __attribute__ ((unused))
+# else
+#   define MTR_UNUSED
+# endif
+#else
+#define MTR_INLINE
+#define MTR_UNUSED
+#endif
+ 
+/* Flag definitions */
+#define MTR_DEFAULT    0x00000000
+#define MTR_TERMINAL     0x00000001
+#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)
+#else
+#define MTR_MAXHIGH    ((MtrHalfWord) ~0)
+#endif
+
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
+typedef unsigned int   MtrHalfWord;
+#else
+typedef unsigned short MtrHalfWord;
+#endif
+
+typedef struct MtrNode {
+    MtrHalfWord flags;
+    MtrHalfWord low;
+    MtrHalfWord size;
+    MtrHalfWord index;
+    struct MtrNode *parent;
+    struct MtrNode *child;
+    struct MtrNode *elder;
+    struct MtrNode *younger;
+} MtrNode;
+
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+/* Flag manipulation macros */
+#define MTR_SET(node, flag)        (node->flags |= (flag))
+#define MTR_RESET(node, flag)    (node->flags &= ~ (flag))
+#define MTR_TEST(node, flag)    (node->flags & (flag))
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Function prototypes                                                       */
+/*---------------------------------------------------------------------------*/
+
+EXTERN MtrNode * Mtr_AllocNode ARGS(());
+EXTERN void Mtr_DeallocNode ARGS((MtrNode *node));
+EXTERN MtrNode * Mtr_InitTree ARGS(());
+EXTERN void Mtr_FreeTree ARGS((MtrNode *node));
+EXTERN MtrNode * Mtr_CopyTree ARGS((MtrNode *node, int expansion));
+EXTERN void Mtr_MakeFirstChild ARGS((MtrNode *parent, MtrNode *child));
+EXTERN void Mtr_MakeLastChild ARGS((MtrNode *parent, MtrNode *child));
+EXTERN MtrNode * Mtr_CreateFirstChild ARGS((MtrNode *parent));
+EXTERN MtrNode * Mtr_CreateLastChild ARGS((MtrNode *parent));
+EXTERN void Mtr_MakeNextSibling ARGS((MtrNode *first, MtrNode *second));
+EXTERN void Mtr_PrintTree ARGS((MtrNode *node));
+EXTERN MtrNode * Mtr_InitGroupTree ARGS((int lower, int size));
+EXTERN MtrNode * Mtr_MakeGroup ARGS((MtrNode *root, unsigned int low, unsigned int high, unsigned int flags));
+EXTERN MtrNode * Mtr_DissolveGroup ARGS((MtrNode *group));
+EXTERN MtrNode * Mtr_FindGroup ARGS((MtrNode *root, unsigned int low, unsigned int high));
+EXTERN int Mtr_SwapGroups ARGS((MtrNode *first, MtrNode *second));
+EXTERN void Mtr_PrintGroups ARGS((MtrNode *root, int silent));
+EXTERN MtrNode * Mtr_ReadGroups ARGS((FILE *fp, int nleaves));
+
+/**AutomaticEnd***************************************************************/
+
+#endif /* __MTR */
diff --git a/src/bdd/mtr/mtrBasic.c b/src/bdd/mtr/mtrBasic.c
new file mode 100644
index 00000000..94105282
--- /dev/null
+++ b/src/bdd/mtr/mtrBasic.c
@@ -0,0 +1,426 @@
+/**CFile***********************************************************************
+
+  FileName    [mtrBasic.c]
+
+  PackageName [mtr]
+
+  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>
+        ]
+
+  SeeAlso     [cudd package]
+
+  Author      [Fabio Somenzi]
+
+  Copyright   [This file was created at the University of Colorado at
+  Boulder.  The University of Colorado at Boulder makes no warranty
+  about the suitability of this software for any purpose.  It is
+  presented on an AS IS basis.]
+
+******************************************************************************/
+
+#include "util_hack.h"
+#include "mtrInt.h"
+
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+#ifndef lint
+static char rcsid[] MTR_UNUSED = "$Id: mtrBasic.c,v 1.1.1.1 2003/02/24 22:24:02 wjiang Exp $";
+#endif
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    [Allocates new tree node.]
+
+  Description [Allocates new tree node. Returns pointer to node.]
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_DeallocNode]
+
+******************************************************************************/
+MtrNode *
+Mtr_AllocNode(
+   )
+{
+    MtrNode *node;
+
+    node = ALLOC(MtrNode,1);
+    return node;
+
+} /* Mtr_AllocNode */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Deallocates tree node.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_AllocNode]
+
+******************************************************************************/
+void
+Mtr_DeallocNode(
+  MtrNode * node /* node to be deallocated */)
+{
+    FREE(node);
+    return;
+
+} /* end of Mtr_DeallocNode */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Initializes tree with one node.]
+
+  Description [Initializes tree with one node. Returns pointer to node.]
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_FreeTree Mtr_InitGroupTree]
+
+******************************************************************************/
+MtrNode *
+Mtr_InitTree(
+   )
+{
+    MtrNode *node;
+
+    node = Mtr_AllocNode();
+    if (node == NULL) return(NULL);
+
+    node->parent = node->child = node->elder = node->younger = NULL;
+    node->flags = 0;
+
+    return(node);
+
+} /* end of Mtr_InitTree */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Disposes of tree rooted at node.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_InitTree]
+
+******************************************************************************/
+void
+Mtr_FreeTree(
+  MtrNode * node)
+{
+    if (node == NULL) return;
+    if (! MTR_TEST(node,MTR_TERMINAL)) Mtr_FreeTree(node->child);
+    Mtr_FreeTree(node->younger);
+    Mtr_DeallocNode(node);
+    return;
+
+} /* end of Mtr_FreeTree */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Makes a copy of tree.]
+
+  Description [Makes a copy of tree. If parameter expansion is greater
+  than 1, it will expand the tree by that factor. It is an error for
+  expansion to be less than 1. Returns a pointer to the copy if
+  successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_InitTree]
+
+******************************************************************************/
+MtrNode *
+Mtr_CopyTree(
+  MtrNode * node,
+  int  expansion)
+{
+    MtrNode *copy;
+
+    if (node == NULL) return(NULL);
+    if (expansion < 1) return(NULL);
+    copy = Mtr_AllocNode();
+    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);
+    }
+    }
+    if (node->younger != 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;
+    copy->size = node->size * expansion;
+    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;
+    }
+    }
+    return(copy);
+    
+} /* end of Mtr_CopyTree */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Makes child the first child of parent.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_MakeLastChild Mtr_CreateFirstChild]
+
+******************************************************************************/
+void
+Mtr_MakeFirstChild(
+  MtrNode * parent,
+  MtrNode * child)
+{
+    child->parent = parent;
+    child->younger = parent->child;
+    child->elder = NULL;
+    if (parent->child != NULL) {
+#ifdef MTR_DEBUG
+    assert(parent->child->elder == NULL);
+#endif
+    parent->child->elder = child;
+    }
+    parent->child = child;
+    return;
+
+} /* end of Mtr_MakeFirstChild */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Makes child the last child of parent.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_MakeFirstChild Mtr_CreateLastChild]
+
+******************************************************************************/
+void
+Mtr_MakeLastChild(
+  MtrNode * parent,
+  MtrNode * child)
+{
+    MtrNode *node;
+
+    child->younger = NULL;
+
+    if (parent->child == NULL) {
+    parent->child = child;
+    child->elder = NULL;
+    } else {
+    for (node = parent->child;
+         node->younger != NULL;
+         node = node->younger);
+    node->younger = child;
+    child->elder = node;
+    }
+    child->parent = parent;
+    return;
+
+} /* end of Mtr_MakeLastChild */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Creates a new node and makes it the first child of parent.]
+
+  Description [Creates a new node and makes it the first child of
+  parent. Returns pointer to new child.]
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_MakeFirstChild Mtr_CreateLastChild]
+
+******************************************************************************/
+MtrNode *
+Mtr_CreateFirstChild(
+  MtrNode * parent)
+{
+    MtrNode *child;
+
+    child = Mtr_AllocNode();
+    if (child == NULL) return(NULL);
+
+    child->child = child->younger = child-> elder = NULL;
+    child->flags = 0;
+    Mtr_MakeFirstChild(parent,child);
+    return(child);
+
+} /* end of Mtr_CreateFirstChild */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Creates a new node and makes it the last child of parent.]
+
+  Description [Creates a new node and makes it the last child of parent.
+  Returns pointer to new child.]
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_MakeLastChild Mtr_CreateFirstChild]
+
+******************************************************************************/
+MtrNode *
+Mtr_CreateLastChild(
+  MtrNode * parent)
+{
+    MtrNode *child;
+
+    child = Mtr_AllocNode();
+    if (child == NULL) return(NULL);
+
+    child->child = child->younger = child->elder = NULL;
+    child->flags = 0;
+    Mtr_MakeLastChild(parent,child);
+    return(child);
+
+} /* end of Mtr_CreateLastChild */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Makes second the next sibling of first.]
+
+  Description [Makes second the next sibling of first. Second becomes a
+  child of the parent of first.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+void
+Mtr_MakeNextSibling(
+  MtrNode * first,
+  MtrNode * second)
+{
+    second->younger = first->younger;
+    if (first->younger != NULL) {
+    first->younger->elder = second;
+    }
+    second->parent = first->parent;
+    first->younger = second;
+    second->elder = first;
+    return;
+
+} /* end of Mtr_MakeNextSibling */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Prints a tree, one node per line.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_PrintGroups]
+
+******************************************************************************/
+void
+Mtr_PrintTree(
+  MtrNode * node)
+{
+    if (node == NULL) return;
+    (void) fprintf(stdout,
+#if SIZEOF_VOID_P == 8
+    "N=0x%-8lx C=0x%-8lx Y=0x%-8lx E=0x%-8lx P=0x%-8lx F=%x L=%d S=%d\n",
+    (unsigned long) node, (unsigned long) node->child,
+    (unsigned long) node->younger, (unsigned long) node->elder,
+    (unsigned long) node->parent, node->flags, node->low, node->size);
+#else
+    "N=0x%-8x C=0x%-8x Y=0x%-8x E=0x%-8x P=0x%-8x F=%x L=%d S=%d\n",
+    (unsigned) node, (unsigned) node->child,
+    (unsigned) node->younger, (unsigned) node->elder,
+    (unsigned) node->parent, node->flags, node->low, node->size);
+#endif
+    if (!MTR_TEST(node,MTR_TERMINAL)) Mtr_PrintTree(node->child);
+    Mtr_PrintTree(node->younger);
+    return;
+
+} /* end of Mtr_PrintTree */
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions                                            */
+/*---------------------------------------------------------------------------*/
+
diff --git a/src/bdd/mtr/mtrGroup.c b/src/bdd/mtr/mtrGroup.c
new file mode 100644
index 00000000..363b776b
--- /dev/null
+++ b/src/bdd/mtr/mtrGroup.c
@@ -0,0 +1,690 @@
+/**CFile***********************************************************************
+
+  FileName    [mtrGroup.c]
+
+  PackageName [mtr]
+
+  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>
+        ]
+
+  SeeAlso     [cudd package]
+
+  Author      [Fabio Somenzi]
+
+  Copyright   [This file was created at the University of Colorado at
+  Boulder.  The University of Colorado at Boulder makes no warranty
+  about the suitability of this software for any purpose.  It is
+  presented on an AS IS basis.]
+
+******************************************************************************/
+
+#include "util_hack.h"
+#include "mtrInt.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+#ifndef lint
+static char rcsid[] MTR_UNUSED = "$Id: mtrGroup.c,v 1.1.1.1 2003/02/24 22:24:02 wjiang Exp $";
+#endif
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+static int mtrShiftHL ARGS((MtrNode *node, int shift));
+
+/**AutomaticEnd***************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+  Synopsis    [Allocate new tree.]
+
+  Description [Allocate new tree with one node, whose low and size
+  fields are specified by the lower and size parameters.
+  Returns pointer to tree root.]
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_InitTree Mtr_FreeTree]
+
+******************************************************************************/
+MtrNode *
+Mtr_InitGroupTree(
+  int  lower,
+  int  size)
+{
+    MtrNode *root;
+
+    root = Mtr_InitTree();
+    if (root == NULL) return(NULL);
+    root->flags = MTR_DEFAULT;
+    root->low = lower;
+    root->size = size;
+    return(root);
+
+} /* end of Mtr_InitGroupTree */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Makes a new group with size leaves starting at low.]
+
+  Description [Makes a new group with size leaves starting at low.
+  If the new group intersects an existing group, it must
+  either contain it or be contained by it.  This procedure relies on
+  the low and size fields of each node. It also assumes that the
+  children of each node are sorted in order of increasing low.  In
+  case of a valid request, the flags of the new group are set to the
+  value passed in `flags.' This can also be used to change the flags
+  of an existing group.  Returns the pointer to the root of the new
+  group upon successful termination; NULL otherwise. If the group
+  already exists, the pointer to its root is returned.]
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_DissolveGroup Mtr_ReadGroups Mtr_FindGroup]
+
+******************************************************************************/
+MtrNode *
+Mtr_MakeGroup(
+  MtrNode * root /* root of the group tree */,
+  unsigned int  low /* lower bound of the group */,
+  unsigned int  size /* upper bound of the group */,
+  unsigned int  flags /* flags for the new group */)
+{
+    MtrNode *node,
+        *first,
+        *last,
+        *previous,
+        *newn;
+
+    /* Sanity check. */
+    if (size == 0)
+    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);
+
+    /* 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);
+    }
+
+    /* At this point we know that the new group is properly contained
+    ** in the group of root. We have two possible cases here: - root
+    ** is a terminal node; - root has children. */
+
+    /* 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);
+    }
+
+    /* Root has children: 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. */
+    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;
+    }
+    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);
+    }
+    /* 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);
+    } 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);
+    } 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);
+    } 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);
+    }
+
+    /* First holds the pointer to the first child contained in the new
+    ** group. Here low <= first->low and low + size >= first->low +
+    ** 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;
+        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);
+    }
+
+    /* First and last point to the first and last of the children of
+    ** root that are included in the new group. Allocate a new node
+    ** and make all children of root between first and last chidren of
+    ** the new node.  Previous points to the child of root immediately
+    ** 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 */
+    newn->low = low;
+    newn->size = size;
+    newn->flags = flags;
+    newn->child = first;
+    newn->parent = root;
+    if (previous == NULL) {
+    root->child = newn;
+    } else {
+    previous->younger = newn;
+    }
+    newn->elder = previous;
+    newn->younger = last->younger;
+    if (last->younger != NULL) {
+    last->younger->elder = newn;
+    }
+    last->younger = NULL;
+    first->elder = NULL;
+    for (node = first; node != NULL; node = node->younger) {
+    node->parent = newn;
+    }
+
+    return(newn);
+
+} /* end of Mtr_MakeGroup */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Merges the children of `group' with the children of its
+  parent.]
+
+  Description [Merges the children of `group' with the children of its
+  parent. Disposes of the node pointed by group. If group is the
+  root of the group tree, this procedure leaves the tree unchanged.
+  Returns the pointer to the parent of `group' upon successful
+  termination; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_MakeGroup]
+
+******************************************************************************/
+MtrNode *
+Mtr_DissolveGroup(
+  MtrNode * group /* group to be dissolved */)
+{
+    MtrNode *parent;
+    MtrNode *last;
+
+    parent = group->parent;
+
+    if (parent == NULL) return(NULL);
+    if (MTR_TEST(group,MTR_TERMINAL) || group->child == NULL) return(NULL);
+
+    /* 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->younger = group->younger;
+    if (group->younger != NULL) {
+    group->younger->elder = last;
+    }
+
+    group->child->elder = group->elder;
+    if (group == parent->child) {
+    parent->child = group->child;
+    } else {
+    group->elder->younger = group->child;
+    }
+
+    Mtr_DeallocNode(group);
+    return(parent);
+
+} /* end of Mtr_DissolveGroup */
+
+
+/**Function********************************************************************
+
+  Synopsis [Finds a group with size leaves starting at low, if it exists.]
+
+  Description [Finds a group with size leaves starting at low, if it
+  exists.  This procedure relies on the low and size fields of each
+  node. It also assumes that the children of each node are sorted in
+  order of increasing low.  Returns the pointer to the root of the
+  group upon successful termination; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+MtrNode *
+Mtr_FindGroup(
+  MtrNode * root /* root of the group tree */,
+  unsigned int  low /* lower bound of the group */,
+  unsigned int  size /* upper bound of the group */)
+{
+    MtrNode *node;
+
+#ifdef MTR_DEBUG
+    /* We cannot have a non-empty proper subgroup of a singleton set. */
+    assert(!MTR_TEST(root,MTR_TERMINAL));
+#endif
+
+    /* Sanity check. */
+    if (size < 1) return(NULL);
+
+    /* Check whether current group includes the group sought.  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);
+
+    if (root->size == size && root->low == low)
+    return(root);
+
+    if (root->child == 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;
+    }
+    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);
+    } else {
+    return(NULL);
+    }
+
+} /* end of Mtr_FindGroup */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Swaps two children of a tree node.]
+
+  Description [Swaps two children of a tree node. Adjusts the high and
+  low fields of the two nodes and their descendants.  The two children
+  must be adjacent. However, first may be the younger sibling of second.
+  Returns 1 in case of success; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+int
+Mtr_SwapGroups(
+  MtrNode * first /* first node to be swapped */,
+  MtrNode * second /* second node to be swapped */)
+{
+    MtrNode *node;
+    MtrNode *parent;
+    int sizeFirst;
+    int sizeSecond;
+
+    if (second->younger == first) { /* make first first */
+    node = first;
+    first = second;
+    second = node;
+    } else if (first->younger != second) { /* non-adjacent */
+    return(0);
+    }
+
+    sizeFirst = first->size;
+    sizeSecond = second->size;
+
+    /* Swap the two nodes. */
+    parent = first->parent;
+    if (parent == NULL || second->parent != parent) return(0);
+    if (parent->child == first) {
+    parent->child = second;
+    } else { /* first->elder != NULL */
+    first->elder->younger = second;
+    }
+    if (second->younger != NULL) {
+    second->younger->elder = first;
+    }
+    first->younger = second->younger;
+    second->elder = first->elder;
+    first->elder = second;
+    second->younger = first;
+
+    /* Adjust the high and low fields. */
+    if (!mtrShiftHL(first,sizeSecond)) return(0);
+    if (!mtrShiftHL(second,-sizeFirst)) return(0);
+
+    return(1);
+
+} /* end of Mtr_SwapGroups */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Prints the groups as a parenthesized list.]
+
+  Description [Prints the groups as a parenthesized list. After each
+  group, the group's flag are printed, preceded by a `|'.  For each
+  flag (except MTR_TERMINAL) a character is printed.
+  <ul>
+  <li>F: MTR_FIXED
+  <li>N: MTR_NEWNODE
+  <li>S: MTR_SOFT
+  </ul>
+  The second argument, silent, if different from 0, causes
+  Mtr_PrintGroups to only check the syntax of the group tree.
+  ]
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_PrintTree]
+
+******************************************************************************/
+void
+Mtr_PrintGroups(
+  MtrNode * root /* root of the group tree */,
+  int  silent /* flag to check tree syntax only */)
+{
+    MtrNode *node;
+
+    assert(root != NULL);
+    assert(root->younger == NULL || root->younger->elder == root);
+    assert(root->elder == NULL || root->elder->younger == root);
+    if (!silent) (void) printf("(%d",root->low);
+    if (MTR_TEST(root,MTR_TERMINAL) || root->child == NULL) {
+    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;
+    }
+    }
+    if (!silent) {
+    (void) printf("%d", root->low + root->size - 1);
+    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;
+
+} /* end of Mtr_PrintGroups */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Reads groups from a file and creates a group tree.]
+
+  Description [Reads groups from a file and creates a group tree.
+  Each group is specified by three fields:
+  <xmp>
+       low size flags.
+  </xmp>
+  Low and size are (short) integers. Flags is a string composed of the
+  following characters (with associated translation):
+  <ul>
+  <li>D: MTR_DEFAULT
+  <li>F: MTR_FIXED
+  <li>N: MTR_NEWNODE
+  <li>S: MTR_SOFT
+  <li>T: MTR_TERMINAL
+  </ul>
+  Normally, the only flags that are needed are D and F.  Groups and
+  fields are separated by white space (spaces, tabs, and newlines).
+  Returns a pointer to the group tree if successful; NULL otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Mtr_InitGroupTree Mtr_MakeGroup]
+
+******************************************************************************/
+MtrNode *
+Mtr_ReadGroups(
+  FILE * fp /* file pointer */,
+  int  nleaves /* number of leaves of the new tree */)
+{
+    int low;
+    int size;
+    int err;
+    unsigned int flags;
+    MtrNode *root;
+    MtrNode *node;
+    char attrib[8*sizeof(unsigned int)+1];
+    char *c;
+
+    root = Mtr_InitGroupTree(0,nleaves);
+    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) {
+        return(NULL);
+    } else if (low < 0 || low+size > nleaves || size < 1) {
+        return(NULL);
+    } else if (strlen(attrib) > 8 * sizeof(MtrHalfWord)) {
+        /* Not enough bits in the flags word to store these many
+        ** attributes. */
+        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) return(NULL);
+    }
+
+    return(root);
+
+} /* end of Mtr_ReadGroups */
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions                                            */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+  Synopsis    [Adjusts the low fields of a node and its descendants.]
+
+  Description [Adjusts the low fields of a node and its
+  descendants. Adds shift to low of each node. Checks that no
+  out-of-bounds values result.  Returns 1 in case of success; 0
+  otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+static int
+mtrShiftHL(
+  MtrNode * node /* group tree node */,
+  int  shift /* amount by which low should be changed */)
+{
+    MtrNode *auxnode;
+    int low;
+
+    low = (int) node->low;
+
+
+    low += shift;
+
+    if (low < 0 || low + (int) (node->size - 1) > (int) MTR_MAXHIGH) return(0);
+
+    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);
+    }
+
+    return(1);
+
+} /* end of mtrShiftHL */
+
diff --git a/src/bdd/mtr/mtrInt.h b/src/bdd/mtr/mtrInt.h
new file mode 100644
index 00000000..a8d5aa6c
--- /dev/null
+++ b/src/bdd/mtr/mtrInt.h
@@ -0,0 +1,65 @@
+/**CHeaderFile*****************************************************************
+
+  FileName    [mtrInt.h]
+
+  PackageName [mtr]
+
+  Synopsis    [Internal data structures of the mtr package]
+
+  Description [In this package all definitions are external.]
+
+  SeeAlso     []
+
+  Author      [Fabio Somenzi]
+
+  Copyright [This file was created at the University of Colorado at
+  Boulder.  The University of Colorado at Boulder makes no warranty
+  about the suitability of this software for any purpose.  It is
+  presented on an AS IS basis.]
+
+  Revision    [$Id: mtrInt.h,v 1.1.1.1 2003/02/24 22:24:02 wjiang Exp $]
+
+******************************************************************************/
+
+#ifndef _MTRINT
+#define _MTRINT
+
+#include "mtr.h"
+
+/*---------------------------------------------------------------------------*/
+/* Nested includes                                                           */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Function prototypes                                                       */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticEnd***************************************************************/
+
+#endif /* _MTRINT */