• David Hauzar's avatar
    Introducting constants with model labels for variables in the term · 0b53e050
    David Hauzar authored
    triggering VC.
    
    - Transformation intro_vc_vars_counterexamp introduces new constant with
    model labels for every variable in the term that trigger VC and axiom
    that this constant is equal to the variable, finds the position of the
    term that trigger VC, and saves this position in meta (for smtv2
    printer).
    
    - Transformation prepare_for_counterexmp additionally performs the
    transformation intro_vc_vars_counterexamp
    
    - smtv2 printer no longer collects the location of the term that
    triggers VC and does not collect variables in this term in a special
    way. Note that this functionality was not yet completely removed from
    the printer. It will be done so after the transformation
    intro_vc_vars_counterexmp will be tested.
    
    The rationale:
    Variables that should be displayed in counterexample are marked
    by model labels ("model", "model_projected", "model_trace:*").
    
    Variables inside the term that triggers VC should be displayed in
    counterexample for that VC. However, many VCs (tasks) can be generated
    for  a signle *.mlw file and only variables in the term that trigger
    the VC (task) that is currently proven should be displayed. That means
    that the process of selecting variables inside the term that triggers
    VC for counterexample must be done while processing the task. It is
    done by transformation intro_vc_vars_counterexmp. This means that smtv2
    printer no longer has to find the position of the term that triggers
    VC and no longer has to collect variables in this term in a special
    way.
    0b53e050
Makefile.in 62.4 KB