Zaid Humaimidi
6f3ce6f7c8
Replace the old Lisp-like array expression representation (["AND", ["PARAM", ...], ...]) with a class hierarchy rooted in an abstract Expression class (Literal, Parameter, Binary, Unary, FunctionCall, Conditional). This gives compile-time type safety to expression construction, evaluation, and pattern matching. Key changes: - New lib/common/expression.ts defines the class hierarchy with map/evaluate/toString methods - Rewrite parser as hand-rolled recursive descent, removing the parsimmon dependency - Extend Path with a colon separator to unify parameter identity and attributes into a single address space (e.g. "Device.WiFi.SSID.1.Name:writable"). The colon field tracks how many trailing segments are attribute qualifiers. PathSet rewritten with separate param/attr segment indexes - Flatten device attribute representation in the UI to colon-delimited keys mirroring the new path syntax
894 lines
28 KiB
TypeScript
894 lines
28 KiB
TypeScript
import { espresso, complement, tautology } from "espresso-iisojs";
|
|
import Expression from "../expression.ts";
|
|
import { parseLikePattern } from "./parser.ts";
|
|
import normalize from "./normalize.ts";
|
|
|
|
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>();
|
|
|
|
public 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;
|
|
}
|
|
|
|
public getClause(v: number): U {
|
|
return this.clauses.get(v);
|
|
}
|
|
|
|
abstract getMinterms(exp: T, res: number): Minterm[];
|
|
abstract getDcSet(minterms: Minterm[]): Minterm[];
|
|
// eslint-disable-next-line @typescript-eslint/no-unused-vars
|
|
canRaise(idx: number, set: Set<number>): boolean {
|
|
return true;
|
|
}
|
|
|
|
// eslint-disable-next-line @typescript-eslint/no-unused-vars
|
|
canLower(idx: number, set: Set<number>): boolean {
|
|
return true;
|
|
}
|
|
|
|
bias(a: number, b: number): number {
|
|
// Bias towards 1 then lower index
|
|
return (b ^ 1) - (a ^ 1);
|
|
}
|
|
|
|
sanitizeMinterms(minterms: Minterm[]): Minterm[] {
|
|
return minterms;
|
|
}
|
|
|
|
minimize(minterms: Minterm[], dcSet: Minterm[] = []): Minterm[] {
|
|
minterms = this.sanitizeMinterms(minterms);
|
|
const canRaise = this.canRaise.bind(this);
|
|
const canLower = this.canLower.bind(this);
|
|
const bias = this.bias.bind(this);
|
|
|
|
return espresso(
|
|
minterms,
|
|
[...this.getDcSet([...minterms, ...dcSet]), ...dcSet],
|
|
{
|
|
canRaise,
|
|
canLower,
|
|
bias,
|
|
},
|
|
);
|
|
}
|
|
}
|
|
|
|
function* findIsNullDeps(exp: Expression): IterableIterator<Expression> {
|
|
if (exp instanceof Expression.Literal) return;
|
|
else if (exp instanceof Expression.Unary) {
|
|
if (exp.operator === "IS NULL" || exp.operator === "IS NOT NULL") return;
|
|
yield* findIsNullDeps(exp.operand);
|
|
} else if (exp instanceof Expression.Binary) {
|
|
yield* findIsNullDeps(exp.left);
|
|
yield* findIsNullDeps(exp.right);
|
|
} else if (exp instanceof Expression.FunctionCall) {
|
|
if (exp.name === "NOW") return;
|
|
else if (exp.name === "LOWER" || exp.name === "UPPER")
|
|
yield* findIsNullDeps(exp.args[0]);
|
|
else if (exp.name === "ROUND") {
|
|
for (const e of exp.args.slice(0, 2)) yield* findIsNullDeps(e);
|
|
}
|
|
} else yield exp;
|
|
}
|
|
|
|
export abstract class Clause {
|
|
private _isNullable: Set<string>;
|
|
protected _expression: Expression;
|
|
abstract getMinterms(
|
|
context: SynthContextBase<Clause>,
|
|
res: number,
|
|
): Minterm[];
|
|
expression(): Expression {
|
|
if (this._expression !== undefined) return this._expression;
|
|
const context = createSynthContext();
|
|
const minterms = this.getMinterms(context, 0b100);
|
|
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 this.expression().toString();
|
|
}
|
|
}
|
|
|
|
// eslint-disable-next-line @typescript-eslint/no-namespace
|
|
export namespace Clause {
|
|
export class Not extends Clause {
|
|
constructor(public operand: Clause) {
|
|
super();
|
|
}
|
|
getMinterms(context: SynthContextBase<Clause>, res: number): Minterm[] {
|
|
let r = res & 0b001;
|
|
if (res & 0b010) r |= 0b100;
|
|
if (res & 0b100) r |= 0b010;
|
|
return this.operand.getMinterms(context, r);
|
|
}
|
|
}
|
|
|
|
export class And extends Clause {
|
|
constructor(public operands: Clause[]) {
|
|
super();
|
|
}
|
|
getMinterms(context: SynthContextBase<Clause>, res: number): Minterm[] {
|
|
res = res & 0b111;
|
|
if (!res) return [];
|
|
if (res === 0b111) return [[]];
|
|
|
|
if (res === 0b110)
|
|
return [
|
|
...this.getMinterms(context, 0b010),
|
|
...this.getMinterms(context, 0b100),
|
|
];
|
|
|
|
if (!(res & 0b010)) return complement(this.getMinterms(context, ~res));
|
|
|
|
const minterms: Minterm[] = [];
|
|
for (const o of this.operands) {
|
|
const m = o.getMinterms(context, res);
|
|
if (m.length === 1 && !m[0].length) return [[]];
|
|
minterms.push(...m);
|
|
}
|
|
|
|
return minterms;
|
|
}
|
|
}
|
|
|
|
export class IsNull extends Clause {
|
|
constructor(public operand: Clause) {
|
|
super();
|
|
}
|
|
getMinterms(context: SynthContextBase<Clause>, res: number): Minterm[] {
|
|
res = res & 0b111;
|
|
const minterms: Minterm[] = [];
|
|
if ((res & 0b110) === 0b110) return [[]];
|
|
if (res & 0b100)
|
|
minterms.push(...this.operand.getMinterms(context, 0b001));
|
|
if (res & 0b010)
|
|
minterms.push(...this.operand.getMinterms(context, 0b110));
|
|
return minterms;
|
|
}
|
|
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 new Expression.Unary("IS NULL", this.operand.expression());
|
|
return super.expression();
|
|
}
|
|
}
|
|
|
|
export class Exp extends Clause {
|
|
constructor(public exp: Expression) {
|
|
super();
|
|
}
|
|
getMinterms(context: SynthContextBase<Clause>, res: number): Minterm[] {
|
|
if (!(this.exp instanceof Expression.Literal))
|
|
return context.getMinterms(this, res);
|
|
if (this.exp.value == null) return res & 0b001 ? [[]] : [];
|
|
if (this.exp.value && res & 0b100) return [[]];
|
|
if (!this.exp.value && res & 0b010) return [[]];
|
|
return [];
|
|
}
|
|
expression(): Expression {
|
|
return this.exp;
|
|
}
|
|
isBoolean(): boolean {
|
|
if (this.exp instanceof Expression.Literal) {
|
|
return (
|
|
this.exp.value === true ||
|
|
this.exp.value === false ||
|
|
this.exp.value == null
|
|
);
|
|
}
|
|
return false;
|
|
}
|
|
}
|
|
|
|
export class Compare extends Clause {
|
|
constructor(
|
|
public lhs: Clause,
|
|
public op: ">" | "<" | "=",
|
|
public rhs: boolean | number | string,
|
|
) {
|
|
super();
|
|
}
|
|
getMinterms(context: SynthContextBase<Clause>, res: number): Minterm[] {
|
|
res = res & 0b111;
|
|
if (!res) return [];
|
|
if (res === 0b111) return [[]];
|
|
if (res === 0b001 || res === 0b110)
|
|
return this.lhs.getMinterms(context, res);
|
|
return context.getMinterms(this, res);
|
|
}
|
|
*getNullables(): IterableIterator<IsNull> {
|
|
yield* this.lhs.getNullables();
|
|
}
|
|
isBoolean(): boolean {
|
|
return true;
|
|
}
|
|
expression(): Expression {
|
|
return new Expression.Binary(
|
|
this.op,
|
|
this.lhs.expression(),
|
|
new Expression.Literal(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 (exp instanceof Expression.FunctionCall) {
|
|
if (exp.name === "UPPER" || exp.name === "LOWER") {
|
|
const p =
|
|
exp.name === "UPPER" ? rhs.toUpperCase() : rhs.toLowerCase();
|
|
if (p === rhs) caseSensitive = false;
|
|
else contradiction = true;
|
|
lhs = new Exp(exp.args[0]);
|
|
}
|
|
}
|
|
this.lhs = lhs;
|
|
this.pattern = parseLikePattern(rhs, esc);
|
|
this.caseSensitive = caseSensitive;
|
|
this.contradiction = contradiction;
|
|
}
|
|
getMinterms(context: SynthContextBase<Clause>, res: number): Minterm[] {
|
|
res = res & 0b111;
|
|
if (!res) return [];
|
|
if (res === 0b111) return [[]];
|
|
if (res === 0b001 || res === 0b110)
|
|
return this.lhs.getMinterms(context, res);
|
|
return context.getMinterms(this, res);
|
|
}
|
|
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 = new Expression.FunctionCall("LOWER", [lhs]);
|
|
else lhs = new Expression.FunctionCall("UPPER", [lhs]);
|
|
} else if (!this.caseSensitive) {
|
|
if (this.rhs === this.rhs.toLocaleUpperCase())
|
|
lhs = new Expression.FunctionCall("UPPER", [lhs]);
|
|
else lhs = new Expression.FunctionCall("LOWER", [lhs]);
|
|
}
|
|
return new Expression.Binary(
|
|
"LIKE",
|
|
lhs,
|
|
new Expression.Literal(this.rhs),
|
|
);
|
|
}
|
|
}
|
|
|
|
export class Conditional extends Clause {
|
|
constructor(
|
|
public condition: Clause,
|
|
public then: Clause,
|
|
public otherwise: Clause,
|
|
) {
|
|
super();
|
|
}
|
|
getMinterms(context: SynthContextBase<Clause>, res: number): Minterm[] {
|
|
const condition = this.condition.getMinterms(context, 0b011);
|
|
if (!condition.length) return this.then.getMinterms(context, res);
|
|
return [
|
|
...complement([...condition, ...this.then.getMinterms(context, ~res)]),
|
|
...complement([
|
|
...complement(condition),
|
|
...this.otherwise.getMinterms(context, ~res),
|
|
]),
|
|
];
|
|
}
|
|
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 }[] = [];
|
|
let clause = this as Conditional;
|
|
|
|
for (;;) {
|
|
let minterms = clause.condition.getMinterms(context, 0b100);
|
|
const then = clause.then.expression();
|
|
if (
|
|
cases.length &&
|
|
then.toString() === cases[cases.length - 1].then.toString()
|
|
)
|
|
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;
|
|
if (clause.otherwise instanceof Conditional) clause = clause.otherwise;
|
|
else
|
|
clause = new Conditional(
|
|
new Exp(new Expression.Literal(true)),
|
|
clause.otherwise,
|
|
new Exp(new Expression.Literal(null)),
|
|
);
|
|
}
|
|
while (
|
|
cases[cases.length - 1].then instanceof Expression.Literal &&
|
|
(cases[cases.length - 1].then as Expression.Literal).value == null
|
|
)
|
|
cases.pop();
|
|
let res: Expression = new Expression.Literal(null);
|
|
while (cases.length) {
|
|
const c = cases.pop();
|
|
if (c.when.length === 1 && !c.when[0].length) {
|
|
res = c.then;
|
|
} else {
|
|
res = new Expression.Conditional(
|
|
context.toExpression(c.when),
|
|
c.then,
|
|
res,
|
|
);
|
|
}
|
|
}
|
|
|
|
this._expression = res;
|
|
return this._expression;
|
|
}
|
|
|
|
isBoolean(): boolean {
|
|
return this.then.isBoolean() && this.otherwise.isBoolean();
|
|
}
|
|
}
|
|
|
|
export function fromExpression(exp: Expression): Clause {
|
|
let res: Clause;
|
|
let negate = false;
|
|
if (exp instanceof Expression.Unary) {
|
|
let op = exp.operator;
|
|
negate = true;
|
|
if (op === "IS NOT NULL") op = "IS NULL";
|
|
else negate = false;
|
|
if (op === "NOT") res = new Clause.Not(fromExpression(exp.operand));
|
|
else if (op === "IS NULL") res = new IsNull(fromExpression(exp.operand));
|
|
} else if (exp instanceof Expression.Binary) {
|
|
let op = exp.operator;
|
|
negate = true;
|
|
if (op === "NOT LIKE") op = "LIKE";
|
|
else if (op === "<>") op = "=";
|
|
else if (op === ">=") op = "<";
|
|
else if (op === "<=") op = ">";
|
|
else negate = false;
|
|
|
|
if (op === "AND") {
|
|
res = new Clause.And([
|
|
fromExpression(exp.left),
|
|
fromExpression(exp.right),
|
|
]);
|
|
} else if (op === "OR") {
|
|
negate = true;
|
|
res = new Clause.And([
|
|
new Clause.Not(fromExpression(exp.left)),
|
|
new Clause.Not(fromExpression(exp.right)),
|
|
]);
|
|
} else if (exp.right instanceof Expression.Literal) {
|
|
if (["=", ">", "<"].includes(op)) {
|
|
if (
|
|
["boolean", "number", "string"].includes(typeof exp.right.value)
|
|
) {
|
|
res = new Compare(
|
|
fromExpression(exp.left),
|
|
op as ">" | "<" | "=",
|
|
exp.right.value,
|
|
);
|
|
}
|
|
} else if (op === "LIKE") {
|
|
if (typeof exp.right.value === "string")
|
|
res = new Like(fromExpression(exp.left), exp.right.value);
|
|
}
|
|
}
|
|
} else if (exp instanceof Expression.Conditional) {
|
|
res = new Conditional(
|
|
fromExpression(exp.condition),
|
|
fromExpression(exp.then),
|
|
fromExpression(exp.otherwise),
|
|
);
|
|
}
|
|
|
|
if (!res) res = new Exp(exp);
|
|
if (negate) res = new Not(res);
|
|
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: number): number[][] {
|
|
const v = this.getVar(clause);
|
|
switch (res & 0b111) {
|
|
case 0b100:
|
|
return [[(v << 2) ^ 3]];
|
|
case 0b010:
|
|
return [[(v << 2) ^ 1]];
|
|
case 0b001:
|
|
return [[v << 2, (v << 2) ^ 2]];
|
|
case 0b110:
|
|
return [[(v << 2) ^ 3], [(v << 2) ^ 1]];
|
|
case 0b101:
|
|
return [[(v << 2) ^ 3], [v << 2, (v << 2) ^ 2]];
|
|
case 0b011:
|
|
return [[(v << 2) ^ 1], [v << 2, (v << 2) ^ 2]];
|
|
default:
|
|
throw new Error("Invalid minterms");
|
|
}
|
|
}
|
|
|
|
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) => c.lhs.toString())) {
|
|
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) => c.lhs.toString())) {
|
|
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) {
|
|
if (clause.operand instanceof Clause.Exp) {
|
|
if (clause.operand.exp instanceof Expression.Parameter) {
|
|
const str = clause.operand.exp.path.toString();
|
|
if (str === "DeviceID.ID" || str === "_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);
|
|
}
|
|
|
|
canLower(idx: number, set: Set<number>): boolean {
|
|
if (idx & 1) return true;
|
|
const clause = this.getClause(idx >> 2);
|
|
if (clause instanceof Clause.IsNull) return true;
|
|
return set.has(idx ^ 3) || set.has(idx ^ 1);
|
|
}
|
|
|
|
bias(a: number, b: number): number {
|
|
// Bias towards 1 then true
|
|
return ((b & 3) ^ 3) - ((a & 3) ^ 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 & 0b0011) === 0b0011) continue loop;
|
|
if ((v & 0b1100) === 0b1100) continue loop;
|
|
const clause = this.clauses.get(k);
|
|
if (!clause) throw new Error("Invalid literal");
|
|
if (clause instanceof Clause.IsNull) {
|
|
if (v === 0b0100) minterm.push((k << 2) ^ 2);
|
|
else if (v === 0b1000) minterm.push((k << 2) ^ 3);
|
|
else throw new Error("Invalid literal");
|
|
continue;
|
|
}
|
|
if ((v & 0b1010) === 0b1010) continue loop;
|
|
const isNullVars = [...clause.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 {
|
|
let res: Expression = new Expression.Literal(false);
|
|
for (const s of sop) {
|
|
let conjs: Expression = new Expression.Literal(true);
|
|
for (const i of s) {
|
|
const clause = this.getClause(i >>> 2);
|
|
if (!clause) throw new Error("Invalid literal");
|
|
if (clause instanceof Clause.IsNull) {
|
|
if (!(i & 2)) throw new Error("Invalid literal");
|
|
} else if (!(i & 1)) {
|
|
// Should never be reached if minimized correctly
|
|
const isNullVars = [...clause.getNullables()].map((c) =>
|
|
this.getVar(c),
|
|
);
|
|
conjs = Expression.and(
|
|
conjs,
|
|
this.toExpression([
|
|
[i ^ 3],
|
|
...isNullVars.map((n) => [(n << 2) ^ 3]),
|
|
]),
|
|
);
|
|
continue;
|
|
}
|
|
|
|
let expr = clause.expression();
|
|
if (!(i & 1) !== !(i & 2)) expr = new Expression.Unary("NOT", expr);
|
|
if (expr instanceof Expression.Unary && expr.operator === "NOT") {
|
|
const e = expr.operand;
|
|
if (e instanceof Expression.Unary) {
|
|
if (e.operator === "IS NULL")
|
|
expr = new Expression.Unary("IS NOT NULL", e.operand);
|
|
else if (e.operator === "IS NOT NULL")
|
|
expr = new Expression.Unary("IS NULL", e.operand);
|
|
else if (e.operator === "NOT") expr = e.operand;
|
|
} else if (e instanceof Expression.Binary) {
|
|
if (e.operator === "LIKE")
|
|
expr = new Expression.Binary("NOT LIKE", e.left, e.right);
|
|
else if (e.operator === "=")
|
|
expr = new Expression.Binary("<>", e.left, e.right);
|
|
else if (e.operator === "<>")
|
|
expr = new Expression.Binary("=", e.left, e.right);
|
|
else if (e.operator === ">")
|
|
expr = new Expression.Binary("<=", e.left, e.right);
|
|
else if (e.operator === ">=")
|
|
expr = new Expression.Binary("<", e.left, e.right);
|
|
else if (e.operator === "<")
|
|
expr = new Expression.Binary(">=", e.left, e.right);
|
|
else if (e.operator === "<=")
|
|
expr = new Expression.Binary(">", e.left, e.right);
|
|
}
|
|
}
|
|
conjs = Expression.and(conjs, expr);
|
|
}
|
|
res = Expression.or(res, conjs);
|
|
}
|
|
return res;
|
|
}
|
|
}
|
|
|
|
// 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 instanceof Expression.Literal && !expr2.value)
|
|
return [expr1, new Expression.Literal(false)];
|
|
|
|
const synth2 = Clause.fromExpression(expr2);
|
|
|
|
if (expr1 instanceof Expression.Literal && !expr1.value) {
|
|
const e = synth2.expression();
|
|
return [e, e];
|
|
}
|
|
|
|
expr1 = normalize(expr1);
|
|
const synth1 = Clause.fromExpression(expr1);
|
|
|
|
const context = new SynthContext();
|
|
|
|
const expr2Minterms = synth2.getMinterms(context, 0b100);
|
|
const expr1Minterms = synth1.getMinterms(context, 0b100);
|
|
|
|
const union = context.minimize([...expr1Minterms, ...expr2Minterms]);
|
|
|
|
const diff = context.minimize(
|
|
complement([...expr1Minterms, ...complement(expr2Minterms)]),
|
|
);
|
|
|
|
return [context.toExpression(union), context.toExpression(diff)];
|
|
}
|
|
|
|
export function covers(expr1: Expression, expr2: Expression): boolean {
|
|
expr2 = normalize(expr2);
|
|
if (expr2 instanceof Expression.Literal && !expr2.value) return true;
|
|
expr1 = normalize(expr1);
|
|
if (expr1 instanceof Expression.Literal && expr1.value) return true;
|
|
|
|
const synt1 = Clause.fromExpression(expr1);
|
|
const synt2 = Clause.fromExpression(expr2);
|
|
|
|
const context = new SynthContext();
|
|
const expr1Minterms = synt1.getMinterms(context, 0b100);
|
|
const expr2Minterms = synt2.getMinterms(context, 0b100);
|
|
|
|
return tautology([
|
|
...context.sanitizeMinterms(complement(expr2Minterms)),
|
|
...context.getDcSet([...expr2Minterms, ...expr1Minterms]),
|
|
...context.sanitizeMinterms(expr1Minterms),
|
|
]);
|
|
}
|