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

  FileName    [abcQbf.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

  Synopsis    [Implementation of a simple QBF solver.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "base/abc/abc.h"
#include "sat/cnf/cnf.h"

ABC_NAMESPACE_IMPL_START


/*
   Implementation of a simple QBF solver along the lines of
   A. Solar-Lezama, L. Tancau, R. Bodik, V. Saraswat, and S. Seshia, 
   "Combinatorial sketching for finite programs", 12th International 
   Conference on Architectural Support for Programming Languages and 
   Operating Systems (ASPLOS 2006), San Jose, CA, October 2006.
*/

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

static void Abc_NtkModelToVector( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
static void Abc_NtkVectorClearPars( Vec_Int_t * vPiValues, int nPars );
static void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars );
static void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars );
static void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars );

extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );

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

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

  Synopsis    [Solve the QBF problem EpAx[M(p,x)].]

  Description [Variables p go first, followed by variable x.
  The number of parameters is nPars. The miter is in pNtk.
  The miter expresses EQUALITY of the implementation and spec.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fDumpCnf, int fVerbose )
{
    Abc_Ntk_t * pNtkVer, * pNtkSyn, * pNtkSyn2, * pNtkTemp;
    Vec_Int_t * vPiValues;
    abctime clkTotal = Abc_Clock(), clkS, clkV;
    int nIters, nInputs, RetValue, fFound = 0;

    assert( Abc_NtkIsStrash(pNtk) );
    assert( Abc_NtkIsComb(pNtk) );
    assert( Abc_NtkPoNum(pNtk) == 1 );
    assert( nPars > 0 && nPars < Abc_NtkPiNum(pNtk) );
//    assert( Abc_NtkPiNum(pNtk)-nPars < 32 );
    nInputs = Abc_NtkPiNum(pNtk) - nPars;

    if ( fDumpCnf )
    {
        // original problem: \exists p \forall x \exists y.  M(p,x,y)
        // negated problem:  \forall p \exists x \exists y. !M(p,x,y)
        extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
        Aig_Man_t * pMan = Abc_NtkToDar( pNtk, 0, 0 );
        Cnf_Dat_t * pCnf = Cnf_Derive( pMan, 0 );
        Vec_Int_t * vVarMap, * vForAlls, * vExists;
        Aig_Obj_t * pObj;
        char * pFileName;
        int i, Entry;
        // create var map
        vVarMap = Vec_IntStart( pCnf->nVars );
        Aig_ManForEachCi( pMan, pObj, i )
            if ( i < nPars )
                Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Aig_ObjId(pObj)], 1 );
        // create various maps
        vForAlls = Vec_IntAlloc( nPars );
        vExists = Vec_IntAlloc( Abc_NtkPiNum(pNtk) - nPars );
        Vec_IntForEachEntry( vVarMap, Entry, i )
            if ( Entry )
                Vec_IntPush( vForAlls, i );
            else
                Vec_IntPush( vExists, i );
        // generate CNF
        pFileName = Extra_FileNameGenericAppend( pNtk->pSpec, ".qdimacs" );
        Cnf_DataWriteIntoFile( pCnf, pFileName, 0, vForAlls, vExists );
        Aig_ManStop( pMan );
        Cnf_DataFree( pCnf );
        Vec_IntFree( vForAlls );
        Vec_IntFree( vExists );
        Vec_IntFree( vVarMap );
        printf( "The 2QBF formula was written into file \"%s\".\n", pFileName );
        return;
    }

    // initialize the synthesized network with 0000-combination
    vPiValues = Vec_IntStart( Abc_NtkPiNum(pNtk) );

    // create random init value
    {
    int i;
    srand( time(NULL) );
    for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
        Vec_IntWriteEntry( vPiValues, i, rand() & 1 );
    }

    Abc_NtkVectorClearPars( vPiValues, nPars );
    pNtkSyn = Abc_NtkMiterCofactor( pNtk, vPiValues );
    if ( fVerbose )
    {
        printf( "Iter %2d : ", 0 );
        printf( "AIG = %6d  ", Abc_NtkNodeNum(pNtkSyn) );
        Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
        printf( "\n" );
    }

    // iteratively solve
    for ( nIters = 0; nIters < nItersMax; nIters++ )
    {
        // solve the synthesis instance
clkS = Abc_Clock();
//        RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
        RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
clkS = Abc_Clock() - clkS;
        if ( RetValue == 0 )
            Abc_NtkModelToVector( pNtkSyn, vPiValues );
        if ( RetValue == 1 )
        {
            break;
        }
        if ( RetValue == -1 )
        {
            printf( "Synthesis timed out.\n" );
            break;
        }
        // there is a counter-example

        // construct the verification instance
        Abc_NtkVectorClearVars( pNtk, vPiValues, nPars );
        pNtkVer = Abc_NtkMiterCofactor( pNtk, vPiValues );
        // complement the output
        Abc_ObjXorFaninC( Abc_NtkPo(pNtkVer,0), 0 );

        // solve the verification instance
clkV = Abc_Clock();
        RetValue = Abc_NtkMiterSat( pNtkVer, 0, 0, 0, NULL, NULL );
clkV = Abc_Clock() - clkV;
        if ( RetValue == 0 )
            Abc_NtkModelToVector( pNtkVer, vPiValues );
        Abc_NtkDelete( pNtkVer );
        if ( RetValue == 1 )
        {
            fFound = 1;
            break;
        }
        if ( RetValue == -1 )
        {
            printf( "Verification timed out.\n" );
            break;
        }
        // there is a counter-example

        // create a new synthesis network
        Abc_NtkVectorClearPars( vPiValues, nPars );
        pNtkSyn2 = Abc_NtkMiterCofactor( pNtk, vPiValues );
        // add to the synthesis instance
        pNtkSyn = Abc_NtkMiterAnd( pNtkTemp = pNtkSyn, pNtkSyn2, 0, 0 );
        Abc_NtkDelete( pNtkSyn2 );
        Abc_NtkDelete( pNtkTemp );

        if ( fVerbose )
        {
            printf( "Iter %2d : ", nIters+1 );
            printf( "AIG = %6d  ", Abc_NtkNodeNum(pNtkSyn) );
            Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
            printf( "  " );
            ABC_PRT( "Syn", clkS );
//            ABC_PRT( "Ver", clkV );
        }
        if ( nIters+1 == nItersMax )
            break;
    }
    Abc_NtkDelete( pNtkSyn );
    // report the results
    if ( fFound )
    {
        printf( "Parameters: " );
        Abc_NtkVectorPrintPars( vPiValues, nPars );
        printf( "\n" );
        printf( "Solved after %d interations.  ", nIters );
    }
    else if ( nIters == nItersMax )
        printf( "Unsolved after %d interations.  ", nIters );
    else if ( nIters == nItersMax )
        printf( "Quit after %d interatios.  ", nItersMax );
    else
        printf( "Implementation does not exist.  " );
    ABC_PRT( "Total runtime", Abc_Clock() - clkTotal );
    Vec_IntFree( vPiValues );
}


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

  Synopsis    [Translates model into the vector of values.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkModelToVector( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
{
    int * pModel, i;
    pModel = pNtk->pModel;
    for ( i = 0; i < Abc_NtkPiNum(pNtk); i++ )
        Vec_IntWriteEntry( vPiValues, i, pModel[i] );
}

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

  Synopsis    [Clears parameters.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkVectorClearPars( Vec_Int_t * vPiValues, int nPars )
{
    int i;
    for ( i = 0; i < nPars; i++ )
        Vec_IntWriteEntry( vPiValues, i, -1 );
}

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

  Synopsis    [Clears variables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars )
{
    int i;
    for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
        Vec_IntWriteEntry( vPiValues, i, -1 );
}

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

  Synopsis    [Clears variables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars )
{
    int i;
    for ( i = 0; i < nPars; i++ )
        printf( "%d", Vec_IntEntry(vPiValues,i) );
}

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

  Synopsis    [Clears variables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars )
{
    int i;
    for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
        printf( "%d", Vec_IntEntry(vPiValues,i) );
}

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


ABC_NAMESPACE_IMPL_END