/* Конъюктивная нормальная форма (JavaScript)
Преобразовать логическую формулу в конъюктивную нормальную форму.
Логическая формула может содержать константы "0" - ложь и "1" - истина,
переменные от "a" до "z",
логические связи "&" - конъюнкция, "|" - дизъюнкция, "~" - отрицание,
скобки.
Логическая формула задаётся в виде аргументы функции cnf, ответ должен выводиться на консоль.
Пример : cnf("(a & b) | ~c"), ответ на консоли может быть : "(a|~c)&(b|~c)".
*/

function cnf(formula) {
    // delete splits
    formula = formula.replace(/\s+/g, '');

    // convert the formula to an array of tokens
    const tokens = formula.split(/([&|()])/);

    function isOperator(token) {
        return token === '&' || token === '|';
    }

    function isVariable(token) {
        return /[a-z]/.test(token);
    }

    function isOpeningParenthesis(token) {
        return token === '(';
    }

    function isClosingParenthesis(token) {
        return token === ')';
    }

    function getOperatorPriority(operator) {
        if (operator === '&') {
            return 2;
        } else if (operator === '|') {
            return 1;
        } else {
            return 0;
        }
    }

    function toReversePolishNotation(tokens) {
        const stack = [];
        const output = [];

        for (let i = 0; i < tokens.length; i++) {
            const token = tokens[i];

            if (isVariable(token)) {
                output.push(token);
            } else if (isOperator(token)) {
                while (
                    stack.length > 0 &&
                    isOperator(stack[stack.length - 1]) &&
                    getOperatorPriority(token) <= getOperatorPriority(stack[stack.length - 1])
                    ) {
                    output.push(stack.pop());
                }
                stack.push(token);
            } else if (isOpeningParenthesis(token)) {
                stack.push(token);
            } else if (isClosingParenthesis(token)) {
                while (!isOpeningParenthesis(stack[stack.length - 1])) {
                    output.push(stack.pop());
                }
                stack.pop();
            }
        }

        while (stack.length > 0) {
            output.push(stack.pop());
        }

        return output;
    }

    function toCNF(tokens) {
        const rpn = toReversePolishNotation(tokens);
        const stack = [];

        for (let i = 0; i < rpn.length; i++) {
            const token = rpn[i];
            if (isVariable(token)) {
                stack.push([token]);
            } else if (isOperator(token)) {
                const right = stack.pop();
                const left = stack.pop();

                if (token === '&') {
                    stack.push(left.concat(right));
                } else if (token === '|') {
                    const result = [];
                        for (let j = 0; j < left.length; j++) {
                            for (let k = 0; k < right.length; k++) {
                                result.push(left[j].concat('|').concat(right[k]));
                            }
                        }

                    stack.push(result);
                }
            }
        }
        return stack[0].map(clause => ('(' + clause + ')')).join('&');
    }

    console.log(toCNF(tokens));
}

cnf("(a & b) | ~c"); // (a|~c)&(b|~c)