SRI-CSL / yices2 / 25365016246

67%

master: 67%

Build Type

Pull #606

github

Committed by disteph

Commit Message

mcsat: trace dropped atoms in preprocessor_build_tuple_model

preprocessor_build_tuple_model has three paths along which a
tuple-blasted atom can quietly fail to appear in the reconstructed
model:

  1. one of the blasted leaf variables has no value in the trail,
  2. the function-type merge in merge_blasted_function_value returns
     null_value for one of several structural reasons (leaf value is
     neither a function nor an update object, a map's arity does not
     match the flattened domain, or a sub-call to build_value_from_flat
     could not rebuild a codomain / domain / default value),
  3. the non-function tuple merge in build_value_from_flat itself
     returns null_value.

Under the previous code each of these branches just `continue`'d or
returned null_value and the caller conditionally invoked
model_map_term only on success. A user inspecting (show-model) would
see the atom missing with no signal anywhere as to why.

Emit a short line under the existing "mcsat::preprocess" trace tag at
each drop site:

  - the leaf-missing case in preprocessor_build_tuple_model names the
    atom and the leaf index that is unassigned;
  - merge_blasted_function_value records a short reason string at each
    of its five `goto done` exits (via a local fail_reason variable
    set immediately before the jump), and emits it from the single
    cleanup label; the caller then adds the concrete atom term;
  - the tuple (non-function) branch in preprocessor_build_tuple_model
    names the atom and notes that the leaves did not decompose.

trace_enabled is a no-op in NDEBUG, so release builds pay nothing at
runtime. mcsat_trace_printf and trace_term_ln are already used from
this file under the same tag, so no new headers or dependencies.

No semantic change to the rebuilt model; the 31 api tests and the 8
tuple .ys regressions still pass in debug, sanitize, and release.

Pull Request Pull Request #606: MCSAT: add support for tuples (incl. nested with function types); blasts tuples in input constraints + reconstitutes them in models and interpolants

Coverage Stats

721 of 967 new or added lines in 3 files covered. (74.56%)

65 existing lines in 1 file now uncovered.

84342 of 126103 relevant lines covered (66.88%)

1633298.86 hits per line