pdrCnf.c File Reference

#include "pdrInt.h"

Go to the source code of this file.

Functions
static ABC_NAMESPACE_IMPL_START int	Pdr_ObjSatVar1 (Pdr_Man_t *p, int k, Aig_Obj_t *pObj)
	DECLARATIONS ///. More...
static int	Pdr_ObjSatVar2FindOrAdd (Pdr_Man_t *p, int k, Aig_Obj_t *pObj, int *pfNewVar)
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)
static int	Pdr_ObjRegNum1 (Pdr_Man_t *p, int k, int iSatVar)
static int	Pdr_ObjRegNum2 (Pdr_Man_t *p, int k, int iSatVar)
int	Pdr_ObjRegNum (Pdr_Man_t *p, int k, int iSatVar)
int	Pdr_ManFreeVar (Pdr_Man_t *p, int k)
static sat_solver *	Pdr_ManNewSolver1 (sat_solver *pSat, Pdr_Man_t *p, int k, int fInit)
static sat_solver *	Pdr_ManNewSolver2 (sat_solver *pSat, Pdr_Man_t *p, int k, int fInit)
sat_solver *	Pdr_ManNewSolver (sat_solver *pSat, Pdr_Man_t *p, int k, int fInit)

Function Documentation

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

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

static sat_solver* Pdr_ManNewSolver1 ( sat_solver *  pSat, Pdr_Man_t *  p, int  k, int  fInit  )

inlinestatic

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

Synopsis [Creates SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 355 of file pdrCnf.c.

{
    Aig_Obj_t * pObj;
    int i;
    assert( pSat );
    if ( p->pCnf1 == NULL )
    {
        int nRegs = p->pAig->nRegs;
        p->pAig->nRegs = Aig_ManCoNum(p->pAig);
        p->pCnf1 = Cnf_DeriveWithMan( p->pCnfMan, p->pAig, Aig_ManCoNum(p->pAig) );
        p->pAig->nRegs = nRegs;
        assert( p->vVar2Reg == NULL );
        p->vVar2Reg = Vec_IntStartFull( p->pCnf1->nVars );
        Saig_ManForEachLi( p->pAig, pObj, i )
            Vec_IntWriteEntry( p->vVar2Reg, Pdr_ObjSatVar(p, k, 3, pObj), i );
    }
    pSat = (sat_solver *)Cnf_DataWriteIntoSolverInt( pSat, p->pCnf1, 1, fInit );
    sat_solver_set_runtime_limit( pSat, p->timeToStop );
    return pSat;
}

static sat_solver* Pdr_ManNewSolver2 ( sat_solver *  pSat, Pdr_Man_t *  p, int  k, int  fInit  )

inlinestatic

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

Synopsis [Creates SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 387 of file pdrCnf.c.

{
    Vec_Int_t * vVar2Ids;
    int i, Entry;
    assert( pSat );
    if ( p->pCnf2 == NULL )
    {
        p->pCnf2     = Cnf_DeriveOtherWithMan( p->pCnfMan, p->pAig, 0 );
#ifdef USE_PG
        p->pCnf2->pClaPols = Cnf_DataDeriveLitPolarities( p->pCnf2 );
#endif
        p->pvId2Vars = ABC_CALLOC( Vec_Int_t, Aig_ManObjNumMax(p->pAig) );
        Vec_PtrGrow( &p->vVar2Ids, 256 );
    }
    // update the variable mapping
    vVar2Ids = (Vec_Int_t *)Vec_PtrGetEntry( &p->vVar2Ids, k );
    if ( vVar2Ids == NULL )
    {
        vVar2Ids = Vec_IntAlloc( 500 );
        Vec_PtrWriteEntry( &p->vVar2Ids, k, vVar2Ids );
    }
    Vec_IntForEachEntry( vVar2Ids, Entry, i )
    {
        if ( Entry == -1 )
            continue;
        assert( Vec_IntEntry( p->pvId2Vars + Entry, k ) > 0 );
        Vec_IntWriteEntry( p->pvId2Vars + Entry, k, 0 );
    }
    Vec_IntClear( vVar2Ids );
    Vec_IntPush( vVar2Ids, -1 );
    // start the SAT solver
//    pSat = sat_solver_new();
    sat_solver_setnvars( pSat, 500 );
    sat_solver_set_runtime_limit( pSat, p->timeToStop );
    return pSat;
}

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

static int Pdr_ObjRegNum1 ( Pdr_Man_t *  p, int  k, int  iSatVar  )

inlinestatic

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 261 of file pdrCnf.c.

{
    int RegId;
    assert( iSatVar >= 0 );
    // consider the case of auxiliary variable
    if ( iSatVar >= p->pCnf1->nVars )
        return -1;
    // consider the case of register output
    RegId = Vec_IntEntry( p->vVar2Reg, iSatVar );
    assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
    return RegId;
}

static int Pdr_ObjRegNum2 ( Pdr_Man_t *  p, int  k, int  iSatVar  )

inlinestatic

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 285 of file pdrCnf.c.

{
    Aig_Obj_t * pObj;
    int ObjId;
    Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(&p->vVar2Ids, k);
    assert( iSatVar > 0 && iSatVar < Vec_IntSize(vVar2Ids) );
    ObjId = Vec_IntEntry( vVar2Ids, iSatVar );
    if ( ObjId == -1 ) // activation variable
        return -1;
    pObj = Aig_ManObj( p->pAig, ObjId );
    if ( Saig_ObjIsLi( p->pAig, pObj ) )
        return Aig_ObjCioId(pObj)-Saig_ManPoNum(p->pAig);
    assert( 0 ); // should be called for register inputs only
    return -1;
}

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

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

static ABC_NAMESPACE_IMPL_START int Pdr_ObjSatVar1 ( Pdr_Man_t *  p, int  k, Aig_Obj_t *  pObj  )

inlinestatic

DECLARATIONS ///.

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

FileName [pdrCnf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Property driven reachability.]

Synopsis [CNF computation on demand.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Returns SAT variable of the given object.]

Description []

SideEffects []

SeeAlso []

Definition at line 54 of file pdrCnf.c.

{
    return p->pCnf1->pVarNums[ Aig_ObjId(pObj) ];
}

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, toLitCond( iVarThis, lit_sign(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, lit_var(*pLit)), Level+1, Pol );
            Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
        }
        RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
        assert( RetValue );
        (void) RetValue;
    }
    return iVarThis;
}

static int Pdr_ObjSatVar2FindOrAdd ( Pdr_Man_t *  p, int  k, Aig_Obj_t *  pObj, int *  pfNewVar  )

inlinestatic

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

Synopsis [Returns SAT variable of the given object.]

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file pdrCnf.c.

{ 
    Vec_Int_t * vId2Vars = p->pvId2Vars + Aig_ObjId(pObj);
    assert( p->pCnf2->pObj2Count[Aig_ObjId(pObj)] >= 0 );
    if ( Vec_IntSize(vId2Vars) == 0 )
        Vec_IntGrow(vId2Vars, 2 * k + 1);
    if ( Vec_IntGetEntry(vId2Vars, k) == 0 )
    {
        sat_solver * pSat = Pdr_ManSolver(p, k);
        Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(&p->vVar2Ids, k);
        int iVarNew = Vec_IntSize( vVar2Ids );
        assert( iVarNew > 0 );
        Vec_IntPush( vVar2Ids, Aig_ObjId(pObj) );
        Vec_IntWriteEntry( vId2Vars, k, iVarNew );
        sat_solver_setnvars( pSat, iVarNew + 1 );
        if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output
        {
            int Lit = toLitCond( iVarNew, 1 );
            int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
            assert( RetValue == 1 );
            (void) RetValue;
            sat_solver_compress( pSat );
        }
        *pfNewVar = 1;
    }
    return Vec_IntEntry( vId2Vars, k );
}