why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2022-03-22T15:55:27Zhttps://gitlab.inria.fr/why3/why3/-/issues/285split_all_full raises out of memory on float theory2022-03-22T15:55:27ZDAILLER 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-26T13:59:30ZDAILLER 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.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/269transformation replace should replace also under the conditions of `if`2019-02-12T12:55:05ZMARCHE 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.0DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/264destruct improvement with if then else2019-02-08T13:47:07ZDAILLER 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-12T16:55:13ZDAILLER 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-31T16:26:45ZMARCHE 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`.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/238Improve case transformation2019-06-18T07:58:40ZDAILLER 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
```DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/235Avoid substituting to proxy symbols2018-11-16T09:02:53ZDAILLER 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.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/233Improve apply2018-11-07T10:08:46ZDAILLER 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-24T10:34:43ZDAILLER 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
```DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/231Add a transformation destruct*2018-11-08T10:28:04ZDAILLER 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.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/210--list-transform should print all transformations2018-11-13T08:45:47ZDAILLER Sylvain--list-transform should print all transformations`--list-transform` should also print transformation with arguments.`--list-transform` should also print transformation with arguments.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/195New split_vc sometimes crashes2018-10-05T09:26:19ZRaphaë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-04T13:07:54ZRaphaël Rieu-HelftModify split_vc to not use simplify_trivial_quantification1.1.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/185transformation ``apply`` should consider ``let`` as a premise2018-10-29T14:27:58ZMARCHE Claudetransformation ``apply`` should consider ``let`` as a premiseIn the following example, I can do ``apply A`` but not ``apply B``. It would be nicer if ``apply`` considers the ``let`` as a premise of the property to apply
```
function f int : int
predicate p int int
axiom A: forall x y. x = f y -> p...In the following example, I can do ``apply A`` but not ``apply B``. It would be nicer if ``apply`` considers the ``let`` as a premise of the property to apply
```
function f int : int
predicate p int int
axiom A: forall x y. x = f y -> p x y
axiom B: forall y. let x = f y in p x y
goal g : p 17 42
```DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/126Transformation `apply` and inductive predicates2018-06-01T14:59:05ZGuillaume MelquiondTransformation `apply` and inductive predicatesThe `apply` transformation does not seem to be able to apply constructors of inductive predicate.
inductive unit = tt : unit
goal g : unit
`apply tt` gives `Transformation raised a general error: apply`The `apply` transformation does not seem to be able to apply constructors of inductive predicate.
inductive unit = tt : unit
goal g : unit
`apply tt` gives `Transformation raised a general error: apply`DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/116Array access in transformations with arguments2018-07-18T15:18:59ZDAILLER SylvainArray access in transformations with argumentsIn transformation with arguments, stuff defined with a notation cannot be reused if the notation is overloaded.
In Array63 module we have:
`function ([]) (a: array 'a) (i: int) : 'a = a.elts i`
And an example is:
```
module Test
use...In transformation with arguments, stuff defined with a notation cannot be reused if the notation is overloaded.
In Array63 module we have:
`function ([]) (a: array 'a) (i: int) : 'a = a.elts i`
And an example is:
```
module Test
use import array.Array
use import mach.array.Array63
constant d: Array.array int
constant e: Array63.array int
goal a: e[1] = 5
goal c: Array.([]) d 3 = 5
end
```
In the above, notation [] cannot be used for array d as the notation [] is used for Array63. In this example, it is not even possible to talk about Array.([]) in transformations.
The complete solution would be to accept qualified expressions in arguments of tactics: this may be difficult.
I think it's possible to disambiguate the mixfix notation as we do for infix (==^ ==^^ etc). It would require to extend the parser a little so that "[ term ]", "[ ^ term ]", "[ ^ ^ term ]" are recognized (or any similar notation).DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/115subst_all and split_intros_goal_wp do not substitute enough2018-05-23T11:40:23ZDAILLER Sylvainsubst_all and split_intros_goal_wp do not substitute enoughIn example verify_this_2018_rouge_et_noir_1, on the last subgoal VC_enum, after split_intros_goal_wp is applied, constant to be substituted remain in subgoal 37 like o o1 etc (as described during gt).
Applying subst_all does not work too...In example verify_this_2018_rouge_et_noir_1, on the last subgoal VC_enum, after split_intros_goal_wp is applied, constant to be substituted remain in subgoal 37 like o o1 etc (as described during gt).
Applying subst_all does not work too. subst seems to work in this case.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/114Problem with infix and val predicate in transformations2018-07-18T15:19:31ZDAILLER SylvainProblem with infix and val predicate in transformationsHello,
In master, the specification of the following is not usable inside transformations with arguments (apply, rewrite, print).
```
(** equality is extensional *)
val predicate (==) (s1 s2: seq 'a)
ensures { result <-> length s...Hello,
In master, the specification of the following is not usable inside transformations with arguments (apply, rewrite, print).
```
(** equality is extensional *)
val predicate (==) (s1 s2: seq 'a)
ensures { result <-> length s1 = length s2 &&
forall i: int. 0 <= i < length s1 -> s1[i] = s2[i] }
ensures { result -> s1 = s2 }
```
This can be reproduce with the following code by searching (==) then trying to print the spec:
```
module Test
use import int.Int
use import seq.Seq
goal f: create 32 (fun x -> x) == empty -> false
end
```
I think the reason is that the spec of this is named "infix ==_spec" in pdecl.ml. This is not recognized as a valid identifier by the parser (I think because of the space and "=="). One solution would be to sanitize the new name introduced in pdecl.ml: we would get "infix_eqeq_spec" and be able to use it in transformations.
This is probably a bigger problem, the solution looks very ad hoc but I think it works.
copying @rrieuhel as you reported the bug, thanks.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/101eliminate_literal, range types and Eprover driver2018-03-28T06:48:33ZRaphaël Rieu-Helfteliminate_literal, range types and Eprover driverOn the following example, launching Eprover fails with this error message:
"internal failure: Failure in transformation eliminate_literal
Ident int63'axiom is already declared, with a different declaration"
The SMT s...On the following example, launching Eprover fails with this error message:
"internal failure: Failure in transformation eliminate_literal
Ident int63'axiom is already declared, with a different declaration"
The SMT solvers work fine.
```
module A
use import int.Int
use import mach.int.Int63
let test (x:int63) : int63
requires { x < 100 }
= x+1
end
```MARCHE ClaudeMARCHE Claude