apply(::DecisionList) repeats shared path work from extracted tree rules

# `apply(::DecisionList)` repeats shared path work from extracted tree rules

## Summary

On a fixed 60-instance interval workload, applying the 13 paths extracted from one decision tree
made **284,760 `SoleData.checkcondition` calls**. Applying the source `DecisionTree` to the **same
plain logiset** made **97,020** calls — **2.94x** as many (284,760 / 97,020). Predictions were
identical.

For context, applying that same tree to the corresponding **passive** representation made **53,760**
condition calls. The decision-list/passive-tree pairing is **5.30x** (284,760 / 53,760), but
that is not like-for-like: the tree is getting passive data while the rule list is getting a plain
logiset. The passive input is why the tree's count is lower. The fair comparison is 2.94x.

This is a cost issue, not a correctness issue.

## Reproduction and measured versions

Fresh run: Julia **1.12.7**, with these pinned commits:

| package | version | commit |
| --- | ---: | --- |
| SoleModels | 0.10.8 | `c4b98a9c093f811d4c99ca655ed02d95da6543e2` |
| SoleData | 0.16.9 | `bc228ea3abf61bf4487ef49d6a502875f9c8da02` |
| SoleLogics | 0.13.7 | `97a55e44f35a840cd992345107391308aa13fb9f` |
| ModalDecisionTrees | 0.5.4 | `2f618fe1e30f953f9f4cfdfaae50dfc6eaffa9b0` |

I ran:

```text
julia --startup-file=no reproduce_issue_fix.jl
```

The host had 12 CPUs. `uptime` immediately before the run was
`23:06:05 ... load average: 2.90, 3.74, 6.09`; immediately after it was
`23:08:42 ... load average: 3.07, 3.46, 5.62`. The load did not rise materially. I make no timing
claim: these are direct condition counts.

The script inserts a counter at the generic leaf callback immediately before
`checkcondition`; it does not change the condition result. It uses a temporary writable copy of
SoleData. Both measured fair calls receive the same `plain_input` object, created with
`use_full_memoization=false` and no condition/relation memoisation. The passive tree count is a
separate context measurement. Warm-up calls are outside counted regions.

Here is the complete runnable script:

