abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
reduce.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: reduce.c
12  purpose: Perform the Espresso-II reduction step
13 
14  Reduction is a technique used to explore larger regions of the
15  optimization space. We replace each cube of F with a smaller
16  cube while still maintaining a cover of the same logic function.
17 */
18 
19 #include "espresso.h"
20 
22 
23 
24 static bool toggle = TRUE;
25 
26 
27 /*
28  reduce -- replace each cube in F with its reduction
29 
30  The reduction of a cube is the smallest cube contained in the cube
31  which can replace the cube in the original cover without changing
32  the cover. This is equivalent to the super cube of all of the
33  essential points in the cube. This can be computed directly.
34 
35  The problem is that the order in which the cubes are reduced can
36  greatly affect the final result. We alternate between two ordering
37  strategies:
38 
39  (1) Order the cubes in ascending order of distance from the
40  largest cube breaking ties by ordering cubes of equal distance
41  in descending order of size (sort_reduce)
42 
43  (2) Order the cubes in descending order of the inner-product of
44  the cube and the column sums (mini_sort)
45 
46  The real workhorse of this section is the routine SCCC which is
47  used to find the Smallest Cube Containing the Complement of a cover.
48  Reduction as proposed by Espresso-II takes a cube and computes its
49  maximal reduction as the intersection between the cube and the
50  smallest cube containing the complement of (F u D - {c}) cofactored
51  against c.
52 
53  As usual, the unate-recursive paradigm is used to compute SCCC.
54  The SCCC of a unate cover is trivial to compute, and thus we perform
55  Shannon Cofactor expansion attempting to drive the cover to be unate
56  as fast as possible.
57 */
58 
60 INOUT pcover F;
61 IN pcover D;
62 {
63  register pcube last, p, cunder, *FD;
64 
65  /* Order the cubes */
66  if (use_random_order)
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 }
99 
100 /* reduce_cube -- find the maximal reduction of a cube */
102 IN pcube *FD, p;
103 {
104  pcube cunder;
105 
106  cunder = sccc(cofactor(FD, p));
107  return set_and(cunder, cunder, p);
108 }
109 
110 
111 /* sccc -- find Smallest Cube Containing the Complement of a cover */
113 INOUT pcube *T; /* T will be disposed of */
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 }
137 
138 
139 pcube sccc_merge(left, right, cl, cr)
140 INOUT register pcube left, right; /* will be disposed of ... */
141 INOUT register pcube cl, cr; /* will be disposed of ... */
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 }
151 
152 
153 /*
154  sccc_cube -- find the smallest cube containing the complement of a cube
155 
156  By DeMorgan's law and the fact that the smallest cube containing a
157  cover is the "or" of the positional cubes, it is simple to see that
158  the SCCC is the universe if the cube has more than two active
159  variables. If there is only a single active variable, then the
160  SCCC is merely the bitwise complement of the cube in that
161  variable. A last special case is no active variables, in which
162  case the SCCC is empty.
163 
164  This is "anded" with the incoming cube result.
165 */
167 register pcube result, p;
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 }
179 
180 /*
181  * sccc_special_cases -- check the special cases for sccc
182  */
183 
185 INOUT pcube *T; /* will be disposed if answer is determined */
186 OUT pcube *result; /* returned only if answer determined */
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 }
263 
pset set_or()
#define set_free(r)
Definition: espresso.h:167
#define new_cube()
Definition: espresso.h:262
char * pc1(pcube c)
Definition: cvrout.c:379
static ABC_NAMESPACE_IMPL_START bool toggle
Definition: reduce.c:24
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define pcover
Definition: espresso.h:264
pset set_copy()
#define set_save(r)
Definition: espresso.h:166
int var(Lit p)
Definition: SolverTypes.h:62
#define INLINEset_and(r, a, b)
Definition: espresso.h:202
#define OUT
Definition: espresso.h:333
pcover sort_reduce(IN pcover T)
Definition: cvrm.c:173
pset set_and()
char * pc2(pcube c)
Definition: cvrout.c:381
#define PRIME
Definition: espresso.h:127
#define free_cube(r)
Definition: espresso.h:263
pcover mini_sort(pcover F, int(*compare)())
Definition: cvrm.c:141
#define SET(set, flag)
Definition: espresso.h:122
pcube sccc_cube(pcube result, pcube p)
Definition: reduce.c:166
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define RESET(set, flag)
Definition: espresso.h:123
#define INLINEset_xor(r, a, b)
Definition: espresso.h:218
#define INOUT
Definition: espresso.h:334
#define IN
Definition: espresso.h:332
pcover random_order(pcover F)
Definition: cvrm.c:199
#define INLINEset_or(r, a, b)
Definition: espresso.h:205
bool setp_equal()
#define REDUCE1
Definition: espresso.h:358
#define print_time(t)
Definition: espresso.h:22
ABC_NAMESPACE_IMPL_START pcube * cofactor(IN pcube *T, IN register pcube c)
Definition: cofactor.c:44
#define CUBELISTSIZE(T)
Definition: espresso.h:329
#define REDUCE
Definition: espresso.h:357
bool full_row()
unsigned int debug
Definition: globals.c:19
pcube sccc(INOUT pcube *T)
Definition: reduce.c:112
pcube reduce_cube(IN pcube *FD, IN pcube p)
Definition: reduce.c:101
pcube * cube2list(pcover A, pcover B)
Definition: cofactor.c:306
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
pcover reduce(INOUT pcover F, IN pcover D)
Definition: reduce.c:59
int cubelist_partition(pcube *T, pcube **A, pcube **B, unsigned int comp_debug)
Definition: cvrm.c:234
int binate_split_select(IN pcube *T, IN register pcube cleft, IN register pcube cright, IN int debug_flag)
Definition: cofactor.c:258
int cactive()
#define ptime()
Definition: util_old.h:283
static int descend(struct saucy *s, struct coloring *c, int target, int min)
Definition: abcSaucy.c:1625
bool use_random_order
Definition: globals.c:38
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
bool sccc_special_cases(INOUT pcube *T, OUT pcube *result)
Definition: reduce.c:184
pcube sccc_merge(INOUT register pcube left, INOUT register pcube right, INOUT register pcube cl, INOUT register pcube cr)
Definition: reduce.c:139
#define TRUE
Definition: cudd.h:88
pcube * scofactor(IN pcube *T, IN pcube c, IN int var)
Definition: cofactor.c:93
#define free_cubelist(T)
Definition: espresso.h:267
void debug_print(pcube *T, char *name, int level)
Definition: cvrout.c:385
#define MAYBE
Definition: espresso.h:257
bool setp_empty()
static int result
Definition: cuddGenetic.c:125
#define ACTIVE
Definition: espresso.h:129
pset_family sf_inactive()
#define pcube
Definition: espresso.h:261
void massive_count(IN pcube *T)
Definition: cofactor.c:131