論理式を変形するやつ

main.js

"use strict";

let variable_names = [];

function tokenize(s) {

    function isNextToken(s, i, t) {
        for (let j = 0; j < t.length; j++) {
            if (s.substr(i, t[j].length) == t[j]) {
                return j;
            }
        }
        return -1;
    }

    let or = ["or", "OR", "+", "|", "||"];
    let and = ["and", "AND", "*", "&&", "&"];
    let not = ["not", "!", "-", "~"];
    let xor = ["xor", "^", "^^"];
    let result = [];
    let vars = {};
    for (let i = 0; i < s.length;) {
        if (s[i] == " ") {
            i++;
            continue;
        }
        {
            let index = isNextToken(s, i, or);
            if (index != -1) {
                result.push({ type: "or" });
                i += or[index].length;
                continue;
            }
        }
        {
            let index = isNextToken(s, i, and);
            if (index != -1) {
                result.push({ type: "and" });
                i += and[index].length;
                continue;
            }
        }
        {
            let index = isNextToken(s, i, not);
            if (index != -1) {
                result.push({ type: "not" });
                i += not[index].length;
                continue;
            }
        }
        {
            let index = isNextToken(s, i, xor);
            if (index != -1) {
                result.push({ type: "xor" });
                i += xor[index].length;
                continue;
            }
        }
        if (s[i] == "(") {
            result.push({ type: "(" });
            i++;
            continue;
        }
        if (s[i] == ")") {
            result.push({ type: ")" });
            i++;
            continue;
        }
        vars[s[i]] = true;
        result.push({ type: "ident", name: s[i] });
        i++;
    }
    variable_names = Object.keys(vars).sort();
    return result;
}

function parse(ts) {
    let parserindex = 0;
    return or(ts);

    function or(ts) {
        let lhs = and(ts);
        while (parserindex < ts.length && (ts[parserindex].type == "or" || ts[parserindex].type == "xor")) {
            let op = ts[parserindex].type;
            parserindex++;
            let rhs = and(ts);
            lhs = { op: op, lhs: lhs, rhs, rhs };
        }
        return lhs;
    }
    function and(ts) {
        let lhs = not(ts);
        while (parserindex < ts.length && (ts[parserindex].type == "and" || ts[parserindex].type == "ident" || ts[parserindex].type == "(" || ts[parserindex].type == "not")) {
            parserindex += (ts[parserindex].type == "and") ? 1 : 0;
            let rhs = not(ts);
            lhs = { op: "and", lhs: lhs, rhs: rhs };
        }
        return lhs;
    }
    function not(ts) {
        if (ts[parserindex].type == "not") {
            parserindex++;
            return { op: "not", expr: not(ts) };
        } else {
            return variable(ts);
        }
    }
    function variable(ts) {
        if (ts[parserindex].type == "(") {
            parserindex++;
            let expr = or(ts);
            console.assert(ts[parserindex].type == ")");
            parserindex++;
            return expr;
        }
        let v = { op: "var", name: ts[parserindex].name };
        parserindex++;
        return v;
    }

}

function dumpTree(t) {
    return dump(t, true);
    function dump(t, isRoot) {
        if (t.op == "var") {
            return t.name;
        }
        if (t.op == "and") {
            return dump(t.lhs, false) + dump(t.rhs, false);
        }
        if (t.op == "or" && isRoot) {
            return dump(t.lhs, true) + " + " + dump(t.rhs, true);
        }
        if (t.op == "or") {
            return "(" + dump(t.lhs, true) + " + " + dump(t.rhs, true) + ")";
        }
        if (t.op == "xor") {
            return "(" + dump(t.lhs, true) + " ^ " + dump(t.rhs, true) + ")";
        }
        if (t.op == "not" && t.expr.op == "var") {
            return "~" + dump(t.expr, true);
        }
        if (t.op == "not") {
            return "~(" + dump(t.expr, true) + ")";
        }
        if (t.op == "0") {
            return "0";
        }
        console.assert(false);
    }
}

function clearObject(obj) {
    for (const key in obj) {
        delete obj[key];
    }
}

function expandXor(tree) {
    return expand(tree);
    function expand(t) {
        if (t.op == "var") {
            return t;
        }
        if (t.op == "and") {
            t.lhs = expand(t.lhs);
            t.rhs = expand(t.rhs);
            return t;
        }
        if (t.op == "or") {
            t.lhs = expand(t.lhs);
            t.rhs = expand(t.rhs);
            return t;
        }
        if (t.op == "not") {
            t.expr = expand(t.expr);
            return t;
        }
        if (t.op == "xor") {
            let rhs = Object.assign({}, t.rhs);
            let lhs = Object.assign({}, t.lhs);
            t.op = "and";
            t.lhs = { op: "or", lhs: lhs, rhs: rhs };
            t.rhs = { op: "not", expr: { op: "and", lhs: lhs, rhs: rhs } };
            console.log(dumpTree(tree));
            return expand(t);
        }
        console.assert(false);
    }
}

function expandNot(tree) {
    return expand(tree);
    function expand(t) {
        if (t.op == "var") {
            return t;
        }
        if (t.op == "and") {
            t.lhs = expand(t.lhs);
            t.rhs = expand(t.rhs);
            return t;
        }
        if (t.op == "or") {
            t.lhs = expand(t.lhs);
            t.rhs = expand(t.rhs);
            return t;
        }
        if (t.op == "not") {
            if (t.expr.op == "var") {
                return t;
            }
            if (t.expr.op == "and") {
                let expr = Object.assign({}, t.expr);
                let lhs = Object.assign({}, expr.lhs);
                let rhs = Object.assign({}, expr.rhs);
                clearObject(t);
                t.op = "or";
                t.lhs = { op: "not", expr: lhs };
                t.rhs = { op: "not", expr: rhs };
                console.log(dumpTree(tree));
                return expand(t);
            }
            if (t.expr.op == "or") {
                let lhs = Object.assign({}, t.expr.lhs);
                let rhs = Object.assign({}, t.expr.rhs);
                clearObject(t);
                t.op = "and";
                t.lhs = { op: "not", expr: lhs };
                t.rhs = { op: "not", expr: rhs };
                console.log(dumpTree(tree));
                return expand(t);
            }
            if (t.expr.op == "not") {
                let expr = Object.assign({}, t.expr.expr);
                t = expr;
                console.log(dumpTree(tree));
                return t;
            }
            console.assert(false);
        }
        console.assert(false);
    }
}

function expandAndOr(tree) {
    return expand(tree);
    function expand(t) {
        if (t.op == "var") {
            return t;
        }
        if (t.op == "or") {
            t.lhs = expand(t.lhs);
            t.rhs = expand(t.rhs);
            return t;
        }
        if (t.op == "not") {
            t.expr = expand(t.expr);
            return t;
        }
        if (t.op == "and") {
            t.lhs = expand(t.lhs);
            t.rhs = expand(t.rhs);

            if (t.rhs.op == "or") {
                t.op = "or";
                let rhs = Object.assign({}, t.rhs);
                let lhs = Object.assign({}, t.lhs);
                t.lhs = { op: "and", lhs: lhs, rhs: rhs.lhs };
                t.rhs = { op: "and", lhs: lhs, rhs: rhs.rhs };
                console.log(dumpTree(tree));
                return expand(t);
            }
            if (t.lhs.op == "or") {
                t.op = "or";
                let rhs = Object.assign({}, t.rhs);
                let lhs = Object.assign({}, t.lhs);
                t.lhs = { op: "and", lhs: lhs.lhs, rhs: rhs };
                t.rhs = { op: "and", lhs: lhs.rhs, rhs: rhs };
                console.log(dumpTree(tree));
                return expand(t);
            }
            return t;
        }
        console.assert(false);
    }
}

function pruneAnd(root) {

    return pruneAndimpl(root);

    function pruneAndimpl(tree) {
        if (tree.op == "or") {
            tree.lhs = pruneAndimpl(tree.lhs);
            tree.rhs = pruneAndimpl(tree.rhs);
            return tree;
        }
        if (tree.op == "and") {
            let d = simple(tree, {});
            if (Object.keys(d).length == 1) {
                let key = Object.keys(d)[0];
                if (d[key] == 0) {
                    return { op: "0" };
                }
                if (d[key] == -1) {
                    return { op: "not", expr: { op: "var", name: key } };
                }
                return { op: "var", name: key };
            }
            let lhs = null;
            Object.keys(d).sort().forEach(key => {
                let rhs;
                if (d[key] == 0) {
                    return { op: "0" };
                } else if (d[key] == -1) {
                    rhs = { op: "not", expr: { op: "var", name: key } };
                } else {
                    rhs = { op: "var", name: key };
                }

                if (lhs != undefined) {
                    lhs = { op: "and", lhs: lhs, rhs: rhs }
                }
                else {
                    lhs = rhs;
                }
            });
            return lhs;
        }

        return tree;
    }

    function simple(subtree, dict) {
        if (subtree.op == "and") {
            dict = simple(subtree.lhs, dict);
            dict = simple(subtree.rhs, dict);
            return dict;
        }
        if (subtree.op == "not") {
            if (dict[subtree.expr.name] != undefined && (dict[subtree.expr.name] == 1 || dict[subtree.expr.name] == 0)) {
                dict[subtree.expr.name] = 0;
                return dict;
            }
            dict[subtree.expr.name] = -1;
            return dict;
        }
        if (subtree.op == "var") {
            if (dict[subtree.name] != undefined && (dict[subtree.name] == -1 || dict[subtree.name] == 0)) {
                dict[subtree.name] = 0;
                return dict;
            }
            dict[subtree.name] = 1;
            return dict;
        }
    }
}

function pruneOr(root) {
    let terms = {};
    let zpruned = pruneZero(root);
    console.log(dumpTree(zpruned));
    makeTermTable(zpruned, true);
    let lhs = undefined;
    Object.keys(terms).sort().forEach(key => {
        if (lhs != undefined) {
            lhs = { op: "or", lhs: lhs, rhs: terms[key] }
        }
        else {
            lhs = terms[key];
        }
    });
    console.log(dumpTree(lhs));
    return lhs;

    function makeTermTable(tree) {
        if (tree.op == "or") {
            makeTermTable(tree.lhs);
            makeTermTable(tree.rhs);
            return;
        }
        if (tree.op == "and" || tree.op == "not" || tree.op == "var") {
            terms[dumpTree(tree)] = tree;
            return;
        }
        console.assert(false);
    }

    function pruneZero(tree) {
        if (tree.op == "or") {
            tree.lhs = pruneZero(tree.lhs);
            tree.rhs = pruneZero(tree.rhs);
            if (tree.lhs.op == "0" && tree.rhs.op == "0") {
                return { op: "0" };
            }
            if (tree.lhs.op == "0") {
                let rhs = Object.assign({}, tree.rhs);
                return rhs;
            }
            if (tree.rhs.op == "0") {
                let lhs = Object.assign({}, tree.lhs);
                return lhs;
            }
        }
        return tree;
    }
}

function normalize(root) {

    return normalizeimpl(root);

    function normalizeimpl(tree) {
        if (tree.op == "or") {
            tree.lhs = normalizeimpl(tree.lhs);
            tree.rhs = normalizeimpl(tree.rhs);
            return tree;
        }
        if (tree.op == "and" || tree.op == "not" || tree.op == "var") {
            let d = listVars(tree, {});
            variable_names.forEach(variable => {
                if (d[variable] == undefined) {
                    let lhs = Object.assign({}, tree)
                    tree = { op: "and", lhs: lhs, rhs: { op: "or", lhs: { op: "var", name: variable }, rhs: { op: "not", expr: { op: "var", name: variable } } } }
                }
            });
            console.log(dumpTree(root));
            return tree;
        }
    }

    function listVars(tree, dict) {
        if (tree.op == "and") {
            dict = listVars(tree.lhs, dict);
            dict = listVars(tree.rhs, dict);
            return dict;
        }
        if (tree.op == "not") {
            dict[tree.expr.name] = true;
            return dict;
        }
        if (tree.op == "var") {
            dict[tree.name] = true;
            return dict;
        }
        console.assert(false);
    }
}