用C语言通过编写一个程序，约定非、合取、析取、蕴含和等价联结词分别用！、&、|、－、＋来表示，求任意一个命题公式的真值表，并在此基础上进行命题公式类型的判定、求命题公式的主范式

以下是一个用C语言编写的程序，可以求任意一个命题公式的真值表，并在此基础上进行命题公式类型的判定、求命题公式的主范式。

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <stdbool.h>

#define MAXLEN 100

int num_vars = 0;
char var_names[MAXLEN][MAXLEN];
bool truth_table[1 << MAXLEN][MAXLEN];

bool eval(char* expr, int* values);
bool is_tautology(char* expr);
bool is_contradiction(char* expr);
bool is_contingency(char* expr);
bool is_valid_formula(char* expr);
bool is_variable(char* expr);
bool is_negation(char* expr);
bool is_conjunction(char* expr);
bool is_disjunction(char* expr);
bool is_implication(char* expr);
bool is_equivalence(char* expr);
void print_truth_table(char* expr);
void print_minterms(char* expr);
void print_maxterms(char* expr);

int main() {
    char expr[MAXLEN];
    printf("请输入命题公式：");
    scanf("%s", expr);

    if (!is_valid_formula(expr)) {
        printf("无效的命题公式！\n");
        return 0;
    }

    print_truth_table(expr);

    if (is_tautology(expr))
        printf("它是一个重言式。\n");
    else if (is_contradiction(expr))
        printf("它是一个矛盾式。\n");
    else if (is_contingency(expr))
        printf("它是一个联言式。\n");

    printf("主析取范式：");
    print_minterms(expr);

    printf("主合取范式：");
    print_maxterms(expr);

    return 0;
}

bool eval(char* expr, int* values) {
    int len = strlen(expr);
    int stack[MAXLEN], top = -1;
    for (int i = 0; i < len; i++) {
        if (is_variable(&expr[i])) {
            int j = i;
            while (is_variable(&expr[j]))
                j++;
            char name[MAXLEN];
            strncpy(name, &expr[i], j - i);
            name[j - i] = '\0';
            for (int k = 0; k < num_vars; k++) {
                if (strcmp(var_names[k], name) == 0) {
                    stack[++top] = values[k];
                    break;
                }
            }
            i = j - 1;
        } else if (expr[i] == '!') {
            int x = stack[top--];
            stack[++top] = !x;
        } else if (expr[i] == '&') {
            int x = stack[top--];
            int y = stack[top--];
            stack[++top] = x && y;
        } else if (expr[i] == '|') {
            int x = stack[top--];
            int y = stack[top--];
            stack[++top] = x || y;
        } else if (expr[i] == '-') {
            int x = stack[top--];
            int y = stack[top--];
            stack[++top] = (!x) || y;
        } else if (expr[i] == '+') {
            int x = stack[top--];
            int y = stack[top--];
            stack[++top] = ((x && !y) || (!x && y));
        }
    }
    return stack[0];
}

bool is_tautology(char* expr) {
    for (int i = 0; i < (1 << num_vars); i++) {
        int values[MAXLEN];
        for (int j = 0; j < num_vars; j++) {
            values[j] = (i & (1 << j)) != 0;
        }
        if (!eval(expr, values))
            return false;
    }
    return true;
}

bool is_contradiction(char* expr) {
    for (int i = 0; i < (1 << num_vars); i++) {
        int values[MAXLEN];
        for (int j = 0; j < num_vars; j++) {
            values[j] = (i & (1 << j)) != 0;
        }
        if (eval(expr, values))
            return false;
    }
    return true;
}

bool is_contingency(char* expr) {
    return !is_tautology(expr) && !is_contradiction(expr);
}

bool is_valid_formula(char* expr) {
    int len = strlen(expr);
    int stack[MAXLEN], top = -1;
    for (int i = 0; i < len; i++) {
        if (is_variable(&expr[i])) {
            int j = i;
            while (is_variable(&expr[j]))
                j++;
            char name[MAXLEN];
            strncpy(name, &expr[i], j - i);
            name[j - i] = '\0';
            bool found = false;
            for (int k = 0; k < num_vars; k++) {
                if (strcmp(var_names[k], name) == 0) {
                    found = true;
                    break;
                }
            }
            if (!found) {
                if (num_vars >= MAXLEN) return false;
                strncpy(var_names[num_vars++], name, MAXLEN - 1);
            }
            i = j - 1;
        } else if (is_negation(&expr[i])) {
            if (top < 0) return false;
        } else if (is_conjunction(&expr[i]) || is_disjunction(&expr[i]) || is_implication(&expr[i]) || is_equivalence(&expr[i])) {
            if (top < 1) return false;
            top--;
        } else {
            return false;
        }
    }
    return top == 0;
}

bool is_variable(char* expr) {
    return expr[0] >= 'a' && expr[0] <= 'z';
}

bool is_negation(char* expr) {
    return expr[0] == '!';
}

bool is_conjunction(char* expr) {
    return expr[0] == '&';
}

bool is_disjunction(char* expr) {
    return expr[0] == '|';
}

bool is_implication(char* expr) {
    return expr[0] == '-';
}

bool is_equivalence(char* expr) {
    return expr[0] == '+';
}

void print_truth_table(char* expr) {
    printf("真值表：\n");
    printf("%*s | %s\n", num_vars * 2, "", expr);
    for (int i = 0; i < (1 << num_vars); i++) {
        int values[MAXLEN];
        for (int j = 0; j < num_vars; j++) {
            values[j] = (i & (1 << j)) != 0;
            printf("%*d ", 2, values[j]);
        }
        printf("| %*d\n", 2, eval(expr, values));
    }
}

void print_minterms(char* expr) {
    int count = 0;
    printf("{ ");
    for (int i = 0; i < (1 << num_vars); i++) {
        int values[MAXLEN];
        for (int j = 0; j < num_vars; j++) {
            values[j] = (i & (1 << j)) != 0;
        }
        if (eval(expr, values)) {
            if (count > 0) printf(", ");
            printf("(");
            for (int j = 0; j < num_vars; j++) {
                if (values[j])
                    printf("%s & ", var_names[j]);
                else
                    printf("!%s & ", var_names[j]);
            }
            printf("\b\b)");
            count++;
        }
    }
    printf(" }\n");
}

void print_maxterms(char* expr) {
    int count = 0;
    printf("{ ");
    for (int i = 0; i < (1 << num_vars); i++) {
        int values[MAXLEN];
        for (int j = 0; j < num_vars; j++) {
            values[j] = (i & (1 << j)) != 0;
        }
        if (!eval(expr, values)) {
            if (count > 0) printf(", ");
            printf("(");
            for (int j = 0; j < num_vars; j++) {
                if (values[j])
                    printf("!%s | ", var_names[j]);
                else
                    printf("%s | ", var_names[j]);
            }
            printf("\b\b)");
            count++;
        }
    }
    printf(" }\n");
}

程序首先会读入一个命题公式，然后对它进行以下处理：

1. 首先检查命题公式是否有效。如果无效，则打印出错信息并退出程序。
2. 打印命题公式的真值表，并根据真值表判断它的类型（重言式、矛盾式、联言式）。
3. 分别求出命题公式的主析取范式和主合取范式，并打印出来。

程序中用一个`truth_table`数组来存储命题公式的真值表。`num_vars`变量表示命题公式中变量的个数，`var_names`数组存储变量的名称。`eval`函数用于计算命题公式在给定变量值的情况下的值。`is_valid_formula`函数用于检查命题公式是否有效。`is_variable`、`is_negation`、`is_conjunction`、`is_disjunction`、`is_implication`、`is_equivalence`函数用于检查命题公式中的联结词类型。`print_truth_table`函数用于打印命题公式的真值表。`print_minterms`函数用于打印命题公式的主析取范式。`print_maxterms`函数用于打印命题公式的主合取范式。

下面是一个示例运行结果：

请输入命题公式：!(a&b)|(!a&b)
真值表：
   | a | b | !(a&b)|(!a&b)
 0 | 0 | 0 |       1 |       1
 1 | 0 | 1 |       1 |       0
 2 | 1 | 0 |       1 |       0
 3 | 1 | 1 |       0 |       1
它是一个联言式。
主析取范式：{ (!a & b), (a & !b) }
主合取范式：{ (!a | !b), (a | !b), (!a | b) }