kit.h File Reference

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

Include dependency graph for kit.h:

Go to the source code of this file.

Classes
struct	Kit_Sop_t_
struct	Kit_Edge_t_
struct	Kit_Node_t_
struct	Kit_Graph_t_
struct	Kit_DsdObj_t_
struct	Kit_DsdNtk_t_
struct	Kit_DsdMan_t_

Macros
#define	Kit_DsdNtkForEachObj(pNtk, pObj, i)
#define	Kit_DsdObjForEachFanin(pNtk, pObj, iLit, i)
#define	Kit_DsdObjForEachFaninReverse(pNtk, pObj, iLit, i)
#define	Kit_PlaForEachCube(pSop, nFanins, pCube)
#define	Kit_PlaCubeForEachVar(pCube, Value, i)
#define	KIT_MIN(a, b)
	MACRO DEFINITIONS ///.
#define	KIT_MAX(a, b)
#define	KIT_INFINITY   (100000000)
#define	Kit_SopForEachCube(cSop, uCube, i)
	ITERATORS ///.
#define	Kit_CubeForEachLiteral(uCube, Lit, nLits, i)
#define	Kit_GraphForEachLeaf(pGraph, pLeaf, i)
#define	Kit_GraphForEachNode(pGraph, pAnd, i)

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Kit_Sop_t_	Kit_Sop_t
	INCLUDES ///.
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
CloudNode *	Kit_TruthToCloud (CloudManager *dd, unsigned *pTruth, int nVars)
	FUNCTION DECLARATIONS ///.
unsigned *	Kit_CloudToTruth (Vec_Int_t *vNodes, int nVars, Vec_Ptr_t *vStore, int fInv)
int	Kit_CreateCloud (CloudManager *dd, CloudNode *pFunc, Vec_Int_t *vNodes)
int	Kit_CreateCloudFromTruth (CloudManager *dd, unsigned *pTruth, int nVars, Vec_Int_t *vNodes)
unsigned *	Kit_TruthCompose (CloudManager *dd, unsigned *pTruth, int nVars, unsigned **pInputs, int nVarsAll, Vec_Ptr_t *vStore, Vec_Int_t *vNodes)
void	Kit_TruthCofSupports (Vec_Int_t *vBddDir, Vec_Int_t *vBddInv, int nVars, Vec_Int_t *vMemory, unsigned *puSupps)
Kit_DsdMan_t *	Kit_DsdManAlloc (int nVars, int nNodes)
	DECLARATIONS ///.
void	Kit_DsdManFree (Kit_DsdMan_t *p)
Kit_DsdNtk_t *	Kit_DsdDeriveNtk (unsigned *pTruth, int nVars, int nLutSize)
unsigned *	Kit_DsdTruthCompute (Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk)
void	Kit_DsdTruth (Kit_DsdNtk_t *pNtk, unsigned *pTruthRes)
void	Kit_DsdTruthPartial (Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned *pTruthRes, unsigned uSupp)
void	Kit_DsdTruthPartialTwo (Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp, int iVar, unsigned *pTruthCo, unsigned *pTruthDec)
void	Kit_DsdPrint (FILE *pFile, Kit_DsdNtk_t *pNtk)
void	Kit_DsdPrintExpanded (Kit_DsdNtk_t *pNtk)
void	Kit_DsdPrintFromTruth (unsigned *pTruth, int nVars)
void	Kit_DsdPrintFromTruth2 (FILE *pFile, unsigned *pTruth, int nVars)
void	Kit_DsdWriteFromTruth (char *pBuffer, unsigned *pTruth, int nVars)
Kit_DsdNtk_t *	Kit_DsdDecompose (unsigned *pTruth, int nVars)
Kit_DsdNtk_t *	Kit_DsdDecomposeExpand (unsigned *pTruth, int nVars)
Kit_DsdNtk_t *	Kit_DsdDecomposeMux (unsigned *pTruth, int nVars, int nDecMux)
void	Kit_DsdVerify (Kit_DsdNtk_t *pNtk, unsigned *pTruth, int nVars)
void	Kit_DsdNtkFree (Kit_DsdNtk_t *pNtk)
int	Kit_DsdNonDsdSizeMax (Kit_DsdNtk_t *pNtk)
Kit_DsdObj_t *	Kit_DsdNonDsdPrimeMax (Kit_DsdNtk_t *pNtk)
unsigned	Kit_DsdNonDsdSupports (Kit_DsdNtk_t *pNtk)
int	Kit_DsdCountAigNodes (Kit_DsdNtk_t *pNtk)
unsigned	Kit_DsdGetSupports (Kit_DsdNtk_t *p)
Kit_DsdNtk_t *	Kit_DsdExpand (Kit_DsdNtk_t *p)
Kit_DsdNtk_t *	Kit_DsdShrink (Kit_DsdNtk_t *p, int pPrios[])
void	Kit_DsdRotate (Kit_DsdNtk_t *p, int pFreqs[])
int	Kit_DsdCofactoring (unsigned *pTruth, int nVars, int *pCofVars, int nLimit, int fVerbose)
Kit_Graph_t *	Kit_SopFactor (Vec_Int_t *vCover, int fCompl, int nVars, Vec_Int_t *vMemory)
	FUNCTION DEFINITIONS ///.
