technical.tex 22.7 KB
Newer Older
1
\chapter{Technical Informations}
2
%HEVEA\cutname{technical.html}
3 4 5 6 7 8 9

\section{Structure of Session Files}

The proof session state is stored in an XML file named
\texttt{\textsl{<dir>}/why3session.xml}, where \texttt{\textsl{<dir>}}
is the directory of the project.
The XML file follows the DTD given in \texttt{share/why3session.dtd} and reproduced below.
10
\lstinputlisting{../share/why3session.dtd}
11 12


13
\section{Prover Detection}
14 15
\label{sec:proverdetecttiondata}

16
The data configuration for the automatic detection of
17 18
installed provers is stored in the file
\texttt{provers-detection-data.conf} typically located in directory
19
\verb|/usr/local/share/why3| after installation. The content of this
20
file is reproduced below.
21 22 23
%BEGIN LATEX
{\footnotesize
%END LATEX
24
\lstinputlisting[language={},morecomment={[l]\#},morestring={[b]"}]{../share/provers-detection-data.conf}
25 26 27
%BEGIN LATEX
}
%END LATEX
28

29
\section{The \texttt{why3.conf} Configuration File}
30 31 32
\label{sec:whyconffile}
\index{why3.conf@\texttt{why3.conf}}\index{configuration file}

33 34 35 36 37 38 39 40 41 42 43 44
One can use a custom configuration file. The \why
tools look for it in the following order:
\begin{enumerate}
\item the file specified by the \texttt{-C} or \texttt{-{}-config} options,
\item the file specified by the environment variable
  \texttt{WHY3CONFIG} if set,
\item the file \texttt{\$HOME/.why3.conf}
  (\texttt{\$USERPROFILE/.why3.conf} under Windows) or, in the case of
  local installation, \texttt{why3.conf} in the top directory of \why sources.
\end{enumerate}
If none of these files exist, a built-in default configuration is used.

45
A section begins with a header inside square brackets and ends at the
46 47 48
beginning of the next section. The header of a section can be a single
identifier, \eg \texttt{[main]}, or it can be composed by a family name
and a single family argument, \eg \texttt{[prover alt-ergo]}.
49

50
Sections contain associations \texttt{key=value}. A value is either
51 52 53
an integer (\eg \texttt{-555}), a boolean (\texttt{true}, \texttt{false}),
or a string (\eg \texttt{"emacs"}). Some specific keys can be attributed
multiple values and are
54
thus allowed to occur several times inside a given section. In that
55
case, the relative order of these associations matters.
56

57
\section{Drivers for External Provers}
58 59
\label{sec:drivers}

60
Drivers for external provers are readable files from directory
61 62 63 64 65 66 67 68 69
\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]

\section{Transformations}
\label{sec:transformations}

70 71 72 73 74
This section documents the available transformations. We first
describe the most important ones, and then we provide a quick
documentation of the others, first the non-splitting ones, \eg those
which produce exactly one goal as result, and the others which produce any
number of goals.
75 76 77 78 79 80

Notice that the set of available transformations in your own
installation is given by
\begin{verbatim}
why3 --list-transforms
\end{verbatim}
81
\index{list-transforms@\verb+--list-transforms+}
82

83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
\subsection{Inlining definitions}

Those transformations generally amount to replace some applications of
function or predicate symbols with its definition.

\begin{description}

\item[inline\_trivial]
  expands and removes definitions of the form
\begin{whycode}
function  f x_1 ... x_n = (g e_1 ... e_k)
predicate p x_1 ... x_n = (q e_1 ... e_k)
\end{whycode}
when each $e_i$ is either a ground term or one of the $x_j$, and
each $x_1 \dots x_n$ occurs at most once in all the $e_i$.
98
\index{inline-trivial@\verb+inline_trivial+}
99 100 101

\item[inline\_goal] expands all outermost symbols of the goal that
  have a non-recursive definition.
102
\index{inline-goal@\verb+inline_goal+}
103 104 105

\item[inline\_all]
  expands all non-recursive definitions.
106
\index{inline-all@\verb+inline_all+}
107 108 109 110 111 112

\end{description}


\subsection{Induction Transformations}

113
\begin{description}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
114
\item[induction\_ty\_lex]
115
  \index{induction-ty-lex@\verb+induction_ty_lex+}
116
  performs structural, lexicographic induction on
117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132
  goals involving universally quantified variables of algebraic data
  types, such as lists, trees, etc. For instance, it transforms the
  following goal
\begin{whycode}
goal G: forall l: list 'a. length l >= 0
\end{whycode}
  into this one:
\begin{whycode}
goal G :
  forall l:list 'a.
     match l with
     | Nil -> length l >= 0
     | Cons a l1 -> length l1 >= 0 -> length l >= 0
     end
\end{whycode}
  When induction can be applied to several variables, the transformation
133
  picks one heuristically. The \verb|[@induction]| attribute can be used to
MARCHE Claude's avatar
MARCHE Claude committed
134
  force induction over one particular variable, \eg with
135
\begin{whycode}
136
goal G: forall l1 [@induction] l2 l3: list 'a.
137 138
        l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3
\end{whycode}
139
induction will be applied on \verb|l1|. If this attribute is attached to
MARCHE Claude's avatar
MARCHE Claude committed
140 141
several variables, a lexicographic induction is performed on these
variables, from left to right.
142

MARCHE Claude's avatar
MARCHE Claude committed
143
%\item[] Induction on inductive predicates.
144

MARCHE Claude's avatar
MARCHE Claude committed
145 146 147
%[TO BE COMPLETED]

% TODO: implement also induction on int !
148

149
\end{description}
150 151 152

\subsection{Simplification by Computation}

153
These transformations simplify the goal by applying several kinds of
MARCHE Claude's avatar
MARCHE Claude committed
154 155 156 157
simplification, described below. The transformations differ only by
the kind of rules they apply:
\begin{description}
\item[compute\_in\_goal] aggressively applies all known
158
  computation/simplification rules.
MARCHE Claude's avatar
MARCHE Claude committed
159
  \index{compute-in-goal@\verb+compute_in_goal+}
160

MARCHE Claude's avatar
MARCHE Claude committed
161
\item[compute\_specified] performs rewriting using only built-in
162
  operators and user-provided rules.
MARCHE Claude's avatar
MARCHE Claude committed
163 164
  \index{compute-specified@\verb+compute_specified+}
\end{description}
165

MARCHE Claude's avatar
MARCHE Claude committed
166
The kinds of simplification are as follows.
167 168 169 170
\begin{itemize}
\item Computations with built-in symbols, \eg operations on integers,
  when applied to explicit constants, are evaluated. This includes
  evaluation of equality when a decision can be made (on integer
171 172 173 174 175
  constants, on constructors of algebraic data types), Boolean
  evaluation, simplification of pattern-matching/conditional expression,
  extraction of record fields, and beta-reduction.
  At best, these computations reduce the goal to
  \verb|true| and the transformations thus does not produce any sub-goal.
176
  For example, a goal
177
  like \verb|6*7=42| is solved by those transformations.
178 179
\item Unfolding of definitions, as done by \verb|inline_goal|. Transformation
  \verb|compute_in_goal| unfolds all definitions, including recursive ones.
180 181
  For \verb|compute_specified|, the user can enable unfolding of a specific
  logic symbol by attaching the meta \verb|rewrite_def| to the symbol.
182 183 184 185 186
\begin{whycode}
function sqr (x:int) : int = x * x
meta "rewrite_def" function sqr
\end{whycode}
\item Rewriting using axioms or lemmas declared as rewrite rules. When
187
  an axiom (or a lemma) has one of the forms
188
\begin{whycode}
189
axiom a: forall ... t1 = t2
190 191 192
\end{whycode}
  or
\begin{whycode}
193
axiom a: forall ... f1 <-> f2
194 195 196
\end{whycode}
  then the user can declare
\begin{whycode}
197
meta "rewrite" prop a
198
\end{whycode}
MARCHE Claude's avatar
MARCHE Claude committed
199
  to turn this axiom into a rewrite rule. Rewriting is always done
200 201
  from left to right. Beware that there is no check for termination
  nor for confluence of the set of rewrite rules declared.
MARCHE Claude's avatar
MARCHE Claude committed
202
\end{itemize}
203
Instead of using a meta, it is possible to declare an axiom as a
204
rewrite rule by adding the \verb|[@rewrite]| attribute on the axiom name or
205 206
on the axiom itself, e.g.:
\begin{whycode}
207 208
axiom a [@rewrite]: forall ... t1 = t2
lemma b: [@rewrite] forall ... f1 <-> f2
209 210 211
\end{whycode}
The second form allows some form of local rewriting, e.g.
\begin{whycode}
212
lemma l: forall x y. ([@rewrite] x = y) -> f x = f y
213
\end{whycode}
214
can be proved by \verb|introduce_premises| followed by \verb|compute_specified|.
MARCHE Claude's avatar
MARCHE Claude committed
215 216 217 218 219 220 221

\paragraph{Bound on the number of reductions}
The computations performed by these transformations can take an
arbitrarily large number of steps, or even not terminate. For this
reason, the number of steps is bounded by a maximal value, which is
set by default to 1000. This value can be increased by another meta,
\eg
222 223 224
\begin{whycode}
meta "compute_max_steps" 1_000_000
\end{whycode}
MARCHE Claude's avatar
MARCHE Claude committed
225 226
When this upper limit is reached, a warning is issued, and the
partly-reduced goal is returned as the result of the transformation.
227 228 229


\subsection{Other Non-Splitting Transformations}
230 231 232

\begin{description}

233 234
\item[eliminate\_algebraic] replaces algebraic data types by first-order
definitions~\cite{paskevich09rr}.
235
\index{eliminate-algebraic@\verb+eliminate_algebraic+}
236

237
\item[eliminate\_builtin] removes definitions of symbols that are
238
  declared as builtin in the driver, \ie with a ``syntax'' rule.
239 240
\index{eliminate-builtin@\verb+eliminate_builtin+}

241
\item[eliminate\_definition\_func]
242
  replaces all function definitions with axioms.
243 244
\index{eliminate-definition-func@\verb+eliminate_definition_func+}

245
\item[eliminate\_definition\_pred]
246
  replaces all predicate definitions with axioms.
247 248
\index{eliminate-definition-pred@\verb+eliminate_definition_pred+}

249
\item[eliminate\_definition]
250
  applies both transformations above.
251 252
\index{eliminate-definition@\verb+eliminate_definition+}

253
\item[eliminate\_mutual\_recursion]
254
  replaces mutually recursive definitions with axioms.
255 256
\index{eliminate-mutual-recursion@\verb+eliminate_mutual_recursion+}

257
\item[eliminate\_recursion]
258
  replaces all recursive definitions with axioms.
259
\index{eliminate-recursion@\verb+eliminate_recursion+}
260 261 262

\item[eliminate\_if\_term] replaces terms of the form \texttt{if
    formula then t2 else t3} by lifting them at the level of formulas.
263
  This may introduce \texttt{if then else} in formulas.
264
\index{eliminate-if-term@\verb+eliminate_if_term+}
265 266 267 268

\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.
269
\index{eliminate-if-fmla@\verb+eliminate_if_fmla+}
270 271

\item[eliminate\_if]
272
  applies both transformations above.
273
\index{eliminate-if@\verb+eliminate_if+}
274 275

\item[eliminate\_inductive] replaces inductive predicates by
276
  (incomplete) axiomatic definitions, \ie construction axioms and
277
  an inversion axiom.
278
\index{eliminate-inductive@\verb+eliminate_inductive+}
279 280

\item[eliminate\_let\_fmla]
281
  eliminates \texttt{let} by substitution, at the predicate level.
282
\index{eliminate-let-fmla@\verb+eliminate_let_fmla+}
283 284

\item[eliminate\_let\_term]
285
  eliminates \texttt{let} by substitution, at the term level.
286
\index{eliminate-let-term@\verb+eliminate_let_term+}
287 288

\item[eliminate\_let]
289
  applies both transformations above.
290
\index{eliminate-let@\verb+eliminate_let+}
291 292 293 294 295 296

% \item[encoding\_decorate\_mono]

% \item[encoding\_enumeration]

\item[encoding\_smt]
Guillaume Melquiond's avatar
Guillaume Melquiond committed
297
  encodes polymorphic types into monomorphic types~\cite{conchon08smt}.
298
\index{encoding-smt@\verb+encoding_smt+}
299 300

\item[encoding\_tptp]
301
  encodes theories into unsorted logic. %~\cite{cruanes10}.
302
\index{encoding-tptp@\verb+encoding_tptp+}
303 304 305 306 307 308 309 310 311 312 313 314

% \item[filter\_trigger] *)

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

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

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

