Experiments with permutations.

2 files changed, 868 insertions, 0 deletions

diff --git a/src/misc/extra/extraUtilPerm.c b/src/misc/extra/extraUtilPerm.c
new file mode 100644
index 00000000..d5b8e080
--- /dev/null
+++ b/src/misc/extra/extraUtilPerm.c
@@ -0,0 +1,867 @@
+/**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 $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include "misc/vec/vec.h"
+#include "aig/gia/gia.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef enum  
+{
+    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_MULTIPLY,
+    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;
+
+typedef struct Abc_ZddObj_ Abc_ZddObj;
+struct Abc_ZddObj_ 
+{
+    unsigned     Var  : 31;
+    unsigned     Mark :  1;
+    unsigned     True;
+    unsigned     False;
+};  
+
+typedef struct Abc_ZddEnt_ Abc_ZddEnt;
+struct Abc_ZddEnt_ 
+{
+    int          Arg0;
+    int          Arg1;
+    int          Arg2;
+    int          Res;
+};
+
+typedef struct Abc_ZddMan_ Abc_ZddMan;
+struct Abc_ZddMan_ 
+{
+    int          nVars;
+    int          nObjs;
+    int          nObjsAlloc;
+    int          nPermSize;
+    unsigned     nUniqueMask;
+    unsigned     nCacheMask;
+    int *        pUnique;
+    int *        pNexts;
+    Abc_ZddEnt * pCache;
+    Abc_ZddObj * pObjs;
+    int          nCacheLookups;
+    int          nCacheMisses;
+    int          nMemory;
+    int *        pV2TI;
+    int *        pV2TJ;
+    int *        pT2V;
+};
+
+static inline int          Abc_ZddIthVar( int i )                                  { return i + 2;                                            }
+static inline unsigned     Abc_ZddHash( int Arg0, int Arg1, int Arg2 )             { return 12582917 * Arg0 + 4256249 * Arg1 + 741457 * Arg2; }
+
+static inline Abc_ZddObj * Abc_ZddNode( Abc_ZddMan * p, int i )                    { return p->pObjs + i;                                     }
+static inline int          Abc_ZddObjId( Abc_ZddMan * p, Abc_ZddObj * pObj )       { return pObj - p->pObjs;                                  }
+static inline int          Abc_ZddObjVar( Abc_ZddMan * p, int i )                  { return Abc_ZddNode(p, i)->Var;                           }
+
+static inline void         Abc_ZddSetVarIJ( Abc_ZddMan * p, int i, int j, int v )  { assert( i < j ); p->pT2V[i * p->nPermSize + j] = v;      }
+static inline int          Abc_ZddVarIJ( Abc_ZddMan * p, int i, int j )            { assert( i < j ); return p->pT2V[i * p->nPermSize + j];   }
+static inline int          Abc_ZddVarsClash( Abc_ZddMan * p, int v0, int v1 )      { 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];  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_ZddCacheLookup( Abc_ZddMan * p, int Arg0, int Arg1, int Arg2 )
+{
+    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;
+}
+static inline int Abc_ZddCacheInsert( Abc_ZddMan * p, int Arg0, int Arg1, int Arg2, int Res )
+{
+    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++;
+    return Res;
+}
+static inline int Abc_ZddUniqueLookup( Abc_ZddMan * p, int Var, int True, int 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;
+    return 0;
+}
+static inline int Abc_ZddUniqueCreate( Abc_ZddMan * p, int Var, int True, int False )
+{
+    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;
+    }
+}
+int Abc_ZddBuildSet( Abc_ZddMan * p, int * pSet, int Size )
+{
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_ZddMan * Abc_ZddManAlloc( int nVars, int nObjs )
+{
+    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 )
+{
+    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 )
+{
+    printf( "ZDD stats: Var = %d  Obj = %d  All = %d  Hits = %d  Miss = %d  ", 
+        p->nVars, p->nObjs, p->nObjsAlloc, p->nCacheLookups-p->nCacheMisses, p->nCacheMisses );
+    printf( "Mem = %.2f MB\n", 4.0*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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ZddDiff( Abc_ZddMan * p, int a, int b )
+{
+    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_ZddUnion( Abc_ZddMan * p, int a, int b )
+{
+    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 );
+}
+int Abc_ZddMinUnion( Abc_ZddMan * p, int a, int b )
+{
+    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 );
+}
+int Abc_ZddIntersect( Abc_ZddMan * p, int a, int b )
+{
+    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 );
+}
+int Abc_ZddCof0( Abc_ZddMan * p, int a, int Var )
+{
+    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 )
+{
+    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 );
+}
+int Abc_ZddMultiply( Abc_ZddMan * p, int a, int Var )
+{
+    Abc_ZddObj * A; 
+    int r0, r1, r;
+    if ( a == 0 )  return 0;
+    if ( a == 1 )  return Abc_ZddIthVar(Var);
+    if ( (r = Abc_ZddCacheLookup(p, a, Var, ABC_ZDD_OPER_MULTIPLY)) >= 0 )
+        return r;
+    A = Abc_ZddNode( p, a );
+    if ( (int)A->Var > Var )
+        r = Abc_ZddUniqueCreate( p, Var, a, 0 );
+    else if ( (int)A->Var < Var )
+    {
+        r0 = Abc_ZddMultiply( p, A->False, Var ),
+        r1 = Abc_ZddMultiply( p, A->True, Var );
+        r  = Abc_ZddUniqueCreate( p, A->Var, r1, r0 );
+    }
+    else assert( 0 );
+    return Abc_ZddCacheInsert( p, a, Var, ABC_ZDD_OPER_MULTIPLY, r );
+}
+int Abc_ZddCountPaths( Abc_ZddMan * p, int a )
+{
+    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_ZddCountNodes( Abc_ZddMan * p, int a )
+{
+    Abc_ZddObj * A;  
+    int r;
+    if ( a < 2 ) return 0;
+    if ( (r = Abc_ZddCacheLookup(p, a, 0, ABC_ZDD_OPER_NODES)) >= 0 )
+        return r;
+    A = Abc_ZddNode( p, a );
+    r = 1 + Abc_ZddCountNodes( p, A->False ) + Abc_ZddCountNodes( p, A->True );
+    return Abc_ZddCacheInsert( p, a, 0, ABC_ZDD_OPER_NODES, r );
+}
+int Abc_ZddCount_rec( Abc_ZddMan * p, int i )
+{
+    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);
+}
+void Abc_ZddUnmark_rec( Abc_ZddMan * p, int i )
+{
+    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 );
+}
+int Abc_ZddCountNodesArray( Abc_ZddMan * p, Vec_Int_t * vNodes )
+{
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ZddThresh( Abc_ZddMan * p, int a, int b )
+{
+    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_ZddDotProduct( Abc_ZddMan * p, int a, int b )
+{
+    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 );
+}
+int Abc_ZddDotMinProduct6( Abc_ZddMan * p, int a, int b )
+{
+    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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ZddPerm( Abc_ZddMan * p, int a, int Var )
+{
+    Abc_ZddObj * A; 
+    int 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 ( (int)A->Var == Var )
+        r = Abc_ZddUniqueCreate( p, A->Var, A->False, A->True );
+    else if ( p->pV2TI[A->Var] > p->pV2TJ[Var] )
+        r = Abc_ZddUniqueCreate( p, Var, a, 0 );
+    else 
+    {
+        int r0, r1, VarTop, VarPerm;
+        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 );
+        if ( Ai == Bj || (Ai == Bi && Aj > Bj) || (Aj == Bj && Ai > Bi) )
+            VarTop  = Var, 
+            VarPerm = A->Var;
+        else if ( Ai == Bi )
+            VarTop  = A->Var, 
+            VarPerm = Abc_ZddVarIJ(p, Aj, Bj);
+        else if ( Aj == Bj )
+            VarTop  = Abc_ZddVarIJ(p, Ai, Bi), 
+            VarPerm = Abc_ZddVarIJ(p, Bi, Bj);
+        else if ( Aj == Bi )
+            VarTop  = A->Var,                  
+            VarPerm = Abc_ZddVarIJ(p, Ai, Bj);
+        else // no clash
+            VarTop  = A->Var, 
+            VarPerm = Var;
+        r0 = Abc_ZddPerm( p, A->False, Var ); 
+        r1 = Abc_ZddPerm( p, A->True, VarPerm );
+        if ( VarTop < Abc_ZddObjVar(p, r0) && VarTop < Abc_ZddObjVar(p, r1) )
+            r = Abc_ZddUniqueCreate( p, VarTop, r1, r0 );
+        else
+        {
+            r1 = Abc_ZddMultiply( p, r1, VarTop );
+            r = Abc_ZddUnion( p, r0, r1 );
+        }
+    }
+    return Abc_ZddCacheInsert( p, a, Var, ABC_ZDD_OPER_PERM, r );
+}
+int Abc_ZddPermProduct( Abc_ZddMan * p, int a, int b )
+{
+    Abc_ZddObj * A, * 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;
+    A = Abc_ZddNode( p, a );
+    B = Abc_ZddNode( p, b );
+    if ( Abc_ZddVarsClash(p, A->Var, B->Var) )
+    {
+        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, r1, r0 );
+        assert( Abc_MinInt(A->Var, B->Var) <= (int)Abc_ZddObjVar(p, r) );
+    }
+    else
+    {
+        if ( A->Var < B->Var )
+            r0 = Abc_ZddPermProduct( p, A->False, b ), 
+            r1 = Abc_ZddPermProduct( p, A->True, b );
+        else if ( A->Var > B->Var )
+            r0 = Abc_ZddPermProduct( p, a, B->False ), 
+            r1 = Abc_ZddPermProduct( p, a, B->True ); 
+        else assert( 0 );
+        r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 );
+    }
+    return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_PERM_PROD, r );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Printing permutations and transpositions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ZddPermPrint( int * pPerm, int Size )
+{
+    int i;
+    printf( "{" );
+    for ( i = 0; i < Size; i++ )
+        printf( " %d", pPerm[i] );
+    printf( " }\n" );
+}
+void Abc_ZddCombPrint( int * pComb, int nTrans )
+{
+    int i;
+    for ( i = 0; i < nTrans; i++ )
+        printf( "(%d %d)", pComb[i] >> 16, pComb[i] & 0xffff );
+    printf( "\n" );
+}
+int Abc_ZddPerm2Comb( int * pPerm, int Size, int * pComb )
+{
+    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_ZddComb2Perm( int * pComb, int nTrans, int * pPerm, int Size )
+{
+    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_ZddPermCombTest()
+{
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Printing ZDDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ZddPrint_rec( Abc_ZddMan * p, int a, int * pPath, int Size )
+{
+    Abc_ZddObj * A;  
+    if ( a == 0 ) return;
+//    if ( a == 1 ) { Abc_ZddPermPrint( pPath, Size ); return; }
+    if ( a == 1 )
+    { 
+        int pPerm[10], pComb[10], i;
+        assert( p->nPermSize <= 10 );
+        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_ZddPrint( Abc_ZddMan * p, int a )
+{
+    int * pPath = ABC_CALLOC( int, p->nVars );
+    Abc_ZddPrint_rec( p, a, pPath, 0 );
+    ABC_FREE( pPath );
+}
+void Abc_ZddPrintTest( Abc_ZddMan * p )
+{
+//    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ZddGiaTest( Gia_Man_t * pGia )
+{
+    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 );
+}
+/*
+    abc 01> &r pj1.aig; &ps; &test
+    pj1      : i/o =   1769/   1063  and =   16285  lev =  156 (12.91)  mem = 0.23 MB
+    Paths = 839934.  Shared nodes = 770999.
+    ZDD stats: Var = 19118  Obj = 11578174  All = 16777216  Hits = 25617277  Miss = 40231476  Mem = 576.00 MB
+*/
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ZddPermTestInt( Abc_ZddMan * p )
+{
+    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_ZddPermTest()
+{
+    Abc_ZddMan * p;
+    p = Abc_ZddManAlloc( 10, 1 << 20 );
+    Abc_ZddManCreatePerms( p, 5 );
+    Abc_ZddPermTestInt( p );
+    Abc_ZddManFree( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
index a21fd103..9c13c146 100644
--- a/src/misc/extra/module.make
+++ b/src/misc/extra/module.make
@@ -12,6 +12,7 @@ SRC +=    src/misc/extra/extraBddAuto.c \
     src/misc/extra/extraUtilFile.c \
     src/misc/extra/extraUtilMemory.c \
     src/misc/extra/extraUtilMisc.c \
+    src/misc/extra/extraUtilPerm.c \
     src/misc/extra/extraUtilProgress.c \
     src/misc/extra/extraUtilReader.c \
     src/misc/extra/extraUtilTruth.c \