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 20.6 KB
 Jean-Christophe Filliâtre committed Dec 17, 2010 1 \chapter{Reference manuals for the \why\ tools}  MARCHE Claude committed Sep 08, 2010 2 \label{chap:manpages}  MARCHE Claude committed Sep 06, 2010 3 4  \section{Compilation, Installation}  MARCHE Claude committed Dec 13, 2010 5 \label{sec:install}  MARCHE Claude committed Sep 06, 2010 6   Jean-Christophe Filliâtre committed Dec 17, 2010 7 Compilation of \why\ must start with a configuration phase which is run as  MARCHE Claude committed Sep 07, 2010 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 committed Dec 08, 2010 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 committed Sep 07, 2010 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 committed Dec 13, 2010 22 \end{itemize}  MARCHE Claude committed Sep 07, 2010 23   MARCHE Claude committed Dec 13, 2010 24 25 For the IDE, additional Ocaml libraries are needed: \begin{itemize}  MARCHE Claude committed Sep 07, 2010 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 committed Dec 13, 2010 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 committed Sep 07, 2010 40 41 \end{itemize}  MARCHE Claude committed Dec 13, 2010 42 43 \subsection{Local use, without installation}  Jean-Christophe Filliâtre committed Dec 17, 2010 44 It is not mandatory to install \why\ to use it. Local use is obtained via  MARCHE Claude committed Dec 13, 2010 45 46 47 48 \begin{verbatim} ./configure --enable-local make \end{verbatim}  MARCHE Claude committed Dec 20, 2010 49 The \why\ executables are then available in the subdirectory \texttt{bin/}.  MARCHE Claude committed Dec 13, 2010 50   Jean-Christophe Filliâtre committed Dec 17, 2010 51 \subsection{Installation of the \why\ library}  MARCHE Claude committed Dec 16, 2010 52 53 \label{sec:installlib}  Jean-Christophe Filliâtre committed Dec 17, 2010 54 By default, the \why\ library is not installed. It can be installed using  MARCHE Claude committed Dec 16, 2010 55 56 57 58 \begin{verbatim} make byte opt make install_lib \end{verbatim}  MARCHE Claude committed Dec 16, 2010 59   MARCHE Claude committed Sep 06, 2010 60 \section{Installation of external provers}  MARCHE Claude committed Sep 06, 2010 61   Jean-Christophe Filliâtre committed Dec 17, 2010 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 committed Dec 13, 2010 64 65 them. There is no need to install these provers before compiling and installing Why.  MARCHE Claude committed Dec 13, 2010 66   MARCHE Claude committed Dec 13, 2010 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 committed Dec 13, 2010 69   Jean-Christophe Filliâtre committed Dec 17, 2010 70 For configuring \why\ to use the provers, follow intructions given in  MARCHE Claude committed Dec 13, 2010 71 Section~\ref{sec:why3config}.  MARCHE Claude committed Dec 13, 2010 72   MARCHE Claude committed Dec 13, 2010 73 74 \section{The \texttt{why3config} command-line tool} \label{sec:why3config}.  MARCHE Claude committed Dec 13, 2010 75   Jean-Christophe Filliâtre committed Dec 17, 2010 76 \why\ must be configured to access external provers. Typically, this is done  MARCHE Claude committed Dec 13, 2010 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}  Jean-Christophe Filliâtre committed Dec 17, 2010 89 of the \why\ data directory (\eg{}  MARCHE Claude committed Dec 13, 2010 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 committed Dec 15, 2010 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 committed Dec 13, 2010 113 \end{itemize}  MARCHE Claude committed Dec 13, 2010 114   Jean-Christophe Filliâtre committed Dec 17, 2010 115 \texttt{why3config} also detects the plugins installed in the \why\  François Bobot committed Dec 15, 2010 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 committed Dec 15, 2010 122 The option \texttt{--autodetect-provers} will detect again the available  François Bobot committed Dec 15, 2010 123 provers and will replace them in the file configuration.  MARCHE Claude committed Dec 15, 2010 124 \texttt{--autodetect-plugins} will do the same for plugins.  François Bobot committed Dec 15, 2010 125   MARCHE Claude committed Sep 06, 2010 126 \section{The \texttt{why3} command-line tool}  MARCHE Claude committed Dec 15, 2010 127 \label{sec:why3ref}  MARCHE Claude committed Sep 06, 2010 128   Jean-Christophe Filliâtre committed Dec 17, 2010 129 \why\ is primarily used to call provers on goals contains by file in  François Bobot committed Dec 15, 2010 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 committed Dec 20, 2010 165 166 \texttt{why3} call the prover sequentially, use \texttt{why3bench} if *) you want to call the provers concurrently. *)  MARCHE Claude committed Dec 17, 2010 167   François Bobot committed Dec 20, 2010 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 committed Dec 17, 2010 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} *)  François Bobot committed Dec 15, 2010 183   MARCHE Claude committed Dec 16, 2010 184 \section{The \texttt{why3ide} GUI}  MARCHE Claude committed Dec 13, 2010 185 186 \label{sec:ideref}  MARCHE Claude committed Dec 16, 2010 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 committed Dec 13, 2010 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 committed Dec 15, 2010 197 \subsection{Left toolbar actions}  MARCHE Claude committed Dec 13, 2010 198 199  \begin{description}  MARCHE Claude committed Dec 15, 2010 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 committed Dec 13, 2010 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 committed Dec 15, 2010 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 committed Dec 13, 2010 216 217 218 219 220 221 222 223 224 \item 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 committed Dec 15, 2010 225 226 \item[Replay] replay all obsolete proofs [NOT YET AVAILABLE]  MARCHE Claude committed Dec 20, 2010 227 \item[Remove] Removes a proof attempt or a transformation.  MARCHE Claude committed Dec 13, 2010 228 229 230 231 232  \end{description} \subsection{Menus}  MARCHE Claude committed Dec 20, 2010 233 \paragraph{Menu \textsf{File}}  MARCHE Claude committed Dec 13, 2010 234 \begin{description}  MARCHE Claude committed Dec 20, 2010 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 committed Dec 13, 2010 240 \end{description}  MARCHE Claude committed Dec 13, 2010 241   MARCHE Claude committed Dec 20, 2010 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 committed Dec 13, 2010 257 258 \subsection{Preferences}  MARCHE Claude committed Dec 15, 2010 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 committed Dec 13, 2010 268 269 \subsection{Structure of the database file}  MARCHE Claude committed Dec 17, 2010 270 271 272 273 [TO BE COMPLETED LATER] \section{The \texttt{why3ml} tool}  Jean-Christophe Filliâtre committed Dec 17, 2010 274 The \texttt{why3ml} is an additional layer on \why\ library for  MARCHE Claude committed Dec 17, 2010 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 committed Dec 20, 2010 280 \texttt{examples/\ programs}. The files \texttt{*.mlw} can be loaded in  MARCHE Claude committed Dec 17, 2010 281 282 283 the GUI. [TO BE COMPLETED LATER]  MARCHE Claude committed Sep 06, 2010 284   François Bobot committed Dec 15, 2010 285 \section{The \texttt{why3bench} tool}  MARCHE Claude committed Dec 20, 2010 286 287  The \texttt{why3bench} tool adds a scheduler on top of the \why\  François Bobot committed Dec 20, 2010 288 library. \texttt{why3bench} is designed to compare various components  MARCHE Claude committed Dec 20, 2010 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 committed Dec 20, 2010 293 \begin{itemize}  MARCHE Claude committed Dec 20, 2010 294 \item csv: the simpler and more informative format, the results are  François Bobot committed Dec 20, 2010 295  represented in an array, the rows corresponds to the  MARCHE Claude committed Dec 20, 2010 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 committed Dec 20, 2010 303 \end{itemize}  François Bobot committed Dec 15, 2010 304   MARCHE Claude committed Dec 20, 2010 305 The compared components can be defined in an \emph{rc-file},  MARCHE Claude committed Dec 20, 2010 306 \texttt{examples/programs/\ prgbench.rc} is such an example. More  MARCHE Claude committed Dec 20, 2010 307 generally a bench configuration file:  François Bobot committed Dec 20, 2010 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 committed Dec 20, 2010 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 committed Dec 20, 2010 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 committed Dec 20, 2010 353 \texttt{tools} can be used to compare different axiomatisation.  François Bobot committed Dec 20, 2010 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}  MARCHE Claude committed Dec 17, 2010 360   MARCHE Claude committed Sep 06, 2010 361 \section{The \texttt{why.conf} configuration file}  François Bobot committed Dec 15, 2010 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 committed Dec 17, 2010 422 a boolean (true, false) or a string (\eg{} "emacs"). One key can appear  François Bobot committed Dec 15, 2010 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 committed Sep 06, 2010 425   MARCHE Claude committed Sep 08, 2010 426 \section{Drivers of external provers}  Andrei Paskevich committed Dec 20, 2010 427 \label{sec:drivers}  MARCHE Claude committed Dec 17, 2010 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 committed Sep 08, 2010 435 436  \section{Transformations}  MARCHE Claude committed Dec 15, 2010 437 \label{sec:transformations}  MARCHE Claude committed Sep 08, 2010 438   MARCHE Claude committed Dec 17, 2010 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.  MARCHE Claude committed Dec 20, 2010 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 committed Sep 08, 2010 449 450 451 \subsection{Non-splitting transformations} \begin{description}  MARCHE Claude committed Dec 17, 2010 452   MARCHE Claude committed Sep 08, 2010 453 454 \item[eliminate\_algebraic] Replaces algebraic data types by first-order definitions~\cite{paskevich09rr}  MARCHE Claude committed Dec 17, 2010 455   MARCHE Claude committed Sep 09, 2010 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 committed Sep 08, 2010 458 \item[eliminate\_definition\_func]  MARCHE Claude committed Dec 17, 2010 459  Replaces all function definitions with axioms.  MARCHE Claude committed Sep 08, 2010 460 \item[eliminate\_definition\_pred]  MARCHE Claude committed Dec 17, 2010 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.  MARCHE Claude committed Dec 17, 2010 468   MARCHE Claude committed Dec 17, 2010 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.  MARCHE Claude committed Dec 17, 2010 472   MARCHE Claude committed Dec 17, 2010 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.  MARCHE Claude committed Dec 17, 2010 476   MARCHE Claude committed Sep 08, 2010 477 \item[eliminate\_if]  MARCHE Claude committed Dec 17, 2010 478  Apply both transformations above.  MARCHE Claude committed Dec 17, 2010 479   MARCHE Claude committed Sep 09, 2010 480 \item[eliminate\_inductive] replaces inductive predicates by  MARCHE Claude committed Dec 17, 2010 481 482  (incomplete) axiomatic definitions, i.e. construction axioms and an inversion axiom.  MARCHE Claude committed Dec 17, 2010 483   MARCHE Claude committed Sep 08, 2010 484 \item[eliminate\_let\_fmla]  MARCHE Claude committed Dec 17, 2010 485 486  Eliminates \texttt{let} by substitution, at the predicate level.  MARCHE Claude committed Sep 08, 2010 487 \item[eliminate\_let\_term]  MARCHE Claude committed Dec 17, 2010 488 489  Eliminates \texttt{let} by substitution, at the term level.  MARCHE Claude committed Sep 09, 2010 490 \item[eliminate\_let]  MARCHE Claude committed Dec 17, 2010 491  Apply both transformations above.  MARCHE Claude committed Dec 17, 2010 492   MARCHE Claude committed Dec 17, 2010 493 494 495 % \item[encoding\_decorate\_mono] % \item[encoding\_enumeration]  MARCHE Claude committed Dec 17, 2010 496   MARCHE Claude committed Sep 08, 2010 497 \item[encoding\_smt]  MARCHE Claude committed Dec 17, 2010 498 499  Encode polymorphic types into monomorphic type~\cite{conchon08smt}.  MARCHE Claude committed Sep 08, 2010 500 \item[encoding\_tptp]  MARCHE Claude committed Dec 17, 2010 501  Encode theories into unsorted logic. %~\cite{cruanes10}.  MARCHE Claude committed Dec 17, 2010 502   MARCHE Claude committed Dec 17, 2010 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}. *)  MARCHE Claude committed Dec 17, 2010 511   MARCHE Claude committed Sep 08, 2010 512 \item[inline\_all]  MARCHE Claude committed Dec 17, 2010 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 committed Sep 08, 2010 518 \item[inline\_trivial]  MARCHE Claude committed Sep 09, 2010 519  removes definitions of the form  MARCHE Claude committed Dec 17, 2010 520   MARCHE Claude committed Sep 09, 2010 521 522 523 \begin{verbatim} logic f x_1 .. x_n = (g e_1 .. e_k) \end{verbatim}  MARCHE Claude committed Dec 17, 2010 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.  MARCHE Claude committed Sep 09, 2010 529   MARCHE Claude committed Dec 17, 2010 530 531 % \item[remove\_triggers] *) % removes the triggers in all quantifications. *)  MARCHE Claude committed Dec 17, 2010 532   MARCHE Claude committed Dec 17, 2010 533 534 \item[simplify\_array] Automatically rewrites the task using the lemma \verb|Select_eq| of theory \verb|array.Array|.  MARCHE Claude committed Dec 17, 2010 535   MARCHE Claude committed Dec 17, 2010 536 537 \item[simplify\_formula] reduces trivial equalities $t=t$ to true and then simplifies propositional structure: removes true, false, f  MARCHE Claude committed Sep 09, 2010 538  and f'' to f'', etc.  MARCHE Claude committed Dec 17, 2010 539 540 541  \item[simplify\_recursive\_definition] reduces mutually recursive definitions if they are not really mutually recursive, e.g.:  MARCHE Claude committed Sep 09, 2010 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 committed Sep 08, 2010 554 \item[simplify\_trivial\_quantification]  MARCHE Claude committed Sep 09, 2010 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 committed Sep 08, 2010 571 \item[simplify\_trivial\_quantification\_in\_goal]  MARCHE Claude committed Dec 17, 2010 572  same as above but applies only in the goal.  MARCHE Claude committed Dec 17, 2010 573   MARCHE Claude committed Sep 08, 2010 574 \item[split\_premise]  MARCHE Claude committed Dec 17, 2010 575  splits conjunctive premises.  MARCHE Claude committed Dec 17, 2010 576   MARCHE Claude committed Sep 08, 2010 577 578 579 580 581 \end{description} \subsection{Splitting transformations} \begin{description}  MARCHE Claude committed Dec 17, 2010 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 committed Sep 08, 2010 593 \item[split\_all]  MARCHE Claude committed Dec 17, 2010 594  composition of \texttt{split\_premise} and \texttt{split\_goal}.  MARCHE Claude committed Dec 17, 2010 595 596  \item[split\_goal] if the goal is a conjunction of goals, returns the  MARCHE Claude committed Dec 17, 2010 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 committed Sep 08, 2010 603 604 \end{description}  MARCHE Claude committed Sep 06, 2010 605   MARCHE Claude committed Sep 06, 2010 606 607 608 609 610 611  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: