diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-17 14:10:32 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-17 14:10:32 -0800 |
| commit | bc010af4be920199d7f1e0bfe4a6d70dcbca042b (patch) | |
| tree | dffc9e6782496df59e731473f28600a89d8ab4c3 /src/proof/pdr | |
| parent | 378af9d94fc32232f638c784fb9cb9095f410bee (diff) | |
| download | abc-bc010af4be920199d7f1e0bfe4a6d70dcbca042b.tar.gz abc-bc010af4be920199d7f1e0bfe4a6d70dcbca042b.tar.bz2 abc-bc010af4be920199d7f1e0bfe4a6d70dcbca042b.zip | |
Promising modification of the generalization procedure in 'pdr'.
Diffstat (limited to 'src/proof/pdr')
| -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--; |