/**CFile***********************************************************************

  FileName    [synthSimple.c]

  PackageName [synth]

  Synopsis    [Simple factorization method.]

  Description []

  Author      [In-Ho Moon, Balakrishna Kumthekar]

  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 "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;

/**AutomaticStart*************************************************************/

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

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

/**AutomaticEnd***************************************************************/


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


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

/**Function********************************************************************

  Synopsis [Factorizes a function using a simple method.]

  Description [Factorizes a function using a simple method. Here simple
  refers that this algorithm tries to factorize just recursively. First
  it finds a divisor, then finds quotient and remainder, and then recurs
  for each.  The argument table consists of a pair of bdd_node and MlTree,
  f is to be factorized, level is the depth of MlTree from top, ref returns 1
  if new MlTree is created for f, otherwise returns 0, comp_d_tree is usually
  NULL except when post factoring takes place(here post factoring is the
  case to factorize a leaf node by another leaf node and a leaf node is a node
  in which there is no divisor), comp_d_tree is a tree which is going to be
  used as a divisor and comp_d_flag is used to indicate which node is going
  to be used as a divisor between regular node and complement node, bring is
  usually NULL except post factoring: when we update an already existing
  tree by further factorization, we pass this tree to reuse it.]

  SideEffects []

  SeeAlso     [SynthGenericFactorTree]

******************************************************************************/
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);
}


/**Function********************************************************************

  Synopsis [Finds a bigger divisor in divisor list.]

  Description [Finds a bigger divisor in divisor list.]

  SideEffects []

  SeeAlso     [SynthSimpleFactorTree SynthGenericFactorTree]

******************************************************************************/
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);
}


/**Function********************************************************************

  Synopsis [Factorizes a function with a common divisor if it exists.]

  Description [Factorizes a function with a common divisor if it exists.]

  SideEffects []

  SeeAlso     [SynthSimpleFactorTree SynthGenericFactorTree]

******************************************************************************/
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);
}


/**Function********************************************************************

  Synopsis [Try to factorize between leaf trees.]

  Description [Try to factorize between leaf trees.]

  SideEffects []

  SeeAlso     [SynthSimpleFactorTree SynthGenericFactorTree]

******************************************************************************/
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);
}


/**Function********************************************************************

  Synopsis [Recursive procedure of SynthSimpleFactorTree and
  SynthGenericFactorTree.]

  Description [Recursive procedure of SynthSimpleFactorTree and
  SynthGenericFactorTree.]

  SideEffects []

  SeeAlso     [SynthSimpleFactorTree SynthGenericFactorTree]

******************************************************************************/
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                                            */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis [Counts the number of literals of a leaf node.]

  Description [Counts the number of literals of a leaf node.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
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);
}