ivy.h File Reference

#include <stdio.h>
#include "misc/extra/extra.h"
#include "misc/vec/vec.h"

Go to the source code of this file.

Data Structures
struct	Ivy_Obj_t_
struct	Ivy_Man_t_
struct	Ivy_FraigParams_t_
struct	Ivy_Cut_t_
struct	Ivy_Store_t_

Macros
#define	IVY_CUT_LIMIT   256
#define	IVY_CUT_INPUT   6
#define	IVY_LEAF_MASK   255
#define	IVY_LEAF_BITS   8
#define	IVY_MIN(a, b)   (((a) < (b))? (a) : (b))
	MACRO DEFINITIONS ///. More...
#define	IVY_MAX(a, b)   (((a) > (b))? (a) : (b))
#define	Ivy_ManForEachPi(p, pObj, i)   Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPis, pObj, i )
	ITERATORS ///. More...
#define	Ivy_ManForEachPo(p, pObj, i)   Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPos, pObj, i )
#define	Ivy_ManForEachObj(p, pObj, i)   Vec_PtrForEachEntry( Ivy_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
#define	Ivy_ManForEachCi(p, pObj, i)   Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCi(pObj) ) {} else
#define	Ivy_ManForEachCo(p, pObj, i)   Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCo(pObj) ) {} else
#define	Ivy_ManForEachNode(p, pObj, i)   Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsNode(pObj) ) {} else
#define	Ivy_ManForEachLatch(p, pObj, i)   Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsLatch(pObj) ) {} else
#define	Ivy_ManForEachNodeVec(p, vIds, pObj, i)   for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Ivy_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
#define	Ivy_ObjForEachFanout(p, pObj, vArray, pFanout, i)

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Ivy_Man_t_	Ivy_Man_t
	INCLUDES ///. More...
typedef struct Ivy_Obj_t_	Ivy_Obj_t
typedef int	Ivy_Edge_t
typedef struct Ivy_FraigParams_t_	Ivy_FraigParams_t
typedef struct Ivy_Cut_t_	Ivy_Cut_t
typedef struct Ivy_Store_t_	Ivy_Store_t

Enumerations
enum	Ivy_Type_t {   IVY_NONE, IVY_PI, IVY_PO, IVY_ASSERT,   IVY_LATCH, IVY_AND, IVY_EXOR, IVY_BUF,   IVY_VOID }
enum	Ivy_Init_t { IVY_INIT_NONE, IVY_INIT_0, IVY_INIT_1, IVY_INIT_DC }

Functions
void	Ivy_ManAddMemory (Ivy_Man_t *p)
static int	Ivy_BitWordNum (int nBits)
static int	Ivy_TruthWordNum (int nVars)
static int	Ivy_InfoHasBit (unsigned *p, int i)
static void	Ivy_InfoSetBit (unsigned *p, int i)
static void	Ivy_InfoXorBit (unsigned *p, int i)
static Ivy_Obj_t *	Ivy_Regular (Ivy_Obj_t *p)
static Ivy_Obj_t *	Ivy_Not (Ivy_Obj_t *p)
static Ivy_Obj_t *	Ivy_NotCond (Ivy_Obj_t *p, int c)
static int	Ivy_IsComplement (Ivy_Obj_t *p)
static Ivy_Obj_t *	Ivy_ManConst0 (Ivy_Man_t *p)
static Ivy_Obj_t *	Ivy_ManConst1 (Ivy_Man_t *p)
static Ivy_Obj_t *	Ivy_ManGhost (Ivy_Man_t *p)
static Ivy_Obj_t *	Ivy_ManPi (Ivy_Man_t *p, int i)
static Ivy_Obj_t *	Ivy_ManPo (Ivy_Man_t *p, int i)
static Ivy_Obj_t *	Ivy_ManObj (Ivy_Man_t *p, int i)
static Ivy_Edge_t	Ivy_EdgeCreate (int Id, int fCompl)
static int	Ivy_EdgeId (Ivy_Edge_t Edge)
static int	Ivy_EdgeIsComplement (Ivy_Edge_t Edge)
static Ivy_Edge_t	Ivy_EdgeRegular (Ivy_Edge_t Edge)
static Ivy_Edge_t	Ivy_EdgeNot (Ivy_Edge_t Edge)
static Ivy_Edge_t	Ivy_EdgeNotCond (Ivy_Edge_t Edge, int fCond)
static Ivy_Edge_t	Ivy_EdgeFromNode (Ivy_Obj_t *pNode)
static Ivy_Obj_t *	Ivy_EdgeToNode (Ivy_Man_t *p, Ivy_Edge_t Edge)
static int	Ivy_LeafCreate (int Id, int Lat)
static int	Ivy_LeafId (int Leaf)
static int	Ivy_LeafLat (int Leaf)
static int	Ivy_ManPiNum (Ivy_Man_t *p)
static int	Ivy_ManPoNum (Ivy_Man_t *p)
static int	Ivy_ManAssertNum (Ivy_Man_t *p)
static int	Ivy_ManLatchNum (Ivy_Man_t *p)
static int	Ivy_ManAndNum (Ivy_Man_t *p)
static int	Ivy_ManExorNum (Ivy_Man_t *p)
static int	Ivy_ManBufNum (Ivy_Man_t *p)
static int	Ivy_ManObjNum (Ivy_Man_t *p)
static int	Ivy_ManObjIdMax (Ivy_Man_t *p)
static int	Ivy_ManNodeNum (Ivy_Man_t *p)
static int	Ivy_ManHashObjNum (Ivy_Man_t *p)
static int	Ivy_ManGetCost (Ivy_Man_t *p)
static Ivy_Type_t	Ivy_ObjType (Ivy_Obj_t *pObj)
static Ivy_Init_t	Ivy_ObjInit (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsConst1 (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsGhost (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsNone (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsPi (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsPo (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsCi (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsCo (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsAssert (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsLatch (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsAnd (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsExor (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsBuf (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsNode (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsTerm (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsHash (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsOneFanin (Ivy_Obj_t *pObj)
static int	Ivy_ObjIsMarkA (Ivy_Obj_t *pObj)
static void	Ivy_ObjSetMarkA (Ivy_Obj_t *pObj)
static void	Ivy_ObjClearMarkA (Ivy_Obj_t *pObj)
static void	Ivy_ObjSetTravId (Ivy_Obj_t *pObj, int TravId)
static void	Ivy_ObjSetTravIdCurrent (Ivy_Man_t *p, Ivy_Obj_t *pObj)
static void	Ivy_ObjSetTravIdPrevious (Ivy_Man_t *p, Ivy_Obj_t *pObj)
static int	Ivy_ObjIsTravIdCurrent (Ivy_Man_t *p, Ivy_Obj_t *pObj)
static int	Ivy_ObjIsTravIdPrevious (Ivy_Man_t *p, Ivy_Obj_t *pObj)
static int	Ivy_ObjId (Ivy_Obj_t *pObj)
static int	Ivy_ObjTravId (Ivy_Obj_t *pObj)
static int	Ivy_ObjPhase (Ivy_Obj_t *pObj)
static int	Ivy_ObjExorFanout (Ivy_Obj_t *pObj)
static int	Ivy_ObjRefs (Ivy_Obj_t *pObj)
static void	Ivy_ObjRefsInc (Ivy_Obj_t *pObj)
static void	Ivy_ObjRefsDec (Ivy_Obj_t *pObj)
static int	Ivy_ObjFaninId0 (Ivy_Obj_t *pObj)
static int	Ivy_ObjFaninId1 (Ivy_Obj_t *pObj)
static int	Ivy_ObjFaninC0 (Ivy_Obj_t *pObj)
static int	Ivy_ObjFaninC1 (Ivy_Obj_t *pObj)
static Ivy_Obj_t *	Ivy_ObjFanin0 (Ivy_Obj_t *pObj)
static Ivy_Obj_t *	Ivy_ObjFanin1 (Ivy_Obj_t *pObj)
static Ivy_Obj_t *	Ivy_ObjChild0 (Ivy_Obj_t *pObj)
static Ivy_Obj_t *	Ivy_ObjChild1 (Ivy_Obj_t *pObj)
static Ivy_Obj_t *	Ivy_ObjChild0Equiv (Ivy_Obj_t *pObj)
static Ivy_Obj_t *	Ivy_ObjChild1Equiv (Ivy_Obj_t *pObj)
static Ivy_Obj_t *	Ivy_ObjEquiv (Ivy_Obj_t *pObj)
static int	Ivy_ObjLevel (Ivy_Obj_t *pObj)
static int	Ivy_ObjLevelNew (Ivy_Obj_t *pObj)
static int	Ivy_ObjFaninPhase (Ivy_Obj_t *pObj)
static void	Ivy_ObjClean (Ivy_Obj_t *pObj)
static void	Ivy_ObjOverwrite (Ivy_Obj_t *pBase, Ivy_Obj_t *pData)
static int	Ivy_ObjWhatFanin (Ivy_Obj_t *pObj, Ivy_Obj_t *pFanin)
static int	Ivy_ObjFanoutC (Ivy_Obj_t *pObj, Ivy_Obj_t *pFanout)
static Ivy_Obj_t *	Ivy_ObjCreateGhost (Ivy_Man_t *p, Ivy_Obj_t *p0, Ivy_Obj_t *p1, Ivy_Type_t Type, Ivy_Init_t Init)
static Ivy_Init_t	Ivy_InitNotCond (Ivy_Init_t Init, int fCompl)
static Ivy_Init_t	Ivy_InitAnd (Ivy_Init_t InitA, Ivy_Init_t InitB)
static Ivy_Init_t	Ivy_InitExor (Ivy_Init_t InitA, Ivy_Init_t InitB)
static Ivy_Obj_t *	Ivy_ManFetchMemory (Ivy_Man_t *p)
static void	Ivy_ManRecycleMemory (Ivy_Man_t *p, Ivy_Obj_t *pEntry)
Ivy_Man_t *	Ivy_ManBalance (Ivy_Man_t *p, int fUpdateLevel)
	FUNCTION DECLARATIONS ///. More...
Ivy_Obj_t *	Ivy_NodeBalanceBuildSuper (Ivy_Man_t *p, Vec_Ptr_t *vSuper, Ivy_Type_t Type, int fUpdateLevel)
Ivy_Obj_t *	Ivy_CanonAnd (Ivy_Man_t *p, Ivy_Obj_t *p0, Ivy_Obj_t *p1)
Ivy_Obj_t *	Ivy_CanonExor (Ivy_Man_t *p, Ivy_Obj_t *p0, Ivy_Obj_t *p1)
Ivy_Obj_t *	Ivy_CanonLatch (Ivy_Man_t *p, Ivy_Obj_t *pObj, Ivy_Init_t Init)
int	Ivy_ManCheck (Ivy_Man_t *p)
	DECLARATIONS ///. More...
int	Ivy_ManCheckFanoutNums (Ivy_Man_t *p)
int	Ivy_ManCheckFanouts (Ivy_Man_t *p)
int	Ivy_ManCheckChoices (Ivy_Man_t *p)
void	Ivy_ManSeqFindCut (Ivy_Man_t *p, Ivy_Obj_t *pNode, Vec_Int_t *vFront, Vec_Int_t *vInside, int nSize)
Ivy_Store_t *	Ivy_NodeFindCutsAll (Ivy_Man_t *p, Ivy_Obj_t *pObj, int nLeaves)
Vec_Int_t *	Ivy_ManDfs (Ivy_Man_t *p)
Vec_Int_t *	Ivy_ManDfsSeq (Ivy_Man_t *p, Vec_Int_t **pvLatches)
void	Ivy_ManCollectCone (Ivy_Obj_t *pObj, Vec_Ptr_t *vFront, Vec_Ptr_t *vCone)
Vec_Vec_t *	Ivy_ManLevelize (Ivy_Man_t *p)
Vec_Int_t *	Ivy_ManRequiredLevels (Ivy_Man_t *p)
int	Ivy_ManIsAcyclic (Ivy_Man_t *p)
int	Ivy_ManSetLevels (Ivy_Man_t *p, int fHaig)
int	Ivy_TruthDsd (unsigned uTruth, Vec_Int_t *vTree)
	FUNCTION DEFINITIONS ///. More...
void	Ivy_TruthDsdPrint (FILE *pFile, Vec_Int_t *vTree)
unsigned	Ivy_TruthDsdCompute (Vec_Int_t *vTree)
void	Ivy_TruthDsdComputePrint (unsigned uTruth)
Ivy_Obj_t *	Ivy_ManDsdConstruct (Ivy_Man_t *p, Vec_Int_t *vFront, Vec_Int_t *vTree)
void	Ivy_ManStartFanout (Ivy_Man_t *p)
	FUNCTION DEFINITIONS ///. More...
void	Ivy_ManStopFanout (Ivy_Man_t *p)
void	Ivy_ObjAddFanout (Ivy_Man_t *p, Ivy_Obj_t *pObj, Ivy_Obj_t *pFanout)
void	Ivy_ObjDeleteFanout (Ivy_Man_t *p, Ivy_Obj_t *pObj, Ivy_Obj_t *pFanout)
void	Ivy_ObjPatchFanout (Ivy_Man_t *p, Ivy_Obj_t *pObj, Ivy_Obj_t *pFanoutOld, Ivy_Obj_t *pFanoutNew)
void	Ivy_ObjCollectFanouts (Ivy_Man_t *p, Ivy_Obj_t *pObj, Vec_Ptr_t *vArray)
Ivy_Obj_t *	Ivy_ObjReadFirstFanout (Ivy_Man_t *p, Ivy_Obj_t *pObj)
int	Ivy_ObjFanoutNum (Ivy_Man_t *p, Ivy_Obj_t *pObj)
void	Ivy_FastMapPerform (Ivy_Man_t *pAig, int nLimit, int fRecovery, int fVerbose)
	FUNCTION DEFINITIONS ///. More...
void	Ivy_FastMapStop (Ivy_Man_t *pAig)
void	Ivy_FastMapReadSupp (Ivy_Man_t *pAig, Ivy_Obj_t *pObj, Vec_Int_t *vLeaves)
void	Ivy_FastMapReverseLevel (Ivy_Man_t *pAig)
int	Ivy_FraigProve (Ivy_Man_t **ppManAig, void *pPars)
Ivy_Man_t *	Ivy_FraigPerform (Ivy_Man_t *pManAig, Ivy_FraigParams_t *pParams)
Ivy_Man_t *	Ivy_FraigMiter (Ivy_Man_t *pManAig, Ivy_FraigParams_t *pParams)
void	Ivy_FraigParamsDefault (Ivy_FraigParams_t *pParams)
	FUNCTION DEFINITIONS ///. More...
void	Ivy_ManHaigStart (Ivy_Man_t *p, int fVerbose)
	FUNCTION DEFINITIONS ///. More...
void	Ivy_ManHaigTrasfer (Ivy_Man_t *p, Ivy_Man_t *pNew)
void	Ivy_ManHaigStop (Ivy_Man_t *p)
void	Ivy_ManHaigPostprocess (Ivy_Man_t *p, int fVerbose)
void	Ivy_ManHaigCreateObj (Ivy_Man_t *p, Ivy_Obj_t *pObj)
void	Ivy_ManHaigCreateChoice (Ivy_Man_t *p, Ivy_Obj_t *pObjOld, Ivy_Obj_t *pObjNew)
void	Ivy_ManHaigSimulate (Ivy_Man_t *p)
Ivy_Man_t *	Ivy_ManStart ()
	DECLARATIONS ///. More...
Ivy_Man_t *	Ivy_ManStartFrom (Ivy_Man_t *p)
Ivy_Man_t *	Ivy_ManDup (Ivy_Man_t *p)
Ivy_Man_t *	Ivy_ManFrames (Ivy_Man_t *pMan, int nLatches, int nFrames, int fInit, Vec_Ptr_t **pvMapping)
void	Ivy_ManStop (Ivy_Man_t *p)
int	Ivy_ManCleanup (Ivy_Man_t *p)
int	Ivy_ManPropagateBuffers (Ivy_Man_t *p, int fUpdateLevel)
void	Ivy_ManPrintStats (Ivy_Man_t *p)
void	Ivy_ManMakeSeq (Ivy_Man_t *p, int nLatches, int *pInits)
void	Ivy_ManStartMemory (Ivy_Man_t *p)
	FUNCTION DEFINITIONS ///. More...
void	Ivy_ManStopMemory (Ivy_Man_t *p)
Ivy_Obj_t *	Ivy_Multi (Ivy_Man_t *p, Ivy_Obj_t **pArgs, int nArgs, Ivy_Type_t Type)
Ivy_Obj_t *	Ivy_Multi1 (Ivy_Man_t *p, Ivy_Obj_t **pArgs, int nArgs, Ivy_Type_t Type)
Ivy_Obj_t *	Ivy_Multi_rec (Ivy_Man_t *p, Ivy_Obj_t **ppObjs, int nObjs, Ivy_Type_t Type)
Ivy_Obj_t *	Ivy_MultiBalance_rec (Ivy_Man_t *p, Ivy_Obj_t **pArgs, int nArgs, Ivy_Type_t Type)
int	Ivy_MultiPlus (Ivy_Man_t *p, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t *vSol)
	FUNCTION DEFINITIONS ///. More...
Ivy_Obj_t *	Ivy_ObjCreatePi (Ivy_Man_t *p)
	DECLARATIONS ///. More...
Ivy_Obj_t *	Ivy_ObjCreatePo (Ivy_Man_t *p, Ivy_Obj_t *pDriver)
Ivy_Obj_t *	Ivy_ObjCreate (Ivy_Man_t *p, Ivy_Obj_t *pGhost)
void	Ivy_ObjConnect (Ivy_Man_t *p, Ivy_Obj_t *pObj, Ivy_Obj_t *pFan0, Ivy_Obj_t *pFan1)
void	Ivy_ObjDisconnect (Ivy_Man_t *p, Ivy_Obj_t *pObj)
void	Ivy_ObjPatchFanin0 (Ivy_Man_t *p, Ivy_Obj_t *pObj, Ivy_Obj_t *pFaninNew)
void	Ivy_ObjDelete (Ivy_Man_t *p, Ivy_Obj_t *pObj, int fFreeTop)
void	Ivy_ObjDelete_rec (Ivy_Man_t *p, Ivy_Obj_t *pObj, int fFreeTop)
void	Ivy_ObjReplace (Ivy_Man_t *p, Ivy_Obj_t *pObjOld, Ivy_Obj_t *pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel)
void	Ivy_NodeFixBufferFanins (Ivy_Man_t *p, Ivy_Obj_t *pNode, int fUpdateLevel)
Ivy_Obj_t *	Ivy_Oper (Ivy_Man_t *p, Ivy_Obj_t *p0, Ivy_Obj_t *p1, Ivy_Type_t Type)
	FUNCTION DEFINITIONS ///. More...
Ivy_Obj_t *	Ivy_And (Ivy_Man_t *p, Ivy_Obj_t *p0, Ivy_Obj_t *p1)
Ivy_Obj_t *	Ivy_Or (Ivy_Man_t *p, Ivy_Obj_t *p0, Ivy_Obj_t *p1)
Ivy_Obj_t *	Ivy_Exor (Ivy_Man_t *p, Ivy_Obj_t *p0, Ivy_Obj_t *p1)
Ivy_Obj_t *	Ivy_Mux (Ivy_Man_t *p, Ivy_Obj_t *pC, Ivy_Obj_t *p1, Ivy_Obj_t *p0)
Ivy_Obj_t *	Ivy_Maj (Ivy_Man_t *p, Ivy_Obj_t *pA, Ivy_Obj_t *pB, Ivy_Obj_t *pC)
Ivy_Obj_t *	Ivy_Miter (Ivy_Man_t *p, Vec_Ptr_t *vPairs)
Ivy_Obj_t *	Ivy_Latch (Ivy_Man_t *p, Ivy_Obj_t *pObj, Ivy_Init_t Init)
Ivy_Man_t *	Ivy_ManResyn0 (Ivy_Man_t *p, int fUpdateLevel, int fVerbose)
	DECLARATIONS ///. More...
Ivy_Man_t *	Ivy_ManResyn (Ivy_Man_t *p, int fUpdateLevel, int fVerbose)
Ivy_Man_t *	Ivy_ManRwsat (Ivy_Man_t *pMan, int fVerbose)
int	Ivy_ManSeqRewrite (Ivy_Man_t *p, int fUpdateLevel, int fUseZeroCost)
int	Ivy_ManRewriteAlg (Ivy_Man_t *p, int fUpdateLevel, int fUseZeroCost)
	FUNCTION DEFINITIONS ///. More...
int	Ivy_ManRewritePre (Ivy_Man_t *p, int fUpdateLevel, int fUseZeroCost, int fVerbose)
	FUNCTION DEFINITIONS ///. More...
int	Ivy_ManRewriteSeq (Ivy_Man_t *p, int fUseZeroCost, int fVerbose)
	FUNCTION DEFINITIONS ///. More...
void	Ivy_ManShow (Ivy_Man_t *pMan, int fHaig, Vec_Ptr_t *vBold)
	FUNCTION DEFINITIONS ///. More...
Ivy_Obj_t *	Ivy_TableLookup (Ivy_Man_t *p, Ivy_Obj_t *pObj)
	FUNCTION DEFINITIONS ///. More...
void	Ivy_TableInsert (Ivy_Man_t *p, Ivy_Obj_t *pObj)
void	Ivy_TableDelete (Ivy_Man_t *p, Ivy_Obj_t *pObj)
void	Ivy_TableUpdate (Ivy_Man_t *p, Ivy_Obj_t *pObj, int ObjIdNew)
int	Ivy_TableCountEntries (Ivy_Man_t *p)
void	Ivy_TableProfile (Ivy_Man_t *p)
void	Ivy_ManIncrementTravId (Ivy_Man_t *p)
	DECLARATIONS ///. More...
void	Ivy_ManCleanTravId (Ivy_Man_t *p)
unsigned *	Ivy_ManCutTruth (Ivy_Man_t *p, Ivy_Obj_t *pRoot, Vec_Int_t *vLeaves, Vec_Int_t *vNodes, Vec_Int_t *vTruth)
void	Ivy_ManCollectCut (Ivy_Man_t *p, Ivy_Obj_t *pRoot, Vec_Int_t *vLeaves, Vec_Int_t *vNodes)
Vec_Int_t *	Ivy_ManLatches (Ivy_Man_t *p)
int	Ivy_ManLevels (Ivy_Man_t *p)
void	Ivy_ManResetLevels (Ivy_Man_t *p)
int	Ivy_ObjMffcLabel (Ivy_Man_t *p, Ivy_Obj_t *pObj)
void	Ivy_ObjUpdateLevel_rec (Ivy_Man_t *p, Ivy_Obj_t *pObj)
void	Ivy_ObjUpdateLevelR_rec (Ivy_Man_t *p, Ivy_Obj_t *pObj, int ReqNew)
int	Ivy_ObjIsMuxType (Ivy_Obj_t *pObj)
Ivy_Obj_t *	Ivy_ObjRecognizeMux (Ivy_Obj_t *pObj, Ivy_Obj_t **ppObjT, Ivy_Obj_t **ppObjE)
Ivy_Obj_t *	Ivy_ObjReal (Ivy_Obj_t *pObj)
void	Ivy_ObjPrintVerbose (Ivy_Man_t *p, Ivy_Obj_t *pObj, int fHaig)
void	Ivy_ManPrintVerbose (Ivy_Man_t *p, int fHaig)
int	Ivy_CutTruthPrint (Ivy_Man_t *p, Ivy_Cut_t *pCut, unsigned uTruth)

Macro Definition Documentation

#define IVY_CUT_INPUT   6

Definition at line 153 of file ivy.h.

#define IVY_CUT_LIMIT   256

Definition at line 152 of file ivy.h.

#define IVY_LEAF_BITS   8

Definition at line 176 of file ivy.h.

#define IVY_LEAF_MASK   255

Definition at line 175 of file ivy.h.

#define Ivy_ManForEachCi	(		p,
			pObj,
			i
	)		Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCi(pObj) ) {} else

Definition at line 396 of file ivy.h.

#define Ivy_ManForEachCo	(		p,
			pObj,
			i
	)		Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCo(pObj) ) {} else

Definition at line 399 of file ivy.h.

#define Ivy_ManForEachLatch	(		p,
			pObj,
			i
	)		Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsLatch(pObj) ) {} else

Definition at line 405 of file ivy.h.

#define Ivy_ManForEachNode	(		p,
			pObj,
			i
	)		Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsNode(pObj) ) {} else

Definition at line 402 of file ivy.h.

#define Ivy_ManForEachNodeVec	(		p,
			vIds,
			pObj,
			i
	)		for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Ivy_ManObj(p, Vec_IntEntry(vIds,i))); i++ )

Definition at line 408 of file ivy.h.

#define Ivy_ManForEachObj	(		p,
			pObj,
			i
	)		Vec_PtrForEachEntry( Ivy_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else

Definition at line 393 of file ivy.h.

#define Ivy_ManForEachPi	(		p,
			pObj,
			i
	)		Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPis, pObj, i )

ITERATORS ///.

Definition at line 387 of file ivy.h.

#define Ivy_ManForEachPo	(		p,
			pObj,
			i
	)		Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPos, pObj, i )

Definition at line 390 of file ivy.h.

#define IVY_MAX	(		a,
			b
	)		(((a) > (b))? (a) : (b))

Definition at line 183 of file ivy.h.

#define IVY_MIN	(		a,
			b
	)		(((a) < (b))? (a) : (b))

MACRO DEFINITIONS ///.

Definition at line 182 of file ivy.h.

#define Ivy_ObjForEachFanout	(		p,
			pObj,
			vArray,
			pFanout,
			i
	)

Value:

for ( i = 0, Ivy_ObjCollectFanouts(p, pObj, vArray);                        \
          i < Vec_PtrSize(vArray) && ((pFanout) = (Ivy_Obj_t *)Vec_PtrEntry(vArray,i)); i++ )

Definition at line 411 of file ivy.h.

Typedef Documentation

typedef struct Ivy_Cut_t_ Ivy_Cut_t

Definition at line 155 of file ivy.h.

typedef int Ivy_Edge_t

Definition at line 48 of file ivy.h.

typedef struct Ivy_FraigParams_t_ Ivy_FraigParams_t

Definition at line 49 of file ivy.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Ivy_Man_t_ Ivy_Man_t

INCLUDES ///.

CFile****************************************************************

FileName [ivy.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id:

ivy.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 46 of file ivy.h.

typedef struct Ivy_Obj_t_ Ivy_Obj_t

Definition at line 47 of file ivy.h.

typedef struct Ivy_Store_t_ Ivy_Store_t

Definition at line 165 of file ivy.h.

Enumeration Type Documentation

enum Ivy_Init_t

Enumerator
IVY_INIT_NONE
IVY_INIT_0
IVY_INIT_1
IVY_INIT_DC

Definition at line 65 of file ivy.h.

             { 
    IVY_INIT_NONE,                   // 0: not a latch
    IVY_INIT_0,                      // 1: zero
    IVY_INIT_1,                      // 2: one
    IVY_INIT_DC                      // 3: don't-care
} Ivy_Init_t;

enum Ivy_Type_t

Enumerator
IVY_NONE
IVY_PI
IVY_PO
IVY_ASSERT
IVY_LATCH
IVY_AND
IVY_EXOR
IVY_BUF
IVY_VOID

Definition at line 52 of file ivy.h.

             { 
    IVY_NONE,                        // 0: non-existent object
    IVY_PI,                          // 1: primary input (and constant 1 node)
    IVY_PO,                          // 2: primary output
    IVY_ASSERT,                      // 3: assertion
    IVY_LATCH,                       // 4: sequential element
    IVY_AND,                         // 5: AND node
    IVY_EXOR,                        // 6: EXOR node
    IVY_BUF,                         // 7: buffer (temporary)
    IVY_VOID                         // 8: unused object
} Ivy_Type_t;

Function Documentation

Ivy_Obj_t* Ivy_And	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	p0,
		Ivy_Obj_t *	p1
	)

Function*************************************************************

Synopsis [Performs canonicization step.]

Description [The argument nodes can be complemented.]

SideEffects []

SeeAlso []

Definition at line 84 of file ivyOper.c.

{
//    Ivy_Obj_t * pFan0, * pFan1;
    // check trivial cases
    if ( p0 == p1 )
        return p0;
    if ( p0 == Ivy_Not(p1) )
        return Ivy_Not(p->pConst1);
    if ( Ivy_Regular(p0) == p->pConst1 )
        return p0 == p->pConst1 ? p1 : Ivy_Not(p->pConst1);
    if ( Ivy_Regular(p1) == p->pConst1 )
        return p1 == p->pConst1 ? p0 : Ivy_Not(p->pConst1);
    // check if it can be an EXOR gate
//    if ( Ivy_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
//        return Ivy_CanonExor( pFan0, pFan1 );
    return Ivy_CanonAnd( p, p0, p1 );
}

static int Ivy_BitWordNum ( int  nBits )

inlinestatic

Definition at line 187 of file ivy.h.

{ return (nBits>>5) + ((nBits&31) > 0);           }

Ivy_Obj_t* Ivy_CanonAnd	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj0,
		Ivy_Obj_t *	pObj1
	)

Function*************************************************************

Synopsis [Creates the canonical form of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 90 of file ivyCanon.c.

{
    Ivy_Obj_t * pGhost, * pResult;
    pGhost = Ivy_ObjCreateGhost( p, pObj0, pObj1, IVY_AND, IVY_INIT_NONE );
    pResult = Ivy_CanonPair_rec( p, pGhost );
    return pResult;
}

Ivy_Obj_t* Ivy_CanonExor	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj0,
		Ivy_Obj_t *	pObj1
	)

Function*************************************************************

Synopsis [Creates the canonical form of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 109 of file ivyCanon.c.

{
    Ivy_Obj_t * pGhost, * pResult;
    int fCompl = Ivy_IsComplement(pObj0) ^ Ivy_IsComplement(pObj1);
    pObj0 = Ivy_Regular(pObj0);
    pObj1 = Ivy_Regular(pObj1);
    pGhost = Ivy_ObjCreateGhost( p, pObj0, pObj1, IVY_EXOR, IVY_INIT_NONE );
    pResult = Ivy_CanonPair_rec( p, pGhost );
    return Ivy_NotCond( pResult, fCompl );
}

Ivy_Obj_t* Ivy_CanonLatch	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj,
		Ivy_Init_t	Init
	)

Function*************************************************************

Synopsis [Creates the canonical form of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 131 of file ivyCanon.c.

{
    Ivy_Obj_t * pGhost, * pResult;
    int fCompl = Ivy_IsComplement(pObj);
    pObj = Ivy_Regular(pObj);
    pGhost = Ivy_ObjCreateGhost( p, pObj, NULL, IVY_LATCH, Ivy_InitNotCond(Init, fCompl) );
    pResult = Ivy_TableLookup( p, pGhost );
    if ( pResult == NULL )
        pResult = Ivy_ObjCreate( p, pGhost );
    return Ivy_NotCond( pResult, fCompl );
}

int Ivy_CutTruthPrint	(	Ivy_Man_t *	p,
		Ivy_Cut_t *	pCut,
		unsigned	uTruth
	)

Function*************************************************************

Synopsis [Performs incremental rewriting of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 771 of file ivyUtil.c.

{
    Vec_Ptr_t * vArray;
    Ivy_Obj_t * pObj, * pFanout;
    int nLatches = 0;
    int nPresent = 0;
    int i, k;
    int fVerbose = 0;

    if ( fVerbose )
        printf( "Trying cut : {" );
    for ( i = 0; i < pCut->nSize; i++ )
    {
        if ( fVerbose )
            printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
        nLatches += Ivy_LeafLat(pCut->pArray[i]);
    }
    if ( fVerbose )
        printf( " }   " );
    if ( fVerbose )
        printf( "Latches = %d. ", nLatches );

    // check if there are latches on the fanout edges
    vArray = Vec_PtrAlloc( 100 );
    for ( i = 0; i < pCut->nSize; i++ )
    {
        pObj = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[i]) );
        Ivy_ObjForEachFanout( p, pObj, vArray, pFanout, k )
        {
            if ( Ivy_ObjIsLatch(pFanout) )
            {
                nPresent++;
                break;
            }
        }
    }
    Vec_PtrSize( vArray );
    if ( fVerbose )
    {
        printf( "Present = %d. ", nPresent );
        if ( nLatches > nPresent )
            printf( "Clauses = %d. ", 2*(nLatches - nPresent) );
        printf( "\n" );
    }
    return ( nLatches > nPresent ) ? 2*(nLatches - nPresent) : 0;
}

static Ivy_Edge_t Ivy_EdgeCreate ( int  Id, int  fCompl  )

inlinestatic

Definition at line 205 of file ivy.h.

{ return (Id << 1) | fCompl;             }

static Ivy_Edge_t Ivy_EdgeFromNode ( Ivy_Obj_t *  pNode )

inlinestatic

Definition at line 211 of file ivy.h.

{ return Ivy_EdgeCreate( Ivy_Regular(pNode)->Id, Ivy_IsComplement(pNode) );          }

static int Ivy_EdgeId ( Ivy_Edge_t  Edge )

inlinestatic

Definition at line 206 of file ivy.h.

{ return Edge >> 1;                      }

static int Ivy_EdgeIsComplement ( Ivy_Edge_t  Edge )

inlinestatic

Definition at line 207 of file ivy.h.

{ return Edge & 1;                       }

static Ivy_Edge_t Ivy_EdgeNot ( Ivy_Edge_t  Edge )

inlinestatic

Definition at line 209 of file ivy.h.

{ return Edge ^ 1;                       }

static Ivy_Edge_t Ivy_EdgeNotCond ( Ivy_Edge_t  Edge, int  fCond  )

inlinestatic

Definition at line 210 of file ivy.h.

{ return Edge ^ fCond;                   }

static Ivy_Edge_t Ivy_EdgeRegular ( Ivy_Edge_t  Edge )

inlinestatic

Definition at line 208 of file ivy.h.

{ return (Edge >> 1) << 1;               }

static Ivy_Obj_t* Ivy_EdgeToNode ( Ivy_Man_t *  p, Ivy_Edge_t  Edge  )

inlinestatic

Definition at line 212 of file ivy.h.

{ return Ivy_NotCond( Ivy_ManObj(p, Ivy_EdgeId(Edge)), Ivy_EdgeIsComplement(Edge) ); }

Ivy_Obj_t* Ivy_Exor	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	p0,
		Ivy_Obj_t *	p1
	)

Function*************************************************************

Synopsis [Performs canonicization step.]

Description [The argument nodes can be complemented.]

SideEffects []

SeeAlso []

Definition at line 113 of file ivyOper.c.

{
/*
    // check trivial cases
    if ( p0 == p1 )
        return Ivy_Not(p->pConst1);
    if ( p0 == Ivy_Not(p1) )
        return p->pConst1;
    if ( Ivy_Regular(p0) == p->pConst1 )
        return Ivy_NotCond( p1, p0 == p->pConst1 );
    if ( Ivy_Regular(p1) == p->pConst1 )
        return Ivy_NotCond( p0, p1 == p->pConst1 );
    // check the table
    return Ivy_CanonExor( p, p0, p1 );
*/
    return Ivy_Or( p, Ivy_And(p, p0, Ivy_Not(p1)), Ivy_And(p, Ivy_Not(p0), p1) );
}

void Ivy_FastMapPerform	(	Ivy_Man_t *	pAig,
		int	nLimit,
		int	fRecovery,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Performs fast K-LUT mapping of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file ivyFastMap.c.

{
    Ivy_SuppMan_t * pMan;
    Ivy_Obj_t * pObj;
    int i, Delay, Area;
    abctime clk, clkTotal = Abc_Clock();
    // start the memory for supports
    pMan = ABC_ALLOC( Ivy_SuppMan_t, 1 );
    memset( pMan, 0, sizeof(Ivy_SuppMan_t) );
    pMan->nLimit = nLimit;
    pMan->nObjs  = Ivy_ManObjIdMax(pAig) + 1;
    pMan->nSize  = sizeof(Ivy_Supp_t) + nLimit * sizeof(int);
    pMan->pMem   = (char *)ABC_ALLOC( char, pMan->nObjs * pMan->nSize );
    memset( pMan->pMem, 0, pMan->nObjs * pMan->nSize );
    pMan->vLuts  = Vec_VecAlloc( 100 );
    pAig->pData  = pMan;
clk = Abc_Clock();
    // set the PI mapping
    Ivy_ObjSuppStart( pAig, Ivy_ManConst1(pAig) );
    Ivy_ManForEachPi( pAig, pObj, i )
        Ivy_ObjSuppStart( pAig, pObj );
    // iterate through all nodes in the topological order
    Ivy_ManForEachNode( pAig, pObj, i )
        Ivy_FastMapNode( pAig, pObj, nLimit );
    // find the best arrival time and area
    Delay = Ivy_FastMapDelay( pAig );
    Area = Ivy_FastMapArea(pAig);
    if ( fVerbose )
        Ivy_FastMapPrint( pAig, Delay, Area, Abc_Clock() - clk, "Delay oriented mapping: " );

// 2-1-2 (doing 2-1-2-1-2 improves 0.5%)

    if ( fRecovery )
    {
clk = Abc_Clock();
    Ivy_FastMapRequired( pAig, Delay, 0 );
    // remap the nodes
    Ivy_FastMapRecover( pAig, nLimit );
    Delay = Ivy_FastMapDelay( pAig );
    Area = Ivy_FastMapArea(pAig);
    if ( fVerbose )
        Ivy_FastMapPrint( pAig, Delay, Area, Abc_Clock() - clk, "Area recovery 2       : " );

clk = Abc_Clock();
    Ivy_FastMapRequired( pAig, Delay, 0 );
    // iterate through all nodes in the topological order
    Ivy_ManForEachNode( pAig, pObj, i )
        Ivy_FastMapNodeArea( pAig, pObj, nLimit );
    Delay = Ivy_FastMapDelay( pAig );
    Area = Ivy_FastMapArea(pAig);
    if ( fVerbose )
        Ivy_FastMapPrint( pAig, Delay, Area, Abc_Clock() - clk, "Area recovery 1       : " );

clk = Abc_Clock();
    Ivy_FastMapRequired( pAig, Delay, 0 );
    // remap the nodes
    Ivy_FastMapRecover( pAig, nLimit );
    Delay = Ivy_FastMapDelay( pAig );
    Area = Ivy_FastMapArea(pAig);
    if ( fVerbose )
        Ivy_FastMapPrint( pAig, Delay, Area, Abc_Clock() - clk, "Area recovery 2       : " );
    }


    s_MappingTime = Abc_Clock() - clkTotal;
    s_MappingMem = pMan->nObjs * pMan->nSize;
/*
    {
        Vec_Ptr_t * vNodes;
        vNodes = Vec_PtrAlloc( 100 );
        Vec_VecForEachEntry( Ivy_Obj_t *, pMan->vLuts, pObj, i, k )
            Vec_PtrPush( vNodes, pObj );
        Ivy_ManShow( pAig, 0, vNodes );
        Vec_PtrFree( vNodes );
    }
*/
}

void Ivy_FastMapReadSupp	(	Ivy_Man_t *	pAig,
		Ivy_Obj_t *	pObj,
		Vec_Int_t *	vLeaves
	)

Function*************************************************************

Synopsis [Creates integer vector with the support of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 793 of file ivyFastMap.c.

{
    Ivy_Supp_t * pSupp;
    pSupp = Ivy_ObjSupp( pAig, pObj );
    vLeaves->nCap   = 8;
    vLeaves->nSize  = pSupp->nSize;
    vLeaves->pArray = pSupp->pArray;
}

void Ivy_FastMapReverseLevel

(

Ivy_Man_t *

pAig

)

void Ivy_FastMapStop

(

Ivy_Man_t *

pAig

)

Function*************************************************************

Synopsis [Cleans memory used for decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 194 of file ivyFastMap.c.

{
    Ivy_SuppMan_t * p = (Ivy_SuppMan_t *)pAig->pData;
    Vec_VecFree( p->vLuts );
    ABC_FREE( p->pMem );
    ABC_FREE( p );
    pAig->pData = NULL;
}

Ivy_Man_t* Ivy_FraigMiter	(	Ivy_Man_t *	pManAig,
		Ivy_FraigParams_t *	pParams
	)

Function*************************************************************

Synopsis [Applies brute-force SAT to the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 480 of file ivyFraig.c.

{
    Ivy_FraigMan_t * p;
    Ivy_Man_t * pManAigNew;
    Ivy_Obj_t * pObj;
    int i;
    abctime clk;
clk = Abc_Clock();
    assert( Ivy_ManLatchNum(pManAig) == 0 );
    p = Ivy_FraigStartSimple( pManAig, pParams );
    // set global limits
    p->nBTLimitGlobal  = s_nBTLimitGlobal;
    p->nInsLimitGlobal = s_nInsLimitGlobal; 
    // duplicate internal nodes
    Ivy_ManForEachNode( p->pManAig, pObj, i )
        pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
    // try to prove each output of the miter
    Ivy_FraigMiterProve( p );
    // add the POs
    Ivy_ManForEachPo( p->pManAig, pObj, i )
        Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
    // clean the new manager
    Ivy_ManForEachObj( p->pManFraig, pObj, i )
    {
        if ( Ivy_ObjFaninVec(pObj) )
            Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
        pObj->pNextFan0 = pObj->pNextFan1 = NULL;
    }
    // remove dangling nodes 
    Ivy_ManCleanup( p->pManFraig );
    pManAigNew = p->pManFraig;
p->timeTotal = Abc_Clock() - clk;

//printf( "Final nodes = %6d. ", Ivy_ManNodeNum(pManAigNew) );
//ABC_PRT( "Time", p->timeTotal );
    Ivy_FraigStop( p );
    return pManAigNew;
}

void Ivy_FraigParamsDefault

(

Ivy_FraigParams_t *

pParams

)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Sets the default solving parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 225 of file ivyFraig.c.

{
    memset( pParams, 0, sizeof(Ivy_FraigParams_t) );
    pParams->nSimWords        =      32;  // the number of words in the simulation info
    pParams->dSimSatur        =   0.005;  // the ratio of refined classes when saturation is reached
    pParams->fPatScores       =       0;  // enables simulation pattern scoring
    pParams->MaxScore         =      25;  // max score after which resimulation is used
    pParams->fDoSparse        =       1;  // skips sparse functions
//    pParams->dActConeRatio    =    0.05;  // the ratio of cone to be bumped
//    pParams->dActConeBumpMax  =     5.0;  // the largest bump of activity
    pParams->dActConeRatio    =     0.3;  // the ratio of cone to be bumped
    pParams->dActConeBumpMax  =    10.0;  // the largest bump of activity

    pParams->nBTLimitNode     =     100;  // conflict limit at a node
    pParams->nBTLimitMiter    =  500000;  // conflict limit at an output
//    pParams->nBTLimitGlobal   =       0;  // conflict limit global
//    pParams->nInsLimitGlobal  =       0;  // inspection limit global
}

Ivy_Man_t* Ivy_FraigPerform	(	Ivy_Man_t *	pManAig,
		Ivy_FraigParams_t *	pParams
	)

Function*************************************************************

Synopsis [Performs fraiging of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 451 of file ivyFraig.c.

{
    Ivy_FraigMan_t * p;
    Ivy_Man_t * pManAigNew;
    abctime clk;
    if ( Ivy_ManNodeNum(pManAig) == 0 )
        return Ivy_ManDup(pManAig);
clk = Abc_Clock();
    assert( Ivy_ManLatchNum(pManAig) == 0 );
    p = Ivy_FraigStart( pManAig, pParams );
    Ivy_FraigSimulate( p );
    Ivy_FraigSweep( p );
    pManAigNew = p->pManFraig;
p->timeTotal = Abc_Clock() - clk;
    Ivy_FraigStop( p );
    return pManAigNew;
}

int Ivy_FraigProve	(	Ivy_Man_t **	ppManAig,
		void *	pPars
	)

Function*************************************************************

Synopsis [Performs combinational equivalence checking for the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 255 of file ivyFraig.c.

{
    Prove_Params_t * pParams = (Prove_Params_t *)pPars;
    Ivy_FraigParams_t Params, * pIvyParams = &Params; 
    Ivy_Man_t * pManAig, * pManTemp;
    int RetValue, nIter;
    abctime clk;//, Counter;
    ABC_INT64_T nSatConfs = 0, nSatInspects = 0;

    // start the network and parameters
    pManAig = *ppManAig;
    Ivy_FraigParamsDefault( pIvyParams );
    pIvyParams->fVerbose = pParams->fVerbose;
    pIvyParams->fProve = 1;

    if ( pParams->fVerbose )
    {
        printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
            pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" );
        printf( "Miter = %d (%3.1f).  Rwr = %d (%3.1f).  Fraig = %d (%3.1f).  Last = %d.\n", 
            pParams->nMiteringLimitStart,  pParams->nMiteringLimitMulti, 
            pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti,
            pParams->nFraigingLimitStart,  pParams->nFraigingLimitMulti, pParams->nMiteringLimitLast );
    }

    // if SAT only, solve without iteration
    if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
    {
        clk = Abc_Clock();
        pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
        pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams );  Ivy_ManStop( pManTemp );
        RetValue = Ivy_FraigMiterStatus( pManAig );
        Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
        *ppManAig = pManAig;
        return RetValue;
    }

    if ( Ivy_ManNodeNum(pManAig) < 500 )
    {
        // run the first mitering
        clk = Abc_Clock();
        pIvyParams->nBTLimitMiter = pParams->nMiteringLimitStart / Ivy_ManPoNum(pManAig);
        pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams );  Ivy_ManStop( pManTemp );
        RetValue = Ivy_FraigMiterStatus( pManAig );
        Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
        if ( RetValue >= 0 )
        {
            *ppManAig = pManAig;
            return RetValue;
        }
    }

    // check the current resource limits
    RetValue = -1;
    for ( nIter = 0; nIter < pParams->nItersMax; nIter++ )
    {
        if ( pParams->fVerbose )
        {
            printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1, 
                 (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 
                 (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) );
            fflush( stdout );
        }

        // try rewriting
        if ( pParams->fUseRewriting )
        { // bug in Ivy_NodeFindCutsAll() when leaves are identical!
/*
            clk = Abc_Clock();
            Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
            pManAig = Ivy_ManRwsat( pManAig, 0 );  
            RetValue = Ivy_FraigMiterStatus( pManAig );
            Ivy_FraigMiterPrint( pManAig, "Rewriting  ", clk, pParams->fVerbose );
*/
        }
        if ( RetValue >= 0 )
            break;

        // catch the situation when ref pattern detects the bug
        RetValue = Ivy_FraigMiterStatus( pManAig );
        if ( RetValue >= 0 )
            break;

        // try fraiging followed by mitering
        if ( pParams->fUseFraiging )
        {
            clk = Abc_Clock();
            pIvyParams->nBTLimitNode  = (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter));
            pIvyParams->nBTLimitMiter = 1 + (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig);
            pManAig = Ivy_FraigPerform_int( pManTemp = pManAig, pIvyParams, pParams->nTotalBacktrackLimit, pParams->nTotalInspectLimit, &nSatConfs, &nSatInspects );  Ivy_ManStop( pManTemp );
            RetValue = Ivy_FraigMiterStatus( pManAig );
            Ivy_FraigMiterPrint( pManAig, "Fraiging   ", clk, pParams->fVerbose );
        }
        if ( RetValue >= 0 )
            break;

        // add to the number of backtracks and inspects
        pParams->nTotalBacktracksMade += nSatConfs;
        pParams->nTotalInspectsMade   += nSatInspects;
        // check if global resource limit is reached
        if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
             (pParams->nTotalInspectLimit   && pParams->nTotalInspectsMade   >= pParams->nTotalInspectLimit) )
        {
            printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
            *ppManAig = pManAig;
            return -1;
        }
    }    
/*
    if ( RetValue < 0 )
    {
        if ( pParams->fVerbose )
        {
            printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
            fflush( stdout );
        }
        clk = Abc_Clock();
        pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
        if ( pParams->nTotalBacktrackLimit )
            s_nBTLimitGlobal  = pParams->nTotalBacktrackLimit - pParams->nTotalBacktracksMade;
        if ( pParams->nTotalInspectLimit )
            s_nInsLimitGlobal = pParams->nTotalInspectLimit -   pParams->nTotalInspectsMade;        
        pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams );  Ivy_ManStop( pManTemp );
        s_nBTLimitGlobal  = 0;
        s_nInsLimitGlobal = 0;        
        RetValue = Ivy_FraigMiterStatus( pManAig );
        Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
        // make sure that the sover never returns "undecided" when infinite resource limits are set
        if( RetValue == -1 && pParams->nTotalInspectLimit == 0 &&
            pParams->nTotalBacktrackLimit == 0 )
        {
            extern void Prove_ParamsPrint( Prove_Params_t * pParams );
            Prove_ParamsPrint( pParams );
            printf("ERROR: ABC has returned \"undecided\" in spite of no limits...\n");
            exit(1);
        }
    }
*/
    // assign the model if it was proved by rewriting (const 1 miter)
    if ( RetValue == 0 && pManAig->pData == NULL )
    {
        pManAig->pData = ABC_ALLOC( int, Ivy_ManPiNum(pManAig) );
        memset( pManAig->pData, 0, sizeof(int) * Ivy_ManPiNum(pManAig) );
    }
    *ppManAig = pManAig;
    return RetValue;
}

static int Ivy_InfoHasBit ( unsigned *  p, int  i  )

inlinestatic

Definition at line 189 of file ivy.h.

{ return (p[(i)>>5] & (1<<((i) & 31))) > 0;       }

static void Ivy_InfoSetBit ( unsigned *  p, int  i  )

inlinestatic

Definition at line 190 of file ivy.h.

{ p[(i)>>5] |= (1<<((i) & 31));                   }

static void Ivy_InfoXorBit ( unsigned *  p, int  i  )

inlinestatic

Definition at line 191 of file ivy.h.

{ p[(i)>>5] ^= (1<<((i) & 31));                   }

static Ivy_Init_t Ivy_InitAnd ( Ivy_Init_t  InitA, Ivy_Init_t  InitB  )

static

Definition at line 340 of file ivy.h.

{
    assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE );
    if ( InitA == IVY_INIT_0 || InitB == IVY_INIT_0 )
        return IVY_INIT_0;
    if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC )
        return IVY_INIT_DC;
    return IVY_INIT_1;
}

static Ivy_Init_t Ivy_InitExor ( Ivy_Init_t  InitA, Ivy_Init_t  InitB  )

static

Definition at line 351 of file ivy.h.

{
    assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE );
    if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC )
        return IVY_INIT_DC;
    if ( InitA == IVY_INIT_0 && InitB == IVY_INIT_1 )
        return IVY_INIT_1;
    if ( InitA == IVY_INIT_1 && InitB == IVY_INIT_0 )
        return IVY_INIT_1;
    return IVY_INIT_0;
}

static Ivy_Init_t Ivy_InitNotCond ( Ivy_Init_t  Init, int  fCompl  )

static

Definition at line 327 of file ivy.h.

{
    assert( Init != IVY_INIT_NONE );
    if ( fCompl == 0 )
        return Init;
    if ( Init == IVY_INIT_0 )
        return IVY_INIT_1;
    if ( Init == IVY_INIT_1 )
        return IVY_INIT_0;
    return IVY_INIT_DC;
}

static int Ivy_IsComplement ( Ivy_Obj_t *  p )

inlinestatic

Definition at line 196 of file ivy.h.

{ return (int)((ABC_PTRUINT_T)(p) & 01);          }

Ivy_Obj_t* Ivy_Latch	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj,
		Ivy_Init_t	Init
	)

Function*************************************************************

Synopsis [Performs canonicization step.]

Description []

SideEffects []

SeeAlso []

Definition at line 287 of file ivyOper.c.

{
    return Ivy_CanonLatch( p, pObj, Init );
}

static int Ivy_LeafCreate ( int  Id, int  Lat  )

inlinestatic

Definition at line 214 of file ivy.h.

{ return (Id << IVY_LEAF_BITS) | Lat;         }

static int Ivy_LeafId ( int  Leaf )

inlinestatic

Definition at line 215 of file ivy.h.

{ return Leaf >> IVY_LEAF_BITS;               }

static int Ivy_LeafLat ( int  Leaf )

inlinestatic

Definition at line 216 of file ivy.h.

{ return Leaf & IVY_LEAF_MASK;                }

Ivy_Obj_t* Ivy_Maj	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pA,
		Ivy_Obj_t *	pB,
		Ivy_Obj_t *	pC
	)

Function*************************************************************

Synopsis [Implements ITE operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 209 of file ivyOper.c.

{
    return Ivy_Or( p, Ivy_Or(p, Ivy_And(p, pA, pB), Ivy_And(p, pA, pC)), Ivy_And(p, pB, pC) );
}

void Ivy_ManAddMemory

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Allocates additional memory for the nodes.]

Description [Allocates IVY_PAGE_SIZE nodes. Aligns memory by 32 bytes. Records the pointer to the AIG manager in the -1 entry.]

SideEffects []

SeeAlso []

Definition at line 89 of file ivyMem.c.

{
    char * pMemory;
    int i, nBytes;
    int EntrySizeMax = 128;
    assert( sizeof(Ivy_Obj_t) <= EntrySizeMax );
    assert( p->pListFree == NULL );
//    assert( (Ivy_ManObjNum(p) & IVY_PAGE_MASK) == 0 );
    // allocate new memory page
    nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + EntrySizeMax;
    pMemory = ABC_ALLOC( char, nBytes );
    Vec_PtrPush( p->vChunks, pMemory );
    // align memory at the 32-byte boundary
    pMemory = pMemory + EntrySizeMax - (((int)(ABC_PTRUINT_T)pMemory) & (EntrySizeMax-1));
    // remember the manager in the first entry
    Vec_PtrPush( p->vPages, pMemory );
    // break the memory down into nodes
    p->pListFree = (Ivy_Obj_t *)pMemory;
    for ( i = 1; i <= IVY_PAGE_MASK; i++ )
    {
        *((char **)pMemory) = pMemory + sizeof(Ivy_Obj_t);
        pMemory += sizeof(Ivy_Obj_t);
    }
    *((char **)pMemory) = NULL;
}

static int Ivy_ManAndNum ( Ivy_Man_t *  p )

inlinestatic

Definition at line 222 of file ivy.h.

{ return p->nObjs[IVY_AND];                   }

static int Ivy_ManAssertNum ( Ivy_Man_t *  p )

inlinestatic

Definition at line 220 of file ivy.h.

{ return p->nObjs[IVY_ASSERT];                }

Ivy_Man_t* Ivy_ManBalance	(	Ivy_Man_t *	p,
		int	fUpdateLevel
	)

FUNCTION DECLARATIONS ///.

FUNCTION DECLARATIONS ///.

Function*************************************************************

Synopsis [Performs algebraic balancing of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file ivyBalance.c.

{
    Ivy_Man_t * pNew;
    Ivy_Obj_t * pObj, * pDriver;
    Vec_Vec_t * vStore;
    int i, NewNodeId;
    // clean the old manager
    Ivy_ManCleanTravId( p );
    // create the new manager 
    pNew = Ivy_ManStart();
    // map the nodes
    Ivy_ManConst1(p)->TravId = Ivy_EdgeFromNode( Ivy_ManConst1(pNew) );
    Ivy_ManForEachPi( p, pObj, i )
        pObj->TravId = Ivy_EdgeFromNode( Ivy_ObjCreatePi(pNew) );
    // if HAIG is defined, trasfer the pointers to the PIs/latches
//    if ( p->pHaig )
//        Ivy_ManHaigTrasfer( p, pNew );
    // balance the AIG
    vStore = Vec_VecAlloc( 50 );
    Ivy_ManForEachPo( p, pObj, i )
    {
        pDriver   = Ivy_ObjReal( Ivy_ObjChild0(pObj) );
        NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(pDriver), vStore, 0, fUpdateLevel );
        NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(pDriver) );
        Ivy_ObjCreatePo( pNew, Ivy_EdgeToNode(pNew, NewNodeId) );
    }
    Vec_VecFree( vStore );
    if ( (i = Ivy_ManCleanup( pNew )) )
    {
//        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
    }
    // check the resulting AIG
    if ( !Ivy_ManCheck(pNew) )
        printf( "Ivy_ManBalance(): The check has failed.\n" );
    return pNew;
}

static int Ivy_ManBufNum ( Ivy_Man_t *  p )

inlinestatic

Definition at line 224 of file ivy.h.

{ return p->nObjs[IVY_BUF];                   }

int Ivy_ManCheck

(

Ivy_Man_t *

p

)

DECLARATIONS ///.

CFile****************************************************************

FileName [ivyCheck.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [AIG checking procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id:

ivyCheck.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Checks the consistency of the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file ivyCheck.c.

{
    Ivy_Obj_t * pObj, * pObj2;
    int i;
    Ivy_ManForEachObj( p, pObj, i )
    {
        // skip deleted nodes
        if ( Ivy_ObjId(pObj) != i )
        {
            printf( "Ivy_ManCheck: Node with ID %d is listed as number %d in the array of objects.\n", pObj->Id, i );
            return 0;
        }
        // consider the constant node and PIs
        if ( i == 0 || Ivy_ObjIsPi(pObj) )
        {
            if ( Ivy_ObjFaninId0(pObj) || Ivy_ObjFaninId1(pObj) || Ivy_ObjLevel(pObj) )
            {
                printf( "Ivy_ManCheck: The AIG has non-standard constant or PI node with ID \"%d\".\n", pObj->Id );
                return 0;
            }
            continue;
        }
        if ( Ivy_ObjIsPo(pObj) )
        {
            if ( Ivy_ObjFaninId1(pObj) )
            {
                printf( "Ivy_ManCheck: The AIG has non-standard PO node with ID \"%d\".\n", pObj->Id );
                return 0;
            }
            continue;
        }
        if ( Ivy_ObjIsBuf(pObj) )
        {
            if ( Ivy_ObjFanin1(pObj) )
            {
                printf( "Ivy_ManCheck: The buffer with ID \"%d\" contains second fanin.\n", pObj->Id );
                return 0;
            }
            continue;
        }
        if ( Ivy_ObjIsLatch(pObj) )
        {
            if ( Ivy_ObjFanin1(pObj) )
            {
                printf( "Ivy_ManCheck: The latch with ID \"%d\" contains second fanin.\n", pObj->Id );
                return 0;
            }
            if ( Ivy_ObjInit(pObj) == IVY_INIT_NONE )
            {
                printf( "Ivy_ManCheck: The latch with ID \"%d\" does not have initial state.\n", pObj->Id );
                return 0;
            }
            pObj2 = Ivy_TableLookup( p, pObj );
            if ( pObj2 != pObj )
                printf( "Ivy_ManCheck: Latch with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
                continue;
        }
        // consider the AND node
        if ( !Ivy_ObjFanin0(pObj) || !Ivy_ObjFanin1(pObj) )
        {
            printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a NULL fanin.\n", pObj->Id );
            return 0;
        }
        if ( Ivy_ObjFaninId0(pObj) >= Ivy_ObjFaninId1(pObj) )
        {
            printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id );
            return 0;
        }
        if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) )
            printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) );
        pObj2 = Ivy_TableLookup( p, pObj );
        if ( pObj2 != pObj )
            printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
        if ( Ivy_ObjRefs(pObj) == 0 )
            printf( "Ivy_ManCheck: Node with ID \"%d\" has no fanouts.\n", pObj->Id );
        // check fanouts
        if ( p->fFanout && Ivy_ObjRefs(pObj) != Ivy_ObjFanoutNum(p, pObj) )
            printf( "Ivy_ManCheck: Node with ID \"%d\" has mismatch between the number of fanouts and refs.\n", pObj->Id );
    }
    // count the number of nodes in the table
    if ( Ivy_TableCountEntries(p) != Ivy_ManAndNum(p) + Ivy_ManExorNum(p) + Ivy_ManLatchNum(p) )
    {
        printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
        return 0;
    }
//    if ( !Ivy_ManCheckFanouts(p) )
//        return 0;
    if ( !Ivy_ManIsAcyclic(p) )
        return 0;
    return 1; 
}

int Ivy_ManCheckChoices

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Checks that each choice node has exactly one node with fanouts.]

Description []

SideEffects []

SeeAlso []

Definition at line 255 of file ivyCheck.c.

{
    Ivy_Obj_t * pObj, * pTemp;
    int i;
    Ivy_ManForEachObj( p->pHaig, pObj, i )
    {
        if ( Ivy_ObjRefs(pObj) == 0 )
            continue;
        // count the number of nodes in the loop
        assert( !Ivy_IsComplement(pObj->pEquiv) );
        for ( pTemp = pObj->pEquiv; pTemp && pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
            if ( Ivy_ObjRefs(pTemp) > 1 )
                printf( "Node %d has member %d in its equiv class with %d fanouts.\n", pObj->Id, pTemp->Id, Ivy_ObjRefs(pTemp) );
    }
    return 1;
}

int Ivy_ManCheckFanoutNums

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Verifies the fanouts.]

Description []

SideEffects []

SeeAlso []

Definition at line 148 of file ivyCheck.c.

{
    Ivy_Obj_t * pObj;
    int i, Counter = 0;
    Ivy_ManForEachObj( p, pObj, i )
        if ( Ivy_ObjIsNode(pObj) )
            Counter += (Ivy_ObjRefs(pObj) == 0);
    if ( Counter )
        printf( "Sequential AIG has %d dangling nodes.\n", Counter );
    return Counter;
}

int Ivy_ManCheckFanouts

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Verifies the fanouts.]

Description []

SideEffects []

SeeAlso []

Definition at line 171 of file ivyCheck.c.

{
    Vec_Ptr_t * vFanouts;
    Ivy_Obj_t * pObj, * pFanout, * pFanin;
    int i, k, RetValue = 1;
    if ( !p->fFanout )
        return 1;
    vFanouts = Vec_PtrAlloc( 100 );
    // make sure every fanin is a fanout
    Ivy_ManForEachObj( p, pObj, i )
    {
        pFanin = Ivy_ObjFanin0(pObj);
        if ( pFanin == NULL )
            continue;
        Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k )
            if ( pFanout == pObj )
                break;
        if ( k == Vec_PtrSize(vFanouts) )
        {
            printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id );
            RetValue = 0;
        }

        pFanin = Ivy_ObjFanin1(pObj);
        if ( pFanin == NULL )
            continue;
        Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k )
            if ( pFanout == pObj )
                break;
        if ( k == Vec_PtrSize(vFanouts) )
        {
            printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id );
            RetValue = 0;
        }
        // check that the previous fanout has the same fanin
        if ( pObj->pPrevFan0 )
        {
            if ( Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) && 
                 Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) && 
                 Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) && 
                 Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) )
            {
                printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan0->Id );
                RetValue = 0;
            }
        }
        // check that the previous fanout has the same fanin
        if ( pObj->pPrevFan1 )
        {
            if ( Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) && 
                 Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) && 
                 Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) && 
                 Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) )
            {
                printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan1->Id );
                RetValue = 0;
            }
        }
    }
    // make sure every fanout is a fanin
    Ivy_ManForEachObj( p, pObj, i )
    {
        Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, k )
            if ( Ivy_ObjFanin0(pFanout) != pObj && Ivy_ObjFanin1(pFanout) != pObj )
            {
                printf( "Node %d is a fanout of node %d but the fanin is not there.\n", pFanout->Id, pObj->Id );
                RetValue = 0;
            }
    }
    Vec_PtrFree( vFanouts );
    return RetValue;
}

void Ivy_ManCleanTravId

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Sets the DFS ordering of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file ivyUtil.c.

{
    Ivy_Obj_t * pObj;
    int i;
    p->nTravIds = 1;
    Ivy_ManForEachObj( p, pObj, i )
        pObj->TravId = 0;
}

int Ivy_ManCleanup

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Removes nodes without fanout.]

Description [Returns the number of dangling nodes removed.]

SideEffects []

SeeAlso []

Definition at line 265 of file ivyMan.c.

{
    Ivy_Obj_t * pNode;
    int i, nNodesOld;
    nNodesOld = Ivy_ManNodeNum(p);
    Ivy_ManForEachObj( p, pNode, i )
        if ( Ivy_ObjIsNode(pNode) || Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) )
            if ( Ivy_ObjRefs(pNode) == 0 )
                Ivy_ObjDelete_rec( p, pNode, 1 );
//printf( "Cleanup removed %d nodes.\n", nNodesOld - Ivy_ManNodeNum(p) );
    return nNodesOld - Ivy_ManNodeNum(p);
}

void Ivy_ManCollectCone	(	Ivy_Obj_t *	pObj,
		Vec_Ptr_t *	vFront,
		Vec_Ptr_t *	vCone
	)

Function*************************************************************

Synopsis [Collects nodes in the cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 195 of file ivyDfs.c.

{
    Ivy_Obj_t * pTemp;
    int i;
    assert( !Ivy_IsComplement(pObj) );
    assert( Ivy_ObjIsNode(pObj) );
    // mark the nodes
    Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pTemp, i )
        Ivy_Regular(pTemp)->fMarkA = 1;
    assert( pObj->fMarkA == 0 );
    // collect the cone
    Vec_PtrClear( vCone );
    Ivy_ManCollectCone_rec( pObj, vCone );
    // unmark the nodes
    Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pTemp, i )
        Ivy_Regular(pTemp)->fMarkA = 0;
}

void Ivy_ManCollectCut	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pRoot,
		Vec_Int_t *	vLeaves,
		Vec_Int_t *	vNodes
	)

Function*************************************************************

Synopsis [Computes truth table of the cut.]

Description [Does not modify the array of leaves. Uses array vTruth to store temporary truth tables. The returned pointer should be used immediately.]

SideEffects []

SeeAlso []

Definition at line 106 of file ivyUtil.c.

{
    int i, Leaf;
    // collect and mark the leaves
    Vec_IntClear( vNodes );
    Vec_IntForEachEntry( vLeaves, Leaf, i )
    {
        Vec_IntPush( vNodes, Leaf );
        Ivy_ManObj(p, Leaf)->fMarkA = 1;
    }
    // collect and mark the nodes
    Ivy_ManCollectCut_rec( p, pRoot, vNodes );
    // clean the nodes
    Vec_IntForEachEntry( vNodes, Leaf, i )
        Ivy_ManObj(p, Leaf)->fMarkA = 0;
}

static Ivy_Obj_t* Ivy_ManConst0 ( Ivy_Man_t *  p )

inlinestatic

Definition at line 198 of file ivy.h.

{ return Ivy_Not(p->pConst1);                     }

static Ivy_Obj_t* Ivy_ManConst1 ( Ivy_Man_t *  p )

inlinestatic

Definition at line 199 of file ivy.h.

{ return p->pConst1;                              }

unsigned* Ivy_ManCutTruth	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pRoot,
		Vec_Int_t *	vLeaves,
		Vec_Int_t *	vNodes,
		Vec_Int_t *	vTruth
	)

Function*************************************************************

Synopsis [Computes truth table of the cut.]

Description [Does not modify the array of leaves. Uses array vTruth to store temporary truth tables. The returned pointer should be used immediately.]

SideEffects []

SeeAlso []

Definition at line 186 of file ivyUtil.c.

{
    static unsigned uTruths[8][8] = { // elementary truth tables
        { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
        { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
        { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
        { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
        { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
    };
    int i, Leaf;
    // collect the cut
    Ivy_ManCollectCut( p, pRoot, vLeaves, vNodes );
    // set the node numbers
    Vec_IntForEachEntry( vNodes, Leaf, i )
        Ivy_ManObj(p, Leaf)->TravId = i;
    // alloc enough memory
    Vec_IntClear( vTruth );
    Vec_IntGrow( vTruth, 8 * Vec_IntSize(vNodes) );
    // set the elementary truth tables
    Vec_IntForEachEntry( vLeaves, Leaf, i )
        memcpy( Ivy_ObjGetTruthStore(i, vTruth), uTruths[i], 8 * sizeof(unsigned) );
    // compute truths for other nodes
    Vec_IntForEachEntryStart( vNodes, Leaf, i, Vec_IntSize(vLeaves) )
        Ivy_ManCutTruthOne( p, Ivy_ManObj(p, Leaf), vTruth, 8 );
    return Ivy_ObjGetTruthStore( pRoot->TravId, vTruth );
}

Vec_Int_t* Ivy_ManDfs

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Collects AND/EXOR nodes in the DFS order from CIs to COs.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file ivyDfs.c.

{
    Vec_Int_t * vNodes;
    Ivy_Obj_t * pObj;
    int i;
    assert( Ivy_ManLatchNum(p) == 0 );
    // make sure the nodes are not marked
    Ivy_ManForEachObj( p, pObj, i )
        assert( !pObj->fMarkA && !pObj->fMarkB );
    // collect the nodes
    vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
    Ivy_ManForEachPo( p, pObj, i )
        Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
    // unmark the collected nodes
//    Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
//        Ivy_ObjClearMarkA(pObj);
    Ivy_ManForEachObj( p, pObj, i )
        Ivy_ObjClearMarkA(pObj);
    // make sure network does not have dangling nodes
    assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
    return vNodes;
}

Vec_Int_t* Ivy_ManDfsSeq	(	Ivy_Man_t *	p,
		Vec_Int_t **	pvLatches
	)

Function*************************************************************

Synopsis [Collects AND/EXOR nodes in the DFS order from CIs to COs.]

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file ivyDfs.c.

{
    Vec_Int_t * vNodes, * vLatches;
    Ivy_Obj_t * pObj;
    int i;
//    assert( Ivy_ManLatchNum(p) > 0 );
    // make sure the nodes are not marked
    Ivy_ManForEachObj( p, pObj, i )
        assert( !pObj->fMarkA && !pObj->fMarkB );
    // collect the latches
    vLatches = Vec_IntAlloc( Ivy_ManLatchNum(p) );
    Ivy_ManForEachLatch( p, pObj, i )
        Vec_IntPush( vLatches, pObj->Id );
    // collect the nodes
    vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
    Ivy_ManForEachPo( p, pObj, i )
        Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
    Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
        Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes );
    // unmark the collected nodes
//    Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
//        Ivy_ObjClearMarkA(pObj);
    Ivy_ManForEachObj( p, pObj, i )
        Ivy_ObjClearMarkA(pObj);
    // make sure network does not have dangling nodes
//    assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );

// temporary!!!

    if ( pvLatches == NULL )
        Vec_IntFree( vLatches );
    else
        *pvLatches = vLatches;
    return vNodes;
}

Ivy_Obj_t* Ivy_ManDsdConstruct	(	Ivy_Man_t *	p,
		Vec_Int_t *	vFront,
		Vec_Int_t *	vTree
	)

Function*************************************************************

Synopsis [Implement DSD in the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 655 of file ivyDsd.c.

{
    int Entry, i;
    // implement latches on the frontier (TEMPORARY!!!)
    Vec_IntForEachEntry( vFront, Entry, i )
        Vec_IntWriteEntry( vFront, i, Ivy_LeafId(Entry) );
    // recursively construct the tree
    return Ivy_ManDsdConstruct_rec( p, vFront, Vec_IntSize(vTree)-1, vTree );
}

Ivy_Man_t* Ivy_ManDup

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Duplicates the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 110 of file ivyMan.c.

{
    Vec_Int_t * vNodes, * vLatches;
    Ivy_Man_t * pNew;
    Ivy_Obj_t * pObj;
    int i;
    // collect latches and nodes in the DFS order
    vNodes = Ivy_ManDfsSeq( p, &vLatches );
    // create the new manager
    pNew = Ivy_ManStart();
    // create the PIs
    Ivy_ManConst1(p)->pEquiv = Ivy_ManConst1(pNew);
    Ivy_ManForEachPi( p, pObj, i )
        pObj->pEquiv = Ivy_ObjCreatePi(pNew);
    // create the fake PIs for latches
    Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
        pObj->pEquiv = Ivy_ObjCreatePi(pNew);
    // duplicate internal nodes
    Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
        if ( Ivy_ObjIsBuf(pObj) )
            pObj->pEquiv = Ivy_ObjChild0Equiv(pObj);
        else
            pObj->pEquiv = Ivy_And( pNew, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
    // add the POs
    Ivy_ManForEachPo( p, pObj, i )
        Ivy_ObjCreatePo( pNew, Ivy_ObjChild0Equiv(pObj) );
    // transform additional PI nodes into latches and connect them
    Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
    {
        assert( !Ivy_ObjFaninC0(pObj) );
        pObj->pEquiv->Type = IVY_LATCH;
        pObj->pEquiv->Init = pObj->Init;
        Ivy_ObjConnect( pNew, pObj->pEquiv, Ivy_ObjChild0Equiv(pObj), NULL );
    }
    // shrink the arrays
    Vec_PtrShrink( pNew->vPis, Ivy_ManPiNum(p) );
    // update the counters of different objects
    pNew->nObjs[IVY_PI] -= Ivy_ManLatchNum(p);
    pNew->nObjs[IVY_LATCH] += Ivy_ManLatchNum(p);
    // free arrays
    Vec_IntFree( vNodes );
    Vec_IntFree( vLatches );
    // make sure structural hashing did not change anything
    assert( Ivy_ManNodeNum(p)  == Ivy_ManNodeNum(pNew) );
    assert( Ivy_ManLatchNum(p) == Ivy_ManLatchNum(pNew) );
    // check the resulting network
    if ( !Ivy_ManCheck(pNew) )
        printf( "Ivy_ManMakeSeq(): The check has failed.\n" );
    return pNew;
}

static int Ivy_ManExorNum ( Ivy_Man_t *  p )

inlinestatic

Definition at line 223 of file ivy.h.

{ return p->nObjs[IVY_EXOR];                  }

static Ivy_Obj_t* Ivy_ManFetchMemory ( Ivy_Man_t *  p )

inlinestatic

Definition at line 364 of file ivy.h.

{ 
    Ivy_Obj_t * pTemp;
    if ( p->pListFree == NULL )
        Ivy_ManAddMemory( p );
    pTemp = p->pListFree;
    p->pListFree = *((Ivy_Obj_t **)pTemp);
    memset( pTemp, 0, sizeof(Ivy_Obj_t) ); 
    return pTemp;
}

Ivy_Man_t* Ivy_ManFrames	(	Ivy_Man_t *	pMan,
		int	nLatches,
		int	nFrames,
		int	fInit,
		Vec_Ptr_t **	pvMapping
	)

Function*************************************************************

Synopsis [Stops the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 172 of file ivyMan.c.

{
    Vec_Ptr_t * vMapping;
    Ivy_Man_t * pNew;
    Ivy_Obj_t * pObj;
    int i, f, nPis, nPos, nIdMax;
    assert( Ivy_ManLatchNum(pMan) == 0 );
    assert( nFrames > 0 );
    // prepare the mapping
    nPis = Ivy_ManPiNum(pMan) - nLatches;
    nPos = Ivy_ManPoNum(pMan) - nLatches;
    nIdMax = Ivy_ManObjIdMax(pMan);
    // create the new manager
    pNew = Ivy_ManStart();
    // set the starting values of latch inputs
    for ( i = 0; i < nLatches; i++ )
        Ivy_ManPo(pMan, nPos+i)->pEquiv = fInit? Ivy_Not(Ivy_ManConst1(pNew)) : Ivy_ObjCreatePi(pNew);
    // add timeframes
    vMapping = Vec_PtrStart( nIdMax * nFrames + 1 );
    for ( f = 0; f < nFrames; f++ )
    {
        // create PIs
        Ivy_ManConst1(pMan)->pEquiv = Ivy_ManConst1(pNew);
        for ( i = 0; i < nPis; i++ )
            Ivy_ManPi(pMan, i)->pEquiv = Ivy_ObjCreatePi(pNew);
        // transfer values to latch outputs
        for ( i = 0; i < nLatches; i++ )
            Ivy_ManPi(pMan, nPis+i)->pEquiv = Ivy_ManPo(pMan, nPos+i)->pEquiv;
        // perform strashing
        Ivy_ManForEachNode( pMan, pObj, i )
            pObj->pEquiv = Ivy_And( pNew, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
        // create POs
        for ( i = 0; i < nPos; i++ )
            Ivy_ManPo(pMan, i)->pEquiv = Ivy_ObjCreatePo( pNew, Ivy_ObjChild0Equiv(Ivy_ManPo(pMan, i)) );
        // set the results of latch inputs
        for ( i = 0; i < nLatches; i++ )
            Ivy_ManPo(pMan, nPos+i)->pEquiv = Ivy_ObjChild0Equiv(Ivy_ManPo(pMan, nPos+i));
        // save the pointers in this frame
        Ivy_ManForEachObj( pMan, pObj, i )
            Vec_PtrWriteEntry( vMapping, f * nIdMax + i, pObj->pEquiv );
    }
    // connect latches
    if ( !fInit )
        for ( i = 0; i < nLatches; i++ )
            Ivy_ObjCreatePo( pNew, Ivy_ManPo(pMan, nPos+i)->pEquiv );
    // remove dangling nodes
    Ivy_ManCleanup(pNew);
    *pvMapping = vMapping;
    // check the resulting network
    if ( !Ivy_ManCheck(pNew) )
        printf( "Ivy_ManFrames(): The check has failed.\n" );
    return pNew;
}

static int Ivy_ManGetCost ( Ivy_Man_t *  p )

inlinestatic

Definition at line 229 of file ivy.h.

{ return p->nObjs[IVY_AND]+3*p->nObjs[IVY_EXOR]+8*p->nObjs[IVY_LATCH]; }

static Ivy_Obj_t* Ivy_ManGhost ( Ivy_Man_t *  p )

inlinestatic

Definition at line 200 of file ivy.h.

{ return &p->Ghost;                               }

void Ivy_ManHaigCreateChoice	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObjOld,
		Ivy_Obj_t *	pObjNew
	)

Function*************************************************************

Synopsis [Sets the pair of equivalent nodes in HAIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 246 of file ivyHaig.c.

{
    Ivy_Obj_t * pObjOldHaig, * pObjNewHaig;
    Ivy_Obj_t * pObjOldHaigR, * pObjNewHaigR;
    int fCompl;
//printf( "\nCreating choice for %d and %d in AIG\n", pObjOld->Id, Ivy_Regular(pObjNew)->Id );

    assert( p->pHaig != NULL );
    assert( !Ivy_IsComplement(pObjOld) );
    // get pointers to the representatives of pObjOld and pObjNew
    pObjOldHaig = pObjOld->pEquiv;
    pObjNewHaig = Ivy_NotCond( Ivy_Regular(pObjNew)->pEquiv, Ivy_IsComplement(pObjNew) );
    // get the classes
    pObjOldHaig = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObjOldHaig)), Ivy_IsComplement(pObjOldHaig) );
    pObjNewHaig = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObjNewHaig)), Ivy_IsComplement(pObjNewHaig) );
    // get regular pointers
    pObjOldHaigR = Ivy_Regular(pObjOldHaig);
    pObjNewHaigR = Ivy_Regular(pObjNewHaig);
    // check if there is phase difference between them
    fCompl = (Ivy_IsComplement(pObjOldHaig) != Ivy_IsComplement(pObjNewHaig));
    // if the class is the same, nothing to do
    if ( pObjOldHaigR == pObjNewHaigR )
        return;
    // if the second node belongs to a class, do not merge classes (for the time being)
    if ( Ivy_ObjRefs(pObjOldHaigR) == 0 || pObjNewHaigR->pEquiv != NULL || 
        Ivy_ObjRefs(pObjNewHaigR) > 0 ) //|| Ivy_ObjIsInTfi_rec(pObjNewHaigR, pObjOldHaigR, 10) )
    {
/*
        if ( pObjNewHaigR->pEquiv != NULL )
            printf( "c" );
        if ( Ivy_ObjRefs(pObjNewHaigR) > 0 )
            printf( "f" );
        printf( " " );
*/
        p->pHaig->nClassesSkip++;
        return;
    }

    // add this node to the class of pObjOldHaig
    assert( Ivy_ObjRefs(pObjOldHaigR) > 0 );
    assert( !Ivy_IsComplement(pObjOldHaigR->pEquiv) );
    if ( pObjOldHaigR->pEquiv == NULL )
        pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl );
    else
        pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR->pEquiv, fCompl );
    pObjOldHaigR->pEquiv = pObjNewHaigR;
//printf( "Setting choice node %d -> %d.\n", pObjOldHaigR->Id, pObjNewHaigR->Id );
    // update the class of the new node
//    Ivy_Regular(pObjNew)->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl ^ Ivy_IsComplement(pObjNew) );
//printf( "Creating choice for %d and %d in HAIG\n", pObjOldHaigR->Id, pObjNewHaigR->Id );

//    if ( pObjOldHaigR->Id == 13 )
//    {
//        Ivy_ManShow( p, 0 );
//        Ivy_ManShow( p->pHaig, 1 );
//    }
//    if ( !Ivy_ManIsAcyclic( p->pHaig ) )
//        printf( "HAIG contains a cycle\n" );
}

void Ivy_ManHaigCreateObj	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj
	)

Function*************************************************************

Synopsis [Creates a new node in HAIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 183 of file ivyHaig.c.

{
    Ivy_Obj_t * pEquiv0, * pEquiv1;
    assert( p->pHaig != NULL );
    assert( !Ivy_IsComplement(pObj) );
    if ( Ivy_ObjType(pObj) == IVY_BUF )
        pObj->pEquiv = Ivy_ObjChild0Equiv(pObj);
    else if ( Ivy_ObjType(pObj) == IVY_LATCH )
    {
//        pObj->pEquiv = Ivy_Latch( p->pHaig, Ivy_ObjChild0Equiv(pObj), pObj->Init );
        pEquiv0 = Ivy_ObjChild0Equiv(pObj);
        pEquiv0 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv0)), Ivy_IsComplement(pEquiv0) );
        pObj->pEquiv = Ivy_Latch( p->pHaig, pEquiv0, (Ivy_Init_t)pObj->Init );
    }
    else if ( Ivy_ObjType(pObj) == IVY_AND )
    {
//        pObj->pEquiv = Ivy_And( p->pHaig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
        pEquiv0 = Ivy_ObjChild0Equiv(pObj);
        pEquiv0 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv0)), Ivy_IsComplement(pEquiv0) );
        pEquiv1 = Ivy_ObjChild1Equiv(pObj);
        pEquiv1 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv1)), Ivy_IsComplement(pEquiv1) );
        pObj->pEquiv = Ivy_And( p->pHaig, pEquiv0, pEquiv1 );
    }
    else assert( 0 );
    // make sure the node points to the representative
//    pObj->pEquiv = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObj->pEquiv)), Ivy_IsComplement(pObj->pEquiv) );
}

void Ivy_ManHaigPostprocess	(	Ivy_Man_t *	p,
		int	fVerbose
	)

Function*************************************************************

Synopsis [Prints statistics of the HAIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file ivyHaig.c.

{
    int nChoices, nChoiceNodes;

    assert( p->pHaig != NULL );

    if ( fVerbose )
    {
        printf( "Final    : " );
        Ivy_ManPrintStats( p );
        printf( "HAIG     : " );
        Ivy_ManPrintStats( p->pHaig );

        // print choice node stats
        nChoiceNodes = Ivy_ManHaigCountChoices( p, &nChoices );
        printf( "Total choice nodes = %d. Total choices = %d. Skipped classes = %d.\n", 
            nChoiceNodes, nChoices, p->pHaig->nClassesSkip ); 
    }

    if ( Ivy_ManIsAcyclic( p->pHaig ) )
    {
        if ( fVerbose )
            printf( "HAIG is acyclic\n" );
    }
    else
        printf( "HAIG contains a cycle\n" );

//    if ( fVerbose )
//        Ivy_ManHaigSimulate( p );
}

void Ivy_ManHaigSimulate

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Simulate HAIG using modified 3-valued simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 440 of file ivyHaig.c.

{
    Vec_Int_t * vNodes, * vLatches, * vLatchesD;
    Ivy_Obj_t * pObj, * pTemp;
    Ivy_Init_t In0, In1;
    int i, k, Counter;
    int fVerbose = 0;

    // check choices
    Ivy_ManCheckChoices( p );

    // switch to HAIG
    assert( p->pHaig != NULL );
    p = p->pHaig;

if ( fVerbose )
Ivy_ManForEachPi( p, pObj, i )
printf( "Setting PI %d\n", pObj->Id );

    // collect latches and nodes in the DFS order
    vNodes = Ivy_ManDfsSeq( p, &vLatches );

if ( fVerbose )
Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
printf( "Collected node %d with fanins %d and %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id );

    // set the PI values
    Ivy_ManConst1(p)->Init = IVY_INIT_1;
    Ivy_ManForEachPi( p, pObj, i )
        pObj->Init = IVY_INIT_0;

    // set the latch values
    Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
        pObj->Init = IVY_INIT_DC;
    // set the latches of D to be determinate
    vLatchesD = (Vec_Int_t *)p->pData;
    Ivy_ManForEachNodeVec( p, vLatchesD, pObj, i )
        pObj->Init = IVY_INIT_0;

    // perform several rounds of simulation
    for ( k = 0; k < 10; k++ )
    {
        // count the number of non-determinate values
        Counter = 0;
        Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
            Counter += ( pObj->Init == IVY_INIT_DC );
        printf( "Iter %d : Non-determinate = %d\n", k, Counter );    
        
        // simulate the internal nodes
        Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
        {
if ( fVerbose )
printf( "Processing node %d with fanins %d and %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id );
            In0 = Ivy_InitNotCond( (Ivy_Init_t)Ivy_ObjFanin0(pObj)->Init, Ivy_ObjFaninC0(pObj) );
            In1 = Ivy_InitNotCond( (Ivy_Init_t)Ivy_ObjFanin1(pObj)->Init, Ivy_ObjFaninC1(pObj) );
            pObj->Init = Ivy_ManHaigSimulateAnd( In0, In1 );
            // simulate the equivalence class if the node is a representative
            if ( pObj->pEquiv && Ivy_ObjRefs(pObj) > 0 )
            {
if ( fVerbose )
printf( "Processing choice node %d\n", pObj->Id );
                In0 = (Ivy_Init_t)pObj->Init;
                assert( !Ivy_IsComplement(pObj->pEquiv) );
                for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
                {
if ( fVerbose )
printf( "Processing secondary node %d\n", pTemp->Id );
                    In1 = Ivy_InitNotCond( (Ivy_Init_t)pTemp->Init, Ivy_IsComplement(pTemp->pEquiv) );
                    In0 = Ivy_ManHaigSimulateChoice( In0, In1 );
                }
                pObj->Init = In0;
            }
        }

        // simulate the latches
        Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
        {
            pObj->Level = Ivy_ObjFanin0(pObj)->Init;
if ( fVerbose )
printf( "Using latch %d with fanin %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id );
        }
        Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
            pObj->Init = pObj->Level, pObj->Level = 0;
    }
    // free arrays
    Vec_IntFree( vNodes );
    Vec_IntFree( vLatches );
}

void Ivy_ManHaigStart	(	Ivy_Man_t *	p,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Starts HAIG for the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 94 of file ivyHaig.c.

{
    Vec_Int_t * vLatches;
    Ivy_Obj_t * pObj;
    int i;
    assert( p->pHaig == NULL );
    p->pHaig = Ivy_ManDup( p );

    if ( fVerbose )
    {
        printf( "Starting : " );
        Ivy_ManPrintStats( p->pHaig );
    }

    // collect latches of design D and set their values to be DC
    vLatches = Vec_IntAlloc( 100 );
    Ivy_ManForEachLatch( p->pHaig, pObj, i )
    {
        pObj->Init = IVY_INIT_DC;
        Vec_IntPush( vLatches, pObj->Id );
    }
    p->pHaig->pData = vLatches;
/*
    {
        int x;
        Ivy_ManShow( p, 0, NULL );
        Ivy_ManShow( p->pHaig, 1, NULL );
        x = 0;
    }
*/
}

void Ivy_ManHaigStop

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Stops HAIG for the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 159 of file ivyHaig.c.

{
    Ivy_Obj_t * pObj;
    int i;
    assert( p->pHaig != NULL );
    Vec_IntFree( (Vec_Int_t *)p->pHaig->pData );
    Ivy_ManStop( p->pHaig );
    p->pHaig = NULL;
    // remove dangling pointers to the HAIG objects
    Ivy_ManForEachObj( p, pObj, i )
        pObj->pEquiv = NULL;
}

void Ivy_ManHaigTrasfer	(	Ivy_Man_t *	p,
		Ivy_Man_t *	pNew
	)

Function*************************************************************

Synopsis [Transfers the HAIG to the newly created manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file ivyHaig.c.

{
    Ivy_Obj_t * pObj;
    int i;
    assert( p->pHaig != NULL );
    Ivy_ManConst1(pNew)->pEquiv = Ivy_ManConst1(p)->pEquiv;
    Ivy_ManForEachPi( pNew, pObj, i )
        pObj->pEquiv = Ivy_ManPi( p, i )->pEquiv;
    pNew->pHaig = p->pHaig;
}

static int Ivy_ManHashObjNum ( Ivy_Man_t *  p )

inlinestatic

Definition at line 228 of file ivy.h.

{ return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR]+p->nObjs[IVY_LATCH];     }

void Ivy_ManIncrementTravId

(

Ivy_Man_t *

p

)

DECLARATIONS ///.

CFile****************************************************************

FileName [ivyUtil.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [Various procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id:

ivyUtil.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Increments the current traversal ID of the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file ivyUtil.c.

{
    if ( p->nTravIds >= (1<<30)-1 - 1000 )
        Ivy_ManCleanTravId( p );
    p->nTravIds++;
}

int Ivy_ManIsAcyclic

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Detects combinational loops.]

Description [This procedure is based on the idea suggested by Donald Chai. As we traverse the network and visit the nodes, we need to distinquish three types of nodes: (1) those that are visited for the first time, (2) those that have been visited in this traversal but are currently not on the traversal path, (3) those that have been visited and are currently on the travesal path. When the node of type (3) is encountered, it means that there is a combinational loop. To mark the three types of nodes, two new values of the traversal IDs are used.]

SideEffects []

SeeAlso []

Definition at line 373 of file ivyDfs.c.

{
    Ivy_Obj_t * pObj;
    int fAcyclic, i;
    // set the traversal ID for this DFS ordering
    Ivy_ManIncrementTravId( p );   
    Ivy_ManIncrementTravId( p );   
    // pObj->TravId == pNet->nTravIds      means "pObj is on the path"
    // pObj->TravId == pNet->nTravIds - 1  means "pObj is visited but is not on the path"
    // pObj->TravId <  pNet->nTravIds - 1  means "pObj is not visited"
    // traverse the network to detect cycles
    fAcyclic = 1;
    Ivy_ManForEachCo( p, pObj, i )
    {
        // traverse the output logic cone
        if ( (fAcyclic = Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pObj))) )
            continue;
        // stop as soon as the first loop is detected
        fprintf( stdout, " (cone of %s \"%d\")\n", Ivy_ObjIsLatch(pObj)? "latch" : "PO", Ivy_ObjId(pObj) );
        break;
    }
    return fAcyclic;
}

Vec_Int_t* Ivy_ManLatches

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Collect the latches.]

Description []

SideEffects []

SeeAlso []

Definition at line 227 of file ivyUtil.c.

{
    Vec_Int_t * vLatches;
    Ivy_Obj_t * pObj;
    int i;
    vLatches = Vec_IntAlloc( Ivy_ManLatchNum(p) );
    Ivy_ManForEachLatch( p, pObj, i )
        Vec_IntPush( vLatches, pObj->Id );
    return vLatches;
}

static int Ivy_ManLatchNum ( Ivy_Man_t *  p )

inlinestatic

Definition at line 221 of file ivy.h.

{ return p->nObjs[IVY_LATCH];                 }

Vec_Vec_t* Ivy_ManLevelize

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Returns the nodes by level.]

Description []

SideEffects []

SeeAlso []

Definition at line 224 of file ivyDfs.c.

{
    Vec_Vec_t * vNodes;
    Ivy_Obj_t * pObj;
    int i;
    vNodes = Vec_VecAlloc( 100 );
    Ivy_ManForEachObj( p, pObj, i )
    {
        assert( !Ivy_ObjIsBuf(pObj) );
        if ( Ivy_ObjIsNode(pObj) )
            Vec_VecPush( vNodes, pObj->Level, pObj );
    }
    return vNodes;
}

int Ivy_ManLevels

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Collect the latches.]

Description []

SideEffects []

SeeAlso []

Definition at line 249 of file ivyUtil.c.

{
    Ivy_Obj_t * pObj;
    int i, LevelMax = 0;
    Ivy_ManForEachPo( p, pObj, i )
        LevelMax = IVY_MAX( LevelMax, (int)Ivy_ObjFanin0(pObj)->Level );
    return LevelMax;
}

void Ivy_ManMakeSeq	(	Ivy_Man_t *	p,
		int	nLatches,
		int *	pInits
	)

Function*************************************************************

Synopsis [Converts a combinational AIG manager into a sequential one.]

Description []

SideEffects []

SeeAlso []

Definition at line 482 of file ivyMan.c.

{
    Ivy_Obj_t * pObj, * pLatch;
    Ivy_Init_t Init;
    int i;
    if ( nLatches == 0 )
        return;
    assert( nLatches < Ivy_ManPiNum(p) && nLatches < Ivy_ManPoNum(p) );
    assert( Ivy_ManPiNum(p) == Vec_PtrSize(p->vPis) );
    assert( Ivy_ManPoNum(p) == Vec_PtrSize(p->vPos) );
    assert( Vec_PtrSize( p->vBufs ) == 0 );
    // create fanouts
    if ( p->fFanout == 0 )
        Ivy_ManStartFanout( p );
    // collect the POs to be converted into latches
    for ( i = 0; i < nLatches; i++ )
    {
        // get the latch value
        Init = pInits? (Ivy_Init_t)pInits[i] : IVY_INIT_0;
        // create latch
        pObj = Ivy_ManPo( p, Ivy_ManPoNum(p) - nLatches + i );
        pLatch = Ivy_Latch( p, Ivy_ObjChild0(pObj), Init );
        Ivy_ObjDisconnect( p, pObj );
        // recycle the old PO object
        Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
        Ivy_ManRecycleMemory( p, pObj );
        // convert the corresponding PI to a buffer and connect it to the latch
        pObj = Ivy_ManPi( p, Ivy_ManPiNum(p) - nLatches + i );
        pObj->Type = IVY_BUF;
        Ivy_ObjConnect( p, pObj, pLatch, NULL );
        // save the buffer
        Vec_PtrPush( p->vBufs, pObj );
    }
    // shrink the arrays
    Vec_PtrShrink( p->vPis, Ivy_ManPiNum(p) - nLatches );
    Vec_PtrShrink( p->vPos, Ivy_ManPoNum(p) - nLatches );
    // update the counters of different objects
    p->nObjs[IVY_PI] -= nLatches;
    p->nObjs[IVY_PO] -= nLatches;
    p->nObjs[IVY_BUF] += nLatches;
    p->nDeleted -= 2 * nLatches;
    // remove dangling nodes
    Ivy_ManCleanup(p);
    Ivy_ManCleanupSeq(p);
/* 
    // check for dangling nodes
    Ivy_ManForEachObj( p, pObj, i )
        if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsPo(pObj) && !Ivy_ObjIsConst1(pObj) )
        {
            assert( Ivy_ObjRefs(pObj) > 0 );
            assert( Ivy_ObjRefs(pObj) == Ivy_ObjFanoutNum(p, pObj) );
        }
*/
    // perform hashing by propagating the buffers
    Ivy_ManPropagateBuffers( p, 0 );
    if ( Ivy_ManBufNum(p) )
        printf( "The number of remaining buffers is %d.\n", Ivy_ManBufNum(p) );
    // fix the levels
    Ivy_ManResetLevels( p );
    // check the resulting network
    if ( !Ivy_ManCheck(p) )
        printf( "Ivy_ManMakeSeq(): The check has failed.\n" );
}

static int Ivy_ManNodeNum ( Ivy_Man_t *  p )

inlinestatic

Definition at line 227 of file ivy.h.

{ return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR];}

static Ivy_Obj_t* Ivy_ManObj ( Ivy_Man_t *  p, int  i  )

inlinestatic

Definition at line 203 of file ivy.h.

{ return (Ivy_Obj_t *)Vec_PtrEntry(p->vObjs, i);  }

static int Ivy_ManObjIdMax ( Ivy_Man_t *  p )

inlinestatic

Definition at line 226 of file ivy.h.

{ return Vec_PtrSize(p->vObjs)-1;             }

static int Ivy_ManObjNum ( Ivy_Man_t *  p )

inlinestatic

Definition at line 225 of file ivy.h.

{ return p->nCreated - p->nDeleted;           }

static Ivy_Obj_t* Ivy_ManPi ( Ivy_Man_t *  p, int  i  )

inlinestatic

Definition at line 201 of file ivy.h.

{ return (Ivy_Obj_t *)Vec_PtrEntry(p->vPis, i);   }

static int Ivy_ManPiNum ( Ivy_Man_t *  p )

inlinestatic

Definition at line 218 of file ivy.h.

{ return p->nObjs[IVY_PI];                    }

static Ivy_Obj_t* Ivy_ManPo ( Ivy_Man_t *  p, int  i  )

inlinestatic

Definition at line 202 of file ivy.h.

{ return (Ivy_Obj_t *)Vec_PtrEntry(p->vPos, i);   }

static int Ivy_ManPoNum ( Ivy_Man_t *  p )

inlinestatic

Definition at line 219 of file ivy.h.

{ return p->nObjs[IVY_PO];                    }

void Ivy_ManPrintStats

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Stops the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 456 of file ivyMan.c.

{
    printf( "PI/PO = %d/%d ", Ivy_ManPiNum(p), Ivy_ManPoNum(p) );
    printf( "A = %7d. ",       Ivy_ManAndNum(p) );
    printf( "L = %5d. ",       Ivy_ManLatchNum(p) );
//    printf( "X = %d. ",       Ivy_ManExorNum(p) );
//    printf( "B = %3d. ",       Ivy_ManBufNum(p) );
    printf( "MaxID = %7d. ",   Ivy_ManObjIdMax(p) );
//    printf( "Cre = %d. ",     p->nCreated );
//    printf( "Del = %d. ",     p->nDeleted );
    printf( "Lev = %3d. ",     Ivy_ManLatchNum(p)? -1 : Ivy_ManLevels(p) );
    printf( "\n" );
    fflush( stdout );
}

void Ivy_ManPrintVerbose	(	Ivy_Man_t *	p,
		int	fHaig
	)

Function*************************************************************

Synopsis [Prints node in HAIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 714 of file ivyUtil.c.

{
    Vec_Int_t * vNodes;
    Ivy_Obj_t * pObj;
    int i;
    printf( "PIs: " );
    Ivy_ManForEachPi( p, pObj, i )
        printf( " %d", pObj->Id );
    printf( "\n" );
    printf( "POs: " );
    Ivy_ManForEachPo( p, pObj, i )
        printf( " %d", pObj->Id );
    printf( "\n" );
    printf( "Latches: " );
    Ivy_ManForEachLatch( p, pObj, i )
        printf( " %d=%d%s", pObj->Id, Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
    printf( "\n" );
    vNodes = Ivy_ManDfsSeq( p, NULL );
    Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
        Ivy_ObjPrintVerbose( p, pObj, fHaig ), printf( "\n" );
    printf( "\n" );
    Vec_IntFree( vNodes );
}

int Ivy_ManPropagateBuffers	(	Ivy_Man_t *	p,
		int	fUpdateLevel
	)

Function*************************************************************

Synopsis [Returns the number of dangling nodes removed.]

Description []

SideEffects []

SeeAlso []

Definition at line 414 of file ivyMan.c.

{
    Ivy_Obj_t * pNode;
    int LimitFactor = 100;
    int NodeBeg = Ivy_ManNodeNum(p);
    int nSteps;
    for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )
    {
        pNode = (Ivy_Obj_t *)Vec_PtrEntryLast(p->vBufs);
        while ( Ivy_ObjIsBuf(pNode) )
            pNode = Ivy_ObjReadFirstFanout( p, pNode );
        // check if this buffer should remain
        if ( Ivy_ManLatchIsSelfFeed(pNode) )
        {
            Vec_PtrPop(p->vBufs);
            continue;
        }
//printf( "Propagating buffer %d with input %d and output %d\n", Ivy_ObjFaninId0(pNode), Ivy_ObjFaninId0(Ivy_ObjFanin0(pNode)), pNode->Id );
//printf( "Latch num %d\n", Ivy_ManLatchNum(p) );
        Ivy_NodeFixBufferFanins( p, pNode, fUpdateLevel );
        if ( nSteps > NodeBeg * LimitFactor )
        {
            printf( "Structural hashing is not finished after %d forward latch moves.\n", NodeBeg * LimitFactor );
            printf( "This circuit cannot be forward-retimed completely. Quitting.\n" );
            break;
        }
    }
//    printf( "Number of steps = %d. Nodes beg = %d. Nodes end = %d.\n", nSteps, NodeBeg, Ivy_ManNodeNum(p) );
    return nSteps;
}

static void Ivy_ManRecycleMemory ( Ivy_Man_t *  p, Ivy_Obj_t *  pEntry  )

inlinestatic

Definition at line 374 of file ivy.h.

{
    pEntry->Type = IVY_NONE; // distinquishes dead node from live node
    *((Ivy_Obj_t **)pEntry) = p->pListFree;
    p->pListFree = pEntry;
}

Vec_Int_t* Ivy_ManRequiredLevels

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Computes required levels for each node.]

Description [Assumes topological ordering of the nodes.]

SideEffects []

SeeAlso []

Definition at line 250 of file ivyDfs.c.

{
    Ivy_Obj_t * pObj;
    Vec_Int_t * vLevelsR;
    Vec_Vec_t * vNodes;
    int i, k, Level, LevelMax;
    assert( p->vRequired == NULL );
    // start the required times
    vLevelsR = Vec_IntStart( Ivy_ManObjIdMax(p) + 1 );
    // iterate through the nodes in the reverse order
    vNodes = Ivy_ManLevelize( p );
    Vec_VecForEachEntryReverseReverse( Ivy_Obj_t *, vNodes, pObj, i, k )
    {
        Level = Vec_IntEntry( vLevelsR, pObj->Id ) + 1 + Ivy_ObjIsExor(pObj);
        if ( Vec_IntEntry( vLevelsR, Ivy_ObjFaninId0(pObj) ) < Level )
            Vec_IntWriteEntry( vLevelsR, Ivy_ObjFaninId0(pObj), Level );
        if ( Vec_IntEntry( vLevelsR, Ivy_ObjFaninId1(pObj) ) < Level )
            Vec_IntWriteEntry( vLevelsR, Ivy_ObjFaninId1(pObj), Level );
    }
    Vec_VecFree( vNodes );
    // convert it into the required times
    LevelMax = Ivy_ManLevels( p );
//printf( "max %5d\n",LevelMax );
    Ivy_ManForEachObj( p, pObj, i )
    {
        Level = Vec_IntEntry( vLevelsR, pObj->Id );
        Vec_IntWriteEntry( vLevelsR, pObj->Id, LevelMax - Level );
//printf( "%5d : %5d %5d\n", pObj->Id, Level, LevelMax - Level );
    }
    p->vRequired = vLevelsR;
    return vLevelsR;
}

void Ivy_ManResetLevels

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Collect the latches.]

Description []

SideEffects []

SeeAlso []

Definition at line 292 of file ivyUtil.c.

{
    Ivy_Obj_t * pObj;
    int i;
    Ivy_ManForEachObj( p, pObj, i )
        pObj->Level = 0;
    Ivy_ManForEachCo( p, pObj, i )
        Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
}

Ivy_Man_t* Ivy_ManResyn	(	Ivy_Man_t *	pMan,
		int	fUpdateLevel,
		int	fVerbose
	)

Function*************************************************************

Synopsis [Performs several passes of rewriting on the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 86 of file ivyResyn.c.

{
    abctime clk;
    Ivy_Man_t * pTemp;

if ( fVerbose ) { printf( "Original:\n" ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );

clk = Abc_Clock();
    pMan = Ivy_ManBalance( pMan, fUpdateLevel );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );

//    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 );
clk = Abc_Clock();
    Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );

clk = Abc_Clock();
    pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
    Ivy_ManStop( pTemp );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );

//    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 );
clk = Abc_Clock();
    Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );

clk = Abc_Clock();
    pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
    Ivy_ManStop( pTemp );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );

//    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 );
clk = Abc_Clock();
    Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );

clk = Abc_Clock();
    pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
    Ivy_ManStop( pTemp );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
    return pMan;
}

Ivy_Man_t* Ivy_ManResyn0	(	Ivy_Man_t *	pMan,
		int	fUpdateLevel,
		int	fVerbose
	)

DECLARATIONS ///.

CFile****************************************************************

FileName [ivyResyn.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [AIG rewriting script.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id:

ivyResyn.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Performs several passes of rewriting on the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file ivyResyn.c.

{
    abctime clk;
    Ivy_Man_t * pTemp;

if ( fVerbose ) { printf( "Original:\n" ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );

clk = Abc_Clock();
    pMan = Ivy_ManBalance( pMan, fUpdateLevel );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );

//    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 );
clk = Abc_Clock();
    Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );

clk = Abc_Clock();
    pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
    Ivy_ManStop( pTemp );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
    return pMan;
}

int Ivy_ManRewriteAlg	(	Ivy_Man_t *	p,
		int	fUpdateLevel,
		int	fUseZeroCost
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Algebraic AIG rewriting.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file ivyRwrAlg.c.

{
    Vec_Int_t * vRequired;
    Vec_Ptr_t * vFront, * vLeaves, * vCone, * vSol;
    Ivy_Obj_t * pObj, * pResult;
    int i, RetValue, LevelR, nNodesOld;
    int CountUsed, CountUndo;
    vRequired = fUpdateLevel? Ivy_ManRequiredLevels( p ) : NULL;
    vFront    = Vec_PtrAlloc( 100 );
    vLeaves   = Vec_PtrAlloc( 100 );
    vCone     = Vec_PtrAlloc( 100 );
    vSol      = Vec_PtrAlloc( 100 );
    // go through the nodes in the topological order
    CountUsed = CountUndo = 0;
    nNodesOld = Ivy_ManObjIdNext(p);
    Ivy_ManForEachObj( p, pObj, i )
    {
        assert( !Ivy_ObjIsBuf(pObj) );
        if ( i >= nNodesOld )
            break;
        // skip no-nodes and MUX roots
        if ( !Ivy_ObjIsNode(pObj) || Ivy_ObjIsExor(pObj) || Ivy_ObjIsMuxType(pObj) )
            continue;
//        if ( pObj->Id > 297 ) // 296 --- 297 
//            break;
        if ( pObj->Id == 297 )
        {
            int x = 0;
        }
        // get the largest algebraic cut
        RetValue = Ivy_ManFindAlgCut( pObj, vFront, vLeaves, vCone );
        // the case of a trivial tree cut
        if ( RetValue == 1 )
            continue;
        // the case of constant 0 cone
        if ( RetValue == -1 )
        {
            Ivy_ObjReplace( pObj, Ivy_ManConst0(p), 1, 0, 1 ); 
            continue;
        }
        assert( Vec_PtrSize(vLeaves) > 2 );
        // get the required level for this node
        LevelR = vRequired? Vec_IntEntry(vRequired, pObj->Id) : 1000000;
        // create a new cone
        pResult = Ivy_NodeRewriteAlg( pObj, vFront, vLeaves, vCone, vSol, LevelR, fUseZeroCost );
        if ( pResult == NULL || pResult == pObj )
            continue;
        assert( Vec_PtrSize(vSol) == 1 || !Ivy_IsComplement(pResult) );
        if ( Ivy_ObjLevel(Ivy_Regular(pResult)) > LevelR && Ivy_ObjRefs(Ivy_Regular(pResult)) == 0 )
            Ivy_ObjDelete_rec(Ivy_Regular(pResult), 1), CountUndo++;
        else
            Ivy_ObjReplace( pObj, pResult, 1, 0, 1 ), CountUsed++; 
    }
    printf( "Used = %d. Undo = %d.\n", CountUsed, CountUndo );
    Vec_PtrFree( vFront );
    Vec_PtrFree( vCone );
    Vec_PtrFree( vSol );
    if ( vRequired ) Vec_IntFree( vRequired );
    if ( i = Ivy_ManCleanup(p) )
        printf( "Cleanup after rewriting removed %d dangling nodes.\n", i );
    if ( !Ivy_ManCheck(p) )
        printf( "Ivy_ManRewriteAlg(): The check has failed.\n" );
    return 1;
}

int Ivy_ManRewritePre	(	Ivy_Man_t *	p,
		int	fUpdateLevel,
		int	fUseZeroCost,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Performs incremental rewriting of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 55 of file ivyRwr.c.

{
    Rwt_Man_t * pManRwt;
    Ivy_Obj_t * pNode;
    int i, nNodes, nGain;
    abctime clk, clkStart = Abc_Clock();
    // start the rewriting manager
    pManRwt = Rwt_ManStart( 0 );
    p->pData = pManRwt;
    if ( pManRwt == NULL )
        return 0; 
    // create fanouts
    if ( fUpdateLevel && p->fFanout == 0 )
        Ivy_ManStartFanout( p );
    // compute the reverse levels if level update is requested
    if ( fUpdateLevel )
        Ivy_ManRequiredLevels( p );
    // set the number of levels
//    p->nLevelMax = Ivy_ManLevels( p );
    // resynthesize each node once
    nNodes = Ivy_ManObjIdMax(p);
    Ivy_ManForEachNode( p, pNode, i )
    {
        // fix the fanin buffer problem
        Ivy_NodeFixBufferFanins( p, pNode, 1 );
        if ( Ivy_ObjIsBuf(pNode) )
            continue;
        // stop if all nodes have been tried once
        if ( i > nNodes )
            break;
        // for each cut, try to resynthesize it
        nGain = Ivy_NodeRewrite( p, pManRwt, pNode, fUpdateLevel, fUseZeroCost );
        if ( nGain > 0 || (nGain == 0 && fUseZeroCost) )
        {
            Dec_Graph_t * pGraph = (Dec_Graph_t *)Rwt_ManReadDecs(pManRwt);
            int fCompl           = Rwt_ManReadCompl(pManRwt);
/*
            {
                Ivy_Obj_t * pObj;
                int i;
                printf( "USING: (" );
                Vec_PtrForEachEntry( Ivy_Obj_t *, Rwt_ManReadLeaves(pManRwt), pObj, i )
                    printf( "%d ", Ivy_ObjFanoutNum(Ivy_Regular(pObj)) );
                printf( ")   Gain = %d.\n", nGain );
            }
            if ( nGain > 0 )
            { // print stats on the MFFC
                extern void Ivy_NodeMffcConeSuppPrint( Ivy_Obj_t * pNode );
                printf( "Node %6d : Gain = %4d  ", pNode->Id, nGain );
                Ivy_NodeMffcConeSuppPrint( pNode );
            }
*/
            // complement the FF if needed
clk = Abc_Clock();
            if ( fCompl ) Dec_GraphComplement( pGraph );
            Ivy_GraphUpdateNetwork( p, pNode, pGraph, fUpdateLevel, nGain );
            if ( fCompl ) Dec_GraphComplement( pGraph );
Rwt_ManAddTimeUpdate( pManRwt, Abc_Clock() - clk );
        }
    }
Rwt_ManAddTimeTotal( pManRwt, Abc_Clock() - clkStart );
    // print stats
    if ( fVerbose )
        Rwt_ManPrintStats( pManRwt );
    // delete the managers
    Rwt_ManStop( pManRwt );
    p->pData = NULL;
    // fix the levels
    if ( fUpdateLevel )
        Vec_IntFree( p->vRequired ), p->vRequired = NULL;
    else
        Ivy_ManResetLevels( p );
    // check
    if ( (i = Ivy_ManCleanup(p)) )
        printf( "Cleanup after rewriting removed %d dangling nodes.\n", i );
    if ( !Ivy_ManCheck(p) )
        printf( "Ivy_ManRewritePre(): The check has failed.\n" );
    return 1;
}

int Ivy_ManRewriteSeq	(	Ivy_Man_t *	p,
		int	fUseZeroCost,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Performs incremental rewriting of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file ivySeq.c.

{ 
    Rwt_Man_t * pManRwt;
    Ivy_Obj_t * pNode;
    int i, nNodes, nGain;
    abctime clk, clkStart = Abc_Clock();

    // set the DC latch values
    Ivy_ManForEachLatch( p, pNode, i )
        pNode->Init = IVY_INIT_DC;
    // start the rewriting manager
    pManRwt = Rwt_ManStart( 0 );
    p->pData = pManRwt;
    if ( pManRwt == NULL )
        return 0; 
    // create fanouts
    if ( p->fFanout == 0 )
        Ivy_ManStartFanout( p );
    // resynthesize each node once
    nNodes = Ivy_ManObjIdMax(p);
    Ivy_ManForEachNode( p, pNode, i )
    {
        assert( !Ivy_ObjIsBuf(pNode) );
        assert( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) );
        assert( !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) );
        // fix the fanin buffer problem
//        Ivy_NodeFixBufferFanins( p, pNode );
//        if ( Ivy_ObjIsBuf(pNode) )
//            continue;
        // stop if all nodes have been tried once
        if ( i > nNodes ) 
            break;
        // for each cut, try to resynthesize it
        nGain = Ivy_NodeRewriteSeq( p, pManRwt, pNode, fUseZeroCost );
        if ( nGain > 0 || (nGain == 0 && fUseZeroCost) )
        {
            Dec_Graph_t * pGraph = (Dec_Graph_t *)Rwt_ManReadDecs(pManRwt);
            int fCompl           = Rwt_ManReadCompl(pManRwt);
            // complement the FF if needed
clk = Abc_Clock();
            if ( fCompl ) Dec_GraphComplement( pGraph );
            Ivy_GraphUpdateNetworkSeq( p, pNode, pGraph, nGain );
            if ( fCompl ) Dec_GraphComplement( pGraph );
Rwt_ManAddTimeUpdate( pManRwt, Abc_Clock() - clk );
        }
    }
Rwt_ManAddTimeTotal( pManRwt, Abc_Clock() - clkStart );
    // print stats
    if ( fVerbose )
        Rwt_ManPrintStats( pManRwt );
    // delete the managers
    Rwt_ManStop( pManRwt );
    p->pData = NULL;
    // fix the levels
    Ivy_ManResetLevels( p );
//    if ( Ivy_ManCheckFanoutNums(p) )
//        printf( "Ivy_ManRewritePre(): The check has failed.\n" );
    // check
    if ( !Ivy_ManCheck(p) )
        printf( "Ivy_ManRewritePre(): The check has failed.\n" );
    return 1;
}

Ivy_Man_t* Ivy_ManRwsat	(	Ivy_Man_t *	pMan,
		int	fVerbose
	)

Function*************************************************************

Synopsis [Performs several passes of rewriting on the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file ivyResyn.c.

{
    abctime clk;
    Ivy_Man_t * pTemp;

if ( fVerbose ) { printf( "Original:\n" ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );

clk = Abc_Clock();
    Ivy_ManRewritePre( pMan, 0, 0, 0 );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );

clk = Abc_Clock();
    pMan = Ivy_ManBalance( pTemp = pMan, 0 );
//    pMan = Ivy_ManDup( pTemp = pMan );
    Ivy_ManStop( pTemp );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );

/*
clk = Abc_Clock();
    Ivy_ManRewritePre( pMan, 0, 0, 0 );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Rewrite", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );

clk = Abc_Clock();
    pMan = Ivy_ManBalance( pTemp = pMan, 0 );
    Ivy_ManStop( pTemp );
if ( fVerbose ) { printf( "\n" ); }
if ( fVerbose ) { ABC_PRT( "Balance", Abc_Clock() - clk ); }
if ( fVerbose ) Ivy_ManPrintStats( pMan );
*/
    return pMan;
}

void Ivy_ManSeqFindCut	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pRoot,
		Vec_Int_t *	vFront,
		Vec_Int_t *	vInside,
		int	nSize
	)

Function*************************************************************

Synopsis [Computes one sequential cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 183 of file ivyCut.c.

{
    assert( !Ivy_IsComplement(pRoot) );
    assert( Ivy_ObjIsNode(pRoot) );
    assert( Ivy_ObjFaninId0(pRoot) );
    assert( Ivy_ObjFaninId1(pRoot) );

    // start the cut 
    Vec_IntClear( vFront );
    Vec_IntPush( vFront, Ivy_LeafCreate(Ivy_ObjFaninId0(pRoot), 0) );
    Vec_IntPush( vFront, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) );

    // start the visited nodes
    Vec_IntClear( vInside );
    Vec_IntPush( vInside, Ivy_LeafCreate(pRoot->Id, 0) );
    Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId0(pRoot), 0) );
    Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) );

    // compute the cut
    while ( Ivy_ManSeqFindCut_int( p, vFront, vInside, nSize ) );
    assert( Vec_IntSize(vFront) <= nSize );
}

int Ivy_ManSeqRewrite	(	Ivy_Man_t *	p,
		int	fUpdateLevel,
		int	fUseZeroCost
	)

int Ivy_ManSetLevels	(	Ivy_Man_t *	p,
		int	fHaig
	)

Function*************************************************************

Synopsis [Sets the levels of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 457 of file ivyDfs.c.

{
    Ivy_Obj_t * pObj;
    int i, LevelMax;
    // check if CIs have choices
    if ( fHaig )
    {
        Ivy_ManForEachCi( p, pObj, i )
            if ( pObj->pEquiv )
                printf( "CI %d has a choice, which will not be visualized.\n", pObj->Id );
    }
    // clean the levels
    Ivy_ManForEachObj( p, pObj, i )
        pObj->Level = 0;
    // compute the levels
    LevelMax = 0;
    Ivy_ManForEachCo( p, pObj, i )
    {
        Ivy_ManSetLevels_rec( Ivy_ObjFanin0(pObj), fHaig );
        LevelMax = IVY_MAX( LevelMax, (int)Ivy_ObjFanin0(pObj)->Level );
    }
    // compute levels of nodes without fanout
    Ivy_ManForEachObj( p, pObj, i )
        if ( (Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj)) && Ivy_ObjRefs(pObj) == 0 )
        {
            Ivy_ManSetLevels_rec( pObj, fHaig );
            LevelMax = IVY_MAX( LevelMax, (int)pObj->Level );
        }
    // clean the marks
    Ivy_ManForEachObj( p, pObj, i )
        Ivy_ObjClearMarkA(pObj);
    return LevelMax;
}

void Ivy_ManShow	(	Ivy_Man_t *	pMan,
		int	fHaig,
		Vec_Ptr_t *	vBold
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file ivyShow.c.

{
    extern void Abc_ShowFile( char * FileNameDot );
    static int Counter = 0;
    char FileNameDot[200];
    FILE * pFile;
    // create the file name
//    Ivy_ShowGetFileName( pMan->pName, FileNameDot );
    sprintf( FileNameDot, "temp%02d.dot", Counter++ );
    // check that the file can be opened
    if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
    {
        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
        return;
    }
    fclose( pFile );
    // generate the file
    Ivy_WriteDotAig( pMan, FileNameDot, fHaig, vBold );
    // visualize the file 
    Abc_ShowFile( FileNameDot );
}

Ivy_Man_t* Ivy_ManStart

(

)

DECLARATIONS ///.

CFile****************************************************************

FileName [ivyMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [AIG manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id:

ivy_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Starts the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file ivyMan.c.

{
    Ivy_Man_t * p;
    // start the manager
    p = ABC_ALLOC( Ivy_Man_t, 1 );
    memset( p, 0, sizeof(Ivy_Man_t) );
    // perform initializations
    p->Ghost.Id   = -1;
    p->nTravIds   =  1;
    p->fCatchExor =  1;
    // allocate arrays for nodes
    p->vPis = Vec_PtrAlloc( 100 );
    p->vPos = Vec_PtrAlloc( 100 );
    p->vBufs = Vec_PtrAlloc( 100 );
    p->vObjs = Vec_PtrAlloc( 100 );
    // prepare the internal memory manager
    Ivy_ManStartMemory( p );
    // create the constant node
    p->pConst1 = Ivy_ManFetchMemory( p );
    p->pConst1->fPhase = 1;
    Vec_PtrPush( p->vObjs, p->pConst1 );
    p->nCreated = 1;
    // start the table
    p->nTableSize = 10007;
    p->pTable = ABC_ALLOC( int, p->nTableSize );
    memset( p->pTable, 0, sizeof(int) * p->nTableSize );
    return p;
}

void Ivy_ManStartFanout

(

Ivy_Man_t *

p

)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Starts the fanout representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 136 of file ivyFanout.c.

{
    Ivy_Obj_t * pObj;
    int i;
    assert( !p->fFanout );
    p->fFanout = 1;
    Ivy_ManForEachObj( p, pObj, i )
    {
        if ( Ivy_ObjFanin0(pObj) )
            Ivy_ObjAddFanout( p, Ivy_ObjFanin0(pObj), pObj );
        if ( Ivy_ObjFanin1(pObj) )
            Ivy_ObjAddFanout( p, Ivy_ObjFanin1(pObj), pObj );
    }
}

Ivy_Man_t* Ivy_ManStartFrom

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Duplicates the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 85 of file ivyMan.c.

{
    Ivy_Man_t * pNew;
    Ivy_Obj_t * pObj;
    int i;
    // create the new manager
    pNew = Ivy_ManStart();
    // create the PIs
    Ivy_ManConst1(p)->pEquiv = Ivy_ManConst1(pNew);
    Ivy_ManForEachPi( p, pObj, i )
        pObj->pEquiv = Ivy_ObjCreatePi(pNew);
    return pNew;
}

void Ivy_ManStartMemory

(

Ivy_Man_t *

p

)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Starts the internal memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file ivyMem.c.

{
    p->vChunks = Vec_PtrAlloc( 128 );
    p->vPages = Vec_PtrAlloc( 128 );
}

void Ivy_ManStop

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Stops the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 238 of file ivyMan.c.

{
    if ( p->time1 ) { ABC_PRT( "Update lev  ", p->time1 ); }
    if ( p->time2 ) { ABC_PRT( "Update levR ", p->time2 ); }
//    Ivy_TableProfile( p );
//    if ( p->vFanouts )  Ivy_ManStopFanout( p );
    if ( p->vChunks )   Ivy_ManStopMemory( p );
    if ( p->vRequired ) Vec_IntFree( p->vRequired );
    if ( p->vPis )      Vec_PtrFree( p->vPis );
    if ( p->vPos )      Vec_PtrFree( p->vPos );
    if ( p->vBufs )     Vec_PtrFree( p->vBufs );
    if ( p->vObjs )     Vec_PtrFree( p->vObjs );
    ABC_FREE( p->pTable );
    ABC_FREE( p );
}

void Ivy_ManStopFanout

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Stops the fanout representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 162 of file ivyFanout.c.

{
    Ivy_Obj_t * pObj;
    int i;
    assert( p->fFanout );
    p->fFanout = 0;
    Ivy_ManForEachObj( p, pObj, i )
        pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
}

void Ivy_ManStopMemory

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Stops the internal memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 66 of file ivyMem.c.

{
    void * pMemory;
    int i;
    Vec_PtrForEachEntry( void *, p->vChunks, pMemory, i )
        ABC_FREE( pMemory );
    Vec_PtrFree( p->vChunks );
    Vec_PtrFree( p->vPages );
    p->pListFree = NULL;
}

Ivy_Obj_t* Ivy_Miter	(	Ivy_Man_t *	p,
		Vec_Ptr_t *	vPairs
	)

Function*************************************************************

Synopsis [Implements the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 264 of file ivyOper.c.

{
    int i;
    assert( vPairs->nSize > 0 );
    assert( vPairs->nSize % 2 == 0 );
    // go through the cubes of the node's SOP
    for ( i = 0; i < vPairs->nSize; i += 2 )
        vPairs->pArray[i/2] = Ivy_Not( Ivy_Exor( p, (Ivy_Obj_t *)vPairs->pArray[i], (Ivy_Obj_t *)vPairs->pArray[i+1] ) );
    vPairs->nSize = vPairs->nSize/2;
    return Ivy_Not( Ivy_Multi_rec( p, (Ivy_Obj_t **)vPairs->pArray, vPairs->nSize, IVY_AND ) );
}

Ivy_Obj_t* Ivy_Multi	(	Ivy_Man_t *	p,
		Ivy_Obj_t **	pArgs,
		int	nArgs,
		Ivy_Type_t	Type
	)

Function*************************************************************

Synopsis [Old code.]

Description []

SideEffects []

SeeAlso []

Definition at line 246 of file ivyOper.c.

{
    assert( Type == IVY_AND || Type == IVY_EXOR );
    assert( nArgs > 0 );
    return Ivy_Multi_rec( p, pArgs, nArgs, Type );
}

Ivy_Obj_t* Ivy_Multi1	(	Ivy_Man_t *	p,
		Ivy_Obj_t **	pArgs,
		int	nArgs,
		Ivy_Type_t	Type
	)

Ivy_Obj_t* Ivy_Multi_rec	(	Ivy_Man_t *	p,
		Ivy_Obj_t **	ppObjs,
		int	nObjs,
		Ivy_Type_t	Type
	)

Function*************************************************************

Synopsis [Constructs the well-balanced tree of gates.]

Description [Disregards levels and possible logic sharing.]

SideEffects []

SeeAlso []

Definition at line 225 of file ivyOper.c.

{
    Ivy_Obj_t * pObj1, * pObj2;
    if ( nObjs == 1 )
        return ppObjs[0];
    pObj1 = Ivy_Multi_rec( p, ppObjs,           nObjs/2,         Type );
    pObj2 = Ivy_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type );
    return Ivy_Oper( p, pObj1, pObj2, Type );
}

Ivy_Obj_t* Ivy_MultiBalance_rec	(	Ivy_Man_t *	p,
		Ivy_Obj_t **	pArgs,
		int	nArgs,
		Ivy_Type_t	Type
	)

int Ivy_MultiPlus	(	Ivy_Man_t *	p,
		Vec_Ptr_t *	vLeaves,
		Vec_Ptr_t *	vCone,
		Ivy_Type_t	Type,
		int	nLimit,
		Vec_Ptr_t *	vSols
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Constructs a balanced tree while taking sharing into account.]

Description [Returns 1 if the implementation exists.]

SideEffects []

SeeAlso []

Definition at line 58 of file ivyMulti.c.

{
    static Ivy_Eva_t pEvals[IVY_EVAL_LIMIT];
    Ivy_Eva_t * pEval, * pFan0, * pFan1;
    Ivy_Obj_t * pObj = NULL; // Suppress "might be used uninitialized"
    Ivy_Obj_t * pTemp;
    int nEvals, nEvalsOld, i, k, x, nLeaves;
    unsigned uMaskAll;

    // consider special cases
    nLeaves = Vec_PtrSize(vLeaves);
    assert( nLeaves > 2 );
    if ( nLeaves > 32 || nLeaves + Vec_PtrSize(vCone) > IVY_EVAL_LIMIT )
        return 0;
//    if ( nLeaves == 1 )
//        return Vec_PtrEntry( vLeaves, 0 );
//    if ( nLeaves == 2 )
//        return Ivy_Oper( Vec_PtrEntry(vLeaves, 0), Vec_PtrEntry(vLeaves, 1), Type );

    // set the leaf entries
    uMaskAll = ((1 << nLeaves) - 1);
    nEvals = 0;
    Vec_PtrForEachEntry( Ivy_Obj_t *, vLeaves, pObj, i )
    {
        pEval = pEvals + nEvals;
        pEval->pArg   = pObj;
        pEval->Mask   = (1 << nEvals);
        pEval->Weight = 1;
        // mark the leaf
        Ivy_Regular(pObj)->TravId = nEvals;
        nEvals++;
    }

    // propagate masks through the cone
    Vec_PtrForEachEntry( Ivy_Obj_t *, vCone, pObj, i )
    {
        pObj->TravId = nEvals + i;
        if ( Ivy_ObjIsBuf(pObj) )
            pEvals[pObj->TravId].Mask = pEvals[Ivy_ObjFanin0(pObj)->TravId].Mask;
        else
            pEvals[pObj->TravId].Mask = pEvals[Ivy_ObjFanin0(pObj)->TravId].Mask | pEvals[Ivy_ObjFanin1(pObj)->TravId].Mask;
    }

    // set the internal entries
    Vec_PtrForEachEntry( Ivy_Obj_t *, vCone, pObj, i )
    {
        if ( i == Vec_PtrSize(vCone) - 1 )
            break;
        // skip buffers
        if ( Ivy_ObjIsBuf(pObj) )
            continue;
        // skip nodes without external fanout
        if ( Ivy_ObjRefs(pObj) == 0 )
            continue;
        assert( !Ivy_IsComplement(pObj) );
        pEval = pEvals + nEvals;
        pEval->pArg   = pObj;
        pEval->Mask   = pEvals[pObj->TravId].Mask;
        pEval->Weight = Extra_WordCountOnes(pEval->Mask);
        // mark the node
        pObj->TravId = nEvals;
        nEvals++;
    }

    // find the available nodes
    nEvalsOld = nEvals;
    for ( i = 1; i < nEvals; i++ )
    for ( k = 0; k < i; k++ )
    {
        pFan0 = pEvals + i;
        pFan1 = pEvals + k;
        pTemp = Ivy_TableLookup(p, Ivy_ObjCreateGhost(p, pFan0->pArg, pFan1->pArg, Type, IVY_INIT_NONE));
        // skip nodes in the cone
        if ( pTemp == NULL || pTemp->fMarkB )
            continue;
        // skip the leaves
        for ( x = 0; x < nLeaves; x++ )
            if ( pTemp == Ivy_Regular((Ivy_Obj_t *)vLeaves->pArray[x]) )
                break;
        if ( x < nLeaves )
            continue;
        pEval = pEvals + nEvals;
        pEval->pArg   = pTemp;
        pEval->Mask   = pFan0->Mask | pFan1->Mask;
        pEval->Weight = (pFan0->Mask & pFan1->Mask) ? Extra_WordCountOnes(pEval->Mask) : pFan0->Weight + pFan1->Weight;
        // save the argument
        pObj->TravId = nEvals;
        nEvals++;
        // quit if the number of entries exceeded the limit
        if ( nEvals == IVY_EVAL_LIMIT )
            goto Outside;
        // quit if we found an acceptable implementation
        if ( pEval->Mask == uMaskAll )
            goto Outside;
    }
Outside:

//    Ivy_MultiPrint( pEvals, nLeaves, nEvals );
    if ( !Ivy_MultiCover( p, pEvals, nLeaves, nEvals, nLimit, vSols ) )
        return 0;
    assert( Vec_PtrSize( vSols ) > 0 );
    return 1;
}

Ivy_Obj_t* Ivy_Mux	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pC,
		Ivy_Obj_t *	p1,
		Ivy_Obj_t *	p0
	)

Function*************************************************************

Synopsis [Implements ITE operation.]

Description []

SideEffects []

SeeAlso []

Definition at line 158 of file ivyOper.c.

{
    Ivy_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp;
    int Count0, Count1;
    // consider trivial cases
    if ( p0 == Ivy_Not(p1) )
        return Ivy_Exor( p, pC, p0 );
    // other cases can be added
    // implement the first MUX (F = C * x1 + C' * x0)
    pTempA1 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pC,          p1, IVY_AND, IVY_INIT_NONE) );
    pTempA2 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pC), p0, IVY_AND, IVY_INIT_NONE) );
    if ( pTempA1 && pTempA2 )
    {
        pTemp = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pTempA1), Ivy_Not(pTempA2), IVY_AND, IVY_INIT_NONE) );
        if ( pTemp ) return Ivy_Not(pTemp);
    }
    Count0 = (pTempA1 != NULL) + (pTempA2 != NULL);
    // implement the second MUX (F' = C * x1' + C' * x0')
    pTempB1 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pC,          Ivy_Not(p1), IVY_AND, IVY_INIT_NONE) );
    pTempB2 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pC), Ivy_Not(p0), IVY_AND, IVY_INIT_NONE) );
    if ( pTempB1 && pTempB2 )
    {
        pTemp = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pTempB1), Ivy_Not(pTempB2), IVY_AND, IVY_INIT_NONE) );
        if ( pTemp ) return pTemp;
    }
    Count1 = (pTempB1 != NULL) + (pTempB2 != NULL);
    // compare and decide which one to implement
    if ( Count0 >= Count1 )
    {
        pTempA1 = pTempA1? pTempA1 : Ivy_And(p, pC,          p1);
        pTempA2 = pTempA2? pTempA2 : Ivy_And(p, Ivy_Not(pC), p0);
        return Ivy_Or( p, pTempA1, pTempA2 );
    }
    pTempB1 = pTempB1? pTempB1 : Ivy_And(p, pC,          Ivy_Not(p1));
    pTempB2 = pTempB2? pTempB2 : Ivy_And(p, Ivy_Not(pC), Ivy_Not(p0));
    return Ivy_Not( Ivy_Or( p, pTempB1, pTempB2 ) );

//    return Ivy_Or( Ivy_And(pC, p1), Ivy_And(Ivy_Not(pC), p0) );
}

Ivy_Obj_t* Ivy_NodeBalanceBuildSuper	(	Ivy_Man_t *	p,
		Vec_Ptr_t *	vSuper,
		Ivy_Type_t	Type,
		int	fUpdateLevel
	)

Function*************************************************************

Synopsis [Builds implication supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 175 of file ivyBalance.c.

{
    Ivy_Obj_t * pObj1, * pObj2;
    int LeftBound;
    assert( vSuper->nSize > 1 );
    // sort the new nodes by level in the decreasing order
    Vec_PtrSort( vSuper, (int (*)(void))Ivy_NodeCompareLevelsDecrease );
    // balance the nodes
    while ( vSuper->nSize > 1 )
    {
        // find the left bound on the node to be paired
        LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vSuper );
        // find the node that can be shared (if no such node, randomize choice)
        Ivy_NodeBalancePermute( p, vSuper, LeftBound, Type == IVY_EXOR );
        // pull out the last two nodes
        pObj1 = (Ivy_Obj_t *)Vec_PtrPop(vSuper);
        pObj2 = (Ivy_Obj_t *)Vec_PtrPop(vSuper);
        Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(p, pObj1, pObj2, Type) );
    }
    return (Ivy_Obj_t *)Vec_PtrEntry(vSuper, 0);
}

Ivy_Store_t* Ivy_NodeFindCutsAll	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj,
		int	nLeaves
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 892 of file ivyCut.c.

{
    static Ivy_Store_t CutStore, * pCutStore = &CutStore;
    Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut;
    Ivy_Obj_t * pLeaf;
    int i, k, iLeaf0, iLeaf1;

    assert( nLeaves <= IVY_CUT_INPUT );

    // start the structure
    pCutStore->nCuts = 0;
    pCutStore->nCutsMax = IVY_CUT_LIMIT;
    // start the trivial cut
    pCutNew->uHash = 0;
    pCutNew->nSize = 1;
    pCutNew->nSizeMax = nLeaves;
    pCutNew->pArray[0] = pObj->Id;
    Ivy_NodeCutHash( pCutNew );
    // add the trivial cut
    Ivy_NodeCutFindOrAdd( pCutStore, pCutNew );
    assert( pCutStore->nCuts == 1 );

    // explore the cuts
    for ( i = 0; i < pCutStore->nCuts; i++ )
    {
        // expand this cut
        pCut = pCutStore->pCuts + i;
        if ( pCut->nSize == 0 )
            continue;
        for ( k = 0; k < pCut->nSize; k++ )
        {
            pLeaf = Ivy_ManObj( p, pCut->pArray[k] );
            if ( Ivy_ObjIsCi(pLeaf) )
                continue;
/*
            *pCutNew = *pCut;
            Ivy_NodeCutShrink( pCutNew, pLeaf->Id );
            if ( !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId0(pLeaf) ) )
                continue;
            if ( Ivy_ObjIsNode(pLeaf) && !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId1(pLeaf) ) )
                continue;
            Ivy_NodeCutHash( pCutNew );
*/
            iLeaf0 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin0(pLeaf)) );
            iLeaf1 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin1(pLeaf)) );
//            if ( iLeaf0 == iLeaf1 ) // strange situation observed on Jan 18, 2007
//                continue;
            if ( !Ivy_NodeCutPrescreen( pCut, iLeaf0, iLeaf1 ) )
                continue;
            if ( iLeaf0 > iLeaf1 )
                Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf1, iLeaf0 );
            else
                Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 );
            Ivy_NodeCutFindOrAddFilter( pCutStore, pCutNew );
            if ( pCutStore->nCuts == IVY_CUT_LIMIT )
                break;
        }
        if ( pCutStore->nCuts == IVY_CUT_LIMIT )
            break;
    }
    Ivy_NodeCompactCuts( pCutStore );
//    Ivy_NodePrintCuts( pCutStore );
    return pCutStore;
}

void Ivy_NodeFixBufferFanins	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pNode,
		int	fUpdateLevel
	)

Function*************************************************************

Synopsis [Fixes buffer fanins.]

Description [This situation happens because NodeReplace is a lazy procedure, which does not propagate the change to the fanouts but instead records the change in the form of a buf/inv node.]

SideEffects []

SeeAlso []

Definition at line 442 of file ivyObj.c.

{
    Ivy_Obj_t * pFanReal0, * pFanReal1, * pResult;
    if ( Ivy_ObjIsPo(pNode) )
    {
        if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) )
            return;
        pFanReal0 = Ivy_ObjReal( Ivy_ObjChild0(pNode) );
        Ivy_ObjPatchFanin0( p, pNode, pFanReal0 );
//        Ivy_ManCheckFanouts( p );
        return;
    }
    if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) && !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) )
        return;
    // get the real fanins
    pFanReal0 = Ivy_ObjReal( Ivy_ObjChild0(pNode) );
    pFanReal1 = Ivy_ObjReal( Ivy_ObjChild1(pNode) );
    // get the new node
    if ( Ivy_ObjIsNode(pNode) )
        pResult = Ivy_Oper( p, pFanReal0, pFanReal1, Ivy_ObjType(pNode) );
    else if ( Ivy_ObjIsLatch(pNode) )
        pResult = Ivy_Latch( p, pFanReal0, Ivy_ObjInit(pNode) );
    else 
        assert( 0 );

//printf( "===== Replacing %d by %d.\n", pNode->Id, pResult->Id );
//Ivy_ObjPrintVerbose( p, pNode, 0 );   printf( "\n" );
//Ivy_ObjPrintVerbose( p, pResult, 0 ); printf( "\n" );

    // perform the replacement
    Ivy_ObjReplace( p, pNode, pResult, 1, 0, fUpdateLevel ); 
}

static Ivy_Obj_t* Ivy_Not ( Ivy_Obj_t *  p )

inlinestatic

Definition at line 194 of file ivy.h.

{ return (Ivy_Obj_t *)((ABC_PTRUINT_T)(p) ^  01); }

static Ivy_Obj_t* Ivy_NotCond ( Ivy_Obj_t *  p, int  c  )

inlinestatic

Definition at line 195 of file ivy.h.

{ return (Ivy_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }

void Ivy_ObjAddFanout	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pFanin,
		Ivy_Obj_t *	pFanout
	)

Function*************************************************************

Synopsis [Add the fanout.]

Description []

SideEffects []

SeeAlso []

Definition at line 183 of file ivyFanout.c.

{
    assert( p->fFanout );
    if ( pFanin->pFanout )
    {
        *Ivy_ObjNextFanoutPlace(pFanin, pFanout) = pFanin->pFanout;
        *Ivy_ObjPrevFanoutPlace(pFanin, pFanin->pFanout) = pFanout;
    }
    pFanin->pFanout = pFanout;
}

static Ivy_Obj_t* Ivy_ObjChild0 ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 273 of file ivy.h.

{ return pObj->pFanin0;                          }

static Ivy_Obj_t* Ivy_ObjChild0Equiv ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 275 of file ivy.h.

{ assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin0(pObj)? Ivy_NotCond(Ivy_ObjFanin0(pObj)->pEquiv, Ivy_ObjFaninC0(pObj)) : NULL;  }

static Ivy_Obj_t* Ivy_ObjChild1 ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 274 of file ivy.h.

{ return pObj->pFanin1;                          }

static Ivy_Obj_t* Ivy_ObjChild1Equiv ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 276 of file ivy.h.

{ assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin1(pObj)? Ivy_NotCond(Ivy_ObjFanin1(pObj)->pEquiv, Ivy_ObjFaninC1(pObj)) : NULL;  }

static void Ivy_ObjClean ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 282 of file ivy.h.

{ 
    int IdSaved = pObj->Id; 
    memset( pObj, 0, sizeof(Ivy_Obj_t) ); 
    pObj->Id = IdSaved; 
}

static void Ivy_ObjClearMarkA ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 252 of file ivy.h.

{ pObj->fMarkA = 0;     }

void Ivy_ObjCollectFanouts	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj,
		Vec_Ptr_t *	vArray
	)

Function*************************************************************

Synopsis [Starts iteration through the fanouts.]

Description [Copies the currently available fanouts into the array.]

SideEffects [Can be used while the fanouts are being removed.]

SeeAlso []

Definition at line 262 of file ivyFanout.c.

{
    Ivy_Obj_t * pFanout;
    assert( p->fFanout );
    assert( !Ivy_IsComplement(pObj) );
    Vec_PtrClear( vArray );
    Ivy_ObjForEachFanoutInt( pObj, pFanout )
        Vec_PtrPush( vArray, pFanout );
}

void Ivy_ObjConnect	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj,
		Ivy_Obj_t *	pFan0,
		Ivy_Obj_t *	pFan1
	)

Function*************************************************************

Synopsis [Connect the object to the fanin.]

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file ivyObj.c.

{
    assert( !Ivy_IsComplement(pObj) );
    assert( Ivy_ObjIsPi(pObj) || Ivy_ObjIsOneFanin(pObj) || pFan1 != NULL );
    // add the first fanin
    pObj->pFanin0 = pFan0;
    pObj->pFanin1 = pFan1;
    // increment references of the fanins and add their fanouts
    if ( Ivy_ObjFanin0(pObj) != NULL )
    {
        Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) );
        if ( p->fFanout )
            Ivy_ObjAddFanout( p, Ivy_ObjFanin0(pObj), pObj );
    }
    if ( Ivy_ObjFanin1(pObj) != NULL )
    {
        Ivy_ObjRefsInc( Ivy_ObjFanin1(pObj) );
        if ( p->fFanout )
            Ivy_ObjAddFanout( p, Ivy_ObjFanin1(pObj), pObj );
    }
    // add the node to the structural hash table
    Ivy_TableInsert( p, pObj );
}

Ivy_Obj_t* Ivy_ObjCreate	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pGhost
	)

Function*************************************************************

Synopsis [Create the new node assuming it does not exist.]

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file ivyObj.c.

{
    Ivy_Obj_t * pObj;
    assert( !Ivy_IsComplement(pGhost) );
    assert( Ivy_ObjIsGhost(pGhost) );
    assert( Ivy_TableLookup(p, pGhost) == NULL );
    // get memory for the new object
    pObj = Ivy_ManFetchMemory( p );
    assert( Ivy_ObjIsNone(pObj) );
    pObj->Id = Vec_PtrSize(p->vObjs);
    Vec_PtrPush( p->vObjs, pObj );
    // add basic info (fanins, compls, type, init)
    pObj->Type = pGhost->Type;
    pObj->Init = pGhost->Init;
    // add connections
    Ivy_ObjConnect( p, pObj, pGhost->pFanin0, pGhost->pFanin1 );
    // compute level
    if ( Ivy_ObjIsNode(pObj) )
        pObj->Level = Ivy_ObjLevelNew(pObj);
    else if ( Ivy_ObjIsLatch(pObj) )
        pObj->Level = 0;
    else if ( Ivy_ObjIsOneFanin(pObj) )
        pObj->Level = Ivy_ObjFanin0(pObj)->Level;
    else if ( !Ivy_ObjIsPi(pObj) )
        assert( 0 );
    // create phase
    if ( Ivy_ObjIsNode(pObj) )
        pObj->fPhase = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) & Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj));
    else if ( Ivy_ObjIsOneFanin(pObj) )
        pObj->fPhase = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj));
    // set the fail TFO flag
    if ( Ivy_ObjIsNode(pObj) )
        pObj->fFailTfo = Ivy_ObjFanin0(pObj)->fFailTfo | Ivy_ObjFanin1(pObj)->fFailTfo;
    // mark the fanins in a special way if the node is EXOR
    if ( Ivy_ObjIsExor(pObj) )
    {
        Ivy_ObjFanin0(pObj)->fExFan = 1;
        Ivy_ObjFanin1(pObj)->fExFan = 1;
    }
    // add PIs/POs to the arrays
    if ( Ivy_ObjIsPi(pObj) )
        Vec_PtrPush( p->vPis, pObj );
    else if ( Ivy_ObjIsPo(pObj) )
        Vec_PtrPush( p->vPos, pObj );
//    else if ( Ivy_ObjIsBuf(pObj) )
//        Vec_PtrPush( p->vBufs, pObj );
    if ( p->vRequired && Vec_IntSize(p->vRequired) <= pObj->Id )
        Vec_IntFillExtra( p->vRequired, 2 * Vec_IntSize(p->vRequired), 1000000 );
    // update node counters of the manager
    p->nObjs[Ivy_ObjType(pObj)]++;
    p->nCreated++;

//    printf( "Adding %sAIG node: ", p->pHaig==NULL? "H":" " );
//    Ivy_ObjPrintVerbose( p, pObj, p->pHaig==NULL );
//    printf( "\n" );

    // if HAIG is defined, create a corresponding node
    if ( p->pHaig )
        Ivy_ManHaigCreateObj( p, pObj );
    return pObj;
}

static Ivy_Obj_t* Ivy_ObjCreateGhost ( Ivy_Man_t *  p, Ivy_Obj_t *  p0, Ivy_Obj_t *  p1, Ivy_Type_t  Type, Ivy_Init_t  Init  )

inlinestatic

Definition at line 308 of file ivy.h.

{
    Ivy_Obj_t * pGhost, * pTemp;
    assert( Type != IVY_AND || !Ivy_ObjIsConst1(Ivy_Regular(p0)) );
    assert( p1 == NULL || !Ivy_ObjIsConst1(Ivy_Regular(p1)) );
    assert( Type == IVY_PI || Ivy_Regular(p0) != Ivy_Regular(p1) );
    assert( Type != IVY_LATCH || !Ivy_IsComplement(p0) );
//    assert( p1 == NULL || (!Ivy_ObjIsLatch(Ivy_Regular(p0)) || !Ivy_ObjIsLatch(Ivy_Regular(p1))) );
    pGhost = Ivy_ManGhost(p);
    pGhost->Type = Type;
    pGhost->Init = Init;
    pGhost->pFanin0 = p0;
    pGhost->pFanin1 = p1;
    if ( p1 && Ivy_ObjFaninId0(pGhost) > Ivy_ObjFaninId1(pGhost) )
        pTemp = pGhost->pFanin0, pGhost->pFanin0 = pGhost->pFanin1, pGhost->pFanin1 = pTemp;
    return pGhost;
}

Ivy_Obj_t* Ivy_ObjCreatePi

(

Ivy_Man_t *

p

)

DECLARATIONS ///.

CFile****************************************************************

FileName [ivyObj.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [Adding/removing objects.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id:

ivyObj.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Create the new node assuming it does not exist.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file ivyObj.c.

{
    return Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, NULL, NULL, IVY_PI, IVY_INIT_NONE) );
}

Ivy_Obj_t* Ivy_ObjCreatePo	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pDriver
	)

Function*************************************************************

Synopsis [Create the new node assuming it does not exist.]

Description []

SideEffects []

SeeAlso []

Definition at line 61 of file ivyObj.c.

{
    return Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pDriver, NULL, IVY_PO, IVY_INIT_NONE) );
}

void Ivy_ObjDelete	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj,
		int	fFreeTop
	)

Function*************************************************************

Synopsis [Deletes the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 255 of file ivyObj.c.

{
    assert( !Ivy_IsComplement(pObj) );
    assert( Ivy_ObjRefs(pObj) == 0 || !fFreeTop );
    // update node counters of the manager
    p->nObjs[pObj->Type]--;
    p->nDeleted++;
    // remove connections
    Ivy_ObjDisconnect( p, pObj );
    // remove PIs/POs from the arrays
    if ( Ivy_ObjIsPi(pObj) )
        Vec_PtrRemove( p->vPis, pObj );
    else if ( Ivy_ObjIsPo(pObj) )
        Vec_PtrRemove( p->vPos, pObj );
    else if ( p->fFanout && Ivy_ObjIsBuf(pObj) )
        Vec_PtrRemove( p->vBufs, pObj );
    // clean and recycle the entry
    if ( fFreeTop )
    {
        // free the node
        Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
        Ivy_ManRecycleMemory( p, pObj );
    }
    else
    {
        int nRefsOld = pObj->nRefs;
        Ivy_Obj_t * pFanout = pObj->pFanout;
        Ivy_ObjClean( pObj );
        pObj->pFanout = pFanout;
        pObj->nRefs = nRefsOld;
    }
}

void Ivy_ObjDelete_rec	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj,
		int	fFreeTop
	)

Function*************************************************************

Synopsis [Deletes the MFFC of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 299 of file ivyObj.c.

{
    Ivy_Obj_t * pFanin0, * pFanin1;
    assert( !Ivy_IsComplement(pObj) );
    assert( !Ivy_ObjIsNone(pObj) );
    if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsPi(pObj) )
        return;
    pFanin0 = Ivy_ObjFanin0(pObj);
    pFanin1 = Ivy_ObjFanin1(pObj);
    Ivy_ObjDelete( p, pObj, fFreeTop );
    if ( pFanin0 && !Ivy_ObjIsNone(pFanin0) && Ivy_ObjRefs(pFanin0) == 0 )
        Ivy_ObjDelete_rec( p, pFanin0, 1 );
    if ( pFanin1 && !Ivy_ObjIsNone(pFanin1) && Ivy_ObjRefs(pFanin1) == 0 )
        Ivy_ObjDelete_rec( p, pFanin1, 1 );
}

void Ivy_ObjDeleteFanout	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pFanin,
		Ivy_Obj_t *	pFanout
	)

Function*************************************************************

Synopsis [Removes the fanout.]

Description []

SideEffects []

SeeAlso []

Definition at line 205 of file ivyFanout.c.

{
    Ivy_Obj_t ** ppPlace1, ** ppPlace2, ** ppPlaceN;
    assert( pFanin->pFanout != NULL );

    ppPlace1 = Ivy_ObjNextFanoutPlace(pFanin, pFanout);
    ppPlaceN = Ivy_ObjPrevNextFanoutPlace(pFanin, pFanout);
    assert( *ppPlaceN == pFanout );
    if ( ppPlaceN )
        *ppPlaceN = *ppPlace1;

    ppPlace2 = Ivy_ObjPrevFanoutPlace(pFanin, pFanout);
    ppPlaceN = Ivy_ObjNextPrevFanoutPlace(pFanin, pFanout);
    assert( ppPlaceN == NULL || *ppPlaceN == pFanout );
    if ( ppPlaceN )
        *ppPlaceN = *ppPlace2;

    *ppPlace1 = NULL;
    *ppPlace2 = NULL;
}

void Ivy_ObjDisconnect	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj
	)

Function*************************************************************

Synopsis [Connect the object to the fanin.]

Description []

SideEffects []

SeeAlso []

Definition at line 185 of file ivyObj.c.

{
    assert( !Ivy_IsComplement(pObj) );
    assert( Ivy_ObjIsPi(pObj) || Ivy_ObjIsOneFanin(pObj) || Ivy_ObjFanin1(pObj) != NULL );
    // remove connections
    if ( pObj->pFanin0 != NULL )
    {
        Ivy_ObjRefsDec(Ivy_ObjFanin0(pObj));
        if ( p->fFanout )
            Ivy_ObjDeleteFanout( p, Ivy_ObjFanin0(pObj), pObj );
    }
    if ( pObj->pFanin1 != NULL )
    {
        Ivy_ObjRefsDec(Ivy_ObjFanin1(pObj));
        if ( p->fFanout )
            Ivy_ObjDeleteFanout( p, Ivy_ObjFanin1(pObj), pObj );
    }
    assert( pObj->pNextFan0 == NULL );
    assert( pObj->pNextFan1 == NULL );
    assert( pObj->pPrevFan0 == NULL );
    assert( pObj->pPrevFan1 == NULL );
    // remove the node from the structural hash table
    Ivy_TableDelete( p, pObj );
    // add the first fanin
    pObj->pFanin0 = NULL;
    pObj->pFanin1 = NULL;
}

static Ivy_Obj_t* Ivy_ObjEquiv ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 277 of file ivy.h.

{ return Ivy_Regular(pObj)->pEquiv? Ivy_NotCond(Ivy_Regular(pObj)->pEquiv, Ivy_IsComplement(pObj)) : NULL; }

static int Ivy_ObjExorFanout ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 263 of file ivy.h.

{ return pObj->fExFan;                           }

static Ivy_Obj_t* Ivy_ObjFanin0 ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 271 of file ivy.h.

{ return Ivy_Regular(pObj->pFanin0);             }

static Ivy_Obj_t* Ivy_ObjFanin1 ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 272 of file ivy.h.

{ return Ivy_Regular(pObj->pFanin1);             }

static int Ivy_ObjFaninC0 ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 269 of file ivy.h.

{ return Ivy_IsComplement(pObj->pFanin0);        }

static int Ivy_ObjFaninC1 ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 270 of file ivy.h.

{ return Ivy_IsComplement(pObj->pFanin1);        }

static int Ivy_ObjFaninId0 ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 267 of file ivy.h.

{ return pObj->pFanin0? Ivy_ObjId(Ivy_Regular(pObj->pFanin0)) : 0; }

static int Ivy_ObjFaninId1 ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 268 of file ivy.h.

{ return pObj->pFanin1? Ivy_ObjId(Ivy_Regular(pObj->pFanin1)) : 0; }

static int Ivy_ObjFaninPhase ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 280 of file ivy.h.

{ return Ivy_IsComplement(pObj)? !Ivy_Regular(pObj)->fPhase : pObj->fPhase; }

static int Ivy_ObjFanoutC ( Ivy_Obj_t *  pObj, Ivy_Obj_t *  pFanout  )

inlinestatic

Definition at line 300 of file ivy.h.

{ 
    if ( Ivy_ObjFanin0(pFanout) == pObj ) return Ivy_ObjFaninC0(pObj); 
    if ( Ivy_ObjFanin1(pFanout) == pObj ) return Ivy_ObjFaninC1(pObj); 
    assert(0); return -1; 
}

int Ivy_ObjFanoutNum	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj
	)

Function*************************************************************

Synopsis [Reads one fanout.]

Description [Returns fanout if there is only one fanout.]

SideEffects []

SeeAlso []

Definition at line 299 of file ivyFanout.c.

{
    Ivy_Obj_t * pFanout;
    int Counter = 0;
    Ivy_ObjForEachFanoutInt( pObj, pFanout )
        Counter++;
    return Counter;
}

static int Ivy_ObjId ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 260 of file ivy.h.

{ return pObj->Id;                               }

static Ivy_Init_t Ivy_ObjInit ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 232 of file ivy.h.

{ return (Ivy_Init_t)pObj->Init;               }

static int Ivy_ObjIsAnd ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 242 of file ivy.h.

{ return pObj->Type == IVY_AND;    }

static int Ivy_ObjIsAssert ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 240 of file ivy.h.

{ return pObj->Type == IVY_ASSERT; }

static int Ivy_ObjIsBuf ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 244 of file ivy.h.

{ return pObj->Type == IVY_BUF;    }

static int Ivy_ObjIsCi ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 238 of file ivy.h.

{ return pObj->Type == IVY_PI || pObj->Type == IVY_LATCH; }

static int Ivy_ObjIsCo ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 239 of file ivy.h.

{ return pObj->Type == IVY_PO || pObj->Type == IVY_LATCH; }

static int Ivy_ObjIsConst1 ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 233 of file ivy.h.

{ return pObj->Id == 0;            }

static int Ivy_ObjIsExor ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 243 of file ivy.h.

{ return pObj->Type == IVY_EXOR;   }

static int Ivy_ObjIsGhost ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 234 of file ivy.h.

{ return pObj->Id < 0;             }

static int Ivy_ObjIsHash ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 247 of file ivy.h.

{ return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR || pObj->Type == IVY_LATCH; }

static int Ivy_ObjIsLatch ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 241 of file ivy.h.

{ return pObj->Type == IVY_LATCH;  }

static int Ivy_ObjIsMarkA ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 250 of file ivy.h.

{ return pObj->fMarkA;  }

int Ivy_ObjIsMuxType

(

Ivy_Obj_t *

pNode

)

Function*************************************************************

Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]

Description []

SideEffects []

SeeAlso []

Definition at line 479 of file ivyUtil.c.

{
    Ivy_Obj_t * pNode0, * pNode1;
    // check that the node is regular
    assert( !Ivy_IsComplement(pNode) );
    // if the node is not AND, this is not MUX
    if ( !Ivy_ObjIsAnd(pNode) )
        return 0;
    // if the children are not complemented, this is not MUX
    if ( !Ivy_ObjFaninC0(pNode) || !Ivy_ObjFaninC1(pNode) )
        return 0;
    // get children
    pNode0 = Ivy_ObjFanin0(pNode);
    pNode1 = Ivy_ObjFanin1(pNode);
    // if the children are not ANDs, this is not MUX
    if ( !Ivy_ObjIsAnd(pNode0) || !Ivy_ObjIsAnd(pNode1) )
        return 0;
    // otherwise the node is MUX iff it has a pair of equal grandchildren
    return (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || 
           (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1))) ||
           (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1))) ||
           (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)));
}

static int Ivy_ObjIsNode ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 245 of file ivy.h.

{ return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR; }

static int Ivy_ObjIsNone ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 235 of file ivy.h.

{ return pObj->Type == IVY_NONE;   }

static int Ivy_ObjIsOneFanin ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 248 of file ivy.h.

{ return pObj->Type == IVY_PO  || pObj->Type == IVY_ASSERT || pObj->Type == IVY_BUF || pObj->Type == IVY_LATCH; }

static int Ivy_ObjIsPi ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 236 of file ivy.h.

{ return pObj->Type == IVY_PI;     }

static int Ivy_ObjIsPo ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 237 of file ivy.h.

{ return pObj->Type == IVY_PO;     }

static int Ivy_ObjIsTerm ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 246 of file ivy.h.

{ return pObj->Type == IVY_PI  || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; }

static int Ivy_ObjIsTravIdCurrent ( Ivy_Man_t *  p, Ivy_Obj_t *  pObj  )

inlinestatic

Definition at line 257 of file ivy.h.

{ return (int )((int)pObj->TravId == p->nTravIds);     }

static int Ivy_ObjIsTravIdPrevious ( Ivy_Man_t *  p, Ivy_Obj_t *  pObj  )

inlinestatic

Definition at line 258 of file ivy.h.

{ return (int )((int)pObj->TravId == p->nTravIds - 1); }

static int Ivy_ObjLevel ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 278 of file ivy.h.

{ return pObj->Level;                            }

static int Ivy_ObjLevelNew ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 279 of file ivy.h.

{ return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level);       }

int Ivy_ObjMffcLabel	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pNode
	)

Function*************************************************************

Synopsis [Labels MFFC with the current label.]

Description []

SideEffects []

SeeAlso []

Definition at line 359 of file ivyUtil.c.

{
    int nConeSize1, nConeSize2;
    assert( !Ivy_IsComplement( pNode ) );
    assert( Ivy_ObjIsNode( pNode ) );
    nConeSize1 = Ivy_ObjRefDeref( p, pNode, 0, 1 ); // dereference
    nConeSize2 = Ivy_ObjRefDeref( p, pNode, 1, 0 ); // reference
    assert( nConeSize1 == nConeSize2 );
    assert( nConeSize1 > 0 );
    return nConeSize1;
}

static void Ivy_ObjOverwrite ( Ivy_Obj_t *  pBase, Ivy_Obj_t *  pData  )

inlinestatic

Definition at line 288 of file ivy.h.

{ 
    int IdSaved = pBase->Id; 
    memcpy( pBase, pData, sizeof(Ivy_Obj_t) ); 
    pBase->Id = IdSaved;         
}

void Ivy_ObjPatchFanin0	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj,
		Ivy_Obj_t *	pFaninNew
	)

Function*************************************************************

Synopsis [Replaces the first fanin of the node by the new fanin.]

Description []

SideEffects []

SeeAlso []

Definition at line 224 of file ivyObj.c.

{
    Ivy_Obj_t * pFaninOld;
    assert( !Ivy_IsComplement(pObj) );
    pFaninOld = Ivy_ObjFanin0(pObj);
    // decrement ref and remove fanout
    Ivy_ObjRefsDec( pFaninOld );
    if ( p->fFanout )
        Ivy_ObjDeleteFanout( p, pFaninOld, pObj );
    // update the fanin
    pObj->pFanin0 = pFaninNew;
    // increment ref and add fanout
    Ivy_ObjRefsInc( Ivy_Regular(pFaninNew) );
    if ( p->fFanout )
        Ivy_ObjAddFanout( p, Ivy_Regular(pFaninNew), pObj );
    // get rid of old fanin
    if ( !Ivy_ObjIsPi(pFaninOld) && !Ivy_ObjIsConst1(pFaninOld) && Ivy_ObjRefs(pFaninOld) == 0 )
        Ivy_ObjDelete_rec( p, pFaninOld, 1 );
}

void Ivy_ObjPatchFanout	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pFanin,
		Ivy_Obj_t *	pFanoutOld,
		Ivy_Obj_t *	pFanoutNew
	)

Function*************************************************************

Synopsis [Replaces the fanout of pOld to be pFanoutNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 237 of file ivyFanout.c.

{
    Ivy_Obj_t ** ppPlace;
    ppPlace = Ivy_ObjPrevNextFanoutPlace(pFanin, pFanoutOld);
    assert( *ppPlace == pFanoutOld );
    if ( ppPlace )
        *ppPlace = pFanoutNew;
    ppPlace = Ivy_ObjNextPrevFanoutPlace(pFanin, pFanoutOld);
    assert( ppPlace == NULL || *ppPlace == pFanoutOld );
    if ( ppPlace )
        *ppPlace = pFanoutNew;
    // assuming that pFanoutNew already points to the next fanout
}

static int Ivy_ObjPhase ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 262 of file ivy.h.

{ return pObj->fPhase;                           }

void Ivy_ObjPrintVerbose	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj,
		int	fHaig
	)

Function*************************************************************

Synopsis [Prints node in HAIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 629 of file ivyUtil.c.

{
    Ivy_Obj_t * pTemp;
    int fShowFanouts = 0;
    assert( !Ivy_IsComplement(pObj) );
    printf( "Node %5d : ", Ivy_ObjId(pObj) );
    if ( Ivy_ObjIsConst1(pObj) )
        printf( "constant 1" );
    else if ( Ivy_ObjIsPi(pObj) )
        printf( "PI" );
    else if ( Ivy_ObjIsPo(pObj) )
        printf( "PO" );
    else if ( Ivy_ObjIsLatch(pObj) )
        printf( "latch (%d%s)", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
    else if ( Ivy_ObjIsBuf(pObj) )
        printf( "buffer (%d%s)", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") );
    else
        printf( "AND( %5d%s, %5d%s )", 
            Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " "), 
            Ivy_ObjFanin1(pObj)->Id, (Ivy_ObjFaninC1(pObj)? "\'" : " ") );
    printf( " (refs = %3d)", Ivy_ObjRefs(pObj) );
    if ( fShowFanouts )
    {
        Vec_Ptr_t * vFanouts;
        Ivy_Obj_t * pFanout;
        int i;
        vFanouts = Vec_PtrAlloc( 10 );
        printf( "\nFanouts:\n" );
        Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
        {
            printf( "    " );
            printf( "Node %5d : ", Ivy_ObjId(pFanout) );
            if ( Ivy_ObjIsPo(pFanout) )
                printf( "PO" );
            else if ( Ivy_ObjIsLatch(pFanout) )
                printf( "latch (%d%s)", Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " ") );
            else if ( Ivy_ObjIsBuf(pFanout) )
                printf( "buffer (%d%s)", Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " ") );
            else
                printf( "AND( %5d%s, %5d%s )", 
                    Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " "), 
                    Ivy_ObjFanin1(pFanout)->Id, (Ivy_ObjFaninC1(pFanout)? "\'" : " ") );
            printf( "\n" );
        }
        Vec_PtrFree( vFanouts );
        return;
    }
    if ( !fHaig )
    {
        if ( pObj->pEquiv == NULL )
            printf( " HAIG node not given" );
        else
            printf( " HAIG node = %d%s", Ivy_Regular(pObj->pEquiv)->Id, (Ivy_IsComplement(pObj->pEquiv)? "\'" : " ") );
        return;
    }
    if ( pObj->pEquiv == NULL )
        return;
    // there are choices
    if ( Ivy_ObjRefs(pObj) > 0 )
    {
        // print equivalence class
        printf( "  { %5d ", pObj->Id );
        assert( !Ivy_IsComplement(pObj->pEquiv) );
        for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
            printf( " %5d%s", pTemp->Id, (Ivy_IsComplement(pTemp->pEquiv)? "\'" : " ") );
        printf( " }" );
        return;
    }
    // this is a secondary node
    for ( pTemp = Ivy_Regular(pObj->pEquiv); Ivy_ObjRefs(pTemp) == 0; pTemp = Ivy_Regular(pTemp->pEquiv) );
    assert( Ivy_ObjRefs(pTemp) > 0 );
    printf( "  class of %d", pTemp->Id );
}

Ivy_Obj_t* Ivy_ObjReadFirstFanout	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj
	)

Function*************************************************************

Synopsis [Reads one fanout.]

Description [Returns fanout if there is only one fanout.]

SideEffects []

SeeAlso []

Definition at line 283 of file ivyFanout.c.

{
    return pObj->pFanout;
}

Ivy_Obj_t* Ivy_ObjReal

(

Ivy_Obj_t *

pObj

)

Function*************************************************************

Synopsis [Returns the real fanin.]

Description []

SideEffects []

SeeAlso []

Definition at line 609 of file ivyUtil.c.

{
    Ivy_Obj_t * pFanin;
    if ( pObj == NULL || !Ivy_ObjIsBuf( Ivy_Regular(pObj) ) )
        return pObj;
    pFanin = Ivy_ObjReal( Ivy_ObjChild0(Ivy_Regular(pObj)) );
    return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) );
}

Ivy_Obj_t* Ivy_ObjRecognizeMux	(	Ivy_Obj_t *	pNode,
		Ivy_Obj_t **	ppNodeT,
		Ivy_Obj_t **	ppNodeE
	)

Function*************************************************************

Synopsis [Recognizes what nodes are control and data inputs of a MUX.]

Description [If the node is a MUX, returns the control variable C. Assigns nodes T and E to be the then and else variables of the MUX. Node C is never complemented. Nodes T and E can be complemented. This function also recognizes EXOR/NEXOR gates as MUXes.]

SideEffects []

SeeAlso []

Definition at line 517 of file ivyUtil.c.

{
    Ivy_Obj_t * pNode0, * pNode1;
    assert( !Ivy_IsComplement(pNode) );
    assert( Ivy_ObjIsMuxType(pNode) );
    // get children
    pNode0 = Ivy_ObjFanin0(pNode);
    pNode1 = Ivy_ObjFanin1(pNode);
    // find the control variable
//    if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
    if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
    {
//        if ( Fraig_IsComplement(pNode1->p1) )
        if ( Ivy_ObjFaninC0(pNode0) )
        { // pNode2->p1 is positive phase of C
            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
            return Ivy_ObjChild0(pNode1);//pNode2->p1;
        }
        else
        { // pNode1->p1 is positive phase of C
            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
            return Ivy_ObjChild0(pNode0);//pNode1->p1;
        }
    }
//    else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
    else if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
    {
//        if ( Fraig_IsComplement(pNode1->p1) )
        if ( Ivy_ObjFaninC0(pNode0) )
        { // pNode2->p2 is positive phase of C
            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
            return Ivy_ObjChild1(pNode1);//pNode2->p2;
        }
        else
        { // pNode1->p1 is positive phase of C
            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
            return Ivy_ObjChild0(pNode0);//pNode1->p1;
        }
    }
//    else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
    else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
    {
//        if ( Fraig_IsComplement(pNode1->p2) )
        if ( Ivy_ObjFaninC1(pNode0) )
        { // pNode2->p1 is positive phase of C
            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
            return Ivy_ObjChild0(pNode1);//pNode2->p1;
        }
        else
        { // pNode1->p2 is positive phase of C
            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
            return Ivy_ObjChild1(pNode0);//pNode1->p2;
        }
    }
//    else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
    else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
    {
//        if ( Fraig_IsComplement(pNode1->p2) )
        if ( Ivy_ObjFaninC1(pNode0) )
        { // pNode2->p2 is positive phase of C
            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
            return Ivy_ObjChild1(pNode1);//pNode2->p2;
        }
        else
        { // pNode1->p2 is positive phase of C
            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
            return Ivy_ObjChild1(pNode0);//pNode1->p2;
        }
    }
    assert( 0 ); // this is not MUX
    return NULL;
}

static int Ivy_ObjRefs ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 264 of file ivy.h.

{ return pObj->nRefs;                            }

static void Ivy_ObjRefsDec ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 266 of file ivy.h.

{ assert( pObj->nRefs > 0 ); pObj->nRefs--;      }

static void Ivy_ObjRefsInc ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 265 of file ivy.h.

{ pObj->nRefs++;                                 }

void Ivy_ObjReplace	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObjOld,
		Ivy_Obj_t *	pObjNew,
		int	fDeleteOld,
		int	fFreeTop,
		int	fUpdateLevel
	)

Function*************************************************************

Synopsis [Replaces one object by another.]

Description [Both objects are currently in the manager. The new object (pObjNew) should be used instead of the old object (pObjOld). If the new object is complemented or used, the buffer is added.]

SideEffects []

SeeAlso []

Definition at line 328 of file ivyObj.c.

{
    int nRefsOld;//, clk;
    // the object to be replaced cannot be complemented
    assert( !Ivy_IsComplement(pObjOld) );
    // the object to be replaced cannot be a terminal
    assert( Ivy_ObjIsNone(pObjOld) || !Ivy_ObjIsPi(pObjOld) );
    // the object to be used cannot be a PO or assert
    assert( !Ivy_ObjIsBuf(Ivy_Regular(pObjNew)) );
    // the object cannot be the same
    assert( pObjOld != Ivy_Regular(pObjNew) );
//printf( "Replacing %d by %d.\n", Ivy_Regular(pObjOld)->Id, Ivy_Regular(pObjNew)->Id );

    // if HAIG is defined, create the choice node
    if ( p->pHaig )
    {
//        if ( pObjOld->Id == 31 )
//        {
//            Ivy_ManShow( p, 0 );
//            Ivy_ManShow( p->pHaig, 1 );
//        }
        Ivy_ManHaigCreateChoice( p, pObjOld, pObjNew );
    }
    // if the new object is complemented or already used, add the buffer
    if ( Ivy_IsComplement(pObjNew) || Ivy_ObjIsLatch(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
        pObjNew = Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pObjNew, NULL, IVY_BUF, IVY_INIT_NONE) );
    assert( !Ivy_IsComplement(pObjNew) );
    if ( fUpdateLevel )
    {
//clk = Abc_Clock();
        // if the new node's arrival time is different, recursively update arrival time of the fanouts
        if ( p->fFanout && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level )
        {
            assert( Ivy_ObjIsNode(pObjOld) );
            pObjOld->Level = pObjNew->Level;
            Ivy_ObjUpdateLevel_rec( p, pObjOld );
        }
//p->time1 += Abc_Clock() - clk;
        // if the new node's required time has changed, recursively update required time of the fanins
//clk = Abc_Clock();
        if ( p->vRequired )
        {
            int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id);
            if ( ReqNew < Vec_IntEntry(p->vRequired, pObjNew->Id) )
            {
                Vec_IntWriteEntry( p->vRequired, pObjNew->Id, ReqNew );
                Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew );
            }
        }
//p->time2 += Abc_Clock() - clk;
    }
    // delete the old object
    if ( fDeleteOld )
        Ivy_ObjDelete_rec( p, pObjOld, fFreeTop );
    // make sure object is not pointing to itself
    assert( Ivy_ObjFanin0(pObjNew) == NULL || pObjOld != Ivy_ObjFanin0(pObjNew) );
    assert( Ivy_ObjFanin1(pObjNew) == NULL || pObjOld != Ivy_ObjFanin1(pObjNew) );
    // make sure the old node has no fanin fanout pointers
    if ( p->fFanout )
    {
        assert( pObjOld->pFanout != NULL );
        assert( pObjNew->pFanout == NULL );
        pObjNew->pFanout = pObjOld->pFanout;
    }
    // transfer the old object
    assert( Ivy_ObjRefs(pObjNew) == 0 );
    nRefsOld = pObjOld->nRefs;  
    Ivy_ObjOverwrite( pObjOld, pObjNew );
    pObjOld->nRefs = nRefsOld;
    // patch the fanout of the fanins 
    if ( p->fFanout )
    {
        Ivy_ObjPatchFanout( p, Ivy_ObjFanin0(pObjOld), pObjNew, pObjOld );
        if ( Ivy_ObjFanin1(pObjOld) )
        Ivy_ObjPatchFanout( p, Ivy_ObjFanin1(pObjOld), pObjNew, pObjOld );
    }
    // update the hash table
    Ivy_TableUpdate( p, pObjNew, pObjOld->Id );
    // recycle the object that was taken over by pObjOld
    Vec_PtrWriteEntry( p->vObjs, pObjNew->Id, NULL );
    Ivy_ManRecycleMemory( p, pObjNew );
    // if the new node is the buffer propagate it
    if ( p->fFanout && Ivy_ObjIsBuf(pObjOld) )
        Vec_PtrPush( p->vBufs, pObjOld );
//    Ivy_ManCheckFanouts( p );
//    printf( "\n" );
/*
    if ( p->pHaig )
    {
        int x;
        Ivy_ManShow( p, 0, NULL );
        Ivy_ManShow( p->pHaig, 1, NULL );
        x = 0;
    }
*/
//    if ( Ivy_ManCheckFanoutNums(p) )
//    {
//        int x = 0;
//    }
}

static void Ivy_ObjSetMarkA ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 251 of file ivy.h.

{ pObj->fMarkA = 1;     }

static void Ivy_ObjSetTravId ( Ivy_Obj_t *  pObj, int  TravId  )

inlinestatic

Definition at line 254 of file ivy.h.

{ pObj->TravId = TravId;                               }

static void Ivy_ObjSetTravIdCurrent ( Ivy_Man_t *  p, Ivy_Obj_t *  pObj  )

inlinestatic

Definition at line 255 of file ivy.h.

{ pObj->TravId = p->nTravIds;                          }

static void Ivy_ObjSetTravIdPrevious ( Ivy_Man_t *  p, Ivy_Obj_t *  pObj  )

inlinestatic

Definition at line 256 of file ivy.h.

{ pObj->TravId = p->nTravIds - 1;                      }

static int Ivy_ObjTravId ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 261 of file ivy.h.

{ return pObj->TravId;                           }

static Ivy_Type_t Ivy_ObjType ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 231 of file ivy.h.

{ return (Ivy_Type_t)pObj->Type;               }

void Ivy_ObjUpdateLevel_rec	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj
	)

Function*************************************************************

Synopsis [Recursively updates fanout levels.]

Description []

SideEffects []

SeeAlso []

Definition at line 382 of file ivyUtil.c.

{
    Ivy_Obj_t * pFanout;
    Vec_Ptr_t * vFanouts;
    int i, LevelNew;
    assert( p->fFanout );
    assert( Ivy_ObjIsNode(pObj) );
    vFanouts = Vec_PtrAlloc( 10 );
    Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
    {
        if ( Ivy_ObjIsCo(pFanout) )
        {
//            assert( (int)Ivy_ObjFanin0(pFanout)->Level <= p->nLevelMax );
            continue;
        }
        LevelNew = Ivy_ObjLevelNew( pFanout );
        if ( (int)pFanout->Level == LevelNew )
            continue;
        pFanout->Level = LevelNew;
        Ivy_ObjUpdateLevel_rec( p, pFanout );
    }
    Vec_PtrFree( vFanouts );
}

void Ivy_ObjUpdateLevelR_rec	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj,
		int	ReqNew
	)

Function*************************************************************

Synopsis [Recursively updates fanout levels.]

Description []

SideEffects []

SeeAlso []

Definition at line 444 of file ivyUtil.c.

{
    Ivy_Obj_t * pFanin;
    if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
        return;
    assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
    // process the first fanin
    pFanin = Ivy_ObjFanin0(pObj);
    if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 )
    {
        Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 );
        Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 );
    }
    if ( Ivy_ObjIsBuf(pObj) )
        return;
    // process the second fanin
    pFanin = Ivy_ObjFanin1(pObj);
    if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 )
    {
        Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 );
        Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 );
    }
}

static int Ivy_ObjWhatFanin ( Ivy_Obj_t *  pObj, Ivy_Obj_t *  pFanin  )

inlinestatic

Definition at line 294 of file ivy.h.

{ 
    if ( Ivy_ObjFanin0(pObj) == pFanin ) return 0; 
    if ( Ivy_ObjFanin1(pObj) == pFanin ) return 1; 
    assert(0); return -1; 
}

Ivy_Obj_t* Ivy_Oper	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	p0,
		Ivy_Obj_t *	p1,
		Ivy_Type_t	Type
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Perform one operation.]

Description [The argument nodes can be complemented.]

SideEffects []

SeeAlso []

Definition at line 63 of file ivyOper.c.

{
    if ( Type == IVY_AND )
        return Ivy_And( p, p0, p1 );
    if ( Type == IVY_EXOR )
        return Ivy_Exor( p, p0, p1 );
    assert( 0 );
    return NULL;
}

Ivy_Obj_t* Ivy_Or	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	p0,
		Ivy_Obj_t *	p1
	)

Function*************************************************************

Synopsis [Implements Boolean OR.]

Description []

SideEffects []

SeeAlso []

Definition at line 142 of file ivyOper.c.

{
    return Ivy_Not( Ivy_And( p, Ivy_Not(p0), Ivy_Not(p1) ) );
}

static Ivy_Obj_t* Ivy_Regular ( Ivy_Obj_t *  p )

inlinestatic

Definition at line 193 of file ivy.h.

{ return (Ivy_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }

int Ivy_TableCountEntries

(

Ivy_Man_t *

p

)

Function*************************************************************

Synopsis [Count the number of nodes in the table.]

Description []

SideEffects []

SeeAlso []

Definition at line 187 of file ivyTable.c.

{
    int i, Counter = 0;
    for ( i = 0; i < p->nTableSize; i++ )
        Counter += (p->pTable[i] != 0);
    return Counter;
}

void Ivy_TableDelete	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj
	)

Function*************************************************************

Synopsis [Deletes the node from the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 132 of file ivyTable.c.

{
    Ivy_Obj_t * pEntry;
    int i, * pPlace;
    assert( !Ivy_IsComplement(pObj) );
    if ( !Ivy_ObjIsHash(pObj) )
        return;
    pPlace = Ivy_TableFind( p, pObj );
    assert( *pPlace == pObj->Id ); // node should be in the table
    *pPlace = 0;
    // rehash the adjacent entries
    i = pPlace - p->pTable;
    for ( i = (i+1) % p->nTableSize; p->pTable[i]; i = (i+1) % p->nTableSize )
    {
        pEntry = Ivy_ManObj( p, p->pTable[i] );
        p->pTable[i] = 0;
        Ivy_TableInsert( p, pEntry );
    }
}

void Ivy_TableInsert	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj
	)

Function*************************************************************

Synopsis [Adds the node to the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file ivyTable.c.

{
    int * pPlace;
    assert( !Ivy_IsComplement(pObj) );
    if ( !Ivy_ObjIsHash(pObj) )
        return;
    if ( (pObj->Id & 63) == 0 )
    {
        if ( p->nTableSize < 2 * Ivy_ManHashObjNum(p) )
            Ivy_TableResize( p );
    }
    pPlace = Ivy_TableFind( p, pObj );
    assert( *pPlace == 0 );
    *pPlace = pObj->Id;
}

Ivy_Obj_t* Ivy_TableLookup	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Checks if node with the given attributes is in the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 71 of file ivyTable.c.

{
    Ivy_Obj_t * pEntry;
    int i;
    assert( !Ivy_IsComplement(pObj) );
    if ( !Ivy_ObjIsHash(pObj) )
        return NULL;
    assert( Ivy_ObjIsLatch(pObj) || Ivy_ObjFaninId0(pObj) > 0 );
    assert( Ivy_ObjFaninId1(pObj) == 0 || Ivy_ObjFaninId0(pObj) < Ivy_ObjFaninId1(pObj) );
    if ( Ivy_ObjFanin0(pObj)->nRefs == 0 || (Ivy_ObjChild1(pObj) && Ivy_ObjFanin1(pObj)->nRefs == 0) )
        return NULL;
    for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
    {
        pEntry = Ivy_ManObj( p, p->pTable[i] );
        if ( Ivy_ObjChild0(pEntry) == Ivy_ObjChild0(pObj) && 
             Ivy_ObjChild1(pEntry) == Ivy_ObjChild1(pObj) && 
             Ivy_ObjInit(pEntry) == Ivy_ObjInit(pObj) && 
             Ivy_ObjType(pEntry) == Ivy_ObjType(pObj) )
            return pEntry;
    }
    return NULL;
}

void Ivy_TableProfile

(

Ivy_Man_t *

p

)

Function********************************************************************

Synopsis [Profiles the hash table.]

Description []

SideEffects []

SeeAlso []

Definition at line 250 of file ivyTable.c.

{
    int i, Counter = 0;
    for ( i = 0; i < p->nTableSize; i++ )
    {
        if ( p->pTable[i] )
            Counter++;
        else if ( Counter )
        {
            printf( "%d ", Counter );
            Counter = 0;
        }
    }
}

void Ivy_TableUpdate	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj,
		int	ObjIdNew
	)

Function*************************************************************

Synopsis [Updates the table to point to the new node.]

Description [If the old node (pObj) is in the table, updates the table to point to an object with different ID (ObjIdNew). The table should not contain an object with ObjIdNew (this is currently not checked).]

SideEffects []

SeeAlso []

Definition at line 165 of file ivyTable.c.

{
    int * pPlace;
    assert( !Ivy_IsComplement(pObj) );
    if ( !Ivy_ObjIsHash(pObj) )
        return;
    pPlace = Ivy_TableFind( p, pObj );
    assert( *pPlace == pObj->Id ); // node should be in the table
    *pPlace = ObjIdNew; 
}

int Ivy_TruthDsd	(	unsigned	uTruth,
		Vec_Int_t *	vTree
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Computes DSD of truth table of 5 variables or less.]

Description [Returns 1 if the function is a constant or is fully DSD decomposable using AND/EXOR/MUX gates.]

SideEffects []

SeeAlso []

Definition at line 166 of file ivyDsd.c.

{
    Ivy_Dec_t Node;
    int i, RetValue;
    // set the PI variables
    Vec_IntClear( vTree );
    for ( i = 0; i < 5; i++ )
        Vec_IntPush( vTree, 0 );
    // check if it is a constant
    if ( uTruth == 0 || ~uTruth == 0 )
    {
        Ivy_DecClear( &Node );
        Node.Type = IVY_DEC_CONST1;
        Node.fCompl = (uTruth == 0);
        Vec_IntPush( vTree, Ivy_DecToInt(Node) );
        return 1;
    }
    // perform the decomposition
    RetValue = Ivy_TruthDecompose_rec( uTruth, vTree );
    if ( RetValue == -1 )
        return 0;
    // get the topmost node
    if ( (RetValue >> 1) < 5 )
    { // add buffer
        Ivy_DecClear( &Node );
        Node.Type = IVY_DEC_BUF;
        Node.fCompl = (RetValue & 1);
        Node.Fan0 = ((RetValue >> 1) << 1);
        Vec_IntPush( vTree, Ivy_DecToInt(Node) );
    }
    else if ( RetValue & 1 )
    { // check if the topmost node has to be complemented
        Node = Ivy_IntToDec( Vec_IntPop(vTree) );
        assert( Node.fCompl == 0 );
        Node.fCompl = (RetValue & 1);
        Vec_IntPush( vTree, Ivy_DecToInt(Node) );
    }
    if ( uTruth != Ivy_TruthDsdCompute(vTree) )
        printf( "Verification failed.\n" );
    return 1;
}

unsigned Ivy_TruthDsdCompute

(

Vec_Int_t *

vTree

)

Function*************************************************************

Synopsis [Computes truth table of decomposition tree for verification.]

Description []

SideEffects []

SeeAlso []

Definition at line 478 of file ivyDsd.c.

{
    return Ivy_TruthDsdCompute_rec( Vec_IntSize(vTree)-1, vTree );
}

void Ivy_TruthDsdComputePrint

(

unsigned

uTruth

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 678 of file ivyDsd.c.

{
    static Vec_Int_t * vTree = NULL;
    if ( vTree == NULL )
        vTree = Vec_IntAlloc( 12 );
    if ( Ivy_TruthDsd( uTruth, vTree ) )
        Ivy_TruthDsdPrint( stdout, vTree );
    else
        printf( "Undecomposable\n" );
}

void Ivy_TruthDsdPrint	(	FILE *	pFile,
		Vec_Int_t *	vTree
	)

Function*************************************************************

Synopsis [Prints the decomposition tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 568 of file ivyDsd.c.

{
    fprintf( pFile, "F = " );
    Ivy_TruthDsdPrint_rec( pFile, Vec_IntSize(vTree)-1, vTree );
    fprintf( pFile, "\n" );
}

static int Ivy_TruthWordNum ( int  nVars )

inlinestatic

Definition at line 188 of file ivy.h.

{ return nVars <= 5 ? 1 : (1 << (nVars - 5));     }