Get rid of most of our copy of micromega's source code (#94)

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