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

  FileName    [cnfFast.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [AIG-to-CNF conversion.]

  Synopsis    []

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - April 28, 2007.]

  Revision    [$Id: cnfFast.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]

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

#include "cnf.h"
#include "bool/kit/kit.h"

ABC_NAMESPACE_IMPL_START

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

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

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

  Synopsis    [Detects multi-input gate rooted at this node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_CollectLeaves_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fStopCompl )
{
    if ( pRoot != pObj && (pObj->fMarkA || (fStopCompl && Aig_IsComplement(pObj))) )
    {
        Vec_PtrPushUnique( vSuper, fStopCompl ? pObj : Aig_Regular(pObj) );
        return;
    }
    assert( Aig_ObjIsNode(pObj) );
    if ( fStopCompl )
    {
        Cnf_CollectLeaves_rec( pRoot, Aig_ObjChild0(pObj), vSuper, 1 );
        Cnf_CollectLeaves_rec( pRoot, Aig_ObjChild1(pObj), vSuper, 1 );
    }
    else
    {
        Cnf_CollectLeaves_rec( pRoot, Aig_ObjFanin0(pObj), vSuper, 0 );
        Cnf_CollectLeaves_rec( pRoot, Aig_ObjFanin1(pObj), vSuper, 0 );
    }
}

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

  Synopsis    [Detects multi-input gate rooted at this node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_CollectLeaves( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper, int fStopCompl )
{
    assert( !Aig_IsComplement(pRoot) );
    Vec_PtrClear( vSuper );
    Cnf_CollectLeaves_rec( pRoot, pRoot, vSuper, fStopCompl );
}

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

  Synopsis    [Collects nodes inside the cone.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_CollectVolume_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
{
    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
        return;
    Aig_ObjSetTravIdCurrent( p, pObj );
    assert( Aig_ObjIsNode(pObj) );
    Cnf_CollectVolume_rec( p, Aig_ObjFanin0(pObj), vNodes );
    Cnf_CollectVolume_rec( p, Aig_ObjFanin1(pObj), vNodes );
    Vec_PtrPush( vNodes, pObj );
}

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

  Synopsis    [Collects nodes inside the cone.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_CollectVolume( Aig_Man_t * p, Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManIncrementTravId( p );
    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
        Aig_ObjSetTravIdCurrent( p, pObj );
    Vec_PtrClear( vNodes );
    Cnf_CollectVolume_rec( p, pRoot, vNodes );
}

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

  Synopsis    [Derive truth table.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
word Cnf_CutDeriveTruth( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
{
    static word Truth6[6] = {
        ABC_CONST(0xAAAAAAAAAAAAAAAA),
        ABC_CONST(0xCCCCCCCCCCCCCCCC),
        ABC_CONST(0xF0F0F0F0F0F0F0F0),
        ABC_CONST(0xFF00FF00FF00FF00),
        ABC_CONST(0xFFFF0000FFFF0000),
        ABC_CONST(0xFFFFFFFF00000000)
    };
    static word C[2] = { 0, ~(word)0 };
    static word S[256];
    Aig_Obj_t * pObj = NULL;
    int i;
    assert( Vec_PtrSize(vLeaves) <= 6 && Vec_PtrSize(vNodes) > 0 );
    assert( Vec_PtrSize(vLeaves) + Vec_PtrSize(vNodes) <= 256 );
    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
    {
        pObj->iData    = i;
        S[pObj->iData] = Truth6[i];
    }
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
    {
        pObj->iData    = Vec_PtrSize(vLeaves) + i;
        S[pObj->iData] = (S[Aig_ObjFanin0(pObj)->iData] ^ C[Aig_ObjFaninC0(pObj)]) & 
                         (S[Aig_ObjFanin1(pObj)->iData] ^ C[Aig_ObjFaninC1(pObj)]);
    }
    return S[pObj->iData];
}


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

  Synopsis    [Collects nodes inside the cone.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
static inline int Cnf_ObjGetLit( Vec_Int_t * vMap, Aig_Obj_t * pObj, int fCompl )
{
    int iSatVar = vMap ? Vec_IntEntry(vMap, Aig_ObjId(pObj)) : Aig_ObjId(pObj);
    assert( iSatVar > 0 );
    return iSatVar + iSatVar + fCompl;
}

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

  Synopsis    [Collects nodes inside the cone.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, 
    Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vMap, Vec_Int_t * vCover, Vec_Int_t * vClauses )
{
    Aig_Obj_t * pLeaf;
    int c, k, Cube, OutLit, RetValue;
    word Truth;
    assert( pRoot->fMarkA );

    Vec_IntClear( vClauses );

    OutLit = Cnf_ObjGetLit( vMap, pRoot, 0 );
    // detect cone
    Cnf_CollectLeaves( pRoot, vLeaves, 0 );
    Cnf_CollectVolume( p, pRoot, vLeaves, vNodes );
    assert( pRoot == Vec_PtrEntryLast(vNodes) );
    // check if this is an AND-gate
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pLeaf, k )
    {
        if ( Aig_ObjFaninC0(pLeaf) && !Aig_ObjFanin0(pLeaf)->fMarkA )
            break;
        if ( Aig_ObjFaninC1(pLeaf) && !Aig_ObjFanin1(pLeaf)->fMarkA )
            break;
    }
    if ( k == Vec_PtrSize(vNodes) )
    {
        Cnf_CollectLeaves( pRoot, vLeaves, 1 );
        // write big clause
        Vec_IntPush( vClauses, 0 );
        Vec_IntPush( vClauses, OutLit );
        Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
            Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, Aig_Regular(pLeaf), !Aig_IsComplement(pLeaf)) );
        // write small clauses
        Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
        {
            Vec_IntPush( vClauses, 0 );
            Vec_IntPush( vClauses, OutLit ^ 1 );
            Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, Aig_Regular(pLeaf), Aig_IsComplement(pLeaf)) );
        }
        return;
    }
    if ( Vec_PtrSize(vLeaves) > 6 )
        printf( "FastCnfGeneration:  Internal error!!!\n" );
    assert( Vec_PtrSize(vLeaves) <= 6 );

    Truth = Cnf_CutDeriveTruth( p, vLeaves, vNodes );
    if ( Truth == 0 || Truth == ~(word)0 )
    {
        Vec_IntPush( vClauses, 0 );
        Vec_IntPush( vClauses, (Truth == 0) ? (OutLit ^ 1) : OutLit );
        return;
    }

    RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
    assert( RetValue >= 0 );

    Vec_IntForEachEntry( vCover, Cube, c )
    {
        Vec_IntPush( vClauses, 0 );
        Vec_IntPush( vClauses, OutLit );
        for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
        {
            if ( (Cube & 3) == 0 )
                continue;
            assert( (Cube & 3) != 3 );
            Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, (Aig_Obj_t *)Vec_PtrEntry(vLeaves,k), (Cube&3)!=1) );
        }
    }

    Truth = ~Truth;

    RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
    assert( RetValue >= 0 );
    Vec_IntForEachEntry( vCover, Cube, c )
    {
        Vec_IntPush( vClauses, 0 );
        Vec_IntPush( vClauses, OutLit ^ 1 );
        for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
        {
            if ( (Cube & 3) == 0 )
                continue;
            assert( (Cube & 3) != 3 );
            Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, (Aig_Obj_t *)Vec_PtrEntry(vLeaves,k), (Cube&3)!=1) );
        }
    }
}


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

  Synopsis    [Marks AIG for CNF computation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_DeriveFastMark( Aig_Man_t * p )
{
    Vec_Int_t * vSupps;
    Vec_Ptr_t * vLeaves, * vNodes;
    Aig_Obj_t * pObj, * pTemp, * pObjC, * pObj0, * pObj1;
    int i, k, nFans, Counter;

    vLeaves = Vec_PtrAlloc( 100 );
    vNodes  = Vec_PtrAlloc( 100 );
    vSupps  = Vec_IntStart( Aig_ManObjNumMax(p) );

    // mark CIs
    Aig_ManForEachCi( p, pObj, i )
        pObj->fMarkA = 1;

    // mark CO drivers
    Aig_ManForEachCo( p, pObj, i )
        Aig_ObjFanin0(pObj)->fMarkA = 1;

    // mark MUX/XOR nodes
    Aig_ManForEachNode( p, pObj, i )
    {
        assert( !pObj->fMarkB );
        if ( !Aig_ObjIsMuxType(pObj) )
            continue;
        pObj0 = Aig_ObjFanin0(pObj);
        if ( pObj0->fMarkB || Aig_ObjRefs(pObj0) > 1 )
            continue;
        pObj1 = Aig_ObjFanin1(pObj);
        if ( pObj1->fMarkB || Aig_ObjRefs(pObj1) > 1 )
            continue;
        // mark nodes
        pObj->fMarkB = 1;
        pObj0->fMarkB = 1;
        pObj1->fMarkB = 1;
        // mark inputs and outputs
        pObj->fMarkA = 1;
        Aig_ObjFanin0(pObj0)->fMarkA = 1;
        Aig_ObjFanin1(pObj0)->fMarkA = 1;
        Aig_ObjFanin0(pObj1)->fMarkA = 1;
        Aig_ObjFanin1(pObj1)->fMarkA = 1;
    }

    // mark nodes with multiple fanouts and pointed to by complemented edges
    Aig_ManForEachNode( p, pObj, i )
    {
        // mark nodes with many fanouts
        if ( Aig_ObjRefs(pObj) > 1 )
            pObj->fMarkA = 1;
        // mark nodes pointed to by a complemented edge
        if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFanin0(pObj)->fMarkB )
            Aig_ObjFanin0(pObj)->fMarkA = 1;
        if ( Aig_ObjFaninC1(pObj) && !Aig_ObjFanin1(pObj)->fMarkB )
            Aig_ObjFanin1(pObj)->fMarkA = 1;
    }

    // compute supergate size for internal marked nodes
    Aig_ManForEachNode( p, pObj, i )
    {
        if ( !pObj->fMarkA )
            continue;
        if ( pObj->fMarkB )
        {
            if ( !Aig_ObjIsMuxType(pObj) )
                continue;
            pObjC = Aig_ObjRecognizeMux( pObj, &pObj1, &pObj0 );
            pObj0 = Aig_Regular(pObj0);
            pObj1 = Aig_Regular(pObj1);
            assert( pObj0->fMarkA );
            assert( pObj1->fMarkA );
//            if ( pObj0 == pObj1 )
//                continue;
            nFans = 1 + (pObj0 == pObj1);
            if ( !pObj0->fMarkB && !Aig_ObjIsCi(pObj0) && Aig_ObjRefs(pObj0) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj0)) < 3 )
            {
                pObj0->fMarkA = 0;
                continue;
            }
            if ( !pObj1->fMarkB && !Aig_ObjIsCi(pObj1) && Aig_ObjRefs(pObj1) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj1)) < 3 )
            {
                pObj1->fMarkA = 0;
                continue;
            }
            continue;
        }

        Cnf_CollectLeaves( pObj, vLeaves, 1 );
        Vec_IntWriteEntry( vSupps, Aig_ObjId(pObj), Vec_PtrSize(vLeaves) );
        if ( Vec_PtrSize(vLeaves) >= 6 )
            continue;
        Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pTemp, k )
        {
            pTemp = Aig_Regular(pTemp);
            assert( pTemp->fMarkA );
            if ( pTemp->fMarkB || Aig_ObjIsCi(pTemp) || Aig_ObjRefs(pTemp) > 1 )
                continue;
            assert( Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 0 );
            if ( Vec_PtrSize(vLeaves) - 1 + Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 6 )
                continue;
            pTemp->fMarkA = 0;
            Vec_IntWriteEntry( vSupps, Aig_ObjId(pObj), 6 );
//printf( "%d %d   ", Vec_PtrSize(vLeaves), Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) );
            break;
        }
    }
    Aig_ManCleanMarkB( p );

    // check CO drivers
    Counter = 0;
    Aig_ManForEachCo( p, pObj, i )
        Counter += !Aig_ObjFanin0(pObj)->fMarkA;
    if ( Counter )
    printf( "PO-driver rule is violated %d times.\n", Counter );

    // check that the AND-gates are fine
    Counter = 0;
    Aig_ManForEachNode( p, pObj, i )
    {
        assert( pObj->fMarkB == 0 );
        if ( !pObj->fMarkA )
            continue;
        Cnf_CollectLeaves( pObj, vLeaves, 0 );
        if ( Vec_PtrSize(vLeaves) <= 6 )
            continue;
        Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, k )
        {
            if ( Aig_ObjFaninC0(pTemp) && !Aig_ObjFanin0(pTemp)->fMarkA )
                Counter++;
            if ( Aig_ObjFaninC1(pTemp) && !Aig_ObjFanin1(pTemp)->fMarkA )
                Counter++;
        }
    }
    if ( Counter )
    printf( "AND-gate rule is violated %d times.\n", Counter );

    Vec_PtrFree( vLeaves );
    Vec_PtrFree( vNodes );
    Vec_IntFree( vSupps );
}


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

  Synopsis    [Counts the number of clauses.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cnf_CutCountClauses( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vCover )
{
    word Truth;
    Aig_Obj_t * pObj;
    int i, RetValue, nSize = 0;
    if ( Vec_PtrSize(vLeaves) > 6 )
    {
        // make sure this is an AND gate
        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        {
            if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFanin0(pObj)->fMarkA )
                printf( "Unusual 1!\n" );
            if ( Aig_ObjFaninC1(pObj) && !Aig_ObjFanin1(pObj)->fMarkA )
                printf( "Unusual 2!\n" );
            continue;

            assert( !Aig_ObjFaninC0(pObj) || Aig_ObjFanin0(pObj)->fMarkA );
            assert( !Aig_ObjFaninC1(pObj) || Aig_ObjFanin1(pObj)->fMarkA );
        }
        return Vec_PtrSize(vLeaves) + 1;
    }
    Truth = Cnf_CutDeriveTruth( p, vLeaves, vNodes );

    RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
    assert( RetValue >= 0 );
    nSize += Vec_IntSize(vCover);

    Truth = ~Truth;

    RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
    assert( RetValue >= 0 );
    nSize += Vec_IntSize(vCover);
    return nSize;
}

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

  Synopsis    [Counts the size of the CNF, assuming marks are set.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cnf_CountCnfSize( Aig_Man_t * p )
{
    Vec_Ptr_t * vLeaves, * vNodes;
    Vec_Int_t * vCover;
    Aig_Obj_t * pObj;
    int nVars = 0, nClauses = 0;
    int i, nSize;

    vLeaves = Vec_PtrAlloc( 100 );
    vNodes  = Vec_PtrAlloc( 100 );
    vCover  = Vec_IntAlloc( 1 << 16 );

    Aig_ManForEachObj( p, pObj, i )
        nVars += pObj->fMarkA;

    Aig_ManForEachNode( p, pObj, i )
    {
        if ( !pObj->fMarkA )
            continue;
        Cnf_CollectLeaves( pObj, vLeaves, 0 );
        Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
        assert( pObj == Vec_PtrEntryLast(vNodes) );

        nSize = Cnf_CutCountClauses( p, vLeaves, vNodes, vCover );
//        printf( "%d(%d) ", Vec_PtrSize(vLeaves), nSize );

        nClauses += nSize;
    }
//    printf( "\n" );
    printf( "Vars = %d  Clauses = %d\n", nVars, nClauses );

    Vec_PtrFree( vLeaves );
    Vec_PtrFree( vNodes );
    Vec_IntFree( vCover );
    return nClauses;
}

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

  Synopsis    [Derives CNF from the marked AIG.]

  Description [Assumes that marking is such that when we traverse from each
  marked node, the logic cone has 6 inputs or less, or it is a multi-input AND.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs )
{
    Cnf_Dat_t * pCnf;
    Vec_Int_t * vLits, * vClas, * vMap, * vTemp;
    Vec_Ptr_t * vLeaves, * vNodes;
    Vec_Int_t * vCover;
    Aig_Obj_t * pObj;
    int i, k, nVars, Entry, OutLit, DriLit;

    vLits = Vec_IntAlloc( 1 << 16 );
    vClas = Vec_IntAlloc( 1 << 12 );
    vMap  = Vec_IntStartFull( Aig_ManObjNumMax(p) );

    // assign variables for the outputs
    nVars = 1;
    if ( nOutputs )
    {
        if ( Aig_ManRegNum(p) == 0 )
        {
            assert( nOutputs == Aig_ManCoNum(p) );
            Aig_ManForEachCo( p, pObj, i )
                Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
        }
        else
        {
            assert( nOutputs == Aig_ManRegNum(p) );
            Aig_ManForEachLiSeq( p, pObj, i )
                Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
        }
    }
    // assign variables to the internal nodes
    Aig_ManForEachNodeReverse( p, pObj, i )
        if ( pObj->fMarkA )
            Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
    // assign variables to the PIs and constant node
    Aig_ManForEachCi( p, pObj, i )
        Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
    Vec_IntWriteEntry( vMap, Aig_ObjId(Aig_ManConst1(p)), nVars++ );

    // create clauses
    vLeaves = Vec_PtrAlloc( 100 );
    vNodes  = Vec_PtrAlloc( 100 );
    vCover  = Vec_IntAlloc( 1 << 16 );
    vTemp   = Vec_IntAlloc( 100 );
    Aig_ManForEachNodeReverse( p, pObj, i )
    {
        if ( !pObj->fMarkA )
            continue;
        Cnf_ComputeClauses( p, pObj, vLeaves, vNodes, vMap, vCover, vTemp );
        Vec_IntForEachEntry( vTemp, Entry, k )
        {
            if ( Entry == 0 )
                Vec_IntPush( vClas, Vec_IntSize(vLits) );
            else
                Vec_IntPush( vLits, Entry );
        }       
    }
    Vec_PtrFree( vLeaves );
    Vec_PtrFree( vNodes );
    Vec_IntFree( vCover );
    Vec_IntFree( vTemp );

    // create clauses for the outputs
    Aig_ManForEachCo( p, pObj, i )
    {
        DriLit = Cnf_ObjGetLit( vMap, Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj) );
        if ( i < Aig_ManCoNum(p) - nOutputs )
        {
            Vec_IntPush( vClas, Vec_IntSize(vLits) );
            Vec_IntPush( vLits, DriLit );
        }
        else
        {
            OutLit = Cnf_ObjGetLit( vMap, pObj, 0 );
            // first clause
            Vec_IntPush( vClas, Vec_IntSize(vLits) );
            Vec_IntPush( vLits, OutLit );
            Vec_IntPush( vLits, DriLit ^ 1 );
            // second clause
            Vec_IntPush( vClas, Vec_IntSize(vLits) );
            Vec_IntPush( vLits, OutLit ^ 1 );
            Vec_IntPush( vLits, DriLit );
        }
    }
 
    // write the constant literal
    OutLit = Cnf_ObjGetLit( vMap, Aig_ManConst1(p), 0 );
    Vec_IntPush( vClas, Vec_IntSize(vLits) );
    Vec_IntPush( vLits, OutLit );

    // create structure
    pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
    pCnf->pMan = p;
    pCnf->nVars = nVars;
    pCnf->nLiterals = Vec_IntSize( vLits );
    pCnf->nClauses  = Vec_IntSize( vClas );
    pCnf->pClauses  = ABC_ALLOC( int *, pCnf->nClauses + 1 );
    pCnf->pClauses[0] = Vec_IntReleaseArray( vLits );
    Vec_IntForEachEntry( vClas, Entry, i )
        pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
    pCnf->pClauses[pCnf->nClauses] = pCnf->pClauses[0] + pCnf->nLiterals;
    pCnf->pVarNums  = Vec_IntReleaseArray( vMap );

    // cleanup
    Vec_IntFree( vLits );
    Vec_IntFree( vClas );
    Vec_IntFree( vMap );
    return pCnf;
}

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

  Synopsis    [Fast CNF computation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs )
{
    Cnf_Dat_t * pCnf = NULL;
    abctime clk;//, clkTotal = Abc_Clock();
//    printf( "\n" );
    Aig_ManCleanMarkAB( p );
    // create initial marking
    clk = Abc_Clock();
    Cnf_DeriveFastMark( p );
//    Abc_PrintTime( 1, "Marking", Abc_Clock() - clk );
    // compute CNF size
    clk = Abc_Clock();
    pCnf = Cnf_DeriveFastClauses( p, nOutputs );
//    Abc_PrintTime( 1, "Clauses", Abc_Clock() - clk );
    // derive the resulting CNF
    Aig_ManCleanMarkA( p );
//    Abc_PrintTime( 1, "TOTAL  ", Abc_Clock() - clkTotal );

//    printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d.   \n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );

//    Cnf_DataFree( pCnf );
//    pCnf = NULL;
    return pCnf;
}

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


ABC_NAMESPACE_IMPL_END