alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

[buddy]

Browse source 
* src/bddio.c (bdd_load): Check the return value of fscanf() to
kill a warning.
This commit is contained in:
Alexandre Duret-Lutz 2010-01-21 15:51:23 +01:00
parent e663c222e5
commit e20ba143bb
2 changed files with 31 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

5
buddy/ChangeLog
View file

@ -1,3 +1,8 @@
2010-01-21 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/bddio.c (bdd_load): Check the return value of fscanf() to
kill a warning.
2009-12-09 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2009-12-09 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Inline bdd_addref() and bdd_delref() to speedup BDD operations. Inline bdd_addref() and bdd_delref() to speedup BDD operations.

50
buddy/src/bddio.c
View file

@ -125,7 +125,7 @@ void bdd_printall(void)
void bdd_fprintall(FILE *ofile) void bdd_fprintall(FILE *ofile)
{ {
int n; int n;
for (n=0 ; n<bddnodesize ; n++) for (n=0 ; n<bddnodesize ; n++)
{ {
if (LOW(n) != -1) if (LOW(n) != -1)
@ -170,19 +170,19 @@ void bdd_fprinttable(FILE *ofile, BDD r)
{ {
BddNode *node; BddNode *node;
int n; int n;
fprintf(ofile, "ROOT: %d\n", r); fprintf(ofile, "ROOT: %d\n", r);
if (r < 2) if (r < 2)
return; return;
bdd_mark(r); bdd_mark(r);
for (n=0 ; n<bddnodesize ; n++) for (n=0 ; n<bddnodesize ; n++)
{ {
if (LEVEL(n) & MARKON) if (LEVEL(n) & MARKON)
{ {
node = &bddnodes[n]; node = &bddnodes[n];
LEVELp(node) &= MARKOFF; LEVELp(node) &= MARKOFF;
fprintf(ofile, "[%5d] ", n); fprintf(ofile, "[%5d] ", n);
@ -213,7 +213,7 @@ DESCR {* Prints all the truth assignments for {\tt r} that would yield
< $x_{2,1}:c_{2,1},\ldots,x_{2,n_2}:c_{2,n_2}$ >\\ < $x_{2,1}:c_{2,1},\ldots,x_{2,n_2}:c_{2,n_2}$ >\\
$\ldots$ \\ $\ldots$ \\
< $x_{N,1}:c_{N,1},\ldots,x_{N,n_3}:c_{N,n_3}$ > } < $x_{N,1}:c_{N,1},\ldots,x_{N,n_3}:c_{N,n_3}$ > }
\end{Ill} \end{Ill}
Where the $x$'s are variable numbers (and the position in the Where the $x$'s are variable numbers (and the position in the
current order) and the $c$'s are the current order) and the $c$'s are the
possible assignments to these. Each set of brackets designates possible assignments to these. Each set of brackets designates
@ -232,7 +232,7 @@ void bdd_printset(BDD r)
void bdd_fprintset(FILE *ofile, BDD r) void bdd_fprintset(FILE *ofile, BDD r)
{ {
int *set; int *set;
if (r < 2) if (r < 2)
{ {
fprintf(ofile, "%s", r == 0 ? "F" : "T"); fprintf(ofile, "%s", r == 0 ? "F" : "T");
@ -244,7 +244,7 @@ void bdd_fprintset(FILE *ofile, BDD r)
bdd_error(BDD_MEMORY); bdd_error(BDD_MEMORY);
return; return;
} }
memset(set, 0, sizeof(int) * bddvarnum); memset(set, 0, sizeof(int) * bddvarnum);
bdd_printset_rec(ofile, r, set); bdd_printset_rec(ofile, r, set);
free(set); free(set);
@ -255,7 +255,7 @@ static void bdd_printset_rec(FILE *ofile, int r, int *set)
{ {
int n; int n;
int first; int first;
if (r == 0) if (r == 0)
return; return;
else else
@ -263,7 +263,7 @@ static void bdd_printset_rec(FILE *ofile, int r, int *set)
{ {
fprintf(ofile, "<"); fprintf(ofile, "<");
first = 1; first = 1;
for (n=0 ; n<bddvarnum ; n++) for (n=0 ; n<bddvarnum ; n++)
{ {
if (set[n] > 0) if (set[n] > 0)
@ -285,10 +285,10 @@ static void bdd_printset_rec(FILE *ofile, int r, int *set)
{ {
set[LEVEL(r)] = 1; set[LEVEL(r)] = 1;
bdd_printset_rec(ofile, LOW(r), set); bdd_printset_rec(ofile, LOW(r), set);
set[LEVEL(r)] = 2; set[LEVEL(r)] = 2;
bdd_printset_rec(ofile, HIGH(r), set); bdd_printset_rec(ofile, HIGH(r), set);
set[LEVEL(r)] = 0; set[LEVEL(r)] = 0;
} }
} }
@ -356,7 +356,7 @@ static void bdd_fprintdot_rec(FILE* ofile, BDD r)
fprintf(ofile, "%d -> %d [style=filled];\n", r, HIGH(r)); fprintf(ofile, "%d -> %d [style=filled];\n", r, HIGH(r));
SETMARK(r); SETMARK(r);
bdd_fprintdot_rec(ofile, LOW(r)); bdd_fprintdot_rec(ofile, LOW(r));
bdd_fprintdot_rec(ofile, HIGH(r)); bdd_fprintdot_rec(ofile, HIGH(r));
} }
@ -401,7 +401,7 @@ int bdd_save(FILE *ofile, BDD r)
fprintf(ofile, "0 0 %d\n", r); fprintf(ofile, "0 0 %d\n", r);
return 0; return 0;
} }
bdd_markcount(r, &n); bdd_markcount(r, &n);
bdd_unmark(r); bdd_unmark(r);
fprintf(ofile, "%d %d\n", n, bddvarnum); fprintf(ofile, "%d %d\n", n, bddvarnum);
@ -409,7 +409,7 @@ int bdd_save(FILE *ofile, BDD r)
for (n=0 ; n<bddvarnum ; n++) for (n=0 ; n<bddvarnum ; n++)
fprintf(ofile, "%d ", bddvar2level[n]); fprintf(ofile, "%d ", bddvar2level[n]);
fprintf(ofile, "\n"); fprintf(ofile, "\n");
err = bdd_save_rec(ofile, r); err = bdd_save_rec(ofile, r);
bdd_unmark(r); bdd_unmark(r);
@ -421,14 +421,14 @@ static int bdd_save_rec(FILE *ofile, int root)
{ {
BddNode *node = &bddnodes[root]; BddNode *node = &bddnodes[root];
int err; int err;
if (root < 2) if (root < 2)
return 0; return 0;
if (LEVELp(node) & MARKON) if (LEVELp(node) & MARKON)
return 0; return 0;
LEVELp(node) |= MARKON; LEVELp(node) |= MARKON;
if ((err=bdd_save_rec(ofile, LOWp(node))) < 0) if ((err=bdd_save_rec(ofile, LOWp(node))) < 0)
return err; return err;
if ((err=bdd_save_rec(ofile, HIGHp(node))) < 0) if ((err=bdd_save_rec(ofile, HIGHp(node))) < 0)
@ -496,21 +496,23 @@ int bdd_load(FILE *ifile, BDD *root)
/* Check for constant true / false */ /* Check for constant true / false */
if (lh_nodenum==0 && vnum==0) if (lh_nodenum==0 && vnum==0)
{ {
fscanf(ifile, "%d", root); if (fscanf(ifile, "%d", root) != 1)
return bdd_error(BDD_FORMAT);
return 0; return 0;
} }
if ((loadvar2level=(int*)malloc(sizeof(int)*vnum)) == NULL) if ((loadvar2level=(int*)malloc(sizeof(int)*vnum)) == NULL)
return bdd_error(BDD_MEMORY); return bdd_error(BDD_MEMORY);
for (n=0 ; n<vnum ; n++) for (n=0 ; n<vnum ; n++)
fscanf(ifile, "%d", &loadvar2level[n]); if (fscanf(ifile, "%d", &loadvar2level[n]) != 1)
return bdd_error(BDD_FORMAT);
if (vnum > bddvarnum) if (vnum > bddvarnum)
bdd_setvarnum(vnum); bdd_setvarnum(vnum);
if ((lh_table=(LoadHash*)malloc(lh_nodenum*sizeof(LoadHash))) == NULL) if ((lh_table=(LoadHash*)malloc(lh_nodenum*sizeof(LoadHash))) == NULL)
return bdd_error(BDD_MEMORY); return bdd_error(BDD_MEMORY);
for (n=0 ; n<lh_nodenum ; n++) for (n=0 ; n<lh_nodenum ; n++)
{ {
lh_table[n].first = -1; lh_table[n].first = -1;
@ -523,16 +525,16 @@ int bdd_load(FILE *ifile, BDD *root)
for (n=0 ; n<lh_nodenum ; n++) for (n=0 ; n<lh_nodenum ; n++)
bdd_delref(lh_table[n].data); bdd_delref(lh_table[n].data);
free(lh_table); free(lh_table);
free(loadvar2level); free(loadvar2level);
*root = 0; *root = 0;
if (tmproot < 0) if (tmproot < 0)
return tmproot; return tmproot;
else else
*root = tmproot; *root = tmproot;
return 0; return 0;
} }
@ -540,7 +542,7 @@ int bdd_load(FILE *ifile, BDD *root)
static int bdd_loaddata(FILE *ifile) static int bdd_loaddata(FILE *ifile)
{ {
int key,var,low,high,root=0,n; int key,var,low,high,root=0,n;
for (n=0 ; n<lh_nodenum ; n++) for (n=0 ; n<lh_nodenum ; n++)
{ {
if (fscanf(ifile,"%d %d %d %d", &key, &var, &low, &high) != 4) if (fscanf(ifile,"%d %d %d %d", &key, &var, &low, &high) != 4)