Kit_Graph_t *	Kit_GraphCreate (int nLeaves)
	DECLARATIONS ///.
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)
Kit_Graph_t *	Kit_TruthToGraph2 (unsigned *pTruth0, unsigned *pTruth1, int nVars, Vec_Int_t *vMemory)
int	Kit_GraphLeafDepth_rec (Kit_Graph_t *pGraph, Kit_Node_t *pNode, Kit_Node_t *pLeaf)
int	Kit_TruthLitNum (unsigned *pTruth, int nVars, Vec_Int_t *vMemory)
int	Kit_IsopNodeNum (unsigned *pTruth0, unsigned *pTruth1, int nVars, Vec_Int_t *vMemory)
Vec_Int_t *	Kit_IsopResub (unsigned *pTruth0, unsigned *pTruth1, int nVars, Vec_Int_t *vMemory)
int	Kit_TruthIsop (unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
int	Kit_TruthIsop2 (unsigned *puTruth0, unsigned *puTruth1, int nVars, Vec_Int_t *vMemory, int fTryBoth, int fReturnTt)
	FUNCTION DEFINITIONS ///.
void	Kit_TruthIsopPrint (unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
void	Kit_TruthIsopPrintCover (Vec_Int_t *vCover, int nVars, int fCompl)
int	Kit_PlaIsConst0 (char *pSop)
	DECLARATIONS ///.
int	Kit_PlaIsConst1 (char *pSop)
int	Kit_PlaIsBuf (char *pSop)
int	Kit_PlaIsInv (char *pSop)
int	Kit_PlaGetVarNum (char *pSop)
int	Kit_PlaGetCubeNum (char *pSop)
int	Kit_PlaIsComplement (char *pSop)
void	Kit_PlaComplement (char *pSop)
char *	Kit_PlaStart (void *p, int nCubes, int nVars)
char *	Kit_PlaCreateFromIsop (void *p, int nVars, Vec_Int_t *vCover)
void	Kit_PlaToIsop (char *pSop, Vec_Int_t *vCover)
char *	Kit_PlaStoreSop (void *p, char *pSop)
char *	Kit_PlaFromTruth (void *p, unsigned *pTruth, int nVars, Vec_Int_t *vCover)
char *	Kit_PlaFromTruthNew (unsigned *pTruth, int nVars, Vec_Int_t *vCover, Vec_Str_t *vStr)
ABC_UINT64_T	Kit_PlaToTruth6 (char *pSop, int nVars)
void	Kit_PlaToTruth (char *pSop, int nVars, Vec_Ptr_t *vVars, unsigned *pTemp, unsigned *pTruth)
void	Kit_SopCreate (Kit_Sop_t *cResult, Vec_Int_t *vInput, int nVars, Vec_Int_t *vMemory)
	DECLARATIONS ///.
void	Kit_SopCreateInverse (Kit_Sop_t *cResult, Vec_Int_t *vInput, int nVars, Vec_Int_t *vMemory)
void	Kit_SopDup (Kit_Sop_t *cResult, Kit_Sop_t *cSop, Vec_Int_t *vMemory)
void	Kit_SopDivideByLiteralQuo (Kit_Sop_t *cSop, int iLit)
void	Kit_SopDivideByCube (Kit_Sop_t *cSop, Kit_Sop_t *cDiv, Kit_Sop_t *vQuo, Kit_Sop_t *vRem, Vec_Int_t *vMemory)
void	Kit_SopDivideInternal (Kit_Sop_t *cSop, Kit_Sop_t *cDiv, Kit_Sop_t *vQuo, Kit_Sop_t *vRem, Vec_Int_t *vMemory)
void	Kit_SopMakeCubeFree (Kit_Sop_t *cSop)
int	Kit_SopIsCubeFree (Kit_Sop_t *cSop)
void	Kit_SopCommonCubeCover (Kit_Sop_t *cResult, Kit_Sop_t *cSop, Vec_Int_t *vMemory)
int	Kit_SopAnyLiteral (Kit_Sop_t *cSop, int nLits)
int	Kit_SopDivisor (Kit_Sop_t *cResult, Kit_Sop_t *cSop, int nLits, Vec_Int_t *vMemory)
void	Kit_SopBestLiteralCover (Kit_Sop_t *cResult, Kit_Sop_t *cSop, unsigned uCube, int nLits, Vec_Int_t *vMemory)
void	Kit_TruthSwapAdjacentVars (unsigned *pOut, unsigned *pIn, int nVars, int Start)
	DECLARATIONS ///.
void	Kit_TruthStretch (unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
void	Kit_TruthPermute (unsigned *pOut, unsigned *pIn, int nVars, char *pPerm, int fReturnIn)
void	Kit_TruthShrink (unsigned *pOut, unsigned *pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn)
int	Kit_TruthVarInSupport (unsigned *pTruth, int nVars, int iVar)
int	Kit_TruthSupportSize (unsigned *pTruth, int nVars)
unsigned	Kit_TruthSupport (unsigned *pTruth, int nVars)
void	Kit_TruthCofactor0 (unsigned *pTruth, int nVars, int iVar)
void	Kit_TruthCofactor1 (unsigned *pTruth, int nVars, int iVar)
void	Kit_TruthCofactor0New (unsigned *pOut, unsigned *pIn, int nVars, int iVar)
void	Kit_TruthCofactor1New (unsigned *pOut, unsigned *pIn, int nVars, int iVar)
int	Kit_TruthVarIsVacuous (unsigned *pOnset, unsigned *pOffset, int nVars, int iVar)
void	Kit_TruthExist (unsigned *pTruth, int nVars, int iVar)
void	Kit_TruthExistNew (unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
void	Kit_TruthExistSet (unsigned *pRes, unsigned *pTruth, int nVars, unsigned uMask)
void	Kit_TruthForall (unsigned *pTruth, int nVars, int iVar)
void	Kit_TruthForallNew (unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
void	Kit_TruthForallSet (unsigned *pRes, unsigned *pTruth, int nVars, unsigned uMask)
void	Kit_TruthUniqueNew (unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
void	Kit_TruthMuxVar (unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
void	Kit_TruthMuxVarPhase (unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar, int fCompl0)
void	Kit_TruthChangePhase (unsigned *pTruth, int nVars, int iVar)
int	Kit_TruthVarsSymm (unsigned *pTruth, int nVars, int iVar0, int iVar1, unsigned *pCof0, unsigned *pCof1)
int	Kit_TruthVarsAntiSymm (unsigned *pTruth, int nVars, int iVar0, int iVar1, unsigned *pCof0, unsigned *pCof1)
int	Kit_TruthMinCofSuppOverlap (unsigned *pTruth, int nVars, int *pVarMin)
int	Kit_TruthBestCofVar (unsigned *pTruth, int nVars, unsigned *pCof0, unsigned *pCof1)
void	Kit_TruthCountOnesInCofs (unsigned *pTruth, int nVars, int *pStore)
void	Kit_TruthCountOnesInCofs0 (unsigned *pTruth, int nVars, int *pStore)
void	Kit_TruthCountOnesInCofsSlow (unsigned *pTruth, int nVars, int *pStore, unsigned *pAux)
unsigned	Kit_TruthHash (unsigned *pIn, int nWords)
unsigned	Kit_TruthSemiCanonicize (unsigned *pInOut, unsigned *pAux, int nVars, char *pCanonPerm)
char *	Kit_TruthDumpToFile (unsigned *pTruth, int nVars, int nFile)
void	Kit_TruthPrintProfile (unsigned *pTruth, int nVars)

Macro Definition Documentation

Kit_CubeForEachLiteral

#define Kit_CubeForEachLiteral	(		uCube,
			Lit,
			nLits,
			i )

Value:

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

Definition at line 502 of file kit.h.

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

Kit_DsdNtkForEachObj

#define Kit_DsdNtkForEachObj	(		pNtk,
			pObj,
			i )

Value:

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

Definition at line 158 of file kit.h.

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

Kit_DsdObjForEachFanin

#define Kit_DsdObjForEachFanin	(		pNtk,
			pObj,
			iLit,
			i )

Value:

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

Definition at line 160 of file kit.h.

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

Kit_DsdObjForEachFaninReverse

#define Kit_DsdObjForEachFaninReverse	(		pNtk,
			pObj,
			iLit,
			i )

Value:

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

Definition at line 162 of file kit.h.

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

Kit_GraphForEachLeaf

#define Kit_GraphForEachLeaf	(		pGraph,
			pLeaf,
			i )

Value:

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

Definition at line 505 of file kit.h.

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

Kit_GraphForEachNode

#define Kit_GraphForEachNode	(		pGraph,
			pAnd,
			i )

Value:

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

Definition at line 507 of file kit.h.

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

KIT_INFINITY

#define KIT_INFINITY   (100000000)

Definition at line 176 of file kit.h.

KIT_MAX

#define KIT_MAX	(		a,
			b )

Value:

(((a) > (b))? (a) : (b))

Definition at line 175 of file kit.h.

KIT_MIN

#define KIT_MIN	(		a,
			b )

Value:

(((a) < (b))? (a) : (b))

MACRO DEFINITIONS ///.

Definition at line 174 of file kit.h.

Kit_PlaCubeForEachVar

#define Kit_PlaCubeForEachVar	(		pCube,
			Value,
			i )

Value:

    for ( i = 0; (pCube[i] != ' ') && (Value = pCube[i]); i++ )

Definition at line 167 of file kit.h.

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

Kit_PlaForEachCube

#define Kit_PlaForEachCube	(		pSop,
			nFanins,
			pCube )

Value:

    for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )

Definition at line 165 of file kit.h.

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

Kit_SopForEachCube

#define Kit_SopForEachCube	(		cSop,
			uCube,
			i )

Value:

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

ITERATORS ///.

Definition at line 500 of file kit.h.

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

Typedef Documentation

Kit_DsdMan_t

typedef struct Kit_DsdMan_t_ Kit_DsdMan_t

Definition at line 137 of file kit.h.

Kit_DsdNtk_t

typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t

Definition at line 124 of file kit.h.

Kit_DsdObj_t

typedef struct Kit_DsdObj_t_ Kit_DsdObj_t

Definition at line 111 of file kit.h.

Kit_Edge_t

typedef struct Kit_Edge_t_ Kit_Edge_t

Definition at line 62 of file kit.h.

Kit_Graph_t

typedef struct Kit_Graph_t_ Kit_Graph_t

Definition at line 88 of file kit.h.

Kit_Node_t

typedef struct Kit_Node_t_ Kit_Node_t

Definition at line 69 of file kit.h.

Kit_Sop_t

typedef typedefABC_NAMESPACE_HEADER_START struct Kit_Sop_t_ Kit_Sop_t

INCLUDES ///.

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

FileName [kit.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

] PARAMETERS /// BASIC TYPES ///

Definition at line 54 of file kit.h.

Enumeration Type Documentation

Kit_Dsd_t

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 101 of file kit.h.

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

Function Documentation

Kit_CloudToTruth()

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

extern

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

Synopsis [Computes composition of truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 229 of file kitCloud.c.

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

Here is the call graph for this function:

Kit_CreateCloud()

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

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 167 of file kitCloud.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_CreateCloudFromTruth()

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

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 209 of file kitCloud.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdCofactoring()

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

extern

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

{
    Kit_DsdNtk_t * ppNtks[5][16] = {
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}
    };
    Kit_DsdNtk_t * pTemp;
    unsigned * ppCofs[5][16];
    int pTryVars[16], nTryVars;
    int nPrimeSizeMin, nPrimeSizeMax, nPrimeSizeCur;
    int nSuppSizeMin, nSuppSizeMax, iVarBest;
    int i, k, v, nStep, nSize, nMemSize;
    assert( nLimit < 5 );
 
    // allocate storage for cofactors
    nMemSize = Kit_TruthWordNum(nVars);
    ppCofs[0][0] = ABC_ALLOC( unsigned, 80 * nMemSize );
    nSize = 0;
    for ( i = 0; i <  5; i++ )
    for ( k = 0; k < 16; k++ )
        ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
    assert( nSize == 80 );
 
    // copy the function
    Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
    ppNtks[0][0] = Kit_DsdDecompose( ppCofs[0][0], nVars );
 
    if ( fVerbose )
        printf( "\nProcessing prime function with %d support variables:\n", nVars );
 
    // perform recursive cofactoring
    for ( nStep = 0; nStep < nLimit; nStep++ )
    {
        nSize = (1 << nStep);
        // find the variables to use in the cofactoring step
        nTryVars = Kit_DsdCofactoringGetVars( ppNtks[nStep], nSize, pTryVars );
        if ( nTryVars == 0 )
            break;
        // cofactor w.r.t. the above variables
        iVarBest = -1;
        nPrimeSizeMin = 10000;
        nSuppSizeMin  = 10000;
        for ( v = 0; v < nTryVars; v++ )
        {
            nPrimeSizeMax = 0;
            nSuppSizeMax = 0;
            for ( i = 0; i < nSize; i++ )
            {
                // cofactor and decompose cofactors          
                Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, pTryVars[v] );
                Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, pTryVars[v] );
                ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars );
                ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars );
                // compute the largest non-decomp block
                nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+0]);
                nPrimeSizeMax  = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
                nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+1]);
                nPrimeSizeMax  = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur );
                // compute the sum total of supports
                nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+0], nVars );
                nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+1], nVars );
                // free the networks
                Kit_DsdNtkFree( ppNtks[nStep+1][2*i+0] );
                Kit_DsdNtkFree( ppNtks[nStep+1][2*i+1] );
            }
            // find the min max support size of the prime component
            if ( nPrimeSizeMin > nPrimeSizeMax || (nPrimeSizeMin == nPrimeSizeMax && nSuppSizeMin > nSuppSizeMax) )
            {
                nPrimeSizeMin = nPrimeSizeMax;
                nSuppSizeMin  = nSuppSizeMax;
                iVarBest      = pTryVars[v];
            }
        }
        assert( iVarBest != -1 );
        // save the variable
        if ( pCofVars )
            pCofVars[nStep] = iVarBest;
        // cofactor w.r.t. the best
        for ( i = 0; i < nSize; i++ )
        {
            Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, iVarBest );
            Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, iVarBest );
            ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars );
            ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars );
            if ( fVerbose )
            {
                ppNtks[nStep+1][2*i+0] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+0] );
                Kit_DsdNtkFree( pTemp );
                ppNtks[nStep+1][2*i+1] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+1] );
                Kit_DsdNtkFree( pTemp );
 
                printf( "Cof%d%d: ", nStep+1, 2*i+0 );
                Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+0] ), printf( "\n" );
                printf( "Cof%d%d: ", nStep+1, 2*i+1 );
                Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+1] ), printf( "\n" );
            }
        }
    }
 
    // free the networks
    for ( i = 0; i <  5; i++ )
    for ( k = 0; k < 16; k++ )
        if ( ppNtks[i][k] )
            Kit_DsdNtkFree( ppNtks[i][k] );
    ABC_FREE( ppCofs[0][0] );
 
    assert( nStep <= nLimit );
    return nStep;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdCountAigNodes()

int Kit_DsdCountAigNodes ( Kit_DsdNtk_t * pNtk )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1896 of file kitDsd.c.

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

Here is the caller graph for this function:

Kit_DsdDecompose()

Kit_DsdNtk_t * Kit_DsdDecompose ( unsigned * pTruth, int nVars )

extern

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

Synopsis [Performs decomposition of the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 2315 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdDecomposeExpand()

Kit_DsdNtk_t * Kit_DsdDecomposeExpand ( unsigned * pTruth, int nVars )

extern

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

Synopsis [Performs decomposition of the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 2331 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdDecomposeMux()

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

extern

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

Synopsis [Performs decomposition of the truth table.]

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

SideEffects []

SeeAlso []

Definition at line 2351 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdDeriveNtk()

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

extern

Kit_DsdExpand()

Kit_DsdNtk_t * Kit_DsdExpand ( Kit_DsdNtk_t * p )

extern

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

Synopsis [Expands the network.]

Description []

SideEffects []

SeeAlso []

Definition at line 1452 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdGetSupports()

unsigned Kit_DsdGetSupports ( Kit_DsdNtk_t * p )

extern

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

Synopsis [Compute the support.]

Description []

SideEffects []

SeeAlso []

Definition at line 1763 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdManAlloc()

Kit_DsdMan_t * Kit_DsdManAlloc ( int nVars, int nNodes )

extern

DECLARATIONS ///.

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

FileName [kitDsd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

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

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

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

Synopsis [Allocates the DSD manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdManFree()

void Kit_DsdManFree ( Kit_DsdMan_t * p )

extern

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

Synopsis [Deallocates the DSD manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 72 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdNonDsdPrimeMax()

Kit_DsdObj_t * Kit_DsdNonDsdPrimeMax ( Kit_DsdNtk_t * pNtk )

extern

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

Synopsis [Returns the largest non-DSD block.]

Description []

SideEffects []

SeeAlso []

Definition at line 1237 of file kitDsd.c.

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

Here is the caller graph for this function:

Kit_DsdNonDsdSizeMax()

int Kit_DsdNonDsdSizeMax ( Kit_DsdNtk_t * pNtk )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1212 of file kitDsd.c.

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

Here is the caller graph for this function:

Kit_DsdNonDsdSupports()

unsigned Kit_DsdNonDsdSupports ( Kit_DsdNtk_t * pNtk )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1265 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdNtkFree()

void Kit_DsdNtkFree ( Kit_DsdNtk_t * pNtk )

extern

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

Synopsis [Deallocate the DSD network.]

Description []

SideEffects []

SeeAlso []

Definition at line 164 of file kitDsd.c.

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

Here is the caller graph for this function:

Kit_DsdPrint()

void Kit_DsdPrint ( FILE * pFile, Kit_DsdNtk_t * pNtk )

extern

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 375 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdPrintExpanded()

void Kit_DsdPrintExpanded ( Kit_DsdNtk_t * pNtk )

extern

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 472 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdPrintFromTruth()

void Kit_DsdPrintFromTruth ( unsigned * pTruth, int nVars )

extern

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 491 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdPrintFromTruth2()

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

extern

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 515 of file kitDsd.c.

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

Here is the call graph for this function:

Kit_DsdRotate()

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

extern

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdShrink()

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

extern

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdTruth()

void Kit_DsdTruth ( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1069 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdTruthCompute()

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

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 664 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdTruthPartial()

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

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1108 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdTruthPartialTwo()

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

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1090 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdVerify()

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

extern

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

Synopsis [Performs decomposition of the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 2493 of file kitDsd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_DsdWriteFromTruth()

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

extern

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

Synopsis [Print the DSD formula.]

Description []

SideEffects []

SeeAlso []

Definition at line 537 of file kitDsd.c.

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

Here is the call graph for this function:

Kit_GraphAddNodeAnd()

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

extern

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

Synopsis [Creates an AND node.]

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file kitGraph.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_GraphAddNodeMux()

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

extern

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

Synopsis [Creates an XOR node.]

Description []

SideEffects []

SeeAlso []

Definition at line 266 of file kitGraph.c.

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

Here is the call graph for this function:

Kit_GraphAddNodeOr()

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

extern

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

Synopsis [Creates an OR node.]

Description []

SideEffects []

SeeAlso []

Definition at line 197 of file kitGraph.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_GraphAddNodeXor()

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

extern

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

Synopsis [Creates an XOR node.]

Description []

SideEffects []

SeeAlso []

Definition at line 225 of file kitGraph.c.

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

Here is the call graph for this function:

Kit_GraphAppendNode()

Kit_Node_t * Kit_GraphAppendNode ( Kit_Graph_t * pGraph )

extern

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

Synopsis [Appends a new node to the graph.]

Description [This procedure is meant for internal use.]

SideEffects []

SeeAlso []

Definition at line 149 of file kitGraph.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_GraphCreate()

Kit_Graph_t * Kit_GraphCreate ( int nLeaves )

extern

DECLARATIONS ///.

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

FileName [kitGraph.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Decomposition graph representation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file kitGraph.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_GraphCreateConst0()

Kit_Graph_t * Kit_GraphCreateConst0 ( )

extern

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

Synopsis [Creates constant 0 graph.]

Description []

SideEffects []

SeeAlso []

Definition at line 70 of file kitGraph.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_GraphCreateConst1()

Kit_Graph_t * Kit_GraphCreateConst1 ( )

extern

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

Synopsis [Creates constant 1 graph.]

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file kitGraph.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_GraphCreateLeaf()

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

extern

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

Synopsis [Creates the literal graph.]

Description []

SideEffects []

SeeAlso []

Definition at line 111 of file kitGraph.c.

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

Here is the call graph for this function:

Kit_GraphFree()

void Kit_GraphFree ( Kit_Graph_t * pGraph )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 132 of file kitGraph.c.

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

Here is the caller graph for this function:

Kit_GraphLeafDepth_rec()

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

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 412 of file kitGraph.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_GraphToTruth()

unsigned Kit_GraphToTruth ( Kit_Graph_t * pGraph )

extern

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

Synopsis [Derives the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file kitGraph.c.

{
    unsigned uTruths[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
    unsigned uTruth = 0, uTruth0, uTruth1;
    Kit_Node_t * pNode;
    int i;
 
    // sanity checks
    assert( Kit_GraphLeaveNum(pGraph) >= 0 );
    assert( Kit_GraphLeaveNum(pGraph) <= pGraph->nSize );
    assert( Kit_GraphLeaveNum(pGraph) <= 5 );
 
    // check for constant function
    if ( Kit_GraphIsConst(pGraph) )
        return Kit_GraphIsComplement(pGraph)? 0 : ~((unsigned)0);
    // check for a literal
    if ( Kit_GraphIsVar(pGraph) )
        return Kit_GraphIsComplement(pGraph)? ~uTruths[Kit_GraphVarInt(pGraph)] : uTruths[Kit_GraphVarInt(pGraph)];
 
    // assign the elementary variables
    Kit_GraphForEachLeaf( pGraph, pNode, i )
        pNode->pFunc = (void *)(long)uTruths[i];
 
    // compute the function for each internal node
    Kit_GraphForEachNode( pGraph, pNode, i )
    {
        uTruth0 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc;
        uTruth1 = (unsigned)(long)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc;
        uTruth0 = pNode->eEdge0.fCompl? ~uTruth0 : uTruth0;
        uTruth1 = pNode->eEdge1.fCompl? ~uTruth1 : uTruth1;
        uTruth = uTruth0 & uTruth1;
        pNode->pFunc = (void *)(long)uTruth;
    }
 
    // complement the result if necessary
    return Kit_GraphIsComplement(pGraph)? ~uTruth : uTruth;
}

Kit_IsopNodeNum()

int Kit_IsopNodeNum ( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory )

extern

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

Synopsis [Transforms the decomposition graph into the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 139 of file kitHop.c.

{
    Kit_Graph_t * pGraph;
    int nNodes;
    // transform truth table into the decomposition tree
    if ( vMemory == NULL )
    {
        vMemory = Vec_IntAlloc( 0 );
        pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
        Vec_IntFree( vMemory );
    }
    else
        pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
    if ( pGraph == NULL )
    {
        printf( "Kit_TruthToGia2(): Converting truth table to AIG has failed for function:\n" );
        Kit_DsdPrintFromTruth( pTruth0, nVars ); printf( "\n" );
        Kit_DsdPrintFromTruth( pTruth1, nVars ); printf( "\n" );
    }
    // derive the AIG for the decomposition tree
    nNodes = Kit_GraphNodeNum( pGraph );
    Kit_GraphFree( pGraph );
    return nNodes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_IsopResub()

Vec_Int_t * Kit_IsopResub ( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory )

extern

Definition at line 200 of file kitHop.c.

{
    Vec_Int_t * vRes = NULL;
    Kit_Graph_t * pGraph;
    int nNodes;
    // transform truth table into the decomposition tree
    if ( vMemory == NULL )
    {
        vMemory = Vec_IntAlloc( 0 );
        pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
        Vec_IntFree( vMemory );
    }
    else
        pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
    if ( pGraph == NULL )
    {
        printf( "Kit_TruthToGia2(): Converting truth table to AIG has failed for function:\n" );
        Kit_DsdPrintFromTruth( pTruth0, nVars ); printf( "\n" );
        Kit_DsdPrintFromTruth( pTruth1, nVars ); printf( "\n" );
    }
    // derive the AIG for the decomposition tree
    nNodes = Kit_GraphNodeNum( pGraph );
    vRes = Vec_IntAlloc( 2*nNodes + 1 );
    Kit_IsopResubInt( pGraph, vRes );
    assert( Vec_IntSize(vRes) == 2*nNodes + 1 );
    Kit_GraphFree( pGraph );
    return vRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_PlaComplement()

void Kit_PlaComplement ( char * pSop )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 181 of file kitPla.c.

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

Here is the caller graph for this function:

Kit_PlaCreateFromIsop()

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

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 243 of file kitPla.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_PlaFromTruth()

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

extern

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

Synopsis [Transforms truth table into the SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 337 of file kitPla.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_PlaFromTruthNew()

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

extern

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

Synopsis [Creates the SOP from TT.]

Description []

SideEffects []

SeeAlso []

Definition at line 406 of file kitPla.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_PlaGetCubeNum()

int Kit_PlaGetCubeNum ( char * pSop )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 138 of file kitPla.c.

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

Here is the caller graph for this function:

Kit_PlaGetVarNum()

int Kit_PlaGetVarNum ( char * pSop )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file kitPla.c.

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

Here is the caller graph for this function:

Kit_PlaIsBuf()

int Kit_PlaIsBuf ( char * pSop )

extern

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

Synopsis [Checks if the cover is a buffer.]

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file kitPla.c.

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

Kit_PlaIsComplement()

int Kit_PlaIsComplement ( char * pSop )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 160 of file kitPla.c.

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

Here is the caller graph for this function:

Kit_PlaIsConst0()

int Kit_PlaIsConst0 ( char * pSop )

extern

DECLARATIONS ///.

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

FileName [kitPla.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

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

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

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

Synopsis [Checks if the cover is constant 0.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file kitPla.c.

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

Here is the caller graph for this function:

Kit_PlaIsConst1()

int Kit_PlaIsConst1 ( char * pSop )

extern

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

Synopsis [Checks if the cover is constant 1.]

Description []

SideEffects []

SeeAlso []

Definition at line 62 of file kitPla.c.

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

Kit_PlaIsInv()

int Kit_PlaIsInv ( char * pSop )

extern

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

Synopsis [Checks if the cover is an inverter.]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file kitPla.c.

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

Kit_PlaStart()

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

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file kitPla.c.

{
    Aig_MmFlex_t * pMan = (Aig_MmFlex_t *)p;
    char * pSopCover, * pCube;
    int i, Length;
 
    Length = nCubes * (nVars + 3);
    pSopCover = Aig_MmFlexEntryFetch( pMan, Length + 1 );
    memset( pSopCover, '-', (size_t)Length );
    pSopCover[Length] = 0;
 
    for ( i = 0; i < nCubes; i++ )
    {
        pCube = pSopCover + i * (nVars + 3);
        pCube[nVars + 0] = ' ';
        pCube[nVars + 1] = '1';
        pCube[nVars + 2] = '\n';
    }
    return pSopCover;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_PlaStoreSop()

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

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 317 of file kitPla.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_PlaToIsop()

void Kit_PlaToIsop ( char * pSop, Vec_Int_t * vCover )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 282 of file kitPla.c.

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

Here is the call graph for this function:

Kit_PlaToTruth()

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

extern

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

Synopsis [Converting SOP into a truth table.]

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

SideEffects []

SeeAlso []

Definition at line 496 of file kitPla.c.

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

Here is the call graph for this function:

Kit_PlaToTruth6()

ABC_UINT64_T Kit_PlaToTruth6 ( char * pSop, int nVars )

extern

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

Synopsis [Converts SOP into a truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 442 of file kitPla.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_SopAnyLiteral()

int Kit_SopAnyLiteral ( Kit_Sop_t * cSop, int nLits )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 370 of file kitSop.c.

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

Here is the caller graph for this function:

Kit_SopBestLiteralCover()

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

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 560 of file kitSop.c.

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

Here is the call graph for this function:

Kit_SopCommonCubeCover()

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

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file kitSop.c.

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

Kit_SopCreate()

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

extern

DECLARATIONS ///.

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

FileName [kitSop.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Procedures involving SOPs.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

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

Synopsis [Creates SOP from the cube array.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file kitSop.c.

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

Kit_SopCreateInverse()

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

extern

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

Synopsis [Creates SOP from the cube array.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file kitSop.c.

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

Here is the caller graph for this function:

Kit_SopDivideByCube()

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

extern

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

Synopsis [Divides cover by one cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file kitSop.c.

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

Here is the caller graph for this function:

Kit_SopDivideByLiteralQuo()

void Kit_SopDivideByLiteralQuo ( Kit_Sop_t * cSop, int iLit )

extern

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

Synopsis [Derives the quotient of division by literal.]

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

SideEffects []

SeeAlso []

Definition at line 121 of file kitSop.c.

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

Here is the caller graph for this function:

Kit_SopDivideInternal()

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

extern

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

Synopsis [Divides cover by one cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file kitSop.c.

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

Here is the call graph for this function:

Kit_SopDivisor()

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

extern

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

Synopsis [Computes the quick divisor of the cover.]

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

SideEffects []

SeeAlso []

Definition at line 534 of file kitSop.c.

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

Here is the call graph for this function:

Kit_SopDup()

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

extern

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

Synopsis [Duplicates SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file kitSop.c.

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

Here is the caller graph for this function:

Kit_SopFactor()

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

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Factors the cover.]

Description []

SideEffects []

SeeAlso []

Definition at line 55 of file kitFactor.c.

{
    Kit_Sop_t Sop, * cSop = &Sop;
    Kit_Graph_t * pFForm;
    Kit_Edge_t eRoot;
//    int nCubes;
 
    // works for up to 15 variables because division procedure
    // used the last bit for marking the cubes going to the remainder
    assert( nVars < 16 );
 
    // check for trivial functions
    if ( Vec_IntSize(vCover) == 0 )
        return Kit_GraphCreateConst0();
    if ( Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0 )
        return Kit_GraphCreateConst1();
 
    // prepare memory manager
//    Vec_IntClear( vMemory );
    Vec_IntGrow( vMemory, KIT_FACTOR_MEM_LIMIT );
 
    // perform CST
    Kit_SopCreateInverse( cSop, vCover, 2 * nVars, vMemory ); // CST
 
    // start the factored form
    pFForm = Kit_GraphCreate( nVars );
    // factor the cover
    eRoot = Kit_SopFactor_rec( pFForm, cSop, 2 * nVars, vMemory );
    // finalize the factored form
    Kit_GraphSetRoot( pFForm, eRoot );
    if ( fCompl )
        Kit_GraphComplement( pFForm );
 
    // verify the factored form
//    nCubes = Vec_IntSize(vCover);
//    Vec_IntShrink( vCover, nCubes );
//    if ( !Kit_SopFactorVerify( vCover, pFForm, nVars ) )
//        printf( "Verification has failed.\n" );
    return pFForm;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_SopIsCubeFree()

int Kit_SopIsCubeFree ( Kit_Sop_t * cSop )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 334 of file kitSop.c.

{
    return Kit_SopCommonCube( cSop ) == 0;
}

Kit_SopMakeCubeFree()

void Kit_SopMakeCubeFree ( Kit_Sop_t * cSop )

extern

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

Synopsis [Makes the cover cube-free.]

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file kitSop.c.

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

Here is the caller graph for this function:

Kit_TruthBestCofVar()

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

extern

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

Synopsis [Find the best cofactoring variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 1365 of file kitTruth.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthChangePhase()

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

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1259 of file kitTruth.c.

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

Here is the caller graph for this function:

Kit_TruthCofactor0()

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

extern

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

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 368 of file kitTruth.c.

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

Here is the caller graph for this function:

Kit_TruthCofactor0New()

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

extern

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 521 of file kitTruth.c.

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

Here is the caller graph for this function:

Kit_TruthCofactor1()

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

extern

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 470 of file kitTruth.c.

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

Here is the caller graph for this function:

Kit_TruthCofactor1New()

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

extern

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

Synopsis [Computes positive cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 573 of file kitTruth.c.

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

Here is the caller graph for this function:

Kit_TruthCofSupports()

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

extern

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

Synopsis [Compute BDD for the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 310 of file kitCloud.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthCompose()

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

extern

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

Synopsis [Computes composition of truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 263 of file kitCloud.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthCountOnesInCofs()

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

extern

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

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

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

SideEffects []

SeeAlso []

Definition at line 1410 of file kitTruth.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthCountOnesInCofs0()

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

extern

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

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

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

SideEffects []

SeeAlso []

Definition at line 1486 of file kitTruth.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthCountOnesInCofsSlow()

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

extern

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

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

Description [Verifies the above procedure.]

SideEffects []

SeeAlso []

Definition at line 1537 of file kitTruth.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthDumpToFile()

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

extern

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

Synopsis [Dumps truth table into a file.]

Description [Generates script file for reading into ABC.]

SideEffects []

SeeAlso []

Definition at line 2004 of file kitTruth.c.

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

Here is the call graph for this function:

Kit_TruthExist()

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

extern

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

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 684 of file kitTruth.c.

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

Here is the caller graph for this function:

Kit_TruthExistNew()

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

extern

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

Synopsis [Existentially quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 738 of file kitTruth.c.

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

Here is the caller graph for this function:

Kit_TruthExistSet()

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

extern

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

Synopsis [Existantially quantifies the set of variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 793 of file kitTruth.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthForall()

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

extern

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

Synopsis [Unversally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 813 of file kitTruth.c.

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

Here is the caller graph for this function:

Kit_TruthForallNew()

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

extern

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

Synopsis [Universally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 867 of file kitTruth.c.

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

Here is the caller graph for this function:

Kit_TruthForallSet()

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

extern

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

Synopsis [Universally quantifies the set of variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 1048 of file kitTruth.c.

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

Here is the call graph for this function:

Kit_TruthHash()

unsigned Kit_TruthHash ( unsigned * pIn, int nWords )

extern

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

Synopsis [Canonicize the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 1560 of file kitTruth.c.

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

Kit_TruthIsop()

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

extern

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthIsop2()

int Kit_TruthIsop2 ( unsigned * puTruth0, unsigned * puTruth1, int nVars, Vec_Int_t * vMemory, int fTryBoth, int fReturnTt )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes ISOP from TT.]

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

SideEffects []

SeeAlso []

Definition at line 55 of file kitIsop.c.

{
    Kit_Sop_t cRes, * pcRes = &cRes;
    Kit_Sop_t cRes2, * pcRes2 = &cRes2;
    unsigned * pResult;
    int RetValue = 0;
    assert( nVars >= 0 && nVars <= 16 );
    // prepare memory manager
    Vec_IntClear( vMemory );
    Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT );
    // compute ISOP for the direct polarity
    Kit_TruthNot( puTruth0, puTruth0, nVars );
    pResult = Kit_TruthIsop_rec( puTruth1, puTruth0, nVars, pcRes, vMemory );
    Kit_TruthNot( puTruth0, puTruth0, nVars );
    if ( pcRes->nCubes == -1 )
    {
        vMemory->nSize = -1;
        return -1;
    }
    assert( Kit_TruthIsImply( puTruth1, pResult, nVars ) );
    Kit_TruthNot( puTruth0, puTruth0, nVars );
    assert( Kit_TruthIsImply( pResult, puTruth0, nVars ) );
    Kit_TruthNot( puTruth0, puTruth0, nVars );
    if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) )
    {
        vMemory->pArray[0] = 0;
        Vec_IntShrink( vMemory, pcRes->nCubes );
        return 0;
    }
    if ( fTryBoth )
    {
        // compute ISOP for the complemented polarity
        Kit_TruthNot( puTruth1, puTruth1, nVars );
        pResult = Kit_TruthIsop_rec( puTruth0, puTruth1, nVars, pcRes2, vMemory );
        Kit_TruthNot( puTruth1, puTruth1, nVars );
        if ( pcRes2->nCubes >= 0 )
        {
            assert( Kit_TruthIsImply( puTruth0, pResult, nVars ) );
            Kit_TruthNot( puTruth1, puTruth1, nVars );
            assert( Kit_TruthIsImply( pResult, puTruth1, nVars ) );
            Kit_TruthNot( puTruth1, puTruth1, nVars );
            if ( pcRes->nCubes > pcRes2->nCubes || (pcRes->nCubes == pcRes2->nCubes && pcRes->nLits > pcRes2->nLits) )
            {
                RetValue = 1;
                pcRes = pcRes2;
            }
        }
    }
//    printf( "%d ", vMemory->nSize );
    // move the cover representation to the beginning of the memory buffer
    if ( fReturnTt )
    {
        int nWords = Kit_TruthWordNum( nVars );
        memmove( vMemory->pArray, pResult, nWords * sizeof(unsigned) );
        Vec_IntShrink( vMemory, nWords );
    }
    else
    {
        memmove( vMemory->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
        Vec_IntShrink( vMemory, pcRes->nCubes );
    }
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthIsopPrint()

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

extern

Definition at line 207 of file kitIsop.c.

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

Here is the call graph for this function:

Kit_TruthIsopPrintCover()

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

extern

Definition at line 183 of file kitIsop.c.

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

Here is the caller graph for this function:

Kit_TruthLitNum()

int Kit_TruthLitNum ( unsigned * pTruth, int nVars, Vec_Int_t * vMemory )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 511 of file kitGraph.c.

{
    Kit_Graph_t * pGraph;
    int RetValue, nLits;
    RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 1 ); 
    if ( RetValue == -1 || Vec_IntSize(vMemory) > (1<<16) )
        return -1;
    assert( RetValue == 0 || RetValue == 1 );
    pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory );
    nLits = 1 + Kit_GraphNodeNum( pGraph );
    Kit_GraphFree( pGraph );
    return nLits;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthMinCofSuppOverlap()

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

extern

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

Synopsis [Computes minimum overlap in supports of cofactors.]

Description []

SideEffects []

SeeAlso []

Definition at line 1315 of file kitTruth.c.

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

Here is the call graph for this function:

Kit_TruthMuxVar()

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

extern

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

Synopsis [Multiplexes two functions with the given variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 1069 of file kitTruth.c.

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

Here is the caller graph for this function:

Kit_TruthMuxVarPhase()

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

extern

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

Synopsis [Multiplexes two functions with the given variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 1125 of file kitTruth.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthPermute()

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

extern

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

Synopsis [Implement give permutation.]

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

SideEffects [The input truth table is modified.]

SeeAlso []

Definition at line 233 of file kitTruth.c.

{
    unsigned * pTemp;
    int i, Temp, fChange, Counter = 0;
    do {
        fChange = 0;
        for ( i = 0; i < nVars-1; i++ )
        {
            assert( pPerm[i] != pPerm[i+1] );
            if ( pPerm[i] <= pPerm[i+1] )
                continue;
            Counter++;
            fChange = 1;
 
            Temp = pPerm[i];
            pPerm[i] = pPerm[i+1];
            pPerm[i+1] = Temp;
 
            Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
            pTemp = pIn; pIn = pOut; pOut = pTemp;
        }
    } while ( fChange );
    if ( fReturnIn ^ !(Counter & 1) )
        Kit_TruthCopy( pOut, pIn, nVars );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthPrintProfile()

void Kit_TruthPrintProfile ( unsigned * pTruth, int nVars )

extern

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

Synopsis [Dumps truth table into a file.]

Description [Generates script file for reading into ABC.]

SideEffects []

SeeAlso []

Definition at line 2203 of file kitTruth.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthSemiCanonicize()

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

extern

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

Synopsis [Canonicize the truth table.]

Description [Returns the phase. ]

SideEffects []

SeeAlso []

Definition at line 1657 of file kitTruth.c.

{
    int pStore[32];
    unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
    int nWords = Kit_TruthWordNum( nVars );
    int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
    unsigned uCanonPhase;
 
    // canonicize output
    uCanonPhase = 0;
    for ( i = 0; i < nVars; i++ )
        pCanonPerm[i] = i;
 
    nOnes = Kit_TruthCountOnes(pIn, nVars);
    //if(pIn[0] & 1)
    if ( (nOnes > nWords * 16) )//|| ((nOnes == nWords * 16) && (pIn[0] & 1)) )
    {
        uCanonPhase |= (1 << nVars);
        Kit_TruthNot( pIn, pIn, nVars );
    }
 
    // collect the minterm counts
    Kit_TruthCountOnesInCofs( pIn, nVars, pStore );
/*
    Kit_TruthCountOnesInCofsSlow( pIn, nVars, pStore2, pAux );
    for ( i = 0; i < 2*nVars; i++ )
    {
        assert( pStore[i] == pStore2[i] );
    }
*/
    // canonicize phase
    for ( i = 0; i < nVars; i++ )
    {
        if ( pStore[2*i+0] >= pStore[2*i+1] )
            continue;
        uCanonPhase |= (1 << i);
        Temp = pStore[2*i+0];
        pStore[2*i+0] = pStore[2*i+1];
        pStore[2*i+1] = Temp;
        Kit_TruthChangePhase( pIn, nVars, i );
    }
 
//    Kit_PrintHexadecimal( stdout, pIn, nVars );
//    printf( "\n" );
 
    // permute
    Counter = 0;
    do {
        fChange = 0;
        for ( i = 0; i < nVars-1; i++ )
        {
            if ( pStore[2*i] >= pStore[2*(i+1)] )
                continue;
            Counter++;
            fChange = 1;
 
            Temp = pCanonPerm[i];
            pCanonPerm[i] = pCanonPerm[i+1];
            pCanonPerm[i+1] = Temp;
 
            Temp = pStore[2*i];
            pStore[2*i] = pStore[2*(i+1)];
            pStore[2*(i+1)] = Temp;
 
            Temp = pStore[2*i+1];
            pStore[2*i+1] = pStore[2*(i+1)+1];
            pStore[2*(i+1)+1] = Temp;
 
            // if the polarity of variables is different, swap them
            if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
            {
                uCanonPhase ^= (1 << i);
                uCanonPhase ^= (1 << (i+1));
            }
 
            Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
            pTemp = pIn; pIn = pOut; pOut = pTemp;
        }
    } while ( fChange );
 
 
/*
    Extra_PrintBinary( stdout, &uCanonPhase, nVars+1 ); printf( " : " );
    for ( i = 0; i < nVars; i++ )
        printf( "%d=%d/%d  ", pCanonPerm[i], pStore[2*i], pStore[2*i+1] );
    printf( "  C = %d\n", Counter );
    Extra_PrintHexadecimal( stdout, pIn, nVars );
    printf( "\n" );
*/
 
/*
    // process symmetric variable groups
    uSymms = 0;
    for ( i = 0; i < nVars-1; i++ )
    {
        if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
            continue;
        if ( pStore[2*i] != pStore[2*i+1] )
            continue;
        if ( Kit_TruthVarsSymm( pIn, nVars, i, i+1 ) )
            continue;
        if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, i+1 ) )
            Kit_TruthChangePhase( pIn, nVars, i+1 );
    }
*/
 
/*
    // process symmetric variable groups
    uSymms = 0;
    for ( i = 0; i < nVars-1; i++ )
    {
        if ( pStore[2*i] != pStore[2*(i+1)] ) // i and i+1 cannot be symmetric
            continue;
        // i and i+1 can be symmetric
        // find the end of this group
        for ( k = i+1; k < nVars; k++ )
            if ( pStore[2*i] != pStore[2*k] ) 
                break;
        Limit = k;
        assert( i < Limit-1 );
        // go through the variables in this group
        for ( j = i + 1; j < Limit; j++ )
        {
            // check symmetry
            if ( Kit_TruthVarsSymm( pIn, nVars, i, j ) )
            {
                uSymms |= (1 << j);
                continue;
            }
            // they are phase-unknown
            if ( pStore[2*i] == pStore[2*i+1] ) 
            {
                if ( Kit_TruthVarsAntiSymm( pIn, nVars, i, j ) )
                {
                    Kit_TruthChangePhase( pIn, nVars, j );
                    uCanonPhase ^= (1 << j);
                    uSymms |= (1 << j);
                    continue;
                }
            }
 
            // they are not symmetric - move j as far as it goes in the group
            for ( k = j; k < Limit-1; k++ )
            {
                Counter++;
 
                Temp = pCanonPerm[k];
                pCanonPerm[k] = pCanonPerm[k+1];
                pCanonPerm[k+1] = Temp;
 
                assert( pStore[2*k] == pStore[2*(k+1)] );
                Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, k );
                pTemp = pIn; pIn = pOut; pOut = pTemp;
            }
            Limit--;
            j--;
        }
        i = Limit - 1;
    }
*/
 
    // swap if it was moved an even number of times
    if ( Counter & 1 )
        Kit_TruthCopy( pOut, pIn, nVars );
    return uCanonPhase;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthShrink()

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

extern

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

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

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

SideEffects [The input truth table is modified.]

SeeAlso []

Definition at line 200 of file kitTruth.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthStretch()

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

extern

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

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

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

SideEffects [The input truth table is modified.]

SeeAlso []

Definition at line 166 of file kitTruth.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthSupport()

unsigned Kit_TruthSupport ( unsigned * pTruth, int nVars )

extern

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

Synopsis [Returns support of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 346 of file kitTruth.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthSupportSize()

int Kit_TruthSupportSize ( unsigned * pTruth, int nVars )

extern

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

Synopsis [Returns the number of support vars.]

Description []

SideEffects []

SeeAlso []

Definition at line 327 of file kitTruth.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthSwapAdjacentVars()

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

extern

DECLARATIONS ///.

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

FileName [kitTruth.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Procedures involving truth tables.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

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

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

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

SideEffects []

SeeAlso []

Definition at line 46 of file kitTruth.c.

{
    static unsigned PMasks[4][3] = {
        { 0x99999999, 0x22222222, 0x44444444 },
        { 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 },
        { 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
        { 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
    };
    int nWords = Kit_TruthWordNum( nVars );
    int i, k, Step, Shift;
 
    assert( iVar < nVars - 1 );
    if ( iVar < 4 )
    {
        Shift = (1 << iVar);
        for ( i = 0; i < nWords; i++ )
            pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
    }
    else if ( iVar > 4 )
    {
        Step = (1 << (iVar - 5));
        for ( k = 0; k < nWords; k += 4*Step )
        {
            for ( i = 0; i < Step; i++ )
                pOut[i] = pIn[i];
            for ( i = 0; i < Step; i++ )
                pOut[Step+i] = pIn[2*Step+i];
            for ( i = 0; i < Step; i++ )
                pOut[2*Step+i] = pIn[Step+i];
            for ( i = 0; i < Step; i++ )
                pOut[3*Step+i] = pIn[3*Step+i];
            pIn  += 4*Step;
            pOut += 4*Step;
        }
    }
    else // if ( iVar == 4 )
    {
        for ( i = 0; i < nWords; i += 2 )
        {
            pOut[i]   = (pIn[i]   & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
            pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i]   & 0xFFFF0000) >> 16);
        }
    }
}

Here is the caller graph for this function:

Kit_TruthToCloud()

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

extern

FUNCTION DECLARATIONS ///.

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

Synopsis [Compute BDD for the truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 148 of file kitCloud.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthToGraph()

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

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 356 of file kitGraph.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthToGraph2()

Kit_Graph_t * Kit_TruthToGraph2 ( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 384 of file kitGraph.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_TruthUniqueNew()

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

extern

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

Synopsis [Universally quantifies the variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 922 of file kitTruth.c.

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

Here is the caller graph for this function:

Kit_TruthVarInSupport()

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

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 270 of file kitTruth.c.

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

Here is the caller graph for this function:

Kit_TruthVarIsVacuous()

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

extern

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

Synopsis [Computes negative cofactor of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 625 of file kitTruth.c.

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

Here is the caller graph for this function:

Kit_TruthVarsAntiSymm()

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

extern

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

Synopsis [Checks antisymmetry of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 1223 of file kitTruth.c.

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

Here is the call graph for this function:

Kit_TruthVarsSymm()

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

extern

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

Synopsis [Checks symmetry of two variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 1187 of file kitTruth.c.

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

Here is the call graph for this function: