path: root/src/proof/cec/cecSplit.c

/**CFile****************************************************************

  FileName    [cecSplit.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Combinational equivalence checking.]

  Synopsis    [Cofactoring for combinational miters.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: cecSplit.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include <math.h>
#include "aig/gia/gia.h"
#include "aig/gia/giaAig.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


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

#ifndef ABC_USE_PTHREADS

int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; }

#else // pthreads are used

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

#if 0 // BDD code

/**Function*************************************************************

  Synopsis    [Permute primary inputs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdManager * Gia_ManBuildBdd( Gia_Man_t * p, Vec_Ptr_t ** pvNodes, int nSkip )
{
    abctime clk = Abc_Clock();
    DdManager * dd;
    DdNode * bBdd, * bBdd0, * bBdd1;
    Vec_Ptr_t * vNodes;
    Gia_Obj_t * pObj;
    int i;
    vNodes = Vec_PtrStart( Gia_ManObjNum(p) );
    dd = Cudd_Init( Gia_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
//    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
    bBdd = Cudd_ReadLogicZero(dd); Cudd_Ref( bBdd );
    Vec_PtrWriteEntry( vNodes, 0, bBdd );  
    Gia_ManForEachPi( p, pObj, i )
    {
        bBdd = i > nSkip ? Cudd_bddIthVar(dd, i) : Cudd_ReadLogicZero(dd); Cudd_Ref( bBdd );
        Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd );
    }
    Gia_ManForEachAnd( p, pObj, i )
    {
        bBdd0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj) );
        bBdd1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj) );
        bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( bBdd );
        Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd );
        if ( i % 10 == 0 )
            printf( "%d ", i );
//        if ( i == 3000 )
//            break;
    }
    printf( "\n" );
    Gia_ManForEachPo( p, pObj, i )
    {
        bBdd = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId0(pObj, Gia_ObjId(p, pObj))), Gia_ObjFaninC0(pObj) );  Cudd_Ref( bBdd );
        Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd );
    }
    if ( bBdd == Cudd_ReadLogicZero(dd) )
        printf( "Equivalent!\n" );
    else
        printf( "Not tquivalent!\n" );
    if ( pvNodes )
        *pvNodes = vNodes;
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    return dd;
}
void Gia_ManDerefBdd( DdManager * dd, Vec_Ptr_t * vNodes )
{
    DdNode * bBdd;
    int i;
    Vec_PtrForEachEntry( DdNode *, vNodes, bBdd, i )
        if ( bBdd )
            Cudd_RecursiveDeref( dd, bBdd );
    if ( Cudd_CheckZeroRef(dd) > 0 )
        printf( "The number of referenced nodes = %d\n", Cudd_CheckZeroRef(dd) );
    Cudd_PrintInfo( dd, stdout );
    Cudd_Quit( dd );
}
void Gia_ManBuildBddTest( Gia_Man_t * p )
{
    Vec_Ptr_t * vNodes;
    DdManager * dd = Gia_ManBuildBdd( p, &vNodes, 50 );
    Gia_ManDerefBdd( dd, vNodes );
}

#endif // BDD code

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_GiaSplitExplore( Gia_Man_t * p )
{
    Gia_Obj_t * pObj, * pFan0, * pFan1;
    int i, Counter = 0;
    assert( p->pMuxes == NULL );
    ABC_FREE( p->pRefs );
    Gia_ManCreateRefs( p ); 
    Gia_ManForEachAnd( p, pObj, i )
    {
        if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
            continue;
        if ( Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) > 1 && 
             Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) > 1 )
             continue;
        printf( "%5d : ", Counter++ );
        printf( "%2d %2d    ", Gia_ObjRefNum(p, Gia_Regular(pFan0)),  Gia_ObjRefNum(p, Gia_Regular(pFan1)) );
        printf( "%2d %2d  \n", Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)), Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) );
    }
}

/**Function*************************************************************

  Synopsis    [Find cofactoring variable.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int * Gia_PermuteSpecialOrder( Gia_Man_t * p )
{
    Vec_Int_t * vPerm;
    Gia_Obj_t * pObj;
    int i, * pOrder;
    Gia_ManCreateRefs( p );
    vPerm = Vec_IntAlloc( Gia_ManPiNum(p) );
    Gia_ManForEachPi( p, pObj, i )
        Vec_IntPush( vPerm, Gia_ObjRefNum(p, pObj) );
    pOrder = Abc_QuickSortCost( Vec_IntArray(vPerm), Vec_IntSize(vPerm), 1 );
    Vec_IntFree( vPerm );
    return pOrder;
}
Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
{
    Gia_Man_t * pNew;
    Vec_Int_t * vPerm;
    int * pOrder = Gia_PermuteSpecialOrder( p );
    vPerm = Vec_IntAllocArray( pOrder, Gia_ManPiNum(p) );
    pNew = Gia_ManDupPerm( p, vPerm );
    Vec_IntFree( vPerm );
    return pNew;
}

/**Function*************************************************************

  Synopsis    [Find cofactoring variable.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_SplitCofVar2( Gia_Man_t * p, int * pnFanouts, int * pnCost )
{
    Gia_Obj_t * pObj;
    int i, iBest = -1, CostBest = -1;
    if ( p->pRefs == NULL )
        Gia_ManCreateRefs( p );
    Gia_ManForEachPi( p, pObj, i )
        if ( CostBest < Gia_ObjRefNum(p, pObj) )
            iBest = i, CostBest = Gia_ObjRefNum(p, pObj);
    assert( iBest >= 0 );
    *pnFanouts = Gia_ObjRefNum(p, Gia_ManPi(p, iBest));
    *pnCost = -1;
    return iBest;
}
int Gia_SplitCofVar( Gia_Man_t * p, int LookAhead, int * pnFanouts, int * pnCost )
{
    Gia_Man_t * pPart;
    int Cost0, Cost1, CostBest = ABC_INFINITY;
    int * pOrder, i, iBest = -1;
    if ( LookAhead == 1 )
        return Gia_SplitCofVar2( p, pnFanouts, pnCost );
    pOrder = Gia_PermuteSpecialOrder( p );
    LookAhead = Abc_MinInt( LookAhead, Gia_ManPiNum(p) );
    for ( i = 0; i < LookAhead; i++ )
    {
        pPart = Gia_ManDupCofactorVar( p, pOrder[i], 0 );
        Cost0 = Gia_ManAndNum(pPart);
        Gia_ManStop( pPart );

        pPart = Gia_ManDupCofactorVar( p, pOrder[i], 1 );
        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 );
*/
    }
    ABC_FREE( pOrder );
    assert( iBest >= 0 );
    *pnFanouts = Gia_ObjRefNum(p, Gia_ManPi(p, iBest));
    *pnCost = CostBest;
    return iBest;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Cex_t * Cec_SplitDeriveModel( Gia_Man_t * p, Cnf_Dat_t * pCnf, sat_solver * pSat )
{
    Abc_Cex_t * pCex;
    Gia_Obj_t * pObj;
    int i, iLit, * pModel;
    pModel = ABC_CALLOC( int, Gia_ManPiNum(p) );
    Gia_ManForEachPi( p, pObj, i )
        pModel[i] = sat_solver_var_value(pSat, pCnf->pVarNums[Gia_ObjId(p, pObj)]);
    if ( p->vCofVars )
        Vec_IntForEachEntry( p->vCofVars, iLit, i )
            pModel[Abc_Lit2Var(iLit)] = !Abc_LitIsCompl(iLit);
    pCex = Abc_CexCreate( 0, Gia_ManPiNum(p), pModel, 0, 0, 0 );
    ABC_FREE( pModel );
    return pCex;
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline Cnf_Dat_t * Cec_GiaDeriveGiaRemapped( Gia_Man_t * p )
{
    Cnf_Dat_t * pCnf;
    Aig_Man_t * pAig = Gia_ManToAigSimple( p );
    pAig->nRegs = 0;
    pCnf = Cnf_Derive( pAig, 0 );//Aig_ManCoNum(pAig) );
    Aig_ManStop( pAig );
    return pCnf;
}
static inline sat_solver * Cec_GiaDeriveSolver( Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut )
{
    sat_solver * pSat;
    int i;
    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] ) )
        {
            // the problem is UNSAT
            sat_solver_delete( pSat );
            return NULL;
        }
    sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
    return pSat;
}
static inline int Cnf_GiaSolveOne( Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut, int * pnVars, int * pnConfs )
{
    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 );
    if ( status == l_True )
        p->pCexComb = Cec_SplitDeriveModel( p, pCnf, pSat );
    sat_solver_delete( pSat );
    if ( status == l_Undef )
        return -1;
    if ( status == l_False )
        return 1;
    return 0;
}
static inline void Cec_GiaSplitClean( Vec_Ptr_t * vStack )
{
    Gia_Man_t * pNew;
    int i;
    Vec_PtrForEachEntry( Gia_Man_t *, vStack, pNew, i )
        Gia_ManStop( pNew );
    Vec_PtrFree( vStack );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fStatus, double Prog, abctime clk )
{
    printf( "%4d : ",             nIter );
    printf( "Depth =%3d  ",       Depth );
    printf( "SatVar =%7d  ",      nVars );
    printf( "SatConf =%7d   ",    nConfs );
    printf( "%s   ",              fStatus ? (fStatus == 1 ? "UNSAT    " : "UNDECIDED") : "SAT      " );
    printf( "Solved %8.4f %%   ", 100*Prog );
    Abc_PrintTime( 1, "Time", clk );
    //ABC_PRTr( "Time", Abc_Clock()-clk );
    fflush( stdout );
}
void Cec_GiaSplitPrintRefs( Gia_Man_t * p )
{
    Gia_Obj_t * pObj;
    int i;
    if ( p->pRefs == NULL )
        Gia_ManCreateRefs( p ); 
    Gia_ManForEachPi( p, pObj, i )
        printf( "%d ", Gia_ObjRefNum(p, pObj) );
    printf( "\n" );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent )
{
    abctime clkTotal = Abc_Clock();
    Vec_Ptr_t * vStack;
    Cnf_Dat_t * pCnf;
    int nSatVars, nSatConfs;
    int nIter, status, RetValue = -1;
    double Progress = 0;
    // check the problem
    pCnf = Cec_GiaDeriveGiaRemapped( p );
    status = Cnf_GiaSolveOne( p, pCnf, nTimeOut, &nSatVars, &nSatConfs );
    Cnf_DataFree( pCnf );
    if ( fVerbose )
        Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
    if ( status == 0 )
    {
        if ( !fSilent )
        printf( "The problem is SAT without cofactoring.\n" );
        return 0;
    }
    if ( status == 1 )
    {
        if ( !fSilent )
        printf( "The problem is UNSAT without cofactoring.\n" );
        return 1;
    }
    assert( status == -1 );
    // create local copy
    vStack = Vec_PtrAlloc( 1000 );
    Vec_PtrPush( vStack, Gia_ManDup(p) );
    // start with the current problem
    for ( nIter = 1; Vec_PtrSize(vStack) > 0; nIter++ )
    {
        // get the last AIG
        Gia_Man_t * pLast = (Gia_Man_t *)Vec_PtrPop( vStack );
        // determine cofactoring variable
        int Depth = 1 + (pLast->vCofVars ? Vec_IntSize(pLast->vCofVars) : 0);
        int nFanouts, Cost, iVar  = Gia_SplitCofVar( pLast, LookAhead, &nFanouts, &Cost );
        // cofactor
        Gia_Man_t * pPart = Gia_ManDupCofactorVar( pLast, iVar, 0 );
        if ( pLast->vCofVars == NULL )
            pLast->vCofVars = Vec_IntAlloc( 100 );
        // print results
        if ( fVeryVerbose )
        {
//            Cec_GiaSplitPrintRefs( pLast );
            printf( "Var = %5d. Fanouts = %5d. Cost = %8d.  AndBefore = %6d.  AndAfter = %6d.\n", 
                iVar, nFanouts, Cost, Gia_ManAndNum(pLast), Gia_ManAndNum(pPart) );
//            Cec_GiaSplitPrintRefs( pPart );
        }
        // create variable
        pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
        Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
        Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
        // solve the problem
        pCnf = Cec_GiaDeriveGiaRemapped( pPart );
        status = Cnf_GiaSolveOne( pPart, pCnf, nTimeOut, &nSatVars, &nSatConfs );
        Cnf_DataFree( pCnf );
        if ( status == 1 )
            Progress += 1.0 / pow(2, Depth);
        if ( fVerbose ) 
            Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
        if ( status == 0 ) // SAT
        {
            p->pCexComb = pPart->pCexComb;  pPart->pCexComb = NULL;
            Gia_ManStop( pLast );
            Gia_ManStop( pPart );
            RetValue = 0;
            break;
        }
        if ( status == 1 ) // UNSAT
            Gia_ManStop( pPart );
        else               // UNDEC
            Vec_PtrPush( vStack, pPart );
        // cofactor
        pPart = Gia_ManDupCofactorVar( pLast, iVar, 1 );
        // create variable
        pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
        Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
        Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 0) );
        Gia_ManStop( pLast );
        // solve the problem
        pCnf = Cec_GiaDeriveGiaRemapped( pPart );
        status = Cnf_GiaSolveOne( pPart, pCnf, nTimeOut, &nSatVars, &nSatConfs );
        Cnf_DataFree( pCnf );
        if ( status == 1 )
            Progress += 1.0 / pow(2, Depth);
        if ( fVerbose )
            Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
        if ( status == 0 ) // SAT
        {
            p->pCexComb = pPart->pCexComb;  pPart->pCexComb = NULL;
            Gia_ManStop( pPart );
            RetValue = 0;
            break;
        }
        if ( status == 1 ) // UNSAT
            Gia_ManStop( pPart );
        else               // UNDEC
            Vec_PtrPush( vStack, pPart );
        if ( nIterMax && nIter >= nIterMax )
            break;
    }
    if ( Vec_PtrSize(vStack) == 0 )
        RetValue = 1;
    // finish
    Cec_GiaSplitClean( vStack );
    if ( !fSilent )
    {
        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 );
        fflush( stdout );
    }
    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         iThread;
    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_GiaSplitTestInt( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent )
{
    abctime clkTotal = Abc_Clock();
    Par_ThData_t ThData[PAR_THR_MAX];
    pthread_t WorkerThread[PAR_THR_MAX];
    Vec_Ptr_t * vStack;
    Cnf_Dat_t * pCnf;
    double Progress = 0;
    int i, status, nSatVars, nSatConfs;
    int nIter = 0, RetValue = -1, fWorkToDo = 1;
    Abc_CexFreeP( &p->pCexComb );
    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 );
    fflush( stdout );
    if ( nProcs == 1 )
        return Cec_GiaSplitTest2( p, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose, fSilent );
    // subtract manager thread
    nProcs--;
    assert( nProcs >= 1 && nProcs <= PAR_THR_MAX );
    // check the problem
    pCnf = Cec_GiaDeriveGiaRemapped( p );
    status = Cnf_GiaSolveOne( p, pCnf, nTimeOut, &nSatVars, &nSatConfs );
    Cnf_DataFree( pCnf );
    if ( fVerbose && status != -1 )
        Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
    if ( status == 0 )
    {
        if ( !fSilent )
        printf( "The problem is SAT without cofactoring.\n" );
        return 0;
    }
    if ( status == 1 )
    {
        if ( !fSilent )
        printf( "The problem is UNSAT without cofactoring.\n" );
        return 1;
    }
    assert( status == -1 );
    // create local copy
    vStack = Vec_PtrAlloc( 1000 );
    Vec_PtrPush( vStack, Gia_ManDup(p) );
    // start threads
    for ( i = 0; i < nProcs; i++ )
    {
        ThData[i].p        = NULL;
        ThData[i].pCnf     = NULL;
        ThData[i].iThread  = i;
        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 = pLast->vCofVars ? Vec_IntSize(pLast->vCofVars) : 0;
                if ( pLast->vCofVars == NULL )
                    pLast->vCofVars = Vec_IntAlloc( 100 );
                if ( fVerbose )
                    Cec_GiaSplitPrint( i+1, Depth, ThData[i].nVars, ThData[i].nConfs, ThData[i].Result, Progress, Abc_Clock() - clkTotal );
                if ( ThData[i].Result == 0 ) // SAT
                {
                    p->pCexComb = pLast->pCexComb;  pLast->pCexComb = NULL;
                    RetValue = 0;
                    goto finish;
                }
                if ( ThData[i].Result == -1 ) // UNDEC
                {
                    // determine cofactoring variable
                    int nFanouts, Cost, iVar = Gia_SplitCofVar( pLast, LookAhead, &nFanouts, &Cost );
                    // cofactor
                    Gia_Man_t * pPart = Gia_ManDupCofactorVar( 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 );
                    // print results
                    if ( fVeryVerbose )
                    {
//                        Cec_GiaSplitPrintRefs( pLast );
                        printf( "Var = %5d. Fanouts = %5d. Cost = %8d.  AndBefore = %6d.  AndAfter = %6d.\n", 
                            iVar, nFanouts, Cost, Gia_ManAndNum(pLast), Gia_ManAndNum(pPart) );
//                        Cec_GiaSplitPrintRefs( pPart );
                    }
                    // cofactor
                    pPart = Gia_ManDupCofactorVar( 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 = (Gia_Man_t*)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 ( !fSilent )
    {
        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 );
        fflush( stdout );
    }
    return RetValue;
}
int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent )
{
    Abc_Cex_t * pCex = NULL;
    Gia_Man_t * pOne;
    Gia_Obj_t * pObj;
    int i, RetValue1, fOneUndef = 0, RetValue = -1;
    Abc_CexFreeP( &p->pCexComb );
    Gia_ManForEachPo( p, pObj, i )
    {
        pOne = Gia_ManDupOutputGroup( p, i, i+1 );
        if ( fVerbose )
            printf( "\nSolving output %d:\n", i );
        RetValue1 = Cec_GiaSplitTestInt( pOne, nProcs, nTimeOut, nIterMax, LookAhead,  fVerbose, fVeryVerbose, fSilent );
        Gia_ManStop( pOne );
        // collect the result
        if ( RetValue1 == 0 && RetValue == -1 )
        {
            pCex = pOne->pCexComb; pOne->pCexComb = NULL;
            pCex->iPo = i;
            RetValue = 0;
        }
        if ( RetValue1 == -1 )
            fOneUndef = 1;
    }
    if ( RetValue == -1 )
        RetValue = fOneUndef ? -1 : 1;
    else
        p->pCexComb = pCex;
    return RetValue;
}

