From 3fcadca93b8d9dd70d9d93412cbacf8d4e851ed7 Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Tue, 26 May 2015 14:03:00 +0200 Subject: micromega : options to limit proof search --- plugins/micromega/mfourier.ml | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) (limited to 'plugins/micromega/mfourier.ml') 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. -- cgit v1.2.3