strategies: improved default ones, documentation

CHANGES

 
 * marks an incompatible change
 
+
+Tools
+
+  o why3 config now generates default proof strategies using the
+    installed provers. These are available under name "Auto level 1"
+    and "Auto level 2" in why3 ide.
+
 Version 0.87.0, March 15, 2016
 ================================
 

ROADMAP

@@ -147,13 +147,12 @@ and no epsilon
    chaque instance necessaires. plutot qu'un seul symbole _match
    polymorphe.
 
-==================== Roadmap for release 0.87 ========================
-
-DATE : ?
+==================== Roadmap for release 0.88 ========================
 
-Release Notes (details in file CHANGES):
+DATE : au plus tard en novembre 2016, pour que ce soit dispo pour les
+etudiants MPRI (pour la feature strategies en particulier)
 
-== TODO ==
+* integrate server feature done by Johannes
 
 * Document src/core/trans.mli, and fill the paragraph on
   transformations in the tutorial: doc/api.tex, section 4.7 "Applying
@@ -164,30 +163,15 @@ Release Notes (details in file CHANGES):
   solution possible: symbol builtin t_neq, inlining systematique au typage
   (ou laisser inline_trivial le faire)
 
-* DONE finalize detect_polymorphism. Allow polymorphic tuples (supported by SMT ?)
-
-  C'est finalisé. Mais les tuples restent polymorphes.
-
-* integrate server feature done by Johannes
-
-* DONE Coq realization of bitvector theory
-
 * make counter-examples feature more robust
 
-* DONE support for both isabelle 2014 and 2015
-  + bugfix for installation
-
-* DONE review support for division operators by SMT provers
-
-* take some time to fix some bugs of the BTS: 18029 at least
-
 * use the file generated by altgr-ergo to replay proofs edited by altgr-ergo
 
   alt-ergo -replay <file>.agr
 
   -> on pourrait le faire en considerant altgr-ergo comme un prouveur interactif
 
-* make the strategy feature public and documented. Possibly generate
+* DONE make the strategy feature public and documented. Possibly generate
   default strategies dynamically at the time of why3 config --detect,
   using the provers detected : for that, we can annotated the provers in
   prover-detection-data.conf to tell if they should be used in the strategies,
@@ -201,6 +185,27 @@ Release Notes (details in file CHANGES):
 
   . or, favor timelimit increase...
 
+* take some time to fix some bugs of the BTS: 18029 at least
+
+
+==================== Roadmap for release 0.87 ========================
+
+DATE : mars 2016
+
+Release Notes (details in file CHANGES):
+
+== TODO ==
+
+* DONE finalize detect_polymorphism. Allow polymorphic tuples (supported by SMT ?)
+
+  C'est finalisé. Mais les tuples restent polymorphes.
+
+* DONE Coq realization of bitvector theory
+
+* DONE support for both isabelle 2014 and 2015
+  + bugfix for installation
+
+* DONE review support for division operators by SMT provers
 
 
 

doc/manpages.tex

@@ -307,17 +307,36 @@ proof obligations, the corresponding proof attempts are marked obsolete.
   actions are performed even if the goal is already proved. The second
   choice allows to compare provers on the same goal.
 
+\item[Strategies] section provides a set of actions that are
+  performed on the selected goal(s):
+  \begin{description}
+  \item[Split] splits the current goal into subgoals if it is a
+    conjunction of two or more goals. It corresponds to the
+    \verb|split_goal_wp| transformation.
+  \item[Inline] inlines the definitions in the conclusion of the goal.
+    It corresponds to the \verb|introduce_premises| transformation
+    follwoed by \verb|inline_goal|.
+  \item[Auto level 1] is a strategy that first applies a few provers
+    on the goal with a short time limit, then splits the goal and
+    tries again on the subgoals
+  \item[Auto level 2] is a strategy more elaborate than level 1, that
+    attempts to apply a few transformations that are typically
+    useful. It also tries the provers with a larger time limit.
+  \end{description}
+  A more detailed description of strategies is given in
+  Section~\ref{sec:strategies}, as well as a description on how to
+  design strategies of your own.
+
 \item[Provers] provide a button for each detected prover. Clicking on such a
   button starts the corresponding prover on the selected goal(s).
 
-\item[Split] splits the current goal into subgoals if it is a
-  conjunction of two or more goals. It corresponds to the
-  \verb|split_goal_wp| transformation.
-
-\item[Inline] replaces the head predicate symbol of the goal with its
-  definition. It corresponds to the
-  \verb|inline_goal| transformation.
+% \item[Inline] replaces the head predicate symbol of the goal with its
+%   definition. It corresponds to the
+%   \verb|inline_goal| transformation.
 
+\item[Tools] section provides a set of specific action that are
+  typically performed on the selected goal(s). :
+  \begin{description}
 \item[Edit] starts an editor on the selected task.
 
   For automatic provers, this allows to see the file sent to the
