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

Promising modification of the generalization procedure in 'pdr'.

This commit is contained in:
Alan Mishchenko 2017-02-17 14:10:32 -08:00
parent 378af9d94f
commit bc010af4be
1 changed files with 10 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/proof/pdr/pdrCore.c
View File

@ -637,6 +637,16 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
Pdr_SetDeref( pCubeTmp );
assert( pCubeMin->nLits > 0 );
// assume the minimized cube
if ( p->pPars->fSimpleGeneral )
{
sat_solver * pSat = Pdr_ManFetchSolver( p, k );
Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCubeMin, 1, 0 );
int RetValue1 = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntArray(vLits1) + Vec_IntSize(vLits1) );
assert( RetValue1 == 1 );
sat_solver_compress( pSat );
}
// get the ordering by decreasing priority
pOrder = Pdr_ManSortByPriority( p, pCubeMin );
j--;