source: vis_dev/glu-2.1/src/calBdd/calExtDet.html@ 8

Last change on this file since 8 was 8, checked in by cecile, 15 years ago

src glu
File size: 42.8 KB
Line 
1<HTML>
2<HEAD><TITLE>The cal package</TITLE></HEAD>
3<BODY>
4
5<DL>
6<dt><pre>
7<A NAME="Cal_AssociationInit"></A>
8int <I></I>
9<B>Cal_AssociationInit</B>(
10 Cal_BddManager <b>bddManager</b>, <i></i>
11 Cal_Bdd * <b>associationInfoUserBdds</b>, <i></i>
12 int <b>pairs</b> <i></i>
13)
14</pre>
15<dd> Creates or finds a variable association. The association is
16 specified by associationInfo, which is a an array of BDD with
17 Cal_BddNull(bddManager) as the end marker. If pairs is 0, the array is
18 assumed to be an array of variables. In this case, each variable is paired
19 with constant BDD one. Such an association may viewed as specifying a set
20 of variables for use with routines such as Cal_BddExists. If pair is not 0,
21 then the even numbered array elements should be variables and the odd numbered
22 elements should be the BDDs which they are mapped to. In both cases, the
23 return value is an integer identifier for this association. If the given
24 association is equivalent to one which already exists, the same identifier
25 is used for both, and the reference count of the association is increased by
26 one.
27<p>
28
29<dd> <b>Side Effects</b> None
30<p>
31
32<dd> <b>See Also</b> <code><a href="#Cal_AssociationQuit">Cal_AssociationQuit</a>
33</code>
34
35<dt><pre>
36<A NAME="Cal_AssociationQuit"></A>
37void <I></I>
38<B>Cal_AssociationQuit</B>(
39 Cal_BddManager <b>bddManager</b>, <i></i>
40 int <b>associationId</b> <i></i>
41)
42</pre>
43<dd> Decrements the reference count of the variable association with
44 identifier id, and frees it if the reference count becomes zero.
45<p>
46
47<dd> <b>Side Effects</b> None
48<p>
49
50<dd> <b>See Also</b> <code><a href="#Cal_AssociationInit">Cal_AssociationInit</a>
51</code>
52
53<dt><pre>
54<A NAME="Cal_AssociationSetCurrent"></A>
55int <I></I>
56<B>Cal_AssociationSetCurrent</B>(
57 Cal_BddManager <b>bddManager</b>, <i></i>
58 int <b>associationId</b> <i></i>
59)
60</pre>
61<dd> Sets the current variable association to the one given by id and
62 returns the ID of the old association. An id of -1 indicates the temporary
63 association
64<p>
65
66<dd> <b>Side Effects</b> None
67<p>
68
69<dt><pre>
70<A NAME="Cal_BddAnd"></A>
71Cal_Bdd <I></I>
72<B>Cal_BddAnd</B>(
73 Cal_BddManager <b>bddManager</b>, <i></i>
74 Cal_Bdd <b>fUserBdd</b>, <i></i>
75 Cal_Bdd <b>gUserBdd</b> <i></i>
76)
77</pre>
78<dd> Returns the BDD for logical AND of f and g
79<p>
80
81<dd> <b>Side Effects</b> None
82<p>
83
84<dt><pre>
85<A NAME="Cal_BddBetween"></A>
86Cal_Bdd <I></I>
87<B>Cal_BddBetween</B>(
88 Cal_BddManager <b>bddManager</b>, <i></i>
89 Cal_Bdd <b>fMinUserBdd</b>, <i></i>
90 Cal_Bdd <b>fMaxUserBdd</b> <i></i>
91)
92</pre>
93<dd> Returns a minimal BDD f which is contains fMin and is
94 contained in fMax ( fMin <= f <= fMax).
95 This operation is typically used in state space searches to simplify
96 the representation for the set of states wich will be expanded at
97 each step (Rk Rk-1' <= f <= Rk).
98<p>
99
100<dd> <b>Side Effects</b> None
101<p>
102
103<dd> <b>See Also</b> <code><a href="#Cal_BddReduce">Cal_BddReduce</a>
104</code>
105
106<dt><pre>
107<A NAME="Cal_BddCofactor"></A>
108Cal_Bdd <I></I>
109<B>Cal_BddCofactor</B>(
110 Cal_BddManager <b>bddManager</b>, <i></i>
111 Cal_Bdd <b>fUserBdd</b>, <i></i>
112 Cal_Bdd <b>cUserBdd</b> <i></i>
113)
114</pre>
115<dd> Returns the generalized cofactor of BDD f with respect
116 to BDD c. The constrain operator given by Coudert et al (ICCAD90) is
117 used to find the generalized cofactor.
118<p>
119
120<dd> <b>Side Effects</b> None.
121<p>
122
123<dd> <b>See Also</b> <code><a href="#Cal_BddReduce">Cal_BddReduce</a>
124</code>
125
126<dt><pre>
127<A NAME="Cal_BddCompose"></A>
128Cal_Bdd <I></I>
129<B>Cal_BddCompose</B>(
130 Cal_BddManager <b>bddManager</b>, <i></i>
131 Cal_Bdd <b>fUserBdd</b>, <i></i>
132 Cal_Bdd <b>gUserBdd</b>, <i></i>
133 Cal_Bdd <b>hUserBdd</b> <i></i>
134)
135</pre>
136<dd> Returns the BDD obtained by substituting a variable by a function
137<p>
138
139<dd> <b>Side Effects</b> None
140<p>
141
142<dt><pre>
143<A NAME="Cal_BddDependsOn"></A>
144int <I></I>
145<B>Cal_BddDependsOn</B>(
146 Cal_BddManager <b>bddManager</b>, <i></i>
147 Cal_Bdd <b>fUserBdd</b>, <i></i>
148 Cal_Bdd <b>varUserBdd</b> <i></i>
149)
150</pre>
151<dd> Returns 1 if f depends on var and returns 0 otherwise.
152<p>
153
154<dd> <b>Side Effects</b> None
155<p>
156
157<dt><pre>
158<A NAME="Cal_BddDumpBdd"></A>
159int <I></I>
160<B>Cal_BddDumpBdd</B>(
161 Cal_BddManager <b>bddManager</b>, <i></i>
162 Cal_Bdd <b>fUserBdd</b>, <i></i>
163 Cal_Bdd * <b>userVars</b>, <i></i>
164 FILE * <b>fp</b> <i></i>
165)
166</pre>
167<dd> Writes an encoded description of the BDD to the file given by fp.
168 The argument vars should be a null-terminated array of variables that include
169 the support of f . These variables need not be in order of increasing index.
170 The function returns a nonzero value if f was written to the file successfully.
171<p>
172
173<dd> <b>Side Effects</b> required
174<p>
175
176<dd> <b>See Also</b> <code>optional
177</code>
178
179<dt><pre>
180<A NAME="Cal_BddDynamicReordering"></A>
181void <I></I>
182<B>Cal_BddDynamicReordering</B>(
183 Cal_BddManager <b>bddManager</b>, <i></i>
184 int <b>technique</b> <i></i>
185)
186</pre>
187<dd> Selects the method for dynamic reordering.
188<p>
189
190<dd> <b>Side Effects</b> None
191<p>
192
193<dd> <b>See Also</b> <code><a href="#Cal_BddReorder">Cal_BddReorder</a>
194</code>
195
196<dt><pre>
197<A NAME="Cal_BddElse"></A>
198Cal_Bdd <I></I>
199<B>Cal_BddElse</B>(
200 Cal_BddManager <b>bddManager</b>, <i></i>
201 Cal_Bdd <b>userBdd</b> <i></i>
202)
203</pre>
204<dd> Returns the negative cofactor of the argument BDD with
205 respect to the top variable of the BDD.
206<p>
207
208<dd> <b>Side Effects</b> The reference count of the returned BDD is increased by 1.
209<p>
210
211<dd> <b>See Also</b> <code><a href="#Cal_BddThen">Cal_BddThen</a>
212</code>
213
214<dt><pre>
215<A NAME="Cal_BddExists"></A>
216Cal_Bdd <I></I>
217<B>Cal_BddExists</B>(
218 Cal_BddManager <b>bddManager</b>, <i></i>
219 Cal_Bdd <b>fUserBdd</b> <i></i>
220)
221</pre>
222<dd> Returns the BDD for f with all the variables that are
223 paired with something in the current variable association
224 existentially quantified out.
225<p>
226
227<dd> <b>Side Effects</b> None.
228<p>
229
230<dd> <b>See Also</b> <code><a href="#Cal_BddRelProd">Cal_BddRelProd</a>
231</code>
232
233<dt><pre>
234<A NAME="Cal_BddForAll"></A>
235Cal_Bdd <I></I>
236<B>Cal_BddForAll</B>(
237 Cal_BddManager <b>bddManager</b>, <i></i>
238 Cal_Bdd <b>fUserBdd</b> <i></i>
239)
240</pre>
241<dd> Returns the BDD for f with all the variables that are
242 paired with something in the current variable association
243 universally quantified out.
244<p>
245
246<dd> <b>Side Effects</b> None.
247<p>
248
249<dt><pre>
250<A NAME="Cal_BddFree"></A>
251void <I></I>
252<B>Cal_BddFree</B>(
253 Cal_BddManager <b>bddManager</b>, <i></i>
254 Cal_Bdd <b>userBdd</b> <i></i>
255)
256</pre>
257<dd> Frees the argument BDD. It is an error to free a BDD
258 more than once.
259<p>
260
261<dd> <b>Side Effects</b> The reference count of the argument BDD is decreased by 1.
262<p>
263
264<dd> <b>See Also</b> <code><a href="#Cal_BddUnFree">Cal_BddUnFree</a>
265</code>
266
267<dt><pre>
268<A NAME="Cal_BddFunctionPrint"></A>
269void <I></I>
270<B>Cal_BddFunctionPrint</B>(
271 Cal_BddManager <b>bddManager</b>, <i></i>
272 Cal_Bdd <b>userBdd</b>, <i></i>
273 char * <b>name</b> <i></i>
274)
275</pre>
276<dd> Prints the function implemented by the argument BDD
277<p>
278
279<dd> <b>Side Effects</b> None
280<p>
281
282<dt><pre>
283<A NAME="Cal_BddFunctionProfileMultiple"></A>
284void <I></I>
285<B>Cal_BddFunctionProfileMultiple</B>(
286 Cal_BddManager <b>bddManager</b>, <i></i>
287 Cal_Bdd * <b>fUserBddArray</b>, <i></i>
288 long * <b>funcCounts</b> <i></i>
289)
290</pre>
291<dd> optional
292<p>
293
294<dd> <b>Side Effects</b> None
295<p>
296
297<dd> <b>See Also</b> <code>optional
298</code>
299
300<dt><pre>
301<A NAME="Cal_BddFunctionProfile"></A>
302void <I></I>
303<B>Cal_BddFunctionProfile</B>(
304 Cal_BddManager <b>bddManager</b>, <i></i>
305 Cal_Bdd <b>fUserBdd</b>, <i></i>
306 long * <b>funcCounts</b> <i></i>
307)
308</pre>
309<dd> The nth entry of the function
310 profile array is the number of subfunctions of f which may be obtained by
311 restricting the variables whose index is less than n. An entry of zero
312 indicates that f is independent of the variable with the corresponding index.
313<p>
314
315<dd> <b>See Also</b> <code>optional
316</code>
317
318<dt><pre>
319<A NAME="Cal_BddGetIfId"></A>
320Cal_BddId_t <I></I>
321<B>Cal_BddGetIfId</B>(
322 Cal_BddManager <b>bddManager</b>, <i></i>
323 Cal_Bdd <b>userBdd</b> <i></i>
324)
325</pre>
326<dd> Returns the id of the top variable of the argument BDD.
327<p>
328
329<dd> <b>Side Effects</b> None
330<p>
331
332<dd> <b>See Also</b> <code><a href="#Cal_BddGetIfIndex">Cal_BddGetIfIndex</a>
333</code>
334
335<dt><pre>
336<A NAME="Cal_BddGetIfIndex"></A>
337Cal_BddId_t <I></I>
338<B>Cal_BddGetIfIndex</B>(
339 Cal_BddManager <b>bddManager</b>, <i></i>
340 Cal_Bdd <b>userBdd</b> <i></i>
341)
342</pre>
343<dd> Returns the index of the top variable of the argument BDD.
344<p>
345
346<dd> <b>Side Effects</b> None
347<p>
348
349<dd> <b>See Also</b> <code><a href="#Cal_BddGetIfId">Cal_BddGetIfId</a>
350</code>
351
352<dt><pre>
353<A NAME="Cal_BddGetRegular"></A>
354Cal_Bdd <I></I>
355<B>Cal_BddGetRegular</B>(
356 Cal_BddManager <b>bddManager</b>, <i></i>
357 Cal_Bdd <b>userBdd</b> <i></i>
358)
359</pre>
360<dd> Returns a BDD with positive from a given BDD with arbitrary phase
361<p>
362
363<dd> <b>Side Effects</b> None.
364<p>
365
366<dt><pre>
367<A NAME="Cal_BddITE"></A>
368Cal_Bdd <I></I>
369<B>Cal_BddITE</B>(
370 Cal_BddManager <b>bddManager</b>, <i></i>
371 Cal_Bdd <b>fUserBdd</b>, <i></i>
372 Cal_Bdd <b>gUserBdd</b>, <i></i>
373 Cal_Bdd <b>hUserBdd</b> <i></i>
374)
375</pre>
376<dd> Returns the BDD for logical If-Then-Else
377
378 Description [Returns the BDD for the logical operation IF f THEN g ELSE h
379 - f g + f' h
380<p>
381
382<dd> <b>Side Effects</b> None
383<p>
384
385<dd> <b>See Also</b> <code><a href="#Cal_BddAnd">Cal_BddAnd</a>
386<a href="#Cal_BddNand">Cal_BddNand</a>
387<a href="#Cal_BddOr">Cal_BddOr</a>
388<a href="#Cal_BddNor">Cal_BddNor</a>
389<a href="#Cal_BddXor">Cal_BddXor</a>
390<a href="#Cal_BddXnor">Cal_BddXnor</a>
391</code>
392
393<dt><pre>
394<A NAME="Cal_BddIdentity"></A>
395Cal_Bdd <I></I>
396<B>Cal_BddIdentity</B>(
397 Cal_BddManager <b>bddManager</b>, <i></i>
398 Cal_Bdd <b>userBdd</b> <i></i>
399)
400</pre>
401<dd> Returns the duplicate BDD of the argument BDD.
402<p>
403
404<dd> <b>Side Effects</b> The reference count of the BDD is increased by 1.
405<p>
406
407<dd> <b>See Also</b> <code><a href="#Cal_BddNot">Cal_BddNot</a>
408</code>
409
410<dt><pre>
411<A NAME="Cal_BddIf"></A>
412Cal_Bdd <I></I>
413<B>Cal_BddIf</B>(
414 Cal_BddManager <b>bddManager</b>, <i></i>
415 Cal_Bdd <b>userBdd</b> <i></i>
416)
417</pre>
418<dd> Returns the BDD corresponding to the top variable of
419 the argument BDD.
420<p>
421
422<dd> <b>Side Effects</b> None.
423<p>
424
425<dt><pre>
426<A NAME="Cal_BddImplies"></A>
427Cal_Bdd <I></I>
428<B>Cal_BddImplies</B>(
429 Cal_BddManager <b>bddManager</b>, <i></i>
430 Cal_Bdd <b>fUserBdd</b>, <i></i>
431 Cal_Bdd <b>gUserBdd</b> <i></i>
432)
433</pre>
434<dd> Computes a BDD that implies conjunction of f and Cal_BddNot(g)
435<p>
436
437<dd> <b>Side Effects</b> none
438<p>
439
440<dd> <b>See Also</b> <code><a href="#Cal_BddIntersects">Cal_BddIntersects</a>
441</code>
442
443<dt><pre>
444<A NAME="Cal_BddIntersects"></A>
445Cal_Bdd <I></I>
446<B>Cal_BddIntersects</B>(
447 Cal_BddManager <b>bddManager</b>, <i></i>
448 Cal_Bdd <b>fUserBdd</b>, <i></i>
449 Cal_Bdd <b>gUserBdd</b> <i></i>
450)
451</pre>
452<dd> Computes a BDD that implies conjunction of f and g.
453<p>
454
455<dd> <b>Side Effects</b> None
456<p>
457
458<dd> <b>See Also</b> <code><a href="#Cal_BddImplies">Cal_BddImplies</a>
459</code>
460
461<dt><pre>
462<A NAME="Cal_BddIsBddConst"></A>
463int <I></I>
464<B>Cal_BddIsBddConst</B>(
465 Cal_BddManager <b>bddManager</b>, <i></i>
466 Cal_Bdd <b>userBdd</b> <i></i>
467)
468</pre>
469<dd> Returns 1 if the argument BDD is either constant one or
470 constant zero, otherwise returns 0.
471<p>
472
473<dd> <b>Side Effects</b> None.
474<p>
475
476<dd> <b>See Also</b> <code><a href="#Cal_BddIsBddOne">Cal_BddIsBddOne</a>
477<a href="#Cal_BddIsBddZero">Cal_BddIsBddZero</a>
478</code>
479
480<dt><pre>
481<A NAME="Cal_BddIsBddNull"></A>
482int <I></I>
483<B>Cal_BddIsBddNull</B>(
484 Cal_BddManager <b>bddManager</b>, <i></i>
485 Cal_Bdd <b>userBdd</b> <i></i>
486)
487</pre>
488<dd> Returns 1 if the argument BDD is NULL, 0 otherwise.
489<p>
490
491<dd> <b>Side Effects</b> None.
492<p>
493
494<dt><pre>
495<A NAME="Cal_BddIsBddOne"></A>
496int <I></I>
497<B>Cal_BddIsBddOne</B>(
498 Cal_BddManager <b>bddManager</b>, <i></i>
499 Cal_Bdd <b>userBdd</b> <i></i>
500)
501</pre>
502<dd> Returns 1 if the argument BDD is constant one, 0 otherwise.
503<p>
504
505<dd> <b>Side Effects</b> None.
506<p>
507
508<dd> <b>See Also</b> <code><a href="#Cal_BddIsBddZero">Cal_BddIsBddZero</a>
509</code>
510
511<dt><pre>
512<A NAME="Cal_BddIsBddZero"></A>
513int <I></I>
514<B>Cal_BddIsBddZero</B>(
515 Cal_BddManager <b>bddManager</b>, <i></i>
516 Cal_Bdd <b>userBdd</b> <i></i>
517)
518</pre>
519<dd> Returns 1 if the argument BDD is constant zero, 0 otherwise.
520<p>
521
522<dd> <b>Side Effects</b> None.
523<p>
524
525<dd> <b>See Also</b> <code><a href="#Cal_BddIsBddOne">Cal_BddIsBddOne</a>
526</code>
527
528<dt><pre>
529<A NAME="Cal_BddIsCube"></A>
530int <I></I>
531<B>Cal_BddIsCube</B>(
532 Cal_BddManager <b>bddManager</b>, <i></i>
533 Cal_Bdd <b>fUserBdd</b> <i></i>
534)
535</pre>
536<dd> Returns 1 if the argument BDD is a cube, 0 otherwise
537<p>
538
539<dd> <b>Side Effects</b> None
540<p>
541
542<dt><pre>
543<A NAME="Cal_BddIsEqual"></A>
544int <I></I>
545<B>Cal_BddIsEqual</B>(
546 Cal_BddManager <b>bddManager</b>, <i></i>
547 Cal_Bdd <b>userBdd1</b>, <i></i>
548 Cal_Bdd <b>userBdd2</b> <i></i>
549)
550</pre>
551<dd> Returns 1 if argument BDDs are equal, 0 otherwise.
552<p>
553
554<dd> <b>Side Effects</b> None.
555<p>
556
557<dt><pre>
558<A NAME="Cal_BddIsProvisional"></A>
559int <I></I>
560<B>Cal_BddIsProvisional</B>(
561 Cal_BddManager <b>bddManager</b>, <i></i>
562 Cal_Bdd <b>userBdd</b> <i></i>
563)
564</pre>
565<dd> Returns 1, if the given user BDD contains
566 provisional BDD node.
567<p>
568
569<dd> <b>Side Effects</b> None.
570<p>
571
572<dt><pre>
573<A NAME="Cal_BddManagerCreateNewVarAfter"></A>
574Cal_Bdd <I></I>
575<B>Cal_BddManagerCreateNewVarAfter</B>(
576 Cal_BddManager <b>bddManager</b>, <i></i>
577 Cal_Bdd <b>userBdd</b> <i></i>
578)
579</pre>
580<dd> Creates and returns a new variable after the specified one in
581 the variable order.
582<p>
583
584<dd> <b>Side Effects</b> None
585<p>
586
587<dt><pre>
588<A NAME="Cal_BddManagerCreateNewVarBefore"></A>
589Cal_Bdd <I></I>
590<B>Cal_BddManagerCreateNewVarBefore</B>(
591 Cal_BddManager <b>bddManager</b>, <i></i>
592 Cal_Bdd <b>userBdd</b> <i></i>
593)
594</pre>
595<dd> Creates and returns a new variable before the specified one in
596 the variable order.
597<p>
598
599<dd> <b>Side Effects</b> None
600<p>
601
602<dt><pre>
603<A NAME="Cal_BddManagerCreateNewVarFirst"></A>
604Cal_Bdd <I></I>
605<B>Cal_BddManagerCreateNewVarFirst</B>(
606 Cal_BddManager <b>bddManager</b> <i></i>
607)
608</pre>
609<dd> Creates and returns a new variable at the start of the
610 variable order.
611<p>
612
613<dd> <b>Side Effects</b> None
614<p>
615
616<dt><pre>
617<A NAME="Cal_BddManagerCreateNewVarLast"></A>
618Cal_Bdd <I></I>
619<B>Cal_BddManagerCreateNewVarLast</B>(
620 Cal_BddManager <b>bddManager</b> <i></i>
621)
622</pre>
623<dd> Creates and returns a new variable at the end of the variable
624 order.
625<p>
626
627<dd> <b>Side Effects</b> None
628<p>
629
630<dt><pre>
631<A NAME="Cal_BddManagerGC"></A>
632int <I></I>
633<B>Cal_BddManagerGC</B>(
634 Cal_BddManager <b>bddManager</b> <i></i>
635)
636</pre>
637<dd> For each variable in the increasing id free nodes with reference
638 count equal to zero freeing a node results in decrementing reference count of
639 then and else nodes by one.
640<p>
641
642<dd> <b>Side Effects</b> None.
643<p>
644
645<dt><pre>
646<A NAME="Cal_BddManagerGetHooks"></A>
647void * <I></I>
648<B>Cal_BddManagerGetHooks</B>(
649 Cal_BddManager <b>bddManager</b> <i></i>
650)
651</pre>
652<dd> Returns the hooks field of the manager.
653<p>
654
655<dd> <b>Side Effects</b> None
656<p>
657
658<dt><pre>
659<A NAME="Cal_BddManagerGetNumNodes"></A>
660unsigned long <I></I>
661<B>Cal_BddManagerGetNumNodes</B>(
662 Cal_BddManager <b>bddManager</b> <i></i>
663)
664</pre>
665<dd> Returns the number of BDD nodes
666<p>
667
668<dd> <b>Side Effects</b> None
669<p>
670
671<dd> <b>See Also</b> <code><a href="#Cal_BddTotalSize">Cal_BddTotalSize</a>
672</code>
673
674<dt><pre>
675<A NAME="Cal_BddManagerGetVarWithId"></A>
676Cal_Bdd <I></I>
677<B>Cal_BddManagerGetVarWithId</B>(
678 Cal_BddManager <b>bddManager</b>, <i></i>
679 Cal_BddId_t <b>id</b> <i></i>
680)
681</pre>
682<dd> Returns the variable with the specified id, null if no
683 such variable exists
684<p>
685
686<dd> <b>Side Effects</b> None
687<p>
688
689<dd> <b>See Also</b> <code>optional
690</code>
691
692<dt><pre>
693<A NAME="Cal_BddManagerGetVarWithIndex"></A>
694Cal_Bdd <I></I>
695<B>Cal_BddManagerGetVarWithIndex</B>(
696 Cal_BddManager <b>bddManager</b>, <i></i>
697 Cal_BddIndex_t <b>index</b> <i></i>
698)
699</pre>
700<dd> Returns the variable with the specified index, null if no
701 such variable exists
702<p>
703
704<dd> <b>Side Effects</b> None
705<p>
706
707<dt><pre>
708<A NAME="Cal_BddManagerInit"></A>
709Cal_BddManager <I></I>
710<B>Cal_BddManagerInit</B>(
711 <b></b> <i></i>
712)
713</pre>
714<dd> Initializes and allocates fields of the BDD manager. Some of the
715 fields are initialized for maxNumVars+1 or numVars+1, whereas some of them are
716 initialized for maxNumVars or numVars. The first kind of fields are associated
717 with the id of a variable and the second ones are with the index of the
718 variable.
719<p>
720
721<dd> <b>Side Effects</b> None
722<p>
723
724<dd> <b>See Also</b> <code><a href="#Cal_BddManagerQuit">Cal_BddManagerQuit</a>
725</code>
726
727<dt><pre>
728<A NAME="Cal_BddManagerQuit"></A>
729int <I></I>
730<B>Cal_BddManagerQuit</B>(
731 Cal_BddManager <b>bddManager</b> <i></i>
732)
733</pre>
734<dd> Frees the BDD manager and all the associated allocations
735<p>
736
737<dd> <b>Side Effects</b> None
738<p>
739
740<dd> <b>See Also</b> <code><a href="#Cal_BddManagerInit">Cal_BddManagerInit</a>
741</code>
742
743<dt><pre>
744<A NAME="Cal_BddManagerSetGCLimit"></A>
745void <I></I>
746<B>Cal_BddManagerSetGCLimit</B>(
747 Cal_BddManager <b>manager</b> <i></i>
748)
749</pre>
750<dd> It tries to set the limit at twice the number of nodes
751 in the manager at the current point. However, the limit is not
752 allowed to fall below the MIN_GC_LIMIT or to exceed the value of
753 node limit (if one exists).
754<p>
755
756<dd> <b>Side Effects</b> None.
757<p>
758
759<dt><pre>
760<A NAME="Cal_BddManagerSetHooks"></A>
761void <I></I>
762<B>Cal_BddManagerSetHooks</B>(
763 Cal_BddManager <b>bddManager</b>, <i></i>
764 void * <b>hooks</b> <i></i>
765)
766</pre>
767<dd> Sets the hooks field of the manager.
768<p>
769
770<dd> <b>Side Effects</b> Hooks field changes.
771<p>
772
773<dt><pre>
774<A NAME="Cal_BddManagerSetParameters"></A>
775void <I></I>
776<B>Cal_BddManagerSetParameters</B>(
777 Cal_BddManager <b>bddManager</b>, <i></i>
778 long <b>reorderingThreshold</b>, <i></i>
779 long <b>maxForwardedNodes</b>, <i></i>
780 double <b>repackAfterGCThreshold</b>, <i></i>
781 double <b>tableRepackThreshold</b> <i></i>
782)
783</pre>
784<dd> This function is used to set the parameters which are
785 used to control the reordering process. "reorderingThreshold"
786 determines the number of nodes below which reordering will NOT be
787 invoked, "maxForwardedNodes" determines the maximum number of
788 forwarded nodes which are allowed (at that point the cleanup must be
789 done), and "repackingThreshold" determines the fraction of the page
790 utilized below which repacking has to be invoked. These parameters
791 have different affect on the computational and memory usage aspects
792 of reordeing. For instance, higher value of "maxForwardedNodes" will
793 result in process consuming more memory, and a lower value on the
794 other hand would invoke the cleanup process repeatedly resulting in
795 increased computation.
796<p>
797
798<dd> <b>Side Effects</b> None
799<p>
800
801<dt><pre>
802<A NAME="Cal_BddMultiwayAnd"></A>
803Cal_Bdd <I></I>
804<B>Cal_BddMultiwayAnd</B>(
805 Cal_BddManager <b>bddManager</b>, <i></i>
806 Cal_Bdd * <b>userBddArray</b> <i></i>
807)
808</pre>
809<dd> Returns the BDD for logical AND of set of BDDs in the bddArray
810<p>
811
812<dd> <b>Side Effects</b> None
813<p>
814
815<dt><pre>
816<A NAME="Cal_BddMultiwayOr"></A>
817Cal_Bdd <I></I>
818<B>Cal_BddMultiwayOr</B>(
819 Cal_BddManager <b>bddManager</b>, <i></i>
820 Cal_Bdd * <b>userBddArray</b> <i></i>
821)
822</pre>
823<dd> Returns the BDD for logical OR of set of BDDs in the bddArray
824<p>
825
826<dd> <b>Side Effects</b> None
827<p>
828
829<dt><pre>
830<A NAME="Cal_BddMultiwayXor"></A>
831Cal_Bdd <I></I>
832<B>Cal_BddMultiwayXor</B>(
833 Cal_BddManager <b>bddManager</b>, <i></i>
834 Cal_Bdd * <b>userBddArray</b> <i></i>
835)
836</pre>
837<dd> Returns the BDD for logical XOR of set of BDDs in the bddArray
838<p>
839
840<dd> <b>Side Effects</b> None
841<p>
842
843<dt><pre>
844<A NAME="Cal_BddNand"></A>
845Cal_Bdd <I></I>
846<B>Cal_BddNand</B>(
847 Cal_BddManager <b>bddManager</b>, <i></i>
848 Cal_Bdd <b>fUserBdd</b>, <i></i>
849 Cal_Bdd <b>gUserBdd</b> <i></i>
850)
851</pre>
852<dd> Returns the BDD for logical NAND of f and g
853<p>
854
855<dd> <b>Side Effects</b> None
856<p>
857
858<dt><pre>
859<A NAME="Cal_BddNewVarBlock"></A>
860Cal_Block <I></I>
861<B>Cal_BddNewVarBlock</B>(
862 Cal_BddManager <b>bddManager</b>, <i></i>
863 Cal_Bdd <b>variable</b>, <i></i>
864 long <b>length</b> <i></i>
865)
866</pre>
867<dd> The block is specified by passing the first
868 variable and the length of the block. The "length" number of
869 consecutive variables starting from "variable" are put in the
870 block.
871<p>
872
873<dd> <b>Side Effects</b> A new block is created.
874<p>
875
876<dt><pre>
877<A NAME="Cal_BddNodeLimit"></A>
878long <I></I>
879<B>Cal_BddNodeLimit</B>(
880 Cal_BddManager <b>bddManager</b>, <i></i>
881 long <b>newLimit</b> <i></i>
882)
883</pre>
884<dd> Sets the node limit to new_limit and returns the old limit.
885<p>
886
887<dd> <b>Side Effects</b> Threshold for garbage collection may change
888<p>
889
890<dd> <b>See Also</b> <code><a href="#Cal_BddManagerGC">Cal_BddManagerGC</a>
891</code>
892
893<dt><pre>
894<A NAME="Cal_BddNor"></A>
895Cal_Bdd <I></I>
896<B>Cal_BddNor</B>(
897 Cal_BddManager <b>bddManager</b>, <i></i>
898 Cal_Bdd <b>fUserBdd</b>, <i></i>
899 Cal_Bdd <b>gUserBdd</b> <i></i>
900)
901</pre>
902<dd> Returns the BDD for logical NOR of f and g
903<p>
904
905<dd> <b>Side Effects</b> None
906<p>
907
908<dt><pre>
909<A NAME="Cal_BddNot"></A>
910Cal_Bdd <I></I>
911<B>Cal_BddNot</B>(
912 Cal_BddManager <b>bddManager</b>, <i></i>
913 Cal_Bdd <b>userBdd</b> <i></i>
914)
915</pre>
916<dd> Returns the complement of the argument BDD.
917<p>
918
919<dd> <b>Side Effects</b> The reference count of the argument BDD is increased by 1.
920<p>
921
922<dd> <b>See Also</b> <code><a href="#Cal_BddIdentity">Cal_BddIdentity</a>
923</code>
924
925<dt><pre>
926<A NAME="Cal_BddOne"></A>
927Cal_Bdd <I></I>
928<B>Cal_BddOne</B>(
929 Cal_BddManager <b>bddManager</b> <i></i>
930)
931</pre>
932<dd> Returns the BDD for the constant one
933<p>
934
935<dd> <b>Side Effects</b> None
936<p>
937
938<dd> <b>See Also</b> <code><a href="#Cal_BddZero">Cal_BddZero</a>
939</code>
940
941<dt><pre>
942<A NAME="Cal_BddOr"></A>
943Cal_Bdd <I></I>
944<B>Cal_BddOr</B>(
945 Cal_BddManager <b>bddManager</b>, <i></i>
946 Cal_Bdd <b>fUserBdd</b>, <i></i>
947 Cal_Bdd <b>gUserBdd</b> <i></i>
948)
949</pre>
950<dd> Returns the BDD for logical OR of f and g
951<p>
952
953<dd> <b>Side Effects</b> None
954<p>
955
956<dt><pre>
957<A NAME="Cal_BddOverflow"></A>
958int <I></I>
959<B>Cal_BddOverflow</B>(
960 Cal_BddManager <b>bddManager</b> <i></i>
961)
962</pre>
963<dd> Returns 1 if the node limit has been exceeded, 0 otherwise. The
964 overflow flag is cleared.
965<p>
966
967<dd> <b>Side Effects</b> None
968<p>
969
970<dd> <b>See Also</b> <code><a href="#Cal_BddNodeLimit">Cal_BddNodeLimit</a>
971</code>
972
973<dt><pre>
974<A NAME="Cal_BddPairwiseAnd"></A>
975Cal_Bdd * <I></I>
976<B>Cal_BddPairwiseAnd</B>(
977 Cal_BddManager <b>bddManager</b>, <i></i>
978 Cal_Bdd * <b>userBddArray</b> <i></i>
979)
980</pre>
981<dd> Returns an array of BDDs obtained by logical AND of BDD pairs
982 specified by an BDD array in which a BDD at an even location is paired with
983 a BDD at an odd location of the array
984<p>
985
986<dd> <b>Side Effects</b> None
987<p>
988
989<dd> <b>See Also</b> <code><a href="#Cal_BddPairwiseOr">Cal_BddPairwiseOr</a>
990</code>
991
992<dt><pre>
993<A NAME="Cal_BddPairwiseOr"></A>
994Cal_Bdd * <I></I>
995<B>Cal_BddPairwiseOr</B>(
996 Cal_BddManager <b>bddManager</b>, <i></i>
997 Cal_Bdd * <b>userBddArray</b> <i></i>
998)
999</pre>
1000<dd> Returns an array of BDDs obtained by logical OR of BDD pairs
1001 specified by an BDD array in which a BDD at an even location is paired with
1002 a BDD at an odd location of the array
1003<p>
1004
1005<dd> <b>Side Effects</b> None
1006<p>
1007
1008<dd> <b>See Also</b> <code><a href="#Cal_BddPairwiseAnd">Cal_BddPairwiseAnd</a>
1009</code>
1010
1011<dt><pre>
1012<A NAME="Cal_BddPairwiseXor"></A>
1013Cal_Bdd * <I></I>
1014<B>Cal_BddPairwiseXor</B>(
1015 Cal_BddManager <b>bddManager</b>, <i></i>
1016 Cal_Bdd * <b>userBddArray</b> <i></i>
1017)
1018</pre>
1019<dd> Returns an array of BDDs obtained by logical XOR of BDD pairs
1020 specified by an BDD array in which a BDD at an even location is paired with
1021 a BDD at an odd location of the array
1022<p>
1023
1024<dd> <b>Side Effects</b> None
1025<p>
1026
1027<dd> <b>See Also</b> <code><a href="#Cal_BddPairwiseAnd">Cal_BddPairwiseAnd</a>
1028</code>
1029
1030<dt><pre>
1031<A NAME="Cal_BddPrintBdd"></A>
1032void <I></I>
1033<B>Cal_BddPrintBdd</B>(
1034 Cal_BddManager <b>bddManager</b>, <i></i>
1035 Cal_Bdd <b>fUserBdd</b>, <i></i>
1036 Cal_VarNamingFn_t <b>VarNamingFn</b>, <i></i>
1037 Cal_TerminalIdFn_t <b>TerminalIdFn</b>, <i></i>
1038 Cal_Pointer_t <b>env</b>, <i></i>
1039 FILE * <b>fp</b> <i></i>
1040)
1041</pre>
1042<dd> Prints a human-readable representation of the BDD f to
1043 the file given by fp. The namingFn should be a pointer to a function
1044 taking a bddManager, a BDD and the pointer given by env. This
1045 function should return either a null pointer or a srting that is the
1046 name of the supplied variable. If it returns a null pointer, a
1047 default name is generated based on the index of the variable. It is
1048 also legal for naminFN to e null; in this case, default names are
1049 generated for all variables. The macro bddNamingFnNone is a null
1050 pointer of suitable type. terminalIdFn should be apointer to a
1051 function taking a bddManager and two longs. plus the pointer given
1052 by the env. It should return either a null pointer. If it returns a
1053 null pointer, or if terminalIdFn is null, then default names are
1054 generated for the terminals. The macro bddTerminalIdFnNone is a null
1055 pointer of suitable type.
1056<p>
1057
1058<dd> <b>Side Effects</b> None.
1059<p>
1060
1061<dt><pre>
1062<A NAME="Cal_BddPrintFunctionProfileMultiple"></A>
1063void <I></I>
1064<B>Cal_BddPrintFunctionProfileMultiple</B>(
1065 Cal_BddManager <b>bddManager</b>, <i></i>
1066 Cal_Bdd * <b>userBdds</b>, <i></i>
1067 Cal_VarNamingFn_t <b>varNamingProc</b>, <i></i>
1068 char * <b>env</b>, <i></i>
1069 int <b>lineLength</b>, <i></i>
1070 FILE * <b>fp</b> <i></i>
1071)
1072</pre>
1073<dd> optional
1074<p>
1075
1076<dd> <b>Side Effects</b> None
1077<p>
1078
1079<dd> <b>See Also</b> <code>optional
1080</code>
1081
1082<dt><pre>
1083<A NAME="Cal_BddPrintFunctionProfile"></A>
1084void <I></I>
1085<B>Cal_BddPrintFunctionProfile</B>(
1086 Cal_BddManager <b>bddManager</b>, <i></i>
1087 Cal_Bdd <b>f</b>, <i></i>
1088 Cal_VarNamingFn_t <b>varNamingProc</b>, <i></i>
1089 char * <b>env</b>, <i></i>
1090 int <b>lineLength</b>, <i></i>
1091 FILE * <b>fp</b> <i></i>
1092)
1093</pre>
1094<dd> optional
1095<p>
1096
1097<dd> <b>Side Effects</b> None
1098<p>
1099
1100<dd> <b>See Also</b> <code>optional
1101</code>
1102
1103<dt><pre>
1104<A NAME="Cal_BddPrintProfileMultiple"></A>
1105void <I></I>
1106<B>Cal_BddPrintProfileMultiple</B>(
1107 Cal_BddManager <b>bddManager</b>, <i></i>
1108 Cal_Bdd * <b>userBdds</b>, <i></i>
1109 Cal_VarNamingFn_t <b>varNamingProc</b>, <i></i>
1110 char * <b>env</b>, <i></i>
1111 int <b>lineLength</b>, <i></i>
1112 FILE * <b>fp</b> <i></i>
1113)
1114</pre>
1115<dd> optional
1116<p>
1117
1118<dd> <b>Side Effects</b> None
1119<p>
1120
1121<dd> <b>See Also</b> <code>optional
1122</code>
1123
1124<dt><pre>
1125<A NAME="Cal_BddPrintProfile"></A>
1126void <I></I>
1127<B>Cal_BddPrintProfile</B>(
1128 Cal_BddManager <b>bddManager</b>, <i></i>
1129 Cal_Bdd <b>fUserBdd</b>, <i></i>
1130 Cal_VarNamingFn_t <b>varNamingProc</b>, <i></i>
1131 char * <b>env</b>, <i></i>
1132 int <b>lineLength</b>, <i></i>
1133 FILE * <b>fp</b> <i></i>
1134)
1135</pre>
1136<dd> optional
1137<p>
1138
1139<dd> <b>Side Effects</b> None
1140<p>
1141
1142<dd> <b>See Also</b> <code>optional
1143</code>
1144
1145<dt><pre>
1146<A NAME="Cal_BddProfileMultiple"></A>
1147void <I></I>
1148<B>Cal_BddProfileMultiple</B>(
1149 Cal_BddManager <b>bddManager</b>, <i></i>
1150 Cal_Bdd * <b>fUserBddArray</b>, <i></i>
1151 long * <b>levelCounts</b>, <i></i>
1152 int <b>negout</b> <i></i>
1153)
1154</pre>
1155<dd> optional
1156<p>
1157
1158<dd> <b>Side Effects</b> None
1159<p>
1160
1161<dd> <b>See Also</b> <code>optional
1162</code>
1163
1164<dt><pre>
1165<A NAME="Cal_BddProfile"></A>
1166void <I></I>
1167<B>Cal_BddProfile</B>(
1168 Cal_BddManager <b>bddManager</b>, <i></i>
1169 Cal_Bdd <b>fUserBdd</b>, <i></i>
1170 long * <b>levelCounts</b>, <i></i>
1171 int <b>negout</b> <i></i>
1172)
1173</pre>
1174<dd> negout is as in Cal_BddSize. levelCounts should be an array of
1175 size Cal_BddVars(bddManager)+1 to hold the profile.
1176<p>
1177
1178<dd> <b>Side Effects</b> None
1179<p>
1180
1181<dd> <b>See Also</b> <code>optional
1182</code>
1183
1184<dt><pre>
1185<A NAME="Cal_BddReduce"></A>
1186Cal_Bdd <I></I>
1187<B>Cal_BddReduce</B>(
1188 Cal_BddManager <b>bddManager</b>, <i></i>
1189 Cal_Bdd <b>fUserBdd</b>, <i></i>
1190 Cal_Bdd <b>cUserBdd</b> <i></i>
1191)
1192</pre>
1193<dd> Returns a BDD which agrees with f for all valuations
1194 which satisfy c. The result is usually smaller in terms of number of
1195 BDD nodes than f. This operation is typically used in state space
1196 searches to simplify the representation for the set of states wich
1197 will be expanded at each step.
1198<p>
1199
1200<dd> <b>Side Effects</b> None
1201<p>
1202
1203<dd> <b>See Also</b> <code><a href="#Cal_BddCofactor">Cal_BddCofactor</a>
1204</code>
1205
1206<dt><pre>
1207<A NAME="Cal_BddRelProd"></A>
1208Cal_Bdd <I></I>
1209<B>Cal_BddRelProd</B>(
1210 Cal_BddManager <b>bddManager</b>, <i></i>
1211 Cal_Bdd <b>fUserBdd</b>, <i></i>
1212 Cal_Bdd <b>gUserBdd</b> <i></i>
1213)
1214</pre>
1215<dd> Returns the BDD for the logical AND of f and g with all
1216 the variables that are paired with something in the current variable
1217 association existentially quantified out.
1218<p>
1219
1220<dd> <b>Side Effects</b> None.
1221<p>
1222
1223<dt><pre>
1224<A NAME="Cal_BddReorder"></A>
1225void <I></I>
1226<B>Cal_BddReorder</B>(
1227 Cal_BddManager <b>bddManager</b> <i></i>
1228)
1229</pre>
1230<dd> Invoke the current dynamic reodering method.
1231<p>
1232
1233<dd> <b>Side Effects</b> Index of a variable may change due to reodering
1234<p>
1235
1236<dd> <b>See Also</b> <code><a href="#Cal_BddDynamicReordering">Cal_BddDynamicReordering</a>
1237</code>
1238
1239<dt><pre>
1240<A NAME="Cal_BddSatisfySupport"></A>
1241Cal_Bdd <I></I>
1242<B>Cal_BddSatisfySupport</B>(
1243 Cal_BddManager <b>bddManager</b>, <i></i>
1244 Cal_Bdd <b>fUserBdd</b> <i></i>
1245)
1246</pre>
1247<dd> The returned BDD which implies f, is true for some valuation on
1248 which f is true, which has at most one node at each level,
1249 and which has exactly one node corresponding to each variable
1250 which is associated with something in the current variable
1251 association.
1252<p>
1253
1254<dd> <b>Side Effects</b> required
1255<p>
1256
1257<dd> <b>See Also</b> <code>optional
1258</code>
1259
1260<dt><pre>
1261<A NAME="Cal_BddSatisfyingFraction"></A>
1262double <I></I>
1263<B>Cal_BddSatisfyingFraction</B>(
1264 Cal_BddManager <b>bddManager</b>, <i></i>
1265 Cal_Bdd <b>fUserBdd</b> <i></i>
1266)
1267</pre>
1268<dd> optional
1269<p>
1270
1271<dd> <b>Side Effects</b> required
1272<p>
1273
1274<dd> <b>See Also</b> <code>optional
1275</code>
1276
1277<dt><pre>
1278<A NAME="Cal_BddSatisfy"></A>
1279Cal_Bdd <I></I>
1280<B>Cal_BddSatisfy</B>(
1281 Cal_BddManager <b>bddManager</b>, <i></i>
1282 Cal_Bdd <b>fUserBdd</b> <i></i>
1283)
1284</pre>
1285<dd> optional
1286<p>
1287
1288<dd> <b>Side Effects</b> required
1289<p>
1290
1291<dd> <b>See Also</b> <code>optional
1292</code>
1293
1294<dt><pre>
1295<A NAME="Cal_BddSetGCMode"></A>
1296void <I></I>
1297<B>Cal_BddSetGCMode</B>(
1298 Cal_BddManager <b>bddManager</b>, <i></i>
1299 int <b>gcMode</b> <i></i>
1300)
1301</pre>
1302<dd> Sets the garbage collection mode, 0 means the garbage
1303 collection should be turned off, 1 means garbage collection should
1304 be on.
1305<p>
1306
1307<dd> <b>Side Effects</b> None.
1308<p>
1309
1310<dt><pre>
1311<A NAME="Cal_BddSizeMultiple"></A>
1312long <I></I>
1313<B>Cal_BddSizeMultiple</B>(
1314 Cal_BddManager <b>bddManager</b>, <i></i>
1315 Cal_Bdd * <b>fUserBddArray</b>, <i></i>
1316 int <b>negout</b> <i></i>
1317)
1318</pre>
1319<dd> optional
1320<p>
1321
1322<dd> <b>Side Effects</b> None
1323<p>
1324
1325<dd> <b>See Also</b> <code>optional
1326</code>
1327
1328<dt><pre>
1329<A NAME="Cal_BddSize"></A>
1330long <I></I>
1331<B>Cal_BddSize</B>(
1332 Cal_BddManager <b>bddManager</b>, <i></i>
1333 Cal_Bdd <b>fUserBdd</b>, <i></i>
1334 int <b>negout</b> <i></i>
1335)
1336</pre>
1337<dd> optional
1338<p>
1339
1340<dd> <b>Side Effects</b> None
1341<p>
1342
1343<dd> <b>See Also</b> <code>optional
1344</code>
1345
1346<dt><pre>
1347<A NAME="Cal_BddStats"></A>
1348void <I></I>
1349<B>Cal_BddStats</B>(
1350 Cal_BddManager <b>bddManager</b>, <i></i>
1351 FILE * <b>fp</b> <i></i>
1352)
1353</pre>
1354<dd> Prints miscellaneous BDD statistics
1355<p>
1356
1357<dd> <b>Side Effects</b> None
1358<p>
1359
1360<dt><pre>
1361<A NAME="Cal_BddSubstitute"></A>
1362Cal_Bdd <I></I>
1363<B>Cal_BddSubstitute</B>(
1364 Cal_BddManager <b>bddManager</b>, <i></i>
1365 Cal_Bdd <b>fUserBdd</b> <i></i>
1366)
1367</pre>
1368<dd> Returns a BDD for f using the substitution defined by current
1369 variable association. Each variable is replaced by its associated BDDs. The
1370 substitution is effective simultaneously
1371<p>
1372
1373<dd> <b>Side Effects</b> None
1374<p>
1375
1376<dd> <b>See Also</b> <code><a href="#Cal_BddCompose">Cal_BddCompose</a>
1377</code>
1378
1379<dt><pre>
1380<A NAME="Cal_BddSupport"></A>
1381void <I></I>
1382<B>Cal_BddSupport</B>(
1383 Cal_BddManager <b>bddManager</b>, <i></i>
1384 Cal_Bdd <b>fUserBdd</b>, <i></i>
1385 Cal_Bdd * <b>support</b> <i></i>
1386)
1387</pre>
1388<dd> optional
1389<p>
1390
1391<dd> <b>Side Effects</b> None
1392<p>
1393
1394<dd> <b>See Also</b> <code>optional
1395</code>
1396
1397<dt><pre>
1398<A NAME="Cal_BddSwapVars"></A>
1399Cal_Bdd <I></I>
1400<B>Cal_BddSwapVars</B>(
1401 Cal_BddManager <b>bddManager</b>, <i></i>
1402 Cal_Bdd <b>fUserBdd</b>, <i></i>
1403 Cal_Bdd <b>gUserBdd</b>, <i></i>
1404 Cal_Bdd <b>hUserBdd</b> <i></i>
1405)
1406</pre>
1407<dd> Returns the BDD obtained by simultaneously substituting variable
1408 g by variable h and variable h and variable g in the BDD f
1409<p>
1410
1411<dd> <b>Side Effects</b> None
1412<p>
1413
1414<dd> <b>See Also</b> <code><a href="#Cal_BddSubstitute">Cal_BddSubstitute</a>
1415</code>
1416
1417<dt><pre>
1418<A NAME="Cal_BddThen"></A>
1419Cal_Bdd <I></I>
1420<B>Cal_BddThen</B>(
1421 Cal_BddManager <b>bddManager</b>, <i></i>
1422 Cal_Bdd <b>userBdd</b> <i></i>
1423)
1424</pre>
1425<dd> Returns the positive cofactor of the argument BDD with
1426 respect to the top variable of the BDD.
1427<p>
1428
1429<dd> <b>Side Effects</b> The reference count of the returned BDD is increased by 1.
1430<p>
1431
1432<dd> <b>See Also</b> <code><a href="#Cal_BddElse">Cal_BddElse</a>
1433</code>
1434
1435<dt><pre>
1436<A NAME="Cal_BddTotalSize"></A>
1437unsigned long <I></I>
1438<B>Cal_BddTotalSize</B>(
1439 Cal_BddManager <b>bddManager</b> <i></i>
1440)
1441</pre>
1442<dd> Returns the number of nodes in the Unique table
1443<p>
1444
1445<dd> <b>Side Effects</b> None
1446<p>
1447
1448<dd> <b>See Also</b> <code><a href="#Cal_BddManagerGetNumNodes">Cal_BddManagerGetNumNodes</a>
1449</code>
1450
1451<dt><pre>
1452<A NAME="Cal_BddType"></A>
1453int <I></I>
1454<B>Cal_BddType</B>(
1455 Cal_BddManager <b>bddManager</b>, <i></i>
1456 Cal_Bdd <b>fUserBdd</b> <i></i>
1457)
1458</pre>
1459<dd> Returns BDD_TYPE_ZERO if f is false, BDD_TYPE_ONE
1460 if f is true, BDD_TYPE_POSVAR is f is an unnegated variable,
1461 BDD_TYPE_NEGVAR if f is a negated variable, BDD_TYPE_OVERFLOW if f
1462 is null, and BDD_TYPE_NONTERMINAL otherwise.
1463<p>
1464
1465<dd> <b>Side Effects</b> None
1466<p>
1467
1468<dt><pre>
1469<A NAME="Cal_BddUnFree"></A>
1470void <I></I>
1471<B>Cal_BddUnFree</B>(
1472 Cal_BddManager <b>bddManager</b>, <i></i>
1473 Cal_Bdd <b>userBdd</b> <i></i>
1474)
1475</pre>
1476<dd> Unfrees the argument BDD. It is an error to pass a BDD
1477 with reference count of zero to be unfreed.
1478<p>
1479
1480<dd> <b>Side Effects</b> The reference count of the argument BDD is increased by 1.
1481<p>
1482
1483<dd> <b>See Also</b> <code><a href="#Cal_BddFree">Cal_BddFree</a>
1484</code>
1485
1486<dt><pre>
1487<A NAME="Cal_BddUndumpBdd"></A>
1488Cal_Bdd <I></I>
1489<B>Cal_BddUndumpBdd</B>(
1490 Cal_BddManager <b>bddManager</b>, <i></i>
1491 Cal_Bdd * <b>userVars</b>, <i></i>
1492 FILE * <b>fp</b>, <i></i>
1493 int * <b>error</b> <i></i>
1494)
1495</pre>
1496<dd> Loads an encoded description of a BDD from the file given by
1497 fp. The argument vars should be a null terminated array of variables that will
1498 become the support of the BDD. As in Cal_BddDumpBdd, these need not be in
1499 the order of increasing index. If the same array of variables in used in
1500 dumping and undumping, the BDD returned will be equal to the one that was
1501 dumped. More generally, if array v1 is used when dumping, and the array v2
1502 is used when undumping, the BDD returned will be equal to the original BDD
1503 with the ith variable in v2 substituted for the ith variable in v1 for all i.
1504 Null BDD is returned in the operation fails for reason (node limit reached,
1505 I/O error, invalid file format, etc.). In this case, an error code is stored
1506 in error. the code will be one of the following.
1507 CAL_BDD_UNDUMP_FORMAT Invalid file format
1508 CAL_BDD_UNDUMP_OVERFLOW Node limit exceeded
1509 CAL_BDD_UNDUMP_IOERROR File I/O error
1510 CAL_BDD_UNDUMP_EOF Unexpected EOF
1511<p>
1512
1513<dd> <b>Side Effects</b> required
1514<p>
1515
1516<dd> <b>See Also</b> <code>optional
1517</code>
1518
1519<dt><pre>
1520<A NAME="Cal_BddVarBlockReorderable"></A>
1521void <I></I>
1522<B>Cal_BddVarBlockReorderable</B>(
1523 Cal_BddManager <b>bddManager</b>, <i></i>
1524 Cal_Block <b>block</b>, <i></i>
1525 int <b>reorderable</b> <i></i>
1526)
1527</pre>
1528<dd> If a block is reorderable, the child blocks are
1529 recursively involved in swapping.
1530<p>
1531
1532<dd> <b>Side Effects</b> None.
1533<p>
1534
1535<dt><pre>
1536<A NAME="Cal_BddVarSubstitute"></A>
1537Cal_Bdd <I></I>
1538<B>Cal_BddVarSubstitute</B>(
1539 Cal_BddManager <b>bddManager</b>, <i></i>
1540 Cal_Bdd <b>fUserBdd</b> <i></i>
1541)
1542</pre>
1543<dd> Returns a BDD for f using the substitution defined by current
1544 variable association. It is assumed that each variable is replaced
1545 by another variable. For the substitution of a variable by a
1546 function, use Cal_BddSubstitute instead.
1547<p>
1548
1549<dd> <b>Side Effects</b> None
1550<p>
1551
1552<dd> <b>See Also</b> <code><a href="#Cal_BddSubstitute">Cal_BddSubstitute</a>
1553</code>
1554
1555<dt><pre>
1556<A NAME="Cal_BddVars"></A>
1557long <I></I>
1558<B>Cal_BddVars</B>(
1559 Cal_BddManager <b>bddManager</b> <i></i>
1560)
1561</pre>
1562<dd> Returns the number of BDD variables
1563<p>
1564
1565<dd> <b>Side Effects</b> None
1566<p>
1567
1568<dt><pre>
1569<A NAME="Cal_BddXnor"></A>
1570Cal_Bdd <I></I>
1571<B>Cal_BddXnor</B>(
1572 Cal_BddManager <b>bddManager</b>, <i></i>
1573 Cal_Bdd <b>fUserBdd</b>, <i></i>
1574 Cal_Bdd <b>gUserBdd</b> <i></i>
1575)
1576</pre>
1577<dd> Returns the BDD for logical exclusive NOR of f and g
1578<p>
1579
1580<dd> <b>Side Effects</b> None
1581<p>
1582
1583<dt><pre>
1584<A NAME="Cal_BddXor"></A>
1585Cal_Bdd <I></I>
1586<B>Cal_BddXor</B>(
1587 Cal_BddManager <b>bddManager</b>, <i></i>
1588 Cal_Bdd <b>fUserBdd</b>, <i></i>
1589 Cal_Bdd <b>gUserBdd</b> <i></i>
1590)
1591</pre>
1592<dd> Returns the BDD for logical exclusive OR of f and g
1593<p>
1594
1595<dd> <b>Side Effects</b> None
1596<p>
1597
1598<dt><pre>
1599<A NAME="Cal_BddZero"></A>
1600Cal_Bdd <I></I>
1601<B>Cal_BddZero</B>(
1602 Cal_BddManager <b>bddManager</b> <i></i>
1603)
1604</pre>
1605<dd> Returns the BDD for the constant zero
1606<p>
1607
1608<dd> <b>Side Effects</b> None
1609<p>
1610
1611<dd> <b>See Also</b> <code><a href="#Cal_BddOne">Cal_BddOne</a>
1612</code>
1613
1614<dt><pre>
1615<A NAME="Cal_MemAllocation"></A>
1616Cal_Address_t <I></I>
1617<B>Cal_MemAllocation</B>(
1618 <b></b> <i></i>
1619)
1620</pre>
1621<dd> Returns the memory allocated.
1622<p>
1623
1624<dd> <b>Side Effects</b> required
1625<p>
1626
1627<dd> <b>See Also</b> <code>optional
1628</code>
1629
1630<dt><pre>
1631<A NAME="Cal_MemFatal"></A>
1632void <I></I>
1633<B>Cal_MemFatal</B>(
1634 char * <b>message</b> <i></i>
1635)
1636</pre>
1637<dd> Prints an error message and exits.
1638<p>
1639
1640<dd> <b>Side Effects</b> required
1641<p>
1642
1643<dd> <b>See Also</b> <code>optional
1644</code>
1645
1646<dt><pre>
1647<A NAME="Cal_MemFreeBlock"></A>
1648void <I></I>
1649<B>Cal_MemFreeBlock</B>(
1650 Cal_Pointer_t <b>p</b> <i></i>
1651)
1652</pre>
1653<dd> Frees the block.
1654<p>
1655
1656<dd> <b>Side Effects</b> required
1657<p>
1658
1659<dd> <b>See Also</b> <code>optional
1660</code>
1661
1662<dt><pre>
1663<A NAME="Cal_MemFreeRecMgr"></A>
1664void <I></I>
1665<B>Cal_MemFreeRecMgr</B>(
1666 Cal_RecMgr <b>mgr</b> <i></i>
1667)
1668</pre>
1669<dd> Frees all the storage associated with the specified record manager.
1670<p>
1671
1672<dd> <b>Side Effects</b> required
1673<p>
1674
1675<dd> <b>See Also</b> <code>optional
1676</code>
1677
1678<dt><pre>
1679<A NAME="Cal_MemFreeRec"></A>
1680void <I></I>
1681<B>Cal_MemFreeRec</B>(
1682 Cal_RecMgr <b>mgr</b>, <i></i>
1683 Cal_Pointer_t <b>rec</b> <i></i>
1684)
1685</pre>
1686<dd> Frees a record managed by the indicated record manager.
1687<p>
1688
1689<dd> <b>Side Effects</b> required
1690<p>
1691
1692<dd> <b>See Also</b> <code>optional
1693</code>
1694
1695<dt><pre>
1696<A NAME="Cal_MemGetBlock"></A>
1697Cal_Pointer_t <I></I>
1698<B>Cal_MemGetBlock</B>(
1699 Cal_Address_t <b>size</b> <i></i>
1700)
1701</pre>
1702<dd> Allocates a new block of the specified size.
1703<p>
1704
1705<dd> <b>Side Effects</b> required
1706<p>
1707
1708<dd> <b>See Also</b> <code>optional
1709</code>
1710
1711<dt><pre>
1712<A NAME="Cal_MemNewRecMgr"></A>
1713Cal_RecMgr <I></I>
1714<B>Cal_MemNewRecMgr</B>(
1715 int <b>size</b> <i></i>
1716)
1717</pre>
1718<dd> Creates a new record manager with the given record size.
1719<p>
1720
1721<dd> <b>Side Effects</b> required
1722<p>
1723
1724<dd> <b>See Also</b> <code>optional
1725</code>
1726
1727<dt><pre>
1728<A NAME="Cal_MemNewRec"></A>
1729Cal_Pointer_t <I></I>
1730<B>Cal_MemNewRec</B>(
1731 Cal_RecMgr <b>mgr</b> <i></i>
1732)
1733</pre>
1734<dd> Allocates a record from the specified record manager.
1735<p>
1736
1737<dd> <b>Side Effects</b> required
1738<p>
1739
1740<dd> <b>See Also</b> <code>optional
1741</code>
1742
1743<dt><pre>
1744<A NAME="Cal_MemResizeBlock"></A>
1745Cal_Pointer_t <I></I>
1746<B>Cal_MemResizeBlock</B>(
1747 Cal_Pointer_t <b>p</b>, <i></i>
1748 Cal_Address_t <b>newSize</b> <i></i>
1749)
1750</pre>
1751<dd> Expands or contracts the block to a new size.
1752 We try to avoid moving the block if possible.
1753<p>
1754
1755<dd> <b>Side Effects</b> required
1756<p>
1757
1758<dd> <b>See Also</b> <code>optional
1759</code>
1760
1761<dt><pre>
1762<A NAME="Cal_PerformanceTest"></A>
1763int <I></I>
1764<B>Cal_PerformanceTest</B>(
1765 Cal_BddManager <b>bddManager</b>, <i></i>
1766 Cal_Bdd * <b>outputBddArray</b>, <i></i>
1767 int <b>numFunctions</b>, <i></i>
1768 int <b>iteration</b>, <i></i>
1769 int <b>seed</b>, <i></i>
1770 int <b>andPerformanceFlag</b>, <i></i>
1771 int <b>multiwayPerformanceFlag</b>, <i></i>
1772 int <b>onewayPerformanceFlag</b>, <i></i>
1773 int <b>quantifyPerformanceFlag</b>, <i></i>
1774 int <b>composePerformanceFlag</b>, <i></i>
1775 int <b>relprodPerformanceFlag</b>, <i></i>
1776 int <b>swapPerformanceFlag</b>, <i></i>
1777 int <b>substitutePerformanceFlag</b>, <i></i>
1778 int <b>sanityCheckFlag</b>, <i></i>
1779 int <b>computeMemoryOverheadFlag</b>, <i></i>
1780 int <b>superscalarFlag</b> <i></i>
1781)
1782</pre>
1783<dd> optional
1784<p>
1785
1786<dd> <b>Side Effects</b> required
1787<p>
1788
1789<dd> <b>See Also</b> <code>optional
1790</code>
1791
1792<dt><pre>
1793<A NAME="Cal_PipelineCreateProvisionalBdd"></A>
1794Cal_Bdd <I></I>
1795<B>Cal_PipelineCreateProvisionalBdd</B>(
1796 Cal_BddManager <b>bddManager</b>, <i></i>
1797 Cal_Bdd <b>fUserBdd</b>, <i></i>
1798 Cal_Bdd <b>gUserBdd</b> <i></i>
1799)
1800</pre>
1801<dd> The provisional BDD is automatically freed once the
1802 pipeline is quitted.
1803<p>
1804
1805<dt><pre>
1806<A NAME="Cal_PipelineExecute"></A>
1807int <I></I>
1808<B>Cal_PipelineExecute</B>(
1809 Cal_BddManager <b>bddManager</b> <i></i>
1810)
1811</pre>
1812<dd> All the results are computed. User should update the
1813 BDDs of interest. Eventually this feature would become transparent.
1814<p>
1815
1816<dd> <b>Side Effects</b> required
1817<p>
1818
1819<dd> <b>See Also</b> <code>optional
1820</code>
1821
1822<dt><pre>
1823<A NAME="Cal_PipelineInit"></A>
1824int <I></I>
1825<B>Cal_PipelineInit</B>(
1826 Cal_BddManager <b>bddManager</b>, <i></i>
1827 Cal_BddOp_t <b>bddOp</b> <i></i>
1828)
1829</pre>
1830<dd> All the operations for this pipeline must be of the
1831 same kind.
1832<p>
1833
1834<dd> <b>Side Effects</b> None.
1835<p>
1836
1837<dt><pre>
1838<A NAME="Cal_PipelineQuit"></A>
1839void <I></I>
1840<B>Cal_PipelineQuit</B>(
1841 Cal_BddManager <b>bddManager</b> <i></i>
1842)
1843</pre>
1844<dd> The user must make sure to update all provisional BDDs
1845 of interest before calling this routine.
1846<p>
1847
1848<dt><pre>
1849<A NAME="Cal_PipelineSetDepth"></A>
1850void <I></I>
1851<B>Cal_PipelineSetDepth</B>(
1852 Cal_BddManager <b>bddManager</b>, <i></i>
1853 int <b>depth</b> <i></i>
1854)
1855</pre>
1856<dd> The "depth" determines the amount of dependency we
1857 would allow in pipelined computation.
1858<p>
1859
1860<dd> <b>Side Effects</b> None.
1861<p>
1862
1863<dt><pre>
1864<A NAME="Cal_PipelineUpdateProvisionalBdd"></A>
1865Cal_Bdd <I></I>
1866<B>Cal_PipelineUpdateProvisionalBdd</B>(
1867 Cal_BddManager <b>bddManager</b>, <i></i>
1868 Cal_Bdd <b>provisionalBdd</b> <i></i>
1869)
1870</pre>
1871<dd> The provisional BDD is automatically freed after
1872 quitting pipeline.
1873<p>
1874
1875<dt><pre>
1876<A NAME="Cal_TempAssociationAugment"></A>
1877void <I></I>
1878<B>Cal_TempAssociationAugment</B>(
1879 Cal_BddManager <b>bddManager</b>, <i></i>
1880 Cal_Bdd * <b>associationInfoUserBdds</b>, <i></i>
1881 int <b>pairs</b> <i></i>
1882)
1883</pre>
1884<dd> Pairs is 0 if the information represents only a list of
1885 variables rather than a full association.
1886<p>
1887
1888<dd> <b>Side Effects</b> None
1889<p>
1890
1891<dt><pre>
1892<A NAME="Cal_TempAssociationInit"></A>
1893void <I></I>
1894<B>Cal_TempAssociationInit</B>(
1895 Cal_BddManager <b>bddManager</b>, <i></i>
1896 Cal_Bdd * <b>associationInfoUserBdds</b>, <i></i>
1897 int <b>pairs</b> <i></i>
1898)
1899</pre>
1900<dd> Pairs is 0 if the information represents only a list of
1901 variables rather than a full association.
1902<p>
1903
1904<dd> <b>Side Effects</b> None
1905<p>
1906
1907<dt><pre>
1908<A NAME="Cal_TempAssociationQuit"></A>
1909void <I></I>
1910<B>Cal_TempAssociationQuit</B>(
1911 Cal_BddManager <b>bddManager</b> <i></i>
1912)
1913</pre>
1914<dd> Cleans up temporary associationoptional
1915<p>
1916
1917<dd> <b>Side Effects</b> None
1918<p>
1919
1920
1921</DL>
1922<HR>
1923Last updated on 970711 20h11
1924</BODY></HTML>
Note: See TracBrowser for help on using the repository browser.