Adding CEC command &splitprove.

5 files changed, 362 insertions, 82 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index bdb07c4c..d7ddb317 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1015,6 +1015,7 @@ extern Gia_Man_t *         Gia_ManDupMarked( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTimes( Gia_Man_t * p, int nTimes );  
 extern Gia_Man_t *         Gia_ManDupDfs( Gia_Man_t * p );  
 extern Gia_Man_t *         Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value );  
+extern Gia_Man_t *         Gia_ManDupExist( Gia_Man_t * p, int iVar );
 extern Gia_Man_t *         Gia_ManDupDfsSkip( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern Gia_Man_t *         Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 0939c091..c7a0f3dc 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1239,6 +1239,100 @@ Gia_Man_t * Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value )
 
 /**Function*************************************************************
 
+  Synopsis    [Existentially quantified given variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupExist( Gia_Man_t * p, int iVar )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( iVar >= 0 && iVar < Gia_ManPiNum(p) );
+    assert( Gia_ManPoNum(p) == 1 );
+    assert( Gia_ManRegNum(p) == 0 );
+    Gia_ManFillValue( p );
+    // find the cofactoring variable
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManHashAlloc( pNew );
+    // compute negative cofactor
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 0 );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachPo( p, pObj, i )
+        pObj->Value = Gia_ObjFanin0Copy(pObj);
+    // compute the positive cofactor
+    Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 1 );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // create OR gate
+    Gia_ManForEachPo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) );
+    Gia_ManHashStop( pNew );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Existentially quantifies the given variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupExist2( Gia_Man_t * p, int iVar )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( iVar >= 0 && iVar < Gia_ManPiNum(p) );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManFillValue( p );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    // first part
+    Gia_ManPi( p, iVar )->Value = 0; // modification!
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ObjFanin0Copy(pObj);
+    // second part
+    Gia_ManPi( p, iVar )->Value = 1; // modification!
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = ~0;
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    // combination
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    pNew->nConstrs = p->nConstrs;
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates AIG in the DFS order while putting CIs first.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7058de3e..a2db62a1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32876,13 +32876,24 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Gia_Man_t * Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, int fVerbose );
-    int c, nTimeOut = 1, nIterMax = 0, LookAhead = 1, fVerbose = 0;
+    extern Gia_Man_t * Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose );
+    int c, nProcs = 1, nTimeOut = 1, nIterMax = 0, LookAhead = 1, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "TILvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PTILvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nProcs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nProcs <= 0 )
+                goto usage;
+            break;
         case 'T':
             if ( globalUtilOptind >= argc )
             {
@@ -32938,12 +32949,13 @@ int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9SplitProve(): The problem is sequential.\n" );
         return 1;
     }
-    Cec_GiaSplitTest( pAbc->pGia, nTimeOut, nIterMax, LookAhead, fVerbose );
+    Cec_GiaSplitTest( pAbc->pGia, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &splitprove [-TIL num] [-vh]\n" );
+    Abc_Print( -2, "usage: &splitprove [-PTIL num] [-vh]\n" );
     Abc_Print( -2, "\t         proves CEC problem by case-splitting\n" );
+    Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n",          nProcs );
     Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n",     nTimeOut );
     Abc_Print( -2, "\t-I num : the max number of iterations (0 = infinity) [default = %d]\n", nIterMax );
     Abc_Print( -2, "\t-L num : maximum look-ahead during cofactoring [default = %d]\n",       LookAhead );
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c
index e04d6224..3e2b70a6 100644
--- a/src/proof/cec/cecSplit.c
+++ b/src/proof/cec/cecSplit.c
@@ -21,10 +21,21 @@
 #include <math.h>
 #include "aig/gia/gia.h"
 #include "aig/gia/giaAig.h"
-//#include "bdd/cudd/cuddInt.h"
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satSolver.h"
 #include "misc/util/utilTruth.h"
+//#include "bdd/cudd/cuddInt.h"
+
+//#ifdef ABC_USE_PTHREADS
+
+#ifdef _WIN32
+#include "../lib/pthread.h"
+#else
+#include <pthread.h>
+#include <unistd.h>
+#endif
+
+//#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -222,12 +233,20 @@ int Gia_SplitCofVar2( Gia_Man_t * p, int LookAhead )
         Cost1 = Gia_ManAndNum(pPart);
         Gia_ManStop( pPart );
 
-        if ( CostBest > Cost0 + Cost1 )
-            CostBest = Cost0 + Cost1, iBest = pOrder[i];
+/*
+        pPart = Gia_ManDupExist( p, pOrder[i] );
+        printf( "%2d : Var = %4d  Refs = %3d  %6d %6d -> %6d    %6d -> %6d\n", 
+            i, pOrder[i], Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])), 
+            Cost0, Cost1, Cost0+Cost1, Gia_ManAndNum(p), Gia_ManAndNum(pPart) );
+        Gia_ManStop( pPart );
+*/
 
 //        printf( "%2d : Var = %4d  Refs = %3d  %6d %6d -> %6d\n", 
 //            i, pOrder[i], Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])), 
 //            Cost0, Cost1, Cost0+Cost1 );
