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/changelog/04-tactics/10765-micromega-caches.rst | 3 +++ doc/sphinx/addendum/micromega.rst | 12 ++++++++++++ 2 files changed, 15 insertions(+) create mode 100644 doc/changelog/04-tactics/10765-micromega-caches.rst (limited to 'doc') diff --git a/doc/changelog/04-tactics/10765-micromega-caches.rst b/doc/changelog/04-tactics/10765-micromega-caches.rst new file mode 100644 index 0000000000..8436b66ec0 --- /dev/null +++ b/doc/changelog/04-tactics/10765-micromega-caches.rst @@ -0,0 +1,3 @@ +- Introduction of flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`. + (see `#10772 `_ for use case) +(`#10765 `_ fixes `#10772 `_ , by Frédéric Besson). 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 From b2c3eca7277ee9653e387ad3b599150b17c38572 Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Thu, 3 Oct 2019 15:34:04 +0200 Subject: fix 10765-micromega-caches.rst --- doc/changelog/04-tactics/10765-micromega-caches.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/changelog/04-tactics/10765-micromega-caches.rst b/doc/changelog/04-tactics/10765-micromega-caches.rst index 8436b66ec0..12d8f68e63 100644 --- a/doc/changelog/04-tactics/10765-micromega-caches.rst +++ b/doc/changelog/04-tactics/10765-micromega-caches.rst @@ -1,3 +1,3 @@ - Introduction of flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`. (see `#10772 `_ for use case) -(`#10765 `_ fixes `#10772 `_ , by Frédéric Besson). + (`#10765 `_ fixes `#10772 `_ , by Frédéric Besson). -- cgit v1.2.3