extraBddTime.c File Reference

#include "extraBdd.h"

Include dependency graph for extraBddTime.c:

Go to the source code of this file.

Macros
#define	CHECK_FACTOR   10

Functions
DdNode *	Extra_bddAndTime (DdManager *dd, DdNode *f, DdNode *g, int TimeOut)
DdNode *	Extra_bddAndAbstractTime (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int TimeOut)
DdNode *	Extra_TransferPermuteTime (DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute, int TimeOut)

Macro Definition Documentation

CHECK_FACTOR

#define CHECK_FACTOR   10

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

FileName [extraBddTime.c]

PackageName [extra]

Synopsis [Procedures to control runtime in BDD operators.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - September 1, 2003.]

Revision [

Id

extraBddTime.c,v 1.0 2003/05/21 18:03:50 alanmi Exp

]

Definition at line 28 of file extraBddTime.c.

Function Documentation

Extra_bddAndAbstractTime()

DdNode * Extra_bddAndAbstractTime	(	DdManager *	manager,
		DdNode *	f,
		DdNode *	g,
		DdNode *	cube,
		int	TimeOut )

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

Synopsis [Takes the AND of two BDDs and simultaneously abstracts the variables in cube.]

Description [Takes the AND of two BDDs and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the result is successful; NULL otherwise. Cudd_bddAndAbstract implements the semiring matrix multiplication algorithm for the boolean semiring.]

SideEffects [None]

SeeAlso [Cudd_addMatrixMultiply Cudd_addTriangle Cudd_bddAnd]

Definition at line 117 of file extraBddTime.c.

{
    DdNode *res;
    int Counter = 0;
 
    do {
    manager->reordered = 0;
    res = cuddBddAndAbstractRecurTime(manager, f, g, cube, &Counter, TimeOut);
    } while (manager->reordered == 1);
    return(res);
 
} /* end of Extra_bddAndAbstractTime */

Extra_bddAndTime()

DdNode * Extra_bddAndTime	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		int	TimeOut )

AutomaticEnd Function********************************************************************

Synopsis [Computes the conjunction of two BDDs f and g.]

Description [Computes the conjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]

SideEffects [None]

SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAndAbstract Cudd_bddIntersect Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor]

Definition at line 83 of file extraBddTime.c.

{
    DdNode *res;
    int Counter = 0;
 
    do {
    dd->reordered = 0;
    res = cuddBddAndRecurTime(dd,f,g, &Counter, TimeOut);
    } while (dd->reordered == 1);
    return(res);
 
} /* end of Extra_bddAndTime */

Extra_TransferPermuteTime()

DdNode * Extra_TransferPermuteTime	(	DdManager *	ddSource,
		DdManager *	ddDestination,
		DdNode *	f,
		int *	Permute,
		int	TimeOut )

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

Synopsis [Convert a {A,B}DD from a manager to another with variable remapping.]

Description [Convert a {A,B}DD from a manager to another one. The orders of the variables in the two managers may be different. Returns a pointer to the {A,B}DD in the destination manager if successful; NULL otherwise. The i-th entry in the array Permute tells what is the index of the i-th variable from the old manager in the new manager.]

SideEffects [None]

SeeAlso []

Definition at line 150 of file extraBddTime.c.

{
    DdNode * bRes;
    do
    {
        ddDestination->reordered = 0;
        bRes = extraTransferPermuteTime( ddSource, ddDestination, f, Permute, TimeOut );
    }
    while ( ddDestination->reordered == 1 );
    return ( bRes );
 
} /* end of Extra_TransferPermuteTime */