From 9d151a85f8e9f7607c6a5349979050465ebfd260 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 7 Aug 2009 14:25:47 +0000
Subject: [PATCH] Addition of get_index_of_first_from_bdd() function to ODD
 lib.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1410 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/include/odd.h  |  1 +
 prism/src/odd/odd.cc | 30 ++++++++++++++++++++++++++++++
 2 files changed, 31 insertions(+)

diff --git a/prism/include/odd.h b/prism/include/odd.h
index d5be9f18..ce9a60c9 100644
--- a/prism/include/odd.h
+++ b/prism/include/odd.h
@@ -51,6 +51,7 @@ struct ODDNode
 // function prototypes
 
 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);
 int get_num_odd_nodes();
 
 //------------------------------------------------------------------------------
diff --git a/prism/src/odd/odd.cc b/prism/src/odd/odd.cc
index 0acf917f..6f09bcdf 100644
--- a/prism/src/odd/odd.cc
+++ b/prism/src/odd/odd.cc
@@ -135,6 +135,36 @@ long add_offsets(DdManager *ddman, ODDNode *odd, int level, int num_vars)
 
 //------------------------------------------------------------------------------
 
+// Get the index (according to an ODD) of the first non-zero enetry of a BDD
+
+int get_index_of_first_from_bdd(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, ODDNode *odd)
+{
+	DdNode *ptr, *ptr_next;;
+	ODDNode *odd_ptr;
+	int i, index;
+	
+	// Go down dd along first non-zero path
+	index = 0;
+	ptr = dd;
+	odd_ptr = odd;
+	for (i = 0; i < num_vars; i++) {
+		ptr_next = (ptr->index > vars[i]->index) ? ptr : Cudd_E(ptr);
+		if (ptr_next != Cudd_ReadZero(ddman)) {
+			odd_ptr = odd_ptr->e;
+		}
+		else {
+			ptr_next = (ptr->index > vars[i]->index) ? ptr : Cudd_T(ptr);
+			index += odd_ptr->eoff;
+			odd_ptr = odd_ptr->t;
+		}
+		ptr = ptr_next;
+	}
+
+	return index;
+}
+
+//------------------------------------------------------------------------------
+
 int get_num_odd_nodes()
 {
 	return num_odd_nodes;