From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- plugins/micromega/certificate.ml | 194 ++------------------------------------- 1 file changed, 7 insertions(+), 187 deletions(-) (limited to 'plugins/micromega/certificate.ml') diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 9f39191f..3a9709b6 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -17,10 +17,9 @@ (* We take as input a list of polynomials [p1...pn] and return an unfeasibility certificate polynomial. *) -type var = int - - +let debug = false +open Util open Big_int open Num open Polynomial @@ -59,9 +58,6 @@ let q_spec = { eqb = Mc.qeq_bool } -let r_spec = z_spec - - let dev_form n_spec p = let rec dev_form p = match p with @@ -84,38 +80,6 @@ let dev_form n_spec p = pow n in dev_form p - -let monomial_to_polynomial mn = - Monomial.fold - (fun v i acc -> - let v = Ml2C.positive v in - 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 - (Mc.PEc (Mc.Zpos Mc.XH)) - - - -let list_to_polynomial vars l = - assert (List.for_all (fun x -> ceiling_num x =/ x) l); - let var x = monomial_to_polynomial (List.nth vars x) in - - let rec xtopoly p i = function - | [] -> p - | 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 Pervasives.(=) c (Mc.PEc (Mc.Zpos Mc.XH)) - then var i - else Mc.PEmul (c,var i) in - let p' = if Pervasives.(=) p (Mc.PEc Mc.Z0) then mn else - Mc.PEadd (mn, p) in - xtopoly p' (i+1) l in - - xtopoly (Mc.PEc Mc.Z0) 0 l - let rec fixpoint f x = let y' = f x in if Pervasives.(=) y' x then y' @@ -135,15 +99,6 @@ let rec_simpl_cone n_spec e = let simplify_cone n_spec c = fixpoint (rec_simpl_cone n_spec) c - -type cone_prod = - Const of cone -| Ideal of cone *cone -| Mult of cone * cone -| Other of cone -and cone = Mc.zWitness - - let factorise_linear_cone c = @@ -224,14 +179,6 @@ let positivity l = in xpositivity 0 l - -let string_of_op = function - | Mc.Strict -> "> 0" - | Mc.NonStrict -> ">= 0" - | Mc.Equal -> "= 0" - | Mc.NonEqual -> "<> 0" - - module MonSet = Set.Make(Monomial) (* If the certificate includes at least one strict inequality, @@ -261,9 +208,6 @@ let build_linear_system l = op = Ge ; cst = Big_int zero_big_int}::(strict::(positivity l)@s0) - -let big_int_to_z = Ml2C.bigint - (* For Q, this is a pity that the certificate has been scaled -- at a lower layer, certificates are using nums... *) let make_certificate n_spec (cert,li) = @@ -296,8 +240,6 @@ let make_certificate n_spec (cert,li) = (simplify_cone n_spec (scalar_product cert' li))) -exception Found of Monomial.t - exception Strict module MonMap = Map.Make(Monomial) @@ -367,7 +309,7 @@ let simple_linear_prover l = 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 li = List.combine l (CList.interval 0 (List.length l -1)) in let (l1,l') = List.partition (fun (x,_) -> if Pervasives.(=) (snd x) Mc.NonEqual then true else false) li in List.map @@ -397,7 +339,7 @@ let nlinear_prover prfdepth (sys: (Mc.q Mc.pExpr * Mc.op1) list) = LinPoly.MonT.clear (); max_nb_cstr := compute_max_nb_cstr sys prfdepth ; (* Assign a proof to the initial hypotheses *) - let sys = mapi (fun c i -> (c,Mc.PsatzIn (Ml2C.nat i))) sys in + let sys = List.mapi (fun i c -> (c,Mc.PsatzIn (Ml2C.nat i))) sys in (* Add all the product of hypotheses *) @@ -452,39 +394,6 @@ let nlinear_prover prfdepth (sys: (Mc.q Mc.pExpr * Mc.op1) list) = | Mc.PsatzZ -> Mc.PsatzZ in Some (map_psatz cert) - - -let make_linear_system l = - let l' = List.map fst l in - 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 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 ; - cst = minus_num ( (Poly.get Monomial.const c))}) l - ,monomials) - - -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 - -(* 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 - -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 = 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 - - (* The prover is (probably) incomplete -- only searching for naive cutting planes *) @@ -494,38 +403,6 @@ let develop_constraint z_spec (e,k) = | Mc.Equal -> (dev_form z_spec e , Eq) | _ -> assert false - -let op_of_op_compat = function - | Ge -> Mc.NonStrict - | Eq -> Mc.Equal - - -let integer_vector coeffs = - let vars , coeffs = List.split coeffs in - List.combine vars (List.map (fun x -> Big_int x) (rats_to_ints coeffs)) - -let integer_cstr {coeffs = coeffs ; op = op ; cst = cst } = - let vars , coeffs = List.split coeffs in - match rats_to_ints (cst::coeffs) with - | cst :: coeffs -> - { - coeffs = List.combine vars (List.map (fun x -> Big_int x) coeffs) ; - op = op ; cst = Big_int cst} - | _ -> assert false - - -let pexpr_of_cstr_compat var cstr = - let {coeffs = coeffs ; op = op ; cst = cst } = integer_cstr cstr in - try - let expr = list_to_polynomial var (Vect.to_list coeffs) in - let d = Ml2C.bigint (denominator cst) in - let n = Ml2C.bigint (numerator cst) in - (pplus (pmult (pconst d) expr) (popp (pconst n)), op_of_op_compat op) - with Failure _ -> failwith "pexpr_of_cstr_compat" - - - - open Sos_types let rec scale_term t = @@ -555,18 +432,6 @@ let scale_term t = let (s,t') = scale_term t in s,t' - -let get_index_of_ith_match f i l = - let rec get j res l = - match l with - | [] -> failwith "bad index" - | e::l -> if f e - then - (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 - - let rec scale_certificate pos = match pos with | Axiom_eq i -> unit_big_int , Axiom_eq i | Axiom_le i -> unit_big_int , Axiom_le i @@ -681,8 +546,6 @@ open Polynomial module Env = struct - type t = int list - let id_of_hyp hyp l = let rec xid_of_hyp i l = match l with @@ -749,9 +612,6 @@ let xlinear_prover sys = | Inl _ -> None -let output_num o n = output_string o (string_of_num n) -let output_bigint o n = output_string o (string_of_big_int n) - let proof_of_farkas prf cert = (* Printf.printf "\nproof_of_farkas %a , %a \n" (pp_list output_prf_rule) prf (pp_list output_bigint) cert ; *) let rec mk_farkas acc prf cert = @@ -894,23 +754,6 @@ let rec ext_gcd a b = let (s,t) = ext_gcd b r in (t, sub_big_int s (mult_big_int q t)) - -let pp_ext_gcd a b = - let a' = big_int_of_int a in - let b' = big_int_of_int b in - - let (x,y) = ext_gcd a' b' in - Printf.fprintf stdout "%s * %s + %s * %s = %s\n" - (string_of_big_int x) (string_of_big_int a') - (string_of_big_int y) (string_of_big_int b') - (string_of_big_int (add_big_int (mult_big_int x a') (mult_big_int y b'))) - -exception Result of (int * (proof * cstr_compat)) - -let split_equations psys = - List.partition (fun (c,p) -> c.op == Eq) - - let extract_coprime (c1,p1) (c2,p2) = let rec exist2 vect1 vect2 = match vect1 , vect2 with @@ -1058,29 +901,6 @@ let reduce_var_change psys = Some (apply_and_normalise pivot_eq sys) - - - -let reduce_pivot psys = - let is_equation (cstr,prf) = - if cstr.op == Eq - then - try - Some (fst (List.hd cstr.coeffs)) - with Not_found -> None - else None in - let (oeq,sys) = extract is_equation psys in - match oeq with - | None -> None (* Nothing to do *) - | Some(v,pc) -> - if debug then - Printf.printf "Bad news : loss of completeness %a=%s" Vect.pp_vect (fst pc).coeffs (string_of_num (fst pc).cst); - Some(pivot_sys v pc sys) - - - - - let iterate_until_stable f x = let rec iter x = match f x with @@ -1225,7 +1045,7 @@ let xlia (can_enum:bool) reduction_equations sys = | None -> None | Some prf -> (*Printf.printf "direct proof %a\n" output_proof prf ; *) - let env = mapi (fun _ i -> i) sys in + let env = List.mapi (fun i _ -> i) sys in let prf = compile_proof env prf in (*try if Mc.zChecker sys' prf then Some prf else @@ -1244,7 +1064,7 @@ let lia (can_enum:bool) (prfdepth:int) sys = max_nb_cstr := compute_max_nb_cstr sys prfdepth ; let sys = List.map (develop_constraint z_spec) sys in let (sys:cstr_compat list) = List.map cstr_compat_of_poly sys in - let sys = mapi (fun c i -> (c,Hyp i)) sys in + let sys = List.mapi (fun i c -> (c,Hyp i)) sys in xlia can_enum reduction_equations sys @@ -1252,7 +1072,7 @@ let nlia enum prfdepth sys = LinPoly.MonT.clear (); max_nb_cstr := compute_max_nb_cstr sys prfdepth; let sys = List.map (develop_constraint z_spec) sys in - let sys = mapi (fun c i -> (c,Hyp i)) sys in + let sys = List.mapi (fun i c -> (c,Hyp i)) sys in let is_linear = List.for_all (fun ((p,_),_) -> Poly.is_linear p) sys in -- cgit v1.2.3