Added switch to PDR to disable expensive generalization step.

2 files changed, 71 insertions, 66 deletions

diff --git a/src/sat/pdr/pdr.h b/src/sat/pdr/pdr.h
index 740eb46f..03854509 100644
--- a/src/sat/pdr/pdr.h
+++ b/src/sat/pdr/pdr.h
@@ -49,6 +49,7 @@ struct Pdr_Par_t_
     int fMonoCnf;     // monolythic CNF
     int fDumpInv;     // dump inductive invariant
     int fShortest;    // forces bug traces to be shortest
+    int fSkipGeneral; // skips expensive generalization step
     int fVerbose;     // verbose output
     int fVeryVerbose; // very verbose output
     int iFrame;       // explored up to this frame
diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c
index cf8c231a..cf57327a 100644
--- a/src/sat/pdr/pdrCore.c
+++ b/src/sat/pdr/pdrCore.c
@@ -302,89 +302,93 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
         p->tGeneral += clock() - clk;
         return 0;
     }
+
     // reduce clause using assumptions
 //    pCubeMin = Pdr_SetDup( pCube );
     pCubeMin = Pdr_ManReduceClause( p, k, pCube );
     if ( pCubeMin == NULL )
         pCubeMin = Pdr_SetDup( pCube );
 
-    // sort literals by their occurences
-    pOrder = Pdr_ManSortByPriority( p, pCubeMin );
-
-    // try removing literals
-    for ( j = 0; j < pCubeMin->nLits; j++ )
+    // perform generalization
+    if ( !p->pPars->fSkipGeneral )
     {
-        // use ordering
-//        i = j;
-        i = pOrder[j];
-
-        // check init state
-        assert( pCubeMin->Lits[i] != -1 );
-        if ( Pdr_SetIsInit(pCubeMin, i) )
-            continue;
-        // try removing this literal
-        Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; 
-        RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
-        if ( RetValue == -1 )
+        // sort literals by their occurences
+        pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+        // try removing literals
+        for ( j = 0; j < pCubeMin->nLits; j++ )
         {
-            Pdr_SetDeref( pCubeMin );
-            return -1;
-        }
-        pCubeMin->Lits[i] = Lit;
-        if ( RetValue == 0 )
-            continue;
+            // use ordering
+    //        i = j;
+            i = pOrder[j];
 
-        // remove j-th entry
-        for ( n = j; n < pCubeMin->nLits-1; n++ )
-            pOrder[n] = pOrder[n+1];
-        j--;
+            // check init state
+            assert( pCubeMin->Lits[i] != -1 );
+            if ( Pdr_SetIsInit(pCubeMin, i) )
+                continue;
+            // try removing this literal
+            Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; 
+            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
+            if ( RetValue == -1 )
+            {
+                Pdr_SetDeref( pCubeMin );
+                return -1;
+            }
+            pCubeMin->Lits[i] = Lit;
+            if ( RetValue == 0 )
+                continue;
 
-        // success - update the cube
-        pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
-        Pdr_SetDeref( pCubeTmp );
-        assert( pCubeMin->nLits > 0 );
-        i--;
+            // remove j-th entry
+            for ( n = j; n < pCubeMin->nLits-1; n++ )
+                pOrder[n] = pOrder[n+1];
+            j--;
 
-        // get the ordering by decreasing priorit
-        pOrder = Pdr_ManSortByPriority( p, pCubeMin );
-    }
+            // success - update the cube
+            pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
+            Pdr_SetDeref( pCubeTmp );
+            assert( pCubeMin->nLits > 0 );
+            i--;
 
-    if ( p->pPars->fTwoRounds )
-    for ( j = 0; j < pCubeMin->nLits; j++ )
-    {
-        // use ordering
-//        i = j;
-        i = pOrder[j];
+            // get the ordering by decreasing priorit
+            pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+        }
 
-        // check init state
-        assert( pCubeMin->Lits[i] != -1 );
-        if ( Pdr_SetIsInit(pCubeMin, i) )
-            continue;
-        // try removing this literal
-        Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; 
-        RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
-        if ( RetValue == -1 )
+        if ( p->pPars->fTwoRounds )
+        for ( j = 0; j < pCubeMin->nLits; j++ )
         {
-            Pdr_SetDeref( pCubeMin );
-            return -1;
-        }
-        pCubeMin->Lits[i] = Lit;
-        if ( RetValue == 0 )
-            continue;
+            // use ordering
+    //        i = j;
+            i = pOrder[j];
 
-        // remove j-th entry
-        for ( n = j; n < pCubeMin->nLits-1; n++ )
-            pOrder[n] = pOrder[n+1];
-        j--;
+            // check init state
+            assert( pCubeMin->Lits[i] != -1 );
+            if ( Pdr_SetIsInit(pCubeMin, i) )
+                continue;
+            // try removing this literal
+            Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; 
+            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
+            if ( RetValue == -1 )
+            {
+                Pdr_SetDeref( pCubeMin );
+                return -1;
+            }
+            pCubeMin->Lits[i] = Lit;
+            if ( RetValue == 0 )
+                continue;
 
-        // success - update the cube
-        pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
-        Pdr_SetDeref( pCubeTmp );
-        assert( pCubeMin->nLits > 0 );
-        i--;
+            // remove j-th entry
+            for ( n = j; n < pCubeMin->nLits-1; n++ )
+                pOrder[n] = pOrder[n+1];
+            j--;
 
-        // get the ordering by decreasing priorit
-        pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+            // success - update the cube
+            pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
+            Pdr_SetDeref( pCubeTmp );
+            assert( pCubeMin->nLits > 0 );
+            i--;
+
+            // get the ordering by decreasing priorit
+            pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+        }
     }
 
     assert( ppCubeMin != NULL );