extraUtilPerm.c File Reference

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

Go to the source code of this file.

Data Structures
struct	Abc_ZddObj_
struct	Abc_ZddEnt_
struct	Abc_ZddMan_

Typedefs
typedef struct Abc_ZddObj_	Abc_ZddObj
typedef struct Abc_ZddEnt_	Abc_ZddEnt
typedef struct Abc_ZddMan_	Abc_ZddMan

Enumerations
enum	Abc_ZddOper {   ABC_ZDD_OPER_NONE, ABC_ZDD_OPER_DIFF, ABC_ZDD_OPER_UNION, ABC_ZDD_OPER_MIN_UNION,   ABC_ZDD_OPER_INTER, ABC_ZDD_OPER_PERM, ABC_ZDD_OPER_PERM_PROD, ABC_ZDD_OPER_COF0,   ABC_ZDD_OPER_COF1, ABC_ZDD_OPER_THRESH, ABC_ZDD_OPER_DOT_PROD, ABC_ZDD_OPER_DOT_PROD_6,   ABC_ZDD_OPER_INSERT, ABC_ZDD_OPER_PATHS, ABC_ZDD_OPER_NODES, ABC_ZDD_OPER_ITE }
	DECLARATIONS ///. More...

Functions
static int	Abc_ZddIthVar (int i)
static unsigned	Abc_ZddHash (int Arg0, int Arg1, int Arg2)
static Abc_ZddObj *	Abc_ZddNode (Abc_ZddMan *p, int i)
static int	Abc_ZddObjId (Abc_ZddMan *p, Abc_ZddObj *pObj)
static int	Abc_ZddObjVar (Abc_ZddMan *p, int i)
static void	Abc_ZddSetVarIJ (Abc_ZddMan *p, int i, int j, int v)
static int	Abc_ZddVarIJ (Abc_ZddMan *p, int i, int j)
static int	Abc_ZddVarsClash (Abc_ZddMan *p, int v0, int v1)
static int	Abc_ZddCacheLookup (Abc_ZddMan *p, int Arg0, int Arg1, int Arg2)
	FUNCTION DEFINITIONS ///. More...
static int	Abc_ZddCacheInsert (Abc_ZddMan *p, int Arg0, int Arg1, int Arg2, int Res)
static int	Abc_ZddUniqueLookup (Abc_ZddMan *p, int Var, int True, int False)
static int	Abc_ZddUniqueCreate (Abc_ZddMan *p, int Var, int True, int False)
int	Abc_ZddBuildSet (Abc_ZddMan *p, int *pSet, int Size)
Abc_ZddMan *	Abc_ZddManAlloc (int nVars, int nObjs)
void	Abc_ZddManCreatePerms (Abc_ZddMan *p, int nPermSize)
void	Abc_ZddManFree (Abc_ZddMan *p)
int	Abc_ZddDiff (Abc_ZddMan *p, int a, int b)
int	Abc_ZddUnion (Abc_ZddMan *p, int a, int b)
int	Abc_ZddMinUnion (Abc_ZddMan *p, int a, int b)
int	Abc_ZddIntersect (Abc_ZddMan *p, int a, int b)
int	Abc_ZddCof0 (Abc_ZddMan *p, int a, int Var)
int	Abc_ZddCof1 (Abc_ZddMan *p, int a, int Var)
int	Abc_ZddCountPaths (Abc_ZddMan *p, int a)
int	Abc_ZddCount_rec (Abc_ZddMan *p, int i)
void	Abc_ZddUnmark_rec (Abc_ZddMan *p, int i)
int	Abc_ZddCountNodes (Abc_ZddMan *p, int i)
int	Abc_ZddCountNodesArray (Abc_ZddMan *p, Vec_Int_t *vNodes)
int	Abc_ZddThresh (Abc_ZddMan *p, int a, int b)
int	Abc_ZddDotProduct (Abc_ZddMan *p, int a, int b)
int	Abc_ZddDotMinProduct6 (Abc_ZddMan *p, int a, int b)
int	Abc_ZddPerm (Abc_ZddMan *p, int a, int Var)
int	Abc_ZddPermProduct (Abc_ZddMan *p, int a, int b)
void	Abc_ZddPermPrint (int *pPerm, int Size)
void	Abc_ZddCombPrint (int *pComb, int nTrans)
int	Abc_ZddPerm2Comb (int *pPerm, int Size, int *pComb)
void	Abc_ZddComb2Perm (int *pComb, int nTrans, int *pPerm, int Size)
void	Abc_ZddPermCombTest ()
void	Abc_ZddPrint_rec (Abc_ZddMan *p, int a, int *pPath, int Size)
void	Abc_ZddPrint (Abc_ZddMan *p, int a)
void	Abc_ZddPrintTest (Abc_ZddMan *p)
void	Abc_ZddGiaTest (Gia_Man_t *pGia)
void	Abc_ZddPermTestInt (Abc_ZddMan *p)
void	Abc_ZddPermTest ()
void	Abc_EnumerateCubeStatesZdd ()

Typedef Documentation

typedef struct Abc_ZddEnt_ Abc_ZddEnt

Definition at line 63 of file extraUtilPerm.c.

typedef struct Abc_ZddMan_ Abc_ZddMan

Definition at line 72 of file extraUtilPerm.c.

typedef struct Abc_ZddObj_ Abc_ZddObj

Definition at line 54 of file extraUtilPerm.c.

Enumeration Type Documentation

enum Abc_ZddOper

DECLARATIONS ///.

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

FileName [extraUtilPerm.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [extra]

Synopsis [Permutation computation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

extraUtilPerm.c,v 1.0 2003/02/01 00:00:00 alanmi Exp

]

Enumerator
ABC_ZDD_OPER_NONE
ABC_ZDD_OPER_DIFF
ABC_ZDD_OPER_UNION
ABC_ZDD_OPER_MIN_UNION
ABC_ZDD_OPER_INTER
ABC_ZDD_OPER_PERM
ABC_ZDD_OPER_PERM_PROD
ABC_ZDD_OPER_COF0
ABC_ZDD_OPER_COF1
ABC_ZDD_OPER_THRESH
ABC_ZDD_OPER_DOT_PROD
ABC_ZDD_OPER_DOT_PROD_6
ABC_ZDD_OPER_INSERT
ABC_ZDD_OPER_PATHS
ABC_ZDD_OPER_NODES
ABC_ZDD_OPER_ITE

Definition at line 34 of file extraUtilPerm.c.

{
    ABC_ZDD_OPER_NONE,
    ABC_ZDD_OPER_DIFF,
    ABC_ZDD_OPER_UNION,
    ABC_ZDD_OPER_MIN_UNION,
    ABC_ZDD_OPER_INTER,
    ABC_ZDD_OPER_PERM,
    ABC_ZDD_OPER_PERM_PROD,
    ABC_ZDD_OPER_COF0,
    ABC_ZDD_OPER_COF1,
    ABC_ZDD_OPER_THRESH,
    ABC_ZDD_OPER_DOT_PROD,
    ABC_ZDD_OPER_DOT_PROD_6,
    ABC_ZDD_OPER_INSERT,
    ABC_ZDD_OPER_PATHS,
    ABC_ZDD_OPER_NODES,
    ABC_ZDD_OPER_ITE
} Abc_ZddOper;

Function Documentation

void Abc_EnumerateCubeStatesZdd

(

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 845 of file extraUtilPerm.c.

{
    int pXYZ[3][9][2] = {
        { {3, 5}, {3,17}, {3,15}, {1, 6}, {1,16}, {1,14}, {2, 4}, {2,18}, {2,13} },
        { {2,14}, {2,24}, {2,12}, {3,13}, {3,23}, {3,10}, {1,15}, {1,22}, {1,11} },
        { {1,10}, {1, 7}, {1, 4}, {3,12}, {3, 9}, {3, 6}, {2,11}, {2, 8}, {2, 5} }  };
#ifdef WIN32
    int LogObj = 24;
#else
    int LogObj = 27;
#endif
    Abc_ZddMan * p;
    int i, k, pComb[9], pPerm[24], nSize;
    int ZddTurn1, ZddTurn2, ZddTurn3, ZddTurns, ZddAll;
    abctime clk = Abc_Clock();
    printf( "Enumerating states of 2x2x2 cube.\n" );
    p = Abc_ZddManAlloc( 24 * 23 / 2, 1 << LogObj ); // finished with 2^27 (4 GB)
    Abc_ZddManCreatePerms( p, 24 );
    // init state
    printf( "Iter %2d -> %8d  Nodes = %7d  Used = %10d  ", 0, 1, 0, 2 );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    // first 9 states
    ZddTurns = 1;
    for ( i = 0; i < 3; i++ )
    {
        for ( k = 0; k < 24; k++ )
            pPerm[k] = k;
        for ( k = 0; k < 9; k++ )
            ABC_SWAP( int, pPerm[pXYZ[i][k][0]-1], pPerm[pXYZ[i][k][1]-1] );
        nSize = Abc_ZddPerm2Comb( pPerm, 24, pComb );
        assert( nSize == 9 );
        for ( k = 0; k < 9; k++ )
            pComb[k] = Abc_ZddVarIJ( p, pComb[k] >> 16, pComb[k] & 0xffff );
        // add first turn
        ZddTurn1  = Abc_ZddBuildSet( p, pComb, 9 );
        ZddTurns = Abc_ZddUnion( p, ZddTurns, ZddTurn1 );
        //Abc_ZddPrint( p, ZddTurn1 );
        // add second turn
        ZddTurn2 = Abc_ZddPermProduct( p, ZddTurn1, ZddTurn1 );
        ZddTurns = Abc_ZddUnion( p, ZddTurns, ZddTurn2 );
        //Abc_ZddPrint( p, ZddTurn2 );
        // add third turn
        ZddTurn3 = Abc_ZddPermProduct( p, ZddTurn2, ZddTurn1 );
        ZddTurns = Abc_ZddUnion( p, ZddTurns, ZddTurn3 );
        //Abc_ZddPrint( p, ZddTurn3 );
        //printf( "\n" );
    }
    //Abc_ZddPrint( p, ZddTurns );
    printf( "Iter %2d -> %8d  Nodes = %7d  Used = %10d  ", 1, Abc_ZddCountPaths(p, ZddTurns), Abc_ZddCountNodes(p, ZddTurns), p->nObjs );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    // other states
    ZddAll = ZddTurns;
    for ( i = 2; i <= 100; i++ )
    {
        int ZddAllPrev = ZddAll;
        ZddAll = Abc_ZddPermProduct( p, ZddAll, ZddTurns );
        printf( "Iter %2d -> %8d  Nodes = %7d  Used = %10d  ", i, Abc_ZddCountPaths(p, ZddAll), Abc_ZddCountNodes(p, ZddAll), p->nObjs );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
        if ( ZddAllPrev == ZddAll )
            break;
    }
    Abc_ZddManFree( p );
}

int Abc_ZddBuildSet	(	Abc_ZddMan *	p,
		int *	pSet,
		int	Size
	)

Definition at line 164 of file extraUtilPerm.c.

{
    int i, Res = 1;
    Vec_IntSelectSort( pSet, Size );
    for ( i = Size - 1; i >= 0; i-- )
        Res = Abc_ZddUniqueCreate( p, pSet[i], Res, 0 );
    return Res;
}

static int Abc_ZddCacheInsert ( Abc_ZddMan *  p, int  Arg0, int  Arg1, int  Arg2, int  Res  )

inlinestatic

Definition at line 125 of file extraUtilPerm.c.

{
    Abc_ZddEnt * pEnt = p->pCache + (Abc_ZddHash(Arg0, Arg1, Arg2) & p->nCacheMask);
    pEnt->Arg0 = Arg0;  pEnt->Arg1 = Arg1;  pEnt->Arg2 = Arg2;  pEnt->Res = Res;
    p->nCacheMisses++;
    assert( Res >= 0 );
    return Res;
}

static int Abc_ZddCacheLookup ( Abc_ZddMan *  p, int  Arg0, int  Arg1, int  Arg2  )

inlinestatic

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 119 of file extraUtilPerm.c.

{
    Abc_ZddEnt * pEnt = p->pCache + (Abc_ZddHash(Arg0, Arg1, Arg2) & p->nCacheMask);
    p->nCacheLookups++;
    return (pEnt->Arg0 == Arg0 && pEnt->Arg1 == Arg1 && pEnt->Arg2 == Arg2) ? pEnt->Res : -1;
}

int Abc_ZddCof0	(	Abc_ZddMan *	p,
		int	a,
		int	Var
	)

Definition at line 348 of file extraUtilPerm.c.

{
    Abc_ZddObj * A; 
    int r0, r1, r;
    if ( a < 2 ) return a;
    A = Abc_ZddNode( p, a );
    if ( (int)A->Var > Var )
        return a;
    if ( (r = Abc_ZddCacheLookup(p, a, Var, ABC_ZDD_OPER_COF0)) >= 0 )
        return r;
    if ( (int)A->Var < Var )
        r0 = Abc_ZddCof0( p, A->False, Var ),
        r1 = Abc_ZddCof0( p, A->True, Var ),
        r  = Abc_ZddUniqueCreate( p, A->Var, r1, r0 );
    else
        r = Abc_ZddCof0( p, A->False, Var );
    return Abc_ZddCacheInsert( p, a, Var, ABC_ZDD_OPER_COF0, r );
}

int Abc_ZddCof1	(	Abc_ZddMan *	p,
		int	a,
		int	Var
	)

Definition at line 366 of file extraUtilPerm.c.

{
    Abc_ZddObj * A; 
    int r0, r1, r;
    if ( a < 2 ) return a;
    A = Abc_ZddNode( p, a );
    if ( (int)A->Var > Var )
        return a;
    if ( (r = Abc_ZddCacheLookup(p, a, Var, ABC_ZDD_OPER_COF1)) >= 0 )
        return r;
    if ( (int)A->Var < Var )
        r0 = Abc_ZddCof1( p, A->False, Var ),
        r1 = Abc_ZddCof1( p, A->True, Var );
    else
        r0 = 0,
        r1 = Abc_ZddCof1( p, A->True, Var );
    r = Abc_ZddUniqueCreate( p, A->Var, r1, r0 );
    return Abc_ZddCacheInsert( p, a, Var, ABC_ZDD_OPER_COF1, r );
}

void Abc_ZddComb2Perm	(	int *	pComb,
		int	nTrans,
		int *	pPerm,
		int	Size
	)

Definition at line 651 of file extraUtilPerm.c.

{
    int v;
    for ( v = 0; v < Size; v++ )
        pPerm[v] = v;
    for ( v = nTrans-1; v >= 0; v-- )
        ABC_SWAP( int, pPerm[pComb[v] >> 16], pPerm[pComb[v] & 0xffff] );
}

void Abc_ZddCombPrint	(	int *	pComb,
		int	nTrans
	)

Definition at line 627 of file extraUtilPerm.c.

{
    int i;
    if ( nTrans == 0 )
        printf( "Empty set" );
    for ( i = 0; i < nTrans; i++ )
        printf( "(%d %d)", pComb[i] >> 16, pComb[i] & 0xffff );
    printf( "\n" );
}

int Abc_ZddCount_rec	(	Abc_ZddMan *	p,
		int	i
	)

Definition at line 409 of file extraUtilPerm.c.

{
    Abc_ZddObj * A;
    if ( i < 2 )
        return 0;
    A = Abc_ZddNode( p, i );
    if ( A->Mark )
        return 0;
    A->Mark = 1;
    return 1 + Abc_ZddCount_rec(p, A->False) + Abc_ZddCount_rec(p, A->True);
}

int Abc_ZddCountNodes	(	Abc_ZddMan *	p,
		int	i
	)

Definition at line 432 of file extraUtilPerm.c.

{
    int Count = Abc_ZddCount_rec( p, i );
    Abc_ZddUnmark_rec( p, i );
    return Count;
}

int Abc_ZddCountNodesArray	(	Abc_ZddMan *	p,
		Vec_Int_t *	vNodes
	)

Definition at line 438 of file extraUtilPerm.c.

{
    int i, Id, Count = 0;
    Vec_IntForEachEntry( vNodes, Id, i )
        Count += Abc_ZddCount_rec( p, Id );
    Vec_IntForEachEntry( vNodes, Id, i )
        Abc_ZddUnmark_rec( p, Id );
    return Count;
}

int Abc_ZddCountPaths	(	Abc_ZddMan *	p,
		int	a
	)

Definition at line 385 of file extraUtilPerm.c.

{
    Abc_ZddObj * A;  
    int r;
    if ( a < 2 ) return a;
    if ( (r = Abc_ZddCacheLookup(p, a, 0, ABC_ZDD_OPER_PATHS)) >= 0 )
        return r;
    A = Abc_ZddNode( p, a );
    r = Abc_ZddCountPaths( p, A->False ) + Abc_ZddCountPaths( p, A->True );
    return Abc_ZddCacheInsert( p, a, 0, ABC_ZDD_OPER_PATHS, r );
}

int Abc_ZddDiff	(	Abc_ZddMan *	p,
		int	a,
		int	b
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file extraUtilPerm.c.

{
    Abc_ZddObj * A, * B; 
    int r0, r1, r;
    if ( a == 0 ) return 0;
    if ( b == 0 ) return a;
    if ( a == b ) return 0;
    if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_DIFF)) >= 0 )
        return r;
    A = Abc_ZddNode( p, a );
    B = Abc_ZddNode( p, b );
    if ( A->Var < B->Var )
        r0 = Abc_ZddDiff( p, A->False, b ), 
        r = Abc_ZddUniqueCreate( p, A->Var, A->True, r0 );
    else if ( A->Var > B->Var )
        r = Abc_ZddDiff( p, a, B->False );
    else
        r0 = Abc_ZddDiff( p, A->False, B->False ), 
        r1 = Abc_ZddDiff( p, A->True, B->True ),
        r = Abc_ZddUniqueCreate( p, A->Var, A->True, r0 );
    return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_DIFF, r );
}

int Abc_ZddDotMinProduct6	(	Abc_ZddMan *	p,
		int	a,
		int	b
	)

Definition at line 501 of file extraUtilPerm.c.

{
    Abc_ZddObj * A, * B; 
    int r0, r1, b2, t1, t2, r;
    if ( a == 0 ) return 0;
    if ( b == 0 ) return 0;
    if ( a == 1 ) return b;
    if ( b == 1 ) return a;
    if ( a > b )  return Abc_ZddDotMinProduct6( p, b, a );
    if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_DOT_PROD_6)) >= 0 )
        return r;
    A = Abc_ZddNode( p, a );
    B = Abc_ZddNode( p, b );
    if ( A->Var < B->Var )
        r0 = Abc_ZddDotMinProduct6( p, A->False, b ), 
        r1 = Abc_ZddDotMinProduct6( p, A->True, b );
    else if ( A->Var > B->Var )
        r0 = Abc_ZddDotMinProduct6( p, a, B->False ), 
        r1 = Abc_ZddDotMinProduct6( p, a, B->True ); 
    else
        r0 = Abc_ZddDotMinProduct6( p, A->False, B->False ),
        b2 = Abc_ZddMinUnion( p, B->False, B->True ), 
        t1 = Abc_ZddDotMinProduct6( p, A->True, b2 ), 
        t2 = Abc_ZddDotMinProduct6( p, A->False, B->True ), 
        r1 = Abc_ZddMinUnion( p, t1, t2 );
    r1 = Abc_ZddThresh( p, r1, 5 ),
    r1 = Abc_ZddDiff( p, r1, r0 ); 
    r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 );
    return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_DOT_PROD_6, r );
}

int Abc_ZddDotProduct	(	Abc_ZddMan *	p,
		int	a,
		int	b
	)

Definition at line 473 of file extraUtilPerm.c.

{
    Abc_ZddObj * A, * B; 
    int r0, r1, b2, t1, t2, r;
    if ( a == 0 ) return 0;
    if ( b == 0 ) return 0;
    if ( a == 1 ) return b;
    if ( b == 1 ) return a;
    if ( a > b )  return Abc_ZddDotProduct( p, b, a );
    if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_DOT_PROD)) >= 0 )
        return r;
    A = Abc_ZddNode( p, a );
    B = Abc_ZddNode( p, b );
    if ( A->Var < B->Var )
        r0 = Abc_ZddDotProduct( p, A->False, b ), 
        r1 = Abc_ZddDotProduct( p, A->True, b );
    else if ( A->Var > B->Var )
        r0 = Abc_ZddDotProduct( p, a, B->False ), 
        r1 = Abc_ZddDotProduct( p, a, B->True ); 
    else
        r0 = Abc_ZddDotProduct( p, A->False, B->False ),
        b2 = Abc_ZddUnion( p, B->False, B->True ), 
        t1 = Abc_ZddDotProduct( p, A->True, b2 ), 
        t2 = Abc_ZddDotProduct( p, A->False, B->True ), 
        r1 = Abc_ZddUnion( p, t1, t2 );
    r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 );
    return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_DOT_PROD, r );
}

void Abc_ZddGiaTest

(

Gia_Man_t *

pGia

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 743 of file extraUtilPerm.c.

{
    Abc_ZddMan * p;
    Gia_Obj_t * pObj;
    Vec_Int_t * vNodes;
    int i, r, Paths = 0;
    p = Abc_ZddManAlloc( Gia_ManObjNum(pGia), 1 << 24 ); // 576 MB  (36 B/node)
    Gia_ManFillValue( pGia );
    Gia_ManForEachCi( pGia, pObj, i )
        pObj->Value = Abc_ZddIthVar( Gia_ObjId(pGia, pObj) );
    vNodes = Vec_IntAlloc( Gia_ManAndNum(pGia) );
    Gia_ManForEachAnd( pGia, pObj, i )
    {
        r = Abc_ZddDotMinProduct6( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
        r = Abc_ZddUnion( p, r, Abc_ZddIthVar(i) );
        pObj->Value = r;
        Vec_IntPush( vNodes, r );
        // print
//        printf( "Node %d:\n", i );
//        Abc_ZddPrint( p, r );
//        printf( "Node %d   ZddNodes = %d\n", i, Abc_ZddCountNodes(p, r) );
    }
    Gia_ManForEachAnd( pGia, pObj, i )
        Paths += Abc_ZddCountPaths(p, pObj->Value);
    printf( "Paths = %d.  Shared nodes = %d.\n", Paths, Abc_ZddCountNodesArray(p, vNodes) );
    Vec_IntFree( vNodes );
    Abc_ZddManFree( p );
}

static unsigned Abc_ZddHash ( int  Arg0, int  Arg1, int  Arg2  )

inlinestatic

Definition at line 94 of file extraUtilPerm.c.

{ return 12582917 * Arg0 + 4256249 * Arg1 + 741457 * Arg2; }

int Abc_ZddIntersect	(	Abc_ZddMan *	p,
		int	a,
		int	b
	)

Definition at line 324 of file extraUtilPerm.c.

{
    Abc_ZddObj * A, * B; 
    int r0, r1, r;
    if ( a == 0 ) return 0;
    if ( b == 0 ) return 0;
    if ( a == b ) return a;
    if ( a > b )  return Abc_ZddIntersect( p, b, a );
    if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_INTER)) >= 0 )
        return r;
    A = Abc_ZddNode( p, a );
    B = Abc_ZddNode( p, b );
    if ( A->Var < B->Var )
        r0 = Abc_ZddIntersect( p, A->False, b ), 
        r1 = A->True;
    else if ( A->Var > B->Var )
        r0 = Abc_ZddIntersect( p, a, B->False ), 
        r1 = B->True;
    else
        r0 = Abc_ZddIntersect( p, A->False, B->False ), 
        r1 = Abc_ZddIntersect( p, A->True, B->True );
    r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 );
    return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_INTER, r );
}

static int Abc_ZddIthVar ( int  i )

inlinestatic

Definition at line 93 of file extraUtilPerm.c.

{ return i + 2;                                            }

Abc_ZddMan* Abc_ZddManAlloc	(	int	nVars,
		int	nObjs
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 184 of file extraUtilPerm.c.

{
    Abc_ZddMan * p; int i;
    p = ABC_CALLOC( Abc_ZddMan, 1 );
    p->nVars       = nVars;
    p->nObjsAlloc  = nObjs;
    p->nUniqueMask = (1 << Abc_Base2Log(nObjs)) - 1;
    p->nCacheMask  = (1 << Abc_Base2Log(nObjs)) - 1;
    p->pUnique     = ABC_CALLOC( int, p->nUniqueMask + 1 );
    p->pNexts      = ABC_CALLOC( int, p->nObjsAlloc );
    p->pCache      = ABC_CALLOC( Abc_ZddEnt, p->nCacheMask + 1 );
    p->pObjs       = ABC_CALLOC( Abc_ZddObj, p->nObjsAlloc );
    p->nObjs       = 2;
    memset( p->pObjs, 0xff, sizeof(Abc_ZddObj) * 2 );
    p->pObjs[0].Var = nVars;
    p->pObjs[1].Var = nVars;
    for ( i = 0; i < nVars; i++ )
        Abc_ZddUniqueCreate( p, i, 1, 0 );
    assert( p->nObjs == nVars + 2 );
    p->nMemory = sizeof(Abc_ZddMan)/4 + 
        p->nUniqueMask + 1 + p->nObjsAlloc + 
        (p->nCacheMask + 1) * sizeof(Abc_ZddEnt)/4 + 
        p->nObjsAlloc * sizeof(Abc_ZddObj)/4;
    return p;
}

void Abc_ZddManCreatePerms	(	Abc_ZddMan *	p,
		int	nPermSize
	)

Definition at line 209 of file extraUtilPerm.c.

{
    int i, j, v = 0;
    assert( 2 * p->nVars == nPermSize * (nPermSize - 1) );
    assert( p->nPermSize == 0 );
    p->nPermSize = nPermSize;
    p->pV2TI = ABC_FALLOC( int, p->nVars );
    p->pV2TJ = ABC_FALLOC( int, p->nVars );
    p->pT2V  = ABC_FALLOC( int, p->nPermSize * p->nPermSize );
    for ( i = 0; i < nPermSize; i++ )
        for ( j = i + 1; j < nPermSize; j++ )
        {
            p->pV2TI[v] = i;
            p->pV2TJ[v] = j;
            Abc_ZddSetVarIJ( p, i, j, v++ );
        }
    assert( v == p->nVars );
}

void Abc_ZddManFree

(

Abc_ZddMan *

p

)

Definition at line 227 of file extraUtilPerm.c.

{
    printf( "ZDD stats: Var = %d  Obj = %d  Alloc = %d  Hit = %d  Miss = %d  ", 
        p->nVars, p->nObjs, p->nObjsAlloc, p->nCacheLookups-p->nCacheMisses, p->nCacheMisses );
    printf( "Mem = %.2f MB\n", 4.0*(int)(p->nMemory/(1<<20)) );
    ABC_FREE( p->pT2V );
    ABC_FREE( p->pV2TI );
    ABC_FREE( p->pV2TJ );
    ABC_FREE( p->pUnique );
    ABC_FREE( p->pNexts );
    ABC_FREE( p->pCache );
    ABC_FREE( p->pObjs );
    ABC_FREE( p );
}

int Abc_ZddMinUnion	(	Abc_ZddMan *	p,
		int	a,
		int	b
	)

Definition at line 299 of file extraUtilPerm.c.

{
    Abc_ZddObj * A, * B; 
    int r0, r1, r;
    if ( a == 0 ) return b;
    if ( b == 0 ) return a;
    if ( a == b ) return a;
    if ( a > b )  return Abc_ZddMinUnion( p, b, a );
    if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_MIN_UNION)) >= 0 )
        return r;
    A = Abc_ZddNode( p, a );
    B = Abc_ZddNode( p, b );
    if ( A->Var < B->Var )
        r0 = Abc_ZddMinUnion( p, A->False, b ), 
        r1 = A->True;
    else if ( A->Var > B->Var )
        r0 = Abc_ZddMinUnion( p, a, B->False ), 
        r1 = B->True;
    else
        r0 = Abc_ZddMinUnion( p, A->False, B->False ), 
        r1 = Abc_ZddMinUnion( p, A->True, B->True );
    r1 = Abc_ZddDiff( p, r1, r0 ); // assume args are minimal
    r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 );
    return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_MIN_UNION, r );
}

static Abc_ZddObj* Abc_ZddNode ( Abc_ZddMan *  p, int  i  )

inlinestatic

Definition at line 96 of file extraUtilPerm.c.

{ return p->pObjs + i;                                     }

static int Abc_ZddObjId ( Abc_ZddMan *  p, Abc_ZddObj *  pObj  )

inlinestatic

Definition at line 97 of file extraUtilPerm.c.

{ return pObj - p->pObjs;                                  }

static int Abc_ZddObjVar ( Abc_ZddMan *  p, int  i  )

inlinestatic

Definition at line 98 of file extraUtilPerm.c.

{ return Abc_ZddNode(p, i)->Var;                           }

int Abc_ZddPerm	(	Abc_ZddMan *	p,
		int	a,
		int	Var
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 543 of file extraUtilPerm.c.

{
    Abc_ZddObj * A; 
    int r0, r1, r;
    assert( Var < p->nVars );
    if ( a == 0 )  return 0;
    if ( a == 1 )  return Abc_ZddIthVar(Var);
    if ( (r = Abc_ZddCacheLookup(p, a, Var, ABC_ZDD_OPER_PERM)) >= 0 )
        return r;
    A = Abc_ZddNode( p, a );
    if ( p->pV2TI[A->Var] > p->pV2TI[Var] ) // Ai > Bi
        r = Abc_ZddUniqueCreate( p, Var, a, 0 );
    else if ( (int)A->Var == Var ) // Ai == Bi && Aj == Bj
        r0 = Abc_ZddPerm( p, A->False, Var ), 
        r  = Abc_ZddUnion( p, r0, A->True );
    else 
    {
        int VarPerm, VarTop;
        int Ai = p->pV2TI[A->Var];
        int Aj = p->pV2TJ[A->Var];
        int Bi = p->pV2TI[Var];
        int Bj = p->pV2TJ[Var];
        assert( Ai < Aj && Bi < Bj && Ai <= Bi );
        if ( Aj == Bi )
            VarPerm = Var,
            VarTop  = Abc_ZddVarIJ(p, Ai, Bj);
        else if ( Aj == Bj )
            VarPerm = Var,
            VarTop  = Abc_ZddVarIJ(p, Ai, Bi);
        else if ( Ai == Bi )
            VarPerm = Abc_ZddVarIJ(p, Abc_MinInt(Aj, Bj), Abc_MaxInt(Aj, Bj)),
            VarTop  = A->Var;
        else // no clash
            VarPerm = Var, 
            VarTop  = A->Var;
        assert( p->pV2TI[VarPerm] > p->pV2TI[VarTop] );
        r0 = Abc_ZddPerm( p, A->False, Var ); 
        r1 = Abc_ZddPerm( p, A->True, VarPerm );
        assert( Abc_ZddObjVar(p, r1) > VarTop );
        if ( Abc_ZddObjVar(p, r0) > VarTop )
            r = Abc_ZddUniqueCreate( p, VarTop, r1, r0 );
        else
            r1 = Abc_ZddUniqueCreate( p, VarTop, r1, 0 ),
            r = Abc_ZddUnion( p, r0, r1 );
    }
    return Abc_ZddCacheInsert( p, a, Var, ABC_ZDD_OPER_PERM, r );
}

int Abc_ZddPerm2Comb	(	int *	pPerm,
		int	Size,
		int *	pComb
	)

Definition at line 636 of file extraUtilPerm.c.

{
    int i, j, nTrans = 0;
    for ( i = 0; i < Size; i++ )
        if ( i != pPerm[i] )
        {
            for ( j = i+1; j < Size; j++ )
                if ( i == pPerm[j] )
                    break;
            pComb[nTrans++] = (i << 16) | j;
            ABC_SWAP( int, pPerm[i], pPerm[j] );
            assert( i == pPerm[i] );
        }
    return nTrans;
}

void Abc_ZddPermCombTest

(

)

Definition at line 659 of file extraUtilPerm.c.

{
    int Size = 10;
    int pPerm[10] = { 6, 5, 7, 0, 3, 2, 1, 8, 9, 4 };
    int pComb[10], nTrans;
    Abc_ZddPermPrint( pPerm, Size );
    nTrans = Abc_ZddPerm2Comb( pPerm, Size, pComb );
    Abc_ZddCombPrint( pComb, nTrans );
    Abc_ZddComb2Perm( pComb, nTrans, pPerm, Size );
    Abc_ZddPermPrint( pPerm, Size );
    Size = 0;
}

void Abc_ZddPermPrint	(	int *	pPerm,
		int	Size
	)

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

Synopsis [Printing permutations and transpositions.]

Description []

SideEffects []

SeeAlso []

Definition at line 619 of file extraUtilPerm.c.

{
    int i;
    printf( "{" );
    for ( i = 0; i < Size; i++ )
        printf( " %2d", pPerm[i] );
    printf( " }\n" );
}

int Abc_ZddPermProduct	(	Abc_ZddMan *	p,
		int	a,
		int	b
	)

Definition at line 590 of file extraUtilPerm.c.

{
    Abc_ZddObj * B; 
    int r0, r1, r;
    if ( a == 0 ) return 0;
    if ( a == 1 ) return b;
    if ( b == 0 ) return 0;
    if ( b == 1 ) return a;
    if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_PERM_PROD)) >= 0 )
        return r;
    B  = Abc_ZddNode( p, b );
    r0 = Abc_ZddPermProduct( p, a, B->False ); 
    r1 = Abc_ZddPermProduct( p, a, B->True ); 
    r1 = Abc_ZddPerm( p, r1, B->Var );
    r  = Abc_ZddUnion( p, r0, r1 );
    return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_PERM_PROD, r );
}

void Abc_ZddPermTest

(

)

Definition at line 824 of file extraUtilPerm.c.

{
    Abc_ZddMan * p;
    p = Abc_ZddManAlloc( 10, 1 << 20 );
    Abc_ZddManCreatePerms( p, 5 );
    Abc_ZddPermTestInt( p );
    Abc_ZddManFree( p );
}

void Abc_ZddPermTestInt

(

Abc_ZddMan *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 789 of file extraUtilPerm.c.

{
    int nPerms = 3;
    int Size = 5;
    int pPerms[3][5] = { {1, 0, 2, 4, 3}, {1, 2, 4, 0, 3}, {0, 3, 2, 1, 4} };
    int pComb[5], nTrans;
    int i, k, Set, Union = 0, iPivot;
    for ( i = 0; i < nPerms; i++ )
        Abc_ZddPermPrint( pPerms[i], Size );
    for ( i = 0; i < nPerms; i++ )
    {
        printf( "Perm %d:\n", i );
        Abc_ZddPermPrint( pPerms[i], Size );
        nTrans = Abc_ZddPerm2Comb( pPerms[i], Size, pComb );
        Abc_ZddCombPrint( pComb, nTrans );
        for ( k = 0; k < nTrans; k++ )
            pComb[k] = Abc_ZddVarIJ( p, pComb[k] >> 16, pComb[k] & 0xFFFF );
        Abc_ZddPermPrint( pComb, nTrans );
        // add to ZDD
        Set = Abc_ZddBuildSet( p, pComb, nTrans );
        Union = Abc_ZddUnion( p, Union, Set );
    }
    printf( "\nResulting set of permutations:\n" );
    Abc_ZddPrint( p, Union );
    printf( "Nodes = %d.   Path = %d.\n", Abc_ZddCountNodes(p, Union), Abc_ZddCountPaths(p, Union) );

    iPivot = Abc_ZddVarIJ( p, 3, 4 );
    Union = Abc_ZddPerm( p, Union, iPivot );

    printf( "\nResulting set of permutations:\n" );
    Abc_ZddPrint( p, Union );
    printf( "Nodes = %d.   Path = %d.\n", Abc_ZddCountNodes(p, Union), Abc_ZddCountPaths(p, Union) );
    printf( "\n" );
}

void Abc_ZddPrint	(	Abc_ZddMan *	p,
		int	a
	)

Definition at line 704 of file extraUtilPerm.c.

{
    int * pPath = ABC_CALLOC( int, p->nVars );
    Abc_ZddPrint_rec( p, a, pPath, 0 );
    ABC_FREE( pPath );
}

void Abc_ZddPrint_rec	(	Abc_ZddMan *	p,
		int	a,
		int *	pPath,
		int	Size
	)

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

Synopsis [Printing ZDDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 683 of file extraUtilPerm.c.

{
    Abc_ZddObj * A;  
    if ( a == 0 ) return;
//    if ( a == 1 ) { Abc_ZddPermPrint( pPath, Size ); return; }
    if ( a == 1 )
    { 
        int pPerm[24], pComb[24], i;
        assert( p->nPermSize <= 24 );
        for ( i = 0; i < Size; i++ )
            pComb[i] = (p->pV2TI[pPath[i]] << 16) | p->pV2TJ[pPath[i]];
        Abc_ZddCombPrint( pComb, Size ); 
        Abc_ZddComb2Perm( pComb, Size, pPerm, p->nPermSize );
        Abc_ZddPermPrint( pPerm, p->nPermSize );
        return; 
    }
    A = Abc_ZddNode( p, a );
    Abc_ZddPrint_rec( p, A->False, pPath, Size );
    pPath[Size] = A->Var;
    Abc_ZddPrint_rec( p, A->True, pPath, Size + 1 );
}

void Abc_ZddPrintTest

(

Abc_ZddMan *

p

)

Definition at line 710 of file extraUtilPerm.c.

{
//    int nSets = 2;
//    int Size = 2;
//    int pSets[2][2] = { {5, 0}, {3, 11} };
    int nSets = 3;
    int Size = 5;
    int pSets[3][5] = { {5, 0, 2, 10, 7}, {3, 11, 10, 7, 2}, {0, 2, 5, 10, 7} };
    int i, Set, Union = 0;
    for ( i = 0; i < nSets; i++ )
    {
        Abc_ZddPermPrint( pSets[i], Size );
        Set = Abc_ZddBuildSet( p, pSets[i], Size );
        Union = Abc_ZddUnion( p, Union, Set );
    }
    printf( "Resulting set:\n" );
    Abc_ZddPrint( p, Union );
    printf( "\n" );
    printf( "Nodes = %d.   Path = %d.\n", Abc_ZddCountNodes(p, Union), Abc_ZddCountPaths(p, Union) );
    Size = 0;
}

static void Abc_ZddSetVarIJ ( Abc_ZddMan *  p, int  i, int  j, int  v  )

inlinestatic

Definition at line 100 of file extraUtilPerm.c.

{ assert( i < j ); p->pT2V[i * p->nPermSize + j] = v;      }

int Abc_ZddThresh	(	Abc_ZddMan *	p,
		int	a,
		int	b
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 459 of file extraUtilPerm.c.

{
    Abc_ZddObj * A; 
    int r0, r1, r;
    if ( a < 2 )  return a;
    if ( b == 0 ) return 0;
    if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_THRESH)) >= 0 )
        return r;
    A  = Abc_ZddNode( p, a );
    r0 = Abc_ZddThresh( p, A->False, b ),
    r1 = Abc_ZddThresh( p, A->True, b-1 );
    r  = Abc_ZddUniqueCreate( p, A->Var, r1, r0 );
    return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_THRESH, r );
}

int Abc_ZddUnion	(	Abc_ZddMan *	p,
		int	a,
		int	b
	)

Definition at line 275 of file extraUtilPerm.c.

{
    Abc_ZddObj * A, * B; 
    int r0, r1, r;
    if ( a == 0 ) return b;
    if ( b == 0 ) return a;
    if ( a == b ) return a;
    if ( a > b )  return Abc_ZddUnion( p, b, a );
    if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_UNION)) >= 0 )
        return r;
    A = Abc_ZddNode( p, a );
    B = Abc_ZddNode( p, b );
    if ( A->Var < B->Var )
        r0 = Abc_ZddUnion( p, A->False, b ), 
        r1 = A->True;
    else if ( A->Var > B->Var )
        r0 = Abc_ZddUnion( p, a, B->False ), 
        r1 = B->True;
    else
        r0 = Abc_ZddUnion( p, A->False, B->False ), 
        r1 = Abc_ZddUnion( p, A->True, B->True );
    r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 );
    return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_UNION, r );
}

static int Abc_ZddUniqueCreate ( Abc_ZddMan *  p, int  Var, int  True, int  False  )

inlinestatic

Definition at line 141 of file extraUtilPerm.c.

{
    assert( Var >= 0 && Var < p->nVars );
    assert( Var < Abc_ZddObjVar(p, True) );
    assert( Var < Abc_ZddObjVar(p, False) );
    if ( True == 0 )
        return False;
    {
        int *q = p->pUnique + (Abc_ZddHash(Var, True, False) & p->nUniqueMask);
        for ( ; *q; q = p->pNexts + *q )
            if ( p->pObjs[*q].Var == (unsigned)Var && p->pObjs[*q].True == (unsigned)True && p->pObjs[*q].False == (unsigned)False )
                return *q;
        if ( p->nObjs == p->nObjsAlloc )
            printf( "Aborting because the number of nodes exceeded %d.\n", p->nObjsAlloc ), fflush(stdout);
        assert( p->nObjs < p->nObjsAlloc );     
        *q = p->nObjs++;
        p->pObjs[*q].Var = Var;
        p->pObjs[*q].True = True;
        p->pObjs[*q].False = False;
//        printf( "Added node %3d: Var = %3d.  True = %3d.  False = %3d\n", *q, Var, True, False );
        return *q;
    }
}

static int Abc_ZddUniqueLookup ( Abc_ZddMan *  p, int  Var, int  True, int  False  )

inlinestatic

Definition at line 133 of file extraUtilPerm.c.

{
    int *q = p->pUnique + (Abc_ZddHash(Var, True, False) & p->nUniqueMask);
    for ( ; *q; q = p->pNexts + *q )
        if ( p->pObjs[*q].Var == (unsigned)Var && p->pObjs[*q].True == (unsigned)True && p->pObjs[*q].False == (unsigned)False )
            return *q;
    return 0;
}

void Abc_ZddUnmark_rec	(	Abc_ZddMan *	p,
		int	i
	)

Definition at line 420 of file extraUtilPerm.c.

{
    Abc_ZddObj * A;
    if ( i < 2 )
        return;
    A = Abc_ZddNode( p, i );
    if ( !A->Mark )
        return;
    A->Mark = 0;
    Abc_ZddUnmark_rec( p, A->False );
    Abc_ZddUnmark_rec( p, A->True );
}

static int Abc_ZddVarIJ ( Abc_ZddMan *  p, int  i, int  j  )

inlinestatic

Definition at line 101 of file extraUtilPerm.c.

{ assert( i < j ); return p->pT2V[i * p->nPermSize + j];   }

static int Abc_ZddVarsClash ( Abc_ZddMan *  p, int  v0, int  v1  )

inlinestatic

Definition at line 102 of file extraUtilPerm.c.

{ return p->pV2TI[v0] == p->pV2TI[v1] || p->pV2TJ[v0] == p->pV2TJ[v1] || p->pV2TI[v0] == p->pV2TJ[v1] || p->pV2TJ[v0] == p->pV2TI[v1];  }