#include "synthInt.h"
Include dependency graph for synthSimple.c:
Go to the source code of this file.
Functions | |
| static int | CountZddLeafLiterals (bdd_manager *dd, bdd_node *node) |
| MlTree * | SynthSimpleFactorTree (bdd_manager *dd, st_table *table, bdd_node *f, int level, int *ref, MlTree *comp_d_tree, int comp_d_flag, MlTree *bring, int verbosity) |
| bdd_node * | SynthFindBiggerDivisorInList (bdd_manager *dd, st_table *table, bdd_node *f, bdd_node *d, int *found, int *comp_d_flag, MlTree **comp_d_tree, int verbosity) |
| MlTree * | SynthGetFactorTreeWithCommonDivisor (bdd_manager *dd, st_table *table, MlTree *(*factoring_func)(bdd_manager *, st_table *, bdd_node *, int, int *, MlTree *, int, MlTree *, int), bdd_node *f, bdd_node *d, int level, int *ref, int verbosity) |
| MlTree * | SynthPostFactorTree (bdd_manager *dd, st_table *table, bdd_node *f, bdd_node *q, bdd_node *d, MlTree *bring, MlTree *comp_d_tree, int comp_d_flag, char *message, int *ref, int verbosity) |
| MlTree * | SynthFactorTreeRecur (bdd_manager *dd, st_table *table, MlTree *(*factoring_func)(bdd_manager *, st_table *, bdd_node *, int, int *, MlTree *, int, MlTree *, int), bdd_node *f, bdd_node *q, bdd_node *d, bdd_node *r, bdd_node *m, MlTree *q_tree, MlTree *d_tree, MlTree *r_tree, MlTree *comp_q_tree, MlTree *comp_d_tree, MlTree *comp_r_tree, MlTree *bring, int level, char *space, char *message, int *ref, int verbosity) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: synthSimple.c,v 1.36 2005/04/23 14:37:51 jinh Exp $" |
| int | CompMode |
| int | UseMtree |
| int | UseCommonDivisor |
| int | TryNodeSharing |
| int | Resubstitution |
| int | RemainderComplement |
| int | noMemoryFlag |
| int | VerifyTreeMode |
Function Documentation
| static int CountZddLeafLiterals | ( | bdd_manager * | dd, |
| bdd_node * | node | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Counts the number of literals of a leaf node.]
Description [Counts the number of literals of a leaf node.]
SideEffects []
SeeAlso []
Definition at line 1172 of file synthSimple.c.
{
int i, *support;
int count = 0;
int sizeZ = bdd_num_zdd_vars(dd);
support = ALLOC(int, sizeZ);
if (!support)
return(-1);
(void)memset((void *)support, 0, sizeof(int) * sizeZ);
SynthZddSupportStep(bdd_regular(node), support);
SynthZddClearFlag(bdd_regular(node));
for (i = 0; i < sizeZ; i++) {
if (support[i])
count++;
}
FREE(support);
return(count);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| MlTree* SynthFactorTreeRecur | ( | bdd_manager * | dd, |
| st_table * | table, | ||
| MlTree *(*)(bdd_manager *, st_table *, bdd_node *, int, int *, MlTree *, int, MlTree *, int) | factoring_func, | ||
| bdd_node * | f, | ||
| bdd_node * | q, | ||
| bdd_node * | d, | ||
| bdd_node * | r, | ||
| bdd_node * | m, | ||
| MlTree * | q_tree, | ||
| MlTree * | d_tree, | ||
| MlTree * | r_tree, | ||
| MlTree * | comp_q_tree, | ||
| MlTree * | comp_d_tree, | ||
| MlTree * | comp_r_tree, | ||
| MlTree * | bring, | ||
| int | level, | ||
| char * | space, | ||
| char * | message, | ||
| int * | ref, | ||
| int | verbosity | ||
| ) |
Function********************************************************************
Synopsis [Recursive procedure of SynthSimpleFactorTree and SynthGenericFactorTree.]
Description [Recursive procedure of SynthSimpleFactorTree and SynthGenericFactorTree.]
SideEffects []
SeeAlso [SynthSimpleFactorTree SynthGenericFactorTree]
Definition at line 782 of file synthSimple.c.
{
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
int q_tree_exist, d_tree_exist, r_tree_exist;
MlTree *m_tree;
MlTree *tree, *tmp_tree;
int q_ref, d_ref, r_ref, m_ref;
char comp_mess[120];
int comp_flag;
q_ref = d_ref = r_ref = 0;
if (verbosity > 1)
(void) fprintf(vis_stdout,"%s[%d] quotient\n", space, level);
q_tree_exist = 0;
if (q_tree) {
q_ref = 1;
q_tree_exist = 1;
} else if (comp_q_tree) {
q_tree = comp_q_tree;
q_ref = 1;
if (verbosity > 1) {
sprintf(comp_mess, "%s\t(C) : ", space);
SynthPrintZddTreeMessage(dd, q, comp_mess);
}
} else {
q_tree = (* factoring_func)(dd, table, q, level + 1,
&q_ref, NULL, 0, NULL, verbosity);
if (!q_tree)
return(NULL);
if (MlTree_IsComplement(q_tree)) {
q_tree = MlTree_Regular(q_tree);
comp_q_tree = q_tree;
} else
bdd_ref(q_tree->node);
}
tmp_tree = q_tree;
q_tree = SynthCheckAndMakeComplement(dd, table, q_tree, &comp_flag,
verbosity);
if (!q_tree) {
if (comp_q_tree != tmp_tree)
bdd_recursive_deref_zdd(dd, tmp_tree->node);
if (q_ref == 0)
SynthFreeMlTree(MlTree_Regular(tmp_tree), 1);
return(NULL);
} else if (q_tree != tmp_tree) {
if (comp_flag)
comp_q_tree = q_tree;
q_ref = 1;
}
if (verbosity > 1)
(void)fprintf(vis_stdout,"%s[%d] divisor\n", space, level);
d_tree_exist = 0;
if (d_tree) {
d_ref = 1;
d_tree_exist = 1;
} else if (comp_d_tree) {
d_tree = comp_d_tree;
d_ref = 1;
if (verbosity > 1) {
sprintf(comp_mess, "%s\t(C) : ", space);
SynthPrintZddTreeMessage(dd, d, comp_mess);
}
} else {
d_tree = (* factoring_func)(dd, table, d, level + 1, &d_ref,
NULL, 0, NULL, verbosity);
if (!d_tree) {
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_tree->node);
if (q_ref == 0)
SynthFreeMlTree(MlTree_Regular(q_tree), 1);
return(NULL);
}
if (MlTree_IsComplement(d_tree)) {
d_tree = MlTree_Regular(d_tree);
comp_d_tree = d_tree;
} else
bdd_ref(d_tree->node);
}
tmp_tree = d_tree;
d_tree = SynthCheckAndMakeComplement(dd, table, d_tree, &comp_flag,
verbosity);
if (!d_tree) {
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_tree->node);
if (comp_d_tree != tmp_tree)
bdd_recursive_deref_zdd(dd, tmp_tree->node);
if (q_ref == 0)
SynthFreeMlTree(MlTree_Regular(q_tree), 1);
if (d_ref == 0)
SynthFreeMlTree(MlTree_Regular(tmp_tree), 1);
return(NULL);
} else if (d_tree != tmp_tree) {
if (comp_flag)
comp_d_tree = d_tree;
d_ref = 1;
}
m_tree = (MlTree *)NULL;
m_ref = 0;
if (UseMtree && m != f) {
m_tree = SynthFindOrCreateMlTree(table, dd, m, 0, 1, &m_ref, verbosity);
if (!m_tree) {
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_tree->node);
if (comp_d_tree != d_tree)
bdd_recursive_deref_zdd(dd, d_tree->node);
if (q_ref == 0)
SynthFreeMlTree(MlTree_Regular(q_tree), 1);
if (d_ref == 0)
SynthFreeMlTree(MlTree_Regular(d_tree), 1);
return(NULL);
}
if (m_ref == 0) {
m_tree->q = q_tree;
m_tree->d = d_tree;
m_tree->r = (MlTree *)NULL;
if (comp_q_tree)
m_tree->q_comp = 1;
if (comp_d_tree)
m_tree->d_comp = 1;
m_tree->q_ref = q_ref;
m_tree->d_ref = d_ref;
m_tree->r_ref = 0;
tmp_tree = m_tree;
m_tree = SynthCheckAndMakeComplement(dd, table, m_tree, &comp_flag,
verbosity);
if (!m_tree) {
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_tree->node);
if (comp_d_tree != d_tree)
bdd_recursive_deref_zdd(dd, d_tree->node);
if (q_ref == 0)
SynthFreeMlTree(MlTree_Regular(q_tree), 1);
if (d_ref == 0)
SynthFreeMlTree(MlTree_Regular(d_tree), 1);
return(NULL);
} else if (m_tree == tmp_tree)
SynthPutMlTreeInList(dd, m_tree, 1);
else {
if (m_tree->candidate)
SynthPutMlTreeInList(dd, m_tree, 1);
else
m_tree = NIL(MlTree);
}
if (m_tree && VerifyTreeMode) {
SynthVerifyTree(dd, m_tree, 0);
SynthVerifyMlTable(dd, table);
}
}
}
if (verbosity > 1)
(void)fprintf(vis_stdout,"%s[%d] remainder\n", space, level);
r_tree_exist = 0;
if (r_tree) {
r_ref = 1;
r_tree_exist = 1;
} else if (comp_r_tree) {
r_tree = comp_r_tree;
r_ref = 1;
if (verbosity > 1) {
sprintf(comp_mess, "%s\t(C) : ", space);
SynthPrintZddTreeMessage(dd, r, comp_mess);
}
} else if (comp_d_tree) {
r_tree = (* factoring_func)(dd, table, r, level + 1,
&r_ref, NULL, 0, NULL, verbosity);
if (!r_tree) {
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_tree->node);
if (comp_d_tree != d_tree)
bdd_recursive_deref_zdd(dd, d_tree->node);
if (q_ref == 0)
SynthFreeMlTree(MlTree_Regular(q_tree), 1);
if (d_ref == 0)
SynthFreeMlTree(MlTree_Regular(d_tree), 1);
if (m_tree && m_ref == 0)
SynthFreeMlTree(MlTree_Regular(m_tree), 1);
return(NULL);
}
if (MlTree_IsComplement(r_tree)) {
r_tree = MlTree_Regular(r_tree);
comp_r_tree = r_tree;
} else
bdd_ref(r_tree->node);
} else {
if (Resubstitution) {
r_tree = (* factoring_func)(dd, table, r, level + 1,
&r_ref, d_tree, 1, NULL, verbosity);
if (!r_tree && (bdd_read_reordered_field(dd) || noMemoryFlag == 1)) {
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_tree->node);
if (comp_d_tree != d_tree)
bdd_recursive_deref_zdd(dd, d_tree->node);
if (q_ref == 0)
SynthFreeMlTree(MlTree_Regular(q_tree), 1);
if (d_ref == 0)
SynthFreeMlTree(MlTree_Regular(d_tree), 1);
if (m_tree && m_ref == 0)
SynthFreeMlTree(MlTree_Regular(m_tree), 1);
return(NULL);
}
}
if (!r_tree) {
r_tree = (* factoring_func)(dd, table, r, level + 1,
&r_ref, NULL, 0, NULL, verbosity);
if (!r_tree) {
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_tree->node);
if (comp_d_tree != d_tree)
bdd_recursive_deref_zdd(dd, d_tree->node);
if (q_ref == 0)
SynthFreeMlTree(MlTree_Regular(q_tree), 1);
if (d_ref == 0)
SynthFreeMlTree(MlTree_Regular(d_tree), 1);
if (m_tree && m_ref == 0)
SynthFreeMlTree(MlTree_Regular(m_tree), 1);
return(NULL);
}
} else {
if (r != one && r != zero)
SynthSetSharedFlag(dd, d_tree);
}
if (MlTree_IsComplement(r_tree)) {
r_tree = MlTree_Regular(r_tree);
comp_r_tree = r_tree;
} else
bdd_ref(r_tree->node);
}
if (RemainderComplement) {
tmp_tree = r_tree;
r_tree = SynthCheckAndMakeComplement(dd, table, r_tree, &comp_flag,
verbosity);
if (!r_tree) {
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_tree->node);
if (comp_d_tree != d_tree)
bdd_recursive_deref_zdd(dd, d_tree->node);
if (comp_r_tree != tmp_tree)
bdd_recursive_deref_zdd(dd, tmp_tree->node);
if (q_ref == 0)
SynthFreeMlTree(MlTree_Regular(q_tree), 1);
if (d_ref == 0)
SynthFreeMlTree(MlTree_Regular(d_tree), 1);
if (r_ref == 0)
SynthFreeMlTree(MlTree_Regular(tmp_tree), 1);
if (m_tree && m_ref == 0)
SynthFreeMlTree(MlTree_Regular(m_tree), 1);
return(NULL);
} else if (r_tree != tmp_tree) {
if (comp_flag)
comp_r_tree = r_tree;
r_ref = 1;
}
}
if ((!q_tree_exist) && (!comp_q_tree))
bdd_recursive_deref_zdd(dd, q_tree->node);
if ((!d_tree_exist) && (!comp_d_tree))
bdd_recursive_deref_zdd(dd, d_tree->node);
if ((!r_tree_exist) && (!comp_r_tree))
bdd_recursive_deref_zdd(dd, r_tree->node);
if (bring) {
tree = bring;
tree->leaf = 0;
tree->q = q_tree;
tree->d = d_tree;
tree->r = r_tree;
if (comp_q_tree)
tree->q_comp = 1;
if (comp_d_tree)
tree->d_comp = 1;
if (comp_r_tree)
tree->r_comp = 1;
tree->q_ref = q_ref;
tree->d_ref = d_ref;
tree->r_ref = r_ref;
if (UseMtree && m_tree && m_ref == 0) {
MlTree_Regular(m_tree)->r = tree;
if (m_tree->r->id == 0) {
assert(0);
/*
if (!SynthUseCandidate(table, dd, m_tree, verbosity)) {
SynthFreeMlTree(MlTree_Regular(m_tree), 1);
return(NULL);
}
*/
}
}
if (verbosity > 1)
SynthPrintMlTreeMessage(dd, tree, message);
if (VerifyTreeMode) {
SynthVerifyTree(dd, tree, 0);
SynthVerifyMlTable(dd, table);
}
return(tree);
}
tree = SynthFindOrCreateMlTree(table, dd, f, 0, 0, ref, verbosity);
if (!tree) {
if (q_ref == 0)
SynthFreeMlTree(MlTree_Regular(q_tree), 1);
if (d_ref == 0)
SynthFreeMlTree(MlTree_Regular(d_tree), 1);
if (r_ref == 0)
SynthFreeMlTree(MlTree_Regular(r_tree), 1);
if (m_tree && m_ref == 0)
SynthFreeMlTree(MlTree_Regular(m_tree), 1);
return(NULL);
}
if (*ref == 1)
(void)fprintf(vis_stdout, "** synth warning: May be duplicate.\n");
tree->q = q_tree;
tree->d = d_tree;
tree->r = r_tree;
if (comp_q_tree)
tree->q_comp = 1;
if (comp_d_tree)
tree->d_comp = 1;
if (comp_r_tree)
tree->r_comp = 1;
tree->q_ref = q_ref;
tree->d_ref = d_ref;
tree->r_ref = r_ref;
if (UseMtree && m_tree && m_ref == 0) {
MlTree_Regular(m_tree)->r = tree;
if (m_tree->r->id == 0) {
assert(0);
/*
if (!SynthUseCandidate(table, dd, m_tree, verbosity)) {
SynthFreeMlTree(MlTree_Regular(tree), 1);
SynthFreeMlTree(MlTree_Regular(m_tree), 1);
return(NULL);
}
*/
}
}
if (verbosity > 1)
SynthPrintMlTreeMessage(dd, tree, message);
SynthPutMlTreeInList(dd, tree, 0);
if (VerifyTreeMode) {
SynthVerifyTree(dd, tree, 0);
SynthVerifyMlTable(dd, table);
}
return(tree);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bdd_node* SynthFindBiggerDivisorInList | ( | bdd_manager * | dd, |
| st_table * | table, | ||
| bdd_node * | f, | ||
| bdd_node * | d, | ||
| int * | found, | ||
| int * | comp_d_flag, | ||
| MlTree ** | comp_d_tree, | ||
| int | verbosity | ||
| ) |
Function********************************************************************
Synopsis [Finds a bigger divisor in divisor list.]
Description [Finds a bigger divisor in divisor list.]
SideEffects []
SeeAlso [SynthSimpleFactorTree SynthGenericFactorTree]
Definition at line 342 of file synthSimple.c.
{
bdd_node *zero = bdd_read_zero(dd);
int size, nSupports;
unsigned int *support;
int flag;
int nL, nLiterals;
bdd_node *candy;
MlTree *cur;
bdd_node *q;
nSupports = SynthGetSupportCount(dd, d);
size = bdd_num_zdd_vars(dd) / (sizeof(unsigned int) * 8) + 1;
support = ALLOC(unsigned int, size);
SynthGetSupportMask(dd, f, support);
flag = 0;
cur = SynthGetHeadTreeOfSize(SynthGetLiteralCount(dd, f) - 1);
nLiterals = CountZddLeafLiterals(dd, d);
if (nLiterals == -1) {
noMemoryFlag = 1;
FREE(support);
bdd_recursive_deref_zdd(dd, d);
return(NULL);
}
while (cur) {
if (cur->nLiterals < nSupports)
break;
nL = CountZddLeafLiterals(dd, cur->node);
if ((!SynthIsSubsetOfSupport(size, cur->support, support)) ||
nL < nLiterals) {
flag = 0;
cur = cur->next;
continue;
}
if (flag)
candy = cur->complement;
else
candy = cur->node;
q = (* SynthGetZddDivideFunc())(dd, f, candy);
if (!q) {
FREE(support);
bdd_recursive_deref_zdd(dd, d);
return(NULL);
}
bdd_ref(q);
bdd_recursive_deref_zdd(dd, q);
if (q != zero) {
if (MlTree_Regular(cur)->candidate) {
if (!SynthUseCandidate(table, dd, cur, verbosity)) {
FREE(support);
bdd_recursive_deref_zdd(dd, d);
return(NULL);
}
}
*found = 1;
*comp_d_flag = flag;
*comp_d_tree = cur;
bdd_recursive_deref_zdd(dd, d);
d = candy;
bdd_ref(d);
break;
}
if (flag == 0 && cur->complement)
flag = 1;
else {
cur = cur->next;
flag = 0;
}
}
FREE(support);
return(d);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| MlTree* SynthGetFactorTreeWithCommonDivisor | ( | bdd_manager * | dd, |
| st_table * | table, | ||
| MlTree *(*)(bdd_manager *, st_table *, bdd_node *, int, int *, MlTree *, int, MlTree *, int) | factoring_func, | ||
| bdd_node * | f, | ||
| bdd_node * | d, | ||
| int | level, | ||
| int * | ref, | ||
| int | verbosity | ||
| ) |
Function********************************************************************
Synopsis [Factorizes a function with a common divisor if it exists.]
Description [Factorizes a function with a common divisor if it exists.]
SideEffects []
SeeAlso [SynthSimpleFactorTree SynthGenericFactorTree]
Definition at line 439 of file synthSimple.c.
{
bdd_node *zero = bdd_read_zero(dd);
bdd_node *cd;
bdd_node *q;
MlTree *tree, *q_tree, *d_tree, *r_tree;
int q_ref, d_ref, r_ref;
MlTree *comp_q_tree = (MlTree *)NULL;
MlTree *comp_d_tree = (MlTree *)NULL;
MlTree *comp_r_tree = (MlTree *)NULL;
int q_tree_exist;
MlTree *tmp_tree;
char message[120];
char space[100];
char comp_mess[120];
int comp_flag;
q_ref = d_ref = r_ref = 0;
if (verbosity > 1) {
SynthGetSpaceString(space, level * 2, 80);
sprintf(message, "%s[%d]out : ", space, level);
}
cd = SynthZddCommonDivisor(dd, f);
if (cd) {
bdd_recursive_deref_zdd(dd, d);
d = cd;
bdd_ref(d);
q = (* SynthGetZddDivideFunc())(dd, f, d);
if (!q) {
bdd_recursive_deref_zdd(dd, d);
return(NULL);
}
bdd_ref(q);
d_tree = (MlTree *)NULL;
if (st_lookup(table, (char *)d, &d_tree)) {
SynthSetSharedFlag(dd, d_tree);
if (MlTree_Regular(d_tree)->candidate) {
if (!SynthUseCandidate(table, dd, d_tree, verbosity)) {
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
return(NULL);
}
}
if (MlTree_IsComplement(d_tree)) {
d_tree = MlTree_Regular(d_tree);
comp_d_tree = d_tree;
}
d_ref = 1;
} else {
d_tree = SynthFindOrCreateMlTree(table, dd, d, 1, 0, &d_ref, verbosity);
if (!d_tree) {
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
return(NULL);
}
if (MlTree_IsComplement(d_tree)) {
d_tree = MlTree_Regular(d_tree);
comp_d_tree = d_tree;
}
tmp_tree = d_tree;
d_tree = SynthCheckAndMakeComplement(dd, table, d_tree, &comp_flag,
verbosity);
if (!d_tree) {
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
return(NULL);
} else if (d_tree == tmp_tree) {
if (d_ref == 0)
SynthPutMlTreeInList(dd, d_tree, 0);
} else {
if (comp_flag)
comp_d_tree = d_tree;
d_ref = 1;
}
}
q_tree = (MlTree *)NULL;
if (st_lookup(table, (char *)q, &q_tree)) {
SynthSetSharedFlag(dd, q_tree);
if (MlTree_Regular(q_tree)->candidate) {
if (!SynthUseCandidate(table, dd, q_tree, verbosity)) {
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
return(NULL);
}
}
if (MlTree_IsComplement(q_tree)) {
q_tree = MlTree_Regular(q_tree);
comp_q_tree = q_tree;
q_tree = (MlTree *)NULL;
}
}
if (verbosity > 1)
(void) fprintf(vis_stdout,"%s[%d] quotient\n", space, level);
q_tree_exist = 0;
if (q_tree) {
q_ref = 1;
q_tree_exist = 1;
} else if (comp_q_tree) {
q_tree = comp_q_tree;
q_ref = 1;
if (verbosity > 1) {
sprintf(comp_mess, "%s\t(C) : ", space);
SynthPrintZddTreeMessage(dd, q, comp_mess);
}
} else {
q_tree = (* factoring_func)(dd, table, q, level + 1,&q_ref,
NULL, 0, NULL, verbosity);
if (!q_tree) {
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
return(NULL);
}
if (MlTree_IsComplement(q_tree)) {
q_tree = MlTree_Regular(q_tree);
comp_q_tree = q_tree;
} else
bdd_ref(q_tree->node);
}
tmp_tree = q_tree;
q_tree = SynthCheckAndMakeComplement(dd, table, q_tree, &comp_flag,
verbosity);
if (!q_tree) {
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_tree->node);
return(NULL);
} else if (q_tree != tmp_tree) {
if (comp_flag)
comp_q_tree = q_tree;
q_ref = 1;
}
r_tree = SynthFindOrCreateMlTree(table, dd, zero, 1, 0, &r_ref, verbosity);
if (!r_tree) {
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_tree->node);
return(NULL);
}
if (MlTree_IsComplement(r_tree)) {
r_tree = MlTree_Regular(r_tree);
comp_r_tree = r_tree;
}
tmp_tree = r_tree;
r_tree = SynthCheckAndMakeComplement(dd, table, r_tree, &comp_flag,
verbosity);
if (!r_tree) {
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_tree->node);
return(NULL);
} else if (r_tree != tmp_tree) {
if (comp_flag)
comp_r_tree = r_tree;
r_ref = 1;
}
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, d);
if ((!q_tree_exist) && (!comp_q_tree))
bdd_recursive_deref_zdd(dd, q_tree->node);
tree = SynthFindOrCreateMlTree(table, dd, f, 0, 0, ref, verbosity);
if (!tree)
return(NULL);
if (*ref == 1)
(void) fprintf(vis_stdout, "** synth warning: May be duplicate.\n");
tree->q = q_tree;
tree->d = d_tree;
tree->r = r_tree;
if (comp_q_tree)
tree->q_comp = 1;
if (comp_d_tree)
tree->d_comp = 1;
if (comp_r_tree)
tree->r_comp = 1;
tree->q_ref = q_ref;
tree->d_ref = d_ref;
tree->r_ref = r_ref;
if (verbosity > 1)
SynthPrintMlTreeMessage(dd, tree, message);
SynthPutMlTreeInList(dd, tree, 0);
if (VerifyTreeMode) {
SynthVerifyTree(dd, tree, 0);
SynthVerifyMlTable(dd, table);
}
return(tree);
} else if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
bdd_recursive_deref_zdd(dd, d);
return(NULL);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| MlTree* SynthPostFactorTree | ( | bdd_manager * | dd, |
| st_table * | table, | ||
| bdd_node * | f, | ||
| bdd_node * | q, | ||
| bdd_node * | d, | ||
| MlTree * | bring, | ||
| MlTree * | comp_d_tree, | ||
| int | comp_d_flag, | ||
| char * | message, | ||
| int * | ref, | ||
| int | verbosity | ||
| ) |
Function********************************************************************
Synopsis [Try to factorize between leaf trees.]
Description [Try to factorize between leaf trees.]
SideEffects []
SeeAlso [SynthSimpleFactorTree SynthGenericFactorTree]
Definition at line 664 of file synthSimple.c.
{
bdd_node *one = bdd_read_one(dd);
bdd_node *r;
MlTree *tree, *r_tree, *tmp_tree;
int q_ref, r_ref;
MlTree *comp_r_tree = (MlTree *)NULL;
int comp_flag;
q_ref = r_ref = 0;
r = bdd_zdd_diff(dd, f, d);
if (!r)
return(NULL);
bdd_ref(r);
r_tree = (MlTree *)NULL;
if (st_lookup(table, (char *)r, &r_tree)) {
SynthSetSharedFlag(dd, r_tree);
if (MlTree_Regular(r_tree)->candidate) {
if (!SynthUseCandidate(table, dd, r_tree, verbosity)) {
bdd_recursive_deref_zdd(dd, r);
return(NULL);
}
}
if (MlTree_IsComplement(r_tree)) {
r_tree = MlTree_Regular(r_tree);
comp_r_tree = r_tree;
}
r_ref = 1;
} else {
r_tree = SynthFindOrCreateMlTree(table, dd, r, 1, 0, &r_ref, verbosity);
if (!r_tree) {
bdd_recursive_deref_zdd(dd, r);
return(NULL);
}
if (MlTree_IsComplement(r_tree)) {
comp_r_tree = MlTree_Regular(r_tree);
r_tree = comp_r_tree;
}
tmp_tree = r_tree;
r_tree = SynthCheckAndMakeComplement(dd, table, r_tree, &comp_flag,
verbosity);
if (!r_tree) {
bdd_recursive_deref_zdd(dd, r);
return(NULL);
} else if (r_tree == tmp_tree) {
if (r_ref == 0)
SynthPutMlTreeInList(dd, r_tree, 0);
} else {
if (comp_flag)
comp_r_tree = r_tree;
r_ref = 1;
}
}
bdd_recursive_deref_zdd(dd, r);
if (bring)
tree = bring;
else {
tree = SynthFindOrCreateMlTree(table, dd, f, 0, 0, ref, verbosity);
if (!tree)
return(NULL);
if (*ref)
(void)fprintf(vis_stdout, "** synth warning: May be duplicate.\n");
}
tree->q = SynthFindOrCreateMlTree(table, dd, one, 1, 0, &q_ref, verbosity);
if (!tree->q)
return(NULL);
if (MlTree_IsComplement(tree->q)) {
tree->q = MlTree_Regular(tree->q);
tree->q_comp = 1;
}
tree->d = comp_d_tree;
tree->r = r_tree;
tree->d_comp = comp_d_flag;
if (comp_r_tree)
tree->r_comp = 1;
tree->q_ref = q_ref;
tree->d_ref = 1;
tree->r_ref = r_ref;
if (verbosity > 1)
SynthPrintMlTreeMessage(dd, tree, message);
if (bring)
bring->leaf = 0;
else
SynthPutMlTreeInList(dd, tree, 0);
if (VerifyTreeMode) {
SynthVerifyTree(dd, tree, 0);
SynthVerifyMlTable(dd, table);
}
return(tree);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| MlTree* SynthSimpleFactorTree | ( | bdd_manager * | dd, |
| st_table * | table, | ||
| bdd_node * | f, | ||
| int | level, | ||
| int * | ref, | ||
| MlTree * | comp_d_tree, | ||
| int | comp_d_flag, | ||
| MlTree * | bring, | ||
| int | verbosity | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Factorizes a function using a simple method.]
Description [Factorizes a function using a simple method. Here simple refers that this algorithm tries to factorize just recursively. First it finds a divisor, then finds quotient and remainder, and then recurs for each. The argument table consists of a pair of bdd_node and MlTree, f is to be factorized, level is the depth of MlTree from top, ref returns 1 if new MlTree is created for f, otherwise returns 0, comp_d_tree is usually NULL except when post factoring takes place(here post factoring is the case to factorize a leaf node by another leaf node and a leaf node is a node in which there is no divisor), comp_d_tree is a tree which is going to be used as a divisor and comp_d_flag is used to indicate which node is going to be used as a divisor between regular node and complement node, bring is usually NULL except post factoring: when we update an already existing tree by further factorization, we pass this tree to reuse it.]
SideEffects []
SeeAlso [SynthGenericFactorTree]
Definition at line 95 of file synthSimple.c.
{
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
bdd_node *d, *q, *r, *m;
MlTree *tree, *q_tree, *d_tree, *r_tree;
char message[120];
char space[100];
MlTree *comp_q_tree = (MlTree *)NULL;
MlTree *comp_r_tree = (MlTree *)NULL;
int found;
MlTree *tmp_tree;
int comp_flag;
if (verbosity > 1) {
SynthGetSpaceString(space, level * 2, 80);
sprintf(message, "%s[%d] in : ", space, level);
SynthPrintZddTreeMessage(dd, f, message);
sprintf(message, "%s[%d]out : ", space, level);
}
if (bring)
tree = (MlTree *)NULL;
else {
tree = SynthLookupMlTable(table, dd, f, 1, verbosity);
/* tree could be NULL because of reordering, or a failure to
* allocate memory or just that f was not in the cache.
* So, we would like return NULL ONLY in the case of
* reordering or failure to allocate memory.
*/
if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
return(NULL);
}
if (tree) {
if (verbosity > 1)
SynthPrintMlTreeMessage(dd, tree, message);
*ref = 1;
return(tree);
}
if (f == one || f == zero) {
tree = SynthFindOrCreateMlTree(table, dd, f, 1, 0, ref, verbosity);
if (!tree)
return(NULL);
tmp_tree = tree;
tree = SynthCheckAndMakeComplement(dd, table, tree, &comp_flag, verbosity);
if (!tree) {
if (*ref == 0)
SynthFreeMlTree(MlTree_Regular(tmp_tree), 1);
return(NULL);
} else if (tree != tmp_tree) {
*ref = 1;
if (comp_flag)
tree = MlTree_Not(tree);
}
if (verbosity > 1)
SynthPrintMlTreeMessage(dd, tree, message);
return(tree);
}
d_tree = (MlTree *)NULL;
if (comp_d_tree) {
if (comp_d_flag)
d = comp_d_tree->complement;
else
d = comp_d_tree->node;
if (!d)
return((MlTree *)NULL);
bdd_ref(d);
} else {
found = 0;
d = (* SynthGetZddDivisorFunc())(dd, f);
if (!d)
return(NULL);
bdd_ref(d);
if (TryNodeSharing) {
/* Here, we don't need to call bdd_ref. */
d = SynthFindBiggerDivisorInList(dd, table, f, d, &found,
&comp_d_flag, &comp_d_tree, verbosity);
if (!d)
return(NULL);
}
if (UseCommonDivisor && found == 0) {
tree = SynthGetFactorTreeWithCommonDivisor(dd, table,
SynthSimpleFactorTree, f, d, level, ref, verbosity);
if (tree)
return(tree);
if (bdd_read_reordered_field(dd) || noMemoryFlag == 1)
return(NULL);
}
}
if (d == f) {
tree = SynthFindOrCreateMlTree(table, dd, f, 1, 0, ref, verbosity);
if (!tree) {
bdd_recursive_deref_zdd(dd, d);
return(NULL);
}
if (verbosity > 1)
SynthPrintMlTreeMessage(dd, tree, message);
tmp_tree = tree;
tree = SynthCheckAndMakeComplement(dd, table, tree, &comp_flag, verbosity);
if (!tree) {
bdd_recursive_deref_zdd(dd, d);
return(NULL);
} else if (tree == tmp_tree) {
if (*ref == 0)
SynthPutMlTreeInList(dd, tree, 0);
} else {
*ref = 1;
if (comp_flag)
tree = MlTree_Not(tree);
}
bdd_recursive_deref_zdd(dd, d);
return(tree);
}
if (!comp_d_tree) {
if (st_lookup(table, (char *)d, &d_tree)) {
SynthSetSharedFlag(dd, d_tree);
if (MlTree_Regular(d_tree)->candidate) {
if (!SynthUseCandidate(table, dd, d_tree, verbosity)) {
bdd_recursive_deref_zdd(dd, d);
return(NULL);
}
}
if (MlTree_IsComplement(d_tree)) {
d_tree = MlTree_Regular(d_tree);
comp_d_tree = d_tree;
d_tree = (MlTree *)NULL;
}
}
} else {
if (!comp_d_flag)
d_tree = comp_d_tree;
}
q = (* SynthGetZddDivideFunc())(dd, f, d);
if (!q) {
bdd_recursive_deref_zdd(dd, d);
return(NULL);
}
bdd_ref(q);
if (comp_d_tree && q == zero) {
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
return((MlTree *)NULL);
}
if (q == one) {
bdd_recursive_deref_zdd(dd, q);
tree = SynthPostFactorTree(dd, table, f, q, d, bring,
comp_d_tree, comp_d_flag, message, ref, verbosity);
bdd_recursive_deref_zdd(dd, d);
return(tree);
}
if (comp_d_tree && d_tree == comp_d_tree)
comp_d_tree = (MlTree *)NULL;
q_tree = (MlTree *)NULL;
if (st_lookup(table, (char *)q, &q_tree)) {
SynthSetSharedFlag(dd, q_tree);
if (MlTree_Regular(q_tree)->candidate) {
if (!SynthUseCandidate(table, dd, q_tree, verbosity)) {
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
return(NULL);
}
}
if (MlTree_IsComplement(q_tree)) {
q_tree = MlTree_Regular(q_tree);
comp_q_tree = q_tree;
q_tree = (MlTree *)NULL;
}
}
m = (* SynthGetZddProductFunc())(dd, d, q);
if (!m) {
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
return(NULL);
}
bdd_ref(m);
r = bdd_zdd_diff(dd, f, m);
if (!r) {
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, m);
return(NULL);
}
bdd_ref(r);
r_tree = (MlTree *)NULL;
if (st_lookup(table, (char *)r, &r_tree)) {
SynthSetSharedFlag(dd, r_tree);
if (MlTree_Regular(r_tree)->candidate) {
if (!SynthUseCandidate(table, dd, r_tree, verbosity)) {
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, m);
bdd_recursive_deref_zdd(dd, r);
return(NULL);
}
}
if (MlTree_IsComplement(r_tree)) {
r_tree = MlTree_Regular(r_tree);
comp_r_tree = r_tree;
r_tree = (MlTree *)NULL;
}
}
tree = SynthFactorTreeRecur(dd, table, SynthSimpleFactorTree,
f, q, d, r, m, q_tree, d_tree, r_tree,
comp_q_tree, comp_d_tree, comp_r_tree,
bring, level, space, message, ref, verbosity);
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, m);
bdd_recursive_deref_zdd(dd, r);
if (VerifyTreeMode) {
SynthVerifyTree(dd, tree, 0);
SynthVerifyMlTable(dd, table);
}
return(tree);
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
| int CompMode |
| int noMemoryFlag |
Definition at line 72 of file synthFactor.c.
Definition at line 71 of file synthFactor.c.
| int Resubstitution |
Definition at line 70 of file synthFactor.c.
| int TryNodeSharing |
Definition at line 69 of file synthFactor.c.
char rcsid [] UNUSED = "$Id: synthSimple.c,v 1.36 2005/04/23 14:37:51 jinh Exp $" [static] |
CFile***********************************************************************
FileName [synthSimple.c]
PackageName [synth]
Synopsis [Simple factorization method.]
Description []
Author [In-Ho Moon, Balakrishna Kumthekar]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Definition at line 21 of file synthSimple.c.
| int UseCommonDivisor |
Definition at line 68 of file synthFactor.c.
| int UseMtree |
Definition at line 67 of file synthFactor.c.
| int VerifyTreeMode |
Definition at line 73 of file synthFactor.c.
