From ccff8bf591ee0b8499cdc9dc9bb2827e4d2dae69 Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Tue, 28 Jan 2020 15:33:22 +0100 Subject: Fix efficiency regression #11436 - The cutting plane has been (sometimes) improved to generate stronger cuts. - There is now some support for profiling the Simplex see documentation for Show Lia Profile. --- doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst | 9 +++++++++ doc/sphinx/addendum/micromega.rst | 6 ++++++ 2 files changed, 15 insertions(+) create mode 100644 doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst (limited to 'doc') diff --git a/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst new file mode 100644 index 0000000000..2a341261e5 --- /dev/null +++ b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst @@ -0,0 +1,9 @@ +- **Added:** + :cmd:`Show Lia Profile` prints some statistics about :tacn:`lia` calls. + (`#11474 `_, by Frédéric Besson). + +- **Fixed:** + Efficiency regression of ``lia`` + (`#11474 `_, + fixes `#11436 `_, + by Frédéric Besson). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index cc19c8b6a9..b0197c500c 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -35,6 +35,12 @@ 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. +.. cmd:: Show Lia Profile + + This command prints some statistics about the amount of pivoting + operations needed by :tacn:`lia` and may be useful to detect + inefficiencies (only meaningful if flag :flag:`Simplex` is set). + .. flag:: Lia Cache This flag (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache` -- cgit v1.2.3