1. 18 Sep, 2018 1 commit
  2. 23 Jun, 2018 1 commit
  3. 15 Jun, 2018 2 commits
  4. 14 Jun, 2018 1 commit
  5. 12 Jan, 2018 1 commit
  6. 22 Dec, 2017 1 commit
  7. 15 Dec, 2017 2 commits
  8. 24 Apr, 2017 1 commit
  9. 23 Apr, 2017 1 commit
  10. 11 Apr, 2017 1 commit
  11. 30 Mar, 2017 1 commit
  12. 08 Mar, 2017 1 commit
  13. 07 Mar, 2017 1 commit
    • Clément Fumex's avatar
      + use literals in ieee_float theory · f88de190
      Clément Fumex authored
      + add 'minInt and 'maxInt attributes for range types
      + add 'eb and 'sb attributes for float types
      + make ieee_float realization compatible with Coq 8.4
      f88de190
  14. 28 Feb, 2017 1 commit
  15. 27 Feb, 2017 1 commit
  16. 25 Jan, 2017 1 commit
    • Clément Fumex's avatar
      + remove unused constant half · 5a44ec01
      Clément Fumex authored
      + add predicate "exact_int"
      + add three axioms on of_int +/-/*
      + add some other axioms
      + guard the theory realization with a dependency to flocq in make file
      5a44ec01
  17. 05 Jan, 2017 1 commit
    • Clément Fumex's avatar
      + remove a few wrong axioms · 9a94aeb8
      Clément Fumex authored
      + simplify some others
      + add a realization of real.Truncate
      + add a, almost complete, realization (missing fma related axioms + some non-axiomatized definitions)
      9a94aeb8
  18. 07 Dec, 2016 3 commits
    • Guillaume Melquiond's avatar
    • Guillaume Melquiond's avatar
      4904245a
    • Guillaume Melquiond's avatar
      Fix various inconsistencies in ieee_float. · b406eb6b
      Guillaume Melquiond authored
      The _rev lemmas cannot mention anything about the to_real values. Indeed,
      with a directed rounding, in case of overflow, the result might still be
      finite, yet be unrelated to the infinitely-precise value.
      
      Note that the lemmas were true for rounding to nearest though (since the
      result is necessarily infinite in case of overflow then), so it might be
      worth adding back some specialized versions for rounding to nearest.
      
      Note also that lemmas for neg, abs, and sqrt, do not need fixing, since
      these operations cannot overflow.
      
      This commit also fixes some issues about to_int_monotonic_int. Indeed,
      large integers are not always representable, so we get to_int RNU x = x >
      i for x = of_int RNU i.
      b406eb6b
  19. 29 Nov, 2016 1 commit
  20. 25 Nov, 2016 1 commit
    • Guillaume Melquiond's avatar
      Add lemmas to go from finite floating-point results to finite inputs. · 9ab5761b
      Guillaume Melquiond authored
      When proving a program that does not allow for exceptional behaviors, the
      context is littered with finiteness facts (due to operator preconditions),
      so these lemmas help some provers by reducing the amount of instantiations
      needed to produce the problem on real numbers.
      
      This patch also adds an axiom so that is_finite, is_infinite, and is_nan
      are actually disjoint. It also modifies the axiom about sqrt so that its
      precondition is expressed on real numbers directly.
      9ab5761b
  21. 14 Oct, 2016 1 commit
  22. 05 Oct, 2016 1 commit
  23. 04 Oct, 2016 1 commit
  24. 03 Oct, 2016 1 commit
  25. 29 Sep, 2016 1 commit
  26. 23 Sep, 2016 2 commits
  27. 22 Sep, 2016 2 commits