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

  FileName    [cnfWrite.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: cnfWrite.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]

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

#include "cnf.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [Derives CNF mapping.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Cnf_ManWriteCnfMapping( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
{
    Vec_Int_t * vResult;
    Aig_Obj_t * pObj;
    Cnf_Cut_t * pCut;
    int i, k, nOffset;
    nOffset = Aig_ManObjNumMax(p->pManAig);
    vResult = Vec_IntStart( nOffset );
    Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
    {
        assert( Aig_ObjIsNode(pObj) );
        pCut = Cnf_ObjBestCut( pObj );
        assert( pCut->nFanins < 5 );
        Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), nOffset );
        Vec_IntPush( vResult, *Cnf_CutTruth(pCut) );
        for ( k = 0; k < pCut->nFanins; k++ )
            Vec_IntPush( vResult, pCut->pFanins[k] );
        for (      ; k < 4; k++ )
            Vec_IntPush( vResult, -1 );
        nOffset += 5;
    }
    return vResult;
}


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

  Synopsis    [Writes the cover into the array.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover )
{
    int Lits[4], Cube, iCube, i, b;
    Vec_IntClear( vCover );
    for ( i = 0; i < nCubes; i++ )
    {
        Cube = pSop[i];
        for ( b = 0; b < 4; b++ )
        {
            if ( Cube % 3 == 0 )
                Lits[b] = 1;
            else if ( Cube % 3 == 1 )
                Lits[b] = 2;
            else
                Lits[b] = 0;
            Cube = Cube / 3;
        }
        iCube = 0;
        for ( b = 0; b < 4; b++ )
            iCube = (iCube << 2) | Lits[b];
        Vec_IntPush( vCover, iCube );
    }
}

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

  Synopsis    [Returns the number of literals in the SOP.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cnf_SopCountLiterals( char * pSop, int nCubes )
{
    int nLits = 0, Cube, i, b;
    for ( i = 0; i < nCubes; i++ )
    {
        Cube = pSop[i];
        for ( b = 0; b < 4; b++ )
        {
            if ( Cube % 3 != 2 )
                nLits++;
            Cube = Cube / 3;
        }
    }
    return nLits;
}

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

  Synopsis    [Returns the number of literals in the SOP.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cnf_IsopCountLiterals( Vec_Int_t * vIsop, int nVars )
{
    int nLits = 0, Cube, i, b;
    Vec_IntForEachEntry( vIsop, Cube, i )
    {
        for ( b = 0; b < nVars; b++ )
        {
            if ( (Cube & 3) == 1 || (Cube & 3) == 2 )
                nLits++;
            Cube >>= 2;
        }
    }
    return nLits;
}

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

  Synopsis    [Writes the cube and returns the number of literals in it.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int * pLiterals )
{
    int nLits = nVars, b;
    for ( b = 0; b < nVars; b++ )
    {
        if ( (Cube & 3) == 1 ) // value 0 --> write positive literal
            *pLiterals++ = 2 * pVars[b];
        else if ( (Cube & 3) == 2 ) // value 1 --> write negative literal
            *pLiterals++ = 2 * pVars[b] + 1;
        else
            nLits--;
        Cube >>= 2;
    }
    return nLits;
}

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

  Synopsis    [Derives CNF for the mapping.]

  Description [The last argument shows the number of last outputs
  of the manager, which will not be converted into clauses but the
  new variables for which will be introduced.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
{
    int fChangeVariableOrder = 0; // should be set to 0 to improve performance
    Aig_Obj_t * pObj;
    Cnf_Dat_t * pCnf;
    Cnf_Cut_t * pCut;
    Vec_Int_t * vCover, * vSopTemp;
    int OutVar, PoVar, pVars[32], * pLits, ** pClas;
    unsigned uTruth;
    int i, k, nLiterals, nClauses, Cube, Number;

    // count the number of literals and clauses
    nLiterals = 1 + Aig_ManCoNum( p->pManAig ) + 3 * nOutputs;
    nClauses = 1 + Aig_ManCoNum( p->pManAig ) + nOutputs;
    Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
    {
        assert( Aig_ObjIsNode(pObj) );
        pCut = Cnf_ObjBestCut( pObj );

        // positive polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
            nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
            assert( p->pSopSizes[uTruth] >= 0 );
            nClauses += p->pSopSizes[uTruth];
        }
        else
        {
            nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
            nClauses += Vec_IntSize(pCut->vIsop[1]);
        }
        // negative polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
            nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
            assert( p->pSopSizes[uTruth] >= 0 );
            nClauses += p->pSopSizes[uTruth];
        }
        else
        {
            nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
            nClauses += Vec_IntSize(pCut->vIsop[0]);
        }
//printf( "%d ", nClauses-(1 + Aig_ManCoNum( p->pManAig )) );
    }
//printf( "\n" );

    // allocate CNF
    pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
    pCnf->pMan = p->pManAig;
    pCnf->nLiterals = nLiterals;
    pCnf->nClauses = nClauses;
    pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
    pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
    pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
    // create room for variable numbers
    pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
//    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p->pManAig) );
    for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ )
        pCnf->pVarNums[i] = -1;

    if ( !fChangeVariableOrder )
    {
        // assign variables to the last (nOutputs) POs
        Number = 1;
        if ( nOutputs )
        {
            if ( Aig_ManRegNum(p->pManAig) == 0 )
            {
                assert( nOutputs == Aig_ManCoNum(p->pManAig) );
                Aig_ManForEachCo( p->pManAig, pObj, i )
                    pCnf->pVarNums[pObj->Id] = Number++;
            }
            else
            {
                assert( nOutputs == Aig_ManRegNum(p->pManAig) );
                Aig_ManForEachLiSeq( p->pManAig, pObj, i )
                    pCnf->pVarNums[pObj->Id] = Number++;
            }
        }
        // assign variables to the internal nodes
        Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
            pCnf->pVarNums[pObj->Id] = Number++;
        // assign variables to the PIs and constant node
        Aig_ManForEachCi( p->pManAig, pObj, i )
            pCnf->pVarNums[pObj->Id] = Number++;
        pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number++;
        pCnf->nVars = Number;
    }
    else
    {
        // assign variables to the last (nOutputs) POs
        Number = Aig_ManObjNumMax(p->pManAig) + 1;
        pCnf->nVars = Number + 1;
        if ( nOutputs )
        {
            if ( Aig_ManRegNum(p->pManAig) == 0 )
            {
                assert( nOutputs == Aig_ManCoNum(p->pManAig) );
                Aig_ManForEachCo( p->pManAig, pObj, i )
                    pCnf->pVarNums[pObj->Id] = Number--;
            }
            else
            {
                assert( nOutputs == Aig_ManRegNum(p->pManAig) );
                Aig_ManForEachLiSeq( p->pManAig, pObj, i )
                    pCnf->pVarNums[pObj->Id] = Number--;
            }
        }
        // assign variables to the internal nodes
        Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
            pCnf->pVarNums[pObj->Id] = Number--;
        // assign variables to the PIs and constant node
        Aig_ManForEachCi( p->pManAig, pObj, i )
            pCnf->pVarNums[pObj->Id] = Number--;
        pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number--;
        assert( Number >= 0 );
    }

    // assign the clauses
    vSopTemp = Vec_IntAlloc( 1 << 16 );
    pLits = pCnf->pClauses[0];
    pClas = pCnf->pClauses;
    Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
    {
        pCut = Cnf_ObjBestCut( pObj );

        // save variables of this cut
        OutVar = pCnf->pVarNums[ pObj->Id ];
        for ( k = 0; k < (int)pCut->nFanins; k++ )
        {
            pVars[k] = pCnf->pVarNums[ pCut->pFanins[k] ];
            assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) );
        }

        // positive polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
            vCover = vSopTemp;
        }
        else
            vCover = pCut->vIsop[1];
        Vec_IntForEachEntry( vCover, Cube, k )
        {
            *pClas++ = pLits;
            *pLits++ = 2 * OutVar; 
            pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
        }

        // negative polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
            vCover = vSopTemp;
        }
        else
            vCover = pCut->vIsop[0];
        Vec_IntForEachEntry( vCover, Cube, k )
        {
            *pClas++ = pLits;
            *pLits++ = 2 * OutVar + 1; 
            pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
        }
    }
    Vec_IntFree( vSopTemp );
 
    // write the constant literal
    OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ];
    assert( OutVar <= Aig_ManObjNumMax(p->pManAig) );
    *pClas++ = pLits;
    *pLits++ = 2 * OutVar; 

    // write the output literals
    Aig_ManForEachCo( p->pManAig, pObj, i )
    {
        OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
        if ( i < Aig_ManCoNum(p->pManAig) - nOutputs )
        {
            *pClas++ = pLits;
            *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
        }
        else
        {
            PoVar = pCnf->pVarNums[ pObj->Id ];
            // first clause
            *pClas++ = pLits;
            *pLits++ = 2 * PoVar; 
            *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); 
            // second clause
            *pClas++ = pLits;
            *pLits++ = 2 * PoVar + 1; 
            *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
        }
    }

    // verify that the correct number of literals and clauses was written
    assert( pLits - pCnf->pClauses[0] == nLiterals );
    assert( pClas - pCnf->pClauses == nClauses );
//Cnf_DataPrint( pCnf, 1 );
    return pCnf;
}


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

  Synopsis    [Derives CNF for the mapping.]

  Description [Derives CNF with obj IDs as SAT vars and mapping of
  objects into clauses (pObj2Clause and pObj2Count).]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Cnf_Dat_t * Cnf_ManWriteCnfOther( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
{
    Aig_Obj_t * pObj;
    Cnf_Dat_t * pCnf;
    Cnf_Cut_t * pCut;
    Vec_Int_t * vCover, * vSopTemp;
    int OutVar, PoVar, pVars[32], * pLits, ** pClas;
    unsigned uTruth;
    int i, k, nLiterals, nClauses, Cube;

    // count the number of literals and clauses
    nLiterals = 1 + 4 * Aig_ManCoNum( p->pManAig );
    nClauses  = 1 + 2 * Aig_ManCoNum( p->pManAig );
    Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
    {
        assert( Aig_ObjIsNode(pObj) );
        pCut = Cnf_ObjBestCut( pObj );
        // positive polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
            nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
            assert( p->pSopSizes[uTruth] >= 0 );
            nClauses += p->pSopSizes[uTruth];
        }
        else
        {
            nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
            nClauses += Vec_IntSize(pCut->vIsop[1]);
        }
        // negative polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
            nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
            assert( p->pSopSizes[uTruth] >= 0 );
            nClauses += p->pSopSizes[uTruth];
        }
        else
        {
            nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
            nClauses += Vec_IntSize(pCut->vIsop[0]);
        }
    }

    // allocate CNF
    pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
    pCnf->pMan = p->pManAig;
    pCnf->nLiterals = nLiterals;
    pCnf->nClauses  = nClauses;
    pCnf->pClauses  = ABC_ALLOC( int *, nClauses + 1 );
    pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
    pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
    // create room for variable numbers
    pCnf->pObj2Clause = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
    pCnf->pObj2Count  = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
    for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ )
        pCnf->pObj2Clause[i] = pCnf->pObj2Count[i] = -1;
    pCnf->nVars = Aig_ManObjNumMax(p->pManAig);

    // clear the PI counters
    Aig_ManForEachCi( p->pManAig, pObj, i )
        pCnf->pObj2Count[pObj->Id] = 0;

    // assign the clauses
    vSopTemp = Vec_IntAlloc( 1 << 16 );
    pLits = pCnf->pClauses[0];
    pClas = pCnf->pClauses;
    Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
    {
        // remember the starting clause
        pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses;
        pCnf->pObj2Count[pObj->Id] = 0;

        // get the best cut
        pCut = Cnf_ObjBestCut( pObj );
        // save variables of this cut
        OutVar = pObj->Id;
        for ( k = 0; k < (int)pCut->nFanins; k++ )
        {
            pVars[k] = pCut->pFanins[k];
            assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) );
        }

        // positive polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
            vCover = vSopTemp;
        }
        else
            vCover = pCut->vIsop[1];
        Vec_IntForEachEntry( vCover, Cube, k )
        {
            *pClas++ = pLits;
            *pLits++ = 2 * OutVar; 
            pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
        }
        pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover);

        // negative polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
            vCover = vSopTemp;
        }
        else
            vCover = pCut->vIsop[0];
        Vec_IntForEachEntry( vCover, Cube, k )
        {
            *pClas++ = pLits;
            *pLits++ = 2 * OutVar + 1; 
            pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
        }
        pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover);
    }
    Vec_IntFree( vSopTemp );

    // write the output literals
    Aig_ManForEachCo( p->pManAig, pObj, i )
    {
        // remember the starting clause
        pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses;
        pCnf->pObj2Count[pObj->Id] = 2;
        // get variables
        OutVar = Aig_ObjFanin0(pObj)->Id;
        PoVar = pObj->Id;
        // first clause
        *pClas++ = pLits;
        *pLits++ = 2 * PoVar; 
        *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); 
        // second clause
        *pClas++ = pLits;
        *pLits++ = 2 * PoVar + 1; 
        *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
    }
 
    // remember the starting clause
    pCnf->pObj2Clause[Aig_ManConst1(p->pManAig)->Id] = pClas - pCnf->pClauses;
    pCnf->pObj2Count[Aig_ManConst1(p->pManAig)->Id] = 1;
    // write the constant literal
    OutVar = Aig_ManConst1(p->pManAig)->Id;
    *pClas++ = pLits;
    *pLits++ = 2 * OutVar; 

    // verify that the correct number of literals and clauses was written
    assert( pLits - pCnf->pClauses[0] == nLiterals );
    assert( pClas - pCnf->pClauses == nClauses );
