Merge PR #8691: Remove some dead code in nsatz and micromega plugins

12 files changed, 7 insertions, 262 deletions

diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index e6edd50878..af292c088f 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -514,7 +514,6 @@ let rec scale_term t =
   | Zero    -> unit_big_int , Zero
   | Const n ->  (denominator n) , Const (Big_int (numerator n))
   | Var n   -> unit_big_int , Var n
-  | Inv _   -> failwith "scale_term : not implemented"
   | Opp t   -> let s, t = scale_term t in s, Opp t
   | Add(t1,t2) -> let s1,y1 = scale_term t1 and s2,y2 = scale_term t2 in
                   let g = gcd_big_int s1 s2 in
@@ -530,7 +529,6 @@ let rec scale_term t =
                       mult_big_int s1 s2 , Mul (y1, y2)
   |  Pow(t,n) -> let s,t = scale_term t in
                  power_big_int_positive_int s  n , Pow(t,n)
-  |   _ -> failwith "scale_term : not implemented"
 
 let scale_term t =
   let (s,t') = scale_term t in
@@ -572,7 +570,6 @@ let rec term_to_q_expr = function
   | Opp p ->   PEopp (term_to_q_expr p)
   | Pow(t,n) ->  PEpow (term_to_q_expr t,Ml2C.n n)
   | Sub(t1,t2) ->  PEsub (term_to_q_expr t1,  term_to_q_expr t2)
-  | _ -> failwith "term_to_q_expr: not implemented"
 
 let term_to_q_pol e = Mc.norm_aux (Ml2C.q (Int 0)) (Ml2C.q (Int 1)) Mc.qplus  Mc.qmult Mc.qminus Mc.qopp Mc.qeq_bool (term_to_q_expr e)
 
@@ -610,7 +607,6 @@ let rec term_to_z_expr = function
   | Opp p ->   PEopp (term_to_z_expr p)
   | Pow(t,n) ->  PEpow (term_to_z_expr t,Ml2C.n n)
   | Sub(t1,t2) ->  PEsub (term_to_z_expr t1,  term_to_z_expr t2)
-  | _ -> failwith "term_to_z_expr: not implemented"
 
 let term_to_z_pol e = Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.Z.add  Mc.Z.mul Mc.Z.sub Mc.Z.opp Mc.zeq_bool (term_to_z_expr e)
 
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 40aeef3959..809731ecc4 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -31,20 +31,12 @@ module IMap =
       r
   end
 
-(*let output_int o i = output_string o (string_of_int i)*)
-
-let iset_pp o s =
-  Printf.fprintf o "{ %a }"
-    (fun o s ->  ISet.iter (fun i -> Printf.fprintf o "%i " i) s) s
-
 let rec pp_list s f o l =
   match l with
     | [] -> ()
     | [e] -> f o e
     | e::l -> f o e ; output_string o s ; pp_list s f o l
 
-let output_bigint o bi = output_string o (Big_int.string_of_big_int bi)
-
 let finally f rst =
   try
     let res = f () in
@@ -61,16 +53,7 @@ let rec try_any l x =
      | None -> try_any l x
      | x -> x
 
-let all_sym_pairs f l = 
-  let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in
-
-  let rec xpairs acc l = 
-    match l with
-      | [] -> acc
-      | e::l -> xpairs (pair_with acc e l) l in
-    xpairs [] l
-
-let all_pairs f l = 
+let all_pairs f l =
   let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in
 
   let rec xpairs acc l = 
@@ -123,26 +106,6 @@ let numerator = function
  | Int i -> Big_int.big_int_of_int i
  | Big_int i -> i
 
-let rec ppcm_list c l =
- match l with
-  | [] -> c
-  | e::l -> ppcm_list (ppcm c (denominator e)) l
-
-let rec rec_gcd_list c l  =
- match l with
-  | [] -> c
-  | e::l -> rec_gcd_list (gcd_big_int  c (numerator e)) l
-
-let gcd_list l =
- let res = rec_gcd_list zero_big_int l in
-  if Int.equal (compare_big_int res zero_big_int) 0
-  then unit_big_int else res
-
-let rats_to_ints l =
- let c = ppcm_list unit_big_int l in
-  List.map (fun x ->  (div_big_int (mult_big_int (numerator x) c)
-			(denominator x))) l
-
 let iterate_until_stable f x =
  let rec iter x =
   match f x with
diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli
index 35ca1e5516..e92f086886 100644
--- a/plugins/micromega/mutils.mli
+++ b/plugins/micromega/mutils.mli
@@ -20,10 +20,6 @@ sig
 
 end
 
-val iset_pp : out_channel -> ISet.t -> unit
-
-val output_bigint : out_channel -> Big_int.big_int -> unit
-
 val numerator : Num.num -> Big_int.big_int
 val denominator : Num.num -> Big_int.big_int
 
@@ -73,15 +69,11 @@ module CoqToCaml : sig
 end
 
 val ppcm : Big_int.big_int -> Big_int.big_int -> Big_int.big_int
-val rats_to_ints : Num.num list -> Big_int.big_int list
 
 val all_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list
-val all_sym_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list
 val try_any : (('a -> 'b option) * 'c) list -> 'a -> 'b option
 val is_sublist : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
 
-val gcd_list : Num.num list -> Big_int.big_int
-
 val extract : ('a -> 'b option) -> 'a list -> ('b * 'a) option * 'a list
 
 val extract_all : ('a -> 'b option) -> 'a list -> ('b * 'a) list * 'a list
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index ee5a0458e8..0209030b64 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -19,11 +19,6 @@ module type PHashtable =
     type 'a t
     type key
 
-    val create : int -> string -> 'a t
-    (** [create i f] creates an empty persistent table
-	with initial size i associated with file [f] *)
-
-
     val open_in : string -> 'a t
     (** [open_in f] rebuilds a table from the records stored in file [f].
 	As marshaling is not type-safe, it migth segault.
@@ -37,11 +32,6 @@ module type PHashtable =
 	(and writes the binding to the file associated with [tbl].)
 	If [key] is already bound, raises KeyAlreadyBound *)
 
-    val close : 'a t -> unit
-    (** [close tbl] is closing the table.
-	Once closed, a table cannot be used.
-	i.e, find,add will raise UnboundTable *)
-
     val memo : string -> (key -> 'a) -> (key -> 'a)
       (** [memo cache f] returns a memo function for [f] using file [cache] as persistent table.
 	  Note that the cache will only be loaded when the function is used for the first time *)
@@ -71,14 +61,6 @@ struct
       }
 
 
-let create i f =
-  let flags = [O_WRONLY; O_TRUNC;O_CREAT] in
-  {
-    outch = out_channel_of_descr (openfile f flags 0o666);
-    status = Open ;
-    htbl = Table.create i
-  }
-
 let finally f rst =
   try
     let res = f () in
@@ -181,15 +163,6 @@ let open_in f =
      end
 
 
-let close t =
-  let {outch = outch ; status = status ; htbl = tbl} = t in
-    match t.status with
-    | Closed -> () (* don't do it twice *)
-    | Open  ->
-	close_out outch ;
-	Table.clear tbl ;
-	t.status <- Closed
-
 let add t k e =
   let {outch = outch ; status = status ; htbl = tbl} = t in
     if status == Closed
diff --git a/plugins/micromega/persistent_cache.mli b/plugins/micromega/persistent_cache.mli
index 240fa490fc..4e7a388aaf 100644
--- a/plugins/micromega/persistent_cache.mli
+++ b/plugins/micromega/persistent_cache.mli
@@ -15,11 +15,6 @@ module type PHashtable =
     type 'a t
     type key
 
-    val create : int -> string -> 'a t
-    (** [create i f] creates an empty persistent table
-        with initial size i associated with file [f] *)
-
-
     val open_in : string -> 'a t
     (** [open_in f] rebuilds a table from the records stored in file [f].
         As marshaling is not type-safe, it migth segault.
@@ -33,11 +28,6 @@ module type PHashtable =
         (and writes the binding to the file associated with [tbl].)
         If [key] is already bound, raises KeyAlreadyBound *)
 
-    val close : 'a t -> unit
-    (** [close tbl] is closing the table.
-        Once closed, a table cannot be used.
-        i.e, find,add will raise UnboundTable *)
-
     val memo : string -> (key -> 'a) -> (key -> 'a)
       (** [memo cache f] returns a memo function for [f] using file [cache] as persistent table.
           Note that the cache will only be loaded when the function is used for the first time *)
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index 5f31b6f145..76e7769e82 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -193,8 +193,6 @@ sig
   val addition : t -> t -> t
   val uminus : t -> t
   val fold : (Monomial.t -> num -> 'a -> 'a) -> t -> 'a -> 'a
-  val is_linear : t -> bool
-  val variables : t -> ISet.t
   val factorise : var -> t  -> t * t
 end =  struct
   (*normalisation bug : 0*x ... *)
@@ -259,10 +257,6 @@ end =  struct
 
   let fold = P.fold
 
-  let is_linear p = P.fold (fun m _ acc -> acc && (Monomial.is_const m || Monomial.is_var m)) p true
-
-  let variables p = P.fold (fun m _ acc -> ISet.union (Monomial.variables m) acc) p ISet.empty
-
   let factorise x p =
     let x = Monomial.var x in
     P.fold (fun m v (px,cx) ->
@@ -294,7 +288,7 @@ let eval_op = function
 
 let string_of_op = function Eq -> "=" | Ge -> ">=" | Gt -> ">"
 
-let output_cstr o {coeffs = coeffs ; op = op ; cst = cst} =
+let output_cstr o { coeffs ; op ; cst } =
   Printf.fprintf o "%a %s %s" Vect.pp coeffs (string_of_op op) (string_of_num cst)
 
 
@@ -466,12 +460,6 @@ module LinPoly = struct
 
 end
 
-let output_nlin_cstr o {coeffs = coeffs ; op = op ; cst = cst} =
-  let p = LinPoly.pol_of_linpol coeffs in
-
-  Printf.fprintf o "%a %s %s" Poly.pp p (string_of_op op) (string_of_num cst)
-
-
 module ProofFormat =  struct
   open Big_int
 
diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli
index 6f26f7a959..f5e9a9f34c 100644
--- a/plugins/micromega/polynomial.mli
+++ b/plugins/micromega/polynomial.mli
@@ -97,20 +97,10 @@ module Poly : sig
   (** [fold f p a] folds f over the monomials of p with non-zero coefficient *)
   val fold : (Monomial.t -> Num.num -> 'a -> 'a) -> t -> 'a -> 'a
 
-  (** [is_linear p]
-      @return true if the polynomial is of the form a1.x1 +...+ an.xn + c
-      i.e every monomial is made of at most a variable *)
-  val is_linear : t -> bool
-
-
   (** [add m n p]
       @return the polynomial n*m + p *)
   val add : Monomial.t -> Num.num -> t -> t
 
-  (** [variables p]
-      @return the set of variables of the polynomial p *)
-  val variables : t -> ISet.t
-
 end
 
 type cstr = {coeffs : Vect.t ; op : op ; cst : Num.num} (** Representation of linear constraints *)
@@ -286,8 +276,6 @@ end
 
 val output_cstr : out_channel -> cstr -> unit
 
-val output_nlin_cstr : out_channel -> cstr -> unit
-
 val opMult : op -> op -> op
 
 (** [module WithProof] constructs polynomials packed with the proof that their sign is correct. *)
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index 42a41e176c..f2dfaa42a5 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -145,11 +145,6 @@ let diagonal (v:vector) =
 (* ------------------------------------------------------------------------- *)
 (* Monomials.                                                                *)
 (* ------------------------------------------------------------------------- *)
-
-let monomial_eval assig (m:monomial) =
-  foldl (fun a x k -> a */ power_num (apply assig x) (Int k))
-        (Int 1) m;;
-
 let monomial_1 = (undefined:monomial);;
 
 let monomial_var x = (x |=> 1 :monomial);;
@@ -166,10 +161,6 @@ let monomial_variables m = dom m;;
 (* ------------------------------------------------------------------------- *)
 (* Polynomials.                                                              *)
 (* ------------------------------------------------------------------------- *)
-
-let eval assig (p:poly) =
-  foldl (fun a m c -> a +/ c */ monomial_eval assig m) (Int 0) p;;
-
 let poly_0 = (undefined:poly);;
 
 let poly_isconst (p:poly) = foldl (fun a m c -> m = monomial_1 && a) true p;;
@@ -289,17 +280,9 @@ let rec poly_of_term t = match t with
 | Const n -> poly_const n
 | Var x -> poly_var x
 | Opp t1 -> poly_neg (poly_of_term t1)
-| Inv t1 ->
-      let p = poly_of_term t1 in
-      if poly_isconst p then poly_const(Int 1 // eval undefined p)
-      else failwith "poly_of_term: inverse of non-constant polyomial"
 | Add (l, r) -> poly_add (poly_of_term l) (poly_of_term r)
 | Sub (l, r) -> poly_sub (poly_of_term l) (poly_of_term r)
 | Mul (l, r) -> poly_mul (poly_of_term l) (poly_of_term r)
-| Div (l, r) ->
-      let p = poly_of_term l and q = poly_of_term r in
-      if poly_isconst q then poly_cmul (Int 1 // eval undefined q) p
-      else failwith "poly_of_term: division by non-constant polynomial"
 | Pow (t, n) ->
       poly_pow (poly_of_term t) n;;
 
diff --git a/plugins/micromega/sos_types.ml b/plugins/micromega/sos_types.ml
index dde1e6c0b0..79d67b6ae9 100644
--- a/plugins/micromega/sos_types.ml
+++ b/plugins/micromega/sos_types.ml
@@ -11,19 +11,17 @@
 (* The type of positivstellensatz -- used to communicate with sos *)
 open Num
 
-type vname = string;;
+type vname = string
 
 type term =
 | Zero
 | Const of Num.num
 | Var of vname
-| Inv of term
 | Opp of term
 | Add of (term * term)
 | Sub of (term * term)
 | Mul of (term * term)
-| Div of (term * term)
-| Pow of (term * int);;
+| Pow of (term * int)
 
 
 let rec output_term o t =
@@ -31,12 +29,10 @@ let rec output_term o t =
     | Zero -> output_string o "0"
     | Const n -> output_string o (string_of_num n)
     | Var n   -> Printf.fprintf o "v%s" n
-    | Inv t   -> Printf.fprintf o "1/(%a)" output_term t
     | Opp t    -> Printf.fprintf o "- (%a)" output_term t
     | Add(t1,t2) -> Printf.fprintf o "(%a)+(%a)" output_term t1 output_term t2
     | Sub(t1,t2) -> Printf.fprintf o "(%a)-(%a)" output_term t1 output_term t2
     | Mul(t1,t2) -> Printf.fprintf o "(%a)*(%a)" output_term t1 output_term t2
-    | Div(t1,t2) -> Printf.fprintf o "(%a)/(%a)" output_term t1 output_term t2
     | Pow(t1,i) -> Printf.fprintf o "(%a)^(%i)" output_term t1 i
 (* ------------------------------------------------------------------------- *)
 (* Data structure for Positivstellensatz refutations.                        *)
diff --git a/plugins/micromega/sos_types.mli b/plugins/micromega/sos_types.mli
index 050ff1e4f7..aa5fb08489 100644
--- a/plugins/micromega/sos_types.mli
+++ b/plugins/micromega/sos_types.mli
@@ -10,19 +10,17 @@
 
 (* The type of positivstellensatz -- used to communicate with sos *)
 
-type vname = string;;
+type vname = string
 
 type term =
 | Zero
 | Const of Num.num
 | Var of vname
-| Inv of term
 | Opp of term
 | Add of (term * term)
 | Sub of (term * term)
 | Mul of (term * term)
-| Div of (term * term)
-| Pow of (term * int);;
+| Pow of (term * int)
 
 val output_term : out_channel -> term -> unit
 
@@ -37,6 +35,6 @@ type positivstellensatz =
  | Monoid of int list
  | Eqmul of term * positivstellensatz
  | Sum of positivstellensatz * positivstellensatz
- | Product of positivstellensatz * positivstellensatz;;
+ | Product of positivstellensatz * positivstellensatz
 
 val output_psatz : out_channel -> positivstellensatz -> unit
diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml
index d3cfd75e56..1caa042db6 100644
--- a/plugins/nsatz/utile.ml
+++ b/plugins/nsatz/utile.ml
@@ -3,116 +3,7 @@
 let pr x =
   if !Flags.debug then (Format.printf "@[%s@]" x; flush(stdout);)else ()
 
-let prn x =
-  if !Flags.debug then (Format.printf "@[%s\n@]" x; flush(stdout);) else ()
-
 let prt0 s = () (* print_string s;flush(stdout)*)
 
-let prt s =
-  if !Flags.debug then (print_string (s^"\n");flush(stdout)) else ()
-
 let sinfo s = if !Flags.debug then Feedback.msg_debug (Pp.str s)
 let info s = if !Flags.debug then Feedback.msg_debug (Pp.str (s ()))
-
-(* Lists *)
-
-let rec list_mem_eq eq x l =
-  match l with
-    [] -> false
-   |y::l1 -> if (eq x y) then true else (list_mem_eq eq x l1)
-
-let set_of_list_eq eq l =
-   let res = ref [] in
-   List.iter (fun x -> if not (list_mem_eq eq x (!res)) then res:=x::(!res)) l;
-   List.rev !res
-
-(**********************************************************************
-  Eléments minimaux pour un ordre partiel de division.
-  E est un ensemble, avec une multiplication
-  et une division partielle div (la fonction div peut échouer),
-  constant est un prédicat qui définit un sous-ensemble C de E.
-*)
-(*
-  Etant donnée une partie A de E, on calcule une partie B de E disjointe de C
-  telle que:
-    - les éléments de A sont des produits d'éléments de B et d'un de C.
-    - B est minimale pour cette propriété.
-*)
-
-let facteurs_liste div constant lp =
-   let lp = List.filter (fun x -> not (constant x)) lp in
-   let rec factor lmin lp = (* lmin: ne se divisent pas entre eux *)
-      match lp with
-        [] -> lmin
-       |p::lp1 ->
-         (let l1 = ref [] in
-          let p_dans_lmin = ref false in
-          List.iter (fun q -> try (let r = div p q in
-                                   if not (constant r)
-				   then l1:=r::(!l1)
-                                   else p_dans_lmin:=true)
-			      with e when CErrors.noncritical e -> ())
-                     lmin;
-          if !p_dans_lmin
-          then factor lmin lp1
-          else if (!l1)=[]
-          (* aucun q de lmin ne divise p *)
-          then (let l1=ref lp1 in
-		let lmin1=ref [] in
-                List.iter (fun q -> try (let r = div q p in
-					 if not (constant r)
-					 then l1:=r::(!l1))
-				    with e when CErrors.noncritical e ->
-                                      lmin1:=q::(!lmin1))
-                          lmin;
-	        factor (List.rev (p::(!lmin1))) !l1)
-          (* au moins un q de lmin divise p non trivialement *)
-          else factor lmin ((!l1)@lp1))
-    in
-    factor [] lp
-
-
-(* On suppose que tout élément de A est produit d'éléments de B et d'un de C:
-   A et B sont deux tableaux,  rend un tableau de couples
-      (élément de C, listes d'indices l)
-   tels que A.(i) = l.(i)_1*Produit(B.(j), j dans l.(i)_2)
-   zero est un prédicat sur E tel que (zero x) => (constant x):
-         si (zero x) est vrai on ne decompose pas x
-   c est un élément quelconque de E.
-*)
-let factorise_tableau div zero c f l1 =
-    let res = Array.make (Array.length f) (c,[]) in
-    Array.iteri (fun i p ->
-      let r = ref p in
-      let li = ref [] in
-      if not (zero p)
-      then
-      Array.iteri (fun j q ->
-	              try (while true do
-                               let rr = div !r q in
-      	                       li:=j::(!li);
-                               r:=rr;
-			   done)
-                      with e when CErrors.noncritical e -> ())
-                  l1;
-      res.(i)<-(!r,!li))
-     f;
-    (l1,res)
-
-
-(* exemples:
-
-let l =  [1;2;6;24;720]
-and div1 = (fun a b -> if a mod b =0 then a/b else failwith "div")
-and constant = (fun x -> x<2)
-and zero = (fun x -> x=0)
-
-
-let f = facteurs_liste div1 constant l
-
-
-factorise_tableau div1 zero 0 (Array.of_list l) (Array.of_list f)
-
-*)
-
-
diff --git a/plugins/nsatz/utile.mli b/plugins/nsatz/utile.mli
index 9308577e0f..5af7ece5a3 100644
--- a/plugins/nsatz/utile.mli
+++ b/plugins/nsatz/utile.mli
@@ -1,19 +1,6 @@
 
 (* Printing *)
 val pr : string -> unit
-val prn : string -> unit
 val prt0 : 'a -> unit
-val prt : string -> unit
 val info : (unit -> string) -> unit
 val sinfo : string -> unit
-
-(* Listes *)
-val list_mem_eq : ('a -> 'b -> bool) -> 'a -> 'b list -> bool
-val set_of_list_eq : ('a -> 'a -> bool) -> 'a list -> 'a list
-
-
-val facteurs_liste : ('a -> 'a -> 'a) -> ('a -> bool) -> 'a list -> 'a list
-val factorise_tableau :
-  ('a -> 'b -> 'a) ->
-  ('a -> bool) ->
-  'a -> 'a array -> 'b array -> 'b array * ('a * int list) array