+
+        if ( CostBest > Cost0 + Cost1 )
+            CostBest = Cost0 + Cost1, iBest = pOrder[i];
     }
     ABC_FREE( pOrder );
     assert( iBest >= 0 );
@@ -255,27 +274,40 @@ static inline Cnf_Dat_t * Cec_GiaDeriveGiaRemapped( Gia_Man_t * p )
     Aig_ManStop( pAig );
     return pCnf;
 }
-static inline sat_solver * Cec_GiaDeriveSolver( Gia_Man_t * p, int nTimeOut )
+static inline sat_solver * Cec_GiaDeriveSolver( Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut )
 {
     sat_solver * pSat;
-    Cnf_Dat_t * pCnf;
-    int i;
-    pCnf = Cec_GiaDeriveGiaRemapped( p );
+    int i, fDerive = (pCnf == NULL);
+    if ( pCnf == NULL )
+        pCnf = Cec_GiaDeriveGiaRemapped( p );
     pSat = sat_solver_new();
     sat_solver_setnvars( pSat, pCnf->nVars );
     for ( i = 0; i < pCnf->nClauses; i++ )
         if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
-            assert( 0 );
+        {
+            // the problem is UNSAT
+            sat_solver_delete( pSat );
+            Cnf_DataFree( pCnf );
+            return NULL;
+        }
     sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
-    Cnf_DataFree( pCnf );
+    if ( fDerive )
+        Cnf_DataFree( pCnf );
     return pSat;
 }
-static inline int Cnf_GiaSolveOne( Gia_Man_t * p, int nTimeOut, int fVerbose, int * pnVars, int * pnConfs )
+static inline int Cnf_GiaSolveOne( Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut, int * pnVars, int * pnConfs )
 {
-    sat_solver * pSat = Cec_GiaDeriveSolver( p, nTimeOut );
-    int status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-    *pnVars    = sat_solver_nvars( pSat );
-    *pnConfs   = sat_solver_nconflicts( pSat );
+    int status;
+    sat_solver * pSat = Cec_GiaDeriveSolver( p, pCnf, nTimeOut );
+    if ( pSat == NULL )
+    {
+        *pnVars = 0;
+        *pnConfs = 0;
+        return 1;
+    }
+    status   = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    *pnVars  = sat_solver_nvars( pSat );
+    *pnConfs = sat_solver_nconflicts( pSat );
     sat_solver_delete( pSat );
     if ( status == l_Undef )
         return -1;
@@ -299,9 +331,9 @@ static inline int Cnf_GiaSolveOne( Gia_Man_t * p, int nTimeOut, int fVerbose, in
     }
 */
 }
