abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
essen.c
Go to the documentation of this file.
1 /*
2  * Revision Control Information
3  *
4  * $Source$
5  * $Author$
6  * $Revision$
7  * $Date$
8  *
9  */
10 /*
11  module: essen.c
12  purpose: Find essential primes in a multiple-valued function
13 */
14 
15 #include "espresso.h"
16 
18 
19 
20 /*
21  essential -- return a cover consisting of the cubes of F which are
22  essential prime implicants (with respect to F u D); Further, remove
23  these cubes from the ON-set F, and add them to the OFF-set D.
24 
25  Sometimes EXPAND can determine that a cube is not an essential prime.
26  If so, it will set the "NONESSEN" flag in the cube.
27 
28  We count on IRREDUNDANT to have set the flag RELESSEN to indicate
29  that a prime was relatively essential (i.e., covers some minterm
30  not contained in any other prime in the current cover), or to have
31  reset the flag to indicate that a prime was relatively redundant
32  (i.e., all minterms covered by other primes in the current cover).
33  Of course, after executing irredundant, all of the primes in the
34  cover are relatively essential, but we can mark the primes which
35  were redundant at the start of irredundant and avoid an extra check
36  on these primes for essentiality.
37 */
38 
40 IN pcover *Fp, *Dp;
41 {
42  register pcube last, p;
43  pcover E, F = *Fp, D = *Dp;
44 
45  /* set all cubes in F active */
46  (void) sf_active(F);
47 
48  /* Might as well start out with some cubes in E */
49  E = new_cover(10);
50 
51  foreach_set(F, last, p) {
52  /* don't test a prime which EXPAND says is nonessential */
53  if (! TESTP(p, NONESSEN)) {
54  /* only test a prime which was relatively essential */
55  if (TESTP(p, RELESSEN)) {
56  /* Check essentiality */
57  if (essen_cube(F, D, p)) {
58  if (debug & ESSEN)
59  printf("ESSENTIAL: %s\n", pc1(p));
60  E = sf_addset(E, p);
61  RESET(p, ACTIVE);
62  F->active_count--;
63  }
64  }
65  }
66  }
67 
68  *Fp = sf_inactive(F); /* delete the inactive cubes from F */
69  *Dp = sf_join(D, E); /* add the essentials to D */
70  sf_free(D);
71  return E;
72 }
73 
74 /*
75  essen_cube -- check if a single cube is essential or not
76 
77  The prime c is essential iff
78 
79  consensus((F u D) # c, c) u D
80 
81  does not contain c.
82 */
83 bool essen_cube(F, D, c)
84 IN pcover F, D;
85 IN pcube c;
86 {
87  pcover H, FD;
88  pcube *H1;
89  bool essen;
90 
91  /* Append F and D together, and take the sharp-consensus with c */
92  FD = sf_join(F, D);
93  H = cb_consensus(FD, c);
94  free_cover(FD);
95 
96  /* Add the don't care set, and see if this covers c */
97  H1 = cube2list(H, D);
98  essen = ! cube_is_covered(H1, c);
99  free_cubelist(H1);
100 
101  free_cover(H);
102  return essen;
103 }
104 
105 
106 /*
107  * cb_consensus -- compute consensus(T # c, c)
108  */
110 register pcover T;
111 register pcube c;
112 {
113  register pcube temp, last, p;
114  register pcover R;
115 
116  R = new_cover(T->count*2);
117  temp = new_cube();
118  foreach_set(T, last, p) {
119  if (p != c) {
120  switch (cdist01(p, c)) {
121  case 0:
122  /* distance-0 needs special care */
123  R = cb_consensus_dist0(R, p, c);
124  break;
125 
126  case 1:
127  /* distance-1 is easy because no sharping required */
128  consensus(temp, p, c);
129  R = sf_addset(R, temp);
130  break;
131  }
132  }
133  }
134  set_free(temp);
135  return R;
136 }
137 
138 
139 /*
140  * form the sharp-consensus for p and c when they intersect
141  * What we are forming is consensus(p # c, c).
142  */
144 pcover R;
145 register pcube p, c;
146 {
147  int var;
148  bool got_one;
149  register pcube temp, mask;
150  register pcube p_diff_c=cube.temp[0], p_and_c=cube.temp[1];
151 
152  /* If c contains p, then this gives us no information for essential test */
153  if (setp_implies(p, c)) {
154  return R;
155  }
156 
157  /* For the multiple-valued variables */
158  temp = new_cube();
159  got_one = FALSE;
160  INLINEset_diff(p_diff_c, p, c);
161  INLINEset_and(p_and_c, p, c);
162 
163  for(var = cube.num_binary_vars; var < cube.num_vars; var++) {
164  /* Check if c(var) is contained in p(var) -- if so, no news */
165  mask = cube.var_mask[var];
166  if (! setp_disjoint(p_diff_c, mask)) {
167  INLINEset_merge(temp, c, p_and_c, mask);
168  R = sf_addset(R, temp);
169  got_one = TRUE;
170  }
171  }
172 
173  /* if no cube so far, add one for the intersection */
174  if (! got_one && cube.num_binary_vars > 0) {
175  /* Add a single cube for the intersection of p and c */
176  INLINEset_and(temp, p, c);
177  R = sf_addset(R, temp);
178  }
179 
180  set_free(temp);
181  return R;
182 }
184 
int cdist01()
#define INLINEset_diff(r, a, b)
Definition: espresso.h:208
#define set_free(r)
Definition: espresso.h:167
#define FALSE
Definition: cudd.h:91
#define new_cube()
Definition: espresso.h:262
char * pc1(pcube c)
Definition: cvrout.c:379
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define free_cover(r)
Definition: espresso.h:266
#define pcover
Definition: espresso.h:264
pcover cb_consensus(pcover T, pcube c)
Definition: essen.c:109
int var(Lit p)
Definition: SolverTypes.h:62
#define INLINEset_and(r, a, b)
Definition: espresso.h:202
ABC_NAMESPACE_IMPL_START pcover essential(IN pcover *Fp, IN pcover *Dp)
Definition: essen.c:39
pcover cb_consensus_dist0(pcover R, pcube p, pcube c)
Definition: essen.c:143
void sf_free()
bool setp_disjoint()
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define RESET(set, flag)
Definition: espresso.h:123
#define IN
Definition: espresso.h:332
pset_family sf_addset()
pset_family sf_join()
#define NONESSEN
Definition: espresso.h:128
unsigned int debug
Definition: globals.c:19
bool cube_is_covered()
pcube * cube2list(pcover A, pcover B)
Definition: cofactor.c:306
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
#define new_cover(i)
Definition: espresso.h:265
bool essen_cube(IN pcover F, IN pcover D, IN pcube c)
Definition: essen.c:83
#define INLINEset_merge(r, a, b, mask)
Definition: espresso.h:225
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
#define TRUE
Definition: cudd.h:88
#define free_cubelist(T)
Definition: espresso.h:267
#define ESSEN
Definition: espresso.h:352
pset_family sf_active()
void consensus()
bool setp_implies()
#define TESTP(set, flag)
Definition: espresso.h:124
#define ACTIVE
Definition: espresso.h:129
pset_family sf_inactive()
#define RELESSEN
Definition: espresso.h:132
#define pcube
Definition: espresso.h:261