Added generation of counter-examples to induction in 'ind'.

src/aig/cec/cecSeq.c

@@ -49,21 +49,20 @@ void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t
     assert( pCex->nBits == pCex->nRegs + pCex->nPis * (pCex->iFrame + 1) );
     assert( pCex->nBits - pCex->nRegs + Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) );
     nWords = Vec_PtrReadWordsSimInfo( vInfo );
-/*
     for ( k = 0; k < pCex->nRegs; k++ )
     {
-        pInfo = Vec_PtrEntry( vInfo, k );
+        pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
         for ( w = 0; w < nWords; w++ )
             pInfo[w] = Gia_InfoHasBit( pCex->pData, k )? ~0 : 0;
     }
-*/
+/*
     for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
     {
         pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
         for ( w = 0; w < nWords; w++ )
             pInfo[w] = 0;
     }
-
+*/
     for ( i = pCex->nRegs; i < pCex->nBits; i++ )
     {
         pInfo = (unsigned *)Vec_PtrEntry( vInfo, k++ );

src/aig/saig/saig.h

@@ -163,7 +163,7 @@ extern int               Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t *
 /*=== saigHaig.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
 /*=== saigInd.c ==========================================================*/
-extern int               Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fVerbose, int fVeryVerbose );
+extern int               Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose );
 /*=== saigIoa.c ==========================================================*/
 extern void              Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );

src/aig/saig/saigInd.c

@@ -142,12 +142,12 @@ void Saig_ManAddUniqueness( sat_solver * pSat, Vec_Int_t * vState, int nRegs, in
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fVerbose, int fVeryVerbose )
+int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
 {
     sat_solver * pSat;
     Aig_Man_t * pAigPart;
     Cnf_Dat_t * pCnfPart;
-    Vec_Int_t * vTopVarNums, * vState;
+    Vec_Int_t * vTopVarNums, * vState, * vTopVarIds = NULL;
     Vec_Ptr_t * vTop, * vBot;
     Aig_Obj_t * pObjPi, * pObjPiCopy, * pObjPo;
     int i, k, f, clk, Lits[2], status, RetValue, nSatVarNum, nConfPrev;
@@ -190,6 +190,24 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique,
         nSatVarNum += pCnfPart->nVars;
         nClauses   += pCnfPart->nClauses;
 
+        // remember top frame var IDs
+        if ( fGetCex && vTopVarIds == NULL )
+        {
+            vTopVarIds = Vec_IntStartFull( Aig_ManPiNum(p) );
+            Aig_ManForEachPi( p, pObjPi, i )
+            {
+                if ( pObjPi->pData == NULL )
+                    continue;
+                pObjPiCopy = (Aig_Obj_t *)pObjPi->pData;
+                assert( Aig_ObjIsPi(pObjPiCopy) );
+                if ( Saig_ObjIsPi(p, pObjPi) )
+                    Vec_IntWriteEntry( vTopVarIds, Aig_ObjPioNum(pObjPi) + Saig_ManRegNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] );
+                else if ( Saig_ObjIsLo(p, pObjPi) )
+                    Vec_IntWriteEntry( vTopVarIds, Aig_ObjPioNum(pObjPi) - Saig_ManPiNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] );
+                else assert( 0 );
+            }
+        }
+
         // stitch variables of top and bot
         assert( Aig_ManPoNum(pAigPart)-1 == Vec_IntSize(vTopVarNums) );
         Aig_ManForEachPo( pAigPart, pObjPo, i )
@@ -294,7 +312,27 @@ nextrun:
             printf( "\n" );
         }
         if ( f == nFramesMax - 1 )
