#include "imgInt.h"
Include dependency graph for imgTfmUtil.c:
Go to the source code of this file.
Functions | |
| static int | SignatureCompare (int *ptrX, int *ptrY) |
| static int | CompareBddPointer (const void *e1, const void *e2) |
| void | ImgVectorConstrain (ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint, array_t *relationArray, array_t **newVector, mdd_t **cube, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube, boolean singleVarFlag) |
| mdd_t * | ImgVectorMinimize (ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint, mdd_t *from, array_t *relationArray, array_t **newVector, mdd_t **cube, array_t **newRelationArray, mdd_t **cofactorCube, mdd_t **abstractCube) |
| void | ImgVectorFree (array_t *vector) |
| int | ImgVectorFunctionSize (array_t *vector) |
| long | ImgVectorBddSize (array_t *vector) |
| array_t * | ImgVectorCopy (ImgTfmInfo_t *info, array_t *vector) |
| ImgComponent_t * | ImgComponentAlloc (ImgTfmInfo_t *info) |
| ImgComponent_t * | ImgComponentCopy (ImgTfmInfo_t *info, ImgComponent_t *comp) |
| void | ImgComponentFree (ImgComponent_t *comp) |
| void | ImgComponentGetSupport (ImgComponent_t *comp) |
| void | ImgSupportCopy (ImgTfmInfo_t *info, char *dsupport, char *ssupport) |
| void | ImgSupportClear (ImgTfmInfo_t *info, char *support) |
| void | ImgSupportPrint (ImgTfmInfo_t *info, char *support) |
| int | ImgSupportCount (ImgTfmInfo_t *info, char *support) |
| array_t * | ImgGetConstrainedRelationArray (ImgTfmInfo_t *info, array_t *relationArray, mdd_t *constraint) |
| array_t * | ImgGetCofactoredRelationArray (array_t *relationArray, mdd_t *func) |
| void | ImgCofactorRelationArray (array_t *relationArray, mdd_t *func) |
| array_t * | ImgGetAbstractedRelationArray (mdd_manager *manager, array_t *relationArray, mdd_t *cube) |
| void | ImgAbstractRelationArray (mdd_manager *manager, array_t *relationArray, mdd_t *cube) |
| array_t * | ImgGetCofactoredAbstractedRelationArray (mdd_manager *manager, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube) |
| array_t * | ImgGetAbstractedCofactoredRelationArray (mdd_manager *manager, array_t *relationArray, mdd_t *cofactorCube, mdd_t *abstractCube) |
| array_t * | ImgGetConstrainedVector (ImgTfmInfo_t *info, array_t *vector, mdd_t *constraint) |
| array_t * | ImgGetCofactoredVector (ImgTfmInfo_t *info, array_t *vector, mdd_t *func) |
| void | ImgCofactorVector (ImgTfmInfo_t *info, array_t *vector, mdd_t *func) |
| mdd_t * | ImgTfmEliminateDependVars (ImgTfmInfo_t *info, array_t *vector, array_t *relationArray, mdd_t *states, array_t **newVector, mdd_t **dependRelations) |
| int | ImgExistConstIntermediateVar (array_t *vector) |
| mdd_t * | ImgGetComposedFunction (array_t *vector) |
| ImgComponent_t * | ImgGetLatchComponent (array_t *vector) |
| array_t * | ImgComposeConstIntermediateVars (ImgTfmInfo_t *info, array_t *vector, mdd_t *constIntermediate, mdd_t **cofactorCube, mdd_t **abstractCube, mdd_t **and_, mdd_t **from) |
| int | ImgCountBddSupports (mdd_t *func) |
| void | ImgCheckConstConstrain (mdd_t *f1, mdd_t *f2, int *f21p, int *f21n) |
| int | ImgConstConstrain (mdd_t *func, mdd_t *constraint) |
| void | ImgPrintVectorDependency (ImgTfmInfo_t *info, array_t *vector, int verbosity) |
| float | ImgPercentVectorDependency (ImgTfmInfo_t *info, array_t *vector, int length, int *nLongs) |
| void | ImgWriteSupportMatrix (ImgTfmInfo_t *info, array_t *vector, array_t *relationArray, char *string) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: imgTfmUtil.c,v 1.23 2005/04/23 14:30:55 jinh Exp $" |
| static double * | signatures |
Function Documentation
| static int CompareBddPointer | ( | const void * | e1, |
| const void * | e2 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Compares two function BDD pointers of components.]
Description [Compares two function BDD pointers of components.]
SideEffects []
Definition at line 2191 of file imgTfmUtil.c.
{
ImgComponent_t *c1, *c2;
unsigned long ptr1, ptr2;
c1 = *((ImgComponent_t **)e1);
c2 = *((ImgComponent_t **)e2);
ptr1 = (unsigned long)bdd_pointer(c1->func);
ptr2 = (unsigned long)bdd_pointer(c2->func);
if (ptr1 > ptr2)
return(1);
else if (ptr1 < ptr2)
return(-1);
else
return(0);
}
Here is the caller graph for this function:
| void ImgAbstractRelationArray | ( | mdd_manager * | manager, |
| array_t * | relationArray, | ||
| mdd_t * | cube | ||
| ) |
Function********************************************************************
Synopsis [Smoothes a relation array with respect to a cube.]
Description [Smoothes a relation array with respect to a cube.]
SideEffects []
Definition at line 1041 of file imgTfmUtil.c.
{
int i;
mdd_t *relation, *abstractedRelation;
array_t *varsArray;
if (bdd_is_tautology(cube, 1))
return;
if (bdd_get_package_name() != CUDD)
varsArray = mdd_get_bdd_support_vars(manager, cube);
else /* to remove uninitialized variable warning*/
varsArray = NIL(array_t);
for (i = 0; i < array_n(relationArray); i++) {
relation = array_fetch(mdd_t *, relationArray, i);
if (bdd_get_package_name() == CUDD)
abstractedRelation = bdd_smooth_with_cube(relation, cube);
else
abstractedRelation = bdd_smooth(relation, varsArray);
if (mdd_equal(abstractedRelation, relation))
mdd_free(abstractedRelation);
else {
mdd_free(relation);
array_insert(mdd_t *, relationArray, i, abstractedRelation);
}
}
if (bdd_get_package_name() != CUDD)
mdd_array_free(varsArray);
}
Here is the caller graph for this function:
| void ImgCheckConstConstrain | ( | mdd_t * | f1, |
| mdd_t * | f2, | ||
| int * | f21p, | ||
| int * | f21n | ||
| ) |
Function********************************************************************
Synopsis [Quick checking whether the results of constrain between two functions are constant.]
Description [Quick checking whether the results of constrain between two functions are constant. Assumes that 1) f1 != f2 and f1 != f2', and 2) neither f1 nor f2 is constant.]
SideEffects []
Definition at line 1741 of file imgTfmUtil.c.
{
if (mdd_lequal(f1, f2, 1, 1)) { /* f2 > f1 */
*f21p = 1;
*f21n = 2;
} else if (mdd_lequal(f2, f1, 1, 0)) { /* f2&f1=0 -> f2 < f1' */
*f21p = 0;
*f21n = 2;
} else if (mdd_lequal(f1, f2, 0, 1)) { /* f2 > f1' */
*f21p = 2;
*f21n = 1;
} else if (mdd_lequal(f2, f1, 1, 1)) { /* f2&f1'=0 -> f2 < f1 */
*f21p = 2;
*f21n = 0;
} else {
*f21p = 2;
*f21n = 2;
}
}
Here is the caller graph for this function:
| void ImgCofactorRelationArray | ( | array_t * | relationArray, |
| mdd_t * | func | ||
| ) |
Function********************************************************************
Synopsis [Cofactors a relation array with respect to a function.]
Description [Cofactors a relation array with respect to a function.]
SideEffects []
Definition at line 965 of file imgTfmUtil.c.
{
int i;
mdd_t *relation, *cofactoredRelation;
if (bdd_is_tautology(func, 1))
return;
for (i = 0; i < array_n(relationArray); i++) {
relation = array_fetch(mdd_t *, relationArray, i);
cofactoredRelation = bdd_cofactor(relation, func);
if (mdd_equal(cofactoredRelation, relation))
mdd_free(cofactoredRelation);
else {
mdd_free(relation);
array_insert(mdd_t *, relationArray, i, cofactoredRelation);
}
}
}
Here is the caller graph for this function:
| void ImgCofactorVector | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | func | ||
| ) |
Function********************************************************************
Synopsis [Cofactors a function vector with respect to a function.]
Description [Cofactors a function vector with respect to a function.]
SideEffects []
Definition at line 1244 of file imgTfmUtil.c.
{
int i;
ImgComponent_t *comp;
mdd_t *cofactoredFunc;
if (bdd_is_tautology(func, 1))
return;
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
cofactoredFunc = bdd_cofactor(comp->func, func);
if (mdd_equal(cofactoredFunc, comp->func))
mdd_free(cofactoredFunc);
else {
mdd_free(comp->func);
comp->func = cofactoredFunc;
ImgSupportClear(info, comp->support);
ImgComponentGetSupport(comp);
}
}
}
Here is the call graph for this function:
| ImgComponent_t* ImgComponentAlloc | ( | ImgTfmInfo_t * | info | ) |
Function********************************************************************
Synopsis [Allocates a component.]
Description [Allocates a component.]
SideEffects []
Definition at line 725 of file imgTfmUtil.c.
{
ImgComponent_t *comp;
comp = ALLOC(ImgComponent_t, 1);
memset(comp, 0, sizeof(ImgComponent_t));
comp->support = ALLOC(char, info->nVars);
ImgSupportClear(info, comp->support);
comp->id = info->nComponents++;
return(comp);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| ImgComponent_t* ImgComponentCopy | ( | ImgTfmInfo_t * | info, |
| ImgComponent_t * | comp | ||
| ) |
Function********************************************************************
Synopsis [Copies a component]
Description [Copies a component]
SideEffects []
Definition at line 748 of file imgTfmUtil.c.
{
ImgComponent_t *newComp;
newComp = ImgComponentAlloc(info);
newComp->func = mdd_dup(comp->func);
newComp->var = mdd_dup(comp->var);
ImgSupportCopy(info, newComp->support, comp->support);
newComp->intermediate = comp->intermediate;
return(newComp);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void ImgComponentFree | ( | ImgComponent_t * | comp | ) |
Function********************************************************************
Synopsis [Frees a component.]
Description [Frees a component.]
SideEffects []
Definition at line 771 of file imgTfmUtil.c.
{
if (comp->func)
mdd_free(comp->func);
if (comp->var != NULL)
mdd_free(comp->var);
FREE(comp->support);
FREE(comp);
}
Here is the caller graph for this function:
| void ImgComponentGetSupport | ( | ImgComponent_t * | comp | ) |
Function********************************************************************
Synopsis [Gets the supports of a component.]
Description [Gets the supports of a component.]
SideEffects []
Definition at line 792 of file imgTfmUtil.c.
{
int index;
var_set_t *supportVarSet;
supportVarSet = bdd_get_support(comp->func);
for (index = 0; index < supportVarSet->n_elts; index++) {
if (var_set_get_elt(supportVarSet, index) == 1)
comp->support[index] = 1;
}
var_set_free(supportVarSet);
}
Here is the caller graph for this function:
| array_t* ImgComposeConstIntermediateVars | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | constIntermediate, | ||
| mdd_t ** | cofactorCube, | ||
| mdd_t ** | abstractCube, | ||
| mdd_t ** | and_, | ||
| mdd_t ** | from | ||
| ) |
Function********************************************************************
Synopsis [Compose the constant intermediate variable functions.]
Description [Compose the constant intermediate variable functions.]
SideEffects []
Definition at line 1529 of file imgTfmUtil.c.
{
int i, n, pos;
array_t *tmpVector, *cofactoredVector;
mdd_t *cofactor, *abstract;
mdd_t *curConstIntermediate, *newConstIntermediate;
mdd_t *tmp, *new_, *func, *varNot, *nsVar;
ImgComponent_t *comp, *comp1;
st_table *equivTable;
int *ptr, *regularPtr;
if (cofactorCube)
cofactor = mdd_one(info->manager);
else
cofactor = NIL(mdd_t);
if (abstractCube)
abstract = mdd_one(info->manager);
else
abstract = NIL(mdd_t);
cofactoredVector = vector;
tmpVector = cofactoredVector;
curConstIntermediate = constIntermediate;
while (!bdd_is_tautology(curConstIntermediate, 1)) {
newConstIntermediate = mdd_one(info->manager);
n = 0;
equivTable = st_init_table(st_ptrcmp, st_ptrhash);
cofactoredVector = array_alloc(ImgComponent_t *, 0);
for (i = 0; i < array_n(tmpVector); i++) {
comp = array_fetch(ImgComponent_t *, tmpVector, i);
func = bdd_cofactor(comp->func, curConstIntermediate);
if (comp->intermediate) {
if (mdd_is_tautology(func, 1)) {
tmp = newConstIntermediate;
newConstIntermediate = mdd_and(tmp, comp->var, 1, 1);
mdd_free(tmp);
mdd_free(func);
continue;
} else if (mdd_is_tautology(func, 0)) {
tmp = newConstIntermediate;
newConstIntermediate = mdd_and(tmp, comp->var, 1, 0);
mdd_free(tmp);
mdd_free(func);
continue;
}
comp1 = ImgComponentAlloc(info);
comp1->var = mdd_dup(comp->var);
comp1->func = func;
comp1->intermediate = 1;
if (mdd_equal(func, comp->func))
ImgSupportCopy(info, comp1->support, comp->support);
else
ImgComponentGetSupport(comp1);
array_insert_last(ImgComponent_t *, cofactoredVector, comp1);
n++;
continue;
}
if (mdd_is_tautology(func, 1)) {
if (cofactor) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = cofactor;
cofactor = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
if (and_) {
tmp = *and_;
*and_ = mdd_and(tmp, comp->var, 1, 1);
mdd_free(tmp);
}
if (from) {
tmp = *from;
*from = bdd_cofactor(tmp, comp->var);
mdd_free(tmp);
}
mdd_free(func);
} else if (mdd_is_tautology(func, 0)) {
if (cofactor) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = cofactor;
cofactor = mdd_and(tmp, nsVar, 1, 0);
mdd_free(tmp);
mdd_free(nsVar);
}
if (and_) {
tmp = *and_;
*and_ = mdd_and(tmp, comp->var, 1, 0);
mdd_free(tmp);
}
if (from) {
tmp = *from;
varNot = bdd_not(comp->var);
*from = bdd_cofactor(tmp, varNot);
mdd_free(tmp);
mdd_free(varNot);
}
mdd_free(func);
} else {
ptr = (int *)bdd_pointer(func);
regularPtr = (int *)((unsigned long)ptr & ~01);
if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) {
comp1 = array_fetch(ImgComponent_t *, cofactoredVector, pos);
if (and_) {
if (mdd_equal(func, comp1->func))
tmp = mdd_xnor(comp->var, comp1->var);
else
tmp = mdd_xor(comp->var, comp1->var);
new_ = mdd_and(tmp, *and_, 1, 1);
mdd_free(tmp);
mdd_free(*and_);
mdd_free(func);
*and_ = new_;
}
if (abstract) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
if (from) {
tmp = *from;
*from = bdd_compose(tmp, comp->var, comp1->var);
mdd_free(tmp);
}
} else {
comp1 = ImgComponentAlloc(info);
comp1->var = mdd_dup(comp->var);
comp1->func = func;
if (mdd_equal(func, comp->func))
ImgSupportCopy(info, comp1->support, comp->support);
else
ImgComponentGetSupport(comp1);
array_insert_last(ImgComponent_t *, cofactoredVector, comp1);
st_insert(equivTable, (char *)regularPtr, (char *)(long)n);
n++;
}
}
}
if (curConstIntermediate != constIntermediate)
mdd_free(curConstIntermediate);
curConstIntermediate = newConstIntermediate;
if (cofactor) {
tmp = cofactor;
cofactor = mdd_and(tmp, curConstIntermediate, 1, 1);
mdd_free(tmp);
}
st_free_table(equivTable);
ImgVectorFree(tmpVector);
tmpVector = cofactoredVector;
}
if (curConstIntermediate != constIntermediate)
mdd_free(curConstIntermediate);
if (cofactorCube)
*cofactorCube = cofactor;
if (abstractCube)
*abstractCube = abstract;
return(cofactoredVector);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int ImgConstConstrain | ( | mdd_t * | func, |
| mdd_t * | constraint | ||
| ) |
Function********************************************************************
Synopsis [Checks whether the result of constrain is constant.]
Description [Checks whether the result of constrain is constant.]
SideEffects []
Definition at line 1772 of file imgTfmUtil.c.
{
if (mdd_lequal(constraint, func, 1, 1)) /* func | constraint = 1 */
return(1);
if (mdd_lequal(func, constraint, 1, 0)) /* func | constraint = 0 */
return(0);
return(2); /* non-constant */
}
Here is the caller graph for this function:
| int ImgCountBddSupports | ( | mdd_t * | func | ) |
Function********************************************************************
Synopsis [Returns the number of BDD supports in a function.]
Description [Returns the number of BDD supports in a function.]
SideEffects []
Definition at line 1713 of file imgTfmUtil.c.
{
int index, nSupports = 0;
var_set_t *supportVarSet;
supportVarSet = bdd_get_support(func);
for (index = 0; index < supportVarSet->n_elts; index++) {
if (var_set_get_elt(supportVarSet, index) == 1)
nSupports++;
}
var_set_free(supportVarSet);
return(nSupports);
}
Here is the caller graph for this function:
| int ImgExistConstIntermediateVar | ( | array_t * | vector | ) |
Function********************************************************************
Synopsis [Checks whether there is a constant function of intermediate variables.]
Description [Checks whether there is a constant function of intermediate variables.]
SideEffects []
Definition at line 1432 of file imgTfmUtil.c.
{
int i;
ImgComponent_t *comp;
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (comp->intermediate) {
if (mdd_is_tautology(comp->func, 1) || mdd_is_tautology(comp->func, 0))
return(1);
}
}
return(0);
}
Here is the caller graph for this function:
| array_t* ImgGetAbstractedCofactoredRelationArray | ( | mdd_manager * | manager, |
| array_t * | relationArray, | ||
| mdd_t * | cofactorCube, | ||
| mdd_t * | abstractCube | ||
| ) |
Function********************************************************************
Synopsis [Smothes and cofactors a relation array.]
Description [Smothes and cofactors a relation array. Returns new relation array.]
SideEffects []
Definition at line 1129 of file imgTfmUtil.c.
{
int i;
array_t *newRelationArray = array_alloc(mdd_t *, 0);
mdd_t *relation, *newRelation, *tmpRelation;
array_t *varsArray;
if (bdd_get_package_name() != CUDD)
varsArray = mdd_get_bdd_support_vars(manager, abstractCube);
else /* to remove uninitialized variable warning*/
varsArray = NIL(array_t);
for (i = 0; i < array_n(relationArray); i++) {
relation = array_fetch(mdd_t *, relationArray, i);
if (bdd_get_package_name() == CUDD)
tmpRelation = bdd_smooth_with_cube(relation, abstractCube);
else
tmpRelation = bdd_smooth(relation, varsArray);
newRelation = bdd_cofactor(tmpRelation, cofactorCube);
mdd_free(tmpRelation);
if (bdd_is_tautology(newRelation, 1))
mdd_free(newRelation);
else
array_insert_last(mdd_t *, newRelationArray, newRelation);
}
if (bdd_get_package_name() != CUDD)
mdd_array_free(varsArray);
return(newRelationArray);
}
| array_t* ImgGetAbstractedRelationArray | ( | mdd_manager * | manager, |
| array_t * | relationArray, | ||
| mdd_t * | cube | ||
| ) |
Function********************************************************************
Synopsis [Smoothes a relation array with respect to a cube.]
Description [Smoothes a relation array with respect to a cube.]
SideEffects []
Definition at line 996 of file imgTfmUtil.c.
{
int i;
array_t *abstractedRelationArray;
mdd_t *relation, *abstractedRelation;
array_t *varsArray;
if (bdd_is_tautology(cube, 1))
return(mdd_array_duplicate(relationArray));
abstractedRelationArray = array_alloc(mdd_t *, 0);
if (bdd_get_package_name() != CUDD)
varsArray = mdd_get_bdd_support_vars(manager, cube);
else /* to remove uninitialized variable warning*/
varsArray = NIL(array_t);
for (i = 0; i < array_n(relationArray); i++) {
relation = array_fetch(mdd_t *, relationArray, i);
if (bdd_get_package_name() == CUDD)
abstractedRelation = bdd_smooth_with_cube(relation, cube);
else
abstractedRelation = bdd_smooth(relation, varsArray);
if (bdd_is_tautology(abstractedRelation, 1))
mdd_free(abstractedRelation);
else
array_insert_last(mdd_t *, abstractedRelationArray, abstractedRelation);
}
if (bdd_get_package_name() != CUDD)
mdd_array_free(varsArray);
return(abstractedRelationArray);
}
Here is the caller graph for this function:
| array_t* ImgGetCofactoredAbstractedRelationArray | ( | mdd_manager * | manager, |
| array_t * | relationArray, | ||
| mdd_t * | cofactorCube, | ||
| mdd_t * | abstractCube | ||
| ) |
Function********************************************************************
Synopsis [Cofactors and smooths a relation array.]
Description [Cofactors and smooths a relation array. Returns new relation array.]
SideEffects []
Definition at line 1084 of file imgTfmUtil.c.
{
int i;
array_t *newRelationArray = array_alloc(mdd_t *, 0);
mdd_t *relation, *newRelation, *tmpRelation;
array_t *varsArray;
if (bdd_get_package_name() != CUDD)
varsArray = mdd_get_bdd_support_vars(manager, abstractCube);
else /* to remove uninitialized variable warning*/
varsArray = NIL(array_t);
for (i = 0; i < array_n(relationArray); i++) {
relation = array_fetch(mdd_t *, relationArray, i);
tmpRelation = bdd_cofactor(relation, cofactorCube);
if (bdd_get_package_name() == CUDD)
newRelation = bdd_smooth_with_cube(tmpRelation, abstractCube);
else
newRelation = bdd_smooth(tmpRelation, varsArray);
mdd_free(tmpRelation);
if (bdd_is_tautology(newRelation, 1))
mdd_free(newRelation);
else
array_insert_last(mdd_t *, newRelationArray, newRelation);
}
if (bdd_get_package_name() != CUDD)
mdd_array_free(varsArray);
return(newRelationArray);
}
Here is the caller graph for this function:
| array_t* ImgGetCofactoredRelationArray | ( | array_t * | relationArray, |
| mdd_t * | func | ||
| ) |
Function********************************************************************
Synopsis [Cofactors a relation array with respect to a function.]
Description [Cofactors a relation array with respect to a function. Returns new relation array.]
SideEffects []
Definition at line 931 of file imgTfmUtil.c.
{
int i;
array_t *cofactoredRelationArray;
mdd_t *relation, *cofactoredRelation;
if (bdd_is_tautology(func, 1))
return(mdd_array_duplicate(relationArray));
cofactoredRelationArray = array_alloc(mdd_t *, 0);
for (i = 0; i < array_n(relationArray); i++) {
relation = array_fetch(mdd_t *, relationArray, i);
cofactoredRelation = bdd_cofactor(relation, func);
if (bdd_is_tautology(cofactoredRelation, 1))
mdd_free(cofactoredRelation);
else
array_insert_last(mdd_t *, cofactoredRelationArray, cofactoredRelation);
}
return(cofactoredRelationArray);
}
Here is the caller graph for this function:
| array_t* ImgGetCofactoredVector | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | func | ||
| ) |
Function********************************************************************
Synopsis [Cofactors a function vector with respect to a function.]
Description [Cofactors a function vector with respect to a function. Returns new function vector.]
SideEffects []
Definition at line 1206 of file imgTfmUtil.c.
{
int i;
array_t *cofactoredVector = array_alloc(ImgComponent_t *, 0);
ImgComponent_t *comp, *cofactoredComp;
mdd_t *cofactoredFunc;
if (bdd_is_tautology(func, 1))
return(ImgVectorCopy(info, vector));
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
cofactoredFunc = bdd_cofactor(comp->func, func);
cofactoredComp = ImgComponentAlloc(info);
cofactoredComp->var = mdd_dup(comp->var);
cofactoredComp->func = cofactoredFunc;
cofactoredComp->intermediate = comp->intermediate;
if (mdd_equal(cofactoredFunc, comp->func))
ImgSupportCopy(info, cofactoredComp->support, comp->support);
else
ImgComponentGetSupport(cofactoredComp);
array_insert_last(ImgComponent_t *, cofactoredVector, cofactoredComp);
}
return(cofactoredVector);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* ImgGetComposedFunction | ( | array_t * | vector | ) |
Function********************************************************************
Synopsis [Returns a function composed all intermediate variables.]
Description [Returns a function composed all intermediate variables.]
SideEffects []
Definition at line 1458 of file imgTfmUtil.c.
{
ImgComponent_t *comp;
mdd_t *func, *newFunc;
int i;
array_t *varArray, *funcArray;
assert(ImgVectorFunctionSize(vector) == 1);
/* no intermediate variables */
if (array_n(vector) == 1) {
comp = array_fetch(ImgComponent_t *, vector, 0);
newFunc = mdd_dup(comp->func);
return(newFunc);
}
func = NIL(mdd_t);
varArray = array_alloc(mdd_t *, 0);
funcArray = array_alloc(mdd_t *, 0);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (comp->intermediate) {
array_insert_last(mdd_t *, varArray, comp->var);
array_insert_last(mdd_t *, funcArray, comp->func);
continue;
}
func = comp->func;
}
newFunc = bdd_vector_compose(func, varArray, funcArray);
array_free(varArray);
array_free(funcArray);
return(newFunc);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* ImgGetConstrainedRelationArray | ( | ImgTfmInfo_t * | info, |
| array_t * | relationArray, | ||
| mdd_t * | constraint | ||
| ) |
Function********************************************************************
Synopsis [Constrains a relation array with respect to a constraint.]
Description [Constrains a relation array with respect to a constraint. Returns new relation array.]
SideEffects []
Definition at line 897 of file imgTfmUtil.c.
{
array_t *constrainedRelationArray;
int dynStatus;
bdd_reorder_type_t dynMethod;
dynStatus = bdd_reordering_status(info->manager, &dynMethod);
if (dynStatus != 0)
bdd_dynamic_reordering_disable(info->manager);
constrainedRelationArray = ImgGetCofactoredRelationArray(relationArray,
constraint);
if (dynStatus != 0) {
bdd_dynamic_reordering(info->manager, dynMethod,
BDD_REORDER_VERBOSITY_DEFAULT);
}
return(constrainedRelationArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* ImgGetConstrainedVector | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | constraint | ||
| ) |
Function********************************************************************
Synopsis [Constrains a function vector with respect to a constraint.]
Description [Constrains a function vector with respect to a constraint. Returns new function vector.]
SideEffects []
Definition at line 1174 of file imgTfmUtil.c.
{
array_t *constrainedVector;
int dynStatus;
bdd_reorder_type_t dynMethod;
dynStatus = bdd_reordering_status(info->manager, &dynMethod);
if (dynStatus != 0)
bdd_dynamic_reordering_disable(info->manager);
constrainedVector = ImgGetCofactoredVector(info, vector, constraint);
if (dynStatus != 0) {
bdd_dynamic_reordering(info->manager, dynMethod,
BDD_REORDER_VERBOSITY_DEFAULT);
}
return(constrainedVector);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| ImgComponent_t* ImgGetLatchComponent | ( | array_t * | vector | ) |
Function********************************************************************
Synopsis [Returns the first latch component.]
Description [Returns the first latch component.]
SideEffects []
Definition at line 1505 of file imgTfmUtil.c.
{
ImgComponent_t *comp;
int i;
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (!comp->intermediate)
return(comp);
}
return(NIL(ImgComponent_t));
}
Here is the caller graph for this function:
| float ImgPercentVectorDependency | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| int | length, | ||
| int * | nLongs | ||
| ) |
Function********************************************************************
Synopsis [Returns the percent of non-zero elements in dependency matrix.]
Description [Returns the percent of non-zero elements in dependency matrix.]
SideEffects []
Definition at line 1918 of file imgTfmUtil.c.
{
int i, j, index, nFuncs, nSupports, nLambdaLatches;
int count, total;
char *support;
ImgComponent_t *comp;
float percent;
int *occurs;
support = ALLOC(char, sizeof(char) * info->nVars);
memset(support, 0, sizeof(char) * info->nVars);
occurs = ALLOC(int, sizeof(int) * info->nVars);
memset(occurs, 0, sizeof(int) * info->nVars);
count = 0;
nFuncs = array_n(vector);
for (i = 0; i < nFuncs; i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
for (j = 0; j < info->nVars; j++) {
if (comp->support[j]) {
support[j] = 1;
count++;
occurs[i]++;
}
}
}
nSupports = 0;
for (i = 0; i < info->nVars; i++) {
if (support[i])
nSupports++;
}
nLambdaLatches = 0;
for (i = 0; i < nFuncs; i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
index = bdd_top_var_id(comp->var);
if (!support[index])
nLambdaLatches++;
}
FREE(support);
*nLongs = 0;
for (i = 0; i < info->nVars; i++) {
if (occurs[i] >= length)
(*nLongs)++;
}
total = (nFuncs - nLambdaLatches) * nSupports;
percent = (float)count / (float)total * 100.0;
return(percent);
}
| void ImgPrintVectorDependency | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| int | verbosity | ||
| ) |
Function********************************************************************
Synopsis [Prints vector dependencies with support.]
Description [Prints vector dependencies with support.]
SideEffects []
Definition at line 1792 of file imgTfmUtil.c.
{
int i, j, index, nFuncs, nSupports;
int nLambdaLatches, nConstLatches, nIntermediateVars;
int count, countStates, total;
int start, end;
char *support, line[80];
ImgComponent_t *comp;
if (verbosity == 0 || (!vector))
return;
support = ALLOC(char, sizeof(char) * info->nVars);
memset(support, 0, sizeof(char) * info->nVars);
count = countStates = 0;
nFuncs = array_n(vector);
for (i = 0; i < nFuncs; i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
for (j = 0; j < info->nVars; j++) {
if (comp->support[j]) {
support[j] = 1;
count++;
if (!st_lookup(info->quantifyVarsTable, (char *)(long)j, NIL(char *)))
countStates++;
}
}
}
nSupports = 0;
for (i = 0; i < info->nVars; i++) {
if (support[i])
nSupports++;
}
nLambdaLatches = 0;
nConstLatches = 0;
nIntermediateVars = 0;
for (i = 0; i < nFuncs; i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
index = bdd_top_var_id(comp->var);
if (!support[index])
nLambdaLatches++;
if (ImgSupportCount(info, comp->support) == 0)
nConstLatches++;
if (comp->intermediate)
nIntermediateVars++;
}
fprintf(vis_stdout, "** tfm info: #vars = %d(%d)\n",
info->nVars - nFuncs + nIntermediateVars, info->nVars);
fprintf(vis_stdout, "** tfm info: #input vars = %d\n",
info->nVars - (nFuncs - nIntermediateVars) * 2 - nIntermediateVars);
fprintf(vis_stdout, "** tfm info: #funcs = %d\n", nFuncs);
fprintf(vis_stdout, "** tfm info: #lambda funcs = %d\n", nLambdaLatches);
fprintf(vis_stdout, "** tfm info: #constant funcs = %d\n", nConstLatches);
fprintf(vis_stdout, "** tfm info: #intermediate funcs = %d\n",
nIntermediateVars);
fprintf(vis_stdout,
"Shared size of transition function vector is %10ld BDD nodes\n",
ImgVectorBddSize(vector));
total = nFuncs * nFuncs;
fprintf(vis_stdout,
"** tfm info: support distribution (state variables) = %.2f%%(%d out of %d)\n",
(float)countStates / (float)total * 100.0, countStates, total);
total = nFuncs * nSupports;
fprintf(vis_stdout,
"** tfm info: support distribution (all variables) = %.2f%% (%d out of %d)\n",
(float)count / (float)total * 100.0, count, total);
if (verbosity < 3) {
FREE(support);
return;
}
fprintf(vis_stdout, "*** function list ***\n");
for (i = 0; i < nFuncs; i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
index = bdd_top_var_id(comp->var);
fprintf(vis_stdout, "[%d] index = %d\n", i, index);
}
start = 0;
end = 74;
if (end >= nFuncs)
end = nFuncs - 1;
while (1) {
fprintf(vis_stdout, "========================================");
fprintf(vis_stdout, "========================================\n");
fprintf(vis_stdout, " 1234567890123456789012345678901234567890");
fprintf(vis_stdout, "12345678901234567890123456789012345\n");
fprintf(vis_stdout, "----------------------------------------");
fprintf(vis_stdout, "----------------------------------------\n");
for (i = 0; i < info->nVars; i++) {
if (!support[i])
continue;
if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *)))
continue;
for (j = start; j <= end; j++) {
comp = array_fetch(ImgComponent_t *, vector, j);
if (comp->support[i])
line[j - start] = '1';
else
line[j - start] = '.';
}
line[j - start] = '\0';
fprintf(vis_stdout, "%4d %s\n", i, line);
}
if (end >= nFuncs - 1)
break;
start += 75;
end += 75;
if (end >= nFuncs)
end = nFuncs - 1;
}
FREE(support);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void ImgSupportClear | ( | ImgTfmInfo_t * | info, |
| char * | support | ||
| ) |
Function********************************************************************
Synopsis [Clears a support array.]
Description [Clears a support array.]
SideEffects []
Definition at line 833 of file imgTfmUtil.c.
{
memset(support, 0, sizeof(char) * info->nVars);
}
Here is the caller graph for this function:
| void ImgSupportCopy | ( | ImgTfmInfo_t * | info, |
| char * | dsupport, | ||
| char * | ssupport | ||
| ) |
Function********************************************************************
Synopsis [Copies the supports of a component.]
Description [Copies the supports of a component. Here support is an array of char.]
SideEffects []
Definition at line 817 of file imgTfmUtil.c.
{
memcpy(dsupport, ssupport, sizeof(char) * info->nVars);
}
Here is the caller graph for this function:
| int ImgSupportCount | ( | ImgTfmInfo_t * | info, |
| char * | support | ||
| ) |
Function********************************************************************
Synopsis [Returns the number of support of a support array.]
Description [Returns the number of support of a support array.]
SideEffects []
Definition at line 873 of file imgTfmUtil.c.
{
int i, nSupports;
nSupports = 0;
for (i = 0; i < info->nVars; i++) {
if (support[i])
nSupports++;
}
return(nSupports);
}
Here is the caller graph for this function:
| void ImgSupportPrint | ( | ImgTfmInfo_t * | info, |
| char * | support | ||
| ) |
Function********************************************************************
Synopsis [Prints a support array.]
Description [Prints a support array.]
SideEffects []
Definition at line 849 of file imgTfmUtil.c.
{
int i;
for (i = 0; i < info->nVars; i++) {
if (support[i])
printf("*");
else
printf(".");
}
printf("\n");
}
| mdd_t* ImgTfmEliminateDependVars | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| array_t * | relationArray, | ||
| mdd_t * | states, | ||
| array_t ** | newVector, | ||
| mdd_t ** | dependRelations | ||
| ) |
Function********************************************************************
Synopsis [Eliminates dependent variables from transition function.]
Description [Eliminates dependent variables from a transition function. Returns a simplified copy of the given states if successful; NULL otherwise.]
SideEffects [vector is also modified.]
SeeAlso []
Definition at line 1282 of file imgTfmUtil.c.
{
int i, j;
int howMany = 0;
/* number of latches that can be eliminated */
mdd_t *var, *newStates, *abs, *positive, *phi;
mdd_t *tmp, *relation;
int nVars;
int nSupports; /* vars in the support of the state set */
int *candidates; /* vars to be considered for elimination */
double minStates;
ImgComponent_t *comp, *newComp;
if (dependRelations) {
*dependRelations = mdd_one(info->manager);
*newVector = array_alloc(ImgComponent_t *, 0);
}
newStates = mdd_dup(states);
nVars = info->nVars;
candidates = ALLOC(int, nVars);
if (candidates == NULL)
return(NULL);
comp = ImgComponentAlloc(info);
comp->func = newStates;
ImgComponentGetSupport(comp);
nSupports = 0;
for (i = 0 ; i < nVars; i++) {
if (comp->support[i]) {
candidates[nSupports] = i;
nSupports++;
}
}
comp->func = NIL(mdd_t);
ImgComponentFree(comp);
/* The signatures of the variables in a function are the number
** of minterms of the positive cofactors with respect to the
** variables themselves. */
signatures = bdd_cof_minterm(newStates);
if (signatures == NULL) {
FREE(candidates);
return(NULL);
}
/* We now extract a positive quantity which is higher for those
** variables that are closer to being essential. */
minStates = signatures[nSupports];
for (i = 0; i < nSupports; i++) {
double z = signatures[i] / minStates - 1.0;
signatures[i] = (z < 0.0) ? -z : z; /* make positive */
}
qsort((void *)candidates, nSupports, sizeof(int),
(int (*)(const void *, const void *))SignatureCompare);
FREE(signatures);
/* Now process the candidates in the given order. */
for (i = 0; i < nSupports; i++) {
var = bdd_var_with_index(info->manager, candidates[i]);
if (bdd_var_is_dependent(newStates, var)) {
abs = bdd_smooth_with_cube(newStates, var);
if (abs == NULL)
return(NULL);
positive = bdd_cofactor(newStates, var);
if (positive == NULL)
return(NULL);
phi = Img_MinimizeImage(positive, abs, Img_DefaultMinimizeMethod_c,
TRUE);
if (phi == NULL)
return(NULL);
mdd_free(positive);
if (bdd_size(phi) < IMG_MAX_DEP_SIZE) {
howMany++;
if (dependRelations) {
for (j = 0; j < array_n(vector); j++) {
comp = array_fetch(ImgComponent_t *, vector, j);
if (mdd_equal(comp->var, var))
continue;
newComp = ImgComponentCopy(info, comp);
array_insert_last(ImgComponent_t *, *newVector, newComp);
}
} else {
for (j = 0; j < array_n(vector); j++) {
comp = array_fetch(ImgComponent_t *, vector, j);
tmp = bdd_compose(comp->func, var, phi);
if (tmp == NULL)
return(NULL);
mdd_free(comp->func);
comp->func = tmp;
ImgSupportClear(info, comp->support);
ImgComponentGetSupport(comp);
}
}
if (relationArray) {
for (j = 0; j < array_n(relationArray); j++) {
relation = array_fetch(mdd_t *, relationArray, j);
if (dependRelations)
tmp = bdd_smooth_with_cube(relation, var);
else
tmp = bdd_compose(relation, var, phi);
mdd_free(relation);
array_insert(mdd_t *, relationArray, j, tmp);
}
}
mdd_free(newStates);
newStates = abs;
if (dependRelations) {
relation = mdd_xnor(var, phi);
tmp = mdd_and(*dependRelations, relation, 1, 1);
mdd_free(*dependRelations);
mdd_free(relation);
*dependRelations = tmp;
}
} else {
mdd_free(abs);
}
mdd_free(phi);
}
}
FREE(candidates);
if (howMany) {
if (info->imageVerbosity > 0)
(void)fprintf(vis_stdout, "Eliminated %d vars.\n", howMany);
info->averageFoundDependVars = (info->averageFoundDependVars *
(float)info->nFoundDependVars + (float)howMany) /
(float)(info->nFoundDependVars + 1);
info->nFoundDependVars++;
}
info->nPrevEliminatedFwd = howMany;
return(newStates);
} /* end of TfmEliminateDependVars */
Here is the call graph for this function:
Here is the caller graph for this function:
| long ImgVectorBddSize | ( | array_t * | vector | ) |
Function********************************************************************
Synopsis [Returns the shared BDD size of a vector.]
Description [Returns the shared BDD size of a vector.]
SideEffects []
Definition at line 671 of file imgTfmUtil.c.
{
array_t *nodeArray;
ImgComponent_t *comp;
int i, size;
nodeArray = array_alloc(mdd_t *, 0);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
array_insert_last(mdd_t *, nodeArray, comp->func);
}
size = bdd_size_multiple(nodeArray);
array_free(nodeArray);
return(size);
}
Here is the caller graph for this function:
| void ImgVectorConstrain | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | constraint, | ||
| array_t * | relationArray, | ||
| array_t ** | newVector, | ||
| mdd_t ** | cube, | ||
| array_t ** | newRelationArray, | ||
| mdd_t ** | cofactorCube, | ||
| mdd_t ** | abstractCube, | ||
| boolean | singleVarFlag | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Constrains a function vector with respect to a constraint.]
Description [Constrains a function vector with respect to a constraint.]
SideEffects []
Definition at line 91 of file imgTfmUtil.c.
{
mdd_t *new_, *res, *old, *tmp;
ImgComponent_t *comp, *comp1;
array_t *vector1;
int i, index;
int dynStatus, dynOff;
bdd_reorder_type_t dynMethod;
st_table *equivTable;
int *ptr, *regularPtr;
int n, pos;
mdd_t *cofactor, *abstract, *nsVar, *constIntermediate;
array_t *tmpRelationArray;
int size;
old = mdd_one(info->manager);
vector1 = array_alloc(ImgComponent_t *, 0);
dynStatus = 0;
if (singleVarFlag)
dynOff = 0;
else
dynOff = 1;
if (dynOff) {
dynStatus = bdd_reordering_status(info->manager, &dynMethod);
if (dynStatus != 0)
bdd_dynamic_reordering_disable(info->manager);
}
if (relationArray) {
cofactor = mdd_one(info->manager);
abstract = mdd_one(info->manager);
} else {
cofactor = NIL(mdd_t);
abstract = NIL(mdd_t);
}
if (info->nIntermediateVars) {
size = ImgVectorFunctionSize(vector);
if (size == array_n(vector))
constIntermediate = NIL(mdd_t);
else
constIntermediate = mdd_one(info->manager);
} else
constIntermediate = NIL(mdd_t);
n = 0;
equivTable = st_init_table(st_ptrcmp, st_ptrhash);
index = (int)bdd_top_var_id(constraint);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (!bdd_is_tautology(constraint, 1)) {
if (singleVarFlag) {
if (comp->support[index])
res = bdd_cofactor(comp->func, constraint);
else
res = mdd_dup(comp->func);
} else
res = bdd_cofactor(comp->func, constraint);
} else
res = mdd_dup(comp->func);
if (bdd_is_tautology(res, 1)) {
if (comp->intermediate) {
tmp = constIntermediate;
constIntermediate = mdd_and(tmp, comp->var, 1, 1);
mdd_free(tmp);
mdd_free(res);
continue;
}
new_ = mdd_and(comp->var, old, 1, 1);
mdd_free(old);
mdd_free(res);
old = new_;
if (cofactor) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = cofactor;
cofactor = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
} else if (bdd_is_tautology(res, 0)) {
if (comp->intermediate) {
tmp = constIntermediate;
constIntermediate = mdd_and(tmp, comp->var, 1, 0);
mdd_free(tmp);
mdd_free(res);
continue;
}
new_ = mdd_and(comp->var, old, 0, 1);
mdd_free(old);
mdd_free(res);
old = new_;
if (cofactor) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = cofactor;
cofactor = mdd_and(tmp, nsVar, 1, 0);
mdd_free(tmp);
mdd_free(nsVar);
}
} else {
if (comp->intermediate) {
comp1 = ImgComponentAlloc(info);
comp1->var = mdd_dup(comp->var);
comp1->func = res;
comp1->intermediate = 1;
if (mdd_equal(res, comp->func))
ImgSupportCopy(info, comp1->support, comp->support);
else
ImgComponentGetSupport(comp1);
array_insert_last(ImgComponent_t *, vector1, comp1);
n++;
continue;
}
ptr = (int *)bdd_pointer(res);
regularPtr = (int *)((unsigned long)ptr & ~01);
if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) {
comp1 = array_fetch(ImgComponent_t *, vector1, pos);
if (mdd_equal(res, comp1->func))
tmp = mdd_xnor(comp->var, comp1->var);
else
tmp = mdd_xor(comp->var, comp1->var);
new_ = mdd_and(tmp, old, 1, 1);
mdd_free(tmp);
mdd_free(old);
mdd_free(res);
old = new_;
if (abstract) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
} else {
comp1 = ImgComponentAlloc(info);
comp1->var = mdd_dup(comp->var);
comp1->func = res;
if (mdd_equal(res, comp->func))
ImgSupportCopy(info, comp1->support, comp->support);
else
ImgComponentGetSupport(comp1);
array_insert_last(ImgComponent_t *, vector1, comp1);
st_insert(equivTable, (char *)regularPtr, (char *)(long)n);
n++;
}
}
}
st_free_table(equivTable);
if (dynOff && dynStatus != 0) {
bdd_dynamic_reordering(info->manager, dynMethod,
BDD_REORDER_VERBOSITY_DEFAULT);
}
if (constIntermediate) {
if (!bdd_is_tautology(constIntermediate, 1)) {
mdd_t *tmpCofactor, *tmpAbstract;
if (relationArray) {
vector1 = ImgComposeConstIntermediateVars(info, vector1,
constIntermediate,
&tmpCofactor, &tmpAbstract,
&old, NIL(mdd_t *));
if (!bdd_is_tautology(tmpCofactor, 1)) {
tmp = cofactor;
cofactor = mdd_and(tmp, tmpCofactor, 1, 1);
mdd_free(tmp);
}
mdd_free(tmpCofactor);
if (!bdd_is_tautology(tmpAbstract, 1)) {
tmp = abstract;
abstract = mdd_and(tmp, tmpAbstract, 1, 1);
mdd_free(tmp);
}
mdd_free(tmpAbstract);
tmp = cofactor;
cofactor = mdd_and(tmp, constIntermediate, 1, 1);
mdd_free(tmp);
} else {
vector1 = ImgComposeConstIntermediateVars(info, vector1,
constIntermediate,
NIL(mdd_t *), NIL(mdd_t *),
&old, NIL(mdd_t *));
}
}
mdd_free(constIntermediate);
}
if (info->option->sortVectorFlag)
array_sort(vector1, CompareBddPointer);
if (relationArray && newRelationArray) {
if (singleVarFlag) {
*newRelationArray = relationArray;
tmp = cofactor;
cofactor = mdd_and(tmp, constraint, 1, 1);
mdd_free(tmp);
} else
*newRelationArray = ImgGetConstrainedRelationArray(info, relationArray,
constraint);
}
if (cofactorCube && abstractCube) {
if (cofactor)
*cofactorCube = cofactor;
if (abstract)
*abstractCube = abstract;
} else {
if (cofactor) {
if (bdd_is_tautology(cofactor, 1))
mdd_free(cofactor);
else {
tmpRelationArray = *newRelationArray;
*newRelationArray = ImgGetCofactoredRelationArray(tmpRelationArray,
cofactor);
mdd_free(cofactor);
if (tmpRelationArray != relationArray)
mdd_array_free(tmpRelationArray);
}
}
if (abstract) {
if (bdd_is_tautology(abstract, 1))
mdd_free(abstract);
else {
tmpRelationArray = *newRelationArray;
*newRelationArray = ImgGetAbstractedRelationArray(info->manager,
tmpRelationArray,
abstract);
mdd_free(abstract);
if (tmpRelationArray != relationArray)
mdd_array_free(tmpRelationArray);
}
}
}
*newVector = vector1;
*cube = old;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* ImgVectorCopy | ( | ImgTfmInfo_t * | info, |
| array_t * | vector | ||
| ) |
Function********************************************************************
Synopsis [Copies a vector.]
Description [Copies a vector.]
SideEffects []
Definition at line 699 of file imgTfmUtil.c.
{
array_t *newVector;
ImgComponent_t *comp, *newComp;
int i;
newVector = array_alloc(ImgComponent_t *, 0);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
newComp = ImgComponentCopy(info, comp);
array_insert_last(ImgComponent_t *, newVector, newComp);
}
return(newVector);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void ImgVectorFree | ( | array_t * | vector | ) |
Function********************************************************************
Synopsis [Frees a function vector.]
Description [Frees a function vector.]
SideEffects []
Definition at line 621 of file imgTfmUtil.c.
{
int i;
ImgComponent_t *comp;
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
ImgComponentFree(comp);
}
array_free(vector);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int ImgVectorFunctionSize | ( | array_t * | vector | ) |
Function********************************************************************
Synopsis [Returns the number of functions in a vector.]
Description [Returns the number of functions in a vector. Excludes the number of intermediate functions.]
SideEffects []
Definition at line 645 of file imgTfmUtil.c.
{
ImgComponent_t *comp;
int i, size;
size = 0;
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (!comp->intermediate)
size++;
}
return(size);
}
Here is the caller graph for this function:
| mdd_t* ImgVectorMinimize | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| mdd_t * | constraint, | ||
| mdd_t * | from, | ||
| array_t * | relationArray, | ||
| array_t ** | newVector, | ||
| mdd_t ** | cube, | ||
| array_t ** | newRelationArray, | ||
| mdd_t ** | cofactorCube, | ||
| mdd_t ** | abstractCube | ||
| ) |
Function********************************************************************
Synopsis [Minimizes a function vector and a from set with respect to an essential cube.]
Description [Minimizes a function vector and a from set with respect to an essential cube. This function is called during eliminating dependent variables.]
SideEffects []
Definition at line 346 of file imgTfmUtil.c.
{
mdd_t *new_, *res, *old, *tmp, *newFrom;
ImgComponent_t *comp, *comp1;
array_t *vector1;
int i;
st_table *equivTable;
int *ptr, *regularPtr;
int n, pos;
mdd_t *cofactor, *abstract, *nsVar, *constIntermediate;
array_t *tmpRelationArray;
int size;
if (from)
newFrom = mdd_dup(from);
else
newFrom = NIL(mdd_t);
if (cube)
old = mdd_one(info->manager);
else
old = NIL(mdd_t);
assert(newVector)
vector1 = array_alloc(ImgComponent_t *, 0);
if (relationArray) {
cofactor = mdd_one(info->manager);
abstract = mdd_one(info->manager);
} else {
cofactor = NIL(mdd_t);
abstract = NIL(mdd_t);
}
if (info->nIntermediateVars) {
size = ImgVectorFunctionSize(vector);
if (size == array_n(vector))
constIntermediate = NIL(mdd_t);
else
constIntermediate = mdd_one(info->manager);
} else
constIntermediate = NIL(mdd_t);
n = 0;
equivTable = st_init_table(st_ptrcmp, st_ptrhash);
for (i = 0; i < array_n(vector); i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
res = bdd_minimize(comp->func, constraint);
if (bdd_is_tautology(res, 1)) {
if (comp->intermediate) {
tmp = constIntermediate;
constIntermediate = mdd_and(tmp, comp->var, 1, 1);
mdd_free(tmp);
mdd_free(res);
continue;
}
if (newFrom) {
tmp = newFrom;
newFrom = bdd_cofactor(tmp, comp->var);
mdd_free(tmp);
}
if (old) {
new_ = mdd_and(comp->var, old, 1, 1);
mdd_free(old);
mdd_free(res);
old = new_;
}
if (cofactor) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = cofactor;
cofactor = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
} else if (bdd_is_tautology(res, 0)) {
if (comp->intermediate) {
tmp = constIntermediate;
constIntermediate = mdd_and(tmp, comp->var, 1, 0);
mdd_free(tmp);
mdd_free(res);
continue;
}
if (newFrom) {
tmp = newFrom;
new_ = mdd_not(comp->var);
newFrom = bdd_cofactor(tmp, new_);
mdd_free(tmp);
mdd_free(new_);
}
if (old) {
new_ = mdd_and(comp->var, old, 0, 1);
mdd_free(old);
mdd_free(res);
old = new_;
}
if (cofactor) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = cofactor;
cofactor = mdd_and(tmp, nsVar, 1, 0);
mdd_free(tmp);
mdd_free(nsVar);
}
} else {
if (comp->intermediate) {
comp1 = ImgComponentAlloc(info);
comp1->var = mdd_dup(comp->var);
comp1->func = res;
comp1->intermediate = 1;
if (mdd_equal(res, comp->func))
ImgSupportCopy(info, comp1->support, comp->support);
else
ImgComponentGetSupport(comp1);
array_insert_last(ImgComponent_t *, vector1, comp1);
n++;
continue;
}
ptr = (int *)bdd_pointer(res);
regularPtr = (int *)((unsigned long)ptr & ~01);
if (st_lookup_int(equivTable, (char *)regularPtr, &pos)) {
comp1 = array_fetch(ImgComponent_t *, vector1, pos);
if (newFrom) {
if (mdd_equal(res, comp1->func)) {
tmp = newFrom;
newFrom = bdd_compose(tmp, comp->var, comp1->var);
mdd_free(tmp);
} else {
tmp = newFrom;
new_ = mdd_not(comp1->var);
newFrom = bdd_compose(tmp, comp->var, new_);
mdd_free(tmp);
mdd_free(new_);
}
}
if (old) {
if (mdd_equal(res, comp1->func))
tmp = mdd_xnor(comp->var, comp1->var);
else
tmp = mdd_xor(comp->var, comp1->var);
new_ = mdd_and(tmp, old, 1, 1);
mdd_free(tmp);
mdd_free(old);
old = new_;
}
mdd_free(res);
if (abstract) {
nsVar = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
tmp = abstract;
abstract = mdd_and(tmp, nsVar, 1, 1);
mdd_free(tmp);
mdd_free(nsVar);
}
} else {
comp1 = ImgComponentAlloc(info);
comp1->var = mdd_dup(comp->var);
comp1->func = res;
if (mdd_equal(res, comp->func))
ImgSupportCopy(info, comp1->support, comp->support);
else
ImgComponentGetSupport(comp1);
array_insert_last(ImgComponent_t *, vector1, comp1);
st_insert(equivTable, (char *)regularPtr, (char *)(long)n);
n++;
}
}
}
st_free_table(equivTable);
if (constIntermediate) {
if (!bdd_is_tautology(constIntermediate, 1)) {
mdd_t *tmpCofactor, *tmpAbstract;
if (relationArray) {
vector1 = ImgComposeConstIntermediateVars(info, vector1,
constIntermediate,
&tmpCofactor, &tmpAbstract,
&old, NIL(mdd_t *));
if (!bdd_is_tautology(tmpCofactor, 1)) {
tmp = cofactor;
cofactor = mdd_and(tmp, tmpCofactor, 1, 1);
mdd_free(tmp);
}
mdd_free(tmpCofactor);
if (!bdd_is_tautology(tmpAbstract, 1)) {
tmp = abstract;
abstract = mdd_and(tmp, tmpAbstract, 1, 1);
mdd_free(tmp);
}
mdd_free(tmpAbstract);
tmp = cofactor;
cofactor = mdd_and(tmp, constIntermediate, 1, 1);
mdd_free(tmp);
} else {
vector1 = ImgComposeConstIntermediateVars(info, vector1,
constIntermediate,
NIL(mdd_t *), NIL(mdd_t *),
&old, NIL(mdd_t *));
}
}
mdd_free(constIntermediate);
}
if (info->option->sortVectorFlag)
array_sort(vector1, CompareBddPointer);
if (newRelationArray)
*newRelationArray = relationArray;
if (cofactorCube && abstractCube) {
if (cofactor) {
if (bdd_is_tautology(cofactor, 1)) {
*cofactorCube = mdd_dup(constraint);
mdd_free(cofactor);
} else {
tmp = cofactor;
cofactor = mdd_and(tmp, constraint, 1, 1);
mdd_free(tmp);
*cofactorCube = cofactor;
}
}
if (abstract)
*abstractCube = abstract;
} else {
if (cofactor) {
if (bdd_is_tautology(cofactor, 1))
mdd_free(cofactor);
else {
tmp = cofactor;
cofactor = mdd_and(tmp, constraint, 1, 1);
mdd_free(tmp);
if (newRelationArray) {
*newRelationArray = ImgGetCofactoredRelationArray(relationArray,
cofactor);
} else
ImgCofactorRelationArray(relationArray, cofactor);
mdd_free(cofactor);
}
}
if (abstract) {
if (bdd_is_tautology(abstract, 1))
mdd_free(abstract);
else {
if (newRelationArray) {
tmpRelationArray = *newRelationArray;
*newRelationArray = ImgGetAbstractedRelationArray(info->manager,
tmpRelationArray,
abstract);
if (tmpRelationArray != relationArray)
mdd_array_free(tmpRelationArray);
} else
ImgAbstractRelationArray(info->manager, relationArray, abstract);
mdd_free(abstract);
}
}
}
if (*newVector == vector)
ImgVectorFree(vector);
*newVector = vector1;
if (cube)
*cube = old;
return(newFrom);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void ImgWriteSupportMatrix | ( | ImgTfmInfo_t * | info, |
| array_t * | vector, | ||
| array_t * | relationArray, | ||
| char * | string | ||
| ) |
Function********************************************************************
Synopsis [Writes a gnuplot file with support matrix.]
Description [Writes a gnuplot file with support matrix.]
SideEffects []
Definition at line 1981 of file imgTfmUtil.c.
{
int i, j, id, nFuncs, nRelations, nRows, nSupports;
int *row, col, varType;
char *support, **relationSupport;
ImgComponent_t *comp;
FILE *fout;
mdd_t *relation, *var;
char *filename;
support = ALLOC(char, sizeof(char) * info->nVars);
memset(support, 0, sizeof(char) * info->nVars);
nRows = 0;
if (vector)
nRows += array_n(vector);
if (relationArray)
nRows += array_n(relationArray);
row = ALLOC(int, sizeof(int) * nRows);
if (string)
filename = string;
else
filename = "support.mat";
fout = fopen(filename, "w");
nRows = 0;
if (vector) {
nFuncs = array_n(vector);
for (i = 0; i < nFuncs; i++) {
comp = array_fetch(ImgComponent_t *, vector, i);
if (ImgSupportCount(info, comp->support) == 0) {
row[i] = -1;
continue;
}
row[i] = nRows;
nRows++;
if (info->option->writeSupportMatrixWithYvars) {
var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
id = (int)bdd_top_var_id(var);
support[id] = 1;
mdd_free(var);
}
for (j = 0; j < info->nVars; j++) {
if (comp->support[j])
support[j] = 1;
}
}
} else
nFuncs = 0;
relationSupport = 0;
if (relationArray && array_n(relationArray) > 0) {
comp = ImgComponentAlloc(info);
nRelations = 0;
relationSupport = ALLOC(char *, sizeof(char *) * array_n(relationArray));
for (i = 0; i < array_n(relationArray); i++) {
relation = array_fetch(mdd_t *, relationArray, i);
comp->func = relation;
ImgSupportClear(info, comp->support);
ImgComponentGetSupport(comp);
if (ImgSupportCount(info, comp->support) <= 1) {
row[i + nFuncs] = -1;
relationSupport[i] = NIL(char);
continue;
}
row[i + nFuncs] = nRows;
nRows++;
for (j = 0; j < info->nVars; j++) {
if (comp->support[j])
support[j] = 1;
}
relationSupport[i] = ALLOC(char, sizeof(char) * info->nVars);
memcpy(relationSupport[i], comp->support, sizeof(char) * info->nVars);
nRelations++;
}
comp->func = NIL(mdd_t);
ImgComponentFree(comp);
} else
nRelations = 0;
nSupports = 0;
for (i = 0; i < info->nVars; i++) {
if (support[i]) {
if (!info->option->writeSupportMatrixWithYvars &&
st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) {
continue;
}
nSupports++;
}
}
col = 0;
for (i = 0; i < info->nVars; i++) {
if (!support[i])
continue;
if (st_lookup(info->rangeVarsTable, (char *)(long)i, NIL(char *))) {
if (info->option->writeSupportMatrixWithYvars)
varType = 3;
else
continue;
} else if (st_lookup(info->quantifyVarsTable, (char *)(long)i, NIL(char *)))
varType = 2;
else
varType = 1;
for (j = 0; j < nFuncs; j++) {
comp = array_fetch(ImgComponent_t *, vector, j);
if (comp->support[i]) {
if (info->option->writeSupportMatrixReverseRow) {
if (info->option->writeSupportMatrixReverseCol) {
fprintf(fout, "%d %d %d\n", nSupports - col, nRows - row[j],
varType);
} else
fprintf(fout, "%d %d %d\n", col + 1, nRows - row[j], varType);
} else {
if (info->option->writeSupportMatrixReverseCol)
fprintf(fout, "%d %d %d\n", nSupports - col, row[j] + 1, varType);
else
fprintf(fout, "%d %d %d\n", col + 1, row[j] + 1, varType);
}
} else if (varType == 3) {
var = ImgSubstitute(comp->var, info->functionData, Img_D2R_c);
id = (int)bdd_top_var_id(var);
mdd_free(var);
if (id == i) {
if (info->option->writeSupportMatrixReverseRow) {
if (info->option->writeSupportMatrixReverseCol)
fprintf(fout, "%d %d 3\n", nSupports - col, nRows - row[j]);
else
fprintf(fout, "%d %d 3\n", col + 1, nRows - row[j]);
} else {
if (info->option->writeSupportMatrixReverseCol)
fprintf(fout, "%d %d 3\n", nSupports - col, row[j] + 1);
else
fprintf(fout, "%d %d 3\n", col + 1, row[j] + 1);
}
}
}
}
if (relationArray) {
for (j = 0; j < array_n(relationArray); j++) {
if (relationSupport[j] && relationSupport[j][i]) {
if (info->option->writeSupportMatrixReverseRow) {
if (info->option->writeSupportMatrixReverseCol) {
fprintf(fout, "%d %d %d\n", nSupports - col,
nRows - row[j + nFuncs], varType);
} else {
fprintf(fout, "%d %d %d\n", col + 1, nRows - row[j + nFuncs],
varType);
}
} else {
if (info->option->writeSupportMatrixReverseCol) {
fprintf(fout, "%d %d %d\n", nSupports - col, row[j + nFuncs] + 1,
varType);
} else {
fprintf(fout, "%d %d %d\n", col + 1, row[j + nFuncs] + 1,
varType);
}
}
}
}
}
col++;
}
fclose(fout);
FREE(support);
FREE(row);
if (nRelations) {
for (i = 0; i < nRelations; i++)
FREE(relationSupport[i]);
FREE(relationSupport);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int SignatureCompare | ( | int * | ptrX, |
| int * | ptrY | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Comparison function used by qsort.]
Description [Comparison function used by qsort to order the variables according to their signatures.]
SideEffects [None]
Definition at line 2171 of file imgTfmUtil.c.
{
if (signatures[*ptrY] > signatures[*ptrX])
return(1);
if (signatures[*ptrY] < signatures[*ptrX])
return(-1);
return(0);
} /* end of SignatureCompare */
Here is the caller graph for this function:
Variable Documentation
double* signatures [static] |
Definition at line 53 of file imgTfmUtil.c.
char rcsid [] UNUSED = "$Id: imgTfmUtil.c,v 1.23 2005/04/23 14:30:55 jinh Exp $" [static] |
CFile***********************************************************************
FileName [imgTfmUtil.c]
PackageName [img]
Synopsis [Routines for image computation using transition function method.]
SeeAlso []
Author [In-Ho Moon]
Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of Colorado. 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 COLORADO 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 COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF COLORADO 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 COLORADO HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
Definition at line 35 of file imgTfmUtil.c.
