abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
sharp.c File Reference
#include "espresso.h"

Go to the source code of this file.

Macros

#define MAGIC   500 /* save 500 cubes before containment */
 

Functions

pcover cv_sharp (pcover A, pcover B)
 
pcover cb_sharp (pcube c, pcover T)
 
pcover cb_recur_sharp (pcube c, pcover T, int first, int last, int level)
 
pcover sharp (pcube a, pcube b)
 
pcover make_disjoint (pcover A)
 
pcover cv_dsharp (pcover A, pcover B)
 
pcover cb1_dsharp (pcover T, pcube c)
 
pcover cb_dsharp (pcube c, pcover T)
 
pcover dsharp (pcube a, pcube b)
 
pcover cv_intersect (pcover A, pcover B)
 

Variables

ABC_NAMESPACE_IMPL_START long start_time
 

Macro Definition Documentation

#define MAGIC   500 /* save 500 cubes before containment */

Definition at line 214 of file sharp.c.

Function Documentation

pcover cb1_dsharp ( pcover  T,
pcube  c 
)

Definition at line 133 of file sharp.c.

136 {
137  pcube last, p;
138  pcover R;
139 
140  R = new_cover(T->count);
141  foreach_set(T, last, p) {
142  R = sf_union(R, dsharp(p, c));
143  }
144  return R;
145 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define pcover
Definition: espresso.h:264
#define foreach_set(R, last, p)
Definition: espresso.h:135
pcover dsharp(pcube a, pcube b)
Definition: sharp.c:172
#define new_cover(i)
Definition: espresso.h:265
pset_family sf_union(INOUT pset_family A, INOUT pset_family B)
Definition: contain.c:121
#define pcube
Definition: espresso.h:261
pcover cb_dsharp ( pcube  c,
pcover  T 
)

Definition at line 149 of file sharp.c.

152 {
153  pcube last, p;
154  pcover Y, Y1;
155 
156  if (T->count == 0) {
157  Y = sf_addset(new_cover(1), c);
158  } else {
159  Y = new_cover(T->count);
160  set_copy(GETSET(Y,Y->count++), c);
161  foreach_set(T, last, p) {
162  Y1 = cb1_dsharp(Y, p);
163  free_cover(Y);
164  Y = Y1;
165  }
166  }
167  return Y;
168 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define free_cover(r)
Definition: espresso.h:266
#define pcover
Definition: espresso.h:264
pset set_copy()
#define foreach_set(R, last, p)
Definition: espresso.h:135
pset_family sf_addset()
pcover cb1_dsharp(pcover T, pcube c)
Definition: sharp.c:133
#define new_cover(i)
Definition: espresso.h:265
#define GETSET(family, index)
Definition: espresso.h:161
#define pcube
Definition: espresso.h:261
pcover cb_recur_sharp ( pcube  c,
pcover  T,
int  first,
int  last,
int  level 
)

Definition at line 52 of file sharp.c.

56 {
57  pcover temp, left, right;
58  int middle;
59 
60  if (first == last) {
61  temp = sharp(c, GETSET(T, first));
62  } else {
63  middle = (first + last) / 2;
64  left = cb_recur_sharp(c, T, first, middle, level+1);
65  right = cb_recur_sharp(c, T, middle+1, last, level+1);
66  temp = cv_intersect(left, right);
67  if ((debug & SHARP) && level < 4) {
68  printf("# SHARP[%d]: %4d = %4d x %4d, time = %s\n",
69  level, temp->count, left->count, right->count,
71  (void) fflush(stdout);
72  }
73  free_cover(left);
74  free_cover(right);
75  }
76  return temp;
77 }
#define free_cover(r)
Definition: espresso.h:266
#define pcover
Definition: espresso.h:264
pcover cb_recur_sharp(pcube c, pcover T, int first, int last, int level)
Definition: sharp.c:52
#define print_time(t)
Definition: espresso.h:22
unsigned int debug
Definition: globals.c:19
pcover cv_intersect(pcover A, pcover B)
Definition: sharp.c:216
#define ptime()
Definition: util_old.h:283
#define GETSET(family, index)
Definition: espresso.h:161
pcover sharp(pcube a, pcube b)
Definition: sharp.c:81
ABC_NAMESPACE_IMPL_START long start_time
Definition: sharp.c:19
#define SHARP
Definition: espresso.h:364
pcover cb_sharp ( pcube  c,
pcover  T 
)

Definition at line 37 of file sharp.c.

40 {
41  if (T->count == 0) {
42  T = sf_addset(new_cover(1), c);
43  } else {
44  start_time = ptime();
45  T = cb_recur_sharp(c, T, 0, T->count-1, 0);
46  }
47  return T;
48 }
pcover cb_recur_sharp(pcube c, pcover T, int first, int last, int level)
Definition: sharp.c:52
pset_family sf_addset()
#define new_cover(i)
Definition: espresso.h:265
#define ptime()
Definition: util_old.h:283
ABC_NAMESPACE_IMPL_START long start_time
Definition: sharp.c:19
pcover cv_dsharp ( pcover  A,
pcover  B 
)

Definition at line 118 of file sharp.c.

120 {
121  register pcube last, p;
122  pcover T;
123 
124  T = new_cover(0);
125  foreach_set(A, last, p) {
126  T = sf_union(T, cb_dsharp(p, B));
127  }
128  return T;
129 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define pcover
Definition: espresso.h:264
pcover cb_dsharp(pcube c, pcover T)
Definition: sharp.c:149
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define new_cover(i)
Definition: espresso.h:265
pset_family sf_union(INOUT pset_family A, INOUT pset_family B)
Definition: contain.c:121
#define pcube
Definition: espresso.h:261
pcover cv_intersect ( pcover  A,
pcover  B 
)

Definition at line 216 of file sharp.c.

218 {
219  register pcube pi, pj, lasti, lastj, pt;
220  pcover T, Tsave = NULL;
221 
222  /* How large should each temporary result cover be ? */
223  T = new_cover(MAGIC);
224  pt = T->data;
225 
226  /* Form pairwise intersection of each cube of A with each cube of B */
227  foreach_set(A, lasti, pi) {
228  foreach_set(B, lastj, pj) {
229  if (cdist0(pi, pj)) {
230  (void) set_and(pt, pi, pj);
231  if (++T->count >= T->capacity) {
232  if (Tsave == NULL)
233  Tsave = sf_contain(T);
234  else
235  Tsave = sf_union(Tsave, sf_contain(T));
236  T = new_cover(MAGIC);
237  pt = T->data;
238  } else
239  pt += T->wsize;
240  }
241  }
242  }
243 
244 
245  if (Tsave == NULL)
246  Tsave = sf_contain(T);
247  else
248  Tsave = sf_union(Tsave, sf_contain(T));
249  return Tsave;
250 }
#define pcover
Definition: espresso.h:264
#define MAGIC
Definition: sharp.c:214
pset set_and()
#define foreach_set(R, last, p)
Definition: espresso.h:135
ABC_NAMESPACE_IMPL_START pset_family sf_contain(INOUT pset_family A)
Definition: contain.c:37
#define new_cover(i)
Definition: espresso.h:265
pset_family sf_union(INOUT pset_family A, INOUT pset_family B)
Definition: contain.c:121
bool cdist0()
#define pcube
Definition: espresso.h:261
pcover cv_sharp ( pcover  A,
pcover  B 
)

Definition at line 23 of file sharp.c.

25 {
26  pcube last, p;
27  pcover T;
28 
29  T = new_cover(0);
30  foreach_set(A, last, p)
31  T = sf_union(T, cb_sharp(p, B));
32  return T;
33 }
pcover cb_sharp(pcube c, pcover T)
Definition: sharp.c:37
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define pcover
Definition: espresso.h:264
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define new_cover(i)
Definition: espresso.h:265
pset_family sf_union(INOUT pset_family A, INOUT pset_family B)
Definition: contain.c:121
#define pcube
Definition: espresso.h:261
pcover dsharp ( pcube  a,
pcube  b 
)

Definition at line 172 of file sharp.c.

174 {
175  register pcube mask, diff, and, temp, temp1 = cube.temp[0];
176  int var;
177  pcover r;
178 
179  r = new_cover(cube.num_vars);
180 
181  if (cdist0(a, b)) {
182  diff = set_diff(new_cube(), a, b);
183  and = set_and(new_cube(), a, b);
184  mask = new_cube();
185  for(var = 0; var < cube.num_vars; var++) {
186  /* check if position var of "a and not b" is not empty */
187  if (! setp_disjoint(diff, cube.var_mask[var])) {
188 
189  /* coordinate var equals the difference between a and b */
190  temp = GETSET(r, r->count++);
191  (void) set_and(temp, diff, cube.var_mask[var]);
192 
193  /* coordinates 0 ... var-1 equal the intersection */
194  INLINEset_and(temp1, and, mask);
195  INLINEset_or(temp, temp, temp1);
196 
197  /* coordinates var+1 .. cube.num_vars equal a */
198  set_or(mask, mask, cube.var_mask[var]);
199  INLINEset_diff(temp1, a, mask);
200  INLINEset_or(temp, temp, temp1);
201  }
202  }
203  free_cube(diff);
204  free_cube(and);
205  free_cube(mask);
206  } else {
207  r = sf_addset(r, a);
208  }
209  return r;
210 }
pset set_or()
#define INLINEset_diff(r, a, b)
Definition: espresso.h:208
#define new_cube()
Definition: espresso.h:262
#define pcover
Definition: espresso.h:264
int var(Lit p)
Definition: SolverTypes.h:62
#define INLINEset_and(r, a, b)
Definition: espresso.h:202
pset set_and()
#define free_cube(r)
Definition: espresso.h:263
bool setp_disjoint()
#define INLINEset_or(r, a, b)
Definition: espresso.h:205
pset_family sf_addset()
pset set_diff()
#define new_cover(i)
Definition: espresso.h:265
#define GETSET(family, index)
Definition: espresso.h:161
bool cdist0()
#define pcube
Definition: espresso.h:261
pcover make_disjoint ( pcover  A)

Definition at line 102 of file sharp.c.

104 {
105  pcover R, new;
106  register pset last, p;
107 
108  R = new_cover(0);
109  foreach_set(A, last, p) {
110  new = cb_dsharp(p, R);
111  R = sf_append(R, new);
112  }
113  return R;
114 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define pcover
Definition: espresso.h:264
pcover cb_dsharp(pcube c, pcover T)
Definition: sharp.c:149
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define new_cover(i)
Definition: espresso.h:265
unsigned int * pset
Definition: espresso.h:73
pset_family sf_append()
pcover sharp ( pcube  a,
pcube  b 
)

Definition at line 81 of file sharp.c.

83 {
84  register int var;
85  register pcube d=cube.temp[0], temp=cube.temp[1], temp1=cube.temp[2];
86  pcover r = new_cover(cube.num_vars);
87 
88  if (cdist0(a, b)) {
89  set_diff(d, a, b);
90  for(var = 0; var < cube.num_vars; var++) {
91  if (! setp_empty(set_and(temp, d, cube.var_mask[var]))) {
92  set_diff(temp1, a, cube.var_mask[var]);
93  set_or(GETSET(r, r->count++), temp, temp1);
94  }
95  }
96  } else {
97  r = sf_addset(r, a);
98  }
99  return r;
100 }
pset set_or()
#define pcover
Definition: espresso.h:264
int var(Lit p)
Definition: SolverTypes.h:62
pset set_and()
pset_family sf_addset()
pset set_diff()
#define new_cover(i)
Definition: espresso.h:265
#define GETSET(family, index)
Definition: espresso.h:161
bool setp_empty()
bool cdist0()
#define pcube
Definition: espresso.h:261

Variable Documentation

ABC_NAMESPACE_IMPL_START long start_time

Definition at line 19 of file sharp.c.