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

  FileName    [baigInt.h]

  PackageName [baig]

  Synopsis    []

  Description [Internal data structures of the bAig package.]

  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: baigInt.h,v 1.21 2005/07/15 21:09:26 jinh Exp $]

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

#ifndef _bAIGINT
#define _bAIGINT

#include "util.h"
#include "array.h"
#include "baig.h"

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

/* Each node occupies 8 location.  The following describes these locations */

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

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



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


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




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

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

EXTERN void bAigSetPassFlag(bAig_Manager_t *manager, bAigEdge_t node);
EXTERN void bAigResetPassFlag(bAig_Manager_t *manager, bAigEdge_t node);
EXTERN int bAigGetPassFlag(bAig_Manager_t *manager, bAigEdge_t node);
EXTERN bAigEdge_t bAigCreateAndNode(bAig_Manager_t *manager, bAigEdge_t node1, bAigEdge_t node2);
EXTERN bAigTransition_t * bAigCreateTransitionRelation( Ntk_Network_t *network, mAig_Manager_t *manager);
EXTERN int bAigCheckInvariantWithAG( bAigTransition_t *t, bAigEdge_t objective);
EXTERN void bAigCleanUpDataFromPreviousExecution(bAigTransition_t *t);
EXTERN bAigEdge_t bAigBuildObjectiveFromFrontierSet(bAigTransition_t *t);
EXTERN satManager_t * bAigCirCUsInterfaceForAX(bAigTransition_t *t);
EXTERN void bAigMarkConeOfInfluenceForAX(bAigTransition_t *t, satManager_t *cm);
EXTERN void bAig_ComputeAX(bAigTransition_t *t);
EXTERN void bAig_PostProcessForAX(bAigTransition_t *t, satManager_t *cm);
EXTERN void bAigCreateSatManagerForLifting(bAigTransition_t *t);
EXTERN void bAigSolveAllSatWithLifting(bAigTransition_t *t);
EXTERN void bAigBlockingClauseAnalysisBasedOnLifting(bAigTransition_t *t, satManager_t *allsat);
EXTERN void bAigCollectAntecdentOfObjective( bAigTransition_t *t, satManager_t *cm, bAigEdge_t obj, satArray_t *clauseArray);
EXTERN void bAigMinimizationBasedOnLifting( bAigTransition_t *t, bAigEdge_t obj, satArray_t *orderArray);
EXTERN int bAigCheckExistenceOfUIP( satManager_t *cm, satArray_t *clauseArray,int mLevel,  bAigEdge_t *fdaLit, int *bLevel);
EXTERN void bAigSolverForLifting(satManager_t *cm, int tLevel);
EXTERN void bAigCollectAntecdentOfObjectiveAux(satManager_t *cm, bAigEdge_t v);
EXTERN int bAigInclusionTestOnInitialStates(bAigTransition_t *t);
EXTERN void bAigPrintTransitionInfo(bAigTransition_t *t);
EXTERN void bAigMinimizationBasedOnLiftingAllAtOnce( bAigTransition_t *t, bAigEdge_t obj, satArray_t *orderArray); 
EXTERN satArray_t * bAigCreateCNFInstanceForInclusionTestOnInitialStates(bAigTransition_t *t);
EXTERN void bAig_CreateCNFFromAIG( bAig_Manager_t *manager, satArray_t *rootArray, satArray_t *cnfArray);
EXTERN void bAigCreateSatManagerForLiftingUnconstrained(bAigTransition_t *t);
EXTERN bAigEdge_t bAigBuildComplementedObjectiveWithCNF( bAigTransition_t *t, satManager_t *cm, satArray_t *narr, satArray_t *carr);
EXTERN void bAigPreProcessingForLiftingInstance(bAigTransition_t *t, satManager_t *cm);



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

#endif /* _bAIGINT */