From 685f43dd6d8470992c3e74b4c14c133e74789796 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 18 Oct 2018 13:44:28 +0200
Subject: [micromega] call csdpcert using path.

---
 plugins/micromega/coq_micromega.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins')

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;
-- 
cgit v1.2.3


From 79aac956aede707ca816360849bfb1ef910ec484 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 9 Sep 2020 17:59:37 +0200
Subject: [micromega] Migrate from num to zarith

We still link num in `coqc` , that will be removed in a separate step.

Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
---
 plugins/micromega/mfourier.ml  |   1 +
 plugins/micromega/numCompat.ml | 143 ++++++++++++++++++++---------------------
 2 files changed, 72 insertions(+), 72 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index 3d1770a541..1c0ddd502a 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)
 
diff --git a/plugins/micromega/numCompat.ml b/plugins/micromega/numCompat.ml
index 4cb91ea520..62f05685aa 100644
--- a/plugins/micromega/numCompat.ml
+++ b/plugins/micromega/numCompat.ml
@@ -31,37 +31,27 @@ 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
+  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')
+  (* 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 gcd = gcd_big_int
+  (* Workaround https://github.com/ocaml/Zarith/issues/58 , remove
+     the abs when zarith 1.9.2 is released *)
+  let gcd x y = Z.abs (Z.gcd x y)
 
+  (* zarith fails with division by zero if x && y == 0 *)
   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))
+    if Z.equal x zero && Z.equal y zero then zero else Z.abs (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
@@ -119,56 +109,65 @@ 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)
+  let neg_one = Q.(neg one)
 
   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
+
+  (* Num round 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
-- 
cgit v1.2.3


From 7bf884b7c525092db74ac2effcf1091bd3c3d46c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 14 Sep 2020 18:23:55 +0200
Subject: [zarith] [micromega] Bump to 1.10 and remove some hacks

In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in
1.10, see

https://github.com/ocaml/Zarith/issues/58
---
 plugins/micromega/numCompat.ml  | 13 +++++--------
 plugins/micromega/numCompat.mli |  7 +++++++
 2 files changed, 12 insertions(+), 8 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/numCompat.ml b/plugins/micromega/numCompat.ml
index 62f05685aa..8cfda32543 100644
--- a/plugins/micromega/numCompat.ml
+++ b/plugins/micromega/numCompat.ml
@@ -31,6 +31,8 @@ module type ZArith = sig
 end
 
 module Z = struct
+  (* Beware this only works fine in ZArith >= 1.10 due to
+     https://github.com/ocaml/Zarith/issues/58 *)
   include Z
 
   (* Constants *)
@@ -39,13 +41,8 @@ module Z = struct
   let power_int = Big_int_Z.power_big_int_positive_int
   let quomod = Big_int_Z.quomod_big_int
 
-  (* Workaround https://github.com/ocaml/Zarith/issues/58 , remove
-     the abs when zarith 1.9.2 is released *)
-  let gcd x y = Z.abs (Z.gcd x y)
-
-  (* zarith fails with division by zero if x && y == 0 *)
-  let lcm x y =
-    if Z.equal x zero && Z.equal y zero then zero else Z.abs (Z.lcm 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 ppcm x y =
     let g = gcd x y in
@@ -144,7 +141,7 @@ module Q : QArith with module Z = Z = struct
   let ceiling q : t = Z.cdiv (Q.num q) (Q.den q) |> Q.of_bigint
   let half = Q.make Z.one Z.two
 
-  (* Num round is to the nearest *)
+  (* We imitate Num's round which is to the nearest *)
   let round q = floor (Q.add half q)
 
   (* XXX: review / improve *)
diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli
index acc6be6ce0..fe0a6e7660 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
 
-- 
cgit v1.2.3


From acb24a1540c33f075a83f9788614e5c2f3335b0a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 14 Sep 2020 18:26:21 +0200
Subject: [micromega] Use `minus_one` built-in zarith constant.

---
 plugins/micromega/certificate.ml | 4 ++--
 plugins/micromega/mfourier.ml    | 2 +-
 plugins/micromega/numCompat.ml   | 3 +--
 plugins/micromega/numCompat.mli  | 4 +++-
 plugins/micromega/polynomial.ml  | 6 +++---
 plugins/micromega/simplex.ml     | 9 +++++----
 plugins/micromega/sos.ml         | 8 ++++----
 plugins/micromega/vect.ml        | 4 ++--
 8 files changed, 21 insertions(+), 19 deletions(-)

(limited to 'plugins')

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/mfourier.ml b/plugins/micromega/mfourier.ml
index 1c0ddd502a..f4d17b8940 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -570,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 8cfda32543..02c4bab497 100644
--- a/plugins/micromega/numCompat.ml
+++ b/plugins/micromega/numCompat.ml
@@ -61,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
@@ -120,7 +120,6 @@ module Q : QArith with module Z = Z = struct
 
   let two = Q.(of_int 2)
   let ten = Q.(of_int 10)
-  let neg_one = Q.(neg one)
 
   module Notations = struct
     let ( // ) = Q.div
diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli
index fe0a6e7660..0b4d52708f 100644
--- a/plugins/micromega/numCompat.mli
+++ b/plugins/micromega/numCompat.mli
@@ -47,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
 
-- 
cgit v1.2.3