src/synth/synthSimple.c

Go to the documentation of this file.

#include "synthInt.h"

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

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


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


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


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

extern  int     CompMode;
extern  int     UseMtree;
extern  int     UseCommonDivisor;
extern  int     TryNodeSharing;
extern  int     Resubstitution;
extern  int     RemainderComplement;
extern  int     noMemoryFlag;
extern  int     VerifyTreeMode;

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

static int CountZddLeafLiterals(bdd_manager *dd, bdd_node *node);

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


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

MlTree *
SynthSimpleFactorTree(bdd_manager *dd,
                      st_table *table,
                      bdd_node *f,
                      int level,
                      int *ref,
                      MlTree *comp_d_tree,
                      int comp_d_flag,
                      MlTree *bring,
                      int verbosity)
{
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  bdd_node      *d, *q, *r, *m;
  MlTree        *tree, *q_tree, *d_tree, *r_tree;
  char          message[120];
  char          space[100];
  MlTree        *comp_q_tree = (MlTree *)NULL;
  MlTree        *comp_r_tree = (MlTree *)NULL;
  int           found;
  MlTree        *tmp_tree;
  int           comp_flag;

  if (verbosity > 1) {
    SynthGetSpaceString(space, level * 2, 80);
    sprintf(message, "%s[%d] in : ", space, level);
    SynthPrintZddTreeMessage(dd, f, message);
    sprintf(message, "%s[%d]out : ", space, level);
  }

  if (bring)
    tree = (MlTree *)NULL;
  else {
    tree = SynthLookupMlTable(table, dd, f, 1, verbosity);
    /* tree could be NULL because of reordering, or a failure to
     * allocate memory or just that f was not in the cache.
     * So, we would like return NULL ONLY in the case of 
     * reordering or failure to allocate memory. 
     */
    if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
      return(NULL);
  }
  if (tree) {
    if (verbosity > 1)
      SynthPrintMlTreeMessage(dd, tree, message);
    *ref = 1;
    return(tree);
  }

  if (f == one || f == zero) {
    tree = SynthFindOrCreateMlTree(table, dd, f, 1, 0, ref, verbosity);
    if (!tree)
      return(NULL);
    tmp_tree = tree;
    tree = SynthCheckAndMakeComplement(dd, table, tree, &comp_flag, verbosity);
    if (!tree) {
      if (*ref == 0)
        SynthFreeMlTree(MlTree_Regular(tmp_tree), 1);
      return(NULL);
    } else if (tree != tmp_tree) {
      *ref = 1;
      if (comp_flag)
        tree = MlTree_Not(tree);
    }
    if (verbosity > 1)
      SynthPrintMlTreeMessage(dd, tree, message);
    return(tree);
  }

  d_tree = (MlTree *)NULL;
  if (comp_d_tree) {
    if (comp_d_flag)
      d = comp_d_tree->complement;
    else
      d = comp_d_tree->node;
    if (!d)
      return((MlTree *)NULL);
    bdd_ref(d);
  } else {
    found = 0;
    d = (* SynthGetZddDivisorFunc())(dd, f);
    if (!d)
      return(NULL);
    bdd_ref(d);
    if (TryNodeSharing) {
      /* Here, we don't need to call bdd_ref. */
      d = SynthFindBiggerDivisorInList(dd, table, f, d, &found,
                                       &comp_d_flag, &comp_d_tree, verbosity);
      if (!d)
        return(NULL);
    }
    if (UseCommonDivisor && found == 0) {
      tree = SynthGetFactorTreeWithCommonDivisor(dd, table,
                         SynthSimpleFactorTree, f, d, level, ref, verbosity);
      if (tree)
        return(tree);
      if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
        return(NULL);
    }
  }
  if (d == f) {
    tree = SynthFindOrCreateMlTree(table, dd, f, 1, 0, ref, verbosity);
    if (!tree) {
      bdd_recursive_deref_zdd(dd, d);
      return(NULL);
    }
    if (verbosity > 1)
      SynthPrintMlTreeMessage(dd, tree, message);
    tmp_tree = tree;
    tree = SynthCheckAndMakeComplement(dd, table, tree, &comp_flag, verbosity);
    if (!tree) {
      bdd_recursive_deref_zdd(dd, d);
      return(NULL);
    } else if (tree == tmp_tree) {
      if (*ref == 0)
        SynthPutMlTreeInList(dd, tree, 0);
    } else {
      *ref = 1;
      if (comp_flag)
        tree = MlTree_Not(tree);
    }
    bdd_recursive_deref_zdd(dd, d);
    return(tree);
  }
  if (!comp_d_tree) {
    if (st_lookup(table, (char *)d, &d_tree)) {
      SynthSetSharedFlag(dd, d_tree);
      if (MlTree_Regular(d_tree)->candidate) {
        if (!SynthUseCandidate(table, dd, d_tree, verbosity)) {
          bdd_recursive_deref_zdd(dd, d);
          return(NULL);
        }
      }
      if (MlTree_IsComplement(d_tree)) {
        d_tree = MlTree_Regular(d_tree);
        comp_d_tree = d_tree;
        d_tree = (MlTree *)NULL;
      }
    }
  } else {
    if (!comp_d_flag)
      d_tree = comp_d_tree;
  }

  q = (* SynthGetZddDivideFunc())(dd, f, d);
  if (!q) {
    bdd_recursive_deref_zdd(dd, d);
    return(NULL);
  }
  bdd_ref(q);
  if (comp_d_tree && q == zero) {
    bdd_recursive_deref_zdd(dd, d);
    bdd_recursive_deref_zdd(dd, q);
    return((MlTree *)NULL);
  }
  if (q == one) {
    bdd_recursive_deref_zdd(dd, q);
    tree = SynthPostFactorTree(dd, table, f, q, d, bring,
                       comp_d_tree, comp_d_flag, message, ref, verbosity);
    bdd_recursive_deref_zdd(dd, d);
    return(tree);
  }

  if (comp_d_tree && d_tree == comp_d_tree)
    comp_d_tree = (MlTree *)NULL;

  q_tree = (MlTree *)NULL;
  if (st_lookup(table, (char *)q, &q_tree)) {
    SynthSetSharedFlag(dd, q_tree);
    if (MlTree_Regular(q_tree)->candidate) {
      if (!SynthUseCandidate(table, dd, q_tree, verbosity)) {
        bdd_recursive_deref_zdd(dd, d);
        bdd_recursive_deref_zdd(dd, q);
        return(NULL);
      }
    }
    if (MlTree_IsComplement(q_tree)) {
      q_tree = MlTree_Regular(q_tree);
      comp_q_tree = q_tree;
      q_tree = (MlTree *)NULL;
    }
  }

  m = (* SynthGetZddProductFunc())(dd, d, q);
  if (!m) {
    bdd_recursive_deref_zdd(dd, d);
    bdd_recursive_deref_zdd(dd, q);
    return(NULL);
  }
  bdd_ref(m);
  r = bdd_zdd_diff(dd, f, m);
  if (!r) {
    bdd_recursive_deref_zdd(dd, d);
    bdd_recursive_deref_zdd(dd, q);
    bdd_recursive_deref_zdd(dd, m);
    return(NULL);
  }
  bdd_ref(r);

  r_tree = (MlTree *)NULL;
  if (st_lookup(table, (char *)r, &r_tree)) {
    SynthSetSharedFlag(dd, r_tree);
    if (MlTree_Regular(r_tree)->candidate) {
      if (!SynthUseCandidate(table, dd, r_tree, verbosity)) {
        bdd_recursive_deref_zdd(dd, d);
        bdd_recursive_deref_zdd(dd, q);
        bdd_recursive_deref_zdd(dd, m);
        bdd_recursive_deref_zdd(dd, r);
        return(NULL);
      }
    }
    if (MlTree_IsComplement(r_tree)) {
      r_tree = MlTree_Regular(r_tree);
      comp_r_tree = r_tree;
      r_tree = (MlTree *)NULL;
    }
  }

  tree = SynthFactorTreeRecur(dd, table, SynthSimpleFactorTree,
                              f, q, d, r, m, q_tree, d_tree, r_tree,
                              comp_q_tree, comp_d_tree, comp_r_tree,
                              bring, level, space, message, ref, verbosity);
  bdd_recursive_deref_zdd(dd, d);
  bdd_recursive_deref_zdd(dd, q);
  bdd_recursive_deref_zdd(dd, m);
  bdd_recursive_deref_zdd(dd, r);

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

  return(tree);
}


