• Sylvain Dailler's avatar
    Q424-012 Parse z3s boolean expression and floating point value · 3a94474f
    Sylvain Dailler authored
    This commit adds parsing for boolean expression and floating point value
    which are returned by z3 on the last version. This adds floating point
    values in the collected data and JSON printed data. This does not add
    boolean expressions because it does not add information.
    Also added transformation eliminate epsilon in driver for Z3 ce.
    
    * drivers/z3_gnatprove_ce.drv
    (eliminate_epsilon): Added transformation eliminate epsilon in driver for
    counterex for z3.
    
    * src/core/model_parser.ml
    (float_type): Added a float_type and functions to send it as JSON data.
    
    * src/driver/collect_data_model.ml
    (convert_array_value): Explicit matching for error handling when adding
    constructs.
    (convert_float): Dummy conversion of float_type to avoid circular
    dependency.
    
    * src/driver/parse_smtv2_model_lexer.mll
    (token): Adding z3 specific boolean expressions. Also adding a way to
    parse all floating point value including those we don't want to print
    because we need to parse them even if we don't want to print them.
    
    * src/driver/parse_smtv2_model_parser.mly
    (smt_term): Adding floating point value case which is handled in the lexer.
    Added boolean_expression case.
    
    * src/driver/smt2_model_defs.ml
    (float_type): Adding a duplicated float_type for dependencies reasons.
    (print_float): Debugging print of float_type.
    (): Adding cases for float in remaining functions.
    
    Change-Id: I5baee2880a9843f0fec61b1bf3edb2a2f3e54bd1
    3a94474f
model_parser.mli 9.79 KB