Merge PR #8743: [micromega] Switch from `Big_int` to ZArith.

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: fajb
Ack-by: liyishuai
Ack-by: maximedenes
Ack-by: ppedrot
Ack-by: soraros
Ack-by: thery
Ack-by: vbgl

19 files changed, 110 insertions, 102 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index cfa6f84147..22658cc9b8 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -19,7 +19,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2020-09-07-V22"
+  CACHEKEY: "bionic_coq-V2020-09-16-V38"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/.merlin.in b/.merlin.in
index fa3473765d..80b0b600eb 100644
--- a/.merlin.in
+++ b/.merlin.in
@@ -54,3 +54,4 @@ S plugins/**
 B plugins/**
 
 PKG threads.posix
+PKG zarith
\ No newline at end of file
diff --git a/INSTALL.md b/INSTALL.md
index 05a92ca005..adc0f557ac 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -18,7 +18,7 @@ To compile Coq yourself, you need:
 - The [num](https://github.com/ocaml/num) library; note that it is
   included in the OCaml distribution for OCaml versions < 4.06.0
 
-- The [ZArith library](https://github.com/ocaml/Zarith) >= 1.8
+- The [ZArith library](https://github.com/ocaml/Zarith) >= 1.10
 
 - The [findlib](http://projects.camlcity.org/projects/findlib.html) library (version >= 1.8.0)
 
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 17228bda8a..be9e774381 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -80,7 +80,7 @@ jobs:
       opam switch set ocaml-base-compiler.$COMPILER
       eval $(opam env)
       opam update
-      opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.9.1
+      opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.10
       opam list
     displayName: 'Install OCaml dependencies'
     env:
diff --git a/coq.opam b/coq.opam
index f44223052d..342adee1f4 100644
--- a/coq.opam
+++ b/coq.opam
@@ -25,7 +25,7 @@ depends: [
   "dune"      { >= "2.5.0"  }
   "ocamlfind" { build }
   "num"
-  "zarith"    { >= "1.9.1" }
+  "zarith"    { >= "1.10" }
 ]
 
 build: [
diff --git a/coq.opam.docker b/coq.opam.docker
index ac1869f344..09065fdffd 100644
--- a/coq.opam.docker
+++ b/coq.opam.docker
@@ -24,7 +24,7 @@ depends: [
   "ocaml"     { >= "4.05.0" }
   "ocamlfind" { build }
   "num"
-  "zarith"    { >= "1.9.1" }
+  "zarith"    { >= "1.10" }
   "conf-findutils" {build}
 ]
 
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index cde1d798a0..fcc585117b 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1026,7 +1026,7 @@ function make_num {
 
 function make_zarith {
   make_ocaml
-  if build_prep https://github.com/ocaml/Zarith/archive release-1.9.1 tar.gz 1 zarith-1.9.1; then
+  if build_prep https://github.com/ocaml/Zarith/archive release-1.10 tar.gz 1 zarith-1.10; then
     logn configure ./configure
     log1 make
     log2 make install
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index ee50d25318..2fcd69e130 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-09-07-V22"
+# CACHEKEY: "bionic_coq-V2020-09-16-V38"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -43,7 +43,7 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages, num to be removed once the migration to
 # micromega is complete, `num` also does not have a version number as
 # the right version to install varies with the compiler version.
-ENV BASE_OPAM="num zarith.1.9.1 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \
+ENV BASE_OPAM="num zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
     BASE_ONLY_OPAM="elpi.1.11.0"
 
@@ -59,7 +59,7 @@ RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opa
 
 # base+32bit switch, note the zarith hack
 RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
-        i386 env CC='gcc -m32' opam install zarith.1.9.1 && \
+        i386 env CC='gcc -m32' opam install zarith.1.10 && \
         opam install $BASE_OPAM
 
 # EDGE switch
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 148c1772bf..9008691bca 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -354,7 +354,7 @@ let is_linear_for v pc =
  *)
 
 let is_linear_substitution sys ((p, o), prf) =
-  let pred v = v =/ Q.one || v =/ Q.neg_one in
+  let pred v = v =/ Q.one || v =/ Q.minus_one in
   match o with
   | Eq -> (
     match
@@ -761,7 +761,7 @@ let reduce_unary psys =
   let is_unary_equation (cstr, prf) =
     if cstr.op == Eq then
       Vect.find
-        (fun v n -> if n =/ Q.one || n =/ Q.neg_one then Some v else None)
+        (fun v n -> if n =/ Q.one || n =/ Q.minus_one then Some v else None)
         cstr.coeffs
     else None
   in
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 44bc20e55f..d2c49c4432 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -2141,6 +2141,7 @@ let really_call_csdpcert :
     List.fold_left Filename.concat (Envars.coqlib ())
       ["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension]
   in
+  let cmdname = if Sys.file_exists cmdname then cmdname else "csdpcert" in
   match (command cmdname [|cmdname|] (provername, poly) : csdp_certificate) with
   | F str ->
     if debug then Printf.fprintf stdout "really_call_csdpcert : %s\n" str;
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index 3d1770a541..f4d17b8940 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -190,6 +190,7 @@ let system_list sys =
 
 let add (v1, c1) (v2, c2) =
   assert (c1 <>/ Q.zero && c2 <>/ Q.zero);
+  (* XXX Can use Q.inv now *)
   let res = mul_add (Q.one // c1) v1 (Q.one // c2) v2 in
   (res, count res)
 
@@ -569,7 +570,7 @@ module Fourier = struct
     (* We add a dummy (fresh) variable for vector *)
     let fresh = List.fold_left (fun fr c -> max fr (Vect.fresh c.coeffs)) 0 l in
     let cstr =
-      {coeffs = Vect.set fresh Q.neg_one vect; op = Eq; cst = Q.zero}
+      {coeffs = Vect.set fresh Q.minus_one vect; op = Eq; cst = Q.zero}
     in
     match solve fresh choose_equality_var choose_variable (cstr :: l) with
     | Inr prf -> None (* This is an unsatisfiability proof *)
diff --git a/plugins/micromega/numCompat.ml b/plugins/micromega/numCompat.ml
index 4cb91ea520..02c4bab497 100644
--- a/plugins/micromega/numCompat.ml
+++ b/plugins/micromega/numCompat.ml
@@ -31,37 +31,24 @@ module type ZArith = sig
 end
 
 module Z = struct
-  type t = Big_int.big_int
-
-  open Big_int
-
-  let zero = zero_big_int
-  let one = unit_big_int
-  let two = big_int_of_int 2
-  let add = Big_int.add_big_int
-  let sub = Big_int.sub_big_int
-  let mul = Big_int.mult_big_int
-  let div = Big_int.div_big_int
-  let neg = Big_int.minus_big_int
-  let sign = Big_int.sign_big_int
-  let equal = eq_big_int
-  let compare = compare_big_int
-  let power_int = power_big_int_positive_int
-  let quomod = quomod_big_int
+  (* Beware this only works fine in ZArith >= 1.10 due to
+     https://github.com/ocaml/Zarith/issues/58 *)
+  include Z
 
-  let ppcm x y =
-    let g = gcd_big_int x y in
-    let x' = div_big_int x g in
-    let y' = div_big_int y g in
-    mult_big_int g (mult_big_int x' y')
-
-  let gcd = gcd_big_int
+  (* Constants *)
+  let two = Z.of_int 2
+  let ten = Z.of_int 10
+  let power_int = Big_int_Z.power_big_int_positive_int
+  let quomod = Big_int_Z.quomod_big_int
 
-  let lcm x y =
-    if eq_big_int x zero && eq_big_int y zero then zero
-    else abs_big_int (div_big_int (mult_big_int x y) (gcd x y))
+  (* zarith fails with division by zero if x == 0 && y == 0 *)
+  let lcm x y = if Z.equal x zero && Z.equal y zero then zero else Z.lcm x y
 
-  let to_string = string_of_big_int
+  let ppcm x y =
+    let g = gcd x y in
+    let x' = Z.div x g in
+    let y' = Z.div y g in
+    Z.mul g (Z.mul x' y')
 end
 
 module type QArith = sig
@@ -74,7 +61,7 @@ module type QArith = sig
   val one : t
   val two : t
   val ten : t
-  val neg_one : t
+  val minus_one : t
 
   module Notations : sig
     val ( // ) : t -> t -> t
@@ -119,56 +106,64 @@ end
 module Q : QArith with module Z = Z = struct
   module Z = Z
 
-  type t = Num.num
+  let pow_check_exp x y =
+    let z_res =
+      if y = 0 then Z.one
+      else if y > 0 then Z.pow x y
+      else (* s < 0 *)
+        Z.pow x (abs y)
+    in
+    let z_res = Q.of_bigint z_res in
+    if 0 <= y then z_res else Q.inv z_res
 
-  open Num
+  include Q
 
-  let of_int x = Int x
-  let zero = Int 0
-  let one = Int 1
-  let two = Int 2
-  let ten = Int 10
-  let neg_one = Int (-1)
+  let two = Q.(of_int 2)
+  let ten = Q.(of_int 10)
 
   module Notations = struct
-    let ( // ) = div_num
-    let ( +/ ) = add_num
-    let ( -/ ) = sub_num
-    let ( */ ) = mult_num
-    let ( =/ ) = eq_num
-    let ( <>/ ) = ( <>/ )
-    let ( >/ ) = ( >/ )
-    let ( >=/ ) = ( >=/ )
-    let ( </ ) = ( </ )
-    let ( <=/ ) = ( <=/ )
+    let ( // ) = Q.div
+    let ( +/ ) = Q.add
+    let ( -/ ) = Q.sub
+    let ( */ ) = Q.mul
+    let ( =/ ) = Q.equal
+    let ( <>/ ) x y = not (Q.equal x y)
+    let ( >/ ) = Q.gt
+    let ( >=/ ) = Q.geq
+    let ( </ ) = Q.lt
+    let ( <=/ ) = Q.leq
   end
 
-  let compare = compare_num
-  let make x y = Big_int x // Big_int y
-
-  let numdom r =
-    let r' = Ratio.normalize_ratio (ratio_of_num r) in
-    (Ratio.numerator_ratio r', Ratio.denominator_ratio r')
-
-  let num x = numdom x |> fst
-  let den x = numdom x |> snd
-  let of_bigint x = Big_int x
-  let to_bigint = big_int_of_num
-  let neg = minus_num
-
-  (* let inv =  *)
-  let max = max_num
-  let min = min_num
-  let sign = sign_num
-  let abs = abs_num
-  let mod_ = mod_num
-  let floor = floor_num
-  let ceiling = ceiling_num
-  let round = round_num
-  let pow2 n = power_num two (Int n)
-  let pow10 n = power_num ten (Int n)
-  let power x = power_num (Int x)
-  let to_string = string_of_num
-  let of_string = num_of_string
-  let to_float = float_of_num
+  (* XXX: review / improve *)
+  let floorZ q : Z.t = Z.fdiv (num q) (den q)
+  let floor q : t = floorZ q |> Q.of_bigint
+  let ceiling q : t = Z.cdiv (Q.num q) (Q.den q) |> Q.of_bigint
+  let half = Q.make Z.one Z.two
+
+  (* We imitate Num's round which is to the nearest *)
+  let round q = floor (Q.add half q)
+
+  (* XXX: review / improve *)
+  let quo x y =
+    let s = sign y in
+    let res = floor (x / abs y) in
+    if Int.equal s (-1) then neg res else res
+
+  let mod_ x y = x - (y * quo x y)
+
+  (* XXX: review / improve *)
+  (* Note that Z.pow doesn't support negative exponents *)
+
+  let pow2 y = pow_check_exp Z.two y
+  let pow10 y = pow_check_exp Z.ten y
+
+  let power (x : int) (y : t) : t =
+    let y =
+      try Q.to_int y
+      with Z.Overflow ->
+        (* XXX: make doesn't link Pp / CErrors for csdpcert, that could be fixed *)
+        raise (Invalid_argument "[micromega] overflow in exponentiation")
+      (* CErrors.user_err (Pp.str "[micromega] overflow in exponentiation") *)
+    in
+    pow_check_exp (Z.of_int x) y
 end
diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli
index acc6be6ce0..0b4d52708f 100644
--- a/plugins/micromega/numCompat.mli
+++ b/plugins/micromega/numCompat.mli
@@ -25,8 +25,15 @@ module type ZArith = sig
   val power_int : t -> int -> t
   val quomod : t -> t -> t * t
   val ppcm : t -> t -> t
+
+  (** [gcd x y] Greatest Common Divisor. Must always return a
+     positive number *)
   val gcd : t -> t -> t
+
+  (** [lcm x y] Least Common Multiplier. Must always return a
+     positive number *)
   val lcm : t -> t -> t
+
   val to_string : t -> string
 end
 
@@ -40,7 +47,9 @@ module type QArith = sig
   val one : t
   val two : t
   val ten : t
-  val neg_one : t
+
+  (** -1 constant  *)
+  val minus_one : t
 
   module Notations : sig
     val ( // ) : t -> t -> t
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index afef41d67e..5c0aa9ef0d 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -156,7 +156,7 @@ let pp_mon o (m, i) =
   if Monomial.is_const m then
     if Q.zero =/ i then () else Printf.fprintf o "%s" (Q.to_string i)
   else if Q.one =/ i then Monomial.pp o m
-  else if Q.neg_one =/ i then Printf.fprintf o "-%a" Monomial.pp m
+  else if Q.minus_one =/ i then Printf.fprintf o "-%a" Monomial.pp m
   else if Q.zero =/ i then ()
   else Printf.fprintf o "%s*%a" (Q.to_string i) Monomial.pp m
 
@@ -912,7 +912,7 @@ module WithProof = struct
       else
         match o with
         | Eq ->
-          Some ((Vect.set 0 Q.neg_one Vect.null, Eq), ProofFormat.Gcd (g, prf))
+          Some ((Vect.set 0 Q.minus_one Vect.null, Eq), ProofFormat.Gcd (g, prf))
         | Gt -> failwith "cutting_plane ignore strict constraints"
         | Ge ->
           (* This is a non-trivial common divisor *)
@@ -999,7 +999,7 @@ module WithProof = struct
     | Some (c, p) -> Some (c, ProofFormat.simplify_prf_rule p)
 
   let is_substitution strict ((p, o), prf) =
-    let pred v = if strict then v =/ Q.one || v =/ Q.neg_one else true in
+    let pred v = if strict then v =/ Q.one || v =/ Q.minus_one else true in
     match o with Eq -> LinPoly.search_linear pred p | _ -> None
 
   let subst1 sys0 =
diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml
index eaa26ded62..f59d65085a 100644
--- a/plugins/micromega/simplex.ml
+++ b/plugins/micromega/simplex.ml
@@ -247,8 +247,8 @@ let solve_column (c : var) (r : var) (e : Vect.t) : Vect.t =
   let a = Vect.get c e in
   if a =/ Q.zero then failwith "Cannot solve column"
   else
-    let a' = Q.neg_one // a in
-    Vect.mul a' (Vect.set r Q.neg_one (Vect.set c Q.zero e))
+    let a' = Q.minus_one // a in
+    Vect.mul a' (Vect.set r Q.minus_one (Vect.set c Q.zero e))
 
 (** [pivot_row r c e]
     @param c is such that c = e
@@ -364,7 +364,8 @@ let push_real (opt : bool) (nw : var) (v : Vect.t) (rst : Restricted.t)
       if n >=/ Q.zero then Sat (t', None)
       else
         let v' = safe_find "push_real" nw t' in
-        Unsat (Vect.set nw Q.one (Vect.set 0 Q.zero (Vect.mul Q.neg_one v'))) )
+        Unsat (Vect.set nw Q.one (Vect.set 0 Q.zero (Vect.mul Q.minus_one v')))
+    )
 
 (** One complication is that equalities needs some pre-processing.
  *)
@@ -399,7 +400,7 @@ let eliminate_equalities (vr0 : var) (l : Polynomial.cstr list) =
         elim (idx + 1) (vr + 1) (IMap.add vr (idx, true) vm) l ((vr, v) :: acc)
       | Eq ->
         let v1 = Vect.set 0 (Q.neg c.cst) c.coeffs in
-        let v2 = Vect.mul Q.neg_one v1 in
+        let v2 = Vect.mul Q.minus_one v1 in
         let vm = IMap.add vr (idx, true) (IMap.add (vr + 1) (idx, false) vm) in
         elim (idx + 1) (vr + 2) vm l ((vr, v1) :: (vr + 1, v2) :: acc)
       | Gt -> raise Strict )
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index 03d2a2d233..aeb9d14555 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -576,7 +576,7 @@ let eliminate_all_equations one =
       else
         let v = choose_variable eq in
         let a = apply eq v in
-        let eq' = equation_cmul (Q.neg_one // a) (undefine v eq) in
+        let eq' = equation_cmul (Q.minus_one // a) (undefine v eq) in
         let elim e =
           let b = tryapplyd e v Q.zero in
           if b =/ Q.zero then e
@@ -814,7 +814,7 @@ let bmatrix_add = combine ( +/ ) (fun x -> x =/ Q.zero)
 let bmatrix_cmul c bm =
   if c =/ Q.zero then undefined else mapf (fun x -> c */ x) bm
 
-let bmatrix_neg = bmatrix_cmul Q.neg_one
+let bmatrix_neg = bmatrix_cmul Q.minus_one
 
 (* ------------------------------------------------------------------------- *)
 (* Smash a block matrix into components.                                     *)
@@ -943,7 +943,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol =
     List.fold_right
       (fun k -> List.nth pvs (k - 1) |-> element vec k)
       (1 -- dim vec)
-      ((0, 0, 0) |=> Q.neg_one)
+      ((0, 0, 0) |=> Q.minus_one)
   in
   let finalassigs =
     foldl (fun a v e -> (v |-> equation_eval newassigs e) a) newassigs allassig
@@ -1166,7 +1166,7 @@ let sumofsquares_general_symmetry tool pol =
       match cls with
       | [] -> raise Sanity
       | [h] -> acc
-      | h :: t -> List.map (fun k -> (k |-> Q.neg_one) (h |=> Q.one)) t @ acc
+      | h :: t -> List.map (fun k -> (k |-> Q.minus_one) (h |=> Q.one)) t @ acc
     in
     List.fold_right mk_eq eqvcls []
   in
diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml
index 3e0b1f2cd9..4df32f2ba4 100644
--- a/plugins/micromega/vect.ml
+++ b/plugins/micromega/vect.ml
@@ -52,7 +52,7 @@ let pp_var_num pp_var o {var = v; coe = n} =
   if Int.equal v 0 then
     if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n)
   else if Q.one =/ n then pp_var o v
-  else if Q.neg_one =/ n then Printf.fprintf o "-%a" pp_var v
+  else if Q.minus_one =/ n then Printf.fprintf o "-%a" pp_var v
   else if Q.zero =/ n then ()
   else Printf.fprintf o "%s*%a" (Q.to_string n) pp_var v
 
@@ -60,7 +60,7 @@ let pp_var_num_smt pp_var o {var = v; coe = n} =
   if Int.equal v 0 then
     if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n)
   else if Q.one =/ n then pp_var o v
-  else if Q.neg_one =/ n then Printf.fprintf o "(- %a)" pp_var v
+  else if Q.minus_one =/ n then Printf.fprintf o "(- %a)" pp_var v
   else if Q.zero =/ n then ()
   else Printf.fprintf o "(* %s %a)" (Q.to_string n) pp_var v
 
diff --git a/test-suite/.csdp.cache.test-suite b/test-suite/.csdp.cache.test-suite
index 046cb067c5..36efdf469e 100644
--- a/test-suite/.csdp.cache.test-suite
+++ b/test-suite/.csdp.cache.test-suite
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 758374c5de..6c373701cf 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -141,7 +141,7 @@ run: $(SUBSYSTEMS)
 bugs: $(BUGS)
 
 clean:
-	rm -f trace .nia.cache .lia.cache output/MExtraction.out
+	rm -f trace .csdp.cache .nia.cache .lia.cache output/MExtraction.out
 	rm -f vos/Makefile vos/Makefile.conf
 	$(SHOW) 'RM        <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>'
 	$(HIDE)find . \( \