Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
3eedbb01
Commit
3eedbb01
authored
Oct 11, 2012
by
Guillaume Melquiond
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Clean documentation of transformations.
parent
659597a2
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
43 additions
and
44 deletions
+43
-44
doc/fix.hva
doc/fix.hva
+1
-0
doc/technical.tex
doc/technical.tex
+42
-44
No files found.
doc/fix.hva
View file @
3eedbb01
...
...
@@ -4,6 +4,7 @@
\newcommand{\bs}{\textbackslash}
\newcommand{\vfill}{}
\newcommand{\hrulefill}{}
\renewcommand{\framebox}[1]{#1}
\makeatletter
\RenewcommandHtml{\@boxed}[1]{{#1}}
...
...
doc/technical.tex
View file @
3eedbb01
...
...
@@ -13,7 +13,7 @@ The XML file follows the DTD given in \texttt{share/why3session.dtd} and reprodu
\section
{
Provers detection data
}
\label
{
sec:proverdetecttiondata
}
All the necessary data configuration for the auto
am
tic detection of
All the necessary data configuration for the auto
ma
tic detection of
installed provers is stored in the file
\texttt
{
provers-detection-data.conf
}
typically located in directory
\verb
|
/usr/local/share/why3
|
after installation. The contents of this
...
...
@@ -134,21 +134,21 @@ why3 --list-transforms
\begin{description}
\item
[eliminate\_algebraic]
R
eplaces algebraic data types by first-order
definitions~
\cite
{
paskevich09rr
}
\item
[eliminate\_algebraic]
r
eplaces algebraic data types by first-order
definitions~
\cite
{
paskevich09rr
}
.
\item
[eliminate\_builtin]
Suppress definitions of symbols which
are
\item
[eliminate\_builtin]
removes definitions of symbols that
are
declared as builtin in the driver,
\ie
with a ``syntax'' rule.
\item
[eliminate\_definition\_func]
R
eplaces all function definitions with axioms.
r
eplaces all function definitions with axioms.
\item
[eliminate\_definition\_pred]
R
eplaces all predicate definitions with axioms.
r
eplaces all predicate definitions with axioms.
\item
[eliminate\_definition]
Apply
both transformations above.
applies
both transformations above.
\item
[eliminate\_mutual\_recursion]
R
eplaces mutually recursive definitions with axioms.
r
eplaces mutually recursive definitions with axioms.
\item
[eliminate\_recursion]
R
eplaces all recursive definitions with axioms.
r
eplaces all recursive definitions with axioms.
\item
[eliminate\_if\_term]
replaces terms of the form
\texttt
{
if
formula then t2 else t3
}
by lifting them at the level of formulas.
...
...
@@ -159,30 +159,30 @@ definitions~\cite{paskevich09rr}
connectives.
\item
[eliminate\_if]
Apply
both transformations above.
applies
both transformations above.
\item
[eliminate\_inductive]
replaces inductive predicates by
(incomplete) axiomatic definitions,
\ie
construction axioms and
an inversion axiom.
\item
[eliminate\_let\_fmla]
E
liminates
\texttt
{
let
}
by substitution, at the predicate level.
e
liminates
\texttt
{
let
}
by substitution, at the predicate level.
\item
[eliminate\_let\_term]
E
liminates
\texttt
{
let
}
by substitution, at the term level.
e
liminates
\texttt
{
let
}
by substitution, at the term level.
\item
[eliminate\_let]
Apply
both transformations above.
applies
both transformations above.
% \item[encoding\_decorate\_mono]
% \item[encoding\_enumeration]
\item
[encoding\_smt]
Encode
polymorphic types into monomorphic type~
\cite
{
conchon08smt
}
.
encodes
polymorphic types into monomorphic type~
\cite
{
conchon08smt
}
.
\item
[encoding\_tptp]
Encode
theories into unsorted logic.
%~\cite{cruanes10}.
encodes
theories into unsorted logic.
%~\cite{cruanes10}.
% \item[filter\_trigger] *)
...
...
@@ -196,18 +196,18 @@ definitions~\cite{paskevich09rr}
\item
[inline\_all]
expands all non-recursive definitions.
\item
[inline\_goal]
E
xpands all outermost symbols of the goal that
\item
[inline\_goal]
e
xpands all outermost symbols of the goal that
have a non-recursive definition.
\item
[inline\_trivial]
removes definitions of the form
\begin{
verbatim
}
function f x
_
1 ..
x
_
n = (g e
_
1
.. e
_
k)
predicate p x
_
1 ..
x
_
n = (q e
_
1
.. e
_
k)
\end{
verbatim
}
\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
$
..
$
x
_
n
$
occur at most once in the
$
e
_
i
$
each
$
x
_
1
\dots
x
_
n
$
occurs at most once in all the
$
e
_
i
$
.
\item
[introduce\_premises]
moves antecedents of implications and
universal quantifications of the goal into the premises of the task.
...
...
@@ -215,46 +215,44 @@ each $x_1$ .. $x_n$ occur at most once in the $e_i$
% \item[remove\_triggers] *)
% removes the triggers in all quantifications. *)
\item
[simplify\_array]
A
utomatically rewrites the task using the lemma
\item
[simplify\_array]
a
utomatically rewrites the task using the lemma
\verb
|
Select_eq
|
of theory
\verb
|
array.Array
|
.
\item
[simplify\_formula]
reduces trivial equalities
$
t
=
t
$
to true and
then simplifies propositional structure: removes true, false,
``f
and f'' to ``f''
, etc.
then simplifies propositional structure: removes true, false,
simplifies
$
f
\land
f
$
to
$
f
$
, etc.
\item
[simplify\_recursive\_definition]
reduces mutually recursive
definitions if they are not really mutually recursive,
\eg
\begin{
verbatim
}
\begin{
whycode
}
function f : ... = .... g ...
with g : .. = e
\end{verbatim}
with g : ... = e
\end{whycode}
becomes
\begin{
verbatim
}
function g : .. = e
function f : ... = ...
.
g ...
\end{
verbatim
}
if
f does not occur in e
\begin{
whycode
}
function g : ..
.
= e
function f : ... = ... g ...
\end{
whycode
}
if
$
f
$
does not occur in
$
e
$
.
\item
[simplify\_trivial\_quantification]
simplifies quantifications of the form
\begin{verbatim}
forall x, x=t -> P(x)
forall x, x=t -> P(x)
\end{verbatim}
or
\begin{verbatim}
forall x, t=x -> P(x)
forall x, t=x -> P(x)
\end{verbatim}
when x does not occur in t
into
when
$
x
$
does not occur in
$
t
$
into
\begin{verbatim}
P(t)
\end{verbatim}
More generally, it applies this simplification whenever
x=t appear
More generally, it applies this simplification whenever
$
x
=
t
$
appears
in a negative position.
\item
[simplify\_trivial\_quantification\_in\_goal]
same as above bu
t applies only in the goal.
is the same as above but i
t applies only in the goal.
\item
[split\_premise]
splits conjunctive premises.
...
...
@@ -266,24 +264,24 @@ P(t)
\begin{description}
\item
[full\_split\_all]
composition of
\texttt
{
split
\_
premise
}
and
\texttt
{
full
\_
split
\_
goal
}
.
performs both
\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.
\item
[simplify\_formula\_and\_task]
is the
same as
\texttt
{
simplify
\_
formula
}
but
it
also removes the goal if it is equivalent to true.
\item
[split\_all]
composition of
\texttt
{
split
\_
premise
}
and
\texttt
{
split
\_
goal
}
.
performs both
\texttt
{
split
\_
premise
}
and
\texttt
{
split
\_
goal
}
.
\item
[split\_goal]
if the goal is a conjunction of goals, returns the
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
.
moves the antecedents into the premises when a goal is an implication
.
\end{description}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment