 24 May, 2017 6 commits


MARCHE Claude authored

Guillaume Melquiond authored

Andrei Paskevich authored
Prevent introduce_premises from splitting too aggressively on the lefthand side:  under quantifiers: "forall x. P /\ Q" =/=> "(forall x. P) /\ (forall x. Q)"  matchwith: "match t with A > P  B > Q" =/=> "(t = A > P) /\ (t = B > Q)"  ifthenelse: "if f then P else Q" =/=> "(f > P) /\ (not f > Q)"  equivalence: "P <> Q" =/=> "(P > Q) /\ (Q > P)" Those splits duplicate formulas, hinder readability and do not really simplify anything. Moreover, in case of a split under a quantifier, they create several universal premises for provers to instantiate, instead of just one. TODO: introduce_premises should be able to split under a singlebranch match. However, this requires special treatment in Introduce.dequant, since the pattern should be rather skolemized than used as a condition.

Guillaume Melquiond authored

Guillaume Melquiond authored

Guillaume Melquiond authored

 23 May, 2017 8 commits


Mário Pereira authored

MARCHE Claude authored

MARCHE Claude authored

Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored
Let's see if this helps our provers to instantiate the axiom.

MARCHE Claude authored

JeanChristophe Filliatre authored

 22 May, 2017 9 commits


Andrei Paskevich authored

MARCHE Claude authored

Andrei Paskevich authored
Instead, we put a "stop_split" over the subsequent postcondition under the (begin > end + 1) assumption. When this assumption is unrealizable (strict for), this allows us to discharge the whole branch as a single goal.


MARCHE Claude authored

Andrei Paskevich authored
We will want to use stop_split higher in the VC formulas.

MARCHE Claude authored
Conflicts: examples/fibonacci.mlw examples/fibonacci/why3session.xml examples/fibonacci/why3shapes.gz examples/koda_ruskey/why3session.xml examples/koda_ruskey/why3shapes.gz examples/schorr_waite_via_recursion/why3session.xml examples/schorr_waite_via_recursion/why3shapes.gz examples/testsprovers/bv/why3session.xml examples/testsprovers/bv/why3shapes.gz examples/testsprovers/ieee_float/why3session.xml examples/tree_of_array/why3session.xml examples/tree_of_array/why3shapes.gz examples/vstte12_bfs/why3session.xml examples/vstte12_bfs/why3shapes.gz theories/int.why theories/real.why

MARCHE Claude authored
The underlying Monoid does not need to be commutative, and is indeed not in example fibonacci.mlw

Guillaume Melquiond authored

 21 May, 2017 3 commits


MARCHE Claude authored

MARCHE Claude authored

Guillaume Melquiond authored

 20 May, 2017 2 commits


Andrei Paskevich authored

Andrei Paskevich authored

 19 May, 2017 12 commits


MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

Guillaume Melquiond authored


Martin Clochard authored

JeanChristophe Filliatre authored

MARCHE Claude authored
