From a9980135a0e599dda1b1c5a31992261ca1702ca9 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Tue, 14 Feb 2012 22:15:49 -0800
Subject: Isomorphism checking code.

---
 src/aig/gia/module.make |  1 +
 src/base/abci/abc.c     |  4 ++-
 src/misc/vec/vecInt.h   | 83 ++++++++++++++++++++++++++++++++++++++++++++++++-
 src/proof/fra/fraClau.c | 18 -----------
 4 files changed, 86 insertions(+), 20 deletions(-)

diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 11ec55f2..aec38f40 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -23,6 +23,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaGlitch.c \
     src/aig/gia/giaHash.c \
     src/aig/gia/giaIf.c \
+    src/aig/gia/giaIso.c \
     src/aig/gia/giaMan.c \
     src/aig/gia/giaMem.c \
     src/aig/gia/giaPat.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 70c51d7a..adaf76b7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27798,6 +27798,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p );
 //    extern int Gia_ManSuppSizeTest( Gia_Man_t * p );
 //    extern void Gia_VtaTest( Gia_Man_t * p, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose );
+    extern void Gia_IsoTest( Gia_Man_t * p );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
@@ -27834,8 +27835,9 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    pAbc->pGia = Gia_VtaTest( pTemp = pAbc->pGia );
 //    Gia_ManStopP( &pTemp );
 //    Gia_ManSuppSizeTest( pAbc->pGia );
-
 //    Gia_VtaTest( pAbc->pGia, 10, 100000, 0, 0, 1 );
+
+    Gia_IsoTest( pAbc->pGia );
     return 0;
 usage:
     Abc_Print( -2, "usage: &test [-svh]\n" );
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 39ab2623..72aa1ab6 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -348,6 +348,22 @@ static inline int Vec_IntSize( Vec_Int_t * p )
     return p->nSize;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntCap( Vec_Int_t * p )
+{
+    return p->nCap;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -453,6 +469,27 @@ static inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin )
     p->nCap   = nCapMin;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Resizes the vector to the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntGrowResize( Vec_Int_t * p, int nCapMin )
+{
+    p->nSize  = nCapMin;
+    if ( p->nCap >= nCapMin )
+        return;
+    p->pArray = ABC_REALLOC( int, p->pArray, nCapMin ); 
+    assert( p->pArray );
+    p->nCap   = nCapMin;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Fills the vector with given number of entries.]
@@ -1215,7 +1252,7 @@ static inline Vec_Int_t * Vec_IntTwoMerge( Vec_Int_t * vArr1, Vec_Int_t * vArr2
 
 /**Function*************************************************************
 
-  Synopsis    [Performs fast mapping for one node.]
+  Synopsis    []
 
   Description []
                
@@ -1239,6 +1276,32 @@ static inline void Vec_IntSelectSort( int * pArray, int nSize )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntSelectSortCost( int * pArray, int nSize, Vec_Int_t * vCosts )
+{
+    int temp, i, j, best_i;
+    for ( i = 0; i < nSize-1; i++ )
+    {
+        best_i = i;
+        for ( j = i+1; j < nSize; j++ )
+            if ( Vec_IntEntry(vCosts, pArray[j]) < Vec_IntEntry(vCosts, pArray[best_i]) )
+                best_i = j;
+        temp = pArray[i]; 
+        pArray[i] = pArray[best_i]; 
+        pArray[best_i] = temp;
+    }
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -1279,6 +1342,24 @@ static inline int Vec_IntCompareVec( Vec_Int_t * p1, Vec_Int_t * p2 )
     return memcmp( Vec_IntArray(p1), Vec_IntArray(p2), sizeof(int)*Vec_IntSize(p1) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Appends the contents of the second vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 )
+{
+    int Entry, i;
+    Vec_IntForEachEntry( vVec2, Entry, i )
+        Vec_IntPush( vVec1, Entry );
+}
+
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/proof/fra/fraClau.c b/src/proof/fra/fraClau.c
index fb87550d..48640d1d 100644
--- a/src/proof/fra/fraClau.c
+++ b/src/proof/fra/fraClau.c
@@ -313,24 +313,6 @@ static Vec_Int_t * Vec_IntSplitHalf( Vec_Int_t * vVec )
     return vPart;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Appends the contents of the second vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 )
-{
-    int Entry, i;
-    Vec_IntForEachEntry( vVec2, Entry, i )
-        Vec_IntPush( vVec1, Entry );
-}
-
 /**Function*************************************************************
 
   Synopsis    [Complements all literals in the clause.]
-- 
cgit v1.2.3