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

Move the free_list management into a separate class for reuse.

* src/misc/freelist.hh, src/misc/freelist.cc: New files.
* src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them.
* src/misc/bddalloc.hh (bdd_allocator): Inherit from free_list and
make dump_free_list visible.
* src/misc/bddalloc.cc (bdd_allocator::allocate_variables): Move
all the code into free_list::register_n() and
bdd_allocator::extend(), and call the former.
(bdd_allocator::release_variables): Move all the code into
free_list::release_n() and call it.
(bdd_allocator::extend): New method.
* src/tgba/bdddict.cc (bdd_dict::dump): Call dump_free_list;
parent b84e6a64
2004-03-18 Alexandre Duret-Lutz <adl@src.lip6.fr>
Move the free_list management into a separate class for reuse.
* src/misc/freelist.hh, src/misc/freelist.cc: New files.
* src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them.
* src/misc/bddalloc.hh (bdd_allocator): Inherit from free_list and
make dump_free_list visible.
* src/misc/bddalloc.cc (bdd_allocator::allocate_variables): Move
all the code into free_list::register_n() and
bdd_allocator::extend(), and call the former.
(bdd_allocator::release_variables): Move all the code into
free_list::release_n() and call it.
(bdd_allocator::extend): New method.
* src/tgba/bdddict.cc (bdd_dict::dump): Call dump_free_list;
2004-03-09 Alexandre Duret-Lutz <adl@src.lip6.fr>
* configure.ac, NEWS: Bump version to 0.0s.
......
......@@ -28,6 +28,7 @@ misc_HEADERS = \
bddalloc.hh \
bddlt.hh \
escape.hh \
freelist.hh \
hash.hh \
minato.hh \
version.hh
......@@ -36,5 +37,6 @@ noinst_LTLIBRARIES = libmisc.la
libmisc_la_SOURCES = \
bddalloc.cc \
escape.cc \
freelist.cc \
minato.cc \
version.cc
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
//
......@@ -32,7 +32,7 @@ namespace spot
: lvarnum(varnum)
{
initialize();
free_list.push_front(pos_lenght_pair(0, lvarnum));
fl.push_front(pos_lenght_pair(0, lvarnum));
}
void
......@@ -71,52 +71,27 @@ namespace spot
int
bdd_allocator::allocate_variables(int n)
{
// Browse the free list until we find N consecutive variables. We
// try not to fragment the list my allocating the variables in the
// smallest free range we find.
free_list_type::iterator best = free_list.end();
free_list_type::iterator cur;
for (cur = free_list.begin(); cur != free_list.end(); ++cur)
{
if (cur->second < n)
continue;
if (n == cur->second)
{
best = cur;
break;
}
if (best == free_list.end()
|| cur->second < best->second)
best = cur;
}
// We have found enough free variables.
if (best != free_list.end())
{
int result = best->first;
best->second -= n;
assert(best->second >= 0);
// Erase the range if it's now empty.
if (best->second == 0)
free_list.erase(best);
else
best->first += n;
return result;
}
return register_n(n);
}
// We haven't found enough adjacent free variables;
// ask BuDDy for some more.
void
bdd_allocator::release_variables(int base, int n)
{
release_n(base, n);
}
int
bdd_allocator::extend(int n)
{
// 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 == lvarnum)
if (fl.size() > 0 && fl.back().first + fl.back().second == lvarnum)
{
int res = free_list.back().first;
int endvar = free_list.back().second;
int res = fl.back().first;
int endvar = fl.back().second;
assert(n > endvar);
extvarnum(n - endvar);
free_list.pop_back();
fl.pop_back();
return res;
}
else
......@@ -127,40 +102,4 @@ namespace spot
return res;
}
}
void
bdd_allocator::release_variables(int base, int n)
{
free_list_type::iterator cur;
int end = base + n;
for (cur = free_list.begin(); cur != free_list.end(); ++cur)
{
// Append to a range ...
if (cur->first + cur->second == base)
{
cur->second += n;
// Maybe the next item on the list can be merged.
free_list_type::iterator next = cur;
++next;
if (next != free_list.end()
&& next->first == end)
{
cur->second += next->second;
free_list.erase(next);
}
return;
}
// ... or prepend to a range ...
if (cur->first == end)
{
cur->first -= n;
cur->second += n;
return;
}
// ... or insert a new range.
if (cur->first > end)
break;
}
free_list.insert(cur, pos_lenght_pair(base, n));
}
}
......@@ -22,14 +22,14 @@
#ifndef SPOT_MISC_BDDALLOC_HH
# define SPOT_MISC_BDDALLOC_HH
#include "freelist.hh"
#include <list>
#include <utility>
namespace spot
{
/// Manage ranges of variables.
class bdd_allocator
class bdd_allocator: private free_list
{
public:
/// Default constructor.
......@@ -40,16 +40,16 @@ namespace spot
int allocate_variables(int n);
/// Release \a n BDD variables starting at \a base.
void release_variables(int base, int n);
using free_list::dump_free_list;
protected:
static bool initialized; ///< Whether the BDD library has been initialized.
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);
virtual int extend(int n);
};
}
......
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "freelist.hh"
#include <cassert>
#include <iostream>
namespace spot
{
free_list::~free_list()
{
}
int
free_list::register_n(int n)
{
// Browse the free list until we find N consecutive variables. We
// try not to fragment the list my allocating the variables in the
// smallest free range we find.
free_list_type::iterator best = fl.end();
free_list_type::iterator cur;
for (cur = fl.begin(); cur != fl.end(); ++cur)
{
if (cur->second < n)
continue;
if (n == cur->second)
{
best = cur;
break;
}
if (best == fl.end()
|| cur->second < best->second)
best = cur;
}
// We have found enough free variables.
if (best != fl.end())
{
int result = best->first;
best->second -= n;
assert(best->second >= 0);
// Erase the range if it's now empty.
if (best->second == 0)
fl.erase(best);
else
best->first += n;
return result;
}
// We haven't found enough adjacent free variables;
// ask for some more.
return extend(n);
}
void
free_list::release_n(int base, int n)
{
free_list_type::iterator cur;
int end = base + n;
for (cur = fl.begin(); cur != fl.end(); ++cur)
{
// Append to a range ...
if (cur->first + cur->second == base)
{
cur->second += n;
// Maybe the next item on the list can be merged.
free_list_type::iterator next = cur;
++next;
if (next != fl.end() && next->first == end)
{
cur->second += next->second;
fl.erase(next);
}
return;
}
// ... or prepend to a range ...
if (cur->first == end)
{
cur->first -= n;
cur->second += n;
return;
}
// ... or insert a new range.
if (cur->first > end)
break;
}
fl.insert(cur, pos_lenght_pair(base, n));
}
std::ostream&
free_list::dump_free_list(std::ostream& os) const
{
free_list_type::const_iterator i;
for (i = fl.begin(); i != fl.end(); ++i)
os << " (" << i->first << ", " << i->second << ")";
return os;
}
}
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_MISC_FREELIST_HH
# define SPOT_MISC_FREELIST_HH
#include <list>
#include <utility>
namespace spot
{
/// Manage list of free integers.
class free_list
{
public:
virtual ~free_list();
/// \brief Find \a n consecutive integers.
///
/// Browse the list of free integers until \a n consecutive
/// integers are found. Extend the list (using extend()) otherwise.
/// \return the first integer of the range
int register_n(int n);
/// Release \a n consecutive integers starting at \a base.
void release_n(int base, int n);
/// Dump the list to \a os for debugging.
std::ostream& dump_free_list(std::ostream& os) const;
protected:
/// Allocate \a n integer.
///
/// This function is called by register_n() when the free list is
/// empty or if \a n consecutive integers could not be found. It
/// should allocate more integers, possibly changing the list, and
/// return the first integer on a range of n consecutive integer
/// requested by the user.
virtual int extend(int n) = 0;
/// Such pairs describe \c second free integer starting at \first.
typedef std::pair<int, int> pos_lenght_pair;
typedef std::list<pos_lenght_pair> free_list_type;
free_list_type fl; ///< Tracks unused BDD variables.
};
}
#endif // SPOT_MISC_FREELIST_HH
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
//
......@@ -269,9 +269,7 @@ namespace spot
to_string(fi->first, os) << "]" << std::endl;
}
os << "Free list:" << std::endl;
free_list_type::const_iterator i;
for (i = free_list.begin(); i != free_list.end(); ++i)
os << " (" << i->first << ", " << i->second << ")";
dump_free_list(os);
os << std::endl;
return os;
}
......
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