Added switches '-c' and '-n' to 'init'.

3 files changed, 113 insertions, 13 deletions

diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index cd978717..dabdf539 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -315,6 +315,70 @@ int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Saig_ManVerifyCexNoClear( Aig_Man_t * pAig, Abc_Cex_t * p )
+{
+    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    Aig_ManCleanMarkB(pAig);
+    Aig_ManConst1(pAig)->fMarkB = 1;
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Saig_ManForEachPi( pAig, pObj, k )
+            pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
+        Aig_ManForEachNode( pAig, pObj, k )
+            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
+                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+        Aig_ManForEachCo( pAig, pObj, k )
+            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+        if ( i == p->iFrame )
+            break;
+        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
+            pObjRo->fMarkB = pObjRi->fMarkB;
+    }
+    assert( iBit == p->nBits );
+    RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
+    //Aig_ManCleanMarkB(pAig);
+    return RetValue;
+}
+Vec_Int_t * Saig_ManReturnFailingState( Aig_Man_t * pAig, Abc_Cex_t * p, int fNextOne )
+{
+    Aig_Obj_t * pObj;
+    Vec_Int_t * vState;
+    int i, RetValue = Saig_ManVerifyCexNoClear( pAig, p );
+    if ( RetValue == 0 )
+    {
+        Aig_ManCleanMarkB(pAig);
+        printf( "CEX does fail the given sequential miter.\n" );
+        return NULL;
+    }
+    vState = Vec_IntAlloc( Aig_ManRegNum(pAig) );
+    if ( fNextOne )
+    {
+        Saig_ManForEachLi( pAig, pObj, i )
+            Vec_IntPush( vState, pObj->fMarkB );
+    }
+    else
+    {
+        Saig_ManForEachLo( pAig, pObj, i )
+            Vec_IntPush( vState, pObj->fMarkB );
+    }
+    Aig_ManCleanMarkB(pAig);
+    return vState;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p )
 {
     Abc_Cex_t * pNew;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1f10be14..37d96dcc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -16493,20 +16493,17 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     Abc_Obj_t * pObj;
+    char * pInitStr = NULL;
+    int fZeros    = 0;
+    int fOnes     = 0;
+    int fRandom   = 0;
+    int fDontCare = 0;
+    int fUseCexCs = 0;
+    int fUseCexNs = 0;
     int c, i;
-    int fZeros;
-    int fOnes;
-    int fRandom;
-    int fDontCare;
-    char * pInitStr;
     // set defaults
-    fZeros    = 0;
-    fOnes     = 0;
-    fRandom   = 0;
-    fDontCare = 0;
-    pInitStr  = NULL;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Szordh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Szordcnh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -16531,6 +16528,12 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             fDontCare ^= 1;
             break;
+        case 'c':
+            fUseCexCs ^= 1;
+            break;
+        case 'n':
+            fUseCexNs ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -16591,17 +16594,50 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_NtkForEachLatch( pNtk, pObj, i )
             Abc_LatchSetInitDc( pObj );
     }
+    else if ( fUseCexCs || fUseCexNs )
+    {
+        extern Vec_Int_t * Saig_ManReturnFailingState( Aig_Man_t * pMan, Abc_Cex_t * p, int fNextOne );
+        Aig_Man_t * pMan;
+        Vec_Int_t * vFailState;
+        if ( fUseCexCs && fUseCexNs )
+        {
+            Abc_Print( -1, "The two options (-c and -n) are incompatible.\n" );
+            return 0;
+        }
+        if ( !Abc_NtkIsStrash(pNtk) )
+        {
+            Abc_Print( -1, "The current network should be an AIG.\n" );
+            return 0;
+        }
+        if ( pAbc->pCex == NULL )
+        {
+            Abc_Print( -1, "The current CEX is not available.\n" );
+            return 0;
+        }
+        pMan = Abc_NtkToDar( pNtk, 0, 1 );
+        vFailState = Saig_ManReturnFailingState( pMan, pAbc->pCex, fUseCexNs );
+        //Vec_IntPrint( vFailState );
+        Aig_ManStop( pMan );
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            if ( Vec_IntEntry( vFailState, i ) )
+                Abc_LatchSetInit1( pObj );
+            else
+                Abc_LatchSetInit0( pObj );
+        Vec_IntFree( vFailState );
+    }
     else
         Abc_Print( -1, "The initial states remain unchanged.\n" );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: init [-zordh] [-S <init_string>]\n" );
+    Abc_Print( -2, "usage: init [-zordcnh] [-S <init_string>]\n" );
     Abc_Print( -2, "\t         resets initial states of all latches\n" );
     Abc_Print( -2, "\t-z     : set zeros initial states [default = %s]\n", fZeros? "yes": "no" );
     Abc_Print( -2, "\t-o     : set ones initial states [default = %s]\n", fOnes? "yes": "no" );
     Abc_Print( -2, "\t-d     : set don't-care initial states [default = %s]\n", fDontCare? "yes": "no" );
     Abc_Print( -2, "\t-r     : set random initial states [default = %s]\n", fRandom? "yes": "no" );
+    Abc_Print( -2, "\t-c     : set failure current state from the CEX (and run \"zero\") [default = %s]\n", fUseCexCs? "yes": "no" );
+    Abc_Print( -2, "\t-n     : set next state after failure from the CEX (and run \"zero\") [default = %s]\n", fUseCexNs? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\t-S str : (optional) initial state  [default = unused]\n" );
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 1214e7b2..d2b74beb 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2307,7 +2307,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
                     if ( pPars->nDropOuts )
                         Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
                 }
-                Abc_Print( 1, " after %d frames", pPars->iFrame );
+                Abc_Print( 1, " after %d frames", pPars->iFrame+2 );
                 Abc_Print( 1, ".   " );
             }
         }