source: vis_dev/glu-2.3/src/cmuBdd/bddswap.c @ 104

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

library glu 2.3
File size: 4.2 KB
Line 
1/* BDD variable exchange routine */
2
3
4#include "bddint.h"
5
6
7static
8bdd
9cmu_bdd_swap_vars_aux_step(cmu_bdd_manager bddm, bdd f, bdd g, bdd h, bdd_indexindex_type h_indexindex, long op)
10{
11  bdd_indexindex_type top_indexindex;
12  bdd_index_type f_index, g_index;
13  bdd f1, f2;
14  bdd g1, g2;
15  bdd temp1, temp2;
16  bdd result;
17
18  BDD_SETUP(f);
19  BDD_SETUP(g);
20  f_index=BDD_INDEX(bddm, f);
21  g_index=BDD_INDEX(bddm, g);
22  if (f_index == bddm->indexes[h_indexindex])
23    {
24      if (op & 1)
25        f=BDD_THEN(f);
26      else
27        f=BDD_ELSE(f);
28      BDD_RESET(f);
29    }
30  if (g_index == bddm->indexes[h_indexindex])
31    {
32      if (op & 1)
33        g=BDD_THEN(g);
34      else
35        g=BDD_ELSE(g);
36      BDD_RESET(g);
37    }
38  if (f == g)
39    {
40    if (op & 1)
41      return (cmu_bdd_compose_temp(bddm, f, h, BDD_ONE(bddm)));
42    else
43      return (cmu_bdd_compose_temp(bddm, f, h, BDD_ZERO(bddm)));
44    }
45  if (f_index >= bddm->indexes[h_indexindex] && g_index >= bddm->indexes[h_indexindex])
46    {
47      BDD_TEMP_INCREFS(f);
48      BDD_TEMP_INCREFS(g);
49      return (bdd_find(bddm, h_indexindex, f, g));
50    }
51  if (bdd_lookup_in_cache2(bddm, op, f, g, &result))
52    return (result);
53  BDD_TOP_VAR2(top_indexindex, bddm, f, g);
54  BDD_COFACTOR(top_indexindex, f, f1, f2);
55  BDD_COFACTOR(top_indexindex, g, g1, g2);
56  temp1=cmu_bdd_swap_vars_aux_step(bddm, f1, g1, h, h_indexindex, op);
57  temp2=cmu_bdd_swap_vars_aux_step(bddm, f2, g2, h, h_indexindex, op);
58  result=bdd_find(bddm, top_indexindex, temp1, temp2);
59  bdd_insert_in_cache2(bddm, op, f, g, result);
60  return (result);
61}
62
63
64static
65bdd
66cmu_bdd_swap_vars_step(cmu_bdd_manager bddm, bdd f, bdd_indexindex_type g_indexindex, bdd h, long op)
67{
68  bdd_index_type f_index;
69  bdd temp1, temp2;
70  bdd result;
71
72  BDD_SETUP(f);
73  if (BDD_IS_CONST(f))
74    return (f);
75  if (bdd_lookup_in_cache2(bddm, op, f, h, &result))
76    return (result);
77  f_index=BDD_INDEX(bddm, f);
78  if (f_index > bddm->indexes[g_indexindex])
79    {
80      temp1=cmu_bdd_compose_temp(bddm, f, h, BDD_ONE(bddm));
81      temp2=cmu_bdd_compose_temp(bddm, f, h, BDD_ZERO(bddm));
82      result=bdd_find(bddm, g_indexindex, temp1, temp2);
83    }
84  else if (f_index < bddm->indexes[g_indexindex])
85    {
86      temp1=cmu_bdd_swap_vars_step(bddm, BDD_THEN(f), g_indexindex, h, op);
87      temp2=cmu_bdd_swap_vars_step(bddm, BDD_ELSE(f), g_indexindex, h, op);
88      result=bdd_find(bddm, BDD_INDEXINDEX(f), temp1, temp2);
89    }
90  else
91    {
92      BDD_SETUP(h);
93      temp1=cmu_bdd_swap_vars_aux_step(bddm, BDD_THEN(f), BDD_ELSE(f), h, BDD_INDEXINDEX(h), OP_SWAPAUX+2*BDD_INDEXINDEX(h)+1);
94      temp2=cmu_bdd_swap_vars_aux_step(bddm, BDD_THEN(f), BDD_ELSE(f), h, BDD_INDEXINDEX(h), OP_SWAPAUX+2*BDD_INDEXINDEX(h));
95      result=bdd_find(bddm, g_indexindex, temp1, temp2);
96    }
97  bdd_insert_in_cache2(bddm, op, f, h, result);
98  return (result);
99}
100
101
102bdd
103cmu_bdd_swap_vars_temp(cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
104{
105  bdd_index_type g_index, h_index;
106
107  BDD_SETUP(f);
108  BDD_SETUP(g);
109  BDD_SETUP(h);
110  g_index=BDD_INDEX(bddm, g);
111  h_index=BDD_INDEX(bddm, h);
112  if (g_index == h_index)
113    {
114      BDD_TEMP_INCREFS(f);
115      return (f);
116    }
117  if (g_index > h_index)
118    return (cmu_bdd_swap_vars_step(bddm, f, BDD_INDEXINDEX(h), g, OP_SWAP+BDD_INDEXINDEX(h)));
119  else
120    return (cmu_bdd_swap_vars_step(bddm, f, BDD_INDEXINDEX(g), h, OP_SWAP+BDD_INDEXINDEX(g)));
121}
122
123
124/* cmu_bdd_swap_vars(bddm, f, g, h) substitutes g for h and h for g in f. */
125
126bdd
127cmu_bdd_swap_vars(cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
128{
129  bdd_index_type g_index, h_index;
130
131  if (bdd_check_arguments(3, f, g, h))
132    {
133      BDD_SETUP(f);
134      BDD_SETUP(g);
135      BDD_SETUP(h);
136      if (cmu_bdd_type_aux(bddm, g) != BDD_TYPE_POSVAR || cmu_bdd_type_aux(bddm, h) != BDD_TYPE_POSVAR)
137        {
138          cmu_bdd_warning("cmu_bdd_swap_vars: second and third arguments are not both positive variables");
139          BDD_INCREFS(f);
140          return (f);
141        }
142      FIREWALL(bddm);
143      g_index=BDD_INDEX(bddm, g);
144      h_index=BDD_INDEX(bddm, h);
145      if (g_index == h_index)
146        {
147          BDD_INCREFS(f);
148          return (f);
149        }
150      if (g_index > h_index)
151        RETURN_BDD(cmu_bdd_swap_vars_step(bddm, f, BDD_INDEXINDEX(h), g, OP_SWAP+BDD_INDEXINDEX(h)));
152      else
153        RETURN_BDD(cmu_bdd_swap_vars_step(bddm, f, BDD_INDEXINDEX(g), h, OP_SWAP+BDD_INDEXINDEX(g)));
154    }
155  return ((bdd)0);
156}
Note: See TracBrowser for help on using the repository browser.