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/cppext.cxx,v 1.2 2003/05/05 13:45:06 aduret Exp $
32 FILE: cppext.cxx
33 DESCR: C++ extension of BDD package
34 AUTH: Jorn Lind
35 DATE: (C) august 1997
36 *************************************************************************/
37 #include <string.h>
38 #include <stdlib.h>
39 #include <iomanip>
40 #include <new>
41 #include "kernel.h"
42 #include "bvecx.h"
43
44 using namespace std;
45
46 /* Formatting objects for iostreams */
47 #define IOFORMAT_SET 0
48 #define IOFORMAT_TABLE 1
49 #define IOFORMAT_DOT 2
50 #define IOFORMAT_ALL 3
51 #define IOFORMAT_FDDSET 4
52
53 int bdd_ioformat::curformat = IOFORMAT_SET;
54 bdd_ioformat bddset(IOFORMAT_SET);
55 bdd_ioformat bddtable(IOFORMAT_TABLE);
56 bdd_ioformat bdddot(IOFORMAT_DOT);
57 bdd_ioformat bddall(IOFORMAT_ALL);
58 bdd_ioformat fddset(IOFORMAT_FDDSET);
59
60 /* Constant true and false extension */
61 const bddxtrue bddtruepp;
62 const bddxfalse bddfalsepp;
63
64 /* Internal prototypes */
65 static void bdd_printset_rec(ostream&, int, int*);
66 static void bdd_printdot_rec(ostream&, int);
67 static void fdd_printset_rec(ostream &, int, int *);
68
69
70 static bddstrmhandler strmhandler_bdd;
71 static bddstrmhandler strmhandler_fdd;
72
73 // Avoid calling C++ version of anodecount
74 #undef bdd_anodecount
75
76 /*************************************************************************
77 Setup (and shutdown)
78 *************************************************************************/
79
80 #undef bdd_init
81
bdd_cpp_init(int n,int c)82 int bdd_cpp_init(int n, int c)
83 {
84 int ok = bdd_init(n,c);
85
86 strmhandler_bdd = NULL;
87 strmhandler_fdd = NULL;
88
89 return ok;
90 }
91
92
93 /*************************************************************************
94 BDD C++ functions
95 *************************************************************************/
96
bdd_buildcube(int val,int width,const bdd * variables)97 bdd bdd_buildcube(int val, int width, const bdd *variables)
98 {
99 BDD *var = NEW(BDD,width);
100 BDD res;
101 int n;
102
103 // No need for ref.cou. since variables[n] holds the reference
104 for (n=0 ; n<width ; n++)
105 var[n] = variables[n].root;
106
107 res = bdd_buildcube(val, width, var);
108
109 free(var);
110
111 return res;
112 }
113
114
bdd_setbddpairs(bddPair * pair,int * oldvar,const bdd * newvar,int size)115 int bdd_setbddpairs(bddPair *pair, int *oldvar, const bdd *newvar, int size)
116 {
117 if (pair == NULL)
118 return 0;
119
120 for (int n=0,e=0 ; n<size ; n++)
121 if ((e=bdd_setbddpair(pair, oldvar[n], newvar[n].root)) < 0)
122 return e;
123
124 return 0;
125 }
126
127
bdd_anodecountpp(const bdd * r,int num)128 int bdd_anodecountpp(const bdd *r, int num)
129 {
130 BDD *cpr = NEW(BDD,num);
131 int cou;
132 int n;
133
134 // No need for ref.cou. since r[n] holds the reference
135 for (n=0 ; n<num ; n++)
136 cpr[n] = r[n].root;
137
138 cou = bdd_anodecount(cpr,num);
139
140 free(cpr);
141
142 return cou;
143 }
144
145
146 /*************************************************************************
147 C++ iostream operators
148 *************************************************************************/
149
150 /*
151 NAME {* bdd\_strm\_hook *}
152 SECTION {* kernel *}
153 SHORT {* Specifies a printing callback handler *}
154 PROTO {* bddstrmhandler bdd_strm_hook(bddstrmhandler handler) *}
155 DESCR {* A printing callback handler for use with BDDs is used to
156 convert the BDD variable number into something readable by the
157 end user. Typically the handler will print a string name
158 instead of the number. A handler could look like this:
159 \begin{verbatim}
160 void printhandler(ostream &o, int var)
161 {
162 extern char **names;
163 o << names[var];
164 }
165 \end{verbatim}
166
167 \noindent
168 The handler can then be passed to BuDDy like this:
169 {\tt bdd\_strm\_hook(printhandler)}.
170
171 No default handler is supplied. The argument {\tt handler} may be
172 NULL if no handler is needed. *}
173 RETURN {* The old handler *}
174 ALSO {* bdd\_printset, bdd\_file\_hook, fdd\_strm\_hook *}
175 */
bdd_strm_hook(bddstrmhandler handler)176 bddstrmhandler bdd_strm_hook(bddstrmhandler handler)
177 {
178 bddstrmhandler old = strmhandler_bdd;
179 strmhandler_bdd = handler;
180 return old;
181 }
182
183
operator <<(ostream & o,const bdd & r)184 ostream &operator<<(ostream &o, const bdd &r)
185 {
186 if (bdd_ioformat::curformat == IOFORMAT_SET)
187 {
188 if (r.root < 2)
189 {
190 o << (r.root == 0 ? "F" : "T");
191 return o;
192 }
193
194 int *set = new (std::nothrow) int[bddvarnum];
195 if (set == NULL)
196 {
197 bdd_error(BDD_MEMORY);
198 return o;
199 }
200
201 memset(set, 0, sizeof(int) * bddvarnum);
202 bdd_printset_rec(o, r.root, set);
203 delete[] set;
204 }
205 else
206 if (bdd_ioformat::curformat == IOFORMAT_TABLE)
207 {
208 o << "ROOT: " << r.root << "\n";
209 if (r.root < 2)
210 return o;
211
212 bdd_mark(r.root);
213
214 for (int n=0 ; n<bddnodesize ; n++)
215 {
216 if (LEVEL(n) & MARKON)
217 {
218 BddNode *node = &bddnodes[n];
219
220 LEVELp(node) &= MARKOFF;
221
222 o << "[" << setw(5) << n << "] ";
223 if (strmhandler_bdd)
224 strmhandler_bdd(o,bddlevel2var[LEVELp(node)]);
225 else
226 o << setw(3) << bddlevel2var[LEVELp(node)];
227 o << " :";
228 o << " " << setw(3) << LOWp(node);
229 o << " " << setw(3) << HIGHp(node);
230 o << "\n";
231 }
232 }
233 }
234 else
235 if (bdd_ioformat::curformat == IOFORMAT_DOT)
236 {
237 o << "digraph G {\n";
238 o << "0 [shape=box, label=\"0\", style=filled, shape=box, height=0.3, width=0.3];\n";
239 o << "1 [shape=box, label=\"1\", style=filled, shape=box, height=0.3, width=0.3];\n";
240
241 bdd_printdot_rec(o, r.root);
242
243 o << "}\n";
244
245 bdd_unmark(r.root);
246 }
247 else
248 if (bdd_ioformat::curformat == IOFORMAT_FDDSET)
249 {
250 if (ISCONST(r.root))
251 {
252 o << (r == 0 ? "F" : "T");
253 return o;
254 }
255
256 int *set = new (std::nothrow) int[bddvarnum];
257 if (set == NULL)
258 {
259 bdd_error(BDD_MEMORY);
260 return o;
261 }
262
263 memset(set, 0, sizeof(int) * bddvarnum);
264 fdd_printset_rec(o, r.root, set);
265 delete[] set;
266 }
267
268 return o;
269 }
270
271
272 /*
273 NAME {* operator{\tt<<} *}
274 SECTION {* fileio *}
275 SHORT {* C++ output operator for BDDs *}
276 PROTO {* ostream &operator<<(ostream &o, const bdd_ioformat &f)
277 ostream &operator<<(ostream &o, const bdd &r) *}
278 DESCR {* BDDs can be printed in various formats using the C++ iostreams
279 library. The formats are the those used in {\tt bdd\_printset},
280 {\tt bdd\_printtable}, {\tt fdd\_printset} and {\tt bdd\_printdot}.
281 The format can be specified with the following format objects:
282 \begin{tabular}{ll}\\
283 {\tt bddset } & BDD level set format \\
284 {\tt bddtable } & BDD level table format \\
285 {\tt bdddot } & Output for use with Dot \\
286 {\tt bddall } & The whole node table \\
287 {\tt fddset } & FDD level set format \\
288 \end{tabular}\\
289
290 \noindent
291 So a BDD {\tt x} can for example be printed as a table with the
292 command\\
293
294 \indent {\tt cout << bddtable << x << endl}.
295 *}
296 RETURN {* The specified output stream *}
297 ALSO {* bdd\_strm\_hook, fdd\_strm\_hook *}
298 */
operator <<(ostream & o,const bdd_ioformat & f)299 ostream &operator<<(ostream &o, const bdd_ioformat &f)
300 {
301 if (f.format == IOFORMAT_SET || f.format == IOFORMAT_TABLE ||
302 f.format == IOFORMAT_DOT || f.format == IOFORMAT_FDDSET)
303 bdd_ioformat::curformat = f.format;
304 else
305 if (f.format == IOFORMAT_ALL)
306 {
307 for (int n=0 ; n<bddnodesize ; n++)
308 {
309 const BddNode *node = &bddnodes[n];
310
311 if (LOWp(node) != -1)
312 {
313 o << "[" << setw(5) << n << "] ";
314 if (strmhandler_bdd)
315 strmhandler_bdd(o,bddlevel2var[LEVELp(node)]);
316 else
317 o << setw(3) << bddlevel2var[LEVELp(node)] << " :";
318 o << " " << setw(3) << LOWp(node);
319 o << " " << setw(3) << HIGHp(node);
320 o << "\n";
321 }
322 }
323 }
324
325 return o;
326 }
327
328
bdd_printset_rec(ostream & o,int r,int * set)329 static void bdd_printset_rec(ostream& o, int r, int* set)
330 {
331 int n;
332 int first;
333
334 if (r == 0)
335 return;
336 else
337 if (r == 1)
338 {
339 o << "<";
340 first = 1;
341
342 for (n=0 ; n<bddvarnum ; n++)
343 {
344 if (set[n] > 0)
345 {
346 if (!first)
347 o << ", ";
348 first = 0;
349 if (strmhandler_bdd)
350 strmhandler_bdd(o,bddlevel2var[n]);
351 else
352 o << bddlevel2var[n];
353 o << ":" << (set[n]==2 ? 1 : 0);
354 }
355 }
356
357 o << ">";
358 }
359 else
360 {
361 set[LEVEL(r)] = 1;
362 bdd_printset_rec(o, LOW(r), set);
363
364 set[LEVEL(r)] = 2;
365 bdd_printset_rec(o, HIGH(r), set);
366
367 set[LEVEL(r)] = 0;
368 }
369 }
370
371
bdd_printdot_rec(ostream & o,int r)372 static void bdd_printdot_rec(ostream& o, int r)
373 {
374 if (ISCONST(r) || MARKED(r))
375 return;
376
377 o << r << "[label=\"";
378 if (strmhandler_bdd)
379 strmhandler_bdd(o,bddlevel2var[LEVEL(r)]);
380 else
381 o << bddlevel2var[LEVEL(r)];
382 o << "\"];\n";
383 o << r << " -> " << LOW(r) << "[style=dotted];\n";
384 o << r << " -> " << HIGH(r) << "[style=filled];\n";
385
386 SETMARK(r);
387
388 bdd_printdot_rec(o, LOW(r));
389 bdd_printdot_rec(o, HIGH(r));
390 }
391
392
fdd_printset_rec(ostream & o,int r,int * set)393 static void fdd_printset_rec(ostream &o, int r, int *set)
394 {
395 int n,m,i;
396 int used = 0;
397 int *binval;
398 int ok, first;
399
400 if (r == 0)
401 return;
402 else
403 if (r == 1)
404 {
405 o << "<";
406 first=1;
407 int fdvarnum = fdd_domainnum();
408
409 for (n=0 ; n<fdvarnum ; n++)
410 {
411 int firstval=1;
412 used = 0;
413 int binsize = fdd_varnum(n);
414 int *vars = fdd_vars(n);
415
416 for (m=0 ; m<binsize ; m++)
417 if (set[vars[m]] != 0)
418 used = 1;
419
420 if (used)
421 {
422 if (!first)
423 o << ", ";
424 first = 0;
425 if (strmhandler_fdd)
426 strmhandler_fdd(o, n);
427 else
428 o << n;
429 o << ":";
430
431 for (m=0 ; m<(1<<binsize) ; m++)
432 {
433 binval = fdddec2bin(n, m);
434 ok=1;
435
436 for (i=0 ; i<binsize && ok ; i++)
437 if (set[vars[i]] == 1 && binval[i] != 0)
438 ok = 0;
439 else
440 if (set[vars[i]] == 2 && binval[i] != 1)
441 ok = 0;
442
443 if (ok)
444 {
445 if (firstval)
446 o << m;
447 else
448 o << "/" << m;
449 firstval = 0;
450 }
451
452 free(binval);
453 }
454 }
455 }
456
457 o << ">";
458 }
459 else
460 {
461 set[bddlevel2var[LEVEL(r)]] = 1;
462 fdd_printset_rec(o, LOW(r), set);
463
464 set[bddlevel2var[LEVEL(r)]] = 2;
465 fdd_printset_rec(o, HIGH(r), set);
466
467 set[bddlevel2var[LEVEL(r)]] = 0;
468 }
469 }
470
471
472 /*=[ FDD I/O functions ]================================================*/
473
474 /*
475 NAME {* fdd\_strm\_hook *}
476 SECTION {* fdd *}
477 SHORT {* Specifies a printing callback handler *}
478 PROTO {* bddstrmhandler fdd_strm_hook(bddstrmhandler handler) *}
479 DESCR {* A printing callback handler for use with FDDs is used to
480 convert the FDD integer identifier into something readable by the
481 end user. Typically the handler will print a string name
482 instead of the identifier. A handler could look like this:
483 \begin{verbatim}
484 void printhandler(ostream &o, int var)
485 {
486 extern char **names;
487 o << names[var];
488 }
489 \end{verbatim}
490
491 \noindent
492 The handler can then be passed to BuDDy like this:
493 {\tt fdd\_strm\_hook(printhandler)}.
494
495 No default handler is supplied. The argument {\tt handler} may be
496 NULL if no handler is needed. *}
497 RETURN {* The old handler *}
498 ALSO {* fdd\_printset, bdd\_file\_hook *}
499 */
fdd_strm_hook(bddstrmhandler handler)500 bddstrmhandler fdd_strm_hook(bddstrmhandler handler)
501 {
502 bddstrmhandler old = strmhandler_fdd;
503 strmhandler_fdd = handler;
504 return old;
505 }
506
507
508 /*************************************************************************
509 bvec functions
510 *************************************************************************/
511
operator =(const bvec & src)512 bvec bvec::operator=(const bvec &src)
513 {
514 if (&src != this)
515 {
516 bvec_free(roots);
517 roots = bvec_copy(src.roots);
518 }
519 return *this;
520 }
521
522
set(int bitnum,const bdd & b)523 void bvec::set(int bitnum, const bdd &b)
524 {
525 bdd_delref(roots.bitvec[bitnum]);
526 roots.bitvec[bitnum] = b.root;
527 bdd_addref(roots.bitvec[bitnum]);
528 }
529
530
531 /*======================================================================*/
532
bvec_map1(const bvec & a,bdd (* fun)(const bdd &))533 bvec bvec_map1(const bvec &a,
534 bdd (*fun)(const bdd &))
535 {
536 bvec res;
537 int n;
538
539 res = bvec_false(a.bitnum());
540 for (n=0 ; n < a.bitnum() ; n++)
541 res.set(n, fun(a[n]));
542
543 return res;
544 }
545
546
bvec_map2(const bvec & a,const bvec & b,bdd (* fun)(const bdd &,const bdd &))547 bvec bvec_map2(const bvec &a, const bvec &b,
548 bdd (*fun)(const bdd &, const bdd &))
549 {
550 bvec res;
551 int n;
552
553 if (a.bitnum() != b.bitnum())
554 {
555 bdd_error(BVEC_SIZE);
556 return res;
557 }
558
559 res = bvec_false(a.bitnum());
560 for (n=0 ; n < a.bitnum() ; n++)
561 res.set(n, fun(a[n], b[n]));
562
563 return res;
564 }
565
566
bvec_map3(const bvec & a,const bvec & b,const bvec & c,bdd (* fun)(const bdd &,const bdd &,const bdd &))567 bvec bvec_map3(const bvec &a, const bvec &b, const bvec &c,
568 bdd (*fun)(const bdd &, const bdd &, const bdd &))
569 {
570 bvec res;
571 int n;
572
573 if (a.bitnum() != b.bitnum() || b.bitnum() != c.bitnum())
574 {
575 bdd_error(BVEC_SIZE);
576 return res;
577 }
578
579 res = bvec_false(a.bitnum());
580 for (n=0 ; n < a.bitnum() ; n++)
581 res.set(n, fun(a[n], b[n], c[n]) );
582
583 return res;
584 }
585
586
operator <<(ostream & o,const bvec & v)587 ostream &operator<<(ostream &o, const bvec &v)
588 {
589 for (int i=0 ; i<v.bitnum() ; ++i)
590 {
591 o << "B" << i << ":\n"
592 << v[i] << "\n";
593 }
594
595 return o;
596 }
597
598 /* EOF */
599