Improvements to 'satclp' (unfinished).

2 files changed, 194 insertions, 69 deletions

diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index f9b02fda..653618c5 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -643,12 +643,15 @@ int Abc_NtkCollapseCountVars( Vec_Str_t * vSop, Vec_Int_t * vSupp )
   SeeAlso     []
 
 ***********************************************************************/
-sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_t * vSupp, Vec_Int_t * vAnds, Vec_Int_t * vMap, sat_solver ** ppSat )
+sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_t * vSupp, Vec_Int_t * vAnds, Vec_Int_t * vMap, sat_solver ** ppSat1, sat_solver ** ppSat2, sat_solver ** ppSat3 )
 {
     int i, k, iObj, status, nVars = 2;
+//    int i, k, iObj, status, nVars = 1;
     Vec_Int_t * vLits = Vec_IntAlloc( 16 );
     sat_solver * pSat = sat_solver_new();
-    if ( ppSat ) *ppSat = sat_solver_new();
+    if ( ppSat1 ) *ppSat1 = sat_solver_new();
+    if ( ppSat2 ) *ppSat2 = sat_solver_new();
+    if ( ppSat3 ) *ppSat3 = sat_solver_new();
     // assign SAT variable numbers
     Vec_IntWriteEntry( vMap, iCoObjId, nVars++ );
     Vec_IntForEachEntry( vSupp, iObj, k )
@@ -656,9 +659,13 @@ sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_
     Vec_IntForEachEntry( vAnds, iObj, k )
         if ( pCnf->pObj2Clause[iObj] != -1 )
             Vec_IntWriteEntry( vMap, iObj, nVars++ );
+//    Vec_IntForEachEntry( vSupp, iObj, k )
+//        Vec_IntWriteEntry( vMap, iObj, nVars++ );
     // create clauses for the internal nodes and for the output
     sat_solver_setnvars( pSat, nVars );
-    if ( ppSat ) sat_solver_setnvars( *ppSat, nVars );
+    if ( ppSat1 ) sat_solver_setnvars( *ppSat1, nVars );
+    if ( ppSat2 ) sat_solver_setnvars( *ppSat2, nVars );
+    if ( ppSat3 ) sat_solver_setnvars( *ppSat3, nVars );
     Vec_IntPush( vAnds, iCoObjId );
     Vec_IntForEachEntry( vAnds, iObj, k )
     {
@@ -676,7 +683,9 @@ sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_
             status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
             assert( status );
             (void) status;
-            if ( ppSat ) sat_solver_addclause( *ppSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
+            if ( ppSat1 ) sat_solver_addclause( *ppSat1, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
+            if ( ppSat2 ) sat_solver_addclause( *ppSat2, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
+            if ( ppSat3 ) sat_solver_addclause( *ppSat3, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
         }
     }
     Vec_IntPop( vAnds );
@@ -696,15 +705,15 @@ sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t * vSupp )
+Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, int fVerbose )
 {
     Vec_Str_t * vSop;
     abctime clk = Abc_Clock();
-    extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
+    extern Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
     Gia_Man_t * pGia  = Gia_ManDupCones( p, &iCo, 1, 1 );
     if ( fVerbose )
         printf( "Output %4d:  Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Gia_ManAndNum(pGia) );
-    vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
+    vSop = Bmc_CollapseOneOld( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
     Gia_ManStop( pGia );
     if ( vSop == NULL )
         return NULL;
@@ -718,13 +727,15 @@ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     return vSop; 
 }
-Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t * vSupp, Vec_Int_t * vMap )
+Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, Vec_Int_t * vMap, int fVerbose )
 {
     Vec_Str_t * vSop;
-    sat_solver * pSat, * pSat2 = NULL;
+    sat_solver * pSat, * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL;
     Gia_Obj_t * pObj;
     abctime clk = Abc_Clock();
-    extern Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
+    extern Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
+    extern Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, sat_solver * pSat2, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
+    extern Vec_Str_t * Bmc_CollapseOne_int3( sat_solver * pSat, sat_solver * pSat1, sat_solver * pSat2, sat_solver * pSat3, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
     int i, iCoObjId = Gia_ObjId( p, Gia_ManCo(p, iCo) );
     Vec_Int_t * vAnds = Vec_IntAlloc( 100 );
     Vec_Int_t * vSuppObjs = Vec_IntAlloc( 100 );
@@ -733,13 +744,18 @@ Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCu
     Gia_ManIncrementTravId( p );
     Gia_ManCollectAnds( p, &iCoObjId, 1, vAnds );
     assert( Vec_IntSize(vAnds) > 0 );
-    pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat2 );
+//    pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat1, &pSat2, &pSat3 );
+    pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, NULL, NULL, NULL );
     Vec_IntFree( vSuppObjs );
     if ( fVerbose )
         printf( "Output %4d:  Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Vec_IntSize(vAnds) );
-    vSop = Bmc_CollapseOne_int( pSat, pSat2, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
+//    vSop = Bmc_CollapseOne_int3( pSat, pSat1, pSat2, pSat3, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
+//    vSop = Bmc_CollapseOne_int2( pSat, pSat1, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
+    vSop = Bmc_CollapseOne_int( pSat, Vec_IntSize(vSupp), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
     sat_solver_delete( pSat );
-    sat_solver_delete( pSat2 );
+    if ( pSat1 ) sat_solver_delete( pSat1 );
+    if ( pSat2 ) sat_solver_delete( pSat2 );
+    if ( pSat3 ) sat_solver_delete( pSat3 );
     Vec_IntFree( vAnds );
     if ( vSop == NULL )
         return NULL;
@@ -794,8 +810,8 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
             Vec_PtrWriteEntry( vSopsRepr, iEntry, (void *)(ABC_PTRINT_T)1 );
             continue;
         }
-//        vSop  = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp );
-        vSop  = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp, vMap );
+      vSop  = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, i ? 0 : fVerbose );
+//      vSop  = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, vMap, i ? 0 : fVerbose );
         if ( vSop == NULL )
             goto finish;
         assert( Vec_IntSize( Vec_WecEntry(vSupps, iCoThis) ) == Abc_SopGetVarNum(Vec_StrArray(vSop)) );
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                                ///