bdd_node *
SynthFindBiggerDivisorInList(bdd_manager *dd,
                             st_table *table,
                             bdd_node *f,
                             bdd_node *d,
                             int *found,
                             int *comp_d_flag,
                             MlTree **comp_d_tree,
                             int verbosity)
{
  bdd_node      *zero = bdd_read_zero(dd);
  int           size, nSupports;
  unsigned int  *support;
  int           flag;
  int           nL, nLiterals;
  bdd_node      *candy;
  MlTree        *cur;
  bdd_node      *q;

  nSupports = SynthGetSupportCount(dd, d);
  size = bdd_num_zdd_vars(dd) / (sizeof(unsigned int) * 8) + 1;
  support = ALLOC(unsigned int, size);
  SynthGetSupportMask(dd, f, support);
  flag = 0;
  cur = SynthGetHeadTreeOfSize(SynthGetLiteralCount(dd, f) - 1);
  nLiterals = CountZddLeafLiterals(dd, d);
  if (nLiterals == -1) {
    noMemoryFlag = 1;
    FREE(support);
    bdd_recursive_deref_zdd(dd, d);
    return(NULL);
  }

  while (cur) {
    if (cur->nLiterals < nSupports)
      break;
    nL = CountZddLeafLiterals(dd, cur->node);

    if ((!SynthIsSubsetOfSupport(size, cur->support, support)) ||
        nL < nLiterals) {
      flag = 0;
      cur = cur->next;
      continue;
    }

    if (flag)
      candy = cur->complement;
    else
      candy = cur->node;
    q = (* SynthGetZddDivideFunc())(dd, f, candy);
    if (!q) {
      FREE(support);
      bdd_recursive_deref_zdd(dd, d);
      return(NULL);
    }
    bdd_ref(q);
    bdd_recursive_deref_zdd(dd, q);
    if (q != zero) {
      if (MlTree_Regular(cur)->candidate) {
        if (!SynthUseCandidate(table, dd, cur, verbosity)) {
          FREE(support);
          bdd_recursive_deref_zdd(dd, d);
          return(NULL);
        }
      }
      *found = 1;
      *comp_d_flag = flag;
      *comp_d_tree = cur;
      bdd_recursive_deref_zdd(dd, d);
      d = candy;
      bdd_ref(d);
      break;
    }
    if (flag == 0 && cur->complement)
      flag = 1;
    else {
      cur = cur->next;
      flag = 0;
    }
  }

  FREE(support);
  return(d);
}


MlTree *
SynthGetFactorTreeWithCommonDivisor(bdd_manager *dd,
                                    st_table *table,
                                    MlTree *(* factoring_func)(bdd_manager *,
                                                               st_table *,
                                                               bdd_node *, int,
                                                               int *, MlTree *,
                                                               int, MlTree *,
                                                               int),
                                    bdd_node *f,
                                    bdd_node *d,
                                    int level,
                                    int *ref,
                                    int verbosity)
{
  bdd_node      *zero = bdd_read_zero(dd);
  bdd_node      *cd;
  bdd_node      *q;
  MlTree        *tree, *q_tree, *d_tree, *r_tree;
  int           q_ref, d_ref, r_ref;
  MlTree        *comp_q_tree = (MlTree *)NULL;
  MlTree        *comp_d_tree = (MlTree *)NULL;
  MlTree        *comp_r_tree = (MlTree *)NULL;
  int           q_tree_exist;
  MlTree        *tmp_tree;
  char          message[120];
  char          space[100];
  char          comp_mess[120];
  int           comp_flag;

  q_ref = d_ref = r_ref = 0;

  if (verbosity > 1) {
    SynthGetSpaceString(space, level * 2, 80);
    sprintf(message, "%s[%d]out : ", space, level);
  }

  cd = SynthZddCommonDivisor(dd, f);
  if (cd) {
    bdd_recursive_deref_zdd(dd, d);
    d = cd;
    bdd_ref(d);
    q = (* SynthGetZddDivideFunc())(dd, f, d);
    if (!q) {
      bdd_recursive_deref_zdd(dd, d);
      return(NULL);
    }
    bdd_ref(q);

    d_tree = (MlTree *)NULL;
    if (st_lookup(table, (char *)d, &d_tree)) {
      SynthSetSharedFlag(dd, d_tree);
      if (MlTree_Regular(d_tree)->candidate) {
        if (!SynthUseCandidate(table, dd, d_tree, verbosity)) {
          bdd_recursive_deref_zdd(dd, d);
          bdd_recursive_deref_zdd(dd, q);
          return(NULL);
        }
      }
      if (MlTree_IsComplement(d_tree)) {
        d_tree = MlTree_Regular(d_tree);
        comp_d_tree = d_tree;
      }
      d_ref = 1;
    } else {
      d_tree = SynthFindOrCreateMlTree(table, dd, d, 1, 0, &d_ref, verbosity);
      if (!d_tree) {
        bdd_recursive_deref_zdd(dd, d);
        bdd_recursive_deref_zdd(dd, q);
        return(NULL);
      }
      if (MlTree_IsComplement(d_tree)) {
        d_tree = MlTree_Regular(d_tree);
        comp_d_tree = d_tree;
      }
      tmp_tree = d_tree;
      d_tree = SynthCheckAndMakeComplement(dd, table, d_tree, &comp_flag,
                                           verbosity);
      if (!d_tree) {
        bdd_recursive_deref_zdd(dd, d);
        bdd_recursive_deref_zdd(dd, q);
        return(NULL);
      } else if (d_tree == tmp_tree) {
        if (d_ref == 0)
          SynthPutMlTreeInList(dd, d_tree, 0);
      } else {
        if (comp_flag)
          comp_d_tree = d_tree;
        d_ref = 1;
      }
    }

    q_tree = (MlTree *)NULL;
    if (st_lookup(table, (char *)q, &q_tree)) {
      SynthSetSharedFlag(dd, q_tree);
      if (MlTree_Regular(q_tree)->candidate) {
        if (!SynthUseCandidate(table, dd, q_tree, verbosity)) {
          bdd_recursive_deref_zdd(dd, d);
          bdd_recursive_deref_zdd(dd, q);
          return(NULL);
        }
      }
      if (MlTree_IsComplement(q_tree)) {
        q_tree = MlTree_Regular(q_tree);
        comp_q_tree = q_tree;
        q_tree = (MlTree *)NULL;
      }
    }

    if (verbosity > 1)
      (void) fprintf(vis_stdout,"%s[%d] quotient\n", space, level);
    q_tree_exist = 0;
    if (q_tree) {
      q_ref = 1;
      q_tree_exist = 1;
    } else if (comp_q_tree) {
      q_tree = comp_q_tree;
      q_ref = 1;
      if (verbosity > 1) {
        sprintf(comp_mess, "%s\t(C) : ", space);
        SynthPrintZddTreeMessage(dd, q, comp_mess);
      }
    } else {
      q_tree = (* factoring_func)(dd, table, q, level + 1,&q_ref,
                                  NULL, 0, NULL, verbosity);
      if (!q_tree) {
        bdd_recursive_deref_zdd(dd, d);
        bdd_recursive_deref_zdd(dd, q);
        return(NULL);
      }
      if (MlTree_IsComplement(q_tree)) {
        q_tree = MlTree_Regular(q_tree);
        comp_q_tree = q_tree;
      } else
        bdd_ref(q_tree->node);
    }
    tmp_tree = q_tree;
    q_tree = SynthCheckAndMakeComplement(dd, table, q_tree, &comp_flag,
                                         verbosity);
    if (!q_tree) {
      bdd_recursive_deref_zdd(dd, d);
      bdd_recursive_deref_zdd(dd, q);
      if (comp_q_tree != q_tree)
        bdd_recursive_deref_zdd(dd, q_tree->node);
      return(NULL);
    } else if (q_tree != tmp_tree) {
      if (comp_flag)
        comp_q_tree = q_tree;
      q_ref = 1;
    }

    r_tree = SynthFindOrCreateMlTree(table, dd, zero, 1, 0, &r_ref, verbosity);
    if (!r_tree) {
      bdd_recursive_deref_zdd(dd, d);
      bdd_recursive_deref_zdd(dd, q);
      if (comp_q_tree != q_tree)
        bdd_recursive_deref_zdd(dd, q_tree->node);
      return(NULL);
    }
    if (MlTree_IsComplement(r_tree)) {
      r_tree = MlTree_Regular(r_tree);
      comp_r_tree = r_tree;
    }
    tmp_tree = r_tree;
    r_tree = SynthCheckAndMakeComplement(dd, table, r_tree, &comp_flag,
                                         verbosity);
    if (!r_tree) {
      bdd_recursive_deref_zdd(dd, d);
      bdd_recursive_deref_zdd(dd, q);
      if (comp_q_tree != q_tree)
        bdd_recursive_deref_zdd(dd, q_tree->node);
      return(NULL);
    } else if (r_tree != tmp_tree) {
      if (comp_flag)
        comp_r_tree = r_tree;
      r_ref = 1;
    }

    bdd_recursive_deref_zdd(dd, q);
    bdd_recursive_deref_zdd(dd, d);
    if ((!q_tree_exist) && (!comp_q_tree))
      bdd_recursive_deref_zdd(dd, q_tree->node);

    tree = SynthFindOrCreateMlTree(table, dd, f, 0, 0, ref, verbosity);
    if (!tree)
      return(NULL);
    if (*ref == 1)
      (void) fprintf(vis_stdout, "** synth warning: May be duplicate.\n");
    tree->q = q_tree;
    tree->d = d_tree;
    tree->r = r_tree;
    if (comp_q_tree)
      tree->q_comp = 1;
    if (comp_d_tree)
      tree->d_comp = 1;
    if (comp_r_tree)
      tree->r_comp = 1;
    tree->q_ref = q_ref;
    tree->d_ref = d_ref;
    tree->r_ref = r_ref;
    if (verbosity > 1)
      SynthPrintMlTreeMessage(dd, tree, message);
    SynthPutMlTreeInList(dd, tree, 0);
    if (VerifyTreeMode) {
      SynthVerifyTree(dd, tree, 0);
      SynthVerifyMlTable(dd, table);
    }
    return(tree);
  } else if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
    bdd_recursive_deref_zdd(dd, d);
  return(NULL);
}


