1. 06 Jul, 2017 1 commit
  2. 12 Apr, 2017 2 commits
    • Sylvain Dailler's avatar
      Q217-025 minor typo · cffa3177
      Sylvain Dailler authored
      Change-Id: Id165717756375db150031589740470cc1e08b8ac
      cffa3177
    • 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