src/aig/kit/kit.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "vec.h"
#include "extra.h"
#include "cloud.h"

Include dependency graph for kit.h:

This graph shows which files directly or indirectly include this file:

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_
Defines
#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 < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
#define	KIT_MIN(a, b) (((a) < (b))? (a) : (b))
#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++ )
#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 struct Kit_Sop_t_	Kit_Sop_t
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 int	Kit_DsdVar2Lit (int Var, int fCompl)
static int	Kit_DsdLit2Var (int Lit)
static int	Kit_DsdLitIsCompl (int Lit)
static int	Kit_DsdLitNot (int Lit)
static int	Kit_DsdLitNotCond (int Lit, int c)
static int	Kit_DsdLitRegular (int Lit)
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 eEdge)
static Kit_Edge_t	Kit_IntToEdge_ (unsigned Edge)
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_Float2Int (float Val)
static float	Kit_Int2Float (int Num)
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_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_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)
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)
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)
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)
unsigned	Kit_DsdNonDsdSupports (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)
Kit_Graph_t *	Kit_GraphCreate (int nLeaves)
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)
void	Kit_SopCreate (Kit_Sop_t cResult, Vec_Int_t vInput, int nVars, Vec_Int_t *vMemory)
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)
void	Kit_TruthStretch (unsigned pOut, unsigned pIn, int nVars, int nVarsAll, unsigned Phase, 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)
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_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, short pStore)
void	Kit_TruthCountOnesInCofsSlow (unsigned pTruth, int nVars, short pStore, unsigned *pAux)
unsigned	Kit_TruthHash (unsigned *pIn, int nWords)
unsigned	Kit_TruthSemiCanonicize (unsigned pInOut, unsigned pAux, int nVars, char pCanonPerm, short pStore)
char *	Kit_TruthDumpToFile (unsigned *pTruth, int nVars, int nFile)

Define Documentation

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

Definition at line 475 of file kit.h.

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

Definition at line 158 of file kit.h.

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

Definition at line 160 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 478 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 480 of file kit.h.

#define KIT_INFINITY (100000000)

Definition at line 169 of file kit.h.

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

Definition at line 168 of file kit.h.

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

MACRO DEFINITIONS ///

Definition at line 167 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 473 of file kit.h.

Typedef Documentation

typedef struct Kit_DsdMan_t_ Kit_DsdMan_t

Definition at line 130 of file kit.h.

typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t

Definition at line 117 of file kit.h.

typedef struct Kit_DsdObj_t_ Kit_DsdObj_t

Definition at line 104 of file kit.h.

typedef struct Kit_Edge_t_ Kit_Edge_t

Definition at line 56 of file kit.h.

typedef struct Kit_Graph_t_ Kit_Graph_t

Definition at line 81 of file kit.h.

typedef struct Kit_Node_t_ Kit_Node_t

Definition at line 63 of file kit.h.

typedef struct Kit_Sop_t_ Kit_Sop_t

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

] INCLUDES /// PARAMETERS /// BASIC TYPES ///

Definition at line 49 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 94 of file kit.h.

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

Function Documentation

static unsigned Kit_BitMask ( int nBits ) [inline, static]

Definition at line 233 of file kit.h.

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

static int Kit_BitWordNum ( int nBits ) [inline, static]

Definition at line 231 of file kit.h.

00231 { 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 223 of file kitCloud.c.

00224 {
00225     unsigned * pThis, * pFan0, * pFan1;
00226     Kit_Mux_t Mux;
00227     int i, Entry;
00228     assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
00229     pThis = Vec_PtrEntry( vStore, 0 );
00230     Kit_TruthFill( pThis, nVars );
00231     Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
00232     {
00233         Mux = *((Kit_Mux_t *)&Entry);
00234         assert( (int)Mux.e < i && (int)Mux.t < i && (int)Mux.v < nVars );          
00235         pFan0 = Vec_PtrEntry( vStore, Mux.e );
00236         pFan1 = Vec_PtrEntry( vStore, Mux.t );
00237         pThis = Vec_PtrEntry( vStore, i );
00238         Kit_TruthMuxVarPhase( pThis, pFan0, pFan1, nVars, fInv? Mux.v : nVars-1-Mux.v, Mux.c );
00239     } 
00240     // complement the result
00241     if ( Mux.i )
00242         Kit_TruthNot( pThis, pThis, nVars );
00243     return pThis;
00244 }

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 161 of file kitCloud.c.

00163 00164 00165 00166 00167 00168 00169 00170 00171 00172 00173 00174 00175     { 00176 00177 00178 00179 00180 00181 00182 00183 00184     } 00185 00186 00187 00188 00189 00190 }

class="fragment">00162 { 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, *((int *)&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 203 of file kitCloud.c.

00204 {
00205     CloudNode * pFunc;
00206     Cloud_Restart( dd );
00207     pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
00208     Vec_IntClear( vNodes );
00209     return Kit_CreateCloud( dd, pFunc, vNodes );
00210 }

static int Kit_CubeContains	(	unsigned	uLarge,
		unsigned	uSmall
	)			`[inline, static]`

Definition at line 190 of file kit.h.

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

static int Kit_CubeHasLit	(	unsigned	uCube,
		int	i
	)			`[inline, static]`

Definition at line 185 of file kit.h.

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

static int Kit_CubeIsMarked ( unsigned uCube ) [inline, static]

Definition at line 194 of file kit.h.

00194 { return Kit_CubeHasLit( uCube, 31 );     }

static unsigned Kit_CubeMark ( unsigned uCube ) [inline, static]

Definition at line 195 of file kit.h.

00195 { return Kit_CubeSetLit( uCube, 31 );     }

static unsigned Kit_CubeMask ( int nVar ) [inline, static]

Definition at line 192 of file kit.h.

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

static unsigned Kit_CubeRemLit	(	unsigned	uCube,
		int	i
	)			`[inline, static]`

Definition at line 188 of file kit.h.

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

static unsigned Kit_CubeSetLit	(	unsigned	uCube,
		int	i
	)			`[inline, static]`

Definition at line 186 of file kit.h.

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

static unsigned Kit_CubeSharp	(	unsigned	uCube,
		unsigned	uMask
	)			`[inline, static]`

Definition at line 191 of file kit.h.

00191 { return uCube & ~uMask;                  }

static unsigned Kit_CubeUnmark ( unsigned uCube ) [inline, static]

Definition at line 196 of file kit.h.

00196 { return Kit_CubeRemLit( uCube, 31 );     }

static unsigned Kit_CubeXorLit	(	unsigned	uCube,
		int	i
	)			`[inline, static]`

Definition at line 187 of file kit.h.

00187 { 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 2266 of file kitDsd.c.

02267 {
02268     Kit_DsdNtk_t * ppNtks[5][16] = {0}, * pTemp;
02269     unsigned * ppCofs[5][16];
02270     int pTryVars[16], nTryVars;
02271     int nPrimeSizeMin, nPrimeSizeMax, nPrimeSizeCur;
02272     int nSuppSizeMin, nSuppSizeMax, iVarBest;
02273     int i, k, v, nStep, nSize, nMemSize;
02274     assert( nLimit < 5 );
02275 
02276     // allocate storage for cofactors
02277     nMemSize = Kit_TruthWordNum(nVars);
02278     ppCofs[0][0] = ALLOC( unsigned, 80 * nMemSize );
02279     nSize = 0;
02280     for ( i = 0; i <  5; i++ )
02281     for ( k = 0; k < 16; k++ )
02282         ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
02283     assert( nSize == 80 );
02284 
02285     // copy the function
02286     Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
02287     ppNtks[0][0] = Kit_DsdDecompose( ppCofs[0][0], nVars );
02288 
02289     if ( fVerbose )
02290         printf( "\nProcessing prime function with %d support variables:\n", nVars );
02291 
02292     // perform recursive cofactoring
02293     for ( nStep = 0; nStep < nLimit; nStep++ )
02294     {
02295         nSize = (1 << nStep);
02296         // find the variables to use in the cofactoring step
02297         nTryVars = Kit_DsdCofactoringGetVars( ppNtks[nStep], nSize, pTryVars );
02298         if ( nTryVars == 0 )
02299             break;
02300         // cofactor w.r.t. the above variables
02301         iVarBest = -1;
02302         nPrimeSizeMin = 10000;
02303         nSuppSizeMin  = 10000;
02304         for ( v = 0; v < nTryVars; v++ )
02305         {
02306             nPrimeSizeMax = 0;
02307             nSuppSizeMax = 0;
02308             for ( i = 0; i < nSize; i++ )
02309             {
02310                 // cofactor and decompose cofactors          
02311                 Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, pTryVars[v] );
02312                 Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, pTryVars[v] );
02313                 ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars );
02314                 ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars );
02315                 // compute the largest non-decomp block
02316                 nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+0]);
02317                 nPrimeSizeMax  = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
02318                 nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+1]);
02319                 nPrimeSizeMax  = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
02320                 // compute the sum total of supports
02321                 nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+0], nVars );
02322                 nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+1], nVars );
02323                 // free the networks
02324                 Kit_DsdNtkFree( ppNtks[nStep+1][2*i+0] );
02325                 Kit_DsdNtkFree( ppNtks[nStep+1][2*i+1] );
02326             }
02327             // find the min max support size of the prime component
02328             if ( nPrimeSizeMin > nPrimeSizeMax || (nPrimeSizeMin == nPrimeSizeMax && nSuppSizeMin > nSuppSizeMax) )
02329             {
02330                 nPrimeSizeMin = nPrimeSizeMax;
02331                 nSuppSizeMin  = nSuppSizeMax;
02332                 iVarBest      = pTryVars[v];
02333             }
02334         }
02335         assert( iVarBest != -1 );
02336         // save the variable
02337         if ( pCofVars )
02338             pCofVars[nStep] = iVarBest;
02339         // cofactor w.r.t. the best
02340         for ( i = 0; i < nSize; i++ )
02341         {
02342             Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, iVarBest );
02343             Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, iVarBest );
02344             ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars );
02345             ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars );
02346             if ( fVerbose )
02347             {
02348                 ppNtks[nStep+1][2*i+0] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+0] );
02349                 Kit_DsdNtkFree( pTemp );
02350                 ppNtks[nStep+1][2*i+1] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+1] );
02351                 Kit_DsdNtkFree( pTemp );
02352 
02353                 printf( "Cof%d%d: ", nStep+1, 2*i+0 );
02354                 Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+0] );
02355                 printf( "Cof%d%d: ", nStep+1, 2*i+1 );
02356                 Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+1] );
02357             }
02358         }
02359     }
02360 
02361     // free the networks
02362     for ( i = 0; i <  5; i++ )
02363     for ( k = 0; k < 16; k++ )
02364         if ( ppNtks[i][k] )
02365             Kit_DsdNtkFree( ppNtks[i][k] );
02366     free( ppCofs[0][0] );
02367 
02368     assert( nStep <= nLimit );
02369     return nStep;
02370 }

Kit_DsdNtk_t* Kit_DsdDecompose	(	unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Performs decomposition of the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 1923 of file kitDsd.c.

01924 {
01925     return Kit_DsdDecomposeInt( pTruth, nVars, 0 );
01926 }

Kit_DsdNtk_t* Kit_DsdDecomposeExpand	(	unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Performs decomposition of the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 1939 of file kitDsd.c.

01940 {
01941     Kit_DsdNtk_t * pNtk, * pTemp;
01942     pNtk = Kit_DsdDecomposeInt( pTruth, nVars, 0 );
01943     pNtk = Kit_DsdExpand( pTemp = pNtk );      
01944     Kit_DsdNtkFree( pTemp );
01945     return pNtk;
01946 }

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 1959 of file kitDsd.c.

01960 {
01961     return Kit_DsdDecomposeInt( pTruth, nVars, nDecMux );
01962 }

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 1145 of file kitDsd.c.

01146 {
01147     Kit_DsdNtk_t * pNew;
01148     Kit_DsdObj_t * pObjNew;
01149     assert( p->nVars <= 16 );
01150     // create a new network
01151     pNew = Kit_DsdNtkAlloc( p->nVars );
01152     // consider simple special cases
01153     if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
01154     {
01155         pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
01156         pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) );
01157         return pNew;
01158     }
01159     if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
01160     {
01161         pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
01162         pObjNew->pFans[0] = Kit_DsdNtkRoot(p)->pFans[0];
01163         pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) );
01164         return pNew;
01165     }
01166     // convert the root node
01167     pNew->Root = Kit_DsdExpandNode_rec( pNew, p, p->Root );
01168     return pNew;
01169 }

unsigned Kit_DsdGetSupports ( Kit_DsdNtk_t * p )

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

Synopsis [Compute the support.]

Description []

SideEffects []

SeeAlso []

Definition at line 1455 of file kitDsd.c.

01456 {
01457     Kit_DsdObj_t * pRoot;
01458     unsigned uSupport;
01459     assert( p->pSupps == NULL );
01460     p->pSupps = ALLOC( unsigned, p->nNodes );
01461     // consider simple special cases
01462     pRoot = Kit_DsdNtkRoot(p);
01463     if ( pRoot->Type == KIT_DSD_CONST1 )
01464     {
01465         assert( p->nNodes == 1 );
01466         uSupport = p->pSupps[0] = 0;
01467     }
01468     if ( pRoot->Type == KIT_DSD_VAR )
01469     {
01470         assert( p->nNodes == 1 );
01471         uSupport = p->pSupps[0] = Kit_DsdLitSupport( p, pRoot->pFans[0] );
01472     }
01473     else
01474         uSupport = Kit_DsdGetSupports_rec( p, p->Root );
01475     assert( uSupport <= 0xFFFF );
01476     return uSupport;
01477 }

