-
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