#include "synthInt.h"
Include dependency graph for synthGen.c:
Go to the source code of this file.
Functions | |
| static MlTree * | LiteralFactoringTree (bdd_manager *dd, st_table *table, bdd_node *f, bdd_node *c, int level, int *ref, MlTree *bring, int verbosity) |
| static bdd_node * | BestLiteral (bdd_manager *dd, bdd_node *f, bdd_node *c) |
| static int | IsCubeFree (bdd_manager *dd, bdd_node *f) |
| static bdd_node * | CommonCube (bdd_manager *dd, bdd_node *f) |
| MlTree * | SynthGenericFactorTree (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 * | SynthMakeCubeFree (bdd_manager *dd, bdd_node *f) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: synthGen.c,v 1.36 2005/05/11 20:17:21 hhhan Exp $" |
| int | UseMtree |
| int | UseCommonDivisor |
| int | TryNodeSharing |
| int | Resubstitution |
| int | RemainderComplement |
| int | noMemoryFlag |
| int | VerifyTreeMode |
Function Documentation
| static bdd_node * BestLiteral | ( | bdd_manager * | dd, |
| bdd_node * | f, | ||
| bdd_node * | c | ||
| ) | [static] |
Function********************************************************************
Synopsis [Selects a literal which occurs in the largest number of cubes.]
Description [Selects a literal which occurs in the largest number of cubes.]
SideEffects []
SeeAlso []
Definition at line 1168 of file synthGen.c.
{
int i, v;
int nvars, max_count;
int *count_f, *count_c;
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
bdd_node *node;
v = -1;
max_count = 0;
nvars = bdd_num_zdd_vars(dd);
count_f = ALLOC(int, nvars);
(void)memset((void *)count_f, 0, sizeof(int) * nvars);
SynthCountLiteralOccurrence(dd, f, count_f);
count_c = ALLOC(int, nvars);
(void)memset((void *)count_c, 0, sizeof(int) * nvars);
SynthCountLiteralOccurrence(dd, c, count_c);
for (i = 0; i < nvars; i++) {
if (count_c[i]) {
if (count_f[i] > max_count) {
v = i;
max_count = count_f[i];
}
}
}
if (v == -1) {
FREE(count_f);
FREE(count_c);
return(zero);
}
node = bdd_zdd_get_node(dd, v, one, zero);
if (!node) {
FREE(count_f);
FREE(count_c);
return(NULL);
}
FREE(count_f);
FREE(count_c);
return(node);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static bdd_node * CommonCube | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) | [static] |
Function********************************************************************
Synopsis [Returns the largest common cube.]
Description [Returns the largest common cube.]
SideEffects []
SeeAlso []
Definition at line 1274 of file synthGen.c.
{
int i, v;
int nvars, max_count, max_pos = 0;
int *count;
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
bdd_node *node;
bdd_node *tmp1, *tmp2;
int ncubes;
if (f == one || f == zero) {
return(f);
}
ncubes = bdd_zdd_count(dd, f);
v = -1;
max_count = 1;
nvars = bdd_num_zdd_vars(dd);
count = ALLOC(int, nvars);
(void)memset((void *)count, 0, sizeof(int) * nvars);
SynthCountLiteralOccurrence(dd, f, count);
for (i = 0; i < nvars; i++) {
if (count[i] > max_count) {
v = i;
max_count = count[i];
max_pos = i;
}
}
if (v == -1 || max_count < ncubes) {
FREE(count);
return(zero);
}
node = bdd_zdd_get_node(dd, v, one, zero);
if (!node) {
FREE(count);
return(NULL);
}
bdd_ref(node);
for (i = max_pos + 1; i < nvars; i++) {
if (count[i] == max_count) {
tmp1 = node;
tmp2 = bdd_zdd_get_node(dd, i, one, zero);
if (!tmp2) {
FREE(count);
bdd_recursive_deref_zdd(dd, tmp1);
return(NULL);
}
bdd_ref(tmp2);
node = (* SynthGetZddProductFunc())(dd, node, tmp2);
if (!node) {
FREE(count);
bdd_recursive_deref_zdd(dd, tmp1);
bdd_recursive_deref_zdd(dd, tmp2);
return(NULL);
}
bdd_ref(node);
bdd_recursive_deref_zdd(dd, tmp1);
bdd_recursive_deref_zdd(dd, tmp2);
}
}
FREE(count);
bdd_deref(node);
return(node);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int IsCubeFree | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) | [static] |
Function********************************************************************
Synopsis [Checks if a node is cube-free.]
Description [Checks if a node is cube-free.]
SideEffects []
SeeAlso []
Definition at line 1228 of file synthGen.c.
{
int i, v;
int nvars, max_count;
int *count;
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
int ncubes;
if (f == one || f == zero)
return(1);
ncubes = bdd_zdd_count(dd, f);
v = -1;
max_count = 1;
nvars = bdd_num_zdd_vars(dd);
count = ALLOC(int, nvars);
(void)memset((void *)count, 0, sizeof(int) * nvars);
SynthCountLiteralOccurrence(dd, f, count);
for (i = 0; i < nvars; i++) {
if (count[i] > max_count) {
v = i;
max_count = count[i];
}
}
FREE(count);
if (v == -1 || max_count < ncubes)
return(1);
return(0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static MlTree * LiteralFactoringTree | ( | bdd_manager * | dd, |
| st_table * | table, | ||
| bdd_node * | f, | ||
| bdd_node * | c, | ||
| int | level, | ||
| int * | ref, | ||
| MlTree * | bring, | ||
| int | verbosity | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Factorizes a node using literal factoring.]
Description [Factorizes a node using literal factoring.]
SideEffects []
SeeAlso []
Definition at line 670 of file synthGen.c.
{
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
bdd_node *l, *q, *r;
bdd_node *m;
char message[80];
char space[80];
MlTree *tree, *q_tree, *d_tree, *r_tree;
int q_ref, d_ref, r_ref, m_ref;
char comp_mess[120];
MlTree *comp_q_tree = (MlTree *)NULL;
MlTree *comp_d_tree = (MlTree *)NULL;
MlTree *comp_r_tree = (MlTree *)NULL;
MlTree *m_tree;
int q_tree_exist, r_tree_exist;
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);
}
l = BestLiteral(dd, f, c);
if (!l)
return(NULL);
bdd_ref(l);
d_tree = (MlTree *)NULL;
if (st_lookup(table, (char *)l, &d_tree)) {
SynthSetSharedFlag(dd, d_tree);
if (MlTree_Regular(d_tree)->candidate) {
if (!SynthUseCandidate(table, dd, d_tree, verbosity)) {
bdd_recursive_deref_zdd(dd, l);
return(NULL);
}
}
if (MlTree_IsComplement(d_tree)) {
d_tree = MlTree_Regular(d_tree);
comp_d_tree = d_tree;
d_tree = (MlTree *)NULL;
}
}
q = (* SynthGetZddDivideFunc())(dd, f, l);
if (!q) {
bdd_recursive_deref_zdd(dd, l);
return(NULL);
}
bdd_ref(q);
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, l);
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, l, q);
if (!m) {
bdd_recursive_deref_zdd(dd, l);
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, l);
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, l);
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;
}
}
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 = SynthGenericFactorTree(dd, table, q, level + 1, &q_ref,
NULL, 0, NULL, verbosity);
if (!q_tree) {
bdd_recursive_deref_zdd(dd, l);
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, m);
bdd_recursive_deref_zdd(dd, r);
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, l);
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, m);
bdd_recursive_deref_zdd(dd, r);
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, tmp_tree->node);
if (q_ref == 0)
SynthFreeMlTree(MlTree_Regular(tmp_tree), 1);
return(NULL);
}
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] literal\n", space, level);
if (d_tree) {
d_ref = 1;
if (verbosity > 1) {
sprintf(comp_mess, "%s\t(R) : ", space);
SynthPrintZddTreeMessage(dd, l, comp_mess);
}
} 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, l, comp_mess);
}
} else {
d_tree = SynthFindOrCreateMlTree(table, dd, l, 1, 0, &d_ref, verbosity);
if (!d_tree) {
bdd_recursive_deref_zdd(dd, l);
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, m);
bdd_recursive_deref_zdd(dd, r);
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)) {
comp_d_tree = MlTree_Regular(d_tree);
d_tree = comp_d_tree;
}
if (verbosity > 1) {
sprintf(comp_mess, "%s\t : ", space);
SynthPrintZddTreeMessage(dd, l, comp_mess);
}
tmp_tree = d_tree;
d_tree = SynthCheckAndMakeComplement(dd, table, d_tree, &comp_flag,
verbosity);
if (!d_tree) {
bdd_recursive_deref_zdd(dd, l);
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, m);
bdd_recursive_deref_zdd(dd, r);
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_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 (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;
}
}
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) {
bdd_recursive_deref_zdd(dd, l);
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, m);
bdd_recursive_deref_zdd(dd, r);
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_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) {
bdd_recursive_deref_zdd(dd, l);
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, m);
bdd_recursive_deref_zdd(dd, r);
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_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);
}
}
}
bdd_recursive_deref_zdd(dd, m);
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 = SynthGenericFactorTree(dd, table, r, level + 1, &r_ref,
NULL, 0, NULL, verbosity);
if (!r_tree) {
bdd_recursive_deref_zdd(dd, l);
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, r);
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_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 = SynthGenericFactorTree(dd, table, r, level + 1,
&r_ref, d_tree, 1, NULL, verbosity);
if (!r_tree && (bdd_read_reordered_field(dd) || noMemoryFlag)) {
bdd_recursive_deref_zdd(dd, l);
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, r);
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_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 = SynthGenericFactorTree(dd, table, r, level + 1,
&r_ref, NULL, 0, NULL, verbosity);
if (!r_tree) {
bdd_recursive_deref_zdd(dd, l);
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, r);
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_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) {
bdd_recursive_deref_zdd(dd, l);
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, r);
if (comp_q_tree != q_tree)
bdd_recursive_deref_zdd(dd, q_tree->node);
if (comp_r_tree != r_tree)
bdd_recursive_deref_zdd(dd, r_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(r_tree), 1);
if (m_tree && m_ref == 0)
SynthFreeMlTree(MlTree_Regular(m_tree), 1);
return(NULL);
}
if (r_tree != tmp_tree) {
if (comp_flag)
comp_r_tree = r_tree;
r_ref = 1;
}
}
bdd_recursive_deref_zdd(dd, l);
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, r);
if ((!q_tree_exist) && (!comp_q_tree))
bdd_recursive_deref_zdd(dd, q_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:
| MlTree* SynthGenericFactorTree | ( | 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 generic method.]
Description [Factorizes a function using a generic method. This algorithm came from the book "Logic Synthesis and Verification Algorithms" by Gary Hachtel and Fabio Somenzi. 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 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 [SynthSimpleFactorTree]
Definition at line 98 of file synthGen.c.
{
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
bdd_node *d, *q, *r, *m, *c;
MlTree *tree, *q_tree, *d_tree, *r_tree;
int q_ref, d_ref, r_ref;
int ncubes;
bdd_node *tmp;
char message[80];
char space[80];
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,
SynthGenericFactorTree, f, d, level, ref, verbosity);
if (tree)
return(tree);
if (bdd_read_reordered_field(dd) || noMemoryFlag == 1) {
bdd_recursive_deref_zdd(dd, d);
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;
comp_d_flag = 1;
d_tree = (MlTree *)NULL;
}
else
comp_d_flag = 0;
}
} 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);
}
ncubes = bdd_zdd_count(dd, q);
if (ncubes == 1) {
if (d_tree || comp_d_tree) {
m = (* SynthGetZddProductFunc())(dd, q, d);
if (!m) {
bdd_recursive_deref_zdd(dd, d);
bdd_recursive_deref_zdd(dd, q);
return(NULL);
}
bdd_ref(m);
bdd_recursive_deref_zdd(dd, d);
r = bdd_zdd_diff(dd, f, m);
bdd_recursive_deref_zdd(dd, m);
if (!r) {
bdd_recursive_deref_zdd(dd, q);
return(NULL);
}
bdd_ref(r);
bdd_recursive_deref_zdd(dd,r);
if (r == zero) {
if (!d_tree)
d_tree = comp_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, q);
return(NULL);
}
}
if (MlTree_IsComplement(q_tree)) {
q_tree = MlTree_Regular(q_tree);
comp_q_tree = q_tree;
}
q_ref = 1;
} else {
q_tree = SynthFindOrCreateMlTree(table, dd, q, 1,
0, &q_ref, verbosity);
if (!q_tree) {
bdd_recursive_deref_zdd(dd, q);
return(NULL);
}
if (MlTree_IsComplement(q_tree)) {
comp_q_tree = MlTree_Regular(q_tree);
q_tree = comp_q_tree;
}
tmp_tree = q_tree;
q_tree = SynthCheckAndMakeComplement(dd, table, q_tree, &comp_flag,
verbosity);
if (!q_tree) {
bdd_recursive_deref_zdd(dd, q);
return(NULL);
} else if (q_tree == tmp_tree) {
if (q_ref == 0)
SynthPutMlTreeInList(dd, q_tree, 0);
} else {
if (comp_flag)
comp_q_tree = q_tree;
q_ref = 1;
}
}
bdd_recursive_deref_zdd(dd, q);
if (bring) {
tree = bring;
tree->leaf = 0;
tree->q = q_tree;
tree->d = d_tree;
tree->r = SynthFindOrCreateMlTree(table, dd, zero,
1, 0, &r_ref, verbosity);
if (!tree->r)
return(NULL);
if (MlTree_IsComplement(tree->r)) {
tree->r = MlTree_Regular(tree->r);
tree->r_comp = 1;
}
if (comp_q_tree)
tree->q_comp = 1;
if (comp_d_flag)
tree->d_comp = 1;
tree->q_ref = q_ref;
tree->d_ref = d_ref;
tree->r_ref = r_ref;
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)
return(NULL);
if (*ref)
(void) fprintf(vis_stdout,
"** synth warning: May be duplicate.\n");
tree->q = q_tree;
tree->d = d_tree;
tree->r = SynthFindOrCreateMlTree(table, dd, zero, 1,
0, &r_ref, verbosity);
if (!tree->r)
return(NULL);
if (MlTree_IsComplement(tree->r)) {
tree->r = MlTree_Regular(tree->r);
tree->r_comp = 1;
}
if (comp_q_tree)
tree->q_comp = 1;
if (comp_d_flag)
tree->d_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
bdd_recursive_deref_zdd(dd, d);
tree = LiteralFactoringTree(dd, table, f, q, level + 1, ref,
bring, verbosity);
if (!tree) {
bdd_recursive_deref_zdd(dd, q);
return(NULL);
}
tmp_tree = tree;
tree = SynthCheckAndMakeComplement(dd, table, tree, &comp_flag, verbosity);
if (!tree) {
bdd_recursive_deref_zdd(dd, q);
return(NULL);
} else if (tree != tmp_tree) {
*ref = 1;
if (comp_flag)
tree = MlTree_Not(tree);
}
bdd_recursive_deref_zdd(dd, q);
if (verbosity > 1)
SynthPrintMlTreeMessage(dd, tree, message);
return(tree);
}
bdd_recursive_deref_zdd(dd, d);
d_tree = comp_d_tree = (MlTree *)NULL;
tmp = q;
q = SynthMakeCubeFree(dd, q);
if (!q) {
bdd_recursive_deref_zdd(dd,tmp);
return(NULL);
}
bdd_ref(q);
bdd_recursive_deref_zdd(dd,tmp);
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, q);
return(NULL);
}
}
if (MlTree_IsComplement(q_tree)) {
q_tree = MlTree_Regular(q_tree);
comp_q_tree = q_tree;
q_tree = (MlTree *)NULL;
}
}
d = (* SynthGetZddDivideFunc())(dd, f, q);
if (!d) {
bdd_recursive_deref_zdd(dd, q);
return(NULL);
}
bdd_ref(d);
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_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;
}
}
if (IsCubeFree(dd, d)) {
tree = SynthFactorTreeRecur(dd, table, SynthGenericFactorTree,
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);
return(tree);
}
bdd_recursive_deref_zdd(dd, q);
bdd_recursive_deref_zdd(dd, r);
c = CommonCube(dd, d);
if (!c) {
bdd_recursive_deref_zdd(dd, d);
return(NULL);
}
bdd_ref(c);
bdd_recursive_deref_zdd(dd, d);
tree = LiteralFactoringTree(dd, table, f, c, level + 1,
ref, bring, verbosity);
if (!tree) {
bdd_recursive_deref_zdd(dd, c);
return(NULL);
}
tmp_tree = tree;
tree = SynthCheckAndMakeComplement(dd, table, tree, &comp_flag, verbosity);
if (!tree) {
bdd_recursive_deref_zdd(dd, c);
if (*ref == 0)
SynthFreeMlTree(MlTree_Regular(tree), 1);
return(NULL);
} else if (tree != tmp_tree) {
*ref = 1;
if (comp_flag)
tree = MlTree_Not(tree);
}
bdd_recursive_deref_zdd(dd, c);
if (verbosity > 1)
SynthPrintMlTreeMessage(dd, tree, message);
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* SynthMakeCubeFree | ( | bdd_manager * | dd, |
| bdd_node * | f | ||
| ) |
Function********************************************************************
Synopsis [Makes a node cube-free.]
Description [Makes a node cube-free. Eliminates the literals that appear in all the cubes.]
SideEffects []
SeeAlso []
Definition at line 571 of file synthGen.c.
{
int i, v;
int nvars, max_count, max_pos = 0;
int *count;
bdd_node *one = bdd_read_one(dd);
bdd_node *zero = bdd_read_zero(dd);
bdd_node *divisor, *node;
bdd_node *tmp1, *tmp2;
int ncubes;
if (f == one || f == zero)
return(f);
/* Compare the number of occurrences of each literal to the number of
* cubes in the cover. If no literal appears more than once, or if no
* literal appears in all cubes, f is already cube-free.
*/
ncubes = bdd_zdd_count(dd, f);
v = -1;
max_count = 1;
nvars = bdd_num_zdd_vars(dd);
count = ALLOC(int, nvars);
(void)memset((void *)count, 0, sizeof(int) * nvars);
SynthCountLiteralOccurrence(dd, f, count);
for (i = 0; i < nvars; i++) {
if (count[i] > max_count) {
v = i;
max_count = count[i];
max_pos = i;
}
}
if (v == -1 || max_count < ncubes) {
FREE(count);
return(f);
}
/* Divide the cover by the first literal appearing in all cubes. */
node = bdd_zdd_get_node(dd, v, one, zero);
if (!node) {
FREE(count);
return(NULL);
}
bdd_ref(node);
divisor = (* SynthGetZddDivideFunc())(dd, f, node);
if (!divisor) {
bdd_recursive_deref_zdd(dd, node);
FREE(count);
return(NULL);
}
bdd_ref(divisor);
bdd_recursive_deref_zdd(dd, node);
/* Divide the cover by the remaining literals appearing in all cubes. */
for (i = max_pos + 1; i < nvars; i++) {
if (count[i] == max_count) {
tmp1 = divisor;
tmp2 = bdd_zdd_get_node(dd, i, one, zero);
if (!tmp2) {
FREE(count);
bdd_recursive_deref_zdd(dd, tmp1);
return(NULL);
}
bdd_ref(tmp2);
divisor = (* SynthGetZddDivideFunc())(dd, divisor, tmp2);
if (!divisor) {
FREE(count);
bdd_recursive_deref_zdd(dd, tmp1);
bdd_recursive_deref_zdd(dd, tmp2);
return(NULL);
}
bdd_ref(divisor);
bdd_recursive_deref_zdd(dd, tmp1);
bdd_recursive_deref_zdd(dd, tmp2);
}
}
FREE(count);
bdd_deref(divisor);
return(divisor);
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
| 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: synthGen.c,v 1.36 2005/05/11 20:17:21 hhhan Exp $" [static] |
CFile***********************************************************************
FileName [synthGen.c]
PackageName [synth]
Synopsis [Generic multilevel 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 synthGen.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.
