summaryrefslogtreecommitdiff
path: root/plugins/micromega/certificate.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/certificate.ml')
-rw-r--r--plugins/micromega/certificate.ml96
1 files changed, 46 insertions, 50 deletions
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 32aeb993..b4f305dd 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -76,7 +76,7 @@ let dev_form n_spec p =
let p = dev_form p in
let n = C2Ml.n n in
let rec pow n =
- if n = 0
+ if Int.equal n 0
then Poly.constant (n_spec.number_to_num n_spec.unit)
else Poly.product p (pow (n-1)) in
pow n in
@@ -87,8 +87,8 @@ let monomial_to_polynomial mn =
Monomial.fold
(fun v i acc ->
let v = Ml2C.positive v in
- let mn = if i = 1 then Mc.PEX v else Mc.PEpow (Mc.PEX v ,Ml2C.n i) in
- if acc = Mc.PEc (Mc.Zpos Mc.XH)
+ let mn = if Int.equal i 1 then Mc.PEX v else Mc.PEpow (Mc.PEX v ,Ml2C.n i) in
+ if Pervasives.(=) acc (Mc.PEc (Mc.Zpos Mc.XH)) (** FIXME *)
then mn
else Mc.PEmul(mn,acc))
mn
@@ -105,10 +105,10 @@ let list_to_polynomial vars l =
| c::l -> if c =/ (Int 0) then xtopoly p (i+1) l
else let c = Mc.PEc (Ml2C.bigint (numerator c)) in
let mn =
- if c = Mc.PEc (Mc.Zpos Mc.XH)
+ if Pervasives.(=) c (Mc.PEc (Mc.Zpos Mc.XH))
then var i
else Mc.PEmul (c,var i) in
- let p' = if p = Mc.PEc Mc.Z0 then mn else
+ let p' = if Pervasives.(=) p (Mc.PEc Mc.Z0) then mn else
Mc.PEadd (mn, p) in
xtopoly p' (i+1) l in
@@ -116,7 +116,7 @@ let list_to_polynomial vars l =
let rec fixpoint f x =
let y' = f x in
- if y' = x then y'
+ if Pervasives.(=) y' x then y'
else fixpoint f y'
let rec_simpl_cone n_spec e =
@@ -153,9 +153,9 @@ let factorise_linear_cone c =
let factorise c1 c2 =
match c1 , c2 with
| Mc.PsatzMulC(x,y) , Mc.PsatzMulC(x',y') ->
- if x = x' then Some (Mc.PsatzMulC(x, Mc.PsatzAdd(y,y'))) else None
+ if Pervasives.(=) x x' then Some (Mc.PsatzMulC(x, Mc.PsatzAdd(y,y'))) else None
| Mc.PsatzMulE(x,y) , Mc.PsatzMulE(x',y') ->
- if x = x' then Some (Mc.PsatzMulE(x, Mc.PsatzAdd(y,y'))) else None
+ if Pervasives.(=) x x' then Some (Mc.PsatzMulE(x, Mc.PsatzAdd(y,y'))) else None
| _ -> None in
let rec rebuild_cone l pending =
@@ -199,7 +199,7 @@ open Mfourier
let constrain_monomial mn l =
let coeffs = List.fold_left (fun acc p -> (Poly.get mn p)::acc) [] l in
- if mn = Monomial.const
+ if Pervasives.(=) mn Monomial.const
then
{ coeffs = Vect.from_list ((Big_int unit_big_int):: (List.rev coeffs)) ;
op = Eq ;
@@ -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,27 +298,28 @@ 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
+ if Pervasives.(=) 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
- (m,if sign_num vl = 0 then vect else (mn,vl)::vect)) p (map,[]) 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 Int.equal (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
- let cmp x y = Pervasives.compare (fst x) (fst y) in
+ let cmp x y = Int.compare (fst x) (fst y) in
snd (List.fold_right (fun (p,op) (map,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 ; *)
@@ -332,8 +332,8 @@ let dual_raw_certificate (l: (Poly.t * Mc.op1) list) =
| Inl cert -> Some (rats_to_ints (Vect.to_list cert))
(* should not use rats_to_ints *)
with x when Errors.noncritical x ->
- if debug
- then (Printf.printf "raw certificate %s" (Printexc.to_string x);
+ if debug
+ then (Printf.printf "raw certificate %s" (Printexc.to_string x);
flush stdout) ;
None
@@ -367,7 +367,7 @@ let linear_prover n_spec l =
let build_system n_spec l =
let li = List.combine l (interval 0 (List.length l -1)) in
let (l1,l') = List.partition
- (fun (x,_) -> if snd x = Mc.NonEqual then true else false) li in
+ (fun (x,_) -> if Pervasives.(=) (snd x) Mc.NonEqual then true else false) li in
List.map
(fun ((x,y),i) -> match y with
Mc.NonEqual -> failwith "cannot happen"
@@ -378,7 +378,7 @@ let linear_prover n_spec l =
let linear_prover n_spec l =
try linear_prover n_spec l
- with x when x <> Sys.Break ->
+ with x when Errors.noncritical x ->
(print_string (Printexc.to_string x); None)
let linear_prover_with_cert spec l =
@@ -394,7 +394,7 @@ let make_linear_system l =
let monomials = List.fold_left (fun acc p -> Poly.addition p acc)
(Poly.constant (Int 0)) l' in
let monomials = Poly.fold
- (fun mn _ l -> if mn = Monomial.const then l else mn::l) monomials [] in
+ (fun mn _ l -> if Pervasives.(=) mn Monomial.const then l else mn::l) monomials [] in
(List.map (fun (c,op) ->
{coeffs = Vect.from_list (List.map (fun mn -> (Poly.get mn c)) monomials) ;
op = op ;
@@ -406,9 +406,7 @@ let pplus x y = Mc.PEadd(x,y)
let pmult x y = Mc.PEmul(x,y)
let pconst x = Mc.PEc x
let popp x = Mc.PEopp x
-
-let debug = false
-
+
(* keep track of enumerated vectors *)
let rec mem p x l =
match l with [] -> false | e::l -> if p x e then true else mem p x l
@@ -417,7 +415,7 @@ let rec remove_assoc p x l =
match l with [] -> [] | e::l -> if p x (fst e) then
remove_assoc p x l else e::(remove_assoc p x l)
-let eq x y = Vect.compare x y = 0
+let eq x y = Int.equal (Vect.compare x y) 0
let remove e l = List.fold_left (fun l x -> if eq x e then l else x::l) [] l
@@ -477,7 +475,7 @@ let rec scale_term t =
let s1' = div_big_int s1 g in
let s2' = div_big_int s2 g in
let e = mult_big_int g (mult_big_int s1' s2') in
- if (compare_big_int e unit_big_int) = 0
+ if Int.equal (compare_big_int e unit_big_int) 0
then (unit_big_int, Add (y1,y2))
else e, Add (Mul(Const (Big_int s2'), y1),
Mul (Const (Big_int s1'), y2))
@@ -499,7 +497,7 @@ let get_index_of_ith_match f i l =
| [] -> failwith "bad index"
| e::l -> if f e
then
- (if j = i then res else get (j+1) (res+1) l )
+ (if Int.equal j i then res else get (j+1) (res+1) l )
else get j (res+1) l in
get 0 0 l
@@ -559,7 +557,7 @@ let q_cert_of_pos pos =
| Axiom_lt i -> Mc.PsatzIn (Ml2C.nat i)
| Monoid l -> product l
| Rational_eq n | Rational_le n | Rational_lt n ->
- if compare_num n (Int 0) = 0 then Mc.PsatzZ else
+ if Int.equal (compare_num n (Int 0)) 0 then Mc.PsatzZ else
Mc.PsatzC (Ml2C.q n)
| Square t -> Mc.PsatzSquare (term_to_q_pol t)
| Eqmul (t, y) -> Mc.PsatzMulC(term_to_q_pol t, _cert_of_pos y)
@@ -590,7 +588,7 @@ let z_cert_of_pos pos =
| Axiom_lt i -> Mc.PsatzIn (Ml2C.nat i)
| Monoid l -> product l
| Rational_eq n | Rational_le n | Rational_lt n ->
- if compare_num n (Int 0) = 0 then Mc.PsatzZ else
+ if Int.equal (compare_num n (Int 0)) 0 then Mc.PsatzZ else
Mc.PsatzC (Ml2C.bigint (big_int_of_num n))
| Square t -> Mc.PsatzSquare (term_to_z_pol t)
| Eqmul (t, y) ->
@@ -631,7 +629,7 @@ struct
let rec xid_of_hyp i l =
match l with
| [] -> failwith "id_of_hyp"
- | hyp'::l -> if hyp = hyp' then i else xid_of_hyp (i+1) l in
+ | hyp'::l -> if Pervasives.(=) hyp hyp' then i else xid_of_hyp (i+1) l in
xid_of_hyp 0 l
end
@@ -757,7 +755,7 @@ let check_sat (cstr,prf) =
if eq_num gcd (Int 1)
then Normalise(cstr,prf)
else
- if sign_num (mod_num cst gcd) = 0
+ if Int.equal (sign_num (mod_num cst gcd)) 0
then (* We can really normalise *)
begin
assert (sign_num gcd >=1 ) ;
@@ -797,18 +795,18 @@ let pivot v (c1,p1) (c2,p2) =
match Vect.get v v1 , Vect.get v v2 with
| None , _ | _ , None -> None
| Some a , Some b ->
- if (sign_num a) * (sign_num b) = -1
+ if Int.equal ((sign_num a) * (sign_num b)) (-1)
then
let cv1 = abs_num b
and cv2 = abs_num a in
Some (xpivot cv1 cv2)
else
- if op1 = Eq
+ if op1 == Eq
then
let cv1 = minus_num (b */ (Int (sign_num a)))
and cv2 = abs_num a in
Some (xpivot cv1 cv2)
- else if op2 = Eq
+ else if op2 == Eq
then
let cv1 = abs_num b
and cv2 = minus_num (a */ (Int (sign_num b))) in
@@ -817,7 +815,7 @@ let pivot v (c1,p1) (c2,p2) =
exception FoundProof of prf_rule
-let rec simpl_sys sys =
+let simpl_sys sys =
List.fold_left (fun acc (c,p) ->
match check_sat (c,p) with
| Tauto -> acc
@@ -831,7 +829,7 @@ let rec simpl_sys sys =
Source: http://en.wikipedia.org/wiki/Extended_Euclidean_algorithm
*)
let rec ext_gcd a b =
- if sign_big_int b = 0
+ if Int.equal (sign_big_int b) 0
then (unit_big_int,zero_big_int)
else
let (q,r) = quomod_big_int a b in
@@ -852,7 +850,7 @@ let pp_ext_gcd a b =
exception Result of (int * (proof * cstr_compat))
let split_equations psys =
- List.partition (fun (c,p) -> c.op = Eq)
+ List.partition (fun (c,p) -> c.op == Eq)
let extract_coprime (c1,p1) (c2,p2) =
@@ -860,9 +858,9 @@ let extract_coprime (c1,p1) (c2,p2) =
match vect1 , vect2 with
| _ , [] | [], _ -> None
| (v1,n1)::vect1' , (v2, n2) :: vect2' ->
- if v1 = v2
+ if Pervasives.(=) v1 v2
then
- if compare_big_int (gcd_big_int (numerator n1) (numerator n2)) unit_big_int = 0
+ if Int.equal (compare_big_int (gcd_big_int (numerator n1) (numerator n2)) unit_big_int) 0
then Some (v1,n1,n2)
else
exist2 vect1' vect2'
@@ -871,7 +869,7 @@ let extract_coprime (c1,p1) (c2,p2) =
then exist2 vect1' vect2
else exist2 vect1 vect2' in
- if c1.op = Eq && c2.op = Eq
+ if c1.op == Eq && c2.op == Eq
then exist2 c1.coeffs c2.coeffs
else None
@@ -928,7 +926,7 @@ let reduce_coprime psys =
(** If there is an equation [eq] of the form 1.x + e = c, do a pivot over x with equation [eq] *)
let reduce_unary psys =
let is_unary_equation (cstr,prf) =
- if cstr.op = Eq
+ if cstr.op == Eq
then
try
Some (fst (List.find (fun (_,n) -> n =/ (Int 1) || n=/ (Int (-1))) cstr.coeffs))
@@ -944,12 +942,12 @@ let reduce_unary psys =
let reduce_non_lin_unary psys =
let is_unary_equation (cstr,prf) =
- if cstr.op = Eq
+ if cstr.op == Eq
then
try
let x = fst (List.find (fun (x,n) -> (n =/ (Int 1) || n=/ (Int (-1))) && Monomial.is_var (LinPoly.MonT.retrieve x) ) cstr.coeffs) in
let x' = LinPoly.MonT.retrieve x in
- if List.for_all (fun (y,_) -> y = x || snd (Monomial.div (LinPoly.MonT.retrieve y) x') = 0) cstr.coeffs
+ if List.for_all (fun (y,_) -> Pervasives.(=) y x || Int.equal (snd (Monomial.div (LinPoly.MonT.retrieve y) x')) 0) cstr.coeffs
then Some x
else None
with Not_found -> None
@@ -976,7 +974,7 @@ let reduce_var_change psys =
Some ((x,v),(x',numerator v'))
with Not_found -> rel_prime vect in
- let rel_prime (cstr,prf) = if cstr.op = Eq then rel_prime cstr.coeffs else None in
+ let rel_prime (cstr,prf) = if cstr.op == Eq then rel_prime cstr.coeffs else None in
let (oeq,sys) = extract rel_prime psys in
@@ -1007,7 +1005,7 @@ let reduce_var_change psys =
let reduce_pivot psys =
let is_equation (cstr,prf) =
- if cstr.op = Eq
+ if cstr.op == Eq
then
try
Some (fst (List.hd cstr.coeffs))
@@ -1067,7 +1065,7 @@ let reduce_var_change psys =
(* For lia, there are no equations => these precautions are not needed *)
(* For nlia, there are equations => do not enumerate over equations! *)
let all_planes sys =
- let (eq,ineq) = List.partition (fun c -> c.op = Eq) sys in
+ let (eq,ineq) = List.partition (fun c -> c.op == Eq) sys in
match eq with
| [] -> List.rev_map (fun c -> c.coeffs) ineq
| _ ->
@@ -1197,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 ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 07:24:15 +0000