summaryrefslogtreecommitdiff
path: root/doc/refman/Omega.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/Omega.tex')
-rw-r--r--doc/refman/Omega.tex226
1 files changed, 0 insertions, 226 deletions
diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex
deleted file mode 100644
index b9e899ce..00000000
--- a/doc/refman/Omega.tex
+++ /dev/null
@@ -1,226 +0,0 @@
-\achapter{Omega: a solver of quantifier-free problems in
-Presburger Arithmetic}
-\aauthor{Pierre Crégut}
-\label{OmegaChapter}
-
-\asection{Description of {\tt omega}}
-\tacindex{omega}
-\label{description}
-
-{\tt omega} solves a goal in Presburger arithmetic, i.e. a universally
-quantified formula made of equations and inequations. Equations may
-be specified either on the type \verb=nat= of natural numbers or on
-the type \verb=Z= of binary-encoded integer numbers. Formulas on
-\verb=nat= are automatically injected into \verb=Z=. The procedure
-may use any hypothesis of the current proof session to solve the goal.
-
-Multiplication is handled by {\tt omega} but only goals where at
-least one of the two multiplicands of products is a constant are
-solvable. This is the restriction meant by ``Presburger arithmetic''.
-
-If the tactic cannot solve the goal, it fails with an error message.
-In any case, the computation eventually stops.
-
-\asubsection{Arithmetical goals recognized by {\tt omega}}
-
-{\tt omega} applied only to quantifier-free formulas built from the
-connectors
-
-\begin{quote}
-\verb=/\, \/, ~, ->=
-\end{quote}
-
-on atomic formulas. Atomic formulas are built from the predicates
-
-\begin{quote}
-\verb!=, le, lt, gt, ge!
-\end{quote}
-
- on \verb=nat= or from the predicates
-
-\begin{quote}
-\verb!=, <, <=, >, >=!
-\end{quote}
-
- on \verb=Z=. In expressions of type \verb=nat=, {\tt omega} recognizes
-
-\begin{quote}
-\verb!plus, minus, mult, pred, S, O!
-\end{quote}
-
-and in expressions of type \verb=Z=, {\tt omega} recognizes
-
-\begin{quote}
-\verb!+, -, *, Zsucc!, and constants.
-\end{quote}
-
-All expressions of type \verb=nat= or \verb=Z= not built on these
-operators are considered abstractly as if they
-were arbitrary variables of type \verb=nat= or \verb=Z=.
-
-\asubsection{Messages from {\tt omega}}
-\label{errors}
-
-When {\tt omega} does not solve the goal, one of the following errors
-is generated:
-
-\begin{ErrMsgs}
-
-\item \errindex{omega can't solve this system}
-
- This may happen if your goal is not quantifier-free (if it is
- universally quantified, try {\tt intros} first; if it contains
- existentials quantifiers too, {\tt omega} is not strong enough to solve your
- goal). This may happen also if your goal contains arithmetical
- operators unknown from {\tt omega}. Finally, your goal may be really
- wrong!
-
-\item \errindex{omega: Not a quantifier-free goal}
-
- If your goal is universally quantified, you should first apply {\tt
- intro} as many time as needed.
-
-\item \errindex{omega: Unrecognized predicate or connective: {\sl ident}}
-
-\item \errindex{omega: Unrecognized atomic proposition: {\sl prop}}
-
-\item \errindex{omega: Can't solve a goal with proposition variables}
-
-\item \errindex{omega: Unrecognized proposition}
-
-\item \errindex{omega: Can't solve a goal with non-linear products}
-
-\item \errindex{omega: Can't solve a goal with equality on {\sl type}}
-
-\end{ErrMsgs}
-
-%% Ce code est débranché pour l'instant
-%%
-% \asubsection{Control over the output}
-% There are some flags that can be set to get more information on the procedure
-
-% \begin{itemize}
-% \item \verb=Time= to get the time used by the procedure
-% \item \verb=System= to visualize the normalized systems.
-% \item \verb=Action= to visualize the actions performed by the OMEGA
-% procedure (see \ref{technical}).
-% \end{itemize}
-
-% \comindex{Set omega Time}
-% \comindex{UnSet omega Time}
-% \comindex{Switch omega Time}
-% \comindex{Set omega System}
-% \comindex{UnSet omega System}
-% \comindex{Switch omega System}
-% \comindex{Set omega Action}
-% \comindex{UnSet omega Action}
-% \comindex{Switch omega Action}
-
-% Use {\tt Set omega {\rm\sl flag}} to set the flag
-% {\rm\sl flag}. Use {\tt Unset omega {\rm\sl flag}} to unset it and
-% {\tt Switch omega {\rm\sl flag}} to toggle it.
-
-\section{Using {\tt omega}}
-
-The {\tt omega} tactic does not belong to the core system. It should be
-loaded by
-\begin{coq_example*}
-Require Import Omega.
-Open Scope Z_scope.
-\end{coq_example*}
-
-\example{}
-
-\begin{coq_example}
-Goal forall m n:Z, 1 + 2 * m <> 2 * n.
-intros; omega.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-
-\example{}
-
-\begin{coq_example}
-Goal forall z:Z, z > 0 -> 2 * z + 1 > z.
-intro; omega.
-\end{coq_example}
-
-% Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+.
-
-\asection{Technical data}
-\label{technical}
-
-\asubsection{Overview of the tactic}
-\begin{itemize}
-
-\item The goal is negated twice and the first negation is introduced as an
- hypothesis.
-\item Hypothesis are decomposed in simple equations or inequations. Multiple
- goals may result from this phase.
-\item Equations and inequations over \verb=nat= are translated over
- \verb=Z=, multiple goals may result from the translation of
- substraction.
-\item Equations and inequations are normalized.
-\item Goals are solved by the {\it OMEGA} decision procedure.
-\item The script of the solution is replayed.
-
-\end{itemize}
-
-\asubsection{Overview of the {\it OMEGA} decision procedure}
-
-The {\it OMEGA} decision procedure involved in the {\tt omega} tactic uses
-a small subset of the decision procedure presented in
-
-\begin{quote}
- "The Omega Test: a fast and practical integer programming
-algorithm for dependence analysis", William Pugh, Communication of the
-ACM , 1992, p 102-114.
-\end{quote}
-
-Here is an overview, look at the original paper for more information.
-
-\begin{itemize}
-
-\item Equations and inequations are normalized by division by the GCD of their
- coefficients.
-\item Equations are eliminated, using the Banerjee test to get a coefficient
- equal to one.
-\item Note that each inequation defines a half space in the space of real value
- of the variables.
- \item Inequations are solved by projecting on the hyperspace
- defined by cancelling one of the variable. They are partitioned
- according to the sign of the coefficient of the eliminated
- variable. Pairs of inequations from different classes define a
- new edge in the projection.
- \item Redundant inequations are eliminated or merged in new
- equations that can be eliminated by the Banerjee test.
-\item The last two steps are iterated until a contradiction is reached
- (success) or there is no more variable to eliminate (failure).
-
-\end{itemize}
-
-It may happen that there is a real solution and no integer one. The last
-steps of the Omega procedure (dark shadow) are not implemented, so the
-decision procedure is only partial.
-
-\asection{Bugs}
-
-\begin{itemize}
-\item The simplification procedure is very dumb and this results in
- many redundant cases to explore.
-
-\item Much too slow.
-
-\item Certainly other bugs! You can report them to
-
-\begin{quote}
- \url{Pierre.Cregut@cnet.francetelecom.fr}
-\end{quote}
-
-\end{itemize}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: