diogo/yap-6.3
Archived
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

simplecudd interface

Browse Source
This commit is contained in:
Vitor Santos Costa 2009-03-09 00:42:12 +00:00
parent 620ac64fdd
commit a6747da26e
9 changed files with 3589 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

281
packages/ProbLog/simplecudd/Example.c Normal file
View File

@ -0,0 +1,281 @@
/******************************************************************************\
* *
* SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html) *
* SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be) *
* *
* Copyright T. Mantadelis and Katholieke Universiteit Leuven 2008 *
* *
* Author: Theofrastos Mantadelis *
* File: Example.c *
* *
********************************************************************************
* *
* The "Artistic License" *
* *
* Preamble *
* *
* The intent of this document is to state the conditions under which a *
* Package may be copied, such that the Copyright Holder maintains some *
* semblance of artistic control over the development of the package, *
* while giving the users of the package the right to use and distribute *
* the Package in a more-or-less customary fashion, plus the right to make *
* reasonable modifications. *
* *
* Definitions: *
* *
* "Package" refers to the collection of files distributed by the *
* Copyright Holder, and derivatives of that collection of files *
* created through textual modification. *
* *
* "Standard Version" refers to such a Package if it has not been *
* modified, or has been modified in accordance with the wishes *
* of the Copyright Holder as specified below. *
* *
* "Copyright Holder" is whoever is named in the copyright or *
* copyrights for the package. *
* *
* "You" is you, if you're thinking about copying or distributing *
* this Package. *
* *
* "Reasonable copying fee" is whatever you can justify on the *
* basis of media cost, duplication charges, time of people involved, *
* and so on. (You will not be required to justify it to the *
* Copyright Holder, but only to the computing community at large *
* as a market that must bear the fee.) *
* *
* "Freely Available" means that no fee is charged for the item *
* itself, though there may be fees involved in handling the item. *
* It also means that recipients of the item may redistribute it *
* under the same conditions they received it. *
* *
* 1. You may make and give away verbatim copies of the source form of the *
* Standard Version of this Package without restriction, provided that you *
* duplicate all of the original copyright notices and associated disclaimers. *
* *
* 2. You may apply bug fixes, portability fixes and other modifications *
* derived from the Public Domain or from the Copyright Holder. A Package *
* modified in such a way shall still be considered the Standard Version. *
* *
* 3. You may otherwise modify your copy of this Package in any way, provided *
* that you insert a prominent notice in each changed file stating how and *
* when you changed that file, and provided that you do at least ONE of the *
* following: *
* *
* a) place your modifications in the Public Domain or otherwise make them *
* Freely Available, such as by posting said modifications to Usenet or *
* an equivalent medium, or placing the modifications on a major archive *
* site such as uunet.uu.net, or by allowing the Copyright Holder to include *
* your modifications in the Standard Version of the Package. *
* *
* b) use the modified Package only within your corporation or organization. *
* *
* c) rename any non-standard executables so the names do not conflict *
* with standard executables, which must also be provided, and provide *
* a separate manual page for each non-standard executable that clearly *
* documents how it differs from the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 4. You may distribute the programs of this Package in object code or *
* executable form, provided that you do at least ONE of the following: *
* *
* a) distribute a Standard Version of the executables and library files, *
* together with instructions (in the manual page or equivalent) on where *
* to get the Standard Version. *
* *
* b) accompany the distribution with the machine-readable source of *
* the Package with your modifications. *
* *
* c) give non-standard executables non-standard names, and clearly *
* document the differences in manual pages (or equivalent), together *
* with instructions on where to get the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 5. You may charge a reasonable copying fee for any distribution of this *
* Package. You may charge any fee you choose for support of this *
* Package. You may not charge a fee for this Package itself. However, *
* you may distribute this Package in aggregate with other (possibly *
* commercial) programs as part of a larger (possibly commercial) software *
* distribution provided that you do not advertise this Package as a *
* product of your own. You may embed this Package's interpreter within *
* an executable of yours (by linking); this shall be construed as a mere *
* form of aggregation, provided that the complete Standard Version of the *
* interpreter is so embedded. *
* *
* 6. The scripts and library files supplied as input to or produced as *
* output from the programs of this Package do not automatically fall *
* under the copyright of this Package, but belong to whoever generated *
* them, and may be sold commercially, and may be aggregated with this *
* Package. If such scripts or library files are aggregated with this *
* Package via the so-called "undump" or "unexec" methods of producing a *
* binary executable image, then distribution of such an image shall *
* neither be construed as a distribution of this Package nor shall it *
* fall under the restrictions of Paragraphs 3 and 4, provided that you do *
* not represent such an executable image as a Standard Version of this *
* Package. *
* *
* 7. C subroutines (or comparably compiled subroutines in other *
* languages) supplied by you and linked into this Package in order to *
* emulate subroutines and variables of the language defined by this *
* Package shall not be considered part of this Package, but are the *
* equivalent of input as in Paragraph 6, provided these subroutines do *
* not change the language in any way that would cause it to fail the *
* regression tests for the language. *
* *
* 8. Aggregation of this Package with a commercial distribution is always *
* permitted provided that the use of this Package is embedded; that is, *
* when no overt attempt is made to make this Package's interfaces visible *
* to the end user of the commercial distribution. Such use shall not be *
* construed as a distribution of this Package. *
* *
* 9. The name of the Copyright Holder may not be used to endorse or promote *
* products derived from this software without specific prior written *
* permission. *
* *
* 10. THIS PACKAGE IS PROVIDED "AS IS" AND WITHOUT ANY EXPRESS OR *
* IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED *
* WARRANTIES OF MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE. *
* *
* The End *
* *
\******************************************************************************/
#include "simplecudd.h"
typedef struct _extmanager {
DdManager *manager;
DdNode *t, *f;
hisqueue *his;
namedvars varmap;
} extmanager;
void DFS(extmanager MyManager, DdNode *Current);
int compexpand(extmanager MyManager, DdNode *Current, extmanager MyManager2, DdNode *Current2);
int bufstrcat(char *targetstr, int targetmem, const char *srcstr);
void getalltruepaths(extmanager MyManager, DdNode *Current, const char *startpath, const char *prevvar);
int main(int argc, char **arg) {
extmanager MyManager;
DdNode *bdd;
bddfileheader fileheader;
int code;
char yn;
code = -1;
if (argc != 2) {
fprintf(stderr, "\nUsage: %s [filename]\nGenerates and traverses a BDD from file\n", arg[0]);
fprintf(stderr, "\nUsage: %s -online\nGenerates and traverses a BDD online mode\n", arg[0]);
return code;
}
RAPIDLOADON;
if (strcmp("-online", arg[1]) == 0) {
MyManager.manager = simpleBDDinit(0);
MyManager.t = HIGH(MyManager.manager);
MyManager.f = LOW(MyManager.manager);
MyManager.varmap = InitNamedVars(1, 0);
bdd = OnlineGenerateBDD(MyManager.manager, &MyManager.varmap);
} else {
fileheader = ReadFileHeader(arg[1]);
switch(fileheader.filetype) {
case BDDFILE_SCRIPT:
MyManager.manager = simpleBDDinit(fileheader.varcnt);
MyManager.t = HIGH(MyManager.manager);
MyManager.f = LOW(MyManager.manager);
MyManager.varmap = InitNamedVars(fileheader.varcnt, fileheader.varstart);
bdd = FileGenerateBDD(MyManager.manager, MyManager.varmap, fileheader);
break;
case BDDFILE_NODEDUMP:
MyManager.manager = simpleBDDinit(fileheader.varcnt);
MyManager.t = HIGH(MyManager.manager);
MyManager.f = LOW(MyManager.manager);
MyManager.varmap = InitNamedVars(fileheader.varcnt, fileheader.varstart);
bdd = LoadNodeDump(MyManager.manager, MyManager.varmap, fileheader.inputfile);
break;
default:
fprintf(stderr, "Error: not a valid file format to load.\n");
return code;
break;
}
}
if (bdd != NULL) {
printf("Do you want to load parameter values from testdata.txt [y]? "); yn = getchar(); getchar();
if (yn == 'y') LoadVariableData(MyManager.varmap, "testdata.txt");
code = 0;
MyManager.his = InitHistory(GetVarCount(MyManager.manager));
if (strcmp("-online", arg[1]) != 0) {
DFS(MyManager, bdd);
printf("Do you need an export [y]? "); yn = getchar(); getchar();
if (yn == 'y') simpleNamedBDDtoDot(MyManager.manager, MyManager.varmap, bdd, "SimpleCUDDExport.dot");
printf("Do you want a save [y]? "); yn = getchar(); getchar();
if (yn == 'y') SaveNodeDump(MyManager.manager, MyManager.varmap, bdd, "SimpleCUDDSave.sav");
printf("Do you want to see all true paths [y]? "); yn = getchar(); getchar();
if (yn == 'y') {
ReInitHistory(MyManager.his, GetVarCount(MyManager.manager));
getalltruepaths(MyManager, bdd, "", "");
}
} else {
onlinetraverse(MyManager.manager, MyManager.varmap, MyManager.his, bdd);
}
}
if (MyManager.manager != NULL) KillBDD(MyManager.manager);
return code;
}
void DFS(extmanager MyManager, DdNode *Current) {
DdNode *h, *l;
hisnode *Found;
char *curnode;
curnode = GetNodeVarNameDisp(MyManager.manager, MyManager.varmap, Current);
if (GetIndex(Current) < MyManager.varmap.varcnt) {
printf("%s(%f,%i,%s)\n", curnode, MyManager.varmap.dvalue[GetIndex(Current)], MyManager.varmap.ivalue[GetIndex(Current)], MyManager.varmap.dynvalue[GetIndex(Current)]);
} else {
printf("%s\n", curnode);
}
if ((Current != MyManager.t) && (Current != MyManager.f) &&
((Found = GetNode(MyManager.his, MyManager.varmap.varstart, Current)) == NULL)) {
l = LowNodeOf(MyManager.manager, Current);
h = HighNodeOf(MyManager.manager, Current);
printf("l(%s)->", curnode);
DFS(MyManager, l);
printf("h(%s)->", curnode);
DFS(MyManager, h);
AddNode(MyManager.his, MyManager.varmap.varstart, Current, 0.0, 0, NULL);
}
}
void getalltruepaths(extmanager MyManager, DdNode *Current, const char *startpath, const char *prevvar) {
DdNode *h, *l;
char *curnode, *curpath;
int pathmaxsize = 1024;
curpath = (char *) malloc(sizeof(char) * pathmaxsize);
curpath[0] = '\0';
pathmaxsize = bufstrcat(curpath, pathmaxsize, startpath);
pathmaxsize = bufstrcat(curpath, pathmaxsize, prevvar);
pathmaxsize = bufstrcat(curpath, pathmaxsize, "*");
curnode = GetNodeVarNameDisp(MyManager.manager, MyManager.varmap, Current);
if (Current == MyManager.t) {
printf("%s\n", curpath);
} else if (Current != MyManager.f) {
h = HighNodeOf(MyManager.manager, Current);
if (h != MyManager.f) {
getalltruepaths(MyManager, h, curpath, curnode);
}
l = LowNodeOf(MyManager.manager, Current);
if (l != MyManager.f) {
pathmaxsize = bufstrcat(curpath, pathmaxsize, "~");
getalltruepaths(MyManager, l, curpath, curnode);
}
}
free(curpath);
}
int bufstrcat(char *targetstr, int targetmem, const char *srcstr) {
int strinc = strlen(srcstr), strsize = strlen(targetstr);
while ((strsize + strinc) > (targetmem - 1)) {
targetmem *= 2;
targetstr = (char *) realloc(targetstr, sizeof(char) * targetmem);
}
strcat(targetstr, srcstr);
return targetmem;
}

131
packages/ProbLog/simplecudd/LICENCE Normal file
View File

@ -0,0 +1,131 @@
The "Artistic License"
Preamble
The intent of this document is to state the conditions under which a
Package may be copied, such that the Copyright Holder maintains some
semblance of artistic control over the development of the package,
while giving the users of the package the right to use and distribute
the Package in a more-or-less customary fashion, plus the right to make
reasonable modifications.
Definitions:
"Package" refers to the collection of files distributed by the
Copyright Holder, and derivatives of that collection of files
created through textual modification.
"Standard Version" refers to such a Package if it has not been
modified, or has been modified in accordance with the wishes
of the Copyright Holder as specified below.
"Copyright Holder" is whoever is named in the copyright or
copyrights for the package.
"You" is you, if you're thinking about copying or distributing
this Package.
"Reasonable copying fee" is whatever you can justify on the
basis of media cost, duplication charges, time of people involved,
and so on. (You will not be required to justify it to the
Copyright Holder, but only to the computing community at large
as a market that must bear the fee.)
"Freely Available" means that no fee is charged for the item
itself, though there may be fees involved in handling the item.
It also means that recipients of the item may redistribute it
under the same conditions they received it.
1. You may make and give away verbatim copies of the source form of the
Standard Version of this Package without restriction, provided that you
duplicate all of the original copyright notices and associated disclaimers.
2. You may apply bug fixes, portability fixes and other modifications
derived from the Public Domain or from the Copyright Holder. A Package
modified in such a way shall still be considered the Standard Version.
3. You may otherwise modify your copy of this Package in any way, provided
that you insert a prominent notice in each changed file stating how and
when you changed that file, and provided that you do at least ONE of the
following:
a) place your modifications in the Public Domain or otherwise make them
Freely Available, such as by posting said modifications to Usenet or
an equivalent medium, or placing the modifications on a major archive
site such as uunet.uu.net, or by allowing the Copyright Holder to include
your modifications in the Standard Version of the Package.
b) use the modified Package only within your corporation or organization.
c) rename any non-standard executables so the names do not conflict
with standard executables, which must also be provided, and provide
a separate manual page for each non-standard executable that clearly
documents how it differs from the Standard Version.
d) make other distribution arrangements with the Copyright Holder.
4. You may distribute the programs of this Package in object code or
executable form, provided that you do at least ONE of the following:
a) distribute a Standard Version of the executables and library files,
together with instructions (in the manual page or equivalent) on where
to get the Standard Version.
b) accompany the distribution with the machine-readable source of
the Package with your modifications.
c) give non-standard executables non-standard names, and clearly
document the differences in manual pages (or equivalent), together
with instructions on where to get the Standard Version.
d) make other distribution arrangements with the Copyright Holder.
5. You may charge a reasonable copying fee for any distribution of this
Package. You may charge any fee you choose for support of this
Package. You may not charge a fee for this Package itself. However,
you may distribute this Package in aggregate with other (possibly
commercial) programs as part of a larger (possibly commercial) software
distribution provided that you do not advertise this Package as a
product of your own. You may embed this Package's interpreter within
an executable of yours (by linking); this shall be construed as a mere
form of aggregation, provided that the complete Standard Version of the
interpreter is so embedded.
6. The scripts and library files supplied as input to or produced as
output from the programs of this Package do not automatically fall
under the copyright of this Package, but belong to whoever generated
them, and may be sold commercially, and may be aggregated with this
Package. If such scripts or library files are aggregated with this
Package via the so-called "undump" or "unexec" methods of producing a
binary executable image, then distribution of such an image shall
neither be construed as a distribution of this Package nor shall it
fall under the restrictions of Paragraphs 3 and 4, provided that you do
not represent such an executable image as a Standard Version of this
Package.
7. C subroutines (or comparably compiled subroutines in other
languages) supplied by you and linked into this Package in order to
emulate subroutines and variables of the language defined by this
Package shall not be considered part of this Package, but are the
equivalent of input as in Paragraph 6, provided these subroutines do
not change the language in any way that would cause it to fail the
regression tests for the language.
8. Aggregation of this Package with a commercial distribution is always
permitted provided that the use of this Package is embedded; that is,
when no overt attempt is made to make this Package's interfaces visible
to the end user of the commercial distribution. Such use shall not be
construed as a distribution of this Package.
9. The name of the Copyright Holder may not be used to endorse or promote
products derived from this software without specific prior written permission.
10. THIS PACKAGE IS PROVIDED "AS IS" AND WITHOUT ANY EXPRESS OR
IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED
WARRANTIES OF MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE.
The End

61
packages/ProbLog/simplecudd/Makefile.in Normal file
View File

@ -0,0 +1,61 @@
#
# default base directory for YAP installation
# (EROOT for architecture-dependent files)
#
prefix = @prefix@
ROOTDIR = $(prefix)
EROOTDIR = @exec_prefix@
#
# where the binary should be
#
BINDIR = $(EROOTDIR)/bin
#
# where YAP should look for libraries
#
LIBDIR=$(EROOTDIR)/lib/Yap
#
#
CC=@CC@
#
#
# You shouldn't need to change what follows.
#
INSTALL=@INSTALL@
INSTALL_DATA=@INSTALL_DATA@
INSTALL_PROGRAM=@INSTALL_PROGRAM@
SHELL=/bin/sh
RANLIB=@RANLIB@
srcdir=@srcdir@
SHLIB_CFLAGS=@SHLIB_CFLAGS@
SHLIB_SUFFIX=@SHLIB_SUFFIX@
#4.1VPATH=@srcdir@:@srcdir@/OPTYap
CWD=$(PWD)
#
CUDD = cudd-2.4.1
DYNAMIC =
CFLAGS = @CFLAGS@
INCLUDE = @CUDD_CPPFLAGS@
LINKFLAGS = -lm
LINKLIBS = @CUDD_LDFLAGS@
default: Example ProbLogBDD
Example: Example.o simplecudd.o general.o
@echo Making Example...
@echo Copyright T. Mantadelis and Katholieke Universiteit Leuven 2008
$(CC) Example.o simplecudd.o general.o $(LINKLIBS) $(LINKFLAGS) -o Example
ProbLogBDD: ProblogBDD.o simplecudd.o general.o
@echo Making ProblogBDD...
@echo Copyright T. Mantadelis, A. Kimmig, B. Gutmann and Katholieke Universiteit Leuven 2008
$(CC) ProblogBDD.o simplecudd.o general.o $(LINKLIBS) $(LINKFLAGS) -o ProblogBDD
%.o : $(srcdir)/%.c
$(CC) $(CFLAGS) $(INCLUDE) $(DYNAMIC) -c $<
clean:
rm -f *.o ProblogBDD Example
install: default
$(INSTALL_PROGRAM) ProblogBDD $(DESTDIR)$(LIBDIR)

675
packages/ProbLog/simplecudd/ProblogBDD.c Normal file
View File

@ -0,0 +1,675 @@
/******************************************************************************\
* *
* SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html) *
* SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be) *
* *
* Copyright T. Mantadelis, A. Kimmig, B. Gutmann *
* and Katholieke Universiteit Leuven 2008 *
* *
* Author: Theofrastos Mantadelis, Angelika Kimmig, Bernd Gutmann *
* File: ProblogBDD.c *
* *
********************************************************************************
* *
* The "Artistic License" *
* *
* Preamble *
* *
* The intent of this document is to state the conditions under which a *
* Package may be copied, such that the Copyright Holder maintains some *
* semblance of artistic control over the development of the package, *
* while giving the users of the package the right to use and distribute *
* the Package in a more-or-less customary fashion, plus the right to make *
* reasonable modifications. *
* *
* Definitions: *
* *
* "Package" refers to the collection of files distributed by the *
* Copyright Holder, and derivatives of that collection of files *
* created through textual modification. *
* *
* "Standard Version" refers to such a Package if it has not been *
* modified, or has been modified in accordance with the wishes *
* of the Copyright Holder as specified below. *
* *
* "Copyright Holder" is whoever is named in the copyright or *
* copyrights for the package. *
* *
* "You" is you, if you're thinking about copying or distributing *
* this Package. *
* *
* "Reasonable copying fee" is whatever you can justify on the *
* basis of media cost, duplication charges, time of people involved, *
* and so on. (You will not be required to justify it to the *
* Copyright Holder, but only to the computing community at large *
* as a market that must bear the fee.) *
* *
* "Freely Available" means that no fee is charged for the item *
* itself, though there may be fees involved in handling the item. *
* It also means that recipients of the item may redistribute it *
* under the same conditions they received it. *
* *
* 1. You may make and give away verbatim copies of the source form of the *
* Standard Version of this Package without restriction, provided that you *
* duplicate all of the original copyright notices and associated disclaimers. *
* *
* 2. You may apply bug fixes, portability fixes and other modifications *
* derived from the Public Domain or from the Copyright Holder. A Package *
* modified in such a way shall still be considered the Standard Version. *
* *
* 3. You may otherwise modify your copy of this Package in any way, provided *
* that you insert a prominent notice in each changed file stating how and *
* when you changed that file, and provided that you do at least ONE of the *
* following: *
* *
* a) place your modifications in the Public Domain or otherwise make them *
* Freely Available, such as by posting said modifications to Usenet or *
* an equivalent medium, or placing the modifications on a major archive *
* site such as uunet.uu.net, or by allowing the Copyright Holder to include *
* your modifications in the Standard Version of the Package. *
* *
* b) use the modified Package only within your corporation or organization. *
* *
* c) rename any non-standard executables so the names do not conflict *
* with standard executables, which must also be provided, and provide *
* a separate manual page for each non-standard executable that clearly *
* documents how it differs from the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 4. You may distribute the programs of this Package in object code or *
* executable form, provided that you do at least ONE of the following: *
* *
* a) distribute a Standard Version of the executables and library files, *
* together with instructions (in the manual page or equivalent) on where *
* to get the Standard Version. *
* *
* b) accompany the distribution with the machine-readable source of *
* the Package with your modifications. *
* *
* c) give non-standard executables non-standard names, and clearly *
* document the differences in manual pages (or equivalent), together *
* with instructions on where to get the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 5. You may charge a reasonable copying fee for any distribution of this *
* Package. You may charge any fee you choose for support of this *
* Package. You may not charge a fee for this Package itself. However, *
* you may distribute this Package in aggregate with other (possibly *
* commercial) programs as part of a larger (possibly commercial) software *
* distribution provided that you do not advertise this Package as a *
* product of your own. You may embed this Package's interpreter within *
* an executable of yours (by linking); this shall be construed as a mere *
* form of aggregation, provided that the complete Standard Version of the *
* interpreter is so embedded. *
* *
* 6. The scripts and library files supplied as input to or produced as *
* output from the programs of this Package do not automatically fall *
* under the copyright of this Package, but belong to whoever generated *
* them, and may be sold commercially, and may be aggregated with this *
* Package. If such scripts or library files are aggregated with this *
* Package via the so-called "undump" or "unexec" methods of producing a *
* binary executable image, then distribution of such an image shall *
* neither be construed as a distribution of this Package nor shall it *
* fall under the restrictions of Paragraphs 3 and 4, provided that you do *
* not represent such an executable image as a Standard Version of this *
* Package. *
* *
* 7. C subroutines (or comparably compiled subroutines in other *
* languages) supplied by you and linked into this Package in order to *
* emulate subroutines and variables of the language defined by this *
* Package shall not be considered part of this Package, but are the *
* equivalent of input as in Paragraph 6, provided these subroutines do *
* not change the language in any way that would cause it to fail the *
* regression tests for the language. *
* *
* 8. Aggregation of this Package with a commercial distribution is always *
* permitted provided that the use of this Package is embedded; that is, *
* when no overt attempt is made to make this Package's interfaces visible *
* to the end user of the commercial distribution. Such use shall not be *
* construed as a distribution of this Package. *
* *
* 9. The name of the Copyright Holder may not be used to endorse or promote *
* products derived from this software without specific prior written *
* permission. *
* *
* 10. THIS PACKAGE IS PROVIDED "AS IS" AND WITHOUT ANY EXPRESS OR *
* IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED *
* WARRANTIES OF MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE. *
* *
* The End *
* *
\******************************************************************************/
#include "simplecudd.h"
#include <signal.h>
typedef struct _parameters {
int loadfile;
int savedfile;
int exportfile;
int inputfile;
int debug;
int errorcnt;
int *error;
int method;
int queryid;
int timeout;
double sigmoid_slope;
int online;
int maxbufsize;
char *ppid;
} parameters;
typedef struct _gradientpair {
double probability;
double gradient;
} gradientpair;
typedef struct _extmanager {
DdManager *manager;
DdNode *t, *f;
hisqueue *his;
namedvars varmap;
} extmanager;
int argtype(const char *arg);
void printhelp(int argc, char **arg);
parameters loadparam(int argc, char **arg);
parameters params;
void handler(int num);
void pidhandler(int num);
void termhandler(int num);
double sigmoid(double x, double slope);
void myexpand(extmanager MyManager, DdNode *Current);
double CalcProbability(extmanager MyManager, DdNode *Current);
double CalcProbabilitySigmoid(extmanager MyManager, DdNode *Current);
gradientpair CalcGradient(extmanager MyManager, DdNode *Current, int TargetVar, char *TargetPattern);
int patterncalculated(char *pattern, extmanager MyManager, int loc);
char * extractpattern(char *thestr);
int main(int argc, char **arg) {
extmanager MyManager;
DdNode *bdd;
bddfileheader fileheader;
int i, ivarcnt, code;
gradientpair tvalue;
double probability = -1.0;
char *varpattern;
varpattern = NULL;
code = -1;
params = loadparam(argc, arg);
if (params.errorcnt > 0) {
printhelp(argc, arg);
for (i = 0; i < params.errorcnt; i++) {
fprintf(stderr, "Error: not known or error at parameter %s.\n", arg[params.error[i]]);
}
return -1;
}
if (params.online == 0 && params.loadfile == -1) {
printhelp(argc, arg);
fprintf(stderr, "Error: you must specify a loading file.\n");
return -1;
}
if (params.method != 0 && arg[params.method][0] != 'g' && arg[params.method][0] != 'p' && arg[params.method][0] != 'o' && arg[params.method][0] != 'l') {
printhelp(argc, arg);
fprintf(stderr, "Error: you must choose a calculation method beetween [p]robability, [g]radient, [l]ine search, [o]nline.\n");
return -1;
}
if (params.debug) DEBUGON;
RAPIDLOADON;
SETMAXBUFSIZE(params.maxbufsize);
signal(SIGINT, termhandler);
if (params.ppid != NULL) {
signal(SIGALRM, pidhandler);
alarm(5);
} else {
signal(SIGALRM, handler);
alarm(params.timeout);
}
if (params.online) {
MyManager.manager = simpleBDDinit(0);
MyManager.t = HIGH(MyManager.manager);
MyManager.f = LOW(MyManager.manager);
MyManager.varmap = InitNamedVars(1, 0);
bdd = OnlineGenerateBDD(MyManager.manager, &MyManager.varmap);
ivarcnt = GetVarCount(MyManager.manager);
} else {
fileheader = ReadFileHeader(arg[params.loadfile]);
switch(fileheader.filetype) {
case BDDFILE_SCRIPT:
if (params.inputfile == -1) {
printhelp(argc, arg);
fprintf(stderr, "Error: an input file is necessary for this type of loading file.\n");
return -1;
}
MyManager.manager = simpleBDDinit(fileheader.varcnt);
MyManager.t = HIGH(MyManager.manager);
MyManager.f = LOW(MyManager.manager);
MyManager.varmap = InitNamedVars(fileheader.varcnt, fileheader.varstart);
bdd = FileGenerateBDD(MyManager.manager, MyManager.varmap, fileheader);
ivarcnt = fileheader.varcnt;
break;
case BDDFILE_NODEDUMP:
if (params.inputfile == -1) {
printhelp(argc, arg);
fprintf(stderr, "Error: an input file is necessary for this type of loading file.\n");
return -1;
}
MyManager.manager = simpleBDDinit(fileheader.varcnt);
MyManager.t = HIGH(MyManager.manager);
MyManager.f = LOW(MyManager.manager);
MyManager.varmap = InitNamedVars(fileheader.varcnt, fileheader.varstart);
bdd = LoadNodeDump(MyManager.manager, MyManager.varmap, fileheader.inputfile);
ivarcnt = fileheader.varcnt;
break;
default:
fprintf(stderr, "Error: not a valid file format to load.\n");
return -1;
break;
}
}
alarm(0);
// problem specifics
if (bdd != NULL) {
ivarcnt = RepairVarcnt(&MyManager.varmap);
code = 0;
if (params.inputfile != -1) {
if (LoadVariableData(MyManager.varmap, arg[params.inputfile]) == -1) return -1;
if (!all_loaded(MyManager.varmap, 1)) return -1;
}
MyManager.his = InitHistory(ivarcnt);
if (params.method != 0) {
switch(arg[params.method][0]) {
case 'g':
for (i = 0; i < MyManager.varmap.varcnt; i++) {
if (MyManager.varmap.vars[i] != NULL) {
varpattern = extractpattern(MyManager.varmap.vars[i]);
if ((varpattern == NULL) || (!patterncalculated(varpattern, MyManager, i))) {
tvalue = CalcGradient(MyManager, bdd, i + MyManager.varmap.varstart, varpattern);
probability = tvalue.probability;
double factor = sigmoid(MyManager.varmap.dvalue[i], params.sigmoid_slope) * (1 - sigmoid(MyManager.varmap.dvalue[i], params.sigmoid_slope)) * params.sigmoid_slope;
if (varpattern == NULL) {
printf("query_gradient(%s,%s,%1.12f).\n", arg[params.queryid], MyManager.varmap.vars[i], tvalue.gradient * factor);
} else {
varpattern[strlen(varpattern) - 2] = '\0';
printf("query_gradient(%s,%s,%1.12f).\n", arg[params.queryid], varpattern, tvalue.gradient * factor);
}
ReInitHistory(MyManager.his, MyManager.varmap.varcnt);
}
if (varpattern != NULL) free(varpattern);
} else {
fprintf(stderr, "Error: no variable name given for parameter.\n");
}
}
if (probability < 0.0) {
// no nodes, so we have to calculate probability ourself
tvalue = CalcGradient(MyManager, bdd, 0 + MyManager.varmap.varstart, NULL);
probability = tvalue.probability;
}
printf("query_probability(%s,%1.12f).\n", arg[params.queryid], probability);
break;
case 'l':
tvalue = CalcGradient(MyManager, bdd, 0 + MyManager.varmap.varstart, NULL);
probability = tvalue.probability;
printf("query_probability(%s,%1.12f).\n", arg[params.queryid], probability);
break;
case 'p':
printf("probability(%1.12f).\n", CalcProbability(MyManager, bdd));
break;
case 'o':
onlinetraverse(MyManager.manager, MyManager.varmap, MyManager.his, bdd);
break;
default:
myexpand(MyManager, bdd);
break;
}
} else {
myexpand(MyManager, bdd);
}
if (params.savedfile > -1) SaveNodeDump(MyManager.manager, MyManager.varmap, bdd, arg[params.savedfile]);
if (params.exportfile > -1) simpleNamedBDDtoDot(MyManager.manager, MyManager.varmap, bdd, arg[params.exportfile]);
ReInitHistory(MyManager.his, MyManager.varmap.varcnt);
free(MyManager.his);
}
if (MyManager.manager != NULL) {
KillBDD(MyManager.manager);
free(MyManager.varmap.dvalue);
free(MyManager.varmap.ivalue);
free(MyManager.varmap.dynvalue);
for (i = 0; i < MyManager.varmap.varcnt; i++)
free(MyManager.varmap.vars[i]);
free(MyManager.varmap.vars);
}
if (params.error != NULL) free(params.error);
return code;
}
/* Shell Parameters handling */
int argtype(const char *arg) {
if (strcmp(arg, "-l") == 0 || strcmp(arg, "--load") == 0) return 0;
if (strcmp(arg, "-e") == 0 || strcmp(arg, "--export") == 0) return 2;
if (strcmp(arg, "-m") == 0 || strcmp(arg, "--method") == 0) return 3;
if (strcmp(arg, "-i") == 0 || strcmp(arg, "--input") == 0) return 4;
if (strcmp(arg, "-h") == 0 || strcmp(arg, "--help") == 0) return 5;
if (strcmp(arg, "-d") == 0 || strcmp(arg, "--debug") == 0) return 6;
if (strcmp(arg, "-id") == 0 || strcmp(arg, "--queryid") == 0) return 7;
if (strcmp(arg, "-t") == 0 || strcmp(arg, "--timeout") == 0) return 8;
if (strcmp(arg, "-sd") == 0 || strcmp(arg, "--savedump") == 0) return 9;
if (strcmp(arg, "-sl") == 0 || strcmp(arg, "--slope") == 0) return 10;
if (strcmp(arg, "-o") == 0 || strcmp(arg, "--online") == 0) return 11;
if (strcmp(arg, "-bs") == 0 || strcmp(arg, "--bufsize") == 0) return 12;
if (strcmp(arg, "-pid") == 0 || strcmp(arg, "--pid") == 0) return 13;
return -1;
}
void printhelp(int argc, char **arg) {
fprintf(stderr, "\nUsage: %s -l [filename] -i [filename] -o (-s(d) [filename] -e [filename] -m [method] -id [queryid] -sl [double]) (-t [seconds] -d -h)\n", arg[0]);
fprintf(stderr, "Generates and traverses a BDD\nMandatory parameters:\n");
fprintf(stderr, "\t-l [filename]\t->\tfilename to load supports two formats:\n\t\t\t\t\t\t1. script with generation instructions\n\t\t\t\t\t\t2. node dump saved file\n");
fprintf(stderr, "\t-i [filename]\t->\tfilename to input problem specifics (mandatory with file formats 1, 2)\n");
fprintf(stderr, "\t-o\t\t->\tgenerates the BDD in online mode instead from a file can be used instead of -l\n");
fprintf(stderr, "Optional parameters:\n");
fprintf(stderr, "\t-sd [filename]\t->\tfilename to save generated BDD in node dump format (fast loading, traverse valid only)\n");
fprintf(stderr, "\t-e [filename]\t->\tfilename to export generated BDD in dot format\n");
fprintf(stderr, "\t-m [method]\t->\tthe calculation method to be used: none(default), [p]robability, [g]radient, [o]nline\n");
fprintf(stderr, "\t-id [queryid]\t->\tthe queries identity name (used by gradient) default: %s\n", arg[0]);
fprintf(stderr, "\t-sl [double]\t->\tthe sigmoid slope (used by gradient) default: 1.0\n");
fprintf(stderr, "Extra parameters:\n");
fprintf(stderr, "\t-t [seconds]\t->\tthe seconds (int) for BDD generation timeout default 0 = no timeout\n");
fprintf(stderr, "\t-pid [pid]\t->\ta process id (int) to check for termination default 0 = no process to check works only under POSIX OS\n");
fprintf(stderr, "\t-bs [bytes]\t->\tthe bytes (int) to use as a maximum buffer size to read files default 0 = no max\n");
fprintf(stderr, "\t-d\t\t->\tRun in debug mode (gives extra messages in stderr)\n");
fprintf(stderr, "\t-h\t\t->\tHelp (displays this message)\n\n");
fprintf(stderr, "Example: %s -l testbdd -i input.txt -m g -id testbdd\n", arg[0]);
}
parameters loadparam(int argc, char **arg) {
int i;
parameters params;
params.loadfile = -1;
params.savedfile = -1;
params.exportfile = -1;
params.method = 0;
params.inputfile = -1;
params.debug = 0;
params.errorcnt = 0;
params.queryid = 0;
params.timeout = 0;
params.sigmoid_slope = 1.0;
params.online = 0;
params.maxbufsize = 0;
params.ppid = NULL;
params.error = (int *) malloc(argc * sizeof(int));
for (i = 1; i < argc; i++) {
switch(argtype(arg[i])) {
case 0:
if (argc > i + 1) {
i++;
params.loadfile = i;
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 2:
if (argc > i + 1) {
i++;
params.exportfile = i;
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 3:
if (argc > i + 1) {
i++;
params.method = i;
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 4:
if (argc > i + 1) {
i++;
params.inputfile = i;
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 5:
printhelp(argc, arg);
break;
case 6:
params.debug = 1;
break;
case 7:
if (argc > i + 1) {
i++;
params.queryid = i;
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 8:
if ((argc > i + 1) && (IsPosNumber(arg[i + 1]))) {
i++;
params.timeout = atoi(arg[i]);
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 9:
if (argc > i + 1) {
i++;
params.savedfile = i;
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 10:
if ((argc > i + 1) && (IsRealNumber(arg[i + 1]))) {
i++;
params.sigmoid_slope = atof(arg[i]);
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 11:
params.online = 1;
break;
case 12:
if ((argc > i + 1) && (IsPosNumber(arg[i + 1]))) {
i++;
params.maxbufsize = atoi(arg[i]);
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
case 13:
if ((argc > i + 1) && (IsPosNumber(arg[i + 1]))) {
i++;
params.ppid = (char *) malloc(sizeof(char) * (strlen(arg[i]) + 1));
strcpy(params.ppid, arg[i]);
} else {
params.error[params.errorcnt] = i;
params.errorcnt++;
}
break;
default:
params.error[params.errorcnt] = i;
params.errorcnt++;
break;
}
}
return params;
}
/* Error Handlers */
void handler(int num) {
fprintf(stderr, "Error: Timeout %i exceeded.\n", params.timeout);
exit(-1);
}
void pidhandler(int num) {
char *s;
if (params.timeout > 0) {
params.timeout -= 5;
if (params.timeout <= 0) {
fprintf(stderr, "Error: Timeout exceeded.\n");
exit(-1);
}
}
s = (char *) malloc(sizeof(char) * (19 + strlen(params.ppid)));
strcpy(s, "ps "); strcat(s, params.ppid); strcat(s, " >/dev/null");
if (system(s) != 0) exit(4);
signal(SIGALRM, pidhandler);
alarm(5);
free(s);
}
void termhandler(int num) {
exit(3);
}
/* General Functions */
double sigmoid(double x, double slope) {
return 1 / (1 + exp(-x * slope));
}
/* Debugging traverse function */
void myexpand(extmanager MyManager, DdNode *Current) {
DdNode *h, *l;
hisnode *Found;
char *curnode;
curnode = GetNodeVarNameDisp(MyManager.manager, MyManager.varmap, Current);
printf("%s\n", curnode);
if ((Current != MyManager.t) && (Current != MyManager.f) &&
((Found = GetNode(MyManager.his, MyManager.varmap.varstart, Current)) == NULL)) {
l = LowNodeOf(MyManager.manager, Current);
h = HighNodeOf(MyManager.manager, Current);
printf("l(%s)->", curnode);
myexpand(MyManager, l);
printf("h(%s)->", curnode);
myexpand(MyManager, h);
AddNode(MyManager.his, MyManager.varmap.varstart, Current, 0.0, 0, NULL);
}
}
/* Angelikas Algorithm */
double CalcProbability(extmanager MyManager, DdNode *Current) {
DdNode *h, *l;
hisnode *Found;
char *curnode;
double lvalue, hvalue, tvalue;
if (params.debug) {
curnode = GetNodeVarNameDisp(MyManager.manager, MyManager.varmap, Current);
fprintf(stderr, "%s\n", curnode);
}
if (Current == MyManager.t) return 1.0;
if (Current == MyManager.f) return 0.0;
if ((Found = GetNode(MyManager.his, MyManager.varmap.varstart, Current)) != NULL) return Found->dvalue;
l = LowNodeOf(MyManager.manager, Current);
h = HighNodeOf(MyManager.manager, Current);
if (params.debug) fprintf(stderr, "l(%s)->", curnode);
lvalue = CalcProbability(MyManager, l);
if (params.debug) fprintf(stderr, "h(%s)->", curnode);
hvalue = CalcProbability(MyManager, h);
tvalue = MyManager.varmap.dvalue[GetIndex(Current) - MyManager.varmap.varstart];
tvalue = tvalue * hvalue + lvalue * (1.0 - tvalue);
AddNode(MyManager.his, MyManager.varmap.varstart, Current, tvalue, 0, NULL);
return tvalue;
}
/* Bernds Algorithm */
gradientpair CalcGradient(extmanager MyManager, DdNode *Current, int TargetVar, char *TargetPattern) {
DdNode *h, *l;
hisnode *Found;
char *curnode;
gradientpair lvalue, hvalue, tvalue;
double this_probability;
double *gradient;
if (params.debug) {
curnode = GetNodeVarNameDisp(MyManager.manager, MyManager.varmap, Current);
fprintf(stderr, "%s\n", curnode);
}
if (Current == MyManager.t) {
tvalue.probability = 1.0;
tvalue.gradient = 0.0;
return tvalue;
}
if (Current == MyManager.f) {
tvalue.probability = 0.0;
tvalue.gradient = 0.0;
return tvalue;
}
if ((Found = GetNode(MyManager.his, MyManager.varmap.varstart, Current)) != NULL) {
tvalue.probability = Found->dvalue;
tvalue.gradient = *((double *) Found->dynvalue);
return tvalue;
}
l = LowNodeOf(MyManager.manager, Current);
h = HighNodeOf(MyManager.manager, Current);
if (params.debug) fprintf(stderr, "l(%s)->", curnode);
lvalue = CalcGradient(MyManager, l, TargetVar, TargetPattern);
if (params.debug) fprintf(stderr, "h(%s)->", curnode);
hvalue = CalcGradient(MyManager, h, TargetVar, TargetPattern);
this_probability = sigmoid(MyManager.varmap.dvalue[GetIndex(Current) - MyManager.varmap.varstart], params.sigmoid_slope);
tvalue.probability = this_probability * hvalue.probability + (1 - this_probability) * lvalue.probability;
tvalue.gradient = this_probability * hvalue.gradient + (1 - this_probability) * lvalue.gradient;
if ((GetIndex(Current) == TargetVar) ||
((TargetPattern != NULL) && patternmatch(TargetPattern, MyManager.varmap.vars[GetIndex(Current)]))) {
tvalue.gradient += hvalue.probability - lvalue.probability;
}
gradient = (double *) malloc(sizeof(double));
*gradient = tvalue.gradient;
AddNode(MyManager.his, MyManager.varmap.varstart, Current, tvalue.probability, 0, gradient);
return tvalue;
}
char * extractpattern(char *thestr) {
char *p;
int i = 0, sl = strlen(thestr);
while((thestr[i] != '_') && (i < sl)) i++;
if (i == sl) return NULL;
i++;
p = (char *) malloc(sizeof(char) * (i + 2));
strncpy(p, thestr, i);
p[i] = '*';
p[i + 1] = '\0';
return p;
}
int patterncalculated(char *pattern, extmanager MyManager, int loc) {
int i;
if (pattern == NULL) return 0;
for (i = loc - 1; i > -1; i--)
if (patternmatch(pattern, MyManager.varmap.vars[i])) return 1;
return 0;
}

141
packages/ProbLog/simplecudd/SimpleCUDD.pl Normal file
View File

@ -0,0 +1,141 @@
:-use_module(library(system)).
%:-use_module(library(clib)).
bdd_init(FDO, FDI, PID):-
exec('/home/theo/BDDs/SimpleCUDD/Version4/Example -online', [pipe(FDO), pipe(FDI), std], PID).
%process_create('/home/theo/BDDs/SimpleCUDD/Version3/Example', ['-online'], [stdin(pipe(FDI)), stdout(pipe(FDO)), process(PID)]).
bdd_commit(FDO, LINE):-
write(FDO, LINE),
write(FDO, '\n').
bdd_kill(FDO, FDI, PID, S):-
bdd_commit(FDO, '@e'),
wait(PID, S),
%process_wait(PID, S),
close(FDO),
close(FDI).
bdd_line([], X, _, L):-
atomic(X),
X \= [],
(bdd_curinter(N) ->
retract(bdd_curinter(N))
;
N = 1
),
M is N + 1,
assert(bdd_curinter(M)),
atomic_concat(['L', N, '=', X], L).
bdd_line(L, X, O, NL):-
atomic(X),
X \= [],
atom(L),
L \= [],
atomic_concat([L, O, X], NL).
bdd_line(L, [], _, L):-!.
bdd_line(L, [X|T], O, R):-
bdd_line(L, X, O, NL),
bdd_line(NL, T, O, R).
bdd_AND(L, X, NL):-
bdd_line(L, X, '*', NL).
bdd_OR(L, X, NL):-
bdd_line(L, X, '+', NL).
bdd_XOR(L, X, NL):-
bdd_line(L, X, '#', NL).
bdd_NAND(L, X, NL):-
bdd_line(L, X, '~*', NL).
bdd_NOR(L, X, NL):-
bdd_line(L, X, '~+', NL).
bdd_XNOR(L, X, NL):-
bdd_line(L, X, '~#', NL).
bdd_not(X, NX):-
atomic(X),
atomic_concat(['~', X], NX).
bdd_laststep(L):-
bdd_curinter(N),
M is N - 1,
atomic_concat(['L', M], L),
!.
bdd_nextDFS(FDO):-
bdd_commit(FDO, '@n').
bdd_nextBFS(FDO):-
bdd_commit(FDO, '@n,BFS').
bdd_current(FDO, FDI, N, Qcnt):-
bdd_commit(FDO, '@c'),
read(FDI, F),
assert(F),
bdd_temp_value(N, Qcnt),
retract(F).
bdd_highnodeof(FDO, FDI, H):-
bdd_commit(FDO, '@h'),
read(FDI, F),
assert(F),
bdd_temp_value(H),
retract(F).
bdd_lownodeof(FDO, FDI, L):-
bdd_commit(FDO, '@l'),
read(FDI, F),
assert(F),
bdd_temp_value(L),
retract(F).
bdd_nodevaluesof(FDO, FDI, N, V):-
atomic_concat(['@v,', N], Q),
bdd_commit(FDO, Q),
read(FDI, F),
assert(F),
bdd_temp_value(V),
retract(F).
/*
bdd_addnodetohis(FDO, N, [D, I, Dyn]):-
atomic_concat(['@a,', N, ',', D, ',', I, ',', Dyn], Q),
bdd_commit(FDO, Q).
bdd_getnodefromhis(FDO, FDI, N, V):-
atomic_concat(['@g,', N], Q),
bdd_commit(FDO, Q),
read(FDI, F),
assert(F),
bdd_temp_value(V),
retract(F).
*/
runme:-
bdd_init(FDO, FDI, PID),
bdd_AND([], ['A', 'B', 'C', 'D', 'E'], L1),
bdd_laststep(L1S),
bdd_commit(FDO, L1),
bdd_AND([], ['A', 'F', 'G', '~B'], L2),
bdd_laststep(L2S),
bdd_commit(FDO, L2),
bdd_AND([], ['A', 'F', 'G', '~C'], L3),
bdd_laststep(L3S),
bdd_commit(FDO, L3),
bdd_OR([], [L1S, L2S, L3S], L4),
bdd_laststep(L4S),
bdd_commit(FDO, L4),
bdd_commit(FDO, L4S),
repeat,
bdd_current(FDO, FDI, N, I),
write(1),nl,
bdd_nodevaluesof(FDO, FDI, N, V),
write(N), write(' ('), write(V), write(')'), nl,
bdd_next(FDO),
I = 0, (N = 'TRUE' ; N = 'FALSE'),
bdd_kill(FDO, FDI, PID, S),
write('BDD terminated with state: '), write(S), nl.

234
packages/ProbLog/simplecudd/general.c Normal file
View File

@ -0,0 +1,234 @@
/******************************************************************************\
* *
* SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html) *
* SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be) *
* *
* Copyright T. Mantadelis and Katholieke Universiteit Leuven 2008 *
* *
* Author: Theofrastos Mantadelis *
* File: general.c *
* *
********************************************************************************
* *
* The "Artistic License" *
* *
* Preamble *
* *
* The intent of this document is to state the conditions under which a *
* Package may be copied, such that the Copyright Holder maintains some *
* semblance of artistic control over the development of the package, *
* while giving the users of the package the right to use and distribute *
* the Package in a more-or-less customary fashion, plus the right to make *
* reasonable modifications. *
* *
* Definitions: *
* *
* "Package" refers to the collection of files distributed by the *
* Copyright Holder, and derivatives of that collection of files *
* created through textual modification. *
* *
* "Standard Version" refers to such a Package if it has not been *
* modified, or has been modified in accordance with the wishes *
* of the Copyright Holder as specified below. *
* *
* "Copyright Holder" is whoever is named in the copyright or *
* copyrights for the package. *
* *
* "You" is you, if you're thinking about copying or distributing *
* this Package. *
* *
* "Reasonable copying fee" is whatever you can justify on the *
* basis of media cost, duplication charges, time of people involved, *
* and so on. (You will not be required to justify it to the *
* Copyright Holder, but only to the computing community at large *
* as a market that must bear the fee.) *
* *
* "Freely Available" means that no fee is charged for the item *
* itself, though there may be fees involved in handling the item. *
* It also means that recipients of the item may redistribute it *
* under the same conditions they received it. *
* *
* 1. You may make and give away verbatim copies of the source form of the *
* Standard Version of this Package without restriction, provided that you *
* duplicate all of the original copyright notices and associated disclaimers. *
* *
* 2. You may apply bug fixes, portability fixes and other modifications *
* derived from the Public Domain or from the Copyright Holder. A Package *
* modified in such a way shall still be considered the Standard Version. *
* *
* 3. You may otherwise modify your copy of this Package in any way, provided *
* that you insert a prominent notice in each changed file stating how and *
* when you changed that file, and provided that you do at least ONE of the *
* following: *
* *
* a) place your modifications in the Public Domain or otherwise make them *
* Freely Available, such as by posting said modifications to Usenet or *
* an equivalent medium, or placing the modifications on a major archive *
* site such as uunet.uu.net, or by allowing the Copyright Holder to include *
* your modifications in the Standard Version of the Package. *
* *
* b) use the modified Package only within your corporation or organization. *
* *
* c) rename any non-standard executables so the names do not conflict *
* with standard executables, which must also be provided, and provide *
* a separate manual page for each non-standard executable that clearly *
* documents how it differs from the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 4. You may distribute the programs of this Package in object code or *
* executable form, provided that you do at least ONE of the following: *
* *
* a) distribute a Standard Version of the executables and library files, *
* together with instructions (in the manual page or equivalent) on where *
* to get the Standard Version. *
* *
* b) accompany the distribution with the machine-readable source of *
* the Package with your modifications. *
* *
* c) give non-standard executables non-standard names, and clearly *
* document the differences in manual pages (or equivalent), together *
* with instructions on where to get the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 5. You may charge a reasonable copying fee for any distribution of this *
* Package. You may charge any fee you choose for support of this *
* Package. You may not charge a fee for this Package itself. However, *
* you may distribute this Package in aggregate with other (possibly *
* commercial) programs as part of a larger (possibly commercial) software *
* distribution provided that you do not advertise this Package as a *
* product of your own. You may embed this Package's interpreter within *
* an executable of yours (by linking); this shall be construed as a mere *
* form of aggregation, provided that the complete Standard Version of the *
* interpreter is so embedded. *
* *
* 6. The scripts and library files supplied as input to or produced as *
* output from the programs of this Package do not automatically fall *
* under the copyright of this Package, but belong to whoever generated *
* them, and may be sold commercially, and may be aggregated with this *
* Package. If such scripts or library files are aggregated with this *
* Package via the so-called "undump" or "unexec" methods of producing a *
* binary executable image, then distribution of such an image shall *
* neither be construed as a distribution of this Package nor shall it *
* fall under the restrictions of Paragraphs 3 and 4, provided that you do *
* not represent such an executable image as a Standard Version of this *
* Package. *
* *
* 7. C subroutines (or comparably compiled subroutines in other *
* languages) supplied by you and linked into this Package in order to *
* emulate subroutines and variables of the language defined by this *
* Package shall not be considered part of this Package, but are the *
* equivalent of input as in Paragraph 6, provided these subroutines do *
* not change the language in any way that would cause it to fail the *
* regression tests for the language. *
* *
* 8. Aggregation of this Package with a commercial distribution is always *
* permitted provided that the use of this Package is embedded; that is, *
* when no overt attempt is made to make this Package's interfaces visible *
* to the end user of the commercial distribution. Such use shall not be *
* construed as a distribution of this Package. *
* *
* 9. The name of the Copyright Holder may not be used to endorse or promote *
* products derived from this software without specific prior written *
* permission. *
* *
* 10. THIS PACKAGE IS PROVIDED "AS IS" AND WITHOUT ANY EXPRESS OR *
* IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED *
* WARRANTIES OF MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE. *
* *
* The End *
* *
\******************************************************************************/
#include "general.h"
/* Number Handling */
int IsRealNumber(char *c) {
int i, l;
l = strlen(c);
if (l <= 0) return 0;
if (l == 1) return IsNumberDigit(c[0]);
for(i = 1; i < strlen(c); i++) {
if (c[i] == '.') return IsPosNumber(&c[i + 1]);
if (!IsNumberDigit(c[i])) return 0;
}
return (IsNumberDigit(c[0]) || IsSignDigit(c[0]));
}
int IsPosNumber(const char *c) {
int i, l;
l = strlen(c);
if (l <= 0) return 0;
for(i = 0; i < strlen(c); i++) {
if (!IsNumberDigit(c[i])) return 0;
}
return 1;
}
int IsNumber(const char *c) {
int i, l;
l = strlen(c);
if (l <= 0) return 0;
if (l == 1) return IsNumberDigit(c[0]);
for(i = 1; i < strlen(c); i++) {
if (!IsNumberDigit(c[i])) return 0;
}
return (IsNumberDigit(c[0]) || IsSignDigit(c[0]));
}
/* File Handling */
char * freadstr(FILE *fd, const char *separators) {
char *str;
int buf, icur = 0, max = 10;
str = (char *) malloc(sizeof(char) * max);
str[0] = '\0';
do {
if ((buf = fgetc(fd)) != EOF) {
if (icur == (max - 1)) {
max = max * 2;
str = (char *) realloc(str, sizeof(char) * max);
}
if (!CharIn((char) buf, separators)) {
str[icur] = (char) buf;
icur++;
str[icur] = '\0';
}
}
} while(!CharIn(buf, separators) && !feof(fd));
return str;
}
int CharIn(const char c, const char *in) {
int i;
for (i = 0; i < strlen(in); i++)
if (c == in[i]) return 1;
return 0;
}
/* string handling */
int patternmatch(char *pattern, char *thestr) {
int i, j = -1, pl = strlen(pattern), sl = strlen(thestr);
for(i = 0; i < pl; i++) {
if (pattern[i] == '*') {
do {
i++;
if (i == pl) return 1;
} while(pattern[i] == '*');
do {
j++;
if (j >= sl) return 0;
if ((thestr[j] == pattern[i]) && patternmatch(pattern + i, thestr + j)) return 1;
} while(1);
} else {
j++;
if (j >= sl) return 0;
if (pattern[i] != thestr[j]) return 0;
}
}
return (pl == sl);
}

159
packages/ProbLog/simplecudd/general.h Normal file
View File

@ -0,0 +1,159 @@
/******************************************************************************\
* *
* SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html) *
* SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be) *
* *
* Copyright T. Mantadelis and Katholieke Universiteit Leuven 2008 *
* *
* Author: Theofrastos Mantadelis *
* File: general.h *
* *
********************************************************************************
* *
* The "Artistic License" *
* *
* Preamble *
* *
* The intent of this document is to state the conditions under which a *
* Package may be copied, such that the Copyright Holder maintains some *
* semblance of artistic control over the development of the package, *
* while giving the users of the package the right to use and distribute *
* the Package in a more-or-less customary fashion, plus the right to make *
* reasonable modifications. *
* *
* Definitions: *
* *
* "Package" refers to the collection of files distributed by the *
* Copyright Holder, and derivatives of that collection of files *
* created through textual modification. *
* *
* "Standard Version" refers to such a Package if it has not been *
* modified, or has been modified in accordance with the wishes *
* of the Copyright Holder as specified below. *
* *
* "Copyright Holder" is whoever is named in the copyright or *
* copyrights for the package. *
* *
* "You" is you, if you're thinking about copying or distributing *
* this Package. *
* *
* "Reasonable copying fee" is whatever you can justify on the *
* basis of media cost, duplication charges, time of people involved, *
* and so on. (You will not be required to justify it to the *
* Copyright Holder, but only to the computing community at large *
* as a market that must bear the fee.) *
* *
* "Freely Available" means that no fee is charged for the item *
* itself, though there may be fees involved in handling the item. *
* It also means that recipients of the item may redistribute it *
* under the same conditions they received it. *
* *
* 1. You may make and give away verbatim copies of the source form of the *
* Standard Version of this Package without restriction, provided that you *
* duplicate all of the original copyright notices and associated disclaimers. *
* *
* 2. You may apply bug fixes, portability fixes and other modifications *
* derived from the Public Domain or from the Copyright Holder. A Package *
* modified in such a way shall still be considered the Standard Version. *
* *
* 3. You may otherwise modify your copy of this Package in any way, provided *
* that you insert a prominent notice in each changed file stating how and *
* when you changed that file, and provided that you do at least ONE of the *
* following: *
* *
* a) place your modifications in the Public Domain or otherwise make them *
* Freely Available, such as by posting said modifications to Usenet or *
* an equivalent medium, or placing the modifications on a major archive *
* site such as uunet.uu.net, or by allowing the Copyright Holder to include *
* your modifications in the Standard Version of the Package. *
* *
* b) use the modified Package only within your corporation or organization. *
* *
* c) rename any non-standard executables so the names do not conflict *
* with standard executables, which must also be provided, and provide *
* a separate manual page for each non-standard executable that clearly *
* documents how it differs from the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 4. You may distribute the programs of this Package in object code or *
* executable form, provided that you do at least ONE of the following: *
* *
* a) distribute a Standard Version of the executables and library files, *
* together with instructions (in the manual page or equivalent) on where *
* to get the Standard Version. *
* *
* b) accompany the distribution with the machine-readable source of *
* the Package with your modifications. *
* *
* c) give non-standard executables non-standard names, and clearly *
* document the differences in manual pages (or equivalent), together *
* with instructions on where to get the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 5. You may charge a reasonable copying fee for any distribution of this *
* Package. You may charge any fee you choose for support of this *
* Package. You may not charge a fee for this Package itself. However, *
* you may distribute this Package in aggregate with other (possibly *
* commercial) programs as part of a larger (possibly commercial) software *
* distribution provided that you do not advertise this Package as a *
* product of your own. You may embed this Package's interpreter within *
* an executable of yours (by linking); this shall be construed as a mere *
* form of aggregation, provided that the complete Standard Version of the *
* interpreter is so embedded. *
* *
* 6. The scripts and library files supplied as input to or produced as *
* output from the programs of this Package do not automatically fall *
* under the copyright of this Package, but belong to whoever generated *
* them, and may be sold commercially, and may be aggregated with this *
* Package. If such scripts or library files are aggregated with this *
* Package via the so-called "undump" or "unexec" methods of producing a *
* binary executable image, then distribution of such an image shall *
* neither be construed as a distribution of this Package nor shall it *
* fall under the restrictions of Paragraphs 3 and 4, provided that you do *
* not represent such an executable image as a Standard Version of this *
* Package. *
* *
* 7. C subroutines (or comparably compiled subroutines in other *
* languages) supplied by you and linked into this Package in order to *
* emulate subroutines and variables of the language defined by this *
* Package shall not be considered part of this Package, but are the *
* equivalent of input as in Paragraph 6, provided these subroutines do *
* not change the language in any way that would cause it to fail the *
* regression tests for the language. *
* *
* 8. Aggregation of this Package with a commercial distribution is always *
* permitted provided that the use of this Package is embedded; that is, *
* when no overt attempt is made to make this Package's interfaces visible *
* to the end user of the commercial distribution. Such use shall not be *
* construed as a distribution of this Package. *
* *
* 9. The name of the Copyright Holder may not be used to endorse or promote *
* products derived from this software without specific prior written *
* permission. *
* *
* 10. THIS PACKAGE IS PROVIDED "AS IS" AND WITHOUT ANY EXPRESS OR *
* IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED *
* WARRANTIES OF MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE. *
* *
* The End *
* *
\******************************************************************************/
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#define IsNumberDigit(c) ('0' <= c && c <= '9')
#define IsSignDigit(c) (c == '+' || c == '-')
#define isOperator(x) (x == '+' || x == '*' || x == '#' || x == '=')
#define freadline(fd) freadstr(fd, "\n");
int IsRealNumber(char *c);
int IsPosNumber(const char *c);
int IsNumber(const char *c);
char * freadstr(FILE *fd, const char *separators);
int CharIn(const char c, const char *in);
int patternmatch(char *pattern, char *thestr);

1620
packages/ProbLog/simplecudd/simplecudd.c Normal file
View File

File diff suppressed because it is too large Load Diff

287
packages/ProbLog/simplecudd/simplecudd.h Normal file
View File

@ -0,0 +1,287 @@
/******************************************************************************\
* *
* SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html) *
* SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be) *
* *
* Copyright T. Mantadelis and Katholieke Universiteit Leuven 2008 *
* *
* Author: Theofrastos Mantadelis *
* File: simplecudd.h *
* *
********************************************************************************
* *
* The "Artistic License" *
* *
* Preamble *
* *
* The intent of this document is to state the conditions under which a *
* Package may be copied, such that the Copyright Holder maintains some *
* semblance of artistic control over the development of the package, *
* while giving the users of the package the right to use and distribute *
* the Package in a more-or-less customary fashion, plus the right to make *
* reasonable modifications. *
* *
* Definitions: *
* *
* "Package" refers to the collection of files distributed by the *
* Copyright Holder, and derivatives of that collection of files *
* created through textual modification. *
* *
* "Standard Version" refers to such a Package if it has not been *
* modified, or has been modified in accordance with the wishes *
* of the Copyright Holder as specified below. *
* *
* "Copyright Holder" is whoever is named in the copyright or *
* copyrights for the package. *
* *
* "You" is you, if you're thinking about copying or distributing *
* this Package. *
* *
* "Reasonable copying fee" is whatever you can justify on the *
* basis of media cost, duplication charges, time of people involved, *
* and so on. (You will not be required to justify it to the *
* Copyright Holder, but only to the computing community at large *
* as a market that must bear the fee.) *
* *
* "Freely Available" means that no fee is charged for the item *
* itself, though there may be fees involved in handling the item. *
* It also means that recipients of the item may redistribute it *
* under the same conditions they received it. *
* *
* 1. You may make and give away verbatim copies of the source form of the *
* Standard Version of this Package without restriction, provided that you *
* duplicate all of the original copyright notices and associated disclaimers. *
* *
* 2. You may apply bug fixes, portability fixes and other modifications *
* derived from the Public Domain or from the Copyright Holder. A Package *
* modified in such a way shall still be considered the Standard Version. *
* *
* 3. You may otherwise modify your copy of this Package in any way, provided *
* that you insert a prominent notice in each changed file stating how and *
* when you changed that file, and provided that you do at least ONE of the *
* following: *
* *
* a) place your modifications in the Public Domain or otherwise make them *
* Freely Available, such as by posting said modifications to Usenet or *
* an equivalent medium, or placing the modifications on a major archive *
* site such as uunet.uu.net, or by allowing the Copyright Holder to include *
* your modifications in the Standard Version of the Package. *
* *
* b) use the modified Package only within your corporation or organization. *
* *
* c) rename any non-standard executables so the names do not conflict *
* with standard executables, which must also be provided, and provide *
* a separate manual page for each non-standard executable that clearly *
* documents how it differs from the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 4. You may distribute the programs of this Package in object code or *
* executable form, provided that you do at least ONE of the following: *
* *
* a) distribute a Standard Version of the executables and library files, *
* together with instructions (in the manual page or equivalent) on where *
* to get the Standard Version. *
* *
* b) accompany the distribution with the machine-readable source of *
* the Package with your modifications. *
* *
* c) give non-standard executables non-standard names, and clearly *
* document the differences in manual pages (or equivalent), together *
* with instructions on where to get the Standard Version. *
* *
* d) make other distribution arrangements with the Copyright Holder. *
* *
* 5. You may charge a reasonable copying fee for any distribution of this *
* Package. You may charge any fee you choose for support of this *
* Package. You may not charge a fee for this Package itself. However, *
* you may distribute this Package in aggregate with other (possibly *
* commercial) programs as part of a larger (possibly commercial) software *
* distribution provided that you do not advertise this Package as a *
* product of your own. You may embed this Package's interpreter within *
* an executable of yours (by linking); this shall be construed as a mere *
* form of aggregation, provided that the complete Standard Version of the *
* interpreter is so embedded. *
* *
* 6. The scripts and library files supplied as input to or produced as *
* output from the programs of this Package do not automatically fall *
* under the copyright of this Package, but belong to whoever generated *
* them, and may be sold commercially, and may be aggregated with this *
* Package. If such scripts or library files are aggregated with this *
* Package via the so-called "undump" or "unexec" methods of producing a *
* binary executable image, then distribution of such an image shall *
* neither be construed as a distribution of this Package nor shall it *
* fall under the restrictions of Paragraphs 3 and 4, provided that you do *
* not represent such an executable image as a Standard Version of this *
* Package. *
* *
* 7. C subroutines (or comparably compiled subroutines in other *
* languages) supplied by you and linked into this Package in order to *
* emulate subroutines and variables of the language defined by this *
* Package shall not be considered part of this Package, but are the *
* equivalent of input as in Paragraph 6, provided these subroutines do *
* not change the language in any way that would cause it to fail the *
* regression tests for the language. *
* *
* 8. Aggregation of this Package with a commercial distribution is always *
* permitted provided that the use of this Package is embedded; that is, *
* when no overt attempt is made to make this Package's interfaces visible *
* to the end user of the commercial distribution. Such use shall not be *
* construed as a distribution of this Package. *
* *
* 9. The name of the Copyright Holder may not be used to endorse or promote *
* products derived from this software without specific prior written *
* permission. *
* *
* 10. THIS PACKAGE IS PROVIDED "AS IS" AND WITHOUT ANY EXPRESS OR *
* IMPLIED WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED *
* WARRANTIES OF MERCHANTIBILITY AND FITNESS FOR A PARTICULAR PURPOSE. *
* *
* The End *
* *
\******************************************************************************/
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <math.h>
#include <time.h>
#include "util.h"
#include "cudd.h"
#include "cuddInt.h"
#include "general.h"
#define IsHigh(manager, node) HIGH(manager) == node
#define IsLow(manager, node) LOW(manager) == node
#define HIGH(manager) Cudd_ReadOne(manager)
#define LOW(manager) Cudd_Not(Cudd_ReadOne(manager))
#define NOT(node) Cudd_Not(node)
#define GetIndex(node) Cudd_NodeReadIndex(node)
#define GetVar(manager, index) Cudd_bddIthVar(manager, index)
#define NewVar(manager) Cudd_bddNewVar(manager)
#define KillBDD(manager) Cudd_Quit(manager)
#define GetVarCount(manager) Cudd_ReadSize(manager)
#define DEBUGON _debug = 1
#define DEBUGOFF _debug = 0
#define RAPIDLOADON _RapidLoad = 1
#define RAPIDLOADOFF _RapidLoad = 0
#define SETMAXBUFSIZE(size) _maxbufsize = size
#define BDDFILE_ERROR -1
#define BDDFILE_OTHER 0
#define BDDFILE_SCRIPT 1
#define BDDFILE_NODEDUMP 2
extern int _RapidLoad;
extern int _debug;
extern int _maxbufsize;
typedef struct _bddfileheader {
FILE *inputfile;
int version;
int varcnt;
int varstart;
int intercnt;
int filetype;
} bddfileheader;
typedef struct _namedvars {
int varcnt;
int varstart;
char **vars;
int *loaded;
double *dvalue;
int *ivalue;
void **dynvalue;
} namedvars;
typedef struct _hisnode {
DdNode *key;
double dvalue;
int ivalue;
void *dynvalue;
} hisnode;
typedef struct _hisqueue {
int cnt;
hisnode *thenode;
} hisqueue;
typedef struct _nodeline {
char *varname;
char *truevar;
char *falsevar;
int nodenum;
int truenode;
int falsenode;
} nodeline;
/* Initialization */
DdManager* simpleBDDinit(int varcnt);
/* BDD Generation */
DdNode* D_BDDAnd(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* D_BDDNand(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* D_BDDOr(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* D_BDDNor(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* D_BDDXor(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* D_BDDXnor(DdManager *manager, DdNode *bdd1, DdNode *bdd2);
DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader fileheader);
DdNode* OnlineGenerateBDD(DdManager *manager, namedvars *varmap);
DdNode* LineParser(DdManager *manager, namedvars varmap, DdNode **inter, int maxinter, char *function, int iline);
DdNode* OnlineLineParser(DdManager *manager, namedvars *varmap, DdNode **inter, int maxinter, char *function, int iline);
DdNode* BDD_Operator(DdManager *manager, DdNode *bdd1, DdNode *bdd2, char Operator, int inegoper);
int getInterBDD(char *function);
char* getFileName(const char *function);
int GetParam(char *inputline, int iParam);
int LoadVariableData(namedvars varmap, char *filename);
/* Named variables */
namedvars InitNamedVars(int varcnt, int varstart);
void EnlargeNamedVars(namedvars *varmap, int newvarcnt);
int AddNamedVarAt(namedvars varmap, const char *varname, int index);
int AddNamedVar(namedvars varmap, const char *varname);
void SetNamedVarValuesAt(namedvars varmap, int index, double dvalue, int ivalue, void *dynvalue);
int SetNamedVarValues(namedvars varmap, const char *varname, double dvalue, int ivalue, void *dynvalue);
int GetNamedVarIndex(const namedvars varmap, const char *varname);
int RepairVarcnt(namedvars *varmap);
char* GetNodeVarName(DdManager *manager, namedvars varmap, DdNode *node);
char* GetNodeVarNameDisp(DdManager *manager, namedvars varmap, DdNode *node);
int all_loaded(namedvars varmap, int disp);
/* Traversal */
DdNode* HighNodeOf(DdManager *manager, DdNode *node);
DdNode* LowNodeOf(DdManager *manager, DdNode *node);
/* Traversal - History */
hisqueue* InitHistory(int varcnt);
void ReInitHistory(hisqueue *HisQueue, int varcnt);
void AddNode(hisqueue *HisQueue, int varstart, DdNode *node, double dvalue, int ivalue, void *dynvalue);
hisnode* GetNode(hisqueue *HisQueue, int varstart, DdNode *node);
int GetNodeIndex(hisqueue *HisQueue, int varstart, DdNode *node);
void onlinetraverse(DdManager *manager, namedvars varmap, hisqueue *HisQueue, DdNode *bdd);
/* Save-load */
bddfileheader ReadFileHeader(char *filename);
int CheckFileVersion(const char *version);
DdNode * LoadNodeDump(DdManager *manager, namedvars varmap, FILE *inputfile);
DdNode * LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes, FILE *inputfile, nodeline current);
DdNode * GetIfExists(DdManager *manager, namedvars varmap, hisqueue *Nodes, char *varname, int nodenum);
int SaveNodeDump(DdManager *manager, namedvars varmap, DdNode *bdd, char *filename);
void SaveExpand(DdManager *manager, namedvars varmap, hisqueue *Nodes, DdNode *Current, FILE *outputfile);
void ExpandNodes(hisqueue *Nodes, int index, int nodenum);
/* Export */
int simpleBDDtoDot(DdManager *manager, DdNode *bdd, char *filename);
int simpleNamedBDDtoDot(DdManager *manager, namedvars varmap, DdNode *bdd, char *filename);