src/misc/espresso/verify.c File Reference

#include "espresso.h"

Include dependency graph for verify.c:

Go to the source code of this file.

Functions
bool	verify (pcover F, pcover Fold, pcover Dold)
bool	PLA_verify (pPLA PLA1, pPLA PLA2)
	PLA_permute (pPLA PLA1, pPLA PLA2)
bool	check_consistency (pPLA PLA)

---

Function Documentation

bool check_consistency

(

pPLA

PLA

)

Definition at line 139 of file verify.c.

{
    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;
}

PLA_permute	(	pPLA	PLA1,
		pPLA	PLA2
	)

Definition at line 86 of file verify.c.

{
    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);
}

bool PLA_verify	(	pPLA	PLA1,
		pPLA	PLA2
	)

Definition at line 57 of file verify.c.

{
    /* 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);
}

bool verify	(	pcover	F,
		pcover	Fold,
		pcover	Dold
	)

Definition at line 19 of file verify.c.

{
    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;
}