manpages.tex 20.6 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
11
12
13
\begin{verbatim}
./configure
\end{verbatim}
This analyzes you current configuration and check if requirements hold.
Compilation requires:
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
14
15
16
\item The Objective Caml compiler, version 3.10 or higher. It is
  available as a binary package for most Unix distributions. For
  debian-based Linux distributions, you can install the packages
MARCHE Claude's avatar
MARCHE Claude committed
17
18
19
20
21
\begin{verbatim}
ocaml ocaml-native-compilers
\end{verbatim}
It is also installable from sources, downloadable from the Web site
\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

MARCHE Claude's avatar
add    
MARCHE Claude committed
24
25
For the IDE, additional Ocaml libraries are needed:
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
26
27
28
29
30
31
32
\item The Lablgtk2 library for Ocaml bindings of the gtk2 graphical library.
 For debian-based Linux distributions, you can install the packages
\begin{verbatim}
liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev
\end{verbatim}
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
36
37
38
39
\item The Ocaml bindings of the sqlite3 library
For debian-based Linux distributions, you can install the package
\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
40
41
\end{itemize}

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

44
It is not mandatory to install \why\ to use it. Local use is obtained via
MARCHE Claude's avatar
add    
MARCHE Claude committed
45
46
47
48
\begin{verbatim}
./configure --enable-local
make
\end{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
49
The \why\ executables are then available in the subdirectory \texttt{bin/}.
MARCHE Claude's avatar
add    
MARCHE Claude committed
50

51
\subsection{Installation of the \why\ library}
MARCHE Claude's avatar
MARCHE Claude committed
52
53
\label{sec:installlib}

54
By default, the \why\ library is not installed. It can be installed using
55
56
57
58
\begin{verbatim}
make byte opt
make install_lib
\end{verbatim}
MARCHE Claude's avatar
MARCHE Claude committed
59

MARCHE Claude's avatar
MARCHE Claude committed
60
\section{Installation of external provers}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
61

62
63
\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
64
65
them. There is no need to install these provers before compiling and
installing Why. 
MARCHE Claude's avatar
add    
MARCHE Claude committed
66

MARCHE Claude's avatar
MARCHE Claude committed
67
68
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
69

70
For configuring \why\ to use the provers, follow intructions given in
MARCHE Claude's avatar
MARCHE Claude committed
71
Section~\ref{sec:why3config}.
MARCHE Claude's avatar
add    
MARCHE Claude committed
72

MARCHE Claude's avatar
MARCHE Claude committed
73
74
\section{The \texttt{why3config} command-line tool}
\label{sec:why3config}.
MARCHE Claude's avatar
add    
MARCHE Claude committed
75

76
\why\ must be configured to access external provers. Typically, this is done
MARCHE Claude's avatar
MARCHE Claude committed
77
78
79
80
81
82
83
84
85
86
87
88
by running either the command line tool
\begin{verbatim}
why3config
\end{verbatim}
or using the menu
\begin{verbatim}
File/Detect provers
\end{verbatim}
of the IDE. This must be done again each time a new prover is installed.

The set of all provers which are attempted to detect is described in
the readable configuration file \texttt{provers-detection-data.conf}
89
of the \why\ data directory (\eg{}
MARCHE Claude's avatar
MARCHE Claude committed
90
91
92
93
94
95
96
97
98
99
100
101
102
\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).

The result of the prover detection is stored in the user's
configuration file (\eg{} \texttt{~/.why.conf}). Again, this file is
human readable, and advanced users may modify it in order to
experiment different ways of calling provers, \eg{} different versions
of the same prover, or with different options.

The provers which are typically attemped for detection are
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
103
104
105
106
107
108
109
110
111
112
\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
113
\end{itemize}
MARCHE Claude's avatar
add    
MARCHE Claude committed
114

115
\texttt{why3config} also detects the plugins installed in the \why\
116
117
118
119
120
121
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,
\texttt{why3config} will only reset unset variables to default value.
MARCHE Claude's avatar
MARCHE Claude committed
122
The option \texttt{--autodetect-provers} will detect again the available
123
provers and will replace them in the file configuration.
MARCHE Claude's avatar
MARCHE Claude committed
124
\texttt{--autodetect-plugins} will do the same for plugins.
125

MARCHE Claude's avatar
doc  
MARCHE Claude committed
126
\section{The \texttt{why3} command-line tool}
MARCHE Claude's avatar
MARCHE Claude committed
127
\label{sec:why3ref}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
128

129
\why\ is primarily used to call provers on goals contains by file in
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
why3 format \texttt{.why} extension. However plugins can register
parser which can extend the known format. \texttt{why3ml} apply the
following steps :
\begin{enumerate}
\item Parse the command line and report error if needed
\item Read the configuration file using the priority defined in
  section\ref{sec:whyconffile}
\item Load the plugins mentionned in the configuration. It will not
  stop if a plugin fail to load.
\item Parse and type the given files using the correct parser in order
  to obtain a set of why theory for each files. It uses
  the filename extension or the \texttt{--format} options to choose
  among the available parsers. \texttt{--list-format} gives the list
  of them.
\item Extract the selected goals inside each selected theories into
  tasks. The goals and theories are selected using the options
  \texttt{-G/--goal} and \texttt{-T/--theory}. One
  \texttt{-T/--theory} applies to the last file appearing on the
  commandline, one \texttt{-G/--goal} applies to the last theory
  appearing on the commandline. If none theories are selected in one
  file, they are all selected. If none goals are selected inside one
  selected theory, they are all selected.
\item Apply the transformation requested
  with \texttt{-a/--apply-transform} in the order they appear on the
  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}
  option. \texttt{--list-provers} lists the known provers, ie the one
  which appear in the configuration file.
\item Print the result of the standard output if \texttt{-D/--driver}
  is used or call the prover and print the result if
  \texttt{-P/--prover} is used.
\end{enumerate}

François Bobot's avatar
François Bobot committed
165
166
\texttt{why3} call the prover sequentially, use \texttt{why3bench} if *)
you want to call the provers concurrently.  *)
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
167

François Bobot's avatar
François Bobot committed
168
169
170
171
172
173
174
175
The provers can answer the following output :
\begin{itemize}
\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
\end{itemize}
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
176
177
178
179
180
181
182
% \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} *)
183

184
\section{The \texttt{why3ide} GUI}
MARCHE Claude's avatar
MARCHE Claude committed
185
186
\label{sec:ideref}

187
188
189
190
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
191
192
193
194
195
196
\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
197
\subsection{Left toolbar actions}
MARCHE Claude's avatar
MARCHE Claude committed
198
199

\begin{description}
MARCHE Claude's avatar
MARCHE Claude committed
200
201
202
203
204
205
\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
206
207
208
209
\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
210
211
212
213
214
215
\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
216
217
218
219
220
221
222
223
224
\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
225
226
\item[Replay] replay all obsolete proofs [NOT YET AVAILABLE]

MARCHE Claude's avatar
MARCHE Claude committed
227
\item[Remove] Removes a proof attempt or a transformation. 
MARCHE Claude's avatar
MARCHE Claude committed
228
229
230
231
232

\end{description}

\subsection{Menus}

233
\paragraph{Menu \textsf{File}}
MARCHE Claude's avatar
MARCHE Claude committed
234
\begin{description}
235
236
237
238
239
\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
240
\end{description}
MARCHE Claude's avatar
MARCHE Claude committed
241

242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
\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
257
258
\subsection{Preferences}

MARCHE Claude's avatar
MARCHE Claude committed
259
260
261
262
263
264
265
266
267
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
\item the maximal number of simultaneous provers allowed to run in parallel. 
\end{itemize}

MARCHE Claude's avatar
MARCHE Claude committed
268
269
\subsection{Structure of the database file}

270
271
272
273
[TO BE COMPLETED LATER]

\section{The \texttt{why3ml} tool}

274
The \texttt{why3ml} is an additional layer on \why\ library for
275
276
277
278
279
generating verification conditions from WhyML programs. This tool and
the syntax of WhyML programs is intentionally left undocumented since
it might evolve significantly in the near future.

For those who want to experiment with it, examples are provided in
MARCHE Claude's avatar
MARCHE Claude committed
280
\texttt{examples/\ programs}. The files \texttt{*.mlw} can be loaded in
281
282
283
the GUI.

[TO BE COMPLETED LATER]
MARCHE Claude's avatar
doc  
MARCHE Claude committed
284

285
\section{The \texttt{why3bench} tool}
MARCHE Claude's avatar
MARCHE Claude committed
286
287

The \texttt{why3bench} tool adds a scheduler on top of the \why\
288
library. \texttt{why3bench} is designed to compare various components
MARCHE Claude's avatar
MARCHE Claude committed
289
290
291
292
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
293
\begin{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
294
\item csv: the simpler and more informative format, the results are
François Bobot's avatar
François Bobot committed
295
  represented in an array, the rows corresponds to the
MARCHE Claude's avatar
MARCHE Claude committed
296
297
298
299
300
301
302
  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
303
\end{itemize}
304

MARCHE Claude's avatar
MARCHE Claude committed
305
The compared components can be defined in an \emph{rc-file},
MARCHE Claude's avatar
MARCHE Claude committed
306
\texttt{examples/programs/\ prgbench.rc} is such an example. More
MARCHE Claude's avatar
MARCHE Claude committed
307
generally a bench configuration file:
François Bobot's avatar
François Bobot committed
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
\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}

MARCHE Claude's avatar
MARCHE Claude committed
346
347
348
349
350
Such a file can defined three families \texttt{tools,probs,bench}. The
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
351
352
\texttt{tools} and \texttt{probs} defined in the same file. The order
of the definitions is irrelevant. Notice that \texttt{loadpath} in a family
MARCHE Claude's avatar
MARCHE Claude committed
353
\texttt{tools} can be used to compare different axiomatisation.
François Bobot's avatar
François Bobot committed
354
355
356
357
358
359

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}
360

MARCHE Claude's avatar
MARCHE Claude committed
361
\section{The \texttt{why.conf} configuration file}
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
\label{sec:whyconffile}
One can defined more than one configuration file. \texttt{why3config}
and all the others \texttt{why3}'s tools use priorities for which
user's configuration file to consider:
\begin{itemize}
\item the file specified by the \texttt{-C} or \texttt{--config} options,
\item the file specified by the environment variable
  \texttt{\$WHY\_CONFIG} if set.
\item the file \texttt{why.conf} or \texttt{.why.conf} in the current
  directory.
\item the file \texttt{\$HOME/.why.conf} or \texttt{\$USERPROFILE/.why.conf}
\end{itemize}
If none of this file exists a built-in default configuration is used
which is saved in a default configuration filename, which is usually
\texttt{\$HOME/.why.conf}.

The configuration file is a human-readable text file, which is
composed by association pairs arranged by sections. Here an example of
a configuration file.

\begin{verbatim}
[main ]
datadir = "/usr/local/share/why3"
libdir = "/usr/local/lib/why3"
loadpath = "/usr/local/share/why3/theories"
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}

A section begin with an header inside square brackets and end at the
next square brackets. Sections can't be nested. The header of a
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.

Inside a section, one key can be associated to an integer (.eg -555),
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
422
a boolean (true, false) or a string (\eg{} "emacs"). One key can appear
423
424
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
425

MARCHE Claude's avatar
MARCHE Claude committed
426
\section{Drivers of external provers}
427
\label{sec:drivers}
428
429
430
431
432
433
434

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
435
436

\section{Transformations}
MARCHE Claude's avatar
MARCHE Claude committed
437
\label{sec:transformations}
MARCHE Claude's avatar
MARCHE Claude committed
438

439
440
441
442
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.

443
444
445
446
447
448
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
449
450
451
\subsection{Non-splitting transformations}

\begin{description}
452

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

456
457
\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
458
\item[eliminate\_definition\_func]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
459
  Replaces all function definitions with axioms.
MARCHE Claude's avatar
MARCHE Claude committed
460
\item[eliminate\_definition\_pred]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
461
462
463
464
465
466
467
  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.
468

MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
469
470
471
\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.
472

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

MARCHE Claude's avatar
MARCHE Claude committed
477
\item[eliminate\_if]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
478
  Apply both transformations above.
479

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

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

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

490
\item[eliminate\_let]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
491
  Apply both transformations above.
492

MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
493
494
495
% \item[encoding\_decorate\_mono]

% \item[encoding\_enumeration]
496

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

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

MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
503
504
505
506
507
508
509
510
% \item[filter\_trigger] *)

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
512
\item[inline\_all]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
513
514
515
516
517
  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
518
\item[inline\_trivial]
519
  removes definitions of the form
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
520

521
522
523
\begin{verbatim}
logic f x_1 .. x_n = (g e_1 .. e_k)
\end{verbatim}
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
524
525
526
527
528
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.
529

MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
530
531
% \item[remove\_triggers] *)
%   removes the triggers in all quantifications. *)
532

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

MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
536
537
\item[simplify\_formula] reduces trivial equalities $t=t$ to true and
  then simplifies propositional structure: removes true, false, ``f
538
  and f'' to ``f'', etc.
539
540
541

\item[simplify\_recursive\_definition] reduces mutually recursive
  definitions if they are not really mutually recursive, e.g.:
542
543
544
545
546
547
548
549
550
551
552
553
\begin{verbatim}
logic f : ... = .... g ...

with g : .. = e
\end{verbatim}
becomes
\begin{verbatim}
logic g : .. = e
logic f : ... = .... g ...
\end{verbatim}
if f does not occur in e

MARCHE Claude's avatar
MARCHE Claude committed
554
\item[simplify\_trivial\_quantification]
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
  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
  into 
\begin{verbatim}
P(t)
\end{verbatim}
  More generally, it applies this simplification whenever x=t appear
  in a negative position.
  
MARCHE Claude's avatar
MARCHE Claude committed
571
\item[simplify\_trivial\_quantification\_in\_goal]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
572
  same as above but applies only in the goal.
573

MARCHE Claude's avatar
MARCHE Claude committed
574
\item[split\_premise]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
575
  splits conjunctive premises.
576

MARCHE Claude's avatar
MARCHE Claude committed
577
578
579
580
581
\end{description}

\subsection{Splitting transformations}

\begin{description}
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
582
583
584
585
586
587
588
589
590
591
592

\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
593
\item[split\_all]
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
594
  composition of \texttt{split\_premise} and \texttt{split\_goal}.
595
596

\item[split\_goal] if the goal is a conjunction of goals, returns the
MARCHE Claude's avatar
roadmap    
MARCHE Claude committed
597
598
599
600
601
602
  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
603
604
\end{description}

MARCHE Claude's avatar
MARCHE Claude committed
605

MARCHE Claude's avatar
doc  
MARCHE Claude committed
606
607
608
609
610
611

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