/**CHeaderFile*****************************************************************

  FileName    [synthInt.h]

  PackageName [synth]

  Synopsis    [Internal declarations.]

  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.]

  Revision    [$Id: synthInt.h,v 1.36 2005/05/13 08:47:48 hhhan Exp $]

******************************************************************************/

#ifndef _SYNTHINT
#define _SYNTHINT

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/
#include "synth.h"
#include "ntm.h"
#include "ntk.h"
#include "ord.h"
#include <string.h>

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


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


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

/**Struct**********************************************************************

  Synopsis    [Structure holding the synthesis command options.]

  Description [Structure holding the synthesis command options.]

  SeeAlso     []

******************************************************************************/
struct SynthInfoDataStruct {
  int factoring; /* factoring method */
  int divisor; /* divisor method */
  int unreachDC; /* use unreachable states as don't cares */
  int reordering; /* allow reordering in BDD and/or ZDD */
  int trySharing; /* try to share more nodes */
  int realign; /* allow realignment to ZDD/BDD after BDD/ZDD reordering */
  char *filehead; /* output file name */
  char *prefix; /* prefix of internal node names */
  boolean eqn; /* if true, output synthesized circuit in equation format too */
};

/**Struct**********************************************************************

  Synopsis    [Structure representing multi-level logic by quotient, divisor,
  and remainder.]

  Description [Structure representing multi-level logic by quotient,
  divisor, and remainder. In spite of the name this is a graph
  structure, not a tree.  Each node of the graph has 3 children:
  quotient, divisor, and remainder. The purpose of the field
  complement is to have both phases in a tree, so if the field 'comp'
  is set to 1, then the field 'complement' is taken instead of the
  field 'node'. When an output function is the same as either another
  output function or the complement of another function, the tree of
  the output function is made by copying the tree of the other
  function, then the field 'ref' of this tree is set to 1. The fields
  'q(d,r)_ref' tell each child tree was newly created or already
  existing, and the fields 'q(d,r)_comp' tell whether each child tree
  is complemented or not.  To increase sharing, every time a function
  is factored, a tree representing quotient * divisor is made if the
  tree does not exist, and the field 'candidate' of this tree is set
  to 1.]

  SeeAlso     []

******************************************************************************/
typedef	struct	ml_tree	{
    bdd_node		*node; /* a ZDD */
    bdd_node		*complement; /* complement ZDD of node */
    struct ml_tree	*q; /* quotient */
    struct ml_tree	*d; /* divisor */
    struct ml_tree	*r; /* remainder */
    unsigned int	*support; /* a set of support of node */
    int			nLiterals; /* number of literals of this ml_tree */
    unsigned short	id; /* id of this ml_tree */
    unsigned 		leaf: 1; /* set to 1 when this ml_tree is leaf */
    unsigned 		pi: 1; /* set to 1 if node is primary input */
    unsigned 		ref: 1; /* set to 1 if this ml_tree is made by
                                 * copying an existing tree */
    unsigned 		q_ref: 1; /* set to 1 if q is already existing tree */
    unsigned 		d_ref: 1; /* set to 1 if d is already existing tree */
    unsigned 		r_ref: 1; /* set to 1 if r is already existing tree */
    unsigned		top: 1; /* set to 1 if this ml_tree is a primary
                                 * output or next state function */
    unsigned		comp: 1; /* take complement of ml_tree if 1 */
    unsigned 		q_comp: 1; /* take complement of q as quotient if 1 */
    unsigned 		d_comp: 1; /* take complement of d as divisor if 1 */
    unsigned 		r_comp: 1; /* take complement of r as remainder if 1 */
    unsigned		shared: 1; /* set to 1 if this ml_tree has more than
    				    * one assendent */
    unsigned		candidate: 1;
    unsigned 		flag: 1;
    unsigned		dummy: 2;
    struct ml_tree	*next;
} MlTree;


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


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


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

#define	MlTree_Not(tree)             ((MlTree *)((long)(tree) ^ 01))
#define	MlTree_IsComplement(tree)    ((long)(tree) & 01)
#define	MlTree_Regular(tree)         ((MlTree *)((long)(tree) & ~01))

#define MAX_EQ_LEN	4096
#define MAX_NAME_LEN	256

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

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

EXTERN int SynthCountMlLiteral(bdd_manager *dd, MlTree *tree, int ref);
EXTERN void SynthZddSupportStep(bdd_node *f, int *support);
EXTERN void SynthZddClearFlag(bdd_node *f);
EXTERN int SynthGetLiteralCount(bdd_manager *dd, bdd_node *node);
EXTERN bdd_node	* SynthZddQuickDivisor(bdd_manager *dd, bdd_node *f);
EXTERN bdd_node	* SynthZddLeastDivisor(bdd_manager *dd, bdd_node *f);
EXTERN bdd_node	* SynthZddMostDivisor(bdd_manager *dd, bdd_node *f);
EXTERN bdd_node	* SynthZddLevelZeroDivisor(bdd_manager *dd, bdd_node *f);
EXTERN bdd_node	* SynthZddCommonDivisor(bdd_manager *dd, bdd_node *f);
EXTERN bdd_node	* SynthZddLpDivisor(bdd_manager *dd, bdd_node *f);
EXTERN void SynthCountLiteralOccurrence(bdd_manager *dd, bdd_node *f, int *count);
EXTERN bdd_node * (* SynthGetZddProductFunc(void)) (bdd_manager *, bdd_node *, bdd_node *);
EXTERN bdd_node * (* SynthGetZddProductRecurFunc(void)) (bdd_manager *, bdd_node *, bdd_node *);
EXTERN bdd_node * (* SynthGetZddDivideFunc(void)) (bdd_manager *, bdd_node *, bdd_node *);
EXTERN bdd_node * (* SynthGetZddDivideRecurFunc(void)) (bdd_manager *, bdd_node *, bdd_node *);
EXTERN  void SynthSetZddDivisorFunc(int mode);
EXTERN bdd_node * (* SynthGetZddDivisorFunc(void)) (bdd_manager *, bdd_node *);
EXTERN void SynthGetSpaceString(char *string, int n, int max);
EXTERN MlTree	* SynthLookupMlTable(st_table *table, bdd_manager *dd, bdd_node *node, int candidate, int verbosity);
EXTERN int SynthUseCandidate(st_table *table, bdd_manager *dd, MlTree *m_tree, int verbosity);
EXTERN MlTree	* SynthFindOrCreateMlTree(st_table *table, bdd_manager *dd, bdd_node *f, int leaf, int candidate, int *ref, int verbosity);
EXTERN void SynthInitMlTable(void);
EXTERN void SynthClearMlTable(bdd_manager *dd, st_table *table);
EXTERN void SynthPutMlTreeInList(bdd_manager *dd, MlTree *tree, int candidate);
EXTERN MlTree * SynthGetHeadTreeOfSize(int size);
EXTERN int SynthGetSupportMask(bdd_manager *dd, bdd_node *node, unsigned int *mask);
EXTERN int SynthGetSupportCount(bdd_manager *dd, bdd_node *node);
EXTERN MlTree	* SynthCheckAndMakeComplement(bdd_manager *dd, st_table *table, MlTree *tree, int *comp_flag, int verbosity);
EXTERN void SynthSetSharedFlag(bdd_manager *dd, MlTree *tree);
EXTERN int SynthPostFactoring(bdd_manager *dd, st_table *table, MlTree *(* factoring_func)(bdd_manager *, st_table *, bdd_node *, int, int *, MlTree *, int, MlTree *, int), int verbosity);
EXTERN void SynthUpdateRefOfParent(MlTree *top);
EXTERN void SynthVerifyTree(bdd_manager *dd, MlTree *tree, int flag);
EXTERN void SynthVerifyMlTable(bdd_manager *dd, st_table *table);
EXTERN void SynthPrintTreeList(MlTree *list);
EXTERN void SynthPrintLeafList(MlTree *list);
EXTERN 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);
EXTERN bdd_node	* SynthMakeCubeFree(bdd_manager *dd, bdd_node *f);
EXTERN void SynthMultiLevelOptimize(Ntk_Network_t *network, bdd_node **combOutBdds, bdd_node **combUpperBdds, char **combOutNames, int *initStates, Synth_InfoData_t *synthInfo, int verbosity);
EXTERN void SynthSetUseFuncDivisor(int mode);
EXTERN void SynthSetOutputOrdering(int mode);
EXTERN void SynthSetCostFactors(float supp, float prob);
EXTERN void SynthSetSupportCount(int *count);
EXTERN void SynthSetProbability(float *prob);
EXTERN  int SynthFindDivisorForLowPower(int *count, int nvars, int min_count, int min_pos);
EXTERN char * SynthGetIthOutputName(int i);
EXTERN int SynthIsSubsetOfSupport(int size, unsigned int *mask1, unsigned int *mask2);
EXTERN 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);
EXTERN 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);
EXTERN 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);
EXTERN 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);
EXTERN 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);
EXTERN void SynthPrintZddTree(bdd_manager *dd, bdd_node *f);
EXTERN void SynthPrintZddTreeMessage(bdd_manager *dd, bdd_node *f, char *mess);
EXTERN void SynthPrintMlTreeMessage(bdd_manager *dd, MlTree *tree, char *mess);
EXTERN void SynthFreeMlTree(MlTree *tree, int flag);
EXTERN void SynthPrintMlTreeWithName(Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, char *mess);
EXTERN int SynthGetChildMlTreeWithName(Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, char *eq);
EXTERN int SynthGetChildTreeWithName(Ntk_Network_t *net, bdd_manager *dd, bdd_node *f, char *eq);
EXTERN int SynthGetPrimaryNodeName(Ntk_Network_t *net, bdd_node *node, char *name);
EXTERN void SynthGetPrimaryIndexName(Ntk_Network_t *net, int index, char *name);
EXTERN void SynthPrintZddCoverWithName(Ntk_Network_t *net, bdd_manager *dd, bdd_node *node);
EXTERN  void SynthMakeComplementString(char *eq);
EXTERN  int SynthStringCompare(char **a, char **b);
EXTERN  void SynthWriteBlifFile(Ntk_Network_t *net, bdd_manager *dd, MlTree **tree, char *filename, int no, bdd_node **ofuncs, int *initStates, int ml_mode, int verbosity);
EXTERN void SynthWriteEqnHeader(FILE *fout, Ntk_Network_t *net, bdd_manager *dd);
EXTERN void SynthWriteEqn(FILE *fout, Ntk_Network_t *net, bdd_manager *dd, MlTree *tree, bdd_node **ofuncs, char *func_name, int ref);
EXTERN void SynthSetInternalNodePrefix(char *prefix);
EXTERN void SynthSetupNodeNameTable(Ntk_Network_t *net);
EXTERN void SynthFreeNodeNameTable(void);
EXTERN void SynthGetInternalNodeName(char *name, int id);
EXTERN void SynthDumpBlif(Ntk_Network_t *net, bdd_manager *dd, int no, bdd_node **ofuncs, char **onames, int *initStates, char *model);

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

#endif /* _SYNTHINT */