pdrCnf.c File Reference

#include "pdrInt.h"

Include dependency graph for pdrCnf.c:

Go to the source code of this file.

Functions
int	Pdr_ObjSatVar2 (Pdr_Man_t *p, int k, Aig_Obj_t *pObj, int Level, int Pol)
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)

Function Documentation

Pdr_ManFreeVar()

int Pdr_ManFreeVar	(	Pdr_Man_t *	p,
		int	k )

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_ManNewSolver()

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

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_ObjRegNum()

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

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 )

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_ObjSatVar2()

int Pdr_ObjSatVar2	(	Pdr_Man_t *	p,
		int	k,
		Aig_Obj_t *	pObj,
		int	Level,
		int	Pol )

Definition at line 200 of file pdrCnf.c.

{
    Vec_Int_t * vLits;
    sat_solver * pSat;
    int fNewVar = 0, iVarThis  = Pdr_ObjSatVar2FindOrAdd( p, k, pObj, &fNewVar );
    int * pLit, i, iVar, iClaBeg, iClaEnd, RetValue;
    if ( Aig_ObjIsCi(pObj) || !fNewVar )
        return iVarThis;
    iClaBeg = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)];
    iClaEnd = iClaBeg + p->pCnf2->pObj2Count[Aig_ObjId(pObj)];
    assert( iClaBeg < iClaEnd );
    pSat = Pdr_ManSolver(p, k);
    vLits = Vec_WecEntry( p->vVLits, Level );
    for ( i = iClaBeg; i < iClaEnd; i++ )
    {
        Vec_IntClear( vLits );
        Vec_IntPush( vLits, Abc_Var2Lit( iVarThis, Abc_LitIsCompl(p->pCnf2->pClauses[i][0]) ) );
        for ( pLit = p->pCnf2->pClauses[i]+1; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
        {
            iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, Abc_Lit2Var(*pLit)), Level+1, Pol );
            Vec_IntPush( vLits, Abc_Var2Lit( iVar, Abc_LitIsCompl(*pLit) ) );
        }
        RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
        assert( RetValue );
        (void) RetValue;
    }
    return iVarThis;
}

Here is the call graph for this function:

Here is the caller graph for this function: