ADDs replaced by BDDs

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);

packages/cplint/cplint_Prob.c

@@ -117,26 +117,31 @@ 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;
+	if (comp)
-   return value;
+   		return 0.0;
+ 	else
+		return 1.0;
   }
   else
 {
-	
+	nodereg=Cudd_Regular(node);
-	value_p=g_hash_table_lookup(nodes,&node);
+	value_p=g_hash_table_lookup(nodes,&nodereg);
 	if (value_p!=NULL)
 	{
+		if (comp)
+			return 1-*value_p;
+		else
 			return *value_p;
 	}
 	else
@@ -144,24 +149,29 @@ so that it is not recomputed
     		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);
+		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];
+      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;
+      T = Cudd_T(node);
-      F = node->type.kids.E;
+      F = Cudd_E(node);
       bits=bits<<1;
+      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);
 
-      res=ProbBool(T,bits+1,nBit-1,posBVar+1,v,vars,nodes)+ 
-        ProbBool(F,bits,nBit-1,posBVar+1,v,vars,nodes);
       return res;
     }
     else
     {
-      
       bits=bits<<1;
-      res=ProbBool(node,bits+1,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,vars,nodes);
+        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;
 }

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<nBVar;i++)
 		   names[i]=inames[i];
-	  	array[0]=add;
+	  	array[0]=function;
 		onames[0]="Out";
 		file = open_file("cpl.dot", "w");
 		Cudd_DumpDot(mgr,1,array,names,onames,file);
@@ -204,7 +204,7 @@ static int compute_prob(void)
 	{
 		dividend=(dividend<<1)+1;
 	}
-	prob=Prob(add,vars,nodes);
+	prob=Prob(function,vars,nodes);
 	out=YAP_MkFloatTerm(prob);
 	g_hash_table_foreach (nodes,dealloc,NULL);
 	g_hash_table_destroy(nodes);