darInt.h File Reference

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

Go to the source code of this file.

Data Structures
struct	Dar_Cut_t_
struct	Dar_Man_t_

Macros
#define	Dar_ObjForEachCutAll(pObj, pCut, i)   for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ )
	MACRO DEFINITIONS ///. More...
#define	Dar_ObjForEachCut(pObj, pCut, i)   for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ ) if ( (pCut)->fUsed==0 ) {} else
#define	Dar_CutForEachLeaf(p, pCut, pLeaf, i)   for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pLeaf) = Aig_ManObj(p, (pCut)->pLeaves[i])), 1); i++ )

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Dar_Man_t_	Dar_Man_t
	INCLUDES ///. More...
typedef struct Dar_Cut_t_	Dar_Cut_t

Functions
static Dar_Cut_t *	Dar_ObjCuts (Aig_Obj_t *pObj)
static void	Dar_ObjSetCuts (Aig_Obj_t *pObj, Dar_Cut_t *pCuts)
void	Dar_ManCutsRestart (Dar_Man_t *p, Aig_Obj_t *pRoot)
	FUNCTION DECLARATIONS ///. More...
void	Dar_ManCutsFree (Dar_Man_t *p)
Dar_Cut_t *	Dar_ObjPrepareCuts (Dar_Man_t *p, Aig_Obj_t *pObj)
Dar_Cut_t *	Dar_ObjComputeCuts_rec (Dar_Man_t *p, Aig_Obj_t *pObj)
Dar_Cut_t *	Dar_ObjComputeCuts (Dar_Man_t *p, Aig_Obj_t *pObj, int fSkipTtMin)
void	Dar_ObjCutPrint (Aig_Man_t *p, Aig_Obj_t *pObj)
Vec_Int_t *	Dar_LibReadNodes ()
Vec_Int_t *	Dar_LibReadOuts ()
Vec_Int_t *	Dar_LibReadPrios ()
void	Dar_LibStart ()
	MACRO DEFINITIONS ///. More...
void	Dar_LibStop ()
void	Dar_LibReturnCanonicals (unsigned *pCanons)
void	Dar_LibEval (Dar_Man_t *p, Aig_Obj_t *pRoot, Dar_Cut_t *pCut, int Required, int *pnMffcSize)
Aig_Obj_t *	Dar_LibBuildBest (Dar_Man_t *p)
Dar_Man_t *	Dar_ManStart (Aig_Man_t *pAig, Dar_RwrPar_t *pPars)
	DECLARATIONS ///. More...
void	Dar_ManStop (Dar_Man_t *p)
void	Dar_ManPrintStats (Dar_Man_t *p)
char **	Dar_Permutations (int n)
void	Dar_Truth4VarNPN (unsigned short **puCanons, char **puPhases, char **puPerms, unsigned char **puMap)

Macro Definition Documentation

#define Dar_CutForEachLeaf	(		p,
			pCut,
			pLeaf,
			i
	)		for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pLeaf) = Aig_ManObj(p, (pCut)->pLeaves[i])), 1); i++ )

Definition at line 124 of file darInt.h.

#define Dar_ObjForEachCut	(		pObj,
			pCut,
			i
	)		for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ ) if ( (pCut)->fUsed==0 ) {} else

Definition at line 121 of file darInt.h.

#define Dar_ObjForEachCutAll	(		pObj,
			pCut,
			i
	)		for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ )

MACRO DEFINITIONS ///.

ITERATORS ///

Definition at line 119 of file darInt.h.

Typedef Documentation

typedef struct Dar_Cut_t_ Dar_Cut_t

Definition at line 52 of file darInt.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Dar_Man_t_ Dar_Man_t

INCLUDES ///.

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

FileName [darInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [Internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

darInt.h,v 1.00 2007/04/28 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 51 of file darInt.h.

Function Documentation

Aig_Obj_t* Dar_LibBuildBest

(

Dar_Man_t *

p

)

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

Synopsis [Reconstructs the best cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 1031 of file darLib.c.

{
    int i, Counter = 4;
    for ( i = 0; i < Vec_PtrSize(p->vLeavesBest); i++ )
        s_DarLib->pDatas[i].pFunc = (Aig_Obj_t *)Vec_PtrEntry( p->vLeavesBest, i );
    Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, p->OutBest), &Counter );
    return Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, p->OutBest) );
}

void Dar_LibEval	(	Dar_Man_t *	p,
		Aig_Obj_t *	pRoot,
		Dar_Cut_t *	pCut,
		int	Required,
		int *	pnMffcSize
	)

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

Synopsis [Evaluates one cut.]

Description [Returns the best gain.]

SideEffects []

SeeAlso []

Definition at line 920 of file darLib.c.

{
    int fTraining = 0;
    float PowerSaved, PowerAdded;
    Dar_LibObj_t * pObj;
    int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained;
    abctime clk = Abc_Clock();
    if ( pCut->nLeaves != 4 )
        return;
    // check if the cut exits and assigns leaves and their levels
    if ( !Dar_LibCutMatch(p, pCut) )
        return;
    // mark MFFC of the node
    nNodesSaved = Dar_LibCutMarkMffc( p->pAig, pRoot, pCut->nLeaves, p->pPars->fPower? &PowerSaved : NULL );
    // evaluate the cut
    Class = s_DarLib->pMap[pCut->uTruth];
    Dar_LibEvalAssignNums( p, Class, pRoot );
    // profile outputs by their savings
    p->nTotalSubgs += s_DarLib->nSubgr0[Class];
    p->ClassSubgs[Class] += s_DarLib->nSubgr0[Class];
    for ( Out = 0; Out < s_DarLib->nSubgr0[Class]; Out++ )
    {
        pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr0[Class][Out]);
        if ( Aig_Regular(s_DarLib->pDatas[pObj->Num].pFunc) == pRoot )
            continue;
        nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required, p->pPars->fPower? &PowerAdded : NULL );
        nNodesGained = nNodesSaved - nNodesAdded;
        if ( p->pPars->fPower && PowerSaved < PowerAdded )
            continue;
        if ( fTraining && nNodesGained >= 0 )
            Dar_LibIncrementScore( Class, Out, nNodesGained + 1 );
        if ( nNodesGained < 0 || (nNodesGained == 0 && !p->pPars->fUseZeros) )
            continue;
        if ( nNodesGained <  p->GainBest || 
            (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->LevelBest) )
            continue;
        // remember this possibility
        Vec_PtrClear( p->vLeavesBest );
        for ( k = 0; k < (int)pCut->nLeaves; k++ )
            Vec_PtrPush( p->vLeavesBest, s_DarLib->pDatas[k].pFunc );
        p->OutBest    = s_DarLib->pSubgr0[Class][Out];
        p->OutNumBest = Out;
        p->LevelBest  = s_DarLib->pDatas[pObj->Num].Level;
        p->GainBest   = nNodesGained;
        p->ClassBest  = Class;
        assert( p->LevelBest <= Required );
        *pnMffcSize   = nNodesSaved;
    }
clk = Abc_Clock() - clk;
p->ClassTimes[Class] += clk;
p->timeEval += clk;
}

Vec_Int_t* Dar_LibReadNodes

(

)

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

Synopsis [Reads library from array.]

Description []

SideEffects []

SeeAlso []

Definition at line 11094 of file darData.c.

{
    Vec_Int_t * vResult;
    int i;
    vResult = Vec_IntAlloc( s_nDataSize1 );
    for ( i = 0; i < s_nDataSize1; i++ )
        Vec_IntPush( vResult, s_Data1[i] );
    return vResult;
}

Vec_Int_t* Dar_LibReadOuts

(

)

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

Synopsis [Reads library from array.]

Description []

SideEffects []

SeeAlso []

Definition at line 11115 of file darData.c.

{
    Vec_Int_t * vResult;
    int i;
    vResult = Vec_IntAlloc( s_nDataSize2 );
    for ( i = 0; i < s_nDataSize2; i++ )
        Vec_IntPush( vResult, s_Data2[i] );
    return vResult;
}

Vec_Int_t* Dar_LibReadPrios

(

)

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

Synopsis [Reads library from array.]

Description []

SideEffects []

SeeAlso []

Definition at line 11136 of file darData.c.

{
    Vec_Int_t * vResult;
    int i;
    vResult = Vec_IntAlloc( s_nDataSize3 );
    for ( i = 0; i < s_nDataSize3; i++ )
        Vec_IntPush( vResult, s_Data3[i] );
    return vResult;
}

void Dar_LibReturnCanonicals

(

unsigned *

pCanons

)

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

Synopsis [Returns canonical truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file darLib.c.

{
    int Visits[222] = {0};
    int i, k;
    // find canonical truth tables
    for ( i = k = 0; i < (1<<16); i++ )
        if ( !Visits[s_DarLib->pMap[i]] )
        {
            Visits[s_DarLib->pMap[i]] = 1;
            pCanons[k++] = ((i<<16) | i);
        }
    assert( k == 222 );
}

void Dar_LibStart

(

)

MACRO DEFINITIONS ///.

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

Synopsis [Starts the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 593 of file darLib.c.

{
//    abctime clk = Abc_Clock();
    if ( s_DarLib != NULL )
        return;
    assert( s_DarLib == NULL );
    s_DarLib = Dar_LibRead();
//    printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal );
//    ABC_PRT( "Time", Abc_Clock() - clk );
}

void Dar_LibStop

(

)

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

Synopsis [Stops the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 615 of file darLib.c.

{
    assert( s_DarLib != NULL );
    Dar_LibFree( s_DarLib );
    s_DarLib = NULL;
}

void Dar_ManCutsFree

(

Dar_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 648 of file darCut.c.

{
    if ( p->pMemCuts == NULL )
        return;
    Aig_MmFixedStop( p->pMemCuts, 0 );
    p->pMemCuts = NULL;
//    Aig_ManCleanData( p );
}

void Dar_ManCutsRestart	(	Dar_Man_t *	p,
		Aig_Obj_t *	pRoot
	)

FUNCTION DECLARATIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 714 of file darCut.c.

{
    Aig_Obj_t * pObj;
    int i;
    Dar_ObjSetCuts( Aig_ManConst1(p->pAig), NULL );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vCutNodes, pObj, i )
        if ( !Aig_ObjIsNone(pObj) )
            Dar_ObjSetCuts( pObj, NULL );
    Vec_PtrClear( p->vCutNodes );
    Aig_MmFixedRestart( p->pMemCuts );
    Dar_ObjPrepareCuts( p, Aig_ManConst1(p->pAig) );
}

void Dar_ManPrintStats

(

Dar_Man_t *

p

)

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

Synopsis [Stops the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 93 of file darMan.c.

{
    unsigned pCanons[222];
    int Gain, i;
    extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );

    Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig);
    printf( "Tried = %8d. Beg = %8d. End = %8d. Gain = %6d. (%6.2f %%).  Cut mem = %d MB\n", 
        p->nNodesTried, p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit, p->nCutMemUsed );
    printf( "Cuts = %8d. Tried = %8d. Used = %8d. Bad = %5d. Skipped = %5d. Ave = %.2f.\n", 
        p->nCutsAll, p->nCutsTried, p->nCutsUsed, p->nCutsBad, p->nCutsSkipped,
        (float)p->nCutsUsed/Aig_ManNodeNum(p->pAig) );

    printf( "Bufs = %5d. BufMax = %5d. BufReplace = %6d. BufFix = %6d.  Levels = %4d.\n", 
        Aig_ManBufNum(p->pAig), p->pAig->nBufMax, p->pAig->nBufReplaces, p->pAig->nBufFixes, Aig_ManLevels(p->pAig) );
    ABC_PRT( "Cuts  ", p->timeCuts );
    ABC_PRT( "Eval  ", p->timeEval );
    ABC_PRT( "Other ", p->timeOther );
    ABC_PRT( "TOTAL ", p->timeTotal );

    if ( !p->pPars->fVeryVerbose )
        return;
    Dar_LibReturnCanonicals( pCanons );
    for ( i = 0; i < 222; i++ )
    {
        if ( p->ClassGains[i] == 0 && p->ClassTimes[i] == 0 )
            continue;
        printf( "%3d : ", i );
        printf( "G = %6d (%5.2f %%)  ", p->ClassGains[i], Gain? 100.0*p->ClassGains[i]/Gain : 0.0 );
        printf( "S = %8d (%5.2f %%)  ", p->ClassSubgs[i], p->nTotalSubgs? 100.0*p->ClassSubgs[i]/p->nTotalSubgs : 0.0 );
        printf( "R = %7d   ", p->ClassGains[i]? p->ClassSubgs[i]/p->ClassGains[i] : 9999999 );
//        Kit_DsdPrintFromTruth( pCanons + i, 4 );
//        ABC_PRTP( "T", p->ClassTimes[i], p->timeEval );
        printf( "\n" );
    }
    fflush( stdout );
}

Dar_Man_t* Dar_ManStart	(	Aig_Man_t *	pAig,
		Dar_RwrPar_t *	pPars
	)

DECLARATIONS ///.

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

FileName [darMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [AIG manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Starts the rewriting manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file darMan.c.

{
    Dar_Man_t * p;
    Aig_ManCleanData( pAig );
    p = ABC_ALLOC( Dar_Man_t, 1 );
    memset( p, 0, sizeof(Dar_Man_t) );
    p->pPars = pPars;
    p->pAig  = pAig;
    p->vCutNodes = Vec_PtrAlloc( 1000 );
    p->pMemCuts = Aig_MmFixedStart( p->pPars->nCutsMax * sizeof(Dar_Cut_t), 1024 );
    p->vLeavesBest = Vec_PtrAlloc( 4 );
    return p;
}

void Dar_ManStop

(

Dar_Man_t *

p

)

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

Synopsis [Stops the rewriting manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 69 of file darMan.c.

{
    if ( p->pPars->fVerbose )
        Dar_ManPrintStats( p );
    if ( p->vCutNodes )
        Vec_PtrFree( p->vCutNodes );
    if ( p->pMemCuts )
        Aig_MmFixedStop( p->pMemCuts, 0 );
    if ( p->vLeavesBest ) 
        Vec_PtrFree( p->vLeavesBest );
    ABC_FREE( p );
}

Dar_Cut_t* Dar_ObjComputeCuts	(	Dar_Man_t *	p,
		Aig_Obj_t *	pObj,
		int	fSkipTtMin
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 738 of file darCut.c.

{
    Aig_Obj_t * pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
    Aig_Obj_t * pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
    Aig_Obj_t * pFaninR0 = Aig_Regular(pFanin0);
    Aig_Obj_t * pFaninR1 = Aig_Regular(pFanin1);
    Dar_Cut_t * pCutSet, * pCut0, * pCut1, * pCut;
    int i, k; 

    assert( !Aig_IsComplement(pObj) );
    assert( Aig_ObjIsNode(pObj) );
    assert( Dar_ObjCuts(pObj) == NULL );
    assert( Dar_ObjCuts(pFaninR0) != NULL );
    assert( Dar_ObjCuts(pFaninR1) != NULL );

    // set up the first cut
    pCutSet = Dar_ObjPrepareCuts( p, pObj );
    // make sure fanins cuts are computed
    Dar_ObjForEachCut( pFaninR0, pCut0, i )
    Dar_ObjForEachCut( pFaninR1, pCut1, k )
    {
        p->nCutsAll++;
        // make sure K-feasible cut exists
        if ( Dar_WordCountOnes(pCut0->uSign | pCut1->uSign) > 4 )
            continue;
        // get the next cut of this node
        pCut = Dar_CutFindFree( p, pObj );
        // create the new cut
        if ( !Dar_CutMerge( pCut, pCut0, pCut1 ) )
        {
            assert( !pCut->fUsed );
            continue;
        }
        p->nCutsTried++;
        // check dominance
        if ( Dar_CutFilter( pObj, pCut ) )
        {
            assert( !pCut->fUsed );
            continue;
        }
        // compute truth table
        pCut->uTruth = 0xFFFF & Dar_CutTruth( pCut, pCut0, pCut1, Aig_IsComplement(pFanin0), Aig_IsComplement(pFanin1) );

        // minimize support of the cut
        if ( !fSkipTtMin && Dar_CutSuppMinimize( pCut ) )
        {
            int RetValue = Dar_CutFilter( pObj, pCut );
            assert( !RetValue );
        }

        // assign the value of the cut
        pCut->Value = Dar_CutFindValue( p, pCut );
        // if the cut contains removed node, do not use it
        if ( pCut->Value == 0 )
        {
            p->nCutsSkipped++;
            pCut->fUsed = 0;
        }
        else if ( pCut->nLeaves < 2 )
            return pCutSet;
    }
    // count the number of nontrivial cuts cuts
    Dar_ObjForEachCut( pObj, pCut, i )
        p->nCutsUsed += pCut->fUsed;
    // discount trivial cut
    p->nCutsUsed--;
    return pCutSet;
}

Dar_Cut_t* Dar_ObjComputeCuts_rec	(	Dar_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 818 of file darCut.c.

{
    if ( Dar_ObjCuts(pObj) )
        return Dar_ObjCuts(pObj);
    if ( Aig_ObjIsCi(pObj) )
        return Dar_ObjPrepareCuts( p, pObj );
    if ( Aig_ObjIsBuf(pObj) )
        return Dar_ObjComputeCuts_rec( p, Aig_ObjFanin0(pObj) );
    Dar_ObjComputeCuts_rec( p, Aig_ObjFanin0(pObj) );
    Dar_ObjComputeCuts_rec( p, Aig_ObjFanin1(pObj) );
    return Dar_ObjComputeCuts( p, pObj, 0 );
}

void Dar_ObjCutPrint	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Prints one cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file darCut.c.

{
    Dar_Cut_t * pCut;
    int i;
    printf( "Cuts for node %d:\n", pObj->Id );
    Dar_ObjForEachCut( pObj, pCut, i )
        Dar_CutPrint( pCut );
//    printf( "\n" );
}

static Dar_Cut_t* Dar_ObjCuts ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 107 of file darInt.h.

{ return (Dar_Cut_t *)pObj->pData;    }

Dar_Cut_t* Dar_ObjPrepareCuts	(	Dar_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 668 of file darCut.c.

{
    Dar_Cut_t * pCutSet, * pCut;
    int i;
    assert( Dar_ObjCuts(pObj) == NULL );
    pObj->nCuts = p->pPars->nCutsMax;
    // create the cutset of the node
    pCutSet = (Dar_Cut_t *)Aig_MmFixedEntryFetch( p->pMemCuts );
    memset( pCutSet, 0, p->pPars->nCutsMax * sizeof(Dar_Cut_t) );
    Dar_ObjSetCuts( pObj, pCutSet );
    Dar_ObjForEachCutAll( pObj, pCut, i )
        pCut->fUsed = 0;
    Vec_PtrPush( p->vCutNodes, pObj );
    // add unit cut if needed
    pCut = pCutSet;
    pCut->fUsed = 1;
    if ( Aig_ObjIsConst1(pObj) )
    {
        pCut->nLeaves = 0;
        pCut->uSign = 0;
        pCut->uTruth = 0xFFFF;
    }
    else
    {
        pCut->nLeaves = 1;
        pCut->pLeaves[0] = pObj->Id;
        pCut->uSign = Aig_ObjCutSign( pObj->Id );
        pCut->uTruth = 0xAAAA;
    }
    pCut->Value = Dar_CutFindValue( p, pCut );
    if ( p->nCutMemUsed < Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) )
        p->nCutMemUsed = Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20);
    return pCutSet;
}

static void Dar_ObjSetCuts ( Aig_Obj_t *  pObj, Dar_Cut_t *  pCuts  )

inlinestatic

Definition at line 108 of file darInt.h.

{ assert( !Aig_ObjIsNone(pObj) ); pObj->pData = pCuts;   }

char** Dar_Permutations

(

int

n

)

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

Synopsis [Computes the set of all permutations.]

Description [The number of permutations in the array is n!. The number of entries in each permutation is n. Therefore, the resulting array is a two-dimentional array of the size: n! x n. To free the resulting array, call ABC_FREE() on the pointer returned by this procedure.]

SideEffects []

SeeAlso []

Definition at line 144 of file darPrec.c.

{
    char Array[50];
    char ** pRes;
    int nFact, i;
    // allocate memory
    nFact = Dar_Factorial( n );
    pRes  = Dar_ArrayAlloc( nFact, n, sizeof(char) );
    // fill in the permutations
    for ( i = 0; i < n; i++ )
        Array[i] = i;
    Dar_Permutations_rec( pRes, nFact, n, Array );
    // print the permutations
/*
    {
    int i, k;
    for ( i = 0; i < nFact; i++ )
    {
        printf( "{" );
        for ( k = 0; k < n; k++ )
            printf( " %d", pRes[i][k] );
        printf( " }\n" );
    }
    }
*/
    return pRes;
}

void Dar_Truth4VarNPN	(	unsigned short **	puCanons,
		char **	puPhases,
		char **	puPerms,
		unsigned char **	puMap
	)

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

Synopsis [Computes NPN canonical forms for 4-variable functions.]

Description []

SideEffects []

SeeAlso []

Definition at line 293 of file darPrec.c.

{
    unsigned short * uCanons;
    unsigned char * uMap;
    unsigned uTruth, uPhase, uPerm;
    char ** pPerms4, * uPhases, * uPerms;
    int nFuncs, nClasses;
    int i, k;

    nFuncs  = (1 << 16);
    uCanons = ABC_CALLOC( unsigned short, nFuncs );
    uPhases = ABC_CALLOC( char, nFuncs );
    uPerms  = ABC_CALLOC( char, nFuncs );
    uMap    = ABC_CALLOC( unsigned char, nFuncs );
    pPerms4 = Dar_Permutations( 4 );

    nClasses = 1;
    nFuncs = (1 << 15);
    for ( uTruth = 1; uTruth < (unsigned)nFuncs; uTruth++ )
    {
        // skip already assigned
        if ( uCanons[uTruth] )
        {
            assert( uTruth > uCanons[uTruth] );
            uMap[~uTruth & 0xFFFF] = uMap[uTruth] = uMap[uCanons[uTruth]];
            continue;
        }
        uMap[uTruth] = nClasses++;
        for ( i = 0; i < 16; i++ )
        {
            uPhase = Dar_TruthPolarize( uTruth, i, 4 );
            for ( k = 0; k < 24; k++ )
            {
                uPerm = Dar_TruthPermute( uPhase, pPerms4[k], 4, 0 );
                if ( uCanons[uPerm] == 0 )
                {
                    uCanons[uPerm] = uTruth;
                    uPhases[uPerm] = i;
                    uPerms[uPerm]  = k;
                    uMap[uPerm]    = uMap[uTruth];

                    uPerm = ~uPerm & 0xFFFF;
                    uCanons[uPerm] = uTruth;
                    uPhases[uPerm] = i | 16;
                    uPerms[uPerm]  = k;
                    uMap[uPerm]    = uMap[uTruth];
                }
                else
                    assert( uCanons[uPerm] == uTruth );
            }
            uPhase = Dar_TruthPolarize( ~uTruth & 0xFFFF, i, 4 ); 
            for ( k = 0; k < 24; k++ )
            {
                uPerm = Dar_TruthPermute( uPhase, pPerms4[k], 4, 0 );
                if ( uCanons[uPerm] == 0 )
                {
                    uCanons[uPerm] = uTruth;
                    uPhases[uPerm] = i;
                    uPerms[uPerm]  = k;
                    uMap[uPerm]    = uMap[uTruth];

                    uPerm = ~uPerm & 0xFFFF;
                    uCanons[uPerm] = uTruth;
                    uPhases[uPerm] = i | 16;
                    uPerms[uPerm]  = k;
                    uMap[uPerm]    = uMap[uTruth];
                }
                else
                    assert( uCanons[uPerm] == uTruth );
            }
        }
    }
    for ( uTruth = 1; uTruth < 0xffff; uTruth++ )
        assert( uMap[uTruth] != 0 );
    uPhases[(1<<16)-1] = 16;
    assert( nClasses == 222 );
    ABC_FREE( pPerms4 );
    if ( puCanons ) 
        *puCanons = uCanons;
    else
        ABC_FREE( uCanons );
    if ( puPhases ) 
        *puPhases = uPhases;
    else
        ABC_FREE( uPhases );
    if ( puPerms ) 
        *puPerms = uPerms;
    else
        ABC_FREE( uPerms );
    if ( puMap ) 
        *puMap = uMap;
    else
        ABC_FREE( uMap );
}