From bc010af4be920199d7f1e0bfe4a6d70dcbca042b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 17 Feb 2017 14:10:32 -0800 Subject: Promising modification of the generalization procedure in 'pdr'. --- src/proof/pdr/pdrCore.c | 10 ++++++++++ 1 file changed, 10 insertions(+) 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--; -- cgit v1.2.3