```julia
# Run with: julia --startup-file=no reproduce_issue_fix.jl
# This self-contained script installs the four pinned package commits into a temporary
# environment, instruments a temporary writable SoleData copy, and measures direct
# condition evaluations (not elapsed time).
using Pkg
const env = mktempdir()
Pkg.activate(env)
Pkg.add([
PackageSpec(url="https://github.com/aclai-lab/SoleModels.jl.git", rev="c4b98a9c093f811d4c99ca655ed02d95da6543e2"),
PackageSpec(url="https://github.com/aclai-lab/SoleData.jl.git", rev="bc228ea3abf61bf4487ef49d6a502875f9c8da02"),
PackageSpec(url="https://github.com/aclai-lab/SoleLogics.jl.git", rev="97a55e44f35a840cd992345107391308aa13fb9f"),
PackageSpec(url="https://github.com/aclai-lab/ModalDecisionTrees.jl.git", rev="2f618fe1e30f953f9f4cfdfaae50dfc6eaffa9b0"),
PackageSpec(name="DataFrames"),
])

# Add the counter before loading SoleData. The replacement is deliberately narrow and
# fails loudly if the upstream call shape changes.
sd = only(p for p in values(Pkg.dependencies()) if p.name == "SoleData")
# Package caches may be read-only, so patch a temporary copy and develop that copy.
patched_sd = joinpath(env, "SoleData-instrumented")
cp(sd.source, patched_sd; force=true)
run(`chmod -R u+rw $patched_sd`)
Pkg.develop(PackageSpec(path=patched_sd))
sd = only(p for p in values(Pkg.dependencies()) if p.name == "SoleData")
checkfile = joinpath(sd.source, "src", "check.jl")
text = read(checkfile, String)
needle = "_w->checkcondition(condition, X, i_instance, _w),"
replacement = "_w->(SoleData._REPRO_COUNT[] += 1; checkcondition(condition, X, i_instance, _w)),"
@assert count(needle, text) == 1 "SoleData check.jl call site changed"
text = replace(text, needle => replacement)
modfile = joinpath(sd.source, "src", "SoleData.jl")
modtext = read(modfile, String)
marker = "module SoleData\n"
@assert count(marker, modtext) == 1
modtext = replace(modtext, marker => marker * "const _REPRO_COUNT = Ref(0)\n")
write(checkfile, text)
write(modfile, modtext)

using Random, DataFrames
using SoleLogics, SoleData, SoleModels, ModalDecisionTrees
const MDT = ModalDecisionTrees
using SoleData: ScalarMetaCondition, VariableMin, VariableMax

const N, LEN = 60, 20
const FEATURES = [VariableMin(1), VariableMax(1), VariableMin(2), VariableMax(2)]
const CONDITIONS = [ScalarMetaCondition(f(i), op)
for i in 1:2 for f in (VariableMin, VariableMax) for op in (>=, <=)]
const RELATIONS = [SoleLogics.IA7Relations..., SoleLogics.globalrel]

function dataset(rng, n)
a = [rand(rng, LEN) for _ in 1:n]
b = [rand(rng, LEN) for _ in 1:n]
y = [rand(rng, ["a", "b"]) for _ in 1:n]
DataFrame(V1=a, V2=b), y
end
plain(df) = scalarlogiset(df, FEATURES; use_full_memoization=false)

function plain_formula(f)
f isa SoleData.MultiFormula ? first(values(f.modforms)) : f
end
function antecedent_formula(rule)
f = SoleModels.antecedent(rule)
f isa SoleLogics.LeftmostLinearForm ? plain_formula(first(SoleLogics.grandchildren(f))) : plain_formula(f)
end
function formula_set(rule)
Set(SoleLogics.subformulas(antecedent_formula(rule)))
end

function run_count(f)
GC.gc()
SoleData._REPRO_COUNT[] = 0
result = f()
SoleData._REPRO_COUNT[], result
end

# Fixed seeds and training settings. Data construction is outside each measured call.
rng = MersenneTwister(42)
df, labels = dataset(rng, N)
train = scalarlogiset(df, FEATURES; conditions=CONDITIONS, relations=RELATIONS,
use_onestep_memoization=true,
onestep_precompute_globmemoset=true,
onestep_precompute_relmemoset=true)
tree = MDT.build_tree(train, labels; rng=MersenneTwister(1))
sole_tree = MDT.translate(tree)
rules = SoleModels.listrules(sole_tree)
@assert length(rules) == 13 "seed no longer produces 13 rules"
# DecisionList takes all but the final rule as its explicit rulebase and the final rule's
# outcome as default, exactly as the extracted-rule workload does.
list = SoleModels.DecisionList(rules[1:end-1], SoleModels.consequent(rules[end]))
df_new, _ = dataset(MersenneTwister(7), N)
model = MDT.ModalDecisionTree(; relations=:IA7, conditions=[minimum, maximum])
passive, _ = MDT.wrapdataset(df_new, model; passive_mode=true)
# Both fair-comparison calls use this same freshly built plain logiset object.
plain_input = SoleData.MultiLogiset([plain(df_new)])

# Warm-up is separate from counting so compilation is not part of the result.
SoleModels.apply(sole_tree, plain_input)
SoleModels.apply(list, plain_input)
plain_tree_count, plain_tree_pred = run_count(() -> SoleModels.apply(sole_tree, plain_input))
list_count, list_pred = run_count(() -> SoleModels.apply(list, plain_input))
passive_tree_count, passive_tree_pred = run_count(() -> SoleModels.apply(sole_tree, passive))
@assert plain_tree_pred == list_pred
@assert passive_tree_pred == plain_tree_pred

sets = formula_set.(rules)
total = sum(length, sets)
distinct = length(union(sets...))
function occurrence_stats(rules)
prior = Set{Any}()
occurrences = 0
repeated_earlier = 0
for rule in rules
fs = collect(SoleLogics.subformulas(antecedent_formula(rule)))
occurrences += length(fs)
repeated_earlier += count(f -> f in prior, fs)
union!(prior, fs)
end
occurrences, repeated_earlier
end
occurrences, repeated_earlier = occurrence_stats(rules)
function tree_branch_formulas(branch)
result = [plain_formula(branch.antecedent)]
for child in (branch.posconsequent, branch.negconsequent)
child isa SoleModels.Branch && append!(result, tree_branch_formulas(child))
end
result
end
tree_formulas = tree_branch_formulas(sole_tree.root)
tree_distinct = length(union(Set.(SoleLogics.subformulas.(tree_formulas))...))
# Count syntax leaves that are condition atoms, rather than all formula subnodes.
condition_atom_count(formula) = count(f -> f isa SoleLogics.AbstractAtom,
SoleLogics.subformulas(formula))
rule_condition_atoms = sum(condition_atom_count(antecedent_formula(rule)) for rule in rules)
tree_condition_atoms = sum(condition_atom_count(f) for f in tree_formulas)

println("Julia ", VERSION)
println("SoleModels ", pkgversion(SoleModels),
" | SoleData ", pkgversion(SoleData),
" | SoleLogics ", pkgversion(SoleLogics),
" | ModalDecisionTrees ", pkgversion(MDT))
println("tree_nodes=", MDT.nnodes(tree), " tree_height=", MDT.height(tree),
" rules=", length(rules), " instances=", N)
println("counter tree decision_list")
println("SoleData.checkcondition ", lpad(plain_tree_count, 8), lpad(list_count, 16))
println("ratio decision_list/plain_tree = ", list_count / plain_tree_count)
println("passive_tree_checkcondition = ", passive_tree_count)
println("ratio passive_tree/plain_tree = ", passive_tree_count / plain_tree_count)
println("antecedent subformula occurrences (all occurrences)=", occurrences,
" distinct=", distinct, " repeated-in-earlier-rules=", repeated_earlier,
" occurrences/distinct=", occurrences / distinct)
println("tree-node distinct subformulas=", tree_distinct,
" rule-occurrences/tree-node-distinct (not a condition-count prediction)=", occurrences / tree_distinct)
println("condition-atom occurrences rule-list=", rule_condition_atoms,
" tree-branch-formulas=", tree_condition_atoms,
" static-leaf-occurrence-ratio=", rule_condition_atoms / tree_condition_atoms)
println("predictions_identical=", plain_tree_pred == list_pred == passive_tree_pred)
println("plain_input_is_same_object=true")
println("plain_input_has_no_memoset=true")
```