//Cnf_DataPrint( pCnf, 1 );
    return pCnf;
}


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

  Synopsis    [Derives a simple CNF for the AIG.]

  Description [The last argument lists the number of last outputs
  of the manager, which will not be converted into clauses. 
  New variables will be introduced for these outputs.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
{
    Aig_Obj_t * pObj;
    Cnf_Dat_t * pCnf;
    int OutVar, PoVar, pVars[32], * pLits, ** pClas;
    int i, nLiterals, nClauses, Number;

    // count the number of literals and clauses
    nLiterals = 1 + 7 * Aig_ManNodeNum(p) + Aig_ManCoNum( p ) + 3 * nOutputs;
    nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManCoNum( p ) + nOutputs;

    // allocate CNF
    pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
    memset( pCnf, 0, sizeof(Cnf_Dat_t) );
    pCnf->pMan = p;
    pCnf->nLiterals = nLiterals;
    pCnf->nClauses = nClauses;
    pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
    pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
    pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;

    // create room for variable numbers
    pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p) );
//    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
    for ( i = 0; i < Aig_ManObjNumMax(p); i++ )
        pCnf->pVarNums[i] = -1;
    // assign variables to the last (nOutputs) POs
    Number = 1;
    if ( nOutputs )
    {
//        assert( nOutputs == Aig_ManRegNum(p) );
//        Aig_ManForEachLiSeq( p, pObj, i )
//            pCnf->pVarNums[pObj->Id] = Number++;
        Aig_ManForEachCo( p, pObj, i )
            pCnf->pVarNums[pObj->Id] = Number++;
    }
    // assign variables to the internal nodes
    Aig_ManForEachNode( p, pObj, i )
        pCnf->pVarNums[pObj->Id] = Number++;
    // assign variables to the PIs and constant node
    Aig_ManForEachCi( p, pObj, i )
        pCnf->pVarNums[pObj->Id] = Number++;
    pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
    pCnf->nVars = Number;
/*
    // print CNF numbers
    printf( "SAT numbers of each node:\n" );
    Aig_ManForEachObj( p, pObj, i )
        printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] );
    printf( "\n" );
*/
    // assign the clauses
    pLits = pCnf->pClauses[0];
    pClas = pCnf->pClauses;
    Aig_ManForEachNode( p, pObj, i )
    {
        OutVar   = pCnf->pVarNums[ pObj->Id ];
        pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
        pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];

        // positive phase
        *pClas++ = pLits;
        *pLits++ = 2 * OutVar; 
        *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj); 
        *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj); 
        // negative phase
        *pClas++ = pLits;
        *pLits++ = 2 * OutVar + 1; 
        *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj); 
        *pClas++ = pLits;
        *pLits++ = 2 * OutVar + 1; 
        *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj); 
    }
 
    // write the constant literal
    OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
    assert( OutVar <= Aig_ManObjNumMax(p) );
    *pClas++ = pLits;
    *pLits++ = 2 * OutVar;  

    // write the output literals
    Aig_ManForEachCo( p, pObj, i )
    {
        OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
        if ( i < Aig_ManCoNum(p) - nOutputs )
        {
            *pClas++ = pLits;
            *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
        }
        else
        {
            PoVar  = pCnf->pVarNums[ pObj->Id ];
            // first clause
            *pClas++ = pLits;
            *pLits++ = 2 * PoVar; 
            *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); 
            // second clause
            *pClas++ = pLits;
            *pLits++ = 2 * PoVar + 1; 
            *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
        }
    }

    // verify that the correct number of literals and clauses was written
    assert( pLits - pCnf->pClauses[0] == nLiterals );
    assert( pClas - pCnf->pClauses == nClauses );
    return pCnf;
}

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

  Synopsis    [Derives a simple CNF for backward retiming computation.]

  Description [The last argument shows the number of last outputs
  of the manager, which will not be converted into clauses. 
  New variables will be introduced for these outputs.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p )
{
    Aig_Obj_t * pObj;
    Cnf_Dat_t * pCnf;
    int OutVar, PoVar, pVars[32], * pLits, ** pClas;
    int i, nLiterals, nClauses, Number;

    // count the number of literals and clauses
    nLiterals = 1 + 7 * Aig_ManNodeNum(p) + 5 * Aig_ManCoNum(p);
    nClauses = 1 + 3 * Aig_ManNodeNum(p) + 3 * Aig_ManCoNum(p);

    // allocate CNF
    pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
    memset( pCnf, 0, sizeof(Cnf_Dat_t) );
    pCnf->pMan = p;
    pCnf->nLiterals = nLiterals;
    pCnf->nClauses = nClauses;
    pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
    pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
    pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;

    // create room for variable numbers
    pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p) );
