removed debug printf, changed module tptree name
This commit is contained in:
parent
cde7bda046
commit
b2238c1644
@ -15,7 +15,7 @@
|
|||||||
:- use_module(library(system)).
|
:- use_module(library(system)).
|
||||||
:- use_module(library(ugraphs)).
|
:- use_module(library(ugraphs)).
|
||||||
:- use_module(params).
|
:- use_module(params).
|
||||||
:- use_module(tptreefile).
|
:- use_module(tptree_lpad).
|
||||||
:- use_module(utility).
|
:- use_module(utility).
|
||||||
|
|
||||||
% :- source.
|
% :- source.
|
||||||
|
@ -15,7 +15,7 @@
|
|||||||
:- use_module(library(system)).
|
:- use_module(library(system)).
|
||||||
:- use_module(library(ugraphs)).
|
:- use_module(library(ugraphs)).
|
||||||
:- use_module(params).
|
:- use_module(params).
|
||||||
:- use_module(tptreefile).
|
:- use_module(tptree_lpad).
|
||||||
:- use_module(utility).
|
:- use_module(utility).
|
||||||
|
|
||||||
% :- source.
|
% :- source.
|
||||||
|
@ -15,7 +15,7 @@
|
|||||||
:- use_module(library(system)).
|
:- use_module(library(system)).
|
||||||
:- use_module(library(ugraphs)).
|
:- use_module(library(ugraphs)).
|
||||||
:- use_module(params).
|
:- use_module(params).
|
||||||
:- use_module(tptreefile).
|
:- use_module(tptree_lpad).
|
||||||
:- use_module(utility).
|
:- use_module(utility).
|
||||||
|
|
||||||
% :- source.
|
% :- source.
|
||||||
|
@ -15,7 +15,7 @@
|
|||||||
:- use_module(library(system)).
|
:- use_module(library(system)).
|
||||||
:- use_module(library(ugraphs)).
|
:- use_module(library(ugraphs)).
|
||||||
:- use_module(params).
|
:- use_module(params).
|
||||||
:- use_module(tptreefile).
|
:- use_module(tptree_lpad).
|
||||||
:- use_module(utility).
|
:- use_module(utility).
|
||||||
|
|
||||||
% :- source.
|
% :- source.
|
||||||
|
@ -15,7 +15,7 @@
|
|||||||
:- use_module(library(system)).
|
:- use_module(library(system)).
|
||||||
:- use_module(library(ugraphs)).
|
:- use_module(library(ugraphs)).
|
||||||
:- use_module(params).
|
:- use_module(params).
|
||||||
:- use_module(tptreefile).
|
:- use_module(tptree_lpad).
|
||||||
:- use_module(utility).
|
:- use_module(utility).
|
||||||
|
|
||||||
% :- source.
|
% :- source.
|
||||||
|
@ -141,6 +141,13 @@
|
|||||||
* The End *
|
* The End *
|
||||||
* *
|
* *
|
||||||
\******************************************************************************/
|
\******************************************************************************/
|
||||||
|
/* modified by Fabrizio Riguzzi in 2009 for dealing with multivalued variables:
|
||||||
|
instead of variables or their negation, the script can contain equations of the
|
||||||
|
form
|
||||||
|
variable=value
|
||||||
|
Multivalued variables are translated to binary variables by means of a log
|
||||||
|
encodimg
|
||||||
|
*/
|
||||||
|
|
||||||
|
|
||||||
#include "simplecudd.h"
|
#include "simplecudd.h"
|
||||||
@ -717,31 +724,17 @@ so that it is not recomputed
|
|||||||
double value;
|
double value;
|
||||||
|
|
||||||
|
|
||||||
//printf("Prob node %d\n",node);
|
|
||||||
//index=Cudd_NodeReadIndex(node);
|
|
||||||
//printf("Prob INdex %d\n",index);
|
|
||||||
if (Cudd_IsConstant(node))
|
if (Cudd_IsConstant(node))
|
||||||
{
|
{
|
||||||
value=Cudd_V(node);//node->type.value;
|
value=Cudd_V(node);
|
||||||
//printf("Value %e comp %d\n",value,comp);
|
if (comp)
|
||||||
if (comp)//Cudd_IsComplement(node))
|
|
||||||
//return (1.0-value);
|
|
||||||
//if (value>0)
|
|
||||||
{
|
{
|
||||||
// printf("return 0");
|
|
||||||
return 0.0;
|
return 0.0;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
// printf("return 1");
|
|
||||||
return 1.0;
|
return 1.0;
|
||||||
}
|
}
|
||||||
/*else
|
|
||||||
if (value>0)
|
|
||||||
return 1.0;
|
|
||||||
else
|
|
||||||
return 0.0;
|
|
||||||
*/ //return value;
|
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
@ -749,22 +742,15 @@ so that it is not recomputed
|
|||||||
|
|
||||||
if (Found!=NULL)
|
if (Found!=NULL)
|
||||||
{
|
{
|
||||||
//printf("value found %e\n",Found->dvalue);
|
|
||||||
return Found->dvalue;
|
return Found->dvalue;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
index=Cudd_NodeReadIndex(node);
|
index=Cudd_NodeReadIndex(node);
|
||||||
//printf("node absent %d comp %d\n",node,comp);
|
|
||||||
//mVarIndex=array_fetch(int,bVar2mVar,index);
|
|
||||||
mVarIndex=MyManager.varmap.bVar2mVar[index];
|
mVarIndex=MyManager.varmap.bVar2mVar[index];
|
||||||
//v=array_fetch(variable,vars,mVarIndex);
|
|
||||||
v=MyManager.varmap.mvars[mVarIndex];
|
v=MyManager.varmap.mvars[mVarIndex];
|
||||||
nBit=v.nBit;
|
nBit=v.nBit;
|
||||||
// printf("calling prob bool mvar %d nbit %d\n",mVarIndex,nBit);
|
|
||||||
//scanf("%d",&r);
|
|
||||||
res=ProbBool(MyManager,node,0,nBit,0,v,comp);
|
res=ProbBool(MyManager,node,0,nBit,0,v,comp);
|
||||||
//printf("New val %e\n",res);
|
|
||||||
AddNode1(MyManager.varmap.bVar2mVar,MyManager.his, MyManager.varmap.varstart, node, res, 0, NULL);
|
AddNode1(MyManager.varmap.bVar2mVar,MyManager.his, MyManager.varmap.varstart, node, res, 0, NULL);
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
@ -778,68 +764,40 @@ double ProbBool(extmanager MyManager, DdNode *node, int bits, int nBit,int posBV
|
|||||||
double p,res;
|
double p,res;
|
||||||
double * probs;
|
double * probs;
|
||||||
int index;
|
int index;
|
||||||
// printf("ProbBool nBit %d\n",nBit);
|
|
||||||
//scanf("%d",&r);
|
|
||||||
probs=v.probabilities;
|
probs=v.probabilities;
|
||||||
if (nBit==0)
|
if (nBit==0)
|
||||||
{
|
{
|
||||||
//printf("last var bits %d larray %d comp %d\n",bits,array_n(probs),comp);
|
|
||||||
// printf("bits %d v.nbit %d\n",bits,v.nBit);
|
|
||||||
if (bits>=v.nVal)
|
if (bits>=v.nVal)
|
||||||
//if (comp)
|
|
||||||
{
|
{
|
||||||
//printf("bits>=v.nbit return 0\n");
|
|
||||||
return 0.0;
|
return 0.0;
|
||||||
}
|
}
|
||||||
//else
|
|
||||||
//{printf("return 0\n");
|
|
||||||
//return 1.0;}}
|
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
// printf("Val %d\n",bits);
|
|
||||||
|
|
||||||
//p=array_fetch(double,probs,bits);
|
|
||||||
p=probs[bits];
|
p=probs[bits];
|
||||||
//printf("prob %e\n",p);
|
|
||||||
res=p*Prob(MyManager,node,comp);
|
res=p*Prob(MyManager,node,comp);
|
||||||
//printf("prob %e\n",p);
|
|
||||||
//printf("bottom %e\n",res);
|
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
//if (correctPosition(node->index,v,node,posBVar))
|
|
||||||
index=Cudd_NodeReadIndex(node);
|
index=Cudd_NodeReadIndex(node);
|
||||||
//printf("index %d\n",Cudd_NodeReadIndex(node));
|
|
||||||
if (correctPosition(index,v,posBVar))
|
if (correctPosition(index,v,posBVar))
|
||||||
{
|
{
|
||||||
//printf("node %d\n",node);
|
T = Cudd_T(node);
|
||||||
T = Cudd_T(node);//node->type.kids.T;
|
F = Cudd_E(node);
|
||||||
F = Cudd_E(node);//node->type.kids.E;
|
|
||||||
bits=bits<<1;
|
bits=bits<<1;
|
||||||
//printf("calling on the true child %di complement %d\n",T,Cudd_IsComplement(T));
|
|
||||||
res=ProbBool(MyManager,T,bits+1,nBit-1,posBVar+1,v,comp);
|
res=ProbBool(MyManager,T,bits+1,nBit-1,posBVar+1,v,comp);
|
||||||
//printf("res %e\ncalling on the else child %d c %d\n",res,F,Cudd_IsComplement(F));
|
|
||||||
//printf("comp %d ",comp);
|
|
||||||
comp=(!comp && Cudd_IsComplement(F)) || (comp && !Cudd_IsComplement(F));
|
comp=(!comp && Cudd_IsComplement(F)) || (comp && !Cudd_IsComplement(F));
|
||||||
//printf("comp %d \n",comp);
|
|
||||||
res=res+
|
res=res+
|
||||||
ProbBool(MyManager,F,bits,nBit-1,posBVar+1,v,comp);
|
ProbBool(MyManager,F,bits,nBit-1,posBVar+1,v,comp);
|
||||||
//printf("res 2 %e\n",res);
|
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
//printf("absent var\n");
|
|
||||||
bits=bits<<1;
|
bits=bits<<1;
|
||||||
// printf("Var =1\n");
|
|
||||||
res=ProbBool(MyManager,node,bits+1,nBit-1,posBVar+1,v,comp);
|
res=ProbBool(MyManager,node,bits+1,nBit-1,posBVar+1,v,comp);
|
||||||
//printf("res 1 %e\n",res);
|
|
||||||
//printf("var =0\n");
|
|
||||||
res=res+
|
res=res+
|
||||||
ProbBool(MyManager,node,bits,nBit-1,posBVar+1,v,comp);
|
ProbBool(MyManager,node,bits,nBit-1,posBVar+1,v,comp);
|
||||||
// printf("res 2 %e\n",res);
|
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -850,12 +808,8 @@ int correctPosition(int index,variable v,int posBVar)
|
|||||||
currently explored by ProbBool */
|
currently explored by ProbBool */
|
||||||
{
|
{
|
||||||
int bvar;
|
int bvar;
|
||||||
//printf("posbvar %d\n",posBVar);
|
|
||||||
//printf("length %d\n",array_n(v.booleanVars));
|
|
||||||
//bvar=array_fetch(DdNode *,v.booleanVars,posBVar);
|
|
||||||
bvar=v.booleanVars[posBVar];
|
bvar=v.booleanVars[posBVar];
|
||||||
|
|
||||||
// return var->index==index;
|
|
||||||
return(bvar==index);
|
return(bvar==index);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -140,6 +140,11 @@
|
|||||||
* The End *
|
* The End *
|
||||||
* *
|
* *
|
||||||
\******************************************************************************/
|
\******************************************************************************/
|
||||||
|
/* modified by Fabrizio Riguzzi in 2009 for dealing with multivalued variables
|
||||||
|
instead of variables or their negation, the script can contain equations of the
|
||||||
|
form
|
||||||
|
variable=value
|
||||||
|
*/
|
||||||
|
|
||||||
|
|
||||||
#include "general.h"
|
#include "general.h"
|
||||||
|
@ -140,6 +140,11 @@
|
|||||||
* The End *
|
* The End *
|
||||||
* *
|
* *
|
||||||
\******************************************************************************/
|
\******************************************************************************/
|
||||||
|
/* modified by Fabrizio Riguzzi in 2009 for dealing with multivalued variables
|
||||||
|
instead of variables or their negation, the script can contain equations of the
|
||||||
|
form
|
||||||
|
variable=value
|
||||||
|
*/
|
||||||
|
|
||||||
|
|
||||||
#include <stdio.h>
|
#include <stdio.h>
|
||||||
|
@ -140,8 +140,11 @@
|
|||||||
* The End *
|
* The End *
|
||||||
* *
|
* *
|
||||||
\******************************************************************************/
|
\******************************************************************************/
|
||||||
|
/* modified by Fabrizio Riguzzi in 2009 for dealing with multivalued variables
|
||||||
|
instead of variables or their negation, the script can contain equations of the
|
||||||
|
form
|
||||||
|
variable=value
|
||||||
|
*/
|
||||||
#include "simplecudd.h"
|
#include "simplecudd.h"
|
||||||
|
|
||||||
/* BDD manager initialization */
|
/* BDD manager initialization */
|
||||||
@ -587,7 +590,6 @@ int LoadMultiVariableData(DdManager * mgr,namedvars varmap, char *filename) {
|
|||||||
varname = (char *) malloc(sizeof(char) * strlen(dataread));
|
varname = (char *) malloc(sizeof(char) * strlen(dataread));
|
||||||
strcpy(varname, dataread);
|
strcpy(varname, dataread);
|
||||||
varmap.vars[index]=varname;
|
varmap.vars[index]=varname;
|
||||||
//printf("vname %d %s\n",index, varmap.vars[index]);
|
|
||||||
|
|
||||||
fscanf(data, "%d\n", &values);
|
fscanf(data, "%d\n", &values);
|
||||||
varmap.loaded[index] = 1;
|
varmap.loaded[index] = 1;
|
||||||
@ -767,7 +769,6 @@ int AddNamedMultiVar(DdManager *mgr,namedvars varmap, const char *varname, int *
|
|||||||
int *booleanVars;
|
int *booleanVars;
|
||||||
char * vname;
|
char * vname;
|
||||||
l=strlen(varname);
|
l=strlen(varname);
|
||||||
//printf("addnamed %s\n",varname);
|
|
||||||
i=0;
|
i=0;
|
||||||
while (varname[i]!='-')
|
while (varname[i]!='-')
|
||||||
{
|
{
|
||||||
@ -776,11 +777,8 @@ int AddNamedMultiVar(DdManager *mgr,namedvars varmap, const char *varname, int *
|
|||||||
vname=(char *)malloc(sizeof(char)*(l+1));
|
vname=(char *)malloc(sizeof(char)*(l+1));
|
||||||
strncpy(vname,varname,i);
|
strncpy(vname,varname,i);
|
||||||
vname[i]='\0';
|
vname[i]='\0';
|
||||||
//printf("addnamed vname %s\n",vname);
|
|
||||||
sscanf(varname+i+1,"%d",value);
|
sscanf(varname+i+1,"%d",value);
|
||||||
index= GetNamedVarIndex(varmap, vname);
|
index= GetNamedVarIndex(varmap, vname);
|
||||||
//printf("index %d\n",index);
|
|
||||||
//printf("init %d\n",varmap.mvars[index].init);
|
|
||||||
if (index == -1 * varmap.varcnt) {
|
if (index == -1 * varmap.varcnt) {
|
||||||
return -1;
|
return -1;
|
||||||
} else if ((index < 0) || (index == 0 && varmap.vars[0] == NULL)) {
|
} else if ((index < 0) || (index == 0 && varmap.vars[0] == NULL)) {
|
||||||
@ -790,16 +788,14 @@ int AddNamedMultiVar(DdManager *mgr,namedvars varmap, const char *varname, int *
|
|||||||
if (varmap.mvars[index].init==0){
|
if (varmap.mvars[index].init==0){
|
||||||
nBit=varmap.mvars[index].nBit;
|
nBit=varmap.mvars[index].nBit;
|
||||||
booleanVars= varmap.mvars[index].booleanVars;
|
booleanVars= varmap.mvars[index].booleanVars;
|
||||||
//Cudd_MakeTreeNode(mgr,boolVars,nBit,MTR_FIXED);
|
|
||||||
for (i=0;i<nBit;i++)
|
for (i=0;i<nBit;i++)
|
||||||
{
|
{
|
||||||
//printf("index %d %d bv %d\n",index,i,boolVars);
|
|
||||||
booleanVars[i]=boolVars;
|
booleanVars[i]=boolVars;
|
||||||
varmap.bVar2mVar[boolVars]=index;
|
varmap.bVar2mVar[boolVars]=index;
|
||||||
boolVars=boolVars+1;
|
boolVars=boolVars+1;
|
||||||
}
|
}
|
||||||
varmap.mvars[index].init=1;
|
varmap.mvars[index].init=1;
|
||||||
} //else printf("index found %d %d bv %d\n",index,i,varmap.mvars[index].booleanVars[0]);
|
}
|
||||||
return index;
|
return index;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -854,7 +850,6 @@ int SetNamedVarValues(namedvars varmap, const char *varname, double dvalue, int
|
|||||||
int GetNamedVarIndex(const namedvars varmap, const char *varname) {
|
int GetNamedVarIndex(const namedvars varmap, const char *varname) {
|
||||||
int i,j;
|
int i,j;
|
||||||
for (i = 0; i < varmap.varcnt; i++) {
|
for (i = 0; i < varmap.varcnt; i++) {
|
||||||
// printf(" %d %s %s\n",i,varmap.vars[i],varname);
|
|
||||||
if (varmap.vars[i] == NULL) return -1 * i;
|
if (varmap.vars[i] == NULL) return -1 * i;
|
||||||
if (strcmp(varmap.vars[i], varname) == 0) return i;
|
if (strcmp(varmap.vars[i], varname) == 0) return i;
|
||||||
}
|
}
|
||||||
@ -969,11 +964,9 @@ DdNode* FileGenerateBDD(DdManager *manager, namedvars varmap, bddfileheader file
|
|||||||
Line = LineParser(manager, varmap, inter, fileheader.intercnt, inputline, iline);
|
Line = LineParser(manager, varmap, inter, fileheader.intercnt, inputline, iline);
|
||||||
endAt = clock();
|
endAt = clock();
|
||||||
secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC)*1000;
|
secs = ((double) (endAt - startAt)) / ((double) CLOCKS_PER_SEC)*1000;
|
||||||
//printf("line %e\n",secs);
|
|
||||||
} else {
|
} else {
|
||||||
interfileheader = ReadFileHeader(filename);
|
interfileheader = ReadFileHeader(filename);
|
||||||
if (interfileheader.inputfile == NULL) {
|
if (interfileheader.inputfile == NULL) {
|
||||||
//Line = simpleBDDload(manager, &varmap, filename);
|
|
||||||
Line = NULL;
|
Line = NULL;
|
||||||
} else {
|
} else {
|
||||||
Line = FileGenerateBDD(manager, varmap, interfileheader);
|
Line = FileGenerateBDD(manager, varmap, interfileheader);
|
||||||
@ -1113,9 +1106,7 @@ DdNode* LineParser(DdManager *manager, namedvars varmap, DdNode **inter, int max
|
|||||||
inegvar = 1;
|
inegvar = 1;
|
||||||
} else {
|
} else {
|
||||||
iconst = 0;
|
iconst = 0;
|
||||||
//printf("term %s\n",term + inegvar);
|
|
||||||
ivar = AddNamedMultiVar(manager,varmap, term + inegvar,&value);
|
ivar = AddNamedMultiVar(manager,varmap, term + inegvar,&value);
|
||||||
//printf("term %s var %d\n",term + inegvar,ivar);
|
|
||||||
|
|
||||||
if (ivar == -1) {
|
if (ivar == -1) {
|
||||||
fprintf(stderr, "Line Parser Error at line: %i. More BDD variables than the reserved term: %s.\n", iline, term);
|
fprintf(stderr, "Line Parser Error at line: %i. More BDD variables than the reserved term: %s.\n", iline, term);
|
||||||
|
@ -140,6 +140,11 @@
|
|||||||
* The End *
|
* The End *
|
||||||
* *
|
* *
|
||||||
\******************************************************************************/
|
\******************************************************************************/
|
||||||
|
/* modified by Fabrizio Riguzzi in 2009 for dealing with multivalued variables
|
||||||
|
instead of variables or their negation, the script can contain equations of the
|
||||||
|
form
|
||||||
|
variable=value
|
||||||
|
*/
|
||||||
|
|
||||||
|
|
||||||
#include <stdio.h>
|
#include <stdio.h>
|
||||||
|
@ -6,8 +6,14 @@
|
|||||||
% remembers shortest prefix of a conjunction only (i.e. a*b+a*b*c results in a*b only, but b*a+a*b*c is not reduced)
|
% remembers shortest prefix of a conjunction only (i.e. a*b+a*b*c results in a*b only, but b*a+a*b*c is not reduced)
|
||||||
% children are sorted, but branches aren't (to speed up search while keeping structure sharing from proof procedure)
|
% children are sorted, but branches aren't (to speed up search while keeping structure sharing from proof procedure)
|
||||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
/* derived from tptree.yap from ProbLog by Fabrizio Riguzzi in 2009
|
||||||
|
for dealing with multivalued variables
|
||||||
|
instead of variables or their negation, the script can contain equations of the
|
||||||
|
form
|
||||||
|
variable=value
|
||||||
|
*/
|
||||||
|
|
||||||
:- module(ptree,[init_ptree/1,
|
:- module(ptree_lpad,[init_ptree/1,
|
||||||
delete_ptree/1,
|
delete_ptree/1,
|
||||||
rename_ptree/2,
|
rename_ptree/2,
|
||||||
member_ptree/2,
|
member_ptree/2,
|
||||||
|
Reference in New Issue
Block a user