diff --git a/packages/cplint/cplint.h b/packages/cplint/cplint.h index 07ff93c40..dc99bbf82 100644 --- a/packages/cplint/cplint.h +++ b/packages/cplint/cplint.h @@ -63,4 +63,5 @@ DdNode * retFactor(DdManager * mgr, factor f, variables v); double Prob(DdNode *node, variables vars,GHashTable * nodes); double ProbBool(DdNode *node, int bits, int nBit,int posBVar,variable v, -variables vars,GHashTable * nodes); +int mVarIndex, +variables vars,GHashTable * nodes, int comp); diff --git a/packages/cplint/cplint_Prob.c b/packages/cplint/cplint_Prob.c index 5ea44a285..c1c7967af 100644 --- a/packages/cplint/cplint_Prob.c +++ b/packages/cplint/cplint_Prob.c @@ -117,52 +117,62 @@ nodes is used to store nodes for which the probability has alread been computed so that it is not recomputed */ { - int index,mVarIndex,nBit; + int index,mVarIndex,nBit,comp; variable v; double res; - double value; double * value_p; - DdNode **key; + DdNode **key,*nodereg; double *rp; - index=node->index; + index=Cudd_NodeReadIndex(node); + comp=Cudd_IsComplement(node); if (Cudd_IsConstant(node)) { - value=node->type.value; - return value; + if (comp) + return 0.0; + else + return 1.0; } else { - - value_p=g_hash_table_lookup(nodes,&node); + nodereg=Cudd_Regular(node); + value_p=g_hash_table_lookup(nodes,&nodereg); if (value_p!=NULL) { - return *value_p; + if (comp) + return 1-*value_p; + else + return *value_p; } else { mVarIndex=vars.bVar2mVar[index]; v=vars.varar[mVarIndex]; nBit=v.nBit; - res=ProbBool(node,0,nBit,0,v,vars,nodes); + res=ProbBool(node,0,nBit,0,v,mVarIndex,vars,nodes,0); key=(DdNode **)malloc(sizeof(DdNode *)); - *key=node; + *key=nodereg; rp=(double *)malloc(sizeof(double)); *rp=res; g_hash_table_insert(nodes, key, rp); - return res; + if (comp) + return 1-res; + else + return res; } } } double ProbBool(DdNode *node, int bits, int nBit,int posBVar,variable v, -variables vars, GHashTable * nodes) +int mVarIndex, +variables vars, GHashTable * nodes,int comp) /* explores a group of binary variables making up the multivalued variable v */ { DdNode *T,*F; double p,res; double * probs; - + int comp1,comp2,index,indexF,mVarIndexF; + probs=v.probabilities; if (nBit==0) { @@ -171,28 +181,41 @@ variables vars, GHashTable * nodes) else { p=probs[bits]; - res=p*Prob(node,vars,nodes); + if (comp) + res=p*(1-Prob(node,vars,nodes)); + else + res=p*Prob(node,vars,nodes); return res; } } else { - if (correctPosition(node->index,v,node,posBVar)) + index=Cudd_NodeReadIndex(node); + if (correctPosition(index,v,node,posBVar)) { - T = node->type.kids.T; - F = node->type.kids.E; + T = Cudd_T(node); + F = Cudd_E(node); bits=bits<<1; - - res=ProbBool(T,bits+1,nBit-1,posBVar+1,v,vars,nodes)+ - ProbBool(F,bits,nBit-1,posBVar+1,v,vars,nodes); + comp1=Cudd_IsComplement(F); + res=ProbBool(T,bits+1,nBit-1,posBVar+1,v,mVarIndex,vars,nodes,comp); + indexF=Cudd_NodeReadIndex(F); + if (Cudd_IsConstant(F)) + mVarIndexF=-1; + else + mVarIndexF=vars.bVar2mVar[indexF]; + if (mVarIndexF==mVarIndex) + comp2=(comp1 && !comp) || (!comp1 && comp); + else + comp2=comp; + res=res+ ProbBool(F,bits,nBit-1,posBVar+1,v,mVarIndex,vars,nodes,comp2); + return res; } else { - bits=bits<<1; - res=ProbBool(node,bits+1,nBit-1,posBVar+1,v,vars,nodes)+ - ProbBool(node,bits,nBit-1,posBVar+1,v,vars,nodes); + res=ProbBool(node,bits+1,nBit-1,posBVar+1,v,mVarIndex,vars,nodes,comp)+ + ProbBool(node,bits,nBit-1,posBVar+1,v,mVarIndex,vars,nodes,comp); return res; } } @@ -203,7 +226,8 @@ int correctPosition(int index,variable v, DdNode * node,int posBVar) currently explored by ProbBool */ { DdNode * bvar; - + int ind; bvar=v.booleanVars[posBVar]; - return bvar->index==index; + ind=Cudd_NodeReadIndex(bvar); + return ind==index; } diff --git a/packages/cplint/cplint_yap.c b/packages/cplint/cplint_yap.c index 04315f360..cdc32d58a 100644 --- a/packages/cplint/cplint_yap.c +++ b/packages/cplint/cplint_yap.c @@ -139,7 +139,7 @@ static int compute_prob(void) YAP_Term out,arg1,arg2,arg3,arg4; variables vars; expr expression; - DdNode * function, * add; + DdNode * function; DdManager * mgr; int nBVar,i,j,intBits,create_dot; FILE * file; @@ -179,7 +179,7 @@ static int compute_prob(void) /* the BDD build by retFunction is converted to an ADD (algebraic decision diagram) because it is easier to interpret and to print */ - add=Cudd_BddToAdd(mgr,function); + //add=Cudd_BddToAdd(mgr,function); //Cudd_PrintInfo(mgr,stderr); if (create_dot) @@ -188,7 +188,7 @@ static int compute_prob(void) nBVar=vars.nBVar; for(i=0;i