SRI-CSL / yices2
69%
master: 69%

LAST BUILD BRANCH: reduce-cdclt
DEFAULT BRANCH: master
Repo Added
Files 486
Badge
Embed ▾
README BADGES
x

If you need to use a raster PNG badge, change the '.svg' to '.png' in the link

Markdown

Textile

RDoc

HTML

Rst

LAST BUILD ON BRANCH mcsat-cached-value-tier-fallback
branch: mcsat-cached-value-tier-fallback
CHANGE BRANCH
x

coverage: 68.798% (+0.005%) from 68.793%
26626294772

Pull #634

github

ahmed-irfan 
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 #634: mcsat: fall back to model cache when target cache value is infeasible

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

Relevant lines Covered
127195 RELEVANT LINES 87507 COVERED LINES
1655238.86 HITS PER LINE
Source Files on mcsat-cached-value-tier-fallback

Recent builds

Builds Branch Commit Type Ran Committer Via Coverage
26626294772 mcsat-cached-value-tier-fallback 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 we... Pull #634 ahmed-irfan github
68.8
See All Builds (2006)