micromega : options to limit proof search

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.