Generalize store quering functions

common/filter-cnf.js

@@ -0,0 +1,138 @@
+"use strict";
+
+function collectRanges(filter, ranges = new Map()) {
+  if (["AND", "OR", "NOT"].includes(filter[0])) {
+    for (let i = 1; i < filter.length; ++i) collectRanges(filter[i], ranges);
+  } else if ([">", ">=", "<", "<=", "=", "<>"].includes(filter[0])) {
+    const key = `${filter[1]}:${typeof filter[2]}`;
+    let s = ranges.get(key);
+    if (!s) ranges.set(key, (s = new Set()));
+    s.add(filter[2]);
+  }
+  return ranges;
+}
+
+function or(cnf1, cnf2) {
+  if (cnf1.length === 0) return cnf2;
+  else if (cnf2.length === 0) return cnf1;
+
+  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 booleanCnf(filter) {
+  const ranges = collectRanges(filter);
+  for (let [k, v] of ranges)
+    if (k.endsWith(":number"))
+      ranges.set(k, Array.from(v).sort((a, b) => a - b));
+    else ranges.set(k, Array.from(v).sort());
+
+  const expressions = new Map();
+  const mutuallyExclusive = new Map();
+
+  function getIsNullVariable(param) {
+    const key = `${param}:null`;
+    let f = expressions.get(key);
+    if (!f) {
+      expressions.set(key, (f = expressions.size + 1));
+      let m = mutuallyExclusive.get(param);
+      if (!m) mutuallyExclusive.set(param, (m = new Set()));
+      m.add(f);
+    }
+    return f;
+  }
+
+  function getComparisonVariables(param, from, fromInclusive, to, toInclusive) {
+    const type = from != null ? typeof from : typeof to;
+    const range = ranges.get(`${param}:${type}`);
+    const vars = [];
+
+    if (from == null) vars.push(`${param}:--${range[0]}`);
+    if (to == null) vars.push(`${param}:${range[range.length - 1]}--`);
+    if (fromInclusive) vars.push(`${param}:${from}`);
+    if (toInclusive) vars.push(`${param}:${to}`);
+
+    for (let i = 1; i < range.length; ++i)
+      if ((from == null || range[i] > from) && (to == null || range[i] <= to)) {
+        vars.push(`${param}:${range[i - 1]}`);
+        vars.push(`${param}:${range[i]}`);
+        vars.push(`${param}:${range[i - 1]}--${range[i]}`);
+      }
+
+    return vars.map(key => {
+      let f = expressions.get(key);
+      if (!f) {
+        expressions.set(key, (f = expressions.size + 1));
+        let m = mutuallyExclusive.get(param);
+        if (!m) mutuallyExclusive.set(param, (m = new Set()));
+        m.add(f);
+      }
+      return f;
+    });
+  }
+
+  const 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) {
+    const 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 in comparisonOperators) {
+      const vars = getComparisonVariables(
+        clause[1],
+        ...comparisonOperators[op](clause[2])
+      );
+      if (negate) return vars.map(x => [0 - x]);
+      else return [vars];
+    } else if (op === "<>") {
+      const vars = getComparisonVariables(
+        clause[1],
+        ...comparisonOperators["="](clause[2])
+      );
+      if (!negate) return vars.map(x => [0 - x]);
+      else return [vars];
+    } else if (op === "IS NULL") {
+      const v = getIsNullVariable(clause[1]);
+      if (negate) return [[0 - v]];
+      else return [[v]];
+    } else if (op === "IS NOT NULL") {
+      const v = getIsNullVariable(clause[1]);
+      if (!negate) return [[0 - v]];
+      else return [[v]];
+    } else {
+      throw new Error(`Unknown operator ${op}`);
+    }
+  }
+
+  const cnf = recursive(filter, false);
+
+  for (let m of mutuallyExclusive.values()) {
+    let ar = 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 };
+}
+
+exports.booleanCnf = booleanCnf;

common/filter-parser.js

