Experiments with word-level data structures.

src/base/wlc/wlcCom.c

@@ -21,7 +21,7 @@
 #include "wlc.h"
 #include "base/wln/wln.h"
 #include "base/main/mainInt.h"
-#include "aig/miniaig/ndr.h"
+//#include "aig/miniaig/ndr.h"
 
 ABC_NAMESPACE_IMPL_START
 

src/base/wln/wlnCom.c

@@ -276,7 +276,7 @@ usage:
 int Abc_CommandSolve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Rtl_LibBlast( Rtl_Lib_t * pLib );
-    extern void Rtl_LibBlast2( Rtl_Lib_t * pLib );
+    extern void Rtl_LibBlast2( Rtl_Lib_t * pLib, Vec_Int_t * vRoots );
     extern void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk );
     extern void Rtl_LibPreprocess( Rtl_Lib_t * pLib );
     extern void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p );
@@ -327,7 +327,7 @@ int Abc_CommandSolve( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( fOldBlast )
             Rtl_LibBlast( pLib );
         else
-            Rtl_LibBlast2( pLib );
+            Rtl_LibBlast2( pLib, NULL );
         if ( fPrepro )
             Rtl_LibPreprocess( pLib );
         Rtl_LibSolve( pLib, NULL );

src/base/wln/wlnGuide.c

@@ -41,26 +41,48 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p )
+int Wln_ReadFindToken( char * pToken, Abc_Nam_t * p )
 {
-    char Buffer[1000] = {'\\'}, * pBuffer = Buffer+1;
-    Vec_Int_t * vTokens = Vec_IntAlloc( 100 );
+    char * pBuffer = Abc_UtilStrsavTwo( "\\", pToken );
+    int RetValue = Abc_NamStrFindOrAdd( p, pBuffer, NULL );
+    ABC_FREE( pBuffer );
+    return RetValue;
+}
+void Wln_PrintGuidance( Vec_Wec_t * vGuide, Abc_Nam_t * p )
+{
+    Vec_Int_t * vLevel; int i, k, Obj; 
+    Vec_WecForEachLevel( vGuide, vLevel, i )
+    {
+        Vec_IntForEachEntry( vLevel, Obj, k )
+            printf( "%s ", Obj >= 0 ? Abc_NamStr(p, Obj) : "[unknown]" );
+        printf( "\n" );
+    }
+}
+Vec_Wec_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p )
+{
+    char * pBuffer = ABC_CALLOC( char, 10000 ), * pToken;
+    Vec_Wec_t * vTokens = Vec_WecAlloc( 100 ); Vec_Int_t * vLevel;
     FILE * pFile = fopen( pFileName, "rb" );
-    while ( fscanf( pFile, "%s", pBuffer ) == 1 )
+    while ( fgets( pBuffer, 10000, pFile ) )
     {
-        if ( pBuffer[(int)strlen(pBuffer)-1] == '\r' )
-            pBuffer[(int)strlen(pBuffer)-1] = 0;
-        if ( !strcmp(pBuffer, "prove") && Vec_IntSize(vTokens) % 4 == 3 ) // account for "property"
-            Vec_IntPush( vTokens, -1 );
-        if ( Vec_IntSize(vTokens) % 4 == 2 || Vec_IntSize(vTokens) % 4 == 3 )
-            Vec_IntPush( vTokens, Abc_NamStrFindOrAdd(p, Buffer, NULL) );
-        else
-            Vec_IntPush( vTokens, Abc_NamStrFindOrAdd(p, pBuffer, NULL) );
+        if ( pBuffer[0] == '#' )
+            continue;
+        vLevel = Vec_WecPushLevel( vTokens );
+        pToken = strtok( pBuffer, " \t\r\n" );
+        while ( pToken )
+        {
+            Vec_IntPush( vLevel, Vec_IntSize(vLevel) < 2 ? Abc_NamStrFindOrAdd(p, pToken, NULL) : Wln_ReadFindToken(pToken, p) );
+            pToken = strtok( NULL, " \t\r\n" );
+        }
+        if ( Vec_IntSize(vLevel) % 4 == 3 ) // account for "property"
+            Vec_IntPush( vLevel, -1 );
+        assert( Vec_IntSize(vLevel) % 4 == 0 );
     }
     fclose( pFile );
-    if ( Vec_IntSize(vTokens) % 4 == 3 ) // account for "property"
-        Vec_IntPush( vTokens, -1 );
-    assert( Vec_IntSize(vTokens) % 4 == 0 );
+    if ( Vec_WecSize(vTokens) == 0 )
+        printf( "Guidance is empty.\n" );
+    //Wln_PrintGuidance( vTokens, p );
+    ABC_FREE( pBuffer );
     return vTokens;
 }
 

src/base/wln/wlnRead.c

@@ -335,6 +335,39 @@ int Rtl_LibFindModule( Rtl_Lib_t * p, int NameId )
             return i;
     return -1;
 }
+int Rtl_LibFindModule2( Rtl_Lib_t * p, int NameId, int iNtk0 )
+{
+    char * pName = Rtl_LibStr( p, NameId );
+    Rtl_Ntk_t * pNtk0 = Rtl_LibNtk( p, iNtk0 );
+    Rtl_Ntk_t * pNtk; int i;
+    int Counts0[4] = {0};  Rtl_NtkCountPio( pNtk0, Counts0 );
+    Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
+        if ( strstr(Rtl_NtkName(pNtk), pName+1) )
+        {
+            int Counts[4] = {0};  Rtl_NtkCountPio( pNtk, Counts );
+            if ( Counts[1] == Counts0[1] && Counts[3] == Counts0[3] )
+                return i;
+        }
+    return -1;
+}
+int Rtl_LibFindTwoModules( Rtl_Lib_t * p, int Name1, int Name2 )
+{
+    int iNtk1 = Rtl_LibFindModule( p, Name1 );
+    if ( Name2 == -1 )
+        return (iNtk1 << 16) | iNtk1;
+    else
+    {
+        int Counts1[4] = {0}, Counts2[4] = {0};
+        int iNtk2 = Rtl_LibFindModule( p, Name2 );
+        Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 );
+        Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 );
+        Rtl_NtkCountPio( pNtk1, Counts1 );
+        Rtl_NtkCountPio( pNtk2, Counts2 );
+        if ( Counts1[1] != Counts2[1] || Counts1[3] != Counts2[3] )
+            iNtk1 = Rtl_LibFindModule2( p, Name1, iNtk2 );
+        return (iNtk1 << 16) | iNtk2;
+    }
+}
 void Rtl_LibPrintStats( Rtl_Lib_t * p )
 {
     Rtl_Ntk_t * pNtk; int i, nSymbs = 0;
@@ -1404,7 +1437,7 @@ void Rtl_NtkUpdateBoxes( Rtl_Ntk_t * p )
     Rtl_NtkForEachCell( p, pCell, i )
     {
         Rtl_Ntk_t * pMod = Rtl_CellNtk( p, pCell );
-        if ( pMod ) 
+        if ( pMod && pMod->iCopy >= 0 ) 
             pCell[2] = ABC_INFINITY + pMod->iCopy;
     }
 }
@@ -2055,12 +2088,73 @@ printf( "Dumped \"%s\" with AIG for module %-20s : ", Buffer, Rtl_ShortenName(Rt
 Gia_ManPrintStats( p->pGia, NULL );
     return p->pGia;
 }
-void Rtl_LibBlast2( Rtl_Lib_t * pLib )
+void Rtl_LibMark_rec( Rtl_Ntk_t * pNtk )
 {
-    Rtl_Ntk_t * p; int i;
-    Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, p, i )
-        if ( p->pGia == NULL )
-            p->pGia = Rtl_NtkBlast2( p );
+    int i, * pCell;
+    if ( pNtk->iCopy == -1 )
+        return;
+    Rtl_NtkForEachCell( pNtk, pCell, i )
+    {
+        Rtl_Ntk_t * pMod = Rtl_CellNtk( pNtk, pCell );
+        if ( pMod )
+            Rtl_LibMark_rec( pMod );
+    }
+    assert( pNtk->iCopy == -2 );
+    pNtk->iCopy = -1;
+}
+void Rtl_LibBlast2( Rtl_Lib_t * pLib, Vec_Int_t * vRoots )
+{
+    Rtl_Ntk_t * pNtk; int i, iNtk;
+    Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
+        pNtk->iCopy = -1;
+    if ( vRoots )
+    {
+        Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
+            pNtk->iCopy = -2;
+        Vec_IntForEachEntry( vRoots, iNtk, i )
+            Rtl_LibMark_rec( Rtl_LibNtk(pLib, iNtk) );
+    }
+    Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
+        if ( pNtk->iCopy == -1 && pNtk->pGia == NULL )
+            pNtk->pGia = Rtl_NtkBlast2( pNtk );
+//    Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
+//        if ( pNtk->iCopy == -2 )
+//            printf( "Skipping network \"%s\" during bit-blasting.\n", Rtl_NtkName(pNtk) );
+    Vec_PtrForEachEntry( Rtl_Ntk_t *, pLib->vNtks, pNtk, i )
+        pNtk->iCopy = -1;
+}
+void Rtl_LibBlastClean( Rtl_Lib_t * p )
+{
+    Rtl_Ntk_t * pNtk; int i;
+    Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
+        Gia_ManStopP( &pNtk->pGia );
+}
+void Rtl_LibSetReplace( Rtl_Lib_t * p, Vec_Wec_t * vGuide )
+{
+    Vec_Int_t * vLevel; int i, iNtk1, iNtk2; 
+    Rtl_Ntk_t * pNtk, * pNtk1, * pNtk2;
+    Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i )
+        pNtk->iCopy = -1;
+    Vec_WecForEachLevel( vGuide, vLevel, i )
+    {
+        int Name1 = Vec_IntEntry( vLevel, 2 );
+        int Name2 = Vec_IntEntry( vLevel, 3 );
+        int iNtk  = Rtl_LibFindTwoModules( p, Name1, Name2 );
+        if ( iNtk == -1 )
+        {
+            printf( "Cannot find networks \"%s\" and \"%s\" in the design.\n", Rtl_LibStr(p, Name1), Rtl_LibStr(p, Name2) ); 
+            break;
+        }
+        iNtk1 = iNtk >> 16;
+        iNtk2 = iNtk & 0xFFFF;
+        pNtk1 = Rtl_LibNtk(p, iNtk1);
+        pNtk2 = Rtl_LibNtk(p, iNtk2);
+        pNtk1->iCopy = iNtk2;
+        if ( iNtk1 == iNtk2 )
+            printf( "Preparing to prove \"%s\".\n", Rtl_NtkName(pNtk1) );
+        else
+            printf( "Preparing to replace \"%s\" by \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
+    }
 }
 
 
@@ -2113,7 +2207,7 @@ finish:
         if ( p != p1 && p != p2 )
             Gia_ManStopP( &p->pGia );
     //Rtl_LibBlast( pLib );
-    Rtl_LibBlast2( pLib );
+    Rtl_LibBlast2( pLib, NULL );
 }
 void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk )
 {
@@ -2185,24 +2279,61 @@ void Wln_SolveProperty( Rtl_Lib_t * p, int iNtk )
     printf( "Proving property \"%s\".\n", Rtl_NtkName(pNtk) );
     Rtl_LibSolve( p, pNtk );
 }
