aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/simplex.mli
diff options
context:
space:
mode:
authorVincent Laporte2020-02-04 10:13:50 +0100
committerVincent Laporte2020-02-04 10:13:50 +0100
commitbc2c6b135e03335f1fde8e15aecb30e002a5d751 (patch)
treebc2d8e57f1eb4c5947a57148d704b3a6827ab3a6 /plugins/micromega/simplex.mli
parent097f779646fe8fedfeff99e2716b11e36e0aa80a (diff)
parentccff8bf591ee0b8499cdc9dc9bb2827e4d2dae69 (diff)
Merge PR #11474: Fix efficiency regression #11436
Ack-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: vbgl
Diffstat (limited to 'plugins/micromega/simplex.mli')
-rw-r--r--plugins/micromega/simplex.mli14
1 files changed, 14 insertions, 0 deletions
diff --git a/plugins/micromega/simplex.mli b/plugins/micromega/simplex.mli
index 19bcce3590..ff672edafd 100644
--- a/plugins/micromega/simplex.mli
+++ b/plugins/micromega/simplex.mli
@@ -9,6 +9,20 @@
(************************************************************************)
open Polynomial
+(** Profiling *)
+
+type profile_info =
+ { number_of_successes : int
+ ; number_of_failures : int
+ ; success_pivots : int
+ ; failure_pivots : int
+ ; average_pivots : int
+ ; maximum_pivots : int }
+
+val get_profile_info : unit -> profile_info
+
+(** Simplex interface *)
+
val optimise : Vect.t -> cstr list -> (Num.num option * Num.num option) option
val find_point : cstr list -> Vect.t option
val find_unsat_certificate : cstr list -> Vect.t option