From 65b89a6b06b5ff2e26883800702cda19d2d980df Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Tue, 17 Sep 2019 18:09:06 +0200
Subject: Improved handling of micromega caches

- Specialised hash and equality functions.
  Avoid collisions in extreme scenarios.
- Flags to disable the use of the caches.

fixes #10772
---
 doc/sphinx/addendum/micromega.rst | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 238106b2e7..4a691bde3a 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -35,6 +35,18 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`,
    use the Simplex method for solving linear goals. If it is not set,
    the decision procedures are using Fourier elimination.
 
+.. flag:: Lia Cache
+
+   This option (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache`
+
+.. flag:: Nia Cache
+
+   This option (set by default) instructs :tacn:`nia` to cache its results in the file `.nia.cache`
+
+.. flag:: Nra Cache
+
+   This option (set by default) instructs :tacn:`nra` to cache its results in the file `.nra.cache`
+
 
 The tactics solve propositional formulas parameterized by atomic
 arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`.
-- 
cgit v1.2.3