aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/micromega/certificate.ml4
-rw-r--r--plugins/micromega/coq_micromega.ml1
-rw-r--r--plugins/micromega/mfourier.ml3
-rw-r--r--plugins/micromega/numCompat.ml145
-rw-r--r--plugins/micromega/numCompat.mli11
-rw-r--r--plugins/micromega/polynomial.ml6
-rw-r--r--plugins/micromega/simplex.ml9
-rw-r--r--plugins/micromega/sos.ml8
-rw-r--r--plugins/micromega/vect.ml4
9 files changed, 99 insertions, 92 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/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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:49:40 +0000