diogo/yap-6.3
Archived
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
Files
30af67b3ca3a43dfe427cf95b932fdc20e03de51
yap-6.3/packages/ProbLog/simplecudd_lfi/simplecudd.c

1867 lines
74 KiB
C
Raw Normal View History

update to recent ProbLog.
2011-06-26 23:13:43 +01:00
/******************************************************************************\
* *
* SimpleCUDD library (www.cs.kuleuven.be/~theo/tools/simplecudd.html) *
* SimpleCUDD was developed at Katholieke Universiteit Leuven(www.kuleuven.be) *
* *
* Copyright Katholieke Universiteit Leuven 2008 *
* *
* Author: Theofrastos Mantadelis, Bernd Gutmann *
* File: simplecudd.c *
* *
********************************************************************************
* *
* Artistic License 2.0 *
* *
* Copyright (c) 2000-2006, The Perl Foundation. *
* *
* Everyone is permitted to copy and distribute verbatim copies of this license *
* document, but changing it is not allowed. *
* *
* Preamble *
* *
* This license establishes the terms under which a given free software Package *
* may be copied, modified, distributed, and/or redistributed. The intent is *
* that the Copyright Holder maintains some artistic control over the *
* development of that Package while still keeping the Package available as *
* open source and free software. *
* *
* You are always permitted to make arrangements wholly outside of this license *
* directly with the Copyright Holder of a given Package. If the terms of this *
* license do not permit the full use that you propose to make of the Package, *
* you should contact the Copyright Holder and seek a different licensing *
* arrangement. *
* Definitions *
* *
* "Copyright Holder" means the individual(s) or organization(s) named in the *
* copyright notice for the entire Package. *
* *
* "Contributor" means any party that has contributed code or other material to *
* the Package, in accordance with the Copyright Holder's procedures. *
* *
* "You" and "your" means any person who would like to copy, distribute, or *
* modify the Package. *
* *
* "Package" means the collection of files distributed by the Copyright Holder, *
* and derivatives of that collection and/or of those files. A given Package *
* may consist of either the Standard Version, or a Modified Version. *
* *
* "Distribute" means providing a copy of the Package or making it accessible *
* to anyone else, or in the case of a company or organization, to others *
* outside of your company or organization. *
* *
* "Distributor Fee" means any fee that you charge for Distributing this *
* Package or providing support for this Package to another party. It does not *
* mean licensing fees. *
* *
* "Standard Version" refers to the Package if it has not been modified, or has *
* been modified only in ways explicitly requested by the Copyright Holder. *
* *
* "Modified Version" means the Package, if it has been changed, and such *
* changes were not explicitly requested by the Copyright Holder. *
* *
* "Original License" means this Artistic License as Distributed with the *
* Standard Version of the Package, in its current version or as it may be *
* modified by The Perl Foundation in the future. *
* *
* "Source" form means the source code, documentation source, and configuration *
* files for the Package. *
* *
* "Compiled" form means the compiled bytecode, object code, binary, or any *
* other form resulting from mechanical transformation or translation of the *
* Source form. *
* Permission for Use and Modification Without Distribution *
* *
* (1) You are permitted to use the Standard Version and create and use *
* Modified Versions for any purpose without restriction, provided that you do *
* not Distribute the Modified Version. *
* Permissions for Redistribution of the Standard Version *
* *
* (2) You may Distribute verbatim copies of the Source form of the Standard *
* Version of this Package in any medium without restriction, either gratis or *
* for a Distributor Fee, provided that you duplicate all of the original *
* copyright notices and associated disclaimers. At your discretion, such *
* verbatim copies may or may not include a Compiled form of the Package. *
* *
* (3) You may apply any bug fixes, portability changes, and other *
* modifications made available from the Copyright Holder. The resulting *
* Package will still be considered the Standard Version, and as such will be *
* subject to the Original License. *
* Distribution of Modified Versions of the Package as Source *
* *
* (4) You may Distribute your Modified Version as Source (either gratis or for *
* a Distributor Fee, and with or without a Compiled form of the Modified *
* Version) provided that you clearly document how it differs from the Standard *
* Version, including, but not limited to, documenting any non-standard *
* features, executables, or modules, and provided that you do at least ONE of *
* the following: *
* *
* (a) make the Modified Version available to the Copyright Holder of the *
* Standard Version, under the Original License, so that the Copyright Holder *
* may include your modifications in the Standard Version. *
* (b) ensure that installation of your Modified Version does not prevent the *
* user installing or running the Standard Version. In addition, the Modified *
* Version must bear a name that is different from the name of the Standard *
* Version. *
* (c) allow anyone who receives a copy of the Modified Version to make the *
* Source form of the Modified Version available to others under *
* (i) the Original License or *
* (ii) a license that permits the licensee to freely copy, modify and *
* redistribute the Modified Version using the same licensing terms that apply *
* to the copy that the licensee received, and requires that the Source form of *
* the Modified Version, and of any works derived from it, be made freely *
* available in that license fees are prohibited but Distributor Fees are *
* allowed. *
* Distribution of Compiled Forms of the Standard Version or Modified Versions *
* without the Source *
* *
* (5) You may Distribute Compiled forms of the Standard Version without the *
* Source, provided that you include complete instructions on how to get the *
* Source of the Standard Version. Such instructions must be valid at the time *
* of your distribution. If these instructions, at any time while you are *
* carrying out such distribution, become invalid, you must provide new *
* instructions on demand or cease further distribution. If you provide valid *
* instructions or cease distribution within thirty days after you become aware *
* that the instructions are invalid, then you do not forfeit any of your *
* rights under this license. *
* *
* (6) You may Distribute a Modified Version in Compiled form without the *
* Source, provided that you comply with Section 4 with respect to the Source *
* of the Modified Version. *
* Aggregating or Linking the Package *
* *
* (7) You may aggregate the Package (either the Standard Version or Modified *
* Version) with other packages and Distribute the resulting aggregation *
* provided that you do not charge a licensing fee for the Package. Distributor *
* Fees are permitted, and licensing fees for other components in the *
* aggregation are permitted. The terms of this license apply to the use and *
* Distribution of the Standard or Modified Versions as included in the *
* aggregation. *
* *
* (8) You are permitted to link Modified and Standard Versions with other *
* works, to embed the Package in a larger work of your own, or to build *
* stand-alone binary or bytecode versions of applications that include the *
* Package, and Distribute the result without restriction, provided the result *
* does not expose a direct interface to the Package. *
* Items That are Not Considered Part of a Modified Version *
* *
* (9) Works (including, but not limited to, modules and scripts) that merely *
* extend or make use of the Package, do not, by themselves, cause the Package *
* to be a Modified Version. In addition, such works are not considered parts *
* of the Package itself, and are not subject to the terms of this license. *
* General Provisions *
* *
* (10) Any use, modification, and distribution of the Standard or Modified *
* Versions is governed by this Artistic License. By using, modifying or *
* distributing the Package, you accept this license. Do not use, modify, or *
* distribute the Package, if you do not accept this license. *
* *
* (11) If your Modified Version has been derived from a Modified Version made *
* by someone other than you, you are nevertheless required to ensure that your *
* Modified Version complies with the requirements of this license. *
* *
* (12) This license does not grant you the right to use any trademark, service *
* mark, tradename, or logo of the Copyright Holder. *
* *
* (13) This license includes the non-exclusive, worldwide, free-of-charge *
* patent license to make, have made, use, offer to sell, sell, import and *
* otherwise transfer the Package with respect to any patent claims licensable *
* by the Copyright Holder that are necessarily infringed by the Package. If *
* you institute patent litigation (including a cross-claim or counterclaim) *
* against any party alleging that the Package constitutes direct or *
* contributory patent infringement, then this Artistic License to you shall *
* terminate on the date that such litigation is filed. *
* *
* (14) Disclaimer of Warranty: THE PACKAGE IS PROVIDED BY THE COPYRIGHT HOLDER *
* AND CONTRIBUTORS "AS IS' AND WITHOUT ANY EXPRESS OR IMPLIED WARRANTIES. THE *
* IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, OR *
* NON-INFRINGEMENT ARE DISCLAIMED TO THE EXTENT PERMITTED BY YOUR LOCAL LAW. *
* UNLESS REQUIRED BY LAW, NO COPYRIGHT HOLDER OR CONTRIBUTOR WILL BE LIABLE *
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING IN *
* ANY WAY OUT OF THE USE OF THE PACKAGE, EVEN IF ADVISED OF THE POSSIBILITY OF *
* SUCH DAMAGE. *
* *
* The End *
* *
\******************************************************************************/
#include <stdlib.h>
#include <errno.h>
#include "simplecudd.h"
fix current and system predicate
2014-11-25 12:03:48 +00:00
int my_index_calc(int varstart, DdNode *node);
int all_loaded_for_deterministic_variables(namedvars varmap, int disp);
update to recent ProbLog.
2011-06-26 23:13:43 +01:00
/* BDD manager initialization */
int _debug = 0;
int _RapidLoad = 0;
int _maxbufsize = 0;
DdManager* simpleBDDinit(int varcnt) {
DdManager *temp;
// fprintf(stderr,"varcnt is %i \n",varcnt);
temp = Cudd_Init(varcnt, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
Cudd_AutodynEnable(temp, CUDD_REORDER_GROUP_SIFT);
//Cudd_AutodynEnable(temp, CUDD_REORDER_RANDOM);
//Cudd_AutodynDisable(temp);
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;
Cudd_Ref(bdd1);
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;
Cudd_Ref(bdd1);
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;
Cudd_Ref(bdd1);
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;
Cudd_Ref(bdd1);
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;
Cudd_Ref(bdd1);
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;
Cudd_Ref(bdd1);
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:
case 2:
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;
Cudd_ReduceHeap(manager, CUDD_REORDER_SIFT_CONVERGE, 1);
f[0] = Cudd_BddToAdd(manager, bdd);
fd = fopen(filename, "w");
if (fd == NULL) {
perror(filename);
return -1;
}
// Cudd_AutodynEnable(mana, CUDD_REORDER_EXACT);
// Cudd_ReduceHeap(manager, CUDD_REORDER_SIFT, 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;
}
char** GetVariableOrder(char *filename, int varcnt) {
FILE *data;
char *dataread, buf, **varname;
int icur = 0, maxbufsize = 10, index = -1;
if ((data = fopen(filename, "r")) == NULL) {
perror(filename);
return NULL;
}
varname = (char **) malloc(sizeof(char *) * varcnt);
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] == '@') {
index++;
varname[index] = (char *) malloc(sizeof(char) * strlen(dataread));
strcpy(varname[index], dataread + 1);
}
} 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 NULL;
}
while (icur > maxbufsize - 1) {
maxbufsize *= 2;
dataread = (char *) realloc(dataread, sizeof(char) * maxbufsize);
}
}
}
fclose(data);
free(dataread);
for(icur=index+1; icur < varcnt; icur++)
varname[icur] = NULL;
return varname;
}
int LoadVariableData(namedvars varmap, char *filename) {
FILE *data;
infinity, try to fix the ffsll mess, warnings
2015-01-05 16:06:32 +00:00
char *dataread, buf, *varname = NULL, *dynvalue;
update to recent ProbLog.
2011-06-26 23:13:43 +01:00
char * unparsed_string;
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(filename);
return -1;
}
dataread = (char *) malloc(sizeof(char) * maxbufsize);
while(!feof(data)) {
fread(&buf, 1, 1, data);
if ((buf == '\n') && icur == 0) {
// ignore empty lines
} else if (buf == '\n') {
dataread[icur] = '\0';
icur = 0;
buf = ' ';
if (dataread[0] == '@') {
if (hasvar) {
for (index = 0; index < varmap.varcnt; index++) {
if ((varmap.vars[index] != NULL) && (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:
// http://www.cplusplus.com/reference/clibrary/cstdlib/strtod/
errno=0; // reset global error indicator
dvalue = strtod(dataread, &unparsed_string);
// check for errors
if (errno == ERANGE || unparsed_string == dataread) {
fprintf(stderr, "Error at file: %s. Variable: %s does not have a valid 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 ((varmap.vars[index] != NULL) && (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;
// fprintf(stderr,"init hisotry %i %i\n",__LINE__,varcnt+2);
HisQueue = (hisqueue *) malloc(sizeof(hisqueue) * (varcnt+2));
for (i = 0; i < varcnt+2; 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 +2; i++) {
if (HisQueue[i].thenode != NULL && !Cudd_IsConstant(HisQueue[i].thenode)) {
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;
}
}
int my_index_calc(int varstart, DdNode *node){
if(Cudd_IsConstant(node)){
return Cudd_V(node);
}else{
int index = GetIndex(node) - varstart+2;
return index;
}
}
void AddNode(hisqueue *HisQueue, int varstart, DdNode *node, double dvalue, int ivalue, void *dynvalue) {
// int index = GetIndex(node) - varstart;
// fprintf(stderr,"----- node added: %p <-> %i <-> %e\n",node,GetIndex(node),dvalue);
int index= my_index_calc(varstart,node);
HisQueue[index].thenode = (hisnode *) realloc(HisQueue[index].thenode, (HisQueue[index].cnt + 1+2/*account for t+f*/) * sizeof(hisnode));
HisQueue[index].thenode[HisQueue[index].cnt].key = node;
HisQueue[index].thenode[HisQueue[index].cnt].dvalue = dvalue;
HisQueue[index].thenode[HisQueue[index].cnt].dvalue2 = -1; //keep backward compatibility
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 index = GetIndex(node) - varstart;
int index= -1;
index=my_index_calc(varstart,node);
// fprintf(stderr,"----- node retuned: %p <-> %i <-> %i \n",node,GetIndex(node),index);
//TODO: this must be check think not initialzied. Null check fails?
// if (Cudd_IsConstant(node) ){
// fprintf(stderr,"----- node retuned: %p <-> %i \n",node,GetIndex(node));
// fprintf(stderr,"returning %p ,,,,, %e\n", &(HisQueue[index].thenode[index]));
// return &(HisQueue[index].thenode[0]);}
int i;//to bug check
for(i = 0; i < HisQueue[index].cnt; i++) {
if (HisQueue[index].thenode[i].key == node){
// fprintf(stderr,"returning %p ....%e \n", &(HisQueue[index].thenode[i]),&(HisQueue[index].thenode[i]).dvalue);
return &(HisQueue[index].thenode[i]);
}
}
// fprintf(stderr,"returning null\n");
return NULL;
}
int GetNodeIndex(hisqueue *HisQueue, int varstart, DdNode *node) {
int i;
// int index = GetIndex(node) - varstart;
int index= my_index_calc(varstart,node);
if (Cudd_IsConstant(node) ){ return index;}
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(void *) * 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(void *) * 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>0){
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;
}
int all_loaded_for_deterministic_variables(namedvars varmap, int disp) {
int i;
char * dummy;
for (i = 0; i < varmap.varcnt; i++) {
if (varmap.loaded[i] == 0) {
// no value specified, make it a deterministic variable
varmap.loaded[i]=1;
varmap.dvalue[i]=1.0;
varmap.ivalue[i]=0;
dummy = malloc(0);
varmap.dynvalue[i]=dummy;
// if (disp) fprintf(stderr, "The variable: %s was not loaded with values.\n", varmap.vars[i]); else return 0;
}
}
return 1;
}
int ImposeOrder(DdManager *manager, const namedvars varmap, char **map) {
int order[varmap.varcnt], i, mappos, index = -1, ivar;
for (i = 0; i < varmap.varcnt; i++) {
if (map[i] != NULL) {
order[i] = GetNamedVarIndex(varmap, map[i]);
index = i;
} else {
order[i] = -1;
}
}
index++;
for (i = 0; i < varmap.varcnt; i++) {
ivar = Cudd_ReadPerm(manager, i);
mappos = get_var_pos_in_map(map, varmap.vars[ivar], varmap.varcnt);
if (mappos == -1) {
order[index] = ivar;
index++;
}
}
if (index != varmap.varcnt)
fprintf(stderr, "Warning possible error in: Impose Order...\n");
return Cudd_ShuffleHeap(manager, order);
}
int get_var_pos_in_map(char **map, const char *var, int varcnt) {
int i;
for (i = 0; i < varcnt; i++) {
if (map[i] == NULL) return -1;
if (strcmp(map[i], var) == 0) return i;
}
return -1;
}
/* Parser */
DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader fileheader) {
return (FileGenerateBDDForest(manager, varmap, fileheader))[0];
}
DdNode** FileGenerateBDDForest(DdManager *manager, namedvars varmap, bddfileheader fileheader) {
int icomment, maxlinesize, icur, iline, curinter, iequal;
DdNode *Line, **inter, **result;
char buf, *inputline, *filename, *subl;
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 (fileheader.version < 2) {
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);
result = (DdNode **) malloc(sizeof(DdNode *) * 1);
result[0] = inter[curinter];
free(inter);
free(inputline);
return result;
} 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 {
// Support for forest
result = (DdNode **) malloc(sizeof(DdNode *) * 10);
maxlinesize = 10;
iline = -1;
for (subl = strtok(inputline, ","); subl != NULL; subl = strtok(NULL, ",")) {
if (subl[0] == 'L' && IsPosNumber(subl + 1)) {
curinter = atoi(subl + 1) - 1;
if (curinter > -1 && curinter < fileheader.intercnt && inter[curinter] != NULL) {
iline++;
if (iline >= (maxlinesize - 1)) {
maxlinesize *= 2;
result = (DdNode **) realloc(result, sizeof(DdNode *) * maxlinesize);
}
result[iline] = inter[curinter];
} else {
fprintf(stderr, "Error at line: %i. Return result asked(%s) doesn't exist.\n", iline, subl);
fclose(fileheader.inputfile);
free(inter);
free(inputline);
free(subl);
return NULL;
}
} else {
fprintf(stderr, "Error at line: %i. Invalid intermediate result format.\n", iline);
fclose(fileheader.inputfile);
free(inter);
free(inputline);
free(subl);
return NULL;
}
}
if (_debug) fprintf(stderr, "Returned: %s\n", inputline);
fclose(fileheader.inputfile);
free(inter);
free(inputline);
free(subl);
iline++;
result[iline] = NULL;
return result;
}
} 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;
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();
infinity, try to fix the ffsll mess, warnings
2015-01-05 16:06:32 +00:00
// secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC);
update to recent ProbLog.
2011-06-26 23:13:43 +01:00
if (_debug) fprintf(stderr, "term: %s of line: %i took: %ld\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();
infinity, try to fix the ffsll mess, warnings
2015-01-05 16:06:32 +00:00
// secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC);
update to recent ProbLog.
2011-06-26 23:13:43 +01:00
if (_debug) fprintf(stderr, "term: %s of line: %i took: %ld\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;
infinity, try to fix the ffsll mess, warnings
2015-01-05 16:06:32 +00:00
// double secs;
update to recent ProbLog.
2011-06-26 23:13:43 +01:00
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();
infinity, try to fix the ffsll mess, warnings
2015-01-05 16:06:32 +00:00
// secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC);
update to recent ProbLog.
2011-06-26 23:13:43 +01:00
if (_debug) fprintf(stderr, "term: %s of line: %i took: %ld\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();
infinity, try to fix the ffsll mess, warnings
2015-01-05 16:06:32 +00:00
// secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC);
update to recent ProbLog.
2011-06-26 23:13:43 +01:00
if (_debug) fprintf(stderr, "term: %s of line: %i took: %ld\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;
fix current and system predicate
2014-11-25 12:03:48 +00:00
int icur, maxlinesize, iline, index, iloop, iQsize, i, inQ, iRoot;
update to recent ProbLog.
2011-06-26 23:13:43 +01:00
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;
iRoot = 1;
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':
if (iRoot) {
iRoot = 0;
printf("bdd_temp_value('%s', %i).\n", GetNodeVarNameDisp(manager, varmap, curnode), 1);
} else {
printf("bdd_temp_value('%s', %i).\n", GetNodeVarNameDisp(manager, varmap, curnode), iQsize);
}
fflush(stdout);
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);
fix current and system predicate
2014-11-25 12:03:48 +00:00
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));
update to recent ProbLog.
2011-06-26 23:13:43 +01:00
inQ = 0;
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)));
fflush(stdout);
break;
case 'l':
printf("bdd_temp_value('%s').\n", GetNodeVarNameDisp(manager, varmap, LowNodeOf(manager, curnode)));
fflush(stdout);
break;
case 'v':
index = GetNamedVarIndex(varmap, inputline + 3);
if (index >= 0) {
printf("bdd_temp_value([%f,%i,%s]).\n", varmap.dvalue[index], varmap.ivalue[index], (char *) varmap.dynvalue[index]);
fflush(stdout);
} 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);
}
Reference in New Issue Copy Permalink