summaryrefslogtreecommitdiffstats
path: root/src/aig/gia/giaAbsGla.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia/giaAbsGla.c')
-rw-r--r--src/aig/gia/giaAbsGla.c210
1 files changed, 1 insertions, 209 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 9b33c066..822a55dd 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -24,7 +24,6 @@
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver2.h"
#include "base/main/main.h"
-#include "aig/saig/saig.h"
ABC_NAMESPACE_IMPL_START
@@ -130,7 +129,7 @@ static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) {
for ( i = 0; (i < (int)pObj->nFanins) && ((pFanin = Gla_ManObj(p, pObj->Fanins[i])),1); i++ )
// some lessons learned from debugging mismatches between GIA and mapped CNF
-// - inputs/output of AND-node maybe PPIs (have SAT vars), but the node is not included in the abstraction
+// - inputs/output of AND-node may be PPIs (have SAT vars), but the node is not included in the abstraction
// - some logic node can be a PPI of one LUT and an internal node of another LUT
////////////////////////////////////////////////////////////////////////
@@ -139,213 +138,6 @@ static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) {
/**Function*************************************************************
- Synopsis [Derive a new counter-example.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPis )
-{
- Abc_Cex_t * pCex;
- int i, f, iPiNum;
- assert( pCexAbs->iPo == 0 );
- // start the counter-example
- pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), pCexAbs->iFrame+1 );
- pCex->iFrame = pCexAbs->iFrame;
- pCex->iPo = pCexAbs->iPo;
- // copy the bit data
- for ( f = 0; f <= pCexAbs->iFrame; f++ )
- for ( i = 0; i < Vec_IntSize(vPis); i++ )
- {
- if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
- {
- iPiNum = Gia_ObjCioId( Gia_ManObj(p, Vec_IntEntry(vPis, i)) );
- Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + iPiNum );
- }
- }
- // verify the counter example
- if ( !Gia_ManVerifyCex( p, pCex, 0 ) )
- {
- Abc_Print( 1, "Gia_ManCexRemap(): Counter-example is invalid.\n" );
- Abc_CexFree( pCex );
- pCex = NULL;
- }
- else
- {
- Abc_Print( 1, "Counter-example verification is successful.\n" );
- Abc_Print( 1, "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
- }
- return pCex;
-}
-
-/**Function*************************************************************
-
- Synopsis [Refines gate-level abstraction using the counter-example.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose )
-{
- extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose );
-// extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
- int fAddOneLayer = 1;
- Abc_Cex_t * pCexNew = NULL;
- Gia_Man_t * pAbs;
- Aig_Man_t * pAig;
- Abc_Cex_t * pCare;
- Vec_Int_t * vPis, * vPPis;
- int f, i, iObjId;
- clock_t clk = clock();
- int nOnes = 0, Counter = 0;
- if ( p->vGateClasses == NULL )
- {
- Abc_Print( 1, "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" );
- return -1;
- }
- // derive abstraction
- pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
- Gia_ManStop( pAbs );
- pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
- if ( Gia_ManPiNum(pAbs) != pCex->nPis )
- {
- Abc_Print( 1, "Gia_ManGlaRefine(): The PI counts in GLA and in CEX do not match.\n" );
- Gia_ManStop( pAbs );
- return -1;
- }
- if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) )
- {
- Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" );
-// Gia_ManStop( pAbs );
-// return -1;
- }
-// else
-// Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is correct.\n" );
- // get inputs
- Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, NULL, NULL );
- assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
- // add missing logic
- if ( fAddOneLayer )
- {
- Gia_Obj_t * pObj;
- // check if this is a real counter-example
- Gia_ObjTerSimSet0( Gia_ManConst0(pAbs) );
- for ( f = 0; f <= pCex->iFrame; f++ )
- {
- Gia_ManForEachPi( pAbs, pObj, i )
- {
- if ( i >= Vec_IntSize(vPis) ) // PPIs
- Gia_ObjTerSimSetX( pObj );
- else if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
- Gia_ObjTerSimSet1( pObj );
- else
- Gia_ObjTerSimSet0( pObj );
- }
- Gia_ManForEachRo( pAbs, pObj, i )
- {
- if ( f == 0 )
- Gia_ObjTerSimSet0( pObj );
- else
- Gia_ObjTerSimRo( pAbs, pObj );
- }
- Gia_ManForEachAnd( pAbs, pObj, i )
- Gia_ObjTerSimAnd( pObj );
- Gia_ManForEachCo( pAbs, pObj, i )
- Gia_ObjTerSimCo( pObj );
- }
- pObj = Gia_ManPo( pAbs, 0 );
- if ( Gia_ObjTerSimGet1(pObj) )
- {
- pCexNew = Gia_ManCexRemap( p, pCex, vPis );
- Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
- }
-// else
-// Abc_Print( 1, "CEX is not real.\n" );
- Gia_ManForEachObj( pAbs, pObj, i )
- Gia_ObjTerSimSetC( pObj );
- if ( pCexNew == NULL )
- {
- // grow one layer
- Vec_IntForEachEntry( vPPis, iObjId, i )
- {
- assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
- Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
- }
- if ( fVerbose )
- {
- Abc_Print( 1, "Additional objects = %d. ", Vec_IntSize(vPPis) );
- Abc_PrintTime( 1, "Time", clock() - clk );
- }
- }
- }
- else
- {
- // minimize the CEX
- pAig = Gia_ManToAigSimple( pAbs );
- pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose );
- Aig_ManStop( pAig );
- if ( pCare == NULL )
- Abc_Print( 1, "Counter-example minimization has failed.\n" );
- // add new objects to the map
- iObjId = -1;
- for ( f = 0; f <= pCare->iFrame; f++ )
- for ( i = 0; i < pCare->nPis; i++ )
- if ( Abc_InfoHasBit( pCare->pData, pCare->nRegs + f * pCare->nPis + i ) )
- {
- nOnes++;
- assert( i >= Vec_IntSize(vPis) );
- iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
- assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
- if ( Vec_IntEntry( p->vGateClasses, iObjId ) > 0 )
- continue;
- assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
- Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
- // Abc_Print( 1, "Adding object %d.\n", iObjId );
- // Gia_ObjPrint( p, Gia_ManObj(p, iObjId) );
- Counter++;
- }
- Abc_CexFree( pCare );
- if ( fVerbose )
- {
- Abc_Print( 1, "Essential bits = %d. Additional objects = %d. ", nOnes, Counter );
- Abc_PrintTime( 1, "Time", clock() - clk );
- }
- // consider the case of SAT
- if ( iObjId == -1 )
- {
- pCexNew = Gia_ManCexRemap( p, pCex, vPis );
- Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
- }
- }
- Vec_IntFree( vPis );
- Vec_IntFree( vPPis );
- Gia_ManStop( pAbs );
- if ( pCexNew )
- {
- ABC_FREE( p->pCexSeq );
- p->pCexSeq = pCexNew;
- return 0;
- }
- // extract abstraction to include min-cut
- if ( fMinCut )
- Nwk_ManDeriveMinCut( p, fVerbose );
- return -1;
-}
-
-
-
-
-
-/**Function*************************************************************
-
Synopsis [Prepares CEX and vMap for refinement.]
Description []
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 05:32:31 +0000