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

  FileName    [intM114p.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Interpolation engine.]

  Synopsis    [Intepolation using interfaced to MiniSat-1.14p.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 24, 2008.]

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

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

#include "intInt.h"
#include "sat/psat/m114p.h"

#ifdef ABC_USE_LIBRARIES

ABC_NAMESPACE_IMPL_START

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

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

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

  Synopsis    [Returns the SAT solver for one interpolation run.]

  Description [pInter is the previous interpolant. pAig is one time frame.
  pFrames is the unrolled time frames.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
M114p_Solver_t Inter_ManDeriveSatSolverM114p( 
    Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter, 
    Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig, 
    Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, 
    Vec_Int_t ** pvMapRoots, Vec_Int_t ** pvMapVars )
{
    M114p_Solver_t pSat;
    Aig_Obj_t * pObj, * pObj2;
    int i, Lits[2];

    // sanity checks
    assert( Aig_ManRegNum(pInter) == 0 );
    assert( Aig_ManRegNum(pAig) > 0 );
    assert( Aig_ManRegNum(pFrames) == 0 );
    assert( Aig_ManCoNum(pInter) == 1 );
    assert( Aig_ManCoNum(pFrames) == 1 );
    assert( Aig_ManCiNum(pInter) == Aig_ManRegNum(pAig) );
//    assert( (Aig_ManCiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );

    // prepare CNFs
    Cnf_DataLift( pCnfAig,   pCnfFrames->nVars );
    Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );

    *pvMapRoots = Vec_IntAlloc( 10000 );
    *pvMapVars = Vec_IntAlloc( 0 );
    Vec_IntFill( *pvMapVars, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars, -1 );
    for ( i = 0; i < pCnfFrames->nVars; i++ )
        Vec_IntWriteEntry( *pvMapVars, i, -2 );

    // start the solver
    pSat = M114p_SolverNew( 1 );
    M114p_SolverSetVarNum( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );

    // add clauses of A
    // interpolant
    for ( i = 0; i < pCnfInter->nClauses; i++ )
    {
        Vec_IntPush( *pvMapRoots, 0 );
        if ( !M114p_SolverAddClause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) )
            assert( 0 );
    }
    // connector clauses
    Aig_ManForEachCi( pInter, pObj, i )
    {
        pObj2 = Saig_ManLo( pAig, i );
        Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
        Vec_IntPush( *pvMapRoots, 0 );
        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
            assert( 0 );
        Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
        Vec_IntPush( *pvMapRoots, 0 );
        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
            assert( 0 );
    }
    // one timeframe
    for ( i = 0; i < pCnfAig->nClauses; i++ )
    {
        Vec_IntPush( *pvMapRoots, 0 );
        if ( !M114p_SolverAddClause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
            assert( 0 );
    }
    // connector clauses
    Aig_ManForEachCi( pFrames, pObj, i )
    { 
        if ( i == Aig_ManRegNum(pAig) )
            break;
//        Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
        Vec_IntWriteEntry( *pvMapVars, pCnfFrames->pVarNums[pObj->Id], i );

        pObj2 = Saig_ManLi( pAig, i );
        Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
        Vec_IntPush( *pvMapRoots, 0 );
        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
            assert( 0 );
        Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
        Vec_IntPush( *pvMapRoots, 0 );
        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
            assert( 0 );
    }
    // add clauses of B
    for ( i = 0; i < pCnfFrames->nClauses; i++ )
    {
        Vec_IntPush( *pvMapRoots, 1 );
        if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
        {
//            assert( 0 );
            break;
        }
    }
    // return clauses to the original state
    Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
    Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
    return pSat;
}


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

  Synopsis    [Performs one resolution step.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Inter_ManResolveM114p( Vec_Int_t * vResolvent, int * pLits, int nLits, int iVar )
{
    int i, k, iLit = -1, fFound = 0;
    // find the variable in the clause
    for ( i = 0; i < vResolvent->nSize; i++ )
        if ( lit_var(vResolvent->pArray[i]) == iVar )
        {
            iLit = vResolvent->pArray[i];
            vResolvent->pArray[i] = vResolvent->pArray[--vResolvent->nSize];
            break;
        }
    assert( iLit != -1 );
    // add other variables
    for ( i = 0; i < nLits; i++ )
    {
        if ( lit_var(pLits[i]) == iVar )
        {
            assert( iLit == lit_neg(pLits[i]) );
            fFound = 1;
            continue;
        }
        // check if this literal appears
        for ( k = 0; k < vResolvent->nSize; k++ )
            if ( vResolvent->pArray[k] == pLits[i] )
                break;
        if ( k < vResolvent->nSize )
            continue;
        // add this literal
        Vec_IntPush( vResolvent, pLits[i] );
    }
    assert( fFound );
    return 1;
}

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

  Synopsis    [Computes interpolant using MiniSat-1.14p.]

  Description [Assumes that the solver returned UNSAT and proof
  logging was enabled. Array vMapRoots maps number of each root clause 
  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
  where <num> is the var's 0-based number in the ordering of C variables.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Inter_ManInterpolateM114pPudlak( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
{
    Aig_Man_t * p;
    Aig_Obj_t * pInter, * pInter2, * pVar;
    Vec_Ptr_t * vInters;
    Vec_Int_t * vLiterals, * vClauses, * vResolvent;
    int * pLitsNext, nLitsNext, nOffset, iLit;
    int * pLits, * pClauses, * pVars;
    int nLits, nVars, i, k, v, iVar;
    assert( M114p_SolverProofIsReady(s) );
    vInters = Vec_PtrAlloc( 1000 );

    vLiterals = Vec_IntAlloc( 10000 );
    vClauses = Vec_IntAlloc( 1000 );
    vResolvent = Vec_IntAlloc( 100 );

    // create elementary variables
    p = Aig_ManStart( 10000 );
    Vec_IntForEachEntry( vMapVars, iVar, i )
        if ( iVar >= 0 )
            Aig_IthVar(p, iVar);
    // process root clauses
    M114p_SolverForEachRoot( s, &pLits, nLits, i )
    {
        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
            pInter = Aig_ManConst1(p);
        else // clause of A
            pInter = Aig_ManConst0(p);
        Vec_PtrPush( vInters, pInter );

        // save the root clause
        Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
        Vec_IntPush( vLiterals, nLits );
        for ( v = 0; v < nLits; v++ )
            Vec_IntPush( vLiterals, pLits[v] );
    }
    assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );

    // process learned clauses
    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
    {
        pInter = Vec_PtrEntry( vInters, pClauses[0] );

        // initialize the resolvent
        nOffset = Vec_IntEntry( vClauses, pClauses[0] );
        nLitsNext = Vec_IntEntry( vLiterals, nOffset );
        pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
        Vec_IntClear( vResolvent );
        for ( v = 0; v < nLitsNext; v++ )
            Vec_IntPush( vResolvent, pLitsNext[v] );

        for ( k = 0; k < nVars; k++ )
        {
            iVar = Vec_IntEntry( vMapVars, pVars[k] );
            pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );

            // resolve it with the next clause
            nOffset = Vec_IntEntry( vClauses, pClauses[k+1] );
            nLitsNext = Vec_IntEntry( vLiterals, nOffset );
            pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
            Inter_ManResolveM114p( vResolvent, pLitsNext, nLitsNext, pVars[k] );

            if ( iVar == -1 ) // var of A
                pInter = Aig_Or( p, pInter, pInter2 );
            else if ( iVar == -2 ) // var of B
                pInter = Aig_And( p, pInter, pInter2 );
            else // var of C
            {
                // check polarity of the pivot variable in the clause
                for ( v = 0; v < nLitsNext; v++ )
                    if ( lit_var(pLitsNext[v]) == pVars[k] )
                        break;
                assert( v < nLitsNext );
                pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) );
                pInter = Aig_Mux( p, pVar, pInter, pInter2 );
            }
        }
        Vec_PtrPush( vInters, pInter );

        // store the resulting clause
        Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
        Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) );
        Vec_IntForEachEntry( vResolvent, iLit, v )
            Vec_IntPush( vLiterals, iLit );
    }
    assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
    assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause
    Vec_PtrFree( vInters );
    Vec_IntFree( vLiterals );
    Vec_IntFree( vClauses );
    Vec_IntFree( vResolvent );
    Aig_ObjCreateCo( p, pInter );
    Aig_ManCleanup( p );
    return p;
}


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

  Synopsis    [Computes interpolant using MiniSat-1.14p.]

  Description [Assumes that the solver returned UNSAT and proof
  logging was enabled. Array vMapRoots maps number of each root clause 
  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
  where <num> is the var's 0-based number in the ordering of C variables.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
{
    Aig_Man_t * p;
    Aig_Obj_t * pInter, * pInter2, * pVar;
    Vec_Ptr_t * vInters;
    int * pLits, * pClauses, * pVars;
    int nLits, nVars, i, k, iVar;
    int nClauses;

    nClauses = M114p_SolverProofClauseNum(s);

    assert( M114p_SolverProofIsReady(s) );

    vInters = Vec_PtrAlloc( 1000 );
    // process root clauses
    p = Aig_ManStart( 10000 );
    M114p_SolverForEachRoot( s, &pLits, nLits, i )
    {
        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
            pInter = Aig_ManConst1(p);
        else // clause of A
        {
            pInter = Aig_ManConst0(p);
            for ( k = 0; k < nLits; k++ )
            {
                iVar = Vec_IntEntry( vMapVars, lit_var(pLits[k]) );
                if ( iVar < 0 ) // var of A or B
                    continue;
                // this is a variable of C
                pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLits[k]) );
                pInter = Aig_Or( p, pInter, pVar );
            }
        }
        Vec_PtrPush( vInters, pInter );
    } 
//    assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );

    // process learned clauses
    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
    {
        pInter = Vec_PtrEntry( vInters, pClauses[0] );
        for ( k = 0; k < nVars; k++ )
        {
            iVar = Vec_IntEntry( vMapVars, pVars[k] );
            pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
            if ( iVar == -1 ) // var of A
                pInter = Aig_Or( p, pInter, pInter2 );
            else // var of B or C
                pInter = Aig_And( p, pInter, pInter2 );
        }
        Vec_PtrPush( vInters, pInter );
    }

    assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
    Vec_PtrFree( vInters );
    Aig_ObjCreateCo( p, pInter );
    Aig_ManCleanup( p );
    assert( Aig_ManCheck(p) );
    return p;
}


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

  Synopsis    [Performs one SAT run with interpolation.]

  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther )
{
    M114p_Solver_t pSat;
    Vec_Int_t * vMapRoots, * vMapVars;
    clock_t clk;
    int status, RetValue;
    assert( p->pInterNew == NULL );
    // derive the SAT solver
    pSat = Inter_ManDeriveSatSolverM114p( p->pInter, p->pCnfInter, 
        p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, 
        &vMapRoots, &vMapVars );
    // solve the problem
clk = clock();
    status = M114p_SolverSolve( pSat, NULL, NULL, 0 );
    p->nConfCur = M114p_SolverGetConflictNum( pSat );
p->timeSat += clock() - clk;
    if ( status == 0 )
    {
        RetValue = 1;
//        Inter_ManpInterpolateM114Report( pSat, vMapRoots, vMapVars );

clk = clock();
        if ( fUsePudlak )
            p->pInterNew = Inter_ManInterpolateM114pPudlak( pSat, vMapRoots, vMapVars );
        else
            p->pInterNew = Inter_ManpInterpolateM114( pSat, vMapRoots, vMapVars );
p->timeInt += clock() - clk;
    }
    else if ( status == 1 )
    {
        RetValue = 0;
    }
    else
    {
        RetValue = -1;
    }
    M114p_SolverDelete( pSat );
    Vec_IntFree( vMapRoots );
    Vec_IntFree( vMapVars );
    return RetValue;
}

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

ABC_NAMESPACE_IMPL_END

#endif