SRI-CSL / yices2 / 26471293823

69%

master: 69%

push

github

Wide projection: skip-and-continue on projection error; document model pruning

Two changes prompted by review:

1. Per-cube projection errors no longer break the SAT-guided loop.
   project_one_cube_into can fail on cubes whose literals contain
   term-kinds the projector does not support (in non-MCSAT builds,
   non-linear arithmetic; in any build, unsupported function or
   bitvector applications). The previous behavior was to abort the
   enumeration on the first such failure and OR(collected, local).
   The new behavior drops the failing cube, blocks its implicant, and
   continues: a different SAT-guided implicant may avoid the offending
   literal and project cleanly.

   The iteration budget now bounds total SAT iterations (not just
   successful projections), which is what stops the loop if every
   implicant uses the same bad literal. If no cube ever projects
   successfully, the wide path falls back to gen_model_by_proj_local
   to obtain a definitive error code via the legacy machinery; we are
   not expecting local to succeed in that case.

   Affects gen_model_by_proj_sat_guided. num_cubes is renamed to
   num_attempts to reflect the new semantics. The dead
   "!have_first && exhausted_sat -> push true_term" branch is removed
   (no longer reachable: !have_first now always triggers the local
   fallback).

2. Documentation: model pruning is now spelled out at the file-top
   docstring of generalization.c and in the algorithm section of the
   PR description. The dual precondition-violation paths -- F not
   model-evaluable (-> ABS_ERROR -> local for the error code) versus
   F evaluating to false at the model (-> MDL_EVAL_FORMULA_FALSE
   directly) -- are documented explicitly. The inaccurate claim that
   non-linear arithmetic is a routine projection error is corrected:
   in MCSAT-enabled builds the projector delegates to libpoly and
   non-linearity is not an error.

Builds clean in MODE=release and MODE=debug. check-api: 36/36 pass.

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

88100 of 127678 relevant lines covered (69.0%)

1626561.04 hits per line