diff options
Diffstat (limited to 'plugins/micromega/simplex.mli')
| -rw-r--r-- | plugins/micromega/simplex.mli | 22 |
1 files changed, 19 insertions, 3 deletions
diff --git a/plugins/micromega/simplex.mli b/plugins/micromega/simplex.mli index 19bcce3590..ab89ded263 100644 --- a/plugins/micromega/simplex.mli +++ b/plugins/micromega/simplex.mli @@ -1,15 +1,31 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) + +open NumCompat open Polynomial -val optimise : Vect.t -> cstr list -> (Num.num option * Num.num option) option +(** 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 -> (Q.t option * Q.t option) option val find_point : cstr list -> Vect.t option val find_unsat_certificate : cstr list -> Vect.t option |