[micromega] Use `minus_one` built-in zarith constant.

8 files changed, 21 insertions, 19 deletions

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