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

  FileName    [synthUtil.c]

  PackageName [synth]

  Synopsis    [Functions to get or to print some information.]

  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: synthUtil.c,v 1.13 1998/08/19 22:51:49 mooni Exp $";

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


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


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


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

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

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

static int GetChildTree(bdd_manager *dd, bdd_node *f, char *eq);
static int GetChildMlTree(bdd_manager *dd, MlTree *tree, char *eq);
static bdd_node	* FindNodeWithIndex(bdd_node *node, int index);
static void GetZddCoverWithNameRecur(Ntk_Network_t *net, bdd_manager *dd, bdd_node *node, char *cover);

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


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


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

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

  Synopsis    [Prints the equation form of a node with internal names.]

  Description [Prints the equation form of a node with internal names.
  If the string length is bigger than MAX_EQ_LEN, the string is truncated.]

  SideEffects []

  SeeAlso     [SynthPrintZddTreeMessage]

******************************************************************************/
void
SynthPrintZddTree(bdd_manager *dd,
		  bdd_node *f)
{
  char	eq[MAX_EQ_LEN];

  GetChildTree(dd, f, eq);
  fprintf(vis_stdout, "%s\n", eq);
}


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

  Synopsis    [Prints the equation form of a node with internal names,
  preceded by a message.]

  Description [Prints the equation form of a node with internal names,
  preceded by a message. If the string length is bigger than MAX_EQ_LEN,
  the string is truncated.]

  SideEffects []

  SeeAlso     [SynthPrintMlTreeMessage]

******************************************************************************/
void
SynthPrintZddTreeMessage(bdd_manager *dd,
			 bdd_node *f,
			 char *mess)
{
  char	eq[MAX_EQ_LEN];

  GetChildTree(dd, f, eq);
  fprintf(vis_stdout, "%s%s\n", mess, eq);
}


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

  Synopsis    [Prints the equation form of a tree with internal names,
  preceded by a message.]

  Description [Prints the equation form of a tree with internal names,
  preceded by a message. If the string length is bigger than MAX_EQ_LEN,
  the string is truncated.]

  SideEffects []

  SeeAlso     [SynthPrintZddTreeMessage SynthPrintMlTreeWithName]

