diff options
-rw-r--r-- | plugins/micromega/certificate.ml | 27 | ||||
-rw-r--r-- | plugins/micromega/coq_micromega.ml | 113 | ||||
-rw-r--r-- | plugins/micromega/mfourier.ml | 20 |
3 files changed, 118 insertions, 42 deletions
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index edb2640c4..86deb4c00 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -381,13 +381,15 @@ let linear_prover n_spec l = with x when Errors.noncritical x -> (print_string (Printexc.to_string x); None) -let linear_prover_with_cert spec l = - match linear_prover spec l with +let linear_prover_with_cert prfdepth spec l = + max_nb_cstr := (let len = List.length l in max len (len * prfdepth)) ; + match linear_prover spec l with | None -> None | Some cert -> Some (make_certificate spec cert) -let nlinear_prover (sys: (Mc.q Mc.pExpr * Mc.op1) list) = +let nlinear_prover prfdepth (sys: (Mc.q Mc.pExpr * Mc.op1) list) = LinPoly.MonT.clear (); + max_nb_cstr := (let len = List.length sys in max len (len * prfdepth)) ; (* Assign a proof to the initial hypotheses *) let sys = mapi (fun c i -> (c,Mc.PsatzIn (Ml2C.nat i))) sys in @@ -1164,8 +1166,9 @@ let reduce_var_change psys = List.for_all (fun (c,p) -> List.for_all (fun (_,n) -> sign_num n <> 0) c.coeffs) sys - let xlia reduction_equations sys = + let xlia (can_enum:bool) reduction_equations sys = + let rec enum_proof (id:int) (sys:prf_sys) : proof option = if debug then (Printf.printf "enum_proof\n" ; flush stdout) ; assert (check_sys sys) ; @@ -1203,7 +1206,7 @@ let reduce_var_change psys = Printf.printf "after reduction: %a \n" (pp_list (fun o (c,_) -> output_cstr o c)) sys ; match linear_prover sys with | Some prf -> Some (Step(id,prf,Done)) - | None -> enum_proof id sys + | None -> if can_enum then enum_proof id sys else None with FoundProof prf -> (* [reduction_equations] can find a proof *) Some(Step(id,prf,Done)) in @@ -1233,16 +1236,18 @@ let reduce_var_change psys = {coeffs = v ; op = o ; cst = minus_num c } - let lia sys = - LinPoly.MonT.clear (); + let lia (can_enum:bool) (prfdepth:int) sys = + LinPoly.MonT.clear (); + max_nb_cstr := (let len = List.length sys in max len (len * prfdepth)) ; let sys = List.map (develop_constraint z_spec) sys in let (sys:cstr_compat list) = List.map cstr_compat_of_poly sys in let sys = mapi (fun c i -> (c,Hyp i)) sys in - xlia reduction_equations sys + xlia can_enum reduction_equations sys - let nlia sys = - LinPoly.MonT.clear (); + let nlia enum prfdepth sys = + LinPoly.MonT.clear (); + max_nb_cstr := (let len = List.length sys in max len (len * prfdepth)) ; let sys = List.map (develop_constraint z_spec) sys in let sys = mapi (fun c i -> (c,Hyp i)) sys in @@ -1268,7 +1273,7 @@ let reduce_var_change psys = let sys = List.map (fun (c,p) -> cstr_compat_of_poly c,p) sys in assert (check_sys sys) ; - xlia (if is_linear then reduction_equations else reduction_non_lin_equations) sys + xlia enum (if is_linear then reduction_equations else reduction_non_lin_equations) sys diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 93588111b..ef1169342 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -19,6 +19,7 @@ open Pp open Mutils open Proofview +open Goptions (** * Debug flag @@ -38,6 +39,53 @@ let time str f x = flush stdout); res + +(* Limit the proof search *) + +let max_depth = max_int + +(* Search limit for provers over Q R *) +let lra_proof_depth = ref max_depth + + +(* Search limit for provers over Z *) +let lia_enum = ref true +let lia_proof_depth = ref max_depth + +let get_lia_option () = + (!lia_enum,!lia_proof_depth) + +let get_lra_option () = + !lra_proof_depth + + + +let _ = + + let int_opt l vref = + { + optsync = true; + optdepr = false; + optname = List.fold_right (^) l ""; + optkey = l ; + optread = (fun () -> Some !vref); + optwrite = (fun x -> vref := (match x with None -> max_depth | Some v -> v)) + } in + + let lia_enum_opt = + { + optsync = true; + optdepr = false; + optname = "Lia Enum"; + optkey = ["Lia";"Enum"]; + optread = (fun () -> !lia_enum); + optwrite = (fun x -> lia_enum := x) + } in + ignore (declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth)) ; + ignore (declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth)) ; + ignore (declare_bool_option lia_enum_opt) + + (** * Initialize a tag type to the Tag module declaration (see Mutils). *) @@ -1421,15 +1469,18 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* * The datastructures that aggregate prover attributes. *) -type ('a,'prf) prover = { +type ('option,'a,'prf) prover = { name : string ; (* name of the prover *) - prover : 'a list -> 'prf option ; (* the prover itself *) + get_option : unit ->'option ; (* find the options of the prover *) + prover : 'option * 'a list -> 'prf option ; (* the prover itself *) hyps : 'prf -> ISet.t ; (* extract the indexes of the hypotheses really used in the proof *) compact : 'prf -> (int -> int) -> 'prf ; (* remap the hyp indexes according to function *) pp_prf : out_channel -> 'prf -> unit ;(* pretting printing of proof *) pp_f : out_channel -> 'a -> unit (* pretty printing of the formulas (polynomials)*) } + + (** * Given a list of provers and a disjunction of atoms, find a proof of any of * the atoms. Returns an (optional) pair of a proof and a prover @@ -1439,7 +1490,7 @@ type ('a,'prf) prover = { let find_witness provers polys1 = let provers = List.map (fun p -> (fun l -> - match p.prover l with + match p.prover (p.get_option (),l) with | None -> None | Some prf -> Some(prf,p)) , p.name) provers in try_any provers (List.map fst polys1) @@ -1494,7 +1545,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) = let res = try prover.compact prf remap with x when Errors.noncritical x -> if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ; (* This should not happen -- this is the recovery plan... *) - match prover.prover (List.map fst new_cl) with + match prover.prover (prover.get_option () ,List.map fst new_cl) with | None -> failwith "proof compaction error" | Some p -> p in @@ -1677,6 +1728,7 @@ let micromega_gen ]) with | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") + | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; Tacticals.New.tclFAIL 0 (Pp.str (" Skipping what remains of this tactic: the complexity of the goal requires " @@ -1762,8 +1814,9 @@ let micromega_genr prover = micromega_order_changer res' env (abstract_wrt_formula ff' ff) ]) with - | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") - | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; + | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "TimeOut") + | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") + | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; Tacticals.New.tclFAIL 0 (Pp.str (" Skipping what remains of this tactic: the complexity of the goal requires " ^ "the use of a specialized external tool called csdp. \n\n" @@ -1929,34 +1982,40 @@ let compact_pt pt f = let lift_pexpr_prover p l = p (List.map (fun (e,o) -> Mc.denorm e , o) l) module CacheZ = PHashtable(struct - type t = (Mc.z Mc.pol * Mc.op1) list + type prover_option = bool * int + + type t = prover_option * ((Mc.z Mc.pol * Mc.op1) list) let equal = (=) let hash = Hashtbl.hash end) module CacheQ = PHashtable(struct - type t = (Mc.q Mc.pol * Mc.op1) list + type t = int * ((Mc.q Mc.pol * Mc.op1) list) let equal = (=) let hash = Hashtbl.hash end) -let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.lia) -let memo_nlia = CacheZ.memo "nlia.cache" (lift_pexpr_prover Certificate.nlia) -let memo_nra = CacheQ.memo "nra.cache" (lift_pexpr_prover (Certificate.nlinear_prover)) +let memo_zlinear_prover = CacheZ.memo "lia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s) +let memo_nlia = CacheZ.memo "nlia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s) +let memo_nra = CacheQ.memo "nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s) + + let linear_prover_Q = { - name = "linear prover"; - prover = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.q_spec) ; - hyps = hyps_of_cone ; - compact = compact_cone ; - pp_prf = pp_psatz pp_q ; - pp_f = fun o x -> pp_pol pp_q o (fst x) + name = "linear prover"; + get_option = get_lra_option ; + prover = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o Certificate.q_spec) l) ; + hyps = hyps_of_cone ; + compact = compact_cone ; + pp_prf = pp_psatz pp_q ; + pp_f = fun o x -> pp_pol pp_q o (fst x) } let linear_prover_R = { name = "linear prover"; - prover = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.q_spec) ; + get_option = get_lra_option ; + prover = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o Certificate.q_spec) l) ; hyps = hyps_of_cone ; compact = compact_cone ; pp_prf = pp_psatz pp_q ; @@ -1965,7 +2024,8 @@ let linear_prover_R = { let nlinear_prover_R = { name = "nra"; - prover = memo_nra ; + get_option = get_lra_option; + prover = memo_nra ; hyps = hyps_of_cone ; compact = compact_cone ; pp_prf = pp_psatz pp_q ; @@ -1974,7 +2034,8 @@ let nlinear_prover_R = { let non_linear_prover_Q str o = { name = "real nonlinear prover"; - prover = call_csdpcert_q (str, o); + get_option = (fun () -> (str,o)); + prover = (fun (o,l) -> call_csdpcert_q o l); hyps = hyps_of_cone; compact = compact_cone ; pp_prf = pp_psatz pp_q ; @@ -1983,7 +2044,8 @@ let non_linear_prover_Q str o = { let non_linear_prover_R str o = { name = "real nonlinear prover"; - prover = call_csdpcert_q (str, o); + get_option = (fun () -> (str,o)); + prover = (fun (o,l) -> call_csdpcert_q o l); hyps = hyps_of_cone; compact = compact_cone; pp_prf = pp_psatz pp_q; @@ -1992,7 +2054,8 @@ let non_linear_prover_R str o = { let non_linear_prover_Z str o = { name = "real nonlinear prover"; - prover = lift_ratproof (call_csdpcert_z (str, o)); + get_option = (fun () -> (str,o)); + prover = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l); hyps = hyps_of_pt; compact = compact_pt; pp_prf = pp_proof_term; @@ -2002,7 +2065,8 @@ let non_linear_prover_Z str o = { let linear_Z = { name = "lia"; - prover = memo_zlinear_prover ; + get_option = get_lia_option; + prover = memo_zlinear_prover ; hyps = hyps_of_pt; compact = compact_pt; pp_prf = pp_proof_term; @@ -2011,7 +2075,8 @@ let linear_Z = { let nlinear_Z = { name = "nlia"; - prover = memo_nlia ; + get_option = get_lia_option; + prover = memo_nlia ; hyps = hyps_of_pt; compact = compact_pt; pp_prf = pp_proof_term; diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 88c1a7836..024720449 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -98,12 +98,12 @@ module PSet = ISet module System = Hashtbl.Make(Vect) - type proof = - | Hyp of int - | Elim of var * proof * proof - | And of proof * proof - +type proof = +| Hyp of int +| Elim of var * proof * proof +| And of proof * proof +let max_nb_cstr = ref max_int type system = { sys : cstr_info ref System.t ; @@ -208,8 +208,7 @@ let merge_cstr_info i1 i2 = *) let xadd_cstr vect cstr_info sys = - if debug && Int.equal (System.length sys mod 1000) 0 then (print_string "*" ; flush stdout) ; - try + try let info = System.find sys vect in match merge_cstr_info cstr_info !info with | None -> raise (SystemContradiction (And(cstr_info.prf, (!info).prf))) @@ -217,6 +216,13 @@ let xadd_cstr vect cstr_info sys = with | Not_found -> System.replace sys vect (ref cstr_info) +exception TimeOut + +let xadd_cstr vect cstr_info sys = + if debug && Int.equal (System.length sys mod 1000) 0 then (print_string "*" ; flush stdout) ; + if System.length sys < !max_nb_cstr + then xadd_cstr vect cstr_info sys + else raise TimeOut type cstr_ext = | Contradiction (** The constraint is contradictory. |