Kukovec

In service of multicore, an experiment initially conducted by @konnov , several classes (e.g. cahces) implement serialization features, which are redundant in the current implementation. We need to decide on...

Following the discussion under https://github.com/informalsystems/apalache/pull/2554#discussion_r1189995434, we should consider simplifying the rewriting rules, by making them return `Option`s (or equivalent). Theoretically, this should suffice for the rewriter, under the assumption that...

Document the behavior and expectations of the various caches

7

Currently, it's not very clear what the caches do and where they're written to/read from.

The transition should be done in two steps: 1. Introduce the precomputed arena as an _unused_ argument passed to all of the rewriting rules 2. One-by-one, replace rewriting rules, such...

It may sometimes happen, in a multi-module scenario where module `A` extends or instantiates module `B`, that an operator in `A` has the same name as a bound variable or...

There are multiple heuristics we could use to decide if/when to cache expressions attached to `ElemPtr`s (to avoid introducing unnecessary SMT variables). We should run different heuristics against a suitable...

Create a framework for testing the performance of various encoding methods.

2

In addition to correctness testing via unit- and integration tests, we need to be able to evaluate how different approaches (e.g. interleaving vs flat set-cherrypick) affect performance.

Remove all instances of `assertGroundExpr` for set membership and refer to `ElemPtr.toSmt` in the reconstruction phase instead.

Scrub examples that use recursion from the documentation.

3

A few tutorial/HOWTO sections of the manual use recursive operators/functions in their examples (sometimes section-long running examples). These sections should be rewritten, since recursion is no longer supported, as of...