******************************************************************************/
void
SynthPrintMlTreeMessage(bdd_manager *dd,
			MlTree *tree,
			char *mess)
{
  char	eq[MAX_EQ_LEN];

  if (MlTree_IsComplement(tree)) {
    tree = MlTree_Regular(tree);
    GetChildMlTree(dd, tree, eq);
    (void) fprintf(vis_stdout, "%s%s'\n", mess, eq);
  } else {
    GetChildMlTree(dd, tree, eq);
    (void) fprintf(vis_stdout, "%s%s\n", mess, eq);
  }
}


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

  Synopsis    [Frees a multi-level tree recursively.]

  Description [Frees a multi-level tree recursively. If the argument flag
  is set to 0, it does not free recursively.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthFreeMlTree(MlTree *tree,
		int flag)
{
  if (!tree)
    return;

  if (tree->ref) {
    FREE(tree);
    return;
  }

  if (tree->support)
    FREE(tree->support);

  if (flag && tree->leaf == 0) {
    if (tree->q_ref == 0)
      SynthFreeMlTree(tree->q, flag);
    if (tree->d_ref == 0)
      SynthFreeMlTree(tree->d, flag);
    if (tree->r_ref == 0)
      SynthFreeMlTree(tree->r, flag);
  }

  FREE(tree);
}


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

  Synopsis    [Prints the equation form of a tree with original names
  and preceded by a message.]

  Description [Prints the equation form of a tree with original names
  and preceded by a message. If the string length is bigger than
  MAX_EQ_LEN, the string is truncated.]

  SideEffects []

  SeeAlso     [SynthPrintMlTreeMessage]

******************************************************************************/
void
SynthPrintMlTreeWithName(Ntk_Network_t *net,
			 bdd_manager *dd,
			 MlTree *tree,
			 char *mess)
{
  char	eq[MAX_EQ_LEN];

  SynthGetChildMlTreeWithName(net, dd, tree, eq);
  fprintf(vis_stdout, "%s%s\n", mess, eq);
}


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

  Synopsis    [Gets the equation form of a tree with original names.]

  Description [Gets the equation form of a tree with original names.]

  SideEffects []

  SeeAlso     [SynthGetChildMlTree]

******************************************************************************/
int
SynthGetChildMlTreeWithName(Ntk_Network_t *net,
			    bdd_manager *dd,
			    MlTree *tree,
			    char *eq)
{
  char		q_eq[MAX_EQ_LEN];
  char		d_eq[MAX_EQ_LEN];
  char		r_eq[MAX_EQ_LEN];
  char		qd_eq[MAX_EQ_LEN];
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*f;
  int		flag;

  f = tree->node;
  if (tree->leaf) {
    flag = SynthGetChildTreeWithName(net, dd, f, eq);
    return(flag);
  }

  if (f == one) {
    sprintf(eq, "one");
    return(0);
  } else if (f == zero) {
    sprintf(eq, "zero");
    return(0);
  }

  flag = SynthGetChildMlTreeWithName(net, dd, tree->q, q_eq);
  if (tree->q_comp)
    SynthMakeComplementString(q_eq);
  if (flag)
    return(1);
  flag = SynthGetChildMlTreeWithName(net, dd, tree->d, d_eq);
  if (tree->d_comp)
    SynthMakeComplementString(d_eq);
  if (flag)
    return(1);
  flag = SynthGetChildMlTreeWithName(net, dd, tree->r, r_eq);
  if (tree->r_comp)
    SynthMakeComplementString(r_eq);
  if (flag)
    return(1);

  if (strcmp(q_eq, "one") == 0)
    sprintf(qd_eq, "%s", d_eq);
  else if (strcmp(q_eq, "zero") == 0)
    sprintf(qd_eq, "zero");
  else if (strcmp(d_eq, "one") == 0)
    sprintf(qd_eq, "%s", q_eq);
  else if (strcmp(d_eq, "zero") == 0)
    sprintf(qd_eq, "zero");
  else {
    if (strlen(q_eq) + strlen(d_eq) + 1 > MAX_EQ_LEN) {
      sprintf(eq, "%s", q_eq);
      if (strlen(eq) == MAX_EQ_LEN - 1) {
	eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
	eq[MAX_EQ_LEN - 1] = '\0';
      } else {
	eq[strlen(eq)] = '#'; /* truncated */
	eq[strlen(eq) + 1] = '\0';
      }
      return(1);
    }
    sprintf(qd_eq, "%s%s", q_eq, d_eq);
  }

  if (strcmp(r_eq, "zero") == 0)
    sprintf(eq, "%s", qd_eq);
  else {
    if (strlen(qd_eq) + strlen(r_eq) + 1 > MAX_EQ_LEN) {
      sprintf(eq, "%s", qd_eq);
      if (strlen(eq) == MAX_EQ_LEN - 1) {
	eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
	eq[MAX_EQ_LEN - 1] = '\0';
      } else {
	eq[strlen(eq)] = '#'; /* truncated */
	eq[strlen(eq) + 1] = '\0';
      }
      return(1);
    }
    sprintf(eq, "(%s + %s)", qd_eq, r_eq);
  }
  return(0);
}


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

  Synopsis    [Gets the equation form of a tree which is a leaf node with
  original names.]

  Description [Gets the equation form of a tree which is a leaf node with
  original names.]

  SideEffects []

  SeeAlso     [SynthGetChildTree]

******************************************************************************/
int
SynthGetChildTreeWithName(Ntk_Network_t *net,
			  bdd_manager *dd,
			  bdd_node *f,
			  char *eq)
{
  char		left[MAX_EQ_LEN];
  char		right[MAX_EQ_LEN];
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  int		id, comp;
  char		name[MAX_NAME_LEN];
  int		flag;

  if (f == one) {
    sprintf(eq, "one");
    return(0);
  } else if (f == zero) {
    sprintf(eq, "zero");
    return(0);
  }

  flag = SynthGetChildTreeWithName(net, dd, bdd_bdd_T(f), left);
  if (flag)
    return(1);
  flag = SynthGetChildTreeWithName(net, dd, bdd_bdd_E(f), right);
  if (flag)
    return(1);

  id = bdd_node_read_index(f);
  comp = id & 0x1;
  id = id >> 1;

  sprintf(name, "%s", Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(net, id)));

  if (comp)
    strcat(name, "'");

  if (strcmp(left, "one") == 0) {
    if (strcmp(right, "zero") == 0)
      sprintf(eq, "%s", name);
    else {
      if (strlen(right) + strlen(name) + 6 > MAX_EQ_LEN) {
	sprintf(eq, "%s", right);
	if (strlen(eq) == MAX_EQ_LEN - 1) {
	  eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
	  eq[MAX_EQ_LEN - 1] = '\0';
	} else {
	  eq[strlen(eq)] = '#'; /* truncated */
	  eq[strlen(eq) + 1] = '\0';
	}
	return(1);
      }
      sprintf(eq, "(%s + %s)", name, right);
    }
  } else {
    if (strcmp(right, "zero") == 0) {
      if (strlen(left) + strlen(name) + 1 > MAX_EQ_LEN) {
	sprintf(eq, "%s", left);
	if (strlen(eq) == MAX_EQ_LEN - 1) {
	  eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
	  eq[MAX_EQ_LEN - 1] = '\0';
	} else {
	  eq[strlen(eq)] = '#'; /* truncated */
	  eq[strlen(eq) + 1] = '\0';
	}
	return(1);
      }
      sprintf(eq, "%s%s", name, left);
    } else {
      if (strlen(right) + strlen(left) + strlen(name) + 6 >
	  MAX_EQ_LEN) {
	sprintf(eq, "%s", right);
	if (strlen(eq) == MAX_EQ_LEN - 1) {
	  eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
	  eq[MAX_EQ_LEN - 1] = '\0';
	} else {
	  eq[strlen(eq)] = '#'; /* truncated */
	  eq[strlen(eq) + 1] = '\0';
	}
	return(1);
      }
      sprintf(eq, "(%s%s + %s)", name, left, right);
    }
  }
  return(0);
}


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

  Synopsis    [Gets the original name of a primary node.]

  Description [Gets the original name of a primary node. Return value
  shows polarity; 0 means positive variable and 1 means negative.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
SynthGetPrimaryNodeName(Ntk_Network_t *net,
			bdd_node *node,
			char *name)
{
  int	id;
  int	comp;
  char	*ntk_name;

  id = bdd_node_read_index(node);
  comp = id % 2;
  id = id >> 1;

  ntk_name = Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(net, id));
  sprintf(name, "%s", ntk_name);

  return(comp);
}


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

  Synopsis    [Gets the original name of a primary node with index.]

  Description [Gets the original name of a primary node with index.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthGetPrimaryIndexName(Ntk_Network_t *net,
			 int index,
			 char *name)
{
  int	id;

  id = index >> 1;
  sprintf(name, "%s", Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(net, id)));
}


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

  Synopsis    [Prints the equation form of a ZDD cover with original names.]

  Description [Prints the equation form of a ZDD cover with original names.
  If the string length is bigger than MAX_EQ_LEN, the string is truncated.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthPrintZddCoverWithName(Ntk_Network_t *net,
			   bdd_manager *dd,
			   bdd_node *node)
{
  char cover[MAX_EQ_LEN];

  fprintf(vis_stdout, "cover =");
  cover[0] = '\0';
  GetZddCoverWithNameRecur(net, dd, node, cover);
  fprintf(vis_stdout, "\n");
}


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

  Synopsis    [Makes the complement name of a node name.]

  Description [Makes the complement name of a node name.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
SynthMakeComplementString(char *eq)
{
  int	len;

  if (strcmp(eq, "zero") == 0) {
    sprintf(eq, "one");
    return;
  } else if (strcmp(eq, "one") == 0) {
    sprintf(eq, "zero");
    return;
  }
  len = strlen(eq);
  if (eq[len - 1] == '\'')
    eq[len - 1] = '\0';
  else {
    if (len == MAX_EQ_LEN - 1) {
      eq[len - 2] = '#'; /* truncated */
      eq[len - 1] = '\'';
    } else
      strcat(eq, "'");
  }
}


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

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

  Synopsis    [Gets an equation form of a ZDD node.]

  Description [Gets an equation form of a ZDD node. Returns 1 if
  eq string is truncated, otherwise normally returns 0.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
GetChildTree(bdd_manager *dd,
	     bdd_node *f,
	     char *eq)
{
  char		left[MAX_EQ_LEN];
  char		right[MAX_EQ_LEN];
  char		tmp[MAX_NAME_LEN];
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  int		flag; /* truncated */

  if (f == one) {
    sprintf(eq, "one");
    return(0);
  } else if (f == zero) {
    sprintf(eq, "zero");
    return(0);
  }

  flag = GetChildTree(dd, bdd_bdd_T(f), left);
  if (flag)
    return(1);
  flag = GetChildTree(dd, bdd_bdd_E(f), right);
  if (flag)
    return(1);

  sprintf(tmp, "v%d", bdd_node_read_index(f));
  if (strcmp(left, "one") == 0) {
    if (strcmp(right, "zero") == 0)
      sprintf(eq, "%s", tmp);
    else {
      if (strlen(right) + strlen(tmp) + 6 > MAX_EQ_LEN) {
	sprintf(eq, "%s", right);
	if (strlen(eq) == MAX_EQ_LEN - 1) {
	  eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
	  eq[MAX_EQ_LEN - 1] = '\0';
	} else {
	  eq[strlen(eq)] = '#'; /* truncated */
	  eq[strlen(eq) + 1] = '\0';
	}
	return(1);
      }
      sprintf(eq, "(%s + %s)", tmp, right);
    }
  } else {
    if (strcmp(right, "zero") == 0) {
      if (strlen(left) + strlen(tmp) + 1 > MAX_EQ_LEN) {
	sprintf(eq, "%s", left);
	if (strlen(eq) == MAX_EQ_LEN - 1) {
	  eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
	  eq[MAX_EQ_LEN - 1] = '\0';
	} else {
	  eq[strlen(eq)] = '#'; /* truncated */
	  eq[strlen(eq) + 1] = '\0';
	}
	return(1);
      }
      sprintf(eq, "%s%s", tmp, left);
    } else {
      if (strlen(right) + strlen(left) + strlen(tmp) + 6 > MAX_EQ_LEN) {
	sprintf(eq, "%s", right);
	if (strlen(eq) == MAX_EQ_LEN - 1) {
	  eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
	  eq[MAX_EQ_LEN - 1] = '\0';
	} else {
	  eq[strlen(eq)] = '#'; /* truncated */
	  eq[strlen(eq) + 1] = '\0';
	}
	return(1);
      }
      sprintf(eq, "(%s%s + %s)", tmp, left, right);
    }
  }
  return(0);
}


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

  Synopsis    [Gets the equation form of a tree with internal name.]

  Description [Gets the equation form of a tree with internal name. Returns
  1 if eq string is truncated, otherwise normally returns 0.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
GetChildMlTree(bdd_manager *dd,
	       MlTree *tree,
	       char *eq)
{
  char		q_eq[MAX_EQ_LEN];
  char		d_eq[MAX_EQ_LEN];
  char		r_eq[MAX_EQ_LEN];
  char		qd_eq[MAX_EQ_LEN];
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  bdd_node	*f;
  int		flag;

  f = tree->node;
  if (tree->leaf) {
    flag = GetChildTree(dd, f, eq);
    return(flag);
  }

  if (f == one) {
    sprintf(eq, "one");
    return(0);
  } else if (f == zero) {
    sprintf(eq, "zero");
    return(0);
  }

  flag = GetChildMlTree(dd, tree->q, q_eq);
  if (tree->q_comp)
    SynthMakeComplementString(q_eq);
  if (flag)
    return(1);
  flag = GetChildMlTree(dd, tree->d, d_eq);
  if (tree->d_comp)
    SynthMakeComplementString(d_eq);
  if (flag)
    return(1);
  flag = GetChildMlTree(dd, tree->r, r_eq);
  if (tree->r_comp)
    SynthMakeComplementString(r_eq);
  if (flag)
    return(1);

  if (strcmp(q_eq, "one") == 0)
    sprintf(qd_eq, "%s", d_eq);
  else if (strcmp(q_eq, "zero") == 0)
    sprintf(qd_eq, "zero");
  else if (strcmp(d_eq, "one") == 0)
    sprintf(qd_eq, "%s", q_eq);
  else if (strcmp(d_eq, "zero") == 0)
    sprintf(qd_eq, "zero");
  else {
    if (strlen(q_eq) + strlen(d_eq) + 1 > MAX_EQ_LEN) {
      sprintf(eq, "%s", q_eq);
      if (strlen(eq) == MAX_EQ_LEN - 1) {
	eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
	eq[MAX_EQ_LEN - 1] = '\0';
      } else {
	eq[strlen(eq)] = '#'; /* truncated */
	eq[strlen(eq) + 1] = '\0';
      }
      return(1);
    }
    sprintf(qd_eq, "%s%s", q_eq, d_eq);
  }

  if (strcmp(r_eq, "zero") == 0)
    sprintf(eq, "%s", qd_eq);
  else {
    if (strlen(qd_eq) + strlen(r_eq) + 1 > MAX_EQ_LEN) {
      sprintf(eq, "%s", qd_eq);
      if (strlen(eq) == MAX_EQ_LEN - 1) {
	eq[MAX_EQ_LEN - 2] = '#'; /* truncated */
	eq[MAX_EQ_LEN - 1] = '\0';
      } else {
	eq[strlen(eq)] = '#'; /* truncated */
	eq[strlen(eq) + 1] = '\0';
      }
      return(1);
    }
    sprintf(eq, "(%s + %s)", qd_eq, r_eq);
  }
  return(0);
}


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

  Synopsis    [Finds a node that has the given index.]

  Description [Finds a node that has the given index among the descendants
  of the given node (this node included). If there exists a node with
  the index, the node is returned, otherwise returns NULL.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static bdd_node	*
FindNodeWithIndex(bdd_node *node,
		  int index)
{
  bdd_node	*tmp;

  if (bdd_is_constant(node))
    return(NULL);
  if (bdd_node_read_index(node) == index)
    return(node);

  tmp = FindNodeWithIndex(bdd_bdd_T(node), index);
  if (tmp)
    return(tmp);
  return(FindNodeWithIndex(bdd_bdd_E(node), index));
}


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

  Synopsis    [Gets the equation form of a ZDD cover with original names.]

  Description [Gets an equation form of a ZDD cover with original names.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static void
GetZddCoverWithNameRecur(Ntk_Network_t *net,
			 bdd_manager *dd,
			 bdd_node *node,
			 char *cover)
{
  bdd_node	*one = bdd_read_one(dd);
  bdd_node	*zero = bdd_read_zero(dd);
  int		len, index;
  char		name[MAX_NAME_LEN], *varName;

  if (node == zero)
    return;

  if (node == one) {
    fprintf(vis_stdout, " + %s", cover);
    return;
  }

  len = strlen(cover);
  index = bdd_node_read_index(node);
  varName = Ntk_NodeReadName(Ntk_NetworkFindNodeByMddId(net, index / 2));
  if (index % 2 == 0)
    sprintf(name, "%s", varName);
  else
    sprintf(name, "%s'", varName);
  strcat(cover, name);
  GetZddCoverWithNameRecur(net, dd, bdd_bdd_T(node), cover);
  cover[len] = '\0';
  GetZddCoverWithNameRecur(net, dd, bdd_bdd_E(node), cover);
  cover[len] = '\0';
}