Bug fix in &uif.

5 files changed, 71 insertions, 20 deletions

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 1164e16b..16ca502c 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -5301,7 +5301,7 @@ Gia_Man_t * Gia_ManDupUif( Gia_Man_t * p )
     }
     iUif = Gia_ManDupUifConstr( pNew, p, pvMap );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManAppendCo( pNew, Gia_ManAppendAnd(pNew, pObj->Value, iUif) );
+        Gia_ManAppendCo( pNew, Gia_ManHashAnd(pNew, pObj->Value, iUif) );
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
     Vec_WecFree( pvMap[0] );
@@ -5336,23 +5336,31 @@ Gia_Man_t * Gia_ManDupBlackBox( Gia_Man_t * p )
     Vec_Int_t * vMap = Gia_ManDupBlackBoxBuildMap( p );
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
-    int i, k = 0;
+    int i, k = 0, iCi = 0, nCis = Gia_ManCiNum(p) + Vec_IntSum(vMap);
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManConst0(p)->Value = 0;
+    for ( i = 0; i < nCis; i++ )
+        Gia_ManAppendCi( pNew );
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachObj1( p, pObj, i )
     {
         if ( Gia_ObjIsBuf(pObj) )
-            pObj->Value = Vec_IntEntry(vMap, k++) ? Gia_ManAppendCi(pNew) : Gia_ObjFanin0Copy(pObj); // out/in
+        {
+            if ( Vec_IntEntry(vMap, k++) ) // out
+                pObj->Value = Gia_ManCiLit(pNew, iCi++);
+            else
+                pObj->Value = Gia_ObjFanin0Copy(pObj);
+        }
         else if ( Gia_ObjIsAnd(pObj) )
             pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         else if ( Gia_ObjIsCi(pObj) )
-            pObj->Value = Gia_ManAppendCi( pNew );
+            pObj->Value = Gia_ManCiLit(pNew, iCi++);
         else if ( Gia_ObjIsCo(pObj) )
             pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     }
+    assert( k == p->nBufs && iCi == nCis );
     pNew = Gia_ManCleanup( pTemp = pNew );
     Gia_ManStop( pTemp );
     Vec_IntFree( vMap );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3312ad07..46b2215a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -37157,6 +37157,12 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         pTemp = Cec5_ManSimulateTest( pAbc->pGia, pPars, fCbs, approxLim, subBatchSz, adaRecycle );
     else
         pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars, 0 );
+    if ( pAbc->pGia->pCexSeq != NULL )
+    {
+        pAbc->Status  = 0;
+        pAbc->nFrames = 0;
+        Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
+    }
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
diff --git a/src/base/wln/wlnCom.c b/src/base/wln/wlnCom.c
index dcf12229..6b754457 100644
--- a/src/base/wln/wlnCom.c
+++ b/src/base/wln/wlnCom.c
@@ -221,15 +221,18 @@ usage:
 ******************************************************************************/
 int Abc_CommandGraft( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Wln_LibGraftOne( Rtl_Lib_t * p, char * pModule1, char * pModule2, int fVerbose );
+    extern void Wln_LibGraftOne( Rtl_Lib_t * p, char * pModule1, char * pModule2, int fInv, int fVerbose );
     Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc);
     char ** pArgvNew; int nArgcNew;
-    int c,  fVerbose  = 0;
+    int c, fInv = 0, fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ivh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'i':
+            fInv ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -251,11 +254,12 @@ int Abc_CommandGraft( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandGraft(): This command expects one AIG file name on the command line.\n" );
         return 1;
     }
-    Wln_LibGraftOne( pLib, pArgvNew[0], pArgvNew[1], fVerbose );
+    Wln_LibGraftOne( pLib, pArgvNew[0], pArgvNew[1], fInv, fVerbose );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%graft [-vh] <module1_name> <module2_name>\n" );
+    Abc_Print( -2, "usage: %%graft [-ivh] <module1_name> <module2_name>\n" );
     Abc_Print( -2, "\t         replace instances of module1 by those of module2\n" );
