SVF::BddCondManager Class Reference

#include <Conditions.h>

Public Member Functions
	BddCondManager ()
	Constructor. More...
	~BddCondManager ()
	Destructor. More...
DdNode *	Cudd_bdd (u32_t i)
unsigned	BddVarNum ()
DdNode *	getTrueCond () const
DdNode *	getFalseCond () const
u32_t	getBDDMemUsage ()
u32_t	getCondNumber ()
u32_t	getMaxLiveCondNumber ()
void	markForRelease (DdNode *cond)
void	ddClearFlag (DdNode *f) const
void	BddSupportStep (DdNode *f, NodeBS &support) const
void	BddSupport (DdNode *f, NodeBS &support) const
void	dump (DdNode *lhs, raw_ostream &O)
std::string	dumpStr (DdNode *lhs) const
void	printMinterms (DdNode *d)
	print minterms and debug information for the Ddnode More...
void	printDbg (DdNode *d)
DdNode *	AND (DdNode *lhs, DdNode *rhs)
	Operations on conditions. More...
DdNode *	OR (DdNode *lhs, DdNode *rhs)
DdNode *	NEG (DdNode *lhs)

Private Member Functions
DdNode *	BddOne () const
DdNode *	BddZero () const

Private Attributes
DdManager *	m_bdd_mgr

Detailed Description

Using Cudd as conditions.

Definition at line 43 of file Conditions.h.

Constructor & Destructor Documentation

BddCondManager()

SVF::BddCondManager::BddCondManager ( )

inline

Constructor.

Definition at line 48 of file Conditions.h.

    {
        m_bdd_mgr = Cudd_Init(0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
    }

~BddCondManager()

SVF::BddCondManager::~BddCondManager ( )

inline

Destructor.

Definition at line 54 of file Conditions.h.

    {
        Cudd_Quit(m_bdd_mgr);
    }

Member Function Documentation

AND()

DdNode * BddCondManager::AND	(	DdNode *	lhs,
		DdNode *	rhs
	)

Operations on conditions.

use Cudd_bddAndLimit interface to avoid bdds blow up

drop the rhs condition

Definition at line 40 of file Conditions.cpp.

{
    if (lhs == getFalseCond() || rhs == getFalseCond())
        return getFalseCond();
    else if (lhs == getTrueCond())
        return rhs;
    else if (rhs == getTrueCond())
        return lhs;
    else
    {
        DdNode* tmp = Cudd_bddAndLimit(m_bdd_mgr, lhs, rhs, Options::MaxBddSize);
        if(tmp==nullptr)
        {
            SVFUtil::writeWrnMsg("exceeds max bdd size \n");
            return lhs;
        }
        else
        {
            Cudd_Ref(tmp);
            return tmp;
        }
    }
}

BddOne()

DdNode* SVF::BddCondManager::BddOne ( ) const

inlineprivate

Definition at line 119 of file Conditions.h.

    {
        return Cudd_ReadOne(m_bdd_mgr);
    }

BddSupport()

void BddCondManager::BddSupport	(	DdNode *	f,
		NodeBS &	support
	)		const

Definition at line 134 of file Conditions.cpp.

{
    BddSupportStep( Cudd_Regular(f), support);
    ddClearFlag(Cudd_Regular(f));
}

BddSupportStep()

void BddCondManager::BddSupportStep	(	DdNode *	f,
		NodeBS &	support
	)		const

Definition at line 121 of file Conditions.cpp.

{
    if (cuddIsConstant(f) || Cudd_IsComplement(f->next))
        return;

    support.set(f->index);

    BddSupportStep(cuddT(f), support);
    BddSupportStep(Cudd_Regular(cuddE(f)), support);
    /* Mark as visited. */
    f->next = Cudd_Complement(f->next);
}

BddVarNum()

unsigned SVF::BddCondManager::BddVarNum ( )

inline

Definition at line 63 of file Conditions.h.

    {
        return Cudd_ReadSize(m_bdd_mgr);
    }

BddZero()

DdNode* SVF::BddCondManager::BddZero ( ) const

inlineprivate

Definition at line 123 of file Conditions.h.

    {
        return Cudd_ReadLogicZero(m_bdd_mgr);
    }

Cudd_bdd()

DdNode* SVF::BddCondManager::Cudd_bdd ( u32_t  i )

inline

Definition at line 59 of file Conditions.h.

    {
        return Cudd_bddIthVar(m_bdd_mgr, i);
    }

ddClearFlag()

void BddCondManager::ddClearFlag

(

DdNode *

f

)

const

Utilities for dumping conditions. These methods use global functions from CUDD package and they can be removed outside this class scope to be used by others.

Definition at line 108 of file Conditions.cpp.

{
    if (!Cudd_IsComplement(f->next))
        return;
    /* Clear visited flag. */
    f->next = Cudd_Regular(f->next);
    if (cuddIsConstant(f))
        return;
    ddClearFlag(cuddT(f));
    ddClearFlag(Cudd_Regular(cuddE(f)));
    return;
}

dump()

void BddCondManager::dump	(	DdNode *	lhs,
		raw_ostream &	O
	)

Dump BDD

Definition at line 143 of file Conditions.cpp.

{
    if (lhs == getTrueCond())
        O << "T";
    else
    {
        NodeBS support;
        BddSupport(lhs, support);
        for (NodeBS::iterator iter = support.begin(); iter != support.end();
                ++iter)
        {
            unsigned rid = *iter;
            O << rid << " ";
        }
    }
}

dumpStr()

std::string BddCondManager::dumpStr

(

DdNode *

lhs

)

const

Dump BDD

Definition at line 163 of file Conditions.cpp.

{
    std::string str;
    if (lhs == getTrueCond())
        str += "T";
    else
    {
        NodeBS support;
        BddSupport(lhs, support);
        for (NodeBS::iterator iter = support.begin(); iter != support.end();
                ++iter)
        {
            unsigned rid = *iter;
            char int2str[16];
            sprintf(int2str, "%d", rid);
            str += int2str;
            str += " ";
        }
    }
    return str;
}

getBDDMemUsage()

u32_t SVF::BddCondManager::getBDDMemUsage ( )

inline

Definition at line 77 of file Conditions.h.

    {
        return Cudd_ReadMemoryInUse(m_bdd_mgr);
    }

getCondNumber()

u32_t SVF::BddCondManager::getCondNumber ( )

inline

Definition at line 81 of file Conditions.h.

    {
        return Cudd_ReadNodeCount(m_bdd_mgr);
    }

getFalseCond()

DdNode* SVF::BddCondManager::getFalseCond ( ) const

inline

Definition at line 72 of file Conditions.h.

    {
        return BddZero();
    }

getMaxLiveCondNumber()

u32_t SVF::BddCondManager::getMaxLiveCondNumber ( )

inline

Definition at line 85 of file Conditions.h.

    {
        return Cudd_ReadPeakLiveNodeCount(m_bdd_mgr);
    }

getTrueCond()

DdNode* SVF::BddCondManager::getTrueCond ( ) const

inline

Definition at line 68 of file Conditions.h.

    {
        return BddOne();
    }

markForRelease()

void SVF::BddCondManager::markForRelease ( DdNode *  cond )

inline

Definition at line 89 of file Conditions.h.

    {
        Cudd_RecursiveDeref(m_bdd_mgr,cond);
    }

NEG()

DdNode * BddCondManager::NEG

(

DdNode *

lhs

)

Definition at line 93 of file Conditions.cpp.

{
    if (lhs == getTrueCond())
        return getFalseCond();
    else if (lhs == getFalseCond())
        return getTrueCond();
    else
        return Cudd_Not(lhs);
}

OR()

DdNode * BddCondManager::OR	(	DdNode *	lhs,
		DdNode *	rhs
	)

Use Cudd_bddOrLimit interface to avoid bdds blow up

drop the two conditions here

Definition at line 68 of file Conditions.cpp.

{
    if (lhs == getTrueCond() || rhs == getTrueCond())
        return getTrueCond();
    else if (lhs == getFalseCond())
        return rhs;
    else if (rhs == getFalseCond())
        return lhs;
    else
    {
        DdNode* tmp = Cudd_bddOrLimit(m_bdd_mgr, lhs, rhs, Options::MaxBddSize);
        if(tmp==nullptr)
        {
            SVFUtil::writeWrnMsg("exceeds max bdd size \n");
            return getTrueCond();
        }
        else
        {
            Cudd_Ref(tmp);
            return tmp;
        }
    }
}

printDbg()

void SVF::BddCondManager::printDbg ( DdNode *  d )

inline

Definition at line 114 of file Conditions.h.

    {
        Cudd_PrintDebug(m_bdd_mgr,d,0,3);
    }

printMinterms()

void SVF::BddCondManager::printMinterms ( DdNode *  d )

inline

print minterms and debug information for the Ddnode

Definition at line 110 of file Conditions.h.

    {
        Cudd_PrintMinterm(m_bdd_mgr,d);
    }

Member Data Documentation

m_bdd_mgr

DdManager* SVF::BddCondManager::m_bdd_mgr

private

Definition at line 128 of file Conditions.h.

---

The documentation for this class was generated from the following files:

• /home/runner/work/SVF-1/SVF-1/include/Util/Conditions.h
• /home/runner/work/SVF-1/SVF-1/lib/Util/Conditions.cpp