[micromega] Switch from Big_int to ZArith.

.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"

.merlin.in

@@ -54,3 +54,4 @@ S plugins/**
 B plugins/**
 
 PKG threads.posix
+PKG zarith

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)
 

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:

coq.opam

@@ -25,7 +25,7 @@ depends: [
   "dune"      { >= "2.5.0"  }
   "ocamlfind" { build }
   "num"
-  "zarith"    { >= "1.9.1" }
+  "zarith"    { >= "1.10" }
 ]
 
 build: [

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}
 ]
 

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

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

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

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;

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 *)

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

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

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 =

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 )