Adding procedures to find the care bits of a counter-example (update).

src/aig/saig/saig.h

@@ -176,7 +176,8 @@ extern Aig_Man_t *       Saig_ManDecPropertyOutput( Aig_Man_t * pAig, int nLits,
 /*=== saigPhase.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose );
 /*=== saigRefSat.c ==========================================================*/
-extern Abc_Cex_t *       Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
+extern Vec_Int_t *       Saig_ManExtendCounterExampleTest3( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
+extern Abc_Cex_t *       Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose );
 /*=== saigRetFwd.c ==========================================================*/
 extern void              Saig_ManMarkAutonomous( Aig_Man_t * p );
 extern Aig_Man_t *       Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose );
@@ -192,6 +193,7 @@ extern Vec_Int_t *       Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirst
 extern Vec_Int_t *       Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fTryFour, int fVerbose );
 /*=== saigSimExt.c ==========================================================*/
 extern Vec_Int_t *       Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose );
+extern Abc_Cex_t *       Saig_ManFindCexCareBitsSense( Aig_Man_t * p, Abc_Cex_t * pCex, int iFirstFlopPi, int fVerbose );
 /*=== saigSimMv.c ==========================================================*/
 extern int               Saig_MvManSimulate( Aig_Man_t * pAig, int fVerbose );
 /*=== saigStrSim.c ==========================================================*/

src/aig/saig/saigAbs.c

@@ -225,7 +225,8 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
         return NULL;
     if ( pnUseStart )
         *pnUseStart = pAbs->pSeqModel->iFrame;
-    vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, 1, fVerbose );
+//    vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, 1, fVerbose );
+    vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, fVerbose );
     if ( vFlopsNew == NULL )
         return NULL;
     if ( Vec_IntSize(vFlopsNew) == 0 )
@@ -238,7 +239,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
     }
     // vFlopsNew contains PI numbers that should be kept in pAbs
     if ( fVerbose )
-        printf( "Adding %d registers to the abstraction.\n", Vec_IntSize(vFlopsNew) );
+        printf( "Adding %d registers to the abstraction.\n\n", Vec_IntSize(vFlopsNew) );
     // add to the abstraction
     Vec_IntForEachEntry( vFlopsNew, Entry, i )
     {
@@ -276,7 +277,8 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex,
     if ( fSensePath )
         vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
     else
-        vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fTryFour, fVerbose );
+//        vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fTryFour, fVerbose );
+        vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
     if ( vFlopsNew == NULL )
     {
         Aig_ManStop( pAbs );

src/aig/saig/saigSimExt2.c

@@ -360,6 +360,118 @@ ABC_PRT( "Time", clock() - clk );
     return vRes;
 }
 
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of PIs for flops that should not be absracted.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Saig_ManDeriveCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
+{
+    Abc_Cex_t * pCare;
+    Aig_Obj_t * pObj;
+    Vec_Int_t * vRes, * vResInv;
+    int i, f, Value;
+//    assert( Aig_ManRegNum(p) > 0 );
+    assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) );
+    // start simulation data
+    Value = Saig_ManSimDataInit2( p, pCex, vSimInfo );
+    assert( Value == SAIG_ONE_NEW );
+    // derive implications of constants and primary inputs
+    Saig_ManForEachLo( p, pObj, i )
+        Saig_ManSetAndDriveImplications_rec( p, pObj, 0, pCex->iFrame, vSimInfo );
+    for ( f = pCex->iFrame; f >= 0; f-- )
+    {
+        Saig_ManSetAndDriveImplications_rec( p, Aig_ManConst1(p), f, pCex->iFrame, vSimInfo );
+        for ( i = 0; i < iFirstFlopPi; i++ )
+            Saig_ManSetAndDriveImplications_rec( p, Aig_ManPi(p, i), f, pCex->iFrame, vSimInfo );
+    }
+    // recursively compute justification
+    Saig_ManExplorePaths_rec( p, Aig_ManPo(p, pCex->iPo), pCex->iFrame, pCex->iFrame, vSimInfo );
+
+    // create CEX
+    pCare = Abc_CexDup( pCex, pCex->nRegs );
+    memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) );
+
+    // select the result
+    vRes = Vec_IntAlloc( 1000 );
+    vResInv = Vec_IntAlloc( 1000 );
+    for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ )
+    {
+        int fFound = 0;
+        for ( f = pCex->iFrame; f >= 0; f-- )
+        {
+            Value = Saig_ManSimInfo2Get( vSimInfo, Aig_ManPi(p, i), f );
+            if ( Saig_ManSimInfo2IsOld( Value ) )
+            {
+                fFound = 1;
+                Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * f + i );
+            }
+        }
+        if ( fFound )
+            Vec_IntPush( vRes, i );
+        else
+            Vec_IntPush( vResInv, i );
+    }
+    // resimulate to make sure it is valid
+    Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv );
+    assert( Value == SAIG_ONE );
+    Vec_IntFree( vResInv );
+    Vec_IntFree( vRes );
+
+    return pCare;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of PIs for flops that should not be absracted.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Saig_ManFindCexCareBitsSense( Aig_Man_t * p, Abc_Cex_t * pCex, int iFirstFlopPi, int fVerbose )
+{
+    Abc_Cex_t * pCare;
+    Vec_Ptr_t * vSimInfo;
+    int clk;
+    if ( Saig_ManPiNum(p) != pCex->nPis )
+    {
+        printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
+            Aig_ManPiNum(p), pCex->nPis );
+        return NULL;
+    }
+    Aig_ManFanoutStart( p );
+    vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Aig_BitWordNum(2*(pCex->iFrame+1)) );
+    Vec_PtrCleanSimInfo( vSimInfo, 0, Aig_BitWordNum(2*(pCex->iFrame+1)) );
+
+clk = clock();
+    pCare = Saig_ManDeriveCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
+    if ( fVerbose )
+    {
+//        printf( "Total new PIs = %3d. Non-removable PIs = %3d.  ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) );
+Abc_CexPrintStats( pCex );
+Abc_CexPrintStats( pCare );
+ABC_PRT( "Time", clock() - clk );
+    }
+
+    Vec_PtrFree( vSimInfo );
+    Aig_ManFanoutStop( p );
+    return pCare;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abc.c

@@ -8626,11 +8626,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nLeafMax     = 10;
     int nDivMax      = 50;
     int nDecMax      =  3;
+    int fNewAlgo     =  0;
+    int fNewOrder    =  0;
     int fVerbose     =  0;
     int fVeryVerbose =  0;
     int c;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CKDNvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CKDNaovwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -8678,6 +8680,12 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nDecMax < 0 ) 
                 goto usage;
             break;
+        case 'a':
+            fNewAlgo ^= 1;
+            break;
+        case 'o':
+            fNewOrder ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -8770,7 +8778,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Abc_Cex_t * pNew;
         Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
-        pNew = Saig_ManFindCexCareBits( pAig, pAbc->pCex, 0, 0 );
+        if ( fNewAlgo )
+            pNew = Saig_ManFindCexCareBitsSense( pAig, pAbc->pCex, 0, fVerbose );
+        else
+            pNew = Saig_ManFindCexCareBits( pAig, pAbc->pCex, 0, fNewOrder, fVerbose );
         Aig_ManStop( pAig );
         Abc_FrameReplaceCex( pAbc, &pNew );
     }
@@ -8779,12 +8790,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     return 0;
 usage:
-    Abc_Print( -2, "usage: test [-CKDN] [-vwh] <file_name>\n" );
+    Abc_Print( -2, "usage: test [-CKDN] [-aovwh] <file_name>\n" );
     Abc_Print( -2, "\t         testbench for new procedures\n" );
     Abc_Print( -2, "\t-C num : the max number of cuts [default = %d]\n", nCutMax );
     Abc_Print( -2, "\t-K num : the max number of leaves [default = %d]\n", nLeafMax );
     Abc_Print( -2, "\t-D num : the max number of divisors [default = %d]\n", nDivMax );
     Abc_Print( -2, "\t-N num : the max number of node inputs [default = %d]\n", nDecMax );
+    Abc_Print( -2, "\t-a     : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes": "no" );
+    Abc_Print( -2, "\t-o     : toggle using new ordering [default = %s]\n", fNewOrder? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");