Version abc70930

5 files changed, 0 insertions, 1356 deletions

diff --git a/src/bdd/mtr/module.make b/src/bdd/mtr/module.make
deleted file mode 100644
index d7fa63d9..00000000
--- a/src/bdd/mtr/module.make
+++ /dev/null
@@ -1,2 +0,0 @@
-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
deleted file mode 100644
index 201329ae..00000000
--- a/src/bdd/mtr/mtr.h
+++ /dev/null
@@ -1,173 +0,0 @@
-/**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
deleted file mode 100644
index 94105282..00000000
--- a/src/bdd/mtr/mtrBasic.c
+++ /dev/null
@@ -1,426 +0,0 @@
-/**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
deleted file mode 100644
index 363b776b..00000000
--- a/src/bdd/mtr/mtrGroup.c
+++ /dev/null
@@ -1,690 +0,0 @@
-/**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
deleted file mode 100644
index a8d5aa6c..00000000
--- a/src/bdd/mtr/mtrInt.h
+++ /dev/null
@@ -1,65 +0,0 @@
-/**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 */