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

  FileName    [saigOutDec.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Sequential AIG package.]

  Synopsis    [Output cone decomposition.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "saig.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [Performs decomposition of the property output.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Saig_ManFindPrimes( Aig_Man_t * pAig, int nLits, int fVerbose )
{
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
    Aig_Obj_t * pObj0, * pObj1, * pRoot, * pMiter;
    Vec_Ptr_t * vPrimes, * vNodes;
    Vec_Int_t * vCube, * vMarks;
    int i0, i1, m, RetValue, Lits[10];
    int fCompl0, fCompl1, nNodes1, nNodes2;
    assert( nLits == 1 || nLits == 2 );
    assert( nLits < 10 );

    // create SAT solver
    pCnf = Cnf_DeriveSimple( pAig, Aig_ManCoNum(pAig) ); 
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );

    // collect nodes in the property output cone
    pMiter = Aig_ManCo( pAig, 0 );
    pRoot  = Aig_ObjFanin0( pMiter );
    vNodes = Aig_ManDfsNodes( pAig, &pRoot, 1 );
    // sort nodes by level and remove the last few
 
    // try single nodes
    vPrimes = Vec_PtrAlloc( 100 );
    // create assumptions
    vMarks = Vec_IntStart( Vec_PtrSize(vNodes) );
    Lits[0] = toLitCond( pCnf->pVarNums[Aig_ObjId(pMiter)], 1 );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj0, i0 )
    if ( pObj0 != pRoot )
    {
        // create assumptions
        Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj0)], pObj0->fPhase );
        // solve the problem
        RetValue = sat_solver_solve( pSat, Lits, Lits+2, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        if ( RetValue == l_False )
        {
            vCube = Vec_IntAlloc( 1 );
            Vec_IntPush( vCube, toLitCond(Aig_ObjId(pObj0), pObj0->fPhase) );
            Vec_PtrPush( vPrimes, vCube );
            if ( fVerbose )
            printf( "Adding prime %d%c\n", Aig_ObjId(pObj0),  pObj0->fPhase?'-':'+' );
            Vec_IntWriteEntry( vMarks, i0, 1 );
        }
    }
    nNodes1 = Vec_PtrSize(vPrimes);
    if ( nLits > 1 )
    {
        // try adding second literal
        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj0, i0 )
        if ( pObj0 != pRoot )
        Vec_PtrForEachEntryStart( Aig_Obj_t *, vNodes, pObj1, i1, i0+1 )
        if ( pObj1 != pRoot )
        {
            if ( Vec_IntEntry(vMarks,i0) || Vec_IntEntry(vMarks,i1) )
                continue;
            for ( m = 0; m < 3; m++ )
            {
                fCompl0 =  m & 1;
                fCompl1 = (m >> 1) & 1;
                // create assumptions
                Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj0)], fCompl0 ^ pObj0->fPhase );
                Lits[2] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj1)], fCompl1 ^ pObj1->fPhase );
                // solve the problem
                RetValue = sat_solver_solve( pSat, Lits, Lits+3, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
                if ( RetValue == l_False )
                {
                    vCube = Vec_IntAlloc( 2 );
                    Vec_IntPush( vCube, toLitCond(Aig_ObjId(pObj0), fCompl0 ^ pObj0->fPhase) );
                    Vec_IntPush( vCube, toLitCond(Aig_ObjId(pObj1), fCompl1 ^ pObj1->fPhase) );
                    Vec_PtrPush( vPrimes, vCube );
                    if ( fVerbose )
                    printf( "Adding prime %d%c %d%c\n", 
                        Aig_ObjId(pObj0), (fCompl0 ^ pObj0->fPhase)?'-':'+', 
                        Aig_ObjId(pObj1), (fCompl1 ^ pObj1->fPhase)?'-':'+' );
                    break;
                }
            }
        }
    }
    nNodes2 = Vec_PtrSize(vPrimes) - nNodes1;

    printf( "Property cone size = %6d    1-lit primes = %5d    2-lit primes = %5d\n", 
        Vec_PtrSize(vNodes), nNodes1, nNodes2 );

    // clean up
    sat_solver_delete( pSat );
    Cnf_DataFree( pCnf );
    Vec_PtrFree( vNodes );
    Vec_IntFree( vMarks );
    return vPrimes;
}

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

  Synopsis    [Performs decomposition of the property output.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManDecPropertyOutput( Aig_Man_t * pAig, int nLits, int fVerbose )
{
    Aig_Man_t * pAigNew = NULL;
    Aig_Obj_t * pObj, * pMiter;
    Vec_Ptr_t * vPrimes;
    Vec_Int_t * vCube;
    int i, k, Lit;

    // compute primes of the comb output function
    vPrimes = Saig_ManFindPrimes( pAig, nLits, fVerbose );

    // start the new manager
    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    pAigNew->nConstrs = pAig->nConstrs;
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pAigNew );
    // add internal nodes of this frame
    Aig_ManForEachNode( pAig, pObj, i )
        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // create original POs of the circuit
    Saig_ManForEachPo( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    // create prime POs of the circuit
    if ( vPrimes )
    Vec_PtrForEachEntry( Vec_Int_t *, vPrimes, vCube, k )
    {
        pMiter = Aig_ManConst1( pAigNew );
        Vec_IntForEachEntry( vCube, Lit, i )
        {
            pObj = Aig_NotCond( Aig_ObjCopy(Aig_ManObj(pAig, Abc_Lit2Var(Lit))), Abc_LitIsCompl(Lit) );
            pMiter = Aig_And( pAigNew, pMiter, pObj );
        }
        Aig_ObjCreateCo( pAigNew, pMiter );
    }
    // transfer to register outputs
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    Aig_ManCleanup( pAigNew );
    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );

    Vec_VecFreeP( (Vec_Vec_t **)&vPrimes );
    return pAigNew;
}


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


ABC_NAMESPACE_IMPL_END