diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-08-06 21:59:14 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-08-06 21:59:14 -0700 |
| commit | ca9803fc98943ed6b23c54057590b05b05c53e76 (patch) | |
| tree | b469e0618d64e27a19014c46d0855a0d66c7efcb /src/aig/gia/giaAbsGla2.c | |
| parent | 94949287fe1ae3a46113102eab7c99d530983c45 (diff) | |
| download | abc-ca9803fc98943ed6b23c54057590b05b05c53e76.tar.gz abc-ca9803fc98943ed6b23c54057590b05b05c53e76.tar.bz2 abc-ca9803fc98943ed6b23c54057590b05b05c53e76.zip | |
Scalable gate-level abstraction.
Diffstat (limited to 'src/aig/gia/giaAbsGla2.c')
| -rw-r--r-- | src/aig/gia/giaAbsGla2.c | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 3dd7e352..daad8c6c 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -20,6 +20,7 @@ #include "gia.h" #include "giaAbsRef.h" +#include "giaAbsRef2.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satSolver2.h" #include "base/main/main.h" @@ -51,6 +52,7 @@ struct Ga2_Man_t_ int nMarked; // total number of marked nodes and flops // refinement Rnm_Man_t * pRnm; // refinement manager + Rf2_Man_t * pRf2; // refinement manager // SAT solver and variables Vec_Ptr_t * vId2Lit; // mapping, for each timeframe, of object ID into SAT literal sat_solver2 * pSat; // incremental SAT solver @@ -333,6 +335,7 @@ int Ga2_ManMarkup( Gia_Man_t * p, int N, int fSimple ) } // Abc_PrintTime( 1, "Time", clock() - clk ); Vec_IntFree( vLeaves ); + Gia_ManCleanValue( p ); return CountMarks; } void Ga2_ManComputeTest( Gia_Man_t * p ) @@ -393,6 +396,7 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) Vec_IntPush( p->vAbs, 0 ); // refinement p->pRnm = Rnm_ManStart( pGia ); +// p->pRf2 = Rf2_ManStart( pGia ); // SAT solver and variables p->vId2Lit = Vec_PtrAlloc( 1000 ); // temporaries @@ -455,6 +459,7 @@ void Ga2_ManStop( Ga2_Man_t * p ) Vec_IntFree( p->vLits ); Vec_IntFree( p->vIsopMem ); Rnm_ManStop( p->pRnm, p->pPars->fVerbose ); +// Rf2_ManStop( p->pRf2, p->pPars->fVerbose ); ABC_FREE( p->pTable ); ABC_FREE( p->pSopSizes ); ABC_FREE( p->pSops[1] ); @@ -1222,6 +1227,7 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p ) int i; Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap ); vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1 ); +// Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 ); Abc_CexFree( pCex ); if ( Vec_IntSize(vVec) == 0 ) { @@ -1351,6 +1357,7 @@ void Gia_Ga2SendAbsracted( Ga2_Man_t * p, int fVerbose ) vGateClasses = Ga2_ManAbsTranslate( p ); pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses ); Vec_IntFreeP( &vGateClasses ); + Gia_ManCleanValue( p->pGia ); // send it out Gia_ManToBridgeAbsNetlist( stdout, pAbs ); Gia_ManStop( pAbs ); |