pdrInt.h File Reference

#include "aig/saig/saig.h"
#include "misc/vec/vecWec.h"
#include "sat/cnf/cnf.h"
#include "pdr.h"
#include "misc/hash/hashInt.h"
#include "aig/gia/giaAig.h"
#include "sat/bsat/satSolver.h"

Include dependency graph for pdrInt.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	Pdr_Set_t_
struct	Pdr_Obl_t_
struct	Pdr_Man_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Txs_Man_t_	Txs_Man_t
	INCLUDES ///.
typedef struct Txs3_Man_t_	Txs3_Man_t
typedef struct Pdr_Set_t_	Pdr_Set_t
typedef struct Pdr_Obl_t_	Pdr_Obl_t
typedef struct Pdr_Man_t_	Pdr_Man_t

Functions
int	Pdr_ObjSatVar (Pdr_Man_t *p, int k, int Pol, Aig_Obj_t *pObj)
	FUNCTION DECLARATIONS ///.
int	Pdr_ObjRegNum (Pdr_Man_t *p, int k, int iSatVar)
int	Pdr_ManFreeVar (Pdr_Man_t *p, int k)
sat_solver *	Pdr_ManNewSolver (sat_solver *pSat, Pdr_Man_t *p, int k, int fInit)
int	Pdr_ManCheckContainment (Pdr_Man_t *p, int k, Pdr_Set_t *pSet)
Vec_Int_t *	Pdr_ManCountFlopsInv (Pdr_Man_t *p)
void	Pdr_ManPrintProgress (Pdr_Man_t *p, int fClose, abctime Time)
	DECLARATIONS ///.
void	Pdr_ManPrintClauses (Pdr_Man_t *p, int kStart)
void	Pdr_ManDumpClauses (Pdr_Man_t *p, char *pFileName, int fProved)
Vec_Str_t *	Pdr_ManDumpString (Pdr_Man_t *p)
void	Pdr_ManReportInvariant (Pdr_Man_t *p)
void	Pdr_ManVerifyInvariant (Pdr_Man_t *p)
Vec_Int_t *	Pdr_ManDeriveInfinityClauses (Pdr_Man_t *p, int fReduce)
Pdr_Man_t *	Pdr_ManStart (Aig_Man_t *pAig, Pdr_Par_t *pPars, Vec_Int_t *vPrioInit)
void	Pdr_ManStop (Pdr_Man_t *p)
Abc_Cex_t *	Pdr_ManDeriveCex (Pdr_Man_t *p)
Abc_Cex_t *	Pdr_ManDeriveCexAbs (Pdr_Man_t *p)
sat_solver *	Pdr_ManCreateSolver (Pdr_Man_t *p, int k)
	DECLARATIONS ///.
sat_solver *	Pdr_ManFetchSolver (Pdr_Man_t *p, int k)
void	Pdr_ManSetPropertyOutput (Pdr_Man_t *p, int k)
Vec_Int_t *	Pdr_ManCubeToLits (Pdr_Man_t *p, int k, Pdr_Set_t *pCube, int fCompl, int fNext)
Vec_Int_t *	Pdr_ManLitsToCube (Pdr_Man_t *p, int k, int *pArray, int nArray)
void	Pdr_ManSolverAddClause (Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
void	Pdr_ManCollectValues (Pdr_Man_t *p, int k, Vec_Int_t *vObjIds, Vec_Int_t *vValues)
int	Pdr_ManCheckCubeCs (Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
int	Pdr_ManCheckCube (Pdr_Man_t *p, int k, Pdr_Set_t *pCube, Pdr_Set_t **ppPred, int nConfLimit, int fTryConf, int fUseLit)
Pdr_Set_t *	Pdr_ManTernarySim (Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
Txs_Man_t *	Txs_ManStart (Pdr_Man_t *pMan, Aig_Man_t *pAig, Vec_Int_t *vPrio)
	FUNCTION DEFINITIONS ///.
void	Txs_ManStop (Txs_Man_t *)
Pdr_Set_t *	Txs_ManTernarySim (Txs_Man_t *p, int k, Pdr_Set_t *pCube)
Txs3_Man_t *	Txs3_ManStart (Pdr_Man_t *pMan, Aig_Man_t *pAig, Vec_Int_t *vPrio)
	FUNCTION DEFINITIONS ///.
void	Txs3_ManStop (Txs3_Man_t *)
Pdr_Set_t *	Txs3_ManTernarySim (Txs3_Man_t *p, int k, Pdr_Set_t *pCube)
Pdr_Set_t *	Pdr_SetAlloc (int nSize)
	DECLARATIONS ///.
Pdr_Set_t *	Pdr_SetCreate (Vec_Int_t *vLits, Vec_Int_t *vPiLits)
Pdr_Set_t *	Pdr_SetCreateFrom (Pdr_Set_t *pSet, int iRemove)
Pdr_Set_t *	Pdr_SetCreateSubset (Pdr_Set_t *pSet, int *pLits, int nLits)
Pdr_Set_t *	Pdr_SetDup (Pdr_Set_t *pSet)
Pdr_Set_t *	Pdr_SetRef (Pdr_Set_t *p)
void	Pdr_SetDeref (Pdr_Set_t *p)
Pdr_Set_t *	ZPdr_SetIntersection (Pdr_Set_t *p1, Pdr_Set_t *p2, Hash_Int_t *keep)
int	Pdr_SetContains (Pdr_Set_t *pOld, Pdr_Set_t *pNew)
int	Pdr_SetContainsSimple (Pdr_Set_t *pOld, Pdr_Set_t *pNew)
int	Pdr_SetIsInit (Pdr_Set_t *p, int iRemove)
int	ZPdr_SetIsInit (Pdr_Set_t *p)
void	Pdr_SetPrint (FILE *pFile, Pdr_Set_t *p, int nRegs, Vec_Int_t *vFlopCounts)
void	ZPdr_SetPrint (Pdr_Set_t *p)
void	Pdr_SetPrintStr (Vec_Str_t *vStr, Pdr_Set_t *p, int nRegs, Vec_Int_t *vFlopCounts)
int	Pdr_SetCompare (Pdr_Set_t **pp1, Pdr_Set_t **pp2)
Pdr_Obl_t *	Pdr_OblStart (int k, int prio, Pdr_Set_t *pState, Pdr_Obl_t *pNext)
Pdr_Obl_t *	Pdr_OblRef (Pdr_Obl_t *p)
void	Pdr_OblDeref (Pdr_Obl_t *p)
int	Pdr_QueueIsEmpty (Pdr_Man_t *p)
Pdr_Obl_t *	Pdr_QueueHead (Pdr_Man_t *p)
Pdr_Obl_t *	Pdr_QueuePop (Pdr_Man_t *p)
void	Pdr_QueueClean (Pdr_Man_t *p)
void	Pdr_QueuePush (Pdr_Man_t *p, Pdr_Obl_t *pObl)
void	Pdr_QueuePrint (Pdr_Man_t *p)
void	Pdr_QueueStop (Pdr_Man_t *p)

Typedef Documentation

Pdr_Man_t

typedef struct Pdr_Man_t_ Pdr_Man_t

Definition at line 95 of file pdrInt.h.

Pdr_Obl_t

typedef struct Pdr_Obl_t_ Pdr_Obl_t

Definition at line 84 of file pdrInt.h.

Pdr_Set_t

typedef struct Pdr_Set_t_ Pdr_Set_t

Definition at line 74 of file pdrInt.h.

Txs3_Man_t

typedef struct Txs3_Man_t_ Txs3_Man_t

Definition at line 72 of file pdrInt.h.

Txs_Man_t

typedef typedefABC_NAMESPACE_HEADER_START struct Txs_Man_t_ Txs_Man_t

INCLUDES ///.

CFile****************************************************************

FileName [pdrInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [Internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

pdrInt.h,v 1.00 2010/11/20 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 71 of file pdrInt.h.

Function Documentation

Pdr_ManCheckContainment()

int Pdr_ManCheckContainment ( Pdr_Man_t * p, int k, Pdr_Set_t * pSet )

extern

Function*************************************************************

Synopsis [Returns 1 if the clause is contained in higher clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 390 of file pdrCore.c.

{
    Pdr_Set_t * pThis;
    Vec_Ptr_t * vArrayK;
    int i, j, kMax = Vec_PtrSize(p->vSolvers)-1;
    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax+1 )
        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pThis, j )
            if ( Pdr_SetContains( pSet, pThis ) )
                return 1;
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManCheckCube()

int Pdr_ManCheckCube ( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf, int fUseLit )

extern

Function*************************************************************

Synopsis [Checks if the cube holds (UNSAT) in the given timeframe.]

Description [Return 1/0 if cube or property are proved to hold/fail in k-th timeframe. Returns the predecessor bad state in ppPred.]

SideEffects []

SeeAlso []

Definition at line 290 of file pdrSat.c.

{ 
    //int fUseLit = 0;
    int fLitUsed = 0;
    sat_solver * pSat;
    Vec_Int_t * vLits;
    int Lit, RetValue;
    abctime clk, Limit;
    p->nCalls++;
    pSat = Pdr_ManFetchSolver( p, k );
    if ( pCube == NULL ) // solve the property
    {
        clk = Abc_Clock();
        Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, k, 2, Aig_ManCo(p->pAig, p->iOutCur)), 0 ); // pos literal (property fails)
        Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
        RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
        sat_solver_set_runtime_limit( pSat, Limit );
        if ( RetValue == l_Undef )
            return -1;
    }
    else // check relative containment in terms of next states
    {
        if ( fUseLit )
        {
            fLitUsed = 1;
            Vec_IntAddToEntry( p->vActVars, k, 1 );
            // add the cube in terms of current state variables
            vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
            // add activation literal
            Lit = Abc_Var2Lit( Pdr_ManFreeVar(p, k), 0 );
            // add activation literal
            Vec_IntPush( vLits, Lit );
            RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
            assert( RetValue == 1 );
            sat_solver_compress( pSat );
            // create assumptions
            vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
            // add activation literal
            Vec_IntPush( vLits, Abc_LitNot(Lit) );
        }
        else
            vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
 
        // solve 
        clk = Abc_Clock();
        Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
        RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), fTryConf ? p->pPars->nConfGenLimit : nConfLimit, 0, 0, 0 );
        sat_solver_set_runtime_limit( pSat, Limit );
        if ( RetValue == l_Undef )
        {
            if ( fTryConf && p->pPars->nConfGenLimit )
                RetValue = l_True;
            else
                return -1;
        }
    }
    clk = Abc_Clock() - clk;
    p->tSat += clk;
    assert( RetValue != l_Undef );
    if ( RetValue == l_False )
    {
        p->tSatUnsat += clk;
        p->nCallsU++;
        if ( ppPred )
            *ppPred = NULL;
        RetValue = 1;
    }
    else // if ( RetValue == l_True )
    {
        p->tSatSat += clk;
        p->nCallsS++;
        if ( ppPred )
        {
            abctime clk = Abc_Clock();
            if ( p->pPars->fNewXSim )
                *ppPred = Txs3_ManTernarySim( p->pTxs3, k, pCube );
            else
                *ppPred = Pdr_ManTernarySim( p, k, pCube );
            p->tTsim += Abc_Clock() - clk;
            p->nXsimLits += (*ppPred)->nLits;
            p->nXsimRuns++;
        }
        RetValue = 0;
    }
 
/* // for some reason, it does not work...
    if ( fLitUsed )
    {
        int RetValue;
        Lit = Abc_LitNot(Lit);
        RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
        assert( RetValue == 1 );
        sat_solver_compress( pSat );
    }
*/
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManCheckCubeCs()

int Pdr_ManCheckCubeCs ( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )

extern

Function*************************************************************

Synopsis [Checks if the cube holds (UNSAT) in the given timeframe.]

Description [Return 1/0 if cube or property are proved to hold/fail in k-th timeframe. Returns the predecessor bad state in ppPred.]

SideEffects []

SeeAlso []

Definition at line 262 of file pdrSat.c.

{ 
    sat_solver * pSat;
    Vec_Int_t * vLits;
    abctime Limit;
    int RetValue;
    pSat = Pdr_ManFetchSolver( p, k );
    vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 );
    Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
    RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
    sat_solver_set_runtime_limit( pSat, Limit );
    if ( RetValue == l_Undef )
        return -1;
    return (RetValue == l_False);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManCollectValues()

void Pdr_ManCollectValues ( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues )

extern

Function*************************************************************

Synopsis [Collects values of the RO/RI variables in k-th SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 236 of file pdrSat.c.

{
    sat_solver * pSat;
    Aig_Obj_t * pObj;
    int iVar, i;
    Vec_IntClear( vValues );
    pSat = Pdr_ManSolver(p, k);
    Aig_ManForEachObjVec( vObjIds, p->pAig, pObj, i )
    {
        iVar = Pdr_ObjSatVar( p, k, 3, pObj ); assert( iVar >= 0 );
        Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManCountFlopsInv()

Vec_Int_t * Pdr_ManCountFlopsInv ( Pdr_Man_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 196 of file pdrInv.c.

{
    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;
}

Here is the call graph for this function:

Pdr_ManCreateSolver()

sat_solver * Pdr_ManCreateSolver ( Pdr_Man_t * p, int k )

extern

DECLARATIONS ///.

CFile****************************************************************

FileName [pdrSat.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [SAT solver procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

pdrSat.c,v 1.00 2010/11/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Creates new SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file pdrSat.c.

{
    sat_solver * pSat;
    Aig_Obj_t * pObj;
    int i;
    assert( Vec_PtrSize(p->vSolvers) == k );
    assert( Vec_VecSize(p->vClauses) == k );
    assert( Vec_IntSize(p->vActVars) == k );
    // create new solver
//    pSat = sat_solver_new();
    pSat = zsat_solver_new_seed(p->pPars->nRandomSeed);
    pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
    Vec_PtrPush( p->vSolvers, pSat );
    Vec_VecExpand( p->vClauses, k );
    Vec_IntPush( p->vActVars, 0 );
    // add property cone
    Saig_ManForEachPo( p->pAig, pObj, i )
        Pdr_ObjSatVar( p, k, 1, pObj );
    return pSat;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManCubeToLits()

Vec_Int_t * Pdr_ManCubeToLits ( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext )

extern

Function*************************************************************

Synopsis [Converts the cube in terms of RO numbers into array of CNF literals.]

Description []

SideEffects []

SeeAlso []

Definition at line 144 of file pdrSat.c.

{
    Aig_Obj_t * pObj;
    int i, iVar, iVarMax = 0;
    abctime clk = Abc_Clock();
    Vec_IntClear( p->vLits );
//    assert( !(fNext && fCompl) );
    for ( i = 0; i < pCube->nLits; i++ )
    {
        if ( pCube->Lits[i] == -1 )
            continue;
        if ( fNext )
            pObj = Saig_ManLi( p->pAig, Abc_Lit2Var(pCube->Lits[i]) );
        else
            pObj = Saig_ManLo( p->pAig, Abc_Lit2Var(pCube->Lits[i]) );
        iVar = Pdr_ObjSatVar( p, k, fNext ? 2 - Abc_LitIsCompl(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
        iVarMax = Abc_MaxInt( iVarMax, iVar );
        Vec_IntPush( p->vLits, Abc_Var2Lit( iVar, fCompl ^ Abc_LitIsCompl(pCube->Lits[i]) ) );
    }
//    sat_solver_setnvars( Pdr_ManSolver(p, k), iVarMax + 1 );
    p->tCnf += Abc_Clock() - clk;
    return p->vLits;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManDeriveCex()

Abc_Cex_t * Pdr_ManDeriveCex ( Pdr_Man_t * p )

extern

Function*************************************************************

Synopsis [Derives counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 408 of file pdrMan.c.

{
    Abc_Cex_t * pCex;
    Pdr_Obl_t * pObl;
    int i, f, Lit, nFrames = 0;
    // count the number of frames
    for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
        nFrames++;
    // create the counter-example
    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
    pCex->iPo    = p->iOutCur;
    pCex->iFrame = nFrames-1;
    for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
        for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
        {
            Lit = pObl->pState->Lits[i];
            if ( Abc_LitIsCompl(Lit) )
                continue;
            if ( Abc_Lit2Var(Lit) >= pCex->nPis ) // allows PPI literals to be thrown away
                continue;
            assert( Abc_Lit2Var(Lit) < pCex->nPis );
            Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Abc_Lit2Var(Lit) );
        }
    assert( f == nFrames );
    if ( !Saig_ManVerifyCex(p->pAig, pCex) )
        printf( "CEX for output %d is not valid.\n", p->iOutCur );
    return pCex;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManDeriveCexAbs()

Abc_Cex_t * Pdr_ManDeriveCexAbs ( Pdr_Man_t * p )

extern

Function*************************************************************

Synopsis [Derives counter-example when abstraction is used.]

Description []

SideEffects []

SeeAlso []

Definition at line 448 of file pdrMan.c.

{
    extern Gia_Man_t * Gia_ManDupAbs( Gia_Man_t * p, Vec_Int_t * vMapPpi2Ff, Vec_Int_t * vMapFf2Ppi );
 
    Gia_Man_t * pAbs;
    Abc_Cex_t * pCex, * pCexCare;
    Pdr_Obl_t * pObl;
    int i, f, Lit, Flop, nFrames = 0;
    int nPis = Saig_ManPiNum(p->pAig);
    int nFfRefined = 0;
    if ( !p->pPars->fUseAbs || !p->vMapPpi2Ff )
        return Pdr_ManDeriveCex(p);
    // restore previous map
    Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
    {
        assert( Vec_IntEntry( p->vMapFf2Ppi, Flop ) == i );
        Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, -1 );
    }
    Vec_IntClear( p->vMapPpi2Ff );
    // count the number of frames
    for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
    {
        for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
        {
            Lit = pObl->pState->Lits[i]; 
            if ( Abc_Lit2Var(Lit) < nPis ) // PI literal
                continue;
            Flop = Abc_Lit2Var(Lit) - nPis;
            if ( Vec_IntEntry(p->vMapFf2Ppi, Flop) >= 0 ) // already used PPI literal
                continue;
            Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, Vec_IntSize(p->vMapPpi2Ff) );
            Vec_IntPush( p->vMapPpi2Ff, Flop );
        }
        nFrames++;
    }
    if ( Vec_IntSize(p->vMapPpi2Ff) == 0 ) // no PPIs -- this is a real CEX
        return Pdr_ManDeriveCex(p);
    if ( p->pPars->fUseSimpleRef )
    {
        // rely on ternary simulation to perform refinement
        Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
        {
            assert( Vec_IntEntry(p->vAbsFlops, Flop) == 0 );
            Vec_IntWriteEntry( p->vAbsFlops, Flop, 1 );
            nFfRefined++;
        }
    }
    else
    {
        // create the counter-example
        pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig) - Vec_IntSize(p->vMapPpi2Ff), Saig_ManPiNum(p->pAig) + Vec_IntSize(p->vMapPpi2Ff), nFrames );
        pCex->iPo    = p->iOutCur;
        pCex->iFrame = nFrames-1;
        for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
            for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
            {
                Lit = pObl->pState->Lits[i];
                if ( Abc_LitIsCompl(Lit) )
                    continue;
                if ( Abc_Lit2Var(Lit) < nPis ) // PI literal
                    Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Abc_Lit2Var(Lit) );
                else
                {
                    int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, Abc_Lit2Var(Lit) - nPis);
                    assert( iPPI < pCex->nPis );
                    Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + iPPI );
                }
            }
        assert( f == nFrames );
        // perform CEX minimization
        pAbs = Gia_ManDupAbs( p->pGia, p->vMapPpi2Ff, p->vMapFf2Ppi );
        pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 0, 0 );
        Gia_ManStop( pAbs );
        assert( pCexCare->nPis == pCex->nPis );
        Abc_CexFree( pCex );
        // detect care PPIs
        for ( f = 0; f < nFrames; f++ )
        {
            for ( i = nPis; i < pCexCare->nPis; i++ )
                if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
                {
                    if ( Vec_IntEntry(p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis)) == 0 ) // currently abstracted
                        Vec_IntWriteEntry( p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis), 1 ), nFfRefined++;
                }
        }
        Abc_CexFree( pCexCare );
        if ( nFfRefined == 0 ) // no refinement -- this is a real CEX
            return Pdr_ManDeriveCex(p);
    }
    //printf( "CEX-based refinement refined %d flops.\n", nFfRefined );
    p->nCexesTotal++;
    p->nCexes++;
    return NULL;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManDeriveInfinityClauses()

Vec_Int_t * Pdr_ManDeriveInfinityClauses ( Pdr_Man_t * p, int fReduce )

extern

Definition at line 595 of file pdrInv.c.

{
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManDumpClauses()

void Pdr_ManDumpClauses ( Pdr_Man_t * p, char * pFileName, int fProved )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 352 of file pdrInv.c.

{
    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 (*)(const void *, const 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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManDumpString()

Vec_Str_t * Pdr_ManDumpString ( Pdr_Man_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 435 of file pdrInv.c.

{
    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 (*)(const void *, const 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;
}

Here is the call graph for this function:

Pdr_ManFetchSolver()

sat_solver * Pdr_ManFetchSolver ( Pdr_Man_t * p, int k )

extern

Function*************************************************************

Synopsis [Returns old or restarted solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file pdrSat.c.

{
    sat_solver * pSat;
    Vec_Ptr_t * vArrayK;
    Pdr_Set_t * pCube;
    int i, j;
    pSat = Pdr_ManSolver(p, k);
    if ( Vec_IntEntry(p->vActVars, k) < p->pPars->nRecycle )
        return pSat;
    assert( k < Vec_PtrSize(p->vSolvers) - 1 );
    p->nStarts++;
//    sat_solver_delete( pSat );
//    pSat = sat_solver_new();
//    sat_solver_restart( pSat );
    zsat_solver_restart_seed( pSat, p->pPars->nRandomSeed );
    // create new SAT solver
    pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
    // write new SAT solver
    Vec_PtrWriteEntry( p->vSolvers, k, pSat );
    Vec_IntWriteEntry( p->vActVars, k, 0 );
    // set the property output
    Pdr_ManSetPropertyOutput( p, k );
    // add the clauses
    Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k )
        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
            Pdr_ManSolverAddClause( p, k, pCube );
    return pSat;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManFreeVar()

int Pdr_ManFreeVar ( Pdr_Man_t * p, int k )

extern

Function*************************************************************

Synopsis [Returns the index of unused SAT variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 332 of file pdrCnf.c.

{
    if ( p->pPars->fMonoCnf )
        return sat_solver_nvars( Pdr_ManSolver(p, k) );
    else
    {
        Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry( &p->vVar2Ids, k );
        Vec_IntPush( vVar2Ids, -1 );
        return Vec_IntSize( vVar2Ids ) - 1;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManLitsToCube()

Vec_Int_t * Pdr_ManLitsToCube ( Pdr_Man_t * p, int k, int * pArray, int nArray )

extern

Function*************************************************************

Synopsis [Converts SAT variables into register IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file pdrSat.c.

{
    int i, RegId;
    Vec_IntClear( p->vLits );
    for ( i = 0; i < nArray; i++ )
    {
        RegId = Pdr_ObjRegNum( p, k, Abc_Lit2Var(pArray[i]) );
        if ( RegId == -1 )
            continue;
        assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
        Vec_IntPush( p->vLits, Abc_Var2Lit(RegId, !Abc_LitIsCompl(pArray[i])) );
    }
    assert( Vec_IntSize(p->vLits) >= 0 && Vec_IntSize(p->vLits) <= nArray );
    return p->vLits;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManNewSolver()

sat_solver * Pdr_ManNewSolver ( sat_solver * pSat, Pdr_Man_t * p, int k, int fInit )

extern

Function*************************************************************

Synopsis [Creates SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 439 of file pdrCnf.c.

{
    assert( pSat != NULL );
    if ( p->pPars->fMonoCnf )
        return Pdr_ManNewSolver1( pSat, p, k, fInit );
    else
        return Pdr_ManNewSolver2( pSat, p, k, fInit );
}

Here is the caller graph for this function:

Pdr_ManPrintClauses()

void Pdr_ManPrintClauses ( Pdr_Man_t * p, int kStart )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 244 of file pdrInv.c.

{
    Vec_Ptr_t * vArrayK;
    Pdr_Set_t * pCube;
    int i, k, Counter = 0;
    Vec_VecForEachLevelStart( p->vClauses, vArrayK, k, kStart )
    {
        Vec_PtrSort( vArrayK, (int (*)(const void *, const 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" ); 
        }
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManPrintProgress()

void Pdr_ManPrintProgress ( Pdr_Man_t * p, int fClose, abctime Time )

extern

DECLARATIONS ///.

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

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file pdrInv.c.

{
    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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManReportInvariant()

void Pdr_ManReportInvariant ( Pdr_Man_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 477 of file pdrInv.c.

{
    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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManSetPropertyOutput()

void Pdr_ManSetPropertyOutput ( Pdr_Man_t * p, int k )

extern

Function*************************************************************

Synopsis [Sets the property output to 0 (sat) forever.]

Description []

SideEffects []

SeeAlso []

Definition at line 179 of file pdrSat.c.

{
    sat_solver * pSat;
    Aig_Obj_t * pObj;
    int Lit, RetValue, i;
    if ( !p->pPars->fUsePropOut )
        return;
    pSat = Pdr_ManSolver(p, k);
    Saig_ManForEachPo( p->pAig, pObj, i )
    {
        // skip solved outputs
        if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
            continue;
        // skip timedout outputs
        if ( p->pPars->vOutMap && Vec_IntEntry(p->pPars->vOutMap, i) == -1 )
            continue;
        Lit = Abc_Var2Lit( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal
        RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
        assert( RetValue == 1 );
    }
    sat_solver_compress( pSat );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManSolverAddClause()

void Pdr_ManSolverAddClause ( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )

extern

Function*************************************************************

Synopsis [Adds one clause in terms of ROs to the k-th SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 213 of file pdrSat.c.

{
    sat_solver * pSat;
    Vec_Int_t * vLits;
    int RetValue;
    pSat  = Pdr_ManSolver(p, k);
    vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
    RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
    assert( RetValue == 1 );
    sat_solver_compress( pSat );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManStart()

Pdr_Man_t * Pdr_ManStart ( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit )

extern

Function*************************************************************

Synopsis [Creates manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 248 of file pdrMan.c.

{
    Pdr_Man_t * p;
    p = ABC_CALLOC( Pdr_Man_t, 1 );
    p->pPars    = pPars;
    p->pAig     = pAig;
    p->pGia     = (pPars->fFlopPrio || p->pPars->fNewXSim || p->pPars->fUseAbs) ? Gia_ManFromAigSimple(pAig) : NULL;
    p->vSolvers = Vec_PtrAlloc( 0 );
    p->vClauses = Vec_VecAlloc( 0 );
    p->pQueue   = NULL;
    p->pOrder   = ABC_ALLOC( int, Aig_ManRegNum(pAig) );
    p->vActVars = Vec_IntAlloc( 256 );
    if ( !p->pPars->fMonoCnf )
        p->vVLits   = Vec_WecStart( 1+Abc_MaxInt(1, Aig_ManLevels(pAig)) );
    // internal use
    p->nPrioShift = Abc_Base2Log(Aig_ManRegNum(pAig));
    if ( vPrioInit )
        p->vPrio = vPrioInit;
    else if ( pPars->fFlopPrio )
        p->vPrio = Pdr_ManDeriveFlopPriorities2(p->pGia, 1);
//    else if ( p->pPars->fNewXSim )
//        p->vPrio = Vec_IntStartNatural( Aig_ManRegNum(pAig) );
    else 
        p->vPrio = Vec_IntStart( Aig_ManRegNum(pAig) );
    p->vLits    = Vec_IntAlloc( 100 );  // array of literals
    p->vCiObjs  = Vec_IntAlloc( 100 );  // cone leaves
    p->vCoObjs  = Vec_IntAlloc( 100 );  // cone roots
    p->vCiVals  = Vec_IntAlloc( 100 );  // cone leaf values
    p->vCoVals  = Vec_IntAlloc( 100 );  // cone root values
    p->vNodes   = Vec_IntAlloc( 100 );  // cone nodes
    p->vUndo    = Vec_IntAlloc( 100 );  // cone undos
    p->vVisits  = Vec_IntAlloc( 100 );  // intermediate
    p->vCi2Rem  = Vec_IntAlloc( 100 );  // CIs to be removed
    p->vRes     = Vec_IntAlloc( 100 );  // final result
    p->pCnfMan  = Cnf_ManStart();
    // ternary simulation
    p->pTxs3    = pPars->fNewXSim ? Txs3_ManStart( p, pAig, p->vPrio ) : NULL;
    // additional AIG data-members
    if ( pAig->pFanData == NULL )
        Aig_ManFanoutStart( pAig );
    if ( pAig->pTerSimData == NULL )
        pAig->pTerSimData = ABC_CALLOC( unsigned, 1 + (Aig_ManObjNumMax(pAig) / 16) );
    // time spent on each outputs
    if ( pPars->nTimeOutOne )
    {
        int i;
        p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) );
        for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
            p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
    }
    if ( pPars->fSolveAll )
    {
        p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
        p->pPars->vOutMap = Vec_IntAlloc( Saig_ManPoNum(pAig) );
        Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 );
    }
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManStop()

void Pdr_ManStop ( Pdr_Man_t * p )

extern

Function*************************************************************

Synopsis [Frees manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 318 of file pdrMan.c.

{
    Pdr_Set_t * pCla;
    sat_solver * pSat;
    int i, k;
    Gia_ManStopP( &p->pGia );
    Aig_ManCleanMarkAB( p->pAig );
    if ( p->pPars->fVerbose ) 
    {
        Abc_Print( 1, "Block =%5d  Oblig =%6d  Clause =%6d  Call =%6d (sat=%.1f%%)  Cex =%4d  Start =%4d\n", 
            p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nCexesTotal, p->nStarts );
        ABC_PRTP( "SAT solving", p->tSat,       p->tTotal );
        ABC_PRTP( "  unsat    ", p->tSatUnsat,  p->tTotal );
        ABC_PRTP( "  sat      ", p->tSatSat,    p->tTotal );
        ABC_PRTP( "Generalize ", p->tGeneral,   p->tTotal );
        ABC_PRTP( "Push clause", p->tPush,      p->tTotal );
        ABC_PRTP( "Ternary sim", p->tTsim,      p->tTotal );
        ABC_PRTP( "Containment", p->tContain,   p->tTotal );
        ABC_PRTP( "CNF compute", p->tCnf,       p->tTotal );
        ABC_PRTP( "Refinement ", p->tAbs,       p->tTotal );
        ABC_PRTP( "TOTAL      ", p->tTotal,     p->tTotal );
        fflush( stdout );
    }
//    Abc_Print( 1, "SS =%6d. SU =%6d. US =%6d. UU =%6d.\n", p->nCasesSS, p->nCasesSU, p->nCasesUS, p->nCasesUU );
    Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i )
        sat_solver_delete( pSat );
    Vec_PtrFree( p->vSolvers );
    Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pCla, i, k )
        Pdr_SetDeref( pCla );
    Vec_VecFree( p->vClauses );
    Pdr_QueueStop( p );
    ABC_FREE( p->pOrder );
    Vec_IntFree( p->vActVars );
    // static CNF
    Cnf_DataFree( p->pCnf1 );
    Vec_IntFreeP( &p->vVar2Reg );
    // dynamic CNF
    Cnf_DataFree( p->pCnf2 );
    if ( p->pvId2Vars )
    for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
        ABC_FREE( p->pvId2Vars[i].pArray );
    ABC_FREE( p->pvId2Vars );
//    Vec_VecFreeP( (Vec_Vec_t **)&p->vVar2Ids );
    for ( i = 0; i < Vec_PtrSize(&p->vVar2Ids); i++ )
        Vec_IntFree( (Vec_Int_t *)Vec_PtrEntry(&p->vVar2Ids, i) );
    ABC_FREE( p->vVar2Ids.pArray );
    Vec_WecFreeP( &p->vVLits );
    // CNF manager
    Cnf_ManStop( p->pCnfMan );
    Vec_IntFreeP( &p->vAbsFlops );
    Vec_IntFreeP( &p->vMapFf2Ppi );
    Vec_IntFreeP( &p->vMapPpi2Ff );
    // terminary simulation
    if ( p->pPars->fNewXSim )
        Txs3_ManStop( p->pTxs3 );
    // internal use
    Vec_IntFreeP( &p->vPrio   );  // priority flops
    Vec_IntFree( p->vLits     );  // array of literals
    Vec_IntFree( p->vCiObjs   );  // cone leaves
    Vec_IntFree( p->vCoObjs   );  // cone roots
    Vec_IntFree( p->vCiVals   );  // cone leaf values
    Vec_IntFree( p->vCoVals   );  // cone root values
    Vec_IntFree( p->vNodes    );  // cone nodes
    Vec_IntFree( p->vUndo     );  // cone undos
    Vec_IntFree( p->vVisits   );  // intermediate
    Vec_IntFree( p->vCi2Rem   );  // CIs to be removed
    Vec_IntFree( p->vRes      );  // final result
    Vec_PtrFreeP( &p->vInfCubes );
    ABC_FREE( p->pTime4Outs );
    if ( p->vCexes )
        Vec_PtrFreeFree( p->vCexes );
    // additional AIG data-members
    if ( p->pAig->pFanData != NULL )
        Aig_ManFanoutStop( p->pAig );
    if ( p->pAig->pTerSimData != NULL )
        ABC_FREE( p->pAig->pTerSimData );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManTernarySim()

Pdr_Set_t * Pdr_ManTernarySim ( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )

extern

Function*************************************************************

Synopsis [Shrinks values using ternary simulation.]

Description [The cube contains the set of flop index literals which, when converted into a clause and applied to the combinational outputs, led to a satisfiable SAT run in frame k (values stored in the SAT solver). If the cube is NULL, it is assumed that the first property output was asserted and failed. The resulting array is a set of flop index literals that asserts the COs. Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]

SideEffects []

SeeAlso []

Definition at line 351 of file pdrTsim.c.

{
    Pdr_Set_t * pRes;
    Vec_Int_t * vPrio   = p->vPrio;    // priority flops (flop indices)
    Vec_Int_t * vPiLits = p->vLits;    // array of literals (0/1 PI values)
    Vec_Int_t * vCiObjs = p->vCiObjs;  // cone leaves (CI obj IDs)
    Vec_Int_t * vCoObjs = p->vCoObjs;  // cone roots (CO obj IDs)
    Vec_Int_t * vCiVals = p->vCiVals;  // cone leaf values (0/1 CI values)
    Vec_Int_t * vCoVals = p->vCoVals;  // cone root values (0/1 CO values)
    Vec_Int_t * vNodes  = p->vNodes;   // cone nodes (node obj IDs)
    Vec_Int_t * vUndo   = p->vUndo;    // cone undos (node obj IDs)
    Vec_Int_t * vVisits = p->vVisits;  // intermediate (obj IDs)
    Vec_Int_t * vCi2Rem = p->vCi2Rem;  // CIs to be removed (CI obj IDs)
    Vec_Int_t * vRes    = p->vRes;     // final result (flop literals)
    Aig_Obj_t * pObj;
    int i, Entry, RetValue;
    //abctime clk = Abc_Clock();
 
    // collect CO objects
    Vec_IntClear( vCoObjs );
    if ( pCube == NULL ) // the target is the property output
    {
//        Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
        Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, p->iOutCur)) );
    }
    else // the target is the cube
    {
        for ( i = 0; i < pCube->nLits; i++ )
        {
            if ( pCube->Lits[i] == -1 )
                continue;
            pObj = Saig_ManLi(p->pAig, (pCube->Lits[i] >> 1));
            Vec_IntPush( vCoObjs, Aig_ObjId(pObj) );
        }
    }
if ( p->pPars->fVeryVerbose )
{
Abc_Print( 1, "Trying to justify cube " );
if ( pCube )
    Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
else
    Abc_Print( 1, "<prop=fail>" );
Abc_Print( 1, " in frame %d.\n", k );
}
 
    // collect CI objects
    Pdr_ManCollectCone( p->pAig, vCoObjs, vCiObjs, vNodes );
    // collect values
    Pdr_ManCollectValues( p, k, vCiObjs, vCiVals );
    Pdr_ManCollectValues( p, k, vCoObjs, vCoVals );
    // simulate for the first time
if ( p->pPars->fVeryVerbose )
Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
    RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL );
    assert( RetValue );
 
    // iteratively remove flops
    if ( p->pPars->fFlopPrio )
    {
        // collect flops and sort them by priority
        Vec_IntClear( vRes );
        Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
        {
            if ( !Saig_ObjIsLo( p->pAig, pObj ) )
                continue;
            Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
            Vec_IntPush( vRes, Entry );
        }
        Vec_IntSelectSortCost( Vec_IntArray(vRes), Vec_IntSize(vRes), vPrio );
 
        // try removing flops starting from low-priority to high-priority
        Vec_IntClear( vCi2Rem );
        Vec_IntForEachEntry( vRes, Entry, i )
        {
            pObj = Aig_ManCi( p->pAig, Saig_ManPiNum(p->pAig) + Entry );
            assert( Saig_ObjIsLo( p->pAig, pObj ) );
            Vec_IntClear( vUndo );
            if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
                Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
            else
                Pdr_ManExtendUndo( p->pAig, vUndo );
        }
    }
    else
    {
        // try removing low-priority flops first
        Vec_IntClear( vCi2Rem );
        Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
        {
            if ( !Saig_ObjIsLo( p->pAig, pObj ) )
                continue;
            Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
            if ( Vec_IntEntry(vPrio, Entry) )
                continue;
            Vec_IntClear( vUndo );
            if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
                Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
            else
                Pdr_ManExtendUndo( p->pAig, vUndo );
        }
        // try removing high-priority flops next
        Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
        {
            if ( !Saig_ObjIsLo( p->pAig, pObj ) )
                continue;
            Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
            if ( !Vec_IntEntry(vPrio, Entry) )
                continue;
            Vec_IntClear( vUndo );
            if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
                Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
            else
                Pdr_ManExtendUndo( p->pAig, vUndo );
        }
    }
 
if ( p->pPars->fVeryVerbose )
Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
    RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, vCi2Rem );
    assert( RetValue );
 
    // derive the set of resulting registers
    Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
    assert( Vec_IntSize(vRes) > 0 );
    //p->tTsim += Abc_Clock() - clk;
 
    // move abstracted literals from flops to inputs
    if ( p->pPars->fUseAbs && p->vAbsFlops )
    {
        int i, iLit, k = 0;
        Vec_IntForEachEntry( vRes, iLit, i )
        {
            if ( Vec_IntEntry(p->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop
                Vec_IntWriteEntry( vRes, k++, iLit );
            else
                Vec_IntPush( vPiLits, 2*Saig_ManPiNum(p->pAig) + iLit );
        }
        Vec_IntShrink( vRes, k );
    }
    pRes = Pdr_SetCreate( vRes, vPiLits );
    //ZH: Disabled assertion because this invariant doesn't hold with down
    //because of the join operation which can bring in initial states
    //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
    return pRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ManVerifyInvariant()

void Pdr_ManVerifyInvariant ( Pdr_Man_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 500 of file pdrInv.c.

{
    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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_ObjRegNum()

int Pdr_ObjRegNum ( Pdr_Man_t * p, int k, int iSatVar )

extern

Function*************************************************************

Synopsis [Returns register number for the given SAT variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 312 of file pdrCnf.c.

{
    if ( p->pPars->fMonoCnf )
        return Pdr_ObjRegNum1( p, k, iSatVar );
    else
        return Pdr_ObjRegNum2( p, k, iSatVar );
}

Here is the caller graph for this function:

Pdr_ObjSatVar()

int Pdr_ObjSatVar ( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj )

extern

FUNCTION DECLARATIONS ///.

Function*************************************************************

Synopsis [Returns SAT variable of the given object.]

Description []

SideEffects []

SeeAlso []

Definition at line 241 of file pdrCnf.c.

{
    if ( p->pPars->fMonoCnf )
        return Pdr_ObjSatVar1( p, k, pObj );
    else
        return Pdr_ObjSatVar2( p, k, pObj, 0, Pol );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_OblDeref()

void Pdr_OblDeref ( Pdr_Obl_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 556 of file pdrUtil.c.

{
    if ( --p->nRefs == 0 )
    {
        if ( p->pNext )
            Pdr_OblDeref( p->pNext );
        Pdr_SetDeref( p->pState );
        ABC_FREE( p );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_OblRef()

Pdr_Obl_t * Pdr_OblRef ( Pdr_Obl_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 539 of file pdrUtil.c.

{
    p->nRefs++;
    return p;
}

Here is the caller graph for this function:

Pdr_OblStart()

Pdr_Obl_t * Pdr_OblStart ( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 515 of file pdrUtil.c.

{
    Pdr_Obl_t * p;
    p = ABC_ALLOC( Pdr_Obl_t, 1 );
    p->iFrame = k;
    p->prio   = prio;
    p->nRefs  = 1;
    p->pState = pState;
    p->pNext  = pNext;
    p->pLink  = NULL;
    return p;    
}

Here is the caller graph for this function:

Pdr_QueueClean()

void Pdr_QueueClean ( Pdr_Man_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 632 of file pdrUtil.c.

{
    Pdr_Obl_t * pThis;
    while ( (pThis = Pdr_QueuePop(p)) )
        Pdr_OblDeref( pThis );
    pThis = NULL;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_QueueHead()

Pdr_Obl_t * Pdr_QueueHead ( Pdr_Man_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 594 of file pdrUtil.c.

{
    return p->pQueue;
}

Here is the caller graph for this function:

Pdr_QueueIsEmpty()

int Pdr_QueueIsEmpty ( Pdr_Man_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 578 of file pdrUtil.c.

{
    return p->pQueue == NULL;
}

Here is the caller graph for this function:

Pdr_QueuePop()

Pdr_Obl_t * Pdr_QueuePop ( Pdr_Man_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 610 of file pdrUtil.c.

{
    Pdr_Obl_t * pRes = p->pQueue;
    if ( p->pQueue == NULL )
        return NULL;
    p->pQueue = p->pQueue->pLink;
    Pdr_OblDeref( pRes );
    p->nQueCur--;
    return pRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_QueuePrint()

void Pdr_QueuePrint ( Pdr_Man_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 681 of file pdrUtil.c.

{
    Pdr_Obl_t * pObl;
    for ( pObl = p->pQueue; pObl; pObl = pObl->pLink )
        Abc_Print( 1, "Frame = %2d.  Prio = %8d.\n", pObl->iFrame, pObl->prio );
}

Pdr_QueuePush()

void Pdr_QueuePush ( Pdr_Man_t * p, Pdr_Obl_t * pObl )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 651 of file pdrUtil.c.

{
    Pdr_Obl_t * pTemp, ** ppPrev;
    p->nObligs++;
    p->nQueCur++;
    p->nQueMax = Abc_MaxInt( p->nQueMax, p->nQueCur );
    Pdr_OblRef( pObl );
    if ( p->pQueue == NULL )
    {
        p->pQueue = pObl;
        return;
    }
    for ( ppPrev = &p->pQueue, pTemp = p->pQueue; pTemp; ppPrev = &pTemp->pLink, pTemp = pTemp->pLink )
        if ( pTemp->iFrame > pObl->iFrame || (pTemp->iFrame == pObl->iFrame && pTemp->prio > pObl->prio) )
            break;
    *ppPrev = pObl;
    pObl->pLink = pTemp;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_QueueStop()

void Pdr_QueueStop ( Pdr_Man_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 699 of file pdrUtil.c.

{
    Pdr_Obl_t * pObl;
    while ( !Pdr_QueueIsEmpty(p) )
    {
        pObl = Pdr_QueuePop(p);
        Pdr_OblDeref( pObl );
    }
    p->pQueue = NULL;
    p->nQueCur = 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pdr_SetAlloc()

Pdr_Set_t * Pdr_SetAlloc ( int nSize )

extern

DECLARATIONS ///.

CFile****************************************************************

FileName [pdrUtil.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [Various utilities.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

pdrUtil.c,v 1.00 2010/11/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file pdrUtil.c.

{
    Pdr_Set_t * p;
    assert( nSize >= 0 && nSize < (1<<30) );
    p = (Pdr_Set_t *)ABC_CALLOC( char, sizeof(Pdr_Set_t) + nSize * sizeof(int) );
    return p;
}

Pdr_SetCompare()

int Pdr_SetCompare ( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 485 of file pdrUtil.c.

{
    Pdr_Set_t * p1 = *pp1;
    Pdr_Set_t * p2 = *pp2;
    int i;
    for ( i = 0; i < p1->nLits && i < p2->nLits; i++ )
    {
        if ( p1->Lits[i] > p2->Lits[i] )
            return -1;
        if ( p1->Lits[i] < p2->Lits[i] )
            return 1;
    }
    if ( i == p1->nLits && i < p2->nLits )
        return -1;
    if ( i < p1->nLits && i == p2->nLits )
        return 1;
    return 0;
}

Here is the caller graph for this function:

Pdr_SetContains()

int Pdr_SetContains ( Pdr_Set_t * pOld, Pdr_Set_t * pNew )

extern

Function*************************************************************

Synopsis [Return 1 if pOld set-theoretically contains pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 382 of file pdrUtil.c.

{
    int * pOldInt, * pNewInt;
    assert( pOld->nLits > 0 );
    assert( pNew->nLits > 0 );
    if ( pOld->nLits < pNew->nLits )
        return 0;
    if ( (pOld->Sign & pNew->Sign) != pNew->Sign )
        return 0;
    pOldInt = pOld->Lits + pOld->nLits - 1;
    pNewInt = pNew->Lits + pNew->nLits - 1;
    while ( pNew->Lits <= pNewInt )
    {
        if ( pOld->Lits > pOldInt )
            return 0;
        assert( *pNewInt != -1 );
        assert( *pOldInt != -1 );
        if ( *pNewInt == *pOldInt )
            pNewInt--, pOldInt--;
        else if ( *pNewInt < *pOldInt )
            pOldInt--;
        else
            return 0;
    }
    return 1;
}

Here is the caller graph for this function:

Pdr_SetContainsSimple()

int Pdr_SetContainsSimple ( Pdr_Set_t * pOld, Pdr_Set_t * pNew )

extern

Function*************************************************************

Synopsis [Return 1 if pOld set-theoretically contains pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 420 of file pdrUtil.c.

{
    int * pOldInt, * pNewInt;
    assert( pOld->nLits > 0 );
    assert( pNew->nLits > 0 );
    pOldInt = pOld->Lits + pOld->nLits - 1;
    pNewInt = pNew->Lits + pNew->nLits - 1;
    while ( pNew->Lits <= pNewInt )
    {
        assert( *pOldInt != -1 );
        if ( *pNewInt == -1 )
        {
            pNewInt--;
            continue;
        }
        if ( pOld->Lits > pOldInt )
            return 0;
        assert( *pNewInt != -1 );
        assert( *pOldInt != -1 );
        if ( *pNewInt == *pOldInt )
            pNewInt--, pOldInt--;
        else if ( *pNewInt < *pOldInt )
            pOldInt--;
        else
            return 0;
    }
    return 1;
}

Pdr_SetCreate()

Pdr_Set_t * Pdr_SetCreate ( Vec_Int_t * vLits, Vec_Int_t * vPiLits )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file pdrUtil.c.

{
    Pdr_Set_t * p;
    int i;
    assert( Vec_IntSize(vLits) + Vec_IntSize(vPiLits) < (1<<30) );
    p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (Vec_IntSize(vLits) + Vec_IntSize(vPiLits)) * sizeof(int) );
    p->nLits  = Vec_IntSize(vLits);
    p->nTotal = Vec_IntSize(vLits) + Vec_IntSize(vPiLits);
    p->nRefs  = 1;
    p->Sign   = 0;
    for ( i = 0; i < p->nLits; i++ )
    {
        p->Lits[i] = Vec_IntEntry(vLits, i);
        p->Sign   |= ((word)1 << (p->Lits[i] % 63));
    }
    Vec_IntSelectSort( p->Lits, p->nLits );
    // remember PI literals 
    for ( i = p->nLits; i < p->nTotal; i++ )
        p->Lits[i] = Vec_IntEntry(vPiLits, i-p->nLits);
    return p;
}

Here is the caller graph for this function:

Pdr_SetCreateFrom()

Pdr_Set_t * Pdr_SetCreateFrom ( Pdr_Set_t * pSet, int iRemove )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file pdrUtil.c.

{
    Pdr_Set_t * p;
    int i, k = 0;
    assert( iRemove >= 0 && iRemove < pSet->nLits );
    p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (pSet->nTotal - 1) * sizeof(int) );
    p->nLits  = pSet->nLits - 1;
    p->nTotal = pSet->nTotal - 1;
    p->nRefs  = 1;
    p->Sign   = 0;
    for ( i = 0; i < pSet->nTotal; i++ )
    {
        if ( i == iRemove )
            continue;
        p->Lits[k++] = pSet->Lits[i];
        if ( i >= pSet->nLits )
            continue;
        p->Sign   |= ((word)1 << (pSet->Lits[i] % 63));
    }
    assert( k == p->nTotal );
    return p;
}

Here is the caller graph for this function:

Pdr_SetCreateSubset()

Pdr_Set_t * Pdr_SetCreateSubset ( Pdr_Set_t * pSet, int * pLits, int nLits )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 132 of file pdrUtil.c.

{
    Pdr_Set_t * p;
    int i, k = 0;
    assert( nLits >= 0 && nLits <= pSet->nLits );
    p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (nLits + pSet->nTotal - pSet->nLits) * sizeof(int) );
    p->nLits  = nLits;
    p->nTotal = nLits + pSet->nTotal - pSet->nLits;
    p->nRefs  = 1;
    p->Sign   = 0;
    for ( i = 0; i < nLits; i++ )
    {
        assert( pLits[i] >= 0 );
        p->Lits[k++] = pLits[i];
        p->Sign   |= ((word)1 << (pLits[i] % 63));
    }
    Vec_IntSelectSort( p->Lits, p->nLits );
    for ( i = pSet->nLits; i < pSet->nTotal; i++ )
        p->Lits[k++] = pSet->Lits[i];
    assert( k == p->nTotal );
    return p;
}

Here is the caller graph for this function:

Pdr_SetDeref()

void Pdr_SetDeref ( Pdr_Set_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file pdrUtil.c.

{
    if ( --p->nRefs == 0 )
        ABC_FREE( p );
}

Here is the caller graph for this function:

Pdr_SetDup()

Pdr_Set_t * Pdr_SetDup ( Pdr_Set_t * pSet )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 166 of file pdrUtil.c.

{
    Pdr_Set_t * p;
    int i;
    p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + pSet->nTotal * sizeof(int) );
    p->nLits  = pSet->nLits;
    p->nTotal = pSet->nTotal;
    p->nRefs  = 1;
    p->Sign   = pSet->Sign;
    for ( i = 0; i < pSet->nTotal; i++ )
        p->Lits[i] = pSet->Lits[i];
    return p;
}

Here is the caller graph for this function:

Pdr_SetIsInit()

int Pdr_SetIsInit ( Pdr_Set_t * pCube, int iRemove )

extern

Function*************************************************************

Synopsis [Return 1 if the state cube contains init state (000...0).]

Description []

SideEffects []

SeeAlso []

Definition at line 460 of file pdrUtil.c.

{
    int i;
    for ( i = 0; i < pCube->nLits; i++ )
    {
        assert( pCube->Lits[i] != -1 );
        if ( i == iRemove )
            continue;
        if ( Abc_LitIsCompl( pCube->Lits[i] ) == 0 )
            return 0;
    }
    return 1;
}

Here is the caller graph for this function:

Pdr_SetPrint()

void Pdr_SetPrint ( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 225 of file pdrUtil.c.

{
    char * pBuff;
    int i, k, Entry;
    pBuff = ABC_ALLOC( char, nRegs + 1 );
    for ( i = 0; i < nRegs; i++ )
        pBuff[i] = '-';
    pBuff[i] = 0;
    for ( i = 0; i < p->nLits; i++ )
    {
        if ( p->Lits[i] == -1 )
            continue;
        pBuff[Abc_Lit2Var(p->Lits[i])] = (Abc_LitIsCompl(p->Lits[i])? '0':'1');
    }
    if ( vFlopCounts )
    {
        // skip some literals
        k = 0;
        Vec_IntForEachEntry( vFlopCounts, Entry, i )
            if ( Entry ) 
                pBuff[k++] = pBuff[i];
        pBuff[k] = 0;
    }
    fprintf( pFile, "%s", pBuff );
    ABC_FREE( pBuff );
}

Here is the caller graph for this function:

Pdr_SetPrintStr()

void Pdr_SetPrintStr ( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 342 of file pdrUtil.c.

{
    char * pBuff;
    int i, k = 0, Entry;
    pBuff = ABC_ALLOC( char, nRegs + 1 );
    for ( i = 0; i < nRegs; i++ )
        pBuff[i] = '-';
    pBuff[i] = 0;
    for ( i = 0; i < p->nLits; i++ )
    {
        if ( p->Lits[i] == -1 )
            continue;
        pBuff[Abc_Lit2Var(p->Lits[i])] = (Abc_LitIsCompl(p->Lits[i])? '0':'1');
    }
    if ( vFlopCounts )
    {
        // skip some literals
        Vec_IntForEachEntry( vFlopCounts, Entry, i )
            if ( Entry ) 
                pBuff[k++] = pBuff[i];
        pBuff[k] = 0;
    }
    Vec_StrPushBuffer( vStr, pBuff, k );
    Vec_StrPush( vStr, ' ' );
    Vec_StrPush( vStr, '1' );
    Vec_StrPush( vStr, '\n' );
    ABC_FREE( pBuff );
}

Here is the caller graph for this function:

Pdr_SetRef()

Pdr_Set_t * Pdr_SetRef ( Pdr_Set_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 191 of file pdrUtil.c.

{
    p->nRefs++;
    return p;
}

Txs3_ManStart()

Txs3_Man_t * Txs3_ManStart ( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio )

extern

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Start and stop the ternary simulation engine.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file pdrTsim3.c.

{
    Txs3_Man_t * p;
//    Aig_Obj_t * pObj;
//    int i;
    assert( Vec_IntSize(vPrio) == Aig_ManRegNum(pAig) );
    p = ABC_CALLOC( Txs3_Man_t, 1 );
    p->pGia    = Gia_ManFromAigSimple(pAig); // user's AIG
//    Aig_ManForEachObj( pAig, pObj, i )
//        assert( i == 0 || pObj->iData == Abc_Var2Lit(i, 0) );
    p->vPrio   = vPrio;                // priority of each flop
    p->vCiObjs = Vec_IntAlloc( 100 );  // cone leaves (CI obj IDs)
    p->vFosPre = Vec_IntAlloc( 100 );  // present flop outputs
    p->vFosAbs = Vec_IntAlloc( 100 );  // absracted flop outputs
    p->vCoObjs = Vec_IntAlloc( 100 );  // cone roots (CO obj IDs)
    p->vCiVals = Vec_IntAlloc( 100 );  // cone leaf values (0/1 CI values)
    p->vCoVals = Vec_IntAlloc( 100 );  // cone root values (0/1 CO values)
    p->vNodes  = Vec_IntAlloc( 100 );  // cone nodes (node obj IDs)
    p->vTemp   = Vec_IntAlloc( 100 );  // cone nodes (node obj IDs)
    p->vPiLits = Vec_IntAlloc( 100 );  // resulting array of PI literals
    p->vFfLits = Vec_IntAlloc( 100 );  // resulting array of flop literals
    p->pMan    = pMan;                 // calling manager
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Txs3_ManStop()

void Txs3_ManStop ( Txs3_Man_t * p )

extern

Definition at line 87 of file pdrTsim3.c.

{
    Gia_ManStop( p->pGia );
    Vec_IntFree( p->vCiObjs );
    Vec_IntFree( p->vFosPre );
    Vec_IntFree( p->vFosAbs );
    Vec_IntFree( p->vCoObjs );
    Vec_IntFree( p->vCiVals );
    Vec_IntFree( p->vCoVals );
    Vec_IntFree( p->vNodes );
    Vec_IntFree( p->vTemp );
    Vec_IntFree( p->vPiLits );
    Vec_IntFree( p->vFfLits );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Txs3_ManTernarySim()

Pdr_Set_t * Txs3_ManTernarySim ( Txs3_Man_t * p, int k, Pdr_Set_t * pCube )

extern

Function*************************************************************

Synopsis [Shrinks values using ternary simulation.]

Description [The cube contains the set of flop index literals which, when converted into a clause and applied to the combinational outputs, led to a satisfiable SAT run in frame k (values stored in the SAT solver). If the cube is NULL, it is assumed that the first property output was asserted and failed. The resulting array is a set of flop index literals that asserts the COs. Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]

SideEffects []

SeeAlso []

Definition at line 188 of file pdrTsim3.c.

{
//    int fTryNew = 1;
//    int fUseLit = 1;
    int fVerbose = 0;
    sat_solver * pSat;
    Pdr_Set_t * pRes;
    Gia_Obj_t * pObj;
    Vec_Int_t * vVar2Ids, * vLits;
    int i, Lit, LitAux, Var, Value, RetValue, nCoreLits, * pCoreLits;//, nLits;
//    if ( k == 0 )
//        fVerbose = 1;
    // collect CO objects
    Vec_IntClear( p->vCoObjs );
    if ( pCube == NULL ) // the target is the property output
    {
        pObj = Gia_ManCo(p->pGia, p->pMan->iOutCur);
        Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
    }
    else // the target is the cube
    {
        int i;
        for ( i = 0; i < pCube->nLits; i++ )
        {
            if ( pCube->Lits[i] == -1 )
                continue;
            pObj = Gia_ManCo(p->pGia, Gia_ManPoNum(p->pGia) + Abc_Lit2Var(pCube->Lits[i]));
            Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
        }
    }
if ( 0 )
{
Abc_Print( 1, "Trying to justify cube " );
if ( pCube )
    Pdr_SetPrint( stdout, pCube, Gia_ManRegNum(p->pGia), NULL );
else
    Abc_Print( 1, "<prop=fail>" );
Abc_Print( 1, " in frame %d.\n", k );
}
 
    // collect CI objects
    Txs3_ManCollectCone( p, fVerbose );
    // collect values
    Pdr_ManCollectValues( p->pMan, k, p->vCiObjs, p->vCiVals );
    Pdr_ManCollectValues( p->pMan, k, p->vCoObjs, p->vCoVals );
 
    // read solver
    pSat = Pdr_ManFetchSolver( p->pMan, k );
    LitAux = Abc_Var2Lit( Pdr_ManFreeVar(p->pMan, k), 0 );
    // add the clause (complemented cube) in terms of next state variables
    if ( pCube == NULL ) // the target is the property output
    {
        vLits = p->pMan->vLits;
        Lit = Abc_Var2Lit( Pdr_ObjSatVar(p->pMan, k, 2, Aig_ManCo(p->pMan->pAig, p->pMan->iOutCur)), 1 ); // neg literal (property holds)
        Vec_IntFill( vLits, 1, Lit );
    }
    else
        vLits = Pdr_ManCubeToLits( p->pMan, k, pCube, 1, 1 );
    // add activation literal
    Vec_IntPush( vLits, LitAux );
    RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
    assert( RetValue == 1 );
    sat_solver_compress( pSat );
 
    // collect assumptions 
    Vec_IntClear( p->vTemp );
    Vec_IntPush( p->vTemp, Abc_LitNot(LitAux) );
    // iterate through the values of the CI variables
    Vec_IntForEachEntryTwo( p->vCiObjs, p->vCiVals, Var, Value, i )
    {
        Aig_Obj_t * pObj = Aig_ManObj( p->pMan->pAig, Var );
//        iVar = Pdr_ObjSatVar( p->pMan, k, fNext ? 2 - lit_sign(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
        int iVar = Pdr_ObjSatVar( p->pMan, k, 3, pObj ); assert( iVar >= 0 );
        assert( Aig_ObjIsCi(pObj) );
        Vec_IntPush( p->vTemp, Abc_Var2Lit(iVar, !Value) );
    }
    if ( fVerbose )
    {
        printf( "Clause with %d lits on lev %d\n", pCube ? pCube->nLits : 0, k );
        Vec_IntPrint( p->vTemp );
    }
 
/*
    // solve with assumptions
//printf( "%d -> ", Vec_IntSize(p->vTemp) );
{
abctime clk = Abc_Clock();
// assume all except flops
    Vec_IntForEachEntryStop( p->vTemp, Lit, i, p->nPiLits + 1 )
        if ( !sat_solver_push(pSat, Lit) )
        {
            assert( 0 );
        }
    nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(p->vTemp) + p->nPiLits + 1, Vec_IntSize(p->vTemp) - p->nPiLits - 1, p->pMan->pPars->nConfLimit );
    Vec_IntShrink( p->vTemp, p->nPiLits + 1 + nLits );
 
p->pMan->tAbs += Abc_Clock() - clk;
    for ( i = 0; i <= p->nPiLits; i++ )
        sat_solver_pop(pSat);
}
//printf( "%d    ", nLits );
*/
 
 
    //check one last time
    RetValue = sat_solver_solve( pSat, Vec_IntArray(p->vTemp), Vec_IntLimit(p->vTemp), 0, 0, 0, 0 );
    assert( RetValue == l_False );
 
    // use analyze final
    nCoreLits = sat_solver_final(pSat, &pCoreLits);
    //assert( Vec_IntSize(p->vTemp) <= nCoreLits );
 
    Vec_IntClear( p->vTemp );
    for ( i = 0; i < nCoreLits; i++ )
        Vec_IntPush( p->vTemp, Abc_LitNot(pCoreLits[i]) );
    Vec_IntSelectSort( Vec_IntArray(p->vTemp), Vec_IntSize(p->vTemp) );
 
    if ( fVerbose )
        Vec_IntPrint( p->vTemp );
 
    // collect the resulting sets
    Vec_IntClear( p->vPiLits );
    Vec_IntClear( p->vFfLits );
    vVar2Ids = (Vec_Int_t *)Vec_PtrGetEntry( &p->pMan->vVar2Ids, k );
    Vec_IntForEachEntry( p->vTemp, Lit, i )
    {
        if ( Lit != Abc_LitNot(LitAux) )
        {
            int Id = Vec_IntEntry( vVar2Ids, Abc_Lit2Var(Lit) );
            Aig_Obj_t * pObj = Aig_ManObj( p->pMan->pAig, Id );
            assert( Aig_ObjIsCi(pObj) );
            if ( Saig_ObjIsPi(p->pMan->pAig, pObj) )
                Vec_IntPush( p->vPiLits, Abc_Var2Lit(Aig_ObjCioId(pObj), Abc_LitIsCompl(Lit)) );
            else
                Vec_IntPush( p->vFfLits, Abc_Var2Lit(Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pMan->pAig), Abc_LitIsCompl(Lit)) );
        }
    }
    assert( Vec_IntSize(p->vTemp) == Vec_IntSize(p->vPiLits) + Vec_IntSize(p->vFfLits) + 1 );
 
    // move abstracted literals from flops to inputs
    if ( p->pMan->pPars->fUseAbs && p->pMan->vAbsFlops )
    {
        int i, iLit, k = 0;
        Vec_IntForEachEntry( p->vFfLits, iLit, i )
        {
            if ( Vec_IntEntry(p->pMan->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop
                Vec_IntWriteEntry( p->vFfLits, k++, iLit );
            else
                Vec_IntPush( p->vPiLits, 2*Saig_ManPiNum(p->pMan->pAig) + iLit );
        }
        Vec_IntShrink( p->vFfLits, k );
    }
 
    if ( fVerbose )
        Vec_IntPrint( p->vPiLits );
    if ( fVerbose )
        Vec_IntPrint( p->vFfLits );
    if ( fVerbose )
        printf( "\n" );
 
    // derive the final set
    pRes = Pdr_SetCreate( p->vFfLits, p->vPiLits );
    //ZH: Disabled assertion because this invariant doesn't hold with down
    //because of the join operation which can bring in initial states
    assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
    return pRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Txs_ManStart()

Txs_Man_t * Txs_ManStart ( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio )

extern

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Start and stop the ternary simulation engine.]

Description []

SideEffects []

SeeAlso []

Definition at line 60 of file pdrTsim2.c.

{
    Txs_Man_t * p;
//    Aig_Obj_t * pObj;
//    int i;
    assert( Vec_IntSize(vPrio) == Aig_ManRegNum(pAig) );
    p = ABC_CALLOC( Txs_Man_t, 1 );
    p->pGia    = Gia_ManFromAigSimple(pAig); // user's AIG
//    Aig_ManForEachObj( pAig, pObj, i )
//        assert( i == 0 || pObj->iData == Abc_Var2Lit(i, 0) );
    p->vPrio   = vPrio;                // priority of each flop
    p->vCiObjs = Vec_IntAlloc( 100 );  // cone leaves (CI obj IDs)
    p->vCoObjs = Vec_IntAlloc( 100 );  // cone roots (CO obj IDs)
    p->vCiVals = Vec_IntAlloc( 100 );  // cone leaf values (0/1 CI values)
    p->vCoVals = Vec_IntAlloc( 100 );  // cone root values (0/1 CO values)
    p->vNodes  = Vec_IntAlloc( 100 );  // cone nodes (node obj IDs)
    p->vTemp   = Vec_IntAlloc( 100 );  // cone nodes (node obj IDs)
    p->vPiLits = Vec_IntAlloc( 100 );  // resulting array of PI literals
    p->vFfLits = Vec_IntAlloc( 100 );  // resulting array of flop literals
    p->pMan    = pMan;                 // calling manager
    return p;
}

Here is the call graph for this function:

Txs_ManStop()

void Txs_ManStop ( Txs_Man_t * p )

extern

Definition at line 82 of file pdrTsim2.c.

{
    Gia_ManStop( p->pGia );
    Vec_IntFree( p->vCiObjs );
    Vec_IntFree( p->vCoObjs );
    Vec_IntFree( p->vCiVals );
    Vec_IntFree( p->vCoVals );
    Vec_IntFree( p->vNodes );
    Vec_IntFree( p->vTemp );
    Vec_IntFree( p->vPiLits );
    Vec_IntFree( p->vFfLits );
    ABC_FREE( p );
}

Here is the call graph for this function:

Txs_ManTernarySim()

Pdr_Set_t * Txs_ManTernarySim ( Txs_Man_t * p, int k, Pdr_Set_t * pCube )

extern

Function*************************************************************

Synopsis [Shrinks values using ternary simulation.]

Description [The cube contains the set of flop index literals which, when converted into a clause and applied to the combinational outputs, led to a satisfiable SAT run in frame k (values stored in the SAT solver). If the cube is NULL, it is assumed that the first property output was asserted and failed. The resulting array is a set of flop index literals that asserts the COs. Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]

SideEffects []

SeeAlso []

Definition at line 490 of file pdrTsim2.c.

{
    int fTryNew = 1;
    Pdr_Set_t * pRes;
    Gia_Obj_t * pObj;
    // collect CO objects
    Vec_IntClear( p->vCoObjs );
    if ( pCube == NULL ) // the target is the property output
    {
        pObj = Gia_ManCo(p->pGia, p->pMan->iOutCur);
        Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
    }
    else // the target is the cube
    {
        int i;
        for ( i = 0; i < pCube->nLits; i++ )
        {
            if ( pCube->Lits[i] == -1 )
                continue;
            pObj = Gia_ManCo(p->pGia, Gia_ManPoNum(p->pGia) + Abc_Lit2Var(pCube->Lits[i]));
            Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
        }
    }
if ( 0 )
{
Abc_Print( 1, "Trying to justify cube " );
if ( pCube )
    Pdr_SetPrint( stdout, pCube, Gia_ManRegNum(p->pGia), NULL );
else
    Abc_Print( 1, "<prop=fail>" );
Abc_Print( 1, " in frame %d.\n", k );
}
 
    // collect CI objects
    Txs_ManCollectCone( p->pGia, p->vCoObjs, p->vCiObjs, p->vNodes );
    // collect values
    Pdr_ManCollectValues( p->pMan, k, p->vCiObjs, p->vCiVals );
    Pdr_ManCollectValues( p->pMan, k, p->vCoObjs, p->vCoVals );
 
    // perform two passes
    Txs_ManForwardPass( p->pGia, p->vPrio, p->vCiObjs, p->vCiVals, p->vNodes, p->vCoObjs, p->vCoVals );
    if ( fTryNew )
        Txs_ManFindCiReduction( p->pGia, p->vPrio, p->vCiObjs, p->vNodes, p->vCoObjs, p->vPiLits, p->vFfLits, p->vTemp );
    else
        Txs_ManBackwardPass( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits );
    Txs_ManVerify( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits, p->vCoObjs, p->vCoVals );
 
    // derive the final set
    pRes = Pdr_SetCreate( p->vFfLits, p->vPiLits );
    //ZH: Disabled assertion because this invariant doesn't hold with down
    //because of the join operation which can bring in initial states
    //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
    return pRes;
}

Here is the call graph for this function:

ZPdr_SetIntersection()

Pdr_Set_t * ZPdr_SetIntersection ( Pdr_Set_t * p1, Pdr_Set_t * p2, Hash_Int_t * keep )

extern

Function*************************************************************

Synopsis [Return the intersection of p1 and p2.]

Description []

SideEffects []

SeeAlso []

Definition at line 283 of file pdrUtil.c.

{
    Pdr_Set_t * pIntersection;
    Vec_Int_t * vCommonLits, * vPiLits;
    int i, j, nLits;
    nLits = p1->nLits;
    if ( p2->nLits < nLits )
        nLits = p2->nLits;
    vCommonLits = Vec_IntAlloc( nLits );
    vPiLits = Vec_IntAlloc( 1 );
    for ( i = 0, j = 0; i < p1->nLits && j < p2->nLits; )
    {
        if ( p1->Lits[i] > p2->Lits[j] )
        {
            if ( Hash_IntExists( keep, p2->Lits[j] ) )
            {
                //about to drop a literal that should not be dropped
                Vec_IntFree( vCommonLits );
                Vec_IntFree( vPiLits );
                return NULL;
            }
            j++;
        }
        else if ( p1->Lits[i] < p2->Lits[j] )
        {
            if ( Hash_IntExists( keep, p1->Lits[i] ) )
            {
                //about to drop a literal that should not be dropped
                Vec_IntFree( vCommonLits );
                Vec_IntFree( vPiLits );
                return NULL;
            }
            i++;
        }
        else
        {
          Vec_IntPush( vCommonLits, p1->Lits[i] );
          i++;
          j++;
        }
    }
    pIntersection = Pdr_SetCreate( vCommonLits, vPiLits );
    Vec_IntFree( vCommonLits );
    Vec_IntFree( vPiLits );
    return pIntersection;
}

Here is the call graph for this function:

Here is the caller graph for this function:

ZPdr_SetIsInit()

int ZPdr_SetIsInit ( Pdr_Set_t * p )

extern

ZPdr_SetPrint()

void ZPdr_SetPrint ( Pdr_Set_t * p )

extern

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 263 of file pdrUtil.c.

{
    int i;
    for ( i = 0; i < p->nLits; i++)
        printf ("%d ", p->Lits[i]);
    printf ("\n");
 
}

Here is the caller graph for this function: