luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Correcting &gla to update status as 'sat' after CEX is found.

This commit is contained in:
Alan Mishchenko 2012-07-20 20:22:10 -07:00
parent 6df122bda6
commit 1d89ae52c3
2 changed files with 2 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/aig/gia/giaAbsGla.c
View File

@ -1964,10 +1964,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
p->timeCex += clock() - clk2;
if ( pCex != NULL )
{
RetValue = 0;
goto finish;
}
// print the result (do not count it towards change)
if ( p->pPars->fVerbose )
Gla_ManAbsPrintFrame( p, -1, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk );
@ -2011,7 +2008,6 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
// make sure, there was no initial abstraction (otherwise, it was invalid)
assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
// pCex = Vga_ManDeriveCex( p );
RetValue = 0;
break;
}
}
@ -2084,6 +2080,7 @@ finish:
Abc_Print( 1, "Counter-example detected in frame %d. ", f );
p->pPars->iFrame = pCex->iFrame - 1;
Vec_IntFreeP( &pAig->vGateClasses );
RetValue = 0;
}
Abc_PrintTime( 1, "Time", clock() - clk );
if ( p->pPars->fVerbose )

5
src/aig/gia/giaAbsVta.c
View File

@ -1621,10 +1621,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
pCex = Vta_ManRefineAbstraction( p, f );
p->timeCex += clock() - clk2;
if ( pCex != NULL )
{
RetValue = 0;
goto finish;
}
// print the result (do not count it towards change)
Vta_ManAbsPrintFrame( p, NULL, f+1, sat_solver2_nconflicts(p->pSat)-nConflsBeg, i, clock() - clk, p->pPars->fVerbose );
}
@ -1653,7 +1650,6 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
// make sure, there was no initial abstraction (otherwise, it was invalid)
assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
pCex = Vga_ManDeriveCex( p );
RetValue = 0;
break;
}
// add the core
@ -1738,6 +1734,7 @@ finish:
Abc_Print( 1, "Counter-example detected in frame %d. ", f );
p->pPars->iFrame = pCex->iFrame - 1;
Vec_IntFreeP( &pAig->vObjClasses );
RetValue = 0;
}
Abc_PrintTime( 1, "Time", clock() - clk );