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

  FileName    [puresatInt.h]

  PackageName [puresat]

  Synopsis    [Internal declarations.]

  Author      [Bing Li]

  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
  All rights reserved.

  Permission is hereby granted, without written agreement and without license
  or royalty fees, to use, copy, modify, and distribute this software and its
  documentation for any purpose, provided that the above copyright notice and
  the following two paragraphs appear in all copies of this software.
  ]

  Revision    [$Id: puresatInt.h,v 1.22 2009/04/11 18:26:31 fabio Exp $]

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

#ifndef _PURESATINT
#define _PURESATINT


/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/

#include "bmcInt.h"
#include "mdd.h"
#include "satInt.h"
#include "sat.h"
#include "puresat.h"
#include "baig.h"

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

#define NO_OP 0
#define MAX_LENGTH 80


#define RESTORE_AIG 0
#define PR 0
#define TESTIP 1
/*#define TIMEFRAME_VERIFY_*/
#define COI 0 /*must be zero*/
#define UNSATCORE 0
#define IP_PROCESS 1 /*MUST be one*/
/*#define TWOLEVEL_MIN 1*/
#define DBG 1
#define LARGEDFS 10000
#define LAI 0 /*latch interface abstraction*/
#define COREREFMIN 0
#define THROUGHPICK 1
#define DIFABSCON 0 /*must be zero,diff abs and contst model*/
#define INCRECON  1/*Incremental Concretization*/
#define AROSAT 1
#define NOREFMIN 0
#define ADD_HIGHRC_LATCH 0
#define INC 0
#define SWITCH 0
#define SWITCH_DA 0 /*switch to DirAdd*/


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

struct PureSatManager {
  int Length;
  int sameAbsCon;
  satArray_t * savedConCls;
  int returnVal;
  satArray_t * AuxObj;
  int switch_da;
  boolean Arosat; /*enable Arosat*/
  boolean CoreRefMin;/*enable unsat proof-based refinement minimization*/
  boolean RefPredict; /*enable refinement prediction*/
  boolean Switch; /* enable dynamic switching*/
  st_table *latchToTableBaigNodes;
  st_table *ClsidxToLatchTable;
  st_table  *CoiTable;
  st_table  *oldCoiTable;
  st_table  *AbsTable;
  st_table  *vertexTable;
  st_table  *SufAbsTable;
  st_table  *supportTable;
  st_table  *IdenLatchTable;  /*store indentical latch*/

  st_table  *node2dfsTable;

  /*for dir cone in abs order*/
  st_table *nicTable;/*num in cone*/
  st_table *niaTable; /*num in abs*/
  boolean incre;
  boolean sss;
  int verbosity;
  char * ltlFileName;
  int timeOutPeriod;
  int oldPos;
  int dbgLevel;
  FILE *dbgOut;
  boolean printInputs;
  array_t * result;
  double tIP; /*general IP time*/
  double tIPUnsat; /*real and bogus Cex detection time*/
  double tIPGen;  /*IP generation time*/
  double tIPImply;/*IP verification time*/
  double tIPCon;  /*IP convergence test time*/
  double tRefMin; /*Refine minimization time*/
  double tRef;    /*Refine time*/
  double tCoreGen;/*Core generation time in refine*/
  double tRefExtract;/*time for extracting ref candidates*/
  double tCon;    /*Incremental concretization time*/
  double tGFree;
  double tPro; /*time for processing*/
  double tExp; /*time for expandsion*/
  array_t *latchArray;
};

struct PureSatIncreSATManager {
  int beginPosition;
  int Length;
  int oldLength;
  int propertyPos;
  BmcCnfClauses_t *cnfClauses;
  satArray_t *savedConCls;
  satManager_t *cm;
};


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

typedef enum {
  dfsWhite_c,   /* unvisited node */
  dfsGrey_c,    /* node on "stack" */
  dfsBlack_c    /* node completely visited */
} DfsColor;

typedef struct PureSatManager PureSat_Manager_t;
typedef struct PureSatIncreSATManager PureSat_IncreSATManager_t;


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

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


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

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

