why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2023-11-13T14:55:01+01:00https://gitlab.inria.fr/why3/why3/-/issues/719`Split_vc` takes a lot of time when used in huge context2023-11-13T14:55:01+01:00François Bobot`Split_vc` takes a lot of time when used in huge context`Split_vc` uses substitution which have a bad behavior with huge context.
```
let simplify_intros =
Trans.compose introduce_premises
(Subst.subst_filtered ~subst_proxy:false subst_filter)
let split_vc =
Trans.compo...`Split_vc` uses substitution which have a bad behavior with huge context.
```
let simplify_intros =
Trans.compose introduce_premises
(Subst.subst_filtered ~subst_proxy:false subst_filter)
let split_vc =
Trans.compose_l
(*** do test:
(Trans.compose Simplify_formula.simplify_trivial_wp_quantification
*)
(Trans.compose generalize_intro Split_goal.split_goal_right)
(Trans.singleton simplify_intros)
```
We are trying to create a toy example, but in any case it seems strange that `split_vc` looks at all the task. What is the goal os this substitution?
The lot of time is that a reload in the IDE can take 14min.1.8.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/196Interaction of smt encoding with meta2021-03-13T00:53:06+01:00DAILLER SylvainInteraction of smt encoding with metaHello,
For the support of counterexamples, I am trying to add meta on a polymorphic functions but it seems that the transformation `encoding_smt_if_poly` breaks the meta I introduced when it monomorphizes the function. I would have expe...Hello,
For the support of counterexamples, I am trying to add meta on a polymorphic functions but it seems that the transformation `encoding_smt_if_poly` breaks the meta I introduced when it monomorphizes the function. I would have expected the meta to be adapted (by the transformation) to the generated ident for the monomorphized function.
For example, the following task:
```
function length (array 'a) : int
(* meta my_meta function length *)
```
is translated to:
```
function length ty uni : uni
(* meta my_meta function length1 *)
```
Note that length1 seem to still refer to the first definition whereas it does not appear anymore in the task: its only apparition is in the meta declaration. Is there a way to keep the meta on my monomorphized function or should I find another solution ?Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/741eliminate_if is not robust enough against if in triggers2023-07-18T19:01:30+02:00Guillaume Cluzeleliminate_if is not robust enough against if in triggersWhen Gappa is called, its driver call the transformation `inline_all` and later `eliminate_if`.
```
module M
function f (x : int) : int = if x = 0 then x else x
predicate p (y : bool) = y
axiom x: forall x, y [f x]. p y -> x = f x...When Gappa is called, its driver call the transformation `inline_all` and later `eliminate_if`.
```
module M
function f (x : int) : int = if x = 0 then x else x
predicate p (y : bool) = y
axiom x: forall x, y [f x]. p y -> x = f x
lemma l: forall y. p y
end
```
The combination of the two transformations fails on a such program and we get a message like:
```
internal failure: Failure in transformation eliminate_if
This expression isn't supported:
if x = 0 then x else x
cannot eliminate 'if-then-else' in trigger terms
```
As the transformation fails, it becomes impossible to use Gappa on any program that uses an axiom with a trigger like exposed in the example.
Wouldn't it be possible to remove the trigger in a such case if it is not possible to do something smarter?https://gitlab.inria.fr/why3/why3/-/issues/727bug `eliminate_algebraic` when meta `keep_types` is set2023-01-12T10:42:09+01:00MARCHE Claudebug `eliminate_algebraic` when meta `keep_types` is setWith the following code
```
meta "eliminate_algebraic" "keep_enums"
meta "eliminate_algebraic" "keep_recs"
meta "eliminate_algebraic" "keep_types"
type list = Nil | Cons int list
predicate mem (x:int) (l:list) =
match l with
| Nil...With the following code
```
meta "eliminate_algebraic" "keep_enums"
meta "eliminate_algebraic" "keep_recs"
meta "eliminate_algebraic" "keep_types"
type list = Nil | Cons int list
predicate mem (x:int) (l:list) =
match l with
| Nil -> false
| Cons y r -> x = y \/ mem x r
end
goal g : mem 1 (Cons 2 (Cons 1 Nil))
```
applying the transformation `eliminate_algebraic` fails with error: `cannot prove termination of mem`https://gitlab.inria.fr/why3/why3/-/issues/715improve transformation used by dreal driver2023-09-06T13:46:27+02:00MARCHE Claudeimprove transformation used by dreal driverThe driver for dreal uses a dedicated transformation `keep_only_arithmetic`. The code for this transformation could be made more elegant, more compact, and could support more cases.
For example, this transformation would completely remo...The driver for dreal uses a dedicated transformation `keep_only_arithmetic`. The code for this transformation could be made more elegant, more compact, and could support more cases.
For example, this transformation would completely remove an hypothesis of the form
```
H: not (arith_fact \/ non_arith_fact)
```
whereas it could keep
```
H: not arith_fact
```BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/693Location warning due to overly long argument due to proof bisection2022-10-03T10:23:29+02:00Guillaume MelquiondLocation warning due to overly long argument due to proof bisectionProof bisection introduces a "remove" transformation in the proof session. It has an argument that lists all the useless symbols. This list can contain hundreds of symbols and thus exceeds 4096 characters. In turn, this causes Why3 to sp...Proof bisection introduces a "remove" transformation in the proof session. It has an argument that lists all the useless symbols. This list can contain hundreds of symbols and thus exceeds 4096 characters. In turn, this causes Why3 to spew warnings in the IDE or when replaying sessions, e.g.,
```console
$ bin/why3 replay --merging-only -L examples/multiprecision/ examples/multiprecision/mpz_set_str
Warning: Loc.user_position: end char number `4098` overflows on next line
```
We should not warn about things that are out of the control of the user.https://gitlab.inria.fr/why3/why3/-/issues/677Cannot run eliminate_symbol after discriminate2022-11-16T13:34:19+01:00Xavier DenisCannot run eliminate_symbol after discriminateIm forwarding an issue from David Ewert which I received over mail:
> I have been trying to get Why3 to completely monomorphise all of the polymorphic logic functions and propositions, in order to avoid the "encoding_smt" transformation...Im forwarding an issue from David Ewert which I received over mail:
> I have been trying to get Why3 to completely monomorphise all of the polymorphic logic functions and propositions, in order to avoid the "encoding_smt" transformation. I've found that the "discriminate" transformation pretty much does what I want (especially when setting meta "select_inst_default" "all", meta "select_lskept_default" "all"). Unfortunately, it still keeps the polymorphic functions and propositions (which I don't want) after introducing the monomorphic ones. I also tried running "eliminate_symbol" after "discriminate" setting "ls:eliminate" for some of the sequence functions hoping this would eliminate the polymorphic versions, but this gave the error: "Failure in transformation eliminate_symbol Ident map is not yet declared". I think that it would be useful for Why3 to have a transformation that runs "discriminate" and then eliminates all polymorphic symbols or at least to allow "eliminate_symbol" to work after "discriminate" (although this seems like more of a hack)
**Note:** He is working with Creusot, so his immediate concern may be solved by !680, but this still seems like a valid bug report.https://gitlab.inria.fr/why3/why3/-/issues/574Record transformation time2021-05-05T18:01:13+02:00Quentin GarcheryRecord transformation timeWhen developping in Why3, one might want to quickly know which part of the replay of a file takes time.
To this end, I think it would be useful if the transformations also recorded the time they spend. It could be stored in the `why3ses...When developping in Why3, one might want to quickly know which part of the replay of a file takes time.
To this end, I think it would be useful if the transformations also recorded the time they spend. It could be stored in the `why3session.xml` with another attribute to the transformation, which would give something like `<transf name="split_vc" time="0.01" >`. It probably should be disabled by default, although it would mean that we should be able to handle session files that differ in this way.
As for prover calls, it could also be shown in the IDE. To not clutter the IDE, it could only be shown if the time goes beyond X seconds.
Would it even make sense to do this ? Is the time spent by transformations too volatile ?https://gitlab.inria.fr/why3/why3/-/issues/567wish: provide monomorphic, clonable modules for references and arrays2024-02-13T17:09:15+01:00MARCHE Claudewish: provide monomorphic, clonable modules for references and arraysPolymorphism is raising several issues. Currently the encoding from Spark to Why3 carefully avoids to produce any polymorphism in the WhyML generated, because provers CVC4 and Z3 are better when tasks have no polymorphism. The counterexa...Polymorphism is raising several issues. Currently the encoding from Spark to Why3 carefully avoids to produce any polymorphism in the WhyML generated, because provers CVC4 and Z3 are better when tasks have no polymorphism. The counterexample features are essentially broken in presence of polymorphism. In the current implementation of "jessie3" in collaboration with TIS, I had to suggest to avoid producing WhyML code involving polymorphism, both for proving efficiency and counterexamples. Recently, Quentin came up with the following trivial example
```
use int.Int
use array.Array
let update a i (v:int)
requires { 0 <= i < length a }
ensures { a[i] = v }
= a[i] <- v
```
which is easily solved by Alt-Ergo, but not by CVC4 nor Z3.
I suggest:
- to provide monomorphic clonable versions of ref.Ref and array.Array in the stdlib, which would allow to program without polymorphism unless needed elsewhere
- to review to current support of polymorphism in Why3: are the drivers appropriate? it seems that in Why3 0.xx, using modules ref.Ref or array.Array was *not* enforcing polymorphism in the generated tasks, but since Why3 1.0 tasks generated are always polymorphic because of type `ref'mk 'a` or `array'mk 'a`https://gitlab.inria.fr/why3/why3/-/issues/330Use hypotheses when doing compile_match2020-10-28T14:07:52+01:00PARREIRA PEREIRA Mário JoséUse hypotheses when doing compile_matchFor the following example:
```
use list.List
constant l: list int = Cons 42 Nil
goal G : 42 = match l with Nil -> 0 | Cons x _ -> x end
```
if I want to get a goal of the form `42 = 42`, I must do first `subst_all` and only then `compi...For the following example:
```
use list.List
constant l: list int = Cons 42 Nil
goal G : 42 = match l with Nil -> 0 | Cons x _ -> x end
```
if I want to get a goal of the form `42 = 42`, I must do first `subst_all` and only then `compile_match` is able to give me `42 = 42`.
Would it be possible for `compile_match` to use hypotheses of the form `H: e = e'` to further simplify goals of the form `match e with e' -> ... end` ?https://gitlab.inria.fr/why3/why3/-/issues/285split_all_full raises out of memory on float theory2022-03-22T16:55:27+01:00DAILLER Sylvainsplit_all_full raises out of memory on float theoryHello,
Using split_all_full on goals containing the ieee_float theory can result in out of memory (see attached file [b.mlw](/uploads/777dac8832951acc1eacf6a489be58ba/b.mlw) ). Most likely, on the hypothesis fma_special, the negative mo...Hello,
Using split_all_full on goals containing the ieee_float theory can result in out of memory (see attached file [b.mlw](/uploads/777dac8832951acc1eacf6a489be58ba/b.mlw) ). Most likely, on the hypothesis fma_special, the negative monoid generated by split_core grows exponentially (which eventually eat all available memory).
I encountered this problem when launching the strategy "1" (problem which should be solved by #282).
Is it possible to optimize the generation of monoids during the transformation, stop the splitting done by the transformation when it grows to a critical size, or disallow part of the splitting ?https://gitlab.inria.fr/why3/why3/-/issues/233Improve apply2018-11-07T11:08:46+01:00DAILLER SylvainImprove applyIn some cases, we would like apply to perform matching on hypothesis too. Coq can do that in:
```
Goal forall P Q, (forall x y, P x y -> Q) -> P 3 4 -> Q.
intros P Q H H1.
apply H with (1:=H1).
```
We could imagine:
`apply H with_hyp ...In some cases, we would like apply to perform matching on hypothesis too. Coq can do that in:
```
Goal forall P Q, (forall x y, P x y -> Q) -> P 3 4 -> Q.
intros P Q H H1.
apply H with (1:=H1).
```
We could imagine:
`apply H with_hyp H1`
To be investigated.MARCHE ClaudeMARCHE Claude