MlTree *
SynthPostFactorTree(bdd_manager *dd,
                    st_table *table,
                    bdd_node *f,
                    bdd_node *q,
                    bdd_node *d,
                    MlTree *bring,
                    MlTree *comp_d_tree,
                    int comp_d_flag,
                    char *message,
                    int *ref,
                    int verbosity)
{
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *r;
  MlTree        *tree, *r_tree, *tmp_tree;
  int           q_ref, r_ref;
  MlTree        *comp_r_tree = (MlTree *)NULL;
  int           comp_flag;

  q_ref = r_ref = 0;

  r = bdd_zdd_diff(dd, f, d);
  if (!r)
    return(NULL);
  bdd_ref(r);
  r_tree = (MlTree *)NULL;
  if (st_lookup(table, (char *)r, &r_tree)) {
    SynthSetSharedFlag(dd, r_tree);
    if (MlTree_Regular(r_tree)->candidate) {
      if (!SynthUseCandidate(table, dd, r_tree, verbosity)) {
        bdd_recursive_deref_zdd(dd, r);
        return(NULL);
      }
    }
    if (MlTree_IsComplement(r_tree)) {
      r_tree = MlTree_Regular(r_tree);
      comp_r_tree = r_tree;
    }
    r_ref = 1;
  } else {
    r_tree = SynthFindOrCreateMlTree(table, dd, r, 1, 0, &r_ref, verbosity);
    if (!r_tree) {
      bdd_recursive_deref_zdd(dd, r);
      return(NULL);
    }
    if (MlTree_IsComplement(r_tree)) {
      comp_r_tree = MlTree_Regular(r_tree);
      r_tree = comp_r_tree;
    }
    tmp_tree = r_tree;
    r_tree = SynthCheckAndMakeComplement(dd, table, r_tree, &comp_flag,
                                         verbosity);
    if (!r_tree) {
      bdd_recursive_deref_zdd(dd, r);
      return(NULL);
    } else if (r_tree == tmp_tree) {
      if (r_ref == 0)
        SynthPutMlTreeInList(dd, r_tree, 0);
    } else {
      if (comp_flag)
        comp_r_tree = r_tree;
      r_ref = 1;
    }
  }
  bdd_recursive_deref_zdd(dd, r);

  if (bring)
    tree = bring;
  else {
    tree = SynthFindOrCreateMlTree(table, dd, f, 0, 0, ref, verbosity);
    if (!tree)
      return(NULL);
    if (*ref)
      (void)fprintf(vis_stdout, "** synth warning: May be duplicate.\n");
  }
  tree->q = SynthFindOrCreateMlTree(table, dd, one, 1, 0, &q_ref, verbosity);
  if (!tree->q)
    return(NULL);
  if (MlTree_IsComplement(tree->q)) {
    tree->q = MlTree_Regular(tree->q);
    tree->q_comp = 1;
  }
  tree->d = comp_d_tree;
  tree->r = r_tree;
  tree->d_comp = comp_d_flag;
  if (comp_r_tree)
    tree->r_comp = 1;
  tree->q_ref = q_ref;
  tree->d_ref = 1;
  tree->r_ref = r_ref;
  if (verbosity > 1)
    SynthPrintMlTreeMessage(dd, tree, message);
  if (bring)
    bring->leaf = 0;
  else
    SynthPutMlTreeInList(dd, tree, 0);
  if (VerifyTreeMode) {
    SynthVerifyTree(dd, tree, 0);
    SynthVerifyMlTable(dd, table);
  }
  return(tree);
}