EXTERN void PureSatInsertNewClauseForSimplePath(array_t *vertexArray, Ntk_Network_t *network, int step1, int step2, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable);
EXTERN void PureSatInsertNewClauseForInit(array_t *vertexArray, Ntk_Network_t *network, int step1, int step2, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable);
EXTERN void PureSatSetInitStatesForSimplePath(array_t * vertexArray, Ntk_Network_t *network, BmcCnfClauses_t *cnfClauses, st_table * nodeToMvfAigTable);
EXTERN boolean PureSatExistASimplePath(Ntk_Network_t *network, PureSat_IncreSATManager_t * pism, array_t * vertexArray, bAigEdge_t property, PureSat_Manager_t * pm);
EXTERN boolean PureSatExistCE(Ntk_Network_t * network, PureSat_IncreSATManager_t * pism, BmcOption_t *options, array_t *vertexArray, bAigEdge_t property, PureSat_Manager_t * pm, int extractCexInfo);
EXTERN boolean PureSatIncreExistCE(Ntk_Network_t * network, PureSat_IncreSATManager_t *pism, array_t *vertexArray, bAigEdge_t property, PureSat_Manager_t * pm);
EXTERN boolean PureSatIncreExistCEForRefineOnAbs(Ntk_Network_t *network, PureSat_IncreSATManager_t *pism, array_t *vertexArray, bAigEdge_t property, boolean firstTime, PureSat_Manager_t * pm);
EXTERN void PureSatGenerateClausesFromStateTostateWithTable(bAig_Manager_t *manager, bAigEdge_t *fromAigArray, bAigEdge_t *toAigArray, int mvfSize, int fromState, int toState, BmcCnfClauses_t *cnfClauses, int outIndex, st_table *ClsidxToLatchTable, char *nodeName);
EXTERN void PureSatGenerateClausesForPath_EnhanceInit(Ntk_Network_t *network, int from, int to, PureSat_IncreSATManager_t * pism, PureSat_Manager_t * pm, st_table *nodeToMvfAigTable, st_table *CoiTable);
EXTERN boolean PureSatCheckInv_SSS(Ntk_Network_t * network, Ctlsp_Formula_t *ltlFormula, PureSat_Manager_t *pm);

EXTERN boolean PureSatCheckInv_FlatIP(Ntk_Network_t * network,
				      Ctlsp_Formula_t *ltlFormula,
				      PureSat_Manager_t *pm);
