Improvements to 'satclp' (unfinished).

3 files changed, 457 insertions, 11 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 4ad3e39a..87ce6b91 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1038,6 +1038,8 @@ static inline int         Gia_ObjCellId( Gia_Man_t * p, int iLit )          { re
     for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ )
 #define Gia_ManForEachCiId( p, Id, i )                                  \
     for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((Id) = Gia_ObjId(p, Gia_ManCi(p, i))); i++ )
+#define Gia_ManForEachCiVec( vVec, p, pObj, i )                         \
+    for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManCi(p, Vec_IntEntry(vVec,i))); i++ )
 #define Gia_ManForEachCiReverse( p, pObj, i )                           \
     for ( i = Vec_IntSize(p->vCis) - 1; (i >= 0) && ((pObj) = Gia_ManCi(p, i)); i-- )
 #define Gia_ManForEachCo( p, pObj, i )                                  \
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index ac7bcdc5..f9b02fda 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -21,6 +21,8 @@
 #include "base/abc/abc.h"
 #include "aig/gia/gia.h"
 #include "misc/vec/vecWec.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satStore.h"
 
 #ifdef ABC_USE_CUDD
 #include "bdd/extrab/extraBdd.h"
@@ -535,6 +537,8 @@ extern Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose );
 extern int         Gia_ManCoLargestSupp( Gia_Man_t * p, Vec_Wec_t * vSupps );
 extern Vec_Wec_t * Gia_ManIsoStrashReduceInt( Gia_Man_t * p, Vec_Wec_t * vSupps, int fVerbose );
 
+extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
+
 /**Function*************************************************************
 
   Synopsis    [Derives GIA for the network.]
@@ -622,12 +626,67 @@ int Abc_NtkCollapseCountVars( Vec_Str_t * vSop, Vec_Int_t * vSupp )
             Vec_IntWriteEntry( vSupp, j++, iVar );
     Vec_IntShrink( vSupp, j );
     Vec_IntFree( vPres );
+//    if ( Vec_IntSize(vSupp) != Abc_SopGetVarNum(Vec_StrArray(vSop)) )
+//        printf( "Mismatch!!!\n" );
     return 1;
 }
 
 
 /**Function*************************************************************
 
+  Synopsis    [Derives SAT solver for one output from the shared CNF.]
+
+  Description []
+               
+  SideEffects []
+
+  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 )
+{
+    int i, k, iObj, status, nVars = 2;
+    Vec_Int_t * vLits = Vec_IntAlloc( 16 );
+    sat_solver * pSat = sat_solver_new();
+    if ( ppSat ) *ppSat = sat_solver_new();
+    // assign SAT variable numbers
+    Vec_IntWriteEntry( vMap, iCoObjId, nVars++ );
+    Vec_IntForEachEntry( vSupp, iObj, k )
+        Vec_IntWriteEntry( vMap, iObj, nVars++ );
+    Vec_IntForEachEntry( vAnds, iObj, k )
+        if ( pCnf->pObj2Clause[iObj] != -1 )
+            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 );
+    Vec_IntPush( vAnds, iCoObjId );
+    Vec_IntForEachEntry( vAnds, iObj, k )
+    {
+        int iClaBeg, iClaEnd, * pLit;
+        if ( pCnf->pObj2Clause[iObj] == -1 )
+            continue;
+        iClaBeg = pCnf->pObj2Clause[iObj];
+        iClaEnd = iClaBeg + pCnf->pObj2Count[iObj];
+        assert( iClaBeg < iClaEnd );
+        for ( i = iClaBeg; i < iClaEnd; i++ )
+        {
+            Vec_IntClear( vLits );
+            for ( pLit = pCnf->pClauses[i]; pLit < pCnf->pClauses[i+1]; pLit++ )
+                Vec_IntPush( vLits, Abc_Lit2LitV(Vec_IntArray(vMap), *pLit) );
+            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) );
+        }
+    }
+    Vec_IntPop( vAnds );
+    Vec_IntFree( vLits );
+    assert( nVars == sat_solver_nvars(pSat) );
+    return pSat;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes SOPs for each output.]
 
   Description []
@@ -651,8 +710,43 @@ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit
         return NULL;
     if ( Vec_StrSize(vSop) == 4 ) // constant
         Vec_IntClear(vSupp);
-    else
-        Abc_NtkCollapseCountVars( vSop, vSupp );
+//    else
+//        Abc_NtkCollapseCountVars( vSop, vSupp );
+    if ( fVerbose )
+        printf( "Supp new = %4d. Sop = %4d.  ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) );
+    if ( fVerbose )
+        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 * vSop;
+    sat_solver * pSat, * pSat2 = 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 );
+    int i, iCoObjId = Gia_ObjId( p, Gia_ManCo(p, iCo) );
+    Vec_Int_t * vAnds = Vec_IntAlloc( 100 );
+    Vec_Int_t * vSuppObjs = Vec_IntAlloc( 100 );
+    Gia_ManForEachCiVec( vSupp, p, pObj, i )
+        Vec_IntPush( vSuppObjs, Gia_ObjId(p, pObj) );
+    Gia_ManIncrementTravId( p );
+    Gia_ManCollectAnds( p, &iCoObjId, 1, vAnds );
+    assert( Vec_IntSize(vAnds) > 0 );
+    pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat2 );
+    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 );
+    sat_solver_delete( pSat );
+    sat_solver_delete( pSat2 );
+    Vec_IntFree( vAnds );
+    if ( vSop == NULL )
+        return NULL;
+    if ( Vec_StrSize(vSop) == 4 ) // constant
+        Vec_IntClear(vSupp);
+//    else
+//        Abc_NtkCollapseCountVars( vSop, vSupp );
     if ( fVerbose )
         printf( "Supp new = %4d. Sop = %4d.  ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) );
     if ( fVerbose )
@@ -667,6 +761,8 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
     Vec_Int_t * vReprs, * vClass, * vReprSuppSizes;
     int i, k, Entry, iCo, * pOrder;
     Vec_Wec_t * vClasses;
+    Cnf_Dat_t * pCnf;
+    Vec_Int_t * vMap;
     // derive classes of outputs
     vClasses = Gia_ManIsoStrashReduceInt( p, vSupps, 0 );
     if ( fVerbose )
@@ -682,6 +778,8 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
     pOrder = Abc_MergeSortCost( Vec_IntArray(vReprSuppSizes), Vec_IntSize(vReprSuppSizes) );
     Vec_IntFree( vReprSuppSizes );
     // consider SOPs for representatives
+    vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
+    pCnf = Mf_ManGenerateCnf( p, 8, 1, 0, 0 );
     vSopsRepr = Vec_PtrStart( Vec_IntSize(vReprs) );
     pProgress = Extra_ProgressBarStart( stdout, Vec_IntSize(vReprs) );
     Extra_ProgressBarUpdate( pProgress, 0, NULL );
@@ -690,7 +788,14 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
         int iEntry        = pOrder[Vec_IntSize(vReprs) - 1 - i];
         int iCoThis       = Vec_IntEntry( vReprs, iEntry );
         Vec_Int_t * vSupp = Vec_WecEntry( vSupps, iCoThis );
-        Vec_Str_t * vSop  = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, i ? 0 : fVerbose, fCanon, fReverse, vSupp );
+        Vec_Str_t * vSop;
+        if ( Vec_IntSize(vSupp) < 2 )
+        {
+            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 );
         if ( vSop == NULL )
             goto finish;
         assert( Vec_IntSize( Vec_WecEntry(vSupps, iCoThis) ) == Abc_SopGetVarNum(Vec_StrArray(vSop)) );
@@ -699,6 +804,8 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
         Vec_StrFree( vSop );
     }
     Extra_ProgressBarStop( pProgress );
+    Cnf_DataFree( pCnf );
+    Vec_IntFree( vMap );
     // derive SOPs for each output
     vSops = Vec_PtrStart( Gia_ManCoNum(p) );
     Vec_WecForEachLevel ( vClasses, vClass, i )
@@ -787,6 +894,7 @@ Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, in
         Vec_IntForEachEntry( vSupp, iCi, k )
             Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) );
         pNodeNew->pData = Vec_PtrEntry( vSops, i );
+        assert( pNodeNew->pData != (void *)(ABC_PTRINT_T)1 );
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     }
     Vec_WecFree( vSupps );
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c
index 826c0a32..57138fce 100644
--- a/src/sat/bmc/bmcClp.c
+++ b/src/sat/bmc/bmcClp.c
@@ -355,7 +355,7 @@ int Bmc_CollapseIrredundantFull( Vec_Str_t * vSop, int nCubes, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon )
+int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon, int fOnOffSetLit )
 {
     int fProfile = 0;
     int k, n, iLit, status;
@@ -369,6 +369,7 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t *
         // check if this literal when expanded overlaps with the on-set
         if ( pSatOn )
         {
+            assert( fOnOffSetLit == -1 );
             // it is ok to skip the first round if the literal is positive
             if ( fCanon && !Abc_LitIsCompl(Save) )
                 continue;
@@ -399,9 +400,13 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t *
             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 ( status == l_Undef )
             return -1;
         if ( status == l_True )
@@ -428,14 +433,18 @@ int Bmc_CollapseExpandRound( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t *
   SeeAlso     []
 
 ***********************************************************************/
-int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit, int fCanon )
+int Bmc_CollapseExpand( 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, 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 );
@@ -450,12 +459,12 @@ int Bmc_CollapseExpand( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLit
             if ( k == nFinal )
                 Vec_IntWriteEntry( vLits, i, -1 );
         }
-        Bmc_CollapseExpandRound( pSat, NULL,   vLits, vNums, vTemp, nBTLimit, fCanon );
+        Bmc_CollapseExpandRound( pSat, NULL,   vLits, vNums, vTemp, nBTLimit, fCanon, fOnOffSetLit );
     }
     else
     {
-        Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon );
-        Bmc_CollapseExpandRound( pSat, NULL,   vLits, vNums, vTemp, nBTLimit, fCanon );
+        Bmc_CollapseExpandRound( pSat, pSatOn, vLits, vNums, vTemp, nBTLimit, fCanon, -1 );
+        Bmc_CollapseExpandRound( pSat, NULL,   vLits, vNums, vTemp, nBTLimit, fCanon, -1 );
     }
     {
         // put into new array
@@ -625,7 +634,7 @@ Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
             printf( "\n" );
         }
         // expand the values
-        status = Bmc_CollapseExpand( pSat[1], fCanon ? pSat[2] : pSat[0], vLits, vNums, vCube, nBTLimit, fCanon );
+        status = Bmc_CollapseExpand( pSat[1], fCanon ? pSat[2] : pSat[0], vLits, vNums, vCube, nBTLimit, fCanon, -1 );
         if ( status < 0 )
         {
             Vec_StrFreeP( &vSop );
@@ -719,7 +728,7 @@ Vec_Str_t * Bmc_CollapseOne2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCa
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
+Vec_Str_t * Bmc_CollapseOne3( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
 {
     int fVeryVerbose = fVerbose;
     int nVars = Gia_ManCiNum(p);
@@ -805,7 +814,7 @@ Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCan
             }
             // expand the values
             if ( fVeryVerbose ) clk = Abc_Clock();
-            status = Bmc_CollapseExpand( pSatClean[!n], pSat[n], vLits, vNums, vCube, nBTLimit, fCanon );
+            status = Bmc_CollapseExpand( pSatClean[!n], pSat[n], vLits, vNums, vCube, nBTLimit, fCanon, -1 );
             if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk;
             if ( status < 0 )
                 goto cleanup; // timeout
@@ -884,6 +893,333 @@ cleanup:
     return vRes;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [This code computes on-set and off-set simultaneously.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat, 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;
+    Vec_Int_t * vVars = Vec_IntAlloc( nVars+1 );
+    Vec_Int_t * vLits = Vec_IntAlloc( nVars+1 );
+    Vec_Int_t * vNums = Vec_IntAlloc( nVars+1 );
+    Vec_Int_t * vCube = Vec_IntAlloc( nVars+1 );
+    int n, v, iVar, pLits[2], iCube = 0, Start, status;
+    abctime clk = 0, Time[2][2] = {{0}};
+    int fComplete[2] = {0};
+    // variables
+    int iOutVar    = 2;
+    int iOOVars[2] = {0, 1};
+//    int iOutVar    = 1;
+//    int iOOVars[2] = {sat_solver_nvars(pSat) - 5, sat_solver_nvars(pSat) - 5 + 1};
+
+    // collect CI variables (0 = onset enable, 1 = offset enable, 2 = output)
+    int iCiVarBeg = 3;
+//    int iCiVarBeg = sat_solver_nvars(pSat) - 5 - nVars;
+    if ( fReverse )
+        for ( v = nVars - 1; v >= 0; v-- )
+            Vec_IntPush( vVars, iCiVarBeg + v );
+    else
+        for ( v = 0; v < nVars; v++ )
+            Vec_IntPush( vVars, iCiVarBeg + v );
+
+    // check that on-set/off-set is sat
+    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 );
+        if ( status == l_Undef )
+            goto cleanup; // timeout
+        if ( status == l_False )
+        {
+            Vec_StrClear( vSop[0] );
+            Vec_StrPrintStr( vSop[0], n ? " 1\n" : " 0\n" );
+            Vec_StrPush( vSop[0], '\0' );
+            fComplete[0] = 1;
+            goto cleanup; // const0/1
+        }
+        // start cover
+        Vec_StrPush( vSop[n], '\0' );
+    }
+
+    // compute cube pairs
+    for ( iCube = 0; nCubeLim == 0 || iCube < nCubeLim; iCube++ )
+    {
+        for ( n = 0; n < 2; n++ )
+        {
+            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 );
+            if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk;
+            if ( status == l_Undef )
+                goto cleanup; // timeout
+            if ( status == l_False )
+            {
+                fComplete[n] = 1;
+                break;
+            }
+            // collect values
+            Vec_IntClear( vLits );
+            Vec_IntForEachEntry( vVars, iVar, v )
+                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) );
+            if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk;
+            if ( status < 0 )
+                goto cleanup; // timeout
+            // collect cube
+            Vec_StrPop( vSop[n] );
+            Start = Vec_StrSize( vSop[n] );
+            Vec_StrFillExtra( vSop[n], Start + nVars + 4, '-' );
+            Vec_StrWriteEntry( vSop[n], Start + nVars + 0, ' ' );
+            Vec_StrWriteEntry( vSop[n], Start + nVars + 1, (char)(n ? '0' : '1') );
+            Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' );
+            Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' );
+            Vec_IntClear( vCube );
+            Vec_IntForEachEntry( vNums, iVar, v )
+            {
+                int iLit = Vec_IntEntry( vLits, iVar );
+                Vec_IntPush( vCube, Abc_LitNot(iLit) );
+                if ( fReverse )
+                    Vec_StrWriteEntry( vSop[n], Start + nVars - iVar - 1, (char)('0' + !Abc_LitIsCompl(iLit)) );
+                else 
+                    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) );
+            if ( status == 0 )
+            {
+                fComplete[n] = 1;
+                break;
+            }
+            assert( status == 1 );
+        }
+        if ( fComplete[0] || fComplete[1] )
+            break;
+    }
+cleanup:
+    Vec_IntFree( vVars );
+    Vec_IntFree( vLits );
+    Vec_IntFree( vNums );
+    Vec_IntFree( vCube );
+    assert( !fComplete[0] || !fComplete[1] );
+    if ( fComplete[0] || fComplete[1] ) // one of the cover is computed
+    {
+        vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL;
+        if ( iCube > 1 )
+//            Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
+            Bmc_CollapseIrredundantFull( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
+    }
+    if ( fVeryVerbose )
+    {
+        int fProfile = 0;
+        printf( "Processed output with %d supp vars. ", nVars );
+        if ( vRes == NULL )
+            printf( "The resulting SOP exceeded %d cubes.\n", nCubeLim );
+        else 
+            printf( "The best cover contains %d cubes.\n", Vec_StrSize(vRes)/(nVars +3) );
+        Abc_PrintTime( 1, "Onset  minterm", Time[0][0] );
+        Abc_PrintTime( 1, "Onset  expand ", Time[0][1] );
+        Abc_PrintTime( 1, "Offset minterm", Time[1][0] );
+        Abc_PrintTime( 1, "Offset expand ", Time[1][1] );
+        if ( fProfile )
+        {
+            Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0;
+            Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0;
+            Abc_PrintTime( 1, "Expand sat    ", clkCheckS ); clkCheckS = 0;
+            Abc_PrintTime( 1, "Expand unsat  ", clkCheckU ); clkCheckU = 0;
+        }
+    }
+    Vec_StrFreeP( &vSop[0] );
+    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*************************************************************
+
+  Synopsis    [This code computes on-set and off-set simultaneously.]
+
+  Description []
+               
+  SideEffects []
+
+  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 )
+{
+    int fVeryVerbose = fVerbose;
+    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 );
+    Vec_Int_t * vCube = Vec_IntAlloc( nVars+1 );
+    int n, v, iVar, pLits[2], iCube = 0, Start, status;
+    abctime clk = 0, Time[2][2] = {{0}};
+    int fComplete[2] = {0};
+    // variables
+    int iOutVar    = 2;
+    int iOOVars[2] = {0, 1};
+//    int iOutVar    = 1;
+//    int iOOVars[2] = {sat_solver_nvars(pSat) - 5, sat_solver_nvars(pSat) - 5 + 1};
+
+    // collect CI variables (0 = onset enable, 1 = offset enable, 2 = output)
+    int iCiVarBeg = 3;
+//    int iCiVarBeg = sat_solver_nvars(pSat) - 5 - nVars;
+    if ( fReverse )
+        for ( v = nVars - 1; v >= 0; v-- )
+            Vec_IntPush( vVars, iCiVarBeg + v );
+    else
+        for ( v = 0; v < nVars; v++ )
+            Vec_IntPush( vVars, iCiVarBeg + v );
+
+    // check that on-set/off-set is sat
+    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 );
+        if ( status == l_Undef )
+            goto cleanup; // timeout
+        if ( status == l_False )
+        {
+            Vec_StrClear( vSop[0] );
+            Vec_StrPrintStr( vSop[0], n ? " 1\n" : " 0\n" );
+            Vec_StrPush( vSop[0], '\0' );
+            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' );
+    }
+
+    // compute cube pairs
+    for ( iCube = 0; nCubeLim == 0 || iCube < nCubeLim; iCube++ )
+    {
+        for ( n = 0; n < 2; n++ )
+        {
+            if ( fVeryVerbose ) clk = Abc_Clock();
+            // get the assignment
+            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
+            if ( status == l_False )
+            {
+                fComplete[n] = 1;
+                break;
+            }
+            // collect values
+            Vec_IntClear( vLits );
+            Vec_IntForEachEntry( vVars, iVar, v )
+                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[!n], NULL, vLits, vNums, vCube, nBTLimit, fCanon, -1 );
+            if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk;
+            if ( status < 0 )
+                goto cleanup; // timeout
+            // collect cube
+            Vec_StrPop( vSop[n] );
+            Start = Vec_StrSize( vSop[n] );
+            Vec_StrFillExtra( vSop[n], Start + nVars + 4, '-' );
+            Vec_StrWriteEntry( vSop[n], Start + nVars + 0, ' ' );
+            Vec_StrWriteEntry( vSop[n], Start + nVars + 1, (char)(n ? '0' : '1') );
+            Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' );
+            Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' );
+            Vec_IntClear( vCube );
+            Vec_IntForEachEntry( vNums, iVar, v )
+            {
+                int iLit = Vec_IntEntry( vLits, iVar );
+                Vec_IntPush( vCube, Abc_LitNot(iLit) );
+                if ( fReverse )
+                    Vec_StrWriteEntry( vSop[n], Start + nVars - iVar - 1, (char)('0' + !Abc_LitIsCompl(iLit)) );
+                else 
+                    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) );
+            if ( status == 0 )
+            {
+                fComplete[n] = 1;
+                break;
+            }
+            assert( status == 1 );
+        }
+        if ( fComplete[0] || fComplete[1] )
+            break;
+    }
+cleanup:
+    Vec_IntFree( vVars );
+    Vec_IntFree( vLits );
+    Vec_IntFree( vNums );
+    Vec_IntFree( vCube );
+    assert( !fComplete[0] || !fComplete[1] );
+    if ( fComplete[0] || fComplete[1] ) // one of the cover is computed
+    {
+        vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL;
+        if ( iCube > 1 )
+//            Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
+            Bmc_CollapseIrredundantFull( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
+    }
+    if ( fVeryVerbose )
+    {
+        int fProfile = 0;
+        printf( "Processed output with %d supp vars. ", nVars );
+        if ( vRes == NULL )
+            printf( "The resulting SOP exceeded %d cubes.\n", nCubeLim );
+        else 
+            printf( "The best cover contains %d cubes.\n", Vec_StrSize(vRes)/(nVars +3) );
+        Abc_PrintTime( 1, "Onset  minterm", Time[0][0] );
+        Abc_PrintTime( 1, "Onset  expand ", Time[0][1] );
+        Abc_PrintTime( 1, "Offset minterm", Time[1][0] );
+        Abc_PrintTime( 1, "Offset expand ", Time[1][1] );
+        if ( fProfile )
+        {
+            Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0;
+            Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0;
+            Abc_PrintTime( 1, "Expand sat    ", clkCheckS ); clkCheckS = 0;
+            Abc_PrintTime( 1, "Expand unsat  ", clkCheckU ); clkCheckU = 0;
+        }
+    }
+    Vec_StrFreeP( &vSop[0] );
+    Vec_StrFreeP( &vSop[1] );
+    return vRes;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////