src/synth/synthFactor.c

Go to the documentation of this file.

#include "synthInt.h"

static char rcsid[] UNUSED = "$Id: synthFactor.c,v 1.49 2005/04/23 14:37:51 jinh Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

typedef struct ml_size_list {
    int                 size;   /* the number of literals */
    char                *string; /* string of the size to put into st_table */
    struct ml_size_list *next;
} MlSizeList;

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

static  bdd_node        *(* ZddProductFunc)(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_product;
static  bdd_node        *(* ZddProductRecurFunc)(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_product_recur;
static  bdd_node        *(* ZddDivideFunc)(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_weak_div;
static  bdd_node        *(* ZddDivideRecurFunc)(bdd_manager *, bdd_node *, bdd_node *) = bdd_zdd_weak_div_recur;
static  bdd_node        *(* ZddDivisorFunc)(bdd_manager *, bdd_node *) = Synth_ZddQuickDivisor;
static  int             NumTree;
static  int             ResolveConflictMode = 0;
static  st_table        *HeadListTable, *TailListTable;
static  MlTree          *MlTreeHead;
static  MlSizeList      *MlSizeHead;

int             UseMtree = 1;
int             UseCommonDivisor = 1;
int             TryNodeSharing = 0;
int             Resubstitution = 1;
int             RemainderComplement = 0;
int             noMemoryFlag = 0;
int             VerifyTreeMode = 0;
                /*
                ** 0 : nothing
                ** 1 : incrementally
                ** 2 : recursively after each factorization
                ** 3 : 2 & dump blif file with bdds
                */

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static MlTree * ResolveConflictNode(bdd_manager *dd, st_table *table, MlTree *tree1, MlTree *tree2, int comp_flag, int verbosity);
static void DeleteMlTree(bdd_manager *dd, st_table *table, MlTree *kill_tree, MlTree *live_tree, int deref, int comp_flag);
static void UnlinkMlTree(MlTree *kill_tree);
static void DeleteMlSizeList(MlTree *tree);
static int InsertMlTable(st_table *table, bdd_node *node, MlTree *tree);
static bdd_node * MakeComplementOfZddCover(bdd_manager *dd, bdd_node *node, int verbosity);
static char * GetIntString(int v);
static void VerifyTreeList(void);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/



/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


bdd_node        *
(* SynthGetZddProductFunc(void))(bdd_manager *, bdd_node *, bdd_node *)
{
    return(ZddProductFunc);
}


bdd_node        *
(* SynthGetZddProductRecurFunc(void))(bdd_manager *, bdd_node *, bdd_node *)
{
    return(ZddProductRecurFunc);
}


bdd_node        *
(* SynthGetZddDivideFunc(void))(bdd_manager *, bdd_node *, bdd_node *)
{
    return(ZddDivideFunc);
}


bdd_node        *
(* SynthGetZddDivideRecurFunc(void))(bdd_manager *, bdd_node *, bdd_node *)
{
    return(ZddDivideRecurFunc);
}


bdd_node        *
(* SynthGetZddDivisorFunc(void))(bdd_manager *, bdd_node *)
{
    return(ZddDivisorFunc);
}


void
SynthSetZddDivisorFunc(int mode)
{
  if (mode == 0)
    ZddDivisorFunc = Synth_ZddQuickDivisor;
  else if (mode == 1)
    ZddDivisorFunc = Synth_ZddLeastDivisor;
  else if (mode == 2)
    ZddDivisorFunc = Synth_ZddMostDivisor;
  else
    ZddDivisorFunc = Synth_ZddLevelZeroDivisor;
}


void
SynthGetSpaceString(char *string,
                    int n,
                    int max)
{
  int   i;

  if (n >= max - 1)
    n = max - 2;

  for (i = 0; i < n; i++)
    string[i] = ' ';
  string[n] = '\0';
}


MlTree  *
SynthLookupMlTable(st_table *table,
                   bdd_manager *dd,
                   bdd_node *node,
                   int candidate,
                   int verbosity)
{
  MlTree        *tree, *m_tree;
  int           flag;

  flag = st_lookup(table, (char *)node, &tree);
  if (flag) {
    if (MlTree_Regular(tree)->candidate) {
      m_tree = MlTree_Regular(tree);
      if (candidate) {
        if (!SynthUseCandidate(table, dd, m_tree, verbosity)) {
          return(NULL);
        }
      }
    }
    if (candidate)
      SynthSetSharedFlag(dd, tree);
    return(tree);
  }

  return((MlTree *)NULL);
}


int
SynthUseCandidate(st_table *table,
                  bdd_manager *dd,
                  MlTree *m_tree,
                  int verbosity)
{
  MlTree        *parent, *c_tree, *tmp_tree;
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  int           ref;
  int           comp_flag;

  m_tree = MlTree_Regular(m_tree);
  if (!m_tree->r) {
    (void) fprintf(vis_stdout,
                   "** synth fatal: Internal error in synthesize_network.\n");
    (void) fprintf(vis_stdout,
                 "** synth fatal: Please report this bug to VIS developers.\n");
    return (0);
  }
  parent = m_tree->r;
  m_tree->r = (MlTree *)NULL;
  m_tree->candidate = 0;
  c_tree = SynthFindOrCreateMlTree(table, dd, zero, 1, 0, &ref, verbosity);
  if (!c_tree)
    return (0);
  if (MlTree_IsComplement(c_tree)) {
    c_tree = MlTree_Regular(c_tree);
    m_tree->r_comp = 1;
  }
  tmp_tree = c_tree;
  c_tree = SynthCheckAndMakeComplement(dd, table, c_tree,
                                       &comp_flag, verbosity);
  if (!c_tree)
    return (0);
  else if (c_tree != tmp_tree) {
    if (comp_flag)
        m_tree->r_comp = 1;
    ref = 1;
  }
  m_tree->r = c_tree;
  m_tree->r_ref = ref;
  parent->q = m_tree;
  parent->q_ref = 0;
  parent->q_comp = 0;
  c_tree = SynthFindOrCreateMlTree(table, dd, one, 1, 0, &ref, verbosity);
  if (!c_tree)
    return (0);
  if (MlTree_IsComplement(c_tree)) {
    c_tree = MlTree_Regular(c_tree);
    parent->d_comp = 1;
  } else
    parent->d_comp = 0;
  parent->d = c_tree;
  parent->d_ref = ref;
  m_tree->id = NumTree;
  NumTree++;
  if (verbosity > 1)
    (void)fprintf(vis_stdout, "** synth info: Used candidate %d.\n",
                  m_tree->id);
  if (VerifyTreeMode) {
    SynthVerifyTree(dd, parent, 0);
    SynthVerifyTree(dd, m_tree, 0);
    SynthVerifyMlTable(dd, table);
  }
  return(1);
}


MlTree  *
SynthFindOrCreateMlTree(st_table *table,
                        bdd_manager *dd,
                        bdd_node *f,
                        int leaf,
                        int candidate,
                        int *ref,
                        int verbosity)
{
  MlTree        *tree;
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);

  tree = SynthLookupMlTable(table, dd, f, 1, verbosity);
  if (tree) {
    if (MlTree_Regular(tree)->candidate) {
      if (!SynthUseCandidate(table, dd, tree, verbosity)) {
        return(NULL);
      }
      SynthSetSharedFlag(dd, tree);
    }
    *ref = 1;
    return(tree);
  } else if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
    return(NULL);

  tree = ALLOC(MlTree, 1);
  if (!tree) {
    noMemoryFlag = 1;
    return(NULL);
  }
  (void)memset((void *)tree, 0, sizeof(MlTree));
  tree->node = f;
  bdd_ref(f);
  tree->leaf = leaf;
  if (bdd_bdd_T(f) == one && bdd_bdd_E(f) == zero)
    tree->pi = 1;
  if (candidate)
    tree->candidate = 1;
  if (!tree->candidate) {
    tree->id = NumTree;
    NumTree++;
  }
  if (!InsertMlTable(table, f, tree)) {
    bdd_recursive_deref_zdd(dd, f);
    FREE(tree);
    return NULL;
  }
  *ref = 0;

  return(tree);
}


void
SynthInitMlTable(void)
{
  NumTree = 1;
  MlTreeHead = NIL(MlTree);
  MlSizeHead = NIL(MlSizeList);
  HeadListTable = st_init_table(strcmp, st_strhash);
  TailListTable = st_init_table(strcmp, st_strhash);
}


void
SynthClearMlTable(bdd_manager *dd,
                  st_table *table)
{
  st_generator  *gen;
  bdd_node              *k;
  MlTree                *r;
  MlSizeList            *l, *next;

  st_foreach_item(table, gen, (&k), (&r)) {
    bdd_recursive_deref_zdd(dd, k);
    if (!MlTree_IsComplement(r))
      SynthFreeMlTree(r, 0);
  }

  NumTree = 1;
  MlTreeHead = NIL(MlTree);

  st_free_table(HeadListTable);
  st_free_table(TailListTable);
  HeadListTable = TailListTable = NIL(st_table);

  l = MlSizeHead;
  while (l) {
    next = l->next;
    FREE(l->string);
    FREE(l);
    l = next;
  }
  MlSizeHead = NIL(MlSizeList);
}


void
SynthPutMlTreeInList(bdd_manager *dd,
                     MlTree *tree,
                     int candidate)
{
  int           i;
  int           word, size;
  unsigned int  *mask;
  int           top;
  MlTree        *last;
  MlSizeList    *list, *pre_list, *new_list;

  word = sizeof(int) * 8;
  size = bdd_num_zdd_vars(dd) / word + 1;

  if (candidate) {
    tree->nLiterals = tree->q->nLiterals + tree->d->nLiterals;

    mask = ALLOC(unsigned int, size);
    for (i = 0; i < size; i++)
      mask[i] = tree->q->support[i] | tree->d->support[i];
    tree->support = mask;
  } else {
    if (tree->nLiterals == 0) {
      top = tree->top;
      tree->top = 1;
      tree->nLiterals = SynthCountMlLiteral(dd, tree, 0);
      tree->top = top;
    }

    if (!tree->support) {
      mask = ALLOC(unsigned int, size);
      (void)memset((void *)mask, 0, size * sizeof(int));
      SynthGetSupportMask(dd, tree->node, mask);
      tree->support = mask;
    }
  }

  if ((!MlTreeHead) || (tree->nLiterals > MlTreeHead->nLiterals)) {
    tree->next = MlTreeHead;
    MlTreeHead = tree;

    list = ALLOC(MlSizeList, 1);
    list->size = tree->nLiterals;
    list->string = GetIntString(list->size);
    list->next = MlSizeHead;
    MlSizeHead = list;

    st_insert(HeadListTable, list->string, (char *)tree);
    st_insert(TailListTable, list->string, (char *)tree);
  } else {
    pre_list = NIL(MlSizeList);
    list = MlSizeHead;
    while (list) {
      if (tree->nLiterals == list->size) {
        if (list == MlSizeHead) {
          tree->next = MlTreeHead;
          MlTreeHead = tree;
          st_insert(HeadListTable, list->string, (char *)tree);
        } else {
          st_lookup(TailListTable, list->string, (&last));
          tree->next = last->next;
          last->next = tree;
          st_insert(TailListTable, list->string, (char *)tree);
        }
        break;
      } else if (tree->nLiterals > list->size) {
        st_lookup(TailListTable, pre_list->string, (&last));
        tree->next = last->next;
        last->next = tree;

        new_list = ALLOC(MlSizeList, 1);
        new_list->size = tree->nLiterals;
        new_list->string = GetIntString(new_list->size);
        new_list->next = list;
        pre_list->next = new_list;

        st_insert(HeadListTable, new_list->string, (char *)tree);
        st_insert(TailListTable, new_list->string, (char *)tree);
        break;
      } else if (!list->next) {
        st_lookup(TailListTable, list->string, (&last));
        tree->next = NIL(MlTree);
        last->next = tree;

        new_list = ALLOC(MlSizeList, 1);
        new_list->size = tree->nLiterals;
        new_list->string = GetIntString(new_list->size);
        new_list->next = NIL(MlSizeList);
        list->next = new_list;

        st_insert(HeadListTable, new_list->string, (char *)tree);
        st_insert(TailListTable, new_list->string, (char *)tree);
        break;
      }
      pre_list = list;
      list = list->next;
    }
  }

  if (VerifyTreeMode)
    VerifyTreeList();
}


MlTree  *
SynthGetHeadTreeOfSize(int size)
{
  MlTree        *head;
  MlSizeList    *list;

  list = MlSizeHead;
  while (list) {
    if (size == list->size) {
      st_lookup(HeadListTable, list->string, (&head));
      return(head);
    } else if (size > list->size)
      return(NULL);
    list = list->next;
  }
  return(NULL);
}


MlTree  *
SynthCheckAndMakeComplement(bdd_manager *dd,
                            st_table *table,
                            MlTree *tree,
                            int *comp_flag,
                            int verbosity)
{
  bdd_node      *c;
  MlTree        *c_tree, *new_;

  if (MlTree_IsComplement(tree))
    return(tree);

  *comp_flag = 0;
  if (!tree->complement) {
    c = MakeComplementOfZddCover(dd, tree->node, verbosity);
    if (!c)
      return(NULL);
    bdd_ref(c);
    c_tree = SynthLookupMlTable(table, dd, (char *)c, 0, verbosity);
    if (c_tree) {
      MlTree *m_tree = MlTree_Regular(c_tree);
      if (MlTree_Regular(tree)->candidate &&
          MlTree_Regular(c_tree)->candidate) {
        /*
        **       tree     m_tree
        **         |\      /|
        **         |   \/   |
        **         | /    \ |
        **         q        d
        **/

        if (ResolveConflictMode == 0 || c_tree == m_tree ||
            tree->nLiterals <= m_tree->nLiterals) {
          /* throw away m_tree and assign c to tree->complement */
          UnlinkMlTree(m_tree);
          bdd_recursive_deref_zdd(dd, m_tree->node);
          bdd_recursive_deref_zdd(dd, m_tree->complement);
          st_delete(table, (char **)(&m_tree->node), NIL(char *));
          st_delete(table, (char **)(&m_tree->complement), NIL(char *));
          if (m_tree->support)
            FREE(m_tree->support);
          FREE(m_tree);
          tree->complement = c;
          if (!InsertMlTable(table, c, MlTree_Not(tree))) {
            tree->complement = NIL(bdd_node);
            bdd_recursive_deref_zdd(dd, c);
            return(NULL);
          }
        } else if (c_tree != m_tree) {
          /* takes m_tree's contents and throws away m_tree */
          UnlinkMlTree(tree);
          UnlinkMlTree(m_tree);
          bdd_recursive_deref_zdd(dd, tree->node);
          st_delete(table, (char **)(&tree->node), NIL(char *));
          if (tree->support)
            FREE(tree->support);
          memcpy(tree, m_tree, sizeof(MlTree));
          FREE(m_tree);
          tree->complement = c;
          if (!InsertMlTable(table, tree->node, tree)) 
            return(NULL);
          if (!InsertMlTable(table, tree->complement, MlTree_Not(tree))) 
            return(NULL);
        } else { /* It never happens at this time,
                  * the case(c_tree == m_tree) is already taken care of.
                  * But, it should be implemented to improve
                  * in the future.
                  */
        }
        if (VerifyTreeMode) {
          SynthVerifyTree(dd, tree, 0);
          SynthVerifyMlTable(dd, table);
        }
        return(tree);
      } else if (MlTree_Regular(tree)->candidate) {
        /*
        **       tree     m_tree
        **         |\      /|\
        **         |   \/   |   \
        **         | /    \ |      \
        **         q        d        r
        **/

        if (tree->r == m_tree) {
          if (c_tree == m_tree)
            *comp_flag = 1;
          else
            *comp_flag = 0;

          if (ResolveConflictMode == 0 || c_tree == m_tree ||
              m_tree->nLiterals <= tree->nLiterals) {
            /* throw away tree and returns m_tree */
            bdd_recursive_deref_zdd(dd, c);
            UnlinkMlTree(tree);
            bdd_recursive_deref_zdd(dd, tree->node);
            st_delete(table, (char **)(&m_tree->node), NIL(char *));
            if (tree->support)
              FREE(tree->support);
            FREE(tree);
          } else if (c_tree != m_tree) {
            /*
            **      tree->complement = m_tree->complement
            **
            **       tree     m_tree
            **         |\      /|\
            **         |   \/   |   \
            **         | /    \ |      \
            **         q        d        r
            **/

            MlTree      *r_tree, *tmp_tree;
            int         r_comp;
            int         ref;
            bdd_node    *zero = bdd_read_zero(dd);

            /* takes tree's contents and throw away tree and m_tree->r */

            bdd_recursive_deref_zdd(dd, c);
            r_tree = SynthFindOrCreateMlTree(table, dd, zero, 1, 0, &ref,
                                             verbosity);
            if (!r_tree)
              return(NULL);
            if (MlTree_IsComplement(r_tree)) {
              r_tree = MlTree_Regular(r_tree);
              m_tree->r_comp = 1;
            }
            tmp_tree = r_tree;
            r_tree = SynthCheckAndMakeComplement(dd, table, r_tree,
                                                 &r_comp, verbosity);
            if (!r_tree)
              return(NULL);
            else if (r_tree != tmp_tree) {
              if (r_comp)
                m_tree->r_comp = 1;
              ref = 1;
            }
            tree->r = r_tree;
            tree->r_ref = ref;
            tree->id = m_tree->id;
            tree->candidate = 0;

            bdd_recursive_deref_zdd(dd, m_tree->node);
            bdd_recursive_deref_zdd(dd, m_tree->complement);
            st_delete(table, (char **)(&m_tree->node), NIL(char *));
            st_delete(table, (char **)(&m_tree->complement), NIL(char *));
            UnlinkMlTree(m_tree);
            if (m_tree->support)
              FREE(m_tree->support);
            ref = m_tree->r_ref;
            r_tree = m_tree->r;
            memcpy(m_tree, tree, sizeof(MlTree));
            FREE(tree);
            SynthPutMlTreeInList(dd, m_tree, 0);

            if (ref) {
              if (r_tree->shared)
                DeleteMlTree(dd, table, r_tree, NULL, 1, 0);
            } else
              DeleteMlTree(dd, table, r_tree, NULL, 1, 0);
          } else { /* It never happens at this time,
                    * the case(c_tree == m_tree) is already taken care of.
                    * But, it should be implemented to improve
                    * in the future.
                    */
          }
          if (VerifyTreeMode) {
            SynthVerifyTree(dd, m_tree, 0);
            SynthVerifyMlTable(dd, table);
          }
          return(m_tree);
        }
        if (!SynthUseCandidate(table, dd, tree, verbosity)) {
          bdd_recursive_deref_zdd(dd, c);
          return(NULL);
        }
        SynthSetSharedFlag(dd, tree);
      } else if (MlTree_Regular(c_tree)->candidate) {
        if (m_tree->r == tree) {
          /*
          **      m_tree     tree
          **         |\      /|\
          **         |   \/   |   \
          **         | /    \ |      \
          **         q        d        r
          **/

          if (ResolveConflictMode == 0 || c_tree == m_tree ||
              tree->nLiterals <= m_tree->nLiterals) {
            /* throw away m_tree and assign c to tree->complement */
            UnlinkMlTree(m_tree);
            bdd_recursive_deref_zdd(dd, m_tree->node);
            bdd_recursive_deref_zdd(dd, m_tree->complement);
            st_delete(table, (char **)(&m_tree->node), NIL(char *));
            st_delete(table, (char **)(&m_tree->complement), NIL(char *));
            if (m_tree->support)
              FREE(m_tree->support);
            FREE(m_tree);
            tree->complement = c;
            if (!InsertMlTable(table, c, MlTree_Not(tree))) {
              tree->complement = NIL(bdd_node);
              bdd_recursive_deref_zdd(dd, c);
              return(NULL);
            }
          } else if (c_tree != m_tree) {
            /*
            **      tree->complement = m_tree->complement
            **
            **      m_tree     tree
            **         |\      /|\
            **         |   \/   |   \
            **         | /    \ |      \
            **         q        d        r
            **/

            MlTree      *r_tree, *tmp_tree;
            int         r_comp;
            int         ref;
            bdd_node    *zero = bdd_read_zero(dd);

            /* takes m_tree's contents and throw away m_tree and tree->r */

            bdd_recursive_deref_zdd(dd, c);
            r_tree = SynthFindOrCreateMlTree(table, dd, zero, 1, 0, &ref,
                                             verbosity);
            if (!r_tree)
              return(NULL);
            if (MlTree_IsComplement(r_tree)) {
              r_tree = MlTree_Regular(r_tree);
              m_tree->r_comp = 1;
            }
            tmp_tree = r_tree;
            r_tree = SynthCheckAndMakeComplement(dd, table, r_tree,
                                                 &r_comp, verbosity);
            if (!r_tree)
              return(NULL);
            else if (r_tree != tmp_tree) {
              if (r_comp)
                m_tree->r_comp = 1;
              ref = 1;
            }
            m_tree->r = r_tree;
            m_tree->r_ref = ref;
            m_tree->id = tree->id;
            m_tree->candidate = 0;

            bdd_recursive_deref_zdd(dd, tree->node);
            st_delete(table, (char **)(&tree->node), NIL(char *));
            UnlinkMlTree(tree);
            if (tree->support)
              FREE(tree->support);
            ref = tree->r_ref;
            r_tree = tree->r;
            memcpy(tree, m_tree, sizeof(MlTree));
            FREE(m_tree);
            SynthPutMlTreeInList(dd, tree, 0);

            if (ref) {
              if (r_tree->shared)
                DeleteMlTree(dd, table, r_tree, NULL, 1, 0);
            } else
              DeleteMlTree(dd, table, r_tree, NULL, 1, 0);
          } else { /* It never happens at this time,
                    * the case(c_tree == m_tree) is already taken care of.
                    * But, it should be implemented to improve
                    * in the future.
                    */
            /*
            **      tree->complement = m_tree->node
            **
            **      m_tree     tree
            **         |\      /|\
            **         |   \/   |   \
            **         | /    \ |      \
            **         q        d        r
            **/
          }
          return(tree);
        }
        if (!SynthUseCandidate(table, dd, m_tree, verbosity)) {
          bdd_recursive_deref_zdd(dd, c);
          return(NULL);
        }
        SynthSetSharedFlag(dd, m_tree);
      }

      bdd_recursive_deref_zdd(dd, c);
      if (c_tree == m_tree)
        *comp_flag = 1;
      else
        *comp_flag = 0;

      if (verbosity)
        (void) fprintf(vis_stdout, "** synth warning: Duplicate entry ...\n");
      new_ = ResolveConflictNode(dd, table, c_tree, tree, *comp_flag, verbosity);
      if (verbosity)
        (void) fprintf(vis_stdout, "** synth info: Conflict was resolved.\n");
      if (VerifyTreeMode) {
        SynthVerifyTree(dd, new_, 0);
        SynthVerifyMlTable(dd, table);
      }
      return(new_);
    } else if (bdd_read_reordered_field(dd) || noMemoryFlag == 1) {
      bdd_recursive_deref_zdd(dd, c);
      return(NULL);
    }
    tree->complement = c;
    if (!InsertMlTable(table, c, MlTree_Not(tree))) {
      tree->complement = NIL(bdd_node);
      bdd_recursive_deref_zdd(dd, c);
      return NULL;
    }
  }
  return(tree);
}


void
SynthSetSharedFlag(bdd_manager *dd,
                   MlTree *tree)
{
  MlTree        *t;
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);

  t = MlTree_Regular(tree);
  if (t->node == zero || t->node == one)
    return;
  if (t->pi == 0)
    t->shared = 1;
}


int
SynthPostFactoring(bdd_manager *dd,
                   st_table *table,
                   MlTree *(* factoring_func)(bdd_manager *, st_table *,
                                              bdd_node *, int, int *, MlTree *,
                                              int, MlTree *, int),
                   int verbosity)
{
  MlTree        *cur, *candy;
  int           ref;
  bdd_node      *q;
  bdd_node      *zero = bdd_read_zero(dd);

  if (VerifyTreeMode) {
    SynthVerifyMlTable(dd, table);
    VerifyTreeList();
  }

  cur = MlTreeHead;
  while (cur) {
    if (cur->leaf) {
      if (cur->nLiterals < 2)
        break;
      candy = cur->next;
      while (candy) {
        if (candy->nLiterals == 1)
          break;
        else if (candy->leaf == 0 ||
                 candy->nLiterals == cur->nLiterals) {
          candy = candy->next;
          continue;
        }

        q = (* ZddDivideFunc)(dd, cur->node, candy->node);
        if (!q)
          return(1);
        bdd_ref(q);
        /* Even though we deref q, it still exists as a
         * pointer and beyond this point, we use it only to
         * check if it is zero or not.
         */
        bdd_recursive_deref_zdd(dd,q);
        if (q != zero) {
          (void) (* factoring_func)(dd, table, cur->node,
                                    0, &ref, candy, 0, cur, verbosity);
          if (VerifyTreeMode) {
            SynthVerifyTree(dd, cur, 0);
            SynthVerifyMlTable(dd, table);
            VerifyTreeList();
          }
          if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
            return(1);

          SynthSetSharedFlag(dd, candy);
          break;
        } else {
          q = (* ZddDivideFunc)(dd, cur->node, 
                                candy->complement);
          if (!q)
            return(1);
          bdd_ref(q);
          /* Even though we deref q, it still exists as a
           * pointer and beyond this point, we use it only
           * to check if it is zero or not.
           */
          bdd_recursive_deref_zdd(dd,q);
          if (q != zero) {
            (void) (* factoring_func)(dd, table, cur->node, 0,
                                      &ref, candy, 1, cur, verbosity);
            if (VerifyTreeMode) {
              SynthVerifyTree(dd, cur, 0);
              SynthVerifyMlTable(dd, table);
              VerifyTreeList();
            }
            if (bdd_read_reordered_field(dd) || noMemoryFlag == 1 )
              return(1);
            SynthSetSharedFlag(dd, candy);
            break;
          }
        }
        candy = candy->next;
      }
    }
    cur = cur->next;
  }
  return(0);
}


void
SynthUpdateRefOfParent(MlTree *top)
{
  MlTree        *cur;

  cur = MlTreeHead;
  while (cur) {
    if (cur->q == top)
      cur->q_ref = 1;
    else if (cur->d == top)
      cur->d_ref = 1;
    else if (cur->r == top)
      cur->r_ref = 1;
    cur = cur->next;
  }
}


void
SynthVerifyTree(bdd_manager *dd,
                MlTree *tree,
                int flag)
{
  bdd_node      *node, *comp;
  bdd_node      *q, *d, *r, *f, *m;
  int           bdd_diff;

  if (flag && !tree->leaf) {
    if (!tree->q_ref)
      SynthVerifyTree(dd, tree->q, flag);
    if (!tree->d_ref)
      SynthVerifyTree(dd, tree->d, flag);
    if (!tree->r_ref)
      SynthVerifyTree(dd, tree->r, flag);
  }

  node = bdd_make_bdd_from_zdd_cover(dd, tree->node);
  if (!node)
    return;
  bdd_ref(node);
  if (tree->complement) {
    comp = bdd_make_bdd_from_zdd_cover(dd, tree->complement);
    if (!comp) {
      bdd_recursive_deref(dd, node);
      return;
    }
    bdd_ref(comp);
    
    if (node != bdd_not_bdd_node(comp)) {
      (void) fprintf(vis_stdout,
        "** synth error: Invalid complement node in tree [%d].\n", tree->id);
    }
    
    bdd_recursive_deref(dd, comp);
  }

  if (tree->leaf) {
    if (tree->q) {
      (void) fprintf(vis_stdout,
             "** synth error: q exists in leaf tree [%d].\n", tree->id);
    }
    if (tree->d) {
      (void) fprintf(vis_stdout,
             "** synth error: d exists in leaf tree [%d].\n", tree->id);
    }
    if (tree->r) {
      (void) fprintf(vis_stdout,
             "** synth error: r exists in leaf tree [%d].\n", tree->id);
    }
    if (tree->q_ref) {
      (void) fprintf(vis_stdout,
             "** synth error: q_ref = 1 in leaf tree [%d].\n", tree->id);
    }
    if (tree->d_ref) {
      (void) fprintf(vis_stdout,
             "** synth error: d_ref = 1 in leaf tree [%d].\n", tree->id);
    }
    if (tree->r_ref) {
      (void) fprintf(vis_stdout,
             "** synth error: r_ref = 1 in leaf tree [%d].\n", tree->id);
    }
    if (tree->q_comp) {
      (void) fprintf(vis_stdout,
             "** synth error: q_comp = 1 in leaf tree [%d].\n", tree->id);
    }
    if (tree->d_comp) {
      (void) fprintf(vis_stdout,
             "** synth error: d_comp = 1 in leaf tree [%d].\n", tree->id);
    }
    if (tree->r_comp) {
      (void) fprintf(vis_stdout,
             "** synth error: r_comp = 1 in leaf tree [%d].\n", tree->id);
    }
    bdd_recursive_deref(dd, node);
    return;
  }
  else {
    if (tree->pi) {
      (void) fprintf(vis_stdout,
             "** synth error: pi = 1 in non-leaf tree [%d].\n", tree->id);
    }
  }

  if (!tree->q) {
    (void) fprintf(vis_stdout,
                   "** synth error: no q in tree [%d].\n", tree->id);
    bdd_recursive_deref(dd, node);
    return;
  }
  if (tree->q_comp)
    q = bdd_make_bdd_from_zdd_cover(dd, tree->q->complement);
  else
    q = bdd_make_bdd_from_zdd_cover(dd, tree->q->node);
  if (!q) {
    (void) fprintf(vis_stdout,
                   "** synth error: no q node in tree [%d].\n", tree->id);
    bdd_recursive_deref(dd, node);
    return;
  }
  bdd_ref(q);
  if (!tree->d) {
    (void) fprintf(vis_stdout,
                   "** synth error: no d in tree [%d].\n", tree->id);
    bdd_recursive_deref(dd, node);
    bdd_recursive_deref(dd, q);
    return;
  }
  if (tree->d_comp)
    d = bdd_make_bdd_from_zdd_cover(dd, tree->d->complement);
  else
    d = bdd_make_bdd_from_zdd_cover(dd, tree->d->node);
  if (!d) {
    (void) fprintf(vis_stdout,
                   "** synth error: no d node in tree [%d].\n", tree->id);
    bdd_recursive_deref(dd, node);
    bdd_recursive_deref(dd, q);
    return;
  }
  bdd_ref(d);
  if (!tree->candidate) {
    if (!tree->r) {
      (void) fprintf(vis_stdout,
                     "** synth error: no r in tree [%d].\n", tree->id);
      bdd_recursive_deref(dd, node);
      bdd_recursive_deref(dd, q);
      bdd_recursive_deref(dd, d);
      return;
    }
    if (tree->r_comp)
      r = bdd_make_bdd_from_zdd_cover(dd, tree->r->complement);
    else
      r = bdd_make_bdd_from_zdd_cover(dd, tree->r->node);
    if (!r) {
      (void) fprintf(vis_stdout,
                     "** synth error: no r node in tree [%d].\n", tree->id);
      bdd_recursive_deref(dd, node);
      bdd_recursive_deref(dd, q);
      bdd_recursive_deref(dd, d);
      return;
    }
    bdd_ref(r);
    
    m = bdd_bdd_and(dd, q, d);
    if (!m) {
      bdd_recursive_deref(dd, node);
      bdd_recursive_deref(dd, q);
      bdd_recursive_deref(dd, d);
      bdd_recursive_deref(dd, r);
      return;
    }
    bdd_ref(m);
    bdd_recursive_deref(dd, q);
    bdd_recursive_deref(dd, d);
    f = bdd_bdd_or(dd, m, r);
    if (!f) {
      bdd_recursive_deref(dd, node);
      bdd_recursive_deref(dd, r);
      bdd_recursive_deref(dd, m);
      return;
    }
    bdd_ref(f);
    bdd_recursive_deref(dd, r);
    bdd_recursive_deref(dd, m);
  } else {
    f = bdd_bdd_and(dd, q, d);
    if (!f) {
      bdd_recursive_deref(dd, node);
      bdd_recursive_deref(dd, q);
      bdd_recursive_deref(dd, d);
      return;
    }
    bdd_ref(f);
    bdd_recursive_deref(dd, q);
    bdd_recursive_deref(dd, d);
  }
  if (!f) {
    bdd_recursive_deref(dd, node);
    return;
  }

  if (f == node)
    bdd_diff = 0;
  else
    bdd_diff = 1;

  bdd_recursive_deref(dd, f);
  bdd_recursive_deref(dd, node);

  if (tree->comp)
    node = tree->complement;
  else
    node = tree->node;
  if (tree->q_comp)
    q = tree->q->complement;
  else
    q = tree->q->node;
  if (tree->d_comp)
    d = tree->d->complement;
  else
    d = tree->d->node;
  if (!tree->candidate) {
    if (tree->r_comp)
      r = tree->r->complement;
    else
      r = tree->r->node;
    m = (* SynthGetZddProductFunc())(dd, d, q);
    if (!m)
      return;
    bdd_ref(m);
    f = bdd_zdd_union(dd, m, r);
    if (!f) {
      bdd_recursive_deref_zdd(dd, m);
      return;
    }
    bdd_ref(f);
    bdd_recursive_deref_zdd(dd, m);
  } else {
    f = (* SynthGetZddProductFunc())(dd, d, q);
    if (!f)
      return;
    bdd_ref(f);
  }
  if (f != node) {
    if (bdd_diff) {
      (void) fprintf(vis_stdout,
             "** synth error: BDD & ZDD f != qd+r in tree [%d - 0x%lx].\n",
             tree->id, (unsigned long)tree);
    }
    else {
      (void) fprintf(vis_stdout,
                     "Warning : ZDD f != qd+r in tree [%d - 0x%lx].\n",
                     tree->id, (unsigned long)tree);
    }
  }
  else if (bdd_diff) {
    (void) fprintf(vis_stdout,
                   "** synth error: BDD f != qd+r in tree [%d - 0x%lx].\n",
                   tree->id, (unsigned long)tree);
  }
  bdd_recursive_deref_zdd(dd, f);
}


void
SynthVerifyMlTable(bdd_manager *dd,
                   st_table *table)
{
  st_generator  *gen;
  bdd_node              *node;
  MlTree                *tree, *reg;

  st_foreach_item(table, gen, (&node), (&tree)) {
    reg = MlTree_Regular(tree);
    if ((reg == tree && node != reg->node) ||
        (reg != tree && node != reg->complement)) {
      (void) fprintf(vis_stdout,
                     "** synth error: wrong node in tree [%d].\n", reg->id);
    }
    tree = reg;
    if (tree->id >= NumTree) {
      (void) fprintf(vis_stdout,
                     "** synth error: wrong id in tree [%d].\n", tree->id);
    }
    if (!tree->leaf) {
      if (!tree->d) {
        (void) fprintf(vis_stdout,
               "** synth error: d doesn't exist in tree [%d].\n", tree->id);
      }
      if (!tree->q) {
        (void) fprintf(vis_stdout,
               "** synth error: q doesn't exist in tree [%d].\n", tree->id);
      }
      if (!tree->r && !tree->candidate) {
        (void) fprintf(vis_stdout,
               "** synth error: r doesn't exist in tree [%d].\n", tree->id);
      }
    }
  }
}


void
SynthPrintTreeList(MlTree *list)
{
  MlTree *cur = list;
  if (!cur)
    cur = MlTreeHead;
  while (cur) {
    printf("%d (%d) - %d [0x%lx]\n", cur->id, cur->nLiterals,
           cur->leaf, (unsigned long)cur);
    cur = cur->next;
  }
}


void
SynthPrintLeafList(MlTree *list)
{
  MlTree *cur = list;
  if (!cur)
    cur = MlTreeHead;
  while (cur) {
    if (cur->leaf)
      printf("%d (%d) [0x%lx]\n", cur->id, cur->nLiterals, (unsigned long)cur);
    cur = cur->next;
  }
}


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


static MlTree *
ResolveConflictNode(bdd_manager *dd,
                    st_table *table,
                    MlTree *tree1,
                    MlTree *tree2,
                    int comp_flag,
                    int verbosity)
{
  MlTree        *live_tree, *kill_tree;

  if (MlTree_IsComplement(tree1))
    tree1 = MlTree_Regular(tree1);
  if (MlTree_IsComplement(tree2))
    tree2 = MlTree_Regular(tree2);

  if (verbosity) {
    if (tree1->complement || tree2->complement)
      (void) fprintf(vis_stdout, "** synth warning: real conflict.\n");
  }

  if (ResolveConflictMode == 0) {
    live_tree = tree1;
    kill_tree = tree2;
  } else {
    if (tree1->nLiterals > tree2->nLiterals) {
      live_tree = tree2;
      kill_tree = tree1;
    } else {
      live_tree = tree1;
      kill_tree = tree2;
    }
  }

  if (!live_tree->complement) {
    if (comp_flag)
      live_tree->complement = kill_tree->node;
    else
      live_tree->complement = kill_tree->complement;
    bdd_ref(live_tree->complement);
    bdd_recursive_deref_zdd(dd, kill_tree->node);
    st_delete(table, (char **)(&kill_tree->node), NIL(char *));
    if (kill_tree->complement) {
        bdd_recursive_deref_zdd(dd, kill_tree->complement);
        st_delete(table, (char **)(&kill_tree->complement), NIL(char *));
    }
    st_insert(table, (char *)live_tree->complement,
              (char *)MlTree_Not(live_tree));
  } else {
    bdd_recursive_deref_zdd(dd, kill_tree->node);
    st_delete(table, (char **)(&kill_tree->node), NIL(char *));
    if (kill_tree->complement) {
        bdd_recursive_deref_zdd(dd, kill_tree->complement);
        st_delete(table, (char **)(&kill_tree->complement), NIL(char *));
    }
  }

  DeleteMlTree(dd, table, kill_tree, live_tree, 0, comp_flag);
  SynthSetSharedFlag(dd, live_tree);

  if (VerifyTreeMode) {
    SynthVerifyTree(dd, live_tree, 0);
    SynthVerifyMlTable(dd, table);
    VerifyTreeList();
  }

  return(live_tree);
}


static void
DeleteMlTree(bdd_manager *dd,
             st_table *table,
             MlTree *kill_tree,
             MlTree *live_tree,
             int deref,
             int comp_flag)
{
  MlTree        *cur, *pre, *next;
  int           ref;

  if (kill_tree->shared && deref) {
    ref = 0;
    cur = MlTreeHead;
    while (cur) {
      if (cur == kill_tree) {
        cur = cur->next;
        continue;
      }
      if (cur->q == kill_tree)
        ref++;
      else if (cur->d == kill_tree)
        ref++;
      else if (cur->r == kill_tree)
        ref++;
      cur = cur->next;
    }

    if (ref == 1)
      kill_tree->shared = 0;
    return;
  }

  DeleteMlSizeList(kill_tree);

  if (kill_tree->id == NumTree - 1)
    NumTree--;
  if (deref) {
    bdd_recursive_deref_zdd(dd, kill_tree->node);
    st_delete(table, (char **)(&kill_tree->node), NIL(char *));
    if (kill_tree->complement) {
        bdd_recursive_deref_zdd(dd, kill_tree->complement);
        st_delete(table, (char **)(&kill_tree->complement), NIL(char *));
    }
  }
  pre = NIL(MlTree);
  cur = MlTreeHead;
  while (cur) {
    if (cur == kill_tree) {
      next = cur->next;
      if (pre)
        pre->next = next;
      else
        MlTreeHead = next;
      cur = next;
      if (!live_tree)
        break;
    } else {
      if (live_tree) {
        if (cur->q == kill_tree) {
          if (comp_flag)
            cur->q_comp ^= 01;
          cur->q = live_tree;
          cur->q_ref = 1;
          if (VerifyTreeMode)
            SynthVerifyTree(dd, cur, 0);
        } else if (cur->d == kill_tree) {
          if (comp_flag)
            cur->d_comp ^= 01;
          cur->d = live_tree;
          cur->d_ref = 1;
          if (VerifyTreeMode)
            SynthVerifyTree(dd, cur, 0);
        } else if (cur->r == kill_tree) {
          if (comp_flag)
            cur->r_comp ^= 01;
          cur->r = live_tree;
          cur->r_ref = 1;
          if (VerifyTreeMode)
            SynthVerifyTree(dd, cur, 0);
        }
      }
      pre = cur;
      cur = cur->next;
    }
  }

  if (kill_tree->leaf == 0) {
    if (kill_tree->q_ref) {
      if (kill_tree->q->shared)
        DeleteMlTree(dd, table, kill_tree->q, NULL, 1, 0);
    } else
      DeleteMlTree(dd, table, kill_tree->q, NULL, 1, 0);
    if (kill_tree->d_ref) {
      if (kill_tree->d->shared)
        DeleteMlTree(dd, table, kill_tree->d, NULL, 1, 0);
    } else
      DeleteMlTree(dd, table, kill_tree->d, NULL, 1, 0);
    if (kill_tree->r_ref) {
      if (kill_tree->r->shared)
        DeleteMlTree(dd, table, kill_tree->r, NULL, 1, 0);
    } else
      DeleteMlTree(dd, table, kill_tree->r, NULL, 1, 0);
  }

  if (kill_tree->support)
    FREE(kill_tree->support);
  FREE(kill_tree);
}


static void
UnlinkMlTree(MlTree *kill_tree)
{
  MlTree        *cur, *pre;

  DeleteMlSizeList(kill_tree);

  pre = (MlTree *)NULL;
  cur = MlTreeHead;
  while (cur) {
    if (cur == kill_tree) {
        if (pre)
          pre->next = cur->next;
        else
          MlTreeHead = cur->next;
        break;
    }
    pre = cur;
    cur = cur->next;
  }
}


static void
DeleteMlSizeList(MlTree *tree)
{
  MlTree        *head, *tail, *cur, *pre;
  MlSizeList    *list, *pre_list;
  int           size;

  size = tree->nLiterals;
  pre_list = NIL(MlSizeList);
  list = MlSizeHead;
  while (list) {
    if (size == list->size) {
      st_lookup(HeadListTable, list->string, (&head));
      st_lookup(TailListTable, list->string, (&tail));
      if (head == tail) {
        assert(tree == head);
        if (pre_list)
          pre_list->next = list->next;
        else
          MlSizeHead = list->next;
        st_delete(HeadListTable, (char **)&list->string, NIL(char *));
        st_delete(TailListTable, (char **)&list->string, NIL(char *));
        FREE(list->string);
        FREE(list);
      } else {
        pre = NIL(MlTree);
        cur = head;
        while (cur) {
          if (cur == tree) {
            if (cur == head) {
              st_delete(HeadListTable, (char **)&list->string, NIL(char *));
              st_insert(HeadListTable, list->string, (char *)cur->next);
            } else if (cur == tail) {
              st_delete(TailListTable, (char **)&list->string, NIL(char *));
              st_insert(TailListTable, list->string, (char *)pre);
            }
            break;
          }
          pre = cur;
          cur = cur->next;
        }
      }
      break;
    } else if (size > list->size)
      break;
    pre_list = list;
    list = list->next;
  }
}


static int
InsertMlTable(st_table *table,
              bdd_node *node,
              MlTree *tree)
{
  int           flag;

  flag = st_insert(table, (char *)node, (char *)tree);
  if (flag == ST_OUT_OF_MEM) {
    (void) fprintf(vis_stdout,"** synth error: Out of Memory.\n");
    noMemoryFlag = 1;
    return (0);
  } else if (flag == 1)
    (void) fprintf(vis_stdout, "** synth warning: Duplicate entry.\n");
  return(1);
}


static bdd_node *
MakeComplementOfZddCover(bdd_manager *dd,
                         bdd_node *node,
                         int verbosity)
{
  bdd_node      *comp;

  if (verbosity > 1) {
    (void) fprintf(vis_stdout,"*****\n");
    SynthPrintZddTreeMessage(dd, node, "R : ");
  }

  comp = bdd_zdd_complement(dd, node);
  if (!comp)
    return(NULL);

  if (verbosity > 1) {
    SynthPrintZddTreeMessage(dd, comp, "C : ");
    (void) fprintf(vis_stdout,"*****\n");
  }

  return(comp);
}


static  char *
GetIntString(int v)
{
  char  string[12];
  char  *ret;

  sprintf(string, "%d", v);
  ret = (char *)ALLOC(char, strlen(string) + 1);
  strcpy(ret, string);
  return(ret);
}


static void
VerifyTreeList(void)
{
  int           count;
  MlTree        *cur, *candy;

  cur = MlTreeHead;
  while (cur) {
    count = 0;
    candy = cur->next;
    if (candy && candy->nLiterals > cur->nLiterals) {
      (void) fprintf(vis_stdout,
             "** synth error: predecessor[%d]'s size < successor[%d]'s size.\n",
                     cur->id, candy->id);
    }
    while (candy) {
      if (cur->id != 0) {
        if (candy->id == cur->id && candy != cur) {
          (void) fprintf(vis_stdout,
                 "** synth error: same id already exists [%d].\n", cur->id);
          break;
        }
      }
      if (candy == cur) {
        if (count > 0) {
          (void) fprintf(vis_stdout,
                 "** synth error: same address already exists [%d - 0x%lx].\n",
                         cur->id, (unsigned long)cur);
          break;
        }
        count++;
      }
      candy = candy->next;
    }
    cur = cur->next;
  }
}