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

  FileName    [satInt.h]

  PackageName [sat]

  Synopsis    []

  Description [Internal data structures of the sat package.]

  SeeAlso     []

  Author      [HoonSang Jin ]

  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: satInt.h,v 1.19 2009/04/11 18:26:37 fabio Exp $]

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


#ifndef _SATINT
#define _SATINT

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/
#include "baig.h"
#include "sat.h"

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

#define LATEST_ACTIVITY_DELETION 0x1
#define MAX_UNRELEVANCE_DELETION 0x2
#define SIMPLE_LATEST_DELETION   0x4

/*Bing:*/
#define RESET_LC 0xfffffffe
#define RESET_DVH  0xfffffffd
#define SCOREUNIT 100000

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


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

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

  Synopsis    [sat option]

  Description []

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

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


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


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

EXTERN satLevel_t * sat_GetDecision( satManager_t *cm, int level);
EXTERN satArray_t * sat_ArrayAlloc(long number);
EXTERN int sat_ImplyStop( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int sat_ImplySplit( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int sat_ImplyConflict( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int sat_ImplyLeftForward( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int sat_ImplyRightForward( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int sat_ImplyForwardOne( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int sat_ImplyPropRight( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int sat_ImplyPropRightOne( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int sat_ImplyPropLeft( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int sat_ImplyPropLeftOne( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int sat_ImplyPropLeftRight( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN satQueue_t * sat_CreateQueue( long MaxElements );
EXTERN satStatistics_t * sat_InitStatistics(void);
EXTERN int  sat_BacktrackWithAdditionalTest( satManager_t *cm, int level);
EXTERN satLinearHead_t * sat_CreateLinearHead( satManager_t *cm, int flag);
EXTERN satLinearCluster_t * sat_CreateCluster( satLinearHead_t *head, satLinearElem_t *e1, satLinearElem_t *e2, int flagIndex, int *idArr);
EXTERN void sat_ExtractAssignmentFromBDD( satLinearHead_t *head, DdManager *mgr, satArray_t *arr, DdNode *cube);
EXTERN DdNode *sat_CofactorBDDArray( satLinearHead_t *head, DdManager *mgr, DdNode *l1, satArray_t *satArr);
EXTERN char * sat_RemoveSpace(char *line);
EXTERN char * sat_CopyWord(char *lp, char *word);
EXTERN satLinearHead_t * sat_CreateHeadForUIP(satManager_t *cm);
EXTERN DdNode * sat_BuildBDDForClause( satManager_t *cm, satLinearHead_t *head, long v, int includeLevel, satArray_t *arr);
EXTERN int  sat_GetUIPFromGivenBDD(satLinearHead_t *head, DdManager *mgr, DdNode *total, satArray_t *arr);
EXTERN void RT_Free(RTManager_t *rm);
EXTERN void ResetRTree(RTManager_t *rm);
EXTERN bAigEdge_t sat_GenerateFwdIP(bAig_Manager_t* manager, satManager_t *cm, RTnode_t  RTnode, int cut);
EXTERN void sat_BuildRT(satManager_t * cm, RTnode_t root, long *lp, long *tmpIP, int size, boolean NotCNF);
EXTERN void sat_GenerateCore_All(satManager_t * cm);
EXTERN void sat_InitLayerScore(satManager_t * cm);

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

#endif /* _SATINT */