Attention une mise à jour du service Gitlab va être effectuée le mardi 14 décembre entre 13h30 et 14h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

manpages.tex 21.9 KB
Newer Older
1
\chapter{Reference manuals for the \why\ tools}
MARCHE Claude's avatar
MARCHE Claude committed
2
\label{chap:manpages}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
3 4

\section{Compilation, Installation}
MARCHE Claude's avatar
MARCHE Claude committed
5
\label{sec:install}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
6

7
Compilation of \why\ must start with a configuration phase which is run as
MARCHE Claude's avatar
MARCHE Claude committed
8 9 10
\begin{verbatim}
./configure
\end{verbatim}
11
This analyzes your current configuration and checks if requirements hold.
MARCHE Claude's avatar
MARCHE Claude committed
12 13
Compilation requires:
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
14 15
\item The Objective Caml compiler, version 3.10 or higher. It is
  available as a binary package for most Unix distributions. For
16
  Debian-based Linux distributions, you can install the packages
MARCHE Claude's avatar
MARCHE Claude committed
17 18 19
\begin{verbatim}
ocaml ocaml-native-compilers
\end{verbatim}
20
It is also installable from sources, downloadable from the site
MARCHE Claude's avatar
MARCHE Claude committed
21
\url{http://caml.inria.fr/ocaml/}
MARCHE Claude's avatar
add  
MARCHE Claude committed
22
\end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
23

24
For the IDE, additional OCaml libraries are needed:
MARCHE Claude's avatar
add  
MARCHE Claude committed
25
\begin{itemize}
26 27
\item The Lablgtk2 library for OCaml bindings of the gtk2 graphical library.
For Debian-based Linux distributions, you can install the packages
MARCHE Claude's avatar
MARCHE Claude committed
28 29 30
\begin{verbatim}
liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev
\end{verbatim}
31 32
It is also installable from sources, available from the site
\url{http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html}
MARCHE Claude's avatar
MARCHE Claude committed
33

34 35
\item The OCaml bindings of the sqlite3 library.
For Debian-based Linux distributions, you can install the package
MARCHE Claude's avatar
MARCHE Claude committed
36 37 38 39 40
\begin{verbatim}
libsqlite3-ocaml-dev
\end{verbatim}
It is also installable from sources, available from the site
\url{http://ocaml.info/home/ocaml_sources.html#ocaml-sqlite3}
MARCHE Claude's avatar
MARCHE Claude committed
41 42
\end{itemize}

43 44 45 46 47
When configuration is finished, you can compile \why.
\begin{verbatim}
make
\end{verbatim}

MARCHE Claude's avatar
add  
MARCHE Claude committed
48 49
\subsection{Local use, without installation}

50 51
It is not mandatory to install \why\ into system directories.
\why\ can be configured and compiled for local use as follows:
MARCHE Claude's avatar
add  
MARCHE Claude committed
52 53 54 55
\begin{verbatim}
./configure --enable-local
make
\end{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
56
The \why\ executables are then available in the subdirectory \texttt{bin/}.
MARCHE Claude's avatar
add  
MARCHE Claude committed
57

58
\subsection{Installation of the \why\ library}
MARCHE Claude's avatar
MARCHE Claude committed
59 60
\label{sec:installlib}

61
By default, the \why\ library is not installed. It can be installed using
62 63 64 65
\begin{verbatim}
make byte opt
make install_lib
\end{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
66

MARCHE Claude's avatar
MARCHE Claude committed
67
\section{Installation of external provers}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
68

69 70
\why\ can use a wide range of external theorem provers. These need to
be installed separately, and then \why\ needs to be configured to use
MARCHE Claude's avatar
MARCHE Claude committed
71
them. There is no need to install these provers before compiling and
72
installing Why.
MARCHE Claude's avatar
add  
MARCHE Claude committed
73

MARCHE Claude's avatar
MARCHE Claude committed
74 75
For installation of external provers, please look at the Why provers
tips page \url{http://why.lri.fr/provers.en.html}.
MARCHE Claude's avatar
add  
MARCHE Claude committed
76

77
For configuring \why\ to use the provers, follow instructions given in
MARCHE Claude's avatar
MARCHE Claude committed
78
Section~\ref{sec:why3config}.
MARCHE Claude's avatar
add  
MARCHE Claude committed
79

MARCHE Claude's avatar
MARCHE Claude committed
80 81
\section{The \texttt{why3config} command-line tool}
\label{sec:why3config}.
MARCHE Claude's avatar
add  
MARCHE Claude committed
82

83
\why\ must be configured to access external provers. Typically, this is done
MARCHE Claude's avatar
MARCHE Claude committed
84 85 86 87 88 89 90 91
by running either the command line tool
\begin{verbatim}
why3config
\end{verbatim}
or using the menu
\begin{verbatim}
File/Detect provers
\end{verbatim}
92
of the IDE. This must be redone each time a new prover is installed.
MARCHE Claude's avatar
MARCHE Claude committed
93

94
The provers which \why\ attempts to detect are described in
MARCHE Claude's avatar
MARCHE Claude committed
95
the readable configuration file \texttt{provers-detection-data.conf}
96
of the \why\ data directory (\eg{}
MARCHE Claude's avatar
MARCHE Claude committed
97 98 99 100 101
\texttt{/usr/local/share/why3}). Advanced users may try to modify this
file to add support for detection of other provers. (In that case,
please consider submitting a new prover configuration on the bug
tracking system).

102 103
The result of provers detection is stored in the user's
configuration file (\verb+~/.why.conf+ or, in the case of local
104
installation, \verb+why.conf+ in Why3 sources top directory). This file
105
is also human-readable, and advanced users may modify it in order to
106
experiment with different ways of calling provers, \eg{} different
107
versions of the same prover, or with different options.
MARCHE Claude's avatar
MARCHE Claude committed
108

109
The provers which are typically looked for are
MARCHE Claude's avatar
MARCHE Claude committed
110
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
111 112 113 114 115 116 117 118 119 120
\item Alt-Ergo~\cite{conchon08smt,ergo}: \url{http://alt-ergo.lri.fr}
\item CVC3~\cite{BarTin-CAV-07}: \url{http://cs.nyu.edu/acsys/cvc3/}
\item Coq~\cite{CoqArt}: \url{http://coq.inria.fr}
\item Eprover~\cite{schulz04ijcar}: \url{http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html}
\item Gappa~\cite{melquiond08rnc}: \url{http://gappa.gforge.inria.fr/}
\item Simplify~\cite{simplify05}: \url{http://secure.ucd.ie/products/opensource/Simplify/}
\item Spass~: \url{http://www.spass-prover.org/}
\item veriT~: \url{http://www.verit-solver.org/}
\item Yices~\cite{DM06}: \url{http://yices.csl.sri.com/}
\item Z3~\cite{z3}: \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}
MARCHE Claude's avatar
MARCHE Claude committed
121
\end{itemize}
MARCHE Claude's avatar
add  
MARCHE Claude committed
122

123
\texttt{why3config} also detects the plugins installed in the \why\
124 125 126 127 128
plugins directory (\eg{} \texttt{/usr/local/lib/why3/plugins}). A
plugin must register itself as a parser, a transformation or a
printer, as explained in the corresponding section.

If the user's configuration file is already present,
129
\texttt{why3config} will only reset unset variables to default value,
130
but will not try to detect provers.
131
The option \texttt{--detect-provers} should be used to force
132 133
\why\ to detect again the available
provers and to replace them in the configuration file. The option
134
\texttt{--detect-plugins} will do the same for plugins.
135

MARCHE Claude's avatar
doc  
MARCHE Claude committed
136
\section{The \texttt{why3} command-line tool}
MARCHE Claude's avatar
MARCHE Claude committed
137
\label{sec:why3ref}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
138

139
\why\ is primarily used to call provers on goals contained in an
140
input file. By default, such a file must be written in \why\ language
141 142 143 144 145
and have the extension \texttt{.why}. However, a dynamically loaded
plugin can register a parser for some other format of logical problems,
\eg{} TPTP or SMTlib.

The \texttt{why3} tool executes the following steps:
146
\begin{enumerate}
147
\item Parse the command line and report errors if needed.
148
\item Read the configuration file using the priority defined in
149 150 151 152 153 154
  Section~\ref{sec:whyconffile}.
\item Load the plugins mentioned in the configuration. It will not
  stop if some plugin fails to load.
\item Parse and typecheck the given files using the correct parser in order
  to obtain a set of \why\ theories for each file. It uses
  the filename extension or the \texttt{--format} option to choose
155
  among the available parsers. The \texttt{--list-format} option gives
156
  the list of registered parsers.
157
\item Extract the selected goals inside each of the selected theories
158 159
  into tasks. The goals and theories are selected using the options
  \texttt{-G/--goal} and \texttt{-T/--theory}. The option
160
  \texttt{-T/--theory} applies to the last file appearing on the
161 162 163 164
  command line, the option \texttt{-G/--goal} applies to the last theory
  appearing on the command line. If no theories are selected in a file,
  then every theory is considered as selected. If no goals are selected
  in a theory, then every goal is considered as selected.
165
\item Apply the transformation requested
166
  with \texttt{-a/--apply-transform} in their order of appearance on the
167 168 169 170
  command line. \texttt{--list-transforms} list the known
  transformations, plugins can add more of them.
\item Apply the driver selected with the \texttt{-D/--driver} option,
  or the driver of the prover selected with \texttt{-P/--prover}
171
  option. \texttt{--list-provers} lists the known provers, i.e.~the ones
172
  which appear in the configuration file.
173 174 175 176
\item If the option \texttt{-P/--prover} is given, call the selected prover
  on each generated task and print the results. If the option
  \texttt{-D/--driver} is given, print each generated task using
  the format specified in the selected driver.
177 178
\end{enumerate}

179 180
%\texttt{why3} calls the provers sequentially, use \texttt{why3bench} if *)
%you want to call the provers concurrently.  *)
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
181

182
The provers can answer the following output:
François Bobot's avatar
François Bobot committed
183
\begin{description}
François Bobot's avatar
François Bobot committed
184 185 186 187 188
\item[Valid] the goal is proved in the given context,
\item[Unknown] the prover stop by itself to search,
\item[Timeout] the prover doesn't have enough time,
\item[Failure] an error occured,
\item[Invalid] the prover know the goal can't be proved
François Bobot's avatar
François Bobot committed
189
\end{description}
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
190 191 192 193 194 195 196
% \why\ can also be *)
% used to provide other informations : *)
% \begin{itemize} *)
% \item \texttt{print-namespace} print the namespace of the selected *)
%   theories *)
% \item TO BE COMPLETED *)
% \end{itemize} *)
197

François Bobot's avatar
François Bobot committed
198 199 200 201 202 203 204 205 206 207
The option \texttt{--bisect} change the behaviors of why3. With this
option, \texttt{-P/--prover} and \texttt{-o/--output} must be given
and a valid goal must be selected. The last step executed by why3 is
replaced by computing a minimal set (in the great majority of the
case) of declarations which still prove the goal. Currently it doesn't
use any information provided by the prover, it call the prover
multiple time with reduced context. The minimal set of declarations is
then written in the prover syntax into a file located in the directory
given to the \texttt{-o/--output} option.

208
\section{The \texttt{why3ide} GUI}
MARCHE Claude's avatar
MARCHE Claude committed
209 210
\label{sec:ideref}

211 212 213 214
The basic usage of the GUI is described by the tutorial of
Section~\ref{sec:gui}. We describe here the command-line options and
the actions of the various menus and buttons of the interface.

MARCHE Claude's avatar
MARCHE Claude committed
215 216 217 218 219 220
\subsection{Command-line options}

\begin{description}
\item[-I] $d$: adds $d$ in the load path, to search for theories.
\end{description}

MARCHE Claude's avatar
MARCHE Claude committed
221
\subsection{Left toolbar actions}
MARCHE Claude's avatar
MARCHE Claude committed
222 223

\begin{description}
MARCHE Claude's avatar
MARCHE Claude committed
224 225 226 227 228 229
\item[Context] The context in which the other tools below will
  apply. If ``only unproved goals'' is selected, no action will ever
  be applied to an already proved goal.  If ``all goals'', then
  actions are performed even if the goal is already proved. The second
  choice allows to compare provers on the same goal.

MARCHE Claude's avatar
MARCHE Claude committed
230 231 232 233
\item[Provers] To each detected prover corresponds to a button in this
  prover framed box. Clicking on this button starts the prover on the
  selected goal(s).

MARCHE Claude's avatar
MARCHE Claude committed
234 235 236 237 238 239
\item[Split] This splits the current goal into subgoals if it is a
  conjunction of two or more goals.

\item[Inline] If the goal is headed by a defined predicate symbol,
  expands it with this definition. [NOT YET AVAILABLE]

MARCHE Claude's avatar
MARCHE Claude committed
240 241 242 243 244 245 246 247 248
\item[Edit] Start an editor on the selected task.

  For automatic provers, this allows to see the file sent to the
  prover.

  For interactive provers, this also allows to add or modify the
  corresponding proof script. The modifications are saved, and can be
  retrieved later even if the goal was modified.

MARCHE Claude's avatar
MARCHE Claude committed
249 250
\item[Replay] replay all obsolete proofs [NOT YET AVAILABLE]

251
\item[Remove] Removes a proof attempt or a transformation.
MARCHE Claude's avatar
MARCHE Claude committed
252 253 254 255 256

\end{description}

\subsection{Menus}

257
\paragraph{Menu \textsf{File}}
MARCHE Claude's avatar
MARCHE Claude committed
258
\begin{description}
259 260 261 262 263
\item[Add File] adds a file in the GUI
\item[Detect provers] runs provers auto-detection
\item[Preferences] opens a window for modifying preferred
  configuration, see details below
\item[Quit] exits the GUI
MARCHE Claude's avatar
MARCHE Claude committed
264
\end{description}
MARCHE Claude's avatar
MARCHE Claude committed
265

266 267 268 269 270 271 272 273 274 275 276 277 278 279 280
\paragraph{Menu \textsf{View}}
\begin{description}
\item[Expand All] expands all the rows of the tree view
\item[Collapse proved goals] closes all the rows of the tree view
  which are proved.
\item[Hide proved goals] completely hides the proved rows of the tree
  view [EXPERIMENTAL]
\end{description}

\paragraph{Menu \textsf{Tools}}
A copy of the tools already available in the left toolbar

\paragraph{Menu \textsf{Help}}
A very short online help, and some information about this software.

MARCHE Claude's avatar
MARCHE Claude committed
281 282
\subsection{Preferences}

MARCHE Claude's avatar
MARCHE Claude committed
283 284 285 286 287 288
The preferences window allows you customize
\begin{itemize}
\item the default editor to use when the \textsf{Edit} button is
  pressed. This might be overidden for a specific prover (the only way
  to do that for the moment is to manually edit the config file)
\item the time limit given to provers, in seconds
289
\item the maximal number of simultaneous provers allowed to run in parallel.
MARCHE Claude's avatar
MARCHE Claude committed
290 291
\end{itemize}

MARCHE Claude's avatar
MARCHE Claude committed
292 293
\subsection{Structure of the database file}

294 295 296 297
[TO BE COMPLETED LATER]

\section{The \texttt{why3ml} tool}

298 299 300 301 302 303 304 305 306 307 308 309 310 311
\texttt{why3ml} is an additional layer on \why\ library for
generating verification conditions from \whyml\ programs.
The command-line of \texttt{why3ml} is identical to that of
\texttt{why3}, but also accepts files with extension \texttt{.mlw} as
input files containing \whyml\ modules (see chapter~\ref{chap:whyml}
and section~\ref{sec:syntax:whyml}). Modules are turned into
theories containing verification conditions as goals, and then
\texttt{why3ml} behaves exactly as \texttt{why3} for the remaining of
the process.
Note that files with extension \texttt{.mlw} can also be loaded in
\texttt{why3ide}.

For those who want to experiment with \whyml, many examples are provided in
\texttt{examples/programs}.
MARCHE Claude's avatar
doc  
MARCHE Claude committed
312

313
\section{The \texttt{why3bench} tool}
MARCHE Claude's avatar
MARCHE Claude committed
314 315

The \texttt{why3bench} tool adds a scheduler on top of the \why\
316
library. \texttt{why3bench} is designed to compare various components
MARCHE Claude's avatar
MARCHE Claude committed
317 318 319 320
of automatic proofs: automatic provers, transformations, definitions
of a theory. For that goal it tries to prove predefined goals using
each component to compare. \texttt{why3bench} allows to output the
comparison in various formats:
François Bobot's avatar
François Bobot committed
321
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
322
\item csv: the simpler and more informative format, the results are
François Bobot's avatar
François Bobot committed
323
  represented in an array, the rows corresponds to the
MARCHE Claude's avatar
MARCHE Claude committed
324 325 326 327 328 329 330
  compared components, the columns correspond to the result
  (Valid,Unknown,Timout,Failure,Invalid) and the CPU time taken in seconds.
\item average: summarizes the number of the five different answers
  for each component. It also gives the average time taken.
\item timeline: for each component it gives the number of valid goals
  along the time (10 slices between 0 and the longest time a component
  takes to prove a goal)
François Bobot's avatar
François Bobot committed
331
\end{itemize}
332

MARCHE Claude's avatar
MARCHE Claude committed
333
The compared components can be defined in an \emph{rc-file},
MARCHE Claude's avatar
MARCHE Claude committed
334
\texttt{examples/programs/\ prgbench.rc} is such an example. More
MARCHE Claude's avatar
MARCHE Claude committed
335
generally a bench configuration file:
François Bobot's avatar
François Bobot committed
336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373
\begin{verbatim}
[probs "myprobs"]
   file = "examples/monbut.why" #relatives to the rc file
   file = "examples/monprogram.mlw"
   theory = "monprogram.T"
   goal = "monbut.T.G"

   transform = "split_goal" #applied in this order
   transform = "..."
   transform = "..."

[tools "mytools"]
   prover = cvc3
   prover = altergo
   #or only one
   driver = "..."
   command = "..."

   loadpath = "..." #added to the one in why.conf
   loadpath = "..."

   timelimit = 30
   memlimit = 300

   use = "toto.T" #use the theory toto (allow to add metas)

   transform = "simplify_array" #only 1 to 1 transformation

[bench "mybench"]
   tools = "mytools"
   tools = ...
   probs = "myprobs"
   probs = ...
   timeline = "prgbench.time"
   average = "prgbench.avg"
   csv = "prgbench.csv"
\end{verbatim}

374
Such a file can define three families \texttt{tools,probs,bench}. The
MARCHE Claude's avatar
MARCHE Claude committed
375 376 377 378
sections \texttt{tools} define a set of components to compare, the
sections \texttt{probs} define a set of goals on which to compare some
components and the sections \texttt{bench} define which components to
compare using which goals. It refers by name to the sections
François Bobot's avatar
François Bobot committed
379 380
\texttt{tools} and \texttt{probs} defined in the same file. The order
of the definitions is irrelevant. Notice that \texttt{loadpath} in a family
381
\texttt{tools} can be used to compare different axiomatizations.
François Bobot's avatar
François Bobot committed
382 383 384 385 386 387

One can run all the bench given in one bench configuration file with
\texttt{why3bench} :
\begin{verbatim}
why3bench -B path_to_my_bench.rc
\end{verbatim}
388

MARCHE Claude's avatar
MARCHE Claude committed
389
\section{The \texttt{why.conf} configuration file}
390
\label{sec:whyconffile}
391 392
One can use a custom configuration file. \texttt{why3config}
and other \texttt{why3} tools use priorities for which
393 394
user's configuration file to consider:
\begin{itemize}
395
\item the file specified by the \texttt{-C} or \texttt{-{}-config} options,
396
\item the file specified by the environment variable
397 398 399 400
  \texttt{WHY3CONFIG} if set.
\item the file \texttt{\$HOME/.why.conf}
  (\texttt{\$USERPROFILE/.why.conf} under Windows) or, in the case of
  local installation, \texttt{why.conf} in Why3 sources top directory.
401
\end{itemize}
402
If none of these files exists, a built-in default configuration is used.
403

404 405 406
The configuration file is a human-readable text file, which consists
of association pairs arranged in sections. Here follows an example of
configuration file.
407 408 409 410

\begin{verbatim}
[main ]
loadpath = "/usr/local/share/why3/theories"
411
magic = 2
412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438
memlimit = 0
running_provers_max = 2
timelimit = 10

[ide ]
default_editor = "emacs"
task_height = 384
tree_width = 438
verbose = 0
window_height = 779
window_width = 638

[prover coq]
command = "coqc %f"
driver = "/usr/local/share/why3/drivers/coq.drv"
editor = "coqide"
name = "Coq"
version = "8.2pl2"

[prover alt-ergo]
command = "why3-cpulimit %t %m alt-ergo %f"
driver = "/usr/local/share/why3/drivers/alt_ergo.drv"
editor = ""
name = "Alt-Ergo"
version = "0.91"
\end{verbatim}

439 440
A section begins with a header inside square brackets and ends at the
beginning of the next section. The header of a
441 442 443 444 445
section can be only one identifier, \texttt{main} and \texttt{ide} in
the example, or it can be composed by a family name and one family
argument, \texttt{prover} is one family name, \texttt{coq} and
\texttt{alt-ergo} are the family argument.

446
Inside a section, one key can be associated with an integer (.eg -555),
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
447
a boolean (true, false) or a string (\eg{} "emacs"). One key can appear
448 449
only once except if its a multi-value key. The order of apparition of
the keys inside a section matter only for the multi-value key.
MARCHE Claude's avatar
MARCHE Claude committed
450

451
\section{Drivers of External Provers}
452
\label{sec:drivers}
453 454 455 456 457 458 459

The drivers of external provers are readable files, in directory
\texttt{drivers}. Experimented users can modify them to change the way
the external provers are called, in particular which transformations
are applied to goals.

[TO BE COMPLETED LATER]
MARCHE Claude's avatar
MARCHE Claude committed
460 461

\section{Transformations}
MARCHE Claude's avatar
MARCHE Claude committed
462
\label{sec:transformations}
MARCHE Claude's avatar
MARCHE Claude committed
463

464 465 466 467
Here is a quick documentation of provided transformations. We give
first the non-splitting ones, \eg{} those which produce one goal as
result, and others which produces any number of goals.

468 469 470 471 472 473
Notice that the set of available transformations in your own
installation is given by
\begin{verbatim}
why3 --list-transforms
\end{verbatim}

MARCHE Claude's avatar
MARCHE Claude committed
474 475 476
\subsection{Non-splitting transformations}

\begin{description}
477

MARCHE Claude's avatar
MARCHE Claude committed
478 479
\item[eliminate\_algebraic] Replaces algebraic data types by first-order
definitions~\cite{paskevich09rr}
480

481 482
\item[eliminate\_builtin] Suppress definitions of symbols which are
  declared as builtin in the driver, i.e. with a ``syntax'' rule.
MARCHE Claude's avatar
MARCHE Claude committed
483
\item[eliminate\_definition\_func]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
484
  Replaces all function definitions with axioms.
MARCHE Claude's avatar
MARCHE Claude committed
485
\item[eliminate\_definition\_pred]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
486 487 488 489 490 491 492
  Replaces all predicate definitions with axioms.
\item[eliminate\_definition]
  Apply both transformations above.
\item[eliminate\_mutual\_recursion]
  Replaces mutually recursive definitions with axioms.
\item[eliminate\_recursion]
  Replaces all recursive definitions with axioms.
493

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
494 495 496
\item[eliminate\_if\_term] replaces terms of the form \texttt{if
    formula then t2 else t3} by lifting them at the level of formulas.
  This may introduce \texttt{if then else } in formulas.
497

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
498 499
\item[eliminate\_if\_fmla] replaces formulas of the form \texttt{if f1 then f2
  else f3} by an equivalent formula using implications and other
500
  connectives.
501

MARCHE Claude's avatar
MARCHE Claude committed
502
\item[eliminate\_if]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
503
  Apply both transformations above.
504

505
\item[eliminate\_inductive] replaces inductive predicates by
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
506 507
  (incomplete) axiomatic definitions, i.e. construction axioms and
  an inversion axiom.
508

MARCHE Claude's avatar
MARCHE Claude committed
509
\item[eliminate\_let\_fmla]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
510 511
  Eliminates \texttt{let} by substitution, at the predicate level.

MARCHE Claude's avatar
MARCHE Claude committed
512
\item[eliminate\_let\_term]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
513 514
  Eliminates \texttt{let} by substitution, at the term level.

515
\item[eliminate\_let]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
516
  Apply both transformations above.
517

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
518 519 520
% \item[encoding\_decorate\_mono]

% \item[encoding\_enumeration]
521

MARCHE Claude's avatar
MARCHE Claude committed
522
\item[encoding\_smt]
523 524
  Encode polymorphic types into monomorphic type~\cite{conchon08smt}.

MARCHE Claude's avatar
MARCHE Claude committed
525
\item[encoding\_tptp]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
526
  Encode theories into unsorted logic. %~\cite{cruanes10}.
527

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
528 529 530 531 532 533 534 535
% \item[filter\_trigger] *)

% \item[filter\_trigger\_builtin] *)

% \item[filter\_trigger\_no\_predicate] *)

% \item[hypothesis\_selection] *)
%   Filter hypothesis of goals~\cite{couchot07ftp,cruanes10}. *)
536

MARCHE Claude's avatar
MARCHE Claude committed
537
\item[inline\_all]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
538 539 540 541 542
  expands all non-recursive definitions.

\item[inline\_goal] Expands all outermost symbols of the goal that
  have a non-recursive definition.

MARCHE Claude's avatar
MARCHE Claude committed
543
\item[inline\_trivial]
544
  removes definitions of the form
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
545

546
\begin{verbatim}
547 548
function  f x_1 .. x_n = (g e_1 .. e_k)
predicate p x_1 .. x_n = (q e_1 .. e_k)
549
\end{verbatim}
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
550 551 552 553 554
when each $e_i$ is either a ground term or one of the $x_j$, and
each $x_1$ .. $x_n$ occur at most once in the $e_i$

\item[introduce\_premises] moves antecedents of implications and
  universal quantifications of the goal into the premises of the task.
555

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
556 557
% \item[remove\_triggers] *)
%   removes the triggers in all quantifications. *)
558

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
559 560
\item[simplify\_array] Automatically rewrites the task using the lemma
  \verb|Select_eq| of theory \verb|array.Array|.
561

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
562 563
\item[simplify\_formula] reduces trivial equalities $t=t$ to true and
  then simplifies propositional structure: removes true, false, ``f
564
  and f'' to ``f'', etc.
565 566 567

\item[simplify\_recursive\_definition] reduces mutually recursive
  definitions if they are not really mutually recursive, e.g.:
568
\begin{verbatim}
569
function f : ... = .... g ...
570 571 572 573 574

with g : .. = e
\end{verbatim}
becomes
\begin{verbatim}
575 576
function g : .. = e
function f : ... = .... g ...
577 578 579
\end{verbatim}
if f does not occur in e

MARCHE Claude's avatar
MARCHE Claude committed
580
\item[simplify\_trivial\_quantification]
581 582 583 584 585 586 587 588 589
  simplifies quantifications of the form
\begin{verbatim}
  forall x, x=t -> P(x)
\end{verbatim}
or
\begin{verbatim}
  forall x, t=x -> P(x)
\end{verbatim}
  when x does not occur in t
590
  into
591 592 593 594 595
\begin{verbatim}
P(t)
\end{verbatim}
  More generally, it applies this simplification whenever x=t appear
  in a negative position.
596

MARCHE Claude's avatar
MARCHE Claude committed
597
\item[simplify\_trivial\_quantification\_in\_goal]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
598
  same as above but applies only in the goal.
599

MARCHE Claude's avatar
MARCHE Claude committed
600
\item[split\_premise]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
601
  splits conjunctive premises.
