diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-08-09 17:53:38 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-08-09 17:53:38 -0700 |
| commit | 5b80d704a1f8ce9514b282b9f722b6caa3671d0e (patch) | |
| tree | 155267223696d415289290d6a13c98e99ea64656 /src/aig/gia/giaAbsGla2.c | |
| parent | d01c0807bdc2b2d544db96207a129c6eb4e32b5d (diff) | |
| download | abc-5b80d704a1f8ce9514b282b9f722b6caa3671d0e.tar.gz abc-5b80d704a1f8ce9514b282b9f722b6caa3671d0e.tar.bz2 abc-5b80d704a1f8ce9514b282b9f722b6caa3671d0e.zip | |
Improved abstraction refinement.
Diffstat (limited to 'src/aig/gia/giaAbsGla2.c')
| -rw-r--r-- | src/aig/gia/giaAbsGla2.c | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 6910f334..d8a18930 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -20,7 +20,7 @@ #include "gia.h" #include "giaAbsRef.h" -#include "giaAbsRef2.h" +//#include "giaAbsRef2.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satSolver2.h" #include "base/main/main.h" @@ -52,7 +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 +// 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 @@ -396,7 +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 ); +// p->pRf2 = Rf2_ManStart( pGia ); // SAT solver and variables p->vId2Lit = Vec_PtrAlloc( 1000 ); // temporaries @@ -459,7 +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 ); +// Rf2_ManStop( p->pRf2, p->pPars->fVerbose ); ABC_FREE( p->pTable ); ABC_FREE( p->pSopSizes ); ABC_FREE( p->pSops[1] ); @@ -1224,11 +1224,9 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p ) Gia_Obj_t * pObj; int i; Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap ); - -// Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 ); + // Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 ); vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1 ); // printf( "Refinement %d\n", Vec_IntSize(vVec) ); - Abc_CexFree( pCex ); if ( Vec_IntSize(vVec) == 0 ) { |