Promising modification of the generalization procedure in 'pdr'.

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--;