Duplicable models: record a model to build independent copies (first step towards multi-threading)

[cprudhom]

Summary

This PR makes a Model duplicable: its construction can be recorded and replayed into independent copies, each of which can be built and solved in its own thread.

It is a first step towards making Choco exploit multi-threaded architectures more easily. Today, a ParallelPortfolio needs the user (or the parsers) to build the same model n times. With this PR, a model is described once and the copies are built concurrently, from a journal shared by all of them. This is also the groundwork for future work: portfolio-level limits, parsers that parse once instead of n times, or other ways of running models in parallel.

The guiding principle: we duplicate a model, not its resolution settings. The search, limits and monitors set on model.getSolver() are not copied.

Model model = Model.record("queens");      // Model.create(...) ≡ new Model(...): nothing recorded
// ... build the model as usual ...
Model copy = model.duplicate();            // an independent copy (not duplicable itself)

ParallelPortfolio portfolio = ParallelPortfolio.of(model, 4);   // model + 3 copies built concurrently
if (portfolio.solve()) {
    Solution s = portfolio.getBestSolution();   // expressed with the variables of `model`
}

What changes

Recording and replay (new package org.chocosolver.solver.spec)

• Model.record(...) creates a RecordingModel that journalizes its construction into a ModelSpec: calls to the factory methods of IModel, posts and unposts, reifications (reify, reifyWith, implies, impliedBy), tasks, hooks, seed, name, objective and groups.
• Only top-level operations are journalized. Decompositions and intermediate variables are rebuilt when the call is replayed.
• RecordingModel is generated at compile time by a new annotation processor (new module choco-codegen, build-time only). New factory methods are therefore covered automatically, and a test checks that every factory over integer and boolean variables is replayed identically.
• Sharing policy between copies:
  • shared: immutable values, and Tuples / HybridTuples / MDDs, which are frozen first (new freeze() methods);
  • copied: arrays, automata and records;
  • rejected: capturing lambdas.
• Whatever cannot be journalized is reported by snapshot() / duplicate() instead of producing a wrong copy.

Custom constraints

• New factory IConstraintFactory.custom(name, vars, propagator), plus a variant with data: custom(name, vars, data, propagator), e.g. model.custom("atMostK", x, 3, PropAtMostK::new). Custom constraints built this way can be duplicated.
• The FlatZinc parser now uses it for BoolSumEq0Reif / BoolSumLeq0Reif.

Portfolio

• ParallelPortfolio.of(model, n): the recorded model is the first worker, plus n-1 copies built concurrently.
• of(model, variants) adds one copy per variant.
• of(spec, n) and of(spec, variants) build all the workers from a ModelSpec.
• getBestSolution() returns the solution expressed with the variables of the recorded model.

Advanced API

• Variant rewrites a spec: seed, settings, search, consistency of allDifferent, table algorithm, added or removed constraints.
• SearchDecl declares a search for each copy, and SpecSolution exchanges solutions between copies.
• SharedObjects is a diagnostic tool that finds mutable objects shared by two models.

Other changes

• Tuples.toMatrix() no longer returns null when the GC has cleared its soft cache.
• FiniteAutomaton.clone() no longer shares its working buffer with the original.
• New assertions check that a constraint or a search strategy only involves variables of its own model.
• RegParser.newModel(...) can be overridden, and RegParser.getModels() returns all the models built by the parser.

Validation

Equivalence: the model built directly, the recorded model and two replayed copies must have the same structure (variables, domains, constraints, propagators, in the same order) and the same search (solutions, nodes, fails). The copies must not share mutable objects.

• 331 instances of the repository: all pass. This is the new test group spec, added to the CI.

• 597 real instances (XCSP 2024 CSP/COP and MiniZinc), one JVM per instance:

  Result	Instances	Detail
  Equivalent	569
  Not journalizable	5	set variables (SETCARD), out of scope
  Out of memory	20	the plain model alone is already huge: e.g., about 5 GB for AircraftAssemblyLine
  Time limit	3

• Unit tests: 1,229 tests in org.chocosolver.solver.spec, which replay every integer and boolean factory method, then the whole 1s group (9,715 tests), with no failure.

Recording overhead: measured on the same 597 real instances (median of 3 runs after warm-up, 6 JVMs in parallel). The figures below are for the 251 instances whose construction takes at least 100 ms.

	Geometric mean	Median	Worst
Building time, recorded / plain	1.017	1.023	2.12 (Takuzu)
duplicate() (replay) / parsing	0.091	0.068	0.97
snapshot() / parsing	—	0.008	0.073
Extra memory of the recorded model	—	+18.5%	+100%

• Time: recording costs about 2%, and a copy is built more than 10 times faster than parsing the instance again.
• Memory: the extra memory is mostly the data kept for the replay. For instance, the tuples of table constraints stay alive in the journal, whereas a plain model releases them once its propagators are built. This is why the worst cases are table-heavy models (WordSquare, +100%). Models made of a very large number of small calls (SAT encodings) also pay for the journal itself.

Limitations and next steps

• Only integer and boolean variables (and tasks) are supported. Set, real and graph variables, as well as getIbexHandler() and removeMinisat(), are reported as not journalizable.
• The resolution settings are not duplicated (search, limits, monitors). Portfolio-level limits and parsers that parse once are left for a follow-up PR.
• Settings mixes modelling and resolution concerns: it should be rationalized in a separate change.

🤖 Generated with Claude Code

[mergify]

This pull request does not currently match the merge queue conditions, so it cannot be queued from here. The box comes back if it matches again.