cnfCut.c File Reference

#include "cnf.h"
#include "bool/kit/kit.h"

Include dependency graph for cnfCut.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Cnf_Cut_t *	Cnf_CutAlloc (Cnf_Man_t *p, int nLeaves)
	DECLARATIONS ///.
void	Cnf_CutFree (Cnf_Cut_t *pCut)
Cnf_Cut_t *	Cnf_CutCreate (Cnf_Man_t *p, Aig_Obj_t *pObj)
void	Cnf_CutPrint (Cnf_Cut_t *pCut)
void	Cnf_CutDeref (Cnf_Man_t *p, Cnf_Cut_t *pCut)
void	Cnf_CutRef (Cnf_Man_t *p, Cnf_Cut_t *pCut)
void	Cnf_CutUpdateRefs (Cnf_Man_t *p, Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, Cnf_Cut_t *pCutRes)
void	Cnf_CutRemoveIthVar (Cnf_Cut_t *pCut, int iVar, int iFan)
void	Cnf_CutInsertIthVar (Cnf_Cut_t *pCut, int iVar, int iFan)
Cnf_Cut_t *	Cnf_CutCompose (Cnf_Man_t *p, Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, int iFan)

Function Documentation

Cnf_CutAlloc()

ABC_NAMESPACE_IMPL_START Cnf_Cut_t * Cnf_CutAlloc	(	Cnf_Man_t *	p,
		int	nLeaves )

DECLARATIONS ///.

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

FileName [cnfCut.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG-to-CNF conversion.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id

cnfCut.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

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

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file cnfCut.c.

{
    Cnf_Cut_t * pCut;
    int nSize = sizeof(Cnf_Cut_t) + sizeof(int) * nLeaves + sizeof(unsigned) * Abc_TruthWordNum(nLeaves);
    pCut = (Cnf_Cut_t *)Aig_MmFlexEntryFetch( p->pMemCuts, nSize );
    pCut->nFanins = nLeaves;
    pCut->nWords = Abc_TruthWordNum(nLeaves);
    pCut->vIsop[0] = pCut->vIsop[1] = NULL;
    return pCut;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cnf_CutCompose()

Cnf_Cut_t * Cnf_CutCompose	(	Cnf_Man_t *	p,
		Cnf_Cut_t *	pCut,
		Cnf_Cut_t *	pCutFan,
		int	iFan )

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

Synopsis [Merges two cuts.]

Description [Returns NULL of the cuts cannot be merged.]

SideEffects []

SeeAlso []

Definition at line 294 of file cnfCut.c.

{
    Cnf_Cut_t * pCutRes;
    static int pFanins[32];
    unsigned * pTruth, * pTruthFan, * pTruthRes;
    unsigned * pTop = p->pTruths[0], * pFan = p->pTruths[2], * pTemp = p->pTruths[3];
    unsigned uPhase, uPhaseFan;
    int i, iVar, nFanins, RetValue;
 
    // make sure the second cut is the fanin of the first
    for ( iVar = 0; iVar < pCut->nFanins; iVar++ )
        if ( pCut->pFanins[iVar] == iFan )
            break;
    assert( iVar < pCut->nFanins );
    // remove this variable
    Cnf_CutRemoveIthVar( pCut, iVar, iFan );
    // merge leaves of the cuts
    nFanins = Cnf_CutMergeLeaves( pCut, pCutFan, pFanins );
    if ( nFanins+1 > p->nMergeLimit )
    {
        Cnf_CutInsertIthVar( pCut, iVar, iFan );
        return NULL;
    }
    // create new cut
    pCutRes = Cnf_CutAlloc( p, nFanins );
    memcpy( pCutRes->pFanins, pFanins, sizeof(int) * nFanins );
    assert( pCutRes->nFanins <= pCut->nFanins + pCutFan->nFanins );
 
    // derive its truth table
    // get the truth tables in the composition space
    pTruth    = Cnf_CutTruth(pCut);
    pTruthFan = Cnf_CutTruth(pCutFan);
    pTruthRes = Cnf_CutTruth(pCutRes);
    for ( i = 0; i < 2*pCutRes->nWords; i++ )
        pTop[i] = pTruth[i % pCut->nWords];
    for ( i = 0; i < pCutRes->nWords; i++ )
        pFan[i] = pTruthFan[i % pCutFan->nWords];
    // move the variable to the end
    uPhase = Kit_BitMask( pCutRes->nFanins+1 ) & ~(1 << iVar);
    Kit_TruthShrink( pTemp, pTop, pCutRes->nFanins, pCutRes->nFanins+1, uPhase, 1 );
    // compute the phases
    uPhase    = Cnf_TruthPhase( pCutRes, pCut    ) | (1 << pCutRes->nFanins);
    uPhaseFan = Cnf_TruthPhase( pCutRes, pCutFan );
    // permute truth-tables to the common support
    Kit_TruthStretch( pTemp, pTop, pCut->nFanins+1,  pCutRes->nFanins+1, uPhase,    1 );
    Kit_TruthStretch( pTemp, pFan, pCutFan->nFanins, pCutRes->nFanins,   uPhaseFan, 1 );
    // perform Boolean operation
    Kit_TruthMux( pTruthRes, pTop, pTop+pCutRes->nWords, pFan, pCutRes->nFanins );
    // return the cut to its original condition
    Cnf_CutInsertIthVar( pCut, iVar, iFan );
    // consider the simple case
    if ( pCutRes->nFanins < 5 )
    {
        pCutRes->Cost = p->pSopSizes[0xFFFF & *pTruthRes] + p->pSopSizes[0xFFFF & ~*pTruthRes];
        return pCutRes;
    }
 
    // derive ISOP for positive phase
    RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
    pCutRes->vIsop[1] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
    // derive ISOP for negative phase
    Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
    RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
    pCutRes->vIsop[0] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
    Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
 
    // compute the cut cost
    if ( pCutRes->vIsop[0] == NULL || pCutRes->vIsop[1] == NULL )
        pCutRes->Cost = 127;
    else if ( Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]) > 127 )
        pCutRes->Cost = 127;
    else
        pCutRes->Cost = Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]);
    return pCutRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cnf_CutCreate()

Cnf_Cut_t * Cnf_CutCreate	(	Cnf_Man_t *	p,
		Aig_Obj_t *	pObj )

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

Synopsis [Creates cut for the given node.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file cnfCut.c.

{
    Dar_Cut_t * pCutBest;
    Cnf_Cut_t * pCut;
    unsigned * pTruth;
    assert( Aig_ObjIsNode(pObj) );
    pCutBest = Dar_ObjBestCut( pObj );
    assert( pCutBest != NULL );
    assert( pCutBest->nLeaves <= 4 );
    pCut = Cnf_CutAlloc( p, pCutBest->nLeaves );
    memcpy( pCut->pFanins, pCutBest->pLeaves, sizeof(int) * pCutBest->nLeaves );
    pTruth = Cnf_CutTruth(pCut);
    *pTruth = (pCutBest->uTruth << 16) | pCutBest->uTruth;
    pCut->Cost = Cnf_CutSopCost( p, pCutBest );
    return pCut;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cnf_CutDeref()

void Cnf_CutDeref	(	Cnf_Man_t *	p,
		Cnf_Cut_t *	pCut )

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

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 135 of file cnfCut.c.

{
    Aig_Obj_t * pObj;
    int i;
    Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
    {
        assert( pObj->nRefs > 0 );
        pObj->nRefs--;
    }
}

Here is the caller graph for this function:

Cnf_CutFree()

void Cnf_CutFree

(

Cnf_Cut_t *

pCut

)

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

Synopsis [Deallocates cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file cnfCut.c.

{
    if ( pCut->vIsop[0] )
        Vec_IntFree( pCut->vIsop[0] );
    if ( pCut->vIsop[1] )
        Vec_IntFree( pCut->vIsop[1] );
}

Here is the caller graph for this function:

Cnf_CutInsertIthVar()

void Cnf_CutInsertIthVar	(	Cnf_Cut_t *	pCut,
		int	iVar,
		int	iFan )

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

Synopsis [Inserts the fanin variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 274 of file cnfCut.c.

{
    int i;
    for ( i = pCut->nFanins; i > iVar; i-- )
        pCut->pFanins[i] = pCut->pFanins[i-1];
    pCut->pFanins[iVar] = iFan;
    pCut->nFanins++;
}

Here is the caller graph for this function:

Cnf_CutPrint()

void Cnf_CutPrint

(

Cnf_Cut_t *

pCut

)

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

Synopsis [Deallocates cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 115 of file cnfCut.c.

{
    int i;
    printf( "{" );
    for ( i = 0; i < pCut->nFanins; i++ )
        printf( "%d ", pCut->pFanins[i] );
    printf( " } " );
}

Cnf_CutRef()

void Cnf_CutRef	(	Cnf_Man_t *	p,
		Cnf_Cut_t *	pCut )

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

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 157 of file cnfCut.c.

{
    Aig_Obj_t * pObj;
    int i;
    Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
    {
        pObj->nRefs++;
    }
}

Here is the caller graph for this function:

Cnf_CutRemoveIthVar()

void Cnf_CutRemoveIthVar	(	Cnf_Cut_t *	pCut,
		int	iVar,
		int	iFan )

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

Synopsis [Removes the fanin variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 254 of file cnfCut.c.

{
    int i;
    assert( pCut->pFanins[iVar] == iFan );
    pCut->nFanins--;
    for ( i = iVar; i < pCut->nFanins; i++ )
        pCut->pFanins[i] = pCut->pFanins[i+1];
}

Here is the caller graph for this function:

Cnf_CutUpdateRefs()

void Cnf_CutUpdateRefs	(	Cnf_Man_t *	p,
		Cnf_Cut_t *	pCut,
		Cnf_Cut_t *	pCutFan,
		Cnf_Cut_t *	pCutRes )

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

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file cnfCut.c.

{
    Cnf_CutDeref( p, pCut );
    Cnf_CutDeref( p, pCutFan );
    Cnf_CutRef( p, pCutRes );
}

Here is the call graph for this function:

Here is the caller graph for this function: