• Sylvain Dailler's avatar
    Q217-025 Use get-model instead of get-values for CE · 1f6da25d
    Sylvain Dailler authored
    This commit allows parsing of the result of get-model from smtsolvers.
    It changes the communication between why3 and Spark for CE to communicate
    records and array as JSON values.
    
     * src/core/model_parser.ml
    (model_value): Adding boolean and record type to model values.
    (print_*): Changed printing functions to print arrays and records as JSON
    values not as strings.
    
     * src/driver/collect_data_model.ml
    (get_variables_*): collect all internal variables of a term and put them
    into a map.
    (add_all_cvc): Add all cvc4 variables in the model to a global map.
    (add_vars_to_table): Add values of variables that can be deduced from ITE
     to the table.
    (corres_else_element): Take the definitions of functions to_rep/of_rep
    and extract the values of internal CVC variables from it.
    (refine_*): Recursively replace internal variables in a term with values
    taken from the table.
    (convert_*): Convert to type model_value from model_parser.ml.
    (create_list): Combine the following to get a list of model_value from
    the parsing of the model.
    
    * src/driver/parse_smtv2_model.ml
    (parse): Changed the detected end of model.
    
    * src/driver/parse_smtv2_model_lexer.mll
    (rule): Added tokens related to model definitions and SPARK definitions of
    records, discriminants and ref.
    
    * src/driver/parse_smtv2_model_parser.mly
    (output): Changed the parser so that it can parse a model as returned by
    Cvc4 or z3.
    
    * src/driver/smt2_model_defs.ml
    (print_*): Added printing functions for terms.
    (make_local*): Changes the AST of terms to differentiate smtsolver
    internal variables, user-defined variables and local variables.
    (subst*): Removes the local let bindings introduced by z3.
    (build_record_discr): Put definitions of discriminants inside the record
    definition.
    
     * src/printer/smtv2.ml
    (print_logic_decl): Removed get-values and added get-model.
    
    * src/transform/intro_projections_counterexmp.ml
    (intro_const_equal_to_term): Only allow projections for attributes first,
    last and field projections. Necessary when the field of a record is
    itself on array on which we want to get First and Last.
    
    * src/transform/intro_vc_vars_counterexmp.ml
    (do_intro): Some definitions moved to intro_projections_counterexmp.ml.
    
    Change-Id: Ib77fb66a2f7c53a9f54cfc300c8984e1fcec8087
    1f6da25d
Makefile.in 69.8 KB