diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/micromega/vect.ml | 115 |
1 files changed, 58 insertions, 57 deletions
diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml index 1742f81b34..c6c6d6047a 100644 --- a/plugins/micromega/vect.ml +++ b/plugins/micromega/vect.ml @@ -19,7 +19,8 @@ type var = int - values are all non-zero *) -type t = (var * Q.t) list +type mono = { var : var; coe : Q.t } +type t = mono list type vector = t (** [equal v1 v2 = true] if the vectors are syntactically equal. *) @@ -29,21 +30,21 @@ let rec equal v1 v2 = | [], [] -> true | [], _ -> false | _ :: _, [] -> false - | (i1, n1) :: v1, (i2, n2) :: v2 -> Int.equal i1 i2 && n1 =/ n2 && equal v1 v2 + | { var = i1; coe = n1 } :: v1, { var = i2; coe = n2 } :: v2 -> Int.equal i1 i2 && n1 =/ n2 && equal v1 v2 let hash v = let rec hash i = function | [] -> i - | (vr, vl) :: l -> hash (i + Hashtbl.hash (vr, Q.to_float vl)) l + | { var = vr; coe = vl } :: l -> hash (i + Hashtbl.hash (vr, Q.to_float vl)) l in Hashtbl.hash (hash 0 v) let null = [] let is_null v = - match v with [] -> true | [(0, x)] when Q.zero =/ x -> true | _ -> false + match v with [] -> true | [{ var = 0; coe = x }] when Q.zero =/ x -> true | _ -> false -let pp_var_num pp_var o (v, n) = +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 @@ -51,7 +52,7 @@ let pp_var_num pp_var o (v, n) = else if Q.zero =/ n then () else Printf.fprintf o "%s*%a" (Q.to_string n) pp_var v -let pp_var_num_smt pp_var o (v, n) = +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 @@ -79,7 +80,7 @@ let from_list (l : Q.t list) = match l with | [] -> [] | e :: l -> - if e <>/ Q.zero then (i, e) :: xfrom_list (i + 1) l + if e <>/ Q.zero then { var = i; coe = e } :: xfrom_list (i + 1) l else xfrom_list (i + 1) l in xfrom_list 0 l @@ -88,68 +89,68 @@ let to_list m = let rec xto_list i l = match l with | [] -> [] - | (x, v) :: l' -> + | { var = x; coe = v } :: l' -> if i = x then v :: xto_list (i + 1) l' else Q.zero :: xto_list (i + 1) l in xto_list 0 m -let cons i v rst = if v =/ Q.zero then rst else (i, v) :: rst +let cons i v rst = if v =/ Q.zero then rst else { var = i; coe = v } :: rst let rec update i f t = match t with | [] -> cons i (f Q.zero) [] - | (k, v) :: l -> ( - match Int.compare i k with - | 0 -> cons k (f v) l + | x :: l -> ( + match Int.compare i x.var with + | 0 -> cons x.var (f x.coe) l | -1 -> cons i (f Q.zero) t - | 1 -> (k, v) :: update i f l + | 1 -> x :: update i f l | _ -> failwith "compare_num" ) let rec set i n t = match t with | [] -> cons i n [] - | (k, v) :: l -> ( - match Int.compare i k with - | 0 -> cons k n l + | x :: l -> ( + match Int.compare i x.var with + | 0 -> cons x.var n l | -1 -> cons i n t - | 1 -> (k, v) :: set i n l + | 1 -> x :: set i n l | _ -> failwith "compare_num" ) -let cst n = if n =/ Q.zero then [] else [(0, n)] +let cst n = if n =/ Q.zero then [] else [{ var = 0; coe = n }] let mul z t = if z =/ Q.zero then [] else if z =/ Q.one then t - else List.map (fun (i, n) -> (i, z */ n)) t + else List.map (fun { var = i; coe = n } -> { var = i; coe = z */ n }) t let div z t = - if z <>/ Q.one then List.map (fun (x, nx) -> (x, nx // z)) t else t + if z <>/ Q.one then List.map (fun { var = x; coe = nx } -> { var = x; coe = nx // z }) t else t -let uminus t = List.map (fun (i, n) -> (i, Q.neg n)) t +let uminus t = List.map (fun { var = i; coe = n } -> { var = i; coe = Q.neg n }) t let rec add (ve1 : t) (ve2 : t) = match (ve1, ve2) with | [], v | v, [] -> v - | (v1, c1) :: l1, (v2, c2) :: l2 -> + | { var = v1; coe = c1 } :: l1, { var = v2; coe = c2 } :: l2 -> let cmp = Int.compare v1 v2 in if cmp == 0 then let s = c1 +/ c2 in - if Q.zero =/ s then add l1 l2 else (v1, s) :: add l1 l2 - else if cmp < 0 then (v1, c1) :: add l1 ve2 - else (v2, c2) :: add l2 ve1 + if Q.zero =/ s then add l1 l2 else { var = v1; coe = s } :: add l1 l2 + else if cmp < 0 then { var = v1; coe = c1 } :: add l1 ve2 + else { var = v2; coe = c2 } :: add l2 ve1 let rec xmul_add (n1 : Q.t) (ve1 : t) (n2 : Q.t) (ve2 : t) = match (ve1, ve2) with | [], _ -> mul n2 ve2 | _, [] -> mul n1 ve1 - | (v1, c1) :: l1, (v2, c2) :: l2 -> + | { var = v1; coe = c1 } :: l1, { var = v2; coe = c2 } :: l2 -> let cmp = Int.compare v1 v2 in if cmp == 0 then let s = (n1 */ c1) +/ (n2 */ c2) in if Q.zero =/ s then xmul_add n1 l1 n2 l2 - else (v1, s) :: xmul_add n1 l1 n2 l2 - else if cmp < 0 then (v1, n1 */ c1) :: xmul_add n1 l1 n2 ve2 - else (v2, n2 */ c2) :: xmul_add n1 ve1 n2 l2 + else { var = v1; coe = s } :: xmul_add n1 l1 n2 l2 + else if cmp < 0 then { var = v1; coe = n1 */ c1 } :: xmul_add n1 l1 n2 ve2 + else { var = v2; coe = n2 */ c2 } :: xmul_add n1 ve1 n2 l2 let mul_add n1 ve1 n2 ve2 = if n1 =/ Q.one && n2 =/ Q.one then add ve1 ve2 else xmul_add n1 ve1 n2 ve2 @@ -157,8 +158,8 @@ let mul_add n1 ve1 n2 ve2 = let compare : t -> t -> int = Mutils.Cmp.compare_list (fun x y -> Mutils.Cmp.compare_lexical - [ (fun () -> Int.compare (fst x) (fst y)) - ; (fun () -> Q.compare (snd x) (snd y)) ]) + [ (fun () -> Int.compare x.var y.var) + ; (fun () -> Q.compare x.coe y.coe) ]) (** [tail v vect] returns - [None] if [v] is not a variable of the vector [vect] @@ -169,7 +170,7 @@ let compare : t -> t -> int = let rec tail (v : var) (vect : t) = match vect with | [] -> None - | (v', vl) :: vect' -> ( + | { var = v'; coe = vl } :: vect' -> ( match Int.compare v' v with | 0 -> Some (vl, vect) (* Ok, found *) | -1 -> tail v vect' (* Might be in the tail *) @@ -178,38 +179,38 @@ let rec tail (v : var) (vect : t) = (* Hopeless *) let get v vect = match tail v vect with None -> Q.zero | Some (vl, _) -> vl -let is_constant v = match v with [] | [(0, _)] -> true | _ -> false -let get_cst vect = match vect with (0, v) :: _ -> v | _ -> Q.zero -let choose v = match v with [] -> None | (vr, vl) :: rst -> Some (vr, vl, rst) -let rec fresh v = match v with [] -> 1 | [(v, _)] -> v + 1 | _ :: v -> fresh v -let variables v = List.fold_left (fun acc (x, _) -> ISet.add x acc) ISet.empty v -let decomp_cst v = match v with (0, vl) :: v -> (vl, v) | _ -> (Q.zero, v) +let is_constant v = match v with [] | [{ var = 0 }] -> true | _ -> false +let get_cst vect = match vect with { var = 0; coe = v } :: _ -> v | _ -> Q.zero +let choose v = match v with [] -> None | { var = vr; coe = vl } :: rst -> Some (vr, vl, rst) +let rec fresh v = match v with [] -> 1 | [{ var = v }] -> v + 1 | _ :: v -> fresh v +let variables v = List.fold_left (fun acc { var = x } -> ISet.add x acc) ISet.empty v +let decomp_cst v = match v with { var = 0; coe = vl } :: v -> (vl, v) | _ -> (Q.zero, v) let rec decomp_at i v = match v with | [] -> (Q.zero, null) - | (vr, vl) :: r -> + | { var = vr; coe = vl } :: r -> if i = vr then (vl, r) else if i < vr then (Q.zero, v) else decomp_at i r -let decomp_fst v = match v with [] -> ((0, Q.zero), []) | x :: v -> (x, v) +let decomp_fst v = match v with [] -> ((0, Q.zero), []) | x :: v -> ((x.var, x.coe), v) let rec subst (vr : int) (e : t) (v : t) = match v with | [] -> [] - | (x, n) :: v' -> ( + | { var = x; coe = n } :: v' -> ( match Int.compare vr x with | 0 -> mul_add n e Q.one v' | -1 -> v - | 1 -> add [(x, n)] (subst vr e v') + | 1 -> add [{ var = x; coe = n }] (subst vr e v') | _ -> assert false ) -let fold f acc v = List.fold_left (fun acc (v, i) -> f acc v i) acc v +let fold f acc v = List.fold_left (fun acc x -> f acc x.var x.coe) acc v let fold_error f acc v = let rec fold acc v = match v with | [] -> Some acc - | (x, i) :: v' -> ( + | { var = x; coe = i } :: v' -> ( match f acc x i with None -> None | Some acc' -> fold acc' v' ) in fold acc v @@ -217,11 +218,11 @@ let fold_error f acc v = let rec find p v = match v with | [] -> None - | (v, n) :: v' -> ( match p v n with None -> find p v' | Some r -> Some r ) + | { var = v; coe = n } :: v' -> ( match p v n with None -> find p v' | Some r -> Some r ) -let for_all p l = List.for_all (fun (v, n) -> p v n) l -let decr_var i v = List.map (fun (v, n) -> (v - i, n)) v -let incr_var i v = List.map (fun (v, n) -> (v + i, n)) v +let for_all p l = List.for_all (fun { var = v; coe = n } -> p v n) l +let decr_var i v = List.map (fun x -> { x with var = x.var - i }) v +let incr_var i v = List.map (fun x -> { x with var = x.var + i }) v let gcd v = let res = @@ -239,12 +240,12 @@ let normalise v = let gcd = fold (fun c _ n -> Z.gcd c (Q.num n)) Z.zero v in if Int.equal (Z.compare gcd Z.zero) 0 then Z.one else gcd in - List.map (fun (x, v) -> (x, v */ Q.of_bigint ppcm // Q.of_bigint gcd)) v + List.map (fun { var = x; coe = v } -> { var = x; coe = v */ Q.of_bigint ppcm // Q.of_bigint gcd }) v let rec exists2 p vect1 vect2 = match (vect1, vect2) with | _, [] | [], _ -> None - | (v1, n1) :: vect1', (v2, n2) :: vect2' -> + | { var = v1; coe = n1 } :: vect1', { var = v2; coe = n2 } :: vect2' -> if Int.equal v1 v2 then if p n1 n2 then Some (v1, n1, n2) else exists2 p vect1' vect2' else if v1 < v2 then exists2 p vect1' vect2 @@ -254,26 +255,26 @@ let dotproduct v1 v2 = let rec dot acc v1 v2 = match (v1, v2) with | [], _ | _, [] -> acc - | (x1, n1) :: v1', (x2, n2) :: v2' -> + | { var = x1; coe = n1 } :: v1', { var = x2; coe = n2 } :: v2' -> if x1 == x2 then dot (acc +/ (n1 */ n2)) v1' v2' else if x1 < x2 then dot acc v1' v2 else dot acc v1 v2' in dot Q.zero v1 v2 -let map f v = List.map (fun (x, v) -> f x v) v +let map f v = List.map (fun { var = x; coe = v } -> f x v) v let abs_min_elt v = match v with | [] -> None - | (v, vl) :: r -> + | { var = v; coe = vl } :: r -> Some (List.fold_left - (fun (v1, vl1) (v2, vl2) -> + (fun (v1, vl1) { var = v2; coe = vl2 } -> if Q.abs vl1 </ Q.abs vl2 then (v1, vl1) else (v2, vl2)) (v, vl) r) -let partition p = List.partition (fun (vr, vl) -> p vr vl) +let partition p = List.partition (fun { var = vr; coe = vl }-> p vr vl) let mkvar x = set x Q.one null module Bound = struct @@ -281,7 +282,7 @@ module Bound = struct let of_vect (v : vector) = match v with - | [(x, v)] -> if x = 0 then None else Some {cst = Q.zero; var = x; coeff = v} - | [(0, v); (x, v')] -> Some {cst = v; var = x; coeff = v'} + | [{ var = x; coe = v }] -> if x = 0 then None else Some {cst = Q.zero; var = x; coeff = v} + | [{ var = 0; coe = v }; { var = x; coe = v' }] -> Some {cst = v; var = x; coeff = v'} | _ -> None end |