#include "mvfInt.h"
Include dependency graph for mvfMvf.c:
Go to the source code of this file.
Functions | |
| void | Mvf_Init (void) |
| void | Mvf_End (void) |
| Mvf_Function_t * | Mvf_FunctionAlloc (mdd_manager *mddManager, int n) |
| void | Mvf_FunctionAddMintermsToComponent (Mvf_Function_t *function, int i, mdd_t *g) |
| mdd_t * | Mvf_FunctionBuildRelationWithVariable (Mvf_Function_t *function, int mddId) |
| int | Mvf_FunctionReadNumComponents (Mvf_Function_t *function) |
| mdd_manager * | Mvf_FunctionReadMddManager (Mvf_Function_t *function) |
| Mvf_Function_t * | Mvf_FunctionDuplicate (Mvf_Function_t *function) |
| void | Mvf_FunctionFree (Mvf_Function_t *function) |
| void | Mvf_FunctionArrayFree (array_t *functionArray) |
| mdd_t * | Mvf_FunctionObtainComponent (Mvf_Function_t *function, int i) |
| mdd_t * | Mvf_FunctionReadComponent (Mvf_Function_t *function, int i) |
| Mvf_Function_t * | Mvf_FunctionCreateFromVariable (mdd_manager *mddManager, int mddId) |
| Mvf_Function_t * | Mvf_FunctionComposeWithFunctionArray (Mvf_Function_t *f, array_t *mddIdArray, array_t *functionArray) |
| Mvf_Function_t * | Mvf_FunctionComposeWithFunction (Mvf_Function_t *f, int mddId, Mvf_Function_t *g) |
| mdd_t * | Mvf_MddComposeWithFunction (mdd_t *f, int mddId, Mvf_Function_t *g) |
| boolean | Mvf_FunctionTestIsDeterministic (Mvf_Function_t *function) |
| boolean | Mvf_FunctionTestIsCompletelySpecified (Mvf_Function_t *function) |
| boolean | Mvf_FunctionTestIsConstant (Mvf_Function_t *function, int *constantValue) |
| boolean | Mvf_FunctionTestIsNonDeterministicConstant (Mvf_Function_t *function) |
| mdd_t * | Mvf_FunctionComputeDomain (Mvf_Function_t *function) |
| boolean | Mvf_FunctionTestIsWellFormed (Mvf_Function_t *function) |
| boolean | Mvf_FunctionTestIsEqualToFunction (Mvf_Function_t *function1, Mvf_Function_t *function2) |
| mdd_t * | Mvf_FunctionsComputeEquivalentSet (Mvf_Function_t *function1, Mvf_Function_t *function2) |
| Mvf_Function_t * | Mvf_FunctionCofactor (Mvf_Function_t *function, mdd_t *wrtMdd) |
| Mvf_Function_t * | Mvf_FunctionMinimize (Mvf_Function_t *f, mdd_t *c) |
| long | Mvf_FunctionArrayComputeNumBddNodes (array_t *functionArray) |
| long | Mvf_FunctionComputeNumBddNodes (Mvf_Function_t *function) |
| int | Mvf_FunctionFindFirstTrueComponent (Mvf_Function_t *function) |
| int | Mvf_FunctionComputeHashValue (Mvf_Function_t *function) |
| array_t * | Mvf_FunctionComputeSupport (Mvf_Function_t *function, mdd_manager *mddMgr, int *value) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: mvfMvf.c,v 1.6 2002/09/08 21:48:24 fabio Exp $" |
Function Documentation
| void Mvf_End | ( | void | ) |
| void Mvf_FunctionAddMintermsToComponent | ( | Mvf_Function_t * | function, |
| int | i, | ||
| mdd_t * | g | ||
| ) |
Function********************************************************************
Synopsis [Adds a set of minterms to the ith component of a function.]
Description [Adds a set of minterms, represented by the onset of an MDD g, to the onset of the ith component of a function. The MDD g is not freed.]
SideEffects []
SeeAlso [Mvf_FunctionAlloc]
Definition at line 122 of file mvfMvf.c.
{
mdd_t *oldComponent;
mdd_t *newComponent;
array_t *mddArray = (array_t *) function;
assert((i >= 0) && (i < array_n(mddArray)));
oldComponent = array_fetch(mdd_t *, mddArray, i);
newComponent = mdd_or(oldComponent, g, 1, 1);
mdd_free(oldComponent);
array_insert(mdd_t *, mddArray, i, newComponent);
}
Here is the caller graph for this function:
| Mvf_Function_t* Mvf_FunctionAlloc | ( | mdd_manager * | mddManager, |
| int | n | ||
| ) |
Function********************************************************************
Synopsis [Allocates a multi-valued function of n components.]
Description [Allocates a multi-valued function of n components. Each component is initialized to the zero MDD.]
SideEffects []
SeeAlso [Mvf_FunctionAddMintermsToComponent Mvf_FunctionCreateFromVariable]
Definition at line 95 of file mvfMvf.c.
{
int i;
array_t *mddArray = array_alloc(mdd_t *, n);
for (i = 0; i < n; i++) {
array_insert(mdd_t *, mddArray, i, mdd_zero(mddManager));
}
return ((Mvf_Function_t *) mddArray);
}
Here is the caller graph for this function:
| long Mvf_FunctionArrayComputeNumBddNodes | ( | array_t * | functionArray | ) |
Function********************************************************************
Synopsis [Returns the number of BDD nodes of an array of multi-valued functions.]
Description [Returns the number of BDD nodes of an array of multi-valued functions. A node shared by several functions is counted only once.]
SideEffects []
Definition at line 908 of file mvfMvf.c.
{
int i;
long numNodes;
array_t *mddArray = array_alloc(mdd_t *, 0);
/* Build an array of all MDDs */
for(i = 0; i < array_n(functionArray); i++) {
int j;
array_t *function = (array_t *)array_fetch(Mvf_Function_t *, functionArray, i);
for(j = 0; j < array_n(function); j++) {
mdd_t *component = array_fetch(mdd_t *, function, j);
array_insert_last(mdd_t *, mddArray, component);
}
}
/* Compute the reduced number of bdd nodes */
numNodes = mdd_size_multiple(mddArray);
array_free(mddArray);
return(numNodes);
}
| void Mvf_FunctionArrayFree | ( | array_t * | functionArray | ) |
Function********************************************************************
Synopsis [Frees an array of multi-valued output functions.]
Description [Frees an array of multi-valued output functions. Does nothing if functionArray is NULL.]
SideEffects []
SeeAlso [Mvf_FunctionFree]
Definition at line 285 of file mvfMvf.c.
{
int i;
if (functionArray != NIL(array_t)) {
for (i = 0; i < array_n(functionArray); i++) {
Mvf_Function_t *function = array_fetch(Mvf_Function_t *, functionArray, i);
Mvf_FunctionFree(function);
}
array_free(functionArray);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mvf_FunctionBuildRelationWithVariable | ( | Mvf_Function_t * | function, |
| int | mddId | ||
| ) |
Function********************************************************************
Synopsis [Returns the MDD representation of the relation (var == function).]
Description [Given a variable x, represented by MDD var "mddId", and a function f:y->z, represented by "function", where x and z take the same number of values, returns the MDD for a (binary) function F(x,y) such that F(x,y) = 1 iff x = f(y). In the binary case it reduces to F(x,y) = x XNOR f(y). Intuitively it describes a function of multi-valued variables by the characteristic function of its input-output relation.]
SideEffects []
Definition at line 155 of file mvfMvf.c.
{
int i;
mvar_type mddVar;
array_t *mddArray = (array_t *) function;
mdd_manager *mddManager = Mvf_FunctionReadMddManager(function);
mdd_t *sumOfFactors = mdd_zero(mddManager);
mddVar = array_fetch(mvar_type, mdd_ret_mvar_list(mddManager), mddId);
assert(mddVar.values == Mvf_FunctionReadNumComponents(function));
for (i = 0; i < array_n(mddArray); i++) {
mdd_t *varLiteral;
mdd_t *factor;
mdd_t *tmp;
mdd_t *fComponent = array_fetch(mdd_t *, mddArray, i);
varLiteral = mdd_eq_c(mddManager, mddId, i);
factor = mdd_and(fComponent, varLiteral, 1, 1);
mdd_free(varLiteral);
/* Take the or of the sumOfFactors so far and the new factor */
tmp = mdd_or(sumOfFactors, factor, 1, 1);
mdd_free(factor);
mdd_free(sumOfFactors);
sumOfFactors = tmp;
}
return sumOfFactors;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Mvf_Function_t* Mvf_FunctionCofactor | ( | Mvf_Function_t * | function, |
| mdd_t * | wrtMdd | ||
| ) |
Function********************************************************************
Synopsis [Calls bdd_cofactor on each component of a multi-valued function.]
Description [Calls bdd_cofactor on each component of a multi-valued function, cofactoring with respect to wrtMDD. Returns the cofactored function. It is an error to call this function with a multi-valued function that contains null MDDs or with a null wrtMdd.]
SideEffects []
Definition at line 844 of file mvfMvf.c.
{
int i;
array_t *mddArray = (array_t *) function;
int numComponents = array_n(mddArray);
array_t *newFunction = array_alloc(mdd_t *, numComponents);
for(i = 0; i < numComponents; i++) {
mdd_t *component = array_fetch(mdd_t *, mddArray, i);
mdd_t *cofactor = bdd_cofactor(component, wrtMdd);
array_insert(mdd_t *, newFunction, i, cofactor);
}
return((Mvf_Function_t *)newFunction);
}
| Mvf_Function_t* Mvf_FunctionComposeWithFunction | ( | Mvf_Function_t * | f, |
| int | mddId, | ||
| Mvf_Function_t * | g | ||
| ) |
Function********************************************************************
Synopsis [Substitutes a variable by a function in a function.]
Description [Given a multi-valued function f, a variable x (mddId), and a multi-valued function g, the procedure replaces every appearance of x in f by function g. That is, if the function f is f(..., x, ...), then the result is f(..., g(), ...). The number of values that x can take and the number of components of g must be equal. The algorithm first computes the sum of factors (x==i)*gi for every value i in the domain of x, where gi is the ith component of g. Then, for each component fi of f, the sum of factors is conjuncted with fi, and x is existentially quantified. The function g must not depend on x. The result depends on all the variables of g and all the variables of f, except for x.]
SideEffects []
SeeAlso [Mvf_MddComposeWithFunction]
Definition at line 451 of file mvfMvf.c.
{
mdd_t *sumOfFactors;
array_t *result;
array_t *values;
int i;
mdd_manager *mddManager = Mvf_FunctionReadMddManager(f);
/* Allocate array to hold values for the literal and the result */
result = array_alloc(mdd_t *, array_n(f));
/*
* Create the sum of factors (x==i * gi). This function will verify that the
* domain of x and the range of g have the same cardinality.
*/
sumOfFactors = Mvf_FunctionBuildRelationWithVariable(g, mddId);
/*
* Result is an array of mdd_t * , result[i] = Exists(x) (f[i] * sumOfFactors)
* The array values holds now the index of the variable to smooth out.
*/
values = array_alloc(int, 1);
array_insert(int, values, 0, mddId);
for(i = 0; i < array_n(f); i++) {
mdd_t *functionUnit = array_fetch(mdd_t *, f, i);
mdd_t *tmp = mdd_and_smooth(mddManager, functionUnit, sumOfFactors, values);
array_insert(mdd_t *, result, i, tmp);
}
/* Clean up */
array_free(values);
mdd_free(sumOfFactors);
return ((Mvf_Function_t *) result);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Mvf_Function_t* Mvf_FunctionComposeWithFunctionArray | ( | Mvf_Function_t * | f, |
| array_t * | mddIdArray, | ||
| array_t * | functionArray | ||
| ) |
Function********************************************************************
Synopsis [Substitutes a set of variables by a set of functions in a function.]
Description [Given a multi-valued function f, an array of variables x1,...,xk, and an array of multi-valued functions g1,...,gk, iteratively calls Mvf_MddComposeWithFunction to substitute each xi by gi. The parameters of the ith call to Mvf_MddComposeWithFunction are the result of composing the first i-1 variables, xi, and gi. The multi-valued function gi must not depend on xi.]
SideEffects []
SeeAlso [Mvf_MddComposeWithFunction]
Definition at line 402 of file mvfMvf.c.
{
Mvf_Function_t *result;
int i;
assert(array_n(mddIdArray) == array_n(functionArray));
/* Make an initial copy of the function */
result = Mvf_FunctionDuplicate(f);
for(i = 0; i < array_n(mddIdArray); i++) {
Mvf_Function_t *tmp;
int mddId = array_fetch(int, mddIdArray, i);
Mvf_Function_t *g = array_fetch(Mvf_Function_t *, functionArray, i);
tmp = Mvf_FunctionComposeWithFunction(result, mddId, g);
Mvf_FunctionFree(result);
result = tmp;
}
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* Mvf_FunctionComputeDomain | ( | Mvf_Function_t * | function | ) |
Function********************************************************************
Synopsis [Computes the domain of a multi-valued function.]
Description [Returns an MDD representing the set of minterms which turn on some component of a function. In other words, returns the union of the onsets of the components. The domain is the tautology if and only if the function is completely specified.]
SideEffects []
SeeAlso [Mvf_FunctionTestIsCompletelySpecified]
Definition at line 721 of file mvfMvf.c.
{
array_t *mddArray = (array_t *) function;
mdd_manager *mddManager = Mvf_FunctionReadMddManager(function);
mdd_t *sum = mdd_multiway_or(mddManager, mddArray);
return sum;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int Mvf_FunctionComputeHashValue | ( | Mvf_Function_t * | function | ) |
Function********************************************************************
Synopsis [Hashes A multi-valued function.]
Description [Hashes A multi-valued function. Each component's top variable id is multiplied by the index of component (+ 1). Returns the sum of this computation on every component. It is an error to call this function with a null multi-valued function.]
SideEffects []
Definition at line 992 of file mvfMvf.c.
{
int i;
int result = 0;
array_t *mddArray = (array_t *) function;
for(i = 0; i < array_n(mddArray); i++) {
mdd_t *component = array_fetch(mdd_t *, mddArray, i);
result += (mdd_top_var_id(component)) * (i + 1);
}
return(result);
}
| long Mvf_FunctionComputeNumBddNodes | ( | Mvf_Function_t * | function | ) |
| array_t* Mvf_FunctionComputeSupport | ( | Mvf_Function_t * | function, |
| mdd_manager * | mddMgr, | ||
| int * | value | ||
| ) |
Function********************************************************************
Synopsis [Computes the variables in the true support of a function.]
Description [Computes the variables in the true support of a function. Does this by taking the union of the result of mdd_get_support on each component of the function. Returns the support as an (ascending) ordered array of MDD ids. If the function is a constant, then a NULL array is returned, and the constant value of the function is written in the "value" variable.]
SideEffects []
SeeAlso [Mvf_FunctionTestIsConstant]
Definition at line 1024 of file mvfMvf.c.
{
int i;
mdd_t *component;
array_t *totalSupportArray;
var_set_t *totalSupportSet;
int numMddVars = array_n(mdd_ret_mvar_list(mddMgr));
/*
* Handle the case where function is just a constant.
*/
if (Mvf_FunctionTestIsConstant(function, value)) {
return NIL(array_t);
}
/*
* Accumulate the union of supports of the function components into a bit
* array.
*/
totalSupportArray = array_alloc(int, 0);
totalSupportSet = var_set_new(numMddVars);
Mvf_FunctionForEachComponent(function, i, component) {
int j;
int mddVarId;
array_t *support = mdd_get_support(mddMgr, component);
arrayForEachItem(int, support, j, mddVarId) {
var_set_set_elt(totalSupportSet, mddVarId);
}
array_free(support);
}
/* Convert the bit array to an array of mdd ids. */
for (i = 0; i < numMddVars; i++) {
if (var_set_get_elt(totalSupportSet, i)) {
array_insert_last(int, totalSupportArray, i);
}
}
var_set_free(totalSupportSet);
return totalSupportArray;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| Mvf_Function_t* Mvf_FunctionCreateFromVariable | ( | mdd_manager * | mddManager, |
| int | mddId | ||
| ) |
Function********************************************************************
Synopsis [Creates the multi-output function for a variable.]
Description [Given a variable, creates a function with as many components as values of the variable. The ith component of the function is true exactly when the variable is equal to the ith value (i.e. fi(x) = (x==i), where x is the variable specified by mddId). For the case where x is binary valued, the result is \[!x, x\]. Assumes that mddId is non-negative.]
SideEffects []
SeeAlso [Mvf_FunctionAlloc]
Definition at line 360 of file mvfMvf.c.
{
int i;
array_t *mvar_list = mdd_ret_mvar_list(mddManager);
mvar_type varInfo;
array_t *result;
assert(mddId >= 0);
varInfo = array_fetch(mvar_type, mvar_list, mddId);
result = array_alloc(mdd_t *, varInfo.values);
for(i = 0; i < varInfo.values; i++) {
mdd_t *literal;
literal = mdd_eq_c(mddManager, mddId, i);
array_insert(mdd_t *, result, i, literal);
}
return ((Mvf_Function_t *) result);
}
Here is the caller graph for this function:
| Mvf_Function_t* Mvf_FunctionDuplicate | ( | Mvf_Function_t * | function | ) |
Function********************************************************************
Synopsis [Duplicates a multi-valued output function.]
Description [Returns a new multi-valued output function, whose constituent MDDs have been duplicated. Assumes that function is not NULL.]
SideEffects []
SeeAlso [Mvf_FunctionFree]
Definition at line 245 of file mvfMvf.c.
{
return ((Mvf_Function_t *) mdd_array_duplicate((array_t *) function));
}
Here is the caller graph for this function:
| int Mvf_FunctionFindFirstTrueComponent | ( | Mvf_Function_t * | function | ) |
Function********************************************************************
Synopsis [Returns the index of the first component of a multi-valued function that is equal to the tautology.]
Description [Returns the index of the first component of a multi-valued function that is equal to the tautology. If the multi-valued function is deterministic, this component is unique. Returns -1 if such a component is not found. It is an error to call this function with a multi-valued function that contains null MDDs.]
SideEffects []
Definition at line 964 of file mvfMvf.c.
{
int i;
array_t *mddArray = (array_t *) function;
for(i = 0; i < array_n(mddArray); i++) {
mdd_t *component = array_fetch(mdd_t *, mddArray, i);
if (mdd_is_tautology(component, 1)) {
return(i);
}
}
return(-1);
}
| void Mvf_FunctionFree | ( | Mvf_Function_t * | function | ) |
Function********************************************************************
Synopsis [Frees a multi-valued output function.]
Description [Frees a multi-valued output function. Does nothing if function is NULL.]
SideEffects []
SeeAlso [Mvf_FunctionAlloc]
Definition at line 265 of file mvfMvf.c.
{
mdd_array_free((array_t *) function);
}
Here is the caller graph for this function:
| Mvf_Function_t* Mvf_FunctionMinimize | ( | Mvf_Function_t * | f, |
| mdd_t * | c | ||
| ) |
Function********************************************************************
Synopsis [Calls bdd_minimize on each component of a multi-valued function.]
Description [Calls bdd_minimize on each component of a multi-valued function f, minimizing with respect to the care function c. The returned function agrees with f wherever c is true, and may or may not agree with f wherever c is false. It is an error to call this function with a multi-valued function that contains null MDDs or with a null care.]
SideEffects []
Definition at line 877 of file mvfMvf.c.
{
int i;
array_t *mddArray = (array_t *) f;
int numComponents = array_n(mddArray);
array_t *newFunction = array_alloc(mdd_t *, numComponents);
for(i = 0; i < numComponents; i++) {
mdd_t *component = array_fetch(mdd_t *, mddArray, i);
mdd_t *minimize = bdd_minimize(component, c);
array_insert(mdd_t *, newFunction, i, minimize);
}
return((Mvf_Function_t *)newFunction);
}
Here is the caller graph for this function:
| mdd_t* Mvf_FunctionObtainComponent | ( | Mvf_Function_t * | function, |
| int | i | ||
| ) |
Function********************************************************************
Synopsis [Returns a copy of the ith component of a multi-valued function.]
Synopsis [Returns a copy of the MDD giving the minterms for which a multi-valued function evaluates to its ith value.]
SideEffects []
SeeAlso [Mvf_FunctionAlloc Mvf_FunctionCreateFromVariable]
Definition at line 312 of file mvfMvf.c.
{
mdd_t *component = array_fetch(mdd_t *, (array_t *) function, i);
return (mdd_dup(component));
}
Here is the caller graph for this function:
| mdd_t* Mvf_FunctionReadComponent | ( | Mvf_Function_t * | function, |
| int | i | ||
| ) |
Function********************************************************************
Synopsis [Returns the ith component of a multi-valued function.]
Synopsis [Returns the MDD giving the minterms for which a multi-valued function evaluates to its ith value. The user should not free this MDD.]
SideEffects []
SeeAlso [Mvf_FunctionObtainComponent Mvf_FunctionAlloc Mvf_FunctionCreateFromVariable]
Definition at line 335 of file mvfMvf.c.
{
mdd_t *component = array_fetch(mdd_t *, (array_t *) function, i);
return (component);
}
Here is the caller graph for this function:
| mdd_manager* Mvf_FunctionReadMddManager | ( | Mvf_Function_t * | function | ) |
Function********************************************************************
Synopsis [Returns the MDD manager of a multi-valued function.]
Description [Returns the MDD manager of a multi-valued function. This procedure assumes that the function has at least one component.]
SideEffects []
SeeAlso [Mvf_FunctionAlloc]
Definition at line 223 of file mvfMvf.c.
{
mdd_t *component = array_fetch(mdd_t *, (array_t *) function, 0);
return (mdd_get_manager(component));
}
Here is the caller graph for this function:
| int Mvf_FunctionReadNumComponents | ( | Mvf_Function_t * | function | ) |
Function********************************************************************
Synopsis [Returns the number of components of a multi-valued function.]
Description [Returns the number of components of a multi-valued function. This is the same number as the value of the parameter passed to Mvf_FunctionAlloc.]
SideEffects []
SeeAlso [Mvf_FunctionAlloc]
Definition at line 203 of file mvfMvf.c.
{
return (array_n((array_t *) function));
}
Here is the caller graph for this function:
| mdd_t* Mvf_FunctionsComputeEquivalentSet | ( | Mvf_Function_t * | function1, |
| Mvf_Function_t * | function2 | ||
| ) |
Function********************************************************************
Synopsis [Returns the set of minterms on which two functions agree.]
Description [Returns the set of minterms on which two functions agree. For f = \[f1, f2, ..., fn\] and g = \[g1, g2, ..., gn\], the returned set is: AND(i = 1, ..., n) (fi XNOR gi). For the special case where f and g are binary valued, this function computes (f XNOR g). It is an error if the two functions have a different number of components.]
SideEffects []
Definition at line 803 of file mvfMvf.c.
{
int i;
array_t *mddArray1 = (array_t *) function1;
array_t *mddArray2 = (array_t *) function2;
int numComponents = array_n(mddArray1);
mdd_manager *mddManager = Mvf_FunctionReadMddManager(function1);
mdd_t *product = mdd_one(mddManager);
assert(numComponents == array_n(mddArray2));
for (i = 0; i < numComponents; i++) {
mdd_t *mdd1 = array_fetch(mdd_t *, mddArray1, i);
mdd_t *mdd2 = array_fetch(mdd_t *, mddArray2, i);
mdd_t *xnor = mdd_xnor(mdd1, mdd2);
mdd_t *temp = product;
product = mdd_and(temp, xnor, 1, 1);
mdd_free(temp);
mdd_free(xnor);
}
return product;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean Mvf_FunctionTestIsCompletelySpecified | ( | Mvf_Function_t * | function | ) |
Function********************************************************************
Synopsis [Returns true if a multi-valued function is completely specified, else false.]
Description [Returns true if a multi-valued function is completely specified, else false. A function is completely specified if, for every minterm over the input space of the function, the function takes at least one value. The complexity of this procedure is linear in the number of values the function can take.]
SideEffects []
SeeAlso [Mvf_FunctionTestIsDeterministic Mvf_FunctionTestIsWellFormed]
Definition at line 609 of file mvfMvf.c.
{
mdd_t *sum = Mvf_FunctionComputeDomain(function);
boolean sumIsTautology = mdd_is_tautology(sum, 1);
mdd_free(sum);
return sumIsTautology;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean Mvf_FunctionTestIsConstant | ( | Mvf_Function_t * | function, |
| int * | constantValue | ||
| ) |
Function********************************************************************
Synopsis [Returns true if a multi-valued function is constant, else false.]
Description [Returns true if a multi-valued function is constant, else false. A function is constant if exactly one component is the tautology, and the remaining components are zero. If the function is a constant, then "value" is set to the constant value of the function. The complexity of this procedure is linear in the number of values the function can take.]
SideEffects []
SeeAlso [Mvf_FunctionTestIsNonDeterministicConstant]
Definition at line 637 of file mvfMvf.c.
{
int i;
array_t *mddArray = (array_t *) function;
int numComponents = array_n(mddArray);
int numTautComps = 0;
for (i = 0; i < numComponents; i++) {
mdd_t *ithComponent = array_fetch(mdd_t *, mddArray, i);
if (mdd_is_tautology(ithComponent, 1)) {
*constantValue = i;
numTautComps++;
}
else if (!mdd_is_tautology(ithComponent, 0)) {
/* this component is not 1 nor 0, so function can't be a constant */
return FALSE;
}
/* else, must be the zero function */
}
return (numTautComps == 1);
}
Here is the caller graph for this function:
| boolean Mvf_FunctionTestIsDeterministic | ( | Mvf_Function_t * | function | ) |
Function********************************************************************
Synopsis [Returns true if a multi-valued function is deterministic, else false.]
Description [Returns true if a multi-valued function is deterministic, else false. A function is deterministic if, for every minterm over the input space of the function, the function takes at most one value. The complexity of this procedure is linear in the number of values the function can take.]
SideEffects []
SeeAlso [Mvf_FunctionTestIsCompletelySpecified Mvf_FunctionTestIsWellFormed]
Definition at line 557 of file mvfMvf.c.
{
int i;
array_t *mddArray = (array_t *) function;
int numComponents = array_n(mddArray);
mdd_t *sum;
if (numComponents == 0) {
return TRUE;
}
sum = mdd_dup(array_fetch(mdd_t *, mddArray, 0));
for (i = 1; i < numComponents; i++) {
mdd_t *temp = sum;
mdd_t *ithComponent = array_fetch(mdd_t *, mddArray, i);
boolean intersectionIsEmpty = mdd_lequal(ithComponent, sum, 1, 0);
/* If the intersection is not empty, then return FALSE. */
if (!intersectionIsEmpty) {
mdd_free(sum);
return FALSE;
}
sum = mdd_or(temp, ithComponent, 1, 1);
mdd_free(temp);
}
mdd_free(sum);
/* The components are pairwise disjoint. */
return TRUE;
}
Here is the caller graph for this function:
| boolean Mvf_FunctionTestIsEqualToFunction | ( | Mvf_Function_t * | function1, |
| Mvf_Function_t * | function2 | ||
| ) |
Function********************************************************************
Synopsis [Returns true if two multi-valued functions are equal, else false.]
Description [Returns true if two multi-valued functions are equal, else false. Two functions are equal if they have the same number of components, and the ith component of one is equal to the ith component of the other.]
SideEffects []
Definition at line 764 of file mvfMvf.c.
{
int i;
array_t *mddArray1 = (array_t *) function1;
array_t *mddArray2 = (array_t *) function2;
int numComponents = array_n(mddArray1);
if (numComponents != array_n(mddArray2)) {
return FALSE;
}
for (i = 0; i < numComponents; i++) {
mdd_t *mdd1 = array_fetch(mdd_t *, mddArray1, i);
mdd_t *mdd2 = array_fetch(mdd_t *, mddArray2, i);
if (!mdd_equal(mdd1, mdd2)) {
return FALSE;
}
}
return TRUE;
}
Here is the caller graph for this function:
| boolean Mvf_FunctionTestIsNonDeterministicConstant | ( | Mvf_Function_t * | function | ) |
Function********************************************************************
Synopsis [Returns true if a multi-valued function is a non-deterministic constant, else false.]
Description [Returns true if a multi-valued function is a non-deterministic constant, else false. A function is a non-deterministic constant if more than one component is the tautology, and the remaining components are zero. The complexity of this procedure is linear in the number of values the function can take.]
SideEffects []
SeeAlso [Mvf_FunctionTestIsConstant]
Definition at line 681 of file mvfMvf.c.
{
int i;
array_t *mddArray = (array_t *) function;
int numComponents = array_n(mddArray);
int numTautComps = 0;
for (i = 0; i < numComponents; i++) {
mdd_t *ithComponent = array_fetch(mdd_t *, mddArray, i);
if (mdd_is_tautology(ithComponent, 1)) {
numTautComps++;
}
else if (!mdd_is_tautology(ithComponent, 0)) {
/* this component is not 1 nor 0, so function can't be a non-det constant */
return FALSE;
}
/* else, must be the zero function */
}
return (numTautComps > 1);
}
Here is the caller graph for this function:
| boolean Mvf_FunctionTestIsWellFormed | ( | Mvf_Function_t * | function | ) |
Function********************************************************************
Synopsis [Returns true if a function is deterministic and completely specified, else false.]
SideEffects []
SeeAlso [Mvf_FunctionTestIsDeterministic Mvf_FunctionTestIsCompletelySpecified]
Definition at line 744 of file mvfMvf.c.
{
return (Mvf_FunctionTestIsDeterministic(function)
&& Mvf_FunctionTestIsCompletelySpecified(function));
}
Here is the call graph for this function:
| void Mvf_Init | ( | void | ) |
| mdd_t* Mvf_MddComposeWithFunction | ( | mdd_t * | f, |
| int | mddId, | ||
| Mvf_Function_t * | g | ||
| ) |
Function********************************************************************
Synopsis [Substitutes a variable by a function in an mdd_t *.]
Description [Given a binary-valued function f, a variable x, and a multi-valued function g, the procedure replaces every appearance of x in f by function g. That is, if the function f is f(..., x, ...), then the result is f(..., g(), ...). The number of values that x can take and the number of components of g must be equal. The algorithm first computes the sum of factors (x==i)*gi for every value i in the domain of x, where gi is the ith component of g, then conjuncts this with f, and finally existentially quantifies x. The function g must not depend on x. The result depends on all the variables of g and all the variables of f, except for x.]
SideEffects []
Definition at line 511 of file mvfMvf.c.
{
mdd_t *sumOfFactors;
mdd_t *result;
array_t *values;
mdd_manager *mddManager = mdd_get_manager(f);
/*
* Create the sum of factors (x==i * gi). This function will verify that the
* domain of x and the range of g have the same cardinality.
*/
sumOfFactors = Mvf_FunctionBuildRelationWithVariable(g, mddId);
/* Result is an mdd_t * , result = Exists(x) (f * sumOfFactors) */
values = array_alloc(int, 1);
array_insert(int, values, 0, mddId);
result = mdd_and_smooth(mddManager, f, sumOfFactors, values);
/* Clean up */
array_free(values);
mdd_free(sumOfFactors);
return result;
}
Here is the call graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: mvfMvf.c,v 1.6 2002/09/08 21:48:24 fabio Exp $" [static] |
CFile***********************************************************************
FileName [mvfMvf.c]
PackageName [mvf]
Synopsis [Routines to create, manipulate and free multi-valued functions.]
SeeAlso [mvf.h]
Author [Tom Shiple]
Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.
IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