@@ -205,10 +205,6 @@ function parseExpression(exp) {
   return lang.ValueExpression.tryParse(exp);
 }
 
-function parseParameter(p) {
-  return lang.Parameter.tryParse(p);
-}
-
 function stringify(filter) {
   function value(v) {
     if (Array.isArray(v))
@@ -271,54 +267,13 @@ function map(filter, callback) {
       }
     }
 
-  return callback(clone || filter) || clone || filter;
-}
+  let r = callback(clone || filter);
+  if (r != null) return r;
 
-function and(filter1, filter2) {
-  if (!filter1) return filter2;
-  else if (!filter2) return filter1;
-
-  let res = ["AND"];
-
-  if (filter1[0] === "AND") res = res.concat(filter1.slice(1));
-  else res.push(filter1);
-
-  if (filter2[0] === "AND") res = res.concat(filter2.slice(1));
-  else res.push(filter2);
-
-  return res;
-}
-
-function evaluateExpressions(filter, now = Date.now()) {
-  return map(filter, exp => {
-    if (exp[0] === "FUNC" && exp[1] === "NOW") {
-      return now;
-    } else if (exp[0] === "*") {
-      let v = exp[1];
-      for (let i = 2; i < exp.length; ++i) v *= exp[i];
-      return v;
-    } else if (exp[0] === "/") {
-      let v = exp[1];
-      for (let i = 2; i < exp.length; ++i) v /= exp[i];
-      return v;
-    } else if (exp[0] === "+") {
-      let v = exp[1];
-      for (let i = 2; i < exp.length; ++i) v += exp[i];
-      return v;
-    } else if (exp[0] === "-") {
-      let v = exp[1];
-      for (let i = 2; i < exp.length; ++i) v -= exp[i];
-      return v;
-    } else if (exp[0] === "||") {
-      return exp.slice(1).join("");
-    }
-  });
+  return clone || filter;
 }
 
 exports.parse = parse;
 exports.parseExpression = parseExpression;
-exports.parseParameter = parseParameter;
 exports.stringify = stringify;
 exports.map = map;
-exports.and = and;
-exports.evaluateExpressions = evaluateExpressions;

common/filter.js

@@ -0,0 +1,157 @@
+"use strict";
+
+const filterParser = require("./filter-parser");
+const filterCnf = require("./filter-cnf");
+const satSolver = require("./sat-solver");
+
+function* permute(arr) {
+  if (arr.length <= 1) {
+    for (let i = 0; i < arr[0]; ++i) yield [i];
+    return;
+  }
+
+  let slc = arr.slice(1);
+  for (let i = 0; i < arr[0]; ++i)
+    for (let innerArr of permute(slc)) yield [i].concat(innerArr);
+}
+
+class Filter {
+  constructor(str) {
+    if (Array.isArray(str)) this.ast = str;
+    else if (str instanceof Filter) this.ast = str.ast;
+    else if (!str) this.ast = null;
+    else this.ast = filterParser.parse(str);
+  }
+
+  toString() {
+    if (!this.string)
+      if (this.ast) this.string = filterParser.stringify(this.ast);
+      else this.string = "";
+
+    return this.string;
+  }
+
+  or(fltr) {
+    if (!fltr || !this.ast) return this;
+
+    let f = ["OR"];
+
+    if (this.ast[0] === "OR") f = f.concat(this.ast.slice(1));
+    else f.push(this.ast);
+
+    if (fltr.ast[0] === "OR") f = f.concat(fltr.ast.slice(1));
+    else f.push(fltr.ast);
+
+    return new Filter(f);
+  }
+
+  and(fltr) {
+    if (!fltr) return this;
+    else if (!this.ast) return fltr;
+
+    let f = ["AND"];
+
+    if (this.ast[0] === "AND") f = f.concat(this.ast.slice(1));
+    else f.push(this.ast);
+
+    if (fltr.ast[0] === "AND") f = f.concat(fltr.ast.slice(1));
+    else f.push(fltr.ast);
+
+    return new Filter(f);
+  }
+
+  not() {
+    if (this.ast[0] === "NOT") return new Filter(this.ast[1]);
+    else return new Filter(["NOT", this.ast]);
+  }
+
+  evaluateExpressions(now = Date.now()) {
+    if (!this.ast) return this;
+    let ast = filterParser.map(this.ast, exp => {
+      if (exp[0] === "FUNC" && exp[1] === "NOW") {
+        return now;
+      } else if (exp[0] === "*") {
+        let v = exp[1];
+        for (let i = 2; i < exp.length; ++i) v *= exp[i];
+        return v;
+      } else if (exp[0] === "/") {
+        let v = exp[1];
+        for (let i = 2; i < exp.length; ++i) v /= exp[i];
+        return v;
+      } else if (exp[0] === "+") {
+        let v = exp[1];
+        for (let i = 2; i < exp.length; ++i) v += exp[i];
+        return v;
+      } else if (exp[0] === "-") {
+        let v = exp[1];
+        for (let i = 2; i < exp.length; ++i) v -= exp[i];
+        return v;
+      } else if (exp[0] === "||") {
+        return exp.slice(1).join("");
+      }
+    });
+
+    if (ast === this.ast) return this;
+    else return new Filter(ast);
+  }
+
+  subset(fltr) {
+    if (!fltr.ast) return true;
+    else if (!this.ast) return false;
+
+    const f = this.not()
+      .or(fltr)
+      .not();
+    const { vars, clauses } = filterCnf.booleanCnf(f.ast);
+    return !satSolver.naiveDpll(clauses, vars);
+  }
+
+  test(obj) {
+    if (!this.ast) return true;
+    return filterParser.map(this.ast, exp => {
+      const op = exp[0];
+
+      if (op === "AND") {
+        for (let i = 1; i < exp.length; ++i) if (!exp[i]) return false;
+        return true;
+      } else if (op === "OR") {
+        for (let i = 1; i < exp.length; ++i) if (exp[i]) return true;
+        return false;
+      } else if (op === "NOT") {
+        return !exp[1];
+      } else if (op === "=") {
+        const val =
+          typeof obj[exp[1]] === "object" ? obj[exp[1]].value[0] : obj[exp[1]];
+        return val === exp[2];
+      } else if (op === "<>") {
+        const val =
+          typeof obj[exp[1]] === "object" ? obj[exp[1]].value[0] : obj[exp[1]];
+        return val !== exp[2];
+      } else if (op === ">=") {
+        const val =
+          typeof obj[exp[1]] === "object" ? obj[exp[1]].value[0] : obj[exp[1]];
+        return typeof val === typeof exp[2] && val >= exp[2];
+      } else if (op === ">") {
+        const val =
+          typeof obj[exp[1]] === "object" ? obj[exp[1]].value[0] : obj[exp[1]];
+        return typeof val === typeof exp[2] && val > exp[2];
+      } else if (op === "<=") {
+        const val =
+          typeof obj[exp[1]] === "object" ? obj[exp[1]].value[0] : obj[exp[1]];
+        return typeof val === typeof exp[2] && val <= exp[2];
+      } else if (op === "<") {
+        const val =
+          typeof obj[exp[1]] === "object" ? obj[exp[1]].value[0] : obj[exp[1]];
+        return typeof val === typeof exp[2] && val < exp[2];
+      } else if (op === "IS NULL") {
+        return obj[exp[1]] == null;
+      } else if (op === "IS NOT NULL") {
+        return obj[exp[1]] != null;
+      } else {
+        throw new Error(`Unsupported operator ${op}`);
+      }
+    });
+  }
+}
+
+module.exports = Filter;

common/sat-solver.js

@@ -0,0 +1,175 @@
+/**
+ * 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.
+ */
+"use strict";
+
+function satisfiableAt(clauses, varVals, varnr, val) {
+  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) {
+  // 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++) {
+        let 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++) {
+      let 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;
+}
+
+function naiveDpll(clauses, maxvarnr) {
+  // 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);
+}
+
+exports.naiveDpll = naiveDpll;