1 /*
2
3 This file is part of the Maude 2 interpreter.
4
5 Copyright 1997-2003 SRI International, Menlo Park, CA 94025, USA.
6
7 This program is free software; you can redistribute it and/or modify
8 it under the terms of the GNU General Public License as published by
9 the Free Software Foundation; either version 2 of the License, or
10 (at your option) any later version.
11
12 This program is distributed in the hope that it will be useful,
13 but WITHOUT ANY WARRANTY; without even the implied warranty of
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 GNU General Public License for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software
19 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.
20
21 */
22
23 //
24 // Class to manage a single BDD package for multiple users.
25 //
26 #ifndef _bddUser_hh_
27 #define _bddUser_hh_
28 #include "bdd.h"
29
30 class BddUser
31 {
32 public:
33 typedef void ErrorHandler(int errorNr);
34
35 BddUser();
36 ~BddUser();
37
38 static bdd ithvar(int i);
39 static bdd nithvar(int i);
40 static void setNrVariables(int nrVariables);
41 static void dump(ostream& s, bdd root);
42 static void setErrorHandler(ErrorHandler* errHandler);
43
44 static bddPair* getCachedPairing();
45
46 private:
47 enum Constants
48 {
49 DEFAULT_NODE_SIZE = 1000,
50 DEFAULT_CACHE_SIZE = 100,
51 DEFAULT_NR_VARIABLES = 10
52 };
53
54 static void gc_handler(int pre, bddGbcStat* stat);
55 static void err_handler(int errcode);
56
57 static int nrUsers;
58
59 static ErrorHandler* errorHandler;
60 //
61 // These structures are expensive to create and destroy so we keep
62 // a cached one and delete it every time the number of variables
63 // increases so it is always the correct size if it exists.
64 //
65 // If code uses this structure, it must be finished with it and
66 // leave it in a clean state (all variables pointing to something
67 // innocuous such as bdd_false() before calling other code that
68 // could potentially use it.
69 //
70 static bddPair* cachedPairing;
71 };
72
73 inline bdd
ithvar(int i)74 BddUser::ithvar(int i)
75 {
76 if (i >= bdd_varnum())
77 bdd_setvarnum(i + 1);
78 return bdd_ithvar(i);
79 }
80
81 inline bdd
nithvar(int i)82 BddUser::nithvar(int i)
83 {
84 if (i >= bdd_varnum())
85 bdd_setvarnum(i + 1);
86 return bdd_nithvar(i);
87 }
88
89 inline void
setNrVariables(int nrVariables)90 BddUser::setNrVariables(int nrVariables)
91 {
92 if (nrVariables > bdd_varnum())
93 {
94 if (cachedPairing != 0)
95 {
96 //
97 // Existing cached pair structure will be the wrong size.
98 //
99 bdd_freepair(cachedPairing);
100 cachedPairing = 0;
101 }
102 bdd_setvarnum(nrVariables);
103 }
104 }
105
106 inline void
setErrorHandler(ErrorHandler * errHandler)107 BddUser::setErrorHandler(ErrorHandler* errHandler)
108 {
109 errorHandler = errHandler;
110 }
111
112 inline bddPair*
getCachedPairing()113 BddUser::getCachedPairing()
114 {
115 if (cachedPairing == 0)
116 cachedPairing = bdd_newpair();
117 return cachedPairing;
118 }
119
120 #endif
121