diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-11 15:45:55 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-11 15:45:55 -0700 |
| commit | da02d5aa9d320b9624a3ae9d85e31aa88838fdd3 (patch) | |
| tree | 58fe7ee09fba3a45208b27518edef1e751e6ea9f | |
| parent | 2427563269566c458f475dfe6fa4388dac80aa02 (diff) | |
| download | abc-da02d5aa9d320b9624a3ae9d85e31aa88838fdd3.tar.gz abc-da02d5aa9d320b9624a3ae9d85e31aa88838fdd3.tar.bz2 abc-da02d5aa9d320b9624a3ae9d85e31aa88838fdd3.zip | |
Handling the trivial case when PO is driven by a constant.
| -rw-r--r-- | src/aig/gia/giaAbsGla.c | 12 | ||||
| -rw-r--r-- | src/aig/gia/giaAbsVta.c | 13 |
2 files changed, 25 insertions, 0 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index a19d4d75..6505c2f2 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -1744,6 +1744,18 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) // preconditions assert( Gia_ManPoNum(pAig) == 1 ); assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax ); + if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) ) + { + if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) ) + { + printf( "Sequential miter is trivially UNSAT.\n" ); + return 1; + } + ABC_FREE( pAig->pCexSeq ); + pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 ); + printf( "Sequential miter is trivially SAT.\n" ); + return 0; + } // compute intial abstraction if ( pAig->vGateClasses == NULL ) diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 735bb823..f7c1e5a5 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -1528,6 +1528,19 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // preconditions assert( Gia_ManPoNum(pAig) == 1 ); assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax ); + if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) ) + { + if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) ) + { + printf( "Sequential miter is trivially UNSAT.\n" ); + return 1; + } + ABC_FREE( pAig->pCexSeq ); + pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 ); + printf( "Sequential miter is trivially SAT.\n" ); + return 0; + } + // compute intial abstraction if ( pAig->vObjClasses == NULL ) { |