| /* |
| */ |
| |
| #include "espresso.h" |
| |
| /* |
| * verify -- check that all minterms of F are contained in (Fold u Dold) |
| * and that all minterms of Fold are contained in (F u Dold). |
| */ |
| bool verify(F, Fold, Dold) |
| pcover F, Fold, Dold; |
| { |
| pcube p, last, *FD; |
| bool verify_error = FALSE; |
| |
| /* Make sure the function didn't grow too large */ |
| FD = cube2list(Fold, Dold); |
| foreach_set(F, last, p) |
| if (! cube_is_covered(FD, p)) { |
| printf("some minterm in F is not covered by Fold u Dold\n"); |
| verify_error = TRUE; |
| if (verbose_debug) printf("%s\n", pc1(p)); else break; |
| } |
| free_cubelist(FD); |
| |
| /* Make sure minimized function covers the original function */ |
| FD = cube2list(F, Dold); |
| foreach_set(Fold, last, p) |
| if (! cube_is_covered(FD, p)) { |
| printf("some minterm in Fold is not covered by F u Dold\n"); |
| verify_error = TRUE; |
| if (verbose_debug) printf("%s\n", pc1(p)); else break; |
| } |
| free_cubelist(FD); |
| |
| return verify_error; |
| } |
| |
| |
| |
| /* |
| * PLA_verify -- verify that two PLA's are identical |
| * |
| * If names are given, row and column permutations are done to make |
| * the comparison meaningful. |
| * |
| */ |
| bool PLA_verify(PLA1, PLA2) |
| pPLA PLA1, PLA2; |
| { |
| /* Check if both have names given; if so, attempt to permute to |
| * match the names |
| */ |
| if (PLA1->label != NULL && PLA1->label[0] != NULL && |
| PLA2->label != NULL && PLA2->label[0] != NULL) { |
| PLA_permute(PLA1, PLA2); |
| } else { |
| fprintf(stderr, "Warning: cannot permute columns without names\n"); |
| return TRUE; |
| } |
| |
| if (PLA1->F->sf_size != PLA2->F->sf_size) { |
| fprintf(stderr, "PLA_verify: PLA's are not the same size\n"); |
| return TRUE; |
| } |
| |
| return verify(PLA2->F, PLA1->F, PLA1->D); |
| } |
| |
| |
| |
| /* |
| * Permute the columns of PLA1 so that they match the order of PLA2 |
| * Discard any columns of PLA1 which are not in PLA2 |
| * Association is strictly by the names of the columns of the cover. |
| */ |
| PLA_permute(PLA1, PLA2) |
| pPLA PLA1, PLA2; |
| { |
| register int i, j, *permute, npermute; |
| register char *labi; |
| char **label; |
| |
| /* determine which columns of PLA1 to save, and place these in the list |
| * "permute"; the order in this list is the final output order |
| */ |
| npermute = 0; |
| permute = ALLOC(int, PLA2->F->sf_size); |
| for(i = 0; i < PLA2->F->sf_size; i++) { |
| labi = PLA2->label[i]; |
| for(j = 0; j < PLA1->F->sf_size; j++) { |
| if (strcmp(labi, PLA1->label[j]) == 0) { |
| permute[npermute++] = j; |
| break; |
| } |
| } |
| } |
| |
| /* permute columns */ |
| if (PLA1->F != NULL) { |
| PLA1->F = sf_permute(PLA1->F, permute, npermute); |
| } |
| if (PLA1->R != NULL) { |
| PLA1->R = sf_permute(PLA1->R, permute, npermute); |
| } |
| if (PLA1->D != NULL) { |
| PLA1->D = sf_permute(PLA1->D, permute, npermute); |
| } |
| |
| /* permute the labels */ |
| label = ALLOC(char *, cube.size); |
| for(i = 0; i < npermute; i++) { |
| label[i] = PLA1->label[permute[i]]; |
| } |
| for(i = npermute; i < cube.size; i++) { |
| label[i] = NULL; |
| } |
| FREE(PLA1->label); |
| PLA1->label = label; |
| |
| FREE(permute); |
| } |
| |
| |
| |
| /* |
| * check_consistency -- test that the ON-set, OFF-set and DC-set form |
| * a partition of the boolean space. |
| */ |
| bool check_consistency(PLA) |
| pPLA PLA; |
| { |
| bool verify_error = FALSE; |
| pcover T; |
| |
| T = cv_intersect(PLA->F, PLA->D); |
| if (T->count == 0) |
| printf("ON-SET and DC-SET are disjoint\n"); |
| else { |
| printf("Some minterm(s) belong to both the ON-SET and DC-SET !\n"); |
| if (verbose_debug) |
| cprint(T); |
| verify_error = TRUE; |
| } |
| (void) fflush(stdout); |
| free_cover(T); |
| |
| T = cv_intersect(PLA->F, PLA->R); |
| if (T->count == 0) |
| printf("ON-SET and OFF-SET are disjoint\n"); |
| else { |
| printf("Some minterm(s) belong to both the ON-SET and OFF-SET !\n"); |
| if (verbose_debug) |
| cprint(T); |
| verify_error = TRUE; |
| } |
| (void) fflush(stdout); |
| free_cover(T); |
| |
| T = cv_intersect(PLA->D, PLA->R); |
| if (T->count == 0) |
| printf("DC-SET and OFF-SET are disjoint\n"); |
| else { |
| printf("Some minterm(s) belong to both the OFF-SET and DC-SET !\n"); |
| if (verbose_debug) |
| cprint(T); |
| verify_error = TRUE; |
| } |
| (void) fflush(stdout); |
| free_cover(T); |
| |
| if (tautology(cube3list(PLA->F, PLA->D, PLA->R))) |
| printf("Union of ON-SET, OFF-SET and DC-SET is the universe\n"); |
| else { |
| T = complement(cube3list(PLA->F, PLA->D, PLA->R)); |
| printf("There are minterms left unspecified !\n"); |
| if (verbose_debug) |
| cprint(T); |
| verify_error = TRUE; |
| free_cover(T); |
| } |
| (void) fflush(stdout); |
| return verify_error; |
| } |