Added command 'cexcut' and 'cexmerge'.

src/aig/gia/gia.h

@@ -767,6 +767,7 @@ extern Gia_Man_t *         Gia_ManDupNormalize( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupUnnomalize( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut );
 extern Gia_Man_t *         Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 );
+extern Gia_Man_t *         Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 );
 extern Gia_Man_t *         Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits );
 extern Gia_Man_t *         Gia_ManDupDfsClasses( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );

src/aig/gia/giaDup.c

@@ -1216,6 +1216,59 @@ Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates transition relation from p1 and property from p2.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
+{
+    Gia_Man_t * pTemp, * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    // there is no flops in p2
+    assert( Gia_ManRegNum(p2) == 0 );
+    // there is only one PO in p2
+    assert( Gia_ManPoNum(p2) == 1 );
+    // flop count of p1 is equal to input count of p2
+    assert( Gia_ManRegNum(p1) == Gia_ManPiNum(p2) );
+
+    // start new AIG
+    pNew = Gia_ManStart( Gia_ManObjNum(p1)+Gia_ManObjNum(p2) );
+    pNew->pName = Abc_UtilStrsav( p1->pName );
+    pNew->pSpec = Abc_UtilStrsav( p1->pSpec );
+    Gia_ManHashAlloc( pNew );
+    // dup first AIG
+    Gia_ManConst0(p1)->Value = 0;
+    Gia_ManForEachCi( p1, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachAnd( p1, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // dup second AIG
+    Gia_ManConst0(p2)->Value = 0;
+    Gia_ManForEachPi( p2, pObj, i )
+        pObj->Value = Gia_ManRo(p1, i)->Value;
+    Gia_ManForEachAnd( p2, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // add property output
+    pObj = Gia_ManPo( p2, 0 );
+    Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    // add flop inputs
+    Gia_ManForEachRi( p1, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManHashStop( pNew );
+//    Gia_ManPrintStats( pGiaNew, 0 );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Print representatives.]
 
   Description []

src/base/abci/abc.c

@@ -365,6 +365,7 @@ static int Abc_CommandAbc9ReachY             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Undo               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Iso                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9CexMerge           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexMin             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbc9AbsDerive          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -820,6 +821,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&undo",         Abc_CommandAbc9Undo,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&iso",          Abc_CommandAbc9Iso,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmerge",     Abc_CommandAbc9CexMerge,     0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmin",       Abc_CommandAbc9CexMin,       0 );
 
     Cmd_CommandAdd( pAbc, "Abstraction",  "&abs_derive",   Abc_CommandAbc9AbsDerive,    0 );
@@ -28661,7 +28663,7 @@ int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
     {
-        Abc_Print( 1, "Current counter-example is not a valid counter-example for &-space AIG \"%s\".\n", Gia_ManName(pAbc->pGia) );
+        Abc_Print( 1, "Current CEX does not fail AIG \"%s\" in the &-space.\n", Gia_ManName(pAbc->pGia) );
         return 0;
     }
     if ( iFrStop == ABC_INFINITY )
@@ -28681,7 +28683,100 @@ usage:
     Abc_Print( -2, "\t         extract logic representation of bad states\n" );
     Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart );
     Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n",   iFrStop );
-    Abc_Print( -2, "\t-v     : toggle printing optimization summary [default = %s]\n", fVerbose? "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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9CexMerge( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Cex_t * pCexNew;
+    int c;
+    int iFrStart = 0;
+    int iFrStop  = ABC_INFINITY;
+    int fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FGvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            iFrStart = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( iFrStart < 0 )
+                goto usage;
+            break;
+        case 'G':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            iFrStop = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( iFrStop < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            Abc_Print( -2, "Unknown switch.\n");
+            goto usage;
+        }
+    }
+
+    if ( pAbc->pCex == NULL )
+    {
+        Abc_Print( 1, "There is no current cex.\n");
+        return 0;
+    }
+    if ( pAbc->pCex2 == NULL )
+    {
+        Abc_Print( 1, "There is no saved cex.\n");
+        return 0;
+    }
+    if ( iFrStop - iFrStart > pAbc->pCex->iFrame )
+    {
+        Abc_Print( 1, "Current CEX does not allow to shorten the saved CEX.\n");
+        return 0;
+    }
+    pCexNew = Abc_CexMerge( pAbc->pCex2, pAbc->pCex, iFrStart, iFrStop );
+    if ( pCexNew == NULL )
+    {
+        Abc_Print( 1, "Merging CEXes has failed.\n");
+        return 0;
+    }
+    // replace the saved CEX
+    ABC_FREE( pAbc->pCex2 );
+    pAbc->pCex2 = pCexNew;
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &cexmerge [-FG num] [-vh]\n" );
+    Abc_Print( -2, "\t         merges the current CEX into the saved one\n" );
+    Abc_Print( -2, "\t         and sets the resulting CEX as the saved one\n" );
+    Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart );
+    Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n",   iFrStop );
+    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;
 }

src/misc/util/utilCex.c

@@ -172,6 +172,64 @@ Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int i
 
 /**Function*************************************************************
 
+  Synopsis    [Derives CEX from comb model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int iFrEnd )
+{
+    Abc_Cex_t * pNew;
+    int nFramesGain;
+    int i, f, iBit;
+
+    if ( iFrBeg < 0 )
+        { printf( "Starting frame is less than 0.\n" ); return NULL; }
+    if ( iFrEnd < 0 )
+        { printf( "Stopping frame is less than 0.\n" ); return NULL; }
+    if ( iFrBeg > pCex->iFrame )
+        { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
+    if ( iFrEnd > pCex->iFrame )
+        { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
+    if ( iFrBeg >= iFrEnd )
+        { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; }
+    assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame );
+    assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame );
+    assert( iFrBeg < iFrEnd );
+
+    assert( pCex->nPis == pPart->nPis );
+    assert( iFrEnd - iFrBeg > pPart->iFrame );
+
+    nFramesGain = (iFrEnd - iFrBeg) - pPart->iFrame;
+    pNew = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 - nFramesGain );
+    pNew->iPo    = pCex->iPo;
+    pNew->iFrame = pCex->iFrame - nFramesGain;
+
+    for ( iBit = 0; iBit < pCex->nRegs; iBit++ )
+        if ( Abc_InfoHasBit(pCex->pData, iBit) )
+            Abc_InfoSetBit( pNew->pData, iBit++ );
+    for ( f = 0; f < iFrBeg; f++ )
+        for ( i = 0; i < pCex->nPis; i++ )
+            if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
+                Abc_InfoSetBit( pNew->pData, iBit++ );
+    for ( f = 0; f < pPart->iFrame; f++ )
+        for ( i = 0; i < pCex->nPis; i++ )
+            if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) )
+                Abc_InfoSetBit( pNew->pData, iBit++ );
+    for ( f = iFrEnd; f <= pCex->iFrame; f++ )
+        for ( i = 0; i < pCex->nPis; i++ )
+            if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) )
+                Abc_InfoSetBit( pNew->pData, iBit++ );
+    assert( iBit == pNew->nBits );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prints out the counter-example.]
 
   Description []

src/misc/util/utilCex.h

@@ -61,6 +61,7 @@ extern Abc_Cex_t *   Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int
 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 Abc_Cex_t *   Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int iFrEnd );
 extern void          Abc_CexPrintStats( Abc_Cex_t * p );
 extern void          Abc_CexPrint( Abc_Cex_t * p );
 extern void          Abc_CexFreeP( Abc_Cex_t ** p );

src/sat/bmc/bmcCexCut.c

@@ -42,9 +42,109 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd )
+Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose )
 {
-    return NULL;
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    Vec_Bit_t * vInitNew;
+    int i, k, iBit = 0;
+
+    if ( iFrBeg < 0 )
+        { printf( "Starting frame is less than 0.\n" ); return NULL; }
+    if ( iFrEnd < 0 )
+        { printf( "Stopping frame is less than 0.\n" ); return NULL; }
+    if ( iFrBeg > pCex->iFrame )
+        { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
+    if ( iFrEnd > pCex->iFrame )
+        { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
+    if ( iFrBeg >= iFrEnd )
+        { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; }
+    assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame );
+    assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame );
+    assert( iFrBeg < iFrEnd );
+
+    // skip trough the first iFrEnd frames
+    Gia_ManCleanMark0(p);
+    Gia_ManForEachRo( p, pObj, i )
+        pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+    vInitNew = Vec_BitStart( Gia_ManRegNum(p) );
+    for ( i = 0; i < iFrEnd; i++ )
+    {
+        // remember values in frame iFrBeg
+        if ( i == iFrBeg )
+            Gia_ManForEachRo( p, pObjRo, k )
+                if ( pObjRo->fMark0 )
+                    Vec_BitWriteEntry( vInitNew, k, 1 );
+        // simulate other values
+        Gia_ManForEachPi( p, pObj, k )
+            pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+        Gia_ManForEachAnd( p, pObj, k )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachCo( p, pObj, k )
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+            pObjRo->fMark0 = pObjRi->fMark0;
+    }
+    assert( i == iFrEnd );
+
+    // create new AIG manager
+    pNew = Gia_ManStart( 10000 );
+    Gia_ManConst0(p)->Value = 1;
+    Gia_ManForEachPi( p, pObj, k )
+        pObj->Value = 1;
+    Gia_ManForEachRo( p, pObjRo, i )
+        pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObjRo->fMark0 );
+    Gia_ManHashStart( p );
+    for ( i = iFrEnd; i <= pCex->iFrame; i++ )
+    {
+        Gia_ManForEachPi( p, pObj, k )
+            pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+        Gia_ManForEachAnd( p, pObj, k )
+        {
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+            if ( pObj->fMark0 )
+                pObj->Value = Gia_ManHashAnd( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+            else if ( !Gia_ObjFanin0(pObj)->fMark0 && !Gia_ObjFanin1(pObj)->fMark0 )
+                pObj->Value = Gia_ManHashOr( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+            else if ( !Gia_ObjFanin0(pObj)->fMark0 )
+                pObj->Value = Gia_ObjFanin0(pObj)->Value;
+            else if ( !Gia_ObjFanin1(pObj)->fMark0 )
+                pObj->Value = Gia_ObjFanin1(pObj)->Value;
+            else assert( 0 );
+        }
+        Gia_ManForEachCo( p, pObj, k )
+        {
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+            pObj->Value = Gia_ObjFanin0(pObj)->Value;
+        }
+        if ( i == pCex->iFrame )
+            break;
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+        {
+            pObjRo->fMark0 = pObjRi->fMark0;
+            pObjRo->Value = pObjRi->Value;
+        }
+    }
+    Gia_ManHashStop( p );
+    assert( iBit == pCex->nBits );
+
+    // create PO
+    Gia_ManAppendCo( pNew, Gia_ManPo(p, pCex->iPo)->Value );
+    // cleanup
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+
+    // create new GIA
+    pNew = Gia_ManDupWithNewPo( p, pTemp = pNew ); 
+    Gia_ManStop( pTemp );
+
+    // create new initial state
+    pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) );
+    Gia_ManStop( pTemp );
+    Vec_BitFree( vInitNew );
+    return pNew;
 }
 
 ////////////////////////////////////////////////////////////////////////