/**Function*************************************************************

  Synopsis    [Print stats about cofactoring variables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cec_GiaPrintCofStats( Gia_Man_t * p )
{
    Gia_Man_t * pCof0, * pCof1;
    Gia_Obj_t * pObj, * pFan0, * pFan1, * pCtrl;
    Vec_Int_t * vMarks;
    int i, Count = 0;
    vMarks = Vec_IntStart( Gia_ManObjNum(p) );
    Gia_ManForEachAnd( p, pObj, i )
    {
        if ( !Gia_ObjIsMuxType(pObj) )
            continue;
        if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
            continue;
        pCtrl = Gia_ObjRecognizeMux( pObj, &pFan1, &pFan0 );
        pCtrl = Gia_Regular(pCtrl);
        Vec_IntAddToEntry( vMarks, Gia_ObjId(p, pCtrl), 1 );
    }
    printf( "The AIG with %d candidate nodes (PI+AND) has %d unique MUX control drivers:\n", 
        Gia_ManCandNum(p), Vec_IntCountPositive(vMarks) );
    Gia_ManLevelNum( p );
    Gia_ManForEachCand( p, pObj, i )
    {
        if ( !Vec_IntEntry(vMarks, i) )
            continue;
        pCof0 = Gia_ManDupCofactorObj( p, i, 0 );
        pCof1 = Gia_ManDupCofactorObj( p, i, 1 );
        printf( "%6d :   ",          Count++ );
        printf( "Obj = %6d   ",      i );
        printf( "MUX refs = %5d   ", Vec_IntEntry(vMarks, i) );
        printf( "Level = %5d   ",    Gia_ObjLevelId(p, i) );
        printf( "Cof0 = %7d   ",     Gia_ManAndNum(pCof0) );
        printf( "Cof1 = %7d   ",     Gia_ManAndNum(pCof1) );
        printf( "\n" );
        Gia_ManStop( pCof0 );
        Gia_ManStop( pCof1 );
    }
    Vec_IntFree( vMarks );
}
void Cec_GiaPrintCofStats2( Gia_Man_t * p )
{
    Gia_Man_t * pCof0, * pCof1;
    Gia_Obj_t * pObj;
    int i;
    Gia_ManLevelNum( p );
    Gia_ManCreateRefs( p );
    Gia_ManForEachPi( p, pObj, i )
    {
        pCof0 = Gia_ManDupCofactorVar( p, i, 0 );
        pCof1 = Gia_ManDupCofactorVar( p, i, 1 );
        printf( "PI %5d :   ",   i );
        printf( "Refs = %5d   ", Gia_ObjRefNum(p, pObj) );
        printf( "Cof0 = %7d   ", Gia_ManAndNum(pCof0) );
        printf( "Cof1 = %7d   ", Gia_ManAndNum(pCof1) );
        printf( "\n" );
        Gia_ManStop( pCof0 );
        Gia_ManStop( pCof1 );
    }
}

#endif // pthreads are used

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END