Isomorphism checking code.

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
@@ -359,6 +359,22 @@ static inline int Vec_IntSize( Vec_Int_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+static inline int Vec_IntCap( Vec_Int_t * p )
+{
+    return p->nCap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline int Vec_IntEntry( Vec_Int_t * p, int i )
 {
     assert( i >= 0 && i < p->nSize );
@@ -455,6 +471,27 @@ static inline void Vec_IntGrow( Vec_Int_t * p, int 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.]
 
   Description []
@@ -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 []
                
@@ -1250,6 +1287,32 @@ static inline void Vec_IntSelectSort( int * pArray, int nSize )
   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    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline void Vec_IntPrint( Vec_Int_t * vVec )
 {
     int i, Entry;
@@ -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
@@ -315,24 +315,6 @@ static Vec_Int_t * Vec_IntSplitHalf( Vec_Int_t * vVec )
 
 /**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.]
 
   Description []