EXTERN void PureSatCmdParse(int argc, char **argv, PureSat_Manager_t *pm);
EXTERN array_t * PureSatRefineOnAbs(Ntk_Network_t *network, PureSat_Manager_t *pm, bAigEdge_t property, int latchThreshHold);
EXTERN PureSat_Manager_t * PureSatManagerAlloc(void);
EXTERN void PureSatManagerFree(PureSat_Manager_t * pm);
EXTERN PureSat_IncreSATManager_t * PureSatIncreSATManagerAlloc(PureSat_Manager_t * pm);
EXTERN void PureSatIncreSATManagerFree(PureSat_Manager_t *pm, PureSat_IncreSATManager_t * pism);
EXTERN void PureSatBmcGetCoiForNtkNode(Ntk_Node_t *node, st_table *CoiTable, st_table *visited);
EXTERN void PureSatBmcGetCoiForLtlFormulaRecursive(Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable, st_table *visited);
EXTERN DfsColor PureSatNodeReadColor(Ntk_Node_t * node);
EXTERN void PureSatNodeSetColor(Ntk_Node_t * node, DfsColor color);
EXTERN void PureSatNodeRecursivelyComputeTransitiveFaninNodes_AllNodes(Ntk_Node_t *node, int * NumofSupports, boolean stopAtLatches);
EXTERN int PureSatNodeComputeCombinationalSupport_AllNodes(Ntk_Network_t *network, array_t * nodeArray, boolean stopAtLatches);
EXTERN void PureSatGenerateSupportTable(Ntk_Network_t *network, PureSat_Manager_t *pm);
EXTERN void PureSatBmcGetCoiForLtlFormula(Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable);
EXTERN void PureSatGetFormulaNodes(Ntk_Network_t *network, Ctlsp_Formula_t *F, array_t *formulaNodes);
EXTERN void PureSatGetFaninLatches(Ntk_Node_t *node, st_table *visited, st_table *vertexTable);
EXTERN st_table * PureSatCreateInitialAbstraction(Ntk_Network_t *network, Ctlsp_Formula_t *invFormula, int * Num, PureSat_Manager_t *pm);
EXTERN void PureSatRecursivelyComputeTableForLatch(Ntk_Network_t * network, st_table *Table, Ntk_Node_t * node);
EXTERN void PureSatComputeTableForLatch(Ntk_Network_t * network, st_table * Table, Ntk_Node_t * Latch);
EXTERN void PureSatGetCoiForVisibleArray_Ring(Ntk_Network_t *network, array_t *visibleArray, int position, st_table *ltlCoiTable);
EXTERN int NumInConeCompare(int *ptrX, int *ptrY);
EXTERN int NumInConeCompare_Ring(int *ptrX, int *ptrY);
EXTERN void PureSatRecursivelyComputeCorrelationforLatch(Ntk_Network_t *network, st_table *AbsTable, st_table * visited, Ntk_Node_t *node, int *count);
EXTERN int PureSatComputeCorrelationforLatch(Ntk_Network_t * network, st_table * AbsTable, Ntk_Node_t *Latch);
EXTERN array_t * PureSatGenerateRingFromAbs(Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *invisibleArray, int * NumInSecondLevel);
EXTERN void PureSatCleanSat(satManager_t * cm);
EXTERN void PureSatReadClauses(PureSat_IncreSATManager_t * pism, PureSat_Manager_t * pm);
EXTERN array_t * PureSatGetImmediateSupportLatches(Ntk_Network_t *network, int beginPosition, array_t *latchNameArray);
EXTERN void PureSatWriteClausesToFile(PureSat_IncreSATManager_t * pism, mAig_Manager_t *maigManager, char *coreFile);
EXTERN void PureSatWriteAllClausesToFile(PureSat_IncreSATManager_t * pism, char *coreFile);
EXTERN array_t * PureSatGetLatchFromTable(Ntk_Network_t *network, PureSat_Manager_t * pm, char *coreFile);
EXTERN array_t * PureSatRemove_char(array_t * array1, int i);

EXTERN boolean PureSat_CheckAceByIP(Ntk_Network_t *network,
			     PureSat_Manager_t * pm,
			     PureSat_IncreSATManager_t *pism,
			     array_t *vertexArray,
			     int * k,
			     Ctlsp_Formula_t *ltlFormula,
			     bAigEdge_t * returnProp,
				    array_t *previousResultArray);
EXTERN boolean PureSatCheckInv_IP(Ntk_Network_t * network, Ctlsp_Formula_t *ltlFormula, PureSat_Manager_t *pm);
EXTERN boolean PureSatIPOnCon(Ntk_Network_t * network, Ctlsp_Formula_t *ltlFormula,PureSat_Manager_t *pm);
EXTERN array_t * PureSat_GetSufAbsFromCore(Ntk_Network_t *network,satManager_t * cm,PureSat_Manager_t *pm,bAigEdge_t property,st_table * SufAbsNameTable);
EXTERN void PureSat_GetSufAbsFromCoreRecur(mAig_Manager_t *manager,satManager_t * cm,RTnode_t RTnode, st_table *ctTable, st_table *refineTable);
EXTERN void PureSat_GetSufAbsFromCoreRecur_2side(mAig_Manager_t *manager,satManager_t * cm,RTnode_t RTnode,st_table *ctTable,st_table *refineTable,st_table *SufNameTable);
EXTERN array_t *PureSat_RefineOnAbs(Ntk_Network_t *network,PureSat_Manager_t *pm,bAigEdge_t property,array_t *previousResultArray,int latchThreshHold,int * sccArray,array_t * sufArray);
EXTERN RTnode_t RTCreateNode(RTManager_t * rm);
EXTERN IP_Manager_t * IPManagerAlloc();
EXTERN void IPManagerFree(IP_Manager_t *ipm);
EXTERN int PureSat_IdentifyConflict(
  satManager_t *cm,
  long left,
  bAigEdge_t right,
  bAigEdge_t node);
EXTERN void PureSatBmcGetCoiForNtkNode_New(
  Ntk_Node_t  *node,
  st_table    *CoiTable,
  st_table    *visited);
EXTERN void PureSatBmcGetCoiForLtlFormulaRecursive_New(
  Ntk_Network_t   *network,
  Ctlsp_Formula_t *formula,
  st_table        *ltlCoiTable,
  st_table        *visited);
EXTERN void PureSatBmcGetCoiForLtlFormula_New(
  Ntk_Network_t   *network,
  Ctlsp_Formula_t *formula,
  st_table        *ltlCoiTable);
EXTERN void PureSat_MarkTransitiveFaninForNode(
	satManager_t *cm,
	bAigEdge_t v,
	unsigned int mask);
EXTERN void PureSat_MarkTransitiveFaninForArray(
	satManager_t *cm,
	satArray_t *arr,
	unsigned int mask);
EXTERN void PureSat_MarkTransitiveFaninForNode2(
	mAig_Manager_t *manager,
	bAigEdge_t v,
	unsigned int mask);
EXTERN void PureSat_MarkTransitiveFaninForArray2(
	mAig_Manager_t *manager,
	satArray_t *arr,
	unsigned int mask);
EXTERN void PureSat_MarkTransitiveFaninForNode3(
	mAig_Manager_t *manager,
	bAigEdge_t v,
	unsigned int mask);
EXTERN void PureSat_MarkTransitiveFaninForArray3(
	mAig_Manager_t *manager,
	satArray_t *arr,
	unsigned int mask);
EXTERN void PureSat_MarkTransitiveFaninForNode4(
	mAig_Manager_t *manager,
	bAigEdge_t v,
	unsigned int mask,
	int bound);
EXTERN void PureSat_MarkTransitiveFaninForArray4(
	mAig_Manager_t *manager,
	satArray_t *arr,
	unsigned int mask,
	int bound);
EXTERN void PureSat_CleanMask(mAig_Manager_t *manager,
			      unsigned int mask);
EXTERN void PureSat_ResetCoi(satManager_t *cm);
EXTERN void PureSat_SetCOI(satManager_t *cm);
EXTERN void PureSatSetLatchCOI(Ntk_Network_t * network,
			       PureSat_Manager_t *pm,
			       satManager_t * cm,
			       st_table * AbsTable,
			       int from,
			       int to);
EXTERN void PureSatSetLatchCOI2(Ntk_Network_t * network,
				PureSat_Manager_t *pm,
				satManager_t * cm,
				bAigEdge_t obj,
				int bound);
EXTERN void PureSatSetCOI(Ntk_Network_t * network,
			  PureSat_Manager_t *pm,
			  satManager_t * cm,
			  st_table * AbsTable,
			  int from,
			  int to,
			  int bound);
EXTERN void PureSatAbstractLatch(bAig_Manager_t *manager,
			  bAigEdge_t v,
			  st_table * tmpTable);
EXTERN void PureSatKillPseudoGVNode(bAig_Manager_t *manager,
				    bAigEdge_t v,
				    st_table * tmpTable);
EXTERN void PureSatKillPseudoGV(Ntk_Network_t * network,
				PureSat_Manager_t *pm,
				st_table * AbsTable,
				int from,
				int to);
EXTERN int PureSat_CountNodesInCoi(satManager_t* cm);
EXTERN void PureSat_ResetManager(mAig_Manager_t *manager,
				 satManager_t *cm, int clean);
EXTERN void PureSat_RestoreAigForDummyNode(mAig_Manager_t *manager,
					   int oldPosition);
EXTERN void PureSatProcessFanout(satManager_t * cm);
EXTERN long PureSatRecoverFanoutNode(satManager_t * cm,
				     bAigEdge_t v);
EXTERN void PureSatRecoverISVNode(satManager_t *cm,
			     bAigEdge_t v);
EXTERN void PureSatRecoverFanout(satManager_t * cm,
				 PureSat_Manager_t *pm);
EXTERN void PureSatPreprocess(Ntk_Network_t * network,
			      satManager_t *cm,
			      PureSat_Manager_t *pm,
			      st_table *vertexTable,
			      int Length);
EXTERN void PureSatPostprocess(bAig_Manager_t *manager,
			       satManager_t *cm,
			       PureSat_Manager_t *pm);
/*EXTERN int PureSat_TestImply_AbRf(Ntk_Network_t *network,
				  satManager_t *cm,
				  PureSat_Manager_t *pm,
				  st_table *vertexTable,
				  bAigEdge_t state1,
				  bAigEdge_t state2);*/
EXTERN int PureSat_TestConvergeForIP(mAig_Manager_t *manager,
				     PureSat_Manager_t *pm,
				     satManager_t *cm,
				     bAigEdge_t state1,
				     bAigEdge_t state2);
EXTERN int PureSat_TestConvergeForIP_AbRf(Ntk_Network_t *network,
				   satManager_t *cm,
				   PureSat_Manager_t *pm,
				   array_t  * CoiArray,
				   bAigEdge_t state1,
					  bAigEdge_t state2);
EXTERN satManager_t * PureSat_SatManagerAlloc(bAig_Manager_t *manager,
					      PureSat_Manager_t *pm,
					      bAigEdge_t     object,
					      array_t        *auxObjectArray);
EXTERN satManager_t * PureSat_SatManagerAlloc_WOCOI(mAig_Manager_t *manager,
						    PureSat_Manager_t *pm,
						    bAigEdge_t     object,
						    array_t    *auxObjectArray);
EXTERN void PureSat_SatFreeManager(satManager_t*cm);
EXTERN void PureSat_PrintAigStatus(mAig_Manager_t *manager);
EXTERN void PureSat_unconnectOutput(
   bAig_Manager_t *manager,
   bAigEdge_t from,
   bAigEdge_t to);
EXTERN void PureSat_MarkGlobalVar(bAig_Manager_t *manager,
				  int length);
EXTERN void PureSat_UnMarkGlobalVar(bAig_Manager_t *manager,
				    int length);
EXTERN void PureSat_MarkGlobalVar_AbRf(bAig_Manager_t *manager,
				       int length);
EXTERN void PuresatMarkVisibleVarWithVPGV(Ntk_Network_t *network,
				  array_t * visibleArray,
				  PureSat_Manager_t *pm,
				  int from,
					  int to);
EXTERN void PuresatMarkVisibleVar(Ntk_Network_t *network,
			   array_t * visibleArray,
			   PureSat_Manager_t *pm,
			   int from,
				  int to);
EXTERN bAigEdge_t PureSat_MapIPRecur(mAig_Manager_t *manager,
			 bAigEdge_t  node,
				     st_table * tmpTable);
EXTERN bAigEdge_t PureSat_MapIP(mAig_Manager_t *manager,
			 bAigEdge_t node,
			 int from,
				int to);
EXTERN void PureSatProcessDummy(bAig_Manager_t *manager,
			 satManager_t *cm,
			 RTnode_t  RTnode);
EXTERN bAigEdge_t
PureSat_FindNodeByName(
  bAig_Manager_t *manager,
  nameType_t     *name,
  int bound);
EXTERN bAigEdge_t
PureSatCreatebAigOfPropFormula(
    Ntk_Network_t *network,
    bAig_Manager_t *manager,
    int bound,
    Ctlsp_Formula_t *ltl,
    int withInitialState);
EXTERN void PureSatMarkObj(bAig_Manager_t * manager,
		    long from,
		    long to);
EXTERN boolean PureSat_ConcretTest(Ntk_Network_t *network,
			    PureSat_Manager_t *pm,
			    array_t *sufArray,
			    bAigEdge_t property,
			    array_t *previousResultArray,
			    int Con,
			    int satStat,
				   int inc);
EXTERN boolean PureSat_ConcretTest_Core(Ntk_Network_t *network,
				 PureSat_Manager_t *pm,
				 array_t *sufArray,
				 bAigEdge_t property,
				 array_t *previousResultArray,
					st_table * junkTable);
EXTERN void PureSatGenerateRingForNode(Ntk_Network_t *network,
				PureSat_Manager_t *pm,
				Ntk_Node_t * node1,
				array_t * ringArray,
				//st_table * node2dfsTable,
				       int *dfs);
EXTERN array_t * PureSatGenerateRing(Ntk_Network_t *network,
			      PureSat_Manager_t *pm,
			      array_t * coreArray,
			      //  st_table *node2dfsTable,
				     int * dfs);
EXTERN void PureSatGenerateDfs(Ntk_Network_t *network,
			PureSat_Manager_t *pm,
			       array_t * vertexArray);
/*EXTERN array_t * PureSatGenerateRCArray(Ntk_Network_t *network,
				 PureSat_Manager_t *pm,
				 array_t *invisibleArray,
				// st_table * node2dfsTable,
				 int *sccArray,
				 int *NumInSecondLevel);*/
EXTERN void PureSatComputeNumGatesInAbsForNode(Ntk_Network_t * network,
					PureSat_Manager_t * pm,
					Ntk_Node_t * node,
					st_table * visited,
					int  * ct,
					       int  * ct1);
EXTERN void PureSatComputeNumGatesInAbs(Ntk_Network_t *network,
				PureSat_Manager_t *pm,
					array_t * invisibleArray);
EXTERN void PureSatComputeNumGatesInConeForNode(Ntk_Network_t * network,
				       PureSat_Manager_t * pm,
				       Ntk_Node_t * node,
				       st_table * visited,
						int  * ct);
EXTERN void PureSatComputeNumGatesInCone(Ntk_Network_t *network,
				PureSat_Manager_t *pm,
					 array_t * latchArray);
EXTERN array_t * PureSatGenerateRCArray_2(Ntk_Network_t *network,
				   PureSat_Manager_t *pm,
				   array_t *invisibleArray,
					  int *NumInSecondLevel);
/*EXTERN array_t * PureSatComputeOrder(Ntk_Network_t *network,
			      PureSat_Manager_t *pm,
			      array_t * vertexArray,
			      array_t * invisibleArray,
			      int * sccArray,
			      int * NumInSecondLevel);*/
EXTERN array_t * PureSatComputeOrder_2(Ntk_Network_t *network,
			      PureSat_Manager_t *pm,
			      array_t * vertexArray,
			      array_t * invisibleArray,
			      int * sccArray,
				       int * NumInSecondLevel);
EXTERN void PureSatAddIdenLatchToAbs(Ntk_Network_t *network,
			      PureSat_Manager_t *pm,
				     array_t *nameArray);
EXTERN void PureSatCreateInitAbsByAIG(bAig_Manager_t *manager,
			  PureSat_Manager_t *pm,
			  bAigEdge_t node,
				 st_table * tmpTable);
EXTERN void PureSat_GetLatchForNode(bAig_Manager_t *manager,
			PureSat_Manager_t *pm,
			bAigEdge_t node,
			array_t * nameArray,
			st_table *tmpTable,
				    int cut);
EXTERN st_table * PureSatGetAigCoi(Ntk_Network_t *network,
			    PureSat_Manager_t *pm,
				   bAigEdge_t property);
EXTERN void PureSatPreProcLatch(Ntk_Network_t *network,
				PureSat_Manager_t *pm);
EXTERN void PureSatGetIndenticalLatch(Ntk_Network_t *network,
				      PureSat_Manager_t *pm);
EXTERN void PureSat_connectOutput(
   bAig_Manager_t *manager,
   bAigEdge_t from,
   bAigEdge_t to,
   int inputIndex);
EXTERN bAigEdge_t
PureSat_HashTableLookup(
  bAig_Manager_t *manager,
  bAigEdge_t  node1,
  bAigEdge_t  node2);
EXTERN int
PureSat_HashTableAdd(
  bAig_Manager_t   *manager,
  bAigEdge_t  nodeIndexParent,
  bAigEdge_t  nodeIndex1,
  bAigEdge_t  nodeIndex2);
EXTERN bAigEdge_t
PureSat_CreateAndNode(
   bAig_Manager_t  *manager,
   bAigEdge_t node1,
   bAigEdge_t node2);
EXTERN bAigEdge_t
PureSat_And2(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2);
EXTERN bAigEdge_t
PureSat_And3(
	   bAig_Manager_t *manager,
	   bAigEdge_t l,
	   bAigEdge_t r);
EXTERN bAigEdge_t
PureSat_And4(
	   bAig_Manager_t *manager,
	   bAigEdge_t l,
	   bAigEdge_t r);
EXTERN int PureSat_Test2LevelMini(bAig_Manager_t *manager,
			   bAigEdge_t l,
			   bAigEdge_t r);
EXTERN bAigEdge_t
PureSat_And(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2);
EXTERN bAigEdge_t
PureSat_Or(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2);
EXTERN bAigEdge_t
PureSat_Xor(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2);
EXTERN bAigEdge_t
PureSat_Eq(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2);
EXTERN bAigEdge_t
PureSat_Then(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2);
EXTERN bAigEdge_t
PureSat_CreateVarNode(
   bAig_Manager_t  *manager,
   nameType_t	   *name);
EXTERN int AS_ImplyStop( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int AS_ImplySplit( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int AS_ImplyConflict( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int AS_ImplyLeftForward( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int AS_ImplyRightForward( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int AS_ImplyForwardOne( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int AS_ImplyPropRight( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int AS_ImplyPropRightOne( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int AS_ImplyPropLeft( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int AS_ImplyPropLeftOne( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN int AS_ImplyPropLeftRight( satManager_t *cm, satLevel_t *d, long v, long left, long right);
EXTERN void
AS_Undo(
	satManager_t *cm,
	satLevel_t *d);
EXTERN void
AS_ImplyCNF(
	satManager_t *cm,
	satLevel_t *d,
	long v,
	satArray_t *wl);
EXTERN int
AS_ImplyNode(
	satManager_t *cm,
	satLevel_t *d,
	long v);

EXTERN void AS_ImplicationMain(
	satManager_t *cm,
	satLevel_t *d);
EXTERN void
AS_ImplyArray(
	satManager_t *cm,
	satLevel_t *d,
	satArray_t *arr);
EXTERN void
AS_PreProcessing(satManager_t *cm);
EXTERN void
AS_Backtrack(
	satManager_t *cm,
	int level);
EXTERN void
AS_UpdateScore(
  satManager_t *cm);
EXTERN void
AS_PeriodicFunctions(satManager_t *cm);
EXTERN satLevel_t *
AS_MakeDecision(satManager_t *cm);
EXTERN void
AS_FindUIP(
	satManager_t *cm,
	satArray_t *clauseArray,
	satLevel_t *d,
	int *objectFlag,
	int *bLevel,
	long *fdaLit);
EXTERN int
AS_ConflictAnalysis(
	satManager_t *cm,
	satLevel_t *d);
EXTERN void
AS_Solve(satManager_t *cm);
EXTERN void AS_Main(satManager_t *cm);
EXTERN void PureSatCreateOneLayer(Ntk_Network_t *network,
				  PureSat_Manager_t *pm,
				  satManager_t *cm,
				  array_t * latchArray,
				  int layer);
EXTERN void PureSatCreateLayer(Ntk_Network_t *network,
			       PureSat_Manager_t *pm,
			       satManager_t *cm,
			       array_t *absModel,
			       array_t *sufArray);
EXTERN void bAig_PureSat_ExpandTimeFrame(
	Ntk_Network_t *network,
	mAig_Manager_t *manager,
	PureSat_Manager_t *pm,
	int bound,
	int withInitialState);
EXTERN bAigTimeFrame_t * bAig_PureSat_InitTimeFrame(
	Ntk_Network_t *network,
	mAig_Manager_t *manager,
	PureSat_Manager_t *pm,
	int withInitialState);
EXTERN void PureSatCheckCoi(bAig_Manager_t *manager);
EXTERN void PureSat_CheckFanoutFanin(bAig_Manager_t *manager);

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

#endif /*_PURESATINT*/