abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
verify.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  */
12 
13 #include "espresso.h"
14 
16 
17 
18 /*
19  * verify -- check that all minterms of F are contained in (Fold u Dold)
20  * and that all minterms of Fold are contained in (F u Dold).
21  */
22 bool verify(F, Fold, Dold)
23 pcover F, Fold, Dold;
24 {
25  pcube p, last, *FD;
26  bool verify_error = FALSE;
27 
28  /* Make sure the function didn't grow too large */
29  FD = cube2list(Fold, Dold);
30  foreach_set(F, last, p)
31  if (! cube_is_covered(FD, p)) {
32  printf("some minterm in F is not covered by Fold u Dold\n");
33  verify_error = TRUE;
34  if (verbose_debug) printf("%s\n", pc1(p)); else break;
35  }
36  free_cubelist(FD);
37 
38  /* Make sure minimized function covers the original function */
39  FD = cube2list(F, Dold);
40  foreach_set(Fold, last, p)
41  if (! cube_is_covered(FD, p)) {
42  printf("some minterm in Fold is not covered by F u Dold\n");
43  verify_error = TRUE;
44  if (verbose_debug) printf("%s\n", pc1(p)); else break;
45  }
46  free_cubelist(FD);
47 
48  return verify_error;
49 }
50 
51 
52 
53 /*
54  * PLA_verify -- verify that two PLA's are identical
55  *
56  * If names are given, row and column permutations are done to make
57  * the comparison meaningful.
58  *
59  */
60 bool PLA_verify(PLA1, PLA2)
61 pPLA PLA1, PLA2;
62 {
63  /* Check if both have names given; if so, attempt to permute to
64  * match the names
65  */
66  if (PLA1->label != NULL && PLA1->label[0] != NULL &&
67  PLA2->label != NULL && PLA2->label[0] != NULL) {
68  PLA_permute(PLA1, PLA2);
69  } else {
70  (void) fprintf(stderr, "Warning: cannot permute columns without names\n");
71  return TRUE;
72  }
73 
74  if (PLA1->F->sf_size != PLA2->F->sf_size) {
75  (void) fprintf(stderr, "PLA_verify: PLA's are not the same size\n");
76  return TRUE;
77  }
78 
79  return verify(PLA2->F, PLA1->F, PLA1->D);
80 }
81 
82 
83 
84 /*
85  * Permute the columns of PLA1 so that they match the order of PLA2
86  * Discard any columns of PLA1 which are not in PLA2
87  * Association is strictly by the names of the columns of the cover.
88  */
89 void PLA_permute(PLA1, PLA2)
90 pPLA PLA1, PLA2;
91 {
92  register int i, j, *permute, npermute;
93  register char *labi;
94  char **label;
95 
96  /* determine which columns of PLA1 to save, and place these in the list
97  * "permute"; the order in this list is the final output order
98  */
99  npermute = 0;
100  permute = ALLOC(int, PLA2->F->sf_size);
101  for(i = 0; i < PLA2->F->sf_size; i++) {
102  labi = PLA2->label[i];
103  for(j = 0; j < PLA1->F->sf_size; j++) {
104  if (strcmp(labi, PLA1->label[j]) == 0) {
105  permute[npermute++] = j;
106  break;
107  }
108  }
109  }
110 
111  /* permute columns */
112  if (PLA1->F != NULL) {
113  PLA1->F = sf_permute(PLA1->F, permute, npermute);
114  }
115  if (PLA1->R != NULL) {
116  PLA1->R = sf_permute(PLA1->R, permute, npermute);
117  }
118  if (PLA1->D != NULL) {
119  PLA1->D = sf_permute(PLA1->D, permute, npermute);
120  }
121 
122  /* permute the labels */
123  label = ALLOC(char *, cube.size);
124  for(i = 0; i < npermute; i++) {
125  label[i] = PLA1->label[permute[i]];
126  }
127  for(i = npermute; i < cube.size; i++) {
128  label[i] = NULL;
129  }
130  FREE(PLA1->label);
131  PLA1->label = label;
132 
133  FREE(permute);
134 }
135 
136 
137 
138 /*
139  * check_consistency -- test that the ON-set, OFF-set and DC-set form
140  * a partition of the boolean space.
141  */
143 pPLA PLA;
144 {
145  bool verify_error = FALSE;
146  pcover T;
147 
148  T = cv_intersect(PLA->F, PLA->D);
149  if (T->count == 0)
150  printf("ON-SET and DC-SET are disjoint\n");
151  else {
152  printf("Some minterm(s) belong to both the ON-SET and DC-SET !\n");
153  if (verbose_debug)
154  cprint(T);
155  verify_error = TRUE;
156  }
157  (void) fflush(stdout);
158  free_cover(T);
159 
160  T = cv_intersect(PLA->F, PLA->R);
161  if (T->count == 0)
162  printf("ON-SET and OFF-SET are disjoint\n");
163  else {
164  printf("Some minterm(s) belong to both the ON-SET and OFF-SET !\n");
165  if (verbose_debug)
166  cprint(T);
167  verify_error = TRUE;
168  }
169  (void) fflush(stdout);
170  free_cover(T);
171 
172  T = cv_intersect(PLA->D, PLA->R);
173  if (T->count == 0)
174  printf("DC-SET and OFF-SET are disjoint\n");
175  else {
176  printf("Some minterm(s) belong to both the OFF-SET and DC-SET !\n");
177  if (verbose_debug)
178  cprint(T);
179  verify_error = TRUE;
180  }
181  (void) fflush(stdout);
182  free_cover(T);
183 
184  if (tautology(cube3list(PLA->F, PLA->D, PLA->R)))
185  printf("Union of ON-SET, OFF-SET and DC-SET is the universe\n");
186  else {
187  T = complement(cube3list(PLA->F, PLA->D, PLA->R));
188  printf("There are minterms left unspecified !\n");
189  if (verbose_debug)
190  cprint(T);
191  verify_error = TRUE;
192  free_cover(T);
193  }
194  (void) fflush(stdout);
195  return verify_error;
196 }
198 
#define FALSE
Definition: cudd.h:91
char * pc1(pcube c)
Definition: cvrout.c:379
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define free_cover(r)
Definition: espresso.h:266
#define pcover
Definition: espresso.h:264
bool tautology()
pcube * cube3list(pcover A, pcover B, pcover C)
Definition: cofactor.c:326
ABC_NAMESPACE_IMPL_START bool verify(pcover F, pcover Fold, pcover Dold)
Definition: verify.c:22
void cprint(pcover T)
Definition: cvrout.c:424
pcover complement(pcube *T)
Definition: compl.c:49
#define foreach_set(R, last, p)
Definition: espresso.h:135
int strcmp()
#define ALLOC(type, num)
Definition: avl.h:27
bool cube_is_covered()
pset_family sf_permute()
pcube * cube2list(pcover A, pcover B)
Definition: cofactor.c:306
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
#define FREE(obj)
Definition: avl.h:31
bool PLA_verify(pPLA PLA1, pPLA PLA2)
Definition: verify.c:60
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
#define TRUE
Definition: cudd.h:88
#define free_cubelist(T)
Definition: espresso.h:267
void PLA_permute(pPLA PLA1, pPLA PLA2)
Definition: verify.c:89
bool verbose_debug
Definition: globals.c:20
bool check_consistency(pPLA PLA)
Definition: verify.c:142
pcover cv_intersect()
#define pcube
Definition: espresso.h:261