alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Move bdd_allocator to src/priv/.

Browse source 
* src/misc/bddalloc.cc, src/misc/bddalloc.hh,
src/misc/freelist.cc, src/misc/freelist.hh: Move ...
* src/priv/bddalloc.cc, src/priv/bddalloc.hh,
src/priv/freelist.cc, src/priv/freelist.hh: ... here.
* src/misc/Makefile.am, src/priv/Makefile.am: Adjust.
* src/tgba/bdddict.cc: Adjust include.
* src/tgbaalgos/ltl2tgba_fm.cc: Remove useless include.
This commit is contained in:
Alexandre Duret-Lutz 2013-06-24 23:45:06 +02:00
parent 9775dfdd4b
commit 1ed43038e8
8 changed files with 21 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/misc/Makefile.am
View file

@ -30,7 +30,6 @@ DISTCLEANFILES = _config.h
misc_HEADERS = \
bareword.hh \
bddalloc.hh \
bddlt.hh \
bddop.hh \
casts.hh \
@ -38,7 +37,6 @@ misc_HEADERS = \
escape.hh \
fixpool.hh \
formater.hh \
freelist.hh \
hash.hh \
hashfunc.hh \
intvcomp.hh \
@ -56,11 +54,9 @@ misc_HEADERS = \
noinst_LTLIBRARIES = libmisc.la
libmisc_la_SOURCES = \
bareword.cc \
bddalloc.cc \
bddop.cc \
escape.cc \
formater.cc \
freelist.cc \
intvcomp.cc \
intvcmp2.cc \
memusage.cc \

115
src/misc/bddalloc.cc
View file

@ -1,115 +0,0 @@
// Copyright (C) 2007, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006, 2007 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#include <bdd.h>
#include <cassert>
#include "bddalloc.hh"
namespace spot
{
bool bdd_allocator::initialized = false;
bdd_allocator::bdd_allocator()
{
initialize();
lvarnum = bdd_varnum();
fl.push_front(pos_lenght_pair(0, lvarnum));
}
void
bdd_allocator::initialize()
{
if (initialized)
return;
initialized = true;
// Buddy might have been initialized by a third-party library.
if (bdd_isrunning())
return;
// The values passed to bdd_init should depends on the problem
// the library is solving. It would be nice to allow users
// to tune this. By the meantime, we take the typical values
// for large examples advocated by the BuDDy manual.
bdd_init(1000000, 10000);
bdd_setvarnum(2);
// Disable the default GC handler. (Note that this will only be
// done if Buddy is initialized by Spot. Otherwise we prefer not
// to overwrite a handler that might have been set by the user.)
bdd_gbc_hook(0);
// When the node time is full, add 500000 nodes, i.e., 10MB.
bdd_setmaxincrease(500000);
}
void
bdd_allocator::extvarnum(int more)
{
int varnum = bdd_varnum();
// If varnum has been extended from another allocator (or
// externally), 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)
{
return register_n(n);
}
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 (!fl.empty() && fl.back().first + fl.back().second == lvarnum)
{
int res = fl.back().first;
int endvar = fl.back().second;
assert(n > endvar);
extvarnum(n - endvar);
fl.pop_back();
return res;
}
else
{
// Otherwise, allocate as much variables as we need.
int res = lvarnum;
extvarnum(n);
return res;
}
}
}

55
src/misc/bddalloc.hh
View file

@ -1,55 +0,0 @@
// Copyright (C) 2003, 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#ifndef SPOT_MISC_BDDALLOC_HH
# define SPOT_MISC_BDDALLOC_HH
#include "freelist.hh"
#include <list>
#include <utility>
namespace spot
{
/// \ingroup misc_tools
/// \brief Manage ranges of variables.
class bdd_allocator: private free_list
{
public:
/// Default constructor.
bdd_allocator();
/// Initialize the BDD library.
static void initialize();
/// Allocate \a n BDD variables.
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.
int lvarnum; ///< number of variables in use in this allocator.
private:
/// Require more variables.
void extvarnum(int more);
virtual int extend(int n);
};
}
#endif // SPOT_MISC_BDDALLOC_HH

218
src/misc/freelist.cc
View file

