1. 01 Feb, 2019 1 commit
  2. 30 Jan, 2019 1 commit
  3. 29 Jan, 2019 1 commit
  4. 23 Jan, 2019 1 commit
    • Sylvain Dailler's avatar
      ce: Add a special case for projected map inside record with one field · 7c318daf
      Sylvain Dailler authored
      Record with one field have a specific treatment in VC generation. The
      combination of this with the projections of first and last elements of
      arrays (that are inside records with one field) were not considered. Hence,
      the necessity of this hackish solution which treat specific case of
      First and Last.
      7c318daf
  5. 20 Dec, 2018 1 commit
    • Sylvain Dailler's avatar
      ce: Adapt counterexamples for API uses · ad0217fa
      Sylvain Dailler authored
      one field record optim: Default name of the record field is taken when an
      empty model_trace is provided.
      Add a registered function allowing removal of some record values before
      displaying to the user.
      ad0217fa
  6. 30 Nov, 2018 1 commit
  7. 22 Oct, 2018 3 commits
    • Sylvain Dailler's avatar
      Treat labels attributes for pretty printing of counterexamples at labels · 215fea13
      Sylvain Dailler authored
      We now use the information inside attributes to correctly associate a
      label to each counterexamples. The information is carried inside
      attributes which are preserved/collected during ce transformations and
      printing to smt2.
      The collection filled during the printing of the task is reused during the
      printing of counterexamples to add "at label" where needed.
      215fea13
    • Sylvain Dailler's avatar
      ce-parsing: Do not confuse constructors with no arguments from variables · c820a81d
      Sylvain Dailler authored
      This is solved by collecting names of constructors with no arguments
      during printing.
      c820a81d
    • Sylvain Dailler's avatar
      In ce collection pass, constants can now have several projections. · da3f5499
      Sylvain Dailler authored
      These projections are necessary because records have changed from
      old system to new system. Previously, a record was never abstract.
      Subsequently, we could always give value to its fields independently.
      Now, when a record (or algebraic type, not handled by this commit) is
      abstract, we use the function defined for its fields as projections.
      So, we need to have several projections per constant in order to represent
      those as values.
      
      This patch is also a first step to the necessary cleaning of ce treatment
      code.
      da3f5499
  8. 24 Jul, 2018 1 commit
  9. 01 Jun, 2018 1 commit
  10. 20 Mar, 2018 1 commit
  11. 19 Mar, 2018 1 commit
  12. 16 Mar, 2018 1 commit
  13. 12 Mar, 2018 1 commit
    • Sylvain Dailler's avatar
      Change the way counterexamples are parsed · 3ea32678
      Sylvain Dailler authored
      The way records are recognized during model parsing is changed:
      we previously recognized records during parsing by looking at the name of
      the variable returned by the prover (mk_r mk__rep etc).
      Now, we collect the names of constructor of records (recognized using
      their id_string beginning with "mk ") during the printing of the smt2
      files. So, after parsing of the model, we can match the name of an
      application with a previously collected constructor: we can recreate
      the record.
      
      The same can be done for all algebraic datatype.
      
      This change also solve the problem of parsing in ce-bench.
      3ea32678
  14. 27 Feb, 2018 1 commit
  15. 21 Feb, 2018 1 commit
  16. 16 Feb, 2018 1 commit
  17. 05 Feb, 2018 1 commit
  18. 19 Jan, 2018 1 commit
  19. 11 Jan, 2018 1 commit
  20. 26 Jun, 2017 1 commit
    • 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
  21. 12 Apr, 2017 2 commits
    • 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
    • MARCHE Claude's avatar
      update header for year 2017 · 216f2ecd
      MARCHE Claude authored
      216f2ecd
  22. 15 Mar, 2016 3 commits
  23. 08 Oct, 2015 1 commit
  24. 06 Oct, 2015 1 commit
  25. 30 Sep, 2015 1 commit
    • David Hauzar's avatar
      Store counterexample information related to VC in a special index. · 924c3f18
      David Hauzar authored
      Since the exact line of the construct that triggers VC may not be
      known, the possibility to map the counterexample information related
      to this construct to dedicated index instead of mapping it to line
      number was added.
      
      Note that the line of the construct that triggers VC is guaranteed to
      be known only if  this construct does not span to multiple lines or if
      the VC is not split.
      924c3f18
  26. 22 Sep, 2015 1 commit
  27. 21 Sep, 2015 1 commit
    • David Hauzar's avatar
      The format of counterexample JSON output changed. · f3aa06e2
      David Hauzar authored
      Model elements in source code line are represented as list of JSON objects
      with attributes "name", "value", and "kind". The attribute "name" is a
      name of a counterexample element, the attribute "value" is the value of
      the counterexample element, and the attribute "kind" is the kind of
      counterexample element, currently one of "old", "result", "error_message",
      and "other".
      f3aa06e2
  28. 07 Sep, 2015 1 commit
  29. 01 Sep, 2015 1 commit
  30. 28 Aug, 2015 1 commit
  31. 30 Jul, 2015 1 commit
  32. 24 Jul, 2015 1 commit
  33. 22 Jul, 2015 1 commit
  34. 16 Jul, 2015 2 commits