SRI-CSL / yices2 / 26469917215

69%

master: 69%

Build Type

Pull #630

github

Committed by disteph

Commit Message

Remove the eager Cartesian wide projection path

gen_model_by_proj_sat_guided semantically subsumes gen_model_by_proj_wide:
every joint cube the syntactic walker would emit is also an implicant of
the polarity-aware Boolean abstraction the SAT-guided enumerator
operates over. The eager path was only reachable from the SAT-guided
front end on abstract_formula_array returning ABS_ERROR, and ABS_ERROR
in turn only fires when a Boolean subterm has no Boolean value in the
given model -- i.e. the API precondition that F be model-true has been
violated. That makes the path effectively unreachable for well-formed
inputs.

Delete the dead code (cube_set_t and its helpers, wide_status_t,
wide_collect_cubes, gen_model_by_proj_wide) and redirect the ABS_ERROR
fallback to gen_model_by_proj_local. Keep WIDE_CUBE_BUDGET and
project_one_cube_into -- both are still used by the SAT-guided path.

Net: -470 lines, no behavior change for well-formed inputs.

Built 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 528 new or added lines in 2 files covered. (76.7%)

97 existing lines in 2 files now uncovered.

88101 of 127683 relevant lines covered (69.0%)

1627033.64 hits per line