SRI-CSL / yices2 / 26470694687

69%

master: 69%

Build Type

Pull #630

github

Committed by disteph

Commit Message

Wide model projection: assert on bug paths, expose cube_budget, drop overclaim

Four small changes prompted by review of the SAT-guided enumerator:

1. Assert on SAT-engine bugs. nsat_solve is documented to return only
   STAT_SAT or STAT_UNSAT (solvers/cdcl/new_sat_solver.h); anything else
   is an internal bug. The previous "fall back to local" branch for
   non-SAT/non-UNSAT status is replaced by an assertion. Mid-loop
   projection errors still fall through to OR(collected, local) because
   those are reachable on legitimate inputs (GEN_PROJ_ERROR_NON_LINEAR,
   GEN_PROJ_ERROR_UNSUPPORTED_ARITH_TERM, ...).

2. Expose the cube budget as an argument. gen_model_by_projection and
   generalize_model now take a uint32_t cube_budget parameter; pass 0 to
   use the built-in default (WIDE_CUBE_BUDGET = 1024). The public
   yices_generalize_model stays mode-driven and always passes 0. Callers
   wanting to tune the budget go through the internal C-level entry
   directly.

3. Be honest about the ABS_ERROR fallback. The previous "effectively
   unreachable defensive fallback" comment was misleading: the path IS
   reachable when eval_boolean_at_model can't produce a Boolean value
   for a Boolean subterm (API precondition violated). The fallback to
   gen_model_by_proj_local exists to delegate error-code reporting to
   the legacy pipeline, which surfaces the specific GEN_EVAL_* /
   MDL_EVAL_* code rather than aborting.

4. Drop the overclaim that the wide cell is "truth-invariant". It is
   strictly broader than the local sign-invariant cell whenever F has
   model-satisfied Boolean structure, but it is not in general the full
   model-truth equivalence class: theory-level relationships between
   distinct atoms aren't reasoned about, and XOR_TERM / EQ_TERM are
   opaque leaves today.

No behavior change for well-formed inputs at the default budget. Builds
clean in MODE=release and MODE=debug. check-api: 36/36 pass.

Pull Request Pull Request #630: Add wide (truth-invariant) model generalization mode

Coverage Stats

405 of 545 new or added lines in 2 files covered. (74.31%)

35 existing lines in 1 file now uncovered.

88101 of 127682 relevant lines covered (69.0%)

1626955.69 hits per line