kitIsop.c File Reference

#include "kit.h"

Include dependency graph for kitIsop.c:

Go to the source code of this file.

Macros
#define	KIT_ISOP_MEM_LIMIT   (1<<20)
	DECLARATIONS ///.

Functions
int	Kit_TruthIsop2 (unsigned *puTruth0, unsigned *puTruth1, int nVars, Vec_Int_t *vMemory, int fTryBoth, int fReturnTt)
	FUNCTION DEFINITIONS ///.
int	Kit_TruthIsop (unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
void	Kit_TruthIsopPrintCover (Vec_Int_t *vCover, int nVars, int fCompl)
void	Kit_TruthIsopPrint (unsigned *puTruth, int nVars, Vec_Int_t *vCover, int fTryBoth)

Macro Definition Documentation

KIT_ISOP_MEM_LIMIT

#define KIT_ISOP_MEM_LIMIT   (1<<20)

DECLARATIONS ///.

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

FileName [kitIsop.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [ISOP computation based on Morreale's algorithm.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

]

Definition at line 31 of file kitIsop.c.

Function Documentation

Kit_TruthIsop()

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

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 )

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 *	vCover,
		int	fTryBoth )

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 )

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: