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

  FileName    [restrInt.h]

  PackageName [restr]

  Synopsis [Internal declarations for state transition graph (STG)
  restructuring package.]

  Author      [Balakrishna Kumthekar <kumtheka@colorado.edu>]

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

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

#ifndef _RESTRINT
#define _RESTRINT

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/
#include "restr.h"
#include "st.h"
#include "mark.h"
#include <string.h>

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


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


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

  Synopsis [Different heuristics to perform the restructuring of state
  transition graph.]

  SeeAlso     []

******************************************************************************/
typedef enum {
  RestrHammingD_c,
  RestrFanin_c,
  RestrFaninFanout_c,
  RestrCProjection_c
} RestructureHeuristic;


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


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


/**Macro***********************************************************************

  Synopsis [Definition of a key to store a partition created solely for
  internal use.]

  SideEffects  [None]

  SeeAlso      []

******************************************************************************/
#define RESTR_PART_NETWORK_APPL_KEY "Restr_PartNetworkApplKey"


/**Macro***********************************************************************

  Synopsis [Definition of a key to store an FSM created solely for internal
  use.]

  SideEffects  [None]

  SeeAlso      []

******************************************************************************/
#define RESTR_FSM_NETWORK_APPL_KEY "Restr_FsmNetworkApplKey"


/**Macro***********************************************************************

  Synopsis [Returns the maximum value of the arguments.]

  SideEffects  [None]

  SeeAlso      []

******************************************************************************/
#define restrMax(x,y)	(((y) > (x)) ? (y) : (x))


/**Macro***********************************************************************

  Synopsis [Returns the minimum value of the arguments.]

  SideEffects  [None]

  SeeAlso      []

******************************************************************************/
#define restrMin(x,y)	(((y) > (x)) ? (x) : (y))

#define MAX_NAME_LEN 256

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

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

EXTERN bdd_node * RestrMinimizeFsmByCProj(bdd_manager *ddManager, bdd_node *equivRel, bdd_node *originalTR, bdd_node *initBdd, bdd_node **xVars, bdd_node **yVars, bdd_node **uVars, bdd_node **vVars, bdd_node **piVars, int nVars, int nPi, array_t **outBdds, bdd_node **newInit);
EXTERN void RestrNamePrintByMddId(Ntk_Network_t *network, array_t *array);
EXTERN void RestrPrintMvfArray(mdd_manager *ddManager, Mvf_Function_t *mvfArray, array_t *nodeArray, array_t *idArray);
EXTERN void RestrPrintAllVarNames(bdd_manager *ddManager);
EXTERN void RestrPrintBddNode(bdd_manager *manager, bdd_node *ddNode);
EXTERN void RestrVerifyFsmEquivBySimulation(bdd_manager *ddManager, bdd_node *oldTr, bdd_node *newTr, array_t *outBdds1, array_t *outBdds2, bdd_node *initBdd1, bdd_node *initBdd2, bdd_node **xVars, bdd_node **yVars, bdd_node **piVars, int nVars, int nPi);
EXTERN void RestrTestIsEquivRelation(bdd_manager *ddManager, bdd_node *rel, bdd_node **xVars, bdd_node **yVars, bdd_node **uVars, bdd_node **vVars, int nVars);
EXTERN void RestrPrintVarArrayNames(bdd_manager *ddManager, bdd_node **xVars, int nVars);
EXTERN void RestrPrintNameArray(array_t *nameArray);
EXTERN int RestrTestIsDeterministic(bdd_manager *ddManager, bdd_node *tr, bdd_node *initBdd, bdd_node **xVars, bdd_node **yVars, int nVars);
EXTERN bdd_node * RestrMinimizeFsmByFaninFanout(bdd_manager *ddManager, bdd_node *equivRel, bdd_node *oldTR, bdd_node **addPTR, bdd_node **possessedProbMatrix, bdd_node *initBdd, bdd_node *reachable, bdd_node *stateProbs, bdd_node **piVars, bdd_node **xVars, bdd_node **yVars, bdd_node **uVars, bdd_node **vVars, int nVars, int nPi, RestructureHeuristic heuristic, array_t **outBdds, bdd_node **newInit);
EXTERN bdd_node * RestrSelectLeastHammingDStates(bdd_manager *dd, bdd_node *oldTR, bdd_node *pTR, bdd_node **xVars, bdd_node **yVars, bdd_node **vVars, int nVars, int nPi);
EXTERN int RestrCommandRestructureFsm(Fsm_Fsm_t *fsm, RestructureHeuristic heuristic, char *orderFileName, boolean equivClasses, boolean nonReachEquiv, boolean eqvMethod, st_table *inputProb, Synth_InfoData_t *synthInfo);
EXTERN array_t * RestrGetOutputArray(Ntk_Network_t *network);
EXTERN bdd_node * RestrCreateProductOutput(bdd_manager *ddManager, array_t *funArray, bdd_node **xVars, bdd_node **yVars, int nVars);
EXTERN array_t * RestrComputeTRWithIds(bdd_manager *ddManager, array_t *nextBdds, bdd_node **xVars, bdd_node **yVars, bdd_node **uVars, bdd_node **vVars, int nVars);
EXTERN bdd_node * RestrGetEquivRelation(bdd_manager *mgr, bdd_node *Lambda, bdd_node *tranRelation, bdd_node **xVars, bdd_node **yVars, bdd_node **uVars, bdd_node **vVars, bdd_node **piVars, int nVars, int nPi, boolean restrVerbose);
EXTERN bdd_node * RestrComputeEquivRelationUsingCofactors(bdd_manager *mgr, bdd_node *Lambda, bdd_node *TR, bdd_node **xVars, bdd_node **yVars, bdd_node **uVars, bdd_node **vVars, bdd_node **piVars, int nVars, int nPi, boolean restrVerbose);
EXTERN bdd_node * RestrComputeTrWithGhostEdges(bdd_manager *mgr, bdd_node **yVars, bdd_node **vVars, bdd_node *tr, bdd_node *equivRelation, int nVars);
EXTERN bdd_node * RestrAddMaximum(bdd_manager *ddManager, bdd_node **f, bdd_node **g);
EXTERN bdd_node * RestrAddEqual(bdd_manager *ddManager, bdd_node **f, bdd_node **g);
EXTERN bdd_node ** RestrBddNodeArrayFromIdArray(bdd_manager *ddManager, array_t *idArray);
EXTERN double RestrAverageBitChange(bdd_manager *manager, bdd_node *probTR, bdd_node **xVars, bdd_node **yVars, int nVars);
EXTERN array_t * RestrCreateNewStateVars(Ntk_Network_t *network, bdd_manager *ddManager, bdd_node **xVars, bdd_node **yVars);
EXTERN void RestrSetInitialOrder(Ntk_Network_t *network, bdd_manager *ddManager);

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

#endif /* _RESTRINT */