Version abc80130

1 files changed, 0 insertions, 193 deletions

diff --git a/src/misc/espresso/verify.c b/src/misc/espresso/verify.c
deleted file mode 100644
index 64342787..00000000
--- a/src/misc/espresso/verify.c
+++ /dev/null
@@ -1,193 +0,0 @@
-/*
- * Revision Control Information
- *
- * $Source$
- * $Author$
- * $Revision$
- * $Date$
- *
- */
-/*
- */
-
-#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 {
-    (void) fprintf(stderr, "Warning: cannot permute columns without names\n");
-    return TRUE;
-    }
-
-    if (PLA1->F->sf_size != PLA2->F->sf_size) {
-    (void) 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;
-}