source: vis_dev/glu-2.3/src/cmuBdd/bdd.c @ 26

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

library glu 2.3
File size: 26.6 KB
Line 
1/* Basic BDD routines */
2
3
4#include "bddint.h"
5
6
7/* cmu_bdd_one(bddm) gives the BDD for true. */
8
9bdd
10cmu_bdd_one(cmu_bdd_manager bddm)
11{
12  return (BDD_ONE(bddm));
13}
14
15
16/* cmu_bdd_zero(bddm) gives the BDD for false. */
17
18bdd
19cmu_bdd_zero(cmu_bdd_manager bddm)
20{
21  return (BDD_ZERO(bddm));
22}
23
24
25bdd
26bdd_make_external(bdd f)
27{
28  BDD_SETUP(f);
29  BDD_INCREFS(f);
30  BDD_TEMP_DECREFS(f);
31  return (f);
32}
33
34
35long
36bdd_find_block(block b, long index)
37{
38  long i, j, k;
39
40  i=0;
41  j=b->num_children-1;
42  while (i <= j)
43    {
44      k=(i+j)/2;
45      if (b->children[k]->first_index <= index && b->children[k]->last_index >= index)
46        return (k);
47      if (b->children[k]->first_index > index)
48        j=k-1;
49      else
50        i=k+1;
51    }
52  return (i);
53}
54
55
56void
57bdd_block_delta(block b, long delta)
58{
59  long i;
60
61  b->first_index+=delta;
62  b->last_index+=delta;
63  for (i=0; i < b->num_children; ++i)
64    bdd_block_delta(b->children[i], delta);
65}
66
67
68static
69block
70shift_block(cmu_bdd_manager bddm, block b, long index)
71{
72  long i, j;
73  block p;
74
75  if (b->first_index >= index)
76    {
77      bdd_block_delta(b, 1l);
78      return (b);
79    }
80  if (b->last_index < index)
81    return (b);
82  b->last_index++;
83  i=bdd_find_block(b, index);
84  if (i == b->num_children || b->children[i]->first_index == index)
85    {
86      b->children=(block *)mem_resize_block((pointer)b->children, (SIZE_T)(sizeof(block)*(b->num_children+1)));
87      for (j=b->num_children-1; j >= i; --j)
88        b->children[j+1]=shift_block(bddm, b->children[j], index);
89      b->num_children++;
90      p=(block)BDD_NEW_REC(bddm, sizeof(struct block_));
91      p->reorderable=0;
92      p->first_index=index;
93      p->last_index=index;
94      p->num_children=0;
95      p->children=0;
96      b->children[i]=p;
97    }
98  else
99    while (i < b->num_children)
100      {
101        shift_block(bddm, b->children[i], index);
102        ++i;
103      }
104  return (b);
105}
106
107
108/* bdd_new_var(bddm, index) creates a new variable with the */
109/* specified index.  Existing variables with greater or equal index */
110/* have their index incremented. */
111
112static
113bdd
114bdd_new_var(cmu_bdd_manager bddm, bdd_index_type index)
115{
116  long i;
117  long temp;
118  long oldmax;
119  assoc_list p;
120  bdd var;
121
122  if (bddm->vars == BDD_MAX_INDEXINDEX)
123    cmu_bdd_fatal("bdd_new_var: no more indexes");
124  if (index > bddm->vars)
125    cmu_bdd_fatal("bdd_new_var: index out of range");
126  if (bddm->vars == bddm->maxvars)
127    {
128      /* Expand indexing tables and variable associations. */
129      oldmax=bddm->maxvars;
130      temp=bddm->maxvars*2;
131      if (temp > BDD_MAX_INDEXINDEX-1)
132        temp=BDD_MAX_INDEXINDEX-1;
133      bddm->maxvars=temp;
134      bddm->variables=(bdd *)mem_resize_block((pointer)bddm->variables,
135                                              (SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
136      bddm->indexes=(bdd_index_type *)mem_resize_block((pointer)bddm->indexes,
137                                                       (SIZE_T)((bddm->maxvars+1)*sizeof(bdd_index_type)));
138      bddm->indexindexes=
139        (bdd_indexindex_type *)mem_resize_block((pointer)bddm->indexindexes,
140                                                (SIZE_T)(bddm->maxvars*sizeof(bdd_indexindex_type)));
141      bddm->unique_table.tables=
142        (var_table *)mem_resize_block((pointer)bddm->unique_table.tables,
143                                      (SIZE_T)((bddm->maxvars+1)*sizeof(var_table)));
144      /* Variable associations are padded with nulls in case new variables */
145      /* are created. */
146      for (p=bddm->assocs; p; p=p->next)
147        {
148          p->va.assoc=(bdd *)mem_resize_block((pointer)p->va.assoc, (SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
149          for (i=oldmax; i < bddm->maxvars; ++i)
150            p->va.assoc[i+1]=0;
151        }
152      bddm->temp_assoc.assoc=(bdd *)mem_resize_block((pointer)bddm->temp_assoc.assoc, (SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
153      for (i=oldmax; i < bddm->maxvars; ++i)
154        bddm->temp_assoc.assoc[i+1]=0;
155    }
156  /* Shift index of following variables. */
157  if (index != bddm->vars)
158    for (i=0; i < bddm->vars; ++i)
159      if (bddm->indexes[i+1] >= index)
160        bddm->indexes[i+1]++;
161  for (p=bddm->assocs; p; p=p->next)
162    if (p->va.last >= index)
163      p->va.last++;
164  if (bddm->temp_assoc.last >= index)
165    bddm->temp_assoc.last++;
166  /* Shift indexindex values. */
167  for (i=bddm->vars; i > index; --i)
168    bddm->indexindexes[i]=bddm->indexindexes[i-1];
169  /* Make a new variable table. */
170  bddm->vars++;
171  bddm->unique_table.tables[bddm->vars]=bdd_new_var_table(bddm);
172  /* Create the variable. */
173  var=bdd_find_aux(bddm, (bdd_indexindex_type)bddm->vars, (INT_PTR)BDD_ONE(bddm), (INT_PTR)BDD_ZERO(bddm));
174  var->refs=BDD_MAX_REFS;
175  /* Record everything. */
176  bddm->variables[bddm->vars]=var;
177  bddm->indexes[bddm->vars]=index;
178  bddm->indexindexes[index]=bddm->vars;
179  /* Make a new variable block containing the variable. */
180  shift_block(bddm, bddm->super_block, (long)index);
181  return (var);
182}
183
184
185/* cmu_bdd_new_var_first(bddm) returns the BDD for a new variable at the */
186/* start of the variable order. */
187
188bdd
189cmu_bdd_new_var_first(cmu_bdd_manager bddm)
190{
191  return (bdd_new_var(bddm, (bdd_index_type)0));
192}
193
194
195/* cmu_bdd_new_var_last(bddm) returns the BDD for a new variable at the */
196/* end of the variable order. */
197
198bdd
199cmu_bdd_new_var_last(cmu_bdd_manager bddm)
200{
201  return (bdd_new_var(bddm, (bdd_index_type)bddm->vars));
202}
203
204
205/* cmu_bdd_new_var_before(bddm, var) returns the BDD for a new variable */
206/* before the specified one in the variable order. */
207
208bdd
209cmu_bdd_new_var_before(cmu_bdd_manager bddm, bdd var)
210{
211  if (bdd_check_arguments(1, var))
212    {
213      BDD_SETUP(var);
214      if (cmu_bdd_type_aux(bddm, var) != BDD_TYPE_POSVAR)
215        {
216          cmu_bdd_warning("cmu_bdd_new_var_before: argument is not a positive variable");
217          if (BDD_IS_CONST(var))
218            return (cmu_bdd_new_var_last(bddm));
219        }
220      return (bdd_new_var(bddm, BDD_INDEX(bddm, var)));
221    }
222  return ((bdd)0);
223}
224
225
226/* cmu_bdd_new_var_after(bddm, var) returns the BDD for a new variable */
227/* after the specified one in the variable order. */
228
229bdd
230cmu_bdd_new_var_after(cmu_bdd_manager bddm, bdd var)
231{
232  if (bdd_check_arguments(1, var))
233    {
234      BDD_SETUP(var);
235      if (cmu_bdd_type_aux(bddm, var) != BDD_TYPE_POSVAR)
236        {
237          cmu_bdd_warning("cmu_bdd_new_var_after: argument is not a positive variable");
238          if (BDD_IS_CONST(var))
239            return (cmu_bdd_new_var_last(bddm));
240        }
241      return (bdd_new_var(bddm, BDD_INDEX(bddm, var)+1));
242    }
243  return ((bdd)0);
244}
245
246
247/* cmu_bdd_var_with_index(bddm, index) returns the variable with the */
248/* specified index, or null if there is no such variable. */
249
250bdd
251cmu_bdd_var_with_index(cmu_bdd_manager bddm, long index)
252{
253  if (index < 0 || index >= bddm->vars)
254    return ((bdd)0);
255  return (bddm->variables[bddm->indexindexes[index]]);
256}
257
258
259/* cmu_bdd_var_with_id(bddm, id) returns the variable with the specified */
260/* id, or null if there is no such variable. */
261
262bdd
263cmu_bdd_var_with_id(cmu_bdd_manager bddm, long indexindex)
264{
265  if (indexindex <= 0 || indexindex > bddm->vars)
266    return ((bdd)0);
267  return (bddm->variables[indexindex]);
268}
269
270
271static
272bdd
273cmu_bdd_and_step(cmu_bdd_manager bddm, bdd f, bdd g)
274{
275  bdd_indexindex_type top_indexindex;
276  bdd f1, f2;
277  bdd g1, g2;
278  bdd temp1, temp2;
279  bdd result;
280
281  BDD_SETUP(f);
282  BDD_SETUP(g);
283  if (BDD_IS_CONST(f))
284    {
285      if (f == BDD_ZERO(bddm))
286        return (f);
287      BDD_TEMP_INCREFS(g);
288      return (g);
289    }
290  /* f is not constant. */
291  if (BDD_IS_CONST(g))
292    {
293      if (g == BDD_ZERO(bddm))
294        return (g);
295      BDD_TEMP_INCREFS(f);
296      return (f);
297    }
298  /* f and g are not constant. */
299  if (BDD_SAME_OR_NEGATIONS(f, g))
300    {
301      if (f == g)
302        {
303          BDD_TEMP_INCREFS(f);
304          return (f);
305        }
306      return (BDD_ZERO(bddm));
307    }
308  /* f and g are not constant and are not equal or negations. */
309  if (BDD_OUT_OF_ORDER(f, g))
310    BDD_SWAP(f, g);
311  if (bdd_lookup_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_ZERO(bddm), (INT_PTR *)&result))
312    return (result);
313  BDD_TOP_VAR2(top_indexindex, bddm, f, g);
314  BDD_COFACTOR(top_indexindex, f, f1, f2);
315  BDD_COFACTOR(top_indexindex, g, g1, g2);
316  temp1=cmu_bdd_and_step(bddm, f1, g1);
317  temp2=cmu_bdd_and_step(bddm, f2, g2);
318  result=bdd_find(bddm, top_indexindex, temp1, temp2);
319  bdd_insert_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_ZERO(bddm), (INT_PTR)result);
320  return (result);
321}
322
323
324static
325bdd
326cmu_bdd_xnor_step(cmu_bdd_manager bddm, bdd f, bdd g)
327{
328  int outneg;
329  bdd_indexindex_type top_indexindex;
330  bdd f1, f2;
331  bdd g1, g2;
332  bdd temp1, temp2;
333  bdd result;
334
335  BDD_SETUP(f);
336  BDD_SETUP(g);
337  if (BDD_IS_CONST(f))
338    {
339      BDD_TEMP_INCREFS(g);
340      if (f == BDD_ONE(bddm))
341        return (g);
342      return (BDD_NOT(g));
343    }
344  if (BDD_IS_CONST(g))
345    {
346      BDD_TEMP_INCREFS(f);
347      if (g == BDD_ONE(bddm))
348        return (f);
349      return (BDD_NOT(f));
350    }
351  /* f and g are not constant. */
352  if (BDD_SAME_OR_NEGATIONS(f, g))
353    {
354      if (f == g)
355        return (BDD_ONE(bddm));
356      return (BDD_ZERO(bddm));
357    }
358  /* f and g are not constant, not same, not negations. */
359  if (BDD_OUT_OF_ORDER(f, g))
360    BDD_SWAP(f, g);
361  if (BDD_IS_OUTPOS(g))
362    outneg=0;
363  else
364    {
365      outneg=1;
366      g=BDD_NOT(g);
367    }
368  /* g is an uncomplemented output pointer. */
369  if (bdd_lookup_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_NOT(g), (INT_PTR *)&result))
370    return (outneg ? BDD_NOT(result) : result);
371  BDD_TOP_VAR2(top_indexindex, bddm, f, g);
372  BDD_COFACTOR(top_indexindex, f, f1, f2);
373  BDD_COFACTOR(top_indexindex, g, g1, g2);
374  temp1=cmu_bdd_xnor_step(bddm, f1, g1);
375  temp2=cmu_bdd_xnor_step(bddm, f2, g2);
376  result=bdd_find(bddm, top_indexindex, temp1, temp2);
377  bdd_insert_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_NOT(g), (INT_PTR)result);
378  return (outneg ? BDD_NOT(result) : result);
379}
380
381
382bdd
383cmu_bdd_ite_step(cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
384{
385  int outneg;
386  bdd_indexindex_type top_indexindex;
387  bdd f1, f2;
388  bdd g1, g2;
389  bdd h1, h2;
390  bdd temp1, temp2;
391  bdd result;
392
393  BDD_SETUP(f);
394  BDD_SETUP(g);
395  BDD_SETUP(h);
396  if (BDD_IS_CONST(f))
397    {
398      if (f == BDD_ONE(bddm))
399        {
400          BDD_TEMP_INCREFS(g);
401          return (g);
402        }
403      BDD_TEMP_INCREFS(h);
404      return (h);
405    }
406  /* f is not constant. */
407  if (BDD_SAME_OR_NEGATIONS(f, g))
408    {
409      if (f == g)
410        g=BDD_ONE(bddm);
411      else
412        g=BDD_ZERO(bddm);
413      BDD_RESET(g);
414    }
415  if (BDD_SAME_OR_NEGATIONS(f, h))
416    {
417      if (f == h)
418        h=BDD_ZERO(bddm);
419      else
420        h=BDD_ONE(bddm);
421      BDD_RESET(h);
422    }
423  if (BDD_IS_CONST(g))
424    {
425      if (BDD_IS_CONST(h))
426        {
427          if (g == h)
428            return (g);
429          BDD_TEMP_INCREFS(f);
430          if (g == BDD_ONE(bddm))
431            return (f);
432          return (BDD_NOT(f));
433        }
434      if (g == BDD_ZERO(bddm))
435        return (cmu_bdd_and_step(bddm, BDD_NOT(f), h));
436      return (BDD_NOT(cmu_bdd_and_step(bddm, BDD_NOT(f), BDD_NOT(h))));
437    }
438  else if (BDD_SAME_OR_NEGATIONS(g, h))
439    {
440      if (g == h)
441        {
442          BDD_TEMP_INCREFS(g);
443          return (g);
444        }
445      return (cmu_bdd_xnor_step(bddm, f, g));
446    }
447  else if (BDD_IS_CONST(h))
448    {
449    if (h == BDD_ZERO(bddm))
450      return (cmu_bdd_and_step(bddm, f, g));
451    else
452      return (BDD_NOT(cmu_bdd_and_step(bddm, f, BDD_NOT(g))));
453    }
454  /* No special cases; it's a real if-then-else. */
455  if (!BDD_IS_OUTPOS(f))
456    {
457      f=BDD_NOT(f);
458      BDD_SWAP(g, h);
459    }
460  /* f is now an uncomplemented output pointer. */
461  if (BDD_IS_OUTPOS(g))
462    outneg=0;
463  else
464    {
465      outneg=1;
466      g=BDD_NOT(g);
467      h=BDD_NOT(h);
468    }
469  /* g is now an uncomplemented output pointer. */
470  if (bdd_lookup_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)h, (INT_PTR *)&result))
471    return (outneg ? BDD_NOT(result) : result);
472  BDD_TOP_VAR3(top_indexindex, bddm, f, g, h);
473  BDD_COFACTOR(top_indexindex, f, f1, f2);
474  BDD_COFACTOR(top_indexindex, g, g1, g2);
475  BDD_COFACTOR(top_indexindex, h, h1, h2);
476  temp1=cmu_bdd_ite_step(bddm, f1, g1, h1);
477  temp2=cmu_bdd_ite_step(bddm, f2, g2, h2);
478  result=bdd_find(bddm, top_indexindex, temp1, temp2);
479  bdd_insert_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)h, (INT_PTR)result);
480  return (outneg ? BDD_NOT(result) : result);
481}
482
483
484/* cmu_bdd_ite(bddm, f, g, h) returns the BDD for "if f then g else h". */
485
486bdd
487cmu_bdd_ite(cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
488{
489  if (bdd_check_arguments(3, f, g, h))
490    {
491      FIREWALL(bddm);
492      RETURN_BDD(cmu_bdd_ite_step(bddm, f, g, h));
493    }
494  return ((bdd)0);
495}
496
497
498/* cmu_bdd_and(bddm, f, g) returns the BDD for "f and g". */
499
500bdd
501cmu_bdd_and(cmu_bdd_manager bddm, bdd f, bdd g)
502{
503  return (cmu_bdd_ite(bddm, f, g, BDD_ZERO(bddm)));
504}
505
506
507/* cmu_bdd_nand(bddm, f, g) returns the BDD for "f nand g". */
508
509bdd
510cmu_bdd_nand(cmu_bdd_manager bddm, bdd f, bdd g)
511{
512  bdd temp;
513
514  if ((temp=cmu_bdd_and(bddm, f, g)))
515    return (BDD_NOT(temp));
516  return ((bdd)0);
517}
518
519
520/* cmu_bdd_or(bddm, f, g) returns the BDD for "f or g". */
521
522bdd
523cmu_bdd_or(cmu_bdd_manager bddm, bdd f, bdd g)
524{
525  return (cmu_bdd_ite(bddm, f, BDD_ONE(bddm), g));
526}
527
528
529/* cmu_bdd_nor(bddm, f, g) returns the BDD for "f nor g". */
530
531bdd
532cmu_bdd_nor(cmu_bdd_manager bddm, bdd f, bdd g)
533{
534  bdd temp;
535
536  if ((temp=cmu_bdd_or(bddm, f, g)))
537    return (BDD_NOT(temp));
538  return ((bdd)0);
539}
540
541
542/* cmu_bdd_xor(bddm, f, g) returns the BDD for "f xor g". */
543
544bdd
545cmu_bdd_xor(cmu_bdd_manager bddm, bdd f, bdd g)
546{
547  return (cmu_bdd_ite(bddm, f, BDD_NOT(g), g));
548}
549
550
551/* cmu_bdd_xnor(bddm, f, g) returns the BDD for "f xnor g". */
552
553bdd
554cmu_bdd_xnor(cmu_bdd_manager bddm, bdd f, bdd g)
555{
556  bdd temp;
557
558  if ((temp=cmu_bdd_xor(bddm, f, g)))
559    return (BDD_NOT(temp));
560  return ((bdd)0);
561}
562
563
564/* cmu_bdd_identity(bddm, f) returns the BDD for f.  (The only effect is */
565/* to increase the reference count for f.) */
566
567bdd
568cmu_bdd_identity(cmu_bdd_manager bddm, bdd f)
569{
570  if (bdd_check_arguments(1, f))
571    {
572      BDD_SETUP(f);
573      BDD_INCREFS(f);
574    }
575  return (f);
576}
577
578
579/* cmu_bdd_not(bddm, f) returns the BDD for "not f". */
580
581bdd
582cmu_bdd_not(cmu_bdd_manager bddm, bdd f)
583{
584  if (bdd_check_arguments(1, f))
585    {
586      BDD_SETUP(f);
587      BDD_INCREFS(f);
588      return (BDD_NOT(f));
589    }
590  return ((bdd)0);
591}
592 
593
594/* cmu_bdd_if(bddm, f) returns the BDD for the variable at the top of f. */
595
596bdd
597cmu_bdd_if(cmu_bdd_manager bddm, bdd f)
598{
599  if (bdd_check_arguments(1, f))
600    {
601      BDD_SETUP(f);
602      if (BDD_IS_CONST(f))
603        {
604          cmu_bdd_warning("cmu_bdd_if: argument is a constant");
605          return (f);
606        }
607      FIREWALL(bddm);
608      RETURN_BDD(BDD_IF(bddm, f));
609    }
610  return (f);
611}
612
613
614/* cmu_bdd_if_index(bddm, f) returns the index for the variable at the top */
615/* of f. */
616
617long
618cmu_bdd_if_index(cmu_bdd_manager bddm, bdd f)
619{
620  if (bdd_check_arguments(1, f))
621    {
622      BDD_SETUP(f);
623      if (BDD_IS_CONST(f))
624        return (-1l);
625      return ((long)BDD_INDEX(bddm, f));
626    }
627  return (-1l);
628}
629
630
631/* cmu_bdd_if_id(bddm, f) returns a unique identifier for the variable at */
632/* the top of f. */
633
634long
635cmu_bdd_if_id(cmu_bdd_manager bddm, bdd f)
636{
637  if (bdd_check_arguments(1, f))
638    {
639      BDD_SETUP(f);
640      if (BDD_IS_CONST(f))
641        return (-1l);
642      return ((long)BDD_INDEXINDEX(f));
643    }
644  return (-1l);
645}
646
647
648/* cmu_bdd_then(bddm, f) returns the BDD for the "then" pointer of f. */
649
650bdd
651cmu_bdd_then(cmu_bdd_manager bddm, bdd f)
652{
653  if (bdd_check_arguments(1, f))
654    {
655      BDD_SETUP(f);
656      if (BDD_IS_CONST(f))
657        {
658          cmu_bdd_warning("cmu_bdd_then: argument is a constant");
659          return (f);
660        }
661      f=BDD_THEN(f);
662      BDD_RESET(f);
663      BDD_INCREFS(f);
664    }
665  return (f);
666}
667 
668
669/* cmu_bdd_else(bddm, f) returns the BDD for the "else" pointer of f. */
670
671bdd
672cmu_bdd_else(cmu_bdd_manager bddm, bdd f)
673{
674  if (bdd_check_arguments(1, f))
675    {
676      BDD_SETUP(f);
677      if (BDD_IS_CONST(f))
678        {
679          cmu_bdd_warning("cmu_bdd_else: argument is a constant");
680          return (f);
681        }
682      f=BDD_ELSE(f);
683      BDD_RESET(f);
684      BDD_INCREFS(f);
685    }
686  return (f);
687}
688
689
690static
691bdd
692cmu_bdd_intersects_step(cmu_bdd_manager bddm, bdd f, bdd g)
693{
694  bdd_indexindex_type top_indexindex;
695  bdd f1, f2;
696  bdd g1, g2;
697  bdd temp;
698
699  BDD_SETUP(f);
700  BDD_SETUP(g);
701  if (BDD_IS_CONST(f))
702    {
703      if (f == BDD_ZERO(bddm))
704        return (f);
705      BDD_TEMP_INCREFS(g);
706      return (g);
707    }
708  /* f is not constant. */
709  if (BDD_IS_CONST(g))
710    {
711      if (g == BDD_ZERO(bddm))
712        return (g);
713      BDD_TEMP_INCREFS(f);
714      return (f);
715    }
716  /* f and g are not constant. */
717  if (BDD_SAME_OR_NEGATIONS(f, g))
718    {
719      if (f == g)
720        {
721          BDD_TEMP_INCREFS(f);
722          return (f);
723        }
724      return (BDD_ZERO(bddm));
725    }
726  /* f and g are not constant and are not equal or negations. */
727  if (BDD_OUT_OF_ORDER(f, g))
728    BDD_SWAP(f, g);
729  if (bdd_lookup_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_ZERO(bddm), (INT_PTR *)&temp))
730    return (temp);
731  BDD_TOP_VAR2(top_indexindex, bddm, f, g);
732  BDD_COFACTOR(top_indexindex, f, f1, f2);
733  BDD_COFACTOR(top_indexindex, g, g1, g2);
734  temp=cmu_bdd_intersects_step(bddm, f1, g1);
735  if (temp != BDD_ZERO(bddm))
736    return (bdd_find(bddm, top_indexindex, temp, BDD_ZERO(bddm)));
737  temp=bdd_find(bddm, top_indexindex, BDD_ZERO(bddm), cmu_bdd_intersects_step(bddm, f2, g2));
738  if (temp == BDD_ZERO(bddm))
739    bdd_insert_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_ZERO(bddm), (INT_PTR)temp);
740  return (temp);
741}
742
743
744/* cmu_bdd_intersects(bddm, f, g) returns a BDD contained in "f and g", */
745/* while building as few nodes as possible.  The idea is that it */
746/* gives us a fast test for intersection, and, when f and g do */
747/* intersect, we can call cmu_bdd_satisfy or cmu_bdd_satisfy_support on the */
748/* result to get a valuation in the intersection. */
749
750bdd
751cmu_bdd_intersects(cmu_bdd_manager bddm, bdd f, bdd g)
752{
753  if (bdd_check_arguments(2, f, g))
754    {
755      FIREWALL(bddm);
756      RETURN_BDD(cmu_bdd_intersects_step(bddm, f, g));
757    }
758  return ((bdd)0);
759}
760
761
762/* cmu_bdd_implies(bddm, f, g) is analogous to cmu_bdd_intersects, but it */
763/* looks for things in "f and not g". */
764
765bdd
766cmu_bdd_implies(cmu_bdd_manager bddm, bdd f, bdd g)
767{
768  if (bdd_check_arguments(2, f, g))
769    {
770      FIREWALL(bddm);
771      RETURN_BDD(cmu_bdd_intersects_step(bddm, f, BDD_NOT(g)));
772    }
773  return ((bdd)0);
774}
775
776
777int
778cmu_bdd_type_aux(cmu_bdd_manager bddm, bdd f)
779{
780  BDD_SETUP(f);
781  if (BDD_IS_CONST(f))
782    {
783      if (f == BDD_ZERO(bddm))
784        return (BDD_TYPE_ZERO);
785      if (f == BDD_ONE(bddm))
786        return (BDD_TYPE_ONE);
787      return (BDD_TYPE_CONSTANT);
788    }
789  if (BDD_THEN(f) == BDD_ONE(bddm) && BDD_ELSE(f) == BDD_ZERO(bddm))
790    return (BDD_TYPE_POSVAR);
791  if (BDD_THEN(f) == BDD_ZERO(bddm) && BDD_ELSE(f) == BDD_ONE(bddm))
792    return (BDD_TYPE_NEGVAR);
793  return (BDD_TYPE_NONTERMINAL);
794}
795
796
797/* cmu_bdd_type(bddm, f) returns BDD_TYPE_ZERO if f is false, BDD_TYPE_ONE */
798/* if f is true, BDD_TYPE_CONSTANT if f is an MTBDD constant, */
799/* BDD_TYPE_POSVAR is f is an unnegated variable, BDD_TYPE_NEGVAR if */
800/* f is a negated variable, BDD_TYPE_OVERFLOW if f is null, and */
801/* BDD_TYPE_NONTERMINAL otherwise. */
802
803int
804cmu_bdd_type(cmu_bdd_manager bddm, bdd f)
805{
806  if (bdd_check_arguments(1, f))
807    return (cmu_bdd_type_aux(bddm, f));
808  return (BDD_TYPE_OVERFLOW);
809}
810
811
812/* cmu_bdd_unfree(bddm, f) increments the reference count for f. */
813
814void
815cmu_bdd_unfree(cmu_bdd_manager bddm, bdd f)
816{
817  if (f)
818    {
819      BDD_SETUP(f);
820      BDD_INCREFS(f);
821    }
822}
823
824
825/* cmu_bdd_free(bddm, f) decrements the reference count for f. */
826
827void
828cmu_bdd_free(cmu_bdd_manager bddm, bdd f)
829{
830  if (f)
831    {
832      BDD_SETUP(f);
833      if (BDD_REFS(f) == 0)
834        cmu_bdd_fatal("cmu_bdd_free: attempt to free node with zero references");
835      else
836        BDD_DECREFS(f);
837    }
838}
839
840
841/* cmu_bdd_vars(bddm) returns the number of variables in existence. */
842
843long
844cmu_bdd_vars(cmu_bdd_manager bddm)
845{
846  return (bddm->vars);
847}
848
849
850/* cmu_bdd_total_size(bddm) returns the number of BDD nodes in existence. */
851
852long
853cmu_bdd_total_size(cmu_bdd_manager bddm)
854{
855  return (bddm->unique_table.entries);
856}
857
858
859/* cmu_bdd_cache_ratio(bddm, new_ratio) sets the cache size ratio to */
860/* new_ratio and returns the old ratio. */
861
862int
863cmu_bdd_cache_ratio(cmu_bdd_manager bddm, int new_ratio)
864{
865  int old_ratio;
866
867  old_ratio=bddm->op_cache.cache_ratio;
868  if (new_ratio < 1)
869    new_ratio=1;
870  else if (new_ratio > 32)
871    new_ratio=32;
872  bddm->op_cache.cache_ratio=new_ratio;
873  return (old_ratio);
874}
875
876
877/* cmu_bdd_node_limit(bddm, new_limit) sets the node limit to */
878/* new_limit and returns the old limit. */
879
880long
881cmu_bdd_node_limit(cmu_bdd_manager bddm, long new_limit)
882{
883  long old_limit;
884
885  old_limit=bddm->unique_table.node_limit;
886  if (new_limit < 0)
887    new_limit=0;
888  bddm->unique_table.node_limit=new_limit;
889  if (new_limit && bddm->unique_table.gc_limit > new_limit)
890    bddm->unique_table.gc_limit=new_limit;
891  return (old_limit);
892}
893
894
895/* cmu_bdd_overflow(bddm) returns 1 if the node limit has been exceeded */
896/* and 0 otherwise.  The overflow flag is cleared. */
897
898int
899cmu_bdd_overflow(cmu_bdd_manager bddm)
900{
901  int result;
902
903  result=bddm->overflow;
904  bddm->overflow=0;
905  return (result);
906}
907
908
909/* cmu_bdd_overflow_closure(bddm, overflow_fn, overflow_env) sets the */
910/* closure to be invoked on overflow.  If overflow_fn is null, it */
911/* indicates that no function should be called. */
912
913void
914cmu_bdd_overflow_closure(cmu_bdd_manager bddm, void (*overflow_fn)(cmu_bdd_manager, pointer), pointer overflow_env)
915{
916  bddm->overflow_fn=overflow_fn;
917  bddm->overflow_env=overflow_env;
918}
919
920
921/* cmu_bdd_abort_closure(bddm, abort_fn, abort_env) sets a closure to be */
922/* invoked when the next find operation is attempted.  This is */
923/* intended for aborting BDD operations from signal handlers.  The */
924/* handler should set this closure so that invoking it will cause */
925/* a longjmp to a recovery routine. */
926
927void
928cmu_bdd_abort_closure(cmu_bdd_manager bddm, void (*abort_fn)(cmu_bdd_manager, pointer), pointer abort_env)
929{
930  bddm->bag_it_fn=abort_fn;
931  bddm->bag_it_env=abort_env;
932}
933
934
935/* cmu_bdd_stats(bddm, fp) prints random statistics to the file indicated */
936/* by fp. */
937
938void
939cmu_bdd_stats(cmu_bdd_manager bddm, FILE *fp)
940{
941  long i;
942  long ue, ce, cs, mem;
943  SIZE_T alloc;
944  assoc_list q;
945
946  ue=bddm->unique_table.entries;
947  ce=bddm->op_cache.entries;
948  cs=bddm->op_cache.size;
949  mem=0;
950  for (i=0; i < bddm->vars; ++i)
951    {
952      mem+=sizeof(struct var_table_);
953      mem+=bddm->unique_table.tables[i]->size*sizeof(bdd);
954    }
955  mem=ue*sizeof(struct bdd_);
956  mem+=cs*sizeof(struct cache_bin_)+ce*sizeof(struct cache_entry_);
957  mem+=bddm->maxvars*(sizeof(bdd_index_type)+sizeof(bdd_indexindex_type)+sizeof(bdd)+sizeof(var_table));
958  for (q=bddm->assocs, i=1; q; q=q->next, ++i);
959  mem+=i*bddm->maxvars*sizeof(bdd);
960  if ((alloc=mem_allocation()))
961    /* mem_allocation may be meaningless depending on mem library. */
962    fprintf(fp, "Memory manager bytes allocated: %ld\n", (long)alloc);
963  fprintf(fp, "Approximate bytes used: %ld\n", mem);
964  fprintf(fp, "Number of nodes: %ld\n", ue);
965  if (bddm->unique_table.node_limit)
966    fprintf(fp, "Node limit: %ld\n", bddm->unique_table.node_limit);
967  else
968    fprintf(fp, "Node limit: ---\n");
969  fprintf(fp, "Overflow: %s\n", bddm->overflow ? "yes" : "no");
970  fprintf(fp, "Approximate bytes per node: %-.2f\n", ((double)mem)/ue);
971  fprintf(fp, "Cache entries: %ld\n", ce);
972  fprintf(fp, "Cache size: %ld\n", 2*cs);
973  fprintf(fp, "Cache load factor: %-.2f\n", ((double)ce)/(2*cs));
974  fprintf(fp, "Cache look ups: %ld\n", bddm->op_cache.lookups);
975  fprintf(fp, "Cache hits: %ld\n", bddm->op_cache.hits);
976  if (bddm->op_cache.lookups)
977    fprintf(fp, "Cache hit rate: %-.2f\n", ((double)(bddm->op_cache.hits))/bddm->op_cache.lookups);
978  else
979    fprintf(fp, "Cache hit rate: ---\n");
980  fprintf(fp, "Cache insertions: %ld\n", bddm->op_cache.inserts);
981  fprintf(fp, "Cache collisions: %ld\n", bddm->op_cache.collisions);
982  fprintf(fp, "Number of variables: %ld\n", bddm->vars);
983  fprintf(fp, "Number of variable associations: %ld\n", i);
984  fprintf(fp, "Number of garbage collections: %ld\n", bddm->unique_table.gcs);
985  fprintf(fp, "Number of nodes garbage collected: %ld\n", bddm->unique_table.freed);
986  fprintf(fp, "Number of find operations: %ld\n", bddm->unique_table.finds);
987}
988
989
990static
991int
992bdd_default_canonical_fn(cmu_bdd_manager bddm, INT_PTR value1, INT_PTR value2, pointer junk)
993{
994  /* Default transformation is treat the value as a 64-bit integer and to */
995  /* negate it if it is positive. */
996  return ((long)value1 > 0 || (!value1 && (long)value2 > 0));
997}
998
999
1000static
1001void
1002bdd_default_transform_fn(cmu_bdd_manager bddm, INT_PTR value1, INT_PTR value2, INT_PTR *result1, INT_PTR *result2, pointer junk)
1003{
1004  if (!value2)
1005    /* Will be a carry when taking 2's complement of value2.  Thus, */
1006    /* take 2's complement of high part. */
1007    value1= -(long)value1;
1008  else
1009    {
1010      value2= -(long)value2;
1011      value1= ~value1;
1012    }
1013  *result1=value1;
1014  *result2=value2;
1015}
1016
1017
1018/* cmu_bdd_init() creates and returns a new BDD manager. */
1019
1020cmu_bdd_manager
1021cmu_bdd_init(void)
1022{
1023  cmu_bdd_manager bddm;
1024  long i;
1025
1026  bddm=(cmu_bdd_manager)mem_get_block((SIZE_T)sizeof(struct bdd_manager_));
1027  bddm->overflow=0;
1028  bddm->overflow_fn=0;
1029  bddm->overflow_env=0;
1030  bddm->bag_it_fn=0;
1031  bddm->bag_it_env=0;
1032  bddm->canonical_fn=bdd_default_canonical_fn;
1033  bddm->transform_fn=bdd_default_transform_fn;
1034  bddm->transform_env=0;
1035  bddm->reorder_fn=0;
1036  bddm->reorder_data=0;
1037  bddm->vars=0;
1038  bddm->maxvars=30; 
1039  bddm->check=1;
1040  bddm->variables=(bdd *)mem_get_block((SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
1041  bddm->indexes=(bdd_index_type *)mem_get_block((SIZE_T)((bddm->maxvars+1)*sizeof(bdd_index_type)));
1042  bddm->indexindexes=(bdd_indexindex_type *)mem_get_block((SIZE_T)(bddm->maxvars*sizeof(bdd_indexindex_type)));
1043  bddm->indexes[BDD_CONST_INDEXINDEX]=BDD_MAX_INDEX;
1044  for (i=0; i < REC_MGRS; ++i)
1045    bddm->rms[i]=mem_new_rec_mgr(MIN_REC_SIZE+ALLOC_ALIGNMENT*i);
1046  bddm->temp_assoc.assoc=(bdd *)mem_get_block((SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
1047  bddm->temp_assoc.last= -1;
1048  for (i=0; i < bddm->maxvars; ++i)
1049    bddm->temp_assoc.assoc[i+1]=0;
1050  bddm->curr_assoc_id= -1;
1051  bddm->curr_assoc= &bddm->temp_assoc;
1052  bddm->assocs=0;
1053  bddm->temp_op= -1;
1054  bddm->super_block=(block)BDD_NEW_REC(bddm, sizeof(struct block_));
1055  bddm->super_block->num_children=0;
1056  bddm->super_block->children=0;
1057  bddm->super_block->reorderable=1;
1058  bddm->super_block->first_index= -1;
1059  bddm->super_block->last_index=0;
1060  cmu_bdd_init_unique(bddm);
1061  cmu_bdd_init_cache(bddm);
1062  bddm->one=bdd_find_terminal(bddm, ~(INT_PTR)0, ~(INT_PTR)0);
1063  bddm->one->refs=BDD_MAX_REFS;
1064  bddm->one->mark=0;
1065  bddm->zero=BDD_NOT(bddm->one);
1066  if (sizeof(double) > 2*sizeof(long))
1067    cmu_bdd_warning("cmu_bdd_init: portability problem for cmu_bdd_satisfying_fraction");
1068  return (bddm);
1069}
1070
1071
1072/* cmu_bdd_quit(bddm) frees all storage associated with the BDD manager */
1073/* bddm. */
1074
1075void
1076cmu_bdd_quit(cmu_bdd_manager bddm)
1077{
1078  int i;
1079  assoc_list p, q;
1080
1081  cmu_bdd_free_unique(bddm);
1082  cmu_bdd_free_cache(bddm);
1083  mem_free_block((pointer)bddm->variables);
1084  mem_free_block((pointer)bddm->indexes);
1085  mem_free_block((pointer)bddm->indexindexes);
1086  mem_free_block((pointer)bddm->temp_assoc.assoc);
1087  for (p=bddm->assocs; p; p=q)
1088    {
1089      q=p->next;
1090      mem_free_block((pointer)p->va.assoc);
1091      BDD_FREE_REC(bddm, (pointer)p, sizeof(struct assoc_list_));
1092    }
1093  BDD_FREE_REC(bddm, (pointer)bddm->super_block, sizeof(struct block_));
1094  for (i=0; i < REC_MGRS; ++i)
1095    mem_free_rec_mgr(bddm->rms[i]);
1096  mem_free_block((pointer)bddm);
1097}
Note: See TracBrowser for help on using the repository browser.