bddalloc.cc 2.67 KB
Newer Older
1
// Copyright (C) 2003, 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// dpartement Systmes Rpartis Coopratifs (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.

22
23
24
25
26
27
28
29
30
31
32
#include <bdd.h>
#include <cassert>
#include "bddalloc.hh"

namespace spot
{
  bool bdd_allocator::initialized = false;

  bdd_allocator::bdd_allocator()
  {
    initialize();
33
    lvarnum = bdd_varnum();
34
    fl.push_front(pos_lenght_pair(0, lvarnum));
35
36
37
38
39
40
41
42
  }

  void
  bdd_allocator::initialize()
  {
    if (initialized)
      return;
    initialized = true;
43
44
45
46
47
    // 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);
48
    bdd_setvarnum(2);
49
50
  }

51
52
53
  void
  bdd_allocator::extvarnum(int more)
  {
54
55
56
    int varnum = bdd_varnum();
    // If varnum has been extended from another allocator (or
    // externally), use the new variables.
57
58
59
60
61
62
63
64
65
66
67
68
69
70
    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;
      }
  }

71
72
73
  int
  bdd_allocator::allocate_variables(int n)
  {
74
75
    return register_n(n);
  }
76

77
78
79
80
81
  void
  bdd_allocator::release_variables(int base, int n)
  {
    release_n(base, n);
  }
82

83
84
85
  int
  bdd_allocator::extend(int n)
  {
86
87
    // If we already have some free variable at the end
    // of the variable space, allocate just the difference.
88
    if (!fl.empty() && fl.back().first + fl.back().second == lvarnum)
89
      {
90
91
	int res = fl.back().first;
	int endvar = fl.back().second;
92
	assert(n > endvar);
93
	extvarnum(n - endvar);
94
	fl.pop_back();
95
96
97
98
99
	return res;
      }
    else
      {
	// Otherwise, allocate as much variables as we need.
100
101
	int res = lvarnum;
	extvarnum(n);
102
103
104
105
	return res;
      }
  }
}