+        {
+            // derive counter-example
+            assert( status == l_True );
+            if ( fGetCex )
+            {
+                int VarNum, iBit = 0;
+                Abc_Cex_t * pCex = Abc_CexAlloc( Aig_ManRegNum(p)-1, Saig_ManPiNum(p), 1 );
+                pCex->iFrame = 0;
+                pCex->iPo = 0;
+                Vec_IntForEachEntryStart( vTopVarIds, VarNum, i, 1 )
+                {
+                    if ( VarNum >= 0 && sat_solver_var_value( pSat, VarNum ) )
+                        Aig_InfoSetBit( pCex->pData, iBit );
+                    iBit++;
+                }
+                assert( iBit == pCex->nBits );
+                Abc_CexFree( p->pSeqModel );
+                p->pSeqModel = pCex;
+            }
             break;
+        }
         if ( fUnique )
         {
             for ( i = 1; i < iLast; i++ )
@@ -333,6 +371,7 @@ nextrun:
     Vec_PtrFree( vTop );
     Vec_PtrFree( vBot );
     Vec_IntFree( vState );
+    Vec_IntFreeP( &vTopVarIds );
     return RetValue;
 }
 

src/base/abci/abc.c

@@ -19546,19 +19546,21 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nConfMax;
     int fUnique;
     int fUniqueAll;
+    int fGetCex;
     int fVerbose;
     int fVeryVerbose;
     int c;
-    extern int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fVerbose, int fVeryVerbose );
+    extern int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose );
     // set defaults
     nFramesMax   =   100;
     nConfMax     =  1000;
     fUnique      =     0;
     fUniqueAll   =     0;
+    fGetCex      =     0;
     fVerbose     =     0;
     fVeryVerbose =     0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCuavwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCuaxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -19590,6 +19592,9 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             fUniqueAll ^= 1;
             break;
+        case 'x':
+            fGetCex ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -19629,15 +19634,21 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    pAbc->Status = Abc_NtkDarInduction( pNtk, nFramesMax, nConfMax, fUnique, fUniqueAll, fVerbose, fVeryVerbose );
+    pAbc->Status = Abc_NtkDarInduction( pNtk, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
+    if ( fGetCex )
+    {
+        Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
+        printf( "The current CEX in ABC is set to be the CEX to induction.\n" );
+    }
     return 0;
 usage:
-    Abc_Print( -2, "usage: ind [-FC num] [-uavwh]\n" );
+    Abc_Print( -2, "usage: ind [-FC num] [-uaxvwh]\n" );
     Abc_Print( -2, "\t         runs the inductive case of the K-step induction\n" );
     Abc_Print( -2, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
     Abc_Print( -2, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
     Abc_Print( -2, "\t-u     : toggle adding uniqueness constraints on demand [default = %s]\n", fUnique? "yes": "no" );
     Abc_Print( -2, "\t-a     : toggle adding uniqueness constraints always [default = %s]\n", fUniqueAll? "yes": "no" );
+    Abc_Print( -2, "\t-x     : toggle returning CEX to induction for the top frame [default = %s]\n", fGetCex? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing additional verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");

src/base/abci/abcDar.c

@@ -3151,16 +3151,15 @@ Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nC
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fVerbose, int fVeryVerbose )
+int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
 { 
-    Aig_Man_t * pMan, * pTemp;
+    Aig_Man_t * pMan;
     int clkTotal = clock();
     int RetValue;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return -1;
-    RetValue = Saig_ManInduction( pTemp = pMan, nFramesMax, nConfMax, fUnique, fUniqueAll, fVerbose, fVeryVerbose );
-    Aig_ManStop( pTemp );
+    RetValue = Saig_ManInduction( pMan, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
     if ( RetValue == 1 )
     {
         printf( "Networks are equivalent.   " );
@@ -3176,6 +3175,13 @@ ABC_PRT( "Time", clock() - clkTotal );
         printf( "Networks are UNDECIDED.   " );
 ABC_PRT( "Time", clock() - clkTotal );
     }
+    if ( fGetCex )
+    {
+        ABC_FREE( pNtk->pModel );
+        ABC_FREE( pNtk->pSeqModel );
+        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
+    }
+    Aig_ManStop( pMan );
     return RetValue;
 }