Enabled counter-example minimization in 'write_counter'.

6 files changed, 62 insertions, 11 deletions

diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 96fdde5e..9f98a8f9 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -136,7 +136,7 @@ extern Vec_Int_t *       Saig_ManFlops2Classes( int nRegs, Vec_Int_t * vFlops );
 extern Abc_Cex_t *       Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs );
 /*=== sswAbsCba.c ==========================================================*/
 extern Vec_Int_t *       Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect );
-extern Abc_Cex_t *       Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose );
+extern Abc_Cex_t *       Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
 extern Vec_Int_t *       Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
 extern Vec_Int_t *       Saig_ManCbaPerform( Aig_Man_t * pAig, int nInputs, Saig_ParBmc_t * pPars );
 /*=== sswAbsPba.c ==========================================================*/
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
index 32b9c129..15f2bdfd 100644
--- a/src/aig/saig/saigAbsCba.c
+++ b/src/aig/saig/saigAbsCba.c
@@ -593,7 +593,7 @@ void Saig_ManCbaShrink( Saig_ManCba_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose )
+Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )
 {
     Saig_ManCba_t * p;
     Vec_Int_t * vReasons;
@@ -611,8 +611,8 @@ Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int
         Saig_ManCbaShrink( p );
 
 
-if ( fVerbose )
-Aig_ManPrintStats( p->pFrames );
+//if ( fVerbose )
+//Aig_ManPrintStats( p->pFrames );
 
     if ( fVerbose )
     {
@@ -629,9 +629,15 @@ ABC_PRT( "Time", clock() - clk );
     Saig_ManCbaStop( p );
 
 if ( fVerbose )
+{
+printf( "Real " );
 Abc_CexPrintStats( pCex );
+}
 if ( fVerbose )
+{
+printf( "Care " );
 Abc_CexPrintStats( pCare );
+}
 
     return pCare;
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c412c42e..a1d32f5b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8881,7 +8881,7 @@ 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_ManCbaFindCexCareBits( pAig, pAbc->pCex, 0, fNewOrder, fVerbose );
+        pNew = Saig_ManCbaFindCexCareBits( pAig, pAbc->pCex, 0, fVerbose );
         Aig_ManStop( pAig );
         Abc_FrameReplaceCex( pAbc, &pNew );
     }
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 1c82d91b..3d1a6ae3 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -20,6 +20,7 @@
 
 #include "ioAbc.h"
 #include "mainInt.h"
+#include "saig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -2012,14 +2013,17 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     Abc_Ntk_t * pNtk;
     char * pFileName;
-    int c;
-    int fNames;
+    int c, fNames;
+    int fMinimize;
     int forceSeq;
+    int fVerbose;
 
     fNames = 0;
+    fMinimize = 0;
     forceSeq = 0;
+    fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "snh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "snmvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2029,6 +2033,12 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
             case 'n':
                 fNames ^= 1;
                 break;
+            case 'm':
+                fMinimize ^= 1;
+                break;
+            case 'v':
+                fVerbose ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -2080,11 +2090,25 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
         }
         if ( fNames )
         {
+            Abc_Cex_t * pCare = NULL;
+            if ( fMinimize )
+            {
+                extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+                Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
+                pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose );
+                if ( pCare == NULL )
+                    printf( "Counter-example minimization has failed.\n" );
+                Aig_ManStop( pAig );
+            }
+            // output flop values (unaffected by the minimization)
             Abc_NtkForEachLatch( pNtk, pObj, i )
                 fprintf( pFile, "%s@0=%c ", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
+            // output PI values (while skipping the minimized ones)
             for ( f = 0; f <= pCex->iFrame; f++ )
                 Abc_NtkForEachPi( pNtk, pObj, i )
-                    fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
+                    if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
+                        fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
+            Abc_CexFreeP( &pCare );
         }
         else
         {
@@ -2125,11 +2149,13 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_counter [-snh] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_counter [-snmvh] <file>\n" );
     fprintf( pAbc->Err, "\t         saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" );
     fprintf( pAbc->Err, "\t         the file contains values for each PI in the natural order\n" );
     fprintf( pAbc->Err, "\t-s     : always report a sequential ctrex (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
     fprintf( pAbc->Err, "\t-n     : write input names into the file [default = %s]\n", fNames? "yes": "no" );
+    fprintf( pAbc->Err, "\t-m     : minimize counter-example by dropping don't-care values [default = %s]\n", fMinimize? "yes": "no" );
+    fprintf( pAbc->Err, "\t-v     : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );  
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
     return 1;
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index 72989535..37205543 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -196,7 +196,7 @@ void Abc_CexPrintStats( Abc_Cex_t * p )
     for ( k = 0; k < p->nBits; k++ )
         Counter += Abc_InfoHasBit(p->pData, k);
     printf( "CEX: iPo = %d  iFrame = %d  nRegs = %d  nPis = %d  nBits = %d  nOnes = %5d (%5.2f %%)\n", 
-        p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, Counter, 100.0 * Counter / p->nBits );
+        p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, Counter, 100.0 * Counter / (p->nBits - p->nRegs) );
 }
 
 /**Function*************************************************************
@@ -244,6 +244,24 @@ void Abc_CexPrint( Abc_Cex_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_CexFreeP( Abc_Cex_t ** p )
+{
+    if ( *p == NULL )
+        return;
+    ABC_FREE( *p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_CexFree( Abc_Cex_t * p )
 {
     ABC_FREE( p );
diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h
index c52806fc..556f2268 100644
--- a/src/misc/util/utilCex.h
+++ b/src/misc/util/utilCex.h
@@ -63,6 +63,7 @@ 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 void          Abc_CexPrintStats( Abc_Cex_t * p );
 extern void          Abc_CexPrint( Abc_Cex_t * p );
+extern void          Abc_CexFreeP( Abc_Cex_t ** p );
 extern void          Abc_CexFree( Abc_Cex_t * p );
 
 ABC_NAMESPACE_HEADER_END