From 00ccf99be6d04c6607b68cc13164be6e4993f8b8 Mon Sep 17 00:00:00 2001 From: Zaid Abdulla Date: Wed, 29 Jul 2020 02:31:31 -0700 Subject: [PATCH] Minimize store queries --- build/build.ts | 14 +- lib/common/bigint-jsbi.ts | 108 ++++ lib/common/bigint.ts | 106 ++++ lib/common/boolean-expression.ts | 964 +++++++++++++++++++++++++++++++ lib/common/expression-cnf.ts | 285 --------- lib/common/expression-parser.ts | 2 +- lib/common/expression.ts | 14 - lib/common/sat-solver.ts | 175 ------ npm-shrinkwrap.json | 13 + package.json | 4 +- ui/store.ts | 68 +-- 11 files changed, 1234 insertions(+), 519 deletions(-) create mode 100644 lib/common/bigint-jsbi.ts create mode 100644 lib/common/bigint.ts create mode 100644 lib/common/boolean-expression.ts delete mode 100644 lib/common/expression-cnf.ts delete mode 100644 lib/common/sat-solver.ts diff --git a/build/build.ts b/build/build.ts index 01ff3b0..a50bbc8 100644 --- a/build/build.ts +++ b/build/build.ts @@ -80,6 +80,8 @@ const externals = [ "codemirror/mode/javascript/javascript", "codemirror/mode/yaml/yaml", "ipaddr.js", + "jsbi", + "yebool", ]; function rmDirSync(dirPath): void { @@ -295,12 +297,22 @@ async function generateFrontendJs(): Promise { const inputFile = path.resolve(INPUT_DIR, "ui/app.ts"); const outputFile = path.resolve(OUTPUT_DIR, "public/app.js"); - const inlineDeps = ["mithril", "parsimmon"]; + const inlineDeps = ["mithril", "parsimmon", "jsbi", "yebool"]; const bundle = await rollup({ input: inputFile, external: externals.filter((e) => !inlineDeps.includes(e)), plugins: [ rollupJson({ preferConst: true }), + { + name: "", + resolveId: function (importee, importer) { + if (importee.endsWith("/bigint")) + return this.resolve(importee + "-jsbi", importer); + else if (importee === "yebool") + return this.resolve("yebool/dist/yebool-jsbi.mjs", importer); + return null; + }, + }, typescript({ tsconfig: "./tsconfig.json" }), nodeResolve(), commonjs(), diff --git a/lib/common/bigint-jsbi.ts b/lib/common/bigint-jsbi.ts new file mode 100644 index 0000000..defc9d7 --- /dev/null +++ b/lib/common/bigint-jsbi.ts @@ -0,0 +1,108 @@ +/** + * 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 . + */ + +import JSBI from "jsbi"; + +export function and(a: JSBI, b: JSBI): JSBI { + return JSBI.bitwiseAnd(a, b); +} + +export function or(a: JSBI, b: JSBI): JSBI { + return JSBI.bitwiseOr(a, b); +} + +export function xor(a: JSBI, b: JSBI): JSBI { + return JSBI.bitwiseXor(a, b); +} + +export function not(a: JSBI): JSBI { + return JSBI.bitwiseNot(a); +} + +export function lshift(a: JSBI, b: JSBI): JSBI { + return JSBI.leftShift(a, b); +} + +export function rshift(a: JSBI, b: JSBI): JSBI { + return JSBI.signedRightShift(a, b); +} + +export function add(a: JSBI, b: JSBI): JSBI { + return JSBI.add(a, b); +} + +export function sub(a: JSBI, b: JSBI): JSBI { + return JSBI.subtract(a, b); +} + +export function mul(a: JSBI, b: JSBI): JSBI { + return JSBI.multiply(a, b); +} + +export function div(a: JSBI, b: JSBI): JSBI { + return JSBI.divide(a, b); +} + +export function exp(a: JSBI, b: JSBI): JSBI { + return JSBI.exponentiate(a, b); +} + +export function rem(a: JSBI, b: JSBI): JSBI { + return JSBI.remainder(a, b); +} + +export function toNumber(a: JSBI): number { + return JSBI.toNumber(a); +} + +export function eq(a: JSBI, b: JSBI): boolean { + return JSBI.equal(a, b); +} + +export function ne(a: JSBI, b: JSBI): boolean { + return JSBI.notEqual(a, b); +} + +export function lt(a: JSBI, b: JSBI): boolean { + return JSBI.lessThan(a, b); +} + +export function lte(a: JSBI, b: JSBI): boolean { + return JSBI.lessThanOrEqual(a, b); +} + +export function gt(a: JSBI, b: JSBI): boolean { + return JSBI.greaterThan(a, b); +} + +export function gte(a: JSBI, b: JSBI): boolean { + return JSBI.greaterThanOrEqual(a, b); +} + +export function asUintN(a: number, b: JSBI): JSBI { + return JSBI.asUintN(a, b); +} + +export function asIntN(a: number, b: JSBI): JSBI { + return JSBI.asIntN(a, b); +} + +const _BigInt = JSBI.BigInt; +type _bigint = JSBI; +export { _BigInt as BigInt, _bigint as bigint }; diff --git a/lib/common/bigint.ts b/lib/common/bigint.ts new file mode 100644 index 0000000..4978ab0 --- /dev/null +++ b/lib/common/bigint.ts @@ -0,0 +1,106 @@ +/** + * 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 . + */ + +export function and(a: bigint, b: bigint): bigint { + return a & b; +} + +export function or(a: bigint, b: bigint): bigint { + return a | b; +} + +export function xor(a: bigint, b: bigint): bigint { + return a ^ b; +} + +export function not(a: bigint): bigint { + return ~a; +} + +export function lshift(a: bigint, b: bigint): bigint { + return a << b; +} + +export function rshift(a: bigint, b: bigint): bigint { + return a >> b; +} + +export function add(a: bigint, b: bigint): bigint { + return a + b; +} + +export function sub(a: bigint, b: bigint): bigint { + return a - b; +} + +export function mul(a: bigint, b: bigint): bigint { + return a * b; +} + +export function div(a: bigint, b: bigint): bigint { + return a / b; +} + +export function exp(a: bigint, b: bigint): bigint { + return a ** b; +} + +export function rem(a: bigint, b: bigint): bigint { + return a % b; +} + +export function toNumber(a: bigint): number { + return Number(a); +} + +export function eq(a: bigint, b: bigint): boolean { + return a === b; +} + +export function ne(a: bigint, b: bigint): boolean { + return a !== b; +} + +export function lt(a: bigint, b: bigint): boolean { + return a < b; +} + +export function lte(a: bigint, b: bigint): boolean { + return a <= b; +} + +export function gt(a: bigint, b: bigint): boolean { + return a > b; +} + +export function gte(a: bigint, b: bigint): boolean { + return a >= b; +} + +export function asUintN(a: number, b: bigint): bigint { + return BigInt.asUintN(a, b); +} + +export function asIntN(a: number, b: bigint): bigint { + return BigInt.asIntN(a, b); +} + +const _BigInt = BigInt; +type _bigint = bigint; +export { _BigInt as BigInt, _bigint as bigint }; diff --git a/lib/common/boolean-expression.ts b/lib/common/boolean-expression.ts new file mode 100644 index 0000000..65b5629 --- /dev/null +++ b/lib/common/boolean-expression.ts @@ -0,0 +1,964 @@ +/** + * 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 . + */ + +import * as BI from "./bigint"; +import { espresso, complement, tautology } from "yebool"; +import { Expression } from "../types"; +import { map } from "./expression-parser"; + +const ZERO = BI.BigInt(0); +const ONE = BI.BigInt(1); +const TWO = BI.BigInt(2); +const NEGATIVE_ONE = BI.BigInt(-1); + +class Indeterminates { + public map: Map; + public sortedKeys: string[]; + + public constructor(str?: string) { + this.map = new Map(); + if (str) { + this.map.set(str, 1); + this.sortedKeys = [str]; + } else { + this.sortedKeys = []; + } + } + + public reciprocal(): Indeterminates { + const res = new Indeterminates(); + res.sortedKeys = this.sortedKeys; + res.map = new Map(); + for (const [k, v] of this.map) res.map.set(k, 0 - v); + return res; + } + + public static multiply( + indeterminates1: Indeterminates, + indeterminates2: Indeterminates + ): Indeterminates { + const res = new Indeterminates(); + res.sortedKeys = indeterminates1.sortedKeys.slice(); + res.map = new Map(indeterminates1.map); + + for (const [key, val] of indeterminates2.map) { + const v = res.map.get(key); + if (!v) { + res.map.set(key, val); + res.sortedKeys.push(key); + } else { + const v2 = val + v; + if (!v2) { + res.map.delete(key); + res.sortedKeys = res.sortedKeys.filter((s) => s !== key); + } else { + res.map.set(key, v2); + } + } + } + + res.sortedKeys.sort((a, b) => { + if (a.length !== b.length) return b.length - a.length; + else if (a > b) return 1; + else if (a < b) return -1; + return 0; + }); + + return res; + } + + public static compare(a: Indeterminates, b: Indeterminates): number { + if (a.sortedKeys.length !== b.sortedKeys.length) + return b.sortedKeys.length - a.sortedKeys.length; + for (let i = 0; i < a.sortedKeys.length; ++i) { + const k1 = a.sortedKeys[i]; + const w1 = a.map.get(k1); + const k2 = b.sortedKeys[i]; + const w2 = b.map.get(k2); + if (w1 !== w2) return w2 - w1; + if (k1.length > k2.length) return -1; + else if (k1.length < k2.length) return 1; + else if (k1 > k2) return 1; + else if (k1 < k2) return -1; + } + return 0; + } +} + +interface Term { + indeterminates: Indeterminates; + coefficientNumerator: BI.bigint; + coefficientDenominator: BI.bigint; +} + +function findGcd(a: BI.bigint, b: BI.bigint): BI.bigint { + while (BI.ne(b, ZERO)) { + const t = b; + b = BI.rem(a, b); + a = t; + } + return a; +} + +class Polynomial { + public terms: Term[]; + + public constructor(terms: Term[]) { + this.terms = terms; + } + + public static simplifyTerms(terms: Term[]): Term[] { + const ts = terms + .slice() + .sort((a: Term, b: Term) => + Indeterminates.compare(a.indeterminates, b.indeterminates) + ); + + for (let i = 1; i < ts.length; ++i) { + const t1 = ts[i - 1]; + const t2 = ts[i]; + if (Indeterminates.compare(t1.indeterminates, t2.indeterminates) === 0) { + const numerator = BI.add( + BI.mul(t1.coefficientNumerator, t2.coefficientDenominator), + BI.mul(t2.coefficientNumerator, t1.coefficientDenominator) + ); + + const denominator = BI.mul( + t1.coefficientDenominator, + t2.coefficientDenominator + ); + + const gcd = findGcd(numerator, denominator); + + ts[i] = { + indeterminates: t2.indeterminates, + coefficientNumerator: BI.div(numerator, gcd), + coefficientDenominator: BI.div(denominator, gcd), + }; + ts[i - 1] = { + indeterminates: t1.indeterminates, + coefficientNumerator: ZERO, + coefficientDenominator: t1.coefficientDenominator, + }; + } + } + return ts.filter((v) => BI.ne(v.coefficientNumerator, ZERO)); + } + + public static fromIndeterminate(indeterminate: Expression): Polynomial { + const indeterminates = new Indeterminates(JSON.stringify(indeterminate)); + const terms = [ + { + indeterminates: indeterminates, + coefficientNumerator: ONE, + coefficientDenominator: ONE, + }, + ]; + return new Polynomial(terms); + } + + public static fromConstant(constant: number): Polynomial { + const [int, frac] = Math.abs(constant).toString(2).split(".", 2); + let numerator = BI.BigInt("0b" + int); + if (constant < 0) numerator = BI.mul(numerator, NEGATIVE_ONE); + let denominator = ONE; + if (frac) { + denominator = BI.exp(TWO, BI.BigInt(frac.length)); + numerator = BI.add( + BI.mul(numerator, denominator), + BI.BigInt("0b" + frac) + ); + } + + const terms = [ + { + indeterminates: new Indeterminates(), + coefficientNumerator: numerator, + coefficientDenominator: denominator, + }, + ]; + + return new Polynomial(terms); + } + + public negation(): Polynomial { + const terms = this.terms.map((t) => ({ + indeterminates: t.indeterminates, + coefficientNumerator: BI.mul(t.coefficientNumerator, NEGATIVE_ONE), + coefficientDenominator: t.coefficientDenominator, + })); + + return new Polynomial(terms); + } + + public reciprocal(): Polynomial { + const terms = this.terms.map((t) => ({ + indeterminates: t.indeterminates.reciprocal(), + coefficientNumerator: t.coefficientDenominator, + coefficientDenominator: t.coefficientNumerator, + })); + return new Polynomial(terms); + } + + public constant(): Polynomial { + const terms = this.terms.filter((t) => !t.indeterminates.sortedKeys.length); + return new Polynomial(terms); + } + + public add(rhs: Polynomial): Polynomial { + return new Polynomial( + Polynomial.simplifyTerms(this.terms.concat(rhs.terms)) + ); + } + + public subtract(rhs: Polynomial): Polynomial { + return this.add(rhs.negation()); + } + + public multiply(rhs: Polynomial): Polynomial { + const terms: Term[] = []; + + for (const t1 of this.terms) { + for (const t2 of rhs.terms) { + const numerator = BI.mul( + t1.coefficientNumerator, + t2.coefficientNumerator + ); + const denominator = BI.mul( + t1.coefficientDenominator, + t2.coefficientDenominator + ); + const gcd = findGcd(numerator, denominator); + + terms.push({ + indeterminates: Indeterminates.multiply( + t1.indeterminates, + t2.indeterminates + ), + coefficientNumerator: BI.div(numerator, gcd), + coefficientDenominator: BI.div(denominator, gcd), + }); + } + } + + return new Polynomial(Polynomial.simplifyTerms(terms)); + } + + public divide(rhs: Polynomial): Polynomial { + return this.multiply(rhs.reciprocal()); + } + + public toString(): string { + const add: string[] = []; + for (const t of this.terms) { + const coefficient = + BI.toNumber(t.coefficientNumerator) / + BI.toNumber(t.coefficientDenominator); + + const mul: string[] = []; + if (t.indeterminates.sortedKeys.length) { + for (const k of t.indeterminates.sortedKeys) { + const w = t.indeterminates.map.get(k); + for (let i = Math.abs(w); i > 0; --i) { + if (w > 0) mul.push(k); + else mul.push(`["/",1,${k}]`); + } + } + + if (coefficient !== 1) mul.push(coefficient.toString()); + + if (mul.length > 1) add.push(`["*",${mul.join(",")}]`); + else add.push(mul["0"]); + } else { + add.push(coefficient.toString()); + } + } + + if (!add.length) return "0"; + else if (add.length === 1) return add[0]; + else return `["+",${add.join(",")}]`; + } +} + +type Minterm = number[]; +type Context = Map; + +abstract class BoolExprSynth { + public abstract true(context: Context): Minterm[]; + public abstract false(context: Context): Minterm[]; + public abstract null(context: Context): Minterm[]; +} + +class TrueSynth extends BoolExprSynth { + public true(): Minterm[] { + return [[]]; + } + public false(): Minterm[] { + return []; + } + public null(): Minterm[] { + return []; + } +} + +class FalseSynth extends BoolExprSynth { + public true(): Minterm[] { + return []; + } + public false(): Minterm[] { + return [[]]; + } + public null(): Minterm[] { + return []; + } +} + +class NullSynth extends BoolExprSynth { + public true(): Minterm[] { + return []; + } + public false(): Minterm[] { + return []; + } + public null(): Minterm[] { + return [[]]; + } +} + +class VarSynth extends BoolExprSynth { + private expStr: string; + private negate: boolean; + public constructor(exp: Expression) { + super(); + this.negate = false; + if (Array.isArray(exp)) { + const op = exp[0]; + if (op === "<>") { + exp = exp.slice(); + exp[0] = "="; + this.negate = true; + } else if (op === ">=") { + exp = exp.slice(); + exp[0] = "<"; + this.negate = true; + } else if (op === "<=") { + exp = exp.slice(); + exp[0] = ">"; + this.negate = true; + } + } + this.expStr = JSON.stringify(exp); + } + public true(context: Context): Minterm[] { + let v = context.get(this.expStr); + if (v == null) context.set(this.expStr, (v = context.size)); + return [[(v << 2) ^ (this.negate ? 1 : 3)]]; + } + public false(context: Context): Minterm[] { + let v = context.get(this.expStr); + if (v == null) context.set(this.expStr, (v = context.size)); + return [[(v << 2) ^ (this.negate ? 3 : 1)]]; + } + public null(context: Context): Minterm[] { + let v = context.get(this.expStr); + if (v == null) context.set(this.expStr, (v = context.size)); + return [[v << 2, (v << 2) ^ 2]]; + } +} + +class NotSynth extends BoolExprSynth { + private exprSynth: BoolExprSynth; + public constructor(e: BoolExprSynth) { + super(); + this.exprSynth = e; + } + public true(context: Context): Minterm[] { + return this.exprSynth.false(context); + } + public false(context: Context): Minterm[] { + return this.exprSynth.true(context); + } + public null(context: Context): Minterm[] { + return this.exprSynth.null(context); + } +} + +class IsNullSynth extends BoolExprSynth { + private exprSynth: BoolExprSynth; + public constructor(e: BoolExprSynth) { + super(); + this.exprSynth = e; + } + public true(context: Context): Minterm[] { + return this.exprSynth.null(context); + } + public false(context: Context): Minterm[] { + return [...this.exprSynth.true(context), ...this.exprSynth.false(context)]; + } + public null(): Minterm[] { + return []; + } +} + +class OrSynth extends BoolExprSynth { + private exprSynths: BoolExprSynth[]; + public constructor(...e: BoolExprSynth[]) { + super(); + this.exprSynths = e; + } + public true(context: Context): Minterm[] { + return this.exprSynths.map((e) => e.true(context)).flat(); + } + public false(context: Context): Minterm[] { + return complement( + this.exprSynths.map((e) => complement(e.false(context))).flat() + ); + } + public null(context: Context): Minterm[] { + const t = this.exprSynths.map((e) => e.true(context)).flat(); + const f = this.exprSynths.map((e) => e.false(context)).flat(); + return complement([...t, ...f]); + } +} + +class AndSynth extends BoolExprSynth { + private exprSynths: BoolExprSynth[]; + public constructor(...e: BoolExprSynth[]) { + super(); + this.exprSynths = e; + } + public true(context: Context): Minterm[] { + return complement( + this.exprSynths.map((e) => complement(e.true(context))).flat() + ); + } + public false(context: Context): Minterm[] { + return this.exprSynths.map((e) => e.false(context)).flat(); + } + public null(context: Context): Minterm[] { + const t = this.exprSynths.map((e) => e.true(context)).flat(); + const f = this.exprSynths.map((e) => e.false(context)).flat(); + return complement([...t, ...f]); + } +} + +const ADDITIVE_IDENTITY = Polynomial.fromConstant(0); +const MULTIPLICATIVE_IDENTITY = Polynomial.fromConstant(1); + +const SWAPPED_OPS = { + "=": "=", + "<>": "<>", + ">": "<", + ">=": "<=", + "<": ">", + "<=": ">=", +}; + +export function normalize(expr: Expression): Expression { + expr = map(expr, (exp) => { + if (!Array.isArray(exp)) return exp; + const op = exp[0]; + + if (op === "+") { + const args = exp.slice(1).map((e) => { + if (e instanceof Polynomial) return e; + else if (typeof e === "number") return Polynomial.fromConstant(e); + else return Polynomial.fromIndeterminate(e); + }); + return (args.reduce( + (previousValue, currentValue) => previousValue.add(currentValue), + ADDITIVE_IDENTITY + ) as unknown) as Expression; + } else if (op === "*") { + const args = exp.slice(1).map((e) => { + if (e instanceof Polynomial) return e; + else if (typeof e === "number") return Polynomial.fromConstant(e); + else return Polynomial.fromIndeterminate(e); + }); + + return (args.reduce( + (previousValue, currentValue) => previousValue.multiply(currentValue), + MULTIPLICATIVE_IDENTITY + ) as unknown) as Expression; + } else if (op === "-") { + const args = exp.slice(1).map((e) => { + if (e instanceof Polynomial) return e; + else if (typeof e === "number") return Polynomial.fromConstant(e); + else return Polynomial.fromIndeterminate(e); + }); + return (args.reduce((previousValue, currentValue) => + previousValue.subtract(currentValue) + ) as unknown) as Expression; + } else if (op === "/") { + const args = exp.slice(1).map((e) => { + if (e instanceof Polynomial) return e; + else if (typeof e === "number") return Polynomial.fromConstant(e); + else return Polynomial.fromIndeterminate(e); + }); + return (args.reduce((previousValue, currentValue) => + previousValue.divide(currentValue) + ) as unknown) as Expression; + } else if (["=", "<>", ">", ">=", "<", "<="].includes(op)) { + let lhs: Polynomial, rhs: Polynomial; + if (exp[1] instanceof Polynomial) lhs = exp[1]; + else if (typeof exp[1] === "number") + lhs = Polynomial.fromConstant(exp[1]); + + if (exp[2] instanceof Polynomial) rhs = exp[2]; + else if (typeof exp[2] === "number") + rhs = Polynomial.fromConstant(exp[2]); + + if (lhs || rhs) { + if (!lhs) lhs = Polynomial.fromIndeterminate(exp[1]); + if (!rhs) rhs = Polynomial.fromIndeterminate(exp[2]); + + lhs = lhs.subtract(rhs); + rhs = lhs.constant().negation(); + lhs = lhs.add(rhs); + + if (!lhs.terms.length) { + exp = [op, JSON.parse(lhs.toString()), JSON.parse(rhs.toString())]; + + if (op === "=") return exp[1] === exp[2]; + else if (op === "<>") return exp[1] !== exp[2]; + else if (op === ">") return exp[1] > exp[2]; + else if (op === ">=") return exp[1] >= exp[2]; + else if (op === "<") return exp[1] < exp[2]; + else if (op === "<=") return exp[1] <= exp[2]; + } else { + let flipOp = 1; + + const n = lhs.terms[0].coefficientNumerator; + const d = lhs.terms[0].coefficientDenominator; + + if (BI.lt(n, ZERO) || BI.lt(d, ZERO)) flipOp *= -1; + + const reciprocal = new Polynomial([ + { + indeterminates: new Indeterminates(), + coefficientNumerator: d, + coefficientDenominator: n, + }, + ]); + + lhs = lhs.multiply(reciprocal); + rhs = rhs.multiply(reciprocal); + + const keys = lhs.terms[0].indeterminates.sortedKeys; + let invert = + lhs.terms[0].indeterminates.map.get(keys[0]) < 0 ? -1 : 0; + + for (const t of lhs.terms) + for (const v of t.indeterminates.map.values()) invert += v; + + if (invert < 0) { + flipOp *= -1; + lhs = lhs.reciprocal(); + rhs = rhs.reciprocal(); + } + + if (flipOp < 0) exp = [SWAPPED_OPS[op], lhs, rhs]; + else exp = [op, lhs, rhs]; + } + } + } + + // Restore polynomial expressions + exp = exp.map((e) => + e instanceof Polynomial ? JSON.parse(e.toString()) : e + ); + + return exp; + }); + + if (expr instanceof Polynomial) expr = JSON.parse(expr.toString()); + + return expr; +} + +function toBoolExprSynth(e: Expression | BoolExprSynth): BoolExprSynth { + if (e instanceof BoolExprSynth) return e; + else if (Array.isArray(e)) return new VarSynth(e); + else if (e == null) return new NullSynth(); + else if (e) return new TrueSynth(); + else return new FalseSynth(); +} + +function sopToExpression( + sop: number[][], + expressions: Map +): Expression { + if (!sop.length) return false; + const res: Expression[] = []; + for (const s of sop) { + if (!s.length) return true; + const and: Expression[] = []; + for (const i of s) { + let expr = expressions.get(i >>> 2); + if (!(i & 1) !== !(i & 2)) expr = ["NOT", expr]; + if (Array.isArray(expr) && expr[0] === "NOT" && Array.isArray(expr[1])) { + const e: Expression[] = expr[1]; + if (e[0] === "IS NULL") expr = ["IS NOT NULL", ...e.slice(1)]; + else if (e[0] === "=") expr = ["<>", ...e.slice(1)]; + else if (e[0] === "<>") expr = ["=", ...e.slice(1)]; + else if (e[0] === ">") expr = ["<=", ...e.slice(1)]; + else if (e[0] === ">=") expr = ["<", ...e.slice(1)]; + else if (e[0] === "<") expr = [">=", ...e.slice(1)]; + else if (e[0] === "<=") expr = [">", ...e.slice(1)]; + else if (e[0] === "NOT") expr = e[1]; + else expr = ["NOT", e]; + } + and.push(expr); + } + if (and.length > 1) res.push(["AND" as any].concat(and)); + else res.push(and[0]); + } + if (res.length > 1) return ["OR" as any].concat(res); + return res[0]; +} + +function generateDcSetAndIsNull( + variables: Map +): { dcSet: number[][]; isNull: Map } { + // TODO support LIKE and NOT LIKE operators + const relations: Map< + string, + { op: string; rhs: boolean | number | string; var: number }[] + > = new Map(); + + for (const [n, e] of variables) { + const op = e[0] as string; + if (["=", ">", "<"].includes(op) && !Array.isArray(e[2])) { + const lhs = JSON.stringify(e[1]); + let r = relations.get(lhs); + if (!r) relations.set(lhs, (r = [])); + r.push({ op: op, rhs: e[2], var: n }); + } else { + const lhs = JSON.stringify(e); + let r = relations.get(lhs); + if (!r) relations.set(lhs, (r = [])); + r.push({ op: "", rhs: null, var: n }); + } + } + + const dcSet: number[][] = []; + const isNull: Map = new Map(); + + for (const [key, rels] of relations) { + const n = variables.size; + variables.set(n, ["IS NULL", JSON.parse(key)]); + + if (key === '["PARAM","DeviceID.ID"]' || key === '["PARAM","_id"]') + dcSet.push([(n << 2) ^ 3]); + + const existingOps = new Map() as Map>; + for (const rel of rels) { + if (!rel.op) continue; + const rhsStr = JSON.stringify(rel.rhs); + const s = existingOps.get(rhsStr); + if (s) s.set(rel.op, rel.var); + else existingOps.set(rhsStr, new Map([[rel.op, rel.var]])); + } + + for (const [k, v] of existingOps) { + if (v.size > 1) { + if (!v.has("=")) { + const va = variables.size; + variables.set(va, ["=", JSON.parse(key), JSON.parse(k)]); + rels.push({ op: "=", rhs: JSON.parse(k), var: va }); + v.set("=", va); + } + + if (!v.has(">")) { + const va = variables.size; + variables.set(va, [">", JSON.parse(key), JSON.parse(k)]); + rels.push({ op: ">", rhs: JSON.parse(k), var: va }); + v.set(">", va); + } + + if (!v.has("<")) { + const va = variables.size; + variables.set(va, ["<", JSON.parse(key), JSON.parse(k)]); + rels.push({ op: "<", rhs: JSON.parse(k), var: va }); + v.set("<", va); + } + + dcSet.push([ + (v.get("=") << 2) ^ 1, + (v.get(">") << 2) ^ 1, + (v.get("<") << 2) ^ 1, + ]); + } + } + + for (let i = 0; i < rels.length; ++i) { + const rel1 = rels[i]; + isNull.set(rel1.var, n); + + dcSet.push([(n << 2) ^ 3, (rel1.var << 2) ^ 1]); + dcSet.push([(n << 2) ^ 3, (rel1.var << 2) ^ 3]); + dcSet.push([(rel1.var << 2) ^ 0, (rel1.var << 2) ^ 2, (n << 2) ^ 2]); + + if (!rel1.op) continue; + for (let j = i + 1; j < rels.length; ++j) { + const rel2 = rels[j]; + if (!rel2.op) continue; + let comp = 0; + if (Array.isArray(rel1.rhs) || Array.isArray(rel2.rhs)) { + if (JSON.stringify(rel1.rhs) !== JSON.stringify(rel2.rhs)) continue; + } else if (typeof rel1.rhs === "string") { + if (typeof rel2.rhs === "string") { + if (rel1.rhs > rel2.rhs) comp = 1; + else if (rel1.rhs < rel2.rhs) comp = -1; + } else { + comp = 1; + } + } else if (typeof rel2.rhs === "string") { + comp = -1; + } else { + comp = +rel1.rhs - +rel2.rhs; + } + + if (rel1.op === rel2.op) { + if (comp === 0) + dcSet.push([(rel1.var << 2) ^ 1, (rel2.var << 2) ^ 1]); + else if (rel1.op === "=") + dcSet.push([(rel1.var << 2) ^ 3, (rel2.var << 2) ^ 3]); + else if ( + (rel1.op === ">" && comp > 0) || + (rel1.op === "<" && comp < 0) + ) + dcSet.push([(rel1.var << 2) ^ 3, (rel2.var << 2) ^ 1]); + else if ( + (rel1.op === "<" && comp > 0) || + (rel1.op === ">" && comp < 0) + ) + dcSet.push([(rel1.var << 2) ^ 1, (rel2.var << 2) ^ 3]); + } else if (rel1.op === "=" || rel2.op === "=") { + let r1 = rel1, + r2 = rel2, + cmp = comp; + if (rel1.op !== "=") { + r2 = rel1; + r1 = rel2; + cmp = -comp; + } + if (r2.op === ">" || r2.op === "<") { + if (cmp === 0) { + dcSet.push([(r1.var << 2) ^ 3, (r2.var << 2) ^ 3]); + } else { + if ((cmp > 0 && r2.op === ">") || (cmp < 0 && r2.op === "<")) + dcSet.push([(r1.var << 2) ^ 3, (r2.var << 2) ^ 1]); + else dcSet.push([(r1.var << 2) ^ 3, (r2.var << 2) ^ 3]); + } + } + } else if ( + [">", "<"].includes(rel1.op) && + [">", "<"].includes(rel2.op) + ) { + if ((rel1.op === ">" && comp < 0) || (rel1.op === "<" && comp > 0)) + dcSet.push([(rel1.var << 2) ^ 1, (rel2.var << 2) ^ 1]); + else dcSet.push([(rel1.var << 2) ^ 3, (rel2.var << 2) ^ 3]); + } + } + } + } + + return { dcSet, isNull }; +} + +function sanitizeMinterms( + minterms: number[][], + isNull: Map +): number[][] { + const res = [] as number[][]; + loop: for (const m of minterms) { + const merged: Map = new Map(); + for (const i of m) + merged.set(i >> 2, (merged.get(i >> 2) || 0) | (1 << (i & 3))); + const minterm: number[] = []; + const perms: number[][] = []; + for (const [k, v] of merged) { + if (v === 0b1010) continue loop; + const n = isNull.get(k) << 2; + const t = k << 2; + if (v === 0b0101) minterm.push(n ^ 3); + else if (v === 0b0001) perms.push([n ^ 3, t ^ 3]); + else if (v === 0b0100) perms.push([n ^ 3, t ^ 1]); + else if (v & 0b1000) minterm.push(t ^ 3); + else if (v & 0b0010) minterm.push(t ^ 1); + } + let ms = [minterm]; + while (perms.length) { + const newMs: number[][] = []; + const perm = perms.pop(); + for (const p of perm) newMs.push(...ms.map((mm) => [...mm, p])); + ms = newMs; + } + res.push(...ms); + } + return res; +} + +function boolExprSynthToExpression(boolExpr: BoolExprSynth): Expression { + const context: Map = new Map(); + let minterms = boolExpr.true(context); + const variables = new Map( + Array.from(context).map(([k, v]) => [v, JSON.parse(k) as Expression]) + ); + const { dcSet, isNull } = generateDcSetAndIsNull(variables); + minterms = sanitizeMinterms(minterms, isNull); + + function canRaise(idx: number, set: Set): boolean { + if (set.size === 1) return true; + const i = idx >>> 2; + const n = isNull.get(i); + if (n == null) { + for (const [k, v] of isNull) { + if (v !== i) continue; + if (set.has((k << 2) ^ 1) || set.has((k << 2) ^ 3)) return true; + } + return false; + } + return (idx & 1) === 0 || set.has((n << 2) ^ 2) || set.has((n << 2) ^ 3); + } + minterms = espresso(minterms, dcSet, { canRaise }); + return sopToExpression(minterms, variables); +} + +function mapCallback(exp: Expression): Expression { + if (!Array.isArray(exp)) return exp; + const op = exp[0]; + if (op === "IS NULL") + return (new IsNullSynth(toBoolExprSynth(exp[1])) as unknown) as Expression; + + if (op === "IS NOT NULL") { + return (new NotSynth( + new IsNullSynth(toBoolExprSynth(exp[1])) + ) as unknown) as Expression; + } else if (op === "NOT") { + return (new NotSynth(toBoolExprSynth(exp[1])) as unknown) as Expression; + } else if (op === "OR") { + return (new OrSynth( + ...exp.slice(1).map((a) => toBoolExprSynth(a)) + ) as unknown) as Expression; + } else if (op === "AND") { + return (new AndSynth( + ...exp.slice(1).map((a) => toBoolExprSynth(a)) + ) as unknown) as Expression; + } + for (let i = 1; i < exp.length; ++i) { + if (exp[i] instanceof BoolExprSynth) + exp[i] = boolExprSynthToExpression(exp[i]); + } + return exp; +} + +export function minimize(expr: Expression): Expression { + expr = normalize(expr); + expr = map(expr, mapCallback); + if (expr instanceof BoolExprSynth) return boolExprSynthToExpression(expr); + return expr; +} + +export function unionDiff( + expr1: Expression, + expr2: Expression +): [Expression, Expression] { + expr2 = normalize(expr2); + + if (!expr2) return [expr1, false]; + + expr2 = map(expr2, mapCallback); + + if (!expr1) { + if (expr2 instanceof BoolExprSynth) + expr2 = boolExprSynthToExpression(expr2); + return [expr2, expr2]; + } + + const b2 = toBoolExprSynth(expr2); + expr1 = normalize(expr1); + expr1 = map(expr1, mapCallback); + const b1 = toBoolExprSynth(expr1); + + const context: Map = new Map(); + + const expr2Minterms = b2.true(context); + const expr1Minterms = b1.true(context); + const expr1NullMinterms = b1.null(context); + const expr1FalseMinterms = b1.false(context); + const variables = new Map( + Array.from(context).map(([k, v]) => [v, JSON.parse(k) as Expression]) + ); + const { dcSet, isNull } = generateDcSetAndIsNull(variables); + + const unionMinterms = sanitizeMinterms( + [...expr1Minterms, ...expr2Minterms], + isNull + ); + const diffMinterms = sanitizeMinterms( + complement([ + ...complement([...expr1NullMinterms, ...expr1FalseMinterms]), + ...complement(expr2Minterms), + ]), + isNull + ); + + function canRaise(idx: number, set: Set): boolean { + if (set.size === 1) return true; + const i = idx >>> 2; + const n = isNull.get(i); + if (n == null) { + for (const [k, v] of isNull) { + if (v !== i) continue; + if (set.has((k << 2) ^ 1) || set.has((k << 2) ^ 3)) return true; + } + return false; + } + return (idx & 1) === 0 || set.has((n << 2) ^ 2) || set.has((n << 2) ^ 3); + } + + const union = espresso(unionMinterms, dcSet, { canRaise }); + const diff = espresso(diffMinterms, dcSet, { canRaise }); + + return [sopToExpression(union, variables), sopToExpression(diff, variables)]; +} + +export function covers(expr1: Expression, expr2: Expression): boolean { + expr2 = normalize(expr2); + if (!expr2) return true; + expr1 = normalize(expr1); + if (!Array.isArray(expr1)) return !!expr1; + + expr1 = map(expr1, mapCallback); + const b1 = toBoolExprSynth(expr1); + expr2 = map(expr2, mapCallback); + const b2 = toBoolExprSynth(expr2); + + const context: Map = new Map(); + const expr1Minterms = b1.true(context); + const expr2Minterms = b2.true(context); + const variables = new Map( + Array.from(context).map(([k, v]) => [v, JSON.parse(k) as Expression]) + ); + const { dcSet } = generateDcSetAndIsNull(variables); + + return tautology([...complement(expr2Minterms), ...dcSet, ...expr1Minterms]); +} diff --git a/lib/common/expression-cnf.ts b/lib/common/expression-cnf.ts deleted file mode 100644 index 2aacf75..0000000 --- a/lib/common/expression-cnf.ts +++ /dev/null @@ -1,285 +0,0 @@ -/** - * Copyright 2013-2019 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 . - */ - -import { map, parseLikePattern } from "./expression-parser"; -import { Expression } from "../types"; - -type CNF = number[][]; - -function or(cnf1: CNF, cnf2: CNF): CNF { - if (cnf1.length === 0) return cnf2; - else if (cnf2.length === 0) return cnf1; - - if (cnf1.length > cnf2.length) { - const c = cnf1; - cnf1 = cnf2; - cnf2 = c; - } - - const res = []; - for (let i = 0; i < cnf1.length; ++i) - for (let j = i; j < cnf2.length; ++j) res.push(cnf1[i].concat(cnf2[j])); - - return res; -} - -function likePatternIncludes(pat1, pat2, idx1 = 0, idx2 = 0): boolean { - while (idx1 < pat1.length && idx2 < pat2.length) { - if (pat1[idx1] === "\\%") { - for (let i = idx2; i <= pat2.length; ++i) - if (likePatternIncludes(pat1, pat2, idx1 + 1, i)) return true; - return false; - } else if (pat2[idx2] === "\\%") { - if (pat1[idx1] !== "\\%") return false; - } else if (pat1[idx1] === "\\_") { - // Ignore - } else if (pat2[idx2] === "\\_") { - return false; - } else if (pat2[idx2] !== pat1[idx1]) { - return false; - } - ++idx1; - ++idx2; - } - - if (idx1 === pat1.length && idx2 === pat2.length) return true; - return false; -} - -export function booleanCnf(exp: Expression): { vars: number; clauses: CNF } { - const ranges = new Map(); - const likePatterns = new Map(); - map(exp, (e) => { - if (!Array.isArray(e)) return e; - if (e[0] === "LIKE" || e[0] === "NOT LIKE") { - if ( - typeof e[2] === "string" && - (e.length >= 4 || (e[3] != null && !Array.isArray(e[3]))) - ) { - const key = JSON.stringify(e[1]); - let s = likePatterns.get(key); - if (!s) likePatterns.set(key, (s = new Map())); - s.set(`${e[3] || ""}:${e[2]}`, parseLikePattern(e[2], e[3])); - } - } else if ([">", ">=", "<", "<=", "=", "<>"].includes(e[0])) { - if (!Array.isArray(e[2])) { - const key = `${JSON.stringify(e[1])}:${typeof e[2]}`; - let s = ranges.get(key); - if (!s) ranges.set(key, (s = new Set())); - s.add(e[2]); - } else if (!Array.isArray(e[1])) { - const key = `${JSON.stringify(e[2])}:${typeof e[1]}`; - let s = ranges.get(key); - if (!s) ranges.set(key, (s = new Set())); - s.add(e[2]); - } - } - return e; - }); - - for (const [k, v] of ranges) { - if (k.endsWith(":number")) { - ranges.set( - k, - Array.from(v as number[]).sort((a: number, b: number) => a - b) - ); - } else { - ranges.set(k, Array.from(v).sort()); - } - } - - const expressions: Map = new Map(); - const mutuallyExclusive: Map> = new Map(); - - function getVariable(lhs, op, rhs = ""): number { - const key = `${lhs}:${op}:${rhs}`; - let f = expressions.get(key); - if (!f) { - expressions.set(key, (f = expressions.size + 1)); - let m = mutuallyExclusive.get(lhs); - if (!m) mutuallyExclusive.set(lhs, (m = new Set())); - m.add(f); - if (rhs || op !== "null") m.add(getVariable(lhs, "null")); - } - return f; - } - - function getComparisonVariables( - lhs, - from, - fromInclusive, - to, - toInclusive - ): number[] { - const type = from != null ? typeof from : typeof to; - const range = ranges.get(`${lhs}:${type}`); - const vars = []; - - if (from == null) vars.push(`${lhs}:--${range[0]}`); - - for (let i = 0; i < range.length; ++i) { - if ( - i > 0 && - (from == null || range[i] > from) && - (to == null || range[i] <= to) - ) - vars.push(`${lhs}:${range[i - 1]}--${range[i]}`); - - if ( - (range[i] > from && range[i] < to) || - (range[i] === from && fromInclusive) || - (range[i] === to && toInclusive) - ) - vars.push(`${lhs}:${range[i]}`); - } - - if (to == null) vars.push(`${lhs}:${range[range.length - 1]}--`); - - return vars.map((key) => { - let f = expressions.get(key); - if (!f) { - expressions.set(key, (f = expressions.size + 1)); - let m = mutuallyExclusive.get(lhs); - if (!m) mutuallyExclusive.set(lhs, (m = new Set())); - m.add(f); - } - return f; - }); - } - - function getLikeVariables(lhs, pat, esc): number[] { - const vars = []; - const pats = likePatterns.get(lhs); - pat = pats.get(`${esc || ""}:${pat}`); - for (const p of pats.values()) { - if (pat === p || likePatternIncludes(pat, p)) - vars.push(`${lhs}:like:${JSON.stringify(p)}`); - } - - return vars.map((key) => { - let f = expressions.get(key); - if (!f) expressions.set(key, (f = expressions.size + 1)); - return f; - }); - } - - interface ComparisonOperators { - [name: string]: (v: string) => [string, boolean, string, boolean]; - } - - const comparisonOperators: ComparisonOperators = { - "=": (v) => [v, true, v, true], - ">": (v) => [v, false, null, null], - ">=": (v) => [v, true, null, null], - "<": (v) => [null, null, v, false], - "<=": (v) => [null, null, v, true], - }; - - function recursive(clause, negate): CNF { - let op = clause[0]; - - if ((op === "AND" && !negate) || (op === "OR" && negate)) { - let res = []; - for (let i = 1; i < clause.length; ++i) - res = res.concat(recursive(clause[i], negate)); - return res; - } else if ((op === "OR" && !negate) || (op === "AND" && negate)) { - let res = []; - for (let i = 1; i < clause.length; ++i) - res = or(res, recursive(clause[i], negate)); - return res; - } else if (op === "NOT") { - return recursive(clause[1], !negate); - } else if (op === "<>") { - const vars = getComparisonVariables( - JSON.stringify(clause[1]), - ...comparisonOperators["="](clause[2]) - ); - if (!negate) return vars.map((x) => [0 - x]); - else return [vars]; - } else if (op === "IS NULL") { - const v = getVariable(JSON.stringify(clause[1]), "null"); - if (negate) return [[0 - v]]; - else return [[v]]; - } else if (op === "IS NOT NULL") { - const v = getVariable(JSON.stringify(clause[1]), "null"); - if (!negate) return [[0 - v]]; - else return [[v]]; - } else if (op in comparisonOperators) { - if (!Array.isArray(clause[2])) { - const vars = getComparisonVariables( - JSON.stringify(clause[1]), - ...comparisonOperators[op](clause[2]) - ); - if (negate) return vars.map((x) => [0 - x]); - else return [vars]; - } else if (!Array.isArray(clause[1])) { - op = { ">": "<", ">=": "<=", "<": ">", "<=": ">=" }[op] || op; - const vars = getComparisonVariables( - JSON.stringify(clause[2]), - ...comparisonOperators[op](clause[1]) - ); - if (negate) return vars.map((x) => [0 - x]); - else return [vars]; - } else { - let lhs = JSON.stringify(clause[1]); - let rhs = JSON.stringify(clause[2]); - // For consistency - if (rhs > lhs) { - const t = rhs; - rhs = lhs; - lhs = t; - op = { ">": "<", ">=": "<=", "<": ">", "<=": ">=" }[op] || op; - } - - const v = getVariable(lhs, op, rhs); - if (negate) return [[0 - v]]; - else return [[v]]; - } - } else if ( - (op === "LIKE" || op === "NOT LIKE") && - !Array.isArray(clause[2]) && - clause[2] != null && - (clause.length >= 4 || clause[3] != null) - ) { - if (op === "NOT LIKE") negate = !negate; - const vars = getLikeVariables( - JSON.stringify(clause[1]), - clause[2], - clause[3] - ); - if (negate) return vars.map((x) => [0 - x]); - else return [vars]; - } else { - const v = getVariable(JSON.stringify(clause), ""); - if (negate) return [[0 - v]]; - else return [[v]]; - } - } - - const cnf = recursive(exp, false); - - for (const m of mutuallyExclusive.values()) { - const ar: number[] = Array.from(m); - for (let i = 0; i < ar.length; ++i) - for (let j = i + 1; j < ar.length; ++j) cnf.push([0 - ar[i], 0 - ar[j]]); - } - - return { vars: expressions.size, clauses: cnf }; -} diff --git a/lib/common/expression-parser.ts b/lib/common/expression-parser.ts index 79fbbc2..493330e 100644 --- a/lib/common/expression-parser.ts +++ b/lib/common/expression-parser.ts @@ -17,7 +17,7 @@ * along with GenieACS. If not, see . */ -import * as parsimmon from "parsimmon"; +import parsimmon from "parsimmon"; import { Expression } from "../types"; // Turn escaped characters into real ones (e.g. "\\n" becomes "\n"). diff --git a/lib/common/expression.ts b/lib/common/expression.ts index 703310b..e08b8d7 100644 --- a/lib/common/expression.ts +++ b/lib/common/expression.ts @@ -18,8 +18,6 @@ */ import { map, mapAsync, parseLikePattern } from "./expression-parser"; -import { booleanCnf } from "./expression-cnf"; -import { naiveDpll } from "./sat-solver"; import { Expression } from "../types"; const isArray = Array.isArray; @@ -317,18 +315,6 @@ export function or(exp1: Expression, exp2: Expression): Expression { return res; } -export function not(exp: Expression): Expression { - if (isArray(exp) && exp[0] === "NOT") return exp[1]; - return ["NOT", exp]; -} - -export function subset(exp1: Expression, exp2: Expression): boolean { - const e = evaluate(["NOT", ["OR", ["NOT", exp1], exp2]]); - if (!isArray(e)) return !e; - const { vars, clauses } = booleanCnf(e); - return !naiveDpll(clauses, vars); -} - export function extractParams(exp: Expression): Expression[] { const params = new Set(); map(exp, (e) => { diff --git a/lib/common/sat-solver.ts b/lib/common/sat-solver.ts deleted file mode 100644 index 1744c3a..0000000 --- a/lib/common/sat-solver.ts +++ /dev/null @@ -1,175 +0,0 @@ -/** - * Naive DPLL solver for propositional logic adapted from - * https://github.com/tammet/logictools - * - * Origianl code by Tanel Tammet released under the MIT license. - * - * Check whether a clause set is satisfiable or contradictory, using a naive - * implementation of the dpll (Davis-Putnam-Logemann-Loveland) procedure - * combining truth table search with the resolution-like unit propagation. - * - * The standard pure-literal rule is not implemented in this naive version, - * since it is not really crucial for the algorithm. - * - * The code is very similar to the pure table solver, except we use a - * unit-propagating, derived-varlist-returing satisfiableAt. - */ - -/* eslint-disable @typescript-eslint/no-use-before-define */ - -function satisfiableAt(clauses, varVals, varnr, val): boolean { - if (varnr !== 0) varVals[varnr] = val; - - const propRes = unitPropagate(clauses, varVals); - if (propRes === 1) { - varVals[varnr] = 0; - return true; - } - - // if result false (-1) unitPropagate restores the varVals state itself - if (propRes === -1) { - varVals[varnr] = 0; - return false; - } - - // find next unassigned var to split - let nextVar = 0; - for (let i = 1; i < varVals.length; i++) { - if (varVals[i] === 0) { - nextVar = i; - break; - } - } - - if (nextVar === 0) throw new Error("Error in satisfiableAt"); - - if ( - satisfiableAt(clauses, varVals, nextVar, 1) || - satisfiableAt(clauses, varVals, nextVar, -1) - ) - // not necessary to restore split var: search is halted anyway - return true; - - // restore split var - varVals[nextVar] = 0; - - // restore derived vars - for (let i = 0; i < propRes.length; i++) varVals[propRes[i]] = 0; - - return false; -} - -/** - * Check whether clauses are satisfiable under the varVals assignment, without - * search. - * - * Iterate through all clauses and check whether - * - * - all literals in the clause are assigned false: undo derived units (set - * values in varVals to 0) and return false immediately - * - * - a clause contains a literal assigned true: skip further actions on this - * clause - * - * - a single literal in the clause is unassigned, all the rest are assigned - * false: derive this literal as a unit clause. - * - * In case at least one literal is derived during the process above, iterate - * the whole process until no more new literals are derived. - * - * Returns: - * - * 1: all clauses were assigned true, hence the clause set is satisfiable. - * The whole search will terminate after that. - * - * -1: clause set is contradictory. Derived units have been restored. - * - * a list of derived variables: the status of the clause set is - * undetermined. The values of variables on the list will be restored (set to - * 0) during backtracking. - */ -function unitPropagate(clauses, varVals): number[] | 1 | -1 { - // all vars with a value derived in the forthcoming main loop - const derivedVars = []; - - // the main loop is run, deriving new unit clauses, until either: - // - the clause set is detected to be unsatisfiable - // - the clause set is detected to be satisfiable - // - there are no more derived unit clauses - - for (;;) { - let allClausesFound = true; // set to false if we find an undetermined clause - const derivedQueue = []; // derived units (literals) during one iteration - for (let i = 0; i < clauses.length; i++) { - const clause = clauses[i]; - let clauseVal = 0; - let unassignedCount = 0; // count unassigned vars in clause - let unassignedLit = 0; // 0 means none found for this clause - - for (let j = 0; j < clause.length; j++) { - const lit = clause[j]; - let nr, polarity; - if (lit < 0) { - nr = 0 - lit; - polarity = -1; - } else { - nr = lit; - polarity = 1; - } - - if (varVals[nr] === polarity) { - clauseVal = 1; - break; - } else if (varVals[nr] === 0) { - unassignedCount++; - unassignedLit = lit; - } - } - - if (clauseVal === 1) continue; // clause is subsumed - - // clause is not subsumed by varVals - if (unassignedCount === 0) { - for (let j = 0; j < derivedVars.length; j++) - varVals[derivedVars[j]] = 0; // restore derived - return -1; - } else if (unassignedCount === 1) { - // unassignedLit is a derived literal - derivedQueue.push(unassignedLit); - } - - if (unassignedCount !== 0) allClausesFound = false; - } - - // if all clauses were subsumed or all the variables in a clause had a value - // no need to restore varVals: whole search finished - if (allClausesFound) return 1; - - // in case there are any derived units present, store to varVals and - // iterate the main loop - if (derivedQueue.length === 0) break; - - // some units were derived: iterate the main loop - for (let j = 0; j < derivedQueue.length; j++) { - const lit = derivedQueue[j]; - let nr, polarity; - if (lit < 0) { - nr = 0 - lit; - polarity = -1; - } else { - nr = lit; - polarity = 1; - } - varVals[nr] = polarity; - derivedVars.push(nr); - } - } - - return derivedVars; -} - -export function naiveDpll(clauses: unknown[], maxvarnr: number): boolean { - // variable values are 0 if not set, 1 if positive, -1 if negative - const varVals = new Int32Array(maxvarnr + 1); - return satisfiableAt(clauses, varVals, 0, 0); -} diff --git a/npm-shrinkwrap.json b/npm-shrinkwrap.json index 5221b9b..bb78550 100644 --- a/npm-shrinkwrap.json +++ b/npm-shrinkwrap.json @@ -5302,6 +5302,11 @@ "esprima": "^4.0.0" } }, + "jsbi": { + "version": "3.1.3", + "resolved": "https://registry.npmjs.org/jsbi/-/jsbi-3.1.3.tgz", + "integrity": "sha512-nBJqA0C6Qns+ZxurbEoIR56wyjiUszpNy70FHvxO5ervMoCbZVE3z3kxr5nKGhlxr/9MhKTSUBs7cAwwuf3g9w==" + }, "jsesc": { "version": "2.5.2", "resolved": "https://registry.npmjs.org/jsesc/-/jsesc-2.5.2.tgz", @@ -10474,6 +10479,14 @@ "camelcase": "^4.1.0" } }, + "yebool": { + "version": "1.0.1", + "resolved": "https://registry.npmjs.org/yebool/-/yebool-1.0.1.tgz", + "integrity": "sha512-PrD+4pRGLSS3c8Z+l4V1EUPGUxtqpCDOobldAijBDAgdRHVtrIcDeZ6BFZDKk6QMmGTCCZhbQYdFKSz5fdBXAw==", + "requires": { + "jsbi": "^3.1.3" + } + }, "ylru": { "version": "1.2.1", "resolved": "https://registry.npmjs.org/ylru/-/ylru-1.2.1.tgz", diff --git a/package.json b/package.json index 1979a26..69424f4 100644 --- a/package.json +++ b/package.json @@ -33,7 +33,8 @@ "mongodb": "^3.2.6", "parsimmon": "^1.13.0", "seedrandom": "^3.0.1", - "yaml": "^1.6.0" + "yaml": "^1.6.0", + "yebool": "^1.0.1" }, "devDependencies": { "@rollup/plugin-commonjs": "^14.0.0", @@ -58,6 +59,7 @@ "eslint": "^7.5.0", "eslint-config-prettier": "^6.11.0", "esm": "^3.2.25", + "jsbi": "^3.1.3", "mithril": "^2.0.3", "postcss": "^7.0.17", "postcss-import": "^12.0.1", diff --git a/ui/store.ts b/ui/store.ts index 664096c..f5c627e 100644 --- a/ui/store.ts +++ b/ui/store.ts @@ -19,13 +19,14 @@ import m from "mithril"; import { stringify } from "../lib/common/expression-parser"; -import { or, and, not, evaluate, subset } from "../lib/common/expression"; +import { or, and, evaluate } from "../lib/common/expression"; import memoize from "../lib/common/memoize"; import { QueryOptions, Expression } from "../lib/types"; import * as notifications from "./notifications"; import { configSnapshot, genieacsVersion } from "./config"; import { QueueTask } from "./task-queue"; import { PingResult } from "../lib/ping"; +import { unionDiff, covers } from "../lib/common/boolean-expression"; const memoizedStringify = memoize(stringify); const memoizedEvaluate = memoize(evaluate); @@ -230,25 +231,13 @@ function limitFilter(filter, sort, bookmark): Expression { and(["IS NULL", ["PARAM", param]], cur) ); } - let f = null; - - if (typeof bookmark[param] !== "string") - f = or(f, [">=", ["PARAM", param], ""]); - f = or(f, [">", ["PARAM", param], bookmark[param]]); return or(f, and(["=", ["PARAM", param], bookmark[param]], cur)); } else { let f: Expression = ["IS NULL", ["PARAM", param]]; if (bookmark[param] == null) return and(f, cur); - - if (typeof bookmark[param] !== "number") { - f = or(f, [">=", ["PARAM", param], 0]); - f = or(f, ["<", ["PARAM", param], 0]); - } - f = or(f, ["<", ["PARAM", param], bookmark[param]]); - return or(f, and(["=", ["PARAM", param], bookmark[param]], cur)); } }, true as Expression) @@ -314,10 +303,7 @@ function inferQuery(resourceType, queryResponse): void { const sort = queries.sort.get(queryResponse); if (bookmark || !limit) { if (bookmark) filter = limitFilter(filter, sort, bookmark); - if ( - resources[resourceType].combinedFilter && - subset(filter, resources[resourceType].combinedFilter) - ) + if (covers(resources[resourceType].combinedFilter, filter)) queries.fulfilled.set(queryResponse, fulfillTimestamp); } @@ -475,51 +461,49 @@ export function fulfill( Promise.all(allPromises) .then(() => { const allPromises2 = []; - for (let [resourceType, toFetch] of Object.entries(toFetchAll)) { + for (const [resourceType, toFetch] of Object.entries(toFetchAll)) { let combinedFilter = null; - toFetch = toFetch.filter((queryResponse) => { + for (const queryResponse of toFetch) { let filter = queries.filter.get(queryResponse); - filter = unpackExpression(filter); - const limit = queries.limit.get(queryResponse); + filter = memoizedEvaluate(filter, null, fulfillTimestamp); const bookmark = queries.bookmark.get(queryResponse); const sort = queries.sort.get(queryResponse); if (bookmark) filter = limitFilter(filter, sort, bookmark); + combinedFilter = or(combinedFilter, filter); + } + + const [union, diff] = unionDiff( + resources[resourceType].combinedFilter, + combinedFilter + ); + + if (!diff) { + for (const queryResponse of toFetch) { + let filter = queries.filter.get(queryResponse); + filter = memoizedEvaluate(filter, null, fulfillTimestamp); + const limit = queries.limit.get(queryResponse); + const bookmark = queries.bookmark.get(queryResponse); + const sort = queries.sort.get(queryResponse); + if (bookmark) filter = limitFilter(filter, sort, bookmark); - if ( - resources[resourceType].combinedFilter && - subset(filter, resources[resourceType].combinedFilter) - ) { queries.value.set( queryResponse, findMatches(resourceType, filter, sort, limit) ); queries.fulfilled.set(queryResponse, fulfillTimestamp); queries.fulfilling.delete(queryResponse); - return false; } + continue; + } - combinedFilter = or(combinedFilter, filter); - return true; - }); - - if (combinedFilter == null) continue; + const combinedFilterDiff = diff; + resources[resourceType].combinedFilter = union; updated = true; let deleted = new Set(); if (!resources[resourceType].combinedFilter) deleted = new Set(resources[resourceType].objects.keys()); - let combinedFilterDiff = combinedFilter; - if (resources[resourceType].combinedFilter) { - combinedFilterDiff = and( - combinedFilterDiff, - not(resources[resourceType].combinedFilter) - ); - } - resources[resourceType].combinedFilter = or( - combinedFilter, - resources[resourceType].combinedFilter - ); allPromises2.push( new Promise((resolve2, reject2) => {