source: vis_dev/glu-2.3/src/calBdd/calExtDet.html

Last change on this file was 13, checked in by cecile, 13 years ago

library glu 2.3
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.