Merge pull request #1481 from informalsystems/romac/trace-insertion-sort

Sort the best traces as we go using insertion sort instead of sorting the whole array each time

quint/src/runtime/trace.ts

@@ -16,6 +16,7 @@ import { EvalResult } from './runtime'
 import { verbosity } from './../verbosity'
 import { Rng } from './../rng'
 import { rv } from './impl/runtimeValue'
+import { insertSorted } from './../util'
 
 /**
  * A snapshot of how a single operator (e.g., an action) was executed.
@@ -329,46 +330,19 @@ class TraceRecorderImpl implements TraceRecorder {
 
     const traceWithSeed = { frame: traceToSave, seed: this.runSeed }
 
-    this.bestTraces.push(traceWithSeed)
-    this.sortTracesByQuality()
-    // Remove the worst trace (if there more traces than needed)
+    // Insert the trace into the list of best traces,
+    // keeping the list sorted by descending quality.
+    this.insertTraceSortedByQuality(traceWithSeed)
+
+    // If there are more traces than needed, remove the worst trace,
+    // ie. the last one, since the traces are sorted by descending quality.
     if (this.bestTraces.length > this.tracesToStore) {
       this.bestTraces.pop()
     }
   }
 
-  private sortTracesByQuality() {
-    const fromResult = (r: Maybe<EvalResult>) => {
-      if (r.isNone()) {
-        return true
-      } else {
-        const rex = r.value.toQuintEx({ nextId: () => 0n })
-        return rex.kind === 'bool' && !rex.value
-      }
-    }
-
-    this.bestTraces.sort((a, b) => {
-      // Prefer short traces for error, and longer traces for non error.
-      // Therefore, trace a is better than trace b iff
-      //  - when a has an error: a is shorter or b has no error;
-      //  - when a has no error: a is longer and b has no error.
-      const aNotOk = fromResult(a.frame.result)
-      const bNotOk = fromResult(b.frame.result)
-      if (aNotOk) {
-        if (bNotOk) {
-          return a.frame.args.length - b.frame.args.length
-        } else {
-          return -1
-        }
-      } else {
-        // a is ok
-        if (bNotOk) {
-          return 1
-        } else {
-          return b.frame.args.length - a.frame.args.length
-        }
-      }
-    })
+  private insertTraceSortedByQuality(trace: Trace) {
+    insertSorted(this.bestTraces, trace, compareTracesByQuality)
   }
 
   // create a bottom frame, which encodes the whole trace
@@ -385,3 +359,37 @@ class TraceRecorderImpl implements TraceRecorder {
     }
   }
 }
+
+// Compare two traces by quality.
+//
+// Prefer short traces for error, and longer traces for non error.
+// Therefore, trace a is better than trace b iff
+//  - when a has an error: a is shorter or b has no error;
+//  - when a has no error: a is longer and b has no error.
+function compareTracesByQuality(a: Trace, b: Trace): number {
+  const fromResult = (r: Maybe<EvalResult>) => {
+    if (r.isNone()) {
+      return true
+    } else {
+      const rex = r.value.toQuintEx({ nextId: () => 0n })
+      return rex.kind === 'bool' && !rex.value
+    }
+  }
+
+  const aNotOk = fromResult(a.frame.result)
+  const bNotOk = fromResult(b.frame.result)
+  if (aNotOk) {
+    if (bNotOk) {
+      return a.frame.args.length - b.frame.args.length
+    } else {
+      return -1
+    }
+  } else {
+    // a is ok
+    if (bNotOk) {
+      return 1
+    } else {
+      return b.frame.args.length - a.frame.args.length
+    }
+  }
+}

quint/src/util.ts

@@ -50,7 +50,7 @@ export function zip<A, B>(a: A[], b: B[]): [A, B][] {
  * otherwise, it is `none`
  *
  * This is like `Array.prototype.find`, except that it works on any iterable and
- * enables trasforming the found value.
+ * enables transforming the found value.
  *
  * Example:
  *
@@ -68,3 +68,47 @@ export function findMap<X, Y>(xs: Iterable<X>, f: (x: X) => Maybe<Y>): Maybe<Y>
   }
   return none<Y>()
 }
+
+/** Insert an item into an array sorted in ascending order by the given comparator.
+ *
+ * Important: The array must be sorted in ascending order.
+ *
+ * Complexity: O(log n)
+ */
+export function insertSorted<A>(array: A[], item: A, cmp: (a: A, b: A) => number): void {
+  if (array.length === 0) {
+    array.push(item)
+    return
+  }
+
+  const index = findInsertionIndex(array, x => cmp(x, item) > 0)
+  array.splice(index, 0, item)
+}
+
+/** Find the first `index` in `array` where the predicate `pred(array[index])` is true.
+ *
+ * Important: The array must be sorted in ascending order.
+ *
+ * Implements a binary search with complexity: O(log n)
+ *
+ * This function is not exported as it is only meant to be used internally by `insertSorted`.
+ */
+function findInsertionIndex<A>(array: A[], pred: (a: A) => boolean): number {
+  var low = 0
+  var high = array.length
+
+  while (low < high) {
+    // Integer version of `Math.floor((low + high) / 2)`
+    const mid = (low + high) >>> 1
+
+    if (pred(array[mid])) {
+      // The element at mid satisfies the predicate, so we need to search to the left
+      high = mid
+    } else {
+      // The element at mid does not satisfy the predicate, so we need to search to the right
+      low = mid + 1
+    }
+  }
+
+  return low
+}

quint/test/util.test.ts

@@ -3,14 +3,14 @@ import { describe, it } from 'mocha'
 
 import { just, none } from '@sweet-monads/maybe'
 
-import { findMap } from '../src/util'
+import { findMap, insertSorted } from '../src/util'
 
 describe('findMap', () => {
   it('is none on empty iterable', () => {
     assert(findMap(new Map().values(), _ => just(42)).isNone(), 'should be none on empty iterable')
   })
 
-  it('is `just` when a vaule can be found', () => {
+  it('is `just` when a value can be found', () => {
     const actual = findMap(
       new Map([
         ['a', 1],
@@ -36,3 +36,44 @@ describe('findMap', () => {
     assert(result.isNone(), 'should be none')
   })
 })
+
+describe('insertSorted', () => {
+  it('can insert into empty array', () => {
+    const array: number[] = []
+    insertSorted(array, 42, (a, b) => a - b)
+    assert.deepEqual([42], array)
+  })
+
+  it('can insert into sorted array', () => {
+    const array = [1, 3, 5]
+    insertSorted(array, 2, (a, b) => a - b)
+    assert.deepEqual([1, 2, 3, 5], array)
+  })
+
+  it('can insert at the beginning of the array', () => {
+    const array = [2, 3, 4]
+    insertSorted(array, 1, (a, b) => a - b)
+    assert.deepEqual([1, 2, 3, 4], array)
+  })
+
+  it('can insert at the end of the array', () => {
+    const array = [1, 2, 3]
+    insertSorted(array, 4, (a, b) => a - b)
+    assert.deepEqual([1, 2, 3, 4], array)
+  })
+
+  it('can insert at the middle of the array', () => {
+    const array = [1, 3, 4]
+    insertSorted(array, 2, (a, b) => a - b)
+    assert.deepEqual([1, 2, 3, 4], array)
+  })
+
+  it('can sort an array of numbers', () => {
+    const array = [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5]
+    var sorted: number[] = []
+    for (const n of array) {
+      insertSorted(sorted, n, (a, b) => a - b)
+    }
+    assert.deepEqual([1, 1, 2, 3, 3, 4, 5, 5, 5, 6, 9], sorted)
+  })
+})