SRI-CSL / yices2 / 22572764567

71%

push

github

Hardened #589 update + added missing API for building tuple and functional values and setting them in model (#604)

strengthens model-value assignment semantics and extends the API for composite values built from yval_t descriptors.

    Harden yices_model_set_yval
    Enforces that the descriptor refers to a valid value in the same model.
    Enforces descriptor/tag consistency (node_tag must match actual value kind).
    Enforces type compatibility with the target variable before assignment.
    Clarify same-model semantics in docs
    yices_model_set_yval documentation now explicitly states that the value must come from the same model instance.
    Add tuple/function builder APIs from yval_t arrays
    Added:
    yices_model_make_tuple
    yices_model_set_tuple
    yices_model_make_mapping
    yices_model_make_function
    yices_model_set_function
    All these APIs validate model consistency of input descriptors and perform type checks for tuple/function construction.
    Add/extend API tests
    Added negative tests for set_yval tag/type mismatch.
    Added tuple/function construction tests.
    Added examples with algebraic leaves (MCSAT-enabled builds): building tuple and function values from algebraic yval_t values and validating results.

136 of 181 new or added lines in 3 files covered. (75.14%)

82882 of 124796 relevant lines covered (66.41%)

1706826.3 hits per line