Commit 256d8005 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 519a67ba
......@@ -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;
}
}
......
......@@ -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);
};
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment