Improvements to 'satclp' (unfinished).

1 files changed, 163 insertions, 54 deletions

diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c
index 57138fce..fbff7679 100644
--- a/src/sat/bmc/bmcClp.c
+++ b/src/sat/bmc/bmcClp.c
@@ -396,17 +396,17 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t *
         Vec_IntWriteEntry( vLits, k, -1 );
         // put into new array
         Vec_IntClear( vTemp );
+        if ( fOnOffSetLit >= 0 )
+            Vec_IntPush( vTemp, fOnOffSetLit );
         Vec_IntForEachEntry( vLits, iLit, n )
             if ( iLit != -1 )
                 Vec_IntPush( vTemp, iLit );
         // check against offset
-        if ( fOnOffSetLit >= 0 )
-            Vec_IntPush( vTemp, fOnOffSetLit );
         if ( fProfile ) clk = Abc_Clock();
         status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 );
         if ( fProfile ) clkCheck2 += Abc_Clock() - clk;
-        if ( fOnOffSetLit >= 0 )
-            Vec_IntPop( vTemp );
+//        if ( fOnOffSetLit >= 0 )
+//            Vec_IntPop( vTemp );
         if ( status == l_Undef )
             return -1;
         if ( status == l_True )
@@ -477,6 +477,105 @@ int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLit
     return 0;
 }
 
+int Bmc_CollapseExpand2( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit )
+{
+    // perform one quick reduction if it is non-canonical
+    if ( !fCanon )
+    {
+        int i, k, iLit, j, iNum, status, nFinal, * pFinal;
+
+        // check against offset
+        if ( fOnOffSetLit >= 0 )
+            Vec_IntPush( vLits, fOnOffSetLit );
+        status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
+        if ( fOnOffSetLit >= 0 )
+            Vec_IntPop( vLits );
+        if ( status == l_Undef )
+            return -1;
+        assert( status == l_False );
+
+        // get subset of literals
+        nFinal = sat_solver_final( pSat, &pFinal );
+        Vec_IntClear( vNums );
+        Vec_IntClear( vTemp );
+        if ( fOnOffSetLit >= 0 )
+        {
+            //Vec_IntPush( vNums, -1 );
+            Vec_IntPush( vTemp, fOnOffSetLit );
+        }
+        Vec_IntForEachEntry( vLits, iLit, i )
+        {
+            for ( k = 0; k < nFinal; k++ )
+                if ( iLit == Abc_LitNot(pFinal[k]) )
+                    break;
+            if ( k == nFinal )
+                continue;
+            Vec_IntPush( vNums, i );
+            Vec_IntPush( vTemp, iLit );
+        }
+
+        // check against offset
+        status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef )
+            return -1;
+        assert( status == l_False );
+
+        // get subset of literals
+        nFinal = sat_solver_final( pSat, &pFinal );
+        j = 0;
+        Vec_IntForEachEntry( vTemp, iLit, i )
+        {
+            if ( iLit == fOnOffSetLit )
+                continue;
+            for ( k = 0; k < nFinal; k++ )
+                if ( iLit == Abc_LitNot(pFinal[k]) )
+                    break;
+            if ( k == nFinal )
+                continue;
+            Vec_IntWriteEntry( vNums, j++, Vec_IntEntry(vNums, i) );
+        }
+        Vec_IntShrink( vNums, j );
+
+
+        // try removing each literal
+        for ( i = 0; i < Vec_IntSize(vNums); i++ )
+        {
+            Vec_IntClear( vTemp );
+            if ( fOnOffSetLit >= 0 )
+                Vec_IntPush( vTemp, fOnOffSetLit );
+            Vec_IntForEachEntry( vNums, iNum, k )
+                if ( k != i )
+                    Vec_IntPush( vTemp, Vec_IntEntry(vLits, iNum) );
+            // check against offset
+            status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 );
+            if ( status == l_Undef )
+                return -1;
+            if ( status == l_True )
+                continue;
+            // remove literal
+            Vec_IntDrop( vNums, i );
+            i--;
+        }
+    }
+    else
+    {
+        Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon, -1 );
+        Bmc_CollapseExpandRound( pSat, NULL,   vLits, vNums, vTemp, nBTLimit, fCanon, -1 );
+    }
+/*
+    {
+        // put into new array
+        int i, iLit;
+        Vec_IntClear( vNums );
+        Vec_IntForEachEntry( vLits, iLit, i )
+            if ( iLit != -1 )
+                Vec_IntPush( vNums, i );
+        //printf( "%d(%d) ", Vec_IntSize(vNums), Vec_IntSize(vLits) );
+    }
+*/
+    return 0;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Returns SAT solver in the 'sat' state with the given assignment.]
@@ -658,8 +757,8 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
             else 
                 Vec_StrWriteEntry( vSop, Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) );
         }
-        if ( fVerbose )
-            printf( "Cube %4d: %s", Count, Vec_StrArray(vSop) + Start );
+        //if ( fVerbose )
+        //    printf( "Cube %4d: %s", Count, Vec_StrArray(vSop) + Start );
         Count++;
         // add cube
         status = sat_solver_addclause( pSat[0], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
@@ -687,7 +786,7 @@ cleanup:
         Bmc_CollapseIrredundant( vSop, Vec_StrSize(vSop)/(nVars +3), nVars );
     return vSop;
 }
-Vec_Str_t * Bmc_CollapseOne2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
+Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
 {
     Vec_Str_t * vSopOn, * vSopOff;
     int nCubesOn = ABC_INFINITY;
@@ -728,13 +827,11 @@ Vec_Str_t * Bmc_CollapseOne2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCa
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Str_t * Bmc_CollapseOne3( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
+Vec_Str_t * Bmc_CollapseOne_int3( sat_solver * pSat0, sat_solver * pSat1, sat_solver * pSat2, sat_solver * pSat3, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
 {
     int fVeryVerbose = fVerbose;
-    int nVars = Gia_ManCiNum(p);
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
-    sat_solver * pSat[2]      = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) };
-    sat_solver * pSatClean[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) };
+    sat_solver * pSat[2]      = { pSat0, pSat1 };
+    sat_solver * pSatClean[2] = { pSat2, pSat3 };
     Vec_Str_t * vSop[2]   = { Vec_StrAlloc(1000),  Vec_StrAlloc(1000)  }, * vRes = NULL;
     Vec_Int_t * vLitsC[2] = { Vec_IntAlloc(nVars), Vec_IntAlloc(nVars) };
     Vec_Int_t * vVars = Vec_IntAlloc( nVars );
@@ -746,7 +843,8 @@ Vec_Str_t * Bmc_CollapseOne3( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCa
     int fComplete[2] = {0};
 
     // collect CI variables
-    iCiVarBeg = pCnf->nVars - nVars;// - 1;
+//    iCiVarBeg = pCnf->nVars - nVars;// - 1;
+    iCiVarBeg = sat_solver_nvars(pSat0) - nVars;
     if ( fReverse )
         for ( v = nVars - 1; v >= 0; v-- )
             Vec_IntPush( vVars, iCiVarBeg + v );
@@ -855,11 +953,6 @@ cleanup:
     Vec_IntFree( vLitsC[1] );
     Vec_IntFree( vNums );
     Vec_IntFree( vCube );
-    Cnf_DataFree( pCnf );
-    sat_solver_delete( pSat[0] );
-    sat_solver_delete( pSat[1] );
-    sat_solver_delete( pSatClean[0] );
-    sat_solver_delete( pSatClean[1] );
     assert( !fComplete[0] || !fComplete[1] );
     if ( fComplete[0] || fComplete[1] ) // one of the cover is computed
     {
@@ -892,6 +985,22 @@ cleanup:
     Vec_StrFreeP( &vSop[1] );
     return vRes;
 }
+Vec_Str_t * Bmc_CollapseOne3( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
+{
+    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    sat_solver * pSat0 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
+    sat_solver * pSat1 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
+    sat_solver * pSat2 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
+    sat_solver * pSat3 = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
+    Vec_Str_t * vSop = Bmc_CollapseOne_int3( pSat0, pSat1, pSat2, pSat3, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
+    sat_solver_delete( pSat0 );
+    sat_solver_delete( pSat1 );
+    sat_solver_delete( pSat2 );
+    sat_solver_delete( pSat3 );
+    Cnf_DataFree( pCnf );
+    return vSop;
+}
+
 
 /**Function*************************************************************
 
@@ -904,10 +1013,11 @@ cleanup:
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
+Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat1, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
 {
     int fVeryVerbose = fVerbose;
-    Vec_Str_t * vSop[2]   = { Vec_StrAlloc(1000),  Vec_StrAlloc(1000)  }, * vRes = NULL;
+    sat_solver * pSat[2] = { pSat1, pSat2 };
+    Vec_Str_t * vSop[2]  = { Vec_StrAlloc(1000),  Vec_StrAlloc(1000)  }, * vRes = NULL;
     Vec_Int_t * vVars = Vec_IntAlloc( nVars+1 );
     Vec_Int_t * vLits = Vec_IntAlloc( nVars+1 );
     Vec_Int_t * vNums = Vec_IntAlloc( nVars+1 );
@@ -935,7 +1045,7 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, int nVars, int nCubeLim, in
     for ( n = 0; n < 2; n++ )
     {
         pLits[0] = Abc_Var2Lit( iOutVar, n ); // n=0 => F=1   n=1 => F=0
-        status = sat_solver_solve( pSat, pLits, pLits + 1, nBTLimit, 0, 0, 0 );
+        status = sat_solver_solve( pSat[n], pLits, pLits + 1, nBTLimit, 0, 0, 0 );
         if ( status == l_Undef )
             goto cleanup; // timeout
         if ( status == l_False )
@@ -946,6 +1056,9 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, int nVars, int nCubeLim, in
             fComplete[0] = 1;
             goto cleanup; // const0/1
         }
+        // add literals to the solver
+        status = sat_solver_addclause( pSat[n], pLits, pLits + 1 );
+        assert( status );
         // start cover
         Vec_StrPush( vSop[n], '\0' );
     }
@@ -957,10 +1070,11 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, int nVars, int nCubeLim, in
         {
             if ( fVeryVerbose ) clk = Abc_Clock();
             // get the assignment
-            sat_solver_clean_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) );
-            pLits[0] = Abc_Var2Lit( iOutVar, n );    // set output
-            pLits[1] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses
-            status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
+            sat_solver_clean_polarity( pSat[n], Vec_IntArray(vVars), Vec_IntSize(vVars) );
+            pLits[0] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses
+//            pLits[1] = Abc_Var2Lit( iOutVar, n );    // set output
+//            status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
+            status = sat_solver_solve( pSat[n], pLits, pLits + 1, 0, 0, 0, 0 );
             if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk;
             if ( status == l_Undef )
                 goto cleanup; // timeout
@@ -972,10 +1086,11 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, int nVars, int nCubeLim, in
             // collect values
             Vec_IntClear( vLits );
             Vec_IntForEachEntry( vVars, iVar, v )
-                Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat, iVar)) );
+                Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[n], iVar)) );
             // expand the values
             if ( fVeryVerbose ) clk = Abc_Clock();
-            status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) );
+//            status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) );
+            status = Bmc_CollapseExpand( pSat[!n], NULL, vLits, vNums, vCube, nBTLimit, fCanon, -1 );
             if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk;
             if ( status < 0 )
                 goto cleanup; // timeout
@@ -999,7 +1114,8 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, int nVars, int nCubeLim, in
             }
             // add cube
             Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) );
-            status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) );
+//            status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) );
+            status = sat_solver_addclause( pSat[n], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
             if ( status == 0 )
             {
                 fComplete[n] = 1;
@@ -1047,15 +1163,6 @@ cleanup:
     Vec_StrFreeP( &vSop[1] );
     return vRes;
 }
-Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
-{
-    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
-    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
-    Vec_Str_t * vSop = Bmc_CollapseOne_int2( pSat, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
-    sat_solver_delete( pSat );
-    Cnf_DataFree( pCnf );
-    return vSop;
-}
 
 
 /**Function*************************************************************
@@ -1069,11 +1176,10 @@ Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCan
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
+Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
 {
     int fVeryVerbose = fVerbose;
-    sat_solver * pSat[2] = { pSat1, pSat2 };
-    Vec_Str_t * vSop[2]  = { Vec_StrAlloc(1000),  Vec_StrAlloc(1000)  }, * vRes = NULL;
+    Vec_Str_t * vSop[2]   = { Vec_StrAlloc(1000),  Vec_StrAlloc(1000)  }, * vRes = NULL;
     Vec_Int_t * vVars = Vec_IntAlloc( nVars+1 );
     Vec_Int_t * vLits = Vec_IntAlloc( nVars+1 );
     Vec_Int_t * vNums = Vec_IntAlloc( nVars+1 );
@@ -1101,7 +1207,7 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVa
     for ( n = 0; n < 2; n++ )
     {
         pLits[0] = Abc_Var2Lit( iOutVar, n ); // n=0 => F=1   n=1 => F=0
-        status = sat_solver_solve( pSat[n], pLits, pLits + 1, nBTLimit, 0, 0, 0 );
+        status = sat_solver_solve( pSat, pLits, pLits + 1, nBTLimit, 0, 0, 0 );
         if ( status == l_Undef )
             goto cleanup; // timeout
         if ( status == l_False )
@@ -1112,9 +1218,6 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVa
             fComplete[0] = 1;
             goto cleanup; // const0/1
         }
-        // add literals to the solver
-        status = sat_solver_addclause( pSat[n], pLits, pLits + 1 );
-        assert( status );
         // start cover
         Vec_StrPush( vSop[n], '\0' );
     }
@@ -1126,11 +1229,10 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVa
         {
             if ( fVeryVerbose ) clk = Abc_Clock();
             // get the assignment
-            sat_solver_clean_polarity( pSat[n], Vec_IntArray(vVars), Vec_IntSize(vVars) );
+            sat_solver_clean_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) );
             pLits[0] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses
-//            pLits[1] = Abc_Var2Lit( iOutVar, n );    // set output
-//            status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
-            status = sat_solver_solve( pSat[n], pLits, pLits + 1, 0, 0, 0, 0 );
+            pLits[1] = Abc_Var2Lit( iOutVar, n );    // set output
+            status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
             if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk;
             if ( status == l_Undef )
                 goto cleanup; // timeout
@@ -1142,11 +1244,10 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVa
             // collect values
             Vec_IntClear( vLits );
             Vec_IntForEachEntry( vVars, iVar, v )
-                Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[n], iVar)) );
+                Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat, iVar)) );
             // expand the values
             if ( fVeryVerbose ) clk = Abc_Clock();
-//            status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) );
-            status = Bmc_CollapseExpand( pSat[!n], NULL, vLits, vNums, vCube, nBTLimit, fCanon, -1 );
+            status = Bmc_CollapseExpand( pSat, NULL, vLits, vNums, vCube, nBTLimit, fCanon, Abc_Var2Lit(iOutVar, !n) );
             if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk;
             if ( status < 0 )
                 goto cleanup; // timeout
@@ -1159,6 +1260,7 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVa
             Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' );
             Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' );
             Vec_IntClear( vCube );
+            Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) );
             Vec_IntForEachEntry( vNums, iVar, v )
             {
                 int iLit = Vec_IntEntry( vLits, iVar );
@@ -1169,9 +1271,7 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat1, sat_solver * pSat2, int nVa
                     Vec_StrWriteEntry( vSop[n], Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) );
             }
             // add cube
-            Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) );
-//            status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) );
-            status = sat_solver_addclause( pSat[n], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
+            status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) );
             if ( status == 0 )
             {
                 fComplete[n] = 1;
@@ -1219,6 +1319,15 @@ cleanup:
     Vec_StrFreeP( &vSop[1] );
     return vRes;
 }
+Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
+{
+    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
+    Vec_Str_t * vSop = Bmc_CollapseOne_int( pSat, Gia_ManCiNum(p), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
+    sat_solver_delete( pSat );
+    Cnf_DataFree( pCnf );
+    return vSop;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///