GitLab

why3 -P alt-ergo examples/tests-provers/div.why -T EuclideanDivTest --eval div_m1_2 --eval mod_m1_2 --eval div_1_m2 --eval mod_1_m2 --eval div_m1_m2 --eval mod_m1_m2

why3 -P alt-ergo examples/tests-provers/div.why -T ComputerDivTest --eval div_m1_2 --eval mod_m1_2 --eval div_1_m2 --eval mod_1_m2 --eval div_m1_m2 --eval mod_m1_m2

why3 examples/euler001.mlw --exec Euler001.run

why3 tests/test_exec.mlw --exec M.x --exec M.y
why3 examples/fact.mlw --exec FactRecursive.test42
Signed-off-by: Claude Marche <Claude.Marche@inria.fr>

the term evaluation.

Test with why3 tests/test_exec.mlw --exec M.x

why3 tests/test-eval.why -P alt-ergo -T T --eval i1 --eval i2 --eval let1 --eval c2 --eval c3 --eval c4 --eval c5 --eval c6 --eval c7 --eval l1 --eval l2 --eval l3 --eval l4 --eval l5 --eval l5a --eval l5b --eval l6a --eval l7 --eval l8 --eval l9 --eval l10 --eval l11

why3 tests/test-eval.why -P alt-ergo -T T --eval i1 --eval i2 --eval let1 --eval c2 --eval c3 --eval c4 --eval c5 --eval l1 --eval l2 --eval l3 --eval l4 --eval l5

why3 tests/test-eval.why -P alt-ergo -T T --eval i1 --eval i2 --eval let1 --eval c2 --eval c3 --eval c4 --eval c5 --eval l1 --eval l2 --eval l3

why3 tests/test-eval.why -P alt-ergo -T T --eval c1 --eval c2 --eval c3

This fixes invariant computation for a program symbol whose signature
contains a new tuple symbol. The early call of flush_tuples will miss
the tuple symbols inside specifications, but these do not participate
in invariant computation, and are not a worry. We still have to use
add_pdecl_with_tuples to catch them, though.

this heuristic does not show any real benefit in our tests.
Most of the time we are better off with per-function annotations.

in a series of tests on available examples, lightweight polymorphism
encoding techniques combined with a more agressive generation of
monomorphic instances (via Discriminate) show better results than
our earlier defaults.

In the same commit:
- remove Encoding_explicit (unsound), Encoding_decoexp (too naive),
  and Encoding_instantiate (subsumed by Discriminate)
- rename Encoding_decorate to Encoding_tags_full and Encoding_guard
  to Encoding_guards_full
- move Encoding_guards_full specific functions from Libencoding to
  Encoding_guards_full
- do not apply type protection in "encoding_tptp" and remove
  Protect_finite which is not needed anymore.