1 /*========================================================================
2 Copyright (C) 1996-2002 by Jorn Lind-Nielsen
3 All rights reserved
4
5 Permission is hereby granted, without written agreement and without
6 license or royalty fees, to use, reproduce, prepare derivative
7 works, distribute, and display this software and its documentation
8 for any purpose, provided that (1) the above copyright notice and
9 the following two paragraphs appear in all copies of the source code
10 and (2) redistributions, including without limitation binaries,
11 reproduce these notices in the supporting documentation. Substantial
12 modifications to this software may be copyrighted by their authors
13 and need not follow the licensing terms described here, provided
14 that the new terms are clearly indicated in all files where they apply.
15
16 IN NO EVENT SHALL JORN LIND-NIELSEN, OR DISTRIBUTORS OF THIS
17 SOFTWARE BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL,
18 INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS
19 SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE AUTHORS OR ANY OF THE
20 ABOVE PARTIES HAVE BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
21
22 JORN LIND-NIELSEN SPECIFICALLY DISCLAIM ANY WARRANTIES, INCLUDING,
23 BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
24 FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
25 ON AN "AS IS" BASIS, AND THE AUTHORS AND DISTRIBUTORS HAVE NO
26 OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR
27 MODIFICATIONS.
28 ========================================================================*/
29
30 /*************************************************************************
31 $Header: /Volumes/CVS/repository/spot/spot/buddy/src/bvec.h,v 1.2 2003/05/05 13:45:05 aduret Exp $
32 FILE: bvec.h
33 DESCR: Boolean (BDD) vector handling
34 AUTH: Jorn Lind
35 DATE: (C) may 1999
36 *************************************************************************/
37
38 #ifndef _BVECX_H
39 #define _BVECX_H
40
41 #include "fddx.h"
42
43 /* Boolean (BDD) vector */
44 /*
45 NAME {* bvec *}
46 SECTION {* bvec *}
47 SHORT {* A boolean vector *}
48 PROTO {* typedef struct s_bvec
49 {
50 int bitnum;
51 BDD *bitvec;
52 } BVEC;
53
54 typedef BVEC bvec; *}
55 DESCR {* This data structure is used to store boolean vectors. The field
56 {\tt bitnum} is the number of elements in the vector and the
57 field {\tt bitvec} contains the actual BDDs in the vector.
58 The C++ version of {\tt bvec} is documented at the beginning of
59 this document *}
60 */
61 typedef struct s_bvec
62 {
63 int bitnum;
64 BDD *bitvec;
65 } BVEC;
66
67 #ifndef CPLUSPLUS
68 typedef BVEC bvec;
69 #endif
70
71
72 #ifdef CPLUSPLUS
73 extern "C" {
74 #endif
75
76 /* Prototypes for bvec.c */
77 BUDDY_API BVEC bvec_copy(BVEC v);
78 BUDDY_API BVEC bvec_true(int bitnum);
79 BUDDY_API BVEC bvec_false(int bitnum);
80 BUDDY_API BVEC bvec_con(int bitnum, int val);
81 BUDDY_API BVEC bvec_var(int bitnum, int offset, int step);
82 BUDDY_API BVEC bvec_varfdd(int var);
83 BUDDY_API BVEC bvec_varvec(int bitnum, int *var);
84 BUDDY_API BVEC bvec_coerce(int bitnum, BVEC v);
85 BUDDY_API int bvec_isconst(BVEC e) __purefn;
86 BUDDY_API int bvec_val(BVEC e) __purefn;
87 BUDDY_API void bvec_free(BVEC v);
88 BUDDY_API BVEC bvec_addref(BVEC v);
89 BUDDY_API BVEC bvec_delref(BVEC v);
90 BUDDY_API BVEC bvec_map1(BVEC a, BDD (*fun)(BDD));
91 BUDDY_API BVEC bvec_map2(BVEC a, BVEC b, BDD (*fun)(BDD,BDD));
92 BUDDY_API BVEC bvec_map3(BVEC a, BVEC b, BVEC c, BDD (*fun)(BDD,BDD,BDD));
93 BUDDY_API BVEC bvec_add(BVEC left, BVEC right);
94 BUDDY_API BVEC bvec_sub(BVEC left, BVEC right);
95 BUDDY_API BVEC bvec_mulfixed(BVEC e, int c);
96 BUDDY_API BVEC bvec_mul(BVEC left, BVEC right);
97 BUDDY_API int bvec_divfixed(BVEC e, int c, BVEC *res, BVEC *rem);
98 BUDDY_API int bvec_div(BVEC left, BVEC right, BVEC *res, BVEC *rem);
99 BUDDY_API BVEC bvec_ite(BDD a, BVEC b, BVEC c);
100 BUDDY_API BVEC bvec_shlfixed(BVEC e, int pos, BDD c);
101 BUDDY_API BVEC bvec_shl(BVEC l, BVEC r, BDD c);
102 BUDDY_API BVEC bvec_shrfixed(BVEC e, int pos, BDD c);
103 BUDDY_API BVEC bvec_shr(BVEC l, BVEC r, BDD c);
104 BUDDY_API BDD bvec_lth(BVEC left, BVEC right);
105 BUDDY_API BDD bvec_lte(BVEC left, BVEC right);
106 BUDDY_API BDD bvec_gth(BVEC left, BVEC right);
107 BUDDY_API BDD bvec_gte(BVEC left, BVEC right);
108 BUDDY_API BDD bvec_equ(BVEC left, BVEC right);
109 BUDDY_API BDD bvec_neq(BVEC left, BVEC right);
110
111 #ifdef CPLUSPLUS
112 }
113 #endif
114
115
116 /*************************************************************************
117 If this file is included from a C++ compiler then the following
118 classes, wrappers and hacks are supplied.
119 *************************************************************************/
120 #ifdef CPLUSPLUS
121
122 /*=== User BVEC class ==================================================*/
123
124 class BUDDY_API bvec
125 {
126 public:
127
bvec(void)128 bvec(void) { roots.bitvec=NULL; roots.bitnum=0; }
bvec(int bitnum)129 bvec(int bitnum) { roots=bvec_false(bitnum); }
bvec(int bitnum,int val)130 bvec(int bitnum, int val) { roots=bvec_con(bitnum,val); }
bvec(const bvec & v)131 bvec(const bvec &v) { roots=bvec_copy(v.roots); }
~bvec(void)132 ~bvec(void) { bvec_free(roots); }
133
134 void set(int i, const bdd &b);
135 bdd operator[](int i) const { return roots.bitvec[i]; }
bitnum(void)136 int bitnum(void) const { return roots.bitnum; }
empty(void)137 int empty(void) const { return roots.bitnum==0; }
138 bvec operator=(const bvec &src);
139
140 private:
141 BVEC roots;
142
bvec(const BVEC & v)143 bvec(const BVEC &v) { roots=v; } /* NOTE: Must be a shallow copy! */
144
145 friend bvec bvec_truepp(int bitnum);
146 friend bvec bvec_falsepp(int bitnum);
147 friend bvec bvec_conpp(int bitnum, int val);
148 friend bvec bvec_varpp(int bitnum, int offset, int step);
149 friend bvec bvec_varfddpp(int var);
150 friend bvec bvec_varvecpp(int bitnum, int *var);
151 friend bvec bvec_coerce(int bitnum, const bvec &v);
152 friend int bvec_isconst(const bvec &e);
153 friend int bvec_val(const bvec &e);
154 friend bvec bvec_copy(const bvec &v);
155 BUDDY_API
156 friend bvec bvec_map1(const bvec &a,
157 bdd (*fun)(const bdd &));
158 BUDDY_API
159 friend bvec bvec_map2(const bvec &a, const bvec &b,
160 bdd (*fun)(const bdd &, const bdd &));
161 BUDDY_API
162 friend bvec bvec_map3(const bvec &a, const bvec &b, const bvec &c,
163 bdd (*fun)(const bdd &, const bdd &, const bdd &));
164 friend bvec bvec_add(const bvec &left, const bvec &right);
165 friend bvec bvec_sub(const bvec &left, const bvec &right);
166 friend bvec bvec_mulfixed(const bvec &e, int c);
167 friend bvec bvec_mul(const bvec &left, const bvec &right);
168 friend int bvec_divfixed(const bvec &e, int c, bvec &res, bvec &rem);
169 friend int bvec_div(const bvec &l, const bvec &r, bvec &res, bvec &rem);
170 friend bvec bvec_ite(const bdd& a, const bvec& b, const bvec& c);
171 friend bvec bvec_shlfixed(const bvec &e, int pos, const bdd &c);
172 friend bvec bvec_shl(const bvec &left, const bvec &right, const bdd &c);
173 friend bvec bvec_shrfixed(const bvec &e, int pos, const bdd &c);
174 friend bvec bvec_shr(const bvec &left, const bvec &right, const bdd &c);
175 friend bdd bvec_lth(const bvec &left, const bvec &right);
176 friend bdd bvec_lte(const bvec &left, const bvec &right);
177 friend bdd bvec_gth(const bvec &left, const bvec &right);
178 friend bdd bvec_gte(const bvec &left, const bvec &right);
179 friend bdd bvec_equ(const bvec &left, const bvec &right);
180 friend bdd bvec_neq(const bvec &left, const bvec &right);
181
182 public:
183 bvec operator&(const bvec &a) const { return bvec_map2(*this, a, bdd_and); }
184 bvec operator^(const bvec &a) const { return bvec_map2(*this, a, bdd_xor); }
185 bvec operator|(const bvec &a) const { return bvec_map2(*this, a, bdd_or); }
186 bvec operator!(void) const { return bvec_map1(*this, bdd_not); }
187 bvec operator<<(int a) const { return bvec_shlfixed(*this,a,bddfalse); }
188 bvec operator<<(const bvec &a) const { return bvec_shl(*this,a,bddfalse); }
189 bvec operator>>(int a) const { return bvec_shrfixed(*this,a,bddfalse); }
190 bvec operator>>(const bvec &a) const { return bvec_shr(*this,a,bddfalse); }
191 bvec operator+(const bvec &a) const { return bvec_add(*this, a); }
192 bvec operator-(const bvec &a) const { return bvec_sub(*this, a); }
193 bvec operator*(int a) const { return bvec_mulfixed(*this, a); }
194 bvec operator*(const bvec a) const { return bvec_mul(*this, a); }
195 bdd operator<(const bvec &a) const { return bvec_lth(*this, a); }
196 bdd operator<=(const bvec &a) const { return bvec_lte(*this, a); }
197 bdd operator>(const bvec &a) const { return bvec_gth(*this, a); }
198 bdd operator>=(const bvec &a) const { return bvec_gte(*this, a); }
199 bdd operator==(const bvec &a) const { return bvec_equ(*this, a); }
200 bdd operator!=(const bvec &a) const { return bvec_neq(*this, a); }
201 };
202
203 BUDDY_API std::ostream &operator<<(std::ostream &, const bvec &);
204
bvec_truepp(int bitnum)205 inline bvec bvec_truepp(int bitnum)
206 { return bvec_true(bitnum); }
207
bvec_falsepp(int bitnum)208 inline bvec bvec_falsepp(int bitnum)
209 { return bvec_false(bitnum); }
210
bvec_conpp(int bitnum,int val)211 inline bvec bvec_conpp(int bitnum, int val)
212 { return bvec_con(bitnum, val); }
213
bvec_varpp(int bitnum,int offset,int step)214 inline bvec bvec_varpp(int bitnum, int offset, int step)
215 { return bvec_var(bitnum, offset, step); }
216
bvec_varfddpp(int var)217 inline bvec bvec_varfddpp(int var)
218 { return bvec_varfdd(var); }
219
bvec_varvecpp(int bitnum,int * var)220 inline bvec bvec_varvecpp(int bitnum, int *var)
221 { return bvec_varvec(bitnum, var); }
222
bvec_coerce(int bitnum,const bvec & v)223 inline bvec bvec_coerce(int bitnum, const bvec &v)
224 { return bvec_coerce(bitnum, v.roots); }
225
bvec_isconst(const bvec & e)226 inline int bvec_isconst(const bvec &e)
227 { return bvec_isconst(e.roots); }
228
bvec_val(const bvec & e)229 inline int bvec_val(const bvec &e)
230 { return bvec_val(e.roots); }
231
bvec_copy(const bvec & v)232 inline bvec bvec_copy(const bvec &v)
233 { return bvec_copy(v.roots); }
234
bvec_add(const bvec & left,const bvec & right)235 inline bvec bvec_add(const bvec &left, const bvec &right)
236 { return bvec_add(left.roots, right.roots); }
237
bvec_sub(const bvec & left,const bvec & right)238 inline bvec bvec_sub(const bvec &left, const bvec &right)
239 { return bvec_sub(left.roots, right.roots); }
240
bvec_mulfixed(const bvec & e,int c)241 inline bvec bvec_mulfixed(const bvec &e, int c)
242 { return bvec_mulfixed(e.roots, c); }
243
bvec_mul(const bvec & left,const bvec & right)244 inline bvec bvec_mul(const bvec &left, const bvec &right)
245 { return bvec_mul(left.roots, right.roots); }
246
bvec_divfixed(const bvec & e,int c,bvec & res,bvec & rem)247 inline int bvec_divfixed(const bvec &e, int c, bvec &res, bvec &rem)
248 { return bvec_divfixed(e.roots, c, &res.roots, &rem.roots); }
249
bvec_div(const bvec & l,const bvec & r,bvec & res,bvec & rem)250 inline int bvec_div(const bvec &l, const bvec &r, bvec &res, bvec &rem)
251 { return bvec_div(l.roots, r.roots, &res.roots, &rem.roots); }
252
bvec_ite(const bdd & a,const bvec & b,const bvec & c)253 inline bvec bvec_ite(const bdd& a, const bvec& b, const bvec& c)
254 { return bvec_ite(a.root, b.roots, c.roots); }
255
bvec_shlfixed(const bvec & e,int pos,const bdd & c)256 inline bvec bvec_shlfixed(const bvec &e, int pos, const bdd &c)
257 { return bvec_shlfixed(e.roots, pos, c.root); }
258
bvec_shl(const bvec & left,const bvec & right,const bdd & c)259 inline bvec bvec_shl(const bvec &left, const bvec &right, const bdd &c)
260 { return bvec_shl(left.roots, right.roots, c.root); }
261
bvec_shrfixed(const bvec & e,int pos,const bdd & c)262 inline bvec bvec_shrfixed(const bvec &e, int pos, const bdd &c)
263 { return bvec_shrfixed(e.roots, pos, c.root); }
264
bvec_shr(const bvec & left,const bvec & right,const bdd & c)265 inline bvec bvec_shr(const bvec &left, const bvec &right, const bdd &c)
266 { return bvec_shr(left.roots, right.roots, c.root); }
267
bvec_lth(const bvec & left,const bvec & right)268 inline bdd bvec_lth(const bvec &left, const bvec &right)
269 { return bvec_lth(left.roots, right.roots); }
270
bvec_lte(const bvec & left,const bvec & right)271 inline bdd bvec_lte(const bvec &left, const bvec &right)
272 { return bvec_lte(left.roots, right.roots); }
273
bvec_gth(const bvec & left,const bvec & right)274 inline bdd bvec_gth(const bvec &left, const bvec &right)
275 { return bvec_gth(left.roots, right.roots); }
276
bvec_gte(const bvec & left,const bvec & right)277 inline bdd bvec_gte(const bvec &left, const bvec &right)
278 { return bvec_gte(left.roots, right.roots); }
279
bvec_equ(const bvec & left,const bvec & right)280 inline bdd bvec_equ(const bvec &left, const bvec &right)
281 { return bvec_equ(left.roots, right.roots); }
282
bvec_neq(const bvec & left,const bvec & right)283 inline bdd bvec_neq(const bvec &left, const bvec &right)
284 { return bvec_neq(left.roots, right.roots); }
285
286
287 /* Hack to allow for overloading */
288 #define bvec_var(a,b,c) bvec_varpp(a,b,c)
289 #define bvec_varfdd(a) bvec_varfddpp(a)
290 #define bvec_varvec(a,b) bvec_varvecpp(a,b)
291 #define bvec_true(a) bvec_truepp(a)
292 #define bvec_false(a) bvec_falsepp(a)
293 #define bvec_con(a,b) bvec_conpp((a),(b))
294
295
296 #endif /* CPLUSPLUS */
297
298 #endif /* _BVECX_H */
299
300 /* EOF */
301