Minimize store queries

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 <http://www.gnu.org/licenses/>.
+ */
+
+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 };

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 <http://www.gnu.org/licenses/>.
+ */
+
+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 };

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 <http://www.gnu.org/licenses/>.
+ */
+
+import * as BI from "./bigint";
+import { espresso, complement, tautology } from "yebool";
+import { Expression } from "../types";
+import { map } from "./expression-parser";
+
+const ZERO = BI.BigInt(0);
+const ONE = BI.BigInt(1);
+const TWO = BI.BigInt(2);
+const NEGATIVE_ONE = BI.BigInt(-1);
+
+class Indeterminates {
+  public map: Map<string, number>;
+  public sortedKeys: string[];
+
+  public constructor(str?: string) {
+    this.map = new Map();
+    if (str) {
+      this.map.set(str, 1);
+      this.sortedKeys = [str];
+    } else {
+      this.sortedKeys = [];
+    }
+  }
+
+  public reciprocal(): Indeterminates {
+    const res = new Indeterminates();
+    res.sortedKeys = this.sortedKeys;
+    res.map = new Map();
+    for (const [k, v] of this.map) res.map.set(k, 0 - v);
+    return res;
+  }
+
+  public static multiply(
+    indeterminates1: Indeterminates,
+    indeterminates2: Indeterminates
+  ): Indeterminates {
+    const res = new Indeterminates();
+    res.sortedKeys = indeterminates1.sortedKeys.slice();
+    res.map = new Map(indeterminates1.map);
+
+    for (const [key, val] of indeterminates2.map) {
+      const v = res.map.get(key);
+      if (!v) {
+        res.map.set(key, val);
+        res.sortedKeys.push(key);
+      } else {
+        const v2 = val + v;
+        if (!v2) {
+          res.map.delete(key);
+          res.sortedKeys = res.sortedKeys.filter((s) => s !== key);
+        } else {
+          res.map.set(key, v2);
+        }
+      }
+    }
+
+    res.sortedKeys.sort((a, b) => {
+      if (a.length !== b.length) return b.length - a.length;
+      else if (a > b) return 1;
+      else if (a < b) return -1;
+      return 0;
+    });
+
+    return res;
+  }
+
+  public static compare(a: Indeterminates, b: Indeterminates): number {
+    if (a.sortedKeys.length !== b.sortedKeys.length)
+      return b.sortedKeys.length - a.sortedKeys.length;
+    for (let i = 0; i < a.sortedKeys.length; ++i) {
+      const k1 = a.sortedKeys[i];
+      const w1 = a.map.get(k1);
+      const k2 = b.sortedKeys[i];
+      const w2 = b.map.get(k2);
+      if (w1 !== w2) return w2 - w1;
+      if (k1.length > k2.length) return -1;
+      else if (k1.length < k2.length) return 1;
+      else if (k1 > k2) return 1;
+      else if (k1 < k2) return -1;
+    }
+    return 0;
+  }
+}
+
+interface Term {
+  indeterminates: Indeterminates;
+  coefficientNumerator: BI.bigint;
+  coefficientDenominator: BI.bigint;
+}
+
+function findGcd(a: BI.bigint, b: BI.bigint): BI.bigint {
+  while (BI.ne(b, ZERO)) {
+    const t = b;
+    b = BI.rem(a, b);
+    a = t;
+  }
+  return a;
+}
+
+class Polynomial {
+  public terms: Term[];
+
+  public constructor(terms: Term[]) {
+    this.terms = terms;
+  }
+
+  public static simplifyTerms(terms: Term[]): Term[] {
+    const ts = terms
+      .slice()
+      .sort((a: Term, b: Term) =>
+        Indeterminates.compare(a.indeterminates, b.indeterminates)
+      );
+
+    for (let i = 1; i < ts.length; ++i) {
+      const t1 = ts[i - 1];
+      const t2 = ts[i];
+      if (Indeterminates.compare(t1.indeterminates, t2.indeterminates) === 0) {
+        const numerator = BI.add(
+          BI.mul(t1.coefficientNumerator, t2.coefficientDenominator),
+          BI.mul(t2.coefficientNumerator, t1.coefficientDenominator)
+        );
+
+        const denominator = BI.mul(
+          t1.coefficientDenominator,
+          t2.coefficientDenominator
+        );
+
+        const gcd = findGcd(numerator, denominator);
+
+        ts[i] = {
+          indeterminates: t2.indeterminates,
+          coefficientNumerator: BI.div(numerator, gcd),
+          coefficientDenominator: BI.div(denominator, gcd),
+        };
+        ts[i - 1] = {
+          indeterminates: t1.indeterminates,
+          coefficientNumerator: ZERO,
+          coefficientDenominator: t1.coefficientDenominator,
+        };
+      }
+    }
+    return ts.filter((v) => BI.ne(v.coefficientNumerator, ZERO));
+  }
+
+  public static fromIndeterminate(indeterminate: Expression): Polynomial {
+    const indeterminates = new Indeterminates(JSON.stringify(indeterminate));
+    const terms = [
+      {
+        indeterminates: indeterminates,
+        coefficientNumerator: ONE,
+        coefficientDenominator: ONE,
+      },
+    ];
+    return new Polynomial(terms);
+  }
+
+  public static fromConstant(constant: number): Polynomial {
+    const [int, frac] = Math.abs(constant).toString(2).split(".", 2);
+    let numerator = BI.BigInt("0b" + int);
+    if (constant < 0) numerator = BI.mul(numerator, NEGATIVE_ONE);
+    let denominator = ONE;
+    if (frac) {
+      denominator = BI.exp(TWO, BI.BigInt(frac.length));
+      numerator = BI.add(
+        BI.mul(numerator, denominator),
+        BI.BigInt("0b" + frac)
+      );
+    }
+
+    const terms = [
+      {
+        indeterminates: new Indeterminates(),
+        coefficientNumerator: numerator,
+        coefficientDenominator: denominator,
+      },
+    ];
+
+    return new Polynomial(terms);
+  }
+
+  public negation(): Polynomial {
+    const terms = this.terms.map((t) => ({
+      indeterminates: t.indeterminates,
+      coefficientNumerator: BI.mul(t.coefficientNumerator, NEGATIVE_ONE),
+      coefficientDenominator: t.coefficientDenominator,
+    }));
+
+    return new Polynomial(terms);
+  }
+
+  public reciprocal(): Polynomial {
+    const terms = this.terms.map((t) => ({
+      indeterminates: t.indeterminates.reciprocal(),
+      coefficientNumerator: t.coefficientDenominator,
+      coefficientDenominator: t.coefficientNumerator,
+    }));
+    return new Polynomial(terms);
+  }
+
+  public constant(): Polynomial {
+    const terms = this.terms.filter((t) => !t.indeterminates.sortedKeys.length);
+    return new Polynomial(terms);
+  }
+
+  public add(rhs: Polynomial): Polynomial {
+    return new Polynomial(
+      Polynomial.simplifyTerms(this.terms.concat(rhs.terms))
+    );
+  }
+
+  public subtract(rhs: Polynomial): Polynomial {
+    return this.add(rhs.negation());
+  }
+
+  public multiply(rhs: Polynomial): Polynomial {
+    const terms: Term[] = [];
+
+    for (const t1 of this.terms) {
+      for (const t2 of rhs.terms) {
+        const numerator = BI.mul(
+          t1.coefficientNumerator,
+          t2.coefficientNumerator
+        );
+        const denominator = BI.mul(
+          t1.coefficientDenominator,
+          t2.coefficientDenominator
+        );
+        const gcd = findGcd(numerator, denominator);
+
+        terms.push({
+          indeterminates: Indeterminates.multiply(
+            t1.indeterminates,
+            t2.indeterminates
+          ),
+          coefficientNumerator: BI.div(numerator, gcd),
+          coefficientDenominator: BI.div(denominator, gcd),
+        });
+      }
+    }
+
+    return new Polynomial(Polynomial.simplifyTerms(terms));
+  }
+
+  public divide(rhs: Polynomial): Polynomial {
+    return this.multiply(rhs.reciprocal());
+  }
+
+  public toString(): string {
+    const add: string[] = [];
+    for (const t of this.terms) {
+      const coefficient =
+        BI.toNumber(t.coefficientNumerator) /
+        BI.toNumber(t.coefficientDenominator);
+
+      const mul: string[] = [];
+      if (t.indeterminates.sortedKeys.length) {
+        for (const k of t.indeterminates.sortedKeys) {
+          const w = t.indeterminates.map.get(k);
+          for (let i = Math.abs(w); i > 0; --i) {
+            if (w > 0) mul.push(k);
+            else mul.push(`["/",1,${k}]`);
+          }
+        }
+
+        if (coefficient !== 1) mul.push(coefficient.toString());
+
+        if (mul.length > 1) add.push(`["*",${mul.join(",")}]`);
+        else add.push(mul["0"]);
+      } else {
+        add.push(coefficient.toString());
+      }
+    }
+
+    if (!add.length) return "0";
+    else if (add.length === 1) return add[0];
+    else return `["+",${add.join(",")}]`;
+  }
+}
+
+type Minterm = number[];
+type Context = Map<string, number>;
+
+abstract class BoolExprSynth {
+  public abstract true(context: Context): Minterm[];
+  public abstract false(context: Context): Minterm[];
+  public abstract null(context: Context): Minterm[];
+}
+
+class TrueSynth extends BoolExprSynth {
+  public true(): Minterm[] {
+    return [[]];
+  }
+  public false(): Minterm[] {
+    return [];
+  }
+  public null(): Minterm[] {
+    return [];
+  }
+}
+
+class FalseSynth extends BoolExprSynth {
+  public true(): Minterm[] {
+    return [];
+  }
+  public false(): Minterm[] {
+    return [[]];
+  }
+  public null(): Minterm[] {
+    return [];
+  }
+}
+
+class NullSynth extends BoolExprSynth {
+  public true(): Minterm[] {
+    return [];
+  }
+  public false(): Minterm[] {
+    return [];
+  }
+  public null(): Minterm[] {
+    return [[]];
+  }
+}
+
+class VarSynth extends BoolExprSynth {
+  private expStr: string;
+  private negate: boolean;
+  public constructor(exp: Expression) {
+    super();
+    this.negate = false;
+    if (Array.isArray(exp)) {
+      const op = exp[0];
+      if (op === "<>") {
+        exp = exp.slice();
+        exp[0] = "=";
+        this.negate = true;
+      } else if (op === ">=") {
+        exp = exp.slice();
+        exp[0] = "<";
+        this.negate = true;
+      } else if (op === "<=") {
+        exp = exp.slice();
+        exp[0] = ">";
+        this.negate = true;
+      }
+    }
+    this.expStr = JSON.stringify(exp);
+  }
+  public true(context: Context): Minterm[] {
+    let v = context.get(this.expStr);
+    if (v == null) context.set(this.expStr, (v = context.size));
+    return [[(v << 2) ^ (this.negate ? 1 : 3)]];
+  }
+  public false(context: Context): Minterm[] {
+    let v = context.get(this.expStr);
+    if (v == null) context.set(this.expStr, (v = context.size));
+    return [[(v << 2) ^ (this.negate ? 3 : 1)]];
+  }
+  public null(context: Context): Minterm[] {
+    let v = context.get(this.expStr);
+    if (v == null) context.set(this.expStr, (v = context.size));
+    return [[v << 2, (v << 2) ^ 2]];
+  }
+}
+
+class NotSynth extends BoolExprSynth {
+  private exprSynth: BoolExprSynth;
+  public constructor(e: BoolExprSynth) {
+    super();
+    this.exprSynth = e;
+  }
+  public true(context: Context): Minterm[] {
+    return this.exprSynth.false(context);
+  }
+  public false(context: Context): Minterm[] {
+    return this.exprSynth.true(context);
+  }
+  public null(context: Context): Minterm[] {
+    return this.exprSynth.null(context);
+  }
+}
+
+class IsNullSynth extends BoolExprSynth {
+  private exprSynth: BoolExprSynth;
+  public constructor(e: BoolExprSynth) {
+    super();
+    this.exprSynth = e;
+  }
+  public true(context: Context): Minterm[] {
+    return this.exprSynth.null(context);
+  }
+  public false(context: Context): Minterm[] {
+    return [...this.exprSynth.true(context), ...this.exprSynth.false(context)];
+  }
+  public null(): Minterm[] {
+    return [];
+  }
+}
+
+class OrSynth extends BoolExprSynth {
+  private exprSynths: BoolExprSynth[];
+  public constructor(...e: BoolExprSynth[]) {
+    super();
+    this.exprSynths = e;
+  }
+  public true(context: Context): Minterm[] {
+    return this.exprSynths.map((e) => e.true(context)).flat();
+  }
+  public false(context: Context): Minterm[] {
+    return complement(
+      this.exprSynths.map((e) => complement(e.false(context))).flat()
+    );
+  }
+  public null(context: Context): Minterm[] {
+    const t = this.exprSynths.map((e) => e.true(context)).flat();
+    const f = this.exprSynths.map((e) => e.false(context)).flat();
+    return complement([...t, ...f]);
+  }
+}
+
+class AndSynth extends BoolExprSynth {
+  private exprSynths: BoolExprSynth[];
+  public constructor(...e: BoolExprSynth[]) {
+    super();
+    this.exprSynths = e;
+  }
+  public true(context: Context): Minterm[] {
+    return complement(
+      this.exprSynths.map((e) => complement(e.true(context))).flat()
+    );
+  }
+  public false(context: Context): Minterm[] {
+    return this.exprSynths.map((e) => e.false(context)).flat();
+  }
+  public null(context: Context): Minterm[] {
+    const t = this.exprSynths.map((e) => e.true(context)).flat();
+    const f = this.exprSynths.map((e) => e.false(context)).flat();
+    return complement([...t, ...f]);
+  }
+}
+
+const ADDITIVE_IDENTITY = Polynomial.fromConstant(0);
+const MULTIPLICATIVE_IDENTITY = Polynomial.fromConstant(1);
+
+const SWAPPED_OPS = {
+  "=": "=",
+  "<>": "<>",
+  ">": "<",
+  ">=": "<=",
+  "<": ">",
+  "<=": ">=",
+};
+
+export function normalize(expr: Expression): Expression {
+  expr = map(expr, (exp) => {
+    if (!Array.isArray(exp)) return exp;
+    const op = exp[0];
+
+    if (op === "+") {
+      const args = exp.slice(1).map((e) => {
+        if (e instanceof Polynomial) return e;
+        else if (typeof e === "number") return Polynomial.fromConstant(e);
+        else return Polynomial.fromIndeterminate(e);
+      });
+      return (args.reduce(
+        (previousValue, currentValue) => previousValue.add(currentValue),
+        ADDITIVE_IDENTITY
+      ) as unknown) as Expression;
+    } else if (op === "*") {
+      const args = exp.slice(1).map((e) => {
+        if (e instanceof Polynomial) return e;
+        else if (typeof e === "number") return Polynomial.fromConstant(e);
+        else return Polynomial.fromIndeterminate(e);
+      });
+
+      return (args.reduce(
+        (previousValue, currentValue) => previousValue.multiply(currentValue),
+        MULTIPLICATIVE_IDENTITY
+      ) as unknown) as Expression;
+    } else if (op === "-") {
+      const args = exp.slice(1).map((e) => {
+        if (e instanceof Polynomial) return e;
+        else if (typeof e === "number") return Polynomial.fromConstant(e);
+        else return Polynomial.fromIndeterminate(e);
+      });
+      return (args.reduce((previousValue, currentValue) =>
+        previousValue.subtract(currentValue)
+      ) as unknown) as Expression;
+    } else if (op === "/") {
+      const args = exp.slice(1).map((e) => {
+        if (e instanceof Polynomial) return e;
+        else if (typeof e === "number") return Polynomial.fromConstant(e);
+        else return Polynomial.fromIndeterminate(e);
+      });
+      return (args.reduce((previousValue, currentValue) =>
+        previousValue.divide(currentValue)
+      ) as unknown) as Expression;
+    } else if (["=", "<>", ">", ">=", "<", "<="].includes(op)) {
+      let lhs: Polynomial, rhs: Polynomial;
+      if (exp[1] instanceof Polynomial) lhs = exp[1];
+      else if (typeof exp[1] === "number")
+        lhs = Polynomial.fromConstant(exp[1]);
+
+      if (exp[2] instanceof Polynomial) rhs = exp[2];
+      else if (typeof exp[2] === "number")
+        rhs = Polynomial.fromConstant(exp[2]);
+
+      if (lhs || rhs) {
+        if (!lhs) lhs = Polynomial.fromIndeterminate(exp[1]);
+        if (!rhs) rhs = Polynomial.fromIndeterminate(exp[2]);
+
+        lhs = lhs.subtract(rhs);
+        rhs = lhs.constant().negation();
+        lhs = lhs.add(rhs);
+
+        if (!lhs.terms.length) {
+          exp = [op, JSON.parse(lhs.toString()), JSON.parse(rhs.toString())];
+
+          if (op === "=") return exp[1] === exp[2];
+          else if (op === "<>") return exp[1] !== exp[2];
+          else if (op === ">") return exp[1] > exp[2];
+          else if (op === ">=") return exp[1] >= exp[2];
+          else if (op === "<") return exp[1] < exp[2];
+          else if (op === "<=") return exp[1] <= exp[2];
+        } else {
+          let flipOp = 1;
+
+          const n = lhs.terms[0].coefficientNumerator;
+          const d = lhs.terms[0].coefficientDenominator;
+
+          if (BI.lt(n, ZERO) || BI.lt(d, ZERO)) flipOp *= -1;
+
+          const reciprocal = new Polynomial([
+            {
+              indeterminates: new Indeterminates(),
+              coefficientNumerator: d,
+              coefficientDenominator: n,
+            },
+          ]);
+
+          lhs = lhs.multiply(reciprocal);
+          rhs = rhs.multiply(reciprocal);
+
+          const keys = lhs.terms[0].indeterminates.sortedKeys;
+          let invert =
+            lhs.terms[0].indeterminates.map.get(keys[0]) < 0 ? -1 : 0;
+
+          for (const t of lhs.terms)
+            for (const v of t.indeterminates.map.values()) invert += v;
+
+          if (invert < 0) {
+            flipOp *= -1;
+            lhs = lhs.reciprocal();
+            rhs = rhs.reciprocal();
+          }
+
+          if (flipOp < 0) exp = [SWAPPED_OPS[op], lhs, rhs];
+          else exp = [op, lhs, rhs];
+        }
+      }
+    }
+
+    // Restore polynomial expressions
+    exp = exp.map((e) =>
+      e instanceof Polynomial ? JSON.parse(e.toString()) : e
+    );
+
+    return exp;
+  });
+
+  if (expr instanceof Polynomial) expr = JSON.parse(expr.toString());
+
+  return expr;
+}
+
+function toBoolExprSynth(e: Expression | BoolExprSynth): BoolExprSynth {
+  if (e instanceof BoolExprSynth) return e;
+  else if (Array.isArray(e)) return new VarSynth(e);
+  else if (e == null) return new NullSynth();
+  else if (e) return new TrueSynth();
+  else return new FalseSynth();
+}
+
+function sopToExpression(
+  sop: number[][],
+  expressions: Map<number, Expression>
+): Expression {
+  if (!sop.length) return false;
+  const res: Expression[] = [];
+  for (const s of sop) {
+    if (!s.length) return true;
+    const and: Expression[] = [];
+    for (const i of s) {
+      let expr = expressions.get(i >>> 2);
+      if (!(i & 1) !== !(i & 2)) expr = ["NOT", expr];
+      if (Array.isArray(expr) && expr[0] === "NOT" && Array.isArray(expr[1])) {
+        const e: Expression[] = expr[1];
+        if (e[0] === "IS NULL") expr = ["IS NOT NULL", ...e.slice(1)];
+        else if (e[0] === "=") expr = ["<>", ...e.slice(1)];
+        else if (e[0] === "<>") expr = ["=", ...e.slice(1)];
+        else if (e[0] === ">") expr = ["<=", ...e.slice(1)];
+        else if (e[0] === ">=") expr = ["<", ...e.slice(1)];
+        else if (e[0] === "<") expr = [">=", ...e.slice(1)];
+        else if (e[0] === "<=") expr = [">", ...e.slice(1)];
+        else if (e[0] === "NOT") expr = e[1];
+        else expr = ["NOT", e];
+      }
+      and.push(expr);
+    }
+    if (and.length > 1) res.push(["AND" as any].concat(and));
+    else res.push(and[0]);
+  }
+  if (res.length > 1) return ["OR" as any].concat(res);
+  return res[0];
+}
+
+function generateDcSetAndIsNull(
+  variables: Map<number, Expression>
+): { dcSet: number[][]; isNull: Map<number, number> } {
+  // TODO support LIKE and NOT LIKE operators
+  const relations: Map<
+    string,
+    { op: string; rhs: boolean | number | string; var: number }[]
+  > = new Map();
+
+  for (const [n, e] of variables) {
+    const op = e[0] as string;
+    if (["=", ">", "<"].includes(op) && !Array.isArray(e[2])) {
+      const lhs = JSON.stringify(e[1]);
+      let r = relations.get(lhs);
+      if (!r) relations.set(lhs, (r = []));
+      r.push({ op: op, rhs: e[2], var: n });
+    } else {
+      const lhs = JSON.stringify(e);
+      let r = relations.get(lhs);
+      if (!r) relations.set(lhs, (r = []));
+      r.push({ op: "", rhs: null, var: n });
+    }
+  }
+
+  const dcSet: number[][] = [];
+  const isNull: Map<number, number> = new Map();
+
+  for (const [key, rels] of relations) {
+    const n = variables.size;
+    variables.set(n, ["IS NULL", JSON.parse(key)]);
+
+    if (key === '["PARAM","DeviceID.ID"]' || key === '["PARAM","_id"]')
+      dcSet.push([(n << 2) ^ 3]);
+
+    const existingOps = new Map() as Map<string, Map<string, number>>;
+    for (const rel of rels) {
+      if (!rel.op) continue;
+      const rhsStr = JSON.stringify(rel.rhs);
+      const s = existingOps.get(rhsStr);
+      if (s) s.set(rel.op, rel.var);
+      else existingOps.set(rhsStr, new Map([[rel.op, rel.var]]));
+    }
+
+    for (const [k, v] of existingOps) {
+      if (v.size > 1) {
+        if (!v.has("=")) {
+          const va = variables.size;
+          variables.set(va, ["=", JSON.parse(key), JSON.parse(k)]);
+          rels.push({ op: "=", rhs: JSON.parse(k), var: va });
+          v.set("=", va);
+        }
+
+        if (!v.has(">")) {
+          const va = variables.size;
+          variables.set(va, [">", JSON.parse(key), JSON.parse(k)]);
+          rels.push({ op: ">", rhs: JSON.parse(k), var: va });
+          v.set(">", va);
+        }
+
+        if (!v.has("<")) {
+          const va = variables.size;
+          variables.set(va, ["<", JSON.parse(key), JSON.parse(k)]);
+          rels.push({ op: "<", rhs: JSON.parse(k), var: va });
+          v.set("<", va);
+        }
+
+        dcSet.push([
+          (v.get("=") << 2) ^ 1,
+          (v.get(">") << 2) ^ 1,
+          (v.get("<") << 2) ^ 1,
+        ]);
+      }
+    }
+
+    for (let i = 0; i < rels.length; ++i) {
+      const rel1 = rels[i];
+      isNull.set(rel1.var, n);
+
+      dcSet.push([(n << 2) ^ 3, (rel1.var << 2) ^ 1]);
+      dcSet.push([(n << 2) ^ 3, (rel1.var << 2) ^ 3]);
+      dcSet.push([(rel1.var << 2) ^ 0, (rel1.var << 2) ^ 2, (n << 2) ^ 2]);
+
+      if (!rel1.op) continue;
+      for (let j = i + 1; j < rels.length; ++j) {
+        const rel2 = rels[j];
+        if (!rel2.op) continue;
+        let comp = 0;
+        if (Array.isArray(rel1.rhs) || Array.isArray(rel2.rhs)) {
+          if (JSON.stringify(rel1.rhs) !== JSON.stringify(rel2.rhs)) continue;
+        } else if (typeof rel1.rhs === "string") {
+          if (typeof rel2.rhs === "string") {
+            if (rel1.rhs > rel2.rhs) comp = 1;
+            else if (rel1.rhs < rel2.rhs) comp = -1;
+          } else {
+            comp = 1;
+          }
+        } else if (typeof rel2.rhs === "string") {
+          comp = -1;
+        } else {
+          comp = +rel1.rhs - +rel2.rhs;
+        }
+
+        if (rel1.op === rel2.op) {
+          if (comp === 0)
+            dcSet.push([(rel1.var << 2) ^ 1, (rel2.var << 2) ^ 1]);
+          else if (rel1.op === "=")
+            dcSet.push([(rel1.var << 2) ^ 3, (rel2.var << 2) ^ 3]);
+          else if (
+            (rel1.op === ">" && comp > 0) ||
+            (rel1.op === "<" && comp < 0)
+          )
+            dcSet.push([(rel1.var << 2) ^ 3, (rel2.var << 2) ^ 1]);
+          else if (
+            (rel1.op === "<" && comp > 0) ||
+            (rel1.op === ">" && comp < 0)
+          )
+            dcSet.push([(rel1.var << 2) ^ 1, (rel2.var << 2) ^ 3]);
+        } else if (rel1.op === "=" || rel2.op === "=") {
+          let r1 = rel1,
+            r2 = rel2,
+            cmp = comp;
+          if (rel1.op !== "=") {
+            r2 = rel1;
+            r1 = rel2;
+            cmp = -comp;
+          }
+          if (r2.op === ">" || r2.op === "<") {
+            if (cmp === 0) {
+              dcSet.push([(r1.var << 2) ^ 3, (r2.var << 2) ^ 3]);
+            } else {
+              if ((cmp > 0 && r2.op === ">") || (cmp < 0 && r2.op === "<"))
+                dcSet.push([(r1.var << 2) ^ 3, (r2.var << 2) ^ 1]);
+              else dcSet.push([(r1.var << 2) ^ 3, (r2.var << 2) ^ 3]);
+            }
+          }
+        } else if (
+          [">", "<"].includes(rel1.op) &&
+          [">", "<"].includes(rel2.op)
+        ) {
+          if ((rel1.op === ">" && comp < 0) || (rel1.op === "<" && comp > 0))
+            dcSet.push([(rel1.var << 2) ^ 1, (rel2.var << 2) ^ 1]);
+          else dcSet.push([(rel1.var << 2) ^ 3, (rel2.var << 2) ^ 3]);
+        }
+      }
+    }
+  }
+
+  return { dcSet, isNull };
+}
+
+function sanitizeMinterms(
+  minterms: number[][],
+  isNull: Map<number, number>
+): number[][] {
+  const res = [] as number[][];
+  loop: for (const m of minterms) {
+    const merged: Map<number, number> = new Map();
+    for (const i of m)
+      merged.set(i >> 2, (merged.get(i >> 2) || 0) | (1 << (i & 3)));
+    const minterm: number[] = [];
+    const perms: number[][] = [];
+    for (const [k, v] of merged) {
+      if (v === 0b1010) continue loop;
+      const n = isNull.get(k) << 2;
+      const t = k << 2;
+      if (v === 0b0101) minterm.push(n ^ 3);
+      else if (v === 0b0001) perms.push([n ^ 3, t ^ 3]);
+      else if (v === 0b0100) perms.push([n ^ 3, t ^ 1]);
+      else if (v & 0b1000) minterm.push(t ^ 3);
+      else if (v & 0b0010) minterm.push(t ^ 1);
+    }
+    let ms = [minterm];
+    while (perms.length) {
+      const newMs: number[][] = [];
+      const perm = perms.pop();
+      for (const p of perm) newMs.push(...ms.map((mm) => [...mm, p]));
+      ms = newMs;
+    }
+    res.push(...ms);
+  }
+  return res;
+}
+
+function boolExprSynthToExpression(boolExpr: BoolExprSynth): Expression {
+  const context: Map<string, number> = new Map();
+  let minterms = boolExpr.true(context);
+  const variables = new Map(
+    Array.from(context).map(([k, v]) => [v, JSON.parse(k) as Expression])
+  );
+  const { dcSet, isNull } = generateDcSetAndIsNull(variables);
+  minterms = sanitizeMinterms(minterms, isNull);
+
+  function canRaise(idx: number, set: Set<number>): boolean {
+    if (set.size === 1) return true;
+    const i = idx >>> 2;
+    const n = isNull.get(i);
+    if (n == null) {
+      for (const [k, v] of isNull) {
+        if (v !== i) continue;
+        if (set.has((k << 2) ^ 1) || set.has((k << 2) ^ 3)) return true;
+      }
+      return false;
+    }
+    return (idx & 1) === 0 || set.has((n << 2) ^ 2) || set.has((n << 2) ^ 3);
+  }
+  minterms = espresso(minterms, dcSet, { canRaise });
+  return sopToExpression(minterms, variables);
+}
+
+function mapCallback(exp: Expression): Expression {
+  if (!Array.isArray(exp)) return exp;
+  const op = exp[0];
+  if (op === "IS NULL")
+    return (new IsNullSynth(toBoolExprSynth(exp[1])) as unknown) as Expression;
+
+  if (op === "IS NOT NULL") {
+    return (new NotSynth(
+      new IsNullSynth(toBoolExprSynth(exp[1]))
+    ) as unknown) as Expression;
+  } else if (op === "NOT") {
+    return (new NotSynth(toBoolExprSynth(exp[1])) as unknown) as Expression;
+  } else if (op === "OR") {
+    return (new OrSynth(
+      ...exp.slice(1).map((a) => toBoolExprSynth(a))
+    ) as unknown) as Expression;
+  } else if (op === "AND") {
+    return (new AndSynth(
+      ...exp.slice(1).map((a) => toBoolExprSynth(a))
+    ) as unknown) as Expression;
+  }
+  for (let i = 1; i < exp.length; ++i) {
+    if (exp[i] instanceof BoolExprSynth)
+      exp[i] = boolExprSynthToExpression(exp[i]);
+  }
+  return exp;
+}
+
+export function minimize(expr: Expression): Expression {
+  expr = normalize(expr);
+  expr = map(expr, mapCallback);
+  if (expr instanceof BoolExprSynth) return boolExprSynthToExpression(expr);
+  return expr;
+}
+
+export function unionDiff(
+  expr1: Expression,
+  expr2: Expression
+): [Expression, Expression] {
+  expr2 = normalize(expr2);
+
+  if (!expr2) return [expr1, false];
+
+  expr2 = map(expr2, mapCallback);
+
+  if (!expr1) {
+    if (expr2 instanceof BoolExprSynth)
+      expr2 = boolExprSynthToExpression(expr2);
+    return [expr2, expr2];
+  }
+
+  const b2 = toBoolExprSynth(expr2);
+  expr1 = normalize(expr1);
+  expr1 = map(expr1, mapCallback);
+  const b1 = toBoolExprSynth(expr1);
+
+  const context: Map<string, number> = new Map();
+
+  const expr2Minterms = b2.true(context);
+  const expr1Minterms = b1.true(context);
+  const expr1NullMinterms = b1.null(context);
+  const expr1FalseMinterms = b1.false(context);
+  const variables = new Map(
+    Array.from(context).map(([k, v]) => [v, JSON.parse(k) as Expression])
+  );
+  const { dcSet, isNull } = generateDcSetAndIsNull(variables);
+
+  const unionMinterms = sanitizeMinterms(
+    [...expr1Minterms, ...expr2Minterms],
+    isNull
+  );
+  const diffMinterms = sanitizeMinterms(
+    complement([
+      ...complement([...expr1NullMinterms, ...expr1FalseMinterms]),
+      ...complement(expr2Minterms),
+    ]),
+    isNull
+  );
+
+  function canRaise(idx: number, set: Set<number>): boolean {
+    if (set.size === 1) return true;
+    const i = idx >>> 2;
+    const n = isNull.get(i);
+    if (n == null) {
+      for (const [k, v] of isNull) {
+        if (v !== i) continue;
+        if (set.has((k << 2) ^ 1) || set.has((k << 2) ^ 3)) return true;
+      }
+      return false;
+    }
+    return (idx & 1) === 0 || set.has((n << 2) ^ 2) || set.has((n << 2) ^ 3);
+  }
+
+  const union = espresso(unionMinterms, dcSet, { canRaise });
+  const diff = espresso(diffMinterms, dcSet, { canRaise });
+
+  return [sopToExpression(union, variables), sopToExpression(diff, variables)];
+}
+
+export function covers(expr1: Expression, expr2: Expression): boolean {
+  expr2 = normalize(expr2);
+  if (!expr2) return true;
+  expr1 = normalize(expr1);
+  if (!Array.isArray(expr1)) return !!expr1;
+
+  expr1 = map(expr1, mapCallback);
+  const b1 = toBoolExprSynth(expr1);
+  expr2 = map(expr2, mapCallback);
+  const b2 = toBoolExprSynth(expr2);
+
+  const context: Map<string, number> = new Map();
+  const expr1Minterms = b1.true(context);
+  const expr2Minterms = b2.true(context);
+  const variables = new Map(
+    Array.from(context).map(([k, v]) => [v, JSON.parse(k) as Expression])
+  );
+  const { dcSet } = generateDcSetAndIsNull(variables);
+
+  return tautology([...complement(expr2Minterms), ...dcSet, ...expr1Minterms]);
+}

lib/common/expression-cnf.ts

@@ -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 <http://www.gnu.org/licenses/>.
- */
-
-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<string, number> = new Map();
-  const mutuallyExclusive: Map<string, Set<number>> = 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 };
-}

lib/common/expression-parser.ts

@@ -17,7 +17,7 @@
  * along with GenieACS.  If not, see <http://www.gnu.org/licenses/>.
  */
 
-import * as parsimmon from "parsimmon";
+import parsimmon from "parsimmon";
 import { Expression } from "../types";
 
 // Turn escaped characters into real ones (e.g. "\\n" becomes "\n").

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<Expression>();
   map(exp, (e) => {

lib/common/sat-solver.ts

@@ -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);
-}