919 lines
29 KiB
TypeScript
919 lines
29 KiB
TypeScript
import { espresso, complement, tautology } from "espresso-iisojs";
|
|
import { Expression } from "../../types";
|
|
import normalize from "./normalize";
|
|
import { map, parseLikePattern } from "./parser";
|
|
|
|
type Minterm = number[];
|
|
|
|
export abstract class SynthContextBase<
|
|
T extends { toString: () => string } = unknown,
|
|
U = unknown,
|
|
> {
|
|
public variables = new Map<string, number>();
|
|
protected clauses = new Map<number, U>();
|
|
|
|
protected getVar(c: U): number {
|
|
const str = c.toString();
|
|
let idx = this.variables.get(str);
|
|
if (idx == null) {
|
|
idx = this.variables.size;
|
|
this.variables.set(str, idx);
|
|
this.clauses.set(idx, c);
|
|
}
|
|
return idx;
|
|
}
|
|
|
|
protected getClause(v: number): U {
|
|
return this.clauses.get(v);
|
|
}
|
|
|
|
abstract getMinterms(exp: T, res: true | false | null): Minterm[];
|
|
abstract getDcSet(minterms: Minterm[]): Minterm[];
|
|
// eslint-disable-next-line @typescript-eslint/no-unused-vars
|
|
canRaise(idx: number, set: Set<number>): boolean {
|
|
return true;
|
|
}
|
|
|
|
sanitizeMinterms(minterms: Minterm[]): Minterm[] {
|
|
return minterms;
|
|
}
|
|
|
|
minimize(minterms: Minterm[], dcSet: Minterm[] = []): Minterm[] {
|
|
minterms = this.sanitizeMinterms(minterms);
|
|
const canRaise = this.canRaise.bind(this);
|
|
return espresso(minterms, [...this.getDcSet(minterms), ...dcSet], {
|
|
canRaise,
|
|
});
|
|
}
|
|
}
|
|
|
|
function* findIsNullDeps(exp: Expression): IterableIterator<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") {
|
|
yield* findIsNullDeps(exp[2]);
|
|
} else if (exp[1] === "ROUND") {
|
|
for (const e of exp.slice(2, 4)) yield* findIsNullDeps(e);
|
|
return;
|
|
}
|
|
} else if (op !== "PARAM") {
|
|
for (const e of exp.slice(1)) yield* findIsNullDeps(e);
|
|
return;
|
|
}
|
|
yield exp;
|
|
}
|
|
|
|
export abstract class Clause {
|
|
private _isNullable: Set<string>;
|
|
protected _expression: Expression;
|
|
abstract true(context: SynthContextBase<Clause>): Minterm[];
|
|
abstract false(context: SynthContextBase<Clause>): Minterm[];
|
|
abstract null(context: SynthContextBase<Clause>): Minterm[];
|
|
expression(): Expression {
|
|
if (this._expression !== undefined) return this._expression;
|
|
const context = createSynthContext();
|
|
const minterms = this.true(context);
|
|
const minimized = context.minimize(minterms);
|
|
this._expression = context.toExpression(minimized) as Expression;
|
|
return this._expression;
|
|
}
|
|
isBoolean(): boolean {
|
|
return true;
|
|
}
|
|
isNullable(c: Clause.IsNull): boolean {
|
|
if (!this._isNullable) {
|
|
this._isNullable = new Set(
|
|
[...this.getNullables()].map((n) => n.toString()),
|
|
);
|
|
}
|
|
return this._isNullable.has(c.toString());
|
|
}
|
|
*getNullables(): IterableIterator<Clause.IsNull> {
|
|
const exp = this.expression();
|
|
for (const e of findIsNullDeps(exp)) {
|
|
if (e === exp) yield new Clause.IsNull(this);
|
|
else yield new Clause.IsNull(new Clause.Exp(e));
|
|
}
|
|
}
|
|
toString(): string {
|
|
return JSON.stringify(this.expression());
|
|
}
|
|
}
|
|
|
|
// eslint-disable-next-line @typescript-eslint/no-namespace
|
|
export namespace Clause {
|
|
export class Not extends Clause {
|
|
constructor(public operand: Clause) {
|
|
super();
|
|
}
|
|
true(context: SynthContextBase<Clause>): Minterm[] {
|
|
return this.operand.false(context);
|
|
}
|
|
false(context: SynthContextBase<Clause>): Minterm[] {
|
|
return this.operand.true(context);
|
|
}
|
|
null(context: SynthContextBase<Clause>): Minterm[] {
|
|
return this.operand.null(context);
|
|
}
|
|
}
|
|
|
|
export class Or extends Clause {
|
|
constructor(public operands: Clause[]) {
|
|
super();
|
|
}
|
|
true(context: SynthContextBase<Clause>): Minterm[] {
|
|
const minterms: Minterm[] = [];
|
|
for (const s of this.operands) {
|
|
const m = s.true(context);
|
|
if (m.length === 1 && !m[0].length) return [[]];
|
|
minterms.push(...m);
|
|
}
|
|
return minterms;
|
|
}
|
|
false(context: SynthContextBase<Clause>): Minterm[] {
|
|
const minterms: Minterm[][] = [];
|
|
const operands = [...this.operands];
|
|
for (const e of operands) {
|
|
if (e instanceof Or) {
|
|
operands.push(...e.operands);
|
|
continue;
|
|
}
|
|
const m = e.false(context);
|
|
if (!m.length) return [];
|
|
minterms.push(m);
|
|
}
|
|
if (!minterms.length) return [[]];
|
|
if (minterms.length === 1) return minterms[0];
|
|
return complement(minterms.map((m) => complement(m)).flat());
|
|
}
|
|
null(context: SynthContextBase<Clause>): Minterm[] {
|
|
const trueMinterms: Minterm[] = [];
|
|
const operands = [...this.operands];
|
|
for (const s of operands) {
|
|
if (s instanceof Or) {
|
|
operands.push(...s.operands);
|
|
continue;
|
|
}
|
|
const t = s.true(context);
|
|
if (t.length === 1 && !t[0].length) return [];
|
|
trueMinterms.push(...t);
|
|
}
|
|
|
|
const nullMinterms: Minterm[] = [];
|
|
for (const s of operands) {
|
|
const n = s.null(context);
|
|
if (n.length === 1 && !n[0].length && !trueMinterms.length) return [[]];
|
|
nullMinterms.push(...n);
|
|
}
|
|
|
|
if (!trueMinterms.length) return nullMinterms;
|
|
return complement([...complement(nullMinterms), ...trueMinterms]);
|
|
}
|
|
}
|
|
|
|
export class And extends Clause {
|
|
constructor(public operands: Clause[]) {
|
|
super();
|
|
}
|
|
true(context: SynthContextBase<Clause>): Minterm[] {
|
|
const minterms: Minterm[][] = [];
|
|
const operands = [...this.operands];
|
|
for (const s of operands) {
|
|
if (s instanceof And) {
|
|
operands.push(...s.operands);
|
|
continue;
|
|
}
|
|
const m = s.true(context);
|
|
if (!m.length) return [];
|
|
if (m.length === 1 && !m[0].length) continue;
|
|
minterms.push(m);
|
|
}
|
|
if (!minterms.length) return [[]];
|
|
if (minterms.length === 1) return minterms[0];
|
|
return complement(minterms.map((m) => complement(m)).flat());
|
|
}
|
|
false(context: SynthContextBase<Clause>): Minterm[] {
|
|
const minterms: Minterm[] = [];
|
|
for (const s of this.operands) {
|
|
const m = s.false(context);
|
|
if (m.length === 1 && !m[0].length) return [[]];
|
|
minterms.push(...m);
|
|
}
|
|
return minterms;
|
|
}
|
|
null(context: SynthContextBase<Clause>): Minterm[] {
|
|
const falseMinterms: Minterm[] = [];
|
|
const operands = [...this.operands];
|
|
for (const s of operands) {
|
|
if (s instanceof And) {
|
|
operands.push(...s.operands);
|
|
continue;
|
|
}
|
|
const f = s.false(context);
|
|
if (f.length === 1 && !f[0].length) return [];
|
|
falseMinterms.push(...f);
|
|
}
|
|
|
|
const nullMinterms: Minterm[] = [];
|
|
for (const s of operands) {
|
|
const n = s.null(context);
|
|
if (n.length === 1 && !n[0].length && !falseMinterms.length)
|
|
return [[]];
|
|
nullMinterms.push(...n);
|
|
}
|
|
|
|
if (!falseMinterms.length) return nullMinterms;
|
|
return complement([...complement(nullMinterms), ...falseMinterms]);
|
|
}
|
|
}
|
|
|
|
export class Case extends Clause {
|
|
constructor(public clauses: Clause[]) {
|
|
super();
|
|
}
|
|
true(context: SynthContextBase<Clause>): Minterm[] {
|
|
const minterms: Minterm[] = [];
|
|
const cumulative: Minterm[] = [];
|
|
for (let i = 0; i < this.clauses.length; i += 2) {
|
|
const w = this.clauses[i].true(context);
|
|
const t = this.clauses[i + 1].true(context);
|
|
minterms.push(
|
|
...complement([...cumulative, ...complement(w), ...complement(t)]),
|
|
);
|
|
if (i < this.clauses.length - 2) {
|
|
cumulative.push(
|
|
...complement([
|
|
...this.clauses[i].false(context),
|
|
...this.clauses[i].null(context),
|
|
]),
|
|
);
|
|
}
|
|
}
|
|
return minterms;
|
|
}
|
|
false(context: SynthContextBase<Clause>): Minterm[] {
|
|
const minterms: Minterm[] = [];
|
|
const cumulative: Minterm[] = [];
|
|
for (let i = 0; i < this.clauses.length; i += 2) {
|
|
const w = this.clauses[i].true(context);
|
|
const t = this.clauses[i + 1].false(context);
|
|
minterms.push(
|
|
...complement([...cumulative, ...complement(w), ...complement(t)]),
|
|
);
|
|
if (i < this.clauses.length - 2) {
|
|
cumulative.push(
|
|
...complement([
|
|
...this.clauses[i].false(context),
|
|
...this.clauses[i].null(context),
|
|
]),
|
|
);
|
|
}
|
|
}
|
|
return minterms;
|
|
}
|
|
null(context: SynthContextBase<Clause>): Minterm[] {
|
|
const minterms: Minterm[] = [];
|
|
const cumulative: Minterm[] = [];
|
|
for (let i = 0; i < this.clauses.length; i += 2) {
|
|
const w = this.clauses[i].true(context);
|
|
const t = this.clauses[i + 1].null(context);
|
|
minterms.push(
|
|
...complement([...cumulative, ...complement(w), ...complement(t)]),
|
|
);
|
|
cumulative.push(
|
|
...complement([
|
|
...this.clauses[i].false(context),
|
|
...this.clauses[i].null(context),
|
|
]),
|
|
);
|
|
}
|
|
minterms.push(...complement([...cumulative]));
|
|
return minterms;
|
|
}
|
|
expression(): Expression {
|
|
if (this._expression != null) return this._expression;
|
|
if (this.isBoolean()) {
|
|
this._expression = new Clause.Not(new Clause.Not(this)).expression();
|
|
return this._expression;
|
|
}
|
|
const context = createSynthContext();
|
|
const cases: { when: Minterm[]; then: Expression }[] = [];
|
|
for (let i = 0; i < this.clauses.length; i += 2) {
|
|
let minterms = this.clauses[i].true(context);
|
|
const then = this.clauses[i + 1].expression();
|
|
if (
|
|
cases.length &&
|
|
JSON.stringify(then) === JSON.stringify(cases[cases.length - 1].then)
|
|
)
|
|
minterms.push(...cases.pop().when);
|
|
minterms = context.minimize(
|
|
minterms,
|
|
cases.flatMap((c) => c.when),
|
|
);
|
|
if (!minterms.length) continue;
|
|
cases.push({ when: minterms, then });
|
|
if (minterms.length === 1 && !minterms[0].length) break;
|
|
}
|
|
while (cases[cases.length - 1].then == null) cases.pop();
|
|
if (!cases.length) return null;
|
|
this._expression = [
|
|
"CASE",
|
|
...cases.flatMap((c) => [context.toExpression(c.when), c.then]),
|
|
];
|
|
return this._expression;
|
|
}
|
|
|
|
isBoolean(): boolean {
|
|
for (let i = 1; i < this.clauses.length; i += 2)
|
|
if (!this.clauses[i].isBoolean()) return false;
|
|
return true;
|
|
}
|
|
}
|
|
|
|
export class IsNull extends Clause {
|
|
private _boolean: Clause;
|
|
constructor(public operand: Clause) {
|
|
super();
|
|
this._boolean = new Not(new Not(this));
|
|
}
|
|
true(context: SynthContextBase<Clause>): Minterm[] {
|
|
return this.operand.null(context);
|
|
}
|
|
false(context: SynthContextBase<Clause>): Minterm[] {
|
|
return complement(this.true(context));
|
|
}
|
|
null(): Minterm[] {
|
|
return [];
|
|
}
|
|
isBoolean(): boolean {
|
|
return true;
|
|
}
|
|
*getNullables(): IterableIterator<IsNull> {
|
|
// Never returns null
|
|
}
|
|
expression(): Expression {
|
|
const nullables = [...this.operand.getNullables()];
|
|
if (nullables.length === 1 && nullables[0].operand === this.operand)
|
|
return ["IS NULL", this.operand.expression()];
|
|
return super.expression();
|
|
}
|
|
}
|
|
|
|
export class Exp extends Clause {
|
|
constructor(public exp: Expression) {
|
|
super();
|
|
}
|
|
true(context: SynthContextBase<Clause>): Minterm[] {
|
|
if (Array.isArray(this.exp)) return context.getMinterms(this, true);
|
|
if (this.exp) return [[]];
|
|
return [];
|
|
}
|
|
false(context: SynthContextBase<Clause>): Minterm[] {
|
|
if (Array.isArray(this.exp)) return context.getMinterms(this, false);
|
|
if (!this.exp && this.exp != null) return [[]];
|
|
return [];
|
|
}
|
|
null(context: SynthContextBase<Clause>): Minterm[] {
|
|
if (Array.isArray(this.exp)) return context.getMinterms(this, null);
|
|
if (this.exp == null) return [[]];
|
|
return [];
|
|
}
|
|
expression(): Expression {
|
|
return this.exp;
|
|
}
|
|
isBoolean(): boolean {
|
|
return this.exp === true || this.exp === false || this.exp == null;
|
|
}
|
|
}
|
|
|
|
export class Compare extends Clause {
|
|
constructor(
|
|
public lhs: Clause,
|
|
public op: ">" | "<" | "=",
|
|
public rhs: boolean | number | string,
|
|
) {
|
|
super();
|
|
}
|
|
true(context: SynthContextBase<Clause>): Minterm[] {
|
|
return context.getMinterms(this, true);
|
|
}
|
|
false(context: SynthContextBase<Clause>): Minterm[] {
|
|
return context.getMinterms(this, false);
|
|
}
|
|
null(context: SynthContextBase<Clause>): Minterm[] {
|
|
return this.lhs.null(context);
|
|
}
|
|
*getNullables(): IterableIterator<IsNull> {
|
|
yield* this.lhs.getNullables();
|
|
}
|
|
isBoolean(): boolean {
|
|
return true;
|
|
}
|
|
expression(): Expression {
|
|
return [this.op, this.lhs.expression(), this.rhs];
|
|
}
|
|
}
|
|
|
|
export class Like extends Clause {
|
|
public readonly caseSensitive: boolean;
|
|
public readonly contradiction: boolean;
|
|
public readonly pattern: string[];
|
|
public readonly lhs: Clause;
|
|
|
|
constructor(
|
|
lhs: Clause,
|
|
public rhs: string,
|
|
public esc?: string,
|
|
) {
|
|
super();
|
|
const exp = lhs.expression();
|
|
let caseSensitive = true;
|
|
let contradiction = false;
|
|
if (Array.isArray(exp)) {
|
|
if (exp[0] === "FUNC") {
|
|
const func = exp[1];
|
|
if (func === "UPPER" || func === "LOWER") {
|
|
const p = func === "UPPER" ? rhs.toUpperCase() : rhs.toLowerCase();
|
|
if (p === rhs) caseSensitive = false;
|
|
else contradiction = true;
|
|
lhs = new Exp(exp[2]);
|
|
}
|
|
}
|
|
}
|
|
this.lhs = lhs;
|
|
this.pattern = parseLikePattern(rhs, esc);
|
|
this.caseSensitive = caseSensitive;
|
|
this.contradiction = contradiction;
|
|
}
|
|
true(context: SynthContextBase<Clause>): Minterm[] {
|
|
return context.getMinterms(this, true);
|
|
}
|
|
false(context: SynthContextBase<Clause>): Minterm[] {
|
|
return context.getMinterms(this, false);
|
|
}
|
|
null(context: SynthContextBase<Clause>): Minterm[] {
|
|
return this.lhs.null(context);
|
|
}
|
|
isBoolean(): boolean {
|
|
return true;
|
|
}
|
|
isNullable(c: IsNull): boolean {
|
|
return this.lhs.isNullable(c);
|
|
}
|
|
getNullables(): IterableIterator<IsNull> {
|
|
return this.lhs.getNullables();
|
|
}
|
|
expression(): Expression {
|
|
let lhs = this.lhs.expression();
|
|
if (this.contradiction) {
|
|
if (this.rhs === this.rhs.toLocaleUpperCase())
|
|
lhs = ["FUNC", "LOWER", lhs];
|
|
else lhs = ["FUNC", "UPPER", lhs];
|
|
} else if (!this.caseSensitive) {
|
|
if (this.rhs === this.rhs.toLocaleUpperCase())
|
|
lhs = ["FUNC", "UPPER", lhs];
|
|
else lhs = ["FUNC", "LOWER", lhs];
|
|
}
|
|
return ["LIKE", lhs, this.rhs, ...(this.esc ? [this.esc] : [])];
|
|
}
|
|
}
|
|
|
|
export function fromExpression(exp: Expression): Clause {
|
|
const res = map(exp, (e) => {
|
|
if (!Array.isArray(e)) return new Clause.Exp(e);
|
|
let op = e[0];
|
|
let negate = true;
|
|
if (op === "NOT LIKE") op = "LIKE";
|
|
else if (op === "IS NOT NULL") op = "IS NULL";
|
|
else if (op === "<>") op = "=";
|
|
else if (op === ">=") op = "<";
|
|
else if (op === "<=") op = ">";
|
|
else negate = false;
|
|
|
|
let clause: Clause;
|
|
if (op === "IS NULL") {
|
|
clause = new Clause.IsNull(e[1]);
|
|
} else if (op === "NOT") {
|
|
clause = new Clause.Not(e[1]);
|
|
} else if (op === "OR") {
|
|
clause = new Clause.Or(e.slice(1));
|
|
} else if (op === "AND") {
|
|
clause = new Clause.And(e.slice(1));
|
|
} else if (op === "CASE") {
|
|
clause = new Clause.Case(e.slice(1));
|
|
} else if (op === "LIKE") {
|
|
const rhs = e[2] instanceof Exp ? e[2].expression() : null;
|
|
const esc = e[3] instanceof Exp ? e[3].expression() : null;
|
|
if (typeof rhs === "string" && typeof esc === "string")
|
|
clause = new Clause.Like(e[1], rhs, esc);
|
|
else if (typeof rhs === "string" && esc == null)
|
|
clause = new Clause.Like(e[1], rhs);
|
|
} else if (op === ">" || op === "<" || op === "=") {
|
|
const rhs = e[2] instanceof Exp ? e[2].expression() : null;
|
|
if (["boolean", "number", "string"].includes(typeof rhs)) {
|
|
clause = new Clause.Compare(
|
|
e[1],
|
|
op,
|
|
rhs as boolean | number | string,
|
|
);
|
|
}
|
|
}
|
|
|
|
if (!clause) {
|
|
const args = e.slice(1).map((a) => (a as Clause).expression());
|
|
clause = new Clause.Exp([op, ...args]);
|
|
}
|
|
|
|
if (negate) clause = new Clause.Not(clause);
|
|
return clause;
|
|
});
|
|
|
|
return res;
|
|
}
|
|
}
|
|
|
|
function groupBy<T, K>(
|
|
input: T[],
|
|
callback: (item: T) => K,
|
|
): Iterable<[K, T[]]> {
|
|
const groups = new Map<K, T[]>();
|
|
for (const item of input) {
|
|
const key = callback(item);
|
|
let arr = groups.get(key);
|
|
if (!arr) groups.set(key, (arr = []));
|
|
arr.push(item);
|
|
}
|
|
|
|
return groups.entries();
|
|
}
|
|
|
|
export class SynthContext extends SynthContextBase<Clause, Clause> {
|
|
constructor() {
|
|
super();
|
|
}
|
|
|
|
getMinterms(clause: Clause, res: true | false | null): number[][] {
|
|
const v = this.getVar(clause);
|
|
if (res === true) return [[(v << 2) ^ 3]];
|
|
else if (res === false) return [[(v << 2) ^ 1]];
|
|
else return [[v << 2, (v << 2) ^ 2]];
|
|
}
|
|
|
|
getDcSet(minterms: Minterm[]): number[][] {
|
|
const dcSet: number[][] = [];
|
|
|
|
const whitelist = new Set([...minterms.flat()].map((v) => v >> 2));
|
|
|
|
const allClauses = [...whitelist].map((v) => this.getClause(v));
|
|
const comparisons = allClauses.filter(
|
|
(c) => c instanceof Clause.Compare,
|
|
) as Clause.Compare[];
|
|
|
|
// Comparisons
|
|
for (const [, clauses] of groupBy(comparisons, (c) =>
|
|
JSON.stringify(c.lhs),
|
|
)) {
|
|
const lhs = clauses[0].lhs;
|
|
const values = new Set(clauses.map((c) => c.rhs));
|
|
const valuesSorted = [...values].sort((a, b) => {
|
|
const ta = typeof a;
|
|
const tb = typeof b;
|
|
if (ta === tb) return a > b ? 1 : -1;
|
|
else if (ta === "string") return 1;
|
|
else if (tb === "string") return -1;
|
|
return +a - +b;
|
|
});
|
|
|
|
for (const [i, v] of valuesSorted.entries()) {
|
|
const eq = this.getVar(new Clause.Compare(lhs, "=", v));
|
|
const gt = this.getVar(new Clause.Compare(lhs, ">", v));
|
|
const lt = this.getVar(new Clause.Compare(lhs, "<", v));
|
|
|
|
dcSet.push([(eq << 2) ^ 3, (gt << 2) ^ 3]);
|
|
dcSet.push([(lt << 2) ^ 3, (gt << 2) ^ 3]);
|
|
dcSet.push([(lt << 2) ^ 3, (eq << 2) ^ 3]);
|
|
dcSet.push([(lt << 2) ^ 1, (eq << 2) ^ 1, (gt << 2) ^ 1]);
|
|
|
|
const negEquivOp = [lt, eq, gt].filter((o) => !whitelist.has(o));
|
|
if (negEquivOp.length === 1) whitelist.add(negEquivOp[0]);
|
|
|
|
for (let j = 0; j < i; j++) {
|
|
const eq2 = this.getVar(
|
|
new Clause.Compare(lhs, "=", valuesSorted[j]),
|
|
);
|
|
const gt2 = this.getVar(
|
|
new Clause.Compare(lhs, ">", valuesSorted[j]),
|
|
);
|
|
const lt2 = this.getVar(
|
|
new Clause.Compare(lhs, "<", valuesSorted[j]),
|
|
);
|
|
|
|
// This is the minimum clauses required if all relavent vars
|
|
// were included in the DC set.
|
|
// dcSet.push([(eq << 2) ^ 3, (eq2 << 2) ^ 3]);
|
|
// dcSet.push([(lt << 2) ^ 1, (gt2 << 2) ^ 1]);
|
|
|
|
// But we use non-minimal set because intermediate vars
|
|
// between any two may not be present in the DC set.
|
|
dcSet.push([(gt2 << 2) ^ 1, (lt << 2) ^ 1]);
|
|
dcSet.push([(eq2 << 2) ^ 3, (lt << 2) ^ 1]);
|
|
dcSet.push([(lt2 << 2) ^ 3, (lt << 2) ^ 1]);
|
|
dcSet.push([(gt2 << 2) ^ 1, (gt << 2) ^ 3]);
|
|
dcSet.push([(gt2 << 2) ^ 1, (eq << 2) ^ 3]);
|
|
dcSet.push([(eq2 << 2) ^ 3, (gt << 2) ^ 3]);
|
|
dcSet.push([(eq2 << 2) ^ 3, (eq << 2) ^ 3]);
|
|
dcSet.push([(lt2 << 2) ^ 3, (gt << 2) ^ 3]);
|
|
dcSet.push([(lt2 << 2) ^ 3, (eq << 2) ^ 3]);
|
|
}
|
|
}
|
|
}
|
|
|
|
// LIKE
|
|
const likes = allClauses.filter(
|
|
(c) => c instanceof Clause.Like,
|
|
) as Clause.Like[];
|
|
|
|
for (const [, clauses] of groupBy(likes, (c) => JSON.stringify(c.lhs))) {
|
|
for (let i1 = 0; i1 < clauses.length; ++i1) {
|
|
const l1 = clauses[i1];
|
|
if (l1.contradiction) {
|
|
dcSet.push([(this.getVar(l1) << 2) ^ 3]);
|
|
continue;
|
|
}
|
|
for (let i2 = i1 + 1; i2 < clauses.length; ++i2) {
|
|
const l2 = clauses[i2];
|
|
if (l2.contradiction) continue;
|
|
let p1 = l1.pattern;
|
|
let p2 = l2.pattern;
|
|
if (!l1.caseSensitive || !l2.caseSensitive) {
|
|
p1 = p1.map((c) => c.toLowerCase());
|
|
p2 = p2.map((c) => c.toLowerCase());
|
|
}
|
|
if (likeDisjoint(p1, p2)) {
|
|
dcSet.push([
|
|
(this.getVar(l1) << 2) ^ 3,
|
|
(this.getVar(l2) << 2) ^ 3,
|
|
]);
|
|
} else if (
|
|
(!l1.caseSensitive || l2.caseSensitive) &&
|
|
likeImplies(p1, p2)
|
|
) {
|
|
dcSet.push([
|
|
(this.getVar(l1) << 2) ^ 2,
|
|
(this.getVar(l2) << 2) ^ 3,
|
|
]);
|
|
dcSet.push([
|
|
(this.getVar(l1) << 2) ^ 1,
|
|
(this.getVar(l2) << 2) ^ 0,
|
|
]);
|
|
} else if (
|
|
(!l2.caseSensitive || l1.caseSensitive) &&
|
|
likeImplies(p2, p1)
|
|
) {
|
|
dcSet.push([
|
|
(this.getVar(l1) << 2) ^ 3,
|
|
(this.getVar(l2) << 2) ^ 2,
|
|
]);
|
|
dcSet.push([
|
|
(this.getVar(l1) << 2) ^ 0,
|
|
(this.getVar(l2) << 2) ^ 1,
|
|
]);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
for (const v of whitelist) {
|
|
const clause = this.getClause(v);
|
|
const nullables = [...clause.getNullables()].map((c) => this.getVar(c));
|
|
if (nullables.length) {
|
|
dcSet.push([
|
|
...nullables.map((n) => (n << 2) ^ 2),
|
|
(v << 2) ^ 0,
|
|
(v << 2) ^ 2,
|
|
]);
|
|
for (const n of nullables) {
|
|
dcSet.push([(n << 2) ^ 3, (v << 2) ^ 1]);
|
|
dcSet.push([(n << 2) ^ 3, (v << 2) ^ 3]);
|
|
whitelist.add(n);
|
|
}
|
|
}
|
|
|
|
if (clause instanceof Clause.IsNull) {
|
|
const str = clause.operand.toString();
|
|
if (str === '["PARAM","DeviceID.ID"]' || str === '["PARAM","_id"]')
|
|
dcSet.push([(v << 2) ^ 3]);
|
|
}
|
|
}
|
|
return dcSet.filter((m) => m.every((v) => whitelist.has(v >> 2)));
|
|
}
|
|
|
|
canRaise(idx: number, set: Set<number>): boolean {
|
|
const clause = this.getClause(idx >> 2);
|
|
if (clause instanceof Clause.IsNull) {
|
|
for (const i of set) {
|
|
if (i === idx || i & 1) continue;
|
|
const c = this.getClause(i >> 2);
|
|
if (c.isNullable(clause)) return false;
|
|
}
|
|
return true;
|
|
}
|
|
return !(idx & 1) || !set.has(idx ^ 3);
|
|
}
|
|
|
|
sanitizeMinterms(minterms: Minterm[]): Minterm[] {
|
|
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 = [...this.clauses.get(k).getNullables()].map((c) =>
|
|
this.getVar(c),
|
|
);
|
|
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;
|
|
}
|
|
|
|
toExpression(sop: number[][]): 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 = this.getClause(i >>> 2).expression() as Expression;
|
|
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];
|
|
}
|
|
conjs.push(expr);
|
|
}
|
|
if (conjs.length > 1) res.push(["AND", ...conjs]);
|
|
else res.push(conjs[0]);
|
|
}
|
|
if (res.length > 1) return ["OR", ...res];
|
|
return res[0];
|
|
}
|
|
}
|
|
|
|
// Classes aren't hoisted in JS but functions are. This function is used to
|
|
// create a new SynthContext instance from inside the Clause class.
|
|
export function createSynthContext(): SynthContext {
|
|
return new SynthContext();
|
|
}
|
|
|
|
export function likeImplies(pat1: string[], pat2: string[]): boolean {
|
|
let backtrack: [number, number] = null;
|
|
|
|
for (let i1 = 0, i2 = 0; ; ++i1, ++i2) {
|
|
while (i1 < pat1.length && pat1[i1] === "\\%") backtrack = [i1++, i2];
|
|
|
|
if (i2 >= pat2.length) return i1 >= pat1.length;
|
|
|
|
const c = i1 < pat1.length ? pat1[i1] : null;
|
|
|
|
if (c !== pat2[i2] && c !== "\\_") {
|
|
if (!backtrack) return false;
|
|
[i1, i2] = backtrack;
|
|
++backtrack[1];
|
|
}
|
|
}
|
|
}
|
|
|
|
export function likeDisjoint(pat1: string[], pat2: string[]): boolean {
|
|
const left1Idx = pat1.indexOf("\\%");
|
|
const left2Idx = pat2.indexOf("\\%");
|
|
const right1Idx = pat1.lastIndexOf("\\%");
|
|
const right2Idx = pat2.lastIndexOf("\\%");
|
|
|
|
const left1 = pat1.slice(0, left1Idx !== -1 ? left1Idx : pat1.length);
|
|
const left2 = pat2.slice(0, left2Idx !== -1 ? left2Idx : pat2.length);
|
|
const right1 = pat1.slice(right1Idx !== -1 ? right1Idx + 1 : 0).reverse();
|
|
const right2 = pat2.slice(right2Idx !== -1 ? right2Idx + 1 : 0).reverse();
|
|
|
|
for (let i = 0; i < Math.min(left1.length, left2.length); ++i) {
|
|
if (left1[i] !== left2[i] && left1[i] !== "\\_" && left2[i] !== "\\_")
|
|
return true;
|
|
}
|
|
|
|
for (let i = 0; i < Math.min(right1.length, right2.length); ++i) {
|
|
if (right1[i] !== right2[i] && right1[i] !== "\\_" && right2[i] !== "\\_")
|
|
return true;
|
|
}
|
|
|
|
if (pat1.length === left1.length)
|
|
return pat2.filter((c) => c !== "\\%").length > pat1.length;
|
|
else if (pat2.length === left2.length)
|
|
return pat1.filter((c) => c !== "\\%").length > pat2.length;
|
|
|
|
return false;
|
|
}
|
|
|
|
export function minimize(expr: Expression, boolean = false): Expression {
|
|
let synth = Clause.fromExpression(normalize(expr));
|
|
if (boolean) synth = new Clause.Not(new Clause.Not(synth));
|
|
return synth.expression();
|
|
}
|
|
|
|
export function unionDiff(
|
|
expr1: Expression,
|
|
expr2: Expression,
|
|
): [Expression, Expression] {
|
|
expr2 = normalize(expr2);
|
|
|
|
if (!expr2) return [expr1, false];
|
|
|
|
const synth2 = Clause.fromExpression(expr2);
|
|
|
|
if (!expr1) {
|
|
const e = synth2.expression();
|
|
return [e, e];
|
|
}
|
|
|
|
expr1 = normalize(expr1);
|
|
const synth1 = Clause.fromExpression(expr1);
|
|
|
|
const context = new SynthContext();
|
|
|
|
const expr2Minterms = synth2.true(context);
|
|
const expr1Minterms = synth1.true(context);
|
|
const expr1NullMinterms = synth1.null(context);
|
|
const expr1FalseMinterms = synth1.false(context);
|
|
|
|
const union = context.minimize([...expr1Minterms, ...expr2Minterms]);
|
|
|
|
const diff = context.minimize(
|
|
complement([
|
|
...complement([...expr1NullMinterms, ...expr1FalseMinterms]),
|
|
...complement(expr2Minterms),
|
|
]),
|
|
);
|
|
|
|
return [context.toExpression(union), context.toExpression(diff)];
|
|
}
|
|
|
|
export function covers(expr1: Expression, expr2: Expression): boolean {
|
|
expr2 = normalize(expr2);
|
|
if (!expr2) return true;
|
|
expr1 = normalize(expr1);
|
|
if (!Array.isArray(expr1)) return !!expr1;
|
|
|
|
const synt1 = Clause.fromExpression(expr1);
|
|
const synt2 = Clause.fromExpression(expr2);
|
|
|
|
const context = new SynthContext();
|
|
const expr1Minterms = synt1.true(context);
|
|
const expr2Minterms = synt2.true(context);
|
|
|
|
return tautology([
|
|
...complement(expr2Minterms),
|
|
...context.getDcSet([...expr2Minterms, ...expr1Minterms]),
|
|
...expr1Minterms,
|
|
]);
|
|
}
|