1. 02 Sep, 2016 1 commit
    • 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
  2. 10 Jun, 2016 1 commit
  3. 15 Mar, 2016 2 commits
  4. 11 Sep, 2015 1 commit
  5. 22 Jul, 2015 2 commits
  6. 15 Jul, 2015 1 commit
  7. 03 Jun, 2015 1 commit
  8. 26 May, 2015 1 commit
  9. 20 Mar, 2015 1 commit
  10. 19 Mar, 2015 1 commit
  11. 04 Mar, 2015 1 commit
  12. 03 Mar, 2015 1 commit
  13. 25 Feb, 2015 1 commit
  14. 14 Mar, 2014 1 commit
  15. 15 Nov, 2013 1 commit
  16. 08 Nov, 2013 1 commit
  17. 03 Nov, 2013 1 commit
    • Andrei Paskevich's avatar
      allow printers to produce "urgent output" · c0e146fa
      Andrei Paskevich authored
      this is useful to declare on-the-fly a new sort which replaces
      a complex type. Otherwise, the printer has to traverse any term
      twice: first, to detect complex types, second, to print the term.
      c0e146fa
  18. 02 Nov, 2013 1 commit
    • Andrei Paskevich's avatar
      implement printers as memoizing transformations · 9640fb2b
      Andrei Paskevich authored
      also, avoid the "encoding_sort" transformation, if it can be done
      directly in the printer.
      
      On the same example as in the previous commits, this gives 5x
      acceleration together with some memory usage reduction.
      9640fb2b
  19. 06 Mar, 2013 1 commit
  20. 05 Feb, 2013 1 commit
  21. 29 Oct, 2012 1 commit
  22. 26 Oct, 2012 1 commit
  23. 20 Oct, 2012 1 commit
    • Andrei Paskevich's avatar
      simplify copyright headers · 11598d2b
      Andrei Paskevich authored
      + create AUTHORS file
      + fix the linking exception in LICENSE
      + update the "About" in IDE
      + remove the trailing whitespace
      + inflate my scores at Ohloh
      11598d2b
  24. 27 Aug, 2012 2 commits
  25. 20 Aug, 2012 1 commit
    • François Bobot's avatar
      session: metas can be added · 3e20cfe5
      François Bobot authored
        - the symbols that appear in the metas are identified in the xml by
          their position in the task:
          - in which declaration
          - in which definition (if that apply otherwise -1)
          - in which constructor(or case in inductive predicate) (if that apply otherwise -1)
          - in which field (if that apply otherwise -1)
      
        - the md5sum of the prefix of the task that end with the declaration is used to know if the
          symbol have been changed, and if it is obsolete.
      
        - currently metas that contains obsolete symbol are removed.
      3e20cfe5
  26. 16 Aug, 2012 1 commit
  27. 03 Aug, 2012 1 commit
    • François Bobot's avatar
      Documentation: add description to all the registration functions · 29201f7c
      François Bobot authored
       (metas, debug flags, transformations, formats) except for label.
      
      This description is used in --list-*. The description can use any of
      the formatting markup of Format "@ " "@[",...
      
      Transformations can also specify from which metas and labels they
      depend, and add informations about how they are interpreted.
      
      TODO:
        - complete and correct the documentation
        - when a transformation use Trans.on_meta, it should be possible to
          add an interpretation of the metas in the documentation.
        - recover a summary version of --list-* ?
        - be able to export in latex?
      29201f7c
  28. 24 Jul, 2012 1 commit
  29. 09 Apr, 2012 1 commit
  30. 20 Dec, 2011 1 commit
    • Guillaume Melquiond's avatar
      Move Coq realizations from a .ml file to a driver file. · cc79baa8
      Guillaume Melquiond authored
      Note that the file is still generated at compilation time.
      
      The "realized" meta takes two arguments. The first one is the path+name of
      the theory, the second one is the translation of it for the target prover.
      The meta is supposed to be put into a printer file, so there is no
      ambiguity on the target. The second argument can be left empty if it can be
      inferred from the first one.
      
      Note that the first argument is not really satisfactory, since it is
      redundant with the theory part of the driver. Moreover, its handling is a
      bit crude: it does not take into account rich qualifiers and it does not
      generate proper error messages if it does not match the theory.
      cc79baa8
  31. 29 Sep, 2011 2 commits
  32. 27 Sep, 2011 1 commit
  33. 18 Sep, 2011 1 commit
  34. 01 Jul, 2011 1 commit
  35. 24 May, 2011 1 commit
  36. 16 May, 2011 1 commit