From a6747da26e3a4bd3ee64333275f01342eb8b89b3 Mon Sep 17 00:00:00 2001 From: Vitor Santos Costa Date: Mon, 9 Mar 2009 00:42:12 +0000 Subject: [PATCH] simplecudd interface --- packages/ProbLog/simplecudd/Example.c | 281 ++++ packages/ProbLog/simplecudd/LICENCE | 131 ++ packages/ProbLog/simplecudd/Makefile.in | 61 + packages/ProbLog/simplecudd/ProblogBDD.c | 675 +++++++++ packages/ProbLog/simplecudd/SimpleCUDD.pl | 141 ++ packages/ProbLog/simplecudd/general.c | 234 +++ packages/ProbLog/simplecudd/general.h | 159 ++ packages/ProbLog/simplecudd/simplecudd.c | 1620 +++++++++++++++++++++ packages/ProbLog/simplecudd/simplecudd.h | 287 ++++ 9 files changed, 3589 insertions(+) create mode 100644 packages/ProbLog/simplecudd/Example.c create mode 100644 packages/ProbLog/simplecudd/LICENCE create mode 100644 packages/ProbLog/simplecudd/Makefile.in create mode 100644 packages/ProbLog/simplecudd/ProblogBDD.c create mode 100644 packages/ProbLog/simplecudd/SimpleCUDD.pl create mode 100644 packages/ProbLog/simplecudd/general.c create mode 100644 packages/ProbLog/simplecudd/general.h create mode 100644 packages/ProbLog/simplecudd/simplecudd.c create mode 100644 packages/ProbLog/simplecudd/simplecudd.h diff --git a/packages/ProbLog/simplecudd/Example.c b/packages/ProbLog/simplecudd/Example.c new file mode 100644 index 000000000..c0dab075f --- /dev/null +++ b/packages/ProbLog/simplecudd/Example.c @@ -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; +} diff --git a/packages/ProbLog/simplecudd/LICENCE b/packages/ProbLog/simplecudd/LICENCE new file mode 100644 index 000000000..5f221241e --- /dev/null +++ b/packages/ProbLog/simplecudd/LICENCE @@ -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 diff --git a/packages/ProbLog/simplecudd/Makefile.in b/packages/ProbLog/simplecudd/Makefile.in new file mode 100644 index 000000000..a1955eca7 --- /dev/null +++ b/packages/ProbLog/simplecudd/Makefile.in @@ -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) diff --git a/packages/ProbLog/simplecudd/ProblogBDD.c b/packages/ProbLog/simplecudd/ProblogBDD.c new file mode 100644 index 000000000..8b38d49e0 --- /dev/null +++ b/packages/ProbLog/simplecudd/ProblogBDD.c @@ -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 + +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; +} diff --git a/packages/ProbLog/simplecudd/SimpleCUDD.pl b/packages/ProbLog/simplecudd/SimpleCUDD.pl new file mode 100644 index 000000000..9fe1ecfb0 --- /dev/null +++ b/packages/ProbLog/simplecudd/SimpleCUDD.pl @@ -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. + diff --git a/packages/ProbLog/simplecudd/general.c b/packages/ProbLog/simplecudd/general.c new file mode 100644 index 000000000..64a7f88e1 --- /dev/null +++ b/packages/ProbLog/simplecudd/general.c @@ -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); +} diff --git a/packages/ProbLog/simplecudd/general.h b/packages/ProbLog/simplecudd/general.h new file mode 100644 index 000000000..4441ed623 --- /dev/null +++ b/packages/ProbLog/simplecudd/general.h @@ -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 +#include +#include + +#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); diff --git a/packages/ProbLog/simplecudd/simplecudd.c b/packages/ProbLog/simplecudd/simplecudd.c new file mode 100644 index 000000000..6ee290377 --- /dev/null +++ b/packages/ProbLog/simplecudd/simplecudd.c @@ -0,0 +1,1620 @@ +/******************************************************************************\ +* * +* 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.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" + +/* BDD manager initialization */ + +int _debug = 0; +int _RapidLoad = 0; +int _maxbufsize = 0; + +DdManager* simpleBDDinit(int varcnt) { + DdManager *temp; + temp = Cudd_Init(varcnt, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0); + Cudd_AutodynEnable(temp, CUDD_REORDER_GROUP_SIFT); + Cudd_SetMaxCacheHard(temp, 1024*1024*1024); + Cudd_SetLooseUpTo(temp, 1024*1024*512); + if (_debug) Cudd_EnableReorderingReporting(temp); + return temp; +} + +/* BDD tree travesrsing */ + +DdNode* HighNodeOf(DdManager *manager, DdNode *node) { + DdNode *tmp; + if (IsHigh(manager, node)) return HIGH(manager); + if (IsLow(manager, node)) return LOW(manager); + tmp = Cudd_Regular(node); + if (Cudd_IsComplement(node)) return NOT(tmp->type.kids.T); + return tmp->type.kids.T; +} + +DdNode* LowNodeOf(DdManager *manager, DdNode *node) { + DdNode *tmp; + if (IsHigh(manager, node)) return HIGH(manager); + if (IsLow(manager, node)) return LOW(manager); + tmp = Cudd_Regular(node); + if (Cudd_IsComplement(node)) return NOT(tmp->type.kids.E); + return tmp->type.kids.E; +} + +/* BDD tree generation */ + +DdNode* D_BDDAnd(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { + DdNode *tmp; + tmp = Cudd_bddAnd(manager, bdd1, bdd2); + Cudd_Ref(tmp); + Cudd_RecursiveDeref(manager, bdd2); + return tmp; +} + +DdNode* D_BDDNand(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { + DdNode *tmp; + tmp = Cudd_bddNand(manager, bdd1, bdd2); + Cudd_Ref(tmp); + Cudd_RecursiveDeref(manager, bdd2); + return tmp; +} + +DdNode* D_BDDOr(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { + DdNode *tmp; + tmp = Cudd_bddOr(manager, bdd1, bdd2); + Cudd_Ref(tmp); + Cudd_RecursiveDeref(manager, bdd2); + return tmp; +} + +DdNode* D_BDDNor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { + DdNode *tmp; + tmp = Cudd_bddNor(manager, bdd1, bdd2); + Cudd_Ref(tmp); + Cudd_RecursiveDeref(manager, bdd2); + return tmp; +} + +DdNode* D_BDDXor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { + DdNode *tmp; + tmp = Cudd_bddXor(manager, bdd1, bdd2); + Cudd_Ref(tmp); + Cudd_RecursiveDeref(manager, bdd2); + return tmp; +} + +DdNode* D_BDDXnor(DdManager *manager, DdNode *bdd1, DdNode *bdd2) { + DdNode *tmp; + tmp = Cudd_bddXnor(manager, bdd1, bdd2); + Cudd_Ref(tmp); + Cudd_RecursiveDeref(manager, bdd2); + return tmp; +} + +/* file manipulation */ + +bddfileheader ReadFileHeader(char *filename) { + bddfileheader temp; + char *header; + temp.inputfile = NULL; + temp.version = 0; + temp.varcnt = 0; + temp.varstart = 0; + temp.intercnt = 0; + temp.filetype = BDDFILE_OTHER; + if ((temp.inputfile = fopen(filename, "r")) == NULL) { + perror(filename); + temp.filetype = BDDFILE_ERROR; + return temp; + } + // Read file header + if (!feof(temp.inputfile)) { + header = freadline(temp.inputfile); + temp.version = CheckFileVersion(header); + if (temp.version > -1) temp.filetype = (strlen(header) == 5) * BDDFILE_SCRIPT + (strlen(header) == 7) * BDDFILE_NODEDUMP; + free(header); + switch (temp.filetype) { + case BDDFILE_SCRIPT: + switch (temp.version) { + case 1: + fscanf(temp.inputfile, "%i\n", &temp.varcnt); + fscanf(temp.inputfile, "%i\n", &temp.varstart); + fscanf(temp.inputfile, "%i\n", &temp.intercnt); + break; + default: + fclose(temp.inputfile); + temp.inputfile = NULL; + break; + } + break; + case BDDFILE_NODEDUMP: + switch (temp.version) { + case 1: + fscanf(temp.inputfile, "%i\n", &temp.varcnt); + fscanf(temp.inputfile, "%i\n", &temp.varstart); + break; + default: + fclose(temp.inputfile); + temp.inputfile = NULL; + break; + } + break; + case BDDFILE_OTHER: + fclose(temp.inputfile); + temp.inputfile = NULL; + break; + default: + fclose(temp.inputfile); + temp.inputfile = NULL; + break; + } + } + return temp; +} + +int CheckFileVersion(const char *version) { + if (strlen(version) < 5) return -1; + if (strlen(version) == 5 && version[0] == '@' && version[1] == 'B' && version[2] == 'D' && version[3] == 'D') return atoi(version + 4); + if (strlen(version) == 7 && version[0] == '@' && version[1] == 'N' && version[2] == 'O' && version[3] == 'D' + && version[4] == 'E' && version[5] == 'S') return atoi(version + 6); + return -1; +} + +int simpleBDDtoDot(DdManager *manager, DdNode *bdd, char *filename) { + DdNode *f[1]; + int ret; + FILE *fd; + f[0] = Cudd_BddToAdd(manager, bdd); + fd = fopen(filename, "w"); + if (fd == NULL) { + perror(filename); + return -1; + } + ret = Cudd_DumpDot(manager, 1, f, NULL, NULL, fd); + fclose(fd); + return ret; +} + +int simpleNamedBDDtoDot(DdManager *manager, namedvars varmap, DdNode *bdd, char *filename) { + DdNode *f[1]; + int ret; + FILE *fd; + f[0] = Cudd_BddToAdd(manager, bdd); + fd = fopen(filename, "w"); + if (fd == NULL) { + perror(filename); + return -1; + } + ret = Cudd_DumpDot(manager, 1, f, varmap.vars, NULL, fd); + fclose(fd); + return ret; +} + +int SaveNodeDump(DdManager *manager, namedvars varmap, DdNode *bdd, char *filename) { + hisqueue *Nodes; + FILE *outputfile; + int i; + if ((outputfile = fopen(filename, "w")) == NULL) { + perror(filename); + return -1; + } + fprintf(outputfile, "%s\n%i\n%i\n", "@NODES1", varmap.varcnt, varmap.varstart); + Nodes = InitHistory(varmap.varcnt); + for (i = 0; i < varmap.varcnt; i++) + fprintf(outputfile, "%s\t%i\n", varmap.vars[i], Cudd_ReadPerm(manager, i)); + if (bdd == HIGH(manager)) fprintf(outputfile, "TRUE\t0\tTRUE\t0\tTRUE\t0\n"); + else if (bdd == LOW(manager)) fprintf(outputfile, "FALSE\t0\tFALSE\t0\tFALSE\t0\n"); + else SaveExpand(manager, varmap, Nodes, bdd, outputfile); + ReInitHistory(Nodes, varmap.varcnt); + free(Nodes); + fclose(outputfile); + return 0; +} + +void SaveExpand(DdManager *manager, namedvars varmap, hisqueue *Nodes, DdNode *Current, FILE *outputfile) { + DdNode *h, *l; + hisnode *Found; + char *curnode; + int inode; + if (Current != HIGH(manager) && Current != LOW(manager)) { + if ((Found = GetNode(Nodes, varmap.varstart, Current)) == NULL) { + AddNode(Nodes, varmap.varstart, Current, 0.0, 0, NULL); + Found = GetNode(Nodes, varmap.varstart, Current); + } + if (!(Found->ivalue)) { + Found->ivalue = 1; + curnode = GetNodeVarNameDisp(manager, varmap, Current); + inode = GetNodeIndex(Nodes, varmap.varstart, Current); + fprintf(outputfile, "%s\t%i\t", curnode, inode); + h = HighNodeOf(manager, Current); + if (h == HIGH(manager)) { + fprintf(outputfile, "TRUE\t0\t"); + } else if (h == LOW(manager)) { + fprintf(outputfile, "FALSE\t0\t"); + } else { + if (GetNode(Nodes, varmap.varstart, h) == NULL) AddNode(Nodes, varmap.varstart, h, 0.0, 0, NULL); + curnode = GetNodeVarNameDisp(manager, varmap, h); + inode = GetNodeIndex(Nodes, varmap.varstart, h); + fprintf(outputfile, "%s\t%i\t", curnode, inode); + } + l = LowNodeOf(manager, Current); + if (l == HIGH(manager)) { + fprintf(outputfile, "TRUE\t0\n"); + } else if (l == LOW(manager)) { + fprintf(outputfile, "FALSE\t0\n"); + } else { + if (GetNode(Nodes, varmap.varstart, l) == NULL) AddNode(Nodes, varmap.varstart, l, 0.0, 0, NULL); + curnode = GetNodeVarNameDisp(manager, varmap, l); + inode = GetNodeIndex(Nodes, varmap.varstart, l); + fprintf(outputfile, "%s\t%i\n", curnode, inode); + } + SaveExpand(manager, varmap, Nodes, l, outputfile); + SaveExpand(manager, varmap, Nodes, h, outputfile); + } + } +} + +DdNode * LoadNodeDump(DdManager *manager, namedvars varmap, FILE *inputfile) { + hisqueue *Nodes; + nodeline temp; + DdNode *ret; + int i, pos, *perm; + char *varnam; + perm = (int *) malloc(sizeof(int) * varmap.varcnt); + Nodes = InitHistory(varmap.varcnt); + for (i = 0; i < varmap.varcnt; i++) { + varnam = freadstr(inputfile, "\t"); + pos = atoi(freadstr(inputfile, "\n")); + AddNamedVarAt(varmap, varnam, pos); + perm[pos] = pos; + } + temp.varname = freadstr(inputfile, "\t"); + fscanf(inputfile, "%i\t", &temp.nodenum); + temp.truevar = freadstr(inputfile, "\t"); + fscanf(inputfile, "%i\t", &temp.truenode); + temp.falsevar = freadstr(inputfile, "\t"); + fscanf(inputfile, "%i\n", &temp.falsenode); + ret = LoadNodeRec(manager, varmap, Nodes, inputfile, temp); + free(temp.varname); + free(temp.truevar); + free(temp.falsevar); + fclose(inputfile); + ReInitHistory(Nodes, varmap.varcnt); + free(Nodes); + Cudd_Ref(ret); + Cudd_ShuffleHeap(manager, perm); + for (i = 0; i < varmap.varcnt; i++) varmap.ivalue[i] = 0; + return ret; +} + +DdNode * LoadNodeRec(DdManager *manager, namedvars varmap, hisqueue *Nodes, FILE *inputfile, nodeline current) { + nodeline temp; + DdNode *newnode, *truenode, *falsenode; + int index; + newnode = GetIfExists(manager, varmap, Nodes, current.varname, current.nodenum); + if (newnode != NULL) return newnode; + falsenode = GetIfExists(manager, varmap, Nodes, current.falsevar, current.falsenode); + if (falsenode == NULL) { + temp.varname = freadstr(inputfile, "\t"); + fscanf(inputfile, "%i\t", &temp.nodenum); + temp.truevar = freadstr(inputfile, "\t"); + fscanf(inputfile, "%i\t", &temp.truenode); + temp.falsevar = freadstr(inputfile, "\t"); + fscanf(inputfile, "%i\n", &temp.falsenode); + falsenode = LoadNodeRec(manager, varmap, Nodes, inputfile, temp); + free(temp.varname); + free(temp.truevar); + free(temp.falsevar); + } + truenode = GetIfExists(manager, varmap, Nodes, current.truevar, current.truenode); + if (truenode == NULL) { + temp.varname = freadstr(inputfile, "\t"); + fscanf(inputfile, "%i\t", &temp.nodenum); + temp.truevar = freadstr(inputfile, "\t"); + fscanf(inputfile, "%i\t", &temp.truenode); + temp.falsevar = freadstr(inputfile, "\t"); + fscanf(inputfile, "%i\n", &temp.falsenode); + truenode = LoadNodeRec(manager, varmap, Nodes, inputfile, temp); + free(temp.varname); + free(temp.truevar); + free(temp.falsevar); + } + index = GetNamedVarIndex(varmap, current.varname); + if (!varmap.ivalue[index]) { + varmap.ivalue[index] = 1; + newnode = GetVar(manager, varmap.varstart + index); + //Cudd_RecursiveDeref(manager, newnode->type.kids.T); + //Cudd_RecursiveDeref(manager, newnode->type.kids.E); + newnode->type.kids.T = Cudd_NotCond(truenode, Cudd_IsComplement(truenode)); + newnode->type.kids.E = Cudd_NotCond(falsenode, Cudd_IsComplement(truenode)); + Cudd_Ref(newnode->type.kids.T); + Cudd_Ref(newnode->type.kids.E); + Cudd_Ref(newnode); + } else { + if (_RapidLoad == 1) { + newnode = cuddAllocNode(manager); + if (newnode != NULL) { + newnode->index = varmap.varstart + index; + newnode->type.kids.T = Cudd_NotCond(truenode, Cudd_IsComplement(truenode)); + newnode->type.kids.E = Cudd_NotCond(falsenode, Cudd_IsComplement(truenode)); + Cudd_Ref(newnode->type.kids.T); + Cudd_Ref(newnode->type.kids.E); + Cudd_Ref(newnode); + } + } else { + newnode = cuddUniqueInter(manager, varmap.varstart + index, Cudd_NotCond(truenode, Cudd_IsComplement(truenode)), Cudd_NotCond(falsenode, Cudd_IsComplement(truenode))); + if (newnode != NULL) { + Cudd_Ref(newnode); + } else { + newnode = cuddAllocNode(manager); + if (newnode != NULL) { + newnode->index = varmap.varstart + index; + newnode->type.kids.T = Cudd_NotCond(truenode, Cudd_IsComplement(truenode)); + newnode->type.kids.E = Cudd_NotCond(falsenode, Cudd_IsComplement(truenode)); + Cudd_Ref(newnode->type.kids.T); + Cudd_Ref(newnode->type.kids.E); + Cudd_Ref(newnode); + } + } + } + } + if (newnode != NULL) { + Nodes[index].thenode[current.nodenum].key = Cudd_NotCond(newnode, Cudd_IsComplement(truenode)); + return Cudd_NotCond(newnode, Cudd_IsComplement(truenode)); + } + return NULL; +} + +DdNode * GetIfExists(DdManager *manager, namedvars varmap, hisqueue *Nodes, char *varname, int nodenum) { + int index; + if (strcmp(varname, "TRUE") == 0) return HIGH(manager); + if (strcmp(varname, "FALSE") == 0) return LOW(manager); + index = GetNamedVarIndex(varmap, varname); + if (index == -1 * varmap.varcnt) { + fprintf(stderr, "Error: more variables requested than initialized.\n"); + exit(-1); + } + if ((index < 0) || (index == 0 && varmap.vars[0] == NULL)) { + index = AddNamedVar(varmap, varname); + } + ExpandNodes(Nodes, index, nodenum); + if (Nodes[index].thenode[nodenum].key != NULL) return Nodes[index].thenode[nodenum].key; + return NULL; +} + +void ExpandNodes(hisqueue *Nodes, int index, int nodenum) { + int i; + if (Nodes[index].cnt > nodenum) return; + Nodes[index].thenode = (hisnode *) realloc(Nodes[index].thenode, (nodenum + 1) * sizeof(hisnode)); + for (i = Nodes[index].cnt; i < nodenum + 1; i++) { + Nodes[index].thenode[i].key = NULL; + Nodes[index].thenode[i].ivalue = 0; + Nodes[index].thenode[i].dvalue = 0.0; + Nodes[index].thenode[i].dynvalue = NULL; + } + Nodes[index].cnt = nodenum + 1; +} + +int LoadVariableData(namedvars varmap, char *filename) { + FILE *data; + char *dataread, buf, *varname, *dynvalue; + double dvalue = 0.0; + int icur = 0, maxbufsize = 10, hasvar = 0, index = -1, idat = 0, ivalue = 0; + dynvalue = NULL; + if ((data = fopen(filename, "r")) == NULL) { + perror("fopen"); + return -1; + } + dataread = (char *) malloc(sizeof(char) * maxbufsize); + while(!feof(data)) { + fread(&buf, 1, 1, data); + if (buf == '\n') { + dataread[icur] = '\0'; + icur = 0; + buf = ' '; + if (dataread[0] == '@') { + if (hasvar) { + for (index = 0; index < varmap.varcnt; index++) { + if (patternmatch(varname, varmap.vars[index])) { + varmap.loaded[index] = 1; + varmap.dvalue[index] = dvalue; + varmap.ivalue[index] = ivalue; + if (varmap.dynvalue[index] != NULL) { + free(varmap.dynvalue[index]); + varmap.dynvalue[index] = NULL; + } + if (dynvalue != NULL) { + varmap.dynvalue[index] = (void *) malloc(sizeof(char) * (strlen(dynvalue) + 1)); + strcpy(varmap.dynvalue[index], dynvalue); + } + } + } + dvalue = 0.0; + ivalue = 0; + if (dynvalue != NULL) { + free(dynvalue); + dynvalue = NULL; + } + free(varname); + } + varname = (char *) malloc(sizeof(char) * strlen(dataread)); + strcpy(varname, dataread + 1); + hasvar = 1; + idat = 0; + } else { + if (hasvar >= 0) { + switch(idat) { + case 0: + if (IsRealNumber(dataread)) dvalue = atof(dataread); + else { + fprintf(stderr, "Error at file: %s. Variable: %s can't have non real value: %s.\n", filename, varname, dataread); + fclose(data); + free(varname); + free(dataread); + return -2; + } + idat++; + break; + case 1: + if (IsNumber(dataread)) ivalue = atoi(dataread); + else { + fprintf(stderr, "Error at file: %s. Variable: %s can't have non integer value: %s.\n", filename, varname, dataread); + fclose(data); + free(varname); + free(dataread); + return -2; + } + idat++; + break; + case 2: + dynvalue = malloc(sizeof(char) * (strlen(dataread) + 1)); + strcpy(dynvalue, dataread); + break; + } + } + } + } else { + dataread[icur] = buf; + icur++; + if (icur == _maxbufsize) { + fprintf(stderr, "Error: Maximum buffer size(%i) exceeded.\n", _maxbufsize); + fclose(data); + free(varname); + free(dataread); + return -2; + } + while (icur > maxbufsize - 1) { + maxbufsize *= 2; + dataread = (char *) realloc(dataread, sizeof(char) * maxbufsize); + } + } + } + if (hasvar) { + for (index = 0; index < varmap.varcnt; index++) { + if (patternmatch(varname, varmap.vars[index])) { + varmap.loaded[index] = 1; + varmap.dvalue[index] = dvalue; + varmap.ivalue[index] = ivalue; + if (dynvalue != NULL) { + varmap.dynvalue[index] = (void *) malloc(sizeof(char) * (strlen(dynvalue) + 1)); + strcpy(varmap.dynvalue[index], dynvalue); + } + } + } + if (dynvalue != NULL) { + free(dynvalue); + dynvalue = NULL; + } + free(varname); + } + fclose(data); + free(dataread); + return 0; +} + +/* Queue for node storing to avoid loops */ + +hisqueue* InitHistory(int varcnt) { + int i; + hisqueue *HisQueue; + HisQueue = (hisqueue *) malloc(sizeof(hisqueue) * varcnt); + for (i = 0; i < varcnt; i++) { + HisQueue[i].thenode = NULL; + HisQueue[i].cnt = 0; + } + return HisQueue; +} + +void ReInitHistory(hisqueue *HisQueue, int varcnt) { + int i, j; + for (i = 0; i < varcnt; i++) { + if (HisQueue[i].thenode != NULL) { + for (j = 0; j < HisQueue[i].cnt; j++) + if (HisQueue[i].thenode[j].dynvalue != NULL) free(HisQueue[i].thenode[j].dynvalue); + free(HisQueue[i].thenode); + HisQueue[i].thenode = NULL; + } + HisQueue[i].cnt = 0; + } +} + +void AddNode(hisqueue *HisQueue, int varstart, DdNode *node, double dvalue, int ivalue, void *dynvalue) { + int index = GetIndex(node) - varstart; + HisQueue[index].thenode = (hisnode *) realloc(HisQueue[index].thenode, (HisQueue[index].cnt + 1) * sizeof(hisnode)); + HisQueue[index].thenode[HisQueue[index].cnt].key = node; + HisQueue[index].thenode[HisQueue[index].cnt].dvalue = dvalue; + HisQueue[index].thenode[HisQueue[index].cnt].ivalue = ivalue; + HisQueue[index].thenode[HisQueue[index].cnt].dynvalue = dynvalue; + HisQueue[index].cnt += 1; +} + +hisnode* GetNode(hisqueue *HisQueue, int varstart, DdNode *node) { + int i; + int index = GetIndex(node) - varstart; + for(i = 0; i < HisQueue[index].cnt; i++) { + if (HisQueue[index].thenode[i].key == node) return &(HisQueue[index].thenode[i]); + } + return NULL; +} + +int GetNodeIndex(hisqueue *HisQueue, int varstart, DdNode *node) { + int i; + int index = GetIndex(node) - varstart; + for(i = 0; i < HisQueue[index].cnt; i++) { + if (HisQueue[index].thenode[i].key == node) return i; + } + return -1; +} + +/* Named variables */ + +namedvars InitNamedVars(int varcnt, int varstart) { + namedvars temp; + int i; + temp.varcnt = varcnt; + temp.varstart = varstart; + temp.vars = (char **) malloc(sizeof(char *) * varcnt); + temp.loaded = (int *) malloc(sizeof(int) * varcnt); + temp.dvalue = (double *) malloc(sizeof(double) * varcnt); + temp.ivalue = (int *) malloc(sizeof(int) * varcnt); + temp.dynvalue = (void **) malloc(sizeof(int) * varcnt); + for (i = 0; i < varcnt; i++) { + temp.vars[i] = NULL; + temp.loaded[i] = 0; + temp.dvalue[i] = 0.0; + temp.ivalue[i] = 0; + temp.dynvalue[i] = NULL; + } + return temp; +} + +void EnlargeNamedVars(namedvars *varmap, int newvarcnt) { + int i; + varmap->vars = (char **) realloc(varmap->vars, sizeof(char *) * newvarcnt); + varmap->loaded = (int *) realloc(varmap->loaded, sizeof(int) * newvarcnt); + varmap->dvalue = (double *) realloc(varmap->dvalue, sizeof(double) * newvarcnt); + varmap->ivalue = (int *) realloc(varmap->ivalue, sizeof(int) * newvarcnt); + varmap->dynvalue = (void **) realloc(varmap->dynvalue, sizeof(int) * newvarcnt); + for (i = varmap->varcnt; i < newvarcnt; i++) { + varmap->vars[i] = NULL; + varmap->loaded[i] = 0; + varmap->dvalue[i] = 0.0; + varmap->ivalue[i] = 0; + varmap->dynvalue[i] = NULL; + } + varmap->varcnt = newvarcnt; +} + +int AddNamedVarAt(namedvars varmap, const char *varname, int index) { + if (varmap.varcnt > index) { + varmap.vars[index] = (char *) malloc(sizeof(char) * (strlen(varname) + 1)); + strcpy(varmap.vars[index], varname); + return index; + } + return -1; +} + +int AddNamedVar(namedvars varmap, const char *varname) { + int index = GetNamedVarIndex(varmap, varname); + if (index == -1 * varmap.varcnt) { + return -1; + } else if ((index < 0) || (index == 0 && varmap.vars[0] == NULL)) { + index *= -1; + varmap.vars[index] = (char *) malloc(sizeof(char) * (strlen(varname) + 1)); + strcpy(varmap.vars[index], varname); + } + return index; +} + +void SetNamedVarValuesAt(namedvars varmap, int index, double dvalue, int ivalue, void *dynvalue) { + varmap.dvalue[index] = dvalue; + varmap.ivalue[index] = ivalue; + varmap.dynvalue[index] = dynvalue; +} + +int SetNamedVarValues(namedvars varmap, const char *varname, double dvalue, int ivalue, void *dynvalue) { + int index = GetNamedVarIndex(varmap, varname); + if (index == -1 * varmap.varcnt) { + return -1; + } else if ((index < 0) || (index == 0 && varmap.vars[0] == NULL)) { + index *= -1; + varmap.vars[index] = (char *) malloc(sizeof(char) * (strlen(varname) + 1)); + strcpy(varmap.vars[index], varname); + varmap.dvalue[index] = dvalue; + varmap.ivalue[index] = ivalue; + varmap.dynvalue[index] = dynvalue; + } else { + varmap.dvalue[index] = dvalue; + varmap.ivalue[index] = ivalue; + varmap.dynvalue[index] = dynvalue; + } + return index; +} + +int GetNamedVarIndex(const namedvars varmap, const char *varname) { + int i; + for (i = 0; i < varmap.varcnt; i++) { + if (varmap.vars[i] == NULL) return -1 * i; + if (strcmp(varmap.vars[i], varname) == 0) return i; + } + return -1 * varmap.varcnt; +} + +char* GetNodeVarName(DdManager *manager, namedvars varmap, DdNode *node) { + if (node == NULL) return NULL; + if (node == HIGH(manager)) return "true"; + if (node == LOW(manager)) return "false"; + return varmap.vars[GetIndex(node) - varmap.varstart]; +} + +char* GetNodeVarNameDisp(DdManager *manager, namedvars varmap, DdNode *node) { + if (HIGH(manager) == node) return "TRUE"; + if (LOW(manager) == node) return "FALSE"; + if (NULL == node) return "(null)"; + return varmap.vars[GetIndex(node) - varmap.varstart]; +} + +int RepairVarcnt(namedvars *varmap) { + while (varmap->vars[varmap->varcnt - 1] == NULL) + varmap->varcnt--; + return varmap->varcnt; +} + +int all_loaded(namedvars varmap, int disp) { + int i, res = 1; + for (i = 0; i < varmap.varcnt; i++) { + if (varmap.loaded[i] == 0) { + res = 0; + if (disp) fprintf(stderr, "The variable: %s was not loaded with values.\n", varmap.vars[i]); else return 0; + } + } + return res; +} + +/* Parser */ + +DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader fileheader) { + int icomment, maxlinesize, icur, iline, curinter, iequal; + DdNode *Line, **inter; + char buf, *inputline, *filename; + bddfileheader interfileheader; + // Initialization of intermediate steps + inter = (DdNode **) malloc(sizeof(DdNode *) * fileheader.intercnt); + for (icur = 0; icur < fileheader.intercnt; icur++) inter[icur] = NULL; + // Read file data + interfileheader.inputfile = NULL; + filename = NULL; // For nested files + iequal = 0; // Flag for encountered = sign + icur = 0; // Pointer for inputline buffer location + iline = 5; // Current file line (first after header) + icomment = 0; // Flag for comments + maxlinesize = 80; // inputline starting buffer size + inputline = (char *) malloc(sizeof(char) * maxlinesize); + while(!feof(fileheader.inputfile)) { + fread(&buf, 1, 1, fileheader.inputfile); + if (buf == ';' || buf == '%' || buf == '$') icomment = 1; + if (buf == '\n') { + if (icomment) icomment = 0; + if (iequal > 1) { + fprintf(stderr, "Error at line: %i. Line contains more than 1 equal(=) signs.\n", iline); + fclose(fileheader.inputfile); + free(inter); + free(inputline); + return NULL; + } else iequal = 0; + if (icur > 0) { + inputline[icur] = '\0'; + if (inputline[0] != 'L') { + fprintf(stderr, "Error at line: %i. Intermediate results should start with L.\n", iline); + fclose(fileheader.inputfile); + free(inter); + free(inputline); + return NULL; + } + curinter = getInterBDD(inputline); + if (curinter == -1) { + if (inputline[0] == 'L' && IsPosNumber(inputline + 1)) { + curinter = atoi(inputline + 1) - 1; + if (curinter > -1 && curinter < fileheader.intercnt && inter[curinter] != NULL) { + if (_debug) fprintf(stderr, "Returned: %s\n", inputline); + fclose(fileheader.inputfile); + Line = inter[curinter]; + free(inter); + free(inputline); + return Line; + } else { + fprintf(stderr, "Error at line: %i. Return result asked doesn't exist.\n", iline); + fclose(fileheader.inputfile); + free(inter); + free(inputline); + return NULL; + } + } else { + fprintf(stderr, "Error at line: %i. Invalid intermediate result format.\n", iline); + fclose(fileheader.inputfile); + free(inter); + free(inputline); + return NULL; + } + } else if (curinter > -1 && curinter < fileheader.intercnt && inter[curinter] == NULL) { + if (_debug) fprintf(stderr, "%i %s\n", curinter, inputline); + filename = getFileName(inputline); + if (filename == NULL) { + Line = LineParser(manager, varmap, inter, fileheader.intercnt, inputline, iline); + } else { + interfileheader = ReadFileHeader(filename); + if (interfileheader.inputfile == NULL) { + //Line = simpleBDDload(manager, &varmap, filename); + Line = NULL; + } else { + Line = FileGenerateBDD(manager, varmap, interfileheader); + } + if (Line == NULL) fprintf(stderr, "Error at line: %i. Error in nested BDD file: %s.\n", iline, filename); + free(filename); + filename = NULL; + interfileheader.inputfile = NULL; + } + if (Line == NULL) { + fclose(fileheader.inputfile); + free(inter); + free(inputline); + return NULL; + } + inter[curinter] = Line; + icur = 0; + } else if (curinter > -1 && curinter < fileheader.intercnt && inter[curinter] != NULL) { + fprintf(stderr, "Error at line: %i. Intermediate results can't be overwritten.\n", iline); + fclose(fileheader.inputfile); + free(inter); + free(inputline); + return NULL; + } else { + fprintf(stderr, "Error at line: %i. Intermediate result asked doesn't exist.\n", iline); + fclose(fileheader.inputfile); + free(inter); + free(inputline); + return NULL; + } + } + iline++; + } else if (buf != ' ' && buf != '\t' && !icomment) { + if (buf == '=') iequal++; + inputline[icur] = buf; + icur += 1; + if (icur == _maxbufsize) { + fprintf(stderr, "Error: Maximum buffer size(%i) exceeded.\n", _maxbufsize); + fclose(fileheader.inputfile); + free(inter); + free(inputline); + return NULL; + } + while (icur > maxlinesize - 1) { + maxlinesize *= 2; + inputline = (char *) realloc(inputline, sizeof(char) * maxlinesize); + } + } + } + fprintf(stderr, "Error, file either doesn't end with a blank line or no return result was asked.\n"); + fclose(fileheader.inputfile); + free(inter); + free(inputline); + return NULL; +} + +int getInterBDD(char *function) { + int i, ret; + char *inter; + for (i = 0; i < strlen(function); i++) { + if (function[i] == '=') { + inter = (char *) malloc(sizeof(char) * i); + strncpy(inter, function + 1, i - 1); + inter[i - 1] = '\0'; + if (IsPosNumber(inter)) { + ret = atoi(inter) - 1; + free(inter); + return ret; + } else { + free(inter); + return -1; + } + } + } + return -1; +} + +char* getFileName(const char *function) { + int i = 0; + char *filename; + while(function[i] != '=' && (i + 1) < strlen(function)) i++; + if ((i + 1) < strlen(function)) { + i++; + if (function[i] == '<' && function[strlen(function) - 1] == '>') { + filename = (char *) malloc(sizeof(char) * strlen(function) - i); + strcpy(filename, function + i + 1); + filename[strlen(function) - i - 2] = '\0'; + return filename; + } + } + return NULL; +} + +DdNode* LineParser(DdManager *manager, namedvars varmap, DdNode **inter, int maxinter, char *function, int iline) { + int istart, iend, ilength, i, symbol, ivar, inegvar, inegoper, iconst; + long startAt, endAt; + double secs; + DdNode *bdd; + char *term, curoper; + bdd = HIGH(manager); + Cudd_Ref(bdd); + term = NULL; + ivar = -1; + curoper = '*'; + istart = -1; + iend = strlen(function) - 1; + ilength = -1; + symbol = -1; + inegvar = 0; + inegoper = 0; + iconst = 0; + for (i = strlen(function) - 1; i > -1; i--) { + if (symbol == -1 && isOperator(function[i])) { + symbol = i; + istart = i + 1; + ilength = iend - i; + iend = i - 1; + if (ilength > 0 && !(ilength == 1 && function[istart] == '~')) { + term = (char *) malloc(sizeof(char) * (ilength + 1)); + strncpy(term, function + istart, ilength); + term[ilength] = '\0'; + } else { + fprintf(stderr, "Line Parser Error at line: %i. An operator was encounter with no term at its right side.\n", iline); + free(term); + return NULL; + } + } + if (symbol != -1) { + if (term[0] == '~') inegvar = 1; else inegvar = 0; + if (term[0 + inegvar] != 'L') { + // Term is a variable + if (strcmp(term + inegvar, "TRUE") == 0) { + iconst = 1; + } else if (strcmp(term + inegvar, "FALSE") == 0) { + iconst = 1; + inegvar = 1; + } else { + iconst = 0; + ivar = AddNamedVar(varmap, term + inegvar); + if (ivar == -1) { + fprintf(stderr, "Line Parser Error at line: %i. More BDD variables than the reserved term: %s.\n", iline, term); + free(term); + return NULL; + } + } + if (_debug) fprintf(stderr, "%s\n", term); + if (_debug && !iconst) fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", + Cudd_CountPathsToNonZero(bdd), + Cudd_CountPath(bdd), + Cudd_DagSize(bdd), + Cudd_CountPathsToNonZero(GetVar(manager, ivar + varmap.varstart)), + Cudd_CountPath(GetVar(manager, ivar + varmap.varstart)), + Cudd_DagSize(GetVar(manager, ivar + varmap.varstart)) ); + startAt = clock(); + if (!iconst) { + if (inegvar) bdd = BDD_Operator(manager, NOT(GetVar(manager, ivar + varmap.varstart)), bdd, curoper, inegoper); + else bdd = BDD_Operator(manager, GetVar(manager, ivar + varmap.varstart), bdd, curoper, inegoper); + } else { + switch(curoper) { + case '+': + if (inegvar ^ inegoper) ; else { + bdd = HIGH(manager); + Cudd_Ref(bdd); + } + break; + case '*': + if (inegvar ^ inegoper) { + bdd = LOW(manager); + Cudd_Ref(bdd); + } + break; + case '#': + if (inegvar ^ inegoper) ; else bdd = NOT(bdd); + break; + } + } + endAt = clock(); + secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC); + if (_debug) fprintf(stderr, "term: %s of line: %i took: %i\n", term, iline, endAt - startAt); + //if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); + if (bdd == NULL) { + fprintf(stderr, "Line Parser Error at line: %i. Error using operator %c on term: %s.\n", iline, curoper, term); + free(term); + return NULL; + } + } else { + // Term is an intermediate result + if (IsPosNumber(term + inegvar + 1)) ivar = atoi(term + inegvar + 1) - 1; else { + fprintf(stderr, "Line Parser Error at line: %i. Invalid intermediate result format term: %s.\n", iline, term); + free(term); + return NULL; + } + if (ivar < 0 || ivar > maxinter || inter[ivar] == NULL) { + fprintf(stderr, "Line Parser Error at line: %i. Usage of undeclared intermediate result term: %s.\n", iline, term); + free(term); + return NULL; + } + if (_debug) fprintf(stderr, "%s\n", term); + if (_debug) fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", + Cudd_CountPathsToNonZero(bdd), + Cudd_CountPath(bdd), + Cudd_DagSize(bdd), + Cudd_CountPathsToNonZero(inter[ivar]), + Cudd_CountPath(inter[ivar]), + Cudd_DagSize(inter[ivar]) ); + startAt = clock(); + if (inegvar) bdd = BDD_Operator(manager, NOT(inter[ivar]), bdd, curoper, inegoper); + else bdd = BDD_Operator(manager, inter[ivar], bdd, curoper, inegoper); + endAt = clock(); + secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC); + if (_debug) fprintf(stderr, "term: %s of line: %i took: %i\n", term, iline, endAt - startAt); + //if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); + if (bdd == NULL) { + fprintf(stderr, "Line Parser Error at line: %i. Error using operator %c on term: %s.\n", iline, curoper, term); + free(term); + return NULL; + } + } + free(term); + term = NULL; + curoper = function[symbol]; + if (curoper == '=') return bdd; + if (function[symbol - 1] == '~') { + inegoper = 1; + i--; + iend--; + } else { + inegoper = 0; + } + symbol = -1; + } + } + return NULL; +} + +DdNode* BDD_Operator(DdManager *manager, DdNode *bdd1, DdNode *bdd2, char Operator, int inegoper) { + switch (Operator) { + case '+': + if (inegoper) return D_BDDNor(manager, bdd1, bdd2); + else return D_BDDOr(manager, bdd1, bdd2); + break; + case '*': + if (inegoper) return D_BDDNand(manager, bdd1, bdd2); + else return D_BDDAnd(manager, bdd1, bdd2); + break; + case '#': + if (inegoper) return D_BDDXnor(manager, bdd1, bdd2); + else return D_BDDXor(manager, bdd1, bdd2); + break; + default: + return NULL; + break; + } +} + +DdNode* OnlineGenerateBDD(DdManager *manager, namedvars *varmap) { + int icomment, maxlinesize, icur, iline, curinter, iequal, iinters, itmp, i; + DdNode *Line, **inter; + char buf, *inputline, *filename; + bddfileheader interfileheader; + // Initialization of intermediate steps + iinters = 1; + inter = (DdNode **) malloc(sizeof(DdNode *) * iinters); + for (icur = 0; icur < iinters; icur++) inter[icur] = NULL; + // Read file data + interfileheader.inputfile = NULL; + filename = NULL; // For nested files + iequal = 0; // Flag for encountered = sign + icur = 0; // Pointer for inputline buffer location + iline = 1; // Current file line (first after header) + icomment = 0; // Flag for comments + maxlinesize = 80; // inputline starting buffer size + inputline = (char *) malloc(sizeof(char) * maxlinesize); + + do { + buf = fgetc(stdin); + if (buf == ';' || buf == '%' || buf == '$') icomment = 1; + if (buf == '\n') { + if (icomment) icomment = 0; + if (iequal > 1) { + fprintf(stderr, "Error at line: %i. Line contains more than 1 equal(=) signs.\n", iline); + free(inter); + free(inputline); + return NULL; + } else iequal = 0; + if (icur > 0) { + inputline[icur] = '\0'; + if (inputline[0] == '@') { + if (inputline[1] == 'e') { + free(inter); + free(inputline); + exit(0); + } else { + itmp = GetParam(inputline, 1); + if (itmp > varmap->varcnt) + EnlargeNamedVars(varmap, itmp); + itmp = GetParam(inputline, 2); + if (itmp > iinters) { + inter = (DdNode **) realloc(inter, sizeof(DdNode *) * itmp); + for (i = iinters; i < itmp; i++) inter[i] = NULL; + iinters = itmp; + } + } + icur = 0; + } else { + if (inputline[0] != 'L') { + fprintf(stderr, "Error at line: %i. Intermediate results should start with L.\n", iline); + free(inter); + free(inputline); + return NULL; + } + curinter = getInterBDD(inputline); + if (curinter == -1) { + if (inputline[0] == 'L' && IsPosNumber(inputline + 1)) { + curinter = atoi(inputline + 1) - 1; + if (curinter > -1 && curinter < iinters && inter[curinter] != NULL) { + if (_debug) fprintf(stderr, "Returned: %s\n", inputline); + Line = inter[curinter]; + free(inter); + free(inputline); + return Line; + } else { + fprintf(stderr, "Error at line: %i. Return result asked doesn't exist.\n", iline); + free(inter); + free(inputline); + return NULL; + } + } else { + fprintf(stderr, "Error at line: %i. Invalid intermediate result format.\n", iline); + free(inter); + free(inputline); + return NULL; + } + } else if (curinter > -1) { + if (curinter >= iinters) { + inter = (DdNode **) realloc(inter, sizeof(DdNode *) * (curinter + 1)); + for (i = iinters; i < curinter + 1; i++) inter[i] = NULL; + iinters = curinter + 1; + } + if (inter[curinter] == NULL) { + if (_debug) fprintf(stderr, "%i %s\n", curinter, inputline); + filename = getFileName(inputline); + if (filename == NULL) { + Line = OnlineLineParser(manager, varmap, inter, iinters, inputline, iline); + } else { + interfileheader = ReadFileHeader(filename); + if (interfileheader.inputfile == NULL) { + //Line = simpleBDDload(manager, varmap, filename); + Line = NULL; + } else { + Line = FileGenerateBDD(manager, *varmap, interfileheader); + } + if (Line == NULL) fprintf(stderr, "Error at line: %i. Error in nested BDD file: %s.\n", iline, filename); + free(filename); + filename = NULL; + interfileheader.inputfile = NULL; + } + if (Line == NULL) { + free(inter); + free(inputline); + return NULL; + } + inter[curinter] = Line; + icur = 0; + } else if (inter[curinter] != NULL) { + fprintf(stderr, "Error at line: %i. Intermediate results can't be overwritten.\n", iline); + free(inter); + free(inputline); + return NULL; + } + } else { + fprintf(stderr, "Error at line: %i. Intermediate result asked doesn't exist.\n", iline); + free(inter); + free(inputline); + return NULL; + } + } + } + iline++; + } else if (buf != ' ' && buf != '\t' && !icomment) { + if (buf == '=') iequal++; + inputline[icur] = buf; + icur += 1; + if (icur == _maxbufsize) { + fprintf(stderr, "Error: Maximum buffer size(%i) exceeded.\n", _maxbufsize); + free(inter); + free(inputline); + return NULL; + } + while (icur > maxlinesize - 1) { + maxlinesize *= 2; + inputline = (char *) realloc(inputline, sizeof(char) * maxlinesize); + } + } + } while(1); + fprintf(stderr, "Error, file either doesn't end with a blank line or no return result was asked.\n"); + free(inter); + free(inputline); + return NULL; +} + +DdNode* OnlineLineParser(DdManager *manager, namedvars *varmap, DdNode **inter, int maxinter, char *function, int iline) { + int istart, iend, ilength, i, symbol, ivar, inegvar, inegoper, iconst; + long startAt, endAt; + double secs; + DdNode *bdd; + char *term, curoper; + bdd = HIGH(manager); + Cudd_Ref(bdd); + term = NULL; + ivar = -1; + curoper = '*'; + istart = -1; + iend = strlen(function) - 1; + ilength = -1; + symbol = -1; + inegvar = 0; + inegoper = 0; + iconst = 0; + for (i = strlen(function) - 1; i > -1; i--) { + if (symbol == -1 && isOperator(function[i])) { + symbol = i; + istart = i + 1; + ilength = iend - i; + iend = i - 1; + if (ilength > 0 && !(ilength == 1 && function[istart] == '~')) { + term = (char *) malloc(sizeof(char) * (ilength + 1)); + strncpy(term, function + istart, ilength); + term[ilength] = '\0'; + } else { + fprintf(stderr, "Line Parser Error at line: %i. An operator was encounter with no term at its right side.\n", iline); + free(term); + return NULL; + } + } + if (symbol != -1) { + if (term[0] == '~') inegvar = 1; else inegvar = 0; + if (term[0 + inegvar] != 'L') { + // Term is a variable + if (strcmp(term + inegvar, "TRUE") == 0) { + iconst = 1; + } else if (strcmp(term + inegvar, "FALSE") == 0) { + iconst = 1; + inegvar = 1; + } else { + iconst = 0; + ivar = AddNamedVar(*varmap, term + inegvar); + if (ivar == -1) { + EnlargeNamedVars(varmap, varmap->varcnt + 1); + ivar = AddNamedVar(*varmap, term + inegvar); + } + if (ivar == -1) { + fprintf(stderr, "Line Parser Error at line: %i. More BDD variables than the reserved term: %s.\n", iline, term); + free(term); + return NULL; + } + } + if (_debug) fprintf(stderr, "%s\n", term); + if (_debug && !iconst) fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", + Cudd_CountPathsToNonZero(bdd), + Cudd_CountPath(bdd), + Cudd_DagSize(bdd), + Cudd_CountPathsToNonZero(GetVar(manager, ivar + varmap->varstart)), + Cudd_CountPath(GetVar(manager, ivar + varmap->varstart)), + Cudd_DagSize(GetVar(manager, ivar + varmap->varstart)) ); + startAt = clock(); + if (!iconst) { + if (inegvar) bdd = BDD_Operator(manager, NOT(GetVar(manager, ivar + varmap->varstart)), bdd, curoper, inegoper); + else bdd = BDD_Operator(manager, GetVar(manager, ivar + varmap->varstart), bdd, curoper, inegoper); + } else { + switch(curoper) { + case '+': + if (inegvar ^ inegoper) ; else { + bdd = HIGH(manager); + Cudd_Ref(bdd); + } + break; + case '*': + if (inegvar ^ inegoper) { + bdd = LOW(manager); + Cudd_Ref(bdd); + } + break; + case '#': + if (inegvar ^ inegoper) ; else bdd = NOT(bdd); + break; + } + } + endAt = clock(); + secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC); + if (_debug) fprintf(stderr, "term: %s of line: %i took: %i\n", term, iline, endAt - startAt); + //if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); + if (bdd == NULL) { + fprintf(stderr, "Line Parser Error at line: %i. Error using operator %c on term: %s.\n", iline, curoper, term); + free(term); + return NULL; + } + } else { + // Term is an intermediate result + if (IsPosNumber(term + inegvar + 1)) ivar = atoi(term + inegvar + 1) - 1; else { + fprintf(stderr, "Line Parser Error at line: %i. Invalid intermediate result format term: %s.\n", iline, term); + free(term); + return NULL; + } + if (ivar < 0 || ivar > maxinter || inter[ivar] == NULL) { + fprintf(stderr, "Line Parser Error at line: %i. Usage of undeclared intermediate result term: %s.\n", iline, term); + free(term); + return NULL; + } + if (_debug) fprintf(stderr, "%s\n", term); + if (_debug) fprintf(stderr, "PNZ1:%.0f P1:%.0f S1:%i PNZ2:%.0f P2:%.0f S2:%i\n", + Cudd_CountPathsToNonZero(bdd), + Cudd_CountPath(bdd), + Cudd_DagSize(bdd), + Cudd_CountPathsToNonZero(inter[ivar]), + Cudd_CountPath(inter[ivar]), + Cudd_DagSize(inter[ivar]) ); + startAt = clock(); + if (inegvar) bdd = BDD_Operator(manager, NOT(inter[ivar]), bdd, curoper, inegoper); + else bdd = BDD_Operator(manager, inter[ivar], bdd, curoper, inegoper); + endAt = clock(); + secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC); + if (_debug) fprintf(stderr, "term: %s of line: %i took: %i\n", term, iline, endAt - startAt); + //if ((endAt - startAt) > 10000000) Cudd_AutodynDisable(manager); + if (bdd == NULL) { + fprintf(stderr, "Line Parser Error at line: %i. Error using operator %c on term: %s.\n", iline, curoper, term); + free(term); + return NULL; + } + } + free(term); + term = NULL; + curoper = function[symbol]; + if (curoper == '=') return bdd; + if (function[symbol - 1] == '~') { + inegoper = 1; + i--; + iend--; + } else { + inegoper = 0; + } + symbol = -1; + } + } + return NULL; +} + +int GetParam(char *inputline, int iParam) { + int icoma, istart, iend, ret; + char *numb; + istart = 1; + icoma = istart; + iend = strlen(inputline); + while((inputline[icoma] != ',') && (icoma < iend)) + icoma++; + if (iParam == 1) { + numb = (char *) malloc(sizeof(char) * icoma); + strncpy(numb, inputline + 1, icoma - 1); + numb[icoma - 1] = '\0'; + if (IsPosNumber(numb)) { + ret = atoi(numb); + free(numb); + return ret; + } + } else if(iParam == 2) { + numb = (char *) malloc(sizeof(char) * (iend - icoma + 1)); + strncpy(numb, inputline + icoma + 1, iend - icoma); + numb[iend - icoma] = '\0'; + if (IsPosNumber(numb)) { + ret = atoi(numb); + free(numb); + return ret; + } + } + return 0; +} + +void onlinetraverse(DdManager *manager, namedvars varmap, hisqueue *HisQueue, DdNode *bdd) { + char buf, *inputline; + int icur, maxlinesize, iline, index, iloop, ivalue, iQsize, i, inQ; + double dvalue; + DdNode **Q, **Q2, *h_node, *l_node, *curnode; + hisqueue *his; + hisnode *hnode; + iloop = 1; + icur = 0; // Pointer for inputline buffer location + iline = 1; // Current file line (first after header) + maxlinesize = 80; // inputline starting buffer size + inputline = (char *) malloc(sizeof(char) * maxlinesize); + curnode = bdd; + iQsize = 0; + Q = (DdNode **) malloc(sizeof(DdNode *) * iQsize); + Q2 = NULL; + his = InitHistory(varmap.varcnt); + do { + buf = fgetc(stdin); + if (buf == '\n') { + inputline[icur] = '\0'; + if ((icur > 0) && (inputline[0] == '@') && (inputline[2] == ',' || inputline[2] == '\0')) { + switch(inputline[1]) { + case 'c': + printf("bdd_temp_value('%s', %i).\n", GetNodeVarNameDisp(manager, varmap, curnode), iQsize); + break; + case 'n': + if (curnode != HIGH(manager) && curnode != LOW(manager) && (hnode = GetNode(his, varmap.varstart, curnode)) == NULL) { + AddNode(his, varmap.varstart, curnode, 0.0, 0, NULL); + l_node = LowNodeOf(manager, curnode); + h_node = HighNodeOf(manager, curnode); + inQ = 0; + for(i = 0; (i < iQsize / 2) && (inQ < 3); i++) + inQ = (Q[i] == l_node) || (Q[iQsize - i] == l_node) + 2 * (Q[i] == h_node) || (Q[iQsize - i] == h_node); + if (inQ & 1 == 0) inQ = inQ + (GetNode(his, varmap.varstart, l_node) != NULL); + if (inQ & 2 == 0) inQ = inQ + 2 * (GetNode(his, varmap.varstart, h_node) != NULL); + if (inQ & 1 == 1) inQ = inQ - (l_node == HIGH(manager) || l_node == LOW(manager)); + if (inQ & 2 == 2) inQ = inQ - 2 * (h_node == HIGH(manager) || h_node == LOW(manager)); + switch(inQ) { + case 0: + iQsize += 2; + Q = (DdNode **) realloc(Q, sizeof(DdNode *) * iQsize); + Q[iQsize - 2] = l_node; + Q[iQsize - 1] = h_node; + break; + case 1: + iQsize++; + Q = (DdNode **) realloc(Q, sizeof(DdNode *) * iQsize); + Q[iQsize - 1] = h_node; + break; + case 2: + iQsize++; + Q = (DdNode **) realloc(Q, sizeof(DdNode *) * iQsize); + Q[iQsize - 1] = l_node; + break; + case 3: + break; + default: + break; + } + } + if (inputline[2] == '\0' || strcmp(inputline + 3, "DFS") == 0) { + if (iQsize > 0) { + iQsize--; + curnode = Q[iQsize]; + Q = (DdNode **) realloc(Q, sizeof(DdNode *) * iQsize); + } + } else if (strcmp(inputline + 3, "BFS") == 0) { + if (iQsize > 0) { + iQsize--; + curnode = Q[0]; + Q2 = (DdNode **) malloc(sizeof(DdNode *) * iQsize); + for(i = 0; i < iQsize; i++) + Q2[i] = Q[i + 1]; + free(Q); + Q = Q2; + } + } else { + fprintf(stderr, "Error: Could not find method: %s, Correct syntax @n,[DFS, BFS].\n", inputline + 3); + free(Q); + free(inputline); + exit(-1); + } + break; + case 'h': + printf("bdd_temp_value('%s').\n", GetNodeVarNameDisp(manager, varmap, HighNodeOf(manager, curnode))); + break; + case 'l': + printf("bdd_temp_value('%s').\n", GetNodeVarNameDisp(manager, varmap, LowNodeOf(manager, curnode))); + break; + case 'v': + index = GetNamedVarIndex(varmap, inputline + 3); + if (index >= 0) { + fprintf(stdout, "bdd_temp_value([%f,%i,%s]).\n", varmap.dvalue[index], varmap.ivalue[index], (char *) varmap.dynvalue[index]); + } else { + fprintf(stderr, "Error: Could not find variable: %s, Correct syntax @v,[variable name].\n", inputline + 3); + free(Q); + free(inputline); + exit(-1); + } + break; + case 'e': + iloop = 0; + break; + default: + fprintf(stderr, "Error: Not recognizable instruction: %s.\n", inputline); + free(Q); + free(inputline); + exit(-1); + break; + } + icur = 0; + } else { + fprintf(stderr, "Error: Not recognizable instruction: %s.\n", inputline); + free(Q); + free(inputline); + exit(-1); + } + iline++; + } else if (buf != ' ' && buf != '\t') { + inputline[icur] = buf; + icur += 1; + if (icur == _maxbufsize) { + fprintf(stderr, "Error: Maximum buffer size(%i) exceeded.\n", _maxbufsize); + free(Q); + free(inputline); + exit(-1); + } + while (icur > maxlinesize - 1) { + maxlinesize *= 2; + inputline = (char *) realloc(inputline, sizeof(char) * maxlinesize); + } + } + } while(iloop); + free(Q); + free(inputline); +} diff --git a/packages/ProbLog/simplecudd/simplecudd.h b/packages/ProbLog/simplecudd/simplecudd.h new file mode 100644 index 000000000..49ed3a5aa --- /dev/null +++ b/packages/ProbLog/simplecudd/simplecudd.h @@ -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 +#include +#include +#include +#include +#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); +