Added bridge integration for multi-output 'bmc3 -a'.

src/base/abci/abc.c

@@ -21901,6 +21901,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Constraints have to be folded (use \"fold\").\n" );
         return 0;
     }
+    pPars->fUseBridge = pAbc->fBridgeMode;
     pAbc->Status = Abc_NtkDarBmc3( pNtk, pPars, fOrDecomp );
     pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame;
     if ( pLogFileName )

src/sat/bmc/bmc.h

@@ -56,6 +56,7 @@ struct Saig_ParBmc_t_
     int         nPisAbstract;   // the number of PIs to abstract
     int         fSolveAll;      // does not stop at the first SAT output
     int         fStoreCex;      // enable storing CEXes in the MO mode
+    int         fUseBridge;     // use bridge interface
     int         fDropSatOuts;   // replace sat outputs by constant 0
     int         nFfToAddMax;    // max number of flops to add during CBA
     int         fSkipRand;      // skip random decisions

src/sat/bmc/bmcBmc3.c

@@ -64,6 +64,8 @@ struct Gia_ManBmc_t_
     char * pSopSizes, ** pSops;    // CNF representation
 };
 
+extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -1424,6 +1426,11 @@ clkOther += Abc_Clock() - clk2;
                         nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
+                if ( p->pPars->fUseBridge )
+                {
+                    Abc_Cex_t * pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
+                    Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
+                }
                 Vec_PtrWriteEntry( p->vCexes, i, pPars->fStoreCex ? Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ) : (void *)(ABC_PTRINT_T)1 );
                 if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) )
                 {
@@ -1514,6 +1521,11 @@ nTimeSat += Abc_Clock() - clk2;
                         nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
+                if ( p->pPars->fUseBridge )
+                {
+                    Abc_Cex_t * pCexNew = Saig_ManGenerateCex( p, f, i );
+                    Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
+                }
                 Vec_PtrWriteEntry( p->vCexes, i, pPars->fStoreCex? Saig_ManGenerateCex( p, f, i ) : (void *)(ABC_PTRINT_T)1 );
                 if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) )
                 {