diff options
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/certificate.ml | 5 | ||||
| -rw-r--r-- | plugins/micromega/sos.ml | 31 | ||||
| -rw-r--r-- | plugins/micromega/zify.ml | 11 |
3 files changed, 26 insertions, 21 deletions
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 9eeba614c7..148c1772bf 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -1020,10 +1020,11 @@ let lia (can_enum : bool) (prfdepth : int) sys = p) sys end; + let bnd1 = bound_monomials sys in let sys = subst sys in - let bnd = bound_monomials sys in + let bnd2 = bound_monomials sys in (* To deal with non-linear monomials *) - let sys = bnd @ saturate_by_linear_equalities sys @ sys in + let sys = bnd1 @ bnd2 @ saturate_by_linear_equalities sys @ sys in let sys' = List.map (fun ((p, o), prf) -> (cstr_of_poly (p, o), prf)) sys in xlia (List.map fst sys) can_enum reduction_equations sys' diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml index 2b04bb80e2..03d2a2d233 100644 --- a/plugins/micromega/sos.ml +++ b/plugins/micromega/sos.ml @@ -80,7 +80,7 @@ let is_zero (d, v) = match v with Empty -> true | _ -> false (* Vectors. Conventionally indexed 1..n. *) (* ------------------------------------------------------------------------- *) -let vector_0 n = ((n, undefined) : vector) +let vector_0 n : vector = (n, undefined) let dim (v : vector) = fst v let vector_const c n = @@ -99,7 +99,7 @@ let vector_of_list l = (* Matrices; again rows and columns indexed from 1. *) (* ------------------------------------------------------------------------- *) -let matrix_0 (m, n) = (((m, n), undefined) : matrix) +let matrix_0 (m, n) : matrix = ((m, n), undefined) let dimensions (m : matrix) = fst m let matrix_cmul c (m : matrix) = @@ -107,7 +107,7 @@ let matrix_cmul c (m : matrix) = if c =/ Q.zero then matrix_0 (i, j) else ((i, j), mapf (fun x -> c */ x) (snd m)) -let matrix_neg (m : matrix) = ((dimensions m, mapf Q.neg (snd m)) : matrix) +let matrix_neg (m : matrix) : matrix = (dimensions m, mapf Q.neg (snd m)) let matrix_add (m1 : matrix) (m2 : matrix) = let d1 = dimensions m1 and d2 = dimensions m2 in @@ -138,7 +138,7 @@ let diagonal (v : vector) = (* Monomials. *) (* ------------------------------------------------------------------------- *) let monomial_1 = (undefined : monomial) -let monomial_var x = (x |=> 1 : monomial) +let monomial_var x : monomial = x |=> 1 let (monomial_mul : monomial -> monomial -> monomial) = combine ( + ) (fun x -> false) @@ -152,16 +152,16 @@ let monomial_variables m = dom m (* ------------------------------------------------------------------------- *) let poly_0 = (undefined : poly) let poly_isconst (p : poly) = foldl (fun a m c -> m = monomial_1 && a) true p -let poly_var x = (monomial_var x |=> Q.one : poly) +let poly_var x : poly = monomial_var x |=> Q.one let poly_const c = if c =/ Q.zero then poly_0 else monomial_1 |=> c let poly_cmul c (p : poly) = if c =/ Q.zero then poly_0 else mapf (fun x -> c */ x) p -let poly_neg (p : poly) = (mapf Q.neg p : poly) +let poly_neg (p : poly) : poly = mapf Q.neg p -let poly_add (p1 : poly) (p2 : poly) = - (combine ( +/ ) (fun x -> x =/ Q.zero) p1 p2 : poly) +let poly_add (p1 : poly) (p2 : poly) : poly = + combine ( +/ ) (fun x -> x =/ Q.zero) p1 p2 let poly_sub p1 p2 = poly_add p1 (poly_neg p2) @@ -1191,14 +1191,13 @@ let sumofsquares_general_symmetry tool pol = let diagents = end_itlist equation_add (List.map (fun i -> apply allassig (i, i)) (1 -- n)) in - let mk_matrix v = - ( ( (n, n) - , foldl - (fun m (i, j) ass -> - let c = tryapplyd ass v Q.zero in - if c =/ Q.zero then m else ((j, i) |-> c) (((i, j) |-> c) m)) - undefined allassig ) - : matrix ) + let mk_matrix v : matrix = + ( (n, n) + , foldl + (fun m (i, j) ass -> + let c = tryapplyd ass v Q.zero in + if c =/ Q.zero then m else ((j, i) |-> c) (((i, j) |-> c) m)) + undefined allassig ) in let mats = List.map mk_matrix qvars and obj = diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 4e1f9a66ac..fa29e6080e 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -1324,9 +1324,14 @@ let do_let tac (h : Constr.named_declaration) = let env = Tacmach.New.pf_env gl in let evd = Tacmach.New.project gl in try - ignore (get_injection env evd (EConstr.of_constr ty)); - tac id.Context.binder_name (EConstr.of_constr t) - (EConstr.of_constr ty) + let x = id.Context.binder_name in + ignore + (let eq = Lazy.force eq in + find_option + (match_operator env evd eq + [|EConstr.of_constr ty; EConstr.mkVar x; EConstr.of_constr t|]) + (HConstr.find_all eq !table_cache)); + tac x (EConstr.of_constr t) (EConstr.of_constr ty) with Not_found -> Tacticals.New.tclIDTAC) let iter_let_aux tac = |