aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega
diff options
context:
space:
mode:
authorGravatar xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-14 08:32:27 +0000
committerGravatar xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-14 08:32:27 +0000
commit2a20061cc2790eedee7fab6230fe1dd2b4d58c24 (patch)
tree29cf49dbd60428709991f9d545b565751c03e858 /plugins/micromega
parentec5ed7870b4b59e05c5e994c9bad35e28685b8bd (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')
-rw-r--r--plugins/micromega/certificate.ml12
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 ->