1. 25 Aug, 2017 1 commit
  2. 24 Aug, 2017 6 commits
  3. 23 Aug, 2017 10 commits
  4. 22 Aug, 2017 2 commits
  5. 18 Aug, 2017 1 commit
  6. 17 Aug, 2017 1 commit
  7. 14 Jul, 2017 1 commit
  8. 13 Jul, 2017 1 commit
  9. 10 Jul, 2017 3 commits
  10. 06 Jul, 2017 1 commit
  11. 30 Jun, 2017 2 commits
  12. 29 Jun, 2017 2 commits
  13. 28 Jun, 2017 3 commits
  14. 26 Jun, 2017 5 commits
    • Sylvain Dailler's avatar
      Q313-019 Add parsing of hexadecimal for float values · 3f4947b3
      Sylvain Dailler authored
      Formerly we only parsed elements of float values as decimals when they can
      be hexadecimal.
      * src/driver/parse_smtv2_model_lexer.mll
      (float_num): Now takes hexadecimal number instead of decimal numbers.
      Change-Id: Ie3c4e3452c7cb68af8767d2859bfbb4bb90e607e
    • 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
      (convert_float): Dummy conversion of float_type to avoid circular
      * 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
    • Sylvain Dailler's avatar
      Q418-025 Printing arrays with bv indices · 3f732c46
      Sylvain Dailler authored
      This commits allows printing of arrays which have indices typed as
      * src/driver/collect_data_model.ml
      (convert_to_indice): Add bitvector case.
      Change-Id: Iafe10e5e6cd1aab0a3e023aeb69df03fde8880e8
    • Sylvain Dailler's avatar
      Added no_inversion and no_selector for eliminate_algebraic transformations · af6c3d91
      Sylvain Dailler authored
      from a commit by Florian Schanda in 2013 (Spark repo 9b954f4).
    • MARCHE Claude's avatar
  15. 22 Jun, 2017 1 commit