@ -1,218 +0,0 @@
// Copyright (C) 2004, 2006 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#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;
remove(best, result, n);
return result;
}
// We haven't found enough adjacent free variables;
// ask for some more.
return extend(n);
}
void
free_list::insert(int base, int n)
{
free_list_type::iterator cur;
int end = base + n;
for (cur = fl.begin(); cur != fl.end(); ++cur)
{
int cend = cur->first + cur->second;
// cur [...]
// to insert [...]
// -----------------------
// result [...] [...]
// (Insert a new range, unconnected.)
if (cur->first > end)
{
break;
}
// cur [...]
// to insert [...]
// -----------------------
// result unknown : we should look at the rest of the freelist.
else if (base > cend)
{
continue;
}
// cur [....[ [......[
// to insert [....[ [..[
// ----------------------------------
// result [......[ [......[
else if (cur->first <= base)
{
if (cend >= end)
// second case : nothing to do
return;
// cur->second is set below.
}
// cur [....[ [..[
// to insert [....[ [.......[
// ----------------------------------
// result [......[ [.......[
else
{
cur->first = base;
// cur->second is set below.
}
// We get here in one of these three situations:
//
// cur [....[ [....[ [..[
// to insert [....[ [....[ [.......[
// -------------------------------------------
// result [......[ [......[ [.......[
//
// cur->first is already set, be cur->second has yet to be.
end = std::max(cend, end);
cur->second = end - cur->first;
// Since we have extended the current range, maybe the next
// items on the list should be merged.
free_list_type::iterator next = cur;
++next;
while (next != fl.end() && next->first <= end)
{
end = std::max(next->first + next->second, end);
cur->second = end - cur->first;
free_list_type::iterator next2 = next++;
fl.erase(next2);
}
return;
}
// We reach this place either because a new unconnected range
// should be inserted in the middle of FL, or at the end.
fl.insert(cur, pos_lenght_pair(base, n));
}
void
free_list::remove(int base, int n)
{
free_list_type::iterator cur = fl.begin();
int end = base + n;
while (cur != fl.end() && cur->first < end)
{
int cend = cur->first + cur->second;
// Remove may invalidate the current iterator, so advance it first.
free_list_type::iterator old = cur++;
if (cend >= base)
{
int newbase = std::max(base, old->first);
int q = std::min(cend, end) - newbase;
remove(old, newbase, q);
}
}
}
void
free_list::remove(free_list_type::iterator i, int base, int n)
{
if (base == i->first)
{
// Removing at the beginning of the range
i->second -= n;
assert(i->second >= 0);
// Erase the range if it's now empty.
if (i->second == 0)
fl.erase(i);
else
i->first += n;
}
else if (base + n == i->first + i->second)
{
// Removing at the end of the range
i->second -= n;
assert(i->second > 0); // cannot be empty because base != i->first
}
else
{
// Removing in the middle of a range.
int b1 = i->first;
int n1 = base - i->first;
int n2 = i->first + i->second - base - n;
assert(n1 > 0);
assert(n2 > 0);
*i = pos_lenght_pair(base + n, n2);
fl.insert(i, pos_lenght_pair(b1, n1));
}
}
void
free_list::release_n(int base, int n)
{
insert(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;
}
int
free_list::free_count() const
{
int res = 0;
free_list_type::const_iterator i;
for (i = fl.begin(); i != fl.end(); ++i)
res += i->second;
return res;
}
}

84
src/misc/freelist.hh
View file

@ -1,84 +0,0 @@
// Copyright (C) 2008 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004, 2006 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#ifndef SPOT_MISC_FREELIST_HH
# define SPOT_MISC_FREELIST_HH
#include <list>
#include <utility>
#include <iosfwd>
namespace spot
{
/// \ingroup misc_tools
/// \brief 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;
/// Extend the list by inserting a new pos-lenght pair.
void insert(int base, int n);
/// Remove \a n consecutive entries from the list, starting at \a base.
void remove(int base, int n = 0);
/// Return the number of free integers on the list.
int free_count() 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 \c 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.
/// Remove \a n consecutive entries from the list, starting at \a base.
void remove(free_list_type::iterator i, int base, int n);
};
}
#endif // SPOT_MISC_FREELIST_HH