Adding &sat -x to save CEXes for multi-output combinational miters.

4 files changed, 56 insertions, 4 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 31f3e270..db8bacf2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -655,6 +655,25 @@ Vec_Int_t * Abc_FrameDeriveStatusArray( Vec_Ptr_t * vCexes )
             Vec_IntWriteEntry( vStatuses, i, 0 ); // set this output as SAT
     return vStatuses;
 }
+Vec_Int_t * Abc_FrameDeriveStatusArray2( Vec_Ptr_t * vCexes )
+{
+    Vec_Int_t * vStatuses;
+    Abc_Cex_t * pCex;
+    int i;
+    if ( vCexes == NULL )
+        return NULL;
+    vStatuses = Vec_IntAlloc( Vec_PtrSize(vCexes) );
+    Vec_IntFill( vStatuses, Vec_PtrSize(vCexes), -1 ); // assume UNDEC
+    Vec_PtrForEachEntry( Abc_Cex_t *, vCexes, pCex, i )
+        if ( pCex == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
+        {
+            Vec_IntWriteEntry( vStatuses, i, 1 ); // set this output as UNSAT
+            Vec_PtrWriteEntry( vCexes, i, NULL );
+        }
+        else if ( pCex != NULL )
+            Vec_IntWriteEntry( vStatuses, i, 0 ); // set this output as SAT
+    return vStatuses;
+}
 
 /**Function*************************************************************
 
@@ -2765,8 +2784,8 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
                     Abc_CexPrintStats( pTemp );
                 }
             }
-            if ( Counter )
-                printf( "In total, %d (out of %d) outputs are \"sat\" but CEXes are not recorded.\n", Counter, Vec_PtrSize(pAbc->vCexVec) );
+//            if ( Counter )
+//                printf( "In total, %d (out of %d) outputs are \"sat\" but CEXes are not recorded.\n", Counter, Vec_PtrSize(pAbc->vCexVec) );
         }
     }
     if ( pAbc->vStatuses )
@@ -33675,7 +33694,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fNewSolver = 0, fCSat = 0;
     Cec_ManSatSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcxvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -33727,6 +33746,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             fCSat ^= 1;
             break;
+        case 'x':
+            pPars->fSaveCexes ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -33759,10 +33781,16 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
         pTemp = Cec_ManSatSolving( pAbc->pGia, pPars );
         Abc_FrameUpdateGia( pAbc, pTemp );
     }
+    if ( pAbc->pGia->vSeqModelVec )
+    {
+        Vec_Int_t * vStatuses = Abc_FrameDeriveStatusArray2( pAbc->pGia->vSeqModelVec );
+        Abc_FrameReplacePoStatuses( pAbc, &vStatuses );
+        Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec );
+    }
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctvh]\n" );
+    Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctxvh]\n" );
     Abc_Print( -2, "\t         performs SAT solving for the combinational outputs\n" );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
@@ -33772,6 +33800,7 @@ usage:
     Abc_Print( -2, "\t-m     : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
     Abc_Print( -2, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" );
     Abc_Print( -2, "\t-t     : toggle using learning in curcuit-based solver [default = %s]\n", pPars->fLearnCls? "yes": "no" );
+    Abc_Print( -2, "\t-x     : toggle solving all outputs and saving counter-examples [default = %s]\n", pPars->fSaveCexes? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index cb4ff27f..757d9fd3 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -51,6 +51,7 @@ struct Cec_ParSat_t_
     int              fCheckMiter;   // the circuit is the miter
 //    int              fFirstStop;    // stop on the first sat output
     int              fLearnCls;     // perform clause learning
+    int              fSaveCexes;    // saves counter-examples
     int              fVerbose;      // verbose stats
 };
 
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index 85fcfa26..250cb69e 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -241,6 +241,8 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
 //    pNew = Gia_ManDupDfsSkip( pAig );
     pNew = Gia_ManDup( pAig );
     Cec_ManPatStop( pPat );
+    pNew->vSeqModelVec = pAig->vSeqModelVec;
+    pAig->vSeqModelVec = NULL;
     return pNew;
 }
 
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index f75914e4..3c21e589 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -673,6 +673,21 @@ p->timeSatUndec += Abc_Clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Cex_t * Cex_ManGenCex( Cec_ManSat_t * p, int iOut )
+{
+    Abc_Cex_t * pCex;
+    int i;
+    pCex = Abc_CexAlloc( 0, Gia_ManCiNum(p->pAig), 1 );
+    pCex->iPo = iOut;
+    pCex->iFrame = 0;
+    for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
+    {
+        int iVar = Cec_ObjSatNum(p, Gia_ManCi(p->pAig, i));
+        if ( iVar > 0 && sat_solver_var_value(p->pSat, iVar) )
+            pCex->pData[i>>5] |= (1<<(i & 31));     
+    }
+    return pCex;
+}
 void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs )
 {
     Bar_Progress_t * pProgress = NULL;
@@ -680,6 +695,9 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
     Gia_Obj_t * pObj;
     int i, status;
     abctime clk = Abc_Clock(), clk2;
+    Vec_PtrFreeP( &pAig->vSeqModelVec );
+    if ( pPars->fSaveCexes )
+        pAig->vSeqModelVec = Vec_PtrStart( Gia_ManCoNum(pAig) );
     // reset the manager
     if ( pPat )
     {
@@ -715,6 +733,8 @@ clk2 = Abc_Clock();
             assert( OrigId1 >= 0 && OrigId2 >= 0 );
             Vec_IntPushTwo( vEquivPairs, OrigId1, OrigId2 );
         }
+        if ( pPars->fSaveCexes && status != -1 )
+            Vec_PtrWriteEntry( pAig->vSeqModelVec, i, status ? (Abc_Cex_t *)(ABC_PTRINT_T)1 : Cex_ManGenCex(p, i) );
 
 /*
         if ( status == -1 )