Adding alternative generalization procedure.

2 files changed, 159 insertions, 7 deletions

diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 501f9be6..0394040f 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -497,7 +497,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Vec_IntSelectSortCostReverseLit( int * pArray, int nSize, Vec_Int_t * vCosts )
+static inline int Vec_IntSelectSortCostReverseLit( int * pArray, int nSize, Vec_Int_t * vCosts )
 {
     int i, j, best_i;
     for ( i = 0; i < nSize-1; i++ )
@@ -508,6 +508,137 @@ static inline void Vec_IntSelectSortCostReverseLit( int * pArray, int nSize, Vec
                 best_i = j;
         ABC_SWAP( int, pArray[i], pArray[best_i] );
     }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs generalization using a different idea.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppCubeMin )
+{
+    int fUseMinAss = 0;
+    sat_solver * pSat = Pdr_ManFetchSolver( p, k );
+    int Order = Vec_IntSelectSortCostReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
+    Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
+    int RetValue, Count = 0, iLit, Lits[2], nLits = Vec_IntSize( vLits1 );
+    // create free variables
+    int i, iUseVar, iAndVar;
+    iAndVar = Pdr_ManFreeVar(p, k);
+    for ( i = 1; i < nLits; i++ )
+        Pdr_ManFreeVar(p, k);
+    iUseVar = Pdr_ManFreeVar(p, k);
+    for ( i = 1; i < nLits; i++ )
+        Pdr_ManFreeVar(p, k);
+    assert( iUseVar == iAndVar + nLits );
+    // if there is only one positive literal, put it in front and always assume
+    if ( fUseMinAss )
+    {
+        for ( i = 0; i < pCube->nLits; i++ )
+            Count += !Abc_LitIsCompl(pCube->Lits[i]);
+        if ( Count == 1 )
+        {
+            for ( i = 0; i < pCube->nLits; i++ )
+                if ( !Abc_LitIsCompl(pCube->Lits[i]) )
+                    break;
+            assert( i < pCube->nLits );
+            ABC_SWAP( int, pCube->Lits[0], pCube->Lits[i] );
+        }
+    }
+    // add clauses for the additional AND-gates
+    Vec_IntForEachEntry( vLits1, iLit, i )
+    {
+        sat_solver_add_buffer_enable( pSat, iAndVar + i, Abc_Lit2Var(iLit), iUseVar + i, Abc_LitIsCompl(iLit) );
+        Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iAndVar + i, 0) );
+    }
+    // add clauses for the additional OR-gate
+    RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits1), Vec_IntLimit(vLits1) );
+    assert( RetValue == 1 );
+    // add implications
+    vLits1 = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
+    assert( Vec_IntSize(vLits1) == nLits );
+    Vec_IntForEachEntry( vLits1, iLit, i )
+    {
+        Lits[0] = Abc_Var2Lit(iUseVar + i, 1);
+        Lits[1] = iLit;
+        RetValue = sat_solver_addclause( pSat, Lits, Lits+2 );
+        assert( RetValue == 1 );
+        Vec_IntWriteEntry( vLits1, i, Abc_Var2Lit(iUseVar + i, 0) );
+    }
+    sat_solver_compress( pSat );
+    // perform minimization
+    if ( fUseMinAss )
+    {
+        if ( Count == 1 )
+        {
+            if ( !sat_solver_push(pSat, Vec_IntEntry(vLits1, 0)) ) // UNSAT after assuming the first (mandatory) literal
+                nLits = 1;
+            else
+                nLits = 1 + sat_solver_minimize_assumptions( pSat, Vec_IntArray(vLits1)+1, nLits-1, p->pPars->nConfLimit );
+            sat_solver_pop(pSat); // unassume the first literal
+        }
+        else
+            nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vLits1), nLits, p->pPars->nConfLimit );
+        Vec_IntShrink( vLits1, nLits );
+    }
+    else
+    {
+        int k, Entry;
+        // try removing one literal at a time in the old-fashioned way
+        Vec_Int_t * vTemp = Vec_IntAlloc( nLits );
+        for ( i = 0; i < nLits; i++ )
+        {
+            // check init state
+            if ( Pdr_SetIsInit(pCube, i) )
+                continue;
+            // load remaining literals
+            Vec_IntClear( vTemp );
+            Vec_IntForEachEntry( vLits1, Entry, k )
+                if ( Entry != -1 && k != i )
+                    Vec_IntPush( vTemp, Entry );
+            // solve with assumptions
+            RetValue = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), p->pPars->nConfLimit, 0, 0, 0 );
+            if ( RetValue == l_False )
+                Vec_IntWriteEntry( vLits1, i, -1 );
+        }
+        Vec_IntFree( vTemp );
+        // compact
+        k = 0;
+        Vec_IntForEachEntry( vLits1, Entry, i )
+            if ( Entry != -1 )
+                Vec_IntWriteEntry( vLits1, k++, Entry );
+        Vec_IntShrink( vLits1, k );
+    }
+    // remap auxiliary literals into original literals
+    Vec_IntForEachEntry( vLits1, iLit, i )
+        Vec_IntWriteEntry( vLits1, i, pCube->Lits[Abc_Lit2Var(iLit)-iUseVar] );
+    // make sure the cube has at least one positive literal
+    if ( fUseMinAss )
+    {
+        Vec_IntForEachEntry( vLits1, iLit, i )
+            if ( !Abc_LitIsCompl(iLit) )
+                break;
+        if ( i == Vec_IntSize(vLits1) )
+        {
+            // find positive lit in the cube
+            for ( i = 0; i < pCube->nLits; i++ )
+                if ( !Abc_LitIsCompl(pCube->Lits[i]) )
+                    break;
+            assert( i < pCube->nLits );
+            Vec_IntPush( vLits1, pCube->Lits[i] );
+        }
+    }
+    // create a subset cube
+    *ppCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits1), Vec_IntSize(vLits1) );
+    assert( !Pdr_SetIsInit(*ppCubeMin, -1) );
+    return 0;
 }
 
 /**Function*************************************************************
@@ -543,8 +674,6 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
         p->tGeneral += clock() - clk;
         return 0;
     }
-    
-    keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 );
 
     // reduce clause using assumptions
 //    pCubeMin = Pdr_SetDup( pCube );
@@ -552,6 +681,31 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
     if ( pCubeMin == NULL )
         pCubeMin = Pdr_SetDup( pCube );
 
+    // perform simplified generalization
+    if ( p->pPars->fSimpleGeneral )
+    {
+        assert( pCubeMin->nLits > 0 );
+        if ( pCubeMin->nLits > 1 )
+        {
+            RetValue = Pdr_ManGeneralize2( p, k, pCubeMin, ppCubeMin );
+            Pdr_SetDeref( pCubeMin );
+            assert( ppCubeMin != NULL );
+            pCubeMin = *ppCubeMin;
+        }
+        *ppCubeMin = pCubeMin;
+        if ( p->pPars->fVeryVerbose )
+        {
+            printf("Cube:\n");
+            for ( i = 0; i < pCubeMin->nLits; i++)
+                printf ("%d ", pCubeMin->Lits[i]);
+            printf("\n");
+        }
+        p->tGeneral += Abc_Clock() - clk;
+        return 1;
+    }
+    
+    keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 );
+
     // perform generalization
     if ( !p->pPars->fSkipGeneral )
     {
@@ -691,9 +845,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
     {
         printf("Cube:\n");
         for ( i = 0; i < pCubeMin->nLits; i++)
-        {
-          printf ("%d ", pCubeMin->Lits[i]);
-        }
+            printf ("%d ", pCubeMin->Lits[i]);
         printf("\n");
     }
     *ppCubeMin = pCubeMin;
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 3d24161e..47fba5e3 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -2178,7 +2178,7 @@ int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int
     if ( nLits == 1 )
     {
         // since the problem is UNSAT, we will try to solve it without assuming the last literal
-        // the result is UNSAT, the last literal can be dropped; otherwise, it is needed
+        // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
         int status = l_False;
         int Temp = s->nConfLimit; 
         s->nConfLimit = nConfLimit;