Added func in odd to convert index to BDD.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2202 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/include/odd.h

@@ -33,6 +33,13 @@
 #include <cudd.h>
 #include <dd.h>
 
+// Flags for building Windows DLLs
+#ifdef __MINGW32__
+	#define EXPORT __declspec(dllexport)
+#else
+	#define EXPORT
+#endif
+
 // odd definitions
 
 typedef struct ODDNode ODDNode;
@@ -52,6 +59,7 @@ struct ODDNode
 
 ODDNode *build_odd(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars);
 int get_index_of_first_from_bdd(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, ODDNode *odd);
+EXPORT DdNode *single_index_to_bdd(DdManager *ddman, int i, DdNode **vars, int num_vars, ODDNode *odd);
 int get_num_odd_nodes();
 
 //------------------------------------------------------------------------------

prism/src/odd/odd.cc

@@ -32,6 +32,7 @@ static int num_odd_nodes = 0;
 // local prototypes
 static ODDNode *build_odd_rec(DdManager *ddman, DdNode *dd, int level, DdNode **vars, int num_vars, ODDNode **tables);
 static long add_offsets(DdManager *ddman, ODDNode *dd, int level, int num_vars);
+static DdNode *single_index_to_bdd_rec(DdManager *ddman, int i, DdNode **vars, int num_vars, int level, ODDNode *odd, long o);
 
 //------------------------------------------------------------------------------
 
@@ -162,6 +163,34 @@ int get_index_of_first_from_bdd(DdManager *ddman, DdNode *dd, DdNode **vars, int
 	return index;
 }
 
+// Get a BDD for a single state given its index and the accompanying ODD.
+
+EXPORT DdNode *single_index_to_bdd(DdManager *ddman, int i, DdNode **vars, int num_vars, ODDNode *odd)
+{
+	return single_index_to_bdd_rec(ddman, i, vars, num_vars, 0, odd, 0);
+}
+
+DdNode *single_index_to_bdd_rec(DdManager *ddman, int i, DdNode **vars, int num_vars, int level, ODDNode *odd, long o)
+{
+	DdNode *dd;
+
+	if (level == num_vars) {
+		return DD_Constant(ddman, 1);
+	}
+	else {
+		if (odd->eoff > i - o) {
+			dd = single_index_to_bdd_rec(ddman, i, vars, num_vars, level+1, odd->e, o);
+			Cudd_Ref(vars[level]);
+			return DD_And(ddman, DD_Not(ddman, vars[level]), dd);
+		}
+		else {
+			dd = single_index_to_bdd_rec(ddman, i, vars, num_vars, level+1, odd->t, o+odd->eoff);
+			Cudd_Ref(vars[level]);
+			return DD_And(ddman, vars[level], dd);
+		}
+	}
+}
+
 //------------------------------------------------------------------------------
 
 int get_num_odd_nodes()