src/aig/dar/darInt.h File Reference

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

Include dependency graph for darInt.h:

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

Go to the source code of this file.

Data Structures
struct	Dar_Cut_t_
struct	Dar_Man_t_
Defines
#define	Dar_ObjForEachCutAll(pObj, pCut, i)   for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ )
#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 struct Dar_Man_t_	Dar_Man_t
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_ManCutsStart (Dar_Man_t *p)
void	Dar_ManCutsFree (Dar_Man_t *p)
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)
Vec_Int_t *	Dar_LibReadNodes ()
Vec_Int_t *	Dar_LibReadOuts ()
Vec_Int_t *	Dar_LibReadPrios ()
void	Dar_LibStart ()
void	Dar_LibStop ()
void	Dar_LibPrepare (int nSubgraphs)
void	Dar_LibReturnCanonicals (unsigned *pCanons)
void	Dar_LibEval (Dar_Man_t *p, Aig_Obj_t *pRoot, Dar_Cut_t *pCut, int Required)
Aig_Obj_t *	Dar_LibBuildBest (Dar_Man_t *p)
Dar_Man_t *	Dar_ManStart (Aig_Man_t *pAig, Dar_RwrPar_t *pPars)
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)

---

Define 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 123 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 120 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 118 of file darInt.h.

---

Typedef Documentation

typedef struct Dar_Cut_t_ Dar_Cut_t

Definition at line 52 of file darInt.h.

typedef struct Dar_Man_t_ Dar_Man_t

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

] INCLUDES /// 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 966 of file darLib.c.

{
    int i, Counter = 4;
    for ( i = 0; i < Vec_PtrSize(p->vLeavesBest); i++ )
        s_DarLib->pDatas[i].pFunc = 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
	)

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

Synopsis [Evaluates one cut.]

Description [Returns the best gain.]

SideEffects []

SeeAlso []

Definition at line 859 of file darLib.c.

{
    int fTraining = 0;
    Dar_LibObj_t * pObj;
    int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained, clk;
    clk = 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 );
    // evaluate the cut
    Class = s_DarLib->pMap[pCut->uTruth];
    Dar_LibEvalAssignNums( p, Class );
    // 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 );
        nNodesGained = nNodesSaved - nNodesAdded;
        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 );
    }
clk = clock() - clk;
p->ClassTimes[Class] += clk;
p->timeEval += clk;
}

void Dar_LibPrepare

(

int

nSubgraphs

)

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

Synopsis [Starts the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 453 of file darLib.c.

{
    Dar_Lib_t * p = s_DarLib;
    int i, k, nNodes0Total;
    if ( p->nSubgraphs == nSubgraphs )
        return;

    // favor special classes:
    //  1 : F = (!d*!c*!b*!a)
    //  4 : F = (!d*!c*!(b*a))
    // 12 : F = (!d*!(c*!(!b*!a)))
    // 20 : F = (!d*!(c*b*a))

    // set the subgraph counters 
    p->nSubgr0Total = 0;
    for ( i = 0; i < 222; i++ )
    {
//        if ( i == 1 || i == 4 || i == 12 || i == 20 ) // special classes 
        if ( i == 1 ) // special classes 
            p->nSubgr0[i] = p->nSubgr[i];
        else
            p->nSubgr0[i] = AIG_MIN( p->nSubgr[i], nSubgraphs );
        p->nSubgr0Total += p->nSubgr0[i];
        for ( k = 0; k < p->nSubgr0[i]; k++ )
            p->pSubgr0[i][k] = p->pSubgr[i][ p->pPrios[i][k] ];
    }

    // count the number of nodes
    // clean node counters
    for ( i = 0; i < 222; i++ )
        p->nNodes0[i] = 0;
    // create traversal IDs
    for ( i = 0; i < p->iObj; i++ )
        Dar_LibObj(p, i)->Num = 0xff;
    // count nodes in each class
    // count the total number of nodes and the largest class
    p->nNodes0Total = 0;
    p->nNodes0Max = 0;
    for ( i = 0; i < 222; i++ )
    {
        for ( k = 0; k < p->nSubgr0[i]; k++ )
            Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 0 );
        p->nNodes0Total += p->nNodes0[i];
        p->nNodes0Max = AIG_MAX( p->nNodes0Max, p->nNodes0[i] );
    }

    // clean node counters
    for ( i = 0; i < 222; i++ )
        p->nNodes0[i] = 0;
    // create traversal IDs
    for ( i = 0; i < p->iObj; i++ )
        Dar_LibObj(p, i)->Num = 0xff;
    // add the nodes to storage
    nNodes0Total = 0;
    for ( i = 0; i < 222; i++ )
    {
        for ( k = 0; k < p->nSubgr0[i]; k++ )
            Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 1 );
         nNodes0Total += p->nNodes0[i];
    }
    assert( nNodes0Total == p->nNodes0Total );
     // prepare the number of the PI nodes
    for ( i = 0; i < 4; i++ )
        Dar_LibObj(p, i)->Num = i;

    // realloc the datas
    Dar_LibCreateData( p, p->nNodes0Max + 32 ); 
    // allocated more because Dar_LibBuildBest() sometimes requires more entries
}

Vec_Int_t* Dar_LibReadNodes

(

)

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

Synopsis [Reads library from array.]

Description []

SideEffects []

SeeAlso []

Definition at line 11093 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 11114 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 11135 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 186 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

(

)

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

Synopsis [Starts the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 568 of file darLib.c.

{
//    int clk = clock();
    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 );
//    PRT( "Time", clock() - clk );
}

void Dar_LibStop

(

)

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

Synopsis [Stops the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 588 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 519 of file darCut.c.

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

void Dar_ManCutsStart

(

Dar_Man_t *

p

)

FUNCTION DECLARATIONS ///

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 581 of file darCut.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManCleanData( p->pAig );
    Aig_MmFixedRestart( p->pMemCuts );
    Dar_ObjPrepareCuts( p, Aig_ManConst1(p->pAig) );
    Aig_ManForEachPi( p->pAig, pObj, i )
        Dar_ObjPrepareCuts( p, pObj );
}

void Dar_ManPrintStats

(

Dar_Man_t *

p

)

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

Synopsis [Stops the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 90 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) );
    PRT( "Cuts  ", p->timeCuts );
    PRT( "Eval  ", p->timeEval );
    PRT( "Other ", p->timeOther );
    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 );
//        PRTP( "T", p->ClassTimes[i], p->timeEval );
        printf( "\n" );
    }
}

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

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

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

Synopsis [Starts the rewriting manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file darMan.c.

{
    Dar_Man_t * p;
    // start the manager
    p = ALLOC( Dar_Man_t, 1 );
    memset( p, 0, sizeof(Dar_Man_t) );
    p->pPars = pPars;
    p->pAig  = pAig;
    // prepare the internal memory manager
    p->pMemCuts = Aig_MmFixedStart( p->pPars->nCutsMax * sizeof(Dar_Cut_t), 1024 );
    // other data
    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 68 of file darMan.c.

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

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 603 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, RetValue;

    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 ( Dar_CutSuppMinimize( pCut ) )
        {
            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 683 of file darCut.c.

{
    if ( Dar_ObjCuts(pObj) )
        return Dar_ObjCuts(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 );
}

static Dar_Cut_t* Dar_ObjCuts

(

Aig_Obj_t *

pObj

)

[inline, static]

Definition at line 106 of file darInt.h.

{ return pObj->pData;    }

static void Dar_ObjSetCuts	(	Aig_Obj_t *	pObj,
		Dar_Cut_t *	pCuts
	)			[inline, static]

Definition at line 107 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 free() on the pointer returned by this procedure.]

SideEffects []

SeeAlso []

Definition at line 141 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 290 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 = ALLOC( unsigned short, nFuncs );
    uPhases = ALLOC( char, nFuncs );
    uPerms  = ALLOC( char, nFuncs );
    uMap    = ALLOC( unsigned char, nFuncs );
    memset( uCanons, 0, sizeof(unsigned short) * nFuncs );
    memset( uPhases, 0, sizeof(char) * nFuncs );
    memset( uPerms,  0, sizeof(char) * nFuncs );
    memset( uMap,    0, sizeof(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;

                    uPerm = ~uPerm & 0xFFFF;
                    uCanons[uPerm] = uTruth;
                    uPhases[uPerm] = i | 16;
                    uPerms[uPerm]  = k;
                }
                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;

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