From 48bdc5144a4b8579393c3ed46ad70b84c4bd1dc2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 29 Aug 2011 18:46:16 +0700 Subject: Making 'reconcile' ignore the difference in flop count. --- src/aig/llb/llb4Cex.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src/aig/llb') diff --git a/src/aig/llb/llb4Cex.c b/src/aig/llb/llb4Cex.c index 603c6e59..4f06b8c6 100644 --- a/src/aig/llb/llb4Cex.c +++ b/src/aig/llb/llb4Cex.c @@ -215,7 +215,9 @@ Vec_Ptr_t * Llb4_Nonlin4VerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p ) Aig_ManCleanMarkB(pAig); Aig_ManConst1(pAig)->fMarkB = 1; Saig_ManForEachLo( pAig, pObj, i ) - pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + pObj->fMarkB = 0; //Aig_InfoHasBit(p->pData, iBit++); + // do not require equal flop count in the AIG and in the CEX + iBit = p->nRegs; for ( i = 0; i <= p->iFrame; i++ ) { // save current state @@ -284,11 +286,13 @@ Abc_Cex_t * Llb4_Nonlin4NormalizeCex( Aig_Man_t * pAigOrg, Aig_Man_t * pAigRpm, printf( "Llb4_Nonlin4NormalizeCex(): The number of flops in the original and reparametrized AIGs do not agree.\n" ); return NULL; } +/* if ( Saig_ManRegNum(pAigRpm) != pCexRpm->nRegs ) { printf( "Llb4_Nonlin4NormalizeCex(): The number of flops in the reparametrized AIG and in the CEX do not agree.\n" ); return NULL; } +*/ if ( Saig_ManPiNum(pAigRpm) != pCexRpm->nPis ) { printf( "Llb4_Nonlin4NormalizeCex(): The number of PIs in the reparametrized AIG and in the CEX do not agree.\n" ); -- cgit v1.2.3