SRI-CSL / yices2 / 26626294772

69%

master: 69%

Build Type

Pull #634

github

Committed by ahmed-irfan

Commit Message

mcsat: fall back to model cache when target cache value is infeasible

When deciding a value, the feasibility-aware plugins (na, ff, bv, uf) used a
single cached hint (target cache preferred, else model cache). If that value
was infeasible they went straight to a fresh pick, discarding the model
cache's saved phase.

Try both cached tiers in priority order instead: tier 1 (target cache), then
tier 2 (model cache), each checked against the variable's feasible set, before
falling back to a fresh pick. The new behavior only fires when the target value
is present but infeasible and the model value is present, feasible, and
different - every other path is unchanged.

Add trail_get_cached_candidates() to own the priority ordering, NULL-stripping,
and dedup (skip tier 2 when identical to tier 1) in one place; each plugin's
decide path is now a plain loop over the returned candidates with only its own
feasibility predicate. bool_plugin keeps the original combined getter (it has
no feasible set).

Also fix a latent copy-paste assert in mcsat_value_eq (VALUE_LIBPOLY vs
VALUE_RATIONAL comparison asserted v1->type instead of v2->type).

Full regression suite: 1726/1726 pass.

Pull Request Pull Request #634: mcsat: fall back to model cache when target cache value is infeasible

Coverage Stats

33 of 33 new or added lines in 5 files covered. (100.0%)

5 existing lines in 2 files now uncovered.

87507 of 127195 relevant lines covered (68.8%)

1655238.86 hits per line