• Sylvain Dailler's avatar
    Why3 altergo counterex - Allowing values to be printed for Altergo · a5d0aa0b
    Sylvain Dailler authored
    We added the generation of identifiers for counterex values inside the
    printer of altergo.
    Also added a file to factorize counterex printing functions that are used
    for both altergo and smtv2.
    
    * Makefile.in
    (cntexmp_printer): Factorization file added to Makefile.
    
    * src/driver/parse_smtv2_model_lexer.mll
    (MODEL): Adding model keyword.
    
    * src/driver/parse_smtv2_model_parser.mly
    (output): Added parsing when keyword model is at beginning of the
     output of the prover.
    
    * src/printer/alt_ergo.ml
    Adding info mimicking smtv2.ml inside most printing functions for counterex
    generation.
    
    * src/printer/cntexmp_printer.ml
    Common functions to alt_ergo.ml and smtv2.ml
    
    * src/printer/smtv2.ml
    Removed functions that are factorized into cntexmp_printer.ml
    a5d0aa0b
Name
Last commit
Last update
..
alt_ergo.ml Loading commit data...
alt_ergo.mli Loading commit data...
cntexmp_printer.ml Loading commit data...
cntexmp_printer.mli Loading commit data...
coq.ml Loading commit data...
coq.mli Loading commit data...
cvc3.ml Loading commit data...
cvc3.mli Loading commit data...
gappa.ml Loading commit data...
gappa.mli Loading commit data...
isabelle.ml Loading commit data...
mathematica.ml Loading commit data...
pvs.ml Loading commit data...
simplify.ml Loading commit data...
simplify.mli Loading commit data...
smtv1.ml Loading commit data...
smtv1.mli Loading commit data...
smtv2.ml Loading commit data...
smtv2.mli Loading commit data...
why3printer.ml Loading commit data...
why3printer.mli Loading commit data...
yices.ml Loading commit data...