From 52980aab9541a12619eb9191a94e9b2ba4684447 Mon Sep 17 00:00:00 2001 From: vblot <24938579+vblot@users.noreply.github.com> Date: Fri, 28 May 2021 17:28:25 +0200 Subject: Get rid of most of our copy of micromega's source code (#94) --- src/lia/lia.ml | 177 ++--------------------------------- src/versions/native/structures.ml | 2 - src/versions/native/structures.mli | 2 - src/versions/standard/structures.ml | 5 +- src/versions/standard/structures.mli | 3 - 5 files changed, 10 insertions(+), 179 deletions(-) diff --git a/src/lia/lia.ml b/src/lia/lia.ml index 4e89f61..53dbf6d 100644 --- a/src/lia/lia.ml +++ b/src/lia/lia.ml @@ -151,178 +151,19 @@ let binop_list tbl op def l = let smt_clause_to_coq_micromega_formula tbl cl = binop_list tbl (fun x y -> Cj (x,y)) TT (List.map Form.neg cl) - -(* backported from Coq *) -type ('option,'a,'prf,'model) prover = { - name : string ; (* name of the prover *) - get_option : unit ->'option ; (* find the options of the prover *) - prover : ('option * 'a list) -> ('prf, 'model) Structures.Micromega_plugin_Certificate.res ; (* the prover itself *) - hyps : 'prf -> Structures.Micromega_plugin_Mutils.ISet.t ; (* extract the indexes of the hypotheses really used in the proof *) - compact : 'prf -> (int -> int) -> 'prf ; (* remap the hyp indexes according to function *) - pp_prf : out_channel -> 'prf -> unit ;(* pretting printing of proof *) - pp_f : out_channel -> 'a -> unit (* pretty printing of the formulas (polynomials)*) -} - -let lia_enum = ref true -let max_depth = max_int -let lia_proof_depth = ref max_depth -let get_lia_option () = - (!Structures.Micromega_plugin_Certificate.use_simplex,!lia_enum,!lia_proof_depth) - -let lift_pexpr_prover p l = p (List.map (fun (e,o) -> Structures.Micromega_plugin_Micromega.denorm e , o) l) - -module CacheZ = Structures.Micromega_plugin_Persistent_cache.PHashtable(struct - type prover_option = bool * bool* int - type t = prover_option * ((Structures.Micromega_plugin_Micromega.z Structures.Micromega_plugin_Micromega.pol * Structures.Micromega_plugin_Micromega.op1) list) - let equal = (=) - let hash = Hashtbl.hash -end) - -let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Structures.Micromega_plugin_Certificate.lia ce b) s) - -let xhyps_of_cone base acc prf = - let rec xtract e acc = - match e with - | Structures.Micromega_plugin_Micromega.PsatzC _ | Structures.Micromega_plugin_Micromega.PsatzZ | Structures.Micromega_plugin_Micromega.PsatzSquare _ -> acc - | Structures.Micromega_plugin_Micromega.PsatzIn n -> let n = (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n) in - if n >= base - then Structures.Micromega_plugin_Mutils.ISet.add (n-base) acc - else acc - | Structures.Micromega_plugin_Micromega.PsatzMulC(_,c) -> xtract c acc - | Structures.Micromega_plugin_Micromega.PsatzAdd(e1,e2) | Structures.Micromega_plugin_Micromega.PsatzMulE(e1,e2) -> xtract e1 (xtract e2 acc) in - - xtract prf acc - -let hyps_of_pt pt = - - let rec xhyps base pt acc = - match pt with - | Structures.Micromega_plugin_Micromega.DoneProof -> acc - | Structures.Micromega_plugin_Micromega.RatProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c) - | Structures.Micromega_plugin_Micromega.CutProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c) - | Structures.Micromega_plugin_Micromega.EnumProof(c1,c2,l) -> - let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in - List.fold_left (fun s x -> xhyps (base + 1) x s) s l in - - xhyps 0 pt Structures.Micromega_plugin_Mutils.ISet.empty - -let compact_cone prf f = - let np n = Structures.Micromega_plugin_Mutils.CamlToCoq.nat (f (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n)) in - - let rec xinterp prf = - match prf with - | Structures.Micromega_plugin_Micromega.PsatzC _ | Structures.Micromega_plugin_Micromega.PsatzZ | Structures.Micromega_plugin_Micromega.PsatzSquare _ -> prf - | Structures.Micromega_plugin_Micromega.PsatzIn n -> Structures.Micromega_plugin_Micromega.PsatzIn (np n) - | Structures.Micromega_plugin_Micromega.PsatzMulC(e,c) -> Structures.Micromega_plugin_Micromega.PsatzMulC(e,xinterp c) - | Structures.Micromega_plugin_Micromega.PsatzAdd(e1,e2) -> Structures.Micromega_plugin_Micromega.PsatzAdd(xinterp e1,xinterp e2) - | Structures.Micromega_plugin_Micromega.PsatzMulE(e1,e2) -> Structures.Micromega_plugin_Micromega.PsatzMulE(xinterp e1,xinterp e2) in - - xinterp prf - -let compact_pt pt f = - let translate ofset x = - if x < ofset then x - else (f (x-ofset) + ofset) in - - let rec compact_pt ofset pt = - match pt with - | Structures.Micromega_plugin_Micromega.DoneProof -> Structures.Micromega_plugin_Micromega.DoneProof - | Structures.Micromega_plugin_Micromega.RatProof(c,pt) -> Structures.Micromega_plugin_Micromega.RatProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt ) - | Structures.Micromega_plugin_Micromega.CutProof(c,pt) -> Structures.Micromega_plugin_Micromega.CutProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt ) - | Structures.Micromega_plugin_Micromega.EnumProof(c1,c2,l) -> Structures.Micromega_plugin_Micromega.EnumProof(compact_cone c1 (translate (ofset)), compact_cone c2 (translate (ofset)), - Structures.Micromega_plugin_Micromega.map (fun x -> compact_pt (ofset+1) x) l) in - compact_pt 0 pt - -let pp_nat o n = Printf.fprintf o "%i" (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n) - -let pp_positive o x = Printf.fprintf o "%i" (Structures.Micromega_plugin_Mutils.CoqToCaml.positive x) - -let pp_z o x = Printf.fprintf o "%s" (Big_int.string_of_big_int (Structures.Micromega_plugin_Mutils.CoqToCaml.z_big_int x)) - -let pp_list op cl elt o l = - let rec _pp o l = - match l with - | [] -> () - | [e] -> Printf.fprintf o "%a" elt e - | e::l -> Printf.fprintf o "%a ,%a" elt e _pp l in - Printf.fprintf o "%s%a%s" op _pp l cl - -let pp_pol pp_c o e = - let rec pp_pol o e = - match e with - | Structures.Micromega_plugin_Micromega.Pc n -> Printf.fprintf o "Pc %a" pp_c n - | Structures.Micromega_plugin_Micromega.Pinj(p,pol) -> Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol - | Structures.Micromega_plugin_Micromega.PX(pol1,p,pol2) -> Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 in - pp_pol o e - -let pp_psatz pp_z o e = - let rec pp_cone o e = - match e with - | Structures.Micromega_plugin_Micromega.PsatzIn n -> - Printf.fprintf o "(In %a)%%nat" pp_nat n - | Structures.Micromega_plugin_Micromega.PsatzMulC(e,c) -> - Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c - | Structures.Micromega_plugin_Micromega.PsatzSquare e -> - Printf.fprintf o "(%a^2)" (pp_pol pp_z) e - | Structures.Micromega_plugin_Micromega.PsatzAdd(e1,e2) -> - Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2 - | Structures.Micromega_plugin_Micromega.PsatzMulE(e1,e2) -> - Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2 - | Structures.Micromega_plugin_Micromega.PsatzC p -> - Printf.fprintf o "(%a)%%positive" pp_z p - | Structures.Micromega_plugin_Micromega.PsatzZ -> - Printf.fprintf o "0" in - pp_cone o e - -let rec pp_proof_term o = function - | Structures.Micromega_plugin_Micromega.DoneProof -> Printf.fprintf o "D" - | Structures.Micromega_plugin_Micromega.RatProof(cone,rst) -> Printf.fprintf o "R[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst - | Structures.Micromega_plugin_Micromega.CutProof(cone,rst) -> Printf.fprintf o "C[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst - | Structures.Micromega_plugin_Micromega.EnumProof(c1,c2,rst) -> - Printf.fprintf o "EP[%a,%a,%a]" - (pp_psatz pp_z) c1 (pp_psatz pp_z) c2 - (pp_list "[" "]" pp_proof_term) rst - -let linear_Z = { - name = "lia"; - get_option = get_lia_option; - prover = memo_zlinear_prover ; - hyps = hyps_of_pt; - compact = compact_pt; - pp_prf = pp_proof_term; - pp_f = fun o x -> pp_pol pp_z o (fst x) -} - -let find_witness p polys1 = - let polys1 = List.map fst polys1 in - match p.prover (p.get_option (), polys1) with - | Structures.Micromega_plugin_Certificate.Model m -> Structures.Micromega_plugin_Certificate.Model m - | Structures.Micromega_plugin_Certificate.Unknown -> Structures.Micromega_plugin_Certificate.Unknown - | Structures.Micromega_plugin_Certificate.Prf prf -> Structures.Micromega_plugin_Certificate.Prf(prf,p) - -let witness_list prover l = +let tauto_lia ff = + let cnf_ff,_ = Structures.Micromega_plugin_Micromega.cnfZ ff in let rec xwitness_list l = match l with - | [] -> Structures.Micromega_plugin_Certificate.Prf [] + | [] -> Some [] | e :: l -> match xwitness_list l with - | Structures.Micromega_plugin_Certificate.Model (m,e) -> Structures.Micromega_plugin_Certificate.Model (m,e) - | Structures.Micromega_plugin_Certificate.Unknown -> Structures.Micromega_plugin_Certificate.Unknown - | Structures.Micromega_plugin_Certificate.Prf l -> - match find_witness prover e with - | Structures.Micromega_plugin_Certificate.Model m -> Structures.Micromega_plugin_Certificate.Model (m,e) - | Structures.Micromega_plugin_Certificate.Unknown -> Structures.Micromega_plugin_Certificate.Unknown - | Structures.Micromega_plugin_Certificate.Prf w -> Structures.Micromega_plugin_Certificate.Prf (w::l) in - xwitness_list l - -let witness_list_tags = witness_list - -let tauto_lia ff = - let prover = linear_Z in - let cnf_ff,_ = Structures.Micromega_plugin_Micromega.cnfZ ff in - match witness_list_tags prover cnf_ff with - | Structures.Micromega_plugin_Certificate.Prf l -> Some (List.map fst l) - | _ -> None + | None -> None + | Some l -> + match Structures.Micromega_plugin_Certificate.lia true max_int (List.map (fun ((e, o), _) -> Structures.Micromega_plugin_Micromega.denorm e, o) e) with + | Structures.Micromega_plugin_Certificate.Prf w -> Some (w::l) + | _ -> None in + xwitness_list cnf_ff (* call to micromega solver *) let build_lia_certif cl = diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml index 0738801..435a1a1 100644 --- a/src/versions/native/structures.ml +++ b/src/versions/native/structures.ml @@ -140,9 +140,7 @@ let mkTrace step_to_coq next carray _ _ _ _ size step def_step r = (* Micromega *) module Micromega_plugin_Micromega = Micromega -module Micromega_plugin_Mutils = Mutils module Micromega_plugin_Certificate = Certificate -module Micromega_plugin_Coq_micromega = Coq_micromega let micromega_coq_proofTerm = Coq_micromega.M.coq_proofTerm diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli index d8071d9..f2775a6 100644 --- a/src/versions/native/structures.mli +++ b/src/versions/native/structures.mli @@ -82,9 +82,7 @@ val mkTrace : (* Micromega *) module Micromega_plugin_Micromega = Micromega -module Micromega_plugin_Mutils = Mutils module Micromega_plugin_Certificate = Certificate -module Micromega_plugin_Coq_micromega = Coq_micromega val micromega_coq_proofTerm : constr lazy_t val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index 9d54b11..863c921 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -170,10 +170,7 @@ let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r = (* Micromega *) module Micromega_plugin_Micromega = Micromega_plugin.Micromega -module Micromega_plugin_Mutils = Micromega_plugin.Mutils module Micromega_plugin_Certificate = Micromega_plugin.Certificate -module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega -module Micromega_plugin_Persistent_cache = Micromega_plugin.Persistent_cache let micromega_coq_proofTerm = (* Cannot contain evars *) @@ -181,7 +178,7 @@ let micromega_coq_proofTerm = let micromega_dump_proof_term p = (* Cannot contain evars *) - EConstr.Unsafe.to_constr (Micromega_plugin_Coq_micromega.dump_proof_term p) + EConstr.Unsafe.to_constr (Micromega_plugin.Coq_micromega.dump_proof_term p) (* Tactics *) diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli index e21a26f..104f3f9 100644 --- a/src/versions/standard/structures.mli +++ b/src/versions/standard/structures.mli @@ -90,10 +90,7 @@ val mkTrace : (* Micromega *) module Micromega_plugin_Micromega = Micromega_plugin.Micromega -module Micromega_plugin_Mutils = Micromega_plugin.Mutils module Micromega_plugin_Certificate = Micromega_plugin.Certificate -module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega -module Micromega_plugin_Persistent_cache = Micromega_plugin.Persistent_cache val micromega_coq_proofTerm : constr lazy_t val micromega_dump_proof_term : Micromega_plugin_Micromega.zArithProof -> constr -- cgit