GitLab

This reverts commit 88191716.

It seems that by default agressive monomorphisation costs too much.
One could be interested, however, in having it as a user-accessible
transformation in IDE.

Produce more monomorphic instances. On the current Why3 examples we
gain more goal than we lose.

fixed Coq printer on mutually recursive functions

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.

 - 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.

Hopefully this solves the problem of unreliable answers from some
provers like Vampire: there is no such answer "unknown" just 0.01
seconds before the time limit anymore

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.

but not use it by default, because of bad caching of smt_encoding
transformations. Because of this, new function symbols appear again
and again, and since we don't forget function symbols in trans-based
printers, we obtain names like at234.

or unknown can be seen as valid...

In addition,
- scan below conjunctions in case there are equalities there too,
- ignore predicate variables and "true" axioms,
- output hypotheses in the proper order,
- explicitly remove NonTrivialRing since it now survives the filtering.

This is getting tedious. There should be a way to drop the content of a
whole theory.

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);
   }
}

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)))));

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)