Counter-example analysis and optimization.

abclib.dsp

@@ -1413,6 +1413,10 @@ SOURCE=.\src\sat\bmc\bmcCexMin1.c
 
 SOURCE=.\src\sat\bmc\bmcCexMin2.c
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bmc\bmcCexTools.c
+# End Source File
 # End Group
 # End Group
 # Begin Group "opt"

src/aig/gia/gia.h

@@ -928,6 +928,7 @@ extern void                Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart
 extern char *              Gia_TimeStamp();
 extern char *              Gia_FileNameGenericAppend( char * pBase, char * pSuffix );
 extern void                Gia_ManIncrementTravId( Gia_Man_t * p );
+extern void                Gia_ManCleanMark01( Gia_Man_t * p );
 extern void                Gia_ManSetMark0( Gia_Man_t * p );
 extern void                Gia_ManCleanMark0( Gia_Man_t * p );
 extern void                Gia_ManCheckMark0( Gia_Man_t * p );

src/aig/gia/giaUtil.c

@@ -157,6 +157,25 @@ void Gia_ManIncrementTravId( Gia_Man_t * p )
     p->nTravIds++;                                                    
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sets phases of the internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCleanMark01( Gia_Man_t * p )  
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManForEachObj( p, pObj, i )
+        pObj->fMark0 = pObj->fMark1 = 0;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Sets phases of the internal nodes.]

src/base/abci/abc.c

@@ -30136,6 +30136,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern void Gia_VtaTest( Gia_Man_t * p, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose );
 //    extern void Gia_IsoTest( Gia_Man_t * p, int fVerbose );
     extern void Ga2_ManComputeTest( Gia_Man_t * p );
+    extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex );
+
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
@@ -30159,6 +30161,11 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" );
         return 1;
     }
+    if ( pAbc->pCex == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Test(): There is no CEX.\n" );
+        return 1;
+    }
 //    Gia_ManFrontTest( pAbc->pGia );
 //    Gia_ManReduceConst( pAbc->pGia, 1 );
 //    Sat_ManTest( pAbc->pGia, Gia_ManCo(pAbc->pGia, 0), 0 );
@@ -30174,7 +30181,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Gia_ManSuppSizeTest( pAbc->pGia );
 //    Gia_VtaTest( pAbc->pGia, 10, 100000, 0, 0, 1 );
 //    Gia_IsoTest( pAbc->pGia, fVerbose );
-    Ga2_ManComputeTest( pAbc->pGia );
+//    Ga2_ManComputeTest( pAbc->pGia );
+    Bmc_CexTest( pAbc->pGia, pAbc->pCex );
     return 0;
 usage:
     Abc_Print( -2, "usage: &test [-svh]\n" );

src/misc/util/utilCex.c

@@ -59,6 +59,17 @@ Abc_Cex_t * Abc_CexAlloc( int nRegs, int nRealPis, int nFrames )
     pCex->nBits  = nRegs + nRealPis * nFrames;
     return pCex;
 }
+Abc_Cex_t * Abc_CexAllocFull( int nRegs, int nRealPis, int nFrames )
+{
+    Abc_Cex_t * pCex;
+    int nWords = Abc_BitWordNum( nRegs + nRealPis * nFrames );
+    pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
+    memset( pCex, 0xFF, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
+    pCex->nRegs  = nRegs;
+    pCex->nPis   = nRealPis;
+    pCex->nBits  = nRegs + nRealPis * nFrames;
+    return pCex;
+}
 
 /**Function*************************************************************
 

src/misc/util/utilCex.h

@@ -57,6 +57,7 @@ struct Abc_Cex_t_
 
 /*=== utilCex.c ===========================================================*/
 extern Abc_Cex_t *   Abc_CexAlloc( int nRegs, int nTruePis, int nFrames );
+extern Abc_Cex_t *   Abc_CexAllocFull( int nRegs, int nTruePis, int nFrames );
 extern Abc_Cex_t *   Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int iFrameOut );
 extern Abc_Cex_t *   Abc_CexCreate( int nRegs, int nTruePis, int * pArray, int iFrame, int iPo, int fSkipRegs );
 extern Abc_Cex_t *   Abc_CexDup( Abc_Cex_t * p, int nRegsNew );

src/sat/bmc/module.make

@@ -4,4 +4,5 @@ SRC +=    src/sat/bmc/bmc.c \
     src/sat/bmc/bmcBmc3.c \
     src/sat/bmc/bmcCexCut.c \
     src/sat/bmc/bmcCexMin1.c \
-    src/sat/bmc/bmcCexMin2.c
+    src/sat/bmc/bmcCexMin2.c \
+    src/sat/bmc/bmcCexTools.c