602

MARCHE Claude's avatar
MARCHE Claude committed
603 604 605 606 607
\end{description}

\subsection{Splitting transformations}

\begin{description}
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
608 609 610 611 612 613 614 615 616 617 618

\item[full\_split\_all]
  composition of \texttt{split\_premise} and \texttt{full\_split\_goal}.

\item[full\_split\_goal] puts the goal in a conjunctive form,
  returns the corresponding set of subgoals. The number of subgoals
  generated may be exponential in the size of the initial goal.

\item[simplify\_formula\_and\_task] same as \texttt{simplify\_formula}
  but also removes the goal if it is equivalent to true.

MARCHE Claude's avatar
MARCHE Claude committed
619
\item[split\_all]
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
620
  composition of \texttt{split\_premise} and \texttt{split\_goal}.
621 622

\item[split\_goal] if the goal is a conjunction of goals, returns the
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
623 624 625 626 627 628
  corresponding set of subgoals. The number of subgoals generated is linear in
  the size of the initial goal.

\item[split\_intro]
  when a goal is an implication, moves the antecedents into the premises.

MARCHE Claude's avatar
MARCHE Claude committed
629 630
\end{description}

MARCHE Claude's avatar
MARCHE Claude committed
631

MARCHE Claude's avatar
doc  
MARCHE Claude committed
632 633 634 635 636 637

%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: