kit.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "misc/extra/extraBdd.h"
#include "cloud.h"

Go to the source code of this file.

Data Structures
struct	Kit_Sop_t_
struct	Kit_Edge_t_
struct	Kit_Node_t_
struct	Kit_Graph_t_
struct	Kit_DsdObj_t_
struct	Kit_DsdNtk_t_
struct	Kit_DsdMan_t_

Macros
#define	Kit_DsdNtkForEachObj(pNtk, pObj, i)   for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
#define	Kit_DsdObjForEachFanin(pNtk, pObj, iLit, i)   for ( i = 0; (i < (int)(pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
#define	Kit_DsdObjForEachFaninReverse(pNtk, pObj, iLit, i)   for ( i = (int)(pObj)->nFans - 1; (i >= 0) && ((iLit) = (pObj)->pFans[i], 1); i-- )
#define	Kit_PlaForEachCube(pSop, nFanins, pCube)   for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )
#define	Kit_PlaCubeForEachVar(pCube, Value, i)   for ( i = 0; (pCube[i] != ' ') && (Value = pCube[i]); i++ )
#define	KIT_MIN(a, b)   (((a) < (b))? (a) : (b))
	MACRO DEFINITIONS ///. More...
#define	KIT_MAX(a, b)   (((a) > (b))? (a) : (b))
#define	KIT_INFINITY   (100000000)
#define	Kit_SopForEachCube(cSop, uCube, i)   for ( i = 0; (i < Kit_SopCubeNum(cSop)) && ((uCube) = Kit_SopCube(cSop, i)); i++ )
	ITERATORS ///. More...
#define	Kit_CubeForEachLiteral(uCube, Lit, nLits, i)   for ( i = 0; (i < (nLits)) && ((Lit) = Kit_CubeHasLit(uCube, i)); i++ )
#define	Kit_GraphForEachLeaf(pGraph, pLeaf, i)   for ( i = 0; (i < (pGraph)->nLeaves) && (((pLeaf) = Kit_GraphNode(pGraph, i)), 1); i++ )
#define	Kit_GraphForEachNode(pGraph, pAnd, i)   for ( i = (pGraph)->nLeaves; (i < (pGraph)->nSize) && (((pAnd) = Kit_GraphNode(pGraph, i)), 1); i++ )

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Kit_Sop_t_	Kit_Sop_t
	INCLUDES ///. More...
typedef struct Kit_Edge_t_	Kit_Edge_t
typedef struct Kit_Node_t_	Kit_Node_t
typedef struct Kit_Graph_t_	Kit_Graph_t
typedef struct Kit_DsdObj_t_	Kit_DsdObj_t
typedef struct Kit_DsdNtk_t_	Kit_DsdNtk_t
typedef struct Kit_DsdMan_t_	Kit_DsdMan_t

Enumerations
enum	Kit_Dsd_t {   KIT_DSD_NONE = 0, KIT_DSD_CONST1, KIT_DSD_VAR, KIT_DSD_AND,   KIT_DSD_XOR, KIT_DSD_PRIME }

Functions
static unsigned	Kit_DsdObjOffset (int nFans)
static unsigned *	Kit_DsdObjTruth (Kit_DsdObj_t *pObj)
static int	Kit_DsdNtkObjNum (Kit_DsdNtk_t *pNtk)
static Kit_DsdObj_t *	Kit_DsdNtkObj (Kit_DsdNtk_t *pNtk, int Id)
static Kit_DsdObj_t *	Kit_DsdNtkRoot (Kit_DsdNtk_t *pNtk)
static int	Kit_DsdLitIsLeaf (Kit_DsdNtk_t *pNtk, int Lit)
static unsigned	Kit_DsdLitSupport (Kit_DsdNtk_t *pNtk, int Lit)
static int	Kit_CubeHasLit (unsigned uCube, int i)
static unsigned	Kit_CubeSetLit (unsigned uCube, int i)
static unsigned	Kit_CubeXorLit (unsigned uCube, int i)
static unsigned	Kit_CubeRemLit (unsigned uCube, int i)
static int	Kit_CubeContains (unsigned uLarge, unsigned uSmall)
static unsigned	Kit_CubeSharp (unsigned uCube, unsigned uMask)
static unsigned	Kit_CubeMask (int nVar)
static int	Kit_CubeIsMarked (unsigned uCube)
static unsigned	Kit_CubeMark (unsigned uCube)
static unsigned	Kit_CubeUnmark (unsigned uCube)
static int	Kit_SopCubeNum (Kit_Sop_t *cSop)
static unsigned	Kit_SopCube (Kit_Sop_t *cSop, int i)
static void	Kit_SopShrink (Kit_Sop_t *cSop, int nCubesNew)
static void	Kit_SopPushCube (Kit_Sop_t *cSop, unsigned uCube)
static void	Kit_SopWriteCube (Kit_Sop_t *cSop, unsigned uCube, int i)
static Kit_Edge_t	Kit_EdgeCreate (int Node, int fCompl)
static unsigned	Kit_EdgeToInt (Kit_Edge_t eEdge)
static Kit_Edge_t	Kit_IntToEdge (unsigned Edge)
static unsigned	Kit_EdgeToInt_ (Kit_Edge_t m)
static Kit_Edge_t	Kit_IntToEdge_ (unsigned m)
static int	Kit_GraphIsConst (Kit_Graph_t *pGraph)
static int	Kit_GraphIsConst0 (Kit_Graph_t *pGraph)
static int	Kit_GraphIsConst1 (Kit_Graph_t *pGraph)
static int	Kit_GraphIsComplement (Kit_Graph_t *pGraph)
static int	Kit_GraphIsVar (Kit_Graph_t *pGraph)
static void	Kit_GraphComplement (Kit_Graph_t *pGraph)
static void	Kit_GraphSetRoot (Kit_Graph_t *pGraph, Kit_Edge_t eRoot)
static int	Kit_GraphLeaveNum (Kit_Graph_t *pGraph)
static int	Kit_GraphNodeNum (Kit_Graph_t *pGraph)
static Kit_Node_t *	Kit_GraphNode (Kit_Graph_t *pGraph, int i)
static Kit_Node_t *	Kit_GraphNodeLast (Kit_Graph_t *pGraph)
static int	Kit_GraphNodeInt (Kit_Graph_t *pGraph, Kit_Node_t *pNode)
static int	Kit_GraphNodeIsVar (Kit_Graph_t *pGraph, Kit_Node_t *pNode)
static Kit_Node_t *	Kit_GraphVar (Kit_Graph_t *pGraph)
static int	Kit_GraphVarInt (Kit_Graph_t *pGraph)
static Kit_Node_t *	Kit_GraphNodeFanin0 (Kit_Graph_t *pGraph, Kit_Node_t *pNode)
static Kit_Node_t *	Kit_GraphNodeFanin1 (Kit_Graph_t *pGraph, Kit_Node_t *pNode)
static int	Kit_GraphRootLevel (Kit_Graph_t *pGraph)
static int	Kit_SuppIsMinBase (int Supp)
static int	Kit_BitWordNum (int nBits)
static int	Kit_TruthWordNum (int nVars)
static unsigned	Kit_BitMask (int nBits)
static void	Kit_TruthSetBit (unsigned *p, int Bit)
static void	Kit_TruthXorBit (unsigned *p, int Bit)
static int	Kit_TruthHasBit (unsigned *p, int Bit)
static int	Kit_WordFindFirstBit (unsigned uWord)
static int	Kit_WordHasOneBit (unsigned uWord)
static int	Kit_WordCountOnes (unsigned uWord)
static int	Kit_TruthCountOnes (unsigned *pIn, int nVars)
static int	Kit_TruthFindFirstBit (unsigned *pIn, int nVars)
static int	Kit_TruthFindFirstZero (unsigned *pIn, int nVars)
static int	Kit_TruthIsEqual (unsigned *pIn0, unsigned *pIn1, int nVars)
static int	Kit_TruthIsEqualWithCare (unsigned *pIn0, unsigned *pIn1, unsigned *pCare, int nVars)
static int	Kit_TruthIsOpposite (unsigned *pIn0, unsigned *pIn1, int nVars)
static int	Kit_TruthIsEqualWithPhase (unsigned *pIn0, unsigned *pIn1, int nVars)
static int	Kit_TruthIsConst0 (unsigned *pIn, int nVars)
static int	Kit_TruthIsConst1 (unsigned *pIn, int nVars)
static int	Kit_TruthIsImply (unsigned *pIn1, unsigned *pIn2, int nVars)
static int	Kit_TruthIsDisjoint (unsigned *pIn1, unsigned *pIn2, int nVars)
static int	Kit_TruthIsDisjoint3 (unsigned *pIn1, unsigned *pIn2, unsigned *pIn3, int nVars)
static void	Kit_TruthCopy (unsigned *pOut, unsigned *pIn, int nVars)
static void	Kit_TruthClear (unsigned *pOut, int nVars)
static void	Kit_TruthFill (unsigned *pOut, int nVars)
static void	Kit_TruthNot (unsigned *pOut, unsigned *pIn, int nVars)
static void	Kit_TruthAnd (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
static void	Kit_TruthOr (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
static void	Kit_TruthXor (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
static void	Kit_TruthSharp (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
static void	Kit_TruthNand (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
static void	Kit_TruthAndPhase (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars, int fCompl0, int fCompl1)
static void	Kit_TruthOrPhase (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars, int fCompl0, int fCompl1)
static void	Kit_TruthMux (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, unsigned *pCtrl, int nVars)
static void	Kit_TruthMuxPhase (unsigned *pOut, unsigned *pIn0, unsigned *pIn1, unsigned *pCtrl, int nVars, int fComp0)
static void	Kit_TruthIthVar (unsigned *pTruth, int nVars, int iVar)
DdNode *	Kit_SopToBdd (DdManager *dd, Kit_Sop_t *cSop, int nVars)
	FUNCTION DECLARATIONS ///. More...
DdNode *	Kit_GraphToBdd (DdManager *dd, Kit_Graph_t *pGraph)
DdNode *	Kit_TruthToBdd (DdManager *dd, unsigned *pTruth, int nVars, int fMSBonTop)
CloudNode *	Kit_TruthToCloud (CloudManager *dd, unsigned *pTruth, int nVars)
unsigned *	Kit_CloudToTruth (Vec_Int_t *vNodes, int nVars, Vec_Ptr_t *vStore, int fInv)
int	Kit_CreateCloud (CloudManager *dd, CloudNode *pFunc, Vec_Int_t *vNodes)
int	Kit_CreateCloudFromTruth (CloudManager *dd, unsigned *pTruth, int nVars, Vec_Int_t *vNodes)
unsigned *	Kit_TruthCompose (CloudManager *dd, unsigned *pTruth, int nVars, unsigned **pInputs, int nVarsAll, Vec_Ptr_t *vStore, Vec_Int_t *vNodes)
void	Kit_TruthCofSupports (Vec_Int_t *vBddDir, Vec_Int_t *vBddInv, int nVars, Vec_Int_t *vMemory, unsigned *puSupps)
Kit_DsdMan_t *	Kit_DsdManAlloc (int nVars, int nNodes)
	DECLARATIONS ///. More...
void	Kit_DsdManFree (Kit_DsdMan_t *p)
Kit_DsdNtk_t *	Kit_DsdDeriveNtk (unsigned *pTruth, int nVars, int nLutSize)
unsigned *	Kit_DsdTruthCompute (Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk)
void	Kit_DsdTruth (Kit_DsdNtk_t *pNtk, unsigned *pTruthRes)
void	Kit_DsdTruthPartial (Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned *pTruthRes, unsigned uSupp)
void	Kit_DsdTruthPartialTwo (Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp, int iVar, unsigned *pTruthCo, unsigned *pTruthDec)
void	Kit_DsdPrint (FILE *pFile, Kit_DsdNtk_t *pNtk)
void	Kit_DsdPrintExpanded (Kit_DsdNtk_t *pNtk)
void	Kit_DsdPrintFromTruth (unsigned *pTruth, int nVars)
void	Kit_DsdPrintFromTruth2 (FILE *pFile, unsigned *pTruth, int nVars)
void	Kit_DsdWriteFromTruth (char *pBuffer, unsigned *pTruth, int nVars)
Kit_DsdNtk_t *	Kit_DsdDecompose (unsigned *pTruth, int nVars)
Kit_DsdNtk_t *	Kit_DsdDecomposeExpand (unsigned *pTruth, int nVars)
Kit_DsdNtk_t *	Kit_DsdDecomposeMux (unsigned *pTruth, int nVars, int nDecMux)
void	Kit_DsdVerify (Kit_DsdNtk_t *pNtk, unsigned *pTruth, int nVars)
void	Kit_DsdNtkFree (Kit_DsdNtk_t *pNtk)
int	Kit_DsdNonDsdSizeMax (Kit_DsdNtk_t *pNtk)
Kit_DsdObj_t *	Kit_DsdNonDsdPrimeMax (Kit_DsdNtk_t *pNtk)
unsigned	Kit_DsdNonDsdSupports (Kit_DsdNtk_t *pNtk)
int	Kit_DsdCountAigNodes (Kit_DsdNtk_t *pNtk)
unsigned	Kit_DsdGetSupports (Kit_DsdNtk_t *p)
Kit_DsdNtk_t *	Kit_DsdExpand (Kit_DsdNtk_t *p)
Kit_DsdNtk_t *	Kit_DsdShrink (Kit_DsdNtk_t *p, int pPrios[])
void	Kit_DsdRotate (Kit_DsdNtk_t *p, int pFreqs[])
int	Kit_DsdCofactoring (unsigned *pTruth, int nVars, int *pCofVars, int nLimit, int fVerbose)
Kit_Graph_t *	Kit_SopFactor (Vec_Int_t *vCover, int fCompl, int nVars, Vec_Int_t *vMemory)
	FUNCTION DEFINITIONS ///. More...
Kit_Graph_t *	Kit_GraphCreate (int nLeaves)
	DECLARATIONS ///. More...
Kit_Graph_t *	Kit_GraphCreateConst0 ()
Kit_Graph_t *	Kit_GraphCreateConst1 ()
Kit_Graph_t *	Kit_GraphCreateLeaf (int iLeaf, int nLeaves, int fCompl)
void	Kit_GraphFree (Kit_Graph_t *pGraph)
Kit_Node_t *	Kit_GraphAppendNode (Kit_Graph_t *pGraph)
Kit_Edge_t	Kit_GraphAddNodeAnd (Kit_Graph_t *pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1)
Kit_Edge_t	Kit_GraphAddNodeOr (Kit_Graph_t *pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1)
Kit_Edge_t	Kit_GraphAddNodeXor (Kit_Graph_t *pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1, int Type)
Kit_Edge_t	Kit_GraphAddNodeMux (Kit_Graph_t *pGraph, Kit_Edge_t eEdgeC, Kit_Edge_t eEdgeT, Kit_Edge_t eEdgeE, int Type)
unsigned	Kit_GraphToTruth (Kit_Graph_t *pGraph)
Kit_Graph_t *	Kit_TruthToGraph (unsigned *pTruth, int nVars, Vec_Int_t *vMemory)
int	Kit_GraphLeafDepth_rec (Kit_Graph_t *pGraph, Kit_Node_t *pNode, Kit_Node_t *pLeaf)
int	Kit_TruthIsop (unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
	FUNCTION DEFINITIONS ///. More...
void	Kit_TruthIsopPrint (unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
void	Kit_TruthIsopPrintCover (Vec_Int_t *vCover, int nVars, int fCompl)
int	Kit_PlaIsConst0 (char *pSop)
	DECLARATIONS ///. More...
int	Kit_PlaIsConst1 (char *pSop)
int	Kit_PlaIsBuf (char *pSop)
int	Kit_PlaIsInv (char *pSop)
int	Kit_PlaGetVarNum (char *pSop)
int	Kit_PlaGetCubeNum (char *pSop)
int	Kit_PlaIsComplement (char *pSop)
void	Kit_PlaComplement (char *pSop)
char *	Kit_PlaStart (void *p, int nCubes, int nVars)
char *	Kit_PlaCreateFromIsop (void *p, int nVars, Vec_Int_t *vCover)
void	Kit_PlaToIsop (char *pSop, Vec_Int_t *vCover)
char *	Kit_PlaStoreSop (void *p, char *pSop)
char *	Kit_PlaFromTruth (void *p, unsigned *pTruth, int nVars, Vec_Int_t *vCover)
char *	Kit_PlaFromTruthNew (unsigned *pTruth, int nVars, Vec_Int_t *vCover, Vec_Str_t *vStr)
ABC_UINT64_T	Kit_PlaToTruth6 (char *pSop, int nVars)
void	Kit_PlaToTruth (char *pSop, int nVars, Vec_Ptr_t *vVars, unsigned *pTemp, unsigned *pTruth)
void	Kit_SopCreate (Kit_Sop_t *cResult, Vec_Int_t *vInput, int nVars, Vec_Int_t *vMemory)
	DECLARATIONS ///. More...
void	Kit_SopCreateInverse (Kit_Sop_t *cResult, Vec_Int_t *vInput, int nVars, Vec_Int_t *vMemory)
void	Kit_SopDup (Kit_Sop_t *cResult, Kit_Sop_t *cSop, Vec_Int_t *vMemory)
void	Kit_SopDivideByLiteralQuo (Kit_Sop_t *cSop, int iLit)
void	Kit_SopDivideByCube (Kit_Sop_t *cSop, Kit_Sop_t *cDiv, Kit_Sop_t *vQuo, Kit_Sop_t *vRem, Vec_Int_t *vMemory)
void	Kit_SopDivideInternal (Kit_Sop_t *cSop, Kit_Sop_t *cDiv, Kit_Sop_t *vQuo, Kit_Sop_t *vRem, Vec_Int_t *vMemory)
void	Kit_SopMakeCubeFree (Kit_Sop_t *cSop)
int	Kit_SopIsCubeFree (Kit_Sop_t *cSop)
void	Kit_SopCommonCubeCover (Kit_Sop_t *cResult, Kit_Sop_t *cSop, Vec_Int_t *vMemory)
int	Kit_SopAnyLiteral (Kit_Sop_t *cSop, int nLits)
int	Kit_SopDivisor (Kit_Sop_t *cResult, Kit_Sop_t *cSop, int nLits, Vec_Int_t *vMemory)
void	Kit_SopBestLiteralCover (Kit_Sop_t *cResult, Kit_Sop_t *cSop, unsigned uCube, int nLits, Vec_Int_t *vMemory)
void	Kit_TruthSwapAdjacentVars (unsigned *pOut, unsigned *pIn, int nVars, int Start)
	DECLARATIONS ///. More...
void	Kit_TruthStretch (unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
void	Kit_TruthPermute (unsigned *pOut, unsigned *pIn, int nVars, char *pPerm, int fReturnIn)
void	Kit_TruthShrink (unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
int	Kit_TruthVarInSupport (unsigned *pTruth, int nVars, int iVar)
int	Kit_TruthSupportSize (unsigned *pTruth, int nVars)
unsigned	Kit_TruthSupport (unsigned *pTruth, int nVars)
void	Kit_TruthCofactor0 (unsigned *pTruth, int nVars, int iVar)
void	Kit_TruthCofactor1 (unsigned *pTruth, int nVars, int iVar)
void	Kit_TruthCofactor0New (unsigned *pOut, unsigned *pIn, int nVars, int iVar)
void	Kit_TruthCofactor1New (unsigned *pOut, unsigned *pIn, int nVars, int iVar)
int	Kit_TruthVarIsVacuous (unsigned *pOnset, unsigned *pOffset, int nVars, int iVar)
void	Kit_TruthExist (unsigned *pTruth, int nVars, int iVar)
void	Kit_TruthExistNew (unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
void	Kit_TruthExistSet (unsigned *pRes, unsigned *pTruth, int nVars, unsigned uMask)
void	Kit_TruthForall (unsigned *pTruth, int nVars, int iVar)
void	Kit_TruthForallNew (unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
void	Kit_TruthForallSet (unsigned *pRes, unsigned *pTruth, int nVars, unsigned uMask)
void	Kit_TruthUniqueNew (unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
void	Kit_TruthMuxVar (unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
void	Kit_TruthMuxVarPhase (unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar, int fCompl0)
void	Kit_TruthChangePhase (unsigned *pTruth, int nVars, int iVar)
int	Kit_TruthVarsSymm (unsigned *pTruth, int nVars, int iVar0, int iVar1, unsigned *pCof0, unsigned *pCof1)
int	Kit_TruthVarsAntiSymm (unsigned *pTruth, int nVars, int iVar0, int iVar1, unsigned *pCof0, unsigned *pCof1)
int	Kit_TruthMinCofSuppOverlap (unsigned *pTruth, int nVars, int *pVarMin)
int	Kit_TruthBestCofVar (unsigned *pTruth, int nVars, unsigned *pCof0, unsigned *pCof1)
void	Kit_TruthCountOnesInCofs (unsigned *pTruth, int nVars, int *pStore)
void	Kit_TruthCountOnesInCofs0 (unsigned *pTruth, int nVars, int *pStore)
void	Kit_TruthCountOnesInCofsSlow (unsigned *pTruth, int nVars, int *pStore, unsigned *pAux)
unsigned	Kit_TruthHash (unsigned *pIn, int nWords)
unsigned	Kit_TruthSemiCanonicize (unsigned *pInOut, unsigned *pAux, int nVars, char *pCanonPerm)
char *	Kit_TruthDumpToFile (unsigned *pTruth, int nVars, int nFile)
void	Kit_TruthPrintProfile (unsigned *pTruth, int nVars)

Macro Definition Documentation

#define Kit_CubeForEachLiteral	(		uCube,
			Lit,
			nLits,
			i
	)		for ( i = 0; (i < (nLits)) && ((Lit) = Kit_CubeHasLit(uCube, i)); i++ )

Definition at line 499 of file kit.h.

#define Kit_DsdNtkForEachObj	(		pNtk,
			pObj,
			i
	)		for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )

Definition at line 155 of file kit.h.

#define Kit_DsdObjForEachFanin	(		pNtk,
			pObj,
			iLit,
			i
	)		for ( i = 0; (i < (int)(pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )

Definition at line 157 of file kit.h.

#define Kit_DsdObjForEachFaninReverse	(		pNtk,
			pObj,
			iLit,
			i
	)		for ( i = (int)(pObj)->nFans - 1; (i >= 0) && ((iLit) = (pObj)->pFans[i], 1); i-- )

Definition at line 159 of file kit.h.

#define Kit_GraphForEachLeaf	(		pGraph,
			pLeaf,
			i
	)		for ( i = 0; (i < (pGraph)->nLeaves) && (((pLeaf) = Kit_GraphNode(pGraph, i)), 1); i++ )

Definition at line 502 of file kit.h.

#define Kit_GraphForEachNode	(		pGraph,
			pAnd,
			i
	)		for ( i = (pGraph)->nLeaves; (i < (pGraph)->nSize) && (((pAnd) = Kit_GraphNode(pGraph, i)), 1); i++ )

Definition at line 504 of file kit.h.

#define KIT_INFINITY   (100000000)

Definition at line 173 of file kit.h.

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

Definition at line 172 of file kit.h.

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

MACRO DEFINITIONS ///.

Definition at line 171 of file kit.h.

#define Kit_PlaCubeForEachVar	(		pCube,
			Value,
			i
	)		for ( i = 0; (pCube[i] != ' ') && (Value = pCube[i]); i++ )

Definition at line 164 of file kit.h.

#define Kit_PlaForEachCube	(		pSop,
			nFanins,
			pCube
	)		for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )

Definition at line 162 of file kit.h.

#define Kit_SopForEachCube	(		cSop,
			uCube,
			i
	)		for ( i = 0; (i < Kit_SopCubeNum(cSop)) && ((uCube) = Kit_SopCube(cSop, i)); i++ )

ITERATORS ///.

Definition at line 497 of file kit.h.

Typedef Documentation

typedef struct Kit_DsdMan_t_ Kit_DsdMan_t

Definition at line 134 of file kit.h.

typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t

Definition at line 121 of file kit.h.

typedef struct Kit_DsdObj_t_ Kit_DsdObj_t

Definition at line 108 of file kit.h.

typedef struct Kit_Edge_t_ Kit_Edge_t

Definition at line 59 of file kit.h.

typedef struct Kit_Graph_t_ Kit_Graph_t

Definition at line 85 of file kit.h.

typedef struct Kit_Node_t_ Kit_Node_t

Definition at line 66 of file kit.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Kit_Sop_t_ Kit_Sop_t

INCLUDES ///.

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

FileName [kit.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 6, 2006.]

Revision [

Id:

kit.h,v 1.00 2006/12/06 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 51 of file kit.h.

Enumeration Type Documentation

enum Kit_Dsd_t

Enumerator
KIT_DSD_NONE
KIT_DSD_CONST1
KIT_DSD_VAR
KIT_DSD_AND
KIT_DSD_XOR
KIT_DSD_PRIME

Definition at line 98 of file kit.h.

             { 
    KIT_DSD_NONE  = 0,  // 0: unknown
    KIT_DSD_CONST1,     // 1: constant 1
    KIT_DSD_VAR,        // 2: elementary variable
    KIT_DSD_AND,        // 3: multi-input AND
    KIT_DSD_XOR,        // 4: multi-input XOR
    KIT_DSD_PRIME       // 5: arbitrary function of 3+ variables
} Kit_Dsd_t;

Function Documentation

static unsigned Kit_BitMask ( int  nBits )

inlinestatic

Definition at line 225 of file kit.h.

{ assert( nBits <= 32 ); return ~((~(unsigned)0) << nBits);               }

static int Kit_BitWordNum ( int  nBits )

inlinestatic

Definition at line 223 of file kit.h.

{ return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); }

unsigned* Kit_CloudToTruth	(	Vec_Int_t *	vNodes,
		int	nVars,
		Vec_Ptr_t *	vStore,
		int	fInv
	)

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

Synopsis [Computes composition of truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file kitCloud.c.

{
    unsigned * pThis, * pFan0, * pFan1;
    Kit_Mux_t Mux;
    int i, Entry;
    assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
    pThis = (unsigned *)Vec_PtrEntry( vStore, 0 );
    Kit_TruthFill( pThis, nVars );
    Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
    {
        Mux = Kit_Int2Mux(Entry);
        assert( (int)Mux.e < i && (int)Mux.t < i && (int)Mux.v < nVars );          
        pFan0 = (unsigned *)Vec_PtrEntry( vStore, Mux.e );
        pFan1 = (unsigned *)Vec_PtrEntry( vStore, Mux.t );
        pThis = (unsigned *)Vec_PtrEntry( vStore, i );
        Kit_TruthMuxVarPhase( pThis, pFan0, pFan1, nVars, fInv? Mux.v : nVars-1-Mux.v, Mux.c );
    } 
    // complement the result
    if ( Mux.i )
        Kit_TruthNot( pThis, pThis, nVars );
    return pThis;
}

int Kit_CreateCloud	(	CloudManager *	dd,
		CloudNode *	pFunc,
		Vec_Int_t *	vNodes
	)

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

Synopsis [Transforms the array of BDDs into the integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 167 of file kitCloud.c.

{
    Kit_Mux_t Mux;
    int nNodes, i;
    // collect BDD nodes
    nNodes = Cloud_DagCollect( dd, pFunc );
    if ( nNodes >= (1<<12) ) // because in Kit_Mux_t edge is 12 bit
        return 0;
    assert( nNodes == Cloud_DagSize( dd, pFunc ) );
    assert( nNodes < dd->nNodesLimit );
    Vec_IntClear( vNodes );
    Vec_IntPush( vNodes, 0 ); // const1 node
    dd->ppNodes[0]->s = 0;
    for ( i = 1; i < nNodes; i++ )
    {
        dd->ppNodes[i]->s = i;
        Mux.v = dd->ppNodes[i]->v;
        Mux.t = dd->ppNodes[i]->t->s;
        Mux.e = Cloud_Regular(dd->ppNodes[i]->e)->s;
        Mux.c = Cloud_IsComplement(dd->ppNodes[i]->e); 
        Mux.i = (i == nNodes - 1)? Cloud_IsComplement(pFunc) : 0;
        // put the MUX into the array
        Vec_IntPush( vNodes, Kit_Mux2Int(Mux) );
    }
    assert( Vec_IntSize(vNodes) == nNodes );
    // reset signatures
    for ( i = 0; i < nNodes; i++ )
        dd->ppNodes[i]->s = dd->nSignCur;
    return 1;
}

int Kit_CreateCloudFromTruth	(	CloudManager *	dd,
		unsigned *	pTruth,
		int	nVars,
		Vec_Int_t *	vNodes
	)

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

Synopsis [Transforms the array of BDDs into the integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 209 of file kitCloud.c.

{
    CloudNode * pFunc;
    Cloud_Restart( dd );
    pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
    Vec_IntClear( vNodes );
    return Kit_CreateCloud( dd, pFunc, vNodes );
}

static int Kit_CubeContains ( unsigned  uLarge, unsigned  uSmall  )

inlinestatic

Definition at line 180 of file kit.h.

{ return (uLarge & uSmall) == uSmall;     }

static int Kit_CubeHasLit ( unsigned  uCube, int  i  )

inlinestatic

Definition at line 175 of file kit.h.

{ return(uCube &  (unsigned)(1<<i)) > 0;  }

static int Kit_CubeIsMarked ( unsigned  uCube )

inlinestatic

Definition at line 184 of file kit.h.

{ return Kit_CubeHasLit( uCube, 31 );     }

static unsigned Kit_CubeMark ( unsigned  uCube )

inlinestatic

Definition at line 185 of file kit.h.

{ return Kit_CubeSetLit( uCube, 31 );     }

static unsigned Kit_CubeMask ( int  nVar )

inlinestatic

Definition at line 182 of file kit.h.

{ return (~(unsigned)0) >> (32-nVar);     }

static unsigned Kit_CubeRemLit ( unsigned  uCube, int  i  )

inlinestatic

Definition at line 178 of file kit.h.

{ return uCube & ~(unsigned)(1<<i);       }

static unsigned Kit_CubeSetLit ( unsigned  uCube, int  i  )

inlinestatic

Definition at line 176 of file kit.h.

{ return uCube |  (unsigned)(1<<i);       }

static unsigned Kit_CubeSharp ( unsigned  uCube, unsigned  uMask  )

inlinestatic

Definition at line 181 of file kit.h.

{ return uCube & ~uMask;                  }

static unsigned Kit_CubeUnmark ( unsigned  uCube )

inlinestatic

Definition at line 186 of file kit.h.

{ return Kit_CubeRemLit( uCube, 31 );     }

static unsigned Kit_CubeXorLit ( unsigned  uCube, int  i  )

inlinestatic

Definition at line 177 of file kit.h.

{ return uCube ^  (unsigned)(1<<i);       }

int Kit_DsdCofactoring	(	unsigned *	pTruth,
		int	nVars,
		int *	pCofVars,
		int	nLimit,
		int	fVerbose
	)

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

Synopsis [Canonical decomposition into completely DSD-structure.]

Description [Returns the number of cofactoring steps. Also returns the cofactoring variables in pVars.]

SideEffects []

SeeAlso []

Definition at line 2678 of file kitDsd.c.

{
    Kit_DsdNtk_t * ppNtks[5][16] = {
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}
    };
    Kit_DsdNtk_t * pTemp;
    unsigned * ppCofs[5][16];
    int pTryVars[16], nTryVars;
    int nPrimeSizeMin, nPrimeSizeMax, nPrimeSizeCur;
    int nSuppSizeMin, nSuppSizeMax, iVarBest;
    int i, k, v, nStep, nSize, nMemSize;
    assert( nLimit < 5 );

    // allocate storage for cofactors
    nMemSize = Kit_TruthWordNum(nVars);
    ppCofs[0][0] = ABC_ALLOC( unsigned, 80 * nMemSize );
    nSize = 0;
    for ( i = 0; i <  5; i++ )
    for ( k = 0; k < 16; k++ )
        ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
    assert( nSize == 80 );

    // copy the function
    Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
    ppNtks[0][0] = Kit_DsdDecompose( ppCofs[0][0], nVars );

    if ( fVerbose )
        printf( "\nProcessing prime function with %d support variables:\n", nVars );

    // perform recursive cofactoring
    for ( nStep = 0; nStep < nLimit; nStep++ )
    {
        nSize = (1 << nStep);
        // find the variables to use in the cofactoring step
        nTryVars = Kit_DsdCofactoringGetVars( ppNtks[nStep], nSize, pTryVars );
        if ( nTryVars == 0 )
            break;
        // cofactor w.r.t. the above variables
        iVarBest = -1;
        nPrimeSizeMin = 10000;
        nSuppSizeMin  = 10000;
        for ( v = 0; v < nTryVars; v++ )
        {
            nPrimeSizeMax = 0;
            nSuppSizeMax = 0;
            for ( i = 0; i < nSize; i++ )
            {
                // cofactor and decompose cofactors          
                Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, pTryVars[v] );
                Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, pTryVars[v] );
                ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars );
                ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars );
                // compute the largest non-decomp block
                nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+0]);
                nPrimeSizeMax  = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
                nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+1]);
                nPrimeSizeMax  = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
                // compute the sum total of supports
                nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+0], nVars );
                nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+1], nVars );
                // free the networks
                Kit_DsdNtkFree( ppNtks[nStep+1][2*i+0] );
                Kit_DsdNtkFree( ppNtks[nStep+1][2*i+1] );
            }
            // find the min max support size of the prime component
            if ( nPrimeSizeMin > nPrimeSizeMax || (nPrimeSizeMin == nPrimeSizeMax && nSuppSizeMin > nSuppSizeMax) )
            {
                nPrimeSizeMin = nPrimeSizeMax;
                nSuppSizeMin  = nSuppSizeMax;
                iVarBest      = pTryVars[v];
            }
        }
        assert( iVarBest != -1 );
        // save the variable
        if ( pCofVars )
            pCofVars[nStep] = iVarBest;
        // cofactor w.r.t. the best
        for ( i = 0; i < nSize; i++ )
        {
            Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, iVarBest );
            Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, iVarBest );
            ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars );
            ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars );
            if ( fVerbose )
            {
                ppNtks[nStep+1][2*i+0] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+0] );
                Kit_DsdNtkFree( pTemp );
                ppNtks[nStep+1][2*i+1] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+1] );
                Kit_DsdNtkFree( pTemp );

                printf( "Cof%d%d: ", nStep+1, 2*i+0 );
                Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+0] ), printf( "\n" );
                printf( "Cof%d%d: ", nStep+1, 2*i+1 );
                Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+1] ), printf( "\n" );
            }
        }
    }

    // free the networks
    for ( i = 0; i <  5; i++ )
    for ( k = 0; k < 16; k++ )
        if ( ppNtks[i][k] )
            Kit_DsdNtkFree( ppNtks[i][k] );
    ABC_FREE( ppCofs[0][0] );

    assert( nStep <= nLimit );
    return nStep;
}

int Kit_DsdCountAigNodes

(

Kit_DsdNtk_t *

pNtk

)

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

Synopsis [Returns 1 if there is a component with more than 3 inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 1895 of file kitDsd.c.

{
    Kit_DsdObj_t * pObj;
    int i, Counter = 0;
    for ( i = 0; i < pNtk->nNodes; i++ )
    {
        pObj = pNtk->pNodes[i];
        if ( pObj->Type == KIT_DSD_AND )
            Counter += ((int)pObj->nFans - 1);
        else if ( pObj->Type == KIT_DSD_XOR )
            Counter += ((int)pObj->nFans - 1) * 3;
        else if ( pObj->Type == KIT_DSD_PRIME ) // assuming MUX decomposition
            Counter += 3;
    }
    return Counter;
}

Kit_DsdNtk_t* Kit_DsdDecompose	(	unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Performs decomposition of the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 2314 of file kitDsd.c.

{
    return Kit_DsdDecomposeInt( pTruth, nVars, 0 );
}

Kit_DsdNtk_t* Kit_DsdDecomposeExpand	(	unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Performs decomposition of the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 2330 of file kitDsd.c.

{
    Kit_DsdNtk_t * pNtk, * pTemp;
    pNtk = Kit_DsdDecomposeInt( pTruth, nVars, 0 );
    pNtk = Kit_DsdExpand( pTemp = pNtk );      
    Kit_DsdNtkFree( pTemp );
    return pNtk;
}

Kit_DsdNtk_t* Kit_DsdDecomposeMux	(	unsigned *	pTruth,
		int	nVars,
		int	nDecMux
	)

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

Synopsis [Performs decomposition of the truth table.]

Description [Uses MUXes to break-down large prime nodes.]

SideEffects []

SeeAlso []

Definition at line 2350 of file kitDsd.c.

{
/*
    Kit_DsdNtk_t * pNew;
    Kit_DsdObj_t * pObjNew;
    assert( nVars <= 16 );
    // create a new network
    pNew = Kit_DsdNtkAlloc( nVars );
    // consider simple special cases
    if ( nVars == 0 )
    {
        pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
        pNew->Root = Abc_Var2Lit( pObjNew->Id, (int)(pTruth[0] == 0) );
        return pNew;
    }
    if ( nVars == 1 )
    {
        pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
        pObjNew->pFans[0] = Abc_Var2Lit( 0, 0 );
        pNew->Root = Abc_Var2Lit( pObjNew->Id, (int)(pTruth[0] != 0xAAAAAAAA) );
        return pNew;
    }
*/
    return Kit_DsdDecomposeInt( pTruth, nVars, nDecMux );
}

Kit_DsdNtk_t* Kit_DsdDeriveNtk	(	unsigned *	pTruth,
		int	nVars,
		int	nLutSize
	)

Kit_DsdNtk_t* Kit_DsdExpand

(

Kit_DsdNtk_t *

p

)

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

Synopsis [Expands the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 1451 of file kitDsd.c.

{
    Kit_DsdNtk_t * pNew;
    Kit_DsdObj_t * pObjNew;
    assert( p->nVars <= 16 );
    // create a new network
    pNew = Kit_DsdNtkAlloc( p->nVars );
    // consider simple special cases
    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
    {
        pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
        pNew->Root = Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(p->Root) );
        return pNew;
    }
    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
    {
        pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
        pObjNew->pFans[0] = Kit_DsdNtkRoot(p)->pFans[0];
        pNew->Root = Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(p->Root) );
        return pNew;
    }
    // convert the root node
    pNew->Root = Kit_DsdExpandNode_rec( pNew, p, p->Root );
    return pNew;
}

unsigned Kit_DsdGetSupports

(

Kit_DsdNtk_t *

p

)

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

Synopsis [Compute the support.]

Description []

SideEffects []

SeeAlso []

Definition at line 1762 of file kitDsd.c.

{
    Kit_DsdObj_t * pRoot;
    unsigned uSupport;
    assert( p->pSupps == NULL );
    p->pSupps = ABC_ALLOC( unsigned, p->nNodes );
    // consider simple special cases
    pRoot = Kit_DsdNtkRoot(p);
    if ( pRoot->Type == KIT_DSD_CONST1 )
    {
        assert( p->nNodes == 1 );
        uSupport = p->pSupps[0] = 0;
    }
    if ( pRoot->Type == KIT_DSD_VAR )
    {
        assert( p->nNodes == 1 );
        uSupport = p->pSupps[0] = Kit_DsdLitSupport( p, pRoot->pFans[0] );
    }
    else
        uSupport = Kit_DsdGetSupports_rec( p, p->Root );
    assert( uSupport <= 0xFFFF );
    return uSupport;
}

static int Kit_DsdLitIsLeaf ( Kit_DsdNtk_t *  pNtk, int  Lit  )

inlinestatic

Definition at line 152 of file kit.h.

{ int Id = Abc_Lit2Var(Lit); assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars; }

static unsigned Kit_DsdLitSupport ( Kit_DsdNtk_t *  pNtk, int  Lit  )

inlinestatic

Definition at line 153 of file kit.h.

{ int Id = Abc_Lit2Var(Lit); assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return pNtk->pSupps? (Id < pNtk->nVars? (1 << Id) : pNtk->pSupps[Id - pNtk->nVars]) : 0; }

Kit_DsdMan_t* Kit_DsdManAlloc	(	int	nVars,
		int	nNodes
	)

DECLARATIONS ///.

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

FileName [kitDsd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Performs disjoint-support decomposition based on truth tables.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 6, 2006.]

Revision [

Id:

kitDsd.c,v 1.00 2006/12/06 00:00:00 alanmi Exp

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

Synopsis [Allocates the DSD manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file kitDsd.c.

{
    Kit_DsdMan_t * p;
    p = ABC_ALLOC( Kit_DsdMan_t, 1 );
    memset( p, 0, sizeof(Kit_DsdMan_t) );
    p->nVars    = nVars;
    p->nWords   = Kit_TruthWordNum( p->nVars );
    p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
    p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords );
    p->dd       = Cloud_Init( 16, 14 );
    p->vTtBdds  = Vec_PtrAllocSimInfo( (1<<12), p->nWords );
    p->vNodes   = Vec_IntAlloc( 512 );
    return p;
}

void Kit_DsdManFree

(

Kit_DsdMan_t *

p

)

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

Synopsis [Deallocates the DSD manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 71 of file kitDsd.c.

{
    Cloud_Quit( p->dd );
    Vec_IntFree( p->vNodes );
    Vec_PtrFree( p->vTtBdds );
    Vec_PtrFree( p->vTtElems );
    Vec_PtrFree( p->vTtNodes );
    ABC_FREE( p );
}

Kit_DsdObj_t* Kit_DsdNonDsdPrimeMax

(

Kit_DsdNtk_t *

pNtk

)

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

Synopsis [Returns the largest non-DSD block.]

Description []

SideEffects []

SeeAlso []

Definition at line 1236 of file kitDsd.c.

{
    Kit_DsdObj_t * pObj, * pObjMax = NULL;
    unsigned i, nSizeMax = 0;
    Kit_DsdNtkForEachObj( pNtk, pObj, i )
    {
        if ( pObj->Type != KIT_DSD_PRIME )
            continue;
        if ( nSizeMax < pObj->nFans )
        {
            nSizeMax = pObj->nFans;
            pObjMax = pObj;
        }
    }
    return pObjMax;
}

int Kit_DsdNonDsdSizeMax

(

Kit_DsdNtk_t *

pNtk

)

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

Synopsis [Returns the size of the largest non-DSD block.]

Description []

SideEffects []

SeeAlso []

Definition at line 1211 of file kitDsd.c.

{
    Kit_DsdObj_t * pObj;
    unsigned i, nSizeMax = 0;
    Kit_DsdNtkForEachObj( pNtk, pObj, i )
    {
        if ( pObj->Type != KIT_DSD_PRIME )
            continue;
        if ( nSizeMax < pObj->nFans )
            nSizeMax = pObj->nFans;
    }
    return nSizeMax;
}

unsigned Kit_DsdNonDsdSupports

(

Kit_DsdNtk_t *

pNtk

)

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

Synopsis [Finds the union of supports of the non-DSD blocks.]

Description []

SideEffects []

SeeAlso []

Definition at line 1264 of file kitDsd.c.

{
    Kit_DsdObj_t * pObj;
    unsigned i, uSupport = 0;
//    ABC_FREE( pNtk->pSupps );
    Kit_DsdGetSupports( pNtk );
    Kit_DsdNtkForEachObj( pNtk, pObj, i )
    {
        if ( pObj->Type != KIT_DSD_PRIME )
            continue;
        uSupport |= Kit_DsdLitSupport( pNtk, Abc_Var2Lit(pObj->Id,0) );
    }
    return uSupport;
}

void Kit_DsdNtkFree

(

Kit_DsdNtk_t *

pNtk

)

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

Synopsis [Deallocate the DSD network.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file kitDsd.c.

{
    Kit_DsdObj_t * pObj;
    unsigned i;
    Kit_DsdNtkForEachObj( pNtk, pObj, i )
        ABC_FREE( pObj );
    ABC_FREE( pNtk->pSupps );
    ABC_FREE( pNtk->pNodes );
    ABC_FREE( pNtk->pMem );
    ABC_FREE( pNtk );
}

static Kit_DsdObj_t* Kit_DsdNtkObj ( Kit_DsdNtk_t *  pNtk, int  Id  )

inlinestatic

Definition at line 150 of file kit.h.

{ assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }

static int Kit_DsdNtkObjNum ( Kit_DsdNtk_t *  pNtk )

inlinestatic

Definition at line 149 of file kit.h.

{ return pNtk->nVars + pNtk->nNodes; }

static Kit_DsdObj_t* Kit_DsdNtkRoot ( Kit_DsdNtk_t *  pNtk )

inlinestatic

Definition at line 151 of file kit.h.

{ return Kit_DsdNtkObj( pNtk, Abc_Lit2Var(pNtk->Root) );                      }

static unsigned Kit_DsdObjOffset ( int  nFans )

inlinestatic

Definition at line 147 of file kit.h.

{ return (nFans >> 1) + ((nFans & 1) > 0);                    }

static unsigned* Kit_DsdObjTruth ( Kit_DsdObj_t *  pObj )

inlinestatic

Definition at line 148 of file kit.h.

{ return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }

void Kit_DsdPrint	(	FILE *	pFile,
		Kit_DsdNtk_t *	pNtk
	)

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 374 of file kitDsd.c.

{
    fprintf( pFile, "F = " );
    if ( Abc_LitIsCompl(pNtk->Root) )
        fprintf( pFile, "!" );
    Kit_DsdPrint_rec( pFile, pNtk, Abc_Lit2Var(pNtk->Root) );
//    fprintf( pFile, "\n" );
}

void Kit_DsdPrintExpanded

(

Kit_DsdNtk_t *

pNtk

)

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 471 of file kitDsd.c.

{
    Kit_DsdNtk_t * pTemp;
    pTemp = Kit_DsdExpand( pNtk );
    Kit_DsdPrint( stdout, pTemp );
    Kit_DsdNtkFree( pTemp );
}

void Kit_DsdPrintFromTruth	(	unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 490 of file kitDsd.c.

{
    Kit_DsdNtk_t * pTemp, * pTemp2;
//    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 8 );
//    Kit_DsdPrintExpanded( pTemp );
    pTemp2 = Kit_DsdExpand( pTemp );
    Kit_DsdPrint( stdout, pTemp2 );
    Kit_DsdVerify( pTemp2, pTruth, nVars ); 
    Kit_DsdNtkFree( pTemp2 );
    Kit_DsdNtkFree( pTemp );
}

void Kit_DsdPrintFromTruth2	(	FILE *	pFile,
		unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 514 of file kitDsd.c.

{
    Kit_DsdNtk_t * pTemp, * pTemp2;
    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 0 );
    pTemp2 = Kit_DsdExpand( pTemp );
    Kit_DsdPrint2( pFile, pTemp2 );
    Kit_DsdVerify( pTemp2, pTruth, nVars ); 
    Kit_DsdNtkFree( pTemp2 );
    Kit_DsdNtkFree( pTemp );
}

void Kit_DsdRotate	(	Kit_DsdNtk_t *	p,
		int	pFreqs[]
	)

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

Synopsis [Rotates the network.]

Description [Transforms prime nodes to have the fanin with the highest frequency of supports go first.]

SideEffects []

SeeAlso []

Definition at line 1671 of file kitDsd.c.

{
    Kit_DsdObj_t * pObj;
    unsigned * pIn, * pOut, * pTemp, k;
    int i, v, Temp, uSuppFanin, iFaninLit, WeightMax, FaninMax, nSwaps;
    int Weights[16];
    // go through the prime nodes
    Kit_DsdNtkForEachObj( p, pObj, i )
    {
        if ( pObj->Type != KIT_DSD_PRIME )
            continue;
        // count the fanin frequencies
        Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
        {
            uSuppFanin = Kit_DsdLitSupport( p, iFaninLit );
            Weights[k] = 0;
            for ( v = 0; v < 16; v++ )
                if ( uSuppFanin & (1 << v) )
                    Weights[k] += pFreqs[v] - 1;
        }
        // find the most frequent fanin
        WeightMax = 0; 
        FaninMax = -1;
        for ( k = 0; k < pObj->nFans; k++ )
            if ( WeightMax < Weights[k] )
            {
                WeightMax = Weights[k];
                FaninMax = k;
            }
        // no need to reorder if there are no frequent fanins
        if ( FaninMax == -1 )
            continue;
        // move the fanins number k to the first place
        nSwaps = 0;
        pIn = Kit_DsdObjTruth(pObj);
        pOut = p->pMem;
//        for ( v = FaninMax; v < ((int)pObj->nFans)-1; v++ )
        for ( v = FaninMax-1; v >= 0; v-- )
        {
            // swap the fanins
            Temp = pObj->pFans[v];
            pObj->pFans[v] = pObj->pFans[v+1];
            pObj->pFans[v+1] = Temp;
            // swap the truth table variables
            Kit_TruthSwapAdjacentVars( pOut, pIn, pObj->nFans, v );
            pTemp = pIn; pIn = pOut; pOut = pTemp;
            nSwaps++;
        }
        if ( nSwaps & 1 )
            Kit_TruthCopy( pOut, pIn, pObj->nFans );
    }    
}

Kit_DsdNtk_t* Kit_DsdShrink	(	Kit_DsdNtk_t *	p,
		int	pPrios[]
	)

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

Synopsis [Shrinks the network.]

Description [Transforms the network to have two-input nodes so that the higher-ordered nodes were decomposed out first.]

SideEffects []

SeeAlso []

Definition at line 1633 of file kitDsd.c.

{
    Kit_DsdNtk_t * pNew;
    Kit_DsdObj_t * pObjNew;
    assert( p->nVars <= 16 );
    // create a new network
    pNew = Kit_DsdNtkAlloc( p->nVars );
    // consider simple special cases
    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
    {
        pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
        pNew->Root = Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(p->Root) );
        return pNew;
    }
    if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
    {
        pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
        pObjNew->pFans[0] = Kit_DsdNtkRoot(p)->pFans[0];
        pNew->Root = Abc_Var2Lit( pObjNew->Id, Abc_LitIsCompl(p->Root) );
        return pNew;
    }
    // convert the root node
    pNew->Root = Kit_DsdShrink_rec( pNew, p, p->Root, pPrios );
    return pNew;
}

void Kit_DsdTruth	(	Kit_DsdNtk_t *	pNtk,
		unsigned *	pTruthRes
	)

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

Synopsis [Derives the truth table of the DSD network.]

Description []

SideEffects []

SeeAlso []

Definition at line 1068 of file kitDsd.c.

{
    Kit_DsdMan_t * p;
    unsigned * pTruth;
    p = Kit_DsdManAlloc( pNtk->nVars, Kit_DsdNtkObjNum(pNtk) );
    pTruth = Kit_DsdTruthCompute( p, pNtk );
    Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
    Kit_DsdManFree( p );
}

unsigned* Kit_DsdTruthCompute	(	Kit_DsdMan_t *	p,
		Kit_DsdNtk_t *	pNtk
	)

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

Synopsis [Derives the truth table of the DSD network.]

Description []

SideEffects []

SeeAlso []

Definition at line 663 of file kitDsd.c.

{
    unsigned * pTruthRes;
    int i;
    // assign elementary truth ables
    assert( pNtk->nVars <= p->nVars );
    for ( i = 0; i < (int)pNtk->nVars; i++ )
        Kit_TruthCopy( (unsigned *)Vec_PtrEntry(p->vTtNodes, i), (unsigned *)Vec_PtrEntry(p->vTtElems, i), p->nVars );
    // compute truth table for each node
    pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Abc_Lit2Var(pNtk->Root) );
    // complement the truth table if needed
    if ( Abc_LitIsCompl(pNtk->Root) )
        Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
    return pTruthRes;
}

void Kit_DsdTruthPartial	(	Kit_DsdMan_t *	p,
		Kit_DsdNtk_t *	pNtk,
		unsigned *	pTruthRes,
		unsigned	uSupp
	)

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

Synopsis [Derives the truth table of the DSD network.]

Description []

SideEffects []

SeeAlso []

Definition at line 1107 of file kitDsd.c.

{
    unsigned * pTruth = Kit_DsdTruthComputeOne( p, pNtk, uSupp );
    Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
/*
    // verification
    {
        // compute the same function using different procedure
        unsigned * pTruthTemp = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes + 1);
        pNtk->pSupps = NULL;
        Kit_DsdTruthComputeTwo( p, pNtk, uSupp, -1, pTruthTemp );
//        if ( !Kit_TruthIsEqual( pTruthTemp, pTruthRes, pNtk->nVars ) )
        if ( !Kit_TruthIsEqualWithPhase( pTruthTemp, pTruthRes, pNtk->nVars ) )
        {
            printf( "Verification FAILED!\n" );
            Kit_DsdPrint( stdout, pNtk );
            Kit_DsdPrintFromTruth( pTruthRes, pNtk->nVars );
            Kit_DsdPrintFromTruth( pTruthTemp, pNtk->nVars );
        }
//        else
//            printf( "Verification successful.\n" );
    }
*/
}

void Kit_DsdTruthPartialTwo	(	Kit_DsdMan_t *	p,
		Kit_DsdNtk_t *	pNtk,
		unsigned	uSupp,
		int	iVar,
		unsigned *	pTruthCo,
		unsigned *	pTruthDec
	)

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

Synopsis [Derives the truth table of the DSD network.]

Description []

SideEffects []

SeeAlso []

Definition at line 1089 of file kitDsd.c.

{
    unsigned * pTruth = Kit_DsdTruthComputeTwo( p, pNtk, uSupp, iVar, pTruthDec );
    if ( pTruthCo )
        Kit_TruthCopy( pTruthCo, pTruth, pNtk->nVars );
}

void Kit_DsdVerify	(	Kit_DsdNtk_t *	pNtk,
		unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Performs decomposition of the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 2492 of file kitDsd.c.

{
    Kit_DsdMan_t * p;
    unsigned * pTruthC;
    p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk)+2 );
    pTruthC = Kit_DsdTruthCompute( p, pNtk );
    if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
        printf( "Verification failed.\n" );
    Kit_DsdManFree( p );
}

void Kit_DsdWriteFromTruth	(	char *	pBuffer,
		unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 536 of file kitDsd.c.

{
    Kit_DsdNtk_t * pTemp, * pTemp2;
//    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 8 );
//    Kit_DsdPrintExpanded( pTemp );
    pTemp2 = Kit_DsdExpand( pTemp );
    Kit_DsdWrite( pBuffer, pTemp2 );
    Kit_DsdVerify( pTemp2, pTruth, nVars ); 
    Kit_DsdNtkFree( pTemp2 );
    Kit_DsdNtkFree( pTemp );
}

static Kit_Edge_t Kit_EdgeCreate ( int  Node, int  fCompl  )

inlinestatic

Definition at line 194 of file kit.h.

{ Kit_Edge_t eEdge = { fCompl, Node }; return eEdge;  }

static unsigned Kit_EdgeToInt ( Kit_Edge_t  eEdge )

inlinestatic

Definition at line 195 of file kit.h.

{ return (eEdge.Node << 1) | eEdge.fCompl;            }

static unsigned Kit_EdgeToInt_ ( Kit_Edge_t  m )

inlinestatic

Definition at line 199 of file kit.h.

{ union { Kit_Edge_t x; unsigned y; } v; v.x = m; return v.y;  }

Kit_Edge_t Kit_GraphAddNodeAnd	(	Kit_Graph_t *	pGraph,
		Kit_Edge_t	eEdge0,
		Kit_Edge_t	eEdge1
	)

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

Synopsis [Creates an AND node.]

Description []

SideEffects []

SeeAlso []

Definition at line 172 of file kitGraph.c.

{
    Kit_Node_t * pNode;
    // get the new node
    pNode = Kit_GraphAppendNode( pGraph );
    // set the inputs and other info
    pNode->eEdge0 = eEdge0;
    pNode->eEdge1 = eEdge1;
    pNode->fCompl0 = eEdge0.fCompl;
    pNode->fCompl1 = eEdge1.fCompl;
    return Kit_EdgeCreate( pGraph->nSize - 1, 0 );
}

Kit_Edge_t Kit_GraphAddNodeMux	(	Kit_Graph_t *	pGraph,
		Kit_Edge_t	eEdgeC,
		Kit_Edge_t	eEdgeT,
		Kit_Edge_t	eEdgeE,
		int	Type
	)

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

Synopsis [Creates an XOR node.]

Description []

SideEffects []

SeeAlso []

Definition at line 265 of file kitGraph.c.

{
    Kit_Edge_t eNode0, eNode1, eNode;
    if ( Type == 0 )
    {
        // derive the first AND
        eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
        // derive the second AND
        eEdgeC.fCompl ^= 1;
        eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
        // derive the final OR
        eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
    }
    else
    {
        // complement the arguments
        eEdgeT.fCompl ^= 1;
        eEdgeE.fCompl ^= 1;
        // derive the first AND
        eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
        // derive the second AND
        eEdgeC.fCompl ^= 1;
        eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
        // derive the final OR
        eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
        eNode.fCompl ^= 1;
    }
    return eNode;
}

Kit_Edge_t Kit_GraphAddNodeOr	(	Kit_Graph_t *	pGraph,
		Kit_Edge_t	eEdge0,
		Kit_Edge_t	eEdge1
	)

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

Synopsis [Creates an OR node.]

Description []

SideEffects []

SeeAlso []

Definition at line 196 of file kitGraph.c.

{
    Kit_Node_t * pNode;
    // get the new node
    pNode = Kit_GraphAppendNode( pGraph );
    // set the inputs and other info
    pNode->eEdge0 = eEdge0;
    pNode->eEdge1 = eEdge1;
    pNode->fCompl0 = eEdge0.fCompl;
    pNode->fCompl1 = eEdge1.fCompl;
    // make adjustments for the OR gate
    pNode->fNodeOr = 1;
    pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl;
    pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl;
    return Kit_EdgeCreate( pGraph->nSize - 1, 1 );
}

Kit_Edge_t Kit_GraphAddNodeXor	(	Kit_Graph_t *	pGraph,
		Kit_Edge_t	eEdge0,
		Kit_Edge_t	eEdge1,
		int	Type
	)

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

Synopsis [Creates an XOR node.]

Description []

SideEffects []

SeeAlso []

Definition at line 224 of file kitGraph.c.

{
    Kit_Edge_t eNode0, eNode1, eNode;
    if ( Type == 0 )
    {
        // derive the first AND
        eEdge0.fCompl ^= 1;
        eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
        eEdge0.fCompl ^= 1;
        // derive the second AND
        eEdge1.fCompl ^= 1;
        eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
        // derive the final OR
        eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
    }
    else
    {
        // derive the first AND
        eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
        // derive the second AND
        eEdge0.fCompl ^= 1;
        eEdge1.fCompl ^= 1;
        eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
        // derive the final OR
        eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
        eNode.fCompl ^= 1;
    }
    return eNode;
}

Kit_Node_t* Kit_GraphAppendNode

(

Kit_Graph_t *

pGraph

)

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

Synopsis [Appends a new node to the graph.]

Description [This procedure is meant for internal use.]

SideEffects []

SeeAlso []

Definition at line 148 of file kitGraph.c.

{
    Kit_Node_t * pNode;
    if ( pGraph->nSize == pGraph->nCap )
    {
        pGraph->pNodes = ABC_REALLOC( Kit_Node_t, pGraph->pNodes, 2 * pGraph->nCap ); 
        pGraph->nCap   = 2 * pGraph->nCap;
    }
    pNode = pGraph->pNodes + pGraph->nSize++;
    memset( pNode, 0, sizeof(Kit_Node_t) );
    return pNode;
}

static void Kit_GraphComplement ( Kit_Graph_t *  pGraph )

inlinestatic

Definition at line 207 of file kit.h.

{ pGraph->eRoot.fCompl ^= 1;                          }

Kit_Graph_t* Kit_GraphCreate

(

int

nLeaves

)

DECLARATIONS ///.

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

FileName [kitGraph.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Decomposition graph representation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 6, 2006.]

Revision [

Id:

kitGraph.c,v 1.00 2006/12/06 00:00:00 alanmi Exp

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

Synopsis [Creates a graph with the given number of leaves.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file kitGraph.c.

{
    Kit_Graph_t * pGraph;
    pGraph = ABC_ALLOC( Kit_Graph_t, 1 );
    memset( pGraph, 0, sizeof(Kit_Graph_t) );
    pGraph->nLeaves = nLeaves;
    pGraph->nSize = nLeaves;
    pGraph->nCap = 2 * nLeaves + 50;
    pGraph->pNodes = ABC_ALLOC( Kit_Node_t, pGraph->nCap );
    memset( pGraph->pNodes, 0, sizeof(Kit_Node_t) * pGraph->nSize );
    return pGraph;
}

Kit_Graph_t* Kit_GraphCreateConst0

(

)

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

Synopsis [Creates constant 0 graph.]

Description []

SideEffects []

SeeAlso []

Definition at line 69 of file kitGraph.c.

{
    Kit_Graph_t * pGraph;
    pGraph = ABC_ALLOC( Kit_Graph_t, 1 );
    memset( pGraph, 0, sizeof(Kit_Graph_t) );
    pGraph->fConst = 1;
    pGraph->eRoot.fCompl = 1;
    return pGraph;
}

Kit_Graph_t* Kit_GraphCreateConst1

(

)

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

Synopsis [Creates constant 1 graph.]

Description []

SideEffects []

SeeAlso []

Definition at line 90 of file kitGraph.c.

{
    Kit_Graph_t * pGraph;
    pGraph = ABC_ALLOC( Kit_Graph_t, 1 );
    memset( pGraph, 0, sizeof(Kit_Graph_t) );
    pGraph->fConst = 1;
    return pGraph;
}

Kit_Graph_t* Kit_GraphCreateLeaf	(	int	iLeaf,
		int	nLeaves,
		int	fCompl
	)

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

Synopsis [Creates the literal graph.]

Description []

SideEffects []

SeeAlso []

Definition at line 110 of file kitGraph.c.

{
    Kit_Graph_t * pGraph;
    assert( 0 <= iLeaf && iLeaf < nLeaves );
    pGraph = Kit_GraphCreate( nLeaves );
    pGraph->eRoot.Node   = iLeaf;
    pGraph->eRoot.fCompl = fCompl;
    return pGraph;
}

void Kit_GraphFree

(

Kit_Graph_t *

pGraph

)

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

Synopsis [Creates a graph with the given number of leaves.]

Description []

SideEffects []

SeeAlso []

Definition at line 131 of file kitGraph.c.

{
    ABC_FREE( pGraph->pNodes );
    ABC_FREE( pGraph );
}

static int Kit_GraphIsComplement ( Kit_Graph_t *  pGraph )

inlinestatic

Definition at line 205 of file kit.h.

{ return pGraph->eRoot.fCompl;                        }

static int Kit_GraphIsConst ( Kit_Graph_t *  pGraph )

inlinestatic

Definition at line 202 of file kit.h.

{ return pGraph->fConst;                              }

static int Kit_GraphIsConst0 ( Kit_Graph_t *  pGraph )

inlinestatic

Definition at line 203 of file kit.h.

{ return pGraph->fConst && pGraph->eRoot.fCompl;      }

static int Kit_GraphIsConst1 ( Kit_Graph_t *  pGraph )

inlinestatic

Definition at line 204 of file kit.h.

{ return pGraph->fConst && !pGraph->eRoot.fCompl;     }

static int Kit_GraphIsVar ( Kit_Graph_t *  pGraph )

inlinestatic

Definition at line 206 of file kit.h.

{ return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves; }

int Kit_GraphLeafDepth_rec	(	Kit_Graph_t *	pGraph,
		Kit_Node_t *	pNode,
		Kit_Node_t *	pLeaf
	)

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

Synopsis [Derives the maximum depth from the leaf to the root.]

Description []

SideEffects []

SeeAlso []

Definition at line 383 of file kitGraph.c.

{
    int Depth0, Depth1, Depth;
    if ( pNode == pLeaf )
        return 0;
    if ( Kit_GraphNodeIsVar(pGraph, pNode) )
        return -100;
    Depth0 = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeFanin0(pGraph, pNode), pLeaf );
    Depth1 = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeFanin1(pGraph, pNode), pLeaf );
    Depth = KIT_MAX( Depth0, Depth1 );
    Depth = (Depth == -100) ? -100 : Depth + 1;
    return Depth;
}

static int Kit_GraphLeaveNum ( Kit_Graph_t *  pGraph )

inlinestatic

Definition at line 209 of file kit.h.

{ return pGraph->nLeaves;                             }

static Kit_Node_t* Kit_GraphNode ( Kit_Graph_t *  pGraph, int  i  )

inlinestatic

Definition at line 211 of file kit.h.

{ return pGraph->pNodes + i;                          }

static Kit_Node_t* Kit_GraphNodeFanin0 ( Kit_Graph_t *  pGraph, Kit_Node_t *  pNode  )

inlinestatic

Definition at line 217 of file kit.h.

{ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.Node);     }

static Kit_Node_t* Kit_GraphNodeFanin1 ( Kit_Graph_t *  pGraph, Kit_Node_t *  pNode  )

inlinestatic

Definition at line 218 of file kit.h.

{ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.Node);     }

static int Kit_GraphNodeInt ( Kit_Graph_t *  pGraph, Kit_Node_t *  pNode  )

inlinestatic

Definition at line 213 of file kit.h.

{ return pNode - pGraph->pNodes;                      }

static int Kit_GraphNodeIsVar ( Kit_Graph_t *  pGraph, Kit_Node_t *  pNode  )

inlinestatic

Definition at line 214 of file kit.h.

{ return Kit_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; }

static Kit_Node_t* Kit_GraphNodeLast ( Kit_Graph_t *  pGraph )

inlinestatic

Definition at line 212 of file kit.h.

{ return pGraph->pNodes + pGraph->nSize - 1;          }

static int Kit_GraphNodeNum ( Kit_Graph_t *  pGraph )

inlinestatic

Definition at line 210 of file kit.h.

{ return pGraph->nSize - pGraph->nLeaves;             }

static int Kit_GraphRootLevel ( Kit_Graph_t *  pGraph )

inlinestatic

Definition at line 219 of file kit.h.

{ return Kit_GraphNode(pGraph, pGraph->eRoot.Node)->Level;                                        }

static void Kit_GraphSetRoot ( Kit_Graph_t *  pGraph, Kit_Edge_t  eRoot  )

inlinestatic

Definition at line 208 of file kit.h.

{ pGraph->eRoot = eRoot;                              }

DdNode* Kit_GraphToBdd	(	DdManager *	dd,
		Kit_Graph_t *	pGraph
	)

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

Synopsis [Converts graph to BDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file kitBdd.c.

{
    DdNode * bFunc, * bFunc0, * bFunc1;
    Kit_Node_t * pNode = NULL; // Suppress "might be used uninitialized"
    int i;

    // sanity checks
    assert( Kit_GraphLeaveNum(pGraph) >= 0 );
    assert( Kit_GraphLeaveNum(pGraph) <= pGraph->nSize );

    // check for constant function
    if ( Kit_GraphIsConst(pGraph) )
        return Cudd_NotCond( b1, Kit_GraphIsComplement(pGraph) );
    // check for a literal
    if ( Kit_GraphIsVar(pGraph) )
        return Cudd_NotCond( Cudd_bddIthVar(dd, Kit_GraphVarInt(pGraph)), Kit_GraphIsComplement(pGraph) );

    // assign the elementary variables
    Kit_GraphForEachLeaf( pGraph, pNode, i )
        pNode->pFunc = Cudd_bddIthVar( dd, i );

    // compute the function for each internal node
    Kit_GraphForEachNode( pGraph, pNode, i )
    {
        bFunc0 = Cudd_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
        bFunc1 = Cudd_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
        pNode->pFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( (DdNode *)pNode->pFunc );
    }

    // deref the intermediate results
    bFunc = (DdNode *)pNode->pFunc;   Cudd_Ref( bFunc );
    Kit_GraphForEachNode( pGraph, pNode, i )
        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pFunc );
    Cudd_Deref( bFunc );

    // complement the result if necessary
    return Cudd_NotCond( bFunc, Kit_GraphIsComplement(pGraph) );
}

unsigned Kit_GraphToTruth

(

Kit_Graph_t *

pGraph

)

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

Synopsis [Derives the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 306 of file kitGraph.c.

{
    unsigned uTruths[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
    unsigned uTruth = 0, uTruth0, uTruth1;
    Kit_Node_t * pNode;
    int i;

    // sanity checks
    assert( Kit_GraphLeaveNum(pGraph) >= 0 );
    assert( Kit_GraphLeaveNum(pGraph) <= pGraph->nSize );
    assert( Kit_GraphLeaveNum(pGraph) <= 5 );

    // check for constant function
    if ( Kit_GraphIsConst(pGraph) )
        return Kit_GraphIsComplement(pGraph)? 0 : ~((unsigned)0);
    // check for a literal
    if ( Kit_GraphIsVar(pGraph) )
        return Kit_GraphIsComplement(pGraph)? ~uTruths[Kit_GraphVarInt(pGraph)] : uTruths[Kit_GraphVarInt(pGraph)];

    // assign the elementary variables
    Kit_GraphForEachLeaf( pGraph, pNode, i )
        pNode->pFunc = (void *)(long)uTruths[i];

    // compute the function for each internal node
    Kit_GraphForEachNode( pGraph, pNode, i )
    {
        uTruth0 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc;
        uTruth1 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc;
        uTruth0 = pNode->eEdge0.fCompl? ~uTruth0 : uTruth0;
        uTruth1 = pNode->eEdge1.fCompl? ~uTruth1 : uTruth1;
        uTruth = uTruth0 & uTruth1;
        pNode->pFunc = (void *)(long)uTruth;
    }

    // complement the result if necessary
    return Kit_GraphIsComplement(pGraph)? ~uTruth : uTruth;
}

static Kit_Node_t* Kit_GraphVar ( Kit_Graph_t *  pGraph )

inlinestatic

Definition at line 215 of file kit.h.

{ assert( Kit_GraphIsVar( pGraph ) );    return Kit_GraphNode( pGraph, pGraph->eRoot.Node );      }

static int Kit_GraphVarInt ( Kit_Graph_t *  pGraph )

inlinestatic

Definition at line 216 of file kit.h.

{ assert( Kit_GraphIsVar( pGraph ) );    return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) ); }

static Kit_Edge_t Kit_IntToEdge ( unsigned  Edge )

inlinestatic

Definition at line 196 of file kit.h.

{ return Kit_EdgeCreate( Edge >> 1, Edge & 1 );       }

static Kit_Edge_t Kit_IntToEdge_ ( unsigned  m )

inlinestatic

Definition at line 200 of file kit.h.

{ union { Kit_Edge_t x; unsigned y; } v; v.y = m; return v.x;  }

void Kit_PlaComplement

(

char *

pSop

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 181 of file kitPla.c.

{
    char * pCur;
    for ( pCur = pSop; *pCur; pCur++ )
        if ( *pCur == '\n' )
        {
            if ( *(pCur - 1) == '0' )
                *(pCur - 1) = '1';
            else if ( *(pCur - 1) == '1' )
                *(pCur - 1) = '0';
            else if ( *(pCur - 1) == 'x' )
                *(pCur - 1) = 'n';
            else if ( *(pCur - 1) == 'n' )
                *(pCur - 1) = 'x';
            else
                assert( 0 );
        }
}

char* Kit_PlaCreateFromIsop	(	void *	p,
		int	nVars,
		Vec_Int_t *	vCover
	)

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

Synopsis [Creates the cover from the ISOP computed from TT.]

Description []

SideEffects []

SeeAlso []

Definition at line 243 of file kitPla.c.

{
    Aig_MmFlex_t * pMan = (Aig_MmFlex_t *)p;
    char * pSop, * pCube;
    int i, k, Entry, Literal;
    assert( Vec_IntSize(vCover) > 0 );
    if ( Vec_IntSize(vCover) == 0 )
        return NULL;
    // start the cover
    pSop = Kit_PlaStart( pMan, Vec_IntSize(vCover), nVars );
    // create cubes
    Vec_IntForEachEntry( vCover, Entry, i )
    {
        pCube = pSop + i * (nVars + 3);
        for ( k = 0; k < nVars; k++ )
        {
            Literal = 3 & (Entry >> (k << 1));
            if ( Literal == 1 )
                pCube[k] = '0';
            else if ( Literal == 2 )
                pCube[k] = '1';
            else if ( Literal != 0 )
                assert( 0 );
        }
    }
    return pSop;
}

char* Kit_PlaFromTruth	(	void *	p,
		unsigned *	pTruth,
		int	nVars,
		Vec_Int_t *	vCover
	)

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

Synopsis [Transforms truth table into the SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 337 of file kitPla.c.

{
    Aig_MmFlex_t * pMan = (Aig_MmFlex_t *)p;
    char * pSop;
    int RetValue;
    if ( Kit_TruthIsConst0(pTruth, nVars) )
        return Kit_PlaStoreSop( pMan, " 0\n" );
    if ( Kit_TruthIsConst1(pTruth, nVars) )
        return Kit_PlaStoreSop( pMan, " 1\n" );
    RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 0 ); // 1 );
    assert( RetValue == 0 || RetValue == 1 );
    pSop = Kit_PlaCreateFromIsop( pMan, nVars, vCover );
    if ( RetValue )
        Kit_PlaComplement( pSop );
    return pSop;
}

char* Kit_PlaFromTruthNew	(	unsigned *	pTruth,
		int	nVars,
		Vec_Int_t *	vCover,
		Vec_Str_t *	vStr
	)

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

Synopsis [Creates the SOP from TT.]

Description []

SideEffects []

SeeAlso []

Definition at line 406 of file kitPla.c.

{
    char * pResult;
    // transform truth table into the SOP
    int RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 1 );
    assert( RetValue == 0 || RetValue == 1 );
    // check the case of constant cover
    if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0) )
    {
        assert( RetValue == 0 );
        Vec_StrClear( vStr );
        Vec_StrAppend( vStr, (Vec_IntSize(vCover) == 0) ? " 0\n" : " 1\n" );
        Vec_StrPush( vStr, '\0' );
        return Vec_StrArray( vStr );
    }
    pResult = Kit_PlaFromIsop( vStr, nVars, vCover );
    if ( RetValue )
        Kit_PlaComplement( pResult );
    if ( nVars < 6 )
        assert( pTruth[0] == (unsigned)Kit_PlaToTruth6(pResult, nVars) );
    else if ( nVars == 6 )
        assert( *((ABC_UINT64_T*)pTruth) == Kit_PlaToTruth6(pResult, nVars) );
    return pResult;
}

int Kit_PlaGetCubeNum

(

char *

pSop

)

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

Synopsis [Reads the number of cubes in the cover.]

Description []

SideEffects []

SeeAlso []

Definition at line 138 of file kitPla.c.

{
    char * pCur;
    int nCubes = 0;
    if ( pSop == NULL )
        return 0;
    for ( pCur = pSop; *pCur; pCur++ )
        nCubes += (*pCur == '\n');
    return nCubes;
}

int Kit_PlaGetVarNum

(

char *

pSop

)

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

Synopsis [Reads the number of variables in the cover.]

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file kitPla.c.

{
    char * pCur;
    for ( pCur = pSop; *pCur != '\n'; pCur++ )
        if ( *pCur == 0 )
            return -1;
    return pCur - pSop - 2;
}

int Kit_PlaIsBuf

(

char *

pSop

)

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

Synopsis [Checks if the cover is a buffer.]

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file kitPla.c.

{
    if ( pSop[4] != 0 )
        return 0;
    if ( (pSop[0] == '1' && pSop[2] == '1') || (pSop[0] == '0' && pSop[2] == '0') )
        return 1;
    return 0;
}

int Kit_PlaIsComplement

(

char *

pSop

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 160 of file kitPla.c.

{
    char * pCur;
    for ( pCur = pSop; *pCur; pCur++ )
        if ( *pCur == '\n' )
            return (int)(*(pCur - 1) == '0' || *(pCur - 1) == 'n');
    assert( 0 );
    return 0;
}

int Kit_PlaIsConst0

(

char *

pSop

)

DECLARATIONS ///.

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

FileName [kitPla.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Manipulating SOP in the form of a C-string.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 6, 2006.]

Revision [

Id:

kitPla.c,v 1.00 2006/12/06 00:00:00 alanmi Exp

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

Synopsis [Checks if the cover is constant 0.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file kitPla.c.

{
    return pSop[0] == ' ' && pSop[1] == '0';
}

int Kit_PlaIsConst1

(

char *

pSop

)

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

Synopsis [Checks if the cover is constant 1.]

Description []

SideEffects []

SeeAlso []

Definition at line 62 of file kitPla.c.

{
    return pSop[0] == ' ' && pSop[1] == '1';
}

int Kit_PlaIsInv

(

char *

pSop

)

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

Synopsis [Checks if the cover is an inverter.]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file kitPla.c.

{
    if ( pSop[4] != 0 )
        return 0;
    if ( (pSop[0] == '0' && pSop[2] == '1') || (pSop[0] == '1' && pSop[2] == '0') )
        return 1;
    return 0;
}

char* Kit_PlaStart	(	void *	p,
		int	nCubes,
		int	nVars
	)

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

Synopsis [Creates the constant 1 cover with the given number of variables and cubes.]

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file kitPla.c.

{
    Aig_MmFlex_t * pMan = (Aig_MmFlex_t *)p;
    char * pSopCover, * pCube;
    int i, Length;

    Length = nCubes * (nVars + 3);
    pSopCover = Aig_MmFlexEntryFetch( pMan, Length + 1 );
    memset( pSopCover, '-', Length );
    pSopCover[Length] = 0;

    for ( i = 0; i < nCubes; i++ )
    {
        pCube = pSopCover + i * (nVars + 3);
        pCube[nVars + 0] = ' ';
        pCube[nVars + 1] = '1';
        pCube[nVars + 2] = '\n';
    }
    return pSopCover;
}

char* Kit_PlaStoreSop	(	void *	p,
		char *	pSop
	)

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

Synopsis [Allocates memory and copies the SOP into it.]

Description []

SideEffects []

SeeAlso []

Definition at line 317 of file kitPla.c.

{
    Aig_MmFlex_t * pMan = (Aig_MmFlex_t *)p;
    char * pStore;
    pStore = Aig_MmFlexEntryFetch( pMan, strlen(pSop) + 1 );
    strcpy( pStore, pSop );
    return pStore;
}

void Kit_PlaToIsop	(	char *	pSop,
		Vec_Int_t *	vCover
	)

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

Synopsis [Creates the cover from the ISOP computed from TT.]

Description []

SideEffects []

SeeAlso []

Definition at line 282 of file kitPla.c.

{
    char * pCube;
    int k, nVars, Entry;
    nVars = Kit_PlaGetVarNum( pSop );
    assert( nVars > 0 );
    // create cubes
    Vec_IntClear( vCover );
    for ( pCube = pSop; *pCube; pCube += nVars + 3 )
    {
        Entry = 0;
        for ( k = nVars - 1; k >= 0; k-- )
            if ( pCube[k] == '0' )
                Entry = (Entry << 2) | 1;
            else if ( pCube[k] == '1' )
                Entry = (Entry << 2) | 2;
            else if ( pCube[k] == '-' )
                Entry = (Entry << 2);
            else 
                assert( 0 );
        Vec_IntPush( vCover, Entry );
    }
}

void Kit_PlaToTruth	(	char *	pSop,
		int	nVars,
		Vec_Ptr_t *	vVars,
		unsigned *	pTemp,
		unsigned *	pTruth
	)

Fnction*************************************************************

Synopsis [Converting SOP into a truth table.]

Description [The SOP is represented as a C-string, as documented in file "bblif.h". The truth table is returned as a bit-string composed of 2^nVars bits. For functions of less than 6 variables, the full machine word is returned. (The truth table looks as if the function had 5 variables.) The use of this procedure should be limited to Boolean functions with no more than 16 inputs.]

SideEffects []

SeeAlso []

Definition at line 496 of file kitPla.c.

{
    int v, c, nCubes, fCompl = 0;
    assert( pSop != NULL );
    assert( nVars >= 0 );
    if ( strlen(pSop) % (nVars + 3) != 0 )
    {
        printf( "Kit_PlaToTruth(): SOP is represented incorrectly.\n" );
        return;
    }
    // iterate through the cubes
    Kit_TruthClear( pTruth, nVars );
    nCubes =  strlen(pSop) / (nVars + 3);
    for ( c = 0; c < nCubes; c++ )
    {
        fCompl = (pSop[nVars+1] == '0');
        Kit_TruthFill( pTemp, nVars );
        // iterate through the literals of the cube
        for ( v = 0; v < nVars; v++ )
            if ( pSop[v] == '1' )
                Kit_TruthAnd( pTemp, pTemp, (unsigned *)Vec_PtrEntry(vVars, v), nVars );
            else if ( pSop[v] == '0' )
                Kit_TruthSharp( pTemp, pTemp, (unsigned *)Vec_PtrEntry(vVars, v), nVars );
        // add cube to storage
        Kit_TruthOr( pTruth, pTruth, pTemp, nVars );
        // go to the next cube
        pSop += (nVars + 3);
    }
    if ( fCompl )
        Kit_TruthNot( pTruth, pTruth, nVars );
}

ABC_UINT64_T Kit_PlaToTruth6	(	char *	pSop,
		int	nVars
	)

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

Synopsis [Converts SOP into a truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 442 of file kitPla.c.

{
    static ABC_UINT64_T Truth[8] = {
        ABC_CONST(0xAAAAAAAAAAAAAAAA),
        ABC_CONST(0xCCCCCCCCCCCCCCCC),
        ABC_CONST(0xF0F0F0F0F0F0F0F0),
        ABC_CONST(0xFF00FF00FF00FF00),
        ABC_CONST(0xFFFF0000FFFF0000),
        ABC_CONST(0xFFFFFFFF00000000),
        ABC_CONST(0x0000000000000000),
        ABC_CONST(0xFFFFFFFFFFFFFFFF)
    };
    ABC_UINT64_T valueAnd, valueOr = Truth[6];
    int v, lit = 0;
    assert( nVars < 7 );
    do {
        valueAnd = Truth[7];
        for ( v = 0; v < nVars; v++, lit++ )
        {
            if ( pSop[lit] == '1' )
                valueAnd &=  Truth[v];
            else if ( pSop[lit] == '0' )
                valueAnd &= ~Truth[v];
            else if ( pSop[lit] != '-' )
                assert( 0 );
        }
        valueOr |= valueAnd;
        assert( pSop[lit] == ' ' );
        lit++;
        lit++;
        assert( pSop[lit] == '\n' );
        lit++;
    } while ( pSop[lit] );
    if ( Kit_PlaIsComplement(pSop) )
        valueOr = ~valueOr;
    return valueOr;
}

int Kit_SopAnyLiteral	(	Kit_Sop_t *	cSop,
		int	nLits
	)

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

Synopsis [Find any literal that occurs more than once.]

Description []

SideEffects []

SeeAlso []

Definition at line 370 of file kitSop.c.

{
    unsigned uCube;
    int i, k, nLitsCur;
    // go through each literal
    for ( i = 0; i < nLits; i++ )
    {
        // go through all the cubes
        nLitsCur = 0;
        Kit_SopForEachCube( cSop, uCube, k )
            if ( Kit_CubeHasLit(uCube, i) )
                nLitsCur++;
        if ( nLitsCur > 1 )
            return i;
    }
    return -1;
}

void Kit_SopBestLiteralCover	(	Kit_Sop_t *	cResult,
		Kit_Sop_t *	cSop,
		unsigned	uCube,
		int	nLits,
		Vec_Int_t *	vMemory
	)

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

Synopsis [Create the one-literal cover with the best literal from cSop.]

Description []

SideEffects []

SeeAlso []

Definition at line 560 of file kitSop.c.

{
    int iLitBest;
    // get the best literal
    iLitBest = Kit_SopBestLiteral( cSop, nLits, uCube );
    // start the cover
    cResult->nCubes = 0;
    cResult->pCubes = Vec_IntFetch( vMemory, 1 );
    // set the cube
    Kit_SopPushCube( cResult, Kit_CubeSetLit(0, iLitBest) );
}

void Kit_SopCommonCubeCover	(	Kit_Sop_t *	cResult,
		Kit_Sop_t *	cSop,
		Vec_Int_t *	vMemory
	)

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

Synopsis [Creates SOP composes of the common cube of the given SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file kitSop.c.

{
    assert( Kit_SopCubeNum(cSop) > 0 );
    cResult->nCubes = 0;
    cResult->pCubes = Vec_IntFetch( vMemory, 1 );
    Kit_SopPushCube( cResult, Kit_SopCommonCube(cSop) );
}

void Kit_SopCreate	(	Kit_Sop_t *	cResult,
		Vec_Int_t *	vInput,
		int	nVars,
		Vec_Int_t *	vMemory
	)

DECLARATIONS ///.

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

FileName [kitSop.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Procedures involving SOPs.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 6, 2006.]

Revision [

Id:

kitSop.c,v 1.00 2006/12/06 00:00:00 alanmi Exp

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

Synopsis [Creates SOP from the cube array.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file kitSop.c.

{
    unsigned uCube;
    int i;
    // start the cover
    cResult->nCubes = 0;
    cResult->pCubes = Vec_IntFetch( vMemory, Vec_IntSize(vInput) );
    // add the cubes
    Vec_IntForEachEntry( vInput, uCube, i )
        Kit_SopPushCube( cResult, uCube );
}

void Kit_SopCreateInverse	(	Kit_Sop_t *	cResult,
		Vec_Int_t *	vInput,
		int	nLits,
		Vec_Int_t *	vMemory
	)

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

Synopsis [Creates SOP from the cube array.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file kitSop.c.

{
    unsigned uCube, uMask = 0;
    int i, nCubes = Vec_IntSize(vInput);
    // start the cover
    cResult->nCubes = 0;
    cResult->pCubes = Vec_IntFetch( vMemory, nCubes );
    // add the cubes
//    Vec_IntForEachEntry( vInput, uCube, i )
    for ( i = 0; i < nCubes; i++ )
    {
        uCube = Vec_IntEntry( vInput, i );
        uMask = ((uCube | (uCube >> 1)) & 0x55555555);
        uMask |= (uMask << 1);
        Kit_SopPushCube( cResult, uCube ^ uMask );
    }
}

static unsigned Kit_SopCube ( Kit_Sop_t *  cSop, int  i  )

inlinestatic

Definition at line 189 of file kit.h.

{ return cSop->pCubes[i];                 }

static int Kit_SopCubeNum ( Kit_Sop_t *  cSop )

inlinestatic

Definition at line 188 of file kit.h.

{ return cSop->nCubes;                    }

void Kit_SopDivideByCube	(	Kit_Sop_t *	cSop,
		Kit_Sop_t *	cDiv,
		Kit_Sop_t *	vQuo,
		Kit_Sop_t *	vRem,
		Vec_Int_t *	vMemory
	)

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

Synopsis [Divides cover by one cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file kitSop.c.

{
    unsigned uCube, uDiv;
    int i;
    // get the only cube
    assert( Kit_SopCubeNum(cDiv) == 1 );
    uDiv = Kit_SopCube(cDiv, 0);
    // allocate covers
    vQuo->nCubes = 0;
    vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
    vRem->nCubes = 0;
    vRem->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
    // sort the cubes
    Kit_SopForEachCube( cSop, uCube, i )
    {
        if ( Kit_CubeContains( uCube, uDiv ) )
            Kit_SopPushCube( vQuo, Kit_CubeSharp(uCube, uDiv) );
        else
            Kit_SopPushCube( vRem, uCube );
    }
}

void Kit_SopDivideByLiteralQuo	(	Kit_Sop_t *	cSop,
		int	iLit
	)

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

Synopsis [Derives the quotient of division by literal.]

Description [Reduces the cover to be equal to the result of division of the given cover by the literal.]

SideEffects []

SeeAlso []

Definition at line 121 of file kitSop.c.

{
    unsigned uCube;
    int i, k = 0;
    Kit_SopForEachCube( cSop, uCube, i )
    {
        if ( Kit_CubeHasLit(uCube, iLit) )
            Kit_SopWriteCube( cSop, Kit_CubeRemLit(uCube, iLit), k++ );
    }
    Kit_SopShrink( cSop, k );
}

void Kit_SopDivideInternal	(	Kit_Sop_t *	cSop,
		Kit_Sop_t *	cDiv,
		Kit_Sop_t *	vQuo,
		Kit_Sop_t *	vRem,
		Vec_Int_t *	vMemory
	)

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

Synopsis [Divides cover by one cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file kitSop.c.

{
    unsigned uCube, uDiv;
    unsigned uCube2 = 0; // Suppress "might be used uninitialized"
    unsigned uDiv2, uQuo;
    int i, i2, k, k2, nCubesRem;
    assert( Kit_SopCubeNum(cSop) >= Kit_SopCubeNum(cDiv) );
    // consider special case
    if ( Kit_SopCubeNum(cDiv) == 1 )
    {
        Kit_SopDivideByCube( cSop, cDiv, vQuo, vRem, vMemory );
        return;
    }
    // allocate quotient
    vQuo->nCubes = 0;
    vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) / Kit_SopCubeNum(cDiv) );
    // for each cube of the cover
    // it either belongs to the quotient or to the remainder
    Kit_SopForEachCube( cSop, uCube, i )
    {
        // skip taken cubes
        if ( Kit_CubeIsMarked(uCube) )
            continue;
        // find a matching cube in the divisor
        uDiv = ~0;
        Kit_SopForEachCube( cDiv, uDiv, k )
            if ( Kit_CubeContains( uCube, uDiv ) )
                break;
        // the cube is not found 
        if ( k == Kit_SopCubeNum(cDiv) )
            continue;
        // the quotient cube exists
        uQuo = Kit_CubeSharp( uCube, uDiv );
        // find corresponding cubes for other cubes of the divisor
        uDiv2 = ~0;
        Kit_SopForEachCube( cDiv, uDiv2, k2 )
        {
            if ( k2 == k )
                continue;
            // find a matching cube
            Kit_SopForEachCube( cSop, uCube2, i2 )
            {
                // skip taken cubes
                if ( Kit_CubeIsMarked(uCube2) )
                    continue;
                // check if the cube can be used
                if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
                    break;
            }
            // the case when the cube is not found
            if ( i2 == Kit_SopCubeNum(cSop) )
                break;
        }
        // we did not find some cubes - continue looking at other cubes
        if ( k2 != Kit_SopCubeNum(cDiv) )
            continue;
        // we found all cubes - add the quotient cube
        Kit_SopPushCube( vQuo, uQuo );

        // mark the first cube
        Kit_SopWriteCube( cSop, Kit_CubeMark(uCube), i );
        // mark other cubes that have this quotient
        Kit_SopForEachCube( cDiv, uDiv2, k2 )
        {
            if ( k2 == k )
                continue;
            // find a matching cube
            Kit_SopForEachCube( cSop, uCube2, i2 )
            {
                // skip taken cubes
                if ( Kit_CubeIsMarked(uCube2) )
                    continue;
                // check if the cube can be used
                if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
                    break;
            }
            assert( i2 < Kit_SopCubeNum(cSop) );
            // the cube is found, mark it 
            // (later we will add all unmarked cubes to the remainder)
            Kit_SopWriteCube( cSop, Kit_CubeMark(uCube2), i2 );
        }
    }
    // determine the number of cubes in the remainder
    nCubesRem = Kit_SopCubeNum(cSop) - Kit_SopCubeNum(vQuo) * Kit_SopCubeNum(cDiv);
    // allocate remainder
    vRem->nCubes = 0;
    vRem->pCubes = Vec_IntFetch( vMemory, nCubesRem );
    // finally add the remaining unmarked cubes to the remainder 
    // and clean the marked cubes in the cover
    Kit_SopForEachCube( cSop, uCube, i )
    {
        if ( !Kit_CubeIsMarked(uCube) )
        {
            Kit_SopPushCube( vRem, uCube );
            continue;
        }
        Kit_SopWriteCube( cSop, Kit_CubeUnmark(uCube), i );
    }
    assert( nCubesRem == Kit_SopCubeNum(vRem) );
}

int Kit_SopDivisor	(	Kit_Sop_t *	cResult,
		Kit_Sop_t *	cSop,
		int	nLits,
		Vec_Int_t *	vMemory
	)

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

Synopsis [Computes the quick divisor of the cover.]

Description [Returns 0, if there is no divisor other than trivial.]

SideEffects []

SeeAlso []

Definition at line 534 of file kitSop.c.

{
    if ( Kit_SopCubeNum(cSop) <= 1 )
        return 0;
    if ( Kit_SopAnyLiteral( cSop, nLits ) == -1 )
        return 0;
    // duplicate the cover
    Kit_SopDup( cResult, cSop, vMemory );
    // perform the kerneling
    Kit_SopDivisorZeroKernel_rec( cResult, nLits );
    assert( Kit_SopCubeNum(cResult) > 0 );
    return 1;
}

void Kit_SopDup	(	Kit_Sop_t *	cResult,
		Kit_Sop_t *	cSop,
		Vec_Int_t *	vMemory
	)

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

Synopsis [Duplicates SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file kitSop.c.

{
    unsigned uCube;
    int i;
    // start the cover
    cResult->nCubes = 0;
    cResult->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
    // add the cubes
    Kit_SopForEachCube( cSop, uCube, i )
        Kit_SopPushCube( cResult, uCube );
}

Kit_Graph_t* Kit_SopFactor	(	Vec_Int_t *	vCover,
		int	fCompl,
		int	nVars,
		Vec_Int_t *	vMemory
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Factors the cover.]

Description []

SideEffects []

SeeAlso []

Definition at line 55 of file kitFactor.c.

{
    Kit_Sop_t Sop, * cSop = &Sop;
    Kit_Graph_t * pFForm;
    Kit_Edge_t eRoot;
//    int nCubes;

    // works for up to 15 variables because division procedure
    // used the last bit for marking the cubes going to the remainder
    assert( nVars < 16 );

    // check for trivial functions
    if ( Vec_IntSize(vCover) == 0 )
        return Kit_GraphCreateConst0();
    if ( Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0 )
        return Kit_GraphCreateConst1();

    // prepare memory manager
//    Vec_IntClear( vMemory );
    Vec_IntGrow( vMemory, KIT_FACTOR_MEM_LIMIT );

    // perform CST
    Kit_SopCreateInverse( cSop, vCover, 2 * nVars, vMemory ); // CST

    // start the factored form
    pFForm = Kit_GraphCreate( nVars );
    // factor the cover
    eRoot = Kit_SopFactor_rec( pFForm, cSop, 2 * nVars, vMemory );
    // finalize the factored form
    Kit_GraphSetRoot( pFForm, eRoot );
    if ( fCompl )
        Kit_GraphComplement( pFForm );

    // verify the factored form
//    nCubes = Vec_IntSize(vCover);
//    Vec_IntShrink( vCover, nCubes );
//    if ( !Kit_SopFactorVerify( vCover, pFForm, nVars ) )
//        printf( "Verification has failed.\n" );
    return pFForm;
}

int Kit_SopIsCubeFree

(

Kit_Sop_t *

cSop

)

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

Synopsis [Checks if the cover is cube-free.]

Description []

SideEffects []

SeeAlso []

Definition at line 334 of file kitSop.c.

{
    return Kit_SopCommonCube( cSop ) == 0;
}

void Kit_SopMakeCubeFree

(

Kit_Sop_t *

cSop

)

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

Synopsis [Makes the cover cube-free.]

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file kitSop.c.

{
    unsigned uMask, uCube;
    int i;
    uMask = Kit_SopCommonCube( cSop );
    if ( uMask == 0 )
        return;
    // remove the common cube
    Kit_SopForEachCube( cSop, uCube, i )
        Kit_SopWriteCube( cSop, Kit_CubeSharp(uCube, uMask), i );
}

static void Kit_SopPushCube ( Kit_Sop_t *  cSop, unsigned  uCube  )

inlinestatic

Definition at line 191 of file kit.h.

{ cSop->pCubes[cSop->nCubes++] = uCube;   }

static void Kit_SopShrink ( Kit_Sop_t *  cSop, int  nCubesNew  )

inlinestatic

Definition at line 190 of file kit.h.

{ cSop->nCubes = nCubesNew;               }

DdNode* Kit_SopToBdd	(	DdManager *	dd,
		Kit_Sop_t *	cSop,
		int	nVars
	)

FUNCTION DECLARATIONS ///.

FUNCTION DECLARATIONS ///.

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

FileName [kitBdd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Procedures involving BDDs.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 6, 2006.]

Revision [

Id:

kitBdd.c,v 1.00 2006/12/06 00:00:00 alanmi Exp

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

Synopsis [Derives the BDD for the given SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file kitBdd.c.

{
    DdNode * bSum, * bCube, * bTemp, * bVar;
    unsigned uCube;
    int Value, i, v;
    assert( nVars < 16 );
    // start the cover
    bSum = Cudd_ReadLogicZero(dd);   Cudd_Ref( bSum );
   // check the logic function of the node
    Kit_SopForEachCube( cSop, uCube, i )
    {
        bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
        for ( v = 0; v < nVars; v++ )
        {
            Value = ((uCube >> 2*v) & 3);
            if ( Value == 1 )
                bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
            else if ( Value == 2 )
                bVar = Cudd_bddIthVar( dd, v );
            else
                continue;
            bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
            Cudd_RecursiveDeref( dd, bTemp );
        }
        bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );   
        Cudd_Ref( bSum );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bCube );
    }
    // complement the result if necessary
    Cudd_Deref( bSum );
    return bSum;
}

static void Kit_SopWriteCube ( Kit_Sop_t *  cSop, unsigned  uCube, int  i  )

inlinestatic

Definition at line 192 of file kit.h.

{ cSop->pCubes[i] = uCube;                }

static int Kit_SuppIsMinBase ( int  Supp )

inlinestatic

Definition at line 221 of file kit.h.

{ return (Supp & (Supp+1)) == 0;                      }

static void Kit_TruthAnd ( unsigned *  pOut, unsigned *  pIn0, unsigned *  pIn1, int  nVars  )

inlinestatic

Definition at line 379 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = pIn0[w] & pIn1[w];
}

static void Kit_TruthAndPhase ( unsigned *  pOut, unsigned *  pIn0, unsigned *  pIn1, int  nVars, int  fCompl0, int  fCompl1  )

inlinestatic

Definition at line 409 of file kit.h.

{
    int w;
    if ( fCompl0 && fCompl1 )
    {
        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
            pOut[w] = ~(pIn0[w] | pIn1[w]);
    }
    else if ( fCompl0 && !fCompl1 )
    {
        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
            pOut[w] = ~pIn0[w] & pIn1[w];
    }
    else if ( !fCompl0 && fCompl1 )
    {
        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
            pOut[w] = pIn0[w] & ~pIn1[w];
    }
    else // if ( !fCompl0 && !fCompl1 )
    {
        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
            pOut[w] = pIn0[w] & pIn1[w];
    }
}

int Kit_TruthBestCofVar	(	unsigned *	pTruth,
		int	nVars,
		unsigned *	pCof0,
		unsigned *	pCof1
	)

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

Synopsis [Find the best cofactoring variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 1365 of file kitTruth.c.

{
    int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
    if ( Kit_TruthIsConst0(pTruth, nVars) || Kit_TruthIsConst1(pTruth, nVars) )
        return -1;
    // iterate through variables
    iBestVar = -1;
    nSuppSizeMin = KIT_INFINITY;
    for ( i = 0; i < nVars; i++ )
    {
        // cofactor the functiona and get support sizes
        Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
        Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
        nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
        nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
        nSuppSizeCur  = nSuppSizeCur0 + nSuppSizeCur1;
        // compare this variable with other variables
        if ( nSuppSizeMin > nSuppSizeCur ) 
        {
            nSuppSizeMin = nSuppSizeCur;
            iBestVar = i;
        }
    }
    assert( iBestVar != -1 );
    // cofactor w.r.t. this variable
    Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
    Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
    return iBestVar;
}

void Kit_TruthChangePhase	(	unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Changes phase of the function w.r.t. one variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 1259 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step;
    unsigned Temp;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = ((pTruth[i] & 0x55555555) << 1) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = ((pTruth[i] & 0x33333333) << 2) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = ((pTruth[i] & 0x0F0F0F0F) << 4) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = ((pTruth[i] & 0x00FF00FF) << 8) | ((pTruth[i] & 0xFF00FF00) >> 8);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = ((pTruth[i] & 0x0000FFFF) << 16) | ((pTruth[i] & 0xFFFF0000) >> 16);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
            {
                Temp = pTruth[i];
                pTruth[i] = pTruth[Step+i];
                pTruth[Step+i] = Temp;
            }
            pTruth += 2*Step;
        }
        return;
    }
}

static void Kit_TruthClear ( unsigned *  pOut, int  nVars  )

inlinestatic

Definition at line 361 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = 0;
}

void Kit_TruthCofactor0	(	unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 368 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
                pTruth[Step+i] = pTruth[i];
            pTruth += 2*Step;
        }
        return;
    }
}

void Kit_TruthCofactor0New	(	unsigned *	pOut,
		unsigned *	pIn,
		int	nVars,
		int	iVar
	)

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 521 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pIn[i] & 0x55555555) | ((pIn[i] & 0x55555555) << 1);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pIn[i] & 0x33333333) | ((pIn[i] & 0x33333333) << 2);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pIn[i] & 0x0F0F0F0F) | ((pIn[i] & 0x0F0F0F0F) << 4);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pIn[i] & 0x00FF00FF) | ((pIn[i] & 0x00FF00FF) << 8);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i] & 0x0000FFFF) << 16);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
                pOut[i] = pOut[Step+i] = pIn[i];
            pIn += 2*Step;
            pOut += 2*Step;
        }
        return;
    }
}

void Kit_TruthCofactor1	(	unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 470 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0xAAAAAAAA) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0xCCCCCCCC) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0xF0F0F0F0) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0xFF00FF00) | ((pTruth[i] & 0xFF00FF00) >> 8);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] = (pTruth[i] & 0xFFFF0000) | ((pTruth[i] & 0xFFFF0000) >> 16);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
                pTruth[i] = pTruth[Step+i];
            pTruth += 2*Step;
        }
        return;
    }
}

void Kit_TruthCofactor1New	(	unsigned *	pOut,
		unsigned *	pIn,
		int	nVars,
		int	iVar
	)

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 573 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pIn[i] & 0xAAAAAAAA) | ((pIn[i] & 0xAAAAAAAA) >> 1);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pIn[i] & 0xCCCCCCCC) | ((pIn[i] & 0xCCCCCCCC) >> 2);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pIn[i] & 0xF0F0F0F0) | ((pIn[i] & 0xF0F0F0F0) >> 4);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pIn[i] & 0xFF00FF00) | ((pIn[i] & 0xFF00FF00) >> 8);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pIn[i] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
                pOut[i] = pOut[Step+i] = pIn[Step+i];
            pIn += 2*Step;
            pOut += 2*Step;
        }
        return;
    }
}

void Kit_TruthCofSupports	(	Vec_Int_t *	vBddDir,
		Vec_Int_t *	vBddInv,
		int	nVars,
		Vec_Int_t *	vMemory,
		unsigned *	puSupps
	)

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

Synopsis [Compute BDD for the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 310 of file kitCloud.c.

{
    Kit_Mux_t Mux;
    unsigned * puSuppAll;
    unsigned * pThis = NULL; // Suppress "might be used uninitialized"
    unsigned * pFan0, * pFan1;
    int i, v, Var, Entry, nSupps;
    nSupps = 2 * nVars;

    // extend storage
    if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddDir) )
        Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddDir) );
    puSuppAll = (unsigned *)Vec_IntArray( vMemory );
    // clear storage for the const node
    memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
    // compute supports from nodes
    Vec_IntForEachEntryStart( vBddDir, Entry, i, 1 )
    {
        Mux = Kit_Int2Mux(Entry);
        Var = nVars - 1 - Mux.v;
        pFan0 = puSuppAll + nSupps * Mux.e;
        pFan1 = puSuppAll + nSupps * Mux.t;
        pThis = puSuppAll + nSupps * i;
        for ( v = 0; v < nSupps; v++ )
            pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
        assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
        assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
        pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
        pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
    }
    // copy the result
    memcpy( puSupps, pThis, sizeof(unsigned) * nSupps );
    // compute the inverse

    // extend storage
    if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddInv) )
        Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddInv) );
    puSuppAll = (unsigned *)Vec_IntArray( vMemory );
    // clear storage for the const node
    memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
    // compute supports from nodes
    Vec_IntForEachEntryStart( vBddInv, Entry, i, 1 )
    {
        Mux = Kit_Int2Mux(Entry);
//        Var = nVars - 1 - Mux.v;
        Var = Mux.v;
        pFan0 = puSuppAll + nSupps * Mux.e;
        pFan1 = puSuppAll + nSupps * Mux.t;
        pThis = puSuppAll + nSupps * i;
        for ( v = 0; v < nSupps; v++ )
            pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
        assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
        assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
        pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
        pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
    }

    // merge supports
    for ( Var = 0; Var < nSupps; Var++ )
        puSupps[Var] = (puSupps[Var] & Kit_BitMask(Var/2)) | (pThis[Var] & ~Kit_BitMask(Var/2));
}

unsigned* Kit_TruthCompose	(	CloudManager *	dd,
		unsigned *	pTruth,
		int	nVars,
		unsigned **	pInputs,
		int	nVarsAll,
		Vec_Ptr_t *	vStore,
		Vec_Int_t *	vNodes
	)

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

Synopsis [Computes composition of truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 263 of file kitCloud.c.

{
    CloudNode * pFunc;
    unsigned * pThis, * pFan0, * pFan1;
    Kit_Mux_t Mux;
    int i, Entry, RetValue;
    // derive BDD from truth table
    Cloud_Restart( dd );
    pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
    // convert it into nodes
    RetValue = Kit_CreateCloud( dd, pFunc, vNodes );
    if ( RetValue == 0 )
        printf( "Kit_TruthCompose(): Internal failure!!!\n" );
    // verify the result
//    pFan0 = Kit_CloudToTruth( vNodes, nVars, vStore, 0 );
//    if ( !Kit_TruthIsEqual( pTruth, pFan0, nVars ) )
//        printf( "Failed!\n" );
    // compute truth table from the BDD
    assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
    pThis = (unsigned *)Vec_PtrEntry( vStore, 0 );
    Kit_TruthFill( pThis, nVarsAll );
    Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
    {
        Mux = Kit_Int2Mux(Entry);
        pFan0 = (unsigned *)Vec_PtrEntry( vStore, Mux.e );
        pFan1 = (unsigned *)Vec_PtrEntry( vStore, Mux.t );
        pThis = (unsigned *)Vec_PtrEntry( vStore, i );
        Kit_TruthMuxPhase( pThis, pFan0, pFan1, pInputs[nVars-1-Mux.v], nVarsAll, Mux.c );
    }
    // complement the result
    if ( Mux.i )
        Kit_TruthNot( pThis, pThis, nVarsAll );
    return pThis;
}

static void Kit_TruthCopy ( unsigned *  pOut, unsigned *  pIn, int  nVars  )

inlinestatic

Definition at line 355 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = pIn[w];
}

static int Kit_TruthCountOnes ( unsigned *  pIn, int  nVars  )

inlinestatic

Definition at line 251 of file kit.h.

{
    int w, Counter = 0;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        Counter += Kit_WordCountOnes(pIn[w]);
    return Counter;
}

void Kit_TruthCountOnesInCofs	(	unsigned *	pTruth,
		int	nVars,
		int *	pStore
	)

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

Synopsis [Counts the number of 1's in each cofactor.]

Description [The resulting numbers are stored in the array of ints, whose length is 2*nVars. The number of 1's is counted in a different space than the original function. For example, if the function depends on k variables, the cofactors are assumed to depend on k-1 variables.]

SideEffects []

SeeAlso []

Definition at line 1410 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Counter;
    memset( pStore, 0, sizeof(int) * 2 * nVars );
    if ( nVars <= 5 )
    {
        if ( nVars > 0 )
        {
            pStore[2*0+0] = Kit_WordCountOnes( pTruth[0] & 0x55555555 );
            pStore[2*0+1] = Kit_WordCountOnes( pTruth[0] & 0xAAAAAAAA );
        }
        if ( nVars > 1 )
        {
            pStore[2*1+0] = Kit_WordCountOnes( pTruth[0] & 0x33333333 );
            pStore[2*1+1] = Kit_WordCountOnes( pTruth[0] & 0xCCCCCCCC );
        }
        if ( nVars > 2 )
        {
            pStore[2*2+0] = Kit_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
            pStore[2*2+1] = Kit_WordCountOnes( pTruth[0] & 0xF0F0F0F0 );
        }
        if ( nVars > 3 )
        {
            pStore[2*3+0] = Kit_WordCountOnes( pTruth[0] & 0x00FF00FF );
            pStore[2*3+1] = Kit_WordCountOnes( pTruth[0] & 0xFF00FF00 );
        }
        if ( nVars > 4 )
        {
            pStore[2*4+0] = Kit_WordCountOnes( pTruth[0] & 0x0000FFFF );
            pStore[2*4+1] = Kit_WordCountOnes( pTruth[0] & 0xFFFF0000 );
        }
        return;
    }
    // nVars >= 6
    // count 1's for all other variables
    for ( k = 0; k < nWords; k++ )
    {
        Counter = Kit_WordCountOnes( pTruth[k] );
        for ( i = 5; i < nVars; i++ )
            if ( k & (1 << (i-5)) )
                pStore[2*i+1] += Counter;
            else
                pStore[2*i+0] += Counter;
    }
    // count 1's for the first five variables
    for ( k = 0; k < nWords/2; k++ )
    {
        pStore[2*0+0] += Kit_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) <<  1) );
        pStore[2*0+1] += Kit_WordCountOnes( (pTruth[0] & 0xAAAAAAAA) | ((pTruth[1] & 0xAAAAAAAA) >>  1) );
        pStore[2*1+0] += Kit_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) <<  2) );
        pStore[2*1+1] += Kit_WordCountOnes( (pTruth[0] & 0xCCCCCCCC) | ((pTruth[1] & 0xCCCCCCCC) >>  2) );
        pStore[2*2+0] += Kit_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) <<  4) );
        pStore[2*2+1] += Kit_WordCountOnes( (pTruth[0] & 0xF0F0F0F0) | ((pTruth[1] & 0xF0F0F0F0) >>  4) );
        pStore[2*3+0] += Kit_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) <<  8) );
        pStore[2*3+1] += Kit_WordCountOnes( (pTruth[0] & 0xFF00FF00) | ((pTruth[1] & 0xFF00FF00) >>  8) );
        pStore[2*4+0] += Kit_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
        pStore[2*4+1] += Kit_WordCountOnes( (pTruth[0] & 0xFFFF0000) | ((pTruth[1] & 0xFFFF0000) >> 16) );
        pTruth += 2;
    }
}

void Kit_TruthCountOnesInCofs0	(	unsigned *	pTruth,
		int	nVars,
		int *	pStore
	)

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

Synopsis [Counts the number of 1's in each negative cofactor.]

Description [The resulting numbers are stored in the array of ints, whose length is nVars. The number of 1's is counted in a different space than the original function. For example, if the function depends on k variables, the cofactors are assumed to depend on k-1 variables.]

SideEffects []

SeeAlso []

Definition at line 1486 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Counter;
    memset( pStore, 0, sizeof(int) * nVars );
    if ( nVars <= 5 )
    {
        if ( nVars > 0 )
            pStore[0] = Kit_WordCountOnes( pTruth[0] & 0x55555555 );
        if ( nVars > 1 )
            pStore[1] = Kit_WordCountOnes( pTruth[0] & 0x33333333 );
        if ( nVars > 2 )
            pStore[2] = Kit_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
        if ( nVars > 3 )
            pStore[3] = Kit_WordCountOnes( pTruth[0] & 0x00FF00FF );
        if ( nVars > 4 )
            pStore[4] = Kit_WordCountOnes( pTruth[0] & 0x0000FFFF );
        return;
    }
    // nVars >= 6
    // count 1's for all other variables
    for ( k = 0; k < nWords; k++ )
    {
        Counter = Kit_WordCountOnes( pTruth[k] );
        for ( i = 5; i < nVars; i++ )
            if ( (k & (1 << (i-5))) == 0 )
                pStore[i] += Counter;
    }
    // count 1's for the first five variables
    for ( k = 0; k < nWords/2; k++ )
    {
        pStore[0] += Kit_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) <<  1) );
        pStore[1] += Kit_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) <<  2) );
        pStore[2] += Kit_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) <<  4) );
        pStore[3] += Kit_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) <<  8) );
        pStore[4] += Kit_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
        pTruth += 2;
    }
}

void Kit_TruthCountOnesInCofsSlow	(	unsigned *	pTruth,
		int	nVars,
		int *	pStore,
		unsigned *	pAux
	)

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

Synopsis [Counts the number of 1's in each cofactor.]

Description [Verifies the above procedure.]

SideEffects []

SeeAlso []

Definition at line 1537 of file kitTruth.c.

{
    int i;
    for ( i = 0; i < nVars; i++ )
    {
        Kit_TruthCofactor0New( pAux, pTruth, nVars, i );
        pStore[2*i+0] = Kit_TruthCountOnes( pAux, nVars ) / 2;
        Kit_TruthCofactor1New( pAux, pTruth, nVars, i );
        pStore[2*i+1] = Kit_TruthCountOnes( pAux, nVars ) / 2;
    }
}

char* Kit_TruthDumpToFile	(	unsigned *	pTruth,
		int	nVars,
		int	nFile
	)

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

Synopsis [Dumps truth table into a file.]

Description [Generates script file for reading into ABC.]

SideEffects []

SeeAlso []

Definition at line 2004 of file kitTruth.c.

{
    static char pFileName[100];
    FILE * pFile;
    sprintf( pFileName, "tt\\s%04d", nFile );
    pFile = fopen( pFileName, "w" );
    fprintf( pFile, "rt " );
    Kit_PrintHexadecimal( pFile, pTruth, nVars );
    fprintf( pFile, "; bdd; sop; ps\n" );
    fclose( pFile );
    return pFileName;
}

void Kit_TruthExist	(	unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 684 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] |=  ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] |=  ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] |=  ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] |=  ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] |=  ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
            {
                pTruth[i]     |= pTruth[Step+i];
                pTruth[Step+i] = pTruth[i];
            }
            pTruth += 2*Step;
        }
        return;
    }
}

void Kit_TruthExistNew	(	unsigned *	pRes,
		unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 738 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] | ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] | ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] | ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] | ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] | ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
            {
                pRes[i]      = pTruth[i] | pTruth[Step+i];
                pRes[Step+i] = pRes[i];
            }
            pRes += 2*Step;
            pTruth += 2*Step;
        }
        return;
    }
}

void Kit_TruthExistSet	(	unsigned *	pRes,
		unsigned *	pTruth,
		int	nVars,
		unsigned	uMask
	)

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

Synopsis [Existantially quantifies the set of variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 793 of file kitTruth.c.

{
    int v;
    Kit_TruthCopy( pRes, pTruth, nVars );
    for ( v = 0; v < nVars; v++ )
        if ( uMask & (1 << v) )
            Kit_TruthExist( pRes, nVars, v );
}

static void Kit_TruthFill ( unsigned *  pOut, int  nVars  )

inlinestatic

Definition at line 367 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = ~(unsigned)0;
}

static int Kit_TruthFindFirstBit ( unsigned *  pIn, int  nVars  )

inlinestatic

Definition at line 258 of file kit.h.

{
    int w;
    for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
        if ( pIn[w] )
            return 32*w + Kit_WordFindFirstBit(pIn[w]);
    return -1;
}

static int Kit_TruthFindFirstZero ( unsigned *  pIn, int  nVars  )

inlinestatic

Definition at line 266 of file kit.h.

{
    int w;
    for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
        if ( ~pIn[w] )
            return 32*w + Kit_WordFindFirstBit(~pIn[w]);
    return -1;
}

void Kit_TruthForall	(	unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Unversally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 813 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] &=  ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] &=  ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] &=  ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] &=  ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pTruth[i] &=  ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
            {
                pTruth[i]     &= pTruth[Step+i];
                pTruth[Step+i] = pTruth[i];
            }
            pTruth += 2*Step;
        }
        return;
    }
}

void Kit_TruthForallNew	(	unsigned *	pRes,
		unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Universally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 867 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] & (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] & (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] & (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] & (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] & (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
            {
                pRes[i]      = pTruth[i] & pTruth[Step+i];
                pRes[Step+i] = pRes[i];
            }
            pRes += 2*Step;
            pTruth += 2*Step;
        }
        return;
    }
}

void Kit_TruthForallSet	(	unsigned *	pRes,
		unsigned *	pTruth,
		int	nVars,
		unsigned	uMask
	)

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

Synopsis [Universally quantifies the set of variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 1048 of file kitTruth.c.

{
    int v;
    Kit_TruthCopy( pRes, pTruth, nVars );
    for ( v = 0; v < nVars; v++ )
        if ( uMask & (1 << v) )
            Kit_TruthForall( pRes, nVars, v );
}

static int Kit_TruthHasBit ( unsigned *  p, int  Bit  )

inlinestatic

Definition at line 229 of file kit.h.

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

unsigned Kit_TruthHash	(	unsigned *	pIn,
		int	nWords
	)

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

Synopsis [Canonicize the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 1560 of file kitTruth.c.

{
    // The 1,024 smallest prime numbers used to compute the hash value
    // http://www.math.utah.edu/~alfeld/math/primelist.html
    static int HashPrimes[1024] = { 2, 3, 5, 
    7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97, 
    101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151, 157, 163, 167, 173, 179, 181, 191, 
    193, 197, 199, 211, 223, 227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281, 283, 
    293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359, 367, 373, 379, 383, 389, 397, 401, 
    409, 419, 421, 431, 433, 439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503, 509, 
    521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593, 599, 601, 607, 613, 617, 619, 631, 
    641, 643, 647, 653, 659, 661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743, 751, 
    757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827, 829, 839, 853, 857, 859, 863, 877, 
    881, 883, 887, 907, 911, 919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997, 
    1009, 1013, 1019, 1021, 1031, 1033, 1039, 1049, 1051, 1061, 1063, 1069, 1087, 1091, 
    1093, 1097, 1103, 1109, 1117, 1123, 1129, 1151, 1153, 1163, 1171, 1181, 1187, 1193, 
    1201, 1213, 1217, 1223, 1229, 1231, 1237, 1249, 1259, 1277, 1279, 1283, 1289, 1291, 
    1297, 1301, 1303, 1307, 1319, 1321, 1327, 1361, 1367, 1373, 1381, 1399, 1409, 1423, 
    1427, 1429, 1433, 1439, 1447, 1451, 1453, 1459, 1471, 1481, 1483, 1487, 1489, 1493, 
    1499, 1511, 1523, 1531, 1543, 1549, 1553, 1559, 1567, 1571, 1579, 1583, 1597, 1601, 
    1607, 1609, 1613, 1619, 1621, 1627, 1637, 1657, 1663, 1667, 1669, 1693, 1697, 1699, 
    1709, 1721, 1723, 1733, 1741, 1747, 1753, 1759, 1777, 1783, 1787, 1789, 1801, 1811, 
    1823, 1831, 1847, 1861, 1867, 1871, 1873, 1877, 1879, 1889, 1901, 1907, 1913, 1931, 
    1933, 1949, 1951, 1973, 1979, 1987, 1993, 1997, 1999, 2003, 2011, 2017, 2027, 2029, 
    2039, 2053, 2063, 2069, 2081, 2083, 2087, 2089, 2099, 2111, 2113, 2129, 2131, 2137, 
    2141, 2143, 2153, 2161, 2179, 2203, 2207, 2213, 2221, 2237, 2239, 2243, 2251, 2267, 
    2269, 2273, 2281, 2287, 2293, 2297, 2309, 2311, 2333, 2339, 2341, 2347, 2351, 2357, 
    2371, 2377, 2381, 2383, 2389, 2393, 2399, 2411, 2417, 2423, 2437, 2441, 2447, 2459, 
    2467, 2473, 2477, 2503, 2521, 2531, 2539, 2543, 2549, 2551, 2557, 2579, 2591, 2593, 
    2609, 2617, 2621, 2633, 2647, 2657, 2659, 2663, 2671, 2677, 2683, 2687, 2689, 2693, 
    2699, 2707, 2711, 2713, 2719, 2729, 2731, 2741, 2749, 2753, 2767, 2777, 2789, 2791, 
    2797, 2801, 2803, 2819, 2833, 2837, 2843, 2851, 2857, 2861, 2879, 2887, 2897, 2903, 
    2909, 2917, 2927, 2939, 2953, 2957, 2963, 2969, 2971, 2999, 3001, 3011, 3019, 3023, 
    3037, 3041, 3049, 3061, 3067, 3079, 3083, 3089, 3109, 3119, 3121, 3137, 3163, 3167, 
    3169, 3181, 3187, 3191, 3203, 3209, 3217, 3221, 3229, 3251, 3253, 3257, 3259, 3271, 
    3299, 3301, 3307, 3313, 3319, 3323, 3329, 3331, 3343, 3347, 3359, 3361, 3371, 3373, 
    3389, 3391, 3407, 3413, 3433, 3449, 3457, 3461, 3463, 3467, 3469, 3491, 3499, 3511, 
    3517, 3527, 3529, 3533, 3539, 3541, 3547, 3557, 3559, 3571, 3581, 3583, 3593, 3607, 
    3613, 3617, 3623, 3631, 3637, 3643, 3659, 3671, 3673, 3677, 3691, 3697, 3701, 3709, 
    3719, 3727, 3733, 3739, 3761, 3767, 3769, 3779, 3793, 3797, 3803, 3821, 3823, 3833, 
    3847, 3851, 3853, 3863, 3877, 3881, 3889, 3907, 3911, 3917, 3919, 3923, 3929, 3931, 
    3943, 3947, 3967, 3989, 4001, 4003, 4007, 4013, 4019, 4021, 4027, 4049, 4051, 4057, 
    4073, 4079, 4091, 4093, 4099, 4111, 4127, 4129, 4133, 4139, 4153, 4157, 4159, 4177, 
    4201, 4211, 4217, 4219, 4229, 4231, 4241, 4243, 4253, 4259, 4261, 4271, 4273, 4283, 
    4289, 4297, 4327, 4337, 4339, 4349, 4357, 4363, 4373, 4391, 4397, 4409, 4421, 4423, 
    4441, 4447, 4451, 4457, 4463, 4481, 4483, 4493, 4507, 4513, 4517, 4519, 4523, 4547, 
    4549, 4561, 4567, 4583, 4591, 4597, 4603, 4621, 4637, 4639, 4643, 4649, 4651, 4657, 
    4663, 4673, 4679, 4691, 4703, 4721, 4723, 4729, 4733, 4751, 4759, 4783, 4787, 4789, 
    4793, 4799, 4801, 4813, 4817, 4831, 4861, 4871, 4877, 4889, 4903, 4909, 4919, 4931, 
    4933, 4937, 4943, 4951, 4957, 4967, 4969, 4973, 4987, 4993, 4999, 5003, 5009, 5011, 
    5021, 5023, 5039, 5051, 5059, 5077, 5081, 5087, 5099, 5101, 5107, 5113, 5119, 5147, 
    5153, 5167, 5171, 5179, 5189, 5197, 5209, 5227, 5231, 5233, 5237, 5261, 5273, 5279, 
    5281, 5297, 5303, 5309, 5323, 5333, 5347, 5351, 5381, 5387, 5393, 5399, 5407, 5413, 
    5417, 5419, 5431, 5437, 5441, 5443, 5449, 5471, 5477, 5479, 5483, 5501, 5503, 5507, 
    5519, 5521, 5527, 5531, 5557, 5563, 5569, 5573, 5581, 5591, 5623, 5639, 5641, 5647, 
    5651, 5653, 5657, 5659, 5669, 5683, 5689, 5693, 5701, 5711, 5717, 5737, 5741, 5743, 
    5749, 5779, 5783, 5791, 5801, 5807, 5813, 5821, 5827, 5839, 5843, 5849, 5851, 5857, 
    5861, 5867, 5869, 5879, 5881, 5897, 5903, 5923, 5927, 5939, 5953, 5981, 5987, 6007, 
    6011, 6029, 6037, 6043, 6047, 6053, 6067, 6073, 6079, 6089, 6091, 6101, 6113, 6121, 
    6131, 6133, 6143, 6151, 6163, 6173, 6197, 6199, 6203, 6211, 6217, 6221, 6229, 6247, 
    6257, 6263, 6269, 6271, 6277, 6287, 6299, 6301, 6311, 6317, 6323, 6329, 6337, 6343, 
    6353, 6359, 6361, 6367, 6373, 6379, 6389, 6397, 6421, 6427, 6449, 6451, 6469, 6473, 
    6481, 6491, 6521, 6529, 6547, 6551, 6553, 6563, 6569, 6571, 6577, 6581, 6599, 6607, 
    6619, 6637, 6653, 6659, 6661, 6673, 6679, 6689, 6691, 6701, 6703, 6709, 6719, 6733, 
    6737, 6761, 6763, 6779, 6781, 6791, 6793, 6803, 6823, 6827, 6829, 6833, 6841, 6857, 
    6863, 6869, 6871, 6883, 6899, 6907, 6911, 6917, 6947, 6949, 6959, 6961, 6967, 6971, 
    6977, 6983, 6991, 6997, 7001, 7013, 7019, 7027, 7039, 7043, 7057, 7069, 7079, 7103, 
    7109, 7121, 7127, 7129, 7151, 7159, 7177, 7187, 7193, 7207, 7211, 7213, 7219, 7229, 
    7237, 7243, 7247, 7253, 7283, 7297, 7307, 7309, 7321, 7331, 7333, 7349, 7351, 7369, 
    7393, 7411, 7417, 7433, 7451, 7457, 7459, 7477, 7481, 7487, 7489, 7499, 7507, 7517, 
    7523, 7529, 7537, 7541, 7547, 7549, 7559, 7561, 7573, 7577, 7583, 7589, 7591, 7603, 
    7607, 7621, 7639, 7643, 7649, 7669, 7673, 7681, 7687, 7691, 7699, 7703, 7717, 7723, 
    7727, 7741, 7753, 7757, 7759, 7789, 7793, 7817, 7823, 7829, 7841, 7853, 7867, 7873, 
    7877, 7879, 7883, 7901, 7907, 7919, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009, 
    8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123, 
    8147, 8161 };
    int i;
    unsigned uHashKey;
    assert( nWords <= 1024 );
    uHashKey = 0;
    for ( i = 0; i < nWords; i++ )
        uHashKey ^= HashPrimes[i] * pIn[i];
    return uHashKey;
}

static int Kit_TruthIsConst0 ( unsigned *  pIn, int  nVars  )

inlinestatic

Definition at line 315 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        if ( pIn[w] )
            return 0;
    return 1;
}

static int Kit_TruthIsConst1 ( unsigned *  pIn, int  nVars  )

inlinestatic

Definition at line 323 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        if ( pIn[w] != ~(unsigned)0 )
            return 0;
    return 1;
}

static int Kit_TruthIsDisjoint ( unsigned *  pIn1, unsigned *  pIn2, int  nVars  )

inlinestatic

Definition at line 339 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        if ( pIn1[w] & pIn2[w] )
            return 0;
    return 1;
}

static int Kit_TruthIsDisjoint3 ( unsigned *  pIn1, unsigned *  pIn2, unsigned *  pIn3, int  nVars  )

inlinestatic

Definition at line 347 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        if ( pIn1[w] & pIn2[w] & pIn3[w] )
            return 0;
    return 1;
}

static int Kit_TruthIsEqual ( unsigned *  pIn0, unsigned *  pIn1, int  nVars  )

inlinestatic

Definition at line 274 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        if ( pIn0[w] != pIn1[w] )
            return 0;
    return 1;
}

static int Kit_TruthIsEqualWithCare ( unsigned *  pIn0, unsigned *  pIn1, unsigned *  pCare, int  nVars  )

inlinestatic

Definition at line 282 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        if ( (pIn0[w] & pCare[w]) != (pIn1[w] & pCare[w]) )
            return 0;
    return 1;
}

static int Kit_TruthIsEqualWithPhase ( unsigned *  pIn0, unsigned *  pIn1, int  nVars  )

inlinestatic

Definition at line 298 of file kit.h.

{
    int w;
    if ( (pIn0[0] & 1) == (pIn1[0] & 1) )
    {
        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
            if ( pIn0[w] != pIn1[w] )
                return 0;
    }
    else
    {
        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
            if ( pIn0[w] != ~pIn1[w] )
                return 0;
    }
    return 1;
}

static int Kit_TruthIsImply ( unsigned *  pIn1, unsigned *  pIn2, int  nVars  )

inlinestatic

Definition at line 331 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        if ( pIn1[w] & ~pIn2[w] )
            return 0;
    return 1;
}

int Kit_TruthIsop	(	unsigned *	puTruth,
		int	nVars,
		Vec_Int_t *	vMemory,
		int	fTryBoth
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes ISOP from TT.]

Description [Returns the cover in vMemory. Uses the rest of array in vMemory as an intermediate memory storage. Returns the cover with -1 cubes, if the the computation exceeded the memory limit (KIT_ISOP_MEM_LIMIT words of intermediate data).]

SideEffects []

SeeAlso []

Definition at line 55 of file kitIsop.c.

{
    Kit_Sop_t cRes, * pcRes = &cRes;
    Kit_Sop_t cRes2, * pcRes2 = &cRes2;
    unsigned * pResult;
    int RetValue = 0;
    assert( nVars >= 0 && nVars <= 16 );
    // if nVars < 5, make sure it does not depend on those vars
//    for ( i = nVars; i < 5; i++ )
//        assert( !Kit_TruthVarInSupport(puTruth, 5, i) );
    // prepare memory manager
    Vec_IntClear( vMemory );
    Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT );
    // compute ISOP for the direct polarity
    pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vMemory );
    if ( pcRes->nCubes == -1 )
    {
        vMemory->nSize = -1;
        return -1;
    }
    assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
    if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) )
    {
        vMemory->pArray[0] = 0;
        Vec_IntShrink( vMemory, pcRes->nCubes );
        return 0;
    }
    if ( fTryBoth )
    {
        // compute ISOP for the complemented polarity
        Kit_TruthNot( puTruth, puTruth, nVars );
        pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vMemory );
        if ( pcRes2->nCubes >= 0 )
        {
            assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
            if ( pcRes->nCubes > pcRes2->nCubes || (pcRes->nCubes == pcRes2->nCubes && pcRes->nLits > pcRes2->nLits) )
            {
                RetValue = 1;
                pcRes = pcRes2;
            }
        }
        Kit_TruthNot( puTruth, puTruth, nVars );
    }
//    printf( "%d ", vMemory->nSize );
    // move the cover representation to the beginning of the memory buffer
    memmove( vMemory->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
    Vec_IntShrink( vMemory, pcRes->nCubes );
    return RetValue;
}

static int Kit_TruthIsOpposite ( unsigned *  pIn0, unsigned *  pIn1, int  nVars  )

inlinestatic

Definition at line 290 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        if ( pIn0[w] != ~pIn1[w] )
            return 0;
    return 1;
}

void Kit_TruthIsopPrint	(	unsigned *	puTruth,
		int	nVars,
		Vec_Int_t *	vMemory,
		int	fTryBoth
	)

Definition at line 128 of file kitIsop.c.

{
    int fCompl = Kit_TruthIsop( puTruth, nVars, vCover, fTryBoth );
    Kit_TruthIsopPrintCover( vCover, nVars, fCompl );
}

void Kit_TruthIsopPrintCover	(	Vec_Int_t *	vCover,
		int	nVars,
		int	fCompl
	)

Definition at line 104 of file kitIsop.c.

{
    int i, k, Entry, Literal;
    if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0) )
    {
        printf( "Constant %d\n", Vec_IntSize(vCover) );
        return;
    }
    Vec_IntForEachEntry( vCover, Entry, i )
    { 
        for ( k = 0; k < nVars; k++ )
        {
            Literal = 3 & (Entry >> (k << 1));
            if ( Literal == 1 ) // neg literal
                printf( "0" );
            else if ( Literal == 2 ) // pos literal
                printf( "1" );
            else if ( Literal == 0 ) 
                printf( "-" );
            else assert( 0 );
        }
        printf( " %d\n", !fCompl );
    }
}

static void Kit_TruthIthVar ( unsigned *  pTruth, int  nVars, int  iVar  )

inlinestatic

Definition at line 473 of file kit.h.

{
    unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
    int k, nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
    if ( iVar < 5 )
    {
        for ( k = 0; k < nWords; k++ )
            pTruth[k] = Masks[iVar];
    }
    else
    {
        for ( k = 0; k < nWords; k++ )
            if ( k & (1 << (iVar-5)) )
                pTruth[k] = ~(unsigned)0;
            else
                pTruth[k] = 0;
    }
}

int Kit_TruthMinCofSuppOverlap	(	unsigned *	pTruth,
		int	nVars,
		int *	pVarMin
	)

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

Synopsis [Computes minimum overlap in supports of cofactors.]

Description []

SideEffects []

SeeAlso []

Definition at line 1315 of file kitTruth.c.

{
    static unsigned uCofactor[16];
    int i, ValueCur, ValueMin, VarMin;
    unsigned uSupp0, uSupp1;
    int nVars0, nVars1;
    assert( nVars <= 9 );
    ValueMin = 32;
    VarMin   = -1;
    for ( i = 0; i < nVars; i++ )
    {
        // get negative cofactor
        Kit_TruthCopy( uCofactor, pTruth, nVars );
        Kit_TruthCofactor0( uCofactor, nVars, i );
        uSupp0 = Kit_TruthSupport( uCofactor, nVars );
        nVars0 = Kit_WordCountOnes( uSupp0 );
//Kit_PrintBinary( stdout, &uSupp0, 8 ); printf( "\n" );
        // get positive cofactor
        Kit_TruthCopy( uCofactor, pTruth, nVars );
        Kit_TruthCofactor1( uCofactor, nVars, i );
        uSupp1 = Kit_TruthSupport( uCofactor, nVars );
        nVars1 = Kit_WordCountOnes( uSupp1 );
//Kit_PrintBinary( stdout, &uSupp1, 8 ); printf( "\n" );
        // get the number of common vars
        ValueCur = Kit_WordCountOnes( uSupp0 & uSupp1 );
        if ( ValueMin > ValueCur && nVars0 <= 5 && nVars1 <= 5 )
        {
            ValueMin = ValueCur;
            VarMin = i;
        }
        if ( ValueMin == 0 )
            break;
    }
    if ( pVarMin )
        *pVarMin = VarMin;
    return ValueMin;
}

static void Kit_TruthMux ( unsigned *  pOut, unsigned *  pIn0, unsigned *  pIn1, unsigned *  pCtrl, int  nVars  )

inlinestatic

Definition at line 457 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
}

static void Kit_TruthMuxPhase ( unsigned *  pOut, unsigned *  pIn0, unsigned *  pIn1, unsigned *  pCtrl, int  nVars, int  fComp0  )

inlinestatic

Definition at line 463 of file kit.h.

{
    int w;
    if ( fComp0 )
        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
            pOut[w] = (~pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
    else
        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
            pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
}

void Kit_TruthMuxVar	(	unsigned *	pOut,
		unsigned *	pCof0,
		unsigned *	pCof1,
		int	nVars,
		int	iVar
	)

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

Synopsis [Multiplexes two functions with the given variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 1069 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
            {
                pOut[i]      = pCof0[i];
                pOut[Step+i] = pCof1[Step+i];
            }
            pOut += 2*Step;
            pCof0 += 2*Step;
            pCof1 += 2*Step;
        }
        return;
    }
}

void Kit_TruthMuxVarPhase	(	unsigned *	pOut,
		unsigned *	pCof0,
		unsigned *	pCof1,
		int	nVars,
		int	iVar,
		int	fCompl0
	)

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

Synopsis [Multiplexes two functions with the given variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 1125 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step;

    if ( fCompl0 == 0 )
    {
        Kit_TruthMuxVar( pOut, pCof0, pCof1, nVars, iVar );
        return;
    }

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (~pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (~pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (~pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (~pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (~pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
            {
                pOut[i]      = ~pCof0[i];
                pOut[Step+i] = pCof1[Step+i];
            }
            pOut += 2*Step;
            pCof0 += 2*Step;
            pCof1 += 2*Step;
        }
        return;
    }
}

static void Kit_TruthNand ( unsigned *  pOut, unsigned *  pIn0, unsigned *  pIn1, int  nVars  )

inlinestatic

Definition at line 403 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = ~(pIn0[w] & pIn1[w]);
}

static void Kit_TruthNot ( unsigned *  pOut, unsigned *  pIn, int  nVars  )

inlinestatic

Definition at line 373 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = ~pIn[w];
}

static void Kit_TruthOr ( unsigned *  pOut, unsigned *  pIn0, unsigned *  pIn1, int  nVars  )

inlinestatic

Definition at line 385 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = pIn0[w] | pIn1[w];
}

static void Kit_TruthOrPhase ( unsigned *  pOut, unsigned *  pIn0, unsigned *  pIn1, int  nVars, int  fCompl0, int  fCompl1  )

inlinestatic

Definition at line 433 of file kit.h.

{
    int w;
    if ( fCompl0 && fCompl1 )
    {
        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
            pOut[w] = ~(pIn0[w] & pIn1[w]);
    }
    else if ( fCompl0 && !fCompl1 )
    {
        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
            pOut[w] = ~pIn0[w] | pIn1[w];
    }
    else if ( !fCompl0 && fCompl1 )
    {
        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
            pOut[w] = pIn0[w] | ~pIn1[w];
    }
    else // if ( !fCompl0 && !fCompl1 )
    {
        for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
            pOut[w] = pIn0[w] | pIn1[w];
    }
}

void Kit_TruthPermute	(	unsigned *	pOut,
		unsigned *	pIn,
		int	nVars,
		char *	pPerm,
		int	fReturnIn
	)

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

Synopsis [Implement give permutation.]

Description [The input and output truth tables are in pIn/pOut. The number of variables is nVars. Permutation is in pPerm.]

SideEffects [The input truth table is modified.]

SeeAlso []

Definition at line 233 of file kitTruth.c.

{
    unsigned * pTemp;
    int i, Temp, fChange, Counter = 0;
    do {
        fChange = 0;
        for ( i = 0; i < nVars-1; i++ )
        {
            assert( pPerm[i] != pPerm[i+1] );
            if ( pPerm[i] <= pPerm[i+1] )
                continue;
            Counter++;
            fChange = 1;

            Temp = pPerm[i];
            pPerm[i] = pPerm[i+1];
            pPerm[i+1] = Temp;

            Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
            pTemp = pIn; pIn = pOut; pOut = pTemp;
        }
    } while ( fChange );
    if ( fReturnIn ^ !(Counter & 1) )
        Kit_TruthCopy( pOut, pIn, nVars );
}

void Kit_TruthPrintProfile	(	unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Dumps truth table into a file.]

Description [Generates script file for reading into ABC.]

SideEffects []

SeeAlso []

Definition at line 2203 of file kitTruth.c.

{
    unsigned uTruth[2];
    if ( nVars >= 6 )
    {
        Kit_TruthPrintProfile_int( pTruth, nVars );
        return;
    }
    assert( nVars >= 2 );
    uTruth[0] = pTruth[0];
    uTruth[1] = pTruth[0];
    Kit_TruthPrintProfile( uTruth, 6 );
}

unsigned Kit_TruthSemiCanonicize	(	unsigned *	pInOut,
		unsigned *	pAux,
		int	nVars,
		char *	pCanonPerm
	)

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

Synopsis [Canonicize the truth table.]

Description [Returns the phase. ]

SideEffects []

SeeAlso []

Definition at line 1657 of file kitTruth.c.

{
    int pStore[32];
    unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
    int nWords = Kit_TruthWordNum( nVars );
    int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
    unsigned uCanonPhase;

    // canonicize output
    uCanonPhase = 0;
    for ( i = 0; i < nVars; i++ )
        pCanonPerm[i] = i;

    nOnes = Kit_TruthCountOnes(pIn, nVars);
    //if(pIn[0] & 1)
    if ( (nOnes > nWords * 16) )//|| ((nOnes == nWords * 16) && (pIn[0] & 1)) )
    {
        uCanonPhase |= (1 << nVars);
        Kit_TruthNot( pIn, pIn, nVars );
    }

    // collect the minterm counts
    Kit_TruthCountOnesInCofs( pIn, nVars, pStore );
/*
    Kit_TruthCountOnesInCofsSlow( pIn, nVars, pStore2, pAux );
    for ( i = 0; i < 2*nVars; i++ )
    {
        assert( pStore[i] == pStore2[i] );
    }
*/
    // canonicize phase
    for ( i = 0; i < nVars; i++ )
    {
        if ( pStore[2*i+0] >= pStore[2*i+1] )
            continue;
        uCanonPhase |= (1 << i);
        Temp = pStore[2*i+0];
        pStore[2*i+0] = pStore[2*i+1];
        pStore[2*i+1] = Temp;
        Kit_TruthChangePhase( pIn, nVars, i );
    }

//    Kit_PrintHexadecimal( stdout, pIn, nVars );
//    printf( "\n" );

    // permute
    Counter = 0;
    do {
        fChange = 0;
        for ( i = 0; i < nVars-1; i++ )
        {
            if ( pStore[2*i] >= pStore[2*(i+1)] )
                continue;
            Counter++;
            fChange = 1;

            Temp = pCanonPerm[i];
            pCanonPerm[i] = pCanonPerm[i+1];
            pCanonPerm[i+1] = Temp;

            Temp = pStore[2*i];
            pStore[2*i] = pStore[2*(i+1)];
            pStore[2*(i+1)] = Temp;

            Temp = pStore[2*i+1];
            pStore[2*i+1] = pStore[2*(i+1)+1];
            pStore[2*(i+1)+1] = Temp;

            // if the polarity of variables is different, swap them
            if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
            {
                uCanonPhase ^= (1 << i);
                uCanonPhase ^= (1 << (i+1));
            }

            Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
            pTemp = pIn; pIn = pOut; pOut = pTemp;
        }
    } while ( fChange );


/*
    Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
    for ( i = 0; i < nVars; i++ )
        printf( "%d=%d/%d  ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] );
    printf( "  C = %d\n", Counter );
    Extra_PrintHexadecimal( stdout, pIn, nVars );
    printf( "\n" );
*/

/*
    // process symmetric variable groups
    uSymms = 0;
    for ( i = 0; i < nVars-1; i++ )
    {
        if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
            continue;
        if ( pStore[2*i] != pStore[2*i+1] )
            continue;
        if ( Kit_TruthVarsSymm( pIn, nVars, i, i+1 ) )
            continue;
        if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, i+1 ) )
            Kit_TruthChangePhase( pIn, nVars, i+1 );
    }
*/

/*
    // process symmetric variable groups
    uSymms = 0;
    for ( i = 0; i < nVars-1; i++ )
    {
        if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
            continue;
        // i and i+1 can be symmetric
        // find the end of this group
        for ( k = i+1; k < nVars; k++ )
            if ( pStore[2*i] != pStore[2*k] ) 
                break;
        Limit = k;
        assert( i < Limit-1 );
        // go through the variables in this group
        for ( j = i + 1; j < Limit; j++ )
        {
            // check symmetry
            if ( Kit_TruthVarsSymm( pIn, nVars, i, j ) )
            {
                uSymms |= (1 << j);
                continue;
            }
            // they are phase-unknown
            if ( pStore[2*i] == pStore[2*i+1] ) 
            {
                if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, j ) )
                {
                    Kit_TruthChangePhase( pIn, nVars, j );
                    uCanonPhase ^= (1 << j);
                    uSymms |= (1 << j);
                    continue;
                }
            }

            // they are not symmetric - move j as far as it goes in the group
            for ( k = j; k < Limit-1; k++ )
            {
                Counter++;

                Temp = pCanonPerm[k];
                pCanonPerm[k] = pCanonPerm[k+1];
                pCanonPerm[k+1] = Temp;

                assert( pStore[2*k] == pStore[2*(k+1)] );
                Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, k );
                pTemp = pIn; pIn = pOut; pOut = pTemp;
            }
            Limit--;
            j--;
        }
        i = Limit - 1;
    }
*/

    // swap if it was moved an even number of times
    if ( Counter & 1 )
        Kit_TruthCopy( pOut, pIn, nVars );
    return uCanonPhase;
}

static void Kit_TruthSetBit ( unsigned *  p, int  Bit  )

inlinestatic

Definition at line 227 of file kit.h.

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

static void Kit_TruthSharp ( unsigned *  pOut, unsigned *  pIn0, unsigned *  pIn1, int  nVars  )

inlinestatic

Definition at line 397 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = pIn0[w] & ~pIn1[w];
}

void Kit_TruthShrink	(	unsigned *	pOut,
		unsigned *	pIn,
		int	nVars,
		int	nVarsAll,
		unsigned	Phase,
		int	fReturnIn
	)

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

Synopsis [Shrinks the truth table according to the phase.]

Description [The input and output truth tables are in pIn/pOut. The current number of variables is nVars. The total number of variables in nVarsAll. The last argument (Phase) shows what variables should remain.]

SideEffects [The input truth table is modified.]

SeeAlso []

Definition at line 200 of file kitTruth.c.

{
    unsigned * pTemp;
    int i, k, Var = 0, Counter = 0;
    for ( i = 0; i < nVarsAll; i++ )
        if ( Phase & (1 << i) )
        {
            for ( k = i-1; k >= Var; k-- )
            {
                Kit_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
                pTemp = pIn; pIn = pOut; pOut = pTemp;
                Counter++;
            }
            Var++;
        }
    assert( Var == nVars );
    // swap if it was moved an even number of times
    if ( fReturnIn ^ !(Counter & 1) )
        Kit_TruthCopy( pOut, pIn, nVarsAll );
}

void Kit_TruthStretch	(	unsigned *	pOut,
		unsigned *	pIn,
		int	nVars,
		int	nVarsAll,
		unsigned	Phase,
		int	fReturnIn
	)

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

Synopsis [Expands the truth table according to the phase.]

Description [The input and output truth tables are in pIn/pOut. The current number of variables is nVars. The total number of variables in nVarsAll. The last argument (Phase) contains shows where the variables should go.]

SideEffects [The input truth table is modified.]

SeeAlso []

Definition at line 166 of file kitTruth.c.

{
    unsigned * pTemp;
    int i, k, Var = nVars - 1, Counter = 0;
    for ( i = nVarsAll - 1; i >= 0; i-- )
        if ( Phase & (1 << i) )
        {
            for ( k = Var; k < i; k++ )
            {
                Kit_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
                pTemp = pIn; pIn = pOut; pOut = pTemp;
                Counter++;
            }
            Var--;
        }
    assert( Var == -1 );
    // swap if it was moved an even number of times
    if ( fReturnIn ^ !(Counter & 1) )
        Kit_TruthCopy( pOut, pIn, nVarsAll );
}

unsigned Kit_TruthSupport	(	unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Returns support of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 346 of file kitTruth.c.

{
    int i, Support = 0;
    for ( i = 0; i < nVars; i++ )
        if ( Kit_TruthVarInSupport( pTruth, nVars, i ) )
            Support |= (1 << i);
    return Support;
}

int Kit_TruthSupportSize	(	unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Returns the number of support vars.]

Description []

SideEffects []

SeeAlso []

Definition at line 327 of file kitTruth.c.

{
    int i, Counter = 0;
    for ( i = 0; i < nVars; i++ )
        Counter += Kit_TruthVarInSupport( pTruth, nVars, i );
    return Counter;
}

void Kit_TruthSwapAdjacentVars	(	unsigned *	pOut,
		unsigned *	pIn,
		int	nVars,
		int	iVar
	)

DECLARATIONS ///.

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

FileName [kitTruth.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Procedures involving truth tables.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 6, 2006.]

Revision [

Id:

kitTruth.c,v 1.00 2006/12/06 00:00:00 alanmi Exp

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

Synopsis [Swaps two adjacent variables in the truth table.]

Description [Swaps var number Start and var number Start+1 (0-based numbers). The input truth table is pIn. The output truth table is pOut.]

SideEffects []

SeeAlso []

Definition at line 46 of file kitTruth.c.

{
    static unsigned PMasks[4][3] = {
        { 0x99999999, 0x22222222, 0x44444444 },
        { 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 },
        { 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
        { 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
    };
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step, Shift;

    assert( iVar < nVars - 1 );
    if ( iVar < 4 )
    {
        Shift = (1 << iVar);
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
    }
    else if ( iVar > 4 )
    {
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 4*Step )
        {
            for ( i = 0; i < Step; i++ )
                pOut[i] = pIn[i];
            for ( i = 0; i < Step; i++ )
                pOut[Step+i] = pIn[2*Step+i];
            for ( i = 0; i < Step; i++ )
                pOut[2*Step+i] = pIn[Step+i];
            for ( i = 0; i < Step; i++ )
                pOut[3*Step+i] = pIn[3*Step+i];
            pIn  += 4*Step;
            pOut += 4*Step;
        }
    }
    else // if ( iVar == 4 )
    {
        for ( i = 0; i < nWords; i += 2 )
        {
            pOut[i]   = (pIn[i]   & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
            pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i]   & 0xFFFF0000) >> 16);
        }
    }
}

DdNode* Kit_TruthToBdd	(	DdManager *	dd,
		unsigned *	pTruth,
		int	nVars,
		int	fMSBonTop
	)

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

Synopsis [Compute BDD corresponding to the truth table.]

Description [If truth table has N vars, the BDD depends on N topmost variables of the BDD manager. The most significant variable of the table is encoded by the topmost variable of the manager. BDD construction is efficient in this case because BDD is constructed one node at a time, by simply adding BDD nodes on top of existent BDD nodes.]

SideEffects []

SeeAlso []

Definition at line 182 of file kitBdd.c.

{
    return Kit_TruthToBdd_rec( dd, pTruth, 0, nVars, nVars, fMSBonTop );
}

CloudNode* Kit_TruthToCloud	(	CloudManager *	dd,
		unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Compute BDD for the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 148 of file kitCloud.c.

{
    CloudNode * pRes;
    pRes = Kit_TruthToCloud_rec( dd, pTruth, nVars, nVars );
//    printf( "%d/%d  ", Count, Cloud_DagSize(dd, pRes) );
    return pRes;
}

Kit_Graph_t* Kit_TruthToGraph	(	unsigned *	pTruth,
		int	nVars,
		Vec_Int_t *	vMemory
	)

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

Synopsis [Derives the factored form from the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 355 of file kitGraph.c.

{
    Kit_Graph_t * pGraph;
    int RetValue;
    // derive SOP
    RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 1 ); // tried 1 and found not useful in "renode"
    if ( RetValue == -1 )
        return NULL;
    if ( Vec_IntSize(vMemory) > (1<<16) )
        return NULL;
//    printf( "Isop size = %d.\n", Vec_IntSize(vMemory) );
    assert( RetValue == 0 || RetValue == 1 );
    // derive factored form
    pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory );
    return pGraph;
}

void Kit_TruthUniqueNew	(	unsigned *	pRes,
		unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Universally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 922 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
        return;
    case 1:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
        return;
    case 2:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
        return;
    case 3:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
        return;
    case 4:
        for ( i = 0; i < nWords; i++ )
            pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
        return;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
            {
                pRes[i]      = pTruth[i] ^ pTruth[Step+i];
                pRes[Step+i] = pRes[i];
            }
            pRes += 2*Step;
            pTruth += 2*Step;
        }
        return;
    }
}

int Kit_TruthVarInSupport	(	unsigned *	pTruth,
		int	nVars,
		int	iVar
	)

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

Synopsis [Returns 1 if TT depends on the given variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 270 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) )
                return 1;
        return 0;
    case 1:
        for ( i = 0; i < nWords; i++ )
            if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) )
                return 1;
        return 0;
    case 2:
        for ( i = 0; i < nWords; i++ )
            if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) )
                return 1;
        return 0;
    case 3:
        for ( i = 0; i < nWords; i++ )
            if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) )
                return 1;
        return 0;
    case 4:
        for ( i = 0; i < nWords; i++ )
            if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) )
                return 1;
        return 0;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
                if ( pTruth[i] != pTruth[Step+i] )
                    return 1;
            pTruth += 2*Step;
        }
        return 0;
    }
}

int Kit_TruthVarIsVacuous	(	unsigned *	pOnset,
		unsigned *	pOffset,
		int	nVars,
		int	iVar
	)

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

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 625 of file kitTruth.c.

{
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step;

    assert( iVar < nVars );
    switch ( iVar )
    {
    case 0:
        for ( i = 0; i < nWords; i++ )
            if ( ((pOnset[i] & (pOffset[i] >> 1)) | (pOffset[i] & (pOnset[i] >> 1))) & 0x55555555 )
                 return 0;
        return 1;
    case 1:
        for ( i = 0; i < nWords; i++ )
            if ( ((pOnset[i] & (pOffset[i] >> 2)) | (pOffset[i] & (pOnset[i] >> 2))) & 0x33333333 )
                 return 0;
            return 1;
    case 2:
        for ( i = 0; i < nWords; i++ )
            if ( ((pOnset[i] & (pOffset[i] >> 4)) | (pOffset[i] & (pOnset[i] >> 4))) & 0x0F0F0F0F )
                 return 0;
        return 1;
    case 3:
        for ( i = 0; i < nWords; i++ )
            if ( ((pOnset[i] & (pOffset[i] >> 8)) | (pOffset[i] & (pOnset[i] >> 8))) & 0x00FF00FF )
                 return 0;
        return 1;
    case 4:
        for ( i = 0; i < nWords; i++ )
            if ( ((pOnset[i] & (pOffset[i] >> 16)) | (pOffset[i] & (pOnset[i] >> 16))) & 0x0000FFFF )
                 return 0;
        return 1;
    default:
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 2*Step )
        {
            for ( i = 0; i < Step; i++ )
                if ( (pOnset[i] & pOffset[Step+i]) | (pOffset[i] & pOnset[Step+i]) )
                     return 0;
            pOnset += 2*Step;
            pOffset += 2*Step;
        }
        return 1;
    }
}

int Kit_TruthVarsAntiSymm	(	unsigned *	pTruth,
		int	nVars,
		int	iVar0,
		int	iVar1,
		unsigned *	pCof0,
		unsigned *	pCof1
	)

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

Synopsis [Checks antisymmetry of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 1223 of file kitTruth.c.

{
    static unsigned uTemp0[32], uTemp1[32];
    if ( pCof0 == NULL )
    {
        assert( nVars <= 10 );
        pCof0 = uTemp0;
    }
    if ( pCof1 == NULL )
    {
        assert( nVars <= 10 );
        pCof1 = uTemp1;
    }
    // compute Cof00
    Kit_TruthCopy( pCof0, pTruth, nVars );
    Kit_TruthCofactor0( pCof0, nVars, iVar0 );
    Kit_TruthCofactor0( pCof0, nVars, iVar1 );
    // compute Cof11
    Kit_TruthCopy( pCof1, pTruth, nVars );
    Kit_TruthCofactor1( pCof1, nVars, iVar0 );
    Kit_TruthCofactor1( pCof1, nVars, iVar1 );
    // compare
    return Kit_TruthIsEqual( pCof0, pCof1, nVars );
}

int Kit_TruthVarsSymm	(	unsigned *	pTruth,
		int	nVars,
		int	iVar0,
		int	iVar1,
		unsigned *	pCof0,
		unsigned *	pCof1
	)

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

Synopsis [Checks symmetry of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 1187 of file kitTruth.c.

{
    static unsigned uTemp0[32], uTemp1[32];
    if ( pCof0 == NULL )
    {
        assert( nVars <= 10 );
        pCof0 = uTemp0;
    }
    if ( pCof1 == NULL )
    {
        assert( nVars <= 10 );
        pCof1 = uTemp1;
    }
    // compute Cof01
    Kit_TruthCopy( pCof0, pTruth, nVars );
    Kit_TruthCofactor0( pCof0, nVars, iVar0 );
    Kit_TruthCofactor1( pCof0, nVars, iVar1 );
    // compute Cof10
    Kit_TruthCopy( pCof1, pTruth, nVars );
    Kit_TruthCofactor1( pCof1, nVars, iVar0 );
    Kit_TruthCofactor0( pCof1, nVars, iVar1 );
    // compare
    return Kit_TruthIsEqual( pCof0, pCof1, nVars );
}

static int Kit_TruthWordNum ( int  nVars )

inlinestatic

Definition at line 224 of file kit.h.

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

static void Kit_TruthXor ( unsigned *  pOut, unsigned *  pIn0, unsigned *  pIn1, int  nVars  )

inlinestatic

Definition at line 391 of file kit.h.

{
    int w;
    for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
        pOut[w] = pIn0[w] ^ pIn1[w];
}

static void Kit_TruthXorBit ( unsigned *  p, int  Bit  )

inlinestatic

Definition at line 228 of file kit.h.

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

static int Kit_WordCountOnes ( unsigned  uWord )

inlinestatic

Definition at line 243 of file kit.h.

{
    uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
    uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
    uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
    uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
    return  (uWord & 0x0000FFFF) + (uWord>>16);
}

static int Kit_WordFindFirstBit ( unsigned  uWord )

inlinestatic

Definition at line 231 of file kit.h.

{
    int i;
    for ( i = 0; i < 32; i++ )
        if ( uWord & (1 << i) )
            return i;
    return -1;
}

static int Kit_WordHasOneBit ( unsigned  uWord )

inlinestatic

Definition at line 239 of file kit.h.

{
    return (uWord & (uWord - 1)) == 0;
}