diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index efb4154f..501f9be6 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -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--; |