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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START
pset_family 
sf_contain (INOUT pset_family A)
 
pset_family sf_rev_contain (INOUT pset_family A)
 
pset_family sf_ind_contain (INOUT pset_family A, INOUT int *row_indices)
 
pset_family sf_dupl (INOUT pset_family A)
 
pset_family sf_union (INOUT pset_family A, INOUT pset_family B)
 
pset_family dist_merge (INOUT pset_family A, IN pset mask)
 
pset_family d1merge (INOUT pset_family A, IN int var)
 
int d1_rm_equal (pset *A1, int(*compare)())
 
int rm_equal (INOUT pset *A1, IN int(*compare)())
 
int rm_contain (INOUT pset *A1)
 
int rm_rev_contain (INOUT pset *A1)
 
int rm2_equal (INOUT register pset *A1, INOUT register pset *B1, OUT pset *E1, IN int(*compare)())
 
int rm2_contain (INOUT pset *A1, IN pset *B1)
 
psetsf_sort (IN pset_family A, IN int(*compare)())
 
psetsf_list (IN register pset_family A)
 
pset_family sf_unlist (IN pset *A1, IN int totcnt, IN int size)
 
pset_family sf_ind_unlist (IN pset *A1, IN int totcnt, IN int size, INOUT int *row_indices, IN register pset pfirst)
 
pset_family sf_merge (INOUT pset *A1, INOUT pset *B1, INOUT pset *E1, IN int totcnt, IN int size)
 

Function Documentation

int d1_rm_equal ( pset A1,
int (*)()  compare 
)

Definition at line 171 of file contain.c.

174 {
175  register int i, j, dest;
176 
177  dest = 0;
178  if (A1[0] != (pcube) NULL) {
179  for(i = 0, j = 1; A1[j] != (pcube) NULL; j++)
180  if ( (*compare)(&A1[i], &A1[j]) == 0) {
181  /* if sets are equal (under the mask) merge them */
182  (void) set_or(A1[i], A1[i], A1[j]);
183  } else {
184  /* sets are unequal, so save the set i */
185  A1[dest++] = A1[i];
186  i = j;
187  }
188  A1[dest++] = A1[i];
189  }
190  A1[dest] = (pcube) NULL;
191  return dest;
192 }
pset set_or()
#define pcube
Definition: espresso.h:261
pset_family d1merge ( INOUT pset_family  A,
IN int  var 
)

Definition at line 161 of file contain.c.

164 {
165  return dist_merge(A, cube.var_mask[var]);
166 }
int var(Lit p)
Definition: SolverTypes.h:62
pset_family dist_merge(INOUT pset_family A, IN pset mask)
Definition: contain.c:141
pset_family dist_merge ( INOUT pset_family  A,
IN pset  mask 
)

Definition at line 141 of file contain.c.

144 {
145  pset *A1;
146  int cnt;
147  pset_family R;
148 
149  (void) set_copy(cube.temp[0], mask);
150  A1 = sf_sort(A, d1_order);
151  cnt = d1_rm_equal(A1, d1_order);
152  R = sf_unlist(A1, cnt, A->sf_size);
153  sf_free(A);
154  return R;
155 }
pset set_copy()
int d1_rm_equal(pset *A1, int(*compare)())
Definition: contain.c:171
void sf_free()
unsigned int * pset
Definition: espresso.h:73
int d1_order()
pset_family sf_unlist(IN pset *A1, IN int totcnt, IN int size)
Definition: contain.c:366
pset * sf_sort(IN pset_family A, IN int(*compare)())
Definition: contain.c:330
int rm2_contain ( INOUT pset A1,
IN pset B1 
)

Definition at line 304 of file contain.c.

