1. 01 Jan, 2017 7 commits
  2. 30 Dec, 2016 1 commit
    • Andrei Paskevich's avatar
      slightly change coloring · 2fbef962
      Andrei Paskevich authored
      - builtin Why3 connectors and parens are "Operator", not "Keyword"
      - square brackets are Normal (just like other used-defined ops)
      2fbef962
  3. 27 Dec, 2016 1 commit
  4. 26 Dec, 2016 2 commits
  5. 22 Dec, 2016 1 commit
  6. 21 Dec, 2016 1 commit
  7. 14 Dec, 2016 1 commit
  8. 02 Nov, 2016 1 commit
  9. 27 Oct, 2016 2 commits
  10. 26 Oct, 2016 1 commit
  11. 20 Oct, 2016 1 commit
  12. 19 Oct, 2016 1 commit
  13. 18 Oct, 2016 2 commits
  14. 10 Oct, 2016 1 commit
  15. 07 Oct, 2016 1 commit
  16. 06 Oct, 2016 1 commit
  17. 04 Oct, 2016 1 commit
  18. 03 Oct, 2016 1 commit
  19. 26 Sep, 2016 1 commit
  20. 23 Sep, 2016 1 commit
  21. 08 Sep, 2016 1 commit
  22. 06 Sep, 2016 3 commits
    • Sylvain Dailler's avatar
      Why3 altergo counterex - Allowing values to be printed for Altergo · a5d0aa0b
      Sylvain Dailler authored
      We added the generation of identifiers for counterex values inside the
      printer of altergo.
      Also added a file to factorize counterex printing functions that are used
      for both altergo and smtv2.
      
      * Makefile.in
      (cntexmp_printer): Factorization file added to Makefile.
      
      * src/driver/parse_smtv2_model_lexer.mll
      (MODEL): Adding model keyword.
      
      * src/driver/parse_smtv2_model_parser.mly
      (output): Added parsing when keyword model is at beginning of the
       output of the prover.
      
      * src/printer/alt_ergo.ml
      Adding info mimicking smtv2.ml inside most printing functions for counterex
      generation.
      
      * src/printer/cntexmp_printer.ml
      Common functions to alt_ergo.ml and smtv2.ml
      
      * src/printer/smtv2.ml
      Removed functions that are factorized into cntexmp_printer.ml
      a5d0aa0b
    • Guillaume Melquiond's avatar
      Merge branch 'bugfix/v0.87' · 219c8bb3
      Guillaume Melquiond authored
      219c8bb3
    • Martin Clochard's avatar
      b2ac5f22
  23. 02 Sep, 2016 2 commits
    • Sylvain Dailler's avatar
      Why3 counterex: Changing the way counterex value are get from prover. · 86ebcd21
      Sylvain Dailler authored
      This commit solve a problem raised by Mohamed Iguernlala. If provers give
      more values than asked, the results of counterex becomes inconsistent.
      
      We changed the way corresponding terms are associated to counterex value.
      Now we have a map containing the term corresponding to a counterex asked to
      a prover.
      
      * src/core/model_parser.ml
      (construct_name): Takes a string and create a model_name.
      (build_model_rec): Changed to use term_map which allow a name of asked
      counterex to correspond to the term asked.
      
      * src/core/printer.ml
      (printer_mapping): Changed type of queried_terms to store correspondance
      between names and terms.
      (printer_args): Changed initial value of queried_terms accordingly.
      
      * src/core/smtv2.ml
      (print_info_model): This function now returns the map of names to terms.
      (print_prop_decl): Changed variable model_list accordingly.
      86ebcd21
    • Guillaume Melquiond's avatar
  24. 01 Sep, 2016 3 commits
  25. 31 Aug, 2016 2 commits