From da02d5aa9d320b9624a3ae9d85e31aa88838fdd3 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 11 Jul 2012 15:45:55 -0700 Subject: Handling the trivial case when PO is driven by a constant. --- src/aig/gia/giaAbsGla.c | 12 ++++++++++++ src/aig/gia/giaAbsVta.c | 13 +++++++++++++ 2 files changed, 25 insertions(+) (limited to 'src') 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 ) { -- cgit v1.2.3