Additional improvements in 'satclp'.

4 files changed, 326 insertions, 22 deletions

diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 19d6ef79..a2f5e138 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -2073,6 +2073,41 @@ void Abc_NtkPermute( Abc_Ntk_t * pNtk, int fInputs, int fOutputs, int fFlops, ch
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_NodeCompareByFanoutCount( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
+{
+    int Diff = Abc_ObjFanoutNum(*pp2) - Abc_ObjFanoutNum(*pp1);
+    if ( Diff < 0 )
+        return -1;
+    if ( Diff > 0 ) 
+        return 1;
+    Diff = strcmp( Abc_ObjName(*pp1), Abc_ObjName(*pp2) );
+    if ( Diff < 0 )
+        return -1;
+    if ( Diff > 0 ) 
+        return 1;
+    return 0; 
+}
+void Abc_NtkPermutePiUsingFanout( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode; int i;
+    qsort( (void *)Vec_PtrArray(pNtk->vPis), Vec_PtrSize(pNtk->vPis), sizeof(Abc_Obj_t *), 
+        (int (*)(const void *, const void *)) Abc_NodeCompareByFanoutCount );
+    Vec_PtrClear( pNtk->vCis );
+    Vec_PtrForEachEntry( Abc_Obj_t *, pNtk->vPis, pNode, i )
+        Vec_PtrPush( pNtk->vCis, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_NtkUnpermute( Abc_Ntk_t * pNtk )
 {
     Vec_Ptr_t * vTemp, * vTemp2, * vLatch;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d6a9b1cc..49924f14 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -20558,15 +20558,17 @@ usage:
 int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Abc_Ntk_t * Abc_NtkRestrashRandom( Abc_Ntk_t * pNtk );
+    extern void Abc_NtkPermutePiUsingFanout( Abc_Ntk_t * pNtk );
     Abc_Ntk_t * pNtk = pAbc->pNtkCur, * pNtkRes = NULL;
     char * pFlopPermFile = NULL;
     int fInputs = 1;
     int fOutputs = 1;
     int fFlops = 1;
     int fNodes = 1;
+    int fFanout = 0;
     int c;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Fiofnh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fiofnxh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -20591,6 +20593,9 @@ int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'n':
             fNodes ^= 1;
             break;
+        case 'x':
+            fFanout ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -20603,6 +20608,16 @@ int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty network.\n" );
         return 1;
     }
+    if ( fFanout )
+    {
+        if ( Abc_NtkLatchNum(pNtk) )
+        {
+            Abc_Print( -1, "Currently \"permute -x\" works only for combinational networks.\n" );
+            return 1;
+        }
+        Abc_NtkPermutePiUsingFanout( pNtk );
+        return 0;
+    }
     if ( fNodes && !Abc_NtkIsStrash(pNtk) )
     {
         Abc_Print( -1, "To permute nodes, the network should be structurally hashed.\n" );
@@ -20622,12 +20637,13 @@ int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: permute [-iofnh] [-F filename]\n" );
+    Abc_Print( -2, "usage: permute [-iofnxh] [-F filename]\n" );
     Abc_Print( -2, "\t                performs random permutation of inputs/outputs/flops\n" );
     Abc_Print( -2, "\t-i            : toggle permuting primary inputs [default = %s]\n", fInputs? "yes": "no" );
     Abc_Print( -2, "\t-o            : toggle permuting primary outputs [default = %s]\n", fOutputs? "yes": "no" );
     Abc_Print( -2, "\t-f            : toggle permuting flip-flops [default = %s]\n", fFlops? "yes": "no" );
     Abc_Print( -2, "\t-n            : toggle deriving new topological ordering of nodes [default = %s]\n", fNodes? "yes": "no" );
+    Abc_Print( -2, "\t-x            : toggle permuting inputs based on their fanout count [default = %s]\n", fFanout? "yes": "no" );
     Abc_Print( -2, "\t-h            : print the command usage\n");
     Abc_Print( -2, "\t-F <filename> : (optional) file with the flop permutation\n" );
     return 1;
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index b78a1206..cc610998 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -20,6 +20,7 @@
 
 #include "base/abc/abc.h"
 #include "aig/gia/gia.h"
+#include "misc/vec/vecWec.h"
 
 #ifdef ABC_USE_CUDD
 #include "bdd/extrab/extraBdd.h"
@@ -290,27 +291,98 @@ Gia_Man_t * Abc_NtkClpOneGia( Abc_Ntk_t * pNtk, int iCo, Vec_Int_t * vSupp )
     Gia_ManStop( pTemp );
     return pNew;
 }
-Vec_Str_t * Abc_NtkClpOne( Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t ** pvSupp )
+Vec_Str_t * Abc_NtkClpOne( Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, int fReverse, Vec_Int_t * vSupp )
 {
-    extern Vec_Int_t * Abc_NtkNodeSupportInt( Abc_Ntk_t * pNtk, int iCo );
+    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 );
-    Vec_Int_t * vSupp = Abc_NtkNodeSupportInt( pNtk, iCo );
     Gia_Man_t * pGia  = Abc_NtkClpOneGia( pNtk, iCo, vSupp );
-    Vec_Str_t * vSop;
     if ( fVerbose )
-        printf( "Output %d:\n", iCo );
+        printf( "Output %d:  \n", iCo );
     vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
     Gia_ManStop( pGia );
-    *pvSupp = vSupp;
     if ( vSop == NULL )
-        Vec_IntFree(vSupp);
-    else if ( Vec_StrSize(vSop) == 4 ) // constant
+        return NULL;
+    if ( Vec_StrSize(vSop) == 4 ) // constant
         Vec_IntClear(vSupp);
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     return vSop; 
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Collect structural support for all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Abc_NtkCreateCoSupps( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Abc_Obj_t * pNode; int i;
+    Vec_Wec_t * vSupps = Vec_WecStart( Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        Vec_IntPush( Vec_WecEntry(vSupps, pNode->Id), i );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Abc_ObjFanin0(pNode)->Id), 
+                          Vec_WecEntry(vSupps, Abc_ObjFanin1(pNode)->Id), 
+                          Vec_WecEntry(vSupps, pNode->Id) ); 
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk );
+    return vSupps;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive array of COs sorted by cone size in the reverse order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeCompareByTemp( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
+{
+    int Diff = (*pp2)->iTemp - (*pp1)->iTemp;
+    if ( Diff < 0 )
+        return -1;
+    if ( Diff > 0 ) 
+        return 1;
+    Diff = strcmp( Abc_ObjName(*pp1), Abc_ObjName(*pp2) );
+    if ( Diff < 0 )
+        return -1;
+    if ( Diff > 0 ) 
+        return 1;
+    return 0; 
+}
+Vec_Ptr_t * Abc_NtkCreateCoOrder( Abc_Ntk_t * pNtk, Vec_Wec_t * vSupps )
+{
+    Abc_Obj_t * pNode; int i;
+    Vec_Ptr_t * vNodes = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pNode->iTemp = Vec_IntSize( Vec_WecEntry(vSupps, Abc_ObjFanin0(pNode)->Id) );
+        Vec_PtrPush( vNodes, pNode );
+    }
+    // order objects alphabetically
+    qsort( (void *)Vec_PtrArray(vNodes), Vec_PtrSize(vNodes), sizeof(Abc_Obj_t *), 
+        (int (*)(const void *, const void *)) Abc_NodeCompareByTemp );
+    // cleanup
+//    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
+//        printf( "%s %d ", Abc_ObjName(pNode), pNode->iTemp );
+//    printf( "\n" );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [SAT-based collapsing.]
 
   Description []
@@ -320,14 +392,13 @@ Vec_Str_t * Abc_NtkClpOne( Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
+Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo, Vec_Int_t * vSupp, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
 {
     Abc_Obj_t * pNodeNew;
-    Vec_Int_t * vSupp;
     Vec_Str_t * vSop;
     int i, iCi;
     // compute SOP of the node
-    vSop = Abc_NtkClpOne( pNtk, iCo, nCubeLim, nBTLimit, fVerbose, fCanon, fReverse, &vSupp );
+    vSop = Abc_NtkClpOne( pNtk, iCo, nCubeLim, nBTLimit, fVerbose, fCanon, fReverse, vSupp );
     if ( vSop == NULL )
         return NULL;
     // create a new node
@@ -335,7 +406,6 @@ Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo,
     // add fanins
     Vec_IntForEachEntry( vSupp, iCi, i )
         Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) );
-    Vec_IntFree( vSupp );
     // transfer the function
     pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vSop) );
     Vec_StrFree( vSop );
@@ -346,17 +416,37 @@ Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int f
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode, * pDriver, * pNodeNew;
-    Vec_Ptr_t * vDriverCopy;
+    Vec_Ptr_t * vDriverCopy, * vCoNodes;
+    Vec_Int_t * vNodeCoIds;
+    Vec_Wec_t * vSupps;
     int i;
+
+//    Abc_NtkForEachCi( pNtk, pNode, i )
+//        printf( "%d ", Abc_ObjFanoutNum(pNode) );
+//    printf( "\n" );
+
+    // compute structural supports
+    vSupps = Abc_NtkCreateCoSupps( pNtk, fVerbose );
+    // order CO nodes by support size
+    vCoNodes = Abc_NtkCreateCoOrder( pNtk, vSupps );
+    // collect CO IDs in this order
+    vNodeCoIds = Vec_IntAlloc( Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        pNode->iTemp = i;
+    Vec_PtrForEachEntry( Abc_Obj_t *, vCoNodes, pNode, i )
+        Vec_IntPush( vNodeCoIds, pNode->iTemp );
+
     // start the new network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
     // collect driver copies
     vDriverCopy = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
-    Abc_NtkForEachCo( pNtk, pNode, i )
+//    Abc_NtkForEachCo( pNtk, pNode, i )
+    Vec_PtrForEachEntry( Abc_Obj_t *, vCoNodes, pNode, i )
         Vec_PtrPush( vDriverCopy, Abc_ObjFanin0(pNode)->pCopy );
     // process the POs
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
-    Abc_NtkForEachCo( pNtk, pNode, i )
+//    Abc_NtkForEachCo( pNtk, pNode, i )
+    Vec_PtrForEachEntry( Abc_Obj_t *, vCoNodes, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         pDriver = Abc_ObjFanin0(pNode);
@@ -365,15 +455,14 @@ Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int f
             Abc_ObjAddFanin( pNode->pCopy, (Abc_Obj_t *)Vec_PtrEntry(vDriverCopy, i) );
             continue;
         }
-/*
         if ( Abc_ObjIsCi(pDriver) )
         {
             pNodeNew = Abc_NtkCreateNode( pNtkNew );
-            Abc_ObjAddFanin( pNodeNew, pDriver->pCopy ); // pDriver->pCopy is removed by GIA construction...
+            Abc_ObjAddFanin( pNodeNew, (Abc_Obj_t *)Vec_PtrEntry(vDriverCopy, i) ); 
             pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? "0 1\n" : "1 1\n" );
+            Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
             continue;
         }
-*/
         if ( pDriver == Abc_AigConst1(pNtk) )
         {
             pNodeNew = Abc_NtkCreateNode( pNtkNew );
@@ -381,7 +470,7 @@ Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int f
             Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
             continue;
         }
-        pNodeNew = Abc_NtkFromSopsOne( pNtkNew, pNtk, i, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
+        pNodeNew = Abc_NtkFromSopsOne( pNtkNew, pNtk, Vec_IntEntry(vNodeCoIds, i), Vec_WecEntry(vSupps, Abc_ObjFanin0(pNode)->Id), nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
         if ( pNodeNew == NULL )
         {
             Abc_NtkDelete( pNtkNew );
@@ -391,6 +480,9 @@ Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int f
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     }
     Vec_PtrFree( vDriverCopy );
+    Vec_PtrFree( vCoNodes );
+    Vec_IntFree( vNodeCoIds );
+    Vec_WecFree( vSupps );
     Extra_ProgressBarStop( pProgress );
     return pNtkNew;
 }
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c
index 10892530..d5610840 100644
--- a/src/sat/bmc/bmcClp.c
+++ b/src/sat/bmc/bmcClp.c
@@ -425,7 +425,7 @@ cleanup:
         Bmc_CollapseIrredundant( vSop, Vec_StrSize(vSop)/(nVars +3), nVars );
     return vSop;
 }
-Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
+Vec_Str_t * Bmc_CollapseOne2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
 {
     Vec_Str_t * vSopOn, * vSopOff;
     int nCubesOn = ABC_INFINITY;
@@ -454,6 +454,167 @@ Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCan
     }
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [This code computes on-set and off-set simultaneously.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, 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) };
+    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 );
+    Vec_Int_t * vLits = Vec_IntAlloc( nVars );
+    Vec_Int_t * vNums = Vec_IntAlloc( nVars );
+    Vec_Int_t * vCube = Vec_IntAlloc( nVars );
+    int n, v, iVar, iLit, iCiVarBeg, iCube, Start, status;
+    abctime clk, Time[2][2] = {{0}};
+    int fComplete[2] = {0};
+
+    // collect CI variables
+    iCiVarBeg = pCnf->nVars - nVars;// - 1;
+    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++ )
+    {
+        iLit = Abc_Var2Lit( 1, n ); // n=0 => F=1   n=1 => F=0
+        status = sat_solver_solve( pSat[n], &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef )
+            goto cleanup; // timeout
+        if ( status == l_False )
+        {
+            Vec_StrPrintStr( vSop[0], n ? " 1\n\0" : " 0\n\0" );
+            fComplete[0] = 1;
+            goto cleanup; // const0/1
+        }
+        // start with all negative literals
+        Vec_IntForEachEntry( vVars, iVar, v )
+            Vec_IntPush( vLitsC[n], Abc_Var2Lit(iVar, 1) );
+        // add literals to the solver
+        status = sat_solver_addclause( pSat[n], &iLit, &iLit + 1 );
+        assert( status );
+        status = sat_solver_addclause( pSatClean[n], &iLit, &iLit + 1 );
+        assert( status );
+        // start cover
+        Vec_StrPush( vSop[n], '\0' );
+    }
+
+    // compute cube pairs
+    for ( iCube = 0; iCube < nCubeLim; iCube++ )
+    {
+        for ( n = 0; n < 2; n++ )
+        {
+            if ( fVeryVerbose ) clk = Abc_Clock();
+            // get the assignment
+            if ( fCanon )
+                status = Bmc_ComputeCanonical( pSat[n], vLitsC[n], vCube, nBTLimit );
+            else
+            {
+                sat_solver_clean_polarity( pSat[n], Vec_IntArray(vVars), Vec_IntSize(vVars) );
+                status = sat_solver_solve( pSat[n], NULL, NULL, 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_IntClear( vLitsC[n] );
+            Vec_IntForEachEntry( vVars, iVar, v )
+            {
+                iLit = Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[n], iVar));
+                Vec_IntPush( vLits, iLit );
+                Vec_IntPush( vLitsC[n], iLit );
+            }
+            // expand the values
+            if ( fVeryVerbose ) clk = Abc_Clock();
+            status = Bmc_CollapseExpand( pSatClean[!n], pSat[n], vLits, vNums, vCube, nBTLimit, fCanon );
+            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 )
+            {
+                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
+            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( vLitsC[0] );
+    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
+    {
+        vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL;
+        Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
+        if ( fVeryVerbose )
+        {
+            printf( "Processed output with %d supp vars and %d cubes.\n", nVars, 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] );
+        }
+    }
+    Vec_StrFreeP( &vSop[0] );
+    Vec_StrFreeP( &vSop[1] );
+    return vRes;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////