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

  FileName    [synthGen.c]

  PackageName [synth]

  Synopsis    [Generic multilevel 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: synthGen.c,v 1.36 2005/05/11 20:17:21 hhhan Exp $";

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


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


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


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

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 MlTree * LiteralFactoringTree(bdd_manager *dd, st_table *table, bdd_node *f, bdd_node *c, int level, int *ref, MlTree *bring, int verbosity);
static bdd_node * BestLiteral(bdd_manager *dd, bdd_node *f, bdd_node *c);
static int IsCubeFree(bdd_manager *dd, bdd_node *f);
static bdd_node * CommonCube(bdd_manager *dd, bdd_node *f);

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


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



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

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

  Synopsis [Factorizes a function using a generic method.]

  Description [Factorizes a function using a generic method. This
  algorithm came from the book "Logic Synthesis and Verification Algorithms"
  by Gary Hachtel and Fabio Somenzi. 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 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     [SynthSimpleFactorTree]

******************************************************************************/
MlTree *
SynthGenericFactorTree(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, *c;
  MlTree	*tree, *q_tree, *d_tree, *r_tree;
  int		q_ref, d_ref, r_ref;
  int		ncubes;
  bdd_node	*tmp;
  char		message[80];
  char		space[80];
  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,
		 SynthGenericFactorTree, f, d, level, ref, verbosity);
      if (tree)
	return(tree);
      if (bdd_read_reordered_field(dd) || noMemoryFlag == 1) {
	bdd_recursive_deref_zdd(dd, d);
	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;
	comp_d_flag = 1;
	d_tree = (MlTree *)NULL;
      }
      else
	comp_d_flag = 0;
    }
  } 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);
  }

  ncubes = bdd_zdd_count(dd, q);
  if (ncubes == 1) {
    if (d_tree || comp_d_tree) {
      m = (* SynthGetZddProductFunc())(dd, q, d);
      if (!m) {
	bdd_recursive_deref_zdd(dd, d);
	bdd_recursive_deref_zdd(dd, q);
	return(NULL);
      }
      bdd_ref(m);
      bdd_recursive_deref_zdd(dd, d);
      r = bdd_zdd_diff(dd, f, m);
      bdd_recursive_deref_zdd(dd, m);
      if (!r) {
	bdd_recursive_deref_zdd(dd, q);
	return(NULL);
      }
      bdd_ref(r);
      bdd_recursive_deref_zdd(dd,r);
      if (r == zero) {
	if (!d_tree)
	  d_tree = comp_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, q);
	      return(NULL);
	    }
	  }
	  if (MlTree_IsComplement(q_tree)) {
	    q_tree = MlTree_Regular(q_tree);
	    comp_q_tree = q_tree;
	  }
	  q_ref = 1;
	} else {
	  q_tree = SynthFindOrCreateMlTree(table, dd, q, 1,
					   0, &q_ref, verbosity);
	  if (!q_tree) {
	    bdd_recursive_deref_zdd(dd, q);
	    return(NULL);
	  }
	  if (MlTree_IsComplement(q_tree)) {
	    comp_q_tree = MlTree_Regular(q_tree);
	    q_tree = comp_q_tree;
	  }
	  tmp_tree = q_tree;
	  q_tree = SynthCheckAndMakeComplement(dd, table, q_tree, &comp_flag,
					       verbosity);
	  if (!q_tree) {
	    bdd_recursive_deref_zdd(dd, q);
	    return(NULL);
	  } else if (q_tree == tmp_tree) {
	    if (q_ref == 0)
	      SynthPutMlTreeInList(dd, q_tree, 0);
	  } else {
	    if (comp_flag)
	      comp_q_tree = q_tree;
	    q_ref = 1;
	  }
	}
	bdd_recursive_deref_zdd(dd, q);

	if (bring) {
	  tree = bring;
	  tree->leaf = 0;
	  tree->q = q_tree;
	  tree->d = d_tree;
	  tree->r = SynthFindOrCreateMlTree(table, dd, zero, 
					    1, 0, &r_ref, verbosity);
	  if (!tree->r)
	    return(NULL);
	  if (MlTree_IsComplement(tree->r)) {
	    tree->r = MlTree_Regular(tree->r);
	    tree->r_comp = 1;
	  }
	  if (comp_q_tree)
	    tree->q_comp = 1;
	  if (comp_d_flag)
	    tree->d_comp = 1;
	  tree->q_ref = q_ref;
	  tree->d_ref = d_ref;
	  tree->r_ref = r_ref;
	  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)
	  return(NULL);
	if (*ref)
	  (void) fprintf(vis_stdout,
			 "** synth warning: May be duplicate.\n");
	tree->q = q_tree;
	tree->d = d_tree;
	tree->r = SynthFindOrCreateMlTree(table, dd, zero, 1, 
					  0, &r_ref, verbosity);
	if (!tree->r)
	  return(NULL);
	if (MlTree_IsComplement(tree->r)) {
	  tree->r = MlTree_Regular(tree->r);
	  tree->r_comp = 1;
	}
	if (comp_q_tree)
	  tree->q_comp = 1;
	if (comp_d_flag)
	  tree->d_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
      bdd_recursive_deref_zdd(dd, d);

    tree = LiteralFactoringTree(dd, table, f, q, level + 1, ref, 
				bring, verbosity);
    if (!tree) {
      bdd_recursive_deref_zdd(dd, q);
      return(NULL);
    }
    tmp_tree = tree;
    tree = SynthCheckAndMakeComplement(dd, table, tree, &comp_flag, verbosity);
    if (!tree) {
      bdd_recursive_deref_zdd(dd, q);
      return(NULL);
    } else if (tree != tmp_tree) {
      *ref = 1;
      if (comp_flag)
	tree = MlTree_Not(tree);
    }
    bdd_recursive_deref_zdd(dd, q);

    if (verbosity > 1)
      SynthPrintMlTreeMessage(dd, tree, message);
    return(tree);
  }
  bdd_recursive_deref_zdd(dd, d);

  d_tree = comp_d_tree = (MlTree *)NULL;

  tmp = q;
  q = SynthMakeCubeFree(dd, q);
  if (!q) {
    bdd_recursive_deref_zdd(dd,tmp);
    return(NULL);
  }
  bdd_ref(q);
  bdd_recursive_deref_zdd(dd,tmp);

  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, q);
	return(NULL);
      }
    }
    if (MlTree_IsComplement(q_tree)) {
      q_tree = MlTree_Regular(q_tree);
      comp_q_tree = q_tree;
      q_tree = (MlTree *)NULL;
    }
  }

  d = (* SynthGetZddDivideFunc())(dd, f, q);
  if (!d) {
    bdd_recursive_deref_zdd(dd, q);
    return(NULL);
  }
  bdd_ref(d);
  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_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;
    }
  }

  if (IsCubeFree(dd, d)) {
    tree = SynthFactorTreeRecur(dd, table, SynthGenericFactorTree,
				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);
    return(tree);
  }

  bdd_recursive_deref_zdd(dd, q);
  bdd_recursive_deref_zdd(dd, r);

  c = CommonCube(dd, d);
  if (!c) {
    bdd_recursive_deref_zdd(dd, d);
    return(NULL);
  }
  bdd_ref(c);
  bdd_recursive_deref_zdd(dd, d);
  tree = LiteralFactoringTree(dd, table, f, c, level + 1,
			      ref, bring, verbosity);
  if (!tree) {
    bdd_recursive_deref_zdd(dd, c);
    return(NULL);
  }
  tmp_tree = tree;
  tree = SynthCheckAndMakeComplement(dd, table, tree, &comp_flag, verbosity);
  if (!tree) {
    bdd_recursive_deref_zdd(dd, c);
    if (*ref == 0)
      SynthFreeMlTree(MlTree_Regular(tree), 1);
    return(NULL);
  } else if (tree != tmp_tree) {
    *ref = 1;
    if (comp_flag)
      tree = MlTree_Not(tree);
  }
  bdd_recursive_deref_zdd(dd, c);

  if (verbosity > 1)
    SynthPrintMlTreeMessage(dd, tree, message);
  if (VerifyTreeMode) {
    SynthVerifyTree(dd, tree, 0);
    SynthVerifyMlTable(dd, table);
  }
  return(tree);
}


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

  Synopsis [Makes a node cube-free.]

  Description [Makes a node cube-free. Eliminates the literals that appear
  in all the cubes.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
bdd_node *
SynthMakeCubeFree(bdd_manager *dd,
		  bdd_node *f)
{
  int		i, v;
  int		nvars, max_count, max_pos = 0;
  int		*count;
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*divisor, *node;
  bdd_node	*tmp1, *tmp2;
  int		ncubes;

  if (f == one || f == zero)
    return(f);

  /* Compare the number of occurrences of each literal to the number of
   * cubes in the cover. If no literal appears more than once, or if no
   * literal appears in all cubes, f is already cube-free.
   */
  ncubes = bdd_zdd_count(dd, f);
  v = -1;
  max_count = 1;
  nvars = bdd_num_zdd_vars(dd);
  count = ALLOC(int, nvars);
  (void)memset((void *)count, 0, sizeof(int) * nvars);
  SynthCountLiteralOccurrence(dd, f, count);
  for (i = 0; i < nvars; i++) {
    if (count[i] > max_count) {
      v = i;
      max_count = count[i];
      max_pos = i;
    }
  }
  if (v == -1 || max_count < ncubes) {
    FREE(count);
    return(f);
  }

  /* Divide the cover by the first literal appearing in all cubes. */
  node = bdd_zdd_get_node(dd, v, one, zero);
  if (!node) {
    FREE(count);
    return(NULL);
  }
  bdd_ref(node);
  divisor = (* SynthGetZddDivideFunc())(dd, f, node);
  if (!divisor) {
    bdd_recursive_deref_zdd(dd, node);
    FREE(count);
    return(NULL);
  }
  bdd_ref(divisor);
  bdd_recursive_deref_zdd(dd, node);

  /* Divide the cover by the remaining literals appearing in all cubes. */
  for (i = max_pos + 1; i < nvars; i++) {
    if (count[i] == max_count) {
      tmp1 = divisor;
      tmp2 = bdd_zdd_get_node(dd, i, one, zero);
      if (!tmp2) {
	FREE(count);
	bdd_recursive_deref_zdd(dd, tmp1);
	return(NULL);
      }
      bdd_ref(tmp2);
      divisor = (* SynthGetZddDivideFunc())(dd, divisor, tmp2);
      if (!divisor) {
	FREE(count);
	bdd_recursive_deref_zdd(dd, tmp1);
	bdd_recursive_deref_zdd(dd, tmp2);
	return(NULL);
      }
      bdd_ref(divisor);
      bdd_recursive_deref_zdd(dd, tmp1);
      bdd_recursive_deref_zdd(dd, tmp2);
    }
  }
  FREE(count);
  bdd_deref(divisor);
  return(divisor);
}


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

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

  Synopsis [Factorizes a node using literal factoring.]

  Description [Factorizes a node using literal factoring.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static MlTree *
LiteralFactoringTree(bdd_manager *dd,
		     st_table *table,
		     bdd_node *f,
		     bdd_node *c,
		     int level,
		     int *ref,
		     MlTree *bring,
		     int verbosity)
{
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*l, *q, *r;
  bdd_node	*m;
  char		message[80];
  char		space[80];
  MlTree	*tree, *q_tree, *d_tree, *r_tree;
  int		q_ref, d_ref, r_ref, m_ref;
  char		comp_mess[120];
  MlTree	*comp_q_tree = (MlTree *)NULL;
  MlTree	*comp_d_tree = (MlTree *)NULL;
  MlTree	*comp_r_tree = (MlTree *)NULL;
  MlTree	*m_tree;
  int		q_tree_exist, r_tree_exist;
  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);
  }

  l = BestLiteral(dd, f, c);
  if (!l)
    return(NULL);
  bdd_ref(l);
  d_tree = (MlTree *)NULL;
  if (st_lookup(table, (char *)l, &d_tree)) {
    SynthSetSharedFlag(dd, d_tree);
    if (MlTree_Regular(d_tree)->candidate) {
      if (!SynthUseCandidate(table, dd, d_tree, verbosity)) {
	bdd_recursive_deref_zdd(dd, l);
	return(NULL);
      }
    }
    if (MlTree_IsComplement(d_tree)) {
      d_tree = MlTree_Regular(d_tree);
      comp_d_tree = d_tree;
      d_tree = (MlTree *)NULL;
    }
  }
  q = (* SynthGetZddDivideFunc())(dd, f, l);
  if (!q) {
    bdd_recursive_deref_zdd(dd, l);
    return(NULL);
  }
  bdd_ref(q);
  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, l);
	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, l, q);
  if (!m) {
    bdd_recursive_deref_zdd(dd, l);
    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, l);
    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, l);
	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;
    }
  }

  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 = SynthGenericFactorTree(dd, table, q, level + 1, &q_ref,
				    NULL, 0, NULL, verbosity);
    if (!q_tree) {
      bdd_recursive_deref_zdd(dd, l);
      bdd_recursive_deref_zdd(dd, q);
      bdd_recursive_deref_zdd(dd, m);
      bdd_recursive_deref_zdd(dd, r);
      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, l);
    bdd_recursive_deref_zdd(dd, q);
    bdd_recursive_deref_zdd(dd, m);
    bdd_recursive_deref_zdd(dd, r);
    if (comp_q_tree != q_tree)
      bdd_recursive_deref_zdd(dd, tmp_tree->node);
    if (q_ref == 0)
      SynthFreeMlTree(MlTree_Regular(tmp_tree), 1);
    return(NULL);
  }
  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] literal\n", space, level);
  if (d_tree) {
    d_ref = 1;
    if (verbosity > 1) {
      sprintf(comp_mess, "%s\t(R) : ", space);
      SynthPrintZddTreeMessage(dd, l, comp_mess);
    }
  } 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, l, comp_mess);
    }
  } else {
    d_tree = SynthFindOrCreateMlTree(table, dd, l, 1, 0, &d_ref, verbosity);
    if (!d_tree) {
      bdd_recursive_deref_zdd(dd, l);
      bdd_recursive_deref_zdd(dd, q);
      bdd_recursive_deref_zdd(dd, m);
      bdd_recursive_deref_zdd(dd, r);
      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)) {
      comp_d_tree = MlTree_Regular(d_tree);
      d_tree = comp_d_tree;
    }
    if (verbosity > 1) {
      sprintf(comp_mess, "%s\t : ", space);
      SynthPrintZddTreeMessage(dd, l, comp_mess);
    }
    tmp_tree = d_tree;
    d_tree = SynthCheckAndMakeComplement(dd, table, d_tree, &comp_flag,
					 verbosity);
    if (!d_tree) {
      bdd_recursive_deref_zdd(dd, l);
      bdd_recursive_deref_zdd(dd, q);
      bdd_recursive_deref_zdd(dd, m);
      bdd_recursive_deref_zdd(dd, r);
      if (comp_q_tree != q_tree)
	bdd_recursive_deref_zdd(dd, q_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 (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;
    }
  }

  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) {
      bdd_recursive_deref_zdd(dd, l);
      bdd_recursive_deref_zdd(dd, q);
      bdd_recursive_deref_zdd(dd, m);
      bdd_recursive_deref_zdd(dd, r);
      if (comp_q_tree != q_tree)
	bdd_recursive_deref_zdd(dd, q_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) {
	bdd_recursive_deref_zdd(dd, l);
	bdd_recursive_deref_zdd(dd, q);
	bdd_recursive_deref_zdd(dd, m);
	bdd_recursive_deref_zdd(dd, r);
	if (comp_q_tree != q_tree)
	  bdd_recursive_deref_zdd(dd, q_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);
      }
    }
  }
  bdd_recursive_deref_zdd(dd, m);

  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 = SynthGenericFactorTree(dd, table, r, level + 1, &r_ref,
				    NULL, 0, NULL, verbosity);
    if (!r_tree) {
      bdd_recursive_deref_zdd(dd, l);
      bdd_recursive_deref_zdd(dd, q);
      bdd_recursive_deref_zdd(dd, r);
      if (comp_q_tree != q_tree)
	bdd_recursive_deref_zdd(dd, q_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 = SynthGenericFactorTree(dd, table, r, level + 1, 
				      &r_ref, d_tree, 1, NULL, verbosity);
      if (!r_tree && (bdd_read_reordered_field(dd) || noMemoryFlag)) {
	bdd_recursive_deref_zdd(dd, l);
	bdd_recursive_deref_zdd(dd, q);
	bdd_recursive_deref_zdd(dd, r);
	if (comp_q_tree != q_tree)
	  bdd_recursive_deref_zdd(dd, q_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 = SynthGenericFactorTree(dd, table, r, level + 1, 
				      &r_ref, NULL, 0, NULL, verbosity);
      if (!r_tree) {
	bdd_recursive_deref_zdd(dd, l);
	bdd_recursive_deref_zdd(dd, q);
	bdd_recursive_deref_zdd(dd, r);
	if (comp_q_tree != q_tree)
	  bdd_recursive_deref_zdd(dd, q_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) {
      bdd_recursive_deref_zdd(dd, l);
      bdd_recursive_deref_zdd(dd, q);
      bdd_recursive_deref_zdd(dd, r);
      if (comp_q_tree != q_tree)
	bdd_recursive_deref_zdd(dd, q_tree->node);
      if (comp_r_tree != r_tree)
	bdd_recursive_deref_zdd(dd, r_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(r_tree), 1);
      if (m_tree && m_ref == 0)
	SynthFreeMlTree(MlTree_Regular(m_tree), 1);
      return(NULL);
    }
    if (r_tree != tmp_tree) {
      if (comp_flag)
	comp_r_tree = r_tree;
      r_ref = 1;
    }
  }

  bdd_recursive_deref_zdd(dd, l);
  bdd_recursive_deref_zdd(dd, q);
  bdd_recursive_deref_zdd(dd, r);
  if ((!q_tree_exist) && (!comp_q_tree))
    bdd_recursive_deref_zdd(dd, q_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);
}

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

  Synopsis [Selects a literal which occurs in the largest number of
  cubes.]

  Description [Selects a literal which occurs in the largest number of
  cubes.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static bdd_node *
BestLiteral(bdd_manager *dd,
	    bdd_node *f,
	    bdd_node *c)
{
  int		i, v;
  int		nvars, max_count;
  int		*count_f, *count_c;
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*node;

  v = -1;
  max_count = 0;
  nvars = bdd_num_zdd_vars(dd);
  count_f = ALLOC(int, nvars);
  (void)memset((void *)count_f, 0, sizeof(int) * nvars);
  SynthCountLiteralOccurrence(dd, f, count_f);
  count_c = ALLOC(int, nvars);
  (void)memset((void *)count_c, 0, sizeof(int) * nvars);
  SynthCountLiteralOccurrence(dd, c, count_c);

  for (i = 0; i < nvars; i++) {
    if (count_c[i]) {
      if (count_f[i] > max_count) {
	v = i;
	max_count = count_f[i];
      }
    }
  }

  if (v == -1) {
    FREE(count_f);
    FREE(count_c);
    return(zero);
  }

  node = bdd_zdd_get_node(dd, v, one, zero);
  if (!node) {
    FREE(count_f);
    FREE(count_c);
    return(NULL);
  }
  FREE(count_f);
  FREE(count_c);
  return(node);
}


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

  Synopsis [Checks if a node is cube-free.]

  Description [Checks if a node is cube-free.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
IsCubeFree(bdd_manager *dd,
	   bdd_node *f)
{
  int		i, v;
  int		nvars, max_count;
  int		*count;
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  int		ncubes;

  if (f == one || f == zero)
    return(1);

  ncubes = bdd_zdd_count(dd, f);
  v = -1;
  max_count = 1;
  nvars = bdd_num_zdd_vars(dd);
  count = ALLOC(int, nvars);
  (void)memset((void *)count, 0, sizeof(int) * nvars);
  SynthCountLiteralOccurrence(dd, f, count);
  for (i = 0; i < nvars; i++) {
    if (count[i] > max_count) {
      v = i;
      max_count = count[i];
    }
  }
  FREE(count);

  if (v == -1 || max_count < ncubes)
    return(1);

  return(0);
}

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

  Synopsis [Returns the largest common cube.]

  Description [Returns the largest common cube.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static bdd_node *
CommonCube(bdd_manager *dd,
	   bdd_node *f)
{
  int		i, v;
  int		nvars, max_count, max_pos = 0;
  int		*count;
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*node;
  bdd_node	*tmp1, *tmp2;
  int		ncubes;

  if (f == one || f == zero) {
    return(f);
  }

  ncubes = bdd_zdd_count(dd, f);
  v = -1;
  max_count = 1;
  nvars = bdd_num_zdd_vars(dd);
  count = ALLOC(int, nvars);
  (void)memset((void *)count, 0, sizeof(int) * nvars);
  SynthCountLiteralOccurrence(dd, f, count);
  for (i = 0; i < nvars; i++) {
    if (count[i] > max_count) {
      v = i;
      max_count = count[i];
      max_pos = i;
    }
  }
  if (v == -1 || max_count < ncubes) {
    FREE(count);
    return(zero);
  }

  node = bdd_zdd_get_node(dd, v, one, zero);
  if (!node) {
    FREE(count);
    return(NULL);
  }
  bdd_ref(node);
  for (i = max_pos + 1; i < nvars; i++) {
    if (count[i] == max_count) {
      tmp1 = node;
      tmp2 = bdd_zdd_get_node(dd, i, one, zero);
      if (!tmp2) {
	FREE(count);
	bdd_recursive_deref_zdd(dd, tmp1);
	return(NULL);
      }
      bdd_ref(tmp2);
      node = (* SynthGetZddProductFunc())(dd, node, tmp2);
      if (!node) {
	FREE(count);
	bdd_recursive_deref_zdd(dd, tmp1);
	bdd_recursive_deref_zdd(dd, tmp2);
	return(NULL);
      }
      bdd_ref(node);
      bdd_recursive_deref_zdd(dd, tmp1);
      bdd_recursive_deref_zdd(dd, tmp2);
    }
  }
  FREE(count);
  bdd_deref(node);
  return(node);
}