why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2019-08-23T14:47:34+02:00https://gitlab.inria.fr/why3/why3/-/issues/377Why3 should not introduce spaces in identifiers2019-08-23T14:47:34+02:00DAILLER SylvainWhy3 should not introduce spaces in identifiersSpaces are introduced in identifiers in some cases. This makes it impossible for the user to use these identifiers in arguments of transformations.
An example with records is the following:
```
use int.Int
type r = {a : int; b : int}
...Spaces are introduced in identifiers in some cases. This makes it impossible for the user to use these identifiers in arguments of transformations.
An example with records is the following:
```
use int.Int
type r = {a : int; b : int}
let f (x y: r): bool
ensures {x.a = y.a}
=
true
```
To explicitly show the problem use the following transformations:
`introduce_premises`
`destruct_term x`
`assert (x2 = mk r x1 x)`
@marche suggest to use tick `'` instead of space because the user would still not be able to define those in .mlw file but they would be able to use them. Here, the result would be something along the lines of `r'mk`.
Note that spaces also appear in the names of goals: they could be removed in favor of `'` too. For example: `f'VC`.
On this issue, I will try to make a MR with the simple replacement of `mk ` with `'mk` to see if it could work. Note that I also expect to change accordingly any code that would recognize a record by looking if its name begins with `mk `.https://gitlab.inria.fr/why3/why3/-/issues/367Trivial goals are not user-friendly2019-12-04T13:24:11+01:00Guillaume MelquiondTrivial goals are not user-friendlyWhen doing `split_vc` on the weakest precondition of `bar`
```
let foo () requires { true } = ()
let bar () = foo (); foo ()
```
we get two subgoals `true` marked as unknown. At this point, the user can either apply `split_vc` or launc...When doing `split_vc` on the weakest precondition of `bar`
```
let foo () requires { true } = ()
let bar () = foo (); foo ()
```
we get two subgoals `true` marked as unknown. At this point, the user can either apply `split_vc` or launch a prover, on each subgoal. In both cases, this is a waste of user time and processor cycles. This becomes especially noticeable after !207, as the number of trivial goals greatly increases.
Two possible solutions:
1. Automatically mark `true` goals as proved.
2. Prevent `split_vc` from generating them.https://gitlab.inria.fr/why3/why3/-/issues/366Incorrect goal location after splitting.2019-07-16T15:01:08+02:00Guillaume MelquiondIncorrect goal location after splitting.Testcase:
```
val bar (x:int): unit requires { x <> 0 }
let foo (x:int) : unit = bar x; bar x
```
When clicking the initially unique goal in the IDE, both calls `bar x` are properly highlighted as being the preconditions to prove. After...Testcase:
```
val bar (x:int): unit requires { x <> 0 }
let foo (x:int) : unit = bar x; bar x
```
When clicking the initially unique goal in the IDE, both calls `bar x` are properly highlighted as being the preconditions to prove. After splitting the goal, both goals cause the IDE to highlight the first call `bar x`, while the second goal is meant to be the precondition of the second call.
Note that this happens quite often in practice. For example, the fast exponentiation algorithm (or its variant, the ancient Egyptian multiplication) contains both divisions and modulos, which all have the same precondition, so all the goals point to the same location of the code.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/280induction_ty_arg_lex expected behavior2019-03-26T14:59:30+01:00DAILLER Sylvaininduction_ty_arg_lex expected behaviorThis is to investigate the behavior of induction_ty_arg_lex that apparently does not do induction on the right elements.
It was reported by users that on this:
```
goal list_simpl_r :
forall l1:list 'a, l2:list 'a, l:list 'a. (l1 ++ l...This is to investigate the behavior of induction_ty_arg_lex that apparently does not do induction on the right elements.
It was reported by users that on this:
```
goal list_simpl_r :
forall l1:list 'a, l2:list 'a, l:list 'a. (l1 ++ l) = (l2 ++ l) -> l1 = l2
```
It was impossible to make a recursion on ``l1``.
This issue should also investigate what changed in induction_ty_lex between 0.88 and 1.00 (on this same goal): apparently, the transformation is less clever.https://gitlab.inria.fr/why3/why3/-/issues/269transformation replace should replace also under the conditions of `if`2019-02-12T13:55:05+01:00MARCHE Claudetransformation replace should replace also under the conditions of `if`Apparently `replace` does traverse the conditions of `if` termsApparently `replace` does traverse the conditions of `if` terms1.3.0https://gitlab.inria.fr/why3/why3/-/issues/264destruct improvement with if then else2019-02-08T14:47:07+01:00DAILLER Sylvaindestruct improvement with if then elseThis issue to keep track of a suggestion by @bbecker to extend destruct to "if .. then .. else":
```
axiom H: if c1 then c2 else c3
```
destruct H would create two branches: one replacing `H` by `c1 `and `c2` and the other one replacin...This issue to keep track of a suggestion by @bbecker to extend destruct to "if .. then .. else":
```
axiom H: if c1 then c2 else c3
```
destruct H would create two branches: one replacing `H` by `c1 `and `c2` and the other one replacing it with `~c1` and `c3`.
Note: Similar behavior can be done for `match`.Benedikt BeckerBenedikt Beckerhttps://gitlab.inria.fr/why3/why3/-/issues/263Removing Inline_trivial2019-02-12T17:55:13+01:00DAILLER SylvainRemoving Inline_trivialHello,
I don't understand what this transformation is used for. At first, I thought it was there for optimization but it seems that removing it from the driver makes `cvc4 1.5` fail on some files (`bench/ce/array_mono.mlw`).
Am I misun...Hello,
I don't understand what this transformation is used for. At first, I thought it was there for optimization but it seems that removing it from the driver makes `cvc4 1.5` fail on some files (`bench/ce/array_mono.mlw`).
Am I misunderstanding the use of this transformation ? I think there may be a bug in the rest of the transformations used for CVC4 if not.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/259improve destruct_alg2019-01-31T17:26:45+01:00MARCHE Claudeimprove destruct_algFeature wishes for improvements:
* allow user to provide the introduced names, e.g `destruct_alg t as x1,x2`
* rename it into something better, e.g. `destruct_term`.Feature wishes for improvements:
* allow user to provide the introduced names, e.g `destruct_alg t as x1,x2`
* rename it into something better, e.g. `destruct_term`.https://gitlab.inria.fr/why3/why3/-/issues/238Improve case transformation2019-06-18T09:58:40+02:00DAILLER SylvainImprove case transformationIt is my feeling that VC generation/split often produces hypotheses containing implications with the same premises (or its negation) such as:
```
H: P -> A
H1: not P -> B
H2: P -> C
```
On these cases, I think the user would like `case...It is my feeling that VC generation/split often produces hypotheses containing implications with the same premises (or its negation) such as:
```
H: P -> A
H1: not P -> B
H2: P -> C
```
On these cases, I think the user would like `case P` to remove unsatisfiable hypothesis and premises. This would give two new context:
```
H: A
H2: C
H3: P
```
and
```
H1: B
H: not P
```https://gitlab.inria.fr/why3/why3/-/issues/235Avoid substituting to proxy symbols2018-11-16T10:02:53+01:00DAILLER SylvainAvoid substituting to proxy symbolsWhen using `subst_all` or `split_vc`, it is not rare to substitute variables to a proxy symbol:
```
H : r = (o [@mlw_proxy_symbol])
Goal : r + r = 5
```
With `subst_all` or `split_vc` would become:
`Goal: o + o = 5`
I think it is be...When using `subst_all` or `split_vc`, it is not rare to substitute variables to a proxy symbol:
```
H : r = (o [@mlw_proxy_symbol])
Goal : r + r = 5
```
With `subst_all` or `split_vc` would become:
`Goal: o + o = 5`
I think it is better to do the substitution from the other side.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 Claudehttps://gitlab.inria.fr/why3/why3/-/issues/232instantiate should be able to remove the general hypothesis2019-09-24T12:34:43+02:00DAILLER Sylvaininstantiate should be able to remove the general hypothesisAdd an optional argument so that on hypothesis:
`H : forall x. x = 0`
`instantiate H 1` generate the following hypotheses (name change and remove hypothesis):
`H : 1 = 0`
instead of
```
H : forall x. x = 0
H_inst : 1 = 0
```Add an optional argument so that on hypothesis:
`H : forall x. x = 0`
`instantiate H 1` generate the following hypotheses (name change and remove hypothesis):
`H : 1 = 0`
instead of
```
H : forall x. x = 0
H_inst : 1 = 0
```https://gitlab.inria.fr/why3/why3/-/issues/231Add a transformation destruct*2018-11-08T11:28:04+01:00DAILLER SylvainAdd a transformation destruct*Add a transformation that performs destruct recursively on an hypothesis. It should handle all currently handled constructs: disjunction, conjunction, implications.
```
predicate p1
predicate p2
predicate p3
axiom H: p1 -> p2 -> p3
go...Add a transformation that performs destruct recursively on an hypothesis. It should handle all currently handled constructs: disjunction, conjunction, implications.
```
predicate p1
predicate p2
predicate p3
axiom H: p1 -> p2 -> p3
goal G: 1 = 1
```
destruct H should produce 3 new goals for p1, p2 and H : p3 |- G ?
[EDIT: To be more clear]
This should produce 3 new subgoals which are the following:
```
predicate p1
predicate p2
predicate p3
goal G : p1
```
```
predicate p1
predicate p2
predicate p3
goal G : p2
```
```
predicate p1
predicate p2
predicate p3
axiom H : p3
goal G : 1 = 1
```
Sorry for the misleading notations.https://gitlab.inria.fr/why3/why3/-/issues/226Restricting behavior of rewrite_list2018-11-07T10:37:53+01:00DAILLER SylvainRestricting behavior of rewrite_listHello,
Currently `rewrite_list` uses the argument `with_terms` but I think it is difficult for the user to understand what these with_terms corresponds to with this transformation. This list of terms is supposed to be used by `apply/rew...Hello,
Currently `rewrite_list` uses the argument `with_terms` but I think it is difficult for the user to understand what these with_terms corresponds to with this transformation. This list of terms is supposed to be used by `apply/rewrite` after matching. For example,
```
module Rewrite
use int.Int
function f int : int
predicate p int
axiom A: forall a. f (a+1) = f 42
axiom B: forall a. f a = f (43 + 1)
goal g : 5 = f 42
end
```
`rewrite <- A with 43 (* To instantiate a *)`
`rewrite <- B with 43 (* To instantiate a *)`
To me, it makes less sense to try to do the same when rewriting several hypothesis at once:
`rewrite_list <- A,B with 43`
Also, I am not sure that it works when trying to instantiate with a different value for A and B. Should we remove this feature ?Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/210--list-transform should print all transformations2018-11-13T09:45:47+01:00DAILLER Sylvain--list-transform should print all transformations`--list-transform` should also print transformation with arguments.`--list-transform` should also print transformation with arguments.https://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/195New split_vc sometimes crashes2018-10-05T11:26:19+02:00Raphaël Rieu-HelftNew split_vc sometimes crashesFollowing commit 22ab5177b, attempting to use split_vc on lemma `valuation_monotonous` in `examples/multiprecision/valuation.mlw` results in a failure (with the new popup!) due to an uncaught NoTerminationProof exception.Following commit 22ab5177b, attempting to use split_vc on lemma `valuation_monotonous` in `examples/multiprecision/valuation.mlw` results in a failure (with the new popup!) due to an uncaught NoTerminationProof exception.1.1.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/188Modify split_vc to not use simplify_trivial_quantification2018-10-04T15:07:54+02:00Raphaël Rieu-HelftModify split_vc to not use simplify_trivial_quantification1.1.0MARCHE ClaudeMARCHE Claude