The fresh output was:

```text
Julia 1.12.7
SoleModels 0.10.8 | SoleData 0.16.9 | SoleLogics 0.13.7 | ModalDecisionTrees 0.5.4
tree_nodes=25 tree_height=7 rules=13 instances=60
counter tree decision_list
SoleData.checkcondition 97020 284760
ratio decision_list/plain_tree = 2.935064935064935
passive_tree_checkcondition = 53760
ratio passive_tree/plain_tree = 0.5541125541125541
antecedent subformula occurrences (all occurrences)=241 distinct=129 repeated-in-earlier-rules=112 occurrences/distinct=1.8682170542635659
tree-node distinct subformulas=48 rule-occurrences/tree-node-distinct (not a condition-count prediction)=5.020833333333333
condition-atom occurrences rule-list=88 tree-branch-formulas=26 static-leaf-occurrence-ratio=3.3846153846153846
predictions_identical=true
plain_input_is_same_object=true
plain_input_has_no_memoset=true
```

## Why I think the repeated work is real

At SoleModels commit `c4b98a9c093f811d4c99ca655ed02d95da6543e2`,
`src/utils/models/other.jl:149-177` applies a decision list sequentially. In particular:

```julia
for rule in rulebase(m)
length(uncovered_idxs) == 0 && break
uncovered_d = slicedataset(d, uncovered_idxs; return_view = true)
idxs_sat = findall(
checkantecedent(rule, uncovered_d, check_args...; check_kwargs...)
)
idxs_sat = uncovered_idxs[idxs_sat]
uncovered_idxs = setdiff(uncovered_idxs, idxs_sat)
end
```

At `src/utils/models/rule-and-branch.jl:477-495`, `checkantecedent` delegates to `check` on the
rule antecedent. At SoleData commit `bc228ea3abf61bf4487ef49d6a502875f9c8da02`,
`src/check.jl:208-214` handles a syntax leaf; line 212 calls
`checkcondition(condition, X, i_instance, _w)`.

`listrules` produces root-to-leaf conjunctions. Thus a prefix decision that is one shared tree
branch appears again in every extracted rule below that branch. The tree can evaluate that
branch at its shared node; the list checks each complete antecedent separately. The list's
`slicedataset` does reduce later work for instances already covered, which is why the dynamic
ratio is not a simple count of all repeated syntax nodes.

## Static analysis, corrected

The earlier `241 / 48 = 5.020833333333333` arithmetic is **not** a valid prediction of the
corrected factor, and I do not use it as corroboration. It counts all syntax nodes against a
tree-node baseline, while the measured counter counts only condition leaves. It also ignores the
shrinking `uncovered_idxs` slices and the passive/plain representation difference.

A fresh leaf-level static proxy counts **88 condition-atom occurrences** in the extracted rules
and **26** in the tree's branch antecedents, or **3.38x** (88 / 26). This is in the
same range as the fresh like-for-like dynamic ratio, but remains an unweighted proxy: sequential
short-circuiting and modal-world traversal make the actual result **2.94x**. The
fresh count of **112 occurrences already seen in earlier rules out of 241 total syntax-subformula
occurrences** directly supports shared-prefix repetition. Overall, the static analysis partly
supports the mechanism, but does not quantitatively predict the measured factor.

## Independent result that is not comparable

A separate batched-evaluation experiment reported a **5.18x** repeated-subformula ratio, but that
was a different extraction-shaped workload and a prototype DAG evaluator: 64 rules at depth 6,
16 instances, 21 worlds per instance, and 704 per-rule DAG-node evaluations over 136 distinct
pooled subformulas. It did not measure this 13-rule/60-instance `SoleData.checkcondition` path.
Its prototype timing was also an evaluator-core experiment, not this API call. I therefore would
not cite that result as corroboration for this issue.

## What is not established

- This is not a correctness bug; the tree and list predictions are identical.
- The 2.94x figure is a direct condition-count result, not an end-to-end wall-clock or allocation
multiplier.
- The factor may differ for other tree shapes, extracted rule sets, frame types, data sizes, or
memoisation settings.
- This does not establish that memoisation interacts with `slicedataset` in a particular way.
- This does not establish that a shared-prefix cache, batched evaluator, or any particular API is
the right fix.
- The separate batched-evaluation prototype does not establish a reachable speedup for this call
path.

Would you be open to checking whether `DecisionList` can reuse shared antecedent/prefix results,
or whether extraction should preserve a tree-shaped evaluation plan? The measured result is a
performance opportunity, not a request for a behavior change.