ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
reduce.c File Reference
#include "espresso.h"
Include dependency graph for reduce.c:

Go to the source code of this file.

Functions

pcover reduce (INOUT pcover F, IN pcover D)
 
pcube reduce_cube (IN pcube *FD, IN pcube p)
 
pcube sccc (INOUT pcube *T)
 
pcube sccc_merge (INOUT register pcube left, INOUT register pcube right, INOUT register pcube cl, INOUT register pcube cr)
 
pcube sccc_cube (pcube result, pcube p)
 
bool sccc_special_cases (INOUT pcube *T, OUT pcube *result)
 

Function Documentation

◆ reduce()

pcover reduce ( INOUT pcover F,
IN pcover D )

Definition at line 59 of file reduce.c.

62{
63 register pcube last, p, cunder, *FD;
64
65 /* Order the cubes */
67 F = random_order(F);
68 else {
69 F = toggle ? sort_reduce(F) : mini_sort(F, descend);
70 toggle = ! toggle;
71 }
72
73 /* Try to reduce each cube */
74 FD = cube2list(F, D);
75 foreach_set(F, last, p) {
76 cunder = reduce_cube(FD, p); /* reduce the cube */
77 if (setp_equal(cunder, p)) { /* see if it actually did */
78 SET(p, ACTIVE); /* cube remains active */
79 SET(p, PRIME); /* cube remains prime ? */
80 } else {
81 if (debug & REDUCE) {
82 printf("REDUCE: %s to %s %s\n",
83 pc1(p), pc2(cunder), print_time(ptime()));
84 }
85 set_copy(p, cunder); /* save reduced version */
86 RESET(p, PRIME); /* cube is no longer prime */
87 if (setp_empty(cunder))
88 RESET(p, ACTIVE); /* if null, kill the cube */
89 else
90 SET(p, ACTIVE); /* cube is active */
91 }
92 free_cube(cunder);
93 }
94 free_cubelist(FD);
95
96 /* Delete any cubes of F which reduced to the empty cube */
97 return sf_inactive(F);
98}
pcover mini_sort(pcover F, int *compare)
Definition cvrm.c:141
char * pc1()
pset_family sf_inactive()
#define ACTIVE
Definition espresso.h:129
#define print_time(t)
Definition espresso.h:22
pcover random_order()
pcube * cube2list()
pcover sort_reduce()
#define pcube
Definition espresso.h:261
#define REDUCE
Definition espresso.h:357
#define free_cube(r)
Definition espresso.h:263
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
pcube reduce_cube()
bool setp_empty()
#define RESET(set, flag)
Definition espresso.h:123
#define PRIME
Definition espresso.h:127
bool use_random_order
Definition globals.c:38
bool setp_equal()
pset set_copy()
#define free_cubelist(T)
Definition espresso.h:267
Cube * p
Definition exorList.c:222
#define ptime()
Definition util_old.h:283
Here is the call graph for this function:

◆ reduce_cube()

pcube reduce_cube ( IN pcube * FD,
IN pcube p )

Definition at line 101 of file reduce.c.

103{
104 pcube cunder;
105
106 cunder = sccc(cofactor(FD, p));
107 return set_and(cunder, cunder, p);
108}
pcube sccc()
pset set_and()
pcube * cofactor()
Here is the call graph for this function:

◆ sccc()

pcube sccc ( INOUT pcube * T)

Definition at line 112 of file reduce.c.

114{
115 pcube r;
116 register pcube cl, cr;
117 register int best;
118 static int sccc_level = 0;
119
120 if (debug & REDUCE1) {
121 debug_print(T, "SCCC", sccc_level++);
122 }
123
124 if (sccc_special_cases(T, &r) == MAYBE) {
125 cl = new_cube();
126 cr = new_cube();
127 best = binate_split_select(T, cl, cr, REDUCE1);
128 r = sccc_merge(sccc(scofactor(T, cl, best)),
129 sccc(scofactor(T, cr, best)), cl, cr);
130 free_cubelist(T);
131 }
132
133 if (debug & REDUCE1)
134 printf("SCCC[%d]: result is %s\n", --sccc_level, pc1(r));
135 return r;
136}
#define new_cube()
Definition espresso.h:262
#define REDUCE1
Definition espresso.h:358
pcube * scofactor()
bool sccc_special_cases()
void debug_print()
pcube sccc_merge()
ABC_NAMESPACE_HEADER_END int binate_split_select()
#define MAYBE
Definition espresso.h:257
Here is the call graph for this function:

◆ sccc_cube()

pcube sccc_cube ( pcube result,
pcube p )

Definition at line 166 of file reduce.c.

168{
169 register pcube temp=cube.temp[0], mask;
170 int var;
171
172 if ((var = cactive(p)) >= 0) {
173 mask = cube.var_mask[var];
174 INLINEset_xor(temp, p, mask);
175 INLINEset_and(result, result, temp);
176 }
177 return result;
178}
#define INLINEset_xor(r, a, b)
Definition espresso.h:218
#define INLINEset_and(r, a, b)
Definition espresso.h:202
int cactive()
unsigned short var
Definition giaNewBdd.h:35
Definition exor.h:123
Here is the call graph for this function:

◆ sccc_merge()

pcube sccc_merge ( INOUT register pcube left,
INOUT register pcube right,
INOUT register pcube cl,
INOUT register pcube cr )

Definition at line 139 of file reduce.c.

142{
143 INLINEset_and(left, left, cl);
144 INLINEset_and(right, right, cr);
145 INLINEset_or(left, left, right);
146 free_cube(right);
147 free_cube(cl);
148 free_cube(cr);
149 return left;
150}
#define INLINEset_or(r, a, b)
Definition espresso.h:205

◆ sccc_special_cases()

bool sccc_special_cases ( INOUT pcube * T,
OUT pcube * result )

Definition at line 184 of file reduce.c.

187{
188 register pcube *T1, p, temp = cube.temp[1], ceil, cof = T[0];
189 pcube *A, *B;
190
191 /* empty cover => complement is universe => SCCC is universe */
192 if (T[2] == NULL) {
193 *result = set_save(cube.fullset);
194 free_cubelist(T);
195 return TRUE;
196 }
197
198 /* row of 1's => complement is empty => SCCC is empty */
199 for(T1 = T+2; (p = *T1++) != NULL; ) {
200 if (full_row(p, cof)) {
201 *result = new_cube();
202 free_cubelist(T);
203 return TRUE;
204 }
205 }
206
207 /* Collect column counts, determine unate variables, etc. */
208 massive_count(T);
209
210 /* If cover is unate (or single cube), apply simple rules to find SCCCU */
211 if (cdata.vars_unate == cdata.vars_active || T[3] == NULL) {
212 *result = set_save(cube.fullset);
213 for(T1 = T+2; (p = *T1++) != NULL; ) {
214 (void) sccc_cube(*result, set_or(temp, p, cof));
215 }
216 free_cubelist(T);
217 return TRUE;
218 }
219
220 /* Check for column of 0's (which can be easily factored( */
221 ceil = set_save(cof);
222 for(T1 = T+2; (p = *T1++) != NULL; ) {
223 INLINEset_or(ceil, ceil, p);
224 }
225 if (! setp_equal(ceil, cube.fullset)) {
226 *result = sccc_cube(set_save(cube.fullset), ceil);
227 if (setp_equal(*result, cube.fullset)) {
228 free_cube(ceil);
229 } else {
230 *result = sccc_merge(sccc(cofactor(T,ceil)),
231 set_save(cube.fullset), ceil, *result);
232 }
233 free_cubelist(T);
234 return TRUE;
235 }
236 free_cube(ceil);
237
238 /* Single active column at this point => tautology => SCCC is empty */
239 if (cdata.vars_active == 1) {
240 *result = new_cube();
241 free_cubelist(T);
242 return TRUE;
243 }
244
245 /* Check for components */
246 if (cdata.var_zeros[cdata.best] < CUBELISTSIZE(T)/2) {
247 if (cubelist_partition(T, &A, &B, debug & REDUCE1) == 0) {
248 return MAYBE;
249 } else {
250 free_cubelist(T);
251 *result = sccc(A);
252 ceil = sccc(B);
253 (void) set_and(*result, *result, ceil);
254 set_free(ceil);
255 return TRUE;
256 }
257 }
258
259 /* Not much we can do about it */
260 return MAYBE;
261}
#define TRUE
Definition abcBm.c:38
bool full_row()
#define set_save(r)
Definition espresso.h:166
#define set_free(r)
Definition espresso.h:167
void massive_count()
int cubelist_partition()
pset set_or()
pcube sccc_cube()
#define CUBELISTSIZE(T)
Definition espresso.h:329
Here is the call graph for this function: