Zaid Abdulla
bc2d258f9c
It's now more intelligent about generating IS NULL clauses. For example, instead of 'LOWER(param) IS NULL' it now generates 'param IS NULL'.
1241 lines
37 KiB
TypeScript
1241 lines
37 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 "espresso-iisojs";
|
|
import { Expression } from "../types";
|
|
import { map } from "./expression-parser";
|
|
import { and, evaluateCallback } from "./expression";
|
|
|
|
const ZERO = BI.BigInt(0);
|
|
const ONE = BI.BigInt(1);
|
|
const TWO = BI.BigInt(2);
|
|
const NEGATIVE_ONE = BI.BigInt(-1);
|
|
|
|
class Indeterminates {
|
|
public declare map: Map<string, number>;
|
|
public declare 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 declare 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[];
|
|
|
|
abstract class BoolExprSynth {
|
|
public abstract true(context: SynthContext): Minterm[];
|
|
public abstract false(context: SynthContext): Minterm[];
|
|
public abstract null(context: SynthContext): 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 declare exp: Expression;
|
|
private declare 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;
|
|
} else if (op === "NOT LIKE") {
|
|
exp = exp.slice();
|
|
exp[0] = "LIKE";
|
|
this.negate = true;
|
|
}
|
|
}
|
|
this.exp = exp;
|
|
}
|
|
public true(context: SynthContext): Minterm[] {
|
|
const v = context.getVariable(this.exp);
|
|
return [[(v << 2) ^ (this.negate ? 1 : 3)]];
|
|
}
|
|
public false(context: SynthContext): Minterm[] {
|
|
const v = context.getVariable(this.exp);
|
|
return [[(v << 2) ^ (this.negate ? 3 : 1)]];
|
|
}
|
|
public null(context: SynthContext): Minterm[] {
|
|
const v = context.getVariable(this.exp);
|
|
return [[v << 2, (v << 2) ^ 2]];
|
|
}
|
|
}
|
|
|
|
class NotSynth extends BoolExprSynth {
|
|
private declare exprSynth: BoolExprSynth;
|
|
public constructor(e: BoolExprSynth) {
|
|
super();
|
|
this.exprSynth = e;
|
|
}
|
|
public true(context: SynthContext): Minterm[] {
|
|
return this.exprSynth.false(context);
|
|
}
|
|
public false(context: SynthContext): Minterm[] {
|
|
return this.exprSynth.true(context);
|
|
}
|
|
public null(context: SynthContext): Minterm[] {
|
|
return this.exprSynth.null(context);
|
|
}
|
|
}
|
|
|
|
class IsNullSynth extends BoolExprSynth {
|
|
private declare exprSynth: BoolExprSynth;
|
|
public constructor(e: BoolExprSynth) {
|
|
super();
|
|
this.exprSynth = e;
|
|
}
|
|
public true(context: SynthContext): Minterm[] {
|
|
return this.exprSynth.null(context);
|
|
}
|
|
public false(context: SynthContext): Minterm[] {
|
|
return [...this.exprSynth.true(context), ...this.exprSynth.false(context)];
|
|
}
|
|
public null(): Minterm[] {
|
|
return [];
|
|
}
|
|
}
|
|
|
|
class OrSynth extends BoolExprSynth {
|
|
private declare exprSynths: BoolExprSynth[];
|
|
public constructor(...e: BoolExprSynth[]) {
|
|
super();
|
|
this.exprSynths = e.filter((ee) => !(ee instanceof FalseSynth));
|
|
const unpacked: BoolExprSynth[] = [];
|
|
this.exprSynths = this.exprSynths.filter((ee) => {
|
|
if (ee instanceof OrSynth) {
|
|
unpacked.push(...ee.exprSynths);
|
|
return false;
|
|
}
|
|
return true;
|
|
});
|
|
this.exprSynths.push(...unpacked);
|
|
}
|
|
public true(context: SynthContext): Minterm[] {
|
|
if (this.exprSynths.length === 0) return [];
|
|
if (this.exprSynths.length === 1) return this.exprSynths[0].true(context);
|
|
if (this.exprSynths.some((e) => e instanceof TrueSynth)) return [[]];
|
|
return this.exprSynths.map((e) => e.true(context)).flat();
|
|
}
|
|
public false(context: SynthContext): Minterm[] {
|
|
if (this.exprSynths.length === 0) return [[]];
|
|
if (this.exprSynths.length === 1) return this.exprSynths[0].false(context);
|
|
if (
|
|
this.exprSynths.some(
|
|
(e) => e instanceof TrueSynth || e instanceof NullSynth
|
|
)
|
|
)
|
|
return [];
|
|
return complement(
|
|
this.exprSynths.map((e) => complement(e.false(context))).flat()
|
|
);
|
|
}
|
|
public null(context: SynthContext): Minterm[] {
|
|
if (this.exprSynths.length === 0) return [];
|
|
if (this.exprSynths.length === 1) return this.exprSynths[0].null(context);
|
|
const n = this.exprSynths.map((e) => e.null(context)).flat();
|
|
const t = this.exprSynths.map((e) => e.true(context)).flat();
|
|
return complement([...complement(n), ...t]);
|
|
}
|
|
}
|
|
|
|
class AndSynth extends BoolExprSynth {
|
|
private declare exprSynths: BoolExprSynth[];
|
|
public constructor(...e: BoolExprSynth[]) {
|
|
super();
|
|
this.exprSynths = e.filter((ee) => !(ee instanceof TrueSynth));
|
|
const unpacked: BoolExprSynth[] = [];
|
|
this.exprSynths = this.exprSynths.filter((ee) => {
|
|
if (ee instanceof AndSynth) {
|
|
unpacked.push(...ee.exprSynths);
|
|
return false;
|
|
}
|
|
return true;
|
|
});
|
|
this.exprSynths.push(...unpacked);
|
|
}
|
|
public true(context: SynthContext): Minterm[] {
|
|
if (this.exprSynths.length === 0) return [[]];
|
|
if (this.exprSynths.length === 1) return this.exprSynths[0].true(context);
|
|
if (
|
|
this.exprSynths.some(
|
|
(e) => e instanceof FalseSynth || e instanceof NullSynth
|
|
)
|
|
)
|
|
return [];
|
|
return complement(
|
|
this.exprSynths.map((e) => complement(e.true(context))).flat()
|
|
);
|
|
}
|
|
public false(context: SynthContext): Minterm[] {
|
|
if (this.exprSynths.length === 0) return [];
|
|
if (this.exprSynths.length === 1) return this.exprSynths[0].false(context);
|
|
if (this.exprSynths.some((e) => e instanceof FalseSynth)) return [[]];
|
|
return this.exprSynths.map((e) => e.false(context)).flat();
|
|
}
|
|
public null(context: SynthContext): Minterm[] {
|
|
if (this.exprSynths.length === 0) return [];
|
|
if (this.exprSynths.length === 1) return this.exprSynths[0].null(context);
|
|
const n = this.exprSynths.map((e) => e.null(context)).flat();
|
|
const f = this.exprSynths.map((e) => e.false(context)).flat();
|
|
return complement([...complement(n), ...f]);
|
|
}
|
|
}
|
|
|
|
class CaseSynth extends BoolExprSynth {
|
|
private declare exprSynths: BoolExprSynth[];
|
|
public constructor(e: BoolExprSynth[]) {
|
|
super();
|
|
this.exprSynths = e;
|
|
}
|
|
public true(context: SynthContext): Minterm[] {
|
|
const minterms: Minterm[] = [];
|
|
const cumulative: Minterm[] = [];
|
|
for (let i = 0; i < this.exprSynths.length; i += 2) {
|
|
const w = this.exprSynths[i].true(context);
|
|
const t = this.exprSynths[i + 1].true(context);
|
|
minterms.push(
|
|
...complement([...cumulative, ...complement(w), ...complement(t)])
|
|
);
|
|
if (i < this.exprSynths.length - 2) {
|
|
cumulative.push(
|
|
...complement([
|
|
...this.exprSynths[i].false(context),
|
|
...this.exprSynths[i].null(context),
|
|
])
|
|
);
|
|
}
|
|
}
|
|
return minterms;
|
|
}
|
|
public false(context: SynthContext): Minterm[] {
|
|
const minterms: Minterm[] = [];
|
|
const cumulative: Minterm[] = [];
|
|
for (let i = 0; i < this.exprSynths.length; i += 2) {
|
|
const w = this.exprSynths[i].true(context);
|
|
const t = this.exprSynths[i + 1].false(context);
|
|
minterms.push(
|
|
...complement([...cumulative, ...complement(w), ...complement(t)])
|
|
);
|
|
if (i < this.exprSynths.length - 2) {
|
|
cumulative.push(
|
|
...complement([
|
|
...this.exprSynths[i].false(context),
|
|
...this.exprSynths[i].null(context),
|
|
])
|
|
);
|
|
}
|
|
}
|
|
return minterms;
|
|
}
|
|
public null(context: SynthContext): Minterm[] {
|
|
const minterms: Minterm[] = [];
|
|
const cumulative: Minterm[] = [];
|
|
for (let i = 0; i < this.exprSynths.length; i += 2) {
|
|
const w = this.exprSynths[i].true(context);
|
|
const t = this.exprSynths[i + 1].null(context);
|
|
minterms.push(
|
|
...complement([...cumulative, ...complement(w), ...complement(t)])
|
|
);
|
|
cumulative.push(
|
|
...complement([
|
|
...this.exprSynths[i].false(context),
|
|
...this.exprSynths[i].null(context),
|
|
])
|
|
);
|
|
}
|
|
minterms.push(...complement([...cumulative]));
|
|
return minterms;
|
|
}
|
|
}
|
|
|
|
const ADDITIVE_IDENTITY = Polynomial.fromConstant(0);
|
|
const MULTIPLICATIVE_IDENTITY = Polynomial.fromConstant(1);
|
|
|
|
const SWAPPED_OPS = {
|
|
"=": "=",
|
|
"<>": "<>",
|
|
">": "<",
|
|
">=": "<=",
|
|
"<": ">",
|
|
"<=": ">=",
|
|
};
|
|
|
|
function normalizeCallback(exp: Expression): Expression {
|
|
if (!Array.isArray(exp)) return exp;
|
|
const op = exp[0];
|
|
|
|
if (op === "FUNC" && exp[1] === "COALESCE") {
|
|
const res: Expression[] = ["CASE"];
|
|
for (let i = 2; i < exp.length; ++i)
|
|
res.push(normalizeCallback(["IS NOT NULL", exp[i]]), exp[i]);
|
|
return normalizeCallback(res);
|
|
}
|
|
|
|
if (op === "CASE") {
|
|
const res = [] as [Expression, Expression][];
|
|
for (let i = 1; i < exp.length; i += 2) {
|
|
let w = exp[i];
|
|
if (w instanceof Polynomial) w = JSON.parse(w.toString());
|
|
if (!Array.isArray(w) && !w) continue;
|
|
const t = exp[i + 1];
|
|
if (!Array.isArray(t) || t[0] !== "CASE") {
|
|
res.push([w, t]);
|
|
continue;
|
|
}
|
|
for (let j = 1; j < t.length; j += 2) res.push([and(w, t[j]), t[j + 1]]);
|
|
res.push([w, null]);
|
|
if (!Array.isArray(w) && w) break;
|
|
}
|
|
while (res[res.length - 1][1] == null) res.pop();
|
|
return ["CASE", ...res.flat()];
|
|
}
|
|
|
|
const permutations: Map<number, [Expression, Expression][]> = new Map();
|
|
for (const [i, e] of exp.entries()) {
|
|
if (!Array.isArray(e)) continue;
|
|
if (e[0] !== "CASE") continue;
|
|
const perms: [Expression, Expression][] = [];
|
|
for (let j = 1; j < e.length; j += 2) perms.push([e[j], e[j + 1]]);
|
|
permutations.set(i, perms);
|
|
}
|
|
|
|
if (permutations.size) {
|
|
let res: [Expression, Expression][] = [[true, exp]];
|
|
for (const [i, perms] of permutations) {
|
|
const res2: [Expression, Expression][] = [];
|
|
for (const [w, t] of perms) {
|
|
res2.push(
|
|
...res.map((r) => {
|
|
const e = (r[1] as Expression[]).slice();
|
|
e[i] = t;
|
|
return [and(w, r[0]), e] as [Expression, Expression];
|
|
})
|
|
);
|
|
}
|
|
res = res2;
|
|
}
|
|
|
|
for (const r of res) r[1] = normalizeCallback(r[1]);
|
|
|
|
if (res[0][0] === true) return res[0][1];
|
|
while (res[res.length - 1][1] == null) res.pop();
|
|
|
|
return ["CASE", ...res.flat()];
|
|
}
|
|
|
|
function toPolynomial(e: Expression): Polynomial {
|
|
if (e == null) return null;
|
|
if (e instanceof Polynomial) return e;
|
|
if (typeof e === "number") return Polynomial.fromConstant(e);
|
|
if (typeof e === "string")
|
|
return Polynomial.fromConstant(parseFloat(e) || 0);
|
|
if (typeof e === "boolean") return Polynomial.fromConstant(+e);
|
|
return Polynomial.fromIndeterminate(e);
|
|
}
|
|
|
|
if (op === "+") {
|
|
const args: Polynomial[] = [];
|
|
for (let i = 1; i < exp.length; ++i) {
|
|
const p = toPolynomial(exp[i]);
|
|
if (p == null) return null;
|
|
args.push(p);
|
|
}
|
|
return (args.reduce(
|
|
(previousValue, currentValue) => previousValue.add(currentValue),
|
|
ADDITIVE_IDENTITY
|
|
) as unknown) as Expression;
|
|
} else if (op === "*") {
|
|
const args: Polynomial[] = [];
|
|
for (let i = 1; i < exp.length; ++i) {
|
|
const p = toPolynomial(exp[i]);
|
|
if (p == null) return null;
|
|
args.push(p);
|
|
}
|
|
return (args.reduce(
|
|
(previousValue, currentValue) => previousValue.multiply(currentValue),
|
|
MULTIPLICATIVE_IDENTITY
|
|
) as unknown) as Expression;
|
|
} else if (op === "-") {
|
|
const args: Polynomial[] = [];
|
|
for (let i = 1; i < exp.length; ++i) {
|
|
const p = toPolynomial(exp[i]);
|
|
if (p == null) return null;
|
|
args.push(p);
|
|
}
|
|
return (args.reduce((previousValue, currentValue) =>
|
|
previousValue.subtract(currentValue)
|
|
) as unknown) as Expression;
|
|
} else if (op === "/") {
|
|
const args: Polynomial[] = [];
|
|
for (let i = 1; i < exp.length; ++i) {
|
|
const p = toPolynomial(exp[i]);
|
|
if (p == null) return null;
|
|
args.push(p);
|
|
}
|
|
return (args.reduce((previousValue, currentValue) =>
|
|
previousValue.divide(currentValue)
|
|
) as unknown) as Expression;
|
|
} else if (["=", "<>", ">", ">=", "<", "<="].includes(op)) {
|
|
if (exp[1] == null || exp[2] == null) return null;
|
|
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
|
|
);
|
|
|
|
exp = evaluateCallback(exp);
|
|
|
|
return exp;
|
|
}
|
|
|
|
export function normalize(expr: Expression): Expression {
|
|
expr = map(expr, normalizeCallback);
|
|
if (expr instanceof Polynomial) {
|
|
expr = JSON.parse(expr.toString());
|
|
} else if (Array.isArray(expr) && expr[0] === "CASE") {
|
|
expr = expr.map((e) =>
|
|
e instanceof Polynomial ? JSON.parse(e.toString()) : e
|
|
);
|
|
}
|
|
return expr;
|
|
}
|
|
|
|
function toBoolExprSynth(e: Expression | BoolExprSynth): BoolExprSynth {
|
|
if (e instanceof BoolExprSynth) return e;
|
|
if (Array.isArray(e)) {
|
|
if (e[0] === "CASE")
|
|
return new CaseSynth(e.slice(1).map((ee) => toBoolExprSynth(ee)));
|
|
return new VarSynth(e);
|
|
}
|
|
if (e == null) return new NullSynth();
|
|
if (e) return new TrueSynth();
|
|
return new FalseSynth();
|
|
}
|
|
|
|
function sopToExpression(sop: number[][], context: SynthContext): Expression {
|
|
if (!sop.length) return false;
|
|
const res: Expression[] = [];
|
|
for (const s of sop) {
|
|
if (!s.length) return true;
|
|
const conjs: Expression[] = [];
|
|
for (const i of s) {
|
|
let expr = context.getExpression(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] === "LIKE") expr = ["NOT LIKE", ...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];
|
|
}
|
|
conjs.push(expr);
|
|
}
|
|
if (conjs.length > 1) res.push(["AND" as any].concat(conjs));
|
|
else res.push(conjs[0]);
|
|
}
|
|
if (res.length > 1) return ["OR" as any].concat(res);
|
|
return res[0];
|
|
}
|
|
|
|
function findIsNullDeps(exp: Expression): Expression[] {
|
|
if (!Array.isArray(exp)) return [];
|
|
const op = exp[0];
|
|
if (op === "IS NULL" || op === "IS NOT NULL") return [];
|
|
|
|
if (op === "FUNC") {
|
|
if (exp[1] === "NOW") {
|
|
return [];
|
|
} else if (exp[1] === "LOWER" || exp[1] === "UPPER") {
|
|
return findIsNullDeps(exp[2]);
|
|
} else if (exp[1] === "ROUND") {
|
|
return exp
|
|
.slice(2, 4)
|
|
.map((e) => findIsNullDeps(e))
|
|
.flat();
|
|
}
|
|
} else if (op !== "PARAM") {
|
|
return exp
|
|
.slice(1)
|
|
.map((e) => findIsNullDeps(e))
|
|
.flat();
|
|
}
|
|
return [exp];
|
|
}
|
|
|
|
class SynthContext {
|
|
private declare _dcSet: number[][];
|
|
private declare _variables: Map<string, number>;
|
|
private declare _expressions: Map<number, Expression>;
|
|
private declare _isNullRelations: Map<number, number[]>;
|
|
private declare _isNullVars: Set<number>;
|
|
private declare _comparisons: Map<
|
|
string,
|
|
Map<string, { eq: number; gt: number; lt: number }>
|
|
>;
|
|
|
|
constructor() {
|
|
this._dcSet = [];
|
|
this._variables = new Map();
|
|
this._expressions = new Map();
|
|
this._isNullRelations = new Map();
|
|
this._isNullVars = new Set();
|
|
this._comparisons = new Map();
|
|
}
|
|
|
|
getVariable(exp: Expression): number {
|
|
const expStr = JSON.stringify(exp);
|
|
if (this._variables.has(expStr)) return this._variables.get(expStr);
|
|
const v = this._variables.size;
|
|
this._variables.set(expStr, v);
|
|
this._expressions.set(v, exp);
|
|
this.generateIsNullDc(v);
|
|
this.generateComparisionDc(v);
|
|
|
|
if (
|
|
expStr === '["IS NULL",["PARAM","DeviceID.ID"]]' ||
|
|
expStr === '["IS NULL",["PARAM","_id"]]'
|
|
)
|
|
this._dcSet.push([(v << 2) ^ 3]);
|
|
|
|
return v;
|
|
}
|
|
|
|
private generateIsNullDc(v: number): void {
|
|
this._isNullRelations.set(v, []);
|
|
const exp = this._expressions.get(v);
|
|
|
|
const isNull = new Set(
|
|
findIsNullDeps(exp).map((e) => this.getVariable(["IS NULL", e]))
|
|
);
|
|
|
|
if (!isNull.size) return;
|
|
|
|
for (const n of isNull) {
|
|
this._isNullVars.add(n);
|
|
this._isNullRelations.get(n).push(v);
|
|
this._isNullRelations.get(v).push(n);
|
|
this._dcSet.push([(n << 2) ^ 3, (v << 2) ^ 1]);
|
|
this._dcSet.push([(n << 2) ^ 3, (v << 2) ^ 3]);
|
|
}
|
|
this._dcSet.push(
|
|
[...isNull].map((n) => (n << 2) ^ 2).concat([(v << 2) ^ 0, (v << 2) ^ 2])
|
|
);
|
|
}
|
|
|
|
private generateComparisionDc(v: number): void {
|
|
const exp = this._expressions.get(v);
|
|
if (!Array.isArray(exp)) return;
|
|
const op = exp[0];
|
|
if (![">", "<", "="].includes(op)) return;
|
|
const rhs = exp[2];
|
|
const rhsStr = JSON.stringify(rhs);
|
|
const lhsStr = JSON.stringify(exp[1]);
|
|
let allComps = this._comparisons.get(lhsStr);
|
|
if (!allComps) this._comparisons.set(lhsStr, (allComps = new Map()));
|
|
if (allComps.has(rhsStr)) return;
|
|
|
|
const comp = {
|
|
eq: -1,
|
|
gt: -1,
|
|
lt: -1,
|
|
};
|
|
|
|
allComps.set(rhsStr, comp);
|
|
|
|
comp.eq = this.getVariable(["=", exp[1], exp[2]]);
|
|
comp.gt = this.getVariable([">", exp[1], exp[2]]);
|
|
comp.lt = this.getVariable(["<", exp[1], exp[2]]);
|
|
|
|
this._dcSet.push([
|
|
(comp.eq << 2) ^ 1,
|
|
(comp.gt << 2) ^ 1,
|
|
(comp.lt << 2) ^ 1,
|
|
]);
|
|
this._dcSet.push([(comp.eq << 2) ^ 3, (comp.gt << 2) ^ 3]);
|
|
this._dcSet.push([(comp.eq << 2) ^ 3, (comp.lt << 2) ^ 3]);
|
|
this._dcSet.push([(comp.gt << 2) ^ 3, (comp.lt << 2) ^ 3]);
|
|
|
|
const type1 = typeof exp[2];
|
|
if (!["boolean", "number", "string"].includes(type1)) return;
|
|
|
|
for (const [rhs2Str, comp2] of allComps) {
|
|
if (comp2 === comp) continue;
|
|
const rhs2 = JSON.parse(rhs2Str);
|
|
const type2 = typeof rhs2;
|
|
|
|
if (!["boolean", "number", "string"].includes(type2)) continue;
|
|
let cmp = 0;
|
|
if (type1 === type2) cmp = rhs > rhs2 ? 1 : -1;
|
|
else if (type1 === "string") cmp = 1;
|
|
else if (type2 === "string") cmp = -1;
|
|
else cmp = +rhs - +rhs2;
|
|
|
|
const c1 = cmp > 0 ? comp : comp2;
|
|
const c2 = cmp > 0 ? comp2 : comp;
|
|
|
|
// This is the minimum clauses required if all relavent vars
|
|
// were included in the DC set.
|
|
// this._dcSet.push([(c1.eq << 2) ^ 3, (c2.eq << 2) ^ 3]);
|
|
// this._dcSet.push([(c1.lt << 2) ^ 1, (c2.gt << 2) ^ 1]);
|
|
|
|
// But we use non-minimal set because intermediate vars
|
|
// between any two may not be present in the DC set.
|
|
this._dcSet.push([(c1.lt << 2) ^ 1, (c2.gt << 2) ^ 1]);
|
|
this._dcSet.push([(c1.lt << 2) ^ 1, (c2.eq << 2) ^ 3]);
|
|
this._dcSet.push([(c1.lt << 2) ^ 1, (c2.lt << 2) ^ 3]);
|
|
this._dcSet.push([(c1.eq << 2) ^ 3, (c2.gt << 2) ^ 1]);
|
|
this._dcSet.push([(c1.eq << 2) ^ 3, (c2.eq << 2) ^ 3]);
|
|
this._dcSet.push([(c1.eq << 2) ^ 3, (c2.lt << 2) ^ 3]);
|
|
this._dcSet.push([(c1.gt << 2) ^ 3, (c2.gt << 2) ^ 1]);
|
|
this._dcSet.push([(c1.gt << 2) ^ 3, (c2.eq << 2) ^ 3]);
|
|
this._dcSet.push([(c1.gt << 2) ^ 3, (c2.lt << 2) ^ 3]);
|
|
}
|
|
}
|
|
|
|
getExpression(v: number): Expression {
|
|
return this._expressions.get(v);
|
|
}
|
|
|
|
getIsNullRelations(v: number): number[] {
|
|
return this._isNullRelations.get(v);
|
|
}
|
|
|
|
isIsNull(v: number): boolean {
|
|
return this._isNullVars.has(v);
|
|
}
|
|
|
|
getDcSet(minterms?: Minterm[]): number[][] {
|
|
if (!minterms) return this._dcSet;
|
|
const vars = new Set(minterms.flat().map((v) => v >> 2));
|
|
|
|
for (const comps of this._comparisons.values()) {
|
|
for (const comp of comps.values()) {
|
|
const c = Object.values(comp).filter((v) => !vars.has(v));
|
|
if (c.length === 1) vars.add(c[0]);
|
|
}
|
|
}
|
|
|
|
for (const n of this._isNullVars)
|
|
if (this._isNullRelations.get(n).some((v) => vars.has(v))) vars.add(n);
|
|
|
|
const dcSet = this._dcSet.filter((m) => m.every((v) => vars.has(v >> 2)));
|
|
|
|
return dcSet;
|
|
}
|
|
}
|
|
|
|
function sanitizeMinterms(
|
|
minterms: number[][],
|
|
context: SynthContext
|
|
): 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 isNullVars = context.getIsNullRelations(k);
|
|
const t = k << 2;
|
|
if (v === 0b0101) {
|
|
if (isNullVars.length === 1) minterm.push((isNullVars[0] << 2) ^ 3);
|
|
else perms.push(isNullVars.map((n) => (n << 2) ^ 3));
|
|
} else if (v === 0b0001) {
|
|
perms.push([...isNullVars.map((n) => (n << 2) ^ 3), t ^ 3]);
|
|
} else if (v === 0b0100) {
|
|
perms.push([...isNullVars.map((n) => (n << 2) ^ 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 = new SynthContext();
|
|
let minterms = boolExpr.true(context);
|
|
minterms = sanitizeMinterms(minterms, context);
|
|
const canRaise = getCanRaiseCallback(context);
|
|
const dcSet = context.getDcSet(minterms);
|
|
minterms = espresso(minterms, dcSet, { canRaise });
|
|
return sopToExpression(minterms, context);
|
|
}
|
|
|
|
function mapCallback(exp: Expression | BoolExprSynth): Expression {
|
|
if (!Array.isArray(exp)) return exp as Expression;
|
|
if (exp[0] === "CASE") {
|
|
exp = exp.slice();
|
|
for (let i = 1; i < exp.length; i += 2) exp[i] = toBoolExprSynth(exp[i]);
|
|
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]);
|
|
} else if (Array.isArray(exp[i]) && exp[i][0] === "CASE") {
|
|
for (let j = 2; j < exp[i].length; j += 2) {
|
|
if (exp[i][j] instanceof BoolExprSynth)
|
|
exp[i][j] = boolExprSynthToExpression(exp[i][j]);
|
|
}
|
|
}
|
|
}
|
|
return exp;
|
|
}
|
|
|
|
function getCanRaiseCallback(
|
|
context: SynthContext
|
|
): (idx: number, set: Set<number>) => boolean {
|
|
return (idx: number, set: Set<number>): boolean => {
|
|
const i = idx >> 2;
|
|
const vars = context.getIsNullRelations(i);
|
|
if (!context.isIsNull(i)) {
|
|
if (!(idx & 1)) return true;
|
|
if (!set.has(idx ^ 3)) return true;
|
|
for (const n of vars) if (set.has((n << 2) ^ 3)) return true;
|
|
for (const n of vars) if (!set.has((n << 2) ^ 2)) return false;
|
|
return true;
|
|
}
|
|
|
|
for (const k of vars) {
|
|
if (set.has((k << 2) ^ 1)) continue;
|
|
if (set.has((k << 2) ^ 3)) continue;
|
|
if (set.has((k << 2) ^ 0)) return false;
|
|
if (set.has((k << 2) ^ 2)) return false;
|
|
}
|
|
return true;
|
|
};
|
|
}
|
|
|
|
export function minimize(expr: Expression, boolean = false): Expression {
|
|
expr = normalize(expr);
|
|
expr = map(expr, mapCallback);
|
|
if (Array.isArray(expr) && expr[0] === "CASE") {
|
|
if (!boolean) {
|
|
const context = new SynthContext();
|
|
const whens = expr.filter((e, i) => i % 2).map((e) => e.true(context));
|
|
const caseDcSet: Minterm[] = [];
|
|
const canRaise = getCanRaiseCallback(context);
|
|
const res: Expression = ["CASE"];
|
|
for (let i = 1; i < expr.length; i += 2) {
|
|
let minterms = sanitizeMinterms(whens[(i - 1) / 2], context);
|
|
const dcSet = context.getDcSet(minterms.concat(caseDcSet));
|
|
minterms = espresso(minterms, dcSet, { canRaise });
|
|
if (!minterms.length) continue;
|
|
const w = sopToExpression(minterms, context);
|
|
let t = expr[i + 1];
|
|
if (t instanceof BoolExprSynth) t = boolExprSynthToExpression(t);
|
|
res.push(w, t);
|
|
if (w === true) break;
|
|
caseDcSet.push(...minterms);
|
|
}
|
|
while (res[res.length - 1] == null) res.splice(-2);
|
|
if (res.length < 3) return null;
|
|
return res;
|
|
}
|
|
expr = (toBoolExprSynth(expr) as unknown) as Expression;
|
|
}
|
|
|
|
if (boolean) expr = (toBoolExprSynth(expr) as unknown) as Expression;
|
|
|
|
if (expr instanceof BoolExprSynth) expr = 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 (Array.isArray(expr2) && expr2[0] === "CASE")
|
|
expr2 = (toBoolExprSynth(expr2) as unknown) as Expression;
|
|
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 = new SynthContext();
|
|
|
|
const expr2Minterms = b2.true(context);
|
|
const expr1Minterms = b1.true(context);
|
|
const expr1NullMinterms = b1.null(context);
|
|
const expr1FalseMinterms = b1.false(context);
|
|
|
|
const unionMinterms = sanitizeMinterms(
|
|
[...expr1Minterms, ...expr2Minterms],
|
|
context
|
|
);
|
|
|
|
const diffMinterms = sanitizeMinterms(
|
|
complement([
|
|
...complement([...expr1NullMinterms, ...expr1FalseMinterms]),
|
|
...complement(expr2Minterms),
|
|
]),
|
|
context
|
|
);
|
|
|
|
const canRaise = getCanRaiseCallback(context);
|
|
|
|
const union = espresso(unionMinterms, context.getDcSet(unionMinterms), {
|
|
canRaise,
|
|
});
|
|
|
|
const diff = espresso(diffMinterms, context.getDcSet(diffMinterms), {
|
|
canRaise,
|
|
});
|
|
|
|
return [sopToExpression(union, context), sopToExpression(diff, context)];
|
|
}
|
|
|
|
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 = new SynthContext();
|
|
const expr1Minterms = b1.true(context);
|
|
const expr2Minterms = b2.true(context);
|
|
|
|
return tautology([
|
|
...complement(expr2Minterms),
|
|
...context.getDcSet(),
|
|
...expr1Minterms,
|
|
]);
|
|
}
|