+    Abc_Print( -2, "\t-i     : toggle using inverse grafting [default = %s]\n", fInv? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/wln/wlnRead.c b/src/base/wln/wlnRead.c
index 8cd4af0c..ed59358f 100644
--- a/src/base/wln/wlnRead.c
+++ b/src/base/wln/wlnRead.c
@@ -48,6 +48,7 @@ struct Rtl_Lib_t_
     Vec_Int_t *           vTokens;   // temp tokens
     int                   pMap[MAX_MAP];  // temp map
     Vec_Int_t *           vMap;      // mapping NameId into wires
+    Vec_Int_t *           vInverses; // inverse equivalences
     Vec_Int_t             vAttrTemp; // temp
     Vec_Int_t             vTemp[TEMP_NUM];  // temp
 };
@@ -325,6 +326,7 @@ void Rtl_LibFree( Rtl_Lib_t * p )
     for ( i = 0; i < TEMP_NUM; i++ )
         ABC_FREE( p->vTemp[i].pArray );
     Vec_IntFreeP( &p->vMap );
+    Vec_IntFreeP( &p->vInverses );
     Vec_IntFreeP( &p->vTokens );
     Abc_NamStop( p->pManName );
     Vec_PtrFree( p->vNtks );
@@ -1764,20 +1766,38 @@ void Rtl_NtkBlastConnect( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCon )
 }
 void Rtl_NtkBlastHierarchy( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCell )
 {
+    extern void Rtl_NtkPrintBufs( Rtl_Ntk_t * p, Vec_Int_t * vBufs );
     extern Gia_Man_t * Rtl_NtkBlast( Rtl_Ntk_t * p );
     extern void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits, int fBufs );
     extern int Gia_ManFindFirst( Rtl_Ntk_t * p, int * pnOuts );
     Rtl_Ntk_t * pModel = Rtl_NtkModule( p, Rtl_CellModule(pCell)-ABC_INFINITY );
     int nIns = 0, nOuts = 0, nOuts1, iFirst1 = Gia_ManFindFirst( pModel, &nOuts1 );
-    int k, Par, Val, nBits = 0;
-    //printf( "Blasting %s -> %s...\n", Rtl_NtkName(p), Rtl_NtkName(pModel) );
+    int k, Par, Val, iThis = -1, nBits = 0;
+    int fFound = 0;
+    //int fFound = p->pLib->vInverses && (iThis = Vec_IntFind(p->pLib->vInverses, pModel->NameId)) >= 0;
     Vec_IntClear( &p->vBitTemp );
     Rtl_CellForEachInput( p, pCell, Par, Val, k )
         Rtl_NtkCollectSignalRange( p, Val );
 //    if ( pModel->pGia == NULL )
 //        pModel->pGia = Rtl_NtkBlast( pModel );
     assert( pModel->pGia );
-    if ( pModel->fRoot )
+    if ( fFound )
+    {
+        // check if the previous one is the inverse one
+        int iThat = Vec_IntEntry( p->pLib->vInverses, iThis ^ 1 );
+        //printf( "Blasting %s -> %s...\n", Rtl_NtkName(p), Rtl_NtkName(pModel) );
+        //Rtl_NtkPrintBufs( p, pNew->vBarBufs );
+        if ( Vec_IntEntry(pNew->vBarBufs, Vec_IntSize(pNew->vBarBufs)-1) == Abc_Var2Lit(iThat, 1) &&
+             Vec_IntEntry(pNew->vBarBufs, Vec_IntSize(pNew->vBarBufs)-2) == Abc_Var2Lit(iThat, 0) )
+        {
+            //printf( "Found matching boundary.\n" );
+        }
+        nIns = nOuts1;
+        Vec_IntForEachEntry( &p->vBitTemp, Val, k )
+            Vec_IntWriteEntry( &p->vBitTemp, k, (k >= iFirst1 && k < iFirst1 + nOuts1) ? Gia_ManAppendBuf(pNew, Val) : Val );
+        Vec_IntPush( pNew->vBarBufs, (nIns << 16) | Abc_Var2Lit(pModel->NameId, 0) );
+    }
+    else if ( pModel->fRoot )
     {
         nIns = Vec_IntSize(&p->vBitTemp);
         Vec_IntForEachEntry( &p->vBitTemp, Val, k )
@@ -1788,7 +1808,7 @@ void Rtl_NtkBlastHierarchy( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCell )
     Gia_ManDupRebuild( pNew, pModel->pGia, &p->vBitTemp, !pModel->fRoot );
     if ( !pModel->fRoot )
         Vec_IntAppend( pNew->vBarBufs, pModel->pGia->vBarBufs );
-    if ( pModel->fRoot )
+    if ( pModel->fRoot || fFound )
     {
         nOuts = Vec_IntSize(&p->vBitTemp);
         Vec_IntForEachEntry( &p->vBitTemp, Val, k )
@@ -2616,7 +2636,7 @@ Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Wln_LibGraftOne( Rtl_Lib_t * p, char * pModule1, char * pModule2, int fVerbose )
+void Wln_LibGraftOne( Rtl_Lib_t * p, char * pModule1, char * pModule2, int fInv, int fVerbose )
 {
     int Name1 = Wln_ReadFindToken( pModule1, p->pManName );
     int Name2 = Wln_ReadFindToken( pModule2, p->pManName );
@@ -2633,12 +2653,23 @@ void Wln_LibGraftOne( Rtl_Lib_t * p, char * pModule1, char * pModule2, int fVerb
         Rtl_Ntk_t * pNtk1 = Rtl_LibNtk(p, iNtk1);
         Rtl_Ntk_t * pNtk2 = Rtl_LibNtk(p, iNtk2);
         assert( iNtk1 != iNtk2 );
-        printf( "Replacing \"%s\" (appearing %d times) by \"%s\" (appearing %d times).\n", 
-            Rtl_NtkName(pNtk1), Rtl_LibCountInsts(p, pNtk1), Rtl_NtkName(pNtk2), Rtl_LibCountInsts(p, pNtk2) );
-        pNtk1->iCopy = iNtk2;
-    //    Rtl_LibSetReplace( p, vGuide );
-        Rtl_LibUpdateBoxes( p );
-        Rtl_LibReorderModules( p );
+        if ( fInv )
+        {
+            printf( "Setting \"%s\" (appearing %d times) and \"%s\" (appearing %d times) as inverse-equivalent.\n", 
+                Rtl_NtkName(pNtk1), Rtl_LibCountInsts(p, pNtk1), Rtl_NtkName(pNtk2), Rtl_LibCountInsts(p, pNtk2) );
+            if ( p->vInverses == NULL )
+                p->vInverses = Vec_IntAlloc( 10 );
+            Vec_IntPushTwo( p->vInverses, pNtk1->NameId, pNtk2->NameId );
+        }
+        else
+        {
+            printf( "Replacing \"%s\" (appearing %d times) by \"%s\" (appearing %d times).\n", 
+                Rtl_NtkName(pNtk1), Rtl_LibCountInsts(p, pNtk1), Rtl_NtkName(pNtk2), Rtl_LibCountInsts(p, pNtk2) );
+            pNtk1->iCopy = iNtk2;
+        //    Rtl_LibSetReplace( p, vGuide );
+            Rtl_LibUpdateBoxes( p );
+            Rtl_LibReorderModules( p );
+        }
     }
 }
 
diff --git a/src/proof/cec/cecSatG3.c b/src/proof/cec/cecSatG3.c
index eaad455b..5f22937c 100644
--- a/src/proof/cec/cecSatG3.c
+++ b/src/proof/cec/cecSatG3.c
@@ -2125,6 +2125,8 @@ Gia_Man_t * Cec5_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars, int fCbs,
 {
     Gia_Man_t * pNew = NULL;
     Cec5_ManPerformSweeping( p, pPars, &pNew, 0, fCbs, approxLim, subBatchSz, adaRecycle );
+    if ( pNew == NULL )
+        pNew = Gia_ManDup( p );
     return pNew;
 }