aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/micromega/coq_micromega.ml12
-rw-r--r--plugins/micromega/mutils.ml4
-rw-r--r--plugins/micromega/vect.ml123
3 files changed, 84 insertions, 55 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index bb539374e2..82f8b5b3e2 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1279,7 +1279,8 @@ module M = struct
let dump_expr i e =
let rec dump_expr = function
| Mc.PEX n ->
- EConstr.mkRel (i + CList.assoc_f Int.equal (CoqToCaml.positive n) vars_idx)
+ EConstr.mkRel
+ (i + CList.assoc_f Int.equal (CoqToCaml.positive n) vars_idx)
| Mc.PEc z -> dexpr.dump_cst z
| Mc.PEadd (e1, e2) ->
EConstr.mkApp (dexpr.dump_add, [|dump_expr e1; dump_expr e2|])
@@ -1294,7 +1295,9 @@ module M = struct
dump_expr e
in
let mkop op e1 e2 =
- try EConstr.mkApp (CList.assoc_f Mutils.Hash.eq_op2 op dexpr.dump_op, [|e1; e2|])
+ try
+ EConstr.mkApp
+ (CList.assoc_f Mutils.Hash.eq_op2 op dexpr.dump_op, [|e1; e2|])
with Not_found ->
EConstr.mkApp (Lazy.force coq_Eq, [|dexpr.interp_typ; e1; e2|])
in
@@ -1606,7 +1609,8 @@ let witness_list_tags p g = witness_list p g
* Prune the proof object, according to the 'diff' between two cnf formulas.
*)
-let compact_proofs (eq_cst : 'cst -> 'cst -> bool) (cnf_ff : 'cst cnf) res (cnf_ff' : 'cst cnf) =
+let compact_proofs (eq_cst : 'cst -> 'cst -> bool) (cnf_ff : 'cst cnf) res
+ (cnf_ff' : 'cst cnf) =
let eq_formula (p1, o1) (p2, o2) =
let open Mutils.Hash in
eq_pol eq_cst p1 p2 && eq_op1 o1 o2
@@ -1651,7 +1655,7 @@ let compact_proofs (eq_cst : 'cst -> 'cst -> bool) (cnf_ff : 'cst cnf) res (cnf_
let eq (f1, (t1, e1)) (f2, (t2, e2)) =
Int.equal (Tag.compare t1 t2) 0
&& eq_formula f1 f2
- && ( = ) (e1 : EConstr.t) (e2 : EConstr.t)
+ && (e1 : EConstr.t) = (e2 : EConstr.t)
(* FIXME: what equality should we use here? *)
in
is_sublist eq hyps new_cl
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 746778cb7c..27b917383b 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -386,7 +386,9 @@ module Hash = struct
Mc.(function Equal -> 0 | NonEqual -> 1 | Strict -> 2 | NonStrict -> 3)
let int_of_eq_op2 =
- Mc.(function OpEq -> 0 | OpNEq -> 1 | OpLe -> 2 | OpGe -> 3 | OpLt -> 4 | OpGt -> 5)
+ Mc.(
+ function
+ | OpEq -> 0 | OpNEq -> 1 | OpLe -> 2 | OpGe -> 3 | OpLt -> 4 | OpGt -> 5)
let eq_op1 o1 o2 = Int.equal (int_of_eq_op1 o1) (int_of_eq_op1 o2)
let eq_op2 o1 o2 = Int.equal (int_of_eq_op2 o1) (int_of_eq_op2 o2)
diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml
index 5a762b168a..15f37868f7 100644
--- a/plugins/micromega/vect.ml
+++ b/plugins/micromega/vect.ml
@@ -19,7 +19,7 @@ type var = int
- values are all non-zero
*)
-type mono = { var : var; coe : Q.t }
+type mono = {var : var; coe : Q.t}
type t = mono list
type vector = t
@@ -30,21 +30,25 @@ let rec equal v1 v2 =
| [], [] -> true
| [], _ -> false
| _ :: _, [] -> false
- | { var = i1; coe = n1 } :: v1, { var = i2; coe = 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
- | { var = vr; coe = 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 | [{ var = 0; coe = 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 { var = v; coe = 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
@@ -52,7 +56,7 @@ let pp_var_num pp_var o { var = v; coe = 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 { var = v; coe = 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
@@ -80,7 +84,7 @@ let from_list (l : Q.t list) =
match l with
| [] -> []
| e :: l ->
- if e <>/ Q.zero then { var = i; coe = 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
@@ -89,12 +93,13 @@ let to_list m =
let rec xto_list i l =
match l with
| [] -> []
- | { var = x; coe = v } :: l' ->
- if Int.equal i x then v :: xto_list (i + 1) l' else Q.zero :: xto_list (i + 1) l
+ | {var = x; coe = v} :: l' ->
+ if Int.equal 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 { var = i; coe = 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
@@ -116,41 +121,43 @@ let rec set i n t =
| 1 -> x :: set i n l
| _ -> failwith "compare_num" )
-let cst n = if n =/ Q.zero then [] else [{ var = 0; coe = 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 { var = i; coe = n } -> { var = i; coe = 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 { var = x; coe = nx } -> { var = x; coe = 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 { var = i; coe = n } -> { var = i; coe = 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
- | { var = v1; coe = c1 } :: l1, { var = v2; coe = 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 { 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
+ 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
- | { var = v1; coe = c1 } :: l1, { var = v2; coe = 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 { 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
+ 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
@@ -158,8 +165,7 @@ 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 x.var y.var)
- ; (fun () -> Q.compare x.coe y.coe) ])
+ [(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]
@@ -170,7 +176,7 @@ let compare : t -> t -> int =
let rec tail (v : var) (vect : t) =
match vect with
| [] -> None
- | { var = v'; coe = 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 *)
@@ -179,29 +185,40 @@ 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 [] | [{ 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 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)
- | { var = vr; coe = vl } :: r ->
- if Int.equal i vr then (vl, r) else if i < vr then (Q.zero, v) else decomp_at i r
+ | {var = vr; coe = vl} :: r ->
+ if Int.equal 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.var, x.coe), 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
| [] -> []
- | { var = x; coe = 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 [{ var = x; coe = 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 x -> f acc x.var x.coe) acc v
@@ -210,7 +227,7 @@ let fold_error f acc v =
let rec fold acc v =
match v with
| [] -> Some acc
- | { var = x; coe = i } :: v' -> (
+ | {var = x; coe = i} :: v' -> (
match f acc x i with None -> None | Some acc' -> fold acc' v' )
in
fold acc v
@@ -218,11 +235,12 @@ let fold_error f acc v =
let rec find p v =
match v with
| [] -> None
- | { var = v; coe = 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 { 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 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 =
@@ -240,12 +258,15 @@ 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 { var = x; coe = v } -> { var = x; coe = 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
- | { var = v1; coe = n1 } :: vect1', { var = v2; coe = 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
@@ -255,26 +276,26 @@ let dotproduct v1 v2 =
let rec dot acc v1 v2 =
match (v1, v2) with
| [], _ | _, [] -> acc
- | { var = x1; coe = n1 } :: v1', { var = x2; coe = n2 } :: v2' ->
+ | {var = x1; coe = n1} :: v1', {var = x2; coe = n2} :: v2' ->
if Int.equal 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 { var = x; coe = 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
- | { var = v; coe = vl } :: r ->
+ | {var = v; coe = vl} :: r ->
Some
(List.fold_left
- (fun (v1, vl1) { var = v2; coe = 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 { var = vr; coe = 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
@@ -282,7 +303,9 @@ module Bound = struct
let of_vect (v : vector) =
match v with
- | [{ var = x; coe = v }] -> if Int.equal 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'}
+ | [{var = x; coe = v}] ->
+ if Int.equal 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 01:37:31 +0000