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

  FileName    [resSat.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Resynthesis package.]

  Synopsis    [Interface with the SAT solver.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - January 15, 2007.]

  Revision    [$Id: resSat.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]

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

#include "base/abc/abc.h"
#include "resInt.h"
#include "aig/hop/hop.h"
#include "sat/bsat/satSolver.h"

ABC_NAMESPACE_IMPL_START


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

extern int Res_SatAddConst1( sat_solver * pSat, int iVar, int fCompl );
extern int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl );
extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 );

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

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

  Synopsis    [Loads AIG into the SAT solver for checking resubstitution.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
{
    void * pCnf = NULL;
    sat_solver * pSat;
    Vec_Ptr_t * vNodes;
    Abc_Obj_t * pObj;
    int i, nNodes, status;

    // make sure fanins contain POs of the AIG
    pObj = (Abc_Obj_t *)Vec_PtrEntry( vFanins, 0 );
    assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );

    // collect reachable nodes
    vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );

    // assign unique numbers to each node
    nNodes = 0;
    Abc_AigConst1(pAig)->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
    Abc_NtkForEachPi( pAig, pObj, i )
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
    Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i ) // useful POs
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;

    // start the solver
    pSat = sat_solver_new();
    sat_solver_store_alloc( pSat );

    // add clause for the constant node
    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
    // add clauses for AND gates
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
        Res_SatAddAnd( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
            (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
    Vec_PtrFree( vNodes );
    // add clauses for POs
    Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i )
        Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
            (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
    // add trivial clauses
    pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 0);
    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // care-set
    pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 1);
    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // on-set

    // bookmark the clauses of A
    sat_solver_store_mark_clauses_a( pSat );

    // duplicate the clauses
    pObj = (Abc_Obj_t *)Vec_PtrEntry(vFanins, 1);
    Sat_SolverDoubleClauses( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy );
    // add the equality constraints
    Vec_PtrForEachEntryStart( Abc_Obj_t *, vFanins, pObj, i, 2 )
        Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, ((int)(ABC_PTRUINT_T)pObj->pCopy) + nNodes, 0 );

    // bookmark the roots
    sat_solver_store_mark_roots( pSat );

    // solve the problem
    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( status == l_False )
    {
        pCnf = sat_solver_store_release( pSat );
//        printf( "unsat\n" );
    }
    else if ( status == l_True )
    {
//        printf( "sat\n" );
    }
    else
    {
//        printf( "undef\n" );
    }
    sat_solver_delete( pSat );
    return pCnf;
}

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

  Synopsis    [Loads AIG into the SAT solver for constrained simulation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, int fOnSet )
{
    sat_solver * pSat;
    Vec_Ptr_t * vFanins;
    Vec_Ptr_t * vNodes;
    Abc_Obj_t * pObj;
    int i, nNodes;

    // start the array
    vFanins = Vec_PtrAlloc( 2 );
    pObj = Abc_NtkPo( pAig, 0 );
    Vec_PtrPush( vFanins, pObj );
    pObj = Abc_NtkPo( pAig, 1 );
    Vec_PtrPush( vFanins, pObj );

    // collect reachable nodes
    vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );

    // assign unique numbers to each node
    nNodes = 0;
    Abc_AigConst1(pAig)->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
    Abc_NtkForEachPi( pAig, pObj, i )
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;
    Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i ) // useful POs
        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)nNodes++;

    // start the solver
    pSat = sat_solver_new();

    // add clause for the constant node
    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
    // add clauses for AND gates
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
        Res_SatAddAnd( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
            (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
    Vec_PtrFree( vNodes );
    // add clauses for the first PO
    pObj = Abc_NtkPo( pAig, 0 );
    Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
        (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
    // add clauses for the second PO
    pObj = Abc_NtkPo( pAig, 1 );
    Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
        (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );

    // add trivial clauses
    pObj = Abc_NtkPo( pAig, 0 );
    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // care-set

    pObj = Abc_NtkPo( pAig, 1 );
    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, !fOnSet ); // on-set

    Vec_PtrFree( vFanins );
    return pSat;
}

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

  Synopsis    [Loads AIG into the SAT solver for constrained simulation.]

  Description [Returns 1 if the required number of patterns are found. 
  Returns 0 if the solver ran out of time or proved a constant. 
  In the latter, case one of the flags, fConst0 or fConst1, are set to 1.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
{
    Vec_Int_t * vLits;
    Vec_Ptr_t * vPats;
    sat_solver * pSat;
    int RetValue = -1; // Suppress "might be used uninitialized"
    int i, k, value, status, Lit, Var, iPat;
    abctime clk = Abc_Clock();

//printf( "Looking for %s:  ", fOnSet? "onset " : "offset" );

    // decide what problem should be solved
    Lit = toLitCond( (int)(ABC_PTRUINT_T)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
    if ( fOnSet )
    {
        iPat = p->nPats1;
        vPats = p->vPats1;
    }
    else
    {
        iPat = p->nPats0;
        vPats = p->vPats0;
    }
    assert( iPat < nPatsLimit );

    // derive the SAT solver
    pSat = (sat_solver *)Res_SatSimulateConstr( p->pAig, fOnSet );
    pSat->fSkipSimplify = 1;
    status = sat_solver_simplify( pSat );
    if ( status == 0 )
    {
        if ( iPat == 0 )
        {
//            if ( fOnSet )
//                p->fConst0 = 1;
//            else
//                p->fConst1 = 1;
            RetValue = 0;
        }
        goto finish;
    }
 
    // enumerate through the SAT assignments
    RetValue = 1;
    vLits = Vec_IntAlloc( 32 );
    for ( k = iPat; k < nPatsLimit; k++ )
    {
        // solve with the assumption
//        status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
        if ( status == l_False )
        {
//printf( "Const %d\n", !fOnSet );
            if ( k == 0 )
            {
                if ( fOnSet )
                    p->fConst0 = 1;
                else
                    p->fConst1 = 1;
                RetValue = 0;
            }
            break;
        }
        else if ( status == l_True )
        {
            // save the pattern
            Vec_IntClear( vLits );
            for ( i = 0; i < p->nTruePis; i++ )
            {
                Var = (int)(ABC_PTRUINT_T)Abc_NtkPi(p->pAig,i)->pCopy;
//                value = (int)(pSat->model.ptr[Var] == l_True);
                value = sat_solver_var_value(pSat, Var);
                if ( value )
                    Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(vPats, i), k );
                Lit = toLitCond( Var, value );
                Vec_IntPush( vLits, Lit );
//                printf( "%d", value );
            }
//            printf( "\n" );

            status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
            if ( status == 0 )
            {
                k++;
                RetValue = 1; 
                break;
            }
        }
        else
        {
//printf( "Undecided\n" );
            if ( k == 0 )
                RetValue = 0;
            else
                RetValue = 1; 
            break;
        }
    }
    Vec_IntFree( vLits );
//printf( "Found %d patterns\n", k - iPat );

    // set the new number of patterns
    if ( fOnSet )
        p->nPats1 = k;
    else
        p->nPats0 = k;

finish:

    sat_solver_delete( pSat );
p->timeSat += Abc_Clock() - clk;
    return RetValue;
}


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

  Synopsis    [Asserts equality of the variable to a constant.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Res_SatAddConst1( sat_solver * pSat, int iVar, int fCompl )
{
    lit Lit = toLitCond( iVar, fCompl );
    if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
        return 0;
    return 1;
}

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

  Synopsis    [Asserts equality of two variables.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
{
    lit Lits[2];

    Lits[0] = toLitCond( iVar0, 0 );
    Lits[1] = toLitCond( iVar1, !fCompl );
    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
        return 0;

    Lits[0] = toLitCond( iVar0, 1 );
    Lits[1] = toLitCond( iVar1, fCompl );
    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
        return 0;

    return 1;
}

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

  Synopsis    [Adds constraints for the two-input AND-gate.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
{
    lit Lits[3];

    Lits[0] = toLitCond( iVar, 1 );
    Lits[1] = toLitCond( iVar0, fCompl0 );
    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
        return 0;

    Lits[0] = toLitCond( iVar, 1 );
    Lits[1] = toLitCond( iVar1, fCompl1 );
    if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
        return 0;

    Lits[0] = toLitCond( iVar, 0 );
    Lits[1] = toLitCond( iVar0, !fCompl0 );
    Lits[2] = toLitCond( iVar1, !fCompl1 );
    if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
        return 0;

    return 1;
}

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


ABC_NAMESPACE_IMPL_END