-static inline int Cnf_GiaCheckOne( Vec_Ptr_t * vStack, Gia_Man_t * p, int nTimeOut, int fVerbose, int * pnVars, int * pnConfs )
+static inline int Cnf_GiaCheckOne( Vec_Ptr_t * vStack, Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut, int * pnVars, int * pnConfs )
 {
-    int status = Cnf_GiaSolveOne( p, nTimeOut, fVerbose, pnVars, pnConfs );
+    int status = Cnf_GiaSolveOne( p, pCnf, nTimeOut, pnVars, pnConfs );
     if ( status == -1 )
     {
         Vec_PtrPush( vStack, p );
@@ -333,13 +365,13 @@ static inline void Cec_GiaSplitClean( Vec_Ptr_t * vStack )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fSatUnsat, double Prog, abctime clk )
+void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fStatus, double Prog, abctime clk )
 {
     printf( "%6d : ",            nIter );
     printf( "Depth =%3d  ",      Depth );
     printf( "SatVar =%7d  ",     nVars );
     printf( "SatConf =%7d   ",   nConfs );
-    printf( "%s   ",             fSatUnsat ? "UNSAT    " : "UNDECIDED" );
+    printf( "%s   ",             fStatus ? (fStatus == 1 ? "UNSAT    " : "UNDECIDED") : "SAT      " );
     printf( "Progress = %.10f   ", Prog );
     Abc_PrintTime( 1, "Time", clk );
     //ABC_PRTr( "Time", Abc_Clock()-clk );
@@ -366,9 +398,9 @@ void Cec_GiaSplitPrintRefs( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead, int fVerbose )
+int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose )
 {
-    abctime clk, clkTotal = Abc_Clock();
+    abctime clkTotal = Abc_Clock();
     Gia_Man_t * pPart0, * pPart1, * pLast;
     Vec_Ptr_t * vStack;
     int nSatVars, nSatConfs, fSatUnsat;
@@ -381,13 +413,12 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead,
     p->vCofVars = Vec_IntAlloc( 100 );
     // start with the current problem
     vStack = Vec_PtrAlloc( 1000 );
-    clk = Abc_Clock();
-    if ( !Cnf_GiaCheckOne(vStack, p, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
+    if ( !Cnf_GiaCheckOne(vStack, p, NULL, nTimeOut, &nSatVars, &nSatConfs) )
         RetValue = 0;
     else
     {
         if ( fVerbose )
-            Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, 0, 0, Abc_Clock() - clk );
+            Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, -1, Progress, Abc_Clock() - clkTotal );
         for ( nIter = 1; Vec_PtrSize(vStack) > 0; nIter++ )
         {
             // get the last AIG
@@ -403,8 +434,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead,
             Vec_IntPush( pPart0->vCofVars, Abc_Var2Lit(iVar, 1) );
             // check this AIG
             fSatUnsat = Vec_PtrSize(vStack);
-            clk = Abc_Clock();
-            if ( !Cnf_GiaCheckOne(vStack, pPart0, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
+            if ( !Cnf_GiaCheckOne(vStack, pPart0, NULL, nTimeOut, &nSatVars, &nSatConfs) )
             {
                 Gia_ManStop( pLast );
                 RetValue = 0;
@@ -414,7 +444,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead,
             if ( fSatUnsat )
                 Progress += 1.0 / pow(2, Depth + 1);
             if ( fVerbose ) 
-                Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk );
+                Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat?1:-1, Progress, Abc_Clock() - clkTotal );
             // cofactor
             pPart1 = Gia_ManDupCofactor( pLast, iVar, 1 );
             // create variable
@@ -424,8 +454,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead,
             Gia_ManStop( pLast );
             // check this AIG
             fSatUnsat = Vec_PtrSize(vStack);
-            clk = Abc_Clock();
-            if ( !Cnf_GiaCheckOne(vStack, pPart1, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
+            if ( !Cnf_GiaCheckOne(vStack, pPart1, NULL, nTimeOut, &nSatVars, &nSatConfs) )
             {
                 RetValue = 0;
                 break;
@@ -434,7 +463,7 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead,
             if ( fSatUnsat )
                 Progress += 1.0 / pow(2, Depth + 1);
             if ( fVerbose )
-                Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk );
+                Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat?1:-1, Progress, Abc_Clock() - clkTotal );
             if ( nIterMax && Vec_PtrSize(vStack) >= nIterMax )
                 break;
         }
@@ -454,6 +483,198 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int nIterMax, int LookAhead,
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+#define PAR_THR_MAX 100
+typedef struct Par_ThData_t_
+{
+    Gia_Man_t * p;
+    Cnf_Dat_t * pCnf;
+    int         nTimeOut;
+    int         fWorking;
+    int         Result;
+    int         nVars;
+    int         nConfs;
+} Par_ThData_t;
+void * Cec_GiaSplitWorkerThread( void * pArg )
+{
+    Par_ThData_t * pThData = (Par_ThData_t *)pArg;
+    volatile int * pPlace = &pThData->fWorking;
+    while ( 1 )
+    {
+        while ( *pPlace == 0 );
+        assert( pThData->fWorking );
+        if ( pThData->p == NULL )
+        {
+            pthread_exit( NULL );
+            assert( 0 );
+            return NULL;
+        }
+        pThData->Result = Cnf_GiaSolveOne( pThData->p, pThData->pCnf, pThData->nTimeOut, &pThData->nVars, &pThData->nConfs );
+        pThData->fWorking = 0;
+    }
+    assert( 0 );
+    return NULL;
+}
+int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose )
+{
+    abctime clkTotal = Abc_Clock();
+    Par_ThData_t ThData[PAR_THR_MAX];
+    pthread_t WorkerThread[PAR_THR_MAX];
+    Vec_Ptr_t * vStack;
+    double Progress = 0;
+    int i, status, nSatVars, nSatConfs;
+    int nIter = 0, RetValue = -1, fWorkToDo = 1;
+    if ( fVerbose )
+        printf( "Solving CEC problem by cofactoring with the following parameters:\n" );
+    if ( fVerbose )
+        printf( "Processes = %d   TimeOut = %d sec   MaxIter = %d   LookAhead = %d   Verbose = %d.\n", nProcs, nTimeOut, nIterMax, LookAhead, fVerbose );
+    if ( nProcs == 1 )
+        return Cec_GiaSplitTest2( p, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose );
+    // subtract manager thread
+    nProcs--;
+    assert( nProcs >= 1 && nProcs <= PAR_THR_MAX );
+    // check the problem
+    status = Cnf_GiaSolveOne( p, NULL, nTimeOut, &nSatVars, &nSatConfs );
+    if ( fVerbose )
+        Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
+    if ( status == 0 )
+    {
+        printf( "The problem is SAT.\n" );
+        return 0;
+    }
+    if ( status == 1 )
+    {
+        printf( "The problem is UNSAT.\n" );
+        return 1;
+    }
+    assert( status == -1 );
+    // create local copy
+    p = Gia_ManDup( p );
+    vStack = Vec_PtrAlloc( 1000 );
+    Vec_PtrPush( vStack, p );
+    // start cofactored variables
+    assert( p->vCofVars == NULL );
+    p->vCofVars = Vec_IntAlloc( 100 );
+    // start threads
+    for ( i = 0; i < nProcs; i++ )
+    {
+        ThData[i].p        = NULL;
+        ThData[i].pCnf     = NULL;
+        ThData[i].nTimeOut = nTimeOut;
+        ThData[i].fWorking = 0;
+        ThData[i].Result   = -1;
+        ThData[i].nVars    = -1;
+        ThData[i].nConfs   = -1;
+        status = pthread_create( WorkerThread + i, NULL,Cec_GiaSplitWorkerThread, (void *)(ThData + i) );  assert( status == 0 );
+    }
+    // look at the threads
+    while ( fWorkToDo )
+    {
+        fWorkToDo = (int)(Vec_PtrSize(vStack) > 0);
+        for ( i = 0; i < nProcs; i++ )
+        {
+            // check if this thread is working
+            if ( ThData[i].fWorking )
+            {
+                fWorkToDo = 1;
+                continue;
+            }
+            // check if this thread has recently finished
+            if ( ThData[i].p != NULL )
+            {
+                Gia_Man_t * pLast = ThData[i].p;
+                int Depth = Vec_IntSize(pLast->vCofVars);
+                if ( fVerbose )
+                    Cec_GiaSplitPrint( nIter, Depth, ThData[i].nVars, ThData[i].nConfs, ThData[i].Result, Progress, Abc_Clock() - clkTotal );
+                if ( ThData[i].Result == 0 ) // SAT
+                {
+                    RetValue = 0;
+                    goto finish;
+                }
+                if ( ThData[i].Result == -1 ) // UNDEC
+                {
+                    // determine cofactoring variable
+                    int iVar = Gia_SplitCofVar2( pLast, LookAhead );
+                    // cofactor
+                    Gia_Man_t * pPart = Gia_ManDupCofactor( pLast, iVar, 0 );
+                    pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
+                    Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
+                    Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
+                    Vec_PtrPush( vStack, pPart );
+                    // cofactor
+                    pPart = Gia_ManDupCofactor( pLast, iVar, 1 );
+                    pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
+                    Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
+                    Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
+                    Vec_PtrPush( vStack, pPart );
+                    // keep working
+                    fWorkToDo = 1;
+                    nIter++;
+                }
+                else
+                    Progress += 1.0 / pow(2, Depth);
+                Gia_ManStopP( &ThData[i].p );
+                if ( ThData[i].pCnf == NULL )
+                    continue;
+                Cnf_DataFree( ThData[i].pCnf );
+                ThData[i].pCnf = NULL;
+            }
+            if ( Vec_PtrSize(vStack) == 0 )
+                continue;
+            // start a new thread
+            assert( ThData[i].p == NULL );
+            ThData[i].p = Vec_PtrPop( vStack );
+            ThData[i].pCnf = Cec_GiaDeriveGiaRemapped( ThData[i].p );
+            ThData[i].fWorking = 1;
+        }
+        if ( nIterMax && nIter >= nIterMax )
+            break;
+    }
+    if ( !fWorkToDo )
+        RetValue = 1;
+finish:
+    // wait till threads finish
+    for ( i = 0; i < nProcs; i++ )
+        if ( ThData[i].fWorking )
+            i = 0;
+    // stop threads
+    for ( i = 0; i < nProcs; i++ )
+    {
+        assert( !ThData[i].fWorking );
+        // cleanup
+        Gia_ManStopP( &ThData[i].p );
+        if ( ThData[i].pCnf == NULL )
+            continue;
+        Cnf_DataFree( ThData[i].pCnf );
+        ThData[i].pCnf = NULL;
+        // stop
+        ThData[i].p = NULL;
+        ThData[i].fWorking = 1;
+    }
+    // finish
+    Cec_GiaSplitClean( vStack );
+    if ( RetValue == 0 )
+        printf( "Problem is SAT " );
+    else if ( RetValue == 1 )
+        printf( "Problem is UNSAT " );
+    else if ( RetValue == -1 )
+        printf( "Problem is UNDECIDED " );
+    else assert( 0 );
+    printf( "after %d case-splits.  ", nIter );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+    return RetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bmc/bmcCexDepth.c b/src/sat/bmc/bmcCexDepth.c
index 3a6584b1..38b57d5f 100644
--- a/src/sat/bmc/bmcCexDepth.c
+++ b/src/sat/bmc/bmcCexDepth.c
@@ -35,54 +35,6 @@ extern int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-
-/**Function*************************************************************
-
-  Synopsis    [Existentially quantified given variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Man_t * Gia_ManDupExist( Gia_Man_t * p, int iVar )
-{
-    Gia_Man_t * pNew, * pTemp;
-    Gia_Obj_t * pObj;
-    int i;
-    assert( iVar >= 0 && iVar < Gia_ManPiNum(p) );
-    assert( Gia_ManPoNum(p) == 1 );
-    assert( Gia_ManRegNum(p) == 0 );
-    Gia_ManFillValue( p );
-    // find the cofactoring variable
-    pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Abc_UtilStrsav( p->pName );
-    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
-    Gia_ManHashAlloc( pNew );
-    // compute negative cofactor
-    Gia_ManConst0(p)->Value = 0;
-    Gia_ManForEachCi( p, pObj, i )
-        pObj->Value = Gia_ManAppendCi(pNew);
-    Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 1 );
-    Gia_ManForEachAnd( p, pObj, i )
-        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-    Gia_ManForEachPo( p, pObj, i )
-        pObj->Value = Gia_ObjFanin0Copy(pObj);
-    // compute the positive cofactor
-    Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 0 );
-    Gia_ManForEachAnd( p, pObj, i )
-        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-    // create OR gate
-    Gia_ManForEachPo( p, pObj, i )
-        pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, pObj->Value, Gia_ObjFanin0Copy(pObj)) );
-    Gia_ManHashStop( pNew );
-    pNew = Gia_ManCleanup( pTemp = pNew );
-    Gia_ManStop( pTemp );
-    return pNew;
-}
-
 /**Function*************************************************************
 
   Synopsis    [Performs targe enlargement of the given size.]