1. 14 Feb, 2012 4 commits
  2. 13 Feb, 2012 1 commit
  3. 10 Feb, 2012 1 commit
  4. 09 Feb, 2012 1 commit
  5. 03 Feb, 2012 1 commit
  6. 12 Jan, 2012 1 commit
  7. 14 Dec, 2011 1 commit
  8. 13 Dec, 2011 1 commit
  9. 30 Nov, 2011 1 commit
    • François Bobot's avatar
      Revert "cvc3 understand definition" · 7a62e628
      François Bobot authored
       - When the encoding can't encode a definition it transform it into an
         axiom. But it's not the same than before. The differences is that
         eliminate algebraic is before this transformation into axiom and
         not after. So if the definition start with a match, in one case
         that give different nice axioms, and in the other case that
         introduce a match function which is polymorph and not well used by
         provers.
      
         Possible solutions :
         1) make the match function easier to use with some modification to
         its definition and discriminate it.
         2) Eliminate the match function when the encoding tranform a
         definition into axioms.
      
      This reverts commit 1f652980.
      7a62e628
  10. 24 Nov, 2011 1 commit
  11. 15 Nov, 2011 1 commit
  12. 12 Nov, 2011 1 commit
  13. 27 Oct, 2011 1 commit
  14. 26 Oct, 2011 1 commit
  15. 30 Sep, 2011 2 commits
    • Andrei Paskevich's avatar
      add the option --realize to Main · 9ab0704b
      Andrei Paskevich authored
      How to use it:
      
          why3 --realize -D drivers/coq-realize.drv -T real.Real -o .
      
              produces Real.v in the current directory
      
          why3 --realize -D drivers/coq-realize.drv -T real.Real
      
              produces real/Real.v in the loadpath near real.why
              (the directory "real" must exist)
      
      If a realization file is already there, it is passed to
      the printer in order to preserve the proofs.
      
      Instead of -D <driver_file>, you can use -P <prover>,
      if that prover uses a corresponding driver. However,
      the prover itself is not used.
      
      You can only realize theories from the loadpath.
      
      At the moment, coq-realize.drv is the only driver
      capable to realize theories in some sensible way.
      For any other driver, the results may be funny.
      
      Realization of WhyML modules is not possible so far.
      
      Realization may break if you directories and filenames
      contain non-alphanumeric symbols.
      
      The whole thing is in very preliminary stage.
      Use with caution.
      9ab0704b
    • MARCHE Claude's avatar
      alternative timeout regexp for vampire · 75e1e522
      MARCHE Claude authored
      75e1e522
  16. 29 Sep, 2011 2 commits
  17. 28 Sep, 2011 1 commit
  18. 26 Sep, 2011 1 commit
  19. 18 Sep, 2011 2 commits
  20. 16 Sep, 2011 2 commits
  21. 13 Sep, 2011 1 commit
  22. 02 Sep, 2011 1 commit
  23. 31 Aug, 2011 1 commit
  24. 23 Aug, 2011 2 commits
    • Guillaume Melquiond's avatar
    • Guillaume Melquiond's avatar
      Add a new transformation that instantiates the axioms marked with the · 4d7dd217
      Guillaume Melquiond authored
      meta "instantiate : auto" on as many terms as possible.
      
      The transformation is rather naive, since it doesn't look for term
      candidates under quantifiers, if-then-else, let-in, and so on. So it can
      only appear late in the transformation pipe.
      
      It is only enabled for Gappa and its target axioms are the ones that state
      that any floating-point value is bounded. It was the last transformation
      from Why2 still missing in Why3.
      
      Thanks to this transformation, Gappa is now able to prove all the safety
      obligations from the following code, including the ones about division and
      downcast, which is definitely frightening.
      
      /*@ assigns \nothing;
        @ ensures \result == \abs(x);
        @*/
      extern double fabs(double x);
      
      /*@ requires \valid(AB_Ptr) && \valid(CD_Ptr);
        @ assigns *AB_Ptr, *CD_Ptr;
        @ ensures \abs(*AB_Ptr) <= 6.111111e-2;
        @ ensures \abs(*CD_Ptr) <= 6.111111e-2;
        @ */
      void limitValue(float *AB_Ptr, float *CD_Ptr)
      {
         double Fabs_AB, Fabs_CD;
         double max;
      
         Fabs_AB = fabs (*AB_Ptr);
         Fabs_CD = fabs (*CD_Ptr);
      
         max = Fabs_AB;
         if (Fabs_CD > Fabs_AB)  max = Fabs_CD;
      
         if ( max > 6.111111e-2)
         {
            *AB_Ptr = (float) (((*AB_Ptr) * 6.111111e-2) / max);
            *CD_Ptr = (float) (((*CD_Ptr) * 6.111111e-2) / max);
         }
      }
      4d7dd217
  25. 22 Aug, 2011 1 commit
    • Guillaume Melquiond's avatar
      Detect syntax errors in CVC3 files. · a4d0d0fe
      Guillaume Melquiond authored
      Note that CVC3 doesn't care about syntax errors and it will still answer
      valid at the end. Currently, CVC3 chokes on the following kind of
      declarations (Div_mult, Abs_real_pos, and so on).
      
        ASSERT
        (FORALL (x : INT, y : INT, z : INT):PATTERN (div(((x * y) + z), x)):
        (((0 < x) AND ((0 <= y) AND (0 <= z))) => (div(((x * y) + z), x) = (y +
        div(z, x)))));
      a4d0d0fe
  26. 26 Jul, 2011 1 commit
    • Jean-Christophe Filliâtre's avatar
      Coq output: recursive definitions · 59b180cb
      Jean-Christophe Filliâtre authored
      introduced new transformation eliminate_non_struct_recursion for that purpose
      uses Decl.check_termination tomake the check and the pretty-print
      (could probably be improved to avoid 3 calls to check_termination)
      59b180cb
  27. 06 Jul, 2011 1 commit
  28. 05 Jul, 2011 3 commits
  29. 29 Jun, 2011 1 commit
  30. 07 Jun, 2011 1 commit