307 {
308  register pset *pa, *pb, a, b, *pdest = A1;
309 
310  /* for each set in the first array ... */
311  for(pa = A1; (a = *pa++) != NULL; ) {
312  /* for each set in the second array which is larger ... */
313  for(pb = B1; (b = *pb++) != NULL && SIZE(b) > SIZE(a); ) {
314  INLINEsetp_implies(a, b, /* when_false => */ continue);
315  /* set was contained in some set of B, so don't save pointer */
316  goto lnext1;
317  }
318  /* set wasn't contained in any set of B, so save the pointer */
319  *pdest++ = a;
320  lnext1: ;
321  }
322 
323  *pdest = NULL; /* sentinel */
324  return pdest - A1; /* # elements in A1 */
325 }
#define INLINEsetp_implies(a, b, when_false)
Definition: espresso.h:228
unsigned int * pset
Definition: espresso.h:73
#define SIZE(set)
Definition: espresso.h:112
int rm2_equal ( INOUT register pset A1,
INOUT register pset B1,
OUT pset E1,
IN int (*)()  compare 
)

Definition at line 274 of file contain.c.

278 {
279  register pset *pda = A1, *pdb = B1, *pde = E1;
280 
281  /* Walk through the arrays advancing pointer to larger cube */
282  for(; *A1 != NULL && *B1 != NULL; )
283  switch((*compare)(A1, B1)) {
284  case -1: /* "a" comes before "b" */
285  *pda++ = *A1++; break;
286  case 0: /* equal cubes */
287  *pde++ = *A1++; B1++; break;
288  case 1: /* "a" is to follow "b" */
289  *pdb++ = *B1++; break;
290  }
291 
292  /* Finish moving down the pointers of A and B */
293  while (*A1 != NULL)
294  *pda++ = *A1++;
295  while (*B1 != NULL)
296  *pdb++ = *B1++;
297  *pda = *pdb = *pde = NULL;
298 
299  return pde - E1;
300 }
unsigned int * pset
Definition: espresso.h:73
int rm_contain ( INOUT pset A1)

Definition at line 214 of file contain.c.

216 {
217  register pset *pa, *pb;
218  register pset *pcheck = NULL; // Suppress "might be used uninitialized"
219  register pset a, b;
220  pset *pdest = A1;
221  int last_size = -1;
222 
223  /* Loop for all cubes of A1 */
224  for(pa = A1; (a = *pa++) != NULL; ) {
225  /* Update the check pointer if the size has changed */
226  if (SIZE(a) != last_size)
227  last_size = SIZE(a), pcheck = pdest;
228  for(pb = A1; pb != pcheck; ) {
229  b = *pb++;
230  INLINEsetp_implies(a, b, /* when_false => */ continue);
231  goto lnext1;
232  }
233  /* set a was not contained by some larger set, so save it */
234  *pdest++ = a;
235  lnext1: ;
236  }
237 
238  *pdest = NULL;
239  return pdest - A1;
240 }
#define INLINEsetp_implies(a, b, when_false)
Definition: espresso.h:228
unsigned int * pset
Definition: espresso.h:73
#define SIZE(set)
Definition: espresso.h:112
int rm_equal ( INOUT pset A1,
IN int (*)()  compare 
)

Definition at line 196 of file contain.c.

199 {
200  register pset *p, *pdest = A1;
201 
202  if (*A1 != NULL) { /* If more than one set */
203  for(p = A1+1; *p != NULL; p++)
204  if ((*compare)(p, p-1) != 0)
205  *pdest++ = *(p-1);
206  *pdest++ = *(p-1);
207  *pdest = NULL;
208  }
209  return pdest - A1;
210 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
unsigned int * pset
Definition: espresso.h:73
int rm_rev_contain ( INOUT pset A1)

Definition at line 244 of file contain.c.

246 {
247  register pset *pa, *pb;
248  register pset *pcheck = NULL; // Suppress "might be used uninitialized"
249  register pset a, b;
250  pset *pdest = A1;
251  int last_size = -1;
252 
253  /* Loop for all cubes of A1 */
254  for(pa = A1; (a = *pa++) != NULL; ) {
255  /* Update the check pointer if the size has changed */
256  if (SIZE(a) != last_size)
257  last_size = SIZE(a), pcheck = pdest;
258  for(pb = A1; pb != pcheck; ) {
259  b = *pb++;
260  INLINEsetp_implies(b, a, /* when_false => */ continue);
261  goto lnext1;
262  }
263  /* the set a did not contain some smaller set, so save it */
264  *pdest++ = a;
265  lnext1: ;
266  }
267 
268  *pdest = NULL;
269  return pdest - A1;
270 }
#define INLINEsetp_implies(a, b, when_false)
Definition: espresso.h:228
unsigned int * pset
Definition: espresso.h:73
#define SIZE(set)
Definition: espresso.h:112

Definition at line 37 of file contain.c.

39 {
40  int cnt;
41  pset *A1;
42  pset_family R;
43 
44  A1 = sf_sort(A, descend); /* sort into descending order */
45  cnt = rm_equal(A1, descend); /* remove duplicates */
46  cnt = rm_contain(A1); /* remove contained sets */
47  R = sf_unlist(A1, cnt, A->sf_size); /* recreate the set family */
48  sf_free(A);
49  return R;
50 }
void sf_free()
unsigned int * pset
Definition: espresso.h:73
static int descend(struct saucy *s, struct coloring *c, int target, int min)
Definition: abcSaucy.c:1625
pset_family sf_unlist(IN pset *A1, IN int totcnt, IN int size)
Definition: contain.c:366
int rm_contain(INOUT pset *A1)
Definition: contain.c:214
int rm_equal(INOUT pset *A1, IN int(*compare)())
Definition: contain.c:196
pset * sf_sort(IN pset_family A, IN int(*compare)())
Definition: contain.c:330
pset_family sf_dupl ( INOUT pset_family  A)

Definition at line 99 of file contain.c.

101 {
102  register int cnt;
103  register pset *A1;
104  pset_family R;
105 
106  A1 = sf_sort(A, descend); /* sort the set family */
107  cnt = rm_equal(A1, descend); /* remove duplicates */
108  R = sf_unlist(A1, cnt, A->sf_size); /* recreate the set family */
109  sf_free(A);
110  return R;
111 }
void sf_free()
unsigned int * pset
Definition: espresso.h:73
static int descend(struct saucy *s, struct coloring *c, int target, int min)
Definition: abcSaucy.c:1625
pset_family sf_unlist(IN pset *A1, IN int totcnt, IN int size)
Definition: contain.c:366
int rm_equal(INOUT pset *A1, IN int(*compare)())
Definition: contain.c:196
pset * sf_sort(IN pset_family A, IN int(*compare)())
Definition: contain.c:330
pset_family sf_ind_contain ( INOUT pset_family  A,
INOUT int *  row_indices 
)

Definition at line 81 of file contain.c.

84 {
85  int cnt;
86  pset *A1;
87  pset_family R;
88 
89  A1 = sf_sort(A, descend); /* sort into descending order */
90  cnt = rm_equal(A1, descend); /* remove duplicates */
91  cnt = rm_contain(A1); /* remove contained sets */
92  R = sf_ind_unlist(A1, cnt, A->sf_size, row_indices, A->data);
93  sf_free(A);
94  return R;
95 }
void sf_free()
unsigned int * pset
Definition: espresso.h:73
static int descend(struct saucy *s, struct coloring *c, int target, int min)
Definition: abcSaucy.c:1625
pset_family sf_ind_unlist(IN pset *A1, IN int totcnt, IN int size, INOUT int *row_indices, IN register pset pfirst)
Definition: contain.c:382
int rm_contain(INOUT pset *A1)
Definition: contain.c:214
int rm_equal(INOUT pset *A1, IN int(*compare)())
Definition: contain.c:196
pset * sf_sort(IN pset_family A, IN int(*compare)())
Definition: contain.c:330
pset_family sf_ind_unlist ( IN pset A1,
IN int  totcnt,
IN int  size,
INOUT int *  row_indices,
IN register pset  pfirst 
)

Definition at line 382 of file contain.c.

387 {
388  register pset pr, p, *pa;
389  register int i, *new_row_indices;
390  pset_family R = sf_new(totcnt, size);
391 
392  R->count = totcnt;
393  new_row_indices = ALLOC(int, totcnt);
394  for(pr = R->data, pa = A1, i=0; (p = *pa++) != NULL; pr += R->wsize, i++) {
395  INLINEset_copy(pr, p);
396  new_row_indices[i] = row_indices[(p - pfirst)/R->wsize];
397  }
398  for(i = 0; i < totcnt; i++)
399  row_indices[i] = new_row_indices[i];
400  FREE(new_row_indices);
401  FREE(A1);
402  return R;
403 }
pset_family sf_new()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int count
Definition: espresso.h:80
#define ALLOC(type, num)
Definition: avl.h:27
#define INLINEset_copy(r, a)
Definition: espresso.h:195
#define FREE(obj)
Definition: avl.h:31
static int size
Definition: cuddSign.c:86
unsigned int * pset
Definition: espresso.h:73
pset data
Definition: espresso.h:82
int wsize
Definition: espresso.h:77
pset* sf_list ( IN register pset_family  A)

Definition at line 351 of file contain.c.

353 {
354  register pset p, last, *pdest, *A1;
355 
356  /* Create a single array pointing to each cube of A */
357  pdest = A1 = ALLOC(pset, A->count + 1);
358  foreach_set(A, last, p)
359  *pdest++ = p; /* save the pointer */
360  *pdest = NULL; /* Sentinel */
361  return A1;
362 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define ALLOC(type, num)
Definition: avl.h:27
unsigned int * pset
Definition: espresso.h:73
pset_family sf_merge ( INOUT pset A1,
INOUT pset B1,
INOUT pset E1,
IN int  totcnt,
IN int  size 
)

Definition at line 407 of file contain.c.

410 {
411  register pset pr, ps, *pmin, *pmid, *pmax;
412  pset_family R;
413  pset *temp[3], *swap;
414  int i, j, n;
415 
416  /* Allocate the result set_family */
417  R = sf_new(totcnt, size);
418  R->count = totcnt;
419  pr = R->data;
420 
421  /* Quick bubble sort to order the top member of the three arrays */
422  n = 3; temp[0] = A1; temp[1] = B1; temp[2] = E1;
423  for(i = 0; i < n-1; i++)
424  for(j = i+1; j < n; j++)
425  if (desc1(*temp[i], *temp[j]) > 0) {
426  swap = temp[j];
427  temp[j] = temp[i];
428  temp[i] = swap;
429  }
430  pmin = temp[0]; pmid = temp[1]; pmax = temp[2];
431 
432  /* Save the minimum element, then update pmin, pmid, pmax */
433  while (*pmin != (pset) NULL) {
434  ps = *pmin++;
435  INLINEset_copy(pr, ps);
436  pr += R->wsize;
437  if (desc1(*pmin, *pmax) > 0) {
438  swap = pmax; pmax = pmin; pmin = pmid; pmid = swap;
439  } else if (desc1(*pmin, *pmid) > 0) {
440  swap = pmin; pmin = pmid; pmid = swap;
441  }
442  }
443 
444  FREE(A1);
445  FREE(B1);
446  FREE(E1);
447  return R;
448 }
int desc1()
pset_family sf_new()
int count
Definition: espresso.h:80
#define INLINEset_copy(r, a)
Definition: espresso.h:195
#define FREE(obj)
Definition: avl.h:31
static int size
Definition: cuddSign.c:86
unsigned int * pset
Definition: espresso.h:73
static void swap(int *a, int x, int y)
Definition: abcSaucy.c:305
pset data
Definition: espresso.h:82
int wsize
Definition: espresso.h:77
pset_family sf_rev_contain ( INOUT pset_family  A)

Definition at line 58 of file contain.c.

60 {
61  int cnt;
62  pset *A1;
63  pset_family R;
64 
65  A1 = sf_sort(A, ascend); /* sort into ascending order */
66  cnt = rm_equal(A1, ascend); /* remove duplicates */
67  cnt = rm_rev_contain(A1); /* remove containing sets */
68  R = sf_unlist(A1, cnt, A->sf_size); /* recreate the set family */
69  sf_free(A);
70  return R;
71 }
void sf_free()
int rm_rev_contain(INOUT pset *A1)
Definition: contain.c:244
int ascend()
unsigned int * pset
Definition: espresso.h:73
pset_family sf_unlist(IN pset *A1, IN int totcnt, IN int size)
Definition: contain.c:366
int rm_equal(INOUT pset *A1, IN int(*compare)())
Definition: contain.c:196
pset * sf_sort(IN pset_family A, IN int(*compare)())
Definition: contain.c:330
pset* sf_sort ( IN pset_family  A,
IN int (*)()  compare 
)

Definition at line 330 of file contain.c.

333 {
334  register pset p, last, *pdest, *A1;
335 
336  /* Create a single array pointing to each cube of A */
337  pdest = A1 = ALLOC(pset, A->count + 1);
338  foreach_set(A, last, p) {
339  PUTSIZE(p, set_ord(p)); /* compute the set size */
340  *pdest++ = p; /* save the pointer */
341  }
342  *pdest = NULL; /* Sentinel -- never seen by sort */
343 
344  /* Sort cubes by size */
345  qsort((char *) A1, A->count, sizeof(pset), compare);
346  return A1;
347 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define PUTSIZE(set, size)
Definition: espresso.h:113
#define foreach_set(R, last, p)
Definition: espresso.h:135
#define ALLOC(type, num)
Definition: avl.h:27
unsigned int * pset
Definition: espresso.h:73
int set_ord()
pset_family sf_union ( INOUT pset_family  A,
INOUT pset_family  B 
)

Definition at line 121 of file contain.c.

123 {
124  int cnt;
125  pset_family R;
126  pset *A1 = sf_list(A), *B1 = sf_list(B), *E1;
127 
128  E1 = ALLOC(pset, MAX(A->count, B->count) + 1);
129  cnt = rm2_equal(A1, B1, E1, descend);
130  cnt += rm2_contain(A1, B1) + rm2_contain(B1, A1);
131  R = sf_merge(A1, B1, E1, cnt, A->sf_size);
132  sf_free(A); sf_free(B);
133  return R;
134 }
void sf_free()
#define ALLOC(type, num)
Definition: avl.h:27
unsigned int * pset
Definition: espresso.h:73
#define MAX(a, b)
Definition: avl.h:23
static int descend(struct saucy *s, struct coloring *c, int target, int min)
Definition: abcSaucy.c:1625
pset * sf_list(IN register pset_family A)
Definition: contain.c:351
pset_family sf_merge(INOUT pset *A1, INOUT pset *B1, INOUT pset *E1, IN int totcnt, IN int size)
Definition: contain.c:407
int rm2_equal(INOUT register pset *A1, INOUT register pset *B1, OUT pset *E1, IN int(*compare)())
Definition: contain.c:274
int rm2_contain(INOUT pset *A1, IN pset *B1)
Definition: contain.c:304
pset_family sf_unlist ( IN pset A1,
IN int  totcnt,
IN int  size 
)

Definition at line 366 of file contain.c.

369 {
370  register pset pr, p, *pa;
371  pset_family R = sf_new(totcnt, size);
372 
373  R->count = totcnt;
374  for(pr = R->data, pa = A1; (p = *pa++) != NULL; pr += R->wsize)
375  INLINEset_copy(pr, p);
376  FREE(A1);
377  return R;
378 }
pset_family sf_new()
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int count
Definition: espresso.h:80
#define INLINEset_copy(r, a)
Definition: espresso.h:195
#define FREE(obj)
Definition: avl.h:31
static int size
Definition: cuddSign.c:86
unsigned int * pset
Definition: espresso.h:73
pset data
Definition: espresso.h:82
int wsize
Definition: espresso.h:77