aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/addendum
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-22 13:45:03 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-07-17 14:15:59 +0200
commit8c43e795c772090b336c0f170a6e5dcab196125d (patch)
tree98508f7e342142dd017da56872f74df73e6fce58 /doc/sphinx/addendum
parentb799252775563b4f46f5ea39cbfc469759e7a296 (diff)
Remove fourier plugin
As stated in the manual, the fourier tactic is subsumed by lra.
Diffstat (limited to 'doc/sphinx/addendum')
-rw-r--r--doc/sphinx/addendum/micromega.rst13
1 files changed, 6 insertions, 7 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 0e9c23b9b..2407a9051 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -96,15 +96,14 @@ and checked to be :math:`-1`.
.. tacn:: lra
:name: lra
-This tactic is searching for *linear* refutations using Fourier
-elimination [#]_. As a result, this tactic explores a subset of the *Cone*
-defined as
+ This tactic is searching for *linear* refutations using Fourier
+ elimination [#]_. As a result, this tactic explores a subset of the *Cone*
+ defined as
- :math:`\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}`
+ :math:`\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}`
-The deductive power of `lra` is the combined deductive power of
-`ring_simplify` and `fourier`. There is also an overlap with the field
-tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`.
+ The deductive power of :tacn:`lra` overlaps with the one of :tacn:`field`
+ tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`.
`lia`: a tactic for linear integer arithmetic