+Vec_Int_t * Wln_ReadNtkRoots( Rtl_Lib_t * p, Vec_Wec_t * vGuide ) 
+{
+    Vec_Int_t * vLevel; int i; 
+    Vec_Int_t * vRoots = Vec_IntAlloc( 100 ); 
+    Vec_WecForEachLevel( vGuide, vLevel, i )
+    {
+        int Name1 = Vec_IntEntry( vLevel, 2 );
+        int Name2 = Vec_IntEntry( vLevel, 3 );
+        int iNtk  = Rtl_LibFindTwoModules( p, Name1, Name2 );
+        if ( iNtk == -1 )
+        {
+            printf( "Cannot find networks \"%s\" and \"%s\" in the design.\n", Rtl_LibStr(p, Name1), Rtl_LibStr(p, Name2) ); 
+            break;
+        }
+/*
+        else
+        {
+            Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk >> 16 );
+            Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk & 0xFFFF );
+            printf( "Matching \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
+        }
+*/
+        Vec_IntPushTwo( vRoots, iNtk >> 16, iNtk & 0xFFFF );
+    }
+    return vRoots;
+}
 void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p )
 {
-    extern Vec_Int_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p );
-    Vec_Int_t * vGuide = Wln_ReadGuidance( pFileName, p->pManName ); int i;
+    extern Vec_Wec_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p );
+    Vec_Wec_t * vGuide = Wln_ReadGuidance( pFileName, p->pManName );
+    Vec_Int_t * vRoots, * vLevel; int i, iNtk1, iNtk2;
     Vec_IntFillExtra( p->vMap, Abc_NamObjNumMax(p->pManName), -1 );
-    Rtl_LibBlast2( p );
-    for ( i = 0; i < Vec_IntSize(vGuide); i += 4 )
-    {
-        int Prove = Vec_IntEntry( vGuide, i+0 );
-        int Type  = Vec_IntEntry( vGuide, i+1 );
-        int Name1 = Vec_IntEntry( vGuide, i+2 );
-        int Name2 = Vec_IntEntry( vGuide, i+3 );
-        int iNtk1 = Rtl_LibFindModule( p, Name1 );
-        int iNtk2 = Name2 == -1 ? -1 : Rtl_LibFindModule( p, Name2 );
+    Rtl_LibSetReplace( p, vGuide );
+    Rtl_LibUpdateBoxes( p );
+    Rtl_LibReorderModules( p );
+    vRoots = Wln_ReadNtkRoots( p, vGuide );
+    Rtl_LibBlast2( p, vRoots );
+    Vec_WecForEachLevel( vGuide, vLevel, i )
+    {
+        int Prove = Vec_IntEntry( vLevel, 0 );
+        int Type  = Vec_IntEntry( vLevel, 1 );
+        int Name1 = Vec_IntEntry( vLevel, 2 );
+        int Name2 = Vec_IntEntry( vLevel, 3 );
+        int iNtk  = Rtl_LibFindTwoModules( p, Name1, Name2 );
+        if ( iNtk == -1 )
+        {
+            printf( "Cannot find networks \"%s\" and \"%s\" in the design.\n", Rtl_LibStr(p, Name1), Rtl_LibStr(p, Name2) ); 
+            break;
+        }
+        iNtk1 = iNtk >> 16;
+        iNtk2 = iNtk & 0xFFFF;
         if ( Prove != Rtl_LibStrId(p, "prove") )
-            printf( "Unknown task in line %d.\n", i/4 );
-        else if ( iNtk1 == -1 )
-            printf( "Network %s cannot be found in this design.\n", Rtl_LibStr(p, Name1) );
+            printf( "Unknown task in line %d.\n", i );
+        //else if ( iNtk1 == -1 )
+        //    printf( "Network %s cannot be found in this design.\n", Rtl_LibStr(p, Name1) );
         else
         {
             if ( Type == Rtl_LibStrId(p, "equal") )
@@ -2215,7 +2346,9 @@ void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p )
         }
         break;
     }
-    Vec_IntFree( vGuide );
+    Rtl_LibBlastClean( p );
+    Vec_WecFree( vGuide );
+    Vec_IntFree( vRoots );
 }
 
 ////////////////////////////////////////////////////////////////////////