\item[introduce\_premises] moves antecedents of implications and
  universal quantifications of the goal into the premises of the task.
315
\index{introduce-premises@\verb+introduce_premises+}
316 317 318 319

% \item[remove\_triggers] *)
%   removes the triggers in all quantifications. *)

320
\item[simplify\_array] automatically rewrites the task using the lemma
321 322
  \verb|Select_eq| of theory \verb|map.Map|.
\index{simplify-array@\verb+simplify_array+}
323 324

\item[simplify\_formula] reduces trivial equalities $t=t$ to true and
325 326
  then simplifies propositional structure: removes true, false, simplifies
  $f \land f$ to $f$, etc.
327
\index{simplify-formula@\verb+simplify_formula+}
328 329

\item[simplify\_recursive\_definition] reduces mutually recursive
330
  definitions if they are not really mutually recursive, \eg
331
\begin{whycode}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
332
function f : ... = ... g ...
333 334
with g : ... = e
\end{whycode}
335
becomes
336 337 338 339 340
\begin{whycode}
function g : ... = e
function f : ... = ... g ...
\end{whycode}
if $f$ does not occur in $e$.
341
\index{simplify-recursive-definition@\verb+simplify_recursive_definition+}
342 343 344

\item[simplify\_trivial\_quantification]
  simplifies quantifications of the form
345
\begin{whycode}
346
forall x, x = t -> P(x)
347
\end{whycode}
348
into
349
\begin{whycode}
350
P(t)
351
\end{whycode}
352 353 354
  when $x$ does not occur in $t$.
  More generally, this simplification is applied whenever $x=t$ or
  $t=x$ appears in negative position.
355
\index{simplify-trivial-quantification@\verb+simplify_trivial_quantification+}
356 357

\item[simplify\_trivial\_quantification\_in\_goal]
358
  is the same as above but it applies only in the goal.
359
\index{simplify-trivial-quantification-in-goal@\verb+simplify_trivial_quantification_in_goal+}
360

361 362
\item[split\_premise] replaces axioms in conjunctive form
  by an equivalent collection of axioms.
363
  In absence of case analysis attributes (see \texttt{split\_goal} for details),
364 365
  the number of axiom generated per initial axiom is
  linear in the size of that initial axiom.
366
\index{split-premise@\verb+split_premise+}
367

368 369 370 371
\item[split\_premise\_full] is similar to \texttt{split\_premise}, but it
  also converts the axioms to conjunctive normal form. The number of
  axioms generated per initial axiom may be exponential in the size of
  the initial axiom.
372 373
\index{split-premise-full@\verb+split_premise_full+}

374 375
\end{description}

Guillaume Melquiond's avatar
Guillaume Melquiond committed
376 377
\subsection{Other Splitting Transformations}
\label{tech:trans:split}
378 379 380

\begin{description}

381 382
\item[simplify\_formula\_and\_task] is the same as \texttt{simplify\_formula}
  but it also removes the goal if it is equivalent to true.
383 384
\index{simplify-formula-and-task@\verb+simplify_formula_and_task+}

385
\item[split\_goal] changes conjunctive goals into the
386
  corresponding set of subgoals. In absence of case analysis attributes,
387 388
  the number of subgoals generated is linear in the size of the initial goal.

389 390
  \paragraph{Behavior on asymmetric connectives and
    \texttt{by}/\texttt{so}}
391

392
  The transformation treats specially asymmetric and
393 394 395 396
  \texttt{by}/\texttt{so} connectives. Asymmetric conjunction
  \verb|A && B| in goal position is handled as syntactic sugar for
  \verb|A /\ (A -> B)|.  The conclusion of the first subgoal can then
  be used to prove the second one.
397

398
  Asymmetric disjunction \verb+A || B+ in hypothesis position is handled as
399 400 401 402
  syntactic sugar for \verb|A \/ ((not A) /\ B)|.
  In particular, a case analysis on such hypothesis would give the negation of
  the first hypothesis in the second case.

403 404 405 406 407 408 409 410 411 412 413
  The \texttt{by} connective is treated as a proof indication. In
  hypothesis position, \verb|A by B| is treated as if it were
  syntactic sugar for its regular interpretation \verb|A|. In goal
  position, it is treated as if \verb|B| was an intermediate step for
  proving \verb|A|. \verb|A by B| is then replaced by \verb|B| and the
  transformation also generates a side-condition subgoal \verb|B -> A|
  representing the logical cut.

  Although splitting stops at disjunctive points like symmetric
  disjunction and left-hand sides of implications, the occurrences of
  the \texttt{by} connective are not restricted. For instance:
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 439 440 441 442 443 444
  \begin{itemize}
  \item Splitting
\begin{whycode}
goal G : (A by B) && C
\end{whycode}
generates the subgoals
\begin{whycode}
goal G1 : B
goal G2 : A -> C
goal G3 : B -> A (* side-condition *)
\end{whycode}
\item Splitting
\begin{whycode}
goal G : (A by B) \/ (C by D)
\end{whycode}
generates
\begin{whycode}
goal G1 : B \/ D
goal G2 : B -> A (* side-condition *)
goal G3 : D -> C (* side-condition *)
\end{whycode}
\item Splitting
\begin{whycode}
goal G : (A by B) || (C by D)
\end{whycode}
generates
\begin{whycode}
goal G1 : B || D
goal G2 : B -> A        (* side-condition *)
goal G3 : B || (D -> C) (* side-condition *)
\end{whycode}
445
Note that due to the asymmetric disjunction, the disjunction is kept in the
446 447 448 449 450 451 452 453 454 455 456 457 458
second side-condition subgoal.
\item Splitting
\begin{whycode}
goal G : exists x. P x by x = 42
\end{whycode}
generates
\begin{whycode}
goal G1 : exists x. x = 42
goal G2 : forall x. x = 42 -> P x (* side-condition *)
\end{whycode}
Note that in the side-condition subgoal, the context is universally closed.
\end{itemize}

459
The \texttt{so} connective plays a similar role in hypothesis position, as it serves as a consequence indication. In goal position, \verb|A so B| is treated as if it were syntactic sugar for its regular interpretation \verb|A|. In hypothesis position, it is treated as if both \verb|A| and \verb|B| were true because \verb|B| is a consequence of \verb|A|. \verb|A so B| is replaced by \verb|A /\ B| and the transformation also generates a side-condition subgoal \verb|A -> B| corresponding to the consequence relation between formula.
460

461 462 463 464
As with the \texttt{by} connective, occurrences of \texttt{so} are
unrestricted. For instance:
\begin{itemize}
\item Splitting
465 466 467 468 469 470 471 472 473 474 475 476 477 478
\begin{whycode}
goal G : (((A so B) \/ C) -> D) && E
\end{whycode}
generates
\begin{whycode}
goal G1 : ((A /\ B) \/ C) -> D
goal G2 : (A \/ C -> D) -> E
goal G3 : A -> B               (* side-condition *)
\end{whycode}
\item Splitting
\begin{whycode}
goal G : A by exists x. P x so Q x so R x by T x
(* reads: A by (exists x. P x so (Q x so (R x by T x))) *)
\end{whycode}
479
generates
480 481 482 483 484 485 486
\begin{whycode}
goal G1 : exists x. P x
goal G2 : forall x. P x -> Q x               (* side-condition *)
goal G3 : forall x. P x -> Q x -> T x        (* side-condition *)
goal G4 : forall x. P x -> Q x -> T x -> R x (* side-condition *)
goal G5 : (exists x. P x /\ Q x /\ R x) -> A (* side-condition *)
\end{whycode}
487
In natural language, this corresponds to the following proof scheme
488 489 490 491
for \verb|A|: There exists a \verb|x| for which \verb|P| holds. Then,
for that witness \verb|Q| and \verb|R| also holds. The last one holds
because \verb|T| holds as well. And from those three conditions on
\verb|x|, we can deduce \verb|A|.
492 493
\end{itemize}

494
\paragraph{Attributes controlling the transformation}
495

496
The transformations in the split family can be controlled by using
497
attributes on formulas.
498

499 500
The \verb|[@stop_split]| attribute can be used to block the splitting of a
formula.  The attribute is removed after blocking, so applying the
501 502
transformation a second time will split the formula. This is can be
used to decompose the splitting process in several steps. Also, if a
503
formula with this attribute is found in non-goal position, its
504
\texttt{by}/\texttt{so} proof indication will be erased by the
505
transformation. In a sense, formulas tagged by \verb|[@stop_split]| are
506
handled as if they were local lemmas.
507

508
The \verb|[@case_split]| attribute can be used to force case analysis on hypotheses.
509 510
For instance, applying \texttt{split\_goal} on
\begin{whycode}
511
goal G : ([@case_split] A \/ B) -> C
512 513 514 515 516 517
\end{whycode}
generates the subgoals
\begin{whycode}
goal G1 : A -> C
goal G2 : B -> C
\end{whycode}
518
Without the attribute, the transformation does nothing because undesired case analysis
519 520
may easily lead to an exponential blow-up.

521
Note that the precise behavior of splitting transformations in presence of
522
the \verb|[@case_split]| attribute is not yet specified
523 524 525
and is likely to change in future versions.

\index{split-goal@\verb+split_goal+}
526 527

\item[split\_all]
528
  performs both \texttt{split\_premise} and \texttt{split\_goal}.
529
\index{split-all@\verb+split_all+}
530

531 532
\item[split\_intro]
  performs both \texttt{split\_goal} and \texttt{introduce\_premises}.
533
\index{split-intro@\verb+split_intro+}
534

535 536
\item[split\_goal\_full]
  has a behavior similar
537 538 539 540 541 542 543 544 545
  to \texttt{split\_goal}, but also converts the goal to conjunctive normal form.
  The number of subgoals generated may be exponential in the size of the initial goal.
\index{split-goal-full@\verb+split_goal_full+}

\item[split\_all\_full]
  performs both \texttt{split\_premise} and \texttt{split\_goal\_full}.
\index{split-all-full@\verb+split_all_full+}


546 547 548
\end{description}


549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570
\section{Proof Strategies}
\label{sec:strategies}

As seen in Section~\ref{sec:ideref}, the IDE provides a few buttons
that trigger the run of simple proof strategies on the selected goals.
Proof strategies can be defined using a basic assembly-style language,
and put into the Why3 configuration file. The commands of this basic
language are:
\begin{itemize}
\item \texttt{c $p$ $t$ $m$} calls the prover $p$ with a time limit
  $t$ and memory limit $m$. On success, the strategy ends, it
  continues to next line otherwise
\item \texttt{t $n$ $lab$} applies the transformation $n$. On success,
  the strategy continues to label $lab$, and is applied to each
  generated sub-goals.  It continues to next line otherwise.
\item \texttt{g $lab$} inconditionally jumps to label $lab$
\item \texttt{$lab$:} declares the label $lab$. The default label
  \texttt{exit} allows to stop the program.
\end{itemize}

To examplify this basic programming language, we give below the
default strategies that are attached to the default buttons of the
571
IDE, assuming that the provers Alt-Ergo 1.30, CVC4 1.5 and Z3 4.5.0
572 573 574 575 576 577 578
were detected by the \verb|why3 config --detect| command
\begin{description}
\item[Split] is bound to the 1-line strategy
\begin{verbatim}
t split_goal_wp exit
\end{verbatim}

579 580 581 582 583 584 585 586 587 588
\item[Auto level 0] is bound to
\begin{verbatim}
c Z3,4.5.0, 1 1000
c Alt-Ergo,1.30, 1 1000
c CVC4,1.5, 1 1000
\end{verbatim}
  The three provers are tried for a time limit of 1 second and memory
  limit of 1~Gb, each in turn. This is a perfect strategy for a first
  attempt to discharge a new goal.

589 590 591
\item[Auto level 1] is bound to
\begin{verbatim}
start:
592 593 594
c Z3,4.5.0, 1 1000
c Alt-Ergo,1.30, 1 1000
c CVC4,1.5, 1 1000
595
t split_goal_wp start
596 597 598
c Z3,4.5.0, 10 4000
c Alt-Ergo,1.30, 10 4000
c CVC4,1.5, 10 4000
599 600 601 602 603 604 605 606 607 608
\end{verbatim}
  The three provers are first tried for a time limit of 1 second and
  memory limit of 1~Gb, each in turn. If none of them succeed, a
  split is attempted. If the split works then the same strategy is
  retried on each sub-goals. If the split does not succeed, the provers
  are tried again with a larger limits.

\item[Auto level 2] is bound to
\begin{verbatim}
start:
609 610
c Z3,4.5.0, 1 1000
c Eprover,2.0, 1 1000
611
c Spass,3.7, 1 1000
612 613
c Alt-Ergo,1.30, 1 1000
c CVC4,1.5, 1 1000
614
t split_goal_wp start
615 616
c Z3,4.5.0, 5 2000
c Eprover,2.0, 5 2000
617
c Spass,3.7, 5 2000
618 619
c Alt-Ergo,1.30, 5 2000
c CVC4,1.5, 5 2000
620 621 622 623 624 625 626
t introduce_premises afterintro
afterintro:
t inline_goal afterinline
g trylongertime
afterinline:
t split_goal_wp start
trylongertime:
627 628
c Z3,4.5.0, 30 4000
c Eprover,2.0, 30 4000
629
c Spass,3.7, 30 4000
630 631
c Alt-Ergo,1.30, 30 4000
c CVC4,1.5, 30 4000
632 633 634 635 636 637 638
\end{verbatim}
  Notice that now 5 provers are used.  The provers are first tried for
  a time limit of 1 second and memory limit of 1~Gb, each in turn. If
  none of them succeed, a split is attempted. If the split works then
  the same strategy is retried on each sub-goals. If the split does
  not succeed, the prover are tried again with limits of 5 s and 2
  Gb. If all fail, we attempt the transformation of introduction of
639
  premises in the context, followed by an inlining of the definitions
640 641 642 643 644 645
  in the goals. We then attempt a split again, if the split succeeds,
  we restart from the beginning, if it fails then provers are tried
  again with 30s and 4 Gb.

\end{description}

646 647 648 649 650
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End: