From 256d800580f6888e462fb51abcf626c56c0c98b3 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 15 Aug 2003 01:20:57 +0000
Subject: [PATCH] varnum can be augmented by other allocator.  Keep track of a
 local varnum (lvarnum) in each allocator. * src/misc/bddalloc.cc
 (bdd_allocator::bdd_allocator): Initialize lvarnum.
 (bdd_allocator::extvarnum): New method. (bdd_allocator::allocate_variables):
 Use lvarnum and extvarnum. * src/misc/bddalloc.hh (bdd_allocator::extvarnum):
 New mathod. (bdd_allocator::lvarnum): New variable.

---
 src/misc/bddalloc.cc | 32 +++++++++++++++++++++++++-------
 src/misc/bddalloc.hh |  6 +++++-
 2 files changed, 30 insertions(+), 8 deletions(-)

diff --git a/src/misc/bddalloc.cc b/src/misc/bddalloc.cc
index e57d8d7dd..3a00941d3 100644
--- a/src/misc/bddalloc.cc
+++ b/src/misc/bddalloc.cc
@@ -8,9 +8,10 @@ namespace spot
   int bdd_allocator::varnum = 2;
 
   bdd_allocator::bdd_allocator()
+    : lvarnum(varnum)
   {
     initialize();
-    free_list.push_front(pos_lenght_pair(0, varnum));
+    free_list.push_front(pos_lenght_pair(0, lvarnum));
   }
 
   void
@@ -23,6 +24,25 @@ namespace spot
     bdd_setvarnum(varnum);
   }
 
+  void
+  bdd_allocator::extvarnum(int more)
+  {
+    // If varnum has been extended from another allocator, use
+    // the new variables.
+    if (lvarnum < varnum)
+      {
+	more -= varnum - lvarnum;
+	lvarnum = varnum;
+      }
+    // If we still need more variable, do allocate them.
+    if (more > 0)
+      {
+	bdd_extvarnum(more);
+	varnum += more;
+	lvarnum = varnum;
+      }
+  }
+
   int
   bdd_allocator::allocate_variables(int n)
   {
@@ -65,22 +85,20 @@ namespace spot
     // If we already have some free variable at the end
     // of the variable space, allocate just the difference.
     if (free_list.size() > 0
-	&& free_list.back().first + free_list.back().second == varnum)
+	&& free_list.back().first + free_list.back().second == lvarnum)
       {
 	int res = free_list.back().first;
 	int endvar = free_list.back().second;
 	assert(n > endvar);
-	bdd_extvarnum(n - endvar);
-	varnum += n - endvar;
+	extvarnum(n - endvar);
 	free_list.pop_back();
 	return res;
       }
     else
       {
 	// Otherwise, allocate as much variables as we need.
-	int res = varnum;
-	bdd_extvarnum(n);
-	varnum += n;
+	int res = lvarnum;
+	extvarnum(n);
 	return res;
       }
   }
diff --git a/src/misc/bddalloc.hh b/src/misc/bddalloc.hh
index 68b66a7e1..4e02cc541 100644
--- a/src/misc/bddalloc.hh
+++ b/src/misc/bddalloc.hh
@@ -21,10 +21,14 @@ namespace spot
     void release_variables(int base, int n);
 
     static bool initialized; ///< Whether the BDD library has been initialized.
-    static int varnum; ///< number of variable in use in the BDD library.
+    static int varnum; ///< number of variables in use in the BDD library.
+    int lvarnum; ///< number of variables in use in this allocator.
     typedef std::pair<int, int> pos_lenght_pair;
     typedef std::list<pos_lenght_pair> free_list_type;
     free_list_type free_list; ///< Tracks unused BDD variables.
+  private:
+    /// Require more variables.
+    void extvarnum(int more);
   };
 
 }