• Sylvain Dailler's avatar
    P530-020 counterex - Printing quantified variables · 27b053f3
    Sylvain Dailler authored
    We changed the prepare_for_counterexamples transformation to allow
    printing of quantified expressions, remove duplications of printed
    examples and adding an incomplete function to print universally
    quantified variables that are positive but not at head of the term.
    * src/transform/intro_projections_counterexmp.ml
    (intro_const_equal_to_term): Generating of the preid for a counterex.
    * src/transform/intro_projections_counterexmp.mli
    (val_intro_const_equal_to_term): Changing signature.
    * src/transform/intro_vc_vars_counterexmp.ml
    (Hprid): Adding a container for preids.
    (do_intro): Adding cases for generation of counterexample in the Tvar
    case, factorising the construction of vc_constant in a function
    new_counter_example_variable. Adding argument vc_map to avoid
    duplication of vc_constants
    (new_counter_example_variable): Adding a check to avoid duplication of
    (remove_positive_foralls): New experimental incomplete function that aims
    at introducting foralls even when they are under a construct.
    "H /\ forall i. P(i)" becomes "i as premisse and H /\ P(i)".
    (intros): Added calls to do_intro and removed optimizations.
    (do_intro_vc_vars_counterexmp): Concatenate results of intros and
    do_intros and create the prop goal.
    * src/transform/introduction.ml
    (stop_intro): Removed stop_intro.
    * src/transform/prepare_for_counterexmp.ml
    (prepare_for_counterexmp2): Removed call to introduce_premisses.
    Change-Id: I836ae9e69b887247eb64196705cc7ad32ba36825
prepare_for_counterexmp.ml 2.07 KB