MlTree *
SynthFactorTreeRecur(bdd_manager *dd,
                     st_table *table,
                     MlTree *(* factoring_func)(bdd_manager *, st_table *,
                                                bdd_node *, int, int *,
                                                MlTree *, int, MlTree *, int),
                     bdd_node *f,
                     bdd_node *q,
                     bdd_node *d,
                     bdd_node *r,
                     bdd_node *m,
                     MlTree *q_tree,
                     MlTree *d_tree,
                     MlTree *r_tree,
                     MlTree *comp_q_tree,
                     MlTree *comp_d_tree,
                     MlTree *comp_r_tree,
                     MlTree *bring,
                     int level,
                     char *space,
                     char *message,
                     int *ref,
                     int verbosity)
{
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  int           q_tree_exist, d_tree_exist, r_tree_exist;
  MlTree        *m_tree;
  MlTree        *tree, *tmp_tree;
  int           q_ref, d_ref, r_ref, m_ref;
  char          comp_mess[120];
  int           comp_flag;

  q_ref = d_ref = r_ref = 0;

  if (verbosity > 1)
    (void) fprintf(vis_stdout,"%s[%d] quotient\n", space, level);
  q_tree_exist = 0;
  if (q_tree) {
    q_ref = 1;
    q_tree_exist = 1;
  } else if (comp_q_tree) {
    q_tree = comp_q_tree;
    q_ref = 1;
    if (verbosity > 1) {
      sprintf(comp_mess, "%s\t(C) : ", space);
      SynthPrintZddTreeMessage(dd, q, comp_mess);
    }
  } else {
    q_tree = (* factoring_func)(dd, table, q, level + 1,
                                &q_ref, NULL, 0, NULL, verbosity);
    if (!q_tree)
      return(NULL);
    if (MlTree_IsComplement(q_tree)) {
      q_tree = MlTree_Regular(q_tree);
      comp_q_tree = q_tree;
    } else
      bdd_ref(q_tree->node);
  }
  tmp_tree = q_tree;
  q_tree = SynthCheckAndMakeComplement(dd, table, q_tree, &comp_flag,
                                       verbosity);
  if (!q_tree) {
    if (comp_q_tree != tmp_tree)
      bdd_recursive_deref_zdd(dd, tmp_tree->node);
    if (q_ref == 0)
      SynthFreeMlTree(MlTree_Regular(tmp_tree), 1);
    return(NULL);
  } else if (q_tree != tmp_tree) {
    if (comp_flag)
      comp_q_tree = q_tree;
    q_ref = 1;
  }

  if (verbosity > 1)
    (void)fprintf(vis_stdout,"%s[%d] divisor\n", space, level);
  d_tree_exist = 0;
  if (d_tree) {
    d_ref = 1;
    d_tree_exist = 1;
  } else if (comp_d_tree) {
    d_tree = comp_d_tree;
    d_ref = 1;
    if (verbosity > 1) {
      sprintf(comp_mess, "%s\t(C) : ", space);
      SynthPrintZddTreeMessage(dd, d, comp_mess);
    }
  } else {
    d_tree = (* factoring_func)(dd, table, d, level + 1, &d_ref,
                                NULL, 0, NULL, verbosity);
    if (!d_tree) {
      if (comp_q_tree != q_tree)
        bdd_recursive_deref_zdd(dd, q_tree->node);
      if (q_ref == 0)
        SynthFreeMlTree(MlTree_Regular(q_tree), 1);
      return(NULL);
    }
    if (MlTree_IsComplement(d_tree)) {
      d_tree = MlTree_Regular(d_tree);
      comp_d_tree = d_tree;
    } else
      bdd_ref(d_tree->node);
  }
  tmp_tree = d_tree;
  d_tree = SynthCheckAndMakeComplement(dd, table, d_tree, &comp_flag,
                                       verbosity);
  if (!d_tree) {
    if (comp_q_tree != q_tree)
      bdd_recursive_deref_zdd(dd, q_tree->node);
    if (comp_d_tree != tmp_tree)
      bdd_recursive_deref_zdd(dd, tmp_tree->node);
    if (q_ref == 0)
      SynthFreeMlTree(MlTree_Regular(q_tree), 1);
    if (d_ref == 0)
      SynthFreeMlTree(MlTree_Regular(tmp_tree), 1);
    return(NULL);
  } else if (d_tree != tmp_tree) {
    if (comp_flag)
      comp_d_tree = d_tree;
    d_ref = 1;
  }

  m_tree = (MlTree *)NULL;
  m_ref = 0;
  if (UseMtree && m != f) {
    m_tree = SynthFindOrCreateMlTree(table, dd, m, 0, 1, &m_ref, verbosity);
    if (!m_tree) {
      if (comp_q_tree != q_tree)
        bdd_recursive_deref_zdd(dd, q_tree->node);
      if (comp_d_tree != d_tree)
        bdd_recursive_deref_zdd(dd, d_tree->node);
      if (q_ref == 0)
        SynthFreeMlTree(MlTree_Regular(q_tree), 1);
      if (d_ref == 0)
        SynthFreeMlTree(MlTree_Regular(d_tree), 1);
      return(NULL);
    }
    if (m_ref == 0) {
      m_tree->q = q_tree;
      m_tree->d = d_tree;
      m_tree->r = (MlTree *)NULL;
      if (comp_q_tree)
        m_tree->q_comp = 1;
      if (comp_d_tree)
        m_tree->d_comp = 1;
      m_tree->q_ref = q_ref;
      m_tree->d_ref = d_ref;
      m_tree->r_ref = 0;

      tmp_tree = m_tree;
      m_tree = SynthCheckAndMakeComplement(dd, table, m_tree, &comp_flag,
                                           verbosity);
      if (!m_tree) {
        if (comp_q_tree != q_tree)
          bdd_recursive_deref_zdd(dd, q_tree->node);
        if (comp_d_tree != d_tree)
          bdd_recursive_deref_zdd(dd, d_tree->node);
        if (q_ref == 0)
          SynthFreeMlTree(MlTree_Regular(q_tree), 1);
        if (d_ref == 0)
          SynthFreeMlTree(MlTree_Regular(d_tree), 1);
        return(NULL);
      } else if (m_tree == tmp_tree)
        SynthPutMlTreeInList(dd, m_tree, 1);
      else {
        if (m_tree->candidate)
          SynthPutMlTreeInList(dd, m_tree, 1);
        else
          m_tree = NIL(MlTree);
      }
      if (m_tree && VerifyTreeMode) {
        SynthVerifyTree(dd, m_tree, 0);
        SynthVerifyMlTable(dd, table);
      }
    }
  }

  if (verbosity > 1)
    (void)fprintf(vis_stdout,"%s[%d] remainder\n", space, level);
  r_tree_exist = 0;
  if (r_tree) {
    r_ref = 1;
    r_tree_exist = 1;
  } else if (comp_r_tree) {
    r_tree = comp_r_tree;
    r_ref = 1;
    if (verbosity > 1) {
      sprintf(comp_mess, "%s\t(C) : ", space);
      SynthPrintZddTreeMessage(dd, r, comp_mess);
    }
  } else if (comp_d_tree) {
    r_tree = (* factoring_func)(dd, table, r, level + 1,
                                &r_ref, NULL, 0, NULL, verbosity);
    if (!r_tree) {
      if (comp_q_tree != q_tree)
        bdd_recursive_deref_zdd(dd, q_tree->node);
      if (comp_d_tree != d_tree)
        bdd_recursive_deref_zdd(dd, d_tree->node);
      if (q_ref == 0)
        SynthFreeMlTree(MlTree_Regular(q_tree), 1);
      if (d_ref == 0)
        SynthFreeMlTree(MlTree_Regular(d_tree), 1);
      if (m_tree && m_ref == 0)
        SynthFreeMlTree(MlTree_Regular(m_tree), 1);
      return(NULL);
    }
    if (MlTree_IsComplement(r_tree)) {
      r_tree = MlTree_Regular(r_tree);
      comp_r_tree = r_tree;
    } else
      bdd_ref(r_tree->node);
  } else {
    if (Resubstitution) {
      r_tree = (* factoring_func)(dd, table, r, level + 1,
                                  &r_ref, d_tree, 1, NULL, verbosity);
      if (!r_tree && (bdd_read_reordered_field(dd) || noMemoryFlag == 1)) {
        if (comp_q_tree != q_tree)
          bdd_recursive_deref_zdd(dd, q_tree->node);
        if (comp_d_tree != d_tree)
          bdd_recursive_deref_zdd(dd, d_tree->node);
        if (q_ref == 0)
          SynthFreeMlTree(MlTree_Regular(q_tree), 1);
        if (d_ref == 0)
          SynthFreeMlTree(MlTree_Regular(d_tree), 1);
        if (m_tree && m_ref == 0)
          SynthFreeMlTree(MlTree_Regular(m_tree), 1);
        return(NULL);
      }
    }
    if (!r_tree) {
      r_tree = (* factoring_func)(dd, table, r, level + 1,
                                  &r_ref, NULL, 0, NULL, verbosity);
      if (!r_tree) {
        if (comp_q_tree != q_tree)
          bdd_recursive_deref_zdd(dd, q_tree->node);
        if (comp_d_tree != d_tree)
          bdd_recursive_deref_zdd(dd, d_tree->node);
        if (q_ref == 0)
          SynthFreeMlTree(MlTree_Regular(q_tree), 1);
        if (d_ref == 0)
          SynthFreeMlTree(MlTree_Regular(d_tree), 1);
        if (m_tree && m_ref == 0)
          SynthFreeMlTree(MlTree_Regular(m_tree), 1);
        return(NULL);
      }
    } else {
      if (r != one && r != zero)
        SynthSetSharedFlag(dd, d_tree);
    }
    if (MlTree_IsComplement(r_tree)) {
      r_tree = MlTree_Regular(r_tree);
      comp_r_tree = r_tree;
    } else
      bdd_ref(r_tree->node);
  }
  if (RemainderComplement) {
    tmp_tree = r_tree;
    r_tree = SynthCheckAndMakeComplement(dd, table, r_tree, &comp_flag,
                                         verbosity);
    if (!r_tree) {
      if (comp_q_tree != q_tree)
        bdd_recursive_deref_zdd(dd, q_tree->node);
      if (comp_d_tree != d_tree)
        bdd_recursive_deref_zdd(dd, d_tree->node);
      if (comp_r_tree != tmp_tree)
        bdd_recursive_deref_zdd(dd, tmp_tree->node);
      if (q_ref == 0)
        SynthFreeMlTree(MlTree_Regular(q_tree), 1);
      if (d_ref == 0)
        SynthFreeMlTree(MlTree_Regular(d_tree), 1);
      if (r_ref == 0)
        SynthFreeMlTree(MlTree_Regular(tmp_tree), 1);
      if (m_tree && m_ref == 0)
        SynthFreeMlTree(MlTree_Regular(m_tree), 1);
      return(NULL);
    } else if (r_tree != tmp_tree) {
      if (comp_flag)
        comp_r_tree = r_tree;
      r_ref = 1;
    }
  }

  if ((!q_tree_exist) && (!comp_q_tree))
    bdd_recursive_deref_zdd(dd, q_tree->node);
  if ((!d_tree_exist) && (!comp_d_tree))
    bdd_recursive_deref_zdd(dd, d_tree->node);
  if ((!r_tree_exist) && (!comp_r_tree))
    bdd_recursive_deref_zdd(dd, r_tree->node);

  if (bring) {
    tree = bring;
    tree->leaf = 0;
    tree->q = q_tree;
    tree->d = d_tree;
    tree->r = r_tree;
    if (comp_q_tree)
      tree->q_comp = 1;
    if (comp_d_tree)
      tree->d_comp = 1;
    if (comp_r_tree)
      tree->r_comp = 1;
    tree->q_ref = q_ref;
    tree->d_ref = d_ref;
    tree->r_ref = r_ref;
    if (UseMtree && m_tree && m_ref == 0) {
      MlTree_Regular(m_tree)->r = tree;
      if (m_tree->r->id == 0) {
        assert(0);
        /*
        if (!SynthUseCandidate(table, dd, m_tree, verbosity)) {
          SynthFreeMlTree(MlTree_Regular(m_tree), 1);
          return(NULL);
        }
        */
      }
    }
    if (verbosity > 1)
      SynthPrintMlTreeMessage(dd, tree, message);
    if (VerifyTreeMode) {
      SynthVerifyTree(dd, tree, 0);
      SynthVerifyMlTable(dd, table);
    }
    return(tree);
  }

  tree = SynthFindOrCreateMlTree(table, dd, f, 0, 0, ref, verbosity);
  if (!tree) {
    if (q_ref == 0)
      SynthFreeMlTree(MlTree_Regular(q_tree), 1);
    if (d_ref == 0)
      SynthFreeMlTree(MlTree_Regular(d_tree), 1);
    if (r_ref == 0)
      SynthFreeMlTree(MlTree_Regular(r_tree), 1);
    if (m_tree && m_ref == 0)
      SynthFreeMlTree(MlTree_Regular(m_tree), 1);
    return(NULL);
  }
  if (*ref == 1)
    (void)fprintf(vis_stdout, "** synth warning: May be duplicate.\n");
  tree->q = q_tree;
  tree->d = d_tree;
  tree->r = r_tree;
  if (comp_q_tree)
    tree->q_comp = 1;
  if (comp_d_tree)
    tree->d_comp = 1;
  if (comp_r_tree)
    tree->r_comp = 1;
  tree->q_ref = q_ref;
  tree->d_ref = d_ref;
  tree->r_ref = r_ref;
  if (UseMtree && m_tree && m_ref == 0) {
    MlTree_Regular(m_tree)->r = tree;
    if (m_tree->r->id == 0) {
      assert(0);
      /*
      if (!SynthUseCandidate(table, dd, m_tree, verbosity)) {
        SynthFreeMlTree(MlTree_Regular(tree), 1);
        SynthFreeMlTree(MlTree_Regular(m_tree), 1);
        return(NULL);
      }
      */
    }
  }
  if (verbosity > 1)
    SynthPrintMlTreeMessage(dd, tree, message);
  SynthPutMlTreeInList(dd, tree, 0);
  if (VerifyTreeMode) {
    SynthVerifyTree(dd, tree, 0);
    SynthVerifyMlTable(dd, table);
  }
  return(tree);
}


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

static int
CountZddLeafLiterals(bdd_manager *dd,
                     bdd_node *node)
{
  int   i, *support;
  int   count = 0;
  int   sizeZ = bdd_num_zdd_vars(dd);

  support = ALLOC(int, sizeZ);
  if (!support)
    return(-1);
  (void)memset((void *)support, 0, sizeof(int) * sizeZ);
  SynthZddSupportStep(bdd_regular(node), support);
  SynthZddClearFlag(bdd_regular(node));
  for (i = 0; i < sizeZ; i++) {
    if (support[i])
      count++;
  }
  FREE(support);
  return(count);
}