aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega')
-rw-r--r--plugins/micromega/certificate.ml20
-rw-r--r--plugins/micromega/certificate.mli6
-rw-r--r--plugins/micromega/coq_micromega.ml91
-rw-r--r--plugins/micromega/persistent_cache.ml46
4 files changed, 65 insertions, 98 deletions
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 1958fff4cc..9eeba614c7 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -27,7 +27,13 @@ open NumCompat
open Q.Notations
open Mutils
-let use_simplex = ref true
+let use_simplex =
+ Goptions.declare_bool_option_and_ref ~depr:false ~key:["Simplex"] ~value:true
+
+(* If set to some [file], arithmetic goals are dumped in [file].v *)
+
+let dump_file =
+ Goptions.declare_stringopt_option_and_ref ~depr:false ~key:["Dump"; "Arith"]
type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown
type zres = (Mc.zArithProof, int * Mc.z list) res
@@ -203,19 +209,19 @@ let fourier_linear_prover l =
| Inl _ -> None
let direct_linear_prover l =
- if !use_simplex then Simplex.find_unsat_certificate l
+ if use_simplex () then Simplex.find_unsat_certificate l
else fourier_linear_prover l
let find_point l =
let open Util in
- if !use_simplex then Simplex.find_point l
+ if use_simplex () then Simplex.find_point l
else
match Mfourier.Fourier.find_point l with
| Inr _ -> None
| Inl cert -> Some cert
let optimise v l =
- if !use_simplex then Simplex.optimise v l else Mfourier.Fourier.optimise v l
+ if use_simplex () then Simplex.optimise v l else Mfourier.Fourier.optimise v l
let dual_raw_certificate l =
if debug then begin
@@ -981,13 +987,11 @@ let xlia_simplex env red sys =
with FoundProof prf -> compile_prf sys (Step (0, prf, Done))
let xlia env0 en red sys =
- if !use_simplex then xlia_simplex env0 red sys else xlia en red sys
-
-let dump_file = ref None
+ if use_simplex () then xlia_simplex env0 red sys else xlia en red sys
let gen_bench (tac, prover) can_enum prfdepth sys =
let res = prover can_enum prfdepth sys in
- ( match !dump_file with
+ ( match dump_file () with
| None -> ()
| Some file ->
let o = open_out (Filename.temp_file ~temp_dir:(Sys.getcwd ()) file ".v") in
diff --git a/plugins/micromega/certificate.mli b/plugins/micromega/certificate.mli
index cabd36ebb7..5b215549b0 100644
--- a/plugins/micromega/certificate.mli
+++ b/plugins/micromega/certificate.mli
@@ -12,16 +12,12 @@ module Mc = Micromega
(** [use_simplex] is bound to the Coq option Simplex.
If set, use the Simplex method, otherwise use Fourier *)
-val use_simplex : bool ref
+val use_simplex : unit -> bool
type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown
type zres = (Mc.zArithProof, int * Mc.z list) res
type qres = (Mc.q Mc.psatz, int * Mc.q list) res
-(** [dump_file] is bound to the Coq option Dump Arith.
- If set to some [file], arithmetic goals are dumped in filexxx.v *)
-val dump_file : string option ref
-
(** [q_cert_of_pos prf] converts a Sos proof into a rational Coq proof *)
val q_cert_of_pos : Sos_types.positivstellensatz -> Mc.q Mc.psatz
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 43f6f5a35e..7e4c4ce5c6 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -37,74 +37,31 @@ let debug = false
let max_depth = max_int
(* Search limit for provers over Q R *)
-let lra_proof_depth = ref max_depth
+let lra_proof_depth =
+ declare_int_option_and_ref ~depr:false ~key:["Lra"; "Depth"] ~value:max_depth
(* Search limit for provers over Z *)
-let lia_enum = ref true
-let lia_proof_depth = ref max_depth
-let get_lia_option () = (!Certificate.use_simplex, !lia_enum, !lia_proof_depth)
-let get_lra_option () = !lra_proof_depth
+let lia_enum =
+ declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Enum"] ~value:true
+
+let lia_proof_depth =
+ declare_int_option_and_ref ~depr:false ~key:["Lia"; "Depth"] ~value:max_depth
+
+let get_lia_option () =
+ (Certificate.use_simplex (), lia_enum (), lia_proof_depth ())
(* Enable/disable caches *)
-let use_lia_cache = ref true
-let use_nia_cache = ref true
-let use_nra_cache = ref true
-let use_csdp_cache = ref true
-
-let () =
- let int_opt l vref =
- { optdepr = false
- ; optkey = l
- ; optread = (fun () -> Some !vref)
- ; optwrite =
- (fun x -> vref := match x with None -> max_depth | Some v -> v) }
- in
- let lia_enum_opt =
- { optdepr = false
- ; optkey = ["Lia"; "Enum"]
- ; optread = (fun () -> !lia_enum)
- ; optwrite = (fun x -> lia_enum := x) }
- in
- let solver_opt =
- { optdepr = false
- ; optkey = ["Simplex"]
- ; optread = (fun () -> !Certificate.use_simplex)
- ; optwrite = (fun x -> Certificate.use_simplex := x) }
- in
- let dump_file_opt =
- { optdepr = false
- ; optkey = ["Dump"; "Arith"]
- ; optread = (fun () -> !Certificate.dump_file)
- ; optwrite = (fun x -> Certificate.dump_file := x) }
- in
- let lia_cache_opt =
- { optdepr = false
- ; optkey = ["Lia"; "Cache"]
- ; optread = (fun () -> !use_lia_cache)
- ; optwrite = (fun x -> use_lia_cache := x) }
- in
- let nia_cache_opt =
- { optdepr = false
- ; optkey = ["Nia"; "Cache"]
- ; optread = (fun () -> !use_nia_cache)
- ; optwrite = (fun x -> use_nia_cache := x) }
- in
- let nra_cache_opt =
- { optdepr = false
- ; optkey = ["Nra"; "Cache"]
- ; optread = (fun () -> !use_nra_cache)
- ; optwrite = (fun x -> use_nra_cache := x) }
- in
- let () = declare_bool_option solver_opt in
- let () = declare_bool_option lia_cache_opt in
- let () = declare_bool_option nia_cache_opt in
- let () = declare_bool_option nra_cache_opt in
- let () = declare_stringopt_option dump_file_opt in
- let () = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in
- let () = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in
- let () = declare_bool_option lia_enum_opt in
- ()
+let use_lia_cache =
+ declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Cache"] ~value:true
+
+let use_nia_cache =
+ declare_bool_option_and_ref ~depr:false ~key:["Nia"; "Cache"] ~value:true
+
+let use_nra_cache =
+ declare_bool_option_and_ref ~depr:false ~key:["Nra"; "Cache"] ~value:true
+
+let use_csdp_cache () = true
(**
* Initialize a tag type to the Tag module declaration (see Mutils).
@@ -2101,7 +2058,7 @@ struct
let memo_opt use_cache cache_file f =
let memof = memo cache_file f in
- fun x -> if !use_cache then memof x else f x
+ fun x -> if use_cache () then memof x else f x
end
module CacheCsdp = MakeCache (struct
@@ -2281,7 +2238,7 @@ let memo_nra =
let linear_prover_Q =
{ name = "linear prover"
- ; get_option = get_lra_option
+ ; get_option = lra_proof_depth
; prover =
(fun (o, l) ->
lift_pexpr_prover (Certificate.linear_prover_with_cert o) l)
@@ -2292,7 +2249,7 @@ let linear_prover_Q =
let linear_prover_R =
{ name = "linear prover"
- ; get_option = get_lra_option
+ ; get_option = lra_proof_depth
; prover =
(fun (o, l) ->
lift_pexpr_prover (Certificate.linear_prover_with_cert o) l)
@@ -2303,7 +2260,7 @@ let linear_prover_R =
let nlinear_prover_R =
{ name = "nra"
- ; get_option = get_lra_option
+ ; get_option = lra_proof_depth
; prover = memo_nra
; hyps = hyps_of_cone
; compact = compact_cone
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index f157a807ad..9051bbb5ca 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -41,13 +41,21 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct
type mode = Closed | Open
type 'a t = {outch : out_channel; mutable status : mode; htbl : 'a Table.t}
- let finally f rst =
- try
- let res = f () in
- rst (); res
- with reraise ->
- (try rst () with any -> raise reraise);
- raise reraise
+ (* XXX: Move to Fun.protect once in Ocaml 4.08 *)
+ let fun_protect ~(finally : unit -> unit) work =
+ let finally_no_exn () =
+ let exception Finally_raised of exn in
+ try finally ()
+ with e ->
+ let bt = Printexc.get_raw_backtrace () in
+ Printexc.raise_with_backtrace (Finally_raised e) bt
+ in
+ match work () with
+ | result -> finally_no_exn (); result
+ | exception work_exn ->
+ let work_bt = Printexc.get_raw_backtrace () in
+ finally_no_exn ();
+ Printexc.raise_with_backtrace work_exn work_bt
let read_key_elem inch =
try Some (Marshal.from_channel inch) with
@@ -76,21 +84,23 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct
let unlock fd =
let pos = lseek fd 0 SEEK_CUR in
- try
- ignore (lseek fd 0 SEEK_SET);
- lockf fd F_ULOCK 1
- with Unix.Unix_error (_, _, _) ->
- ()
- (* Here, this is really bad news --
- there is a pending lock which could cause a deadlock.
- Should it be an anomaly or produce a warning ?
- *);
- ignore (lseek fd pos SEEK_SET)
+ let () =
+ try
+ ignore (lseek fd 0 SEEK_SET);
+ lockf fd F_ULOCK 1
+ with Unix.Unix_error (_, _, _) ->
+ (* Here, this is really bad news --
+ there is a pending lock which could cause a deadlock.
+ Should it be an anomaly or produce a warning ?
+ *)
+ ()
+ in
+ ignore (lseek fd pos SEEK_SET)
(* We make the assumption that an acquired lock can always be released *)
let do_under_lock kd fd f =
- if lock kd fd then finally f (fun () -> unlock fd) else f ()
+ if lock kd fd then fun_protect f ~finally:(fun () -> unlock fd) else f ()
let open_in f =
let flags = [O_RDONLY; O_CREAT] in
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 22:49:34 +0000