Boolean Logic

Boolean Logic

---

Time Limit:1s	Memory limit:32M
Accepted Submit:3	Total Submit:6

---

Propositions are logical formulas consisting of proposition symbols and connecting operators. They are recursively defined by the following rules:

1. All proposition symbols (in this problem, lower-case alphabetic characters, e.g., a and z) are propositions.
2. If P is a proposition, (!P) is a proposition, and P is a direct subformula of it.
3. If P and Q are propositions, (P&Q), (P|Q), (P-->Q), and (P<->Q) are propositions, and P and Q are direct subformulas of them.
4. Nothing else is a proposition.

The operations !, &, |, -->, and <-> denote logical negation, conjunction, disjunction, implication, and equivalence, respectively. A proposition P is a subformula of a proposition R if P=R or P is a direct subformula of a proposition Q and Q is a subformula of R.

Let P be a proposition and assign boolean values (i.e., 0 or 1) to all proposition symbols that occur in P. This induces a boolean value to all subformulas of P according to the standard semantics of the logical operators:

negation	conjunction	disjunction	implication	equivalence
!0=1	0&0=0	0|0=0	0-->0=1	0<->0=1
!1=0	0&1=0	0|1=1	0-->1=1	0<->1=0
	1&0=0	1|0=1	1-->0=0	1<->0=0
	1&1=1	1|1=1	1-->1=1	1<->1=1

This way, a value for P can be calculated. This value depends on the choice of the assignment of boolean values to the proposition symbols. If P contains n different proposition symbols, there are 2ⁿ different assignments. To evaluate all possible assignments we may use truth tables.

A truth table contains one line per assignment (i.e., 2ⁿ lines in total). Every line contains the values of all subformulas under the chosen assignment. The value of a subformula is aligned with the proposition symbol, if the subformula is a proposition symbol, and with the center of the operator otherwise.

Input Specification

The input contains several test cases, each on a separate line. Every test case denotes a proposition and may contain arbitrary amounts of spaces in between. The input file terminates immediately after the newline symbol following the last test case.

Output Specification

For each test case generate a truth table for the denoted proposition. Start the truth table by repeating the input line. Evaluate the proposition (and its subformulas) for all assignments to its variables, and output one line for each assignment. The line must have the same length as the corresponding input line and must consist only of spaces and the characters 0 and 1. Output an empty line after each test case.

Let s₁,...,s_n be the proposition symbols in the denoted proposition sorted in alphabetic order. Then, all assignments of 0 to s₁ must precede the assignments of 1 to s₁. Within each of these blocks of assignments, all assignments of 0 to s₂ must precede the assignments of 1 to s₂, and so on.

Sample Input

((b --> a) <-> ((! a) --> (! b)))
  ((y &  a)   -  ->(c |c))

Sample Output

((b --> a) <-> ((! a) --> (! b)))
  0  1  0   1    1 0   1   1 0   
  1  0  0   1    1 0   0   0 1   
  0  1  1   1    0 1   1   1 0   
  1  1  1   1    0 1   1   0 1   

  ((y &  a)   -  ->(c |c))
    0 0  0       1  0 00  
    1 0  0       1  0 00  
    0 0  0       1  1 11  
    1 0  0       1  1 11  
    0 0  1       1  0 00  
    1 1  1       0  0 00  
    0 0  1       1  1 11  
    1 1  1       1  1 11  

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

#define NEG 26
#define CONG 27
#define DISG 28
#define IMPL 29
#define EQUI 30

#define sym_neg(x) (!(x))
#define sym_conj(x, y) ((x) & (y))
#define sym_disj(x, y) ((x) | (y))
#define sym_impl(x, y) (!(((x) ^ (y)) & (x)))
#define sym_euqi(x, y) ((x) == (y))

struct mem
{
    int type;
    int position;
};
struct mem arr[200];
int stack[200];
int opnd[26];

char in[200];
int index;

int build(int i)
{
    int position;

    if (in[i] == '\0')
        return i;
    
    while (in[i])
    {
        if (in[i] == ' ')
        {
            ++i;
            continue;
        }
        if (in[i] == '(')
        {
            return build(i + 1);
        }
        else if (in[i] == ')')
        {
            return i + 1;
        }
        else if (in[i] == '!')
        {
            position = i;
            i = build(i + 1);
            arr[index].type = 26;
            arr[index].position = position;
            index++;
        }
        else if (in[i] == '&')
        {
            position = i;
            i = build(i + 1);
            arr[index].type = 27;
            arr[index].position = position;
            index++;
        }
        else if (in[i] == '|')
        {
            position = i;
            i = build(i + 1);
            arr[index].type = 28;
            arr[index].position = position;
            index++;
        }
        else if (in[i] == '-')
        {
            ++i;
            while (in[i] != '>')
            {
                if (in[i] == '-')
                    position = i;
                ++i;
            }
            i = build(i + 1);
            arr[index].type = 29;
            arr[index].position = position;
            index++;
        }
        else if (in[i] == '<')
        {
            ++i;
            while (in[i] != '>')
            {
                if (in[i] == '-')
                    position = i;
                ++i;
            }
            i = build(i + 1);
            arr[index].type = 30;
            arr[index].position = position;
            index++;
        }
        else
        {
            arr[index].position = i;
            arr[index].type = in[i] - 'a';
            opnd[in[i] - 'a'] = 1;
            index++;
            ++i;
        }
    }

    return i;
}

int main()
{
    int i, j, top, val, num, len;
    char *p = NULL;
    char out[200];

    while (gets(in))
    {
        len = strlen(in);
        printf("%s\n", in);

        memset(out, ' ', sizeof(out));
        memset(opnd, 0, sizeof(opnd));
        out[len] = '\0';

        index = 0;
        build(0);

        num = 0;
        for (i = 25; i >= 0; --i)
        {
            if (opnd[i])
                opnd[i] = ++num;
        }

        for (i = 0, val = 0; i < (1 << num); ++i, ++val)
        {
            top = 0;
            for (j = 0; j < index; ++j)
            {
                if (arr[j].type < 26)
                {
                    stack[top] = (((1 << (opnd[arr[j].type] - 1)) & val) == 0 ? 0 : 1);
                    out[arr[j].position] = stack[top] + '0';
                    ++top;
                }
                else
                {
                    switch(arr[j].type)
                    {
                    case 26:
                        --top;
                        stack[top] = sym_neg(stack[top]);
                        out[arr[j].position] = stack[top] + '0';
                        ++top;
                        break;
                    case 27:
                        top -= 2;
                        stack[top] = sym_conj(stack[top], stack[top + 1]);
                        out[arr[j].position] = stack[top] + '0';
                        ++top;
                        break;
                    case 28:
                        top -= 2;
                        stack[top] = sym_disj(stack[top], stack[top + 1]);
                        out[arr[j].position] = stack[top] + '0';
                        ++top;
                        break;
                    case 29:
                        top -= 2;
                        stack[top] = sym_impl(stack[top], stack[top + 1]);
                        out[arr[j].position] = stack[top] + '0';
                        ++top;
                        break;
                    case 30:
                        top -= 2;
                        stack[top] = sym_euqi(stack[top], stack[top + 1]);
                        out[arr[j].position] = stack[top] + '0';
                        ++top;
                        break;
                    }
                }
            }
            printf("%s\n", out);
        }

        printf("\n");
    }

    return 0;
}