@@ -340,6 +359,7 @@ proof obligations, the corresponding proof attempts are marked obsolete.
 
 \item[Interrupt] cancels all the proof attempts currently scheduled
   but not yet started.
+\end{description}
 
 \end{description}
 
@@ -350,7 +370,7 @@ proof obligations, the corresponding proof attempts are marked obsolete.
 \begin{description}
 \item[Add File] adds a file in the GUI.
 %\item[Detect provers] runs provers auto-detection
-\item[Preferences] opens a window for modifying preferred
+]\item[Preferences] opens a window for modifying preferred
   configuration parameters, see details below.
 \item[Reload] reloads the input files from disk, and update the session state accordingly.
 \item[Save session] saves current session state on disk. The policy to decide when to save the session is configurable, as described in the preferences below.

doc/technical.tex

@@ -604,6 +604,94 @@ and is likely to change in future versions.
 \end{description}
 
 
+\section{Proof Strategies}
+\label{sec:strategies}
+
+As seen in Section~\ref{sec:ideref}, the IDE provides a few buttons
+that trigger the run of simple proof strategies on the selected goals.
+Proof strategies can be defined using a basic assembly-style language,
+and put into the Why3 configuration file. The commands of this basic
+language are:
+\begin{itemize}
+\item \texttt{c $p$ $t$ $m$} calls the prover $p$ with a time limit
+  $t$ and memory limit $m$. On success, the strategy ends, it
+  continues to next line otherwise
+\item \texttt{t $n$ $lab$} applies the transformation $n$. On success,
+  the strategy continues to label $lab$, and is applied to each
+  generated sub-goals.  It continues to next line otherwise.
+\item \texttt{g $lab$} inconditionally jumps to label $lab$
+\item \texttt{$lab$:} declares the label $lab$. The default label
+  \texttt{exit} allows to stop the program.
+\end{itemize}
+
+To examplify this basic programming language, we give below the
+default strategies that are attached to the default buttons of the
+IDE, assuming that the provers Alt-Ergo 1.01, CVC4 1.4 and Z3 4.4.1
+were detected by the \verb|why3 config --detect| command
+\begin{description}
+\item[Split] is bound to the 1-line strategy
+\begin{verbatim}
+t split_goal_wp exit
+\end{verbatim}
+
+\item[Auto level 1] is bound to
+\begin{verbatim}
+start:
+c Z3,4.4.1, 1 1000
+c Alt-Ergo,1.01, 1 1000
+c CVC4,1.4, 1 1000
+t split_goal_wp start
+c Z3,4.4.1, 10 4000
+c Alt-Ergo,1.01, 10 4000
+c CVC4,1.4, 10 4000
+\end{verbatim}
+  The three provers are first tried for a time limit of 1 second and
+  memory limit of 1~Gb, each in turn. If none of them succeed, a
+  split is attempted. If the split works then the same strategy is
+  retried on each sub-goals. If the split does not succeed, the provers
+  are tried again with a larger limits.
+
+\item[Auto level 2] is bound to
+\begin{verbatim}
+start:
+c Z3,4.4.1, 1 1000
+c Eprover,1.8-001, 1 1000
+c Spass,3.7, 1 1000
+c Alt-Ergo,1.01, 1 1000
+c CVC4,1.4, 1 1000
+t split_goal_wp start
+c Z3,4.4.1, 5 2000
+c Eprover,1.8-001, 5 2000
+c Spass,3.7, 5 2000
+c Alt-Ergo,1.01, 5 2000
+c CVC4,1.4, 5 2000
+t introduce_premises afterintro
+afterintro:
+t inline_goal afterinline
+g trylongertime
+afterinline:
+t split_goal_wp start
+trylongertime:
+c Z3,4.4.1, 30 4000
+c Eprover,1.8-001, 30 4000
+c Spass,3.7, 30 4000
+c Alt-Ergo,1.01, 30 4000
+c CVC4,1.4, 30 4000
+
+\end{verbatim}
+  Notice that now 5 provers are used.  The provers are first tried for
+  a time limit of 1 second and memory limit of 1~Gb, each in turn. If
+  none of them succeed, a split is attempted. If the split works then
+  the same strategy is retried on each sub-goals. If the split does
+  not succeed, the prover are tried again with limits of 5 s and 2
+  Gb. If all fail, we attempt the transformation of introduction of
+  premises in the context, followed by an inlining of the definiiions
+  in the goals. We then attempt a split again, if the split succeeds,
+  we restart from the beginning, if it fails then provers are tried
+  again with 30s and 4 Gb.
+
+\end{description}
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-PDF-mode: t

share/provers-detection-data.conf

@@ -186,6 +186,7 @@ version_old = "1.5"
 version_old = "1.4"
 command = "%e -s -R -xAuto -tAuto --cpu-limit=%t --tstp-in %f"
 driver = "drivers/eprover.drv"
+use_at_auto_level = 2
 
 [ATP gappa]
 name = "Gappa"
@@ -266,6 +267,7 @@ version_regexp = "SPASS V \\([^ \n\t]+\\)"
 version_ok = "3.7"
 command = "%e -TPTP -PGiven=0 -PProblem=0 -TimeLimit=%t %f"
 driver = "drivers/spass.drv"
+use_at_auto_level = 2
 
 [ATP spass]
 name = "Spass"
@@ -276,6 +278,7 @@ version_regexp = "SPASS[^ \n\t]* V \\([^ \n\t]+\\)"
 version_ok = "3.8ds"
 command = "%e -Isabelle=1 -PGiven=0 -TimeLimit=%t %f"
 driver = "drivers/spass_types.drv"
+use_at_auto_level = 2
 
 [ATP vampire]
 name = "Vampire"

src/driver/autodetection.ml

@@ -328,8 +328,8 @@ let generate_auto_strategies config =
   eprintf "Generating strategies:@.";
   Hprover.iter
     (fun p (lev,b) ->
-      if b then eprintf "  Prover %a will be used in Auto level >= %d@."
-           Whyconf.print_prover p lev) prover_auto_levels;
+     if b then eprintf "  Prover %a will be used in Auto level >= %d@."
+                       Whyconf.print_prover p lev) prover_auto_levels;
   (* Split *)
   let code = "t split_goal_wp exit" in
   let split = {
@@ -338,15 +338,23 @@ let generate_auto_strategies config =
       strategy_shortcut = "s";
       strategy_code = code }
   in
+  (* Inline *)
+  let code = "t introduce_premises next next: t inline_goal exit" in
+  let inline = {
+      strategy_name = "Inline";
+      strategy_desc = "Inline@ definitions@ in@ the@ conclusion@ of@ the@ goal";
+      strategy_shortcut = "i";
+      strategy_code = code }
+  in
   (* Auto level 1 *)
   let provers_level1 =
     Hprover.fold
       (fun p (lev,b) acc ->
        if b && lev = 1 then
-           let name =
-             p.Whyconf.prover_name ^ "," ^
-               p.Whyconf.prover_version ^ "," ^ p.Whyconf.prover_altern
-           in name :: acc
+         let name =
+           p.Whyconf.prover_name ^ "," ^
+             p.Whyconf.prover_version ^ "," ^ p.Whyconf.prover_altern
+         in name :: acc
        else acc) prover_auto_levels []
   in
   fprintf str_formatter "start:@\n";
@@ -365,10 +373,10 @@ let generate_auto_strategies config =
     Hprover.fold
       (fun p (lev,b) acc ->
        if b && lev >= 1 && lev <= 2 then
-           let name =
-             p.Whyconf.prover_name ^ "," ^
-               p.Whyconf.prover_version ^ "," ^ p.Whyconf.prover_altern
-           in name :: acc
+         let name =
+           p.Whyconf.prover_name ^ "," ^
+             p.Whyconf.prover_version ^ "," ^ p.Whyconf.prover_altern
+         in name :: acc
        else acc) prover_auto_levels []
   in
   fprintf str_formatter "start:@\n";
@@ -376,15 +384,12 @@ let generate_auto_strategies config =
   fprintf str_formatter "t split_goal_wp start@\n";
   List.iter (fun s -> fprintf str_formatter "c %s 5 2000@\n" s) provers_level2;
   fprintf str_formatter "t introduce_premises afterintro@\n";
-  fprintf str_formatter "g inline@\n";
   fprintf str_formatter "afterintro:@\n";
-  fprintf str_formatter "t split_goal_wp start@\n";
-  fprintf str_formatter "inline:@\n";
   fprintf str_formatter "t inline_goal afterinline@\n";
-  fprintf str_formatter "g longtime@\n";
+  fprintf str_formatter "g trylongertime@\n";
   fprintf str_formatter "afterinline:@\n";
   fprintf str_formatter "t split_goal_wp start@\n";
-  fprintf str_formatter "longtime:@\n";
+  fprintf str_formatter "trylongertime:@\n";
   List.iter (fun s -> fprintf str_formatter "c %s 30 4000@\n" s) provers_level2;
   let code = flush_str_formatter () in
   let auto2 = {
@@ -393,7 +398,9 @@ let generate_auto_strategies config =
       strategy_shortcut = "2";
       strategy_code = code }
   in
-  add_strategy (add_strategy (add_strategy config split) auto1) auto2
+  add_strategy
+    (add_strategy
+       (add_strategy (add_strategy config inline) split) auto1) auto2
 
 let detect_exec env main data acc exec_name =
   let s = ask_prover_version env exec_name data.version_switch in