abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
sparse.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: sparse.c
12 
13  make_sparse is a last-step cleanup to reduce the total number
14  of literals in the cover.
15 
16  This is done by reducing the "sparse" variables (using a modified
17  version of irredundant rather than reduce), followed by expanding
18  the "dense" variables (using modified version of expand).
19 */
20 
21 #include "espresso.h"
22 
24 
25 
27 pcover F, D, R;
28 {
29  cost_t cost, best_cost;
30 
31  cover_cost(F, &best_cost);
32 
33  do {
34  EXECUTE(F = mv_reduce(F, D), MV_REDUCE_TIME, F, cost);
35  if (cost.total == best_cost.total)
36  break;
37  copy_cost(&cost, &best_cost);
38 
39  EXECUTE(F = expand(F, R, TRUE), RAISE_IN_TIME, F, cost);
40  if (cost.total == best_cost.total)
41  break;
42  copy_cost(&cost, &best_cost);
43  } while (force_irredundant);
44 
45  return F;
46 }
47 
48 /*
49  mv_reduce -- perform an "optimal" reduction of the variables which
50  we desire to be sparse
51 
52  This could be done using "reduce" and then saving just the desired
53  part of the reduction. Instead, this version uses IRRED to find
54  which cubes of an output are redundant. Note that this gets around
55  the cube-ordering problem.
56 
57  In normal use, it is expected that the cover is irredundant and
58  hence no cubes will be reduced to the empty cube (however, this is
59  checked for and such cubes will be deleted)
60 */
61 
62 pcover
63 mv_reduce(F, D)
64 pcover F, D;
65 {
66  register int i, var;
67  register pcube p, p1, last;
68  int index;
69  pcover F1, D1;
70  pcube *F_cube_table;
71 
72  /* loop for each multiple-valued variable */
73  for(var = 0; var < cube.num_vars; var++) {
74 
75  if (cube.sparse[var]) {
76 
77  /* loop for each part of the variable */
78  for(i = cube.first_part[var]; i <= cube.last_part[var]; i++) {
79 
80  /* remember mapping of F1 cubes back to F cubes */
81  F_cube_table = ALLOC(pcube, F->count);
82 
83  /* 'cofactor' against part #i of variable #var */
84  F1 = new_cover(F->count);
85  foreach_set(F, last, p) {
86  if (is_in_set(p, i)) {
87  F_cube_table[F1->count] = p;
88  p1 = GETSET(F1, F1->count++);
89  (void) set_diff(p1, p, cube.var_mask[var]);
90  set_insert(p1, i);
91  }
92  }
93 
94  /* 'cofactor' against part #i of variable #var */
95  /* not really necessary -- just more efficient ? */
96  D1 = new_cover(D->count);
97  foreach_set(D, last, p) {
98  if (is_in_set(p, i)) {
99  p1 = GETSET(D1, D1->count++);
100  (void) set_diff(p1, p, cube.var_mask[var]);
101  set_insert(p1, i);
102  }
103  }
104 
105  mark_irredundant(F1, D1);
106 
107  /* now remove part i from cubes which are redundant */
108  index = 0;
109  foreach_set(F1, last, p1) {
110  if (! TESTP(p1, ACTIVE)) {
111  p = F_cube_table[index];
112 
113  /* don't reduce a variable which is full
114  * (unless it is the output variable)
115  */
116  if (var == cube.num_vars-1 ||
117  ! setp_implies(cube.var_mask[var], p)) {
118  set_remove(p, i);
119  }
120  RESET(p, PRIME);
121  }
122  index++;
123  }
124 
125  free_cover(F1);
126  free_cover(D1);
127  FREE(F_cube_table);
128  }
129  }
130  }
131 
132  /* Check if any cubes disappeared */
133  (void) sf_active(F);
134  for(var = 0; var < cube.num_vars; var++) {
135  if (cube.sparse[var]) {
136  foreach_active_set(F, last, p) {
137  if (setp_disjoint(p, cube.var_mask[var])) {
138  RESET(p, ACTIVE);
139  F->active_count--;
140  }
141  }
142  }
143  }
144 
145  if (F->count != F->active_count) {
146  F = sf_inactive(F);
147  }
148  return F;
149 }
151 
ABC_NAMESPACE_IMPL_START void cover_cost(IN pcover F, INOUT pcost cost)
Definition: cvrmisc.c:17
#define MV_REDUCE_TIME
Definition: espresso.h:384
void copy_cost(pcost s, pcost d)
Definition: cvrmisc.c:86
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define free_cover(r)
Definition: espresso.h:266
#define pcover
Definition: espresso.h:264
int var(Lit p)
Definition: SolverTypes.h:62
#define PRIME
Definition: espresso.h:127
bool setp_disjoint()
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define RESET(set, flag)
Definition: espresso.h:123
pcover expand()
pset set_diff()
#define ALLOC(type, num)
Definition: avl.h:27
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
#define RAISE_IN_TIME
Definition: espresso.h:385
bool force_irredundant
Definition: globals.c:27
pcover mv_reduce(pcover F, pcover D)
Definition: sparse.c:63
#define FREE(obj)
Definition: avl.h:31
#define is_in_set(set, e)
Definition: espresso.h:170
#define new_cover(i)
Definition: espresso.h:265
void mark_irredundant()
#define foreach_active_set(R, last, p)
Definition: espresso.h:139
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
#define set_remove(set, e)
Definition: espresso.h:171
#define TRUE
Definition: cudd.h:88
pset_family sf_active()
#define set_insert(set, e)
Definition: espresso.h:172
#define GETSET(family, index)
Definition: espresso.h:161
bool setp_implies()
#define TESTP(set, flag)
Definition: espresso.h:124
#define ACTIVE
Definition: espresso.h:129
ABC_NAMESPACE_IMPL_START pcover make_sparse(pcover F, pcover D, pcover R)
Definition: sparse.c:26
#define EXECUTE(fct, i, S, cost)
Definition: espresso.h:422
pset_family sf_inactive()
static int best_cost
Definition: pair.c:366
#define pcube
Definition: espresso.h:261