static int Kit_DsdLit2Var ( int Lit ) [inline, static]

Definition at line 144 of file kit.h.

00144 { return Lit >> 1;           }

static int Kit_DsdLitIsCompl ( int Lit ) [inline, static]

Definition at line 145 of file kit.h.

00145 { return Lit & 1;            }

static int Kit_DsdLitIsLeaf	(	Kit_DsdNtk_t *	pNtk,
		int	Lit
	)			`[inline, static]`

Definition at line 155 of file kit.h.

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

static int Kit_DsdLitNot ( int Lit ) [inline, static]

Definition at line 146 of file kit.h.

00146 { return Lit ^ 1;            }

static int Kit_DsdLitNotCond	(	int	Lit,
		int	c
	)			`[inline, static]`

Definition at line 147 of file kit.h.

00147 { return Lit ^ (int)(c > 0); }

static int Kit_DsdLitRegular ( int Lit ) [inline, static]

Definition at line 148 of file kit.h.

00148 { return Lit & 0xfe;         }

static unsigned Kit_DsdLitSupport	(	Kit_DsdNtk_t *	pNtk,
		int	Lit
	)			`[inline, static]`

Definition at line 156 of file kit.h.

00156 { int Id = Kit_DsdLit2Var(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
	)

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

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

Synopsis [Allocates the DSD manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file kitDsd.c.

00043 {
00044     Kit_DsdMan_t * p;
00045     p = ALLOC( Kit_DsdMan_t, 1 );
00046     memset( p, 0, sizeof(Kit_DsdMan_t) );
00047     p->nVars    = nVars;
00048     p->nWords   = Kit_TruthWordNum( p->nVars );
00049     p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
00050     p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords );
00051     p->dd       = Cloud_Init( 16, 14 );
00052     p->vTtBdds  = Vec_PtrAllocSimInfo( (1<<12), p->nWords );
00053     p->vNodes   = Vec_IntAlloc( 512 );
00054     return p;
00055 }

void Kit_DsdManFree ( Kit_DsdMan_t * p )

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

Synopsis [Deallocates the DSD manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file kitDsd.c.

00069 {
00070     Cloud_Quit( p->dd );
00071     Vec_IntFree( p->vNodes );
00072     Vec_PtrFree( p->vTtBdds );
00073     Vec_PtrFree( p->vTtElems );
00074     Vec_PtrFree( p->vTtNodes );
00075     free( p );
00076 }

int Kit_DsdNonDsdSizeMax ( Kit_DsdNtk_t * pNtk )

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

Synopsis [Counts the number of blocks of the given number of inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 969 of file kitDsd.c.

00970 {
00971     Kit_DsdObj_t * pObj;
00972     unsigned i, nSizeMax = 0;
00973     Kit_DsdNtkForEachObj( pNtk, pObj, i )
00974     {
00975         if ( pObj->Type != KIT_DSD_PRIME )
00976             continue;
00977         if ( nSizeMax < pObj->nFans )
00978             nSizeMax = pObj->nFans;
00979     }
00980     return nSizeMax;
00981 }

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 994 of file kitDsd.c.

00995 {
00996     Kit_DsdObj_t * pObj;
00997     unsigned i, uSupport = 0;
00998 //    FREE( pNtk->pSupps );
00999     Kit_DsdGetSupports( pNtk );
01000     Kit_DsdNtkForEachObj( pNtk, pObj, i )
01001     {
01002         if ( pObj->Type != KIT_DSD_PRIME )
01003             continue;
01004         uSupport |= Kit_DsdLitSupport( pNtk, Kit_DsdVar2Lit(pObj->Id,0) );
01005     }
01006     return uSupport;
01007 }

void Kit_DsdNtkFree ( Kit_DsdNtk_t * pNtk )

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

Synopsis [Deallocate the DSD network.]

Description []

SideEffects []

SeeAlso []

Definition at line 160 of file kitDsd.c.

00161 {
00162     Kit_DsdObj_t * pObj;
00163     unsigned i;
00164     Kit_DsdNtkForEachObj( pNtk, pObj, i )
00165         free( pObj );
00166     FREE( pNtk->pSupps );
00167     free( pNtk->pNodes );
00168     free( pNtk->pMem );
00169     free( pNtk );
00170 }

static Kit_DsdObj_t* Kit_DsdNtkObj	(	Kit_DsdNtk_t *	pNtk,
		int	Id
	)			`[inline, static]`

Definition at line 153 of file kit.h.

00153 { 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 ) [inline, static]

Definition at line 152 of file kit.h.

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

static Kit_DsdObj_t* Kit_DsdNtkRoot ( Kit_DsdNtk_t * pNtk ) [inline, static]

Definition at line 154 of file kit.h.

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

static unsigned Kit_DsdObjOffset ( int nFans ) [inline, static]

Definition at line 150 of file kit.h.

00150 { return (nFans >> 2) + ((nFans & 3) > 0);                    }

static unsigned* Kit_DsdObjTruth ( Kit_DsdObj_t * pObj ) [inline, static]

Definition at line 151 of file kit.h.

00151 { 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 265 of file kitDsd.c.

00266 {
00267     fprintf( pFile, "F = " );
00268     if ( Kit_DsdLitIsCompl(pNtk->Root) )
00269         fprintf( pFile, "!" );
00270     Kit_DsdPrint_rec( pFile, pNtk, Kit_DsdLit2Var(pNtk->Root) );
00271     fprintf( pFile, "\n" );
00272 }

void Kit_DsdPrintExpanded ( Kit_DsdNtk_t * pNtk )

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 285 of file kitDsd.c.

00286 {
00287     Kit_DsdNtk_t * pTemp;
00288     pTemp = Kit_DsdExpand( pNtk );
00289     Kit_DsdPrint( stdout, pTemp );
00290     Kit_DsdNtkFree( pTemp );
00291 }

void Kit_DsdPrintFromTruth	(	unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 304 of file kitDsd.c.

00305 {
00306     Kit_DsdNtk_t * pTemp;
00307     pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
00308     Kit_DsdVerify( pTemp, pTruth, nVars ); 
00309     Kit_DsdPrintExpanded( pTemp );
00310     Kit_DsdNtkFree( pTemp );
00311 }

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 1364 of file kitDsd.c.

01365 {
01366     Kit_DsdObj_t * pObj;
01367     unsigned * pIn, * pOut, * pTemp, k;
01368     int i, v, Temp, uSuppFanin, iFaninLit, WeightMax, FaninMax, nSwaps;
01369     int Weights[16];
01370     // go through the prime nodes
01371     Kit_DsdNtkForEachObj( p, pObj, i )
01372     {
01373         if ( pObj->Type != KIT_DSD_PRIME )
01374             continue;
01375         // count the fanin frequencies
01376         Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k )
01377         {
01378             uSuppFanin = Kit_DsdLitSupport( p, iFaninLit );
01379             Weights[k] = 0;
01380             for ( v = 0; v < 16; v++ )
01381                 if ( uSuppFanin & (1 << v) )
01382                     Weights[k] += pFreqs[v] - 1;
01383         }
01384         // find the most frequent fanin
01385         WeightMax = 0; 
01386         FaninMax = -1;
01387         for ( k = 0; k < pObj->nFans; k++ )
01388             if ( WeightMax < Weights[k] )
01389             {
01390                 WeightMax = Weights[k];
01391                 FaninMax = k;
01392             }
01393         // no need to reorder if there are no frequent fanins
01394         if ( FaninMax == -1 )
01395             continue;
01396         // move the fanins number k to the first place
01397         nSwaps = 0;
01398         pIn = Kit_DsdObjTruth(pObj);
01399         pOut = p->pMem;
01400 //        for ( v = FaninMax; v < ((int)pObj->nFans)-1; v++ )
01401         for ( v = FaninMax-1; v >= 0; v-- )
01402         {
01403             // swap the fanins
01404             Temp = pObj->pFans[v];
01405             pObj->pFans[v] = pObj->pFans[v+1];
01406             pObj->pFans[v+1] = Temp;
01407             // swap the truth table variables
01408             Kit_TruthSwapAdjacentVars( pOut, pIn, pObj->nFans, v );
01409             pTemp = pIn; pIn = pOut; pOut = pTemp;
01410             nSwaps++;
01411         }
01412         if ( nSwaps & 1 )
01413             Kit_TruthCopy( pOut, pIn, pObj->nFans );
01414     }    
01415 }

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 1326 of file kitDsd.c.

01327 {
01328     Kit_DsdNtk_t * pNew;
01329     Kit_DsdObj_t * pObjNew;
01330     assert( p->nVars <= 16 );
01331     // create a new network
01332     pNew = Kit_DsdNtkAlloc( p->nVars );
01333     // consider simple special cases
01334     if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 )
01335     {
01336         pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 );
01337         pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) );
01338         return pNew;
01339     }
01340     if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR )
01341     {
01342         pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 );
01343         pObjNew->pFans[0] = Kit_DsdNtkRoot(p)->pFans[0];
01344         pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) );
01345         return pNew;
01346     }
01347     // convert the root node
01348     pNew->Root = Kit_DsdShrink_rec( pNew, p, p->Root, pPrios );
01349     return pNew;
01350 }

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 826 of file kitDsd.c.

00827 {
00828     Kit_DsdMan_t * p;
00829     unsigned * pTruth;
00830     p = Kit_DsdManAlloc( pNtk->nVars, Kit_DsdNtkObjNum(pNtk) );
00831     pTruth = Kit_DsdTruthCompute( p, pNtk );
00832     Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
00833     Kit_DsdManFree( p );
00834 }

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 425 of file kitDsd.c.

00426 {
00427     unsigned * pTruthRes;
00428     int i;
00429     // assign elementary truth ables
00430     assert( pNtk->nVars <= p->nVars );
00431     for ( i = 0; i < (int)pNtk->nVars; i++ )
00432         Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars );
00433     // compute truth table for each node
00434     pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root) );
00435     // complement the truth table if needed
00436     if ( Kit_DsdLitIsCompl(pNtk->Root) )
00437         Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
00438     return pTruthRes;
00439 }

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 865 of file kitDsd.c.

00866 {
00867     unsigned * pTruth = Kit_DsdTruthComputeOne( p, pNtk, uSupp );
00868     Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
00869 /*
00870     // verification
00871     {
00872         // compute the same function using different procedure
00873         unsigned * pTruthTemp = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes + 1);
00874         pNtk->pSupps = NULL;
00875         Kit_DsdTruthComputeTwo( p, pNtk, uSupp, -1, pTruthTemp );
00876 //        if ( !Kit_TruthIsEqual( pTruthTemp, pTruthRes, pNtk->nVars ) )
00877         if ( !Kit_TruthIsEqualWithPhase( pTruthTemp, pTruthRes, pNtk->nVars ) )
00878         {
00879             printf( "Verification FAILED!\n" );
00880             Kit_DsdPrint( stdout, pNtk );
00881             Kit_DsdPrintFromTruth( pTruthRes, pNtk->nVars );
00882             Kit_DsdPrintFromTruth( pTruthTemp, pNtk->nVars );
00883         }
00884 //        else
00885 //            printf( "Verification successful.\n" );
00886     }
00887 */
00888 }

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 847 of file kitDsd.c.

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

static int Kit_DsdVar2Lit	(	int	Var,
		int	fCompl
	)			`[inline, static]`

Definition at line 143 of file kit.h.

00143 { return Var + Var + fCompl; }

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 2080 of file kitDsd.c.

02081 {
02082     Kit_DsdMan_t * p;
02083     unsigned * pTruthC;
02084     p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk)+2 );
02085     pTruthC = Kit_DsdTruthCompute( p, pNtk );
02086     if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
02087         printf( "Verification failed.\n" );
02088     Kit_DsdManFree( p );
02089 }

static Kit_Edge_t Kit_EdgeCreate	(	int	Node,
		int	fCompl
	)			`[inline, static]`

Definition at line 204 of file kit.h.

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

static unsigned Kit_EdgeToInt ( Kit_Edge_t eEdge ) [inline, static]

Definition at line 205 of file kit.h.

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

static unsigned Kit_EdgeToInt_ ( Kit_Edge_t eEdge ) [inline, static]

Definition at line 207 of file kit.h.

00207 { return *(unsigned *)&eEdge;                         }

static int Kit_Float2Int ( float Val ) [inline, static]

Definition at line 229 of file kit.h.

00229 { return *((int *)&Val);               }

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 169 of file kitGraph.c.

00170 {
00171     Kit_Node_t * pNode;
00172     // get the new node
00173     pNode = Kit_GraphAppendNode( pGraph );
00174     // set the inputs and other info
00175     pNode->eEdge0 = eEdge0;
00176     pNode->eEdge1 = eEdge1;
00177     pNode->fCompl0 = eEdge0.fCompl;
00178     pNode->fCompl1 = eEdge1.fCompl;
00179     return Kit_EdgeCreate( pGraph->nSize - 1, 0 );
00180 }

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 262 of file kitGraph.c.

00263 {
00264     Kit_Edge_t eNode0, eNode1, eNode;
00265     if ( Type == 0 )
00266     {
00267         // derive the first AND
00268         eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
00269         // derive the second AND
00270         eEdgeC.fCompl ^= 1;
00271         eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
00272         // derive the final OR
00273         eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
00274     }
00275     else
00276     {
00277         // complement the arguments
00278         eEdgeT.fCompl ^= 1;
00279         eEdgeE.fCompl ^= 1;
00280         // derive the first AND
00281         eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
00282         // derive the second AND
00283         eEdgeC.fCompl ^= 1;
00284         eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
00285         // derive the final OR
00286         eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
00287         eNode.fCompl ^= 1;
00288     }
00289     return eNode;
00290 }

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 193 of file kitGraph.c.

00194 {
00195     Kit_Node_t * pNode;
00196     // get the new node
00197     pNode = Kit_GraphAppendNode( pGraph );
00198     // set the inputs and other info
00199     pNode->eEdge0 = eEdge0;
00200     pNode->eEdge1 = eEdge1;
00201     pNode->fCompl0 = eEdge0.fCompl;
00202     pNode->fCompl1 = eEdge1.fCompl;
00203     // make adjustments for the OR gate
00204     pNode->fNodeOr = 1;
00205     pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl;
00206     pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl;
00207     return Kit_EdgeCreate( pGraph->nSize - 1, 1 );
00208 }

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 221 of file kitGraph.c.

00222 {
00223     Kit_Edge_t eNode0, eNode1, eNode;
00224     if ( Type == 0 )
00225     {
00226         // derive the first AND
00227         eEdge0.fCompl ^= 1;
00228         eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
00229         eEdge0.fCompl ^= 1;
00230         // derive the second AND
00231         eEdge1.fCompl ^= 1;
00232         eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
00233         // derive the final OR
00234         eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
00235     }
00236     else
00237     {
00238         // derive the first AND
00239         eNode0 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
00240         // derive the second AND
00241         eEdge0.fCompl ^= 1;
00242         eEdge1.fCompl ^= 1;
00243         eNode1 = Kit_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
00244         // derive the final OR
00245         eNode = Kit_GraphAddNodeOr( pGraph, eNode0, eNode1 );
00246         eNode.fCompl ^= 1;
00247     }
00248     return eNode;
00249 }

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 145 of file kitGraph.c.

00146 {
00147     Kit_Node_t * pNode;
00148     if ( pGraph->nSize == pGraph->nCap )
00149     {
00150         pGraph->pNodes = REALLOC( Kit_Node_t, pGraph->pNodes, 2 * pGraph->nCap ); 
00151         pGraph->nCap   = 2 * pGraph->nCap;
00152     }
00153     pNode = pGraph->pNodes + pGraph->nSize++;
00154     memset( pNode, 0, sizeof(Kit_Node_t) );
00155     return pNode;
00156 }

static void Kit_GraphComplement ( Kit_Graph_t * pGraph ) [inline, static]

Definition at line 215 of file kit.h.

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

Kit_Graph_t* Kit_GraphCreate ( int nLeaves )

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file kitGraph.c.

00043 {
00044     Kit_Graph_t * pGraph;
00045     pGraph = ALLOC( Kit_Graph_t, 1 );
00046     memset( pGraph, 0, sizeof(Kit_Graph_t) );
00047     pGraph->nLeaves = nLeaves;
00048     pGraph->nSize = nLeaves;
00049     pGraph->nCap = 2 * nLeaves + 50;
00050     pGraph->pNodes = ALLOC( Kit_Node_t, pGraph->nCap );
00051     memset( pGraph->pNodes, 0, sizeof(Kit_Node_t) * pGraph->nSize );
00052     return pGraph;
00053 }

Kit_Graph_t* Kit_GraphCreateConst0 ( )

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

Synopsis [Creates constant 0 graph.]

Description []

SideEffects []

SeeAlso []

Definition at line 66 of file kitGraph.c.

00067 {
00068     Kit_Graph_t * pGraph;
00069     pGraph = ALLOC( Kit_Graph_t, 1 );
00070     memset( pGraph, 0, sizeof(Kit_Graph_t) );
00071     pGraph->fConst = 1;
00072     pGraph->eRoot.fCompl = 1;
00073     return pGraph;
00074 }

Kit_Graph_t* Kit_GraphCreateConst1 ( )

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

Synopsis [Creates constant 1 graph.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file kitGraph.c.

00088 {
00089     Kit_Graph_t * pGraph;
00090     pGraph = ALLOC( Kit_Graph_t, 1 );
00091     memset( pGraph, 0, sizeof(Kit_Graph_t) );
00092     pGraph->fConst = 1;
00093     return pGraph;
00094 }

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

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

Synopsis [Creates the literal graph.]

Description []

SideEffects []

SeeAlso []

Definition at line 107 of file kitGraph.c.

00108 {
00109     Kit_Graph_t * pGraph;
00110     assert( 0 <= iLeaf && iLeaf < nLeaves );
00111     pGraph = Kit_GraphCreate( nLeaves );
00112     pGraph->eRoot.Node   = iLeaf;
00113     pGraph->eRoot.fCompl = fCompl;
00114     return pGraph;
00115 }

void Kit_GraphFree ( Kit_Graph_t * pGraph )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file kitGraph.c.

00129 {
00130     FREE( pGraph->pNodes );
00131     free( pGraph );
00132 }

static int Kit_GraphIsComplement ( Kit_Graph_t * pGraph ) [inline, static]

Definition at line 213 of file kit.h.

00213 { return pGraph->eRoot.fCompl;                        }

static int Kit_GraphIsConst ( Kit_Graph_t * pGraph ) [inline, static]

Definition at line 210 of file kit.h.

00210 { return pGraph->fConst;                              }

static int Kit_GraphIsConst0 ( Kit_Graph_t * pGraph ) [inline, static]

Definition at line 211 of file kit.h.

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

static int Kit_GraphIsConst1 ( Kit_Graph_t * pGraph ) [inline, static]

Definition at line 212 of file kit.h.

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

static int Kit_GraphIsVar ( Kit_Graph_t * pGraph ) [inline, static]

Definition at line 214 of file kit.h.

00214 { 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 380 of file kitGraph.c.

00381 {
00382     int Depth0, Depth1, Depth;
00383     if ( pNode == pLeaf )
00384         return 0;
00385     if ( Kit_GraphNodeIsVar(pGraph, pNode) )
00386         return -100;
00387     Depth0 = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeFanin0(pGraph, pNode), pLeaf );
00388     Depth1 = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeFanin1(pGraph, pNode), pLeaf );
00389     Depth = KIT_MAX( Depth0, Depth1 );
00390     Depth = (Depth == -100) ? -100 : Depth + 1;
00391     return Depth;
00392 }

static int Kit_GraphLeaveNum ( Kit_Graph_t * pGraph ) [inline, static]

Definition at line 217 of file kit.h.

00217 { return pGraph->nLeaves;                             }

static Kit_Node_t* Kit_GraphNode	(	Kit_Graph_t *	pGraph,
		int	i
	)			`[inline, static]`

Definition at line 219 of file kit.h.

00219 { return pGraph->pNodes + i;                          }

static Kit_Node_t* Kit_GraphNodeFanin0	(	Kit_Graph_t *	pGraph,
		Kit_Node_t *	pNode
	)			`[inline, static]`

Definition at line 225 of file kit.h.

00225 { 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
	)			`[inline, static]`

Definition at line 226 of file kit.h.

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

static int Kit_GraphNodeInt	(	Kit_Graph_t *	pGraph,
		Kit_Node_t *	pNode
	)			`[inline, static]`

Definition at line 221 of file kit.h.

00221 { return pNode - pGraph->pNodes;                      }

static int Kit_GraphNodeIsVar	(	Kit_Graph_t *	pGraph,
		Kit_Node_t *	pNode
	)			`[inline, static]`

Definition at line 222 of file kit.h.

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

static Kit_Node_t* Kit_GraphNodeLast ( Kit_Graph_t * pGraph ) [inline, static]

Definition at line 220 of file kit.h.

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

static int Kit_GraphNodeNum ( Kit_Graph_t * pGraph ) [inline, static]

Definition at line 218 of file kit.h.

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

static int Kit_GraphRootLevel ( Kit_Graph_t * pGraph ) [inline, static]

Definition at line 227 of file kit.h.

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

static void Kit_GraphSetRoot	(	Kit_Graph_t *	pGraph,
		Kit_Edge_t	eRoot
	)			`[inline, static]`

Definition at line 216 of file kit.h.

00216 { pGraph->eRoot = eRoot;                              }

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

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

Synopsis [Converts graph to BDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 88 of file kitBdd.c.

00089 {
00090     DdNode * bFunc, * bFunc0, * bFunc1;
00091     Kit_Node_t * pNode;
00092     int i;
00093 
00094     // sanity checks
00095     assert( Kit_GraphLeaveNum(pGraph) >= 0 );
00096     assert( Kit_GraphLeaveNum(pGraph) <= pGraph->nSize );
00097 
00098     // check for constant function
00099     if ( Kit_GraphIsConst(pGraph) )
00100         return Cudd_NotCond( b1, Kit_GraphIsComplement(pGraph) );
00101     // check for a literal
00102     if ( Kit_GraphIsVar(pGraph) )
00103         return Cudd_NotCond( Cudd_bddIthVar(dd, Kit_GraphVarInt(pGraph)), Kit_GraphIsComplement(pGraph) );
00104 
00105     // assign the elementary variables
00106     Kit_GraphForEachLeaf( pGraph, pNode, i )
00107         pNode->pFunc = Cudd_bddIthVar( dd, i );
00108 
00109     // compute the function for each internal node
00110     Kit_GraphForEachNode( pGraph, pNode, i )
00111     {
00112         bFunc0 = Cudd_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
00113         bFunc1 = Cudd_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
00114         pNode->pFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( pNode->pFunc );
00115     }
00116 
00117     // deref the intermediate results
00118     bFunc = pNode->pFunc;   Cudd_Ref( bFunc );
00119     Kit_GraphForEachNode( pGraph, pNode, i )
00120         Cudd_RecursiveDeref( dd, pNode->pFunc );
00121     Cudd_Deref( bFunc );
00122 
00123     // complement the result if necessary
00124     return Cudd_NotCond( bFunc, Kit_GraphIsComplement(pGraph) );
00125 }

unsigned Kit_GraphToTruth ( Kit_Graph_t * pGraph )

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

Synopsis [Derives the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 303 of file kitGraph.c.

00304 {
00305     unsigned uTruths[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
00306     unsigned uTruth = 0, uTruth0, uTruth1;
00307     Kit_Node_t * pNode;
00308     int i;
00309 
00310     // sanity checks
00311     assert( Kit_GraphLeaveNum(pGraph) >= 0 );
00312     assert( Kit_GraphLeaveNum(pGraph) <= pGraph->nSize );
00313     assert( Kit_GraphLeaveNum(pGraph) <= 5 );
00314 
00315     // check for constant function
00316     if ( Kit_GraphIsConst(pGraph) )
00317         return Kit_GraphIsComplement(pGraph)? 0 : ~((unsigned)0);
00318     // check for a literal
00319     if ( Kit_GraphIsVar(pGraph) )
00320         return Kit_GraphIsComplement(pGraph)? ~uTruths[Kit_GraphVarInt(pGraph)] : uTruths[Kit_GraphVarInt(pGraph)];
00321 
00322     // assign the elementary variables
00323     Kit_GraphForEachLeaf( pGraph, pNode, i )
00324         pNode->pFunc = (void *)(long)uTruths[i];
00325 
00326     // compute the function for each internal node
00327     Kit_GraphForEachNode( pGraph, pNode, i )
00328     {
00329         uTruth0 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc;
00330         uTruth1 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc;
00331         uTruth0 = pNode->eEdge0.fCompl? ~uTruth0 : uTruth0;
00332         uTruth1 = pNode->eEdge1.fCompl? ~uTruth1 : uTruth1;
00333         uTruth = uTruth0 & uTruth1;
00334         pNode->pFunc = (void *)(long)uTruth;
00335     }
00336 
00337     // complement the result if necessary
00338     return Kit_GraphIsComplement(pGraph)? ~uTruth : uTruth;
00339 }

static Kit_Node_t* Kit_GraphVar ( Kit_Graph_t * pGraph ) [inline, static]

Definition at line 223 of file kit.h.

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

static int Kit_GraphVarInt ( Kit_Graph_t * pGraph ) [inline, static]

Definition at line 224 of file kit.h.

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

static float Kit_Int2Float ( int Num ) [inline, static]

Definition at line 230 of file kit.h.

00230 { return *((float *)&Num);             }

static Kit_Edge_t Kit_IntToEdge ( unsigned Edge ) [inline, static]

Definition at line 206 of file kit.h.

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

static Kit_Edge_t Kit_IntToEdge_ ( unsigned Edge ) [inline, static]

Definition at line 208 of file kit.h.

00208 { return *(Kit_Edge_t *)&Edge;                        }

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 365 of file kitSop.c.

00366 {
00367     unsigned uCube;
00368     int i, k, nLitsCur;
00369     // go through each literal
00370     for ( i = 0; i < nLits; i++ )
00371     {
00372         // go through all the cubes
00373         nLitsCur = 0;
00374         Kit_SopForEachCube( cSop, uCube, k )
00375             if ( Kit_CubeHasLit(uCube, i) )
00376                 nLitsCur++;
00377         if ( nLitsCur > 1 )
00378             return i;
00379     }
00380     return -1;
00381 }

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 555 of file kitSop.c.

00556 {
00557     int iLitBest;
00558     // get the best literal
00559     iLitBest = Kit_SopBestLiteral( cSop, nLits, uCube );
00560     // start the cover
00561     cResult->nCubes = 0;
00562     cResult->pCubes = Vec_IntFetch( vMemory, 1 );
00563     // set the cube
00564     Kit_SopPushCube( cResult, Kit_CubeSetLit(0, iLitBest) );
00565 }

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 345 of file kitSop.c.

00346 {
00347     assert( Kit_SopCubeNum(cSop) > 0 );
00348     cResult->nCubes = 0;
00349     cResult->pCubes = Vec_IntFetch( vMemory, 1 );
00350     Kit_SopPushCube( cResult, Kit_SopCommonCube(cSop) );
00351 }

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

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

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

Synopsis [Creates SOP from the cube array.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file kitSop.c.

00043 {
00044     unsigned uCube;
00045     int i;
00046     // start the cover
00047     cResult->nCubes = 0;
00048     cResult->pCubes = Vec_IntFetch( vMemory, Vec_IntSize(vInput) );
00049     // add the cubes
00050     Vec_IntForEachEntry( vInput, uCube, i )
00051         Kit_SopPushCube( cResult, uCube );
00052 }

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 65 of file kitSop.c.

00066 {
00067     unsigned uCube, uMask = 0;
00068     int i, nCubes = Vec_IntSize(vInput);
00069     // start the cover
00070     cResult->nCubes = 0;
00071     cResult->pCubes = Vec_IntFetch( vMemory, nCubes );
00072     // add the cubes
00073 //    Vec_IntForEachEntry( vInput, uCube, i )
00074     for ( i = 0; i < nCubes; i++ )
00075     {
00076         uCube = Vec_IntEntry( vInput, i );
00077         uMask = ((uCube | (uCube >> 1)) & 0x55555555);
00078         uMask |= (uMask << 1);
00079         Kit_SopPushCube( cResult, uCube ^ uMask );
00080     }
00081 }

static unsigned Kit_SopCube	(	Kit_Sop_t *	cSop,
		int	i
	)			`[inline, static]`

Definition at line 199 of file kit.h.

00199 { return cSop->pCubes[i];                 }

static int Kit_SopCubeNum ( Kit_Sop_t * cSop ) [inline, static]

Definition at line 198 of file kit.h.

00198 { 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 142 of file kitSop.c.

00143 {
00144     unsigned uCube, uDiv;
00145     int i;
00146     // get the only cube
00147     assert( Kit_SopCubeNum(cDiv) == 1 );
00148     uDiv = Kit_SopCube(cDiv, 0);
00149     // allocate covers
00150     vQuo->nCubes = 0;
00151     vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
00152     vRem->nCubes = 0;
00153     vRem->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
00154     // sort the cubes
00155     Kit_SopForEachCube( cSop, uCube, i )
00156     {
00157         if ( Kit_CubeContains( uCube, uDiv ) )
00158             Kit_SopPushCube( vQuo, Kit_CubeSharp(uCube, uDiv) );
00159         else
00160             Kit_SopPushCube( vRem, uCube );
00161     }
00162 }

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 118 of file kitSop.c.

00119 {
00120     unsigned uCube;
00121     int i, k = 0;
00122     Kit_SopForEachCube( cSop, uCube, i )
00123     {
00124         if ( Kit_CubeHasLit(uCube, iLit) )
00125             Kit_SopWriteCube( cSop, Kit_CubeRemLit(uCube, iLit), k++ );
00126     }
00127     Kit_SopShrink( cSop, k );
00128 }

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 175 of file kitSop.c.

00176 {
00177     unsigned uCube, uDiv, uCube2, uDiv2, uQuo;
00178     int i, i2, k, k2, nCubesRem;
00179     assert( Kit_SopCubeNum(cSop) >= Kit_SopCubeNum(cDiv) );
00180     // consider special case
00181     if ( Kit_SopCubeNum(cDiv) == 1 )
00182     {
00183         Kit_SopDivideByCube( cSop, cDiv, vQuo, vRem, vMemory );
00184         return;
00185     }
00186     // allocate quotient
00187     vQuo->nCubes = 0;
00188     vQuo->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) / Kit_SopCubeNum(cDiv) );
00189     // for each cube of the cover
00190     // it either belongs to the quotient or to the remainder
00191     Kit_SopForEachCube( cSop, uCube, i )
00192     {
00193         // skip taken cubes
00194         if ( Kit_CubeIsMarked(uCube) )
00195             continue;
00196         // find a matching cube in the divisor
00197         uDiv = ~0;
00198         Kit_SopForEachCube( cDiv, uDiv, k )
00199             if ( Kit_CubeContains( uCube, uDiv ) )
00200                 break;
00201         // the cube is not found 
00202         if ( k == Kit_SopCubeNum(cDiv) )
00203             continue;
00204         // the quotient cube exists
00205         uQuo = Kit_CubeSharp( uCube, uDiv );
00206         // find corresponding cubes for other cubes of the divisor
00207         uDiv2 = ~0;
00208         Kit_SopForEachCube( cDiv, uDiv2, k2 )
00209         {
00210             if ( k2 == k )
00211                 continue;
00212             // find a matching cube
00213             Kit_SopForEachCube( cSop, uCube2, i2 )
00214             {
00215                 // skip taken cubes
00216                 if ( Kit_CubeIsMarked(uCube2) )
00217                     continue;
00218                 // check if the cube can be used
00219                 if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
00220                     break;
00221             }
00222             // the case when the cube is not found
00223             if ( i2 == Kit_SopCubeNum(cSop) )
00224                 break;
00225         }
00226         // we did not find some cubes - continue looking at other cubes
00227         if ( k2 != Kit_SopCubeNum(cDiv) )
00228             continue;
00229         // we found all cubes - add the quotient cube
00230         Kit_SopPushCube( vQuo, uQuo );
00231 
00232         // mark the first cube
00233         Kit_SopWriteCube( cSop, Kit_CubeMark(uCube), i );
00234         // mark other cubes that have this quotient
00235         Kit_SopForEachCube( cDiv, uDiv2, k2 )
00236         {
00237             if ( k2 == k )
00238                 continue;
00239             // find a matching cube
00240             Kit_SopForEachCube( cSop, uCube2, i2 )
00241             {
00242                 // skip taken cubes
00243                 if ( Kit_CubeIsMarked(uCube2) )
00244                     continue;
00245                 // check if the cube can be used
00246                 if ( Kit_CubeContains( uCube2, uDiv2 ) && uQuo == Kit_CubeSharp( uCube2, uDiv2 ) )
00247                     break;
00248             }
00249             assert( i2 < Kit_SopCubeNum(cSop) );
00250             // the cube is found, mark it 
00251             // (later we will add all unmarked cubes to the remainder)
00252             Kit_SopWriteCube( cSop, Kit_CubeMark(uCube2), i2 );
00253         }
00254     }
00255     // determine the number of cubes in the remainder
00256     nCubesRem = Kit_SopCubeNum(cSop) - Kit_SopCubeNum(vQuo) * Kit_SopCubeNum(cDiv);
00257     // allocate remainder
00258     vRem->nCubes = 0;
00259     vRem->pCubes = Vec_IntFetch( vMemory, nCubesRem );
00260     // finally add the remaining unmarked cubes to the remainder 
00261     // and clean the marked cubes in the cover
00262     Kit_SopForEachCube( cSop, uCube, i )
00263     {
00264         if ( !Kit_CubeIsMarked(uCube) )
00265         {
00266             Kit_SopPushCube( vRem, uCube );
00267             continue;
00268         }
00269         Kit_SopWriteCube( cSop, Kit_CubeUnmark(uCube), i );
00270     }
00271     assert( nCubesRem == Kit_SopCubeNum(vRem) );
00272 }

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 529 of file kitSop.c.

00530 {
00531     if ( Kit_SopCubeNum(cSop) <= 1 )
00532         return 0;
00533     if ( Kit_SopAnyLiteral( cSop, nLits ) == -1 )
00534         return 0;
00535     // duplicate the cover
00536     Kit_SopDup( cResult, cSop, vMemory );
00537     // perform the kerneling
00538     Kit_SopDivisorZeroKernel_rec( cResult, nLits );
00539     assert( Kit_SopCubeNum(cResult) > 0 );
00540     return 1;
00541 }

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 94 of file kitSop.c.

00095 {
00096     unsigned uCube;
00097     int i;
00098     // start the cover
00099     cResult->nCubes = 0;
00100     cResult->pCubes = Vec_IntFetch( vMemory, Kit_SopCubeNum(cSop) );
00101     // add the cubes
00102     Kit_SopForEachCube( cSop, uCube, i )
00103         Kit_SopPushCube( cResult, uCube );
00104 }

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 52 of file kitFactor.c.

00053 {
00054     Kit_Sop_t Sop, * cSop = &Sop;
00055     Kit_Graph_t * pFForm;
00056     Kit_Edge_t eRoot;
00057 //    int nCubes;
00058 
00059     // works for up to 15 variables because divisin procedure
00060     // used the last bit for marking the cubes going to the remainder
00061     assert( nVars < 16 );
00062 
00063     // check for trivial functions
00064     if ( Vec_IntSize(vCover) == 0 )
00065         return Kit_GraphCreateConst0();
00066     if ( Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0 )
00067         return Kit_GraphCreateConst1();
00068 
00069     // prepare memory manager
00070 //    Vec_IntClear( vMemory );
00071     Vec_IntGrow( vMemory, KIT_FACTOR_MEM_LIMIT );
00072 
00073     // perform CST
00074     Kit_SopCreateInverse( cSop, vCover, 2 * nVars, vMemory ); // CST
00075 
00076     // start the factored form
00077     pFForm = Kit_GraphCreate( nVars );
00078     // factor the cover
00079     eRoot = Kit_SopFactor_rec( pFForm, cSop, 2 * nVars, vMemory );
00080     // finalize the factored form
00081     Kit_GraphSetRoot( pFForm, eRoot );
00082     if ( fCompl )
00083         Kit_GraphComplement( pFForm );
00084 
00085     // verify the factored form
00086 //    nCubes = Vec_IntSize(vCover);
00087 //    Vec_IntShrink( vCover, nCubes );
00088 //    if ( !Kit_SopFactorVerify( vCover, pFForm, nVars ) )
00089 //        printf( "Verification has failed.\n" );
00090     return pFForm;
00091 }

int Kit_SopIsCubeFree ( Kit_Sop_t * cSop )

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 329 of file kitSop.c.

00330 {
00331     return Kit_SopCommonCube( cSop ) == 0;
00332 }

void Kit_SopMakeCubeFree ( Kit_Sop_t * cSop )

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

Synopsis [Makes the cover cube-free.]

Description []

SideEffects []

SeeAlso []

Definition at line 306 of file kitSop.c.

00307 {
00308     unsigned uMask, uCube;
00309     int i;
00310     uMask = Kit_SopCommonCube( cSop );
00311     if ( uMask == 0 )
00312         return;
00313     // remove the common cube
00314     Kit_SopForEachCube( cSop, uCube, i )
00315         Kit_SopWriteCube( cSop, Kit_CubeSharp(uCube, uMask), i );
00316 }

static void Kit_SopPushCube	(	Kit_Sop_t *	cSop,
		unsigned	uCube
	)			`[inline, static]`

Definition at line 201 of file kit.h.

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

static void Kit_SopShrink	(	Kit_Sop_t *	cSop,
		int	nCubesNew
	)			`[inline, static]`

Definition at line 200 of file kit.h.

00200 { cSop->nCubes = nCubesNew;               }

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

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

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

Synopsis [Derives the BDD for the given SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file kitBdd.c.

00044 {
00045     DdNode * bSum, * bCube, * bTemp, * bVar;
00046     unsigned uCube;
00047     int Value, i, v;
00048     assert( nVars < 16 );
00049     // start the cover
00050     bSum = Cudd_ReadLogicZero(dd);   Cudd_Ref( bSum );
00051    // check the logic function of the node
00052     Kit_SopForEachCube( cSop, uCube, i )
00053     {
00054         bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
00055         for ( v = 0; v < nVars; v++ )
00056         {
00057             Value = ((uCube >> 2*v) & 3);
00058             if ( Value == 1 )
00059                 bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
00060             else if ( Value == 2 )
00061                 bVar = Cudd_bddIthVar( dd, v );
00062             else
00063                 continue;
00064             bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
00065             Cudd_RecursiveDeref( dd, bTemp );
00066         }
00067         bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );   
00068         Cudd_Ref( bSum );
00069         Cudd_RecursiveDeref( dd, bTemp );
00070         Cudd_RecursiveDeref( dd, bCube );
00071     }
00072     // complement the result if necessary
00073     Cudd_Deref( bSum );
00074     return bSum;
00075 }

static void Kit_SopWriteCube	(	Kit_Sop_t *	cSop,
		unsigned	uCube,
		int	i
	)			`[inline, static]`

Definition at line 202 of file kit.h.

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

static void Kit_TruthAnd	(	unsigned *	pOut,
		unsigned *	pIn0,
		unsigned *	pIn1,
		int	nVars
	)			`[inline, static]`

Definition at line 379 of file kit.h.

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

static void Kit_TruthAndPhase	(	unsigned *	pOut,
		unsigned *	pIn0,
		unsigned *	pIn1,
		int	nVars,
		int	fCompl0,
		int	fCompl1
	)			`[inline, static]`

Definition at line 409 of file kit.h.

00410 {
00411     int w;
00412     if ( fCompl0 && fCompl1 )
00413     {
00414         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00415             pOut[w] = ~(pIn0[w] | pIn1[w]);
00416     }
00417     else if ( fCompl0 && !fCompl1 )
00418     {
00419         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00420             pOut[w] = ~pIn0[w] & pIn1[w];
00421     }
00422     else if ( !fCompl0 && fCompl1 )
00423     {
00424         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00425             pOut[w] = pIn0[w] & ~pIn1[w];
00426     }
00427     else // if ( !fCompl0 && !fCompl1 )
00428     {
00429         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00430             pOut[w] = pIn0[w] & pIn1[w];
00431     }
00432 }

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

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

Synopsis [Find the best cofactoring variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 1127 of file kitTruth.c.

01128 {
01129     int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
01130     if ( Kit_TruthIsConst0(pTruth, nVars) || Kit_TruthIsConst1(pTruth, nVars) )
01131         return -1;
01132     // iterate through variables
01133     iBestVar = -1;
01134     nSuppSizeMin = KIT_INFINITY;
01135     for ( i = 0; i < nVars; i++ )
01136     {
01137         // cofactor the functiona and get support sizes
01138         Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
01139         Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
01140         nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
01141         nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
01142         nSuppSizeCur  = nSuppSizeCur0 + nSuppSizeCur1;
01143         // compare this variable with other variables
01144         if ( nSuppSizeMin > nSuppSizeCur ) 
01145         {
01146             nSuppSizeMin = nSuppSizeCur;
01147             iBestVar = i;
01148         }
01149     }
01150     assert( iBestVar != -1 );
01151     // cofactor w.r.t. this variable
01152     Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
01153     Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
01154     return iBestVar;
01155 }

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 1021 of file kitTruth.c.

01022 {
01023     int nWords = Kit_TruthWordNum( nVars );
01024     int i, k, Step;
01025     unsigned Temp;
01026 
01027     assert( iVar < nVars );
01028     switch ( iVar )
01029     {
01030     case 0:
01031         for ( i = 0; i < nWords; i++ )
01032             pTruth[i] = ((pTruth[i] & 0x55555555) << 1) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
01033         return;
01034     case 1:
01035         for ( i = 0; i < nWords; i++ )
01036             pTruth[i] = ((pTruth[i] & 0x33333333) << 2) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
01037         return;
01038     case 2:
01039         for ( i = 0; i < nWords; i++ )
01040             pTruth[i] = ((pTruth[i] & 0x0F0F0F0F) << 4) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
01041         return;
01042     case 3:
01043         for ( i = 0; i < nWords; i++ )
01044             pTruth[i] = ((pTruth[i] & 0x00FF00FF) << 8) | ((pTruth[i] & 0xFF00FF00) >> 8);
01045         return;
01046     case 4:
01047         for ( i = 0; i < nWords; i++ )
01048             pTruth[i] = ((pTruth[i] & 0x0000FFFF) << 16) | ((pTruth[i] & 0xFFFF0000) >> 16);
01049         return;
01050     default:
01051         Step = (1 << (iVar - 5));
01052         for ( k = 0; k < nWords; k += 2*Step )
01053         {
01054             for ( i = 0; i < Step; i++ )
01055             {
01056                 Temp = pTruth[i];
01057                 pTruth[i] = pTruth[Step+i];
01058                 pTruth[Step+i] = Temp;
01059             }
01060             pTruth += 2*Step;
01061         }
01062         return;
01063     }
01064 }

static void Kit_TruthClear	(	unsigned *	pOut,
		int	nVars
	)			`[inline, static]`

Definition at line 361 of file kit.h.

00362 {
00363     int w;
00364     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00365         pOut[w] = 0;
00366 }

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

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

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file kitTruth.c.

00329 {
00330     int nWords = Kit_TruthWordNum( nVars );
00331     int i, k, Step;
00332 
00333     assert( iVar < nVars );
00334     switch ( iVar )
00335     {
00336     case 0:
00337         for ( i = 0; i < nWords; i++ )
00338             pTruth[i] = (pTruth[i] & 0x55555555) | ((pTruth[i] & 0x55555555) << 1);
00339         return;
00340     case 1:
00341         for ( i = 0; i < nWords; i++ )
00342             pTruth[i] = (pTruth[i] & 0x33333333) | ((pTruth[i] & 0x33333333) << 2);
00343         return;
00344     case 2:
00345         for ( i = 0; i < nWords; i++ )
00346             pTruth[i] = (pTruth[i] & 0x0F0F0F0F) | ((pTruth[i] & 0x0F0F0F0F) << 4);
00347         return;
00348     case 3:
00349         for ( i = 0; i < nWords; i++ )
00350             pTruth[i] = (pTruth[i] & 0x00FF00FF) | ((pTruth[i] & 0x00FF00FF) << 8);
00351         return;
00352     case 4:
00353         for ( i = 0; i < nWords; i++ )
00354             pTruth[i] = (pTruth[i] & 0x0000FFFF) | ((pTruth[i] & 0x0000FFFF) << 16);
00355         return;
00356     default:
00357         Step = (1 << (iVar - 5));
00358         for ( k = 0; k < nWords; k += 2*Step )
00359         {
00360             for ( i = 0; i < Step; i++ )
00361                 pTruth[Step+i] = pTruth[i];
00362             pTruth += 2*Step;
00363         }
00364         return;
00365     }
00366 }

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 430 of file kitTruth.c.

00431 {
00432     int nWords = Kit_TruthWordNum( nVars );
00433     int i, k, Step;
00434 
00435     assert( iVar < nVars );
00436     switch ( iVar )
00437     {
00438     case 0:
00439         for ( i = 0; i < nWords; i++ )
00440             pOut[i] = (pIn[i] & 0x55555555) | ((pIn[i] & 0x55555555) << 1);
00441         return;
00442     case 1:
00443         for ( i = 0; i < nWords; i++ )
00444             pOut[i] = (pIn[i] & 0x33333333) | ((pIn[i] & 0x33333333) << 2);
00445         return;
00446     case 2:
00447         for ( i = 0; i < nWords; i++ )
00448             pOut[i] = (pIn[i] & 0x0F0F0F0F) | ((pIn[i] & 0x0F0F0F0F) << 4);
00449         return;
00450     case 3:
00451         for ( i = 0; i < nWords; i++ )
00452             pOut[i] = (pIn[i] & 0x00FF00FF) | ((pIn[i] & 0x00FF00FF) << 8);
00453         return;
00454     case 4:
00455         for ( i = 0; i < nWords; i++ )
00456             pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i] & 0x0000FFFF) << 16);
00457         return;
00458     default:
00459         Step = (1 << (iVar - 5));
00460         for ( k = 0; k < nWords; k += 2*Step )
00461         {
00462             for ( i = 0; i < Step; i++ )
00463                 pOut[i] = pOut[Step+i] = pIn[i];
00464             pIn += 2*Step;
00465             pOut += 2*Step;
00466         }
00467         return;
00468     }
00469 }

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

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 379 of file kitTruth.c.

00380 {
00381     int nWords = Kit_TruthWordNum( nVars );
00382     int i, k, Step;
00383 
00384     assert( iVar < nVars );
00385     switch ( iVar )
00386     {
00387     case 0:
00388         for ( i = 0; i < nWords; i++ )
00389             pTruth[i] = (pTruth[i] & 0xAAAAAAAA) | ((pTruth[i] & 0xAAAAAAAA) >> 1);
00390         return;
00391     case 1:
00392         for ( i = 0; i < nWords; i++ )
00393             pTruth[i] = (pTruth[i] & 0xCCCCCCCC) | ((pTruth[i] & 0xCCCCCCCC) >> 2);
00394         return;
00395     case 2:
00396         for ( i = 0; i < nWords; i++ )
00397             pTruth[i] = (pTruth[i] & 0xF0F0F0F0) | ((pTruth[i] & 0xF0F0F0F0) >> 4);
00398         return;
00399     case 3:
00400         for ( i = 0; i < nWords; i++ )
00401             pTruth[i] = (pTruth[i] & 0xFF00FF00) | ((pTruth[i] & 0xFF00FF00) >> 8);
00402         return;
00403     case 4:
00404         for ( i = 0; i < nWords; i++ )
00405             pTruth[i] = (pTruth[i] & 0xFFFF0000) | ((pTruth[i] & 0xFFFF0000) >> 16);
00406         return;
00407     default:
00408         Step = (1 << (iVar - 5));
00409         for ( k = 0; k < nWords; k += 2*Step )
00410         {
00411             for ( i = 0; i < Step; i++ )
00412                 pTruth[i] = pTruth[Step+i];
00413             pTruth += 2*Step;
00414         }
00415         return;
00416     }
00417 }

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 482 of file kitTruth.c.

00483 {
00484     int nWords = Kit_TruthWordNum( nVars );
00485     int i, k, Step;
00486 
00487     assert( iVar < nVars );
00488     switch ( iVar )
00489     {
00490     case 0:
00491         for ( i = 0; i < nWords; i++ )
00492             pOut[i] = (pIn[i] & 0xAAAAAAAA) | ((pIn[i] & 0xAAAAAAAA) >> 1);
00493         return;
00494     case 1:
00495         for ( i = 0; i < nWords; i++ )
00496             pOut[i] = (pIn[i] & 0xCCCCCCCC) | ((pIn[i] & 0xCCCCCCCC) >> 2);
00497         return;
00498     case 2:
00499         for ( i = 0; i < nWords; i++ )
00500             pOut[i] = (pIn[i] & 0xF0F0F0F0) | ((pIn[i] & 0xF0F0F0F0) >> 4);
00501         return;
00502     case 3:
00503         for ( i = 0; i < nWords; i++ )
00504             pOut[i] = (pIn[i] & 0xFF00FF00) | ((pIn[i] & 0xFF00FF00) >> 8);
00505         return;
00506     case 4:
00507         for ( i = 0; i < nWords; i++ )
00508             pOut[i] = (pIn[i] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
00509         return;
00510     default:
00511         Step = (1 << (iVar - 5));
00512         for ( k = 0; k < nWords; k += 2*Step )
00513         {
00514             for ( i = 0; i < Step; i++ )
00515                 pOut[i] = pOut[Step+i] = pIn[Step+i];
00516             pIn += 2*Step;
00517             pOut += 2*Step;
00518         }
00519         return;
00520     }
00521 }

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 304 of file kitCloud.c.

00305 {
00306     Kit_Mux_t Mux;
00307     unsigned * puSuppAll, * pThis, * pFan0, * pFan1;
00308     int i, v, Var, Entry, nSupps;
00309     nSupps = 2 * nVars;
00310 
00311     // extend storage
00312     if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddDir) )
00313         Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddDir) );
00314     puSuppAll = Vec_IntArray( vMemory );
00315     // clear storage for the const node
00316     memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
00317     // compute supports from nodes
00318     Vec_IntForEachEntryStart( vBddDir, Entry, i, 1 )
00319     {
00320         Mux = *((Kit_Mux_t *)&Entry);
00321         Var = nVars - 1 - Mux.v;
00322         pFan0 = puSuppAll + nSupps * Mux.e;
00323         pFan1 = puSuppAll + nSupps * Mux.t;
00324         pThis = puSuppAll + nSupps * i;
00325         for ( v = 0; v < nSupps; v++ )
00326             pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
00327         assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
00328         assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
00329         pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
00330         pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
00331     }
00332     // copy the result
00333     memcpy( puSupps, pThis, sizeof(unsigned) * nSupps );
00334     // compute the inverse
00335 
00336     // extend storage
00337     if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddInv) )
00338         Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddInv) );
00339     puSuppAll = Vec_IntArray( vMemory );
00340     // clear storage for the const node
00341     memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
00342     // compute supports from nodes
00343     Vec_IntForEachEntryStart( vBddInv, Entry, i, 1 )
00344     {
00345         Mux = *((Kit_Mux_t *)&Entry);
00346 //        Var = nVars - 1 - Mux.v;
00347         Var = Mux.v;
00348         pFan0 = puSuppAll + nSupps * Mux.e;
00349         pFan1 = puSuppAll + nSupps * Mux.t;
00350         pThis = puSuppAll + nSupps * i;
00351         for ( v = 0; v < nSupps; v++ )
00352             pThis[v] = pFan0[v] | pFan1[v] | (1<<Var);
00353         assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
00354         assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
00355         pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
00356         pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
00357     }
00358 
00359     // merge supports
00360     for ( Var = 0; Var < nSupps; Var++ )
00361         puSupps[Var] = (puSupps[Var] & Kit_BitMask(Var/2)) | (pThis[Var] & ~Kit_BitMask(Var/2));
00362 }

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 257 of file kitCloud.c.

00259 {
00260     CloudNode * pFunc;
00261     unsigned * pThis, * pFan0, * pFan1;
00262     Kit_Mux_t Mux;
00263     int i, Entry, RetValue;
00264     // derive BDD from truth table
00265     Cloud_Restart( dd );
00266     pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
00267     // convert it into nodes
00268     RetValue = Kit_CreateCloud( dd, pFunc, vNodes );
00269     if ( RetValue == 0 )
00270         printf( "Kit_TruthCompose(): Internal failure!!!\n" );
00271     // verify the result
00272 //    pFan0 = Kit_CloudToTruth( vNodes, nVars, vStore, 0 );
00273 //    if ( !Kit_TruthIsEqual( pTruth, pFan0, nVars ) )
00274 //        printf( "Failed!\n" );
00275     // compute truth table from the BDD
00276     assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
00277     pThis = Vec_PtrEntry( vStore, 0 );
00278     Kit_TruthFill( pThis, nVarsAll );
00279     Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
00280     {
00281         Mux = *((Kit_Mux_t *)&Entry);
00282         pFan0 = Vec_PtrEntry( vStore, Mux.e );
00283         pFan1 = Vec_PtrEntry( vStore, Mux.t );
00284         pThis = Vec_PtrEntry( vStore, i );
00285         Kit_TruthMuxPhase( pThis, pFan0, pFan1, pInputs[nVars-1-Mux.v], nVarsAll, Mux.c );
00286     }
00287     // complement the result
00288     if ( Mux.i )
00289         Kit_TruthNot( pThis, pThis, nVarsAll );
00290     return pThis;
00291 }

static void Kit_TruthCopy	(	unsigned *	pOut,
		unsigned *	pIn,
		int	nVars
	)			`[inline, static]`

Definition at line 355 of file kit.h.

00356 {
00357     int w;
00358     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00359         pOut[w] = pIn[w];
00360 }

static int Kit_TruthCountOnes	(	unsigned *	pIn,
		int	nVars
	)			`[inline, static]`

Definition at line 259 of file kit.h.

00260 {
00261     int w, Counter = 0;
00262     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00263         Counter += Kit_WordCountOnes(pIn[w]);
00264     return Counter;
00265 }

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

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

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

Description [The resulting numbers are stored in the array of shorts, 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 1172 of file kitTruth.c.

01173 {
01174     int nWords = Kit_TruthWordNum( nVars );
01175     int i, k, Counter;
01176     memset( pStore, 0, sizeof(short) * 2 * nVars );
01177     if ( nVars <= 5 )
01178     {
01179         if ( nVars > 0 )
01180         {
01181             pStore[2*0+0] = Kit_WordCountOnes( pTruth[0] & 0x55555555 );
01182             pStore[2*0+1] = Kit_WordCountOnes( pTruth[0] & 0xAAAAAAAA );
01183         }
01184         if ( nVars > 1 )
01185         {
01186             pStore[2*1+0] = Kit_WordCountOnes( pTruth[0] & 0x33333333 );
01187             pStore[2*1+1] = Kit_WordCountOnes( pTruth[0] & 0xCCCCCCCC );
01188         }
01189         if ( nVars > 2 )
01190         {
01191             pStore[2*2+0] = Kit_WordCountOnes( pTruth[0] & 0x0F0F0F0F );
01192             pStore[2*2+1] = Kit_WordCountOnes( pTruth[0] & 0xF0F0F0F0 );
01193         }
01194         if ( nVars > 3 )
01195         {
01196             pStore[2*3+0] = Kit_WordCountOnes( pTruth[0] & 0x00FF00FF );
01197             pStore[2*3+1] = Kit_WordCountOnes( pTruth[0] & 0xFF00FF00 );
01198         }
01199         if ( nVars > 4 )
01200         {
01201             pStore[2*4+0] = Kit_WordCountOnes( pTruth[0] & 0x0000FFFF );
01202             pStore[2*4+1] = Kit_WordCountOnes( pTruth[0] & 0xFFFF0000 );
01203         }
01204         return;
01205     }
01206     // nVars >= 6
01207     // count 1's for all other variables
01208     for ( k = 0; k < nWords; k++ )
01209     {
01210         Counter = Kit_WordCountOnes( pTruth[k] );
01211         for ( i = 5; i < nVars; i++ )
01212             if ( k & (1 << (i-5)) )
01213                 pStore[2*i+1] += Counter;
01214             else
01215                 pStore[2*i+0] += Counter;
01216     }
01217     // count 1's for the first five variables
01218     for ( k = 0; k < nWords/2; k++ )
01219     {
01220         pStore[2*0+0] += Kit_WordCountOnes( (pTruth[0] & 0x55555555) | ((pTruth[1] & 0x55555555) <<  1) );
01221         pStore[2*0+1] += Kit_WordCountOnes( (pTruth[0] & 0xAAAAAAAA) | ((pTruth[1] & 0xAAAAAAAA) >>  1) );
01222         pStore[2*1+0] += Kit_WordCountOnes( (pTruth[0] & 0x33333333) | ((pTruth[1] & 0x33333333) <<  2) );
01223         pStore[2*1+1] += Kit_WordCountOnes( (pTruth[0] & 0xCCCCCCCC) | ((pTruth[1] & 0xCCCCCCCC) >>  2) );
01224         pStore[2*2+0] += Kit_WordCountOnes( (pTruth[0] & 0x0F0F0F0F) | ((pTruth[1] & 0x0F0F0F0F) <<  4) );
01225         pStore[2*2+1] += Kit_WordCountOnes( (pTruth[0] & 0xF0F0F0F0) | ((pTruth[1] & 0xF0F0F0F0) >>  4) );
01226         pStore[2*3+0] += Kit_WordCountOnes( (pTruth[0] & 0x00FF00FF) | ((pTruth[1] & 0x00FF00FF) <<  8) );
01227         pStore[2*3+1] += Kit_WordCountOnes( (pTruth[0] & 0xFF00FF00) | ((pTruth[1] & 0xFF00FF00) >>  8) );
01228         pStore[2*4+0] += Kit_WordCountOnes( (pTruth[0] & 0x0000FFFF) | ((pTruth[1] & 0x0000FFFF) << 16) );
01229         pStore[2*4+1] += Kit_WordCountOnes( (pTruth[0] & 0xFFFF0000) | ((pTruth[1] & 0xFFFF0000) >> 16) );
01230         pTruth += 2;
01231     }
01232 }

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

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

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

Description [Verifies the above procedure.]

SideEffects []

SeeAlso []

Definition at line 1245 of file kitTruth.c.

01246 {
01247     int i;
01248     for ( i = 0; i < nVars; i++ )
01249     {
01250         Kit_TruthCofactor0New( pAux, pTruth, nVars, i );
01251         pStore[2*i+0] = Kit_TruthCountOnes( pAux, nVars ) / 2;
01252         Kit_TruthCofactor1New( pAux, pTruth, nVars, i );
01253         pStore[2*i+1] = Kit_TruthCountOnes( pAux, nVars ) / 2;
01254     }
01255 }

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 1703 of file kitTruth.c.

01704 {
01705     static char pFileName[100];
01706     FILE * pFile;
01707     sprintf( pFileName, "tt\\s%04d", nFile );
01708     pFile = fopen( pFileName, "w" );
01709     fprintf( pFile, "rt " );
01710     Kit_PrintHexadecimal( pFile, pTruth, nVars );
01711     fprintf( pFile, "; bdd; sop; ps\n" );
01712     fclose( pFile );
01713     return pFileName;
01714 }

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

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

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 535 of file kitTruth.c.

00536 {
00537     int nWords = Kit_TruthWordNum( nVars );
00538     int i, k, Step;
00539 
00540     assert( iVar < nVars );
00541     switch ( iVar )
00542     {
00543     case 0:
00544         for ( i = 0; i < nWords; i++ )
00545             pTruth[i] |=  ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
00546         return;
00547     case 1:
00548         for ( i = 0; i < nWords; i++ )
00549             pTruth[i] |=  ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
00550         return;
00551     case 2:
00552         for ( i = 0; i < nWords; i++ )
00553             pTruth[i] |=  ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
00554         return;
00555     case 3:
00556         for ( i = 0; i < nWords; i++ )
00557             pTruth[i] |=  ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
00558         return;
00559     case 4:
00560         for ( i = 0; i < nWords; i++ )
00561             pTruth[i] |=  ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
00562         return;
00563     default:
00564         Step = (1 << (iVar - 5));
00565         for ( k = 0; k < nWords; k += 2*Step )
00566         {
00567             for ( i = 0; i < Step; i++ )
00568             {
00569                 pTruth[i]     |= pTruth[Step+i];
00570                 pTruth[Step+i] = pTruth[i];
00571             }
00572             pTruth += 2*Step;
00573         }
00574         return;
00575     }
00576 }

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

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

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 589 of file kitTruth.c.

00590 {
00591     int nWords = Kit_TruthWordNum( nVars );
00592     int i, k, Step;
00593 
00594     assert( iVar < nVars );
00595     switch ( iVar )
00596     {
00597     case 0:
00598         for ( i = 0; i < nWords; i++ )
00599             pRes[i] =  pTruth[i] | ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
00600         return;
00601     case 1:
00602         for ( i = 0; i < nWords; i++ )
00603             pRes[i] =  pTruth[i] | ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
00604         return;
00605     case 2:
00606         for ( i = 0; i < nWords; i++ )
00607             pRes[i] =  pTruth[i] | ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
00608         return;
00609     case 3:
00610         for ( i = 0; i < nWords; i++ )
00611             pRes[i] =  pTruth[i] | ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
00612         return;
00613     case 4:
00614         for ( i = 0; i < nWords; i++ )
00615             pRes[i] =  pTruth[i] | ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
00616         return;
00617     default:
00618         Step = (1 << (iVar - 5));
00619         for ( k = 0; k < nWords; k += 2*Step )
00620         {
00621             for ( i = 0; i < Step; i++ )
00622             {
00623                 pRes[i]      = pTruth[i] | pTruth[Step+i];
00624                 pRes[Step+i] = pRes[i];
00625             }
00626             pRes += 2*Step;
00627             pTruth += 2*Step;
00628         }
00629         return;
00630     }
00631 }

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 644 of file kitTruth.c.

00645 {
00646     int v;
00647     Kit_TruthCopy( pRes, pTruth, nVars );
00648     for ( v = 0; v < nVars; v++ )
00649         if ( uMask & (1 << v) )
00650             Kit_TruthExist( pRes, nVars, v );
00651 }

static void Kit_TruthFill	(	unsigned *	pOut,
		int	nVars
	)			`[inline, static]`

Definition at line 367 of file kit.h.

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

static int Kit_TruthFindFirstBit	(	unsigned *	pIn,
		int	nVars
	)			`[inline, static]`

Definition at line 266 of file kit.h.

00267 {
00268     int w;
00269     for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
00270         if ( pIn[w] )
00271             return 32*w + Kit_WordFindFirstBit(pIn[w]);
00272     return -1;
00273 }

static int Kit_TruthFindFirstZero	(	unsigned *	pIn,
		int	nVars
	)			`[inline, static]`

Definition at line 274 of file kit.h.

00275 {
00276     int w;
00277     for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
00278         if ( ~pIn[w] )
00279             return 32*w + Kit_WordFindFirstBit(~pIn[w]);
00280     return -1;
00281 }

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

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

Synopsis [Unversally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 664 of file kitTruth.c.

00665 {
00666     int nWords = Kit_TruthWordNum( nVars );
00667     int i, k, Step;
00668 
00669     assert( iVar < nVars );
00670     switch ( iVar )
00671     {
00672     case 0:
00673         for ( i = 0; i < nWords; i++ )
00674             pTruth[i] &=  ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
00675         return;
00676     case 1:
00677         for ( i = 0; i < nWords; i++ )
00678             pTruth[i] &=  ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
00679         return;
00680     case 2:
00681         for ( i = 0; i < nWords; i++ )
00682             pTruth[i] &=  ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
00683         return;
00684     case 3:
00685         for ( i = 0; i < nWords; i++ )
00686             pTruth[i] &=  ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
00687         return;
00688     case 4:
00689         for ( i = 0; i < nWords; i++ )
00690             pTruth[i] &=  ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
00691         return;
00692     default:
00693         Step = (1 << (iVar - 5));
00694         for ( k = 0; k < nWords; k += 2*Step )
00695         {
00696             for ( i = 0; i < Step; i++ )
00697             {
00698                 pTruth[i]     &= pTruth[Step+i];
00699                 pTruth[Step+i] = pTruth[i];
00700             }
00701             pTruth += 2*Step;
00702         }
00703         return;
00704     }
00705 }

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

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

Synopsis [Universally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 718 of file kitTruth.c.

00719 {
00720     int nWords = Kit_TruthWordNum( nVars );
00721     int i, k, Step;
00722 
00723     assert( iVar < nVars );
00724     switch ( iVar )
00725     {
00726     case 0:
00727         for ( i = 0; i < nWords; i++ )
00728             pRes[i] =  pTruth[i] & (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
00729         return;
00730     case 1:
00731         for ( i = 0; i < nWords; i++ )
00732             pRes[i] =  pTruth[i] & (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
00733         return;
00734     case 2:
00735         for ( i = 0; i < nWords; i++ )
00736             pRes[i] =  pTruth[i] & (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
00737         return;
00738     case 3:
00739         for ( i = 0; i < nWords; i++ )
00740             pRes[i] =  pTruth[i] & (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
00741         return;
00742     case 4:
00743         for ( i = 0; i < nWords; i++ )
00744             pRes[i] =  pTruth[i] & (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
00745         return;
00746     default:
00747         Step = (1 << (iVar - 5));
00748         for ( k = 0; k < nWords; k += 2*Step )
00749         {
00750             for ( i = 0; i < Step; i++ )
00751             {
00752                 pRes[i]      = pTruth[i] & pTruth[Step+i];
00753                 pRes[Step+i] = pRes[i];
00754             }
00755             pRes += 2*Step;
00756             pTruth += 2*Step;
00757         }
00758         return;
00759     }
00760 }

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 828 of file kitTruth.c.

00829 {
00830     int v;
00831     Kit_TruthCopy( pRes, pTruth, nVars );
00832     for ( v = 0; v < nVars; v++ )
00833         if ( uMask & (1 << v) )
00834             Kit_TruthForall( pRes, nVars, v );
00835 }

static int Kit_TruthHasBit	(	unsigned *	p,
		int	Bit
	)			`[inline, static]`

Definition at line 237 of file kit.h.

00237 { 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 1268 of file kitTruth.c.

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

static int Kit_TruthIsConst0	(	unsigned *	pIn,
		int	nVars
	)			`[inline, static]`

Definition at line 315 of file kit.h.

00316 {
00317     int w;
00318     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00319         if ( pIn[w] )
00320             return 0;
00321     return 1;
00322 }

static int Kit_TruthIsConst1	(	unsigned *	pIn,
		int	nVars
	)			`[inline, static]`

Definition at line 323 of file kit.h.

00324 {
00325     int w;
00326     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00327         if ( pIn[w] != ~(unsigned)0 )
00328             return 0;
00329     return 1;
00330 }

static int Kit_TruthIsDisjoint	(	unsigned *	pIn1,
		unsigned *	pIn2,
		int	nVars
	)			`[inline, static]`

Definition at line 339 of file kit.h.

00340 {
00341     int w;
00342     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00343         if ( pIn1[w] & pIn2[w] )
00344             return 0;
00345     return 1;
00346 }

static int Kit_TruthIsDisjoint3	(	unsigned *	pIn1,
		unsigned *	pIn2,
		unsigned *	pIn3,
		int	nVars
	)			`[inline, static]`

Definition at line 347 of file kit.h.

00348 {
00349     int w;
00350     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00351         if ( pIn1[w] & pIn2[w] & pIn3[w] )
00352             return 0;
00353     return 1;
00354 }

static int Kit_TruthIsEqual	(	unsigned *	pIn0,
		unsigned *	pIn1,
		int	nVars
	)			`[inline, static]`

Definition at line 282 of file kit.h.

00283 {
00284     int w;
00285     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00286         if ( pIn0[w] != pIn1[w] )
00287             return 0;
00288     return 1;
00289 }

static int Kit_TruthIsEqualWithPhase	(	unsigned *	pIn0,
		unsigned *	pIn1,
		int	nVars
	)			`[inline, static]`

Definition at line 298 of file kit.h.

00299 {
00300     int w;
00301     if ( (pIn0[0] & 1) == (pIn1[0] & 1) )
00302     {
00303         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00304             if ( pIn0[w] != pIn1[w] )
00305                 return 0;
00306     }
00307     else
00308     {
00309         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00310             if ( pIn0[w] != ~pIn1[w] )
00311                 return 0;
00312     }
00313     return 1;
00314 }

static int Kit_TruthIsImply	(	unsigned *	pIn1,
		unsigned *	pIn2,
		int	nVars
	)			`[inline, static]`

Definition at line 331 of file kit.h.

00332 {
00333     int w;
00334     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00335         if ( pIn1[w] & ~pIn2[w] )
00336             return 0;
00337     return 1;
00338 }

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 52 of file kitIsop.c.

00053 {
00054     Kit_Sop_t cRes, * pcRes = &cRes;
00055     Kit_Sop_t cRes2, * pcRes2 = &cRes2;
00056     unsigned * pResult;
00057     int RetValue = 0;
00058     assert( nVars >= 0 && nVars < 16 );
00059     // if nVars < 5, make sure it does not depend on those vars
00060 //    for ( i = nVars; i < 5; i++ )
00061 //        assert( !Kit_TruthVarInSupport(puTruth, 5, i) );
00062     // prepare memory manager
00063     Vec_IntClear( vMemory );
00064     Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT );
00065     // compute ISOP for the direct polarity
00066     pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vMemory );
00067     if ( pcRes->nCubes == -1 )
00068     {
00069         vMemory->nSize = -1;
00070         return -1;
00071     }
00072     assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
00073     if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) )
00074     {
00075         vMemory->pArray[0] = 0;
00076         Vec_IntShrink( vMemory, pcRes->nCubes );
00077         return 0;
00078     }
00079     if ( fTryBoth )
00080     {
00081         // compute ISOP for the complemented polarity
00082         Kit_TruthNot( puTruth, puTruth, nVars );
00083         pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vMemory );
00084         if ( pcRes2->nCubes >= 0 )
00085         {
00086             assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
00087             if ( pcRes->nCubes > pcRes2->nCubes )
00088             {
00089                 RetValue = 1;
00090                 pcRes = pcRes2;
00091             }
00092         }
00093         Kit_TruthNot( puTruth, puTruth, nVars );
00094     }
00095 //    printf( "%d ", vMemory->nSize );
00096     // move the cover representation to the beginning of the memory buffer
00097     memmove( vMemory->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
00098     Vec_IntShrink( vMemory, pcRes->nCubes );
00099     return RetValue;
00100 }

static int Kit_TruthIsOpposite	(	unsigned *	pIn0,
		unsigned *	pIn1,
		int	nVars
	)			`[inline, static]`

Definition at line 290 of file kit.h.

00291 {
00292     int w;
00293     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00294         if ( pIn0[w] != ~pIn1[w] )
00295             return 0;
00296     return 1;
00297 }

static void Kit_TruthIthVar	(	unsigned *	pTruth,
		int	nVars,
		int	iVar
	)			`[inline, static]`

Definition at line 449 of file kit.h.

00450 {
00451     unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
00452     int k, nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
00453     if ( iVar < 5 )
00454     {
00455         for ( k = 0; k < nWords; k++ )
00456             pTruth[k] = Masks[iVar];
00457     }
00458     else
00459     {
00460         for ( k = 0; k < nWords; k++ )
00461             if ( k & (1 << (iVar-5)) )
00462                 pTruth[k] = ~(unsigned)0;
00463             else
00464                 pTruth[k] = 0;
00465     }
00466 }

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

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

Synopsis [Computes minimum overlap in supports of cofactors.]

Description []

SideEffects []

SeeAlso []

Definition at line 1077 of file kitTruth.c.

01078 {
01079     static unsigned uCofactor[16];
01080     int i, ValueCur, ValueMin, VarMin;
01081     unsigned uSupp0, uSupp1;
01082     int nVars0, nVars1;
01083     assert( nVars <= 9 );
01084     ValueMin = 32;
01085     VarMin   = -1;
01086     for ( i = 0; i < nVars; i++ )
01087     {
01088         // get negative cofactor
01089         Kit_TruthCopy( uCofactor, pTruth, nVars );
01090         Kit_TruthCofactor0( uCofactor, nVars, i );
01091         uSupp0 = Kit_TruthSupport( uCofactor, nVars );
01092         nVars0 = Kit_WordCountOnes( uSupp0 );
01093 //Kit_PrintBinary( stdout, &uSupp0, 8 ); printf( "\n" );
01094         // get positive cofactor
01095         Kit_TruthCopy( uCofactor, pTruth, nVars );
01096         Kit_TruthCofactor1( uCofactor, nVars, i );
01097         uSupp1 = Kit_TruthSupport( uCofactor, nVars );
01098         nVars1 = Kit_WordCountOnes( uSupp1 );
01099 //Kit_PrintBinary( stdout, &uSupp1, 8 ); printf( "\n" );
01100         // get the number of common vars
01101         ValueCur = Kit_WordCountOnes( uSupp0 & uSupp1 );
01102         if ( ValueMin > ValueCur && nVars0 <= 5 && nVars1 <= 5 )
01103         {
01104             ValueMin = ValueCur;
01105             VarMin = i;
01106         }
01107         if ( ValueMin == 0 )
01108             break;
01109     }
01110     if ( pVarMin )
01111         *pVarMin = VarMin;
01112     return ValueMin;
01113 }

static void Kit_TruthMux	(	unsigned *	pOut,
		unsigned *	pIn0,
		unsigned *	pIn1,
		unsigned *	pCtrl,
		int	nVars
	)			`[inline, static]`

Definition at line 433 of file kit.h.

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

static void Kit_TruthMuxPhase	(	unsigned *	pOut,
		unsigned *	pIn0,
		unsigned *	pIn1,
		unsigned *	pCtrl,
		int	nVars,
		int	fComp0
	)			`[inline, static]`

Definition at line 439 of file kit.h.

00440 {
00441     int w;
00442     if ( fComp0 )
00443         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00444             pOut[w] = (~pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
00445     else
00446         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00447             pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
00448 }

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 849 of file kitTruth.c.

00850 {
00851     int nWords = Kit_TruthWordNum( nVars );
00852     int i, k, Step;
00853 
00854     assert( iVar < nVars );
00855     switch ( iVar )
00856     {
00857     case 0:
00858         for ( i = 0; i < nWords; i++ )
00859             pOut[i] = (pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
00860         return;
00861     case 1:
00862         for ( i = 0; i < nWords; i++ )
00863             pOut[i] = (pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
00864         return;
00865     case 2:
00866         for ( i = 0; i < nWords; i++ )
00867             pOut[i] = (pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
00868         return;
00869     case 3:
00870         for ( i = 0; i < nWords; i++ )
00871             pOut[i] = (pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
00872         return;
00873     case 4:
00874         for ( i = 0; i < nWords; i++ )
00875             pOut[i] = (pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
00876         return;
00877     default:
00878         Step = (1 << (iVar - 5));
00879         for ( k = 0; k < nWords; k += 2*Step )
00880         {
00881             for ( i = 0; i < Step; i++ )
00882             {
00883                 pOut[i]      = pCof0[i];
00884                 pOut[Step+i] = pCof1[Step+i];
00885             }
00886             pOut += 2*Step;
00887             pCof0 += 2*Step;
00888             pCof1 += 2*Step;
00889         }
00890         return;
00891     }
00892 }

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 905 of file kitTruth.c.

00906 {
00907     int nWords = Kit_TruthWordNum( nVars );
00908     int i, k, Step;
00909 
00910     if ( fCompl0 == 0 )
00911     {
00912         Kit_TruthMuxVar( pOut, pCof0, pCof1, nVars, iVar );
00913         return;
00914     }
00915 
00916     assert( iVar < nVars );
00917     switch ( iVar )
00918     {
00919     case 0:
00920         for ( i = 0; i < nWords; i++ )
00921             pOut[i] = (~pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA);
00922         return;
00923     case 1:
00924         for ( i = 0; i < nWords; i++ )
00925             pOut[i] = (~pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC);
00926         return;
00927     case 2:
00928         for ( i = 0; i < nWords; i++ )
00929             pOut[i] = (~pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0);
00930         return;
00931     case 3:
00932         for ( i = 0; i < nWords; i++ )
00933             pOut[i] = (~pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00);
00934         return;
00935     case 4:
00936         for ( i = 0; i < nWords; i++ )
00937             pOut[i] = (~pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000);
00938         return;
00939     default:
00940         Step = (1 << (iVar - 5));
00941         for ( k = 0; k < nWords; k += 2*Step )
00942         {
00943             for ( i = 0; i < Step; i++ )
00944             {
00945                 pOut[i]      = ~pCof0[i];
00946                 pOut[Step+i] = pCof1[Step+i];
00947             }
00948             pOut += 2*Step;
00949             pCof0 += 2*Step;
00950             pCof1 += 2*Step;
00951         }
00952         return;
00953     }
00954 }

static void Kit_TruthNand	(	unsigned *	pOut,
		unsigned *	pIn0,
		unsigned *	pIn1,
		int	nVars
	)			`[inline, static]`

Definition at line 403 of file kit.h.

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

static void Kit_TruthNot	(	unsigned *	pOut,
		unsigned *	pIn,
		int	nVars
	)			`[inline, static]`

Definition at line 373 of file kit.h.

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

static void Kit_TruthOr	(	unsigned *	pOut,
		unsigned *	pIn0,
		unsigned *	pIn1,
		int	nVars
	)			`[inline, static]`

Definition at line 385 of file kit.h.

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

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

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

Synopsis [Canonicize the truth table.]

Description [Returns the phase. ]

SideEffects []

SeeAlso []

Definition at line 1365 of file kitTruth.c.

01366 {
01367 //    short pStore2[32];
01368     unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
01369 //    int nWords = Kit_TruthWordNum( nVars );
01370     int i, Temp, fChange, Counter;//, nOnes;//, k, j, w, Limit;
01371     unsigned uCanonPhase;
01372 
01373     // canonicize output
01374     uCanonPhase = 0;
01375 /*
01376     nOnes = Kit_TruthCountOnes(pIn, nVars);
01377     if ( (nOnes > nWords * 16) )//|| ((nOnes == nWords * 16) && (pIn[0] & 1)) )
01378     {
01379         uCanonPhase |= (1 << nVars);
01380         Kit_TruthNot( pIn, pIn, nVars );
01381     }
01382 */
01383     // collect the minterm counts
01384     Kit_TruthCountOnesInCofs( pIn, nVars, pStore );
01385 //    Kit_TruthCountOnesInCofsSlow( pIn, nVars, pStore2, pAux );
01386 //    for ( i = 0; i < 2*nVars; i++ )
01387 //    {
01388 //        assert( pStore[i] == pStore2[i] );
01389 //    }
01390 
01391     // canonicize phase
01392     for ( i = 0; i < nVars; i++ )
01393     {
01394         if ( pStore[2*i+0] >= pStore[2*i+1] )
01395             continue;
01396         uCanonPhase |= (1 << i);
01397         Temp = pStore[2*i+0];
01398         pStore[2*i+0] = pStore[2*i+1];
01399         pStore[2*i+1] = Temp;
01400         Kit_TruthChangePhase( pIn, nVars, i );
01401     }
01402 
01403 //    Kit_PrintHexadecimal( stdout, pIn, nVars );
01404 //    printf( "\n" );
01405 
01406     // permute
01407     Counter = 0;
01408     do {
01409         fChange = 0;
01410         for ( i = 0; i < nVars-1; i++ )
01411         {
01412             if ( pStore[2*i] >= pStore[2*(i+1)] )
01413                 continue;
01414             Counter++;
01415             fChange = 1;
01416 
01417             Temp = pCanonPerm[i];
01418             pCanonPerm[i] = pCanonPerm[i+1];
01419             pCanonPerm[i+1] = Temp;
01420 
01421             Temp = pStore[2*i];
01422             pStore[2*i] = pStore[2*(i+1)];
01423             pStore[2*(i+1)] = Temp;
01424 
01425             Temp = pStore[2*i+1];
01426             pStore[2*i+1] = pStore[2*(i+1)+1];
01427             pStore[2*(i+1)+1] = Temp;
01428 
01429             // if the polarity of variables is different, swap them
01430             if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
01431             {
01432                 uCanonPhase ^= (1 << i);
01433                 uCanonPhase ^= (1 << (i+1));
01434             }
01435 
01436             Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
01437             pTemp = pIn; pIn = pOut; pOut = pTemp;
01438         }
01439     } while ( fChange );
01440 
01441 /*
01442     Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
01443     for ( i = 0; i < nVars; i++ )
01444         printf( "%d=%d/%d  ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] );
01445     printf( "  C = %d\n", Counter );
01446     Extra_PrintHexadecimal( stdout, pIn, nVars );
01447     printf( "\n" );
01448 */
01449 
01450 /*
01451     // process symmetric variable groups
01452     uSymms = 0;
01453     for ( i = 0; i < nVars-1; i++ )
01454     {
01455         if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
01456             continue;
01457         if ( pStore[2*i] != pStore[2*i+1] )
01458             continue;
01459         if ( Kit_TruthVarsSymm( pIn, nVars, i, i+1 ) )
01460             continue;
01461         if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, i+1 ) )
01462             Kit_TruthChangePhase( pIn, nVars, i+1 );
01463     }
01464 */
01465 
01466 /*
01467     // process symmetric variable groups
01468     uSymms = 0;
01469     for ( i = 0; i < nVars-1; i++ )
01470     {
01471         if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
01472             continue;
01473         // i and i+1 can be symmetric
01474         // find the end of this group
01475         for ( k = i+1; k < nVars; k++ )
01476             if ( pStore[2*i] != pStore[2*k] ) 
01477                 break;
01478         Limit = k;
01479         assert( i < Limit-1 );
01480         // go through the variables in this group
01481         for ( j = i + 1; j < Limit; j++ )
01482         {
01483             // check symmetry
01484             if ( Kit_TruthVarsSymm( pIn, nVars, i, j ) )
01485             {
01486                 uSymms |= (1 << j);
01487                 continue;
01488             }
01489             // they are phase-unknown
01490             if ( pStore[2*i] == pStore[2*i+1] ) 
01491             {
01492                 if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, j ) )
01493                 {
01494                     Kit_TruthChangePhase( pIn, nVars, j );
01495                     uCanonPhase ^= (1 << j);
01496                     uSymms |= (1 << j);
01497                     continue;
01498                 }
01499             }
01500 
01501             // they are not symmetric - move j as far as it goes in the group
01502             for ( k = j; k < Limit-1; k++ )
01503             {
01504                 Counter++;
01505 
01506                 Temp = pCanonPerm[k];
01507                 pCanonPerm[k] = pCanonPerm[k+1];
01508                 pCanonPerm[k+1] = Temp;
01509 
01510                 assert( pStore[2*k] == pStore[2*(k+1)] );
01511                 Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, k );
01512                 pTemp = pIn; pIn = pOut; pOut = pTemp;
01513             }
01514             Limit--;
01515             j--;
01516         }
01517         i = Limit - 1;
01518     }
01519 */
01520 
01521     // swap if it was moved an even number of times
01522     if ( Counter & 1 )
01523         Kit_TruthCopy( pOut, pIn, nVars );
01524     return uCanonPhase;
01525 }

static void Kit_TruthSetBit	(	unsigned *	p,
		int	Bit
	)			`[inline, static]`

Definition at line 235 of file kit.h.

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

static void Kit_TruthSharp	(	unsigned *	pOut,
		unsigned *	pIn0,
		unsigned *	pIn1,
		int	nVars
	)			`[inline, static]`

Definition at line 397 of file kit.h.

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

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) contains shows what variables should remain.]

SideEffects []

SeeAlso []

Definition at line 197 of file kitTruth.c.

00198 {
00199     unsigned * pTemp;
00200     int i, k, Var = 0, Counter = 0;
00201     for ( i = 0; i < nVarsAll; i++ )
00202         if ( Phase & (1 << i) )
00203         {
00204             for ( k = i-1; k >= Var; k-- )
00205             {
00206                 Kit_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
00207                 pTemp = pIn; pIn = pOut; pOut = pTemp;
00208                 Counter++;
00209             }
00210             Var++;
00211         }
00212     assert( Var == nVars );
00213     // swap if it was moved an even number of times
00214     if ( fReturnIn ^ !(Counter & 1) )
00215         Kit_TruthCopy( pOut, pIn, nVarsAll );
00216 }

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 []

SeeAlso []

Definition at line 163 of file kitTruth.c.

00164 {
00165     unsigned * pTemp;
00166     int i, k, Var = nVars - 1, Counter = 0;
00167     for ( i = nVarsAll - 1; i >= 0; i-- )
00168         if ( Phase & (1 << i) )
00169         {
00170             for ( k = Var; k < i; k++ )
00171             {
00172                 Kit_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
00173                 pTemp = pIn; pIn = pOut; pOut = pTemp;
00174                 Counter++;
00175             }
00176             Var--;
00177         }
00178     assert( Var == -1 );
00179     // swap if it was moved an even number of times
00180     if ( fReturnIn ^ !(Counter & 1) )
00181         Kit_TruthCopy( pOut, pIn, nVarsAll );
00182 }

unsigned Kit_TruthSupport	(	unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Returns support of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 306 of file kitTruth.c.

00307 {
00308     int i, Support = 0;
00309     for ( i = 0; i < nVars; i++ )
00310         if ( Kit_TruthVarInSupport( pTruth, nVars, i ) )
00311             Support |= (1 << i);
00312     return Support;
00313 }

int Kit_TruthSupportSize	(	unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Returns the number of support vars.]

Description []

SideEffects []

SeeAlso []

Definition at line 287 of file kitTruth.c.

00288 {
00289     int i, Counter = 0;
00290     for ( i = 0; i < nVars; i++ )
00291         Counter += Kit_TruthVarInSupport( pTruth, nVars, i );
00292     return Counter;
00293 }

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

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

] DECLARATIONS /// 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 43 of file kitTruth.c.

00044 {
00045     static unsigned PMasks[4][3] = {
00046         { 0x99999999, 0x22222222, 0x44444444 },
00047         { 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 },
00048         { 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
00049         { 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
00050     };
00051     int nWords = Kit_TruthWordNum( nVars );
00052     int i, k, Step, Shift;
00053 
00054     assert( iVar < nVars - 1 );
00055     if ( iVar < 4 )
00056     {
00057         Shift = (1 << iVar);
00058         for ( i = 0; i < nWords; i++ )
00059             pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
00060     }
00061     else if ( iVar > 4 )
00062     {
00063         Step = (1 << (iVar - 5));
00064         for ( k = 0; k < nWords; k += 4*Step )
00065         {
00066             for ( i = 0; i < Step; i++ )
00067                 pOut[i] = pIn[i];
00068             for ( i = 0; i < Step; i++ )
00069                 pOut[Step+i] = pIn[2*Step+i];
00070             for ( i = 0; i < Step; i++ )
00071                 pOut[2*Step+i] = pIn[Step+i];
00072             for ( i = 0; i < Step; i++ )
00073                 pOut[3*Step+i] = pIn[3*Step+i];
00074             pIn  += 4*Step;
00075             pOut += 4*Step;
00076         }
00077     }
00078     else // if ( iVar == 4 )
00079     {
00080         for ( i = 0; i < nWords; i += 2 )
00081         {
00082             pOut[i]   = (pIn[i]   & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
00083             pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i]   & 0xFFFF0000) >> 16);
00084         }
00085     }
00086 }

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 179 of file kitBdd.c.

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

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

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

Synopsis [Compute BDD for the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 142 of file kitCloud.c.

00143 {
00144     CloudNode * pRes;
00145     pRes = Kit_TruthToCloud_rec( dd, pTruth, nVars, nVars );
00146 //    printf( "%d/%d  ", Count, Cloud_DagSize(dd, pRes) );
00147     return pRes;
00148 }

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 352 of file kitGraph.c.

00353 {
00354     Kit_Graph_t * pGraph;
00355     int RetValue;
00356     // derive SOP
00357     RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 1 ); // tried 1 and found not useful in "renode"
00358     if ( RetValue == -1 )
00359         return NULL;
00360     if ( Vec_IntSize(vMemory) > 128 )
00361         return NULL;
00362 //    printf( "Isop size = %d.\n", Vec_IntSize(vMemory) );
00363     assert( RetValue == 0 || RetValue == 1 );
00364     // derive factored form
00365     pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory );
00366     return pGraph;
00367 }

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

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

Synopsis [Universally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 773 of file kitTruth.c.

00774 {
00775     int nWords = Kit_TruthWordNum( nVars );
00776     int i, k, Step;
00777 
00778     assert( iVar < nVars );
00779     switch ( iVar )
00780     {
00781     case 0:
00782         for ( i = 0; i < nWords; i++ )
00783             pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
00784         return;
00785     case 1:
00786         for ( i = 0; i < nWords; i++ )
00787             pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
00788         return;
00789     case 2:
00790         for ( i = 0; i < nWords; i++ )
00791             pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
00792         return;
00793     case 3:
00794         for ( i = 0; i < nWords; i++ )
00795             pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
00796         return;
00797     case 4:
00798         for ( i = 0; i < nWords; i++ )
00799             pRes[i] =  pTruth[i] ^ (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
00800         return;
00801     default:
00802         Step = (1 << (iVar - 5));
00803         for ( k = 0; k < nWords; k += 2*Step )
00804         {
00805             for ( i = 0; i < Step; i++ )
00806             {
00807                 pRes[i]      = pTruth[i] ^ pTruth[Step+i];
00808                 pRes[Step+i] = pRes[i];
00809             }
00810             pRes += 2*Step;
00811             pTruth += 2*Step;
00812         }
00813         return;
00814     }
00815 }

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 230 of file kitTruth.c.

00231 {
00232     int nWords = Kit_TruthWordNum( nVars );
00233     int i, k, Step;
00234 
00235     assert( iVar < nVars );
00236     switch ( iVar )
00237     {
00238     case 0:
00239         for ( i = 0; i < nWords; i++ )
00240             if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) )
00241                 return 1;
00242         return 0;
00243     case 1:
00244         for ( i = 0; i < nWords; i++ )
00245             if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) )
00246                 return 1;
00247         return 0;
00248     case 2:
00249         for ( i = 0; i < nWords; i++ )
00250             if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) )
00251                 return 1;
00252         return 0;
00253     case 3:
00254         for ( i = 0; i < nWords; i++ )
00255             if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) )
00256                 return 1;
00257         return 0;
00258     case 4:
00259         for ( i = 0; i < nWords; i++ )
00260             if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) )
00261                 return 1;
00262         return 0;
00263     default:
00264         Step = (1 << (iVar - 5));
00265         for ( k = 0; k < nWords; k += 2*Step )
00266         {
00267             for ( i = 0; i < Step; i++ )
00268                 if ( pTruth[i] != pTruth[Step+i] )
00269                     return 1;
00270             pTruth += 2*Step;
00271         }
00272         return 0;
00273     }
00274 }

static int Kit_TruthWordNum ( int nVars ) [inline, static]

Definition at line 232 of file kit.h.

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

static void Kit_TruthXor	(	unsigned *	pOut,
		unsigned *	pIn0,
		unsigned *	pIn1,
		int	nVars
	)			`[inline, static]`

Definition at line 391 of file kit.h.

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

static void Kit_TruthXorBit	(	unsigned *	p,
		int	Bit
	)			`[inline, static]`

Definition at line 236 of file kit.h.

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

static int Kit_WordCountOnes ( unsigned uWord ) [inline, static]

Definition at line 251 of file kit.h.

00252 {
00253     uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
00254     uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
00255     uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
00256     uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
00257     return  (uWord & 0x0000FFFF) + (uWord>>16);
00258 }

static int Kit_WordFindFirstBit ( unsigned uWord ) [inline, static]

Definition at line 239 of file kit.h.

00240 {
00241     int i;
00242     for ( i = 0; i < 32; i++ )
00243         if ( uWord & (1 << i) )
00244             return i;
00245     return -1;
00246 }

static int Kit_WordHasOneBit ( unsigned uWord ) [inline, static]

Definition at line 247 of file kit.h.

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

src/aig/kit/kit.h File Reference

Data Structures

Defines

Typedefs

Enumerations

Functions

Define Documentation

Typedef Documentation

Enumeration Type Documentation

Function Documentation