Updated 'iprove' to generate seq CEX when CEC fails.

4 files changed, 34 insertions, 2 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 035f0d4c..e6d2f052 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10633,6 +10633,13 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_PrintTime( 1, "Time", clock() - clk );
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkTemp );
+    // update counter example
+    if ( RetValue == 0 && Abc_NtkLatchNum(pNtkTemp) == 0 )
+    {
+        Abc_Cex_t * pCex = Abc_CexDeriveFromCombModel( pNtkTemp->pModel, Abc_NtkPiNum(pNtkTemp), 0, iOut );
+        Abc_FrameReplaceCex( pAbc, &pCex );
+
+    }
     return 0;
 
 usage:
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 092350ca..52ac5192 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -520,8 +520,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
     pFanin = Abc_ObjFanin0(pObj);
     if ( Abc_ObjFanin0(pObj)->fPhase != (unsigned)Abc_ObjFaninC0(pObj) )
     {
-        pNtk->pModel = ABC_ALLOC( int, Abc_NtkPiNum(pNtk) );
-        memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkPiNum(pNtk) );
+        pNtk->pModel = ABC_CALLOC( int, Abc_NtkCiNum(pNtk) );
         return 0;
     }
 
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index a4cf5e33..69cd37cf 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -152,6 +152,30 @@ Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew )
 
 /**Function*************************************************************
 
+  Synopsis    [Derives CEX from comb model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int iPo )
+{
+    Abc_Cex_t * pCex;
+    int i;
+    pCex = Abc_CexAlloc( nRegs, nPis, 1 );
+    pCex->iPo = iPo;
+    pCex->iFrame = 0;
+    for ( i = 0; i < nPis; i++ )
+        if ( pModel[i] )
+            pCex->pData[i>>5] |= (1<<(i & 31));     
+    return pCex;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prints out the counter-example.]
 
   Description []
@@ -196,6 +220,7 @@ void Abc_CexFree( Abc_Cex_t * p )
     ABC_FREE( p );
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h
index f0ee57b1..dfe5050a 100644
--- a/src/misc/util/utilCex.h
+++ b/src/misc/util/utilCex.h
@@ -60,6 +60,7 @@ extern Abc_Cex_t *   Abc_CexAlloc( int nRegs, int nTruePis, int nFrames );
 extern Abc_Cex_t *   Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int iFrameOut );
 extern Abc_Cex_t *   Abc_CexCreate( int nRegs, int nTruePis, int * pArray, int iFrame, int iPo, int fSkipRegs );
 extern Abc_Cex_t *   Abc_CexDup( Abc_Cex_t * p, int nRegsNew );
+extern Abc_Cex_t *   Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int iPo );
 extern void          Abc_CexPrint( Abc_Cex_t * p );
 extern void          Abc_CexFree( Abc_Cex_t * p );