//    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
    for ( i = 0; i < Aig_ManObjNumMax(p); i++ )
        pCnf->pVarNums[i] = -1;
    // assign variables to the last (nOutputs) POs
    Number = 1;
    Aig_ManForEachCo( p, pObj, i )
        pCnf->pVarNums[pObj->Id] = Number++;
    // assign variables to the internal nodes
    Aig_ManForEachNode( p, pObj, i )
        pCnf->pVarNums[pObj->Id] = Number++;
    // assign variables to the PIs and constant node
    Aig_ManForEachCi( p, pObj, i )
        pCnf->pVarNums[pObj->Id] = Number++;
    pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
    pCnf->nVars = Number;
    // assign the clauses
    pLits = pCnf->pClauses[0];
    pClas = pCnf->pClauses;
    Aig_ManForEachNode( p, pObj, i )
    {
        OutVar   = pCnf->pVarNums[ pObj->Id ];
        pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
        pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];

        // positive phase
        *pClas++ = pLits;
        *pLits++ = 2 * OutVar; 
        *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj); 
        *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj); 
        // negative phase
        *pClas++ = pLits;
        *pLits++ = 2 * OutVar + 1; 
        *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj); 
        *pClas++ = pLits;
        *pLits++ = 2 * OutVar + 1; 
        *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj); 
    }
 
    // write the constant literal
    OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
    assert( OutVar <= Aig_ManObjNumMax(p) );
    *pClas++ = pLits;
    *pLits++ = 2 * OutVar; 

    // write the output literals
    Aig_ManForEachCo( p, pObj, i )
    {
        OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
        PoVar  = pCnf->pVarNums[ pObj->Id ];
        // first clause
        *pClas++ = pLits;
        *pLits++ = 2 * PoVar; 
        *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); 
        // second clause
        *pClas++ = pLits;
        *pLits++ = 2 * PoVar + 1; 
        *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
        // final clause (init-state is always 0 -> set the output to 0)
        *pClas++ = pLits;
        *pLits++ = 2 * PoVar + 1; 
    }

    // verify that the correct number of literals and clauses was written
    assert( pLits - pCnf->pClauses[0] == nLiterals );
    assert( pClas - pCnf->pClauses == nClauses );
    return pCnf;
}

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


ABC_NAMESPACE_IMPL_END