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

5 files changed, 44 insertions, 13 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 0f282e28..70fda8d4 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -762,6 +762,18 @@ static inline void Gia_AigerWriteUnsigned( Vec_Str_t * vStr, unsigned x )
     ch = x;
     Vec_StrPush( vStr, ch );
 }
+static inline void Gia_AigerWriteUnsignedFile( FILE * pFile, unsigned x )
+{
+    unsigned char ch;
+    while (x & ~0x7f)
+    {
+        ch = (x & 0x7f) | 0x80;
+        fputc( ch, pFile );
+        x >>= 7;
+    }
+    ch = x;
+    fputc( ch, pFile );
+}
 static inline int Gia_AigerWriteUnsignedBuffer( unsigned char * pBuffer, int Pos, unsigned x )
 {
     unsigned char ch;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c3c8925f..266df256 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -12547,7 +12547,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandSendStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex );
+    extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
     int c;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "" ) ) != EOF )
@@ -12570,7 +12570,7 @@ int Abc_CommandSendStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Status is \"sat\", but current CEX is not available.\n" );
         return 1;
     }
-    Gia_ManToBridgeResult( stdout, pAbc->Status, pAbc->pCex );
+    Gia_ManToBridgeResult( stdout, pAbc->Status, pAbc->pCex, 0 );
     return 0;
 
 usage:
@@ -23754,6 +23754,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     // run the procedure
+    pPars->fUseBridge = pAbc->fBatchMode;
     pAbc->Status  = Abc_NtkDarPdr( pNtk, pPars );
     pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame;
     Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap );
diff --git a/src/misc/util/utilBridge.c b/src/misc/util/utilBridge.c
index 96e41d5b..6279b98b 100644
--- a/src/misc/util/utilBridge.c
+++ b/src/misc/util/utilBridge.c
@@ -191,7 +191,7 @@ int Gia_ManToBridgeBadAbs( FILE * pFile )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManFromBridgeHolds( FILE * pFile )
+void Gia_ManFromBridgeHolds( FILE * pFile, int iPoProved )
 {
     fprintf( pFile, "%.6d", 101 /*message type = Result*/);
     fprintf( pFile, " " );
@@ -200,11 +200,12 @@ void Gia_ManFromBridgeHolds( FILE * pFile )
 
     fputc( (char)BRIDGE_VALUE_1, pFile ); // true
     fputc( (char)1, pFile ); // size of vector (Armin's encoding)
-    fputc( (char)0, pFile ); // number of the property (Armin's encoding)
+//    fputc( (char)0, pFile ); // number of the property (Armin's encoding)
+    Gia_AigerWriteUnsignedFile( pFile, iPoProved ); // number of the property (Armin's encoding)
     fputc( (char)0, pFile ); // no invariant
     fflush(pFile);
 }
-void Gia_ManFromBridgeUnknown( FILE * pFile )
+void Gia_ManFromBridgeUnknown( FILE * pFile, int iPoProved )
 {
     fprintf( pFile, "%.6d", 101 /*message type = Result*/);
     fprintf( pFile, " " );
@@ -213,7 +214,8 @@ void Gia_ManFromBridgeUnknown( FILE * pFile )
 
     fputc( (char)BRIDGE_VALUE_X, pFile ); // undef
     fputc( (char)1, pFile ); // size of vector (Armin's encoding)
-    fputc( (char)0, pFile ); // number of the property (Armin's encoding)
+//    fputc( (char)0, pFile ); // number of the property (Armin's encoding)
+    Gia_AigerWriteUnsignedFile( pFile, iPoProved ); // number of the property (Armin's encoding)
     fflush(pFile);
 }
 void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
@@ -222,7 +224,8 @@ void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
     Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
     Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // false
     Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
-    Vec_StrPush( vStr, (char)0 ); // number of the property (Armin's encoding)
+//    Vec_StrPush( vStr, (char)0 ); // number of the property (Armin's encoding)
+    Gia_AigerWriteUnsigned( vStr, pCex->iPo ); // number of the property (Armin's encoding)
     Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
     Gia_AigerWriteUnsigned( vStr, pCex->iFrame ); // depth
 
@@ -246,14 +249,14 @@ void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
     Vec_StrFree( vStr );
     fflush(pFile);
 }
-int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex )
+int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved )
 {
     if ( Result == 0 ) // sat
         Gia_ManFromBridgeCex( pFile, pCex );
     else if ( Result == 1 ) // unsat
-        Gia_ManFromBridgeHolds( pFile );
+        Gia_ManFromBridgeHolds( pFile, iPoProved );
     else if ( Result == -1 ) // undef
-        Gia_ManFromBridgeUnknown( pFile );
+        Gia_ManFromBridgeUnknown( pFile, iPoProved );
     else assert( 0 );
     return 1;
 }
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index f32fe0b3..83c71b1d 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -59,6 +59,7 @@ struct Pdr_Par_t_
     int fSilent;          // totally silent execution
     int fSolveAll;        // do not stop when found a SAT output
     int fStoreCex;        // enable storing counter-examples in MO mode
+    int fUseBridge;       // use bridge interface
     int nFailOuts;        // the number of failed outputs
     int nDropOuts;        // the number of timed out outputs
     int nProveOuts;       // the number of proved outputs
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 16af76fd..6d2f1c43 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -27,6 +27,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -574,6 +576,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
     int fPrintClauses = 0;
     Pdr_Set_t * pCube = NULL;
     Aig_Obj_t * pObj;
+    Abc_Cex_t * pCexNew;
     int k, RetValue = -1;
     int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
     abctime clkStart = Abc_Clock(), clkOne = 0;
@@ -603,15 +606,19 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             {
                 if ( !p->pPars->fSolveAll )
                 {
-                    p->pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur );
+                    pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur );
+                    p->pAig->pSeqModel = pCexNew;
                     return 0; // SAT
                 }
+                pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
                 p->pPars->nFailOuts++;
                 if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
                 Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",  
                     nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
                 assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
-                Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 );
+                if ( p->pPars->fUseBridge )
+                    Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
+                Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
                 if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
                 {
                     if ( p->pPars->fVerbose ) 
@@ -709,9 +716,12 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                             return 0; // SAT
                         }
                         p->pPars->nFailOuts++;
+                        pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
                         if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
                         assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
-                        Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 );
+                        if ( p->pPars->fUseBridge )
+                            Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
+                        Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
                         if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
                         {
                             if ( p->pPars->fVerbose ) 
@@ -794,7 +804,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             if ( p->pPars->vOutMap )
                 for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ )
                     if ( Vec_IntEntry(p->pPars->vOutMap, k) == -2 ) // unknown
+                    {
                         Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat
+                        if ( p->pPars->fUseBridge )
+                            Gia_ManToBridgeResult( stdout, 1, NULL, k );
+                    }
             if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
                 return 1; // UNSAT
             if ( p->pPars->nFailOuts > 0 )