Issues · Why3 / why3 · GitLab

Compute inside an hypothesis

#13 · created Oct 31, 2017 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated Jan 05, 2018
Add simpl

#14 · created Oct 31, 2017 by DAILLER Sylvain component: transformations
- CLOSED
- 2
updated Jan 05, 2018
destruct_alg improvement

#15 · created Oct 31, 2017 by DAILLER Sylvain component: transformations priority: high
- CLOSED
- 2
updated Nov 15, 2017
subst should remove declarations

#16 · created Oct 31, 2017 by DAILLER Sylvain component: transformations priority: medium
- CLOSED
- 4
updated May 16, 2018
Error in transformation remove

#17 · created Oct 31, 2017 by DAILLER Sylvain component: transformations
- CLOSED
- 2
updated May 10, 2019
Case should add expl to its new subgoals

#18 · created Oct 31, 2017 by DAILLER Sylvain component: transformations priority: medium
- CLOSED
- 1
updated Nov 16, 2017
Apply with x

#19 · created Oct 31, 2017 by DAILLER Sylvain Nov 15, 2017 component: transformations priority: high
- CLOSED
- 2
updated Nov 16, 2017
recursive destruct

#20 · created Oct 31, 2017 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated Apr 29, 2019
induction_pr with arguments

#22 · created Oct 31, 2017 by DAILLER Sylvain component: transformations priority: low
- CLOSED
- 1
- 3
updated Mar 27, 2019
Add a revert transformation

#23 · created Oct 31, 2017 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated Dec 20, 2017
Apply coercions in replace parameters

#24 · created Nov 07, 2017 by Raphaël Rieu-Helft component: transformations
- CLOSED
- 1
- 1
updated Dec 09, 2019
Do not require the user to provide the labels in replace parameters

#25 · created Nov 07, 2017 by Raphaël Rieu-Helft component: transformations
- CLOSED
- 1
updated Nov 10, 2017
typing of transformation argument should not ignore coercion

#34 · created Nov 16, 2017 by MARCHE Claude component: transformations
- CLOSED
- 1
updated Nov 17, 2017
Incorrect ident parsing in transformations

#71 · created Jan 08, 2018 by Raphaël Rieu-Helft component: transformations priority: high
- CLOSED
- 3
updated Feb 02, 2018
first_order_matching may instantiate matching variables using bound variables

#79 · created Jan 22, 2018 by CLOCHARD Martin component: transformations soundness
- CLOSED
- 4
updated Feb 02, 2018
Improve handling of premises

#88 · created Feb 14, 2018 by Guillaume Melquiond component: graphical user interface component: transformations feature wish
- CLOSED
- 5
updated Aug 29, 2018
Simplification of array initializer for generated Why3 code

#99 · created Mar 14, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated Jun 18, 2019
eliminate_literal, range types and Eprover driver

#101 · created Mar 27, 2018 by Raphaël Rieu-Helft component: drivers component: transformations
- CLOSED
- 0
updated Mar 28, 2018
Problem with infix and val predicate in transformations

#114 · created May 04, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 2
updated Jul 18, 2018
subst_all and split_intros_goal_wp do not substitute enough

#115 · created May 07, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated May 23, 2018
Array access in transformations with arguments

#116 · created May 07, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated Jul 18, 2018
simplify_trivial_quantification kills some goals

#120 · created May 22, 2018 by Raphaël Rieu-Helft component: transformations priority: high
- CLOSED
- 4
updated May 22, 2018
Transformation `apply` and inductive predicates

#126 · created Jun 01, 2018 by Guillaume Melquiond component: transformations
- CLOSED
- 2
updated Jun 01, 2018
Transformation `split_vc` and term shapes

#128 · created Jun 01, 2018 by Guillaume Melquiond 1.0.0 component: session component: transformations priority: blocker
- CLOSED
- 1
- 0
updated Jun 13, 2018
transformation ``apply`` should consider ``let`` as a premise

#185 · created Sep 20, 2018 by MARCHE Claude component: transformations feature wish
- CLOSED
- 4
updated Oct 29, 2018
Modify split_vc to not use simplify_trivial_quantification

#188 · created Sep 28, 2018 by Raphaël Rieu-Helft 1.1.0 component: transformations
- CLOSED
- 1
- 0
updated Oct 04, 2018
New split_vc sometimes crashes

#195 · created Oct 02, 2018 by Raphaël Rieu-Helft 1.1.0 component: transformations
- CLOSED
- 4
updated Oct 05, 2018
Interaction of smt encoding with meta

#196 · created Oct 03, 2018 by DAILLER Sylvain component: transformations feature wish priority: low
- 3
updated Mar 12, 2021
--list-transform should print all transformations

#210 · created Oct 12, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 0
updated Nov 13, 2018
Restricting behavior of rewrite_list

#226 · created Oct 29, 2018 by DAILLER Sylvain component: transformations priority: low
- CLOSED
- 2
updated Nov 07, 2018
Add a transformation destruct*

#231 · created Nov 07, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 5
updated Nov 08, 2018
instantiate should be able to remove the general hypothesis

#232 · created Nov 07, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated Sep 24, 2019
Improve apply

#233 · created Nov 07, 2018 by DAILLER Sylvain component: transformations
- 0
updated Nov 07, 2018
Avoid substituting to proxy symbols

#235 · created Nov 13, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 2
updated Nov 16, 2018
Improve case transformation

#238 · created Nov 14, 2018 by DAILLER Sylvain component: transformations
- CLOSED
- 1
updated Jun 18, 2019
improve destruct_alg

#259 · created Jan 28, 2019 by MARCHE Claude component: transformations
- CLOSED
- 1
- 2
updated Jan 31, 2019
Removing Inline_trivial

#263 · created Jan 31, 2019 by DAILLER Sylvain component: drivers component: transformations
- CLOSED
- 1
- 0
updated Feb 12, 2019
destruct improvement with if then else

#264 · created Jan 31, 2019 by DAILLER Sylvain component: transformations
- CLOSED
- 2
- 2
updated Feb 08, 2019
transformation replace should replace also under the conditions of `if`

#269 · created Feb 05, 2019 by MARCHE Claude 1.3.0 component: transformations
- CLOSED
- 4
updated Feb 12, 2019
induction_ty_arg_lex expected behavior

#280 · created Mar 01, 2019 by DAILLER Sylvain component: transformations
- CLOSED
- 1
- 0
updated Mar 26, 2019
split_all_full raises out of memory on float theory

#285 · created Mar 24, 2019 by DAILLER Sylvain component: transformations
- 0
updated Mar 22, 2022
Use hypotheses when doing compile_match

#330 · created May 29, 2019 by PARREIRA PEREIRA Mário José component: transformations feature wish
- 5
updated Oct 28, 2020
Incorrect goal location after splitting.

#366 · created Jul 11, 2019 by Guillaume Melquiond component: graphical user interface component: transformations
- CLOSED
- 1
- 11
updated Jul 16, 2019
Trivial goals are not user-friendly

#367 · created Jul 15, 2019 by Guillaume Melquiond component: session component: transformations
- CLOSED
- 5
updated Dec 04, 2019
Why3 should not introduce spaces in identifiers

#377 · created Aug 22, 2019 by DAILLER Sylvain component: transformations
- CLOSED
- 1
- 1
updated Aug 23, 2019
List transformation with arguments and documentation

#380 · created Sep 03, 2019 by DAILLER Sylvain component: transformations
- CLOSED
- 17
updated Nov 22, 2019
`apply with` and `rewrite with` should give more details (e.g., quantifier names) when the number of arguments do not match

#399 · created Oct 25, 2019 by Guillaume Melquiond component: transformations
- CLOSED
- 1
- 2
updated Oct 28, 2019
Hide does not work

#405 · created Oct 31, 2019 by DAILLER Sylvain component: transformations
- CLOSED
- 1
- 0
updated Nov 04, 2019
destruct/case transformations incorrectly handle polymorphic formulas

#525 · created Jan 14, 2021 by Quentin Garchery 1.4.0 component: transformations soundness
- CLOSED
- 1
- 4
updated Jul 13, 2021
wish: provide monomorphic, clonable modules for references and arrays

#567 · created Mar 31, 2021 by MARCHE Claude To be discussed component: drivers component: theories component: transformations
- 14
updated Mar 22, 2022
Record transformation time

#574 · created Apr 29, 2021 by Quentin Garchery To be discussed component: session component: transformations feature wish
- 11
updated May 05, 2021