path: root/src/proof/pdr/pdrInv.c

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

  FileName    [pdrInv.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Property driven reachability.]

  Synopsis    [Invariant computation, printing, verification.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - November 20, 2010.]

  Revision    [$Id: pdrInv.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]

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

#include "pdrInt.h"
#include "base/abc/abc.h"      // for Abc_NtkCollectCioNames()
#include "base/main/main.h"    // for Abc_FrameReadGlobalFrame()
#include "aig/ioa/ioa.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
{
    Vec_Ptr_t * vVec;
    int i, ThisSize, Length, LengthStart;
    if ( Vec_PtrSize(p->vSolvers) < 2 )
    {
        Abc_Print(1, "Frame " );
        Abc_Print(1, "Clauses                                                     " );
        Abc_Print(1, "Max Queue " );
        Abc_Print(1, "Flops " );
        Abc_Print(1, "Cex      " );
        Abc_Print(1, "Time" );
        Abc_Print(1, "\n" );
        return;
    }
    if ( Abc_FrameIsBatchMode() && !fClose )
        return;
    // count the total length of the printout
    Length = 0;
    Vec_VecForEachLevel( p->vClauses, vVec, i )
        Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
    // determine the starting point
    LengthStart = Abc_MaxInt( 0, Length - 60 );
    Abc_Print( 1, "%3d :", Vec_PtrSize(p->vSolvers)-1 );
    ThisSize = 5;
    if ( LengthStart > 0 )
    {
        Abc_Print( 1, " ..." );
        ThisSize += 4;
    }
    Length = 0;
    Vec_VecForEachLevel( p->vClauses, vVec, i )
    {
        if ( Length < LengthStart )
        {
            Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
            continue;
        }
        Abc_Print( 1, " %d", Vec_PtrSize(vVec) );
        Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
        ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
    }
    for ( i = ThisSize; i < 70; i++ )
        Abc_Print( 1, " " );
    Abc_Print( 1, "%5d", p->nQueMax );
    Abc_Print( 1, "%6d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops );
    if ( p->pPars->fUseAbs )
    Abc_Print( 1, "%4d", p->nCexes );
    Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
    if ( p->pPars->fSolveAll )
        Abc_Print( 1, "  CEX =%4d", p->pPars->nFailOuts );
    if ( p->pPars->nTimeOutOne )
        Abc_Print( 1, "  T/O =%3d", p->pPars->nDropOuts );
    Abc_Print( 1, "%s", fClose ? "\n":"\r" );
    if ( fClose )
        p->nQueMax = 0, p->nCexes = 0;
    fflush( stdout );
}

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

  Synopsis    [Counts how many times each flop appears in the set of cubes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
{
    Vec_Int_t * vFlopCount;
    Pdr_Set_t * pCube;
    int i, n;
    vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) );
    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
    {
        if ( pCube->nRefs == -1 )
            continue;
        for ( n = 0; n < pCube->nLits; n++ )
        {
            assert( pCube->Lits[n] >= 0 && pCube->Lits[n] < 2*Aig_ManRegNum(p->pAig) );
            Vec_IntAddToEntry( vFlopCount, pCube->Lits[n] >> 1, 1 );
        }
    }
    return vFlopCount;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Pdr_ManFindInvariantStart( Pdr_Man_t * p )
{
    Vec_Ptr_t * vArrayK;
    int k, kMax = Vec_PtrSize(p->vSolvers)-1;
    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax+1 )
        if ( Vec_PtrSize(vArrayK) == 0 )
            return k;
//    return -1;
    // if there is no starting point (as in case of SAT or undecided), return the last frame
//    Abc_Print( 1, "The last timeframe contains %d clauses.\n", Vec_PtrSize(Vec_VecEntry(p->vClauses, kMax)) );
    return kMax;
}

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

  Synopsis    [Counts the number of variables used in the clauses.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Pdr_ManCollectCubes( Pdr_Man_t * p, int kStart )
{
    Vec_Ptr_t * vResult;
    Vec_Ptr_t * vArrayK;
    Pdr_Set_t * pSet;
    int i, j;
    vResult = Vec_PtrAlloc( 100 );
    Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, kStart )
        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pSet, j )
            Vec_PtrPush( vResult, pSet );
    return vResult;
}

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Pdr_ManCountFlopsInv( Pdr_Man_t * p )
{
    int kStart = Pdr_ManFindInvariantStart(p);
    Vec_Ptr_t *vCubes = Pdr_ManCollectCubes(p, kStart);
    Vec_Int_t * vInv = Pdr_ManCountFlops( p, vCubes );
    Vec_PtrFree(vCubes);
    return vInv;
}

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

  Synopsis    [Counts the number of variables used in the clauses.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Pdr_ManCountVariables( Pdr_Man_t * p, int kStart )
{
    Vec_Int_t * vFlopCounts;
    Vec_Ptr_t * vCubes;
    int i, Entry, Counter = 0;
    if ( p->vInfCubes == NULL )
        vCubes = Pdr_ManCollectCubes( p, kStart );
    else
        vCubes = Vec_PtrDup( p->vInfCubes );
    vFlopCounts = Pdr_ManCountFlops( p, vCubes );
    Vec_IntForEachEntry( vFlopCounts, Entry, i )
        Counter += (Entry > 0);
    Vec_IntFreeP( &vFlopCounts );
    Vec_PtrFree( vCubes );
    return Counter;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart )
{
    Vec_Ptr_t * vArrayK;
    Pdr_Set_t * pCube;
    int i, k, Counter = 0;
    Vec_VecForEachLevelStart( p->vClauses, vArrayK, k, kStart )
    {
        Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
        {
            Abc_Print( 1, "C=%4d. F=%4d ", Counter++, k );
            Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );  
            Abc_Print( 1, "\n" ); 
        }
    }
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     [] 

***********************************************************************/
void Pdr_SetPrintOne( Pdr_Set_t * p )
{
    int i;
    Abc_Print(1, "Clause: {" );
    for ( i = 0; i < p->nLits; i++ )
        Abc_Print(1, " %s%d", Abc_LitIsCompl(p->Lits[i])? "!":"", Abc_Lit2Var(p->Lits[i]) );
    Abc_Print(1, " }\n" );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     [] 

***********************************************************************/
Aig_Man_t * Pdr_ManDupAigWithClauses( Aig_Man_t * p, Vec_Ptr_t * vCubes )
{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj, * pObjNew, * pLit;
    Pdr_Set_t * pCube;
    int i, n;
    // create the new manager
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    // create the PIs
    Aig_ManCleanData( p );
    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
    Aig_ManForEachCi( p, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    // create outputs for each cube
    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
    {
//        Pdr_SetPrintOne( pCube );
        pObjNew = Aig_ManConst1(pNew);
        for ( n = 0; n < pCube->nLits; n++ )
        {
            assert( Abc_Lit2Var(pCube->Lits[n]) < Saig_ManRegNum(p) );
            pLit = Aig_NotCond( Aig_ManCi(pNew, Saig_ManPiNum(p) + Abc_Lit2Var(pCube->Lits[n])), Abc_LitIsCompl(pCube->Lits[n]) );
            pObjNew = Aig_And( pNew, pObjNew, pLit );
        }
        Aig_ObjCreateCo( pNew, pObjNew );
    }
    // duplicate internal nodes
    Aig_ManForEachNode( p, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // add the POs
    Saig_ManForEachLi( p, pObj, i )
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    Aig_ManCleanup( pNew );
    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
    // check the resulting network
    if ( !Aig_ManCheck(pNew) )
        Abc_Print(1, "Aig_ManDupSimple(): The check has failed.\n" );
    return pNew;
}
void Pdr_ManDumpAig( Aig_Man_t * p, Vec_Ptr_t * vCubes )
{
    Aig_Man_t * pNew = Pdr_ManDupAigWithClauses( p, vCubes );
    Ioa_WriteAiger( pNew, "aig_with_clauses.aig", 0, 0 );
    Aig_ManStop( pNew );
    Abc_Print(1, "Dumped modified AIG into file \"aig_with_clauses.aig\".\n" );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     [] 

***********************************************************************/
void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
{
    FILE * pFile;
    Vec_Int_t * vFlopCounts;
    Vec_Ptr_t * vCubes;
    Pdr_Set_t * pCube;
    char ** pNamesCi;
    int i, kStart, Count = 0;
    // create file
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        Abc_Print( 1, "Cannot open file \"%s\" for writing invariant.\n", pFileName );
        return;
    } 
    // collect cubes
    kStart = Pdr_ManFindInvariantStart( p );
    if ( fProved )
        vCubes = Pdr_ManCollectCubes( p, kStart );
    else
        vCubes = Vec_PtrDup( p->vInfCubes );
    Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
//    Pdr_ManDumpAig( p->pAig, vCubes );
    // count cubes
    Count = 0;
    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
    {
        if ( pCube->nRefs == -1 )
            continue;
        Count++;
    }
    // collect variable appearances
    vFlopCounts = p->pPars->fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
    // output the header
    if ( fProved )
        fprintf( pFile, "# Inductive invariant for \"%s\"\n", p->pAig->pName );
    else
        fprintf( pFile, "# Clauses of the last timeframe for \"%s\"\n", p->pAig->pName );
    fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() );
    fprintf( pFile, ".i %d\n", p->pPars->fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) );
    fprintf( pFile, ".o 1\n" );
    fprintf( pFile, ".p %d\n", Count );
    // output flop names
    pNamesCi = Abc_NtkCollectCioNames( Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ), 0 );
    if ( pNamesCi )
    {
        fprintf( pFile, ".ilb" );
        for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
            if ( !p->pPars->fUseSupp || Vec_IntEntry( vFlopCounts, i ) )
                fprintf( pFile, " %s", pNamesCi[Saig_ManPiNum(p->pAig) + i] );
        fprintf( pFile, "\n" );
        ABC_FREE( pNamesCi );
        fprintf( pFile, ".ob inv\n" );
    }
    // output cubes
    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
    {
        if ( pCube->nRefs == -1 )
            continue;
        Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );  
        fprintf( pFile, " 1\n" ); 
    }
    fprintf( pFile, ".e\n\n" );
    fclose( pFile );
    Vec_IntFreeP( &vFlopCounts );
    Vec_PtrFree( vCubes );
    if ( fProved )
        Abc_Print( 1, "Inductive invariant was written into file \"%s\".\n", pFileName );
    else
        Abc_Print( 1, "Clauses of the last timeframe were written into file \"%s\".\n", pFileName );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     [] 

***********************************************************************/
Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p )
{
    Vec_Str_t * vStr;
    Vec_Int_t * vFlopCounts;
    Vec_Ptr_t * vCubes;
    Pdr_Set_t * pCube;
    int i, kStart;
    vStr = Vec_StrAlloc( 1000 );
    // collect cubes
    kStart = Pdr_ManFindInvariantStart( p );
    if ( p->vInfCubes == NULL )
        vCubes = Pdr_ManCollectCubes( p, kStart );
    else
        vCubes = Vec_PtrDup( p->vInfCubes );
    Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
    // collect variable appearances
    vFlopCounts = p->pPars->fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
    // output cubes
    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
    {
        if ( pCube->nRefs == -1 )
            continue;
        Pdr_SetPrintStr( vStr, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );  
    }
    Vec_IntFreeP( &vFlopCounts );
    Vec_PtrFree( vCubes );
    Vec_StrPush( vStr, '\0' );
    return vStr;
}


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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Pdr_ManReportInvariant( Pdr_Man_t * p )
{
    Vec_Ptr_t * vCubes;
    int kStart = Pdr_ManFindInvariantStart( p );
    vCubes = Pdr_ManCollectCubes( p, kStart );
    Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d) (cex = %d, ave = %.2f)\n", 
        kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig), p->nCexesTotal, 1.0*p->nXsimLits/p->nXsimRuns );
//    Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d)\n", 
//        kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) );
    Vec_PtrFree( vCubes );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Pdr_ManVerifyInvariant( Pdr_Man_t * p )
{
    sat_solver * pSat;
    Vec_Int_t * vLits;
    Vec_Ptr_t * vCubes;
    Pdr_Set_t * pCube;
    int i, kStart, kThis, RetValue, Counter = 0;
    abctime clk = Abc_Clock();
    // collect cubes used in the inductive invariant
    kStart = Pdr_ManFindInvariantStart( p );
    vCubes = Pdr_ManCollectCubes( p, kStart );
    // create solver with the cubes
    kThis = Vec_PtrSize(p->vSolvers);
    pSat  = Pdr_ManCreateSolver( p, kThis );
    // add the property output
//    Pdr_ManSetPropertyOutput( p, kThis );
    // add the clauses
    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
    {
        vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 );
        RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
        assert( RetValue );
        sat_solver_compress( pSat );
    }
    // check each clause
    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
    {
        vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 );
        RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
        if ( RetValue != l_False )
        {
            Abc_Print( 1, "Verification of clause %d failed.\n", i );
            Counter++;
        }
    }
    if ( Counter )
        Abc_Print( 1, "Verification of %d clauses has failed.\n", Counter );
    else
    {
        Abc_Print( 1, "Verification of invariant with %d clauses was successful.  ", Vec_PtrSize(vCubes) );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    }
//    sat_solver_delete( pSat );
    Vec_PtrFree( vCubes );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
{
    sat_solver * pSat;
    Vec_Int_t * vLits;
    Pdr_Set_t * pCube;
    int i, kThis, RetValue, fChanges = 0, Counter = 0;
    // create solver with the cubes
    kThis = Vec_PtrSize(p->vSolvers);
    pSat  = Pdr_ManCreateSolver( p, kThis );
    // add the clauses
    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
    {
        if ( pCube->nRefs == -1 ) // skip non-inductive
            continue;
        vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 );
        RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
        assert( RetValue );
        sat_solver_compress( pSat );
    }
    // check each clause
    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
    {
        if ( pCube->nRefs == -1 ) // skip non-inductive
            continue;
        vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 );
        RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
        if ( RetValue != l_False ) // mark as non-inductive
        {
            pCube->nRefs = -1;
            fChanges = 1;
        }
        else
            Counter++;
    }
    //Abc_Print(1, "Clauses = %d.\n", Counter );
    //sat_solver_delete( pSat );
    return fChanges;
}
Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce )
{
    Vec_Int_t * vResult;
    Vec_Ptr_t * vCubes;
    Pdr_Set_t * pCube;
    int i, v, kStart;
    // collect cubes used in the inductive invariant
    kStart = Pdr_ManFindInvariantStart( p );
    vCubes = Pdr_ManCollectCubes( p, kStart );
    // refine as long as there are changes
    if ( fReduce )
        while ( Pdr_ManDeriveMarkNonInductive(p, vCubes) );
    // collect remaining clauses
    vResult = Vec_IntAlloc( 1000 );
    Vec_IntPush( vResult, 0 );
    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
    {
        if ( pCube->nRefs == -1 ) // skip non-inductive
            continue;
        Vec_IntAddToEntry( vResult, 0, 1 );
        Vec_IntPush( vResult, pCube->nLits );
        for ( v = 0; v < pCube->nLits; v++ )
            Vec_IntPush( vResult, pCube->Lits[v] );
    }
    //Vec_PtrFree( vCubes );
    Vec_PtrFreeP( &p->vInfCubes );
    p->vInfCubes = vCubes;
    Vec_IntPush( vResult, Aig_ManRegNum(p->pAig) );
    return vResult;
}



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

  Synopsis    [Remove clauses while maintaining the invariant.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
#define Pdr_ForEachCube( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 1 )

Vec_Int_t * Pdr_InvMap( Vec_Int_t * vCounts )
{
    int i, k = 0, Count;
    Vec_Int_t * vMap = Vec_IntStart( Vec_IntSize(vCounts) );
    Vec_IntForEachEntry( vCounts, Count, i )
        if ( Count )
            Vec_IntWriteEntry( vMap, i, k++ );
    return vMap;
}
Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv )
{
    int i, k, * pCube, * pList = Vec_IntArray(vInv);
    Vec_Int_t * vCounts = Vec_IntStart( Vec_IntEntryLast(vInv) );
    Pdr_ForEachCube( pList, pCube, i )
        for ( k = 0; k < pCube[0]; k++ )
            Vec_IntAddToEntry( vCounts, Abc_Lit2Var(pCube[k+1]), 1 );
    return vCounts;
}
int Pdr_InvUsedFlopNum( Vec_Int_t * vInv )
{
    Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
    int nZeros = Vec_IntCountZero( vCounts );
    Vec_IntFree( vCounts );
    return Vec_IntEntryLast(vInv) - nZeros;
}

Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts )
{
    Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
    Vec_Int_t * vMap = Pdr_InvMap( vCounts );
    int nVars = Vec_IntSize(vCounts) - Vec_IntCountZero(vCounts);
    int i, k, * pCube, * pList = Vec_IntArray(vInv);
    char * pBuffer = ABC_ALLOC( char, nVars );
    for ( i = 0; i < nVars; i++ )
        pBuffer[i] = '-';
    Pdr_ForEachCube( pList, pCube, i )
    {
        for ( k = 0; k < pCube[0]; k++ )
            pBuffer[Vec_IntEntry(vMap, Abc_Lit2Var(pCube[k+1]))] = '0' + !Abc_LitIsCompl(pCube[k+1]);
        for ( k = 0; k < nVars; k++ )
            Vec_StrPush( vStr, pBuffer[k] );
        Vec_StrPush( vStr, ' ' );
        Vec_StrPush( vStr, '1' );
        Vec_StrPush( vStr, '\n' );
        for ( k = 0; k < pCube[0]; k++ )
            pBuffer[Vec_IntEntry(vMap, Abc_Lit2Var(pCube[k+1]))] = '-';
    }
    Vec_StrPush( vStr, '\0' );
    ABC_FREE( pBuffer );
    Vec_IntFree( vMap );
    return vStr;
}
void Pdr_InvPrint( Vec_Int_t * vInv, int fVerbose )
{
    Abc_Print(1, "Invariant contains %d clauses with %d literals and %d flops (out of %d).\n", Vec_IntEntry(vInv, 0), Vec_IntSize(vInv)-Vec_IntEntry(vInv, 0)-2, Pdr_InvUsedFlopNum(vInv), Vec_IntEntryLast(vInv) );
    if ( fVerbose )
    {
        Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
        Vec_Str_t * vStr = Pdr_InvPrintStr( vInv, vCounts );
        Abc_Print(1, "%s", Vec_StrArray( vStr ) );
        Vec_IntFree( vCounts );
        Vec_StrFree( vStr );
    }
}

int Pdr_InvCheck_int( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose, sat_solver * pSat, int fSkip )
{
    int nBTLimit = 0;
    int fCheckProperty = 1;
    int i, k, status, nFailed = 0, nFailedOuts = 0; 
    // collect cubes
    int * pCube, * pList = Vec_IntArray(vInv);
    // create variables
    Vec_Int_t * vLits = Vec_IntAlloc(100);
    int iFoVarBeg = sat_solver_nvars(pSat) - Gia_ManRegNum(p);
    int iFiVarBeg = 1 + Gia_ManPoNum(p);
    // add cubes
    Pdr_ForEachCube( pList, pCube, i )
    {
        // collect literals
        Vec_IntClear( vLits );
        for ( k = 0; k < pCube[0]; k++ )
            if ( pCube[k+1] != -1 )
                Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) );
        if ( Vec_IntSize(vLits) == 0 )
        {
            Vec_IntFree( vLits );
            return 1;
        }
        // add it to the solver
        status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
        assert( status == 1 );
    }
    // verify property output
    if ( fCheckProperty )
    {
        for ( i = 0; i < Gia_ManPoNum(p); i++ )
        {
            Vec_IntFill( vLits, 1, Abc_Var2Lit(1+i, 0) );
            status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
            if ( status == l_Undef ) // timeout
                break;
            if ( status == l_True ) // sat - property fails
            {
                if ( fVerbose )
                    Abc_Print(1, "Coverage check failed for output %d.\n", i );
                nFailedOuts++;
                if ( fSkip )
                {
                    Vec_IntFree( vLits );
                    return 1;
                }
                continue;
            }
            assert( status == l_False ); // unsat - property holds
        }
    }
    // iterate through cubes in the direct order
    Pdr_ForEachCube( pList, pCube, i )
    {
        // collect cube
        Vec_IntClear( vLits );
        for ( k = 0; k < pCube[0]; k++ )
            if ( pCube[k+1] != -1 )
                Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) );
        // check if this cube intersects with the complement of other cubes in the solver
        // if it does not intersect, then it is redundant and can be skipped
        status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
        if ( status != l_True && fVerbose )
            Abc_Print(1, "Finished checking clause %d (out of %d)...\r", i, pList[0] );
        if ( status == l_Undef ) // timeout
            break;
        if ( status == l_False ) // unsat -- correct
            continue;
        assert( status == l_True );
        if ( fVerbose )
            Abc_Print(1, "Inductiveness check failed for clause %d.\n", i );
        nFailed++;
        if ( fSkip )
        {
            Vec_IntFree( vLits );
            return 1;
        }
    }
    Vec_IntFree( vLits );
    return nFailed + nFailedOuts;
}

int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose )
{
    int RetValue;
    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    assert( sat_solver_nvars(pSat) == pCnf->nVars );
    Cnf_DataFree( pCnf );
    RetValue = Pdr_InvCheck_int( p, vInv, fVerbose, pSat, 0 );
    sat_solver_delete( pSat );
    return RetValue;
}

Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose )
{
    int nBTLimit = 0;
    int fCheckProperty = 1;
    abctime clk = Abc_Clock();
    int n, i, k, status, nLits, fFailed = 0, fCannot = 0, nRemoved = 0; 
    Vec_Int_t * vRes = NULL;
    // create SAT solver
    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0];
    // create variables
    Vec_Int_t * vLits = Vec_IntAlloc(100);
    Vec_Bit_t * vRemoved = Vec_BitStart( nCubes );
    int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p);
    int iFiVarBeg = 1 + Gia_ManPoNum(p);
    int iAuxVarBeg = sat_solver_nvars(pSat);
    // allocate auxiliary variables
    assert( sat_solver_nvars(pSat) == pCnf->nVars );
    sat_solver_setnvars( pSat, sat_solver_nvars(pSat) + nCubes );
    // add clauses
    Pdr_ForEachCube( pList, pCube, i )
    {
        // collect literals
        Vec_IntFill( vLits, 1, Abc_Var2Lit(iAuxVarBeg + i, 1) ); // neg aux literal
        for ( k = 0; k < pCube[0]; k++ )
            Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) );
        // add it to the solver
        status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
        assert( status == 1 );
    }
    // iterate through clauses 
    Pdr_ForEachCube( pList, pCube, i )
    {
        if ( Vec_BitEntry(vRemoved, i) )
            continue;
        // collect aux literals for remaining clauses
        Vec_IntClear( vLits );
        for ( k = 0; k < nCubes; k++ )
            if ( k != i && !Vec_BitEntry(vRemoved, k) ) // skip this cube and already removed cubes
                Vec_IntPush( vLits, Abc_Var2Lit(iAuxVarBeg + k, 0) ); // pos aux literal
        nLits = Vec_IntSize( vLits );
        // check if the property still holds
        if ( fCheckProperty )
        {
            for ( k = 0; k < Gia_ManPoNum(p); k++ )
            {
                Vec_IntShrink( vLits, nLits );
                Vec_IntPush( vLits, Abc_Var2Lit(1+k, 0) );
                status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
                if ( status == l_Undef ) // timeout
                {
                    fFailed = 1;
                    break;
                }
                if ( status == l_True ) // sat - property fails
                    break;
                assert( status == l_False ); // unsat - property holds
            }
            if ( fFailed )
                break;
            if ( k < Gia_ManPoNum(p) )
                continue;
        }
        // check other clauses
        fCannot = 0;
        Pdr_ForEachCube( pList, pCube, n )
        {
            if ( Vec_BitEntry(vRemoved, n) || n == i )
                continue;
            // collect cube
            Vec_IntShrink( vLits, nLits );
            for ( k = 0; k < pCube[0]; k++ )
               Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) );
            // check if this cube intersects with the complement of other cubes in the solver
            // if it does not intersect, then it is redundant and can be skipped
            status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
            if ( status == l_Undef ) // timeout
            {
                fFailed = 1;
                break;
            }
            if ( status == l_False ) // unsat -- correct
                continue;
            assert( status == l_True );
            // cannot remove
            fCannot = 1;
            break;
        }
        if ( fFailed )
            break;
        if ( fCannot )
            continue;
        if ( fVerbose )
        Abc_Print(1, "Removing clause %d.\n", i );
        Vec_BitWriteEntry( vRemoved, i, 1 );
        nRemoved++;
    }
    if ( nRemoved )
        Abc_Print(1, "Invariant minimization reduced %d clauses (out of %d).  ", nRemoved, nCubes );
    else
        Abc_Print(1, "Invariant minimization did not change the invariant.  " ); 
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    // cleanup cover
    if ( !fFailed && nRemoved > 0 ) // finished without timeout and removed some cubes
    {
        vRes = Vec_IntAlloc( 1000 );
        Vec_IntPush( vRes, nCubes-nRemoved );
        Pdr_ForEachCube( pList, pCube, i )
            if ( !Vec_BitEntry(vRemoved, i) )
                for ( k = 0; k <= pCube[0]; k++ )
                    Vec_IntPush( vRes, pCube[k] );
        Vec_IntPush( vRes, Vec_IntEntryLast(vInv) );
    }
    Cnf_DataFree( pCnf );
    sat_solver_delete( pSat );
    Vec_BitFree( vRemoved );
    Vec_IntFree( vLits );
    return vRes;
}

Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose )
{
    Vec_Int_t * vRes = NULL;
    abctime clk = Abc_Clock();
    int i, k, nLits = 0, * pCube, * pList = Vec_IntArray(vInv), nRemoved = 0;
    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
    sat_solver * pSat;
//    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    Pdr_ForEachCube( pList, pCube, i )
    {
        nLits += pCube[0];
        for ( k = 0; k < pCube[0]; k++ )
        {
            int Save = pCube[k+1];
            pCube[k+1] = -1;
            //sat_solver_bookmark( pSat );
            pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
            if ( Pdr_InvCheck_int(p, vInv, 0, pSat, 1) )
                pCube[k+1] = Save;
            else
            {
                if ( fVerbose )
                Abc_Print(1, "Removing lit %d from clause %d.\n", k, i );
                nRemoved++;
            }
            sat_solver_delete( pSat );
            //sat_solver_rollback( pSat );
            //sat_solver_bookmark( pSat );
        }
    }
    Cnf_DataFree( pCnf );
    //sat_solver_delete( pSat );
    if ( nRemoved )
        Abc_Print(1, "Invariant minimization reduced %d literals (out of %d).  ", nRemoved, nLits );
    else
        Abc_Print(1, "Invariant minimization did not change the invariant.  " ); 
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    if ( nRemoved > 0 ) // finished without timeout and removed some lits
    {
        vRes = Vec_IntAlloc( 1000 );
        Vec_IntPush( vRes, pList[0] );
        Pdr_ForEachCube( pList, pCube, i )
        {
            int nLits = 0;
            for ( k = 0; k < pCube[0]; k++ )
                if ( pCube[k+1] != -1 )
                    nLits++;
            Vec_IntPush( vRes, nLits );
            for ( k = 0; k < pCube[0]; k++ )
                if ( pCube[k+1] != -1 )
                    Vec_IntPush( vRes, pCube[k+1] );
        }
        Vec_IntPush( vRes, Vec_IntEntryLast(vInv) );
    }
    return vRes;
}

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


ABC_NAMESPACE_IMPL_END