diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-19 23:45:11 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-19 23:45:11 +0700 |
| commit | 9ec9d9f315b9025e5406eea59d310f5fa48cf69f (patch) | |
| tree | 97b6712a16801e1c055463ef3b35f9ed35f64438 | |
| parent | 19ce8396f03df14028219b9d4efd93a852f30219 (diff) | |
| download | abc-9ec9d9f315b9025e5406eea59d310f5fa48cf69f.tar.gz abc-9ec9d9f315b9025e5406eea59d310f5fa48cf69f.tar.bz2 abc-9ec9d9f315b9025e5406eea59d310f5fa48cf69f.zip | |
New abstraction code.
| -rw-r--r-- | src/aig/saig/saigAbsGla.c | 20 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 5 |
2 files changed, 20 insertions, 5 deletions
diff --git a/src/aig/saig/saigAbsGla.c b/src/aig/saig/saigAbsGla.c index 681b10c3..696088ce 100644 --- a/src/aig/saig/saigAbsGla.c +++ b/src/aig/saig/saigAbsGla.c @@ -665,10 +665,10 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in if ( fVerbose ) { - if ( TimeLimit ) - printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit ); - else - printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax ); + if ( TimeLimit ) + printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit ); + else + printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax ); } // start the solver @@ -748,6 +748,14 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in if ( !Aig_GlaObjAddToSolver( p, pObj, g ) ) printf( "Error! SAT solver became UNSAT.\n" ); } + if ( Vec_IntSize(vPPiRefine) == 0 ) + { + Vec_IntFreeP( &p->vIncluded ); + Vec_IntFree( vPPiRefine ); + Aig_ManStop( pAbs ); + Abc_CexFree( pCex ); + break; + } Vec_IntFree( vPPiRefine ); Aig_ManStop( pAbs ); Abc_CexFree( pCex ); @@ -764,6 +772,8 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in p->timeTotal = clock() - clkTotal; if ( f == nFramesMax ) printf( "Finished %d frames without exceeding conflict limit (%d).\n", f, nConfLimit ); + else if ( p->vIncluded == NULL ) + printf( "The problem is SAT in frame %d. The CEX is currently not produced.\n", f ); else printf( "Ran out of conflict limit (%d) at frame %d.\n", nConfLimit, f ); // print stats @@ -774,7 +784,7 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in ABC_PRTP( "Total ", p->timeTotal, p->timeTotal ); } // prepare return value - if ( !fNaiveCnf ) + if ( !fNaiveCnf && p->vIncluded ) Aig_GlaExtendIncluded( p ); vResult = p->vIncluded; p->vIncluded = NULL; Aig_GlaManStop( p ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5b77f5b0..fb25e8ca 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28975,6 +28975,11 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "The network is combinational.\n" ); return 0; } + if ( Gia_ManPoNum(pAbc->pGia) > 1 ) + { + Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" ); + return 0; + } pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fNaiveCnf ); if ( pPars->nStart == 0 ) pAbc->nFrames = pPars->iFrame; |