source: vis_dev/glu-2.3/src/cmuBdd/bddcomp.c @ 76

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

library glu 2.3

File size: 5.3 KB
Line 
1/* BDD composition routines */
2
3
4#include "bddint.h"
5
6
7static
8bdd
9bdd_restrict_step(cmu_bdd_manager bddm, bdd f, bdd_indexindex_type g_indexindex, bdd h, long op)
10{
11  bdd temp1, temp2;
12  bdd result;
13
14  BDD_SETUP(f);
15  if (BDD_INDEX(bddm, f) > bddm->indexes[g_indexindex])
16    {
17      /* f doesn't depend on the variable g. */
18      BDD_TEMP_INCREFS(f);
19      return (f);
20    }
21  if (BDD_INDEXINDEX(f) == g_indexindex)
22    {
23      /* Do the restriction. */
24      result=(h == BDD_ONE(bddm) ? BDD_THEN(f) : BDD_ELSE(f));
25      {
26        BDD_SETUP(result);
27        BDD_TEMP_INCREFS(result);
28        return (result);
29      }
30    }
31  if (bdd_lookup_in_cache2(bddm, op, BDD_OUTPOS(f), h, &result))
32    return (BDD_IS_OUTPOS(f) ? result : BDD_NOT(result));
33  temp1=bdd_restrict_step(bddm, BDD_THEN(f), g_indexindex, h, op);
34  temp2=bdd_restrict_step(bddm, BDD_ELSE(f), g_indexindex, h, op);
35  result=bdd_find(bddm, BDD_INDEXINDEX(f), temp1, temp2);
36  if (BDD_IS_OUTPOS(f))
37    bdd_insert_in_cache2(bddm, op, f, h, result);
38  else
39    bdd_insert_in_cache2(bddm, op, BDD_NOT(f), h, BDD_NOT(result));
40  return (result);
41}
42
43
44static
45bdd
46cmu_bdd_compose_step(cmu_bdd_manager bddm, bdd f, bdd_indexindex_type g_indexindex, bdd h, long op)
47{
48  bdd_indexindex_type top_indexindex;
49  bdd f1, f2;
50  bdd h1, h2;
51  bdd temp1, temp2;
52  bdd result;
53
54  BDD_SETUP(f);
55  BDD_SETUP(h);
56  /* Use restriction if possible. */
57  if (BDD_IS_CONST(h))
58    return (bdd_restrict_step(bddm, f, g_indexindex, h, op));
59  if (BDD_INDEX(bddm, f) > bddm->indexes[g_indexindex])
60    {
61      /* f doesn't depend on the variable g. */
62      BDD_TEMP_INCREFS(f);
63      return (f);
64    }
65  if (bdd_lookup_in_cache2(bddm, op, BDD_OUTPOS(f), h, &result))
66    return (BDD_IS_OUTPOS(f) ? result : BDD_NOT(result));
67  if (BDD_INDEXINDEX(f) == g_indexindex)
68    {
69      /* Do the replacement. */
70      bddm->op_cache.cache_level++;
71      result=cmu_bdd_ite_step(bddm, h, BDD_THEN(f), BDD_ELSE(f));
72      bddm->op_cache.cache_level--;
73    }
74  else
75    {
76      BDD_TOP_VAR2(top_indexindex, bddm, f, h);
77      BDD_COFACTOR(top_indexindex, f, f1, f2);
78      BDD_COFACTOR(top_indexindex, h, h1, h2);
79      temp1=cmu_bdd_compose_step(bddm, f1, g_indexindex, h1, op);
80      temp2=cmu_bdd_compose_step(bddm, f2, g_indexindex, h2, op);
81      result=bdd_find(bddm, top_indexindex, temp1, temp2);
82    }
83  if (BDD_IS_OUTPOS(f))
84    bdd_insert_in_cache2(bddm, op, f, h, result);
85  else
86    bdd_insert_in_cache2(bddm, op, BDD_NOT(f), h, BDD_NOT(result));
87  return (result);
88}
89
90
91/* cmu_bdd_compose_temp is used internally by cmu_bdd_swap_vars. */
92
93bdd
94cmu_bdd_compose_temp(cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
95{
96  BDD_SETUP(g);
97  return (cmu_bdd_compose_step(bddm, f, BDD_INDEXINDEX(g), h, OP_COMP+BDD_INDEXINDEX(g)));
98}
99
100
101/* cmu_bdd_compose(bddm, f, g, h) returns the BDD for substituting h for */
102/* the variable g in f.  h may depend on g. */
103
104bdd
105cmu_bdd_compose(cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
106{
107  if (bdd_check_arguments(3, f, g, h))
108    {
109      BDD_SETUP(f);
110      BDD_SETUP(g);
111      if (cmu_bdd_type_aux(bddm, g) != BDD_TYPE_POSVAR)
112        {
113          cmu_bdd_warning("cmu_bdd_compose: second argument is not a positive variable");
114          BDD_INCREFS(f);
115          return (f);
116        }
117      FIREWALL(bddm);
118      RETURN_BDD(cmu_bdd_compose_step(bddm, f, BDD_INDEXINDEX(g), h, OP_COMP+BDD_INDEXINDEX(g)));
119    }
120  return ((bdd)0);
121}
122
123
124bdd
125cmu_bdd_substitute_step(cmu_bdd_manager bddm, bdd f, long op, bdd (*ite_fn)(cmu_bdd_manager, bdd, bdd, bdd), var_assoc subst)
126{
127  bdd g;
128  bdd temp1, temp2;
129  bdd result;
130  bdd_index_type g_index;
131
132  BDD_SETUP(f);
133  if ((long)BDD_INDEX(bddm, f) > subst->last)
134    {
135      BDD_TEMP_INCREFS(f);
136      return (f);
137    }
138  if (bdd_lookup_in_cache1(bddm, op, BDD_OUTPOS(f), &result))
139    return (BDD_IS_OUTPOS(f) ? result : BDD_NOT(result));
140  g=subst->assoc[BDD_INDEXINDEX(f)];
141  /* See if we are substituting a constant at this level. */
142  if (g == BDD_ONE(bddm))
143    return (cmu_bdd_substitute_step(bddm, BDD_THEN(f), op, ite_fn, subst));
144  if (g == BDD_ZERO(bddm))
145    return (cmu_bdd_substitute_step(bddm, BDD_ELSE(f), op, ite_fn, subst));
146  temp1=cmu_bdd_substitute_step(bddm, BDD_THEN(f), op, ite_fn, subst);
147  temp2=cmu_bdd_substitute_step(bddm, BDD_ELSE(f), op, ite_fn, subst);
148  if (!g)
149    g=BDD_IF(bddm, f);
150  {
151    BDD_SETUP(g);
152    BDD_SETUP(temp1);
153    BDD_SETUP(temp2);
154    if (g == BDD_IF(bddm, g) &&
155        (g_index=BDD_INDEX(bddm, g)) < BDD_INDEX(bddm, temp1) &&
156        g_index < BDD_INDEX(bddm, temp2))
157      /* Substituting with variable above the tops of the subresults. */
158      result=bdd_find(bddm, BDD_INDEXINDEX(g), temp1, temp2);
159    else
160      {
161        /* Do an ITE. */
162        bddm->op_cache.cache_level++;
163        result=(*ite_fn)(bddm, g, temp1, temp2);
164        BDD_TEMP_DECREFS(temp1);
165        BDD_TEMP_DECREFS(temp2);
166        bddm->op_cache.cache_level--;
167      }
168  }
169  if (BDD_IS_OUTPOS(f))
170    bdd_insert_in_cache1(bddm, op, f, result);
171  else
172    bdd_insert_in_cache1(bddm, op, BDD_NOT(f), BDD_NOT(result));
173  return (result);
174}
175
176
177/* cmu_bdd_substitute(bddm, f) returns the BDD for substituting in f */
178/* according to the current variable association. */
179
180bdd
181cmu_bdd_substitute(cmu_bdd_manager bddm, bdd f)
182{
183  long op;
184
185  if (bdd_check_arguments(1, f))
186    {
187      FIREWALL(bddm);
188      if (bddm->curr_assoc_id == -1)
189        op=bddm->temp_op--;
190      else
191        op=OP_SUBST+bddm->curr_assoc_id;
192      RETURN_BDD(cmu_bdd_substitute_step(bddm, f, op, cmu_bdd_ite_step, bddm->curr_assoc));
193    }
194  return ((bdd)0);
195}
Note: See TracBrowser for help on using the repository browser.