1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* 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 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 find_point : cstr list -> Vect.t option
val find_unsat_certificate : cstr list -> Vect.t option
val integer_solver :
WithProof.t list -> ProofFormat.proof option
|
