Fixing the problem with outputting word-level CEXes.

2 files changed, 48 insertions, 2 deletions

diff --git a/src/base/io/io.c b/src/base/io/io.c
index a85d64ef..e68985f3 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -2446,12 +2446,35 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
             fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1);
             // output flop values (unaffected by the minimization)
             Abc_NtkForEachLatch( pNtk, pObj, i )
-                fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
+            {
+                char * pObjName = Abc_ObjName(Abc_ObjFanout0(pObj));
+                int ii, NameLen = strlen(pObjName);
+                // check if there is a PI with a matching name
+                Abc_Obj_t * pObjPi;
+                Abc_NtkForEachPi( pNtk, pObjPi, ii )
+                    if ( !strncmp(Abc_ObjName(pObjPi), pObjName, NameLen) && !strncmp(Abc_ObjName(pObjPi)+NameLen, "_init", 5) )
+                    {
+                        if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+ii) )
+                            fprintf( pFile, "%s@%d=%c\n", pObjName, 0, '0'+Abc_InfoHasBit(pCex->pData, pCare->nRegs+ii) );
+                        break;
+                    }
+                if ( ii != Abc_NtkPiNum(pNtk) )
+                    continue;
+                if ( !strncmp(pObjName, "abc_reset_flop", 14) )
+                    continue;
+                fprintf( pFile, "%s@0=%c\n", pObjName, '0'+!Abc_LatchIsInit0(pObj) );
+            }
             // output PI values (while skipping the minimized ones)
             for ( f = 0; f <= pCex->iFrame; f++ )
                 Abc_NtkForEachPi( pNtk, pObj, i )
+                {
+                    // skip names with "_init" in the end
+                    int NameLen = strlen(Abc_ObjName(pObj));
+                    if ( NameLen > 5 && !strncmp(Abc_ObjName(pObj)+NameLen-5, "_init", 5) )
+                        continue;
                     if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
                         fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
+                }
             Abc_CexFreeP( &pCare );
         }
         else
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 01b6e64c..1c757bd1 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -1150,6 +1150,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
     int i, k, b, iFanin, iLit, nAndPrev, * pFans0, * pFans1, * pFans2, * pFans3;
     int nFFins = 0, nFFouts = 0, curPi = 0, curPo = 0, nFf2Regs = 0;
     int nBitCis = 0, nBitCos = 0, fAdded = 0;
+    int iFirstAddPi = -1;  // remembers the first additional PI that stands for DC-flop output
     Wlc_BstPar_t Par, * pPar = &Par;
     Wlc_BstParDefault( pPar );
     pPar = pParIn ? pParIn : pPar;
@@ -2122,9 +2123,14 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
         {
             char Buffer[100];
             sprintf( Buffer, "%s%d", "init", i );
-            Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
+            //Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
+            // save NULL at this time - to be overwritten later
+            //printf( "Adding NULL in position %d\n", Vec_PtrSize(pNew->vNamesIn) );
+            Vec_PtrPush( pNew->vNamesIn, NULL );
             fAdded = 1;
         }
+        // remember the place in the array where the first real flop is
+        iFirstAddPi = Vec_PtrSize(pNew->vNamesIn);
     }
     Wlc_NtkForEachCi( p, pObj, i )
     if ( !Wlc_ObjIsPi(pObj) )
@@ -2141,6 +2147,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
                 Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
             }
     }
+/*
     Wlc_NtkForEachFf2( p, pObj, i )
     {
         char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
@@ -2159,6 +2166,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
                 Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
             }
     }
+*/
     Wlc_NtkForEachFf2( p, pObj, i )
     {
         char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
@@ -2191,6 +2199,21 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
         }
     }
     assert( Vec_PtrSize(pNew->vNamesIn) == Gia_ManCiNum(pNew) );
+    // finish creating names of additional primary inputs
+    if ( p->pInits )
+    {
+        int Length = strlen(p->pInits);
+        assert( iFirstAddPi >= 0 );
+        for ( i = 0; i < Length; i++ )
+        if ( p->pInits[i] == 'x' || p->pInits[i] == 'X' )
+        {
+            char Buffer[1000];
+            sprintf( Buffer, "%s_init", (char *)Vec_PtrEntry(pNew->vNamesIn, iFirstAddPi+i) );
+            assert( Vec_PtrEntry(pNew->vNamesIn, iFirstAddPi-Length+i) == NULL );
+            Vec_PtrWriteEntry( pNew->vNamesIn, iFirstAddPi-Length+i, Abc_UtilStrsav(Buffer) );
+            //printf( "Replacing NULL in position %d\n", iFirstAddPi-Length+i );
+        }
+    }
     // create output names
     pNew->vNamesOut = Vec_PtrAlloc( Gia_ManCoNum(pNew) );
     Wlc_NtkForEachFf2( p, pObj, i )