diff options
| author |  xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-14 08:32:27 +0000 |
|---|---|---|
| committer | xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-14 08:32:27 +0000 |
| commit | 2a20061cc2790eedee7fab6230fe1dd2b4d58c24 (patch) | |
| tree | 29cf49dbd60428709991f9d545b565751c03e858 /plugins/micromega/certificate.ml | |
| parent | ec5ed7870b4b59e05c5e994c9bad35e28685b8bd (diff) | |
Remove some uses of local modules (some were unused, some were costly).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16883 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/micromega/certificate.ml')
| -rw-r--r-- | plugins/micromega/certificate.ml | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 2e8030ebf..8db2841c2 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -230,6 +230,7 @@ let string_of_op = function | Mc.NonEqual -> "<> 0" +module MonSet = Set.Make(Monomial) (* If the certificate includes at least one strict inequality, the obtained polynomial can also be 0 *) @@ -238,8 +239,6 @@ let build_linear_system l = (* Gather the monomials: HINT add up of the polynomials ==> This does not work anymore *) let l' = List.map fst l in - let module MonSet = Set.Make(Monomial) in - let monomials = List.fold_left (fun acc p -> Poly.fold (fun m _ acc -> MonSet.add m acc) p acc) @@ -299,16 +298,17 @@ exception Found of Monomial.t exception Strict +module MonMap = Map.Make(Monomial) + let primal l = let vr = ref 0 in - let module Mmn = Map.Make(Monomial) in let vect_of_poly map p = Poly.fold (fun mn vl (map,vect) -> if mn = Monomial.const then (map,vect) else - let (mn,m) = try (Mmn.find mn map,map) with Not_found -> let res = (!vr, Mmn.add mn !vr map) in incr vr ; res in + let (mn,m) = try (MonMap.find mn map,map) with Not_found -> let res = (!vr, MonMap.add mn !vr map) in incr vr ; res in (m,if sign_num vl = 0 then vect else (mn,vl)::vect)) p (map,[]) in let op_op = function Mc.NonStrict -> Ge |Mc.Equal -> Eq | _ -> raise Strict in @@ -319,7 +319,7 @@ let primal l = let (mp,vect) = vect_of_poly map p in let cstr = {coeffs = List.sort cmp vect; op = op_op op ; cst = minus_num (Poly.get Monomial.const p)} in - (mp,cstr::l)) l (Mmn.empty,[])) + (mp,cstr::l)) l (MonMap.empty,[])) let dual_raw_certificate (l: (Poly.t * Mc.op1) list) = (* List.iter (fun (p,op) -> Printf.fprintf stdout "%a %s 0\n" Poly.pp p (string_of_op op) ) l ; *) @@ -1195,8 +1195,6 @@ let reduce_var_change psys = let is_linear = List.for_all (fun ((p,_),_) -> Poly.is_linear p) sys in - let module MonMap = Map.Make(Monomial) in - let collect_square = List.fold_left (fun acc ((p,_),_) -> Poly.fold (fun m _ acc -> |