離散數學 求命題公式的主析取範式和主合取範式

Description

輸入命題公式的合式公式，求出公式的真值表，並輸出該公式的主合取範式和主析取範式。

Input

命題公式的合式公式

Output

公式的主析取範式和主合取範式，輸出形式爲：「 mi ∨ mj ; Mi ∧ Mj」 ，極小項和 ∨ 符號之間有一個空格，極大項和 ∧ 符號之間有一個空格；主析取範式和主合取範式之間用「 ; 」隔開，「 ; 」先後各有一個空格。 永真式的主合取範式爲 1 ，永假式的主析取範式爲 0 。

輸入公式的符號說明：
! 非，至關於書面符號中的 「 ¬ 」
& 與，至關於書面符號中的 「 ∧ 」
| 或，至關於書面符號中的 「 ∨ 」

• 蘊含聯結詞，至關於書面符號中的 「 → 」
• 等價聯結詞，至關於書面符號中的 「 ↔ 」
  ( 前括號
  ) 後括號

Code

#include <cstdio>
#include <cstring>
#include <cmath>
#define N 1000
#define MAX 10000000
char s[N];
bool table[30];
int explain[30];
int value[MAX];
int sum = 0;
int priority(char c)
{
    switch (c)
    {
        case '#': return -1;
        case '!': return 5;
        case '&': return 4;
        case '|': return 3;
        case '-': return 2;
        case '+': return 1;
        case '(': return 0;
        default: return 0;
    }
}
void postfix()
{
    char post[N] = { '\0' };
    int pp = -1;
    char stack[N] = { '#' };
    int ps = 0;

    int len = strlen(s);
    for (int i = 0; i < len; i++)
    {
        if (s[i] >= 'a' && s[i] <= 'z')
        {
            post[++pp] = s[i];
            continue;
        }
        if (s[i] == '!' || s[i] == '&' || s[i] == '|' || s[i] == '-' || s[i] == '+')
        {
            while (priority(s[i]) <= priority(stack[ps]))
                post[++pp] = stack[ps--];
            stack[++ps] = s[i];
            continue;
        }
        if (s[i] == '(')
        {
            stack[++ps] = s[i];
            continue;
        }
        if (s[i] == ')')
        {
            while (stack[ps] != '(') post[++pp] = stack[ps--];
            ps--;
            continue;
        }
    }
    while (ps) post[++pp] = stack[ps--];
    strcpy(s, post);
    int l = strlen(s);
}
void settable()
{
    memset(table, 0, sizeof(table));
    int len = strlen(s);
    for (int i = 0; i < len; i++)
    {
        if (s[i] >= 'a' && s[i] < 'z')
            table[s[i] - 'a'] = true;
    }
    for (int i = 0; i < 26; i++)
        if (table[i]) sum++;
    sum = pow(2, sum);
}
int btoi()
{
    int sum = 0, weight = 1;
    for (int i = 25; i >= 0; i--)
        if (table[i])
        {
            if (explain[i]) sum += weight;
            weight *= 2;
        }
    return sum;
}
int calc(int a, int b, char c)
{
    switch (c)
    {
        case '&': return a * b;
        case '|': if (a + b) return 1; else return 0;
        case '-': if (a == 1 && b == 0) return 0; else return 1;
        case '+': return !((a + b) & 1);
    }
}
int work()
{
    int stack[N], ps = -1;
    int len = strlen(s);
    for (int i = 0; i < len; i++)
    {
        if (s[i] >= 'a' && s[i] <= 'z')
        {
            stack[++ps] = explain[s[i] - 'a'];
            continue;
        }
        if (s[i] == '!')
        {
            stack[ps] = (stack[ps] + 1) & 1;
            continue;
        }
        int ans = calc(stack[ps - 1], stack[ps], s[i]);
        stack[--ps] = ans;
    }
    return stack[0];
}
void assign()
{
    int x = btoi();
    int ans = work();
    value[x] = ans;
}
void generate(char c)
{
    while (c <= 'z' && table[c - 'a'] == false) c++;
    if (c > 'z')
    {
        assign();
        return;
    }
    explain[c - 'a'] = 0;
    generate(c + 1);
    explain[c - 'a'] = 1;
    generate(c + 1);
}
void output1()
{
    int i = 0;
    while (i < sum && !value[i]) i++;
    if (i >= sum)
    {
        printf("0 ; ");
        return;
    }
    printf("m%d", i);
    for (i++; i < sum; i++)
        if (value[i]) printf(" ∨ m%d", i);
    printf(" ; ");
}
void output2()
{
    int i = 0;
    while (i < sum && value[i]) i++;
    if (i >= sum)
    {
        printf("1\n");
        return;
    }
    printf("M%d", i);
    for (i++; i < sum; i++)
        if (!value[i]) printf(" ∧ M%d", i);
    printf("\n");
}
int main()
{
    scanf("%s", s);
    postfix();
    settable();
    memset(value, 0, sizeof(value));
    memset(explain, 0, sizeof(explain));
    generate('a');
    output1();
    output2();
    return 0;
}