Boolean function equivalence (SEERC 2015 Problem A)

compare.cpp

#include <iostream>
#include <cstdio>
#include <vector>
#include <string>
#include <exception>
#include <algorithm>
using namespace std;

const char NOT_SIGN = '~';
const char AND_SIGN = '^';
const char OR_SIGN  = 'V';

enum NodeType { VAR, NOT, AND, OR };

struct Node {
    NodeType type;
    Node *left;
    Node *right;
    char var;

    Node(NodeType type, Node *left, Node *right, char var = '#'):
        type(type), left(left), right(right), var(var) {}
};

typedef vector< Node* > NodeList;
typedef NodeList OrList;
typedef NodeList AndList;
typedef vector< OrList* > AndOrList;

Node* var_node(char var) {
    return new Node(VAR, nullptr, nullptr, var);
}

Node* not_node(Node *left) {
    return new Node(NOT, left, nullptr);
}

Node* and_node(Node *left, Node *right) {
    return new Node(AND, left, right);
}

Node* or_node(Node *left, Node *right) {
    return new Node(OR, left, right);
}

bool is_var(Node *node) {
    return node && node->type == VAR;
}

bool is_not(Node *node) {
    return node && node->type == NOT;
}

bool is_and(Node *node) {
    return node && node->type == AND;
}

bool is_or(Node *node) {
    return node && node->type == OR;
}

string parse_line;
int parse_pos;

char consume_char() {
    while (parse_pos < parse_line.size()) {
        auto c = parse_line[parse_pos++];
        if (c != ' ') {
            return c;
        }
    }
    throw logic_error("consume_char: end of line");
}

char consume_char(char expected) {
    auto c = consume_char();
    if (c != expected) {
        throw logic_error("consume_char: unexpected character");
    }
    return c;
}

Node* parse() {
    auto c = consume_char();
    if (c == '(') {
        auto left = parse();
        auto op = consume_char();
        if (op == ')') {
            return left;
        }
        auto right = parse();
        consume_char(')');
        if (op == AND_SIGN) {
            return and_node(left, right);
        }
        if (op == OR_SIGN) {
            return or_node(left, right);
        }
        throw logic_error("parse: unknown operator");
    }
    else if (c == NOT_SIGN) {
        return not_node(parse());
    }
    else if (('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z')) {
        return var_node(c);
    }
    throw logic_error("parse: no parse");
}

Node* read_line() {
    string line;
    getline(cin, line);
    parse_line = '(' + line + ')';
    parse_pos = 0;
    return parse();
}

ostream& operator<<(ostream &out, Node *node) {
    if (!node) {
        out << "NULL node";
    }
    else if (is_var(node)) {
        out << node->var;
    }
    else if (is_not(node)) {
        out << NOT_SIGN << node->left;
    }
    else if (is_and(node)) {
        out << "(" << node->left << AND_SIGN << node->right << ")";
    }
    else if (is_or(node)) {
        out << "(" << node->left << OR_SIGN << node->right << ")";
    }
    return out;
}

Node* push_nots(Node *node) {
    if (!node) {
        throw logic_error("push_nots: null node");
    }
    else if (is_not(node)) {
        if (is_not(node->left)) {
            return push_nots(node->left->left);
        }
        else if (is_and(node->left) || is_or(node->left)) {
            auto left = node->left->left;
            auto right = node->left->right;
            auto type = node->left->type;
            delete node;
            return type == AND
                ? or_node (push_nots(not_node(left)), push_nots(not_node(right)))
                : and_node(push_nots(not_node(left)), push_nots(not_node(right)));
        }
        else {
            return node;
        }
    }
    else if (is_and(node) || is_or(node)) {
        node->left  = push_nots(node->left);
        node->right = push_nots(node->right);
        return node;
    }
    else {
        return node;
    }
}

Node* to_and_form(Node *node) {
    if (!node) {
        throw logic_error("to_and_form: null node");
    }
    auto left = node->left;
    auto right = node->right;
    if (is_and(node)) {
        node->left = to_and_form(left);
        node->right = to_and_form(right);
        return node;
    }
    else if (is_or(node)) {
        left = to_and_form(left);
        right = to_and_form(right);
        if (is_and(left) || is_and(right)) {
            delete node;
            Node *a, *b, *c;
            if (is_and(left)) {
                // (a & b) | c
                a = left->left;
                b = left->right;
                c = right;
            }
            else {
                // c | (a & b)
                a = right->left;
                b = right->right;
                c = left;
            }
            // (a | c) & (b | c)
            return and_node(to_and_form(or_node(a, c)), to_and_form(or_node(b, c)));
        }
        else {
            node->left = left;
            node->right = right;
            return node;
        }
    }
    else {
        return node;
    }
}

OrList* to_or_list(Node *node, OrList *result = nullptr) {
    if (!node) {
        throw logic_error("to_or_list: null node");
    }
    if (is_and(node)) {
        throw logic_error("to_or_list: AND node inside OR form");
    }
    if (result == nullptr) {
        result = new OrList();
    }
    if (is_or(node)) {
        to_or_list(node->left, result);
        to_or_list(node->right, result);
    }
    else {
        if (is_not(node) && !is_var(node->left)) {
            throw logic_error("to_or_list: NOT of non-VAR node");
        }
        result->push_back(node);
    }
    return result;
}

// node in AND-form required
AndList* to_and_list(Node *node, AndList *result = nullptr) {
    if (!node) {
        throw logic_error("to_and_list: null node");
    }
    if (result == nullptr) {
        result = new AndList();
    }
    if (is_and(node)) {
        to_and_list(node->left, result);
        to_and_list(node->right, result);
    }
    else {
        result->push_back(node);
    }
    return result;
}

AndOrList* to_and_or_list(Node *node) {
    auto result = new AndOrList();
    auto and_list = to_and_list(node);
    for (auto &inner_node : *and_list) {
        auto or_list = to_or_list(inner_node);
        result->push_back(or_list);
    }
    delete and_list;
    return result;
}

char get_atom_var(Node *node) {
    if (!node) {
        throw logic_error("get_atom_var: null node");
    }
    else if (is_var(node)) {
        return node->var;
    }
    else if (is_not(node) && is_var(node->left)) {
        return node->left->var;
    }
    else {
        throw logic_error("get_atom_var: complex node");
    }
}

bool is_true(OrList *or_list) {
    for (int i = 0; i < or_list->size(); ++i) {
        auto node_i = or_list->at(i);
        for (int j = i + 1; j < or_list->size(); ++j) {
            auto node_j = or_list->at(j);
            if (is_not(node_i) != is_not(node_j)
                && get_atom_var(node_i) == get_atom_var(node_j)) {
                return true;
            }
        }
    }
    return false;
}

bool is_true(AndOrList *and_or_list) {
    for (auto &or_list : *and_or_list) {
        if (!is_true(or_list)) {
            return false;
        }
    }
    return true;
}

bool is_true(Node *node) {
    return is_true(to_and_or_list(to_and_form(push_nots(node))));
}

Node* clone(Node *node) {
    if (!node) {
        return nullptr;
    }
    return new Node(node->type, clone(node->left), clone(node->right), node->var);
}

bool implies(Node *a, Node *b) {
    a = clone(a);
    b = clone(b);
    return is_true(or_node(not_node(a), b));
}

bool equivalent(Node *a, Node *b) {
    return implies(a, b) && implies(b, a);
}

int main() {
    auto a = read_line();
    auto b = read_line();
    string ans = equivalent(a, b) ? "1" : "0";
    cout << ans << "\n";
    return 0;
}