source: vis_dev/glu-2.3/src/cmuBdd/bddreduce.c @ 23

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

library glu 2.3
File size: 3.2 KB
Line 
1/* BDD reduce routines */
2
3
4#include "bddint.h"
5
6
7static
8bdd
9cmu_bdd_reduce_step(cmu_bdd_manager bddm, bdd f, bdd c)
10{
11  bdd_indexindex_type top_indexindex;
12  bdd f1, f2;
13  bdd c1, c2;
14  bdd temp1, temp2;
15  bdd result;
16
17  BDD_SETUP(f);
18  BDD_SETUP(c);
19  if (BDD_IS_CONST(c))
20    {
21      if (c == BDD_ZERO(bddm))
22        return ((bdd)0);
23      BDD_TEMP_INCREFS(f);
24      return (f);
25    }
26  if (BDD_IS_CONST(f))
27    return (f);
28  if (bdd_lookup_in_cache2(bddm, OP_RED, f, c, &result))
29    return (result);
30  BDD_TOP_VAR2(top_indexindex, bddm, f, c);
31  BDD_COFACTOR(top_indexindex, f, f1, f2);
32  BDD_COFACTOR(top_indexindex, c, c1, c2);
33  if (f == f1)
34    {
35      bddm->op_cache.cache_level++;
36      temp1=cmu_bdd_ite_step(bddm, c1, BDD_ONE(bddm), c2);
37      bddm->op_cache.cache_level--;
38      result=cmu_bdd_reduce_step(bddm, f, temp1);
39      {
40        BDD_SETUP(temp1);
41        BDD_TEMP_DECREFS(temp1);
42      }
43    }
44  else
45    {
46      temp1=cmu_bdd_reduce_step(bddm, f1, c1);
47      temp2=cmu_bdd_reduce_step(bddm, f2, c2);
48      if (!temp1)
49        result=temp2;
50      else if (!temp2)
51        result=temp1;
52      else
53        result=bdd_find(bddm, top_indexindex, temp1, temp2);
54    }
55  bdd_insert_in_cache2(bddm, OP_RED, f, c, result);
56  return (result);
57}
58
59
60/* cmu_bdd_reduce(bddm, f, c) returns a BDD which agrees with f for all */
61/* valuations for which c is true, and which is hopefully smaller than */
62/* f. */
63
64bdd
65cmu_bdd_reduce(cmu_bdd_manager bddm, bdd f, bdd c)
66{
67  bdd result;
68
69  if (bdd_check_arguments(2, f, c))
70    {
71      FIREWALL(bddm);
72      result=cmu_bdd_reduce_step(bddm, f, c);
73      if (!result)
74        return (BDD_ZERO(bddm));
75      RETURN_BDD(result);
76    }
77  return ((bdd)0);
78}
79
80
81static
82bdd
83cmu_bdd_cofactor_step(cmu_bdd_manager bddm, bdd f, bdd c)
84{
85  bdd_indexindex_type top_indexindex;
86  bdd f1, f2;
87  bdd c1, c2;
88  bdd temp1, temp2;
89  bdd result;
90
91  BDD_SETUP(f);
92  BDD_SETUP(c);
93  if (BDD_IS_CONST(c))
94    {
95      if (c == BDD_ZERO(bddm))
96        return ((bdd)0);
97      BDD_TEMP_INCREFS(f);
98      return (f);
99    }
100  if (BDD_IS_CONST(f))
101    return (f);
102  if (bdd_lookup_in_cache2(bddm, OP_COFACTOR, f, c, &result))
103    return (result);
104  BDD_TOP_VAR2(top_indexindex, bddm, f, c);
105  BDD_COFACTOR(top_indexindex, f, f1, f2);
106  BDD_COFACTOR(top_indexindex, c, c1, c2);
107  temp1=cmu_bdd_cofactor_step(bddm, f1, c1);
108  temp2=cmu_bdd_cofactor_step(bddm, f2, c2);
109  if (!temp1)
110    result=temp2;
111  else if (!temp2)
112    result=temp1;
113  else
114    result=bdd_find(bddm, top_indexindex, temp1, temp2);
115  bdd_insert_in_cache2(bddm, OP_COFACTOR, f, c, result);
116  return (result);
117}
118
119
120/* cmu_bdd_cofactor(bddm, f, c) returns a BDD for the generalized cofactor */
121/* of f by c.  This operation has the useful property that if */
122/* [f1, ..., fn] is a function vector and fi|c denotes the g.c. of fi */
123/* by c, then the image of [f1|c, ..., fn|c] over all valuations is */
124/* the same as the image of [f1, ..., fn] over the valuations for */
125/* which c is true. */
126
127bdd
128cmu_bdd_cofactor(cmu_bdd_manager bddm, bdd f, bdd c)
129{
130  if (bdd_check_arguments(2, f, c))
131    {
132      if (c == BDD_ZERO(bddm))
133        {
134          cmu_bdd_warning("cmu_bdd_cofactor: second argument is false");
135          return (BDD_ONE(bddm));
136        }
137      FIREWALL(bddm);
138      RETURN_BDD(cmu_bdd_cofactor_step(bddm, f, c));
139    }
140  return ((bdd)0);
141}
Note: See TracBrowser for help on using the repository browser.