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

  FileName    [maig.h]

  PackageName [maig]

  Synopsis    [multi-valued AND/INVERTER graph]

  Description []

  SeeAlso     []

  Author      [Mohammad Awedh]

  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: maig.h,v 1.8 2005/05/18 18:11:59 jinh Exp $]


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

#ifndef _MAIG
#define _MAIG

#include "vm.h"
#include "util.h"
#include "var_set.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/
 
#define mAig_And   bAig_And
#define mAig_Or    bAig_Or
#define mAig_Xor   bAig_Xor
#define mAig_Not   bAig_Not
#define mAig_Eq    bAig_Eq
#define mAig_Then  bAig_Then
#define mAig_Zero  bAig_Zero
#define mAig_One   bAig_One
#define mAig_NULL  bAig_NULL

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

typedef struct mAigMvarStruct mAigMvar_t;
typedef struct mAigBvarStruct mAigBvar_t;

typedef long     mAigEdge_t;
typedef struct bAigManagerStruct mAig_Manager_t;

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

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

  Synopsis    [Multi-valued Variable]

  Description [This structure stores an information about a Multi-value variable.]

******************************************************************************/
struct mAigMvarStruct {
    int  mVarId;          /* Uniquely identifies this mVar node in mVarList*/
    char *name;	          /* Name of multi-value node */
    int  values;	  /* This mvar takes vlaues from 0 -- values-1 */
    int  encodeLength;    /* Number of binary variables needed to encode this 
                             mvar */
    int  bVars;          /* The array index of the first bVar in the bVarList
                            the size of the binary encoding equal encodeLength
                            and code arrange from  most significant bit to 
                            least significant bit */
};

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

  Synopsis    [Binary-valued varaible]

  Description [Thsi structure contians information about binary-vlaue node]

*****************************************************************************/
struct mAigBvarStruct {
    mAigEdge_t node;  /* Binary function of this node in the AndInv graph */
    int mVarId;          /* This bVar node belongs to mVar node mVarId       */
};


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


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

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

EXTERN void mAig_Init(void);
EXTERN void mAig_End(void);
EXTERN array_t * mAig_ArrayDuplicate(array_t *mAigArray);
EXTERN mAig_Manager_t * mAig_initAig(void);
EXTERN void mAig_quit(mAig_Manager_t *manager);
EXTERN mAigEdge_t mAig_EquC(mAig_Manager_t * mgr, mAigEdge_t mVarId, int constant);
EXTERN mAigEdge_t mAig_CreateVar(mAig_Manager_t * mgr, char * name, int value);
EXTERN array_t * mAigReadBinVarList(mAig_Manager_t * manager);
EXTERN array_t * mAigReadMulVarList(mAig_Manager_t * manager);
EXTERN mAigEdge_t mAig_CreateVarFromAig(mAig_Manager_t * mgr, char * name, array_t *mvfAig);

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

#endif /* _MAIG */