summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/sat/bmc/bmcCexTools.c322
1 files changed, 258 insertions, 64 deletions
diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c
index f7252bc0..87d88fd0 100644
--- a/src/sat/bmc/bmcCexTools.c
+++ b/src/sat/bmc/bmcCexTools.c
@@ -39,6 +39,262 @@ static inline int Bmc_CexSim( Vec_Wrd_t * vSims, int iObj, int i )
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Bmc_CexBitCount( Abc_Cex_t * p, int nInputs )
+{
+ int k, Counter = 0, Counter2 = 0;
+ if ( p == NULL )
+ {
+ printf( "The counter example is NULL.\n" );
+ return -1;
+ }
+ for ( k = 0; k < p->nBits; k++ )
+ {
+ Counter += Abc_InfoHasBit(p->pData, k);
+ if ( (k - p->nRegs) % p->nPis < nInputs )
+ Counter2 += Abc_InfoHasBit(p->pData, k);
+ }
+ return Counter2;
+}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bmc_CexDumpStats( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare, Abc_Cex_t * pCexEss, Abc_Cex_t * pCexMin, clock_t clk )
+{
+ int nInputs = Gia_ManPiNum(p);
+ int nBitsTotal = (pCex->iFrame + 1) * nInputs;
+ int nBitsCare = Bmc_CexBitCount(pCexCare, nInputs);
+ int nBitsDC = nBitsTotal - nBitsCare;
+ int nBitsEss = Bmc_CexBitCount(pCexEss, nInputs);
+ int nBitsOpt = nBitsCare - nBitsEss;
+ int nBitsMin = Bmc_CexBitCount(pCexMin, nInputs);
+
+ FILE * pTable = fopen( "cex/stats.txt", "a+" );
+ fprintf( pTable, "%s ", p->pName );
+ fprintf( pTable, "%d ", nInputs );
+ fprintf( pTable, "%d ", Gia_ManRegNum(p) );
+ fprintf( pTable, "%d ", pCex->iFrame + 1 );
+ fprintf( pTable, "%d ", nBitsTotal );
+ fprintf( pTable, "%.2f ", 100.0 * nBitsDC / nBitsTotal );
+ fprintf( pTable, "%.2f ", 100.0 * nBitsOpt / nBitsTotal );
+ fprintf( pTable, "%.2f ", 100.0 * nBitsEss / nBitsTotal );
+ fprintf( pTable, "%.2f ", 100.0 * nBitsMin / nBitsTotal );
+ fprintf( pTable, "%.2f ", 1.0*clk/(CLOCKS_PER_SEC) );
+ fprintf( pTable, "\n" );
+ fclose( pTable );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bmc_CexDumpAogStats( Gia_Man_t * p, clock_t clk )
+{
+ FILE * pTable = fopen( "cex/aig_stats.txt", "a+" );
+ fprintf( pTable, "%s ", p->pName );
+ fprintf( pTable, "%d ", Gia_ManPiNum(p) );
+ fprintf( pTable, "%d ", Gia_ManAndNum(p) );
+ fprintf( pTable, "%d ", Gia_ManLevelNum(p) );
+ fprintf( pTable, "%.2f ", 1.0*clk/(CLOCKS_PER_SEC) );
+ fprintf( pTable, "\n" );
+ fclose( pTable );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs initialized unrolling till the last frame.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Bmc_CexPerformUnrolling( Gia_Man_t * p, Abc_Cex_t * pCex )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+ int i, k;
+ assert( Gia_ManRegNum(p) > 0 );
+ pNew = Gia_ManStart( (pCex->iFrame + 1) * Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachRi( p, pObj, k )
+ pObj->Value = 0;
+ Gia_ManHashAlloc( pNew );
+ for ( i = 0; i <= pCex->iFrame; i++ )
+ {
+ Gia_ManForEachPi( p, pObj, k )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+ pObjRo->Value = pObjRi->Value;
+ Gia_ManForEachAnd( p, pObj, k )
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ Gia_ManForEachCo( p, pObj, k )
+ pObj->Value = Gia_ObjFanin0Copy(pObj);
+ }
+ Gia_ManHashStop( pNew );
+ pObj = Gia_ManPo(p, pCex->iPo);
+ Gia_ManAppendCo( pNew, pObj->Value );
+ // cleanup
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+void Bmc_CexPerformUnrollingTest( Gia_Man_t * p, Abc_Cex_t * pCex )
+{
+ Gia_Man_t * pNew;
+ clock_t clk = clock();
+ pNew = Bmc_CexPerformUnrolling( p, pCex );
+ Gia_ManPrintStats( pNew, 0, 0, 0 );
+ Gia_WriteAiger( pNew, "unroll.aig", 0, 0 );
+//Bmc_CexDumpAogStats( pNew, clock() - clk );
+ Gia_ManStop( pNew );
+ printf( "CE-induced network is written into file \"unroll.aig\".\n" );
+ Abc_PrintTime( 1, "Time", clock() - clk );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes CE-induced network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Bmc_CexBuildNetwork( Gia_Man_t * p, Abc_Cex_t * pCex )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+ int fCompl0, fCompl1;
+ int i, k, iBit = pCex->nRegs;
+ // start the manager
+ pNew = Gia_ManStart( 1000 );
+ pNew->pName = Abc_UtilStrsav( "unate" );
+ // set const0
+ Gia_ManConst0(p)->fMark0 = 0;
+ Gia_ManConst0(p)->fMark1 = 1;
+ Gia_ManConst0(p)->Value = ~0;
+ // set init state
+ Gia_ManForEachRi( p, pObj, k )
+ {
+ pObj->fMark0 = 0;
+ pObj->fMark1 = 1;
+ pObj->Value = ~0;
+ }
+ Gia_ManHashAlloc( pNew );
+ for ( i = 0; i <= pCex->iFrame; i++ )
+ {
+ // primary inputs
+ Gia_ManForEachPi( p, pObj, k )
+ {
+ pObj->fMark0 = Abc_InfoHasBit( pCex->pData, iBit++ );
+ pObj->fMark1 = 0;
+ pObj->Value = Gia_ManAppendCi(pNew);
+ }
+ // transfer
+ Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+ {
+ pObjRo->fMark0 = pObjRi->fMark0;
+ pObjRo->fMark1 = pObjRi->fMark1;
+ pObjRo->Value = pObjRi->Value;
+ }
+ // internal nodes
+ Gia_ManForEachAnd( p, pObj, k )
+ {
+ fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+ fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
+ pObj->fMark0 = fCompl0 & fCompl1;
+ if ( pObj->fMark0 )
+ pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1;
+ else if ( !fCompl0 && !fCompl1 )
+ pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
+ else if ( !fCompl0 )
+ pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
+ else if ( !fCompl1 )
+ pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1;
+ else assert( 0 );
+ pObj->Value = ~0;
+ if ( pObj->fMark1 )
+ continue;
+ if ( pObj->fMark0 )
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+ else if ( !fCompl0 && !fCompl1 )
+ pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+ else if ( !fCompl0 )
+ pObj->Value = Gia_ObjFanin0(pObj)->Value;
+ else if ( !fCompl1 )
+ pObj->Value = Gia_ObjFanin1(pObj)->Value;
+ else assert( 0 );
+ assert( pObj->Value > 0 );
+ }
+ // combinational outputs
+ Gia_ManForEachCo( p, pObj, k )
+ {
+ pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+ pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
+ pObj->Value = Gia_ObjFanin0(pObj)->Value;
+ }
+ }
+ Gia_ManHashStop( pNew );
+ assert( iBit == pCex->nBits );
+ // create primary output
+ pObj = Gia_ManPo(p, pCex->iPo);
+ assert( pObj->fMark0 == 1 );
+ assert( pObj->fMark1 == 0 );
+ assert( pObj->Value > 0 );
+ Gia_ManAppendCo( pNew, pObj->Value );
+ // cleanup
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+void Bmc_CexBuildNetworkTest( Gia_Man_t * p, Abc_Cex_t * pCex )
+{
+ Gia_Man_t * pNew;
+ clock_t clk = clock();
+ pNew = Bmc_CexBuildNetwork( p, pCex );
+ Gia_ManPrintStats( pNew, 0, 0, 0 );
+ Gia_WriteAiger( pNew, "unate.aig", 0, 0 );
+//Bmc_CexDumpAogStats( pNew, clock() - clk );
+ Gia_ManStop( pNew );
+ printf( "CE-induced network is written into file \"unate.aig\".\n" );
+ Abc_PrintTime( 1, "Time", clock() - clk );
+}
+
+
+/**Function*************************************************************
+
Synopsis [Prints one counter-example.]
Description []
@@ -548,70 +804,6 @@ Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_
/**Function*************************************************************
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Bmc_CexBitCount( Abc_Cex_t * p, int nInputs )
-{
- int k, Counter = 0, Counter2 = 0;
- if ( p == NULL )
- {
- printf( "The counter example is NULL.\n" );
- return -1;
- }
- for ( k = 0; k < p->nBits; k++ )
- {
- Counter += Abc_InfoHasBit(p->pData, k);
- if ( (k - p->nRegs) % p->nPis < nInputs )
- Counter2 += Abc_InfoHasBit(p->pData, k);
- }
- return Counter2;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Bmc_CexDumpStats( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare, Abc_Cex_t * pCexEss, Abc_Cex_t * pCexMin, clock_t clk )
-{
- int nInputs = Gia_ManPiNum(p);
- int nBitsTotal = (pCex->iFrame + 1) * nInputs;
- int nBitsCare = Bmc_CexBitCount(pCexCare, nInputs);
- int nBitsDC = nBitsTotal - nBitsCare;
- int nBitsEss = Bmc_CexBitCount(pCexEss, nInputs);
- int nBitsOpt = nBitsCare - nBitsEss;
- int nBitsMin = Bmc_CexBitCount(pCexMin, nInputs);
-
- FILE * pTable = fopen( "cex/stats.txt", "a+" );
- fprintf( pTable, "%s ", p->pName );
- fprintf( pTable, "%d ", nInputs );
- fprintf( pTable, "%d ", Gia_ManRegNum(p) );
- fprintf( pTable, "%d ", pCex->iFrame + 1 );
- fprintf( pTable, "%d ", nBitsTotal );
- fprintf( pTable, "%.2f ", 100.0 * nBitsDC / nBitsTotal );
- fprintf( pTable, "%.2f ", 100.0 * nBitsOpt / nBitsTotal );
- fprintf( pTable, "%.2f ", 100.0 * nBitsEss / nBitsTotal );
- fprintf( pTable, "%.2f ", 100.0 * nBitsMin / nBitsTotal );
- fprintf( pTable, "%.2f ", 1.0*clk/(CLOCKS_PER_SEC) );
- fprintf( pTable, "\n" );
- fclose( pTable );
-}
-
-/**Function*************************************************************
-
Synopsis [Computes essential bits of the CEX.]
Description []
@@ -647,6 +839,8 @@ void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
Abc_CexFreeP( &pCexMin );
Abc_PrintTime( 1, "Time", clock() - clk );
+// Bmc_CexBuildNetworkTest( p, pCex );
+// Bmc_CexPerformUnrollingTest( p, pCex );
}
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 00:40:52 +0000