[micromega] Add numerical compatibility layer.

Only significant change is in gcd / lcm which now are typed in `Z.t`

1 files changed, 26 insertions, 26 deletions

diff --git a/plugins/micromega/vect.mli b/plugins/micromega/vect.mli
index 4b814cbb82..56c8ce87dd 100644
--- a/plugins/micromega/vect.mli
+++ b/plugins/micromega/vect.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Num
+open NumCompat
 open Mutils
 
 type var = int
@@ -50,18 +50,18 @@ val pp_smt : out_channel -> t -> unit
 val variables : t -> ISet.t
 (** [variables v] returns the set of variables with non-zero coefficients *)
 
-val get_cst : t -> num
+val get_cst : t -> Q.t
 (** [get_cst v] returns c i.e. the coefficient of the variable zero *)
 
-val decomp_cst : t -> num * t
+val decomp_cst : t -> Q.t * t
 (** [decomp_cst v] returns the pair (c,a1.x1+...+an.xn) *)
 
-val decomp_at : int -> t -> num * t
+val decomp_at : int -> t -> Q.t * t
 (** [decomp_cst v] returns the pair (ai, ai+1.xi+...+an.xn) *)
 
-val decomp_fst : t -> (var * num) * t
+val decomp_fst : t -> (var * Q.t) * t
 
-val cst : num -> t
+val cst : Q.t -> t
 (** [cst c] returns the vector v=c+0.x1+...+0.xn *)
 
 val is_constant : t -> bool
@@ -74,33 +74,33 @@ val null : t
 val is_null : t -> bool
 (** [is_null v] returns whether [v] is the [null] vector i.e [equal v  null] *)
 
-val get : var -> t -> num
+val get : var -> t -> Q.t
 (** [get xi v] returns the coefficient ai of the variable [xi].
     [get] is also defined for the variable 0 *)
 
-val set : var -> num -> t -> t
+val set : var -> Q.t -> t -> t
 (** [set xi ai' v] returns the vector c+a1.x1+...ai'.xi+...+an.xn
     i.e. the coefficient of the variable xi is set to ai' *)
 
 val mkvar : var -> t
 (** [mkvar xi] returns 1.xi *)
 
-val update : var -> (num -> num) -> t -> t
+val update : var -> (Q.t -> Q.t) -> t -> t
 (** [update xi f v] returns c+a1.x1+...+f(ai).xi+...+an.xn *)
 
 val fresh : t -> int
 (** [fresh v] return the fresh variable with index 1+ max (variables v) *)
 
-val choose : t -> (var * num * t) option
+val choose : t -> (var * Q.t * t) option
 (** [choose v] decomposes a vector [v] depending on whether it is [null] or not.
     @return None if v is [null]
     @return Some(x,n,r) where v = r + n.x  x is the smallest variable with non-zero coefficient n <> 0.
  *)
 
-val from_list : num list -> t
+val from_list : Q.t list -> t
 (** [from_list l] returns the vector c+a1.x1...an.xn from the list of coefficient [l=c;a1;...;an] *)
 
-val to_list : t -> num list
+val to_list : t -> Q.t list
 (** [to_list v] returns the list of all coefficient of the vector v i.e. [c;a1;...;an]
     The list representation is (obviously) not sparsed
     and therefore certain ai may be 0 *)
@@ -114,7 +114,7 @@ val incr_var : int -> t -> t
 (** [incr_var i v] increments the variables of the vector [v] by the amount [i].
  *)
 
-val gcd : t -> Big_int.big_int
+val gcd : t -> Z.t
 (** [gcd v] returns gcd(num(c),num(a1),...,num(an)) where num extracts
    the numerator of a rational value. *)
 
@@ -130,17 +130,17 @@ val add : t -> t -> t
     @return c1+c1'+ (a1+a1').x1 + ... + (an+an').xn
  *)
 
-val mul : num -> t -> t
+val mul : Q.t -> t -> t
 (** [mul a v] is vector multiplication of vector [v] by a scalar [a].
     @return a.v = a.c+a.a1.x1+...+a.an.xn *)
 
-val mul_add : num -> t -> num -> t -> t
+val mul_add : Q.t -> t -> Q.t -> t -> t
 (** [mul_add c1 v1 c2 v2] returns the linear combination c1.v1+c2.v2 *)
 
 val subst : int -> t -> t -> t
 (** [subst x v v'] replaces x by v in vector v' *)
 
-val div : num -> t -> t
+val div : Q.t -> t -> t
 (** [div c1 v1] returns the mutiplication by the inverse of c1 i.e (1/c1).v1 *)
 
 val uminus : t -> t
@@ -148,36 +148,36 @@ val uminus : t -> t
 
 (** {1 Iterators} *)
 
-val fold : ('acc -> var -> num -> 'acc) -> 'acc -> t -> 'acc
+val fold : ('acc -> var -> Q.t -> 'acc) -> 'acc -> t -> 'acc
 (** [fold f acc v] returns f (f (f acc 0 c ) x1 a1 ) ... xn an *)
 
-val fold_error : ('acc -> var -> num -> 'acc option) -> 'acc -> t -> 'acc option
+val fold_error : ('acc -> var -> Q.t -> 'acc option) -> 'acc -> t -> 'acc option
 (** [fold_error f acc v] is the same as
     [fold (fun acc x i -> match acc with None -> None | Some acc' -> f acc' x i) (Some acc) v]
     but with early exit...
  *)
 
-val find : (var -> num -> 'c option) -> t -> 'c option
+val find : (var -> Q.t -> 'c option) -> t -> 'c option
 (** [find f v] returns the first [f xi ai] such that [f xi ai <> None].
     If no such xi ai exists, it returns None *)
 
-val for_all : (var -> num -> bool) -> t -> bool
+val for_all : (var -> Q.t -> bool) -> t -> bool
 (** [for_all p v] returns /\_{i>=0} (f xi ai) *)
 
-val exists2 : (num -> num -> bool) -> t -> t -> (var * num * num) option
+val exists2 : (Q.t -> Q.t -> bool) -> t -> t -> (var * Q.t * Q.t) option
 (** [exists2 p v v'] returns Some(xi,ai,ai')
     if p(xi,ai,ai') holds and ai,ai' <> 0.
     It returns None if no such pair of coefficient exists. *)
 
-val dotproduct : t -> t -> num
+val dotproduct : t -> t -> Q.t
 (** [dotproduct v1 v2] is the dot product of v1 and v2. *)
 
-val map : (var -> num -> 'a) -> t -> 'a list
-val abs_min_elt : t -> (var * num) option
-val partition : (var -> num -> bool) -> t -> t * t
+val map : (var -> Q.t -> 'a) -> t -> 'a list
+val abs_min_elt : t -> (var * Q.t) option
+val partition : (var -> Q.t -> bool) -> t -> t * t
 
 module Bound : sig
-  type t = {cst : num; var : var; coeff : num}
+  type t = {cst : Q.t; var : var; coeff : Q.t}
   (** represents a0 + ai.xi  *)
 
   val of_vect : vector -> t option