ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
gasp.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: gasp.c
12
13 The "last_gasp" heuristic computes the reduction of each cube in
14 the cover (without replacement) and then performs an expansion of
15 these cubes. The cubes which expand to cover some other cube are
16 added to the original cover and irredundant finds a minimal subset.
17
18 If one of the reduced cubes expands to cover some other reduced
19 cube, then the new prime thus generated is a candidate for reducing
20 the size of the cover.
21
22 super_gasp is a variation on this strategy which extracts a minimal
23 subset from the set of all prime implicants which cover all
24 maximally reduced cubes.
25*/
26
27#include "espresso.h"
28
30
31
32
33/*
34 * reduce_gasp -- compute the maximal reduction of each cube of F
35 *
36 * If a cube does not reduce, it remains prime; otherwise, it is marked
37 * as nonprime. If the cube is redundant (should NEVER happen here) we
38 * just crap out ...
39 *
40 * A cover with all of the cubes of F is returned. Those that did
41 * reduce are marked "NONPRIME"; those that reduced are marked "PRIME".
42 * The cubes are in the same order as in F.
43 */
44static pcover reduce_gasp(F, D)
45pcover F, D;
46{
47 pcube p, last, cunder, *FD;
48 pcover G;
49
50 G = new_cover(F->count);
51 FD = cube2list(F, D);
52
53 /* Reduce cubes of F without replacement */
54 foreach_set(F, last, p) {
55 cunder = reduce_cube(FD, p);
56 if (setp_empty(cunder)) {
57 fatal("empty reduction in reduce_gasp, shouldn't happen");
58 } else if (setp_equal(cunder, p)) {
59 SET(cunder, PRIME); /* just to make sure */
60 G = sf_addset(G, p); /* it did not reduce ... */
61 } else {
62 RESET(cunder, PRIME); /* it reduced ... */
63 G = sf_addset(G, cunder);
64 }
65 if (debug & GASP) {
66 printf("REDUCE_GASP: %s reduced to %s\n", pc1(p), pc2(cunder));
67 }
68 free_cube(cunder);
69 }
70
71 free_cubelist(FD);
72 return G;
73}
74
75/*
76 * expand_gasp -- expand each nonprime cube of F into a prime implicant
77 *
78 * The gasp strategy differs in that only those cubes which expand to
79 * cover some other cube are saved; also, all cubes are expanded
80 * regardless of whether they become covered or not.
81 */
82
83pcover expand_gasp(F, D, R, Foriginal)
85IN pcover D;
86IN pcover R;
87IN pcover Foriginal;
88{
89 int c1index;
90 pcover G;
91
92 /* Try to expand each nonprime and noncovered cube */
93 G = new_cover(10);
94 for(c1index = 0; c1index < F->count; c1index++) {
95 expand1_gasp(F, D, R, Foriginal, c1index, &G);
96 }
97 G = sf_dupl(G);
98 G = expand(G, R, /*nonsparse*/ FALSE); /* Make them prime ! */
99 return G;
100}
101
102
103
104/*
105 * expand1 -- Expand a single cube against the OFF-set, using the gasp strategy
106 */
107void expand1_gasp(F, D, R, Foriginal, c1index, G)
108pcover F; /* reduced cubes of ON-set */
109pcover D; /* DC-set */
110pcover R; /* OFF-set */
111pcover Foriginal; /* ON-set before reduction (same order as F) */
112int c1index; /* which index of F (or Freduced) to be checked */
113pcover *G;
114{
115 register int c2index;
116 register pcube p, last, c2under;
117 pcube RAISE, FREESET, temp, *FD, c2essential;
118 pcover F1;
119
120 if (debug & EXPAND1) {
121 printf("\nEXPAND1_GASP: \t%s\n", pc1(GETSET(F, c1index)));
122 }
123
124 RAISE = new_cube();
125 FREESET = new_cube();
126 temp = new_cube();
127
128 /* Initialize the OFF-set */
129 R->active_count = R->count;
130 foreach_set(R, last, p) {
131 SET(p, ACTIVE);
132 }
133 /* Initialize the reduced ON-set, all nonprime cubes become active */
134 F->active_count = F->count;
135 foreachi_set(F, c2index, c2under) {
136 if (c1index == c2index || TESTP(c2under, PRIME)) {
137 F->active_count--;
138 RESET(c2under, ACTIVE);
139 } else {
140 SET(c2under, ACTIVE);
141 }
142 }
143
144 /* Initialize the raising and unassigned sets */
145 (void) set_copy(RAISE, GETSET(F, c1index));
146 (void) set_diff(FREESET, cube.fullset, RAISE);
147
148 /* Determine parts which must be lowered */
149 essen_parts(R, F, RAISE, FREESET);
150
151 /* Determine parts which can always be raised */
152 essen_raising(R, RAISE, FREESET);
153
154 /* See which, if any, of the reduced cubes we can cover */
155 foreachi_set(F, c2index, c2under) {
156 if (TESTP(c2under, ACTIVE)) {
157 /* See if this cube can be covered by an expansion */
158 if (setp_implies(c2under, RAISE) ||
159 feasibly_covered(R, c2under, RAISE, temp)) {
160
161 /* See if c1under can expanded to cover c2 reduced against
162 * (F - c1) u c1under; if so, c2 can definitely be removed !
163 */
164
165 /* Copy F and replace c1 with c1under */
166 F1 = sf_save(Foriginal);
167 (void) set_copy(GETSET(F1, c1index), GETSET(F, c1index));
168
169 /* Reduce c2 against ((F - c1) u c1under) */
170 FD = cube2list(F1, D);
171 c2essential = reduce_cube(FD, GETSET(F1, c2index));
172 free_cubelist(FD);
173 sf_free(F1);
174
175 /* See if c2essential is covered by an expansion of c1under */
176 if (feasibly_covered(R, c2essential, RAISE, temp)) {
177 (void) set_or(temp, RAISE, c2essential);
178 RESET(temp, PRIME); /* cube not prime */
179 *G = sf_addset(*G, temp);
180 }
181 set_free(c2essential);
182 }
183 }
184 }
185
186 free_cube(RAISE);
187 free_cube(FREESET);
188 free_cube(temp);
189}
190
191/* irred_gasp -- Add new primes to F and find an irredundant subset */
193pcover F, D, G; /* G is disposed of */
194{
195 if (G->count != 0)
196 F = irredundant(sf_append(F, G), D);
197 else
198 free_cover(G);
199 return F;
200}
201
202
203/* last_gasp */
204pcover last_gasp(F, D, R, cost)
205pcover F, D, R;
206cost_t *cost;
207{
208 pcover G, G1;
209
210 EXECUTE(G = reduce_gasp(F, D), GREDUCE_TIME, G, *cost);
211 EXECUTE(G1 = expand_gasp(G, D, R, F), GEXPAND_TIME, G1, *cost);
212 free_cover(G);
213 EXECUTE(F = irred_gasp(F, D, G1), GIRRED_TIME, F, *cost);
214 return F;
215}
216
217
218/* super_gasp */
219pcover super_gasp(F, D, R, cost)
220pcover F, D, R;
221cost_t *cost;
222{
223 pcover G, G1;
224
225 EXECUTE(G = reduce_gasp(F, D), GREDUCE_TIME, G, *cost);
226 EXECUTE(G1 = all_primes(G, R), GEXPAND_TIME, G1, *cost);
227 free_cover(G);
228 EXEC(G = sf_dupl(sf_append(F, G1)), "NEWPRIMES", G);
229 EXECUTE(F = irredundant(G, D), IRRED_TIME, F, *cost);
230 return F;
231}
233
#define FALSE
Definition abcBm.c:37
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define pcover
Definition espresso.h:264
pset_family sf_addset()
#define new_cube()
Definition espresso.h:262
char * pc1()
pcover expand()
pcover all_primes()
void essen_parts()
#define GEXPAND_TIME
Definition espresso.h:379
#define set_free(r)
Definition espresso.h:167
#define foreachi_set(R, i, p)
Definition espresso.h:143
#define TESTP(set, flag)
Definition espresso.h:124
pcover expand_gasp()
struct cost_struct cost_t
#define ACTIVE
Definition espresso.h:129
pcover irred_gasp()
void essen_raising()
#define EXPAND1
Definition espresso.h:354
void fatal()
#define GASP
Definition espresso.h:355
pcube * cube2list()
#define INOUT
Definition espresso.h:334
pset_family sf_dupl()
void sf_free()
#define pcube
Definition espresso.h:261
#define EXECUTE(fct, i, S, cost)
Definition espresso.h:422
#define free_cover(r)
Definition espresso.h:266
pcover super_gasp()
#define GETSET(family, index)
Definition espresso.h:161
#define GREDUCE_TIME
Definition espresso.h:381
pset set_diff()
#define free_cube(r)
Definition espresso.h:263
pset_family sf_save()
char * pc2()
#define foreach_set(R, last, p)
Definition espresso.h:135
unsigned int debug
Definition globals.c:19
#define SET(set, flag)
Definition espresso.h:122
#define IRRED_TIME
Definition espresso.h:377
pcube reduce_cube()
bool setp_empty()
bool setp_implies()
#define IN
Definition espresso.h:332
#define RESET(set, flag)
Definition espresso.h:123
#define PRIME
Definition espresso.h:127
bool feasibly_covered()
#define GIRRED_TIME
Definition espresso.h:380
pcover irredundant()
pcover last_gasp()
pset set_or()
#define EXEC(fct, name, S)
Definition espresso.h:418
pset_family sf_append()
void expand1_gasp()
bool setp_equal()
pset set_copy()
#define free_cubelist(T)
Definition espresso.h:267
#define new_cover(i)
Definition espresso.h:265
Cube * p
Definition exorList.c:222
Definition exor.h:123