manpages.tex 2.85 KB
 MARCHE Claude committed Sep 06, 2010 1 2 3 4 \chapter{Reference manuals for the Why3 tools} \section{Compilation, Installation}  MARCHE Claude committed Sep 07, 2010 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 Compilation of Why3 must start with a configuration phase which is run as \begin{verbatim} ./configure \end{verbatim} This analyzes you current configuration and check if requirements hold. Compilation requires: \begin{itemize} \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 \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/} \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} \item TODO: sqlite3 \end{itemize}  MARCHE Claude committed Sep 06, 2010 30 \section{Installation of external provers}  MARCHE Claude committed Sep 06, 2010 31 32 33 34 35 36 37  \section{The \texttt{why3} command-line tool} \section{The \texttt{why3ml} tool} \section{The \texttt{why3ide} tool}  MARCHE Claude committed Sep 06, 2010 38 39 \section{The \texttt{why.conf} configuration file}  MARCHE Claude committed Sep 08, 2010 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 \section{Drivers of external provers} \section{Transformations} \subsection{Non-splitting transformations} \begin{description} \item[eliminate\_algebraic] Replaces algebraic data types by first-order definitions~\cite{paskevich09rr} \item[eliminate\_builtin] \item[eliminate\_definition] \item[eliminate\_definition\_func] \item[eliminate\_definition\_pred] \item[eliminate\_if] \item[eliminate\_if\_fmla] \item[eliminate\_if\_term] \item[eliminate\_inductive] \item[eliminate\_let] \item[eliminate\_let\_fmla] \item[eliminate\_let\_term] \item[eliminate\_mutual\_recursion] \item[eliminate\_recursion] \item[encoding\_decorate\_mono] \item[encoding\_enumeration] \item[encoding\_simple2] \item[encoding\_smt]  MARCHE Claude committed Sep 08, 2010 66 Should we cite \cite{conchon08smt} here?  MARCHE Claude committed Sep 08, 2010 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 \item[encoding\_tptp] \item[filter\_trigger] \item[filter\_trigger\_builtin] \item[filter\_trigger\_no\_predicate] \item[hypothesis\_selection] \item[inline\_all] \item[inline\_trivial] \item[remove\_triggers] \item[simplify\_array] \item[simplify\_formula] \item[simplify\_recursive\_definition] \item[simplify\_trivial\_quantification] \item[simplify\_trivial\_quantification\_in\_goal] \item[split\_premise] \end{description} \subsection{Splitting transformations} \begin{description} \item[right\_split] \item[simplify\_formula\_and\_task] \item[split\_all] \item[split\_goal] \item[split\_goal\_pos\_all] \item[split\_goal\_pos\_axiom] \item[split\_goal\_pos\_goal] \item[split\_goal\_pos\_neg\_all] \item[split\_goal\_pos\_neg\_axiom] \item[split\_goal\_pos\_neg\_goal] \end{description}  MARCHE Claude committed Sep 06, 2010 98   MARCHE Claude committed Sep 06, 2010 99 100 101 102 103 104  %%% Local Variables: %%% mode: latex %%% TeX-PDF-mode: t %%% TeX-master: "manual" %%% End: