965 lines
28 KiB
TypeScript
965 lines
28 KiB
TypeScript
/**
|
|
* Copyright 2013-2020 GenieACS Inc.
|
|
*
|
|
* This file is part of GenieACS.
|
|
*
|
|
* GenieACS is free software: you can redistribute it and/or modify
|
|
* it under the terms of the GNU Affero General Public License as
|
|
* published by the Free Software Foundation, either version 3 of the
|
|
* License, or (at your option) any later version.
|
|
*
|
|
* GenieACS is distributed in the hope that it will be useful,
|
|
* but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
* GNU Affero General Public License for more details.
|
|
*
|
|
* You should have received a copy of the GNU Affero General Public License
|
|
* along with GenieACS. If not, see <http://www.gnu.org/licenses/>.
|
|
*/
|
|
|
|
import * as BI from "./bigint";
|
|
import { espresso, complement, tautology } from "yebool";
|
|
import { Expression } from "../types";
|
|
import { map } from "./expression-parser";
|
|
|
|
const ZERO = BI.BigInt(0);
|
|
const ONE = BI.BigInt(1);
|
|
const TWO = BI.BigInt(2);
|
|
const NEGATIVE_ONE = BI.BigInt(-1);
|
|
|
|
class Indeterminates {
|
|
public map: Map<string, number>;
|
|
public sortedKeys: string[];
|
|
|
|
public constructor(str?: string) {
|
|
this.map = new Map();
|
|
if (str) {
|
|
this.map.set(str, 1);
|
|
this.sortedKeys = [str];
|
|
} else {
|
|
this.sortedKeys = [];
|
|
}
|
|
}
|
|
|
|
public reciprocal(): Indeterminates {
|
|
const res = new Indeterminates();
|
|
res.sortedKeys = this.sortedKeys;
|
|
res.map = new Map();
|
|
for (const [k, v] of this.map) res.map.set(k, 0 - v);
|
|
return res;
|
|
}
|
|
|
|
public static multiply(
|
|
indeterminates1: Indeterminates,
|
|
indeterminates2: Indeterminates
|
|
): Indeterminates {
|
|
const res = new Indeterminates();
|
|
res.sortedKeys = indeterminates1.sortedKeys.slice();
|
|
res.map = new Map(indeterminates1.map);
|
|
|
|
for (const [key, val] of indeterminates2.map) {
|
|
const v = res.map.get(key);
|
|
if (!v) {
|
|
res.map.set(key, val);
|
|
res.sortedKeys.push(key);
|
|
} else {
|
|
const v2 = val + v;
|
|
if (!v2) {
|
|
res.map.delete(key);
|
|
res.sortedKeys = res.sortedKeys.filter((s) => s !== key);
|
|
} else {
|
|
res.map.set(key, v2);
|
|
}
|
|
}
|
|
}
|
|
|
|
res.sortedKeys.sort((a, b) => {
|
|
if (a.length !== b.length) return b.length - a.length;
|
|
else if (a > b) return 1;
|
|
else if (a < b) return -1;
|
|
return 0;
|
|
});
|
|
|
|
return res;
|
|
}
|
|
|
|
public static compare(a: Indeterminates, b: Indeterminates): number {
|
|
if (a.sortedKeys.length !== b.sortedKeys.length)
|
|
return b.sortedKeys.length - a.sortedKeys.length;
|
|
for (let i = 0; i < a.sortedKeys.length; ++i) {
|
|
const k1 = a.sortedKeys[i];
|
|
const w1 = a.map.get(k1);
|
|
const k2 = b.sortedKeys[i];
|
|
const w2 = b.map.get(k2);
|
|
if (w1 !== w2) return w2 - w1;
|
|
if (k1.length > k2.length) return -1;
|
|
else if (k1.length < k2.length) return 1;
|
|
else if (k1 > k2) return 1;
|
|
else if (k1 < k2) return -1;
|
|
}
|
|
return 0;
|
|
}
|
|
}
|
|
|
|
interface Term {
|
|
indeterminates: Indeterminates;
|
|
coefficientNumerator: BI.bigint;
|
|
coefficientDenominator: BI.bigint;
|
|
}
|
|
|
|
function findGcd(a: BI.bigint, b: BI.bigint): BI.bigint {
|
|
while (BI.ne(b, ZERO)) {
|
|
const t = b;
|
|
b = BI.rem(a, b);
|
|
a = t;
|
|
}
|
|
return a;
|
|
}
|
|
|
|
class Polynomial {
|
|
public terms: Term[];
|
|
|
|
public constructor(terms: Term[]) {
|
|
this.terms = terms;
|
|
}
|
|
|
|
public static simplifyTerms(terms: Term[]): Term[] {
|
|
const ts = terms
|
|
.slice()
|
|
.sort((a: Term, b: Term) =>
|
|
Indeterminates.compare(a.indeterminates, b.indeterminates)
|
|
);
|
|
|
|
for (let i = 1; i < ts.length; ++i) {
|
|
const t1 = ts[i - 1];
|
|
const t2 = ts[i];
|
|
if (Indeterminates.compare(t1.indeterminates, t2.indeterminates) === 0) {
|
|
const numerator = BI.add(
|
|
BI.mul(t1.coefficientNumerator, t2.coefficientDenominator),
|
|
BI.mul(t2.coefficientNumerator, t1.coefficientDenominator)
|
|
);
|
|
|
|
const denominator = BI.mul(
|
|
t1.coefficientDenominator,
|
|
t2.coefficientDenominator
|
|
);
|
|
|
|
const gcd = findGcd(numerator, denominator);
|
|
|
|
ts[i] = {
|
|
indeterminates: t2.indeterminates,
|
|
coefficientNumerator: BI.div(numerator, gcd),
|
|
coefficientDenominator: BI.div(denominator, gcd),
|
|
};
|
|
ts[i - 1] = {
|
|
indeterminates: t1.indeterminates,
|
|
coefficientNumerator: ZERO,
|
|
coefficientDenominator: t1.coefficientDenominator,
|
|
};
|
|
}
|
|
}
|
|
return ts.filter((v) => BI.ne(v.coefficientNumerator, ZERO));
|
|
}
|
|
|
|
public static fromIndeterminate(indeterminate: Expression): Polynomial {
|
|
const indeterminates = new Indeterminates(JSON.stringify(indeterminate));
|
|
const terms = [
|
|
{
|
|
indeterminates: indeterminates,
|
|
coefficientNumerator: ONE,
|
|
coefficientDenominator: ONE,
|
|
},
|
|
];
|
|
return new Polynomial(terms);
|
|
}
|
|
|
|
public static fromConstant(constant: number): Polynomial {
|
|
const [int, frac] = Math.abs(constant).toString(2).split(".", 2);
|
|
let numerator = BI.BigInt("0b" + int);
|
|
if (constant < 0) numerator = BI.mul(numerator, NEGATIVE_ONE);
|
|
let denominator = ONE;
|
|
if (frac) {
|
|
denominator = BI.exp(TWO, BI.BigInt(frac.length));
|
|
numerator = BI.add(
|
|
BI.mul(numerator, denominator),
|
|
BI.BigInt("0b" + frac)
|
|
);
|
|
}
|
|
|
|
const terms = [
|
|
{
|
|
indeterminates: new Indeterminates(),
|
|
coefficientNumerator: numerator,
|
|
coefficientDenominator: denominator,
|
|
},
|
|
];
|
|
|
|
return new Polynomial(terms);
|
|
}
|
|
|
|
public negation(): Polynomial {
|
|
const terms = this.terms.map((t) => ({
|
|
indeterminates: t.indeterminates,
|
|
coefficientNumerator: BI.mul(t.coefficientNumerator, NEGATIVE_ONE),
|
|
coefficientDenominator: t.coefficientDenominator,
|
|
}));
|
|
|
|
return new Polynomial(terms);
|
|
}
|
|
|
|
public reciprocal(): Polynomial {
|
|
const terms = this.terms.map((t) => ({
|
|
indeterminates: t.indeterminates.reciprocal(),
|
|
coefficientNumerator: t.coefficientDenominator,
|
|
coefficientDenominator: t.coefficientNumerator,
|
|
}));
|
|
return new Polynomial(terms);
|
|
}
|
|
|
|
public constant(): Polynomial {
|
|
const terms = this.terms.filter((t) => !t.indeterminates.sortedKeys.length);
|
|
return new Polynomial(terms);
|
|
}
|
|
|
|
public add(rhs: Polynomial): Polynomial {
|
|
return new Polynomial(
|
|
Polynomial.simplifyTerms(this.terms.concat(rhs.terms))
|
|
);
|
|
}
|
|
|
|
public subtract(rhs: Polynomial): Polynomial {
|
|
return this.add(rhs.negation());
|
|
}
|
|
|
|
public multiply(rhs: Polynomial): Polynomial {
|
|
const terms: Term[] = [];
|
|
|
|
for (const t1 of this.terms) {
|
|
for (const t2 of rhs.terms) {
|
|
const numerator = BI.mul(
|
|
t1.coefficientNumerator,
|
|
t2.coefficientNumerator
|
|
);
|
|
const denominator = BI.mul(
|
|
t1.coefficientDenominator,
|
|
t2.coefficientDenominator
|
|
);
|
|
const gcd = findGcd(numerator, denominator);
|
|
|
|
terms.push({
|
|
indeterminates: Indeterminates.multiply(
|
|
t1.indeterminates,
|
|
t2.indeterminates
|
|
),
|
|
coefficientNumerator: BI.div(numerator, gcd),
|
|
coefficientDenominator: BI.div(denominator, gcd),
|
|
});
|
|
}
|
|
}
|
|
|
|
return new Polynomial(Polynomial.simplifyTerms(terms));
|
|
}
|
|
|
|
public divide(rhs: Polynomial): Polynomial {
|
|
return this.multiply(rhs.reciprocal());
|
|
}
|
|
|
|
public toString(): string {
|
|
const add: string[] = [];
|
|
for (const t of this.terms) {
|
|
const coefficient =
|
|
BI.toNumber(t.coefficientNumerator) /
|
|
BI.toNumber(t.coefficientDenominator);
|
|
|
|
const mul: string[] = [];
|
|
if (t.indeterminates.sortedKeys.length) {
|
|
for (const k of t.indeterminates.sortedKeys) {
|
|
const w = t.indeterminates.map.get(k);
|
|
for (let i = Math.abs(w); i > 0; --i) {
|
|
if (w > 0) mul.push(k);
|
|
else mul.push(`["/",1,${k}]`);
|
|
}
|
|
}
|
|
|
|
if (coefficient !== 1) mul.push(coefficient.toString());
|
|
|
|
if (mul.length > 1) add.push(`["*",${mul.join(",")}]`);
|
|
else add.push(mul["0"]);
|
|
} else {
|
|
add.push(coefficient.toString());
|
|
}
|
|
}
|
|
|
|
if (!add.length) return "0";
|
|
else if (add.length === 1) return add[0];
|
|
else return `["+",${add.join(",")}]`;
|
|
}
|
|
}
|
|
|
|
type Minterm = number[];
|
|
type Context = Map<string, number>;
|
|
|
|
abstract class BoolExprSynth {
|
|
public abstract true(context: Context): Minterm[];
|
|
public abstract false(context: Context): Minterm[];
|
|
public abstract null(context: Context): Minterm[];
|
|
}
|
|
|
|
class TrueSynth extends BoolExprSynth {
|
|
public true(): Minterm[] {
|
|
return [[]];
|
|
}
|
|
public false(): Minterm[] {
|
|
return [];
|
|
}
|
|
public null(): Minterm[] {
|
|
return [];
|
|
}
|
|
}
|
|
|
|
class FalseSynth extends BoolExprSynth {
|
|
public true(): Minterm[] {
|
|
return [];
|
|
}
|
|
public false(): Minterm[] {
|
|
return [[]];
|
|
}
|
|
public null(): Minterm[] {
|
|
return [];
|
|
}
|
|
}
|
|
|
|
class NullSynth extends BoolExprSynth {
|
|
public true(): Minterm[] {
|
|
return [];
|
|
}
|
|
public false(): Minterm[] {
|
|
return [];
|
|
}
|
|
public null(): Minterm[] {
|
|
return [[]];
|
|
}
|
|
}
|
|
|
|
class VarSynth extends BoolExprSynth {
|
|
private expStr: string;
|
|
private negate: boolean;
|
|
public constructor(exp: Expression) {
|
|
super();
|
|
this.negate = false;
|
|
if (Array.isArray(exp)) {
|
|
const op = exp[0];
|
|
if (op === "<>") {
|
|
exp = exp.slice();
|
|
exp[0] = "=";
|
|
this.negate = true;
|
|
} else if (op === ">=") {
|
|
exp = exp.slice();
|
|
exp[0] = "<";
|
|
this.negate = true;
|
|
} else if (op === "<=") {
|
|
exp = exp.slice();
|
|
exp[0] = ">";
|
|
this.negate = true;
|
|
}
|
|
}
|
|
this.expStr = JSON.stringify(exp);
|
|
}
|
|
public true(context: Context): Minterm[] {
|
|
let v = context.get(this.expStr);
|
|
if (v == null) context.set(this.expStr, (v = context.size));
|
|
return [[(v << 2) ^ (this.negate ? 1 : 3)]];
|
|
}
|
|
public false(context: Context): Minterm[] {
|
|
let v = context.get(this.expStr);
|
|
if (v == null) context.set(this.expStr, (v = context.size));
|
|
return [[(v << 2) ^ (this.negate ? 3 : 1)]];
|
|
}
|
|
public null(context: Context): Minterm[] {
|
|
let v = context.get(this.expStr);
|
|
if (v == null) context.set(this.expStr, (v = context.size));
|
|
return [[v << 2, (v << 2) ^ 2]];
|
|
}
|
|
}
|
|
|
|
class NotSynth extends BoolExprSynth {
|
|
private exprSynth: BoolExprSynth;
|
|
public constructor(e: BoolExprSynth) {
|
|
super();
|
|
this.exprSynth = e;
|
|
}
|
|
public true(context: Context): Minterm[] {
|
|
return this.exprSynth.false(context);
|
|
}
|
|
public false(context: Context): Minterm[] {
|
|
return this.exprSynth.true(context);
|
|
}
|
|
public null(context: Context): Minterm[] {
|
|
return this.exprSynth.null(context);
|
|
}
|
|
}
|
|
|
|
class IsNullSynth extends BoolExprSynth {
|
|
private exprSynth: BoolExprSynth;
|
|
public constructor(e: BoolExprSynth) {
|
|
super();
|
|
this.exprSynth = e;
|
|
}
|
|
public true(context: Context): Minterm[] {
|
|
return this.exprSynth.null(context);
|
|
}
|
|
public false(context: Context): Minterm[] {
|
|
return [...this.exprSynth.true(context), ...this.exprSynth.false(context)];
|
|
}
|
|
public null(): Minterm[] {
|
|
return [];
|
|
}
|
|
}
|
|
|
|
class OrSynth extends BoolExprSynth {
|
|
private exprSynths: BoolExprSynth[];
|
|
public constructor(...e: BoolExprSynth[]) {
|
|
super();
|
|
this.exprSynths = e;
|
|
}
|
|
public true(context: Context): Minterm[] {
|
|
return this.exprSynths.map((e) => e.true(context)).flat();
|
|
}
|
|
public false(context: Context): Minterm[] {
|
|
return complement(
|
|
this.exprSynths.map((e) => complement(e.false(context))).flat()
|
|
);
|
|
}
|
|
public null(context: Context): Minterm[] {
|
|
const t = this.exprSynths.map((e) => e.true(context)).flat();
|
|
const f = this.exprSynths.map((e) => e.false(context)).flat();
|
|
return complement([...t, ...f]);
|
|
}
|
|
}
|
|
|
|
class AndSynth extends BoolExprSynth {
|
|
private exprSynths: BoolExprSynth[];
|
|
public constructor(...e: BoolExprSynth[]) {
|
|
super();
|
|
this.exprSynths = e;
|
|
}
|
|
public true(context: Context): Minterm[] {
|
|
return complement(
|
|
this.exprSynths.map((e) => complement(e.true(context))).flat()
|
|
);
|
|
}
|
|
public false(context: Context): Minterm[] {
|
|
return this.exprSynths.map((e) => e.false(context)).flat();
|
|
}
|
|
public null(context: Context): Minterm[] {
|
|
const t = this.exprSynths.map((e) => e.true(context)).flat();
|
|
const f = this.exprSynths.map((e) => e.false(context)).flat();
|
|
return complement([...t, ...f]);
|
|
}
|
|
}
|
|
|
|
const ADDITIVE_IDENTITY = Polynomial.fromConstant(0);
|
|
const MULTIPLICATIVE_IDENTITY = Polynomial.fromConstant(1);
|
|
|
|
const SWAPPED_OPS = {
|
|
"=": "=",
|
|
"<>": "<>",
|
|
">": "<",
|
|
">=": "<=",
|
|
"<": ">",
|
|
"<=": ">=",
|
|
};
|
|
|
|
export function normalize(expr: Expression): Expression {
|
|
expr = map(expr, (exp) => {
|
|
if (!Array.isArray(exp)) return exp;
|
|
const op = exp[0];
|
|
|
|
if (op === "+") {
|
|
const args = exp.slice(1).map((e) => {
|
|
if (e instanceof Polynomial) return e;
|
|
else if (typeof e === "number") return Polynomial.fromConstant(e);
|
|
else return Polynomial.fromIndeterminate(e);
|
|
});
|
|
return (args.reduce(
|
|
(previousValue, currentValue) => previousValue.add(currentValue),
|
|
ADDITIVE_IDENTITY
|
|
) as unknown) as Expression;
|
|
} else if (op === "*") {
|
|
const args = exp.slice(1).map((e) => {
|
|
if (e instanceof Polynomial) return e;
|
|
else if (typeof e === "number") return Polynomial.fromConstant(e);
|
|
else return Polynomial.fromIndeterminate(e);
|
|
});
|
|
|
|
return (args.reduce(
|
|
(previousValue, currentValue) => previousValue.multiply(currentValue),
|
|
MULTIPLICATIVE_IDENTITY
|
|
) as unknown) as Expression;
|
|
} else if (op === "-") {
|
|
const args = exp.slice(1).map((e) => {
|
|
if (e instanceof Polynomial) return e;
|
|
else if (typeof e === "number") return Polynomial.fromConstant(e);
|
|
else return Polynomial.fromIndeterminate(e);
|
|
});
|
|
return (args.reduce((previousValue, currentValue) =>
|
|
previousValue.subtract(currentValue)
|
|
) as unknown) as Expression;
|
|
} else if (op === "/") {
|
|
const args = exp.slice(1).map((e) => {
|
|
if (e instanceof Polynomial) return e;
|
|
else if (typeof e === "number") return Polynomial.fromConstant(e);
|
|
else return Polynomial.fromIndeterminate(e);
|
|
});
|
|
return (args.reduce((previousValue, currentValue) =>
|
|
previousValue.divide(currentValue)
|
|
) as unknown) as Expression;
|
|
} else if (["=", "<>", ">", ">=", "<", "<="].includes(op)) {
|
|
let lhs: Polynomial, rhs: Polynomial;
|
|
if (exp[1] instanceof Polynomial) lhs = exp[1];
|
|
else if (typeof exp[1] === "number")
|
|
lhs = Polynomial.fromConstant(exp[1]);
|
|
|
|
if (exp[2] instanceof Polynomial) rhs = exp[2];
|
|
else if (typeof exp[2] === "number")
|
|
rhs = Polynomial.fromConstant(exp[2]);
|
|
|
|
if (lhs || rhs) {
|
|
if (!lhs) lhs = Polynomial.fromIndeterminate(exp[1]);
|
|
if (!rhs) rhs = Polynomial.fromIndeterminate(exp[2]);
|
|
|
|
lhs = lhs.subtract(rhs);
|
|
rhs = lhs.constant().negation();
|
|
lhs = lhs.add(rhs);
|
|
|
|
if (!lhs.terms.length) {
|
|
exp = [op, JSON.parse(lhs.toString()), JSON.parse(rhs.toString())];
|
|
|
|
if (op === "=") return exp[1] === exp[2];
|
|
else if (op === "<>") return exp[1] !== exp[2];
|
|
else if (op === ">") return exp[1] > exp[2];
|
|
else if (op === ">=") return exp[1] >= exp[2];
|
|
else if (op === "<") return exp[1] < exp[2];
|
|
else if (op === "<=") return exp[1] <= exp[2];
|
|
} else {
|
|
let flipOp = 1;
|
|
|
|
const n = lhs.terms[0].coefficientNumerator;
|
|
const d = lhs.terms[0].coefficientDenominator;
|
|
|
|
if (BI.lt(n, ZERO) || BI.lt(d, ZERO)) flipOp *= -1;
|
|
|
|
const reciprocal = new Polynomial([
|
|
{
|
|
indeterminates: new Indeterminates(),
|
|
coefficientNumerator: d,
|
|
coefficientDenominator: n,
|
|
},
|
|
]);
|
|
|
|
lhs = lhs.multiply(reciprocal);
|
|
rhs = rhs.multiply(reciprocal);
|
|
|
|
const keys = lhs.terms[0].indeterminates.sortedKeys;
|
|
let invert =
|
|
lhs.terms[0].indeterminates.map.get(keys[0]) < 0 ? -1 : 0;
|
|
|
|
for (const t of lhs.terms)
|
|
for (const v of t.indeterminates.map.values()) invert += v;
|
|
|
|
if (invert < 0) {
|
|
flipOp *= -1;
|
|
lhs = lhs.reciprocal();
|
|
rhs = rhs.reciprocal();
|
|
}
|
|
|
|
if (flipOp < 0) exp = [SWAPPED_OPS[op], lhs, rhs];
|
|
else exp = [op, lhs, rhs];
|
|
}
|
|
}
|
|
}
|
|
|
|
// Restore polynomial expressions
|
|
exp = exp.map((e) =>
|
|
e instanceof Polynomial ? JSON.parse(e.toString()) : e
|
|
);
|
|
|
|
return exp;
|
|
});
|
|
|
|
if (expr instanceof Polynomial) expr = JSON.parse(expr.toString());
|
|
|
|
return expr;
|
|
}
|
|
|
|
function toBoolExprSynth(e: Expression | BoolExprSynth): BoolExprSynth {
|
|
if (e instanceof BoolExprSynth) return e;
|
|
else if (Array.isArray(e)) return new VarSynth(e);
|
|
else if (e == null) return new NullSynth();
|
|
else if (e) return new TrueSynth();
|
|
else return new FalseSynth();
|
|
}
|
|
|
|
function sopToExpression(
|
|
sop: number[][],
|
|
expressions: Map<number, Expression>
|
|
): Expression {
|
|
if (!sop.length) return false;
|
|
const res: Expression[] = [];
|
|
for (const s of sop) {
|
|
if (!s.length) return true;
|
|
const and: Expression[] = [];
|
|
for (const i of s) {
|
|
let expr = expressions.get(i >>> 2);
|
|
if (!(i & 1) !== !(i & 2)) expr = ["NOT", expr];
|
|
if (Array.isArray(expr) && expr[0] === "NOT" && Array.isArray(expr[1])) {
|
|
const e: Expression[] = expr[1];
|
|
if (e[0] === "IS NULL") expr = ["IS NOT NULL", ...e.slice(1)];
|
|
else if (e[0] === "=") expr = ["<>", ...e.slice(1)];
|
|
else if (e[0] === "<>") expr = ["=", ...e.slice(1)];
|
|
else if (e[0] === ">") expr = ["<=", ...e.slice(1)];
|
|
else if (e[0] === ">=") expr = ["<", ...e.slice(1)];
|
|
else if (e[0] === "<") expr = [">=", ...e.slice(1)];
|
|
else if (e[0] === "<=") expr = [">", ...e.slice(1)];
|
|
else if (e[0] === "NOT") expr = e[1];
|
|
else expr = ["NOT", e];
|
|
}
|
|
and.push(expr);
|
|
}
|
|
if (and.length > 1) res.push(["AND" as any].concat(and));
|
|
else res.push(and[0]);
|
|
}
|
|
if (res.length > 1) return ["OR" as any].concat(res);
|
|
return res[0];
|
|
}
|
|
|
|
function generateDcSetAndIsNull(
|
|
variables: Map<number, Expression>
|
|
): { dcSet: number[][]; isNull: Map<number, number> } {
|
|
// TODO support LIKE and NOT LIKE operators
|
|
const relations: Map<
|
|
string,
|
|
{ op: string; rhs: boolean | number | string; var: number }[]
|
|
> = new Map();
|
|
|
|
for (const [n, e] of variables) {
|
|
const op = e[0] as string;
|
|
if (["=", ">", "<"].includes(op) && !Array.isArray(e[2])) {
|
|
const lhs = JSON.stringify(e[1]);
|
|
let r = relations.get(lhs);
|
|
if (!r) relations.set(lhs, (r = []));
|
|
r.push({ op: op, rhs: e[2], var: n });
|
|
} else {
|
|
const lhs = JSON.stringify(e);
|
|
let r = relations.get(lhs);
|
|
if (!r) relations.set(lhs, (r = []));
|
|
r.push({ op: "", rhs: null, var: n });
|
|
}
|
|
}
|
|
|
|
const dcSet: number[][] = [];
|
|
const isNull: Map<number, number> = new Map();
|
|
|
|
for (const [key, rels] of relations) {
|
|
const n = variables.size;
|
|
variables.set(n, ["IS NULL", JSON.parse(key)]);
|
|
|
|
if (key === '["PARAM","DeviceID.ID"]' || key === '["PARAM","_id"]')
|
|
dcSet.push([(n << 2) ^ 3]);
|
|
|
|
const existingOps = new Map() as Map<string, Map<string, number>>;
|
|
for (const rel of rels) {
|
|
if (!rel.op) continue;
|
|
const rhsStr = JSON.stringify(rel.rhs);
|
|
const s = existingOps.get(rhsStr);
|
|
if (s) s.set(rel.op, rel.var);
|
|
else existingOps.set(rhsStr, new Map([[rel.op, rel.var]]));
|
|
}
|
|
|
|
for (const [k, v] of existingOps) {
|
|
if (v.size > 1) {
|
|
if (!v.has("=")) {
|
|
const va = variables.size;
|
|
variables.set(va, ["=", JSON.parse(key), JSON.parse(k)]);
|
|
rels.push({ op: "=", rhs: JSON.parse(k), var: va });
|
|
v.set("=", va);
|
|
}
|
|
|
|
if (!v.has(">")) {
|
|
const va = variables.size;
|
|
variables.set(va, [">", JSON.parse(key), JSON.parse(k)]);
|
|
rels.push({ op: ">", rhs: JSON.parse(k), var: va });
|
|
v.set(">", va);
|
|
}
|
|
|
|
if (!v.has("<")) {
|
|
const va = variables.size;
|
|
variables.set(va, ["<", JSON.parse(key), JSON.parse(k)]);
|
|
rels.push({ op: "<", rhs: JSON.parse(k), var: va });
|
|
v.set("<", va);
|
|
}
|
|
|
|
dcSet.push([
|
|
(v.get("=") << 2) ^ 1,
|
|
(v.get(">") << 2) ^ 1,
|
|
(v.get("<") << 2) ^ 1,
|
|
]);
|
|
}
|
|
}
|
|
|
|
for (let i = 0; i < rels.length; ++i) {
|
|
const rel1 = rels[i];
|
|
isNull.set(rel1.var, n);
|
|
|
|
dcSet.push([(n << 2) ^ 3, (rel1.var << 2) ^ 1]);
|
|
dcSet.push([(n << 2) ^ 3, (rel1.var << 2) ^ 3]);
|
|
dcSet.push([(rel1.var << 2) ^ 0, (rel1.var << 2) ^ 2, (n << 2) ^ 2]);
|
|
|
|
if (!rel1.op) continue;
|
|
for (let j = i + 1; j < rels.length; ++j) {
|
|
const rel2 = rels[j];
|
|
if (!rel2.op) continue;
|
|
let comp = 0;
|
|
if (Array.isArray(rel1.rhs) || Array.isArray(rel2.rhs)) {
|
|
if (JSON.stringify(rel1.rhs) !== JSON.stringify(rel2.rhs)) continue;
|
|
} else if (typeof rel1.rhs === "string") {
|
|
if (typeof rel2.rhs === "string") {
|
|
if (rel1.rhs > rel2.rhs) comp = 1;
|
|
else if (rel1.rhs < rel2.rhs) comp = -1;
|
|
} else {
|
|
comp = 1;
|
|
}
|
|
} else if (typeof rel2.rhs === "string") {
|
|
comp = -1;
|
|
} else {
|
|
comp = +rel1.rhs - +rel2.rhs;
|
|
}
|
|
|
|
if (rel1.op === rel2.op) {
|
|
if (comp === 0)
|
|
dcSet.push([(rel1.var << 2) ^ 1, (rel2.var << 2) ^ 1]);
|
|
else if (rel1.op === "=")
|
|
dcSet.push([(rel1.var << 2) ^ 3, (rel2.var << 2) ^ 3]);
|
|
else if (
|
|
(rel1.op === ">" && comp > 0) ||
|
|
(rel1.op === "<" && comp < 0)
|
|
)
|
|
dcSet.push([(rel1.var << 2) ^ 3, (rel2.var << 2) ^ 1]);
|
|
else if (
|
|
(rel1.op === "<" && comp > 0) ||
|
|
(rel1.op === ">" && comp < 0)
|
|
)
|
|
dcSet.push([(rel1.var << 2) ^ 1, (rel2.var << 2) ^ 3]);
|
|
} else if (rel1.op === "=" || rel2.op === "=") {
|
|
let r1 = rel1,
|
|
r2 = rel2,
|
|
cmp = comp;
|
|
if (rel1.op !== "=") {
|
|
r2 = rel1;
|
|
r1 = rel2;
|
|
cmp = -comp;
|
|
}
|
|
if (r2.op === ">" || r2.op === "<") {
|
|
if (cmp === 0) {
|
|
dcSet.push([(r1.var << 2) ^ 3, (r2.var << 2) ^ 3]);
|
|
} else {
|
|
if ((cmp > 0 && r2.op === ">") || (cmp < 0 && r2.op === "<"))
|
|
dcSet.push([(r1.var << 2) ^ 3, (r2.var << 2) ^ 1]);
|
|
else dcSet.push([(r1.var << 2) ^ 3, (r2.var << 2) ^ 3]);
|
|
}
|
|
}
|
|
} else if (
|
|
[">", "<"].includes(rel1.op) &&
|
|
[">", "<"].includes(rel2.op)
|
|
) {
|
|
if ((rel1.op === ">" && comp < 0) || (rel1.op === "<" && comp > 0))
|
|
dcSet.push([(rel1.var << 2) ^ 1, (rel2.var << 2) ^ 1]);
|
|
else dcSet.push([(rel1.var << 2) ^ 3, (rel2.var << 2) ^ 3]);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
return { dcSet, isNull };
|
|
}
|
|
|
|
function sanitizeMinterms(
|
|
minterms: number[][],
|
|
isNull: Map<number, number>
|
|
): number[][] {
|
|
const res = [] as number[][];
|
|
loop: for (const m of minterms) {
|
|
const merged: Map<number, number> = new Map();
|
|
for (const i of m)
|
|
merged.set(i >> 2, (merged.get(i >> 2) || 0) | (1 << (i & 3)));
|
|
const minterm: number[] = [];
|
|
const perms: number[][] = [];
|
|
for (const [k, v] of merged) {
|
|
if (v === 0b1010) continue loop;
|
|
const n = isNull.get(k) << 2;
|
|
const t = k << 2;
|
|
if (v === 0b0101) minterm.push(n ^ 3);
|
|
else if (v === 0b0001) perms.push([n ^ 3, t ^ 3]);
|
|
else if (v === 0b0100) perms.push([n ^ 3, t ^ 1]);
|
|
else if (v & 0b1000) minterm.push(t ^ 3);
|
|
else if (v & 0b0010) minterm.push(t ^ 1);
|
|
}
|
|
let ms = [minterm];
|
|
while (perms.length) {
|
|
const newMs: number[][] = [];
|
|
const perm = perms.pop();
|
|
for (const p of perm) newMs.push(...ms.map((mm) => [...mm, p]));
|
|
ms = newMs;
|
|
}
|
|
res.push(...ms);
|
|
}
|
|
return res;
|
|
}
|
|
|
|
function boolExprSynthToExpression(boolExpr: BoolExprSynth): Expression {
|
|
const context: Map<string, number> = new Map();
|
|
let minterms = boolExpr.true(context);
|
|
const variables = new Map(
|
|
Array.from(context).map(([k, v]) => [v, JSON.parse(k) as Expression])
|
|
);
|
|
const { dcSet, isNull } = generateDcSetAndIsNull(variables);
|
|
minterms = sanitizeMinterms(minterms, isNull);
|
|
|
|
function canRaise(idx: number, set: Set<number>): boolean {
|
|
if (set.size === 1) return true;
|
|
const i = idx >>> 2;
|
|
const n = isNull.get(i);
|
|
if (n == null) {
|
|
for (const [k, v] of isNull) {
|
|
if (v !== i) continue;
|
|
if (set.has((k << 2) ^ 1) || set.has((k << 2) ^ 3)) return true;
|
|
}
|
|
return false;
|
|
}
|
|
return (idx & 1) === 0 || set.has((n << 2) ^ 2) || set.has((n << 2) ^ 3);
|
|
}
|
|
minterms = espresso(minterms, dcSet, { canRaise });
|
|
return sopToExpression(minterms, variables);
|
|
}
|
|
|
|
function mapCallback(exp: Expression): Expression {
|
|
if (!Array.isArray(exp)) return exp;
|
|
const op = exp[0];
|
|
if (op === "IS NULL")
|
|
return (new IsNullSynth(toBoolExprSynth(exp[1])) as unknown) as Expression;
|
|
|
|
if (op === "IS NOT NULL") {
|
|
return (new NotSynth(
|
|
new IsNullSynth(toBoolExprSynth(exp[1]))
|
|
) as unknown) as Expression;
|
|
} else if (op === "NOT") {
|
|
return (new NotSynth(toBoolExprSynth(exp[1])) as unknown) as Expression;
|
|
} else if (op === "OR") {
|
|
return (new OrSynth(
|
|
...exp.slice(1).map((a) => toBoolExprSynth(a))
|
|
) as unknown) as Expression;
|
|
} else if (op === "AND") {
|
|
return (new AndSynth(
|
|
...exp.slice(1).map((a) => toBoolExprSynth(a))
|
|
) as unknown) as Expression;
|
|
}
|
|
for (let i = 1; i < exp.length; ++i) {
|
|
if (exp[i] instanceof BoolExprSynth)
|
|
exp[i] = boolExprSynthToExpression(exp[i]);
|
|
}
|
|
return exp;
|
|
}
|
|
|
|
export function minimize(expr: Expression): Expression {
|
|
expr = normalize(expr);
|
|
expr = map(expr, mapCallback);
|
|
if (expr instanceof BoolExprSynth) return boolExprSynthToExpression(expr);
|
|
return expr;
|
|
}
|
|
|
|
export function unionDiff(
|
|
expr1: Expression,
|
|
expr2: Expression
|
|
): [Expression, Expression] {
|
|
expr2 = normalize(expr2);
|
|
|
|
if (!expr2) return [expr1, false];
|
|
|
|
expr2 = map(expr2, mapCallback);
|
|
|
|
if (!expr1) {
|
|
if (expr2 instanceof BoolExprSynth)
|
|
expr2 = boolExprSynthToExpression(expr2);
|
|
return [expr2, expr2];
|
|
}
|
|
|
|
const b2 = toBoolExprSynth(expr2);
|
|
expr1 = normalize(expr1);
|
|
expr1 = map(expr1, mapCallback);
|
|
const b1 = toBoolExprSynth(expr1);
|
|
|
|
const context: Map<string, number> = new Map();
|
|
|
|
const expr2Minterms = b2.true(context);
|
|
const expr1Minterms = b1.true(context);
|
|
const expr1NullMinterms = b1.null(context);
|
|
const expr1FalseMinterms = b1.false(context);
|
|
const variables = new Map(
|
|
Array.from(context).map(([k, v]) => [v, JSON.parse(k) as Expression])
|
|
);
|
|
const { dcSet, isNull } = generateDcSetAndIsNull(variables);
|
|
|
|
const unionMinterms = sanitizeMinterms(
|
|
[...expr1Minterms, ...expr2Minterms],
|
|
isNull
|
|
);
|
|
const diffMinterms = sanitizeMinterms(
|
|
complement([
|
|
...complement([...expr1NullMinterms, ...expr1FalseMinterms]),
|
|
...complement(expr2Minterms),
|
|
]),
|
|
isNull
|
|
);
|
|
|
|
function canRaise(idx: number, set: Set<number>): boolean {
|
|
if (set.size === 1) return true;
|
|
const i = idx >>> 2;
|
|
const n = isNull.get(i);
|
|
if (n == null) {
|
|
for (const [k, v] of isNull) {
|
|
if (v !== i) continue;
|
|
if (set.has((k << 2) ^ 1) || set.has((k << 2) ^ 3)) return true;
|
|
}
|
|
return false;
|
|
}
|
|
return (idx & 1) === 0 || set.has((n << 2) ^ 2) || set.has((n << 2) ^ 3);
|
|
}
|
|
|
|
const union = espresso(unionMinterms, dcSet, { canRaise });
|
|
const diff = espresso(diffMinterms, dcSet, { canRaise });
|
|
|
|
return [sopToExpression(union, variables), sopToExpression(diff, variables)];
|
|
}
|
|
|
|
export function covers(expr1: Expression, expr2: Expression): boolean {
|
|
expr2 = normalize(expr2);
|
|
if (!expr2) return true;
|
|
expr1 = normalize(expr1);
|
|
if (!Array.isArray(expr1)) return !!expr1;
|
|
|
|
expr1 = map(expr1, mapCallback);
|
|
const b1 = toBoolExprSynth(expr1);
|
|
expr2 = map(expr2, mapCallback);
|
|
const b2 = toBoolExprSynth(expr2);
|
|
|
|
const context: Map<string, number> = new Map();
|
|
const expr1Minterms = b1.true(context);
|
|
const expr2Minterms = b2.true(context);
|
|
const variables = new Map(
|
|
Array.from(context).map(([k, v]) => [v, JSON.parse(k) as Expression])
|
|
);
|
|
const { dcSet } = generateDcSetAndIsNull(variables);
|
|
|
|
return tautology([...complement(expr2Minterms), ...dcSet, ...expr1Minterms]);
|
|
}
|