SRI-CSL / yices2 / 26463497199

69%

push

github

mcsat: tighten trail cache update and GC sweep loops (#632)

* mcsat: iterate trail elements in trail_update_extra_cache

Replace the two cache-size loops with a single pass over trail->elements.
The old code iterated [0, cache.size) and filtered with trail_has_value;
the set of vars satisfying that filter is exactly trail->elements (modulo
the to_repropagate transient), so direct iteration is equivalent and runs
in O(|trail|) instead of O(|max variable index|). Both cache writes share
one trail_get_value call.

* mcsat: fuse trail_gc_sweep into a single pass

Collapse the three per-cache loops into one iteration over [1, model.size).
Each unmarked variable's marked-set lookup now happens once instead of
three times. Skip the variable_null sentinel (var=0) and drop the dead
trailing assert.

20 of 20 new or added lines in 1 file covered. (100.0%)

87467 of 127158 relevant lines covered (68.79%)

1623934.46 hits per line