aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega')
-rw-r--r--plugins/micromega/.ocamlformat1
-rw-r--r--plugins/micromega/.ocamlformat-ignore1
-rw-r--r--plugins/micromega/certificate.ml2
-rw-r--r--plugins/micromega/certificate.mli16
-rw-r--r--plugins/micromega/coq_micromega.ml46
-rw-r--r--plugins/micromega/coq_micromega.mli2
-rw-r--r--plugins/micromega/mfourier.ml4
-rw-r--r--plugins/micromega/mutils.ml8
-rw-r--r--plugins/micromega/mutils.mli4
-rw-r--r--plugins/micromega/persistent_cache.mli10
-rw-r--r--plugins/micromega/polynomial.mli110
-rw-r--r--plugins/micromega/simplex.ml4
-rw-r--r--plugins/micromega/vect.ml146
-rw-r--r--plugins/micromega/vect.mli76
-rw-r--r--plugins/micromega/zify.ml6
15 files changed, 244 insertions, 192 deletions
diff --git a/plugins/micromega/.ocamlformat b/plugins/micromega/.ocamlformat
new file mode 100644
index 0000000000..a22a2ff88c
--- /dev/null
+++ b/plugins/micromega/.ocamlformat
@@ -0,0 +1 @@
+disable=false
diff --git a/plugins/micromega/.ocamlformat-ignore b/plugins/micromega/.ocamlformat-ignore
new file mode 100644
index 0000000000..157a987754
--- /dev/null
+++ b/plugins/micromega/.ocamlformat-ignore
@@ -0,0 +1 @@
+micromega.ml
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 824abdaf89..1958fff4cc 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -651,10 +651,10 @@ let z_cert_of_pos pos =
in
simplify_cone z_spec (_cert_of_pos pos)
-open Mutils
(** All constraints (initial or derived) have an index and have a justification i.e., proof.
Given a constraint, all the coefficients are always integers.
*)
+open Mutils
open Polynomial
diff --git a/plugins/micromega/certificate.mli b/plugins/micromega/certificate.mli
index d8c9ade04d..cabd36ebb7 100644
--- a/plugins/micromega/certificate.mli
+++ b/plugins/micromega/certificate.mli
@@ -10,36 +10,36 @@
module Mc = Micromega
-val use_simplex : bool ref
(** [use_simplex] is bound to the Coq option Simplex.
If set, use the Simplex method, otherwise use Fourier *)
+val use_simplex : bool ref
type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown
type zres = (Mc.zArithProof, int * Mc.z list) res
type qres = (Mc.q Mc.psatz, int * Mc.q list) res
-val dump_file : string option ref
(** [dump_file] is bound to the Coq option Dump Arith.
If set to some [file], arithmetic goals are dumped in filexxx.v *)
+val dump_file : string option ref
-val q_cert_of_pos : Sos_types.positivstellensatz -> Mc.q Mc.psatz
(** [q_cert_of_pos prf] converts a Sos proof into a rational Coq proof *)
+val q_cert_of_pos : Sos_types.positivstellensatz -> Mc.q Mc.psatz
-val z_cert_of_pos : Sos_types.positivstellensatz -> Mc.z Mc.psatz
(** [z_cert_of_pos prf] converts a Sos proof into an integer Coq proof *)
+val z_cert_of_pos : Sos_types.positivstellensatz -> Mc.z Mc.psatz
-val lia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres
(** [lia enum depth sys] generates an unsat proof for the linear constraints in [sys].
If the Simplex option is set, any failure to find a proof should be considered as a bug. *)
+val lia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres
-val nlia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres
(** [nlia enum depth sys] generates an unsat proof for the non-linear constraints in [sys].
The solver is incomplete -- the problem is undecidable *)
+val nlia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres
-val linear_prover_with_cert : int -> (Mc.q Mc.pExpr * Mc.op1) list -> qres
(** [linear_prover_with_cert depth sys] generates an unsat proof for the linear constraints in [sys].
Over the rationals, the solver is complete. *)
+val linear_prover_with_cert : int -> (Mc.q Mc.pExpr * Mc.op1) list -> qres
-val nlinear_prover : int -> (Mc.q Mc.pExpr * Mc.op1) list -> qres
(** [nlinear depth sys] generates an unsat proof for the non-linear constraints in [sys].
The solver is incompete -- the problem is decidable. *)
+val nlinear_prover : int -> (Mc.q Mc.pExpr * Mc.op1) list -> qres
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 87778f7f7b..43f6f5a35e 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 + List.assoc (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 (List.assoc 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
@@ -1473,6 +1476,9 @@ let parse_goal gl parse_arith (env : Env.t) hyps term =
let lhyps, env, tg = parse_hyps gl parse_arith env tg hyps in
(lhyps, f, env)
+(**
+ * The datastructures that aggregate theory-dependent proof values.
+ *)
type ('synt_c, 'prf) domain_spec =
{ typ : EConstr.constr
; (* is the type of the interpretation domain - Z, Q, R*)
@@ -1480,10 +1486,8 @@ type ('synt_c, 'prf) domain_spec =
; (* is the type of the syntactic coeffs - Z , Q , Rcst *)
dump_coeff : 'synt_c -> EConstr.constr
; proof_typ : EConstr.constr
- ; dump_proof : 'prf -> EConstr.constr }
-(**
- * The datastructures that aggregate theory-dependent proof values.
- *)
+ ; dump_proof : 'prf -> EConstr.constr
+ ; coeff_eq : 'synt_c -> 'synt_c -> bool }
let zz_domain_spec =
lazy
@@ -1491,7 +1495,8 @@ let zz_domain_spec =
; coeff = Lazy.force coq_Z
; dump_coeff = dump_z
; proof_typ = Lazy.force coq_proofTerm
- ; dump_proof = dump_proof_term }
+ ; dump_proof = dump_proof_term
+ ; coeff_eq = Mc.zeq_bool }
let qq_domain_spec =
lazy
@@ -1499,7 +1504,8 @@ let qq_domain_spec =
; coeff = Lazy.force coq_Q
; dump_coeff = dump_q
; proof_typ = Lazy.force coq_QWitness
- ; dump_proof = dump_psatz coq_Q dump_q }
+ ; dump_proof = dump_psatz coq_Q dump_q
+ ; coeff_eq = Mc.qeq_bool }
let max_tag f =
1 + Tag.to_int (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) f (Tag.from 0))
@@ -1603,7 +1609,12 @@ 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 (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
+ in
let compact_proof (old_cl : 'cst clause) (prf, prover) (new_cl : 'cst clause)
=
let new_cl = List.mapi (fun i (f, _) -> (f, i)) new_cl in
@@ -1611,7 +1622,7 @@ let compact_proofs (cnf_ff : 'cst cnf) res (cnf_ff' : 'cst cnf) =
let formula =
try fst (List.nth old_cl i) with Failure _ -> failwith "bad old index"
in
- List.assoc formula new_cl
+ CList.assoc_f eq_formula formula new_cl
in
(* if debug then
begin
@@ -1641,7 +1652,13 @@ let compact_proofs (cnf_ff : 'cst cnf) res (cnf_ff' : 'cst cnf) =
(new_cl : 'cst clause) =
let hyps_idx = prover.hyps prf in
let hyps = selecti hyps_idx old_cl in
- is_sublist ( = ) hyps new_cl
+ 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)
+ (* FIXME: what equality should we use here? *)
+ in
+ is_sublist eq hyps new_cl
in
let cnf_res = List.combine cnf_ff res in
(* we get pairs clause * proof *)
@@ -1798,7 +1815,7 @@ let micromega_tauto pre_process cnf spec prover env
| None -> failwith "abstraction is wrong"
| Some res -> ()
end ; *)
- let res' = compact_proofs cnf_ff res cnf_ff' in
+ let res' = compact_proofs spec.coeff_eq cnf_ff res cnf_ff' in
let ff', res', ids = (ff', res', Mc.ids_of_formula ff') in
let res' = dump_list spec.proof_typ spec.dump_proof res' in
Prf (ids, ff', res')
@@ -1946,7 +1963,8 @@ let micromega_genr prover tac =
; coeff = Lazy.force coq_Rcst
; dump_coeff = dump_q
; proof_typ = Lazy.force coq_QWitness
- ; dump_proof = dump_psatz coq_Q dump_q }
+ ; dump_proof = dump_psatz coq_Q dump_q
+ ; coeff_eq = Mc.qeq_bool }
in
Proofview.Goal.enter (fun gl ->
let sigma = Tacmach.New.project gl in
@@ -1979,7 +1997,7 @@ let micromega_genr prover tac =
| Prf (ids, ff', res') ->
let ff, ids =
formula_hyps_concl
- (List.filter (fun (n, _) -> List.mem n ids) hyps)
+ (List.filter (fun (n, _) -> CList.mem_f Id.equal n ids) hyps)
concl
in
let ff' = abstract_wrt_formula ff' ff in
diff --git a/plugins/micromega/coq_micromega.mli b/plugins/micromega/coq_micromega.mli
index f2f7fd424f..679290891d 100644
--- a/plugins/micromega/coq_micromega.mli
+++ b/plugins/micromega/coq_micromega.mli
@@ -24,5 +24,5 @@ val print_lia_profile : unit -> unit
(** {5 Use Micromega independently from tactics. } *)
-val dump_proof_term : Micromega.zArithProof -> EConstr.t
(** [dump_proof_term] generates the Coq representation of a Micromega proof witness *)
+val dump_proof_term : Micromega.zArithProof -> EConstr.t
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index 5ed7d9865e..3d1770a541 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -17,8 +17,8 @@ open Vect
let debug = false
let compare_float (p : float) q = pervasives_compare p q
-open Itv
(** Implementation of intervals *)
+open Itv
type vector = Vect.t
@@ -47,8 +47,8 @@ and cstr_info = {bound : interval; prf : proof; pos : int; neg : int}
[v] is an upper-bound of the set of variables which appear in [s].
*)
-exception SystemContradiction of proof
(** To be thrown when a system has no solution *)
+exception SystemContradiction of proof
(** Pretty printing *)
let rec pp_proof o prf =
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index f9a23751bf..27b917383b 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -385,7 +385,13 @@ module Hash = struct
let int_of_eq_op1 =
Mc.(function Equal -> 0 | NonEqual -> 1 | Strict -> 2 | NonStrict -> 3)
- let eq_op1 o1 o2 = int_of_eq_op1 o1 = int_of_eq_op1 o2
+ let int_of_eq_op2 =
+ 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)
let hash_op1 h o = combine h (int_of_eq_op1 o)
let rec eq_positive p1 p2 =
diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli
index 5e0c913996..09d55cf073 100644
--- a/plugins/micromega/mutils.mli
+++ b/plugins/micromega/mutils.mli
@@ -26,8 +26,8 @@ end
module IMap : sig
include Map.S with type key = int
- val from : key -> 'elt t -> 'elt t
(** [from k m] returns the submap of [m] with keys greater or equal k *)
+ val from : key -> 'elt t -> 'elt t
end
module Cmp : sig
@@ -43,6 +43,7 @@ module Tag : sig
val max : t -> t -> t
val from : int -> t
val to_int : t -> int
+ val compare : t -> t -> int
end
module TagSet : CSig.SetS with type elt = Tag.t
@@ -73,6 +74,7 @@ end
module Hash : sig
val eq_op1 : Micromega.op1 -> Micromega.op1 -> bool
+ val eq_op2 : Micromega.op2 -> Micromega.op2 -> bool
val eq_positive : Micromega.positive -> Micromega.positive -> bool
val eq_z : Micromega.z -> Micromega.z -> bool
val eq_q : Micromega.q -> Micromega.q -> bool
diff --git a/plugins/micromega/persistent_cache.mli b/plugins/micromega/persistent_cache.mli
index 16d3f0a517..08e8c53757 100644
--- a/plugins/micromega/persistent_cache.mli
+++ b/plugins/micromega/persistent_cache.mli
@@ -14,25 +14,25 @@ module type PHashtable = sig
type 'a t
type key
- val open_in : string -> 'a t
(** [open_in f] rebuilds a table from the records stored in file [f].
As marshaling is not type-safe, it might segfault.
*)
+ val open_in : string -> 'a t
- val find : 'a t -> key -> 'a
(** find has the specification of Hashtable.find *)
+ val find : 'a t -> key -> 'a
- val add : 'a t -> key -> 'a -> unit
(** [add tbl key elem] adds the binding [key] [elem] to the table [tbl].
(and writes the binding to the file associated with [tbl].)
If [key] is already bound, raises KeyAlreadyBound *)
+ val add : 'a t -> key -> 'a -> unit
- val memo : string -> (key -> 'a) -> key -> 'a
(** [memo cache f] returns a memo function for [f] using file [cache] as persistent table.
Note that the cache will only be loaded when the function is used for the first time *)
+ val memo : string -> (key -> 'a) -> key -> 'a
- val memo_cond : string -> (key -> bool) -> (key -> 'a) -> key -> 'a
(** [memo cache cond f] only use the cache if [cond k] holds for the key [k]. *)
+ val memo_cond : string -> (key -> bool) -> (key -> 'a) -> key -> 'a
end
module PHashtable (Key : HashedType) : PHashtable with type key = Key.t
diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli
index bdd77440bb..9c09f76691 100644
--- a/plugins/micromega/polynomial.mli
+++ b/plugins/micromega/polynomial.mli
@@ -17,52 +17,52 @@ val max_nb_cstr : int ref
type var = int
module Monomial : sig
- type t
(** A monomial is represented by a multiset of variables *)
+ type t
- val fold : (var -> int -> 'a -> 'a) -> t -> 'a -> 'a
(** [fold f m acc]
folds over the variables with multiplicities *)
+ val fold : (var -> int -> 'a -> 'a) -> t -> 'a -> 'a
- val degree : t -> int
(** [degree m] is the sum of the degrees of each variable *)
+ val degree : t -> int
- val const : t
(** [const]
@return the empty monomial i.e. without any variable *)
+ val const : t
val is_const : t -> bool
- val var : var -> t
(** [var x]
@return the monomial x^1 *)
+ val var : var -> t
- val prod : t -> t -> t
(** [prod n m]
@return the monomial n*m *)
+ val prod : t -> t -> t
- val sqrt : t -> t option
(** [sqrt m]
@return [Some r] iff r^2 = m *)
+ val sqrt : t -> t option
- val is_var : t -> bool
(** [is_var m]
@return [true] iff m = x^1 for some variable x *)
+ val is_var : t -> bool
- val get_var : t -> var option
(** [get_var m]
@return [x] iff m = x^1 for variable x *)
+ val get_var : t -> var option
- val div : t -> t -> t * int
(** [div m1 m2]
@return a pair [mr,n] such that mr * (m2)^n = m1 where n is maximum *)
+ val div : t -> t -> t * int
- val compare : t -> t -> int
(** [compare m1 m2] provides a total order over monomials*)
+ val compare : t -> t -> int
- val variables : t -> ISet.t
(** [variables m]
@return the set of variables with (strictly) positive multiplicities *)
+ val variables : t -> ISet.t
end
module MonMap : sig
@@ -82,36 +82,36 @@ module Poly : sig
type t
- val constant : Q.t -> t
(** [constant c]
@return the constant polynomial c *)
+ val constant : Q.t -> t
- val variable : var -> t
(** [variable x]
@return the polynomial 1.x^1 *)
+ val variable : var -> t
- val addition : t -> t -> t
(** [addition p1 p2]
@return the polynomial p1+p2 *)
+ val addition : t -> t -> t
- val product : t -> t -> t
(** [product p1 p2]
@return the polynomial p1*p2 *)
+ val product : t -> t -> t
- val uminus : t -> t
(** [uminus p]
@return the polynomial -p i.e product by -1 *)
+ val uminus : t -> t
- val get : Monomial.t -> t -> Q.t
(** [get mi p]
@return the coefficient ai of the monomial mi. *)
+ val get : Monomial.t -> t -> Q.t
- val fold : (Monomial.t -> Q.t -> 'a -> 'a) -> t -> 'a -> 'a
(** [fold f p a] folds f over the monomials of p with non-zero coefficient *)
+ val fold : (Monomial.t -> Q.t -> 'a -> 'a) -> t -> 'a -> 'a
- val add : Monomial.t -> Q.t -> t -> t
(** [add m n p]
@return the polynomial n*m + p *)
+ val add : Monomial.t -> Q.t -> t -> t
end
type cstr = {coeffs : Vect.t; op : op; cst : Q.t}
@@ -125,9 +125,9 @@ val eval_op : op -> Q.t -> Q.t -> bool
val opAdd : op -> op -> op
-val is_strict : cstr -> bool
(** [is_strict c]
@return whether the constraint is strict i.e. c.op = Gt *)
+val is_strict : cstr -> bool
exception Strict
@@ -147,70 +147,70 @@ module LinPoly : sig
This is done using the monomial tables of the module MonT. *)
module MonT : sig
- val clear : unit -> unit
(** [clear ()] clears the mapping. *)
+ val clear : unit -> unit
- val reserve : int -> unit
(** [reserve i] reserves the integer i *)
+ val reserve : int -> unit
- val get_fresh : unit -> int
(** [get_fresh ()] return the first fresh variable *)
+ val get_fresh : unit -> int
- val retrieve : int -> Monomial.t
(** [retrieve x]
@return the monomial corresponding to the variable [x] *)
+ val retrieve : int -> Monomial.t
- val register : Monomial.t -> int
(** [register m]
@return the variable index for the monomial m *)
+ val register : Monomial.t -> int
end
- val linpol_of_pol : Poly.t -> t
(** [linpol_of_pol p] linearise the polynomial p *)
+ val linpol_of_pol : Poly.t -> t
- val var : var -> t
(** [var x]
@return 1.y where y is the variable index of the monomial x^1.
*)
+ val var : var -> t
- val coq_poly_of_linpol : (Q.t -> 'a) -> t -> 'a Mc.pExpr
(** [coq_poly_of_linpol c p]
@param p is a multi-variate polynomial.
@param c maps a rational to a Coq polynomial coefficient.
@return the coq expression corresponding to polynomial [p].*)
+ val coq_poly_of_linpol : (Q.t -> 'a) -> t -> 'a Mc.pExpr
- val of_monomial : Monomial.t -> t
(** [of_monomial m]
@returns 1.x where x is the variable (index) for monomial m *)
+ val of_monomial : Monomial.t -> t
- val of_vect : Vect.t -> t
(** [of_vect v]
@returns a1.x1 + ... + an.xn
This is not the identity because xi is the variable index of xi^1
*)
+ val of_vect : Vect.t -> t
- val variables : t -> ISet.t
(** [variables p]
@return the set of variables of the polynomial p
interpreted as a multi-variate polynomial *)
+ val variables : t -> ISet.t
- val is_variable : t -> var option
(** [is_variable p]
@return Some x if p = a.x for a >= 0 *)
+ val is_variable : t -> var option
- val is_linear : t -> bool
(** [is_linear p]
@return whether the multi-variate polynomial is linear. *)
+ val is_linear : t -> bool
- val is_linear_for : var -> t -> bool
(** [is_linear_for x p]
@return true if the polynomial is linear in x
i.e can be written c*x+r where c is a constant and r is independent from x *)
+ val is_linear_for : var -> t -> bool
- val constant : Q.t -> t
(** [constant c]
@return the constant polynomial c
*)
+ val constant : Q.t -> t
(** [search_linear pred p]
@return a variable x such p = a.x + b such that
@@ -219,44 +219,44 @@ module LinPoly : sig
val search_linear : (Q.t -> bool) -> t -> var option
- val search_all_linear : (Q.t -> bool) -> t -> var list
(** [search_all_linear pred p]
@return all the variables x such p = a.x + b such that
p is linear in x i.e x does not occur in b and
a is a constant such that [pred a] *)
+ val search_all_linear : (Q.t -> bool) -> t -> var list
val get_bound : t -> Vect.Bound.t option
- val product : t -> t -> t
(** [product p q]
@return the product of the polynomial [p*q] *)
+ val product : t -> t -> t
- val factorise : var -> t -> t * t
(** [factorise x p]
@return [a,b] such that [p = a.x + b]
and [x] does not occur in [b] *)
+ val factorise : var -> t -> t * t
- val collect_square : t -> Monomial.t MonMap.t
(** [collect_square p]
@return a mapping m such that m[s] = s^2
for every s^2 that is a monomial of [p] *)
+ val collect_square : t -> Monomial.t MonMap.t
- val monomials : t -> ISet.t
(** [monomials p]
@return the set of monomials. *)
+ val monomials : t -> ISet.t
- val degree : t -> int
(** [degree p]
@return return the maximum degree *)
+ val degree : t -> int
- val pp_var : out_channel -> var -> unit
(** [pp_var o v] pretty-prints a monomial indexed by v. *)
+ val pp_var : out_channel -> var -> unit
- val pp : out_channel -> t -> unit
(** [pp o p] pretty-prints a polynomial. *)
+ val pp : out_channel -> t -> unit
- val pp_goal : string -> out_channel -> (t * op) list -> unit
(** [pp_goal typ o l] pretty-prints the list of constraints as a Coq goal. *)
+ val pp_goal : string -> out_channel -> (t * op) list -> unit
end
module ProofFormat : sig
@@ -318,47 +318,47 @@ val opMult : op -> op -> op
module WithProof : sig
type t = (LinPoly.t * op) * ProofFormat.prf_rule
- exception InvalidProof
(** [InvalidProof] is raised if the operation is invalid. *)
+ exception InvalidProof
val compare : t -> t -> int
val annot : string -> t -> t
val of_cstr : cstr * ProofFormat.prf_rule -> t
- val output : out_channel -> t -> unit
(** [out_channel chan c] pretty-prints the constraint [c] over the channel [chan] *)
+ val output : out_channel -> t -> unit
val output_sys : out_channel -> t list -> unit
- val zero : t
(** [zero] represents the tautology (0=0) *)
+ val zero : t
- val const : Q.t -> t
(** [const n] represents the tautology (n>=0) *)
+ val const : Q.t -> t
- val product : t -> t -> t
(** [product p q]
@return the polynomial p*q with its sign and proof *)
+ val product : t -> t -> t
- val addition : t -> t -> t
(** [addition p q]
@return the polynomial p+q with its sign and proof *)
+ val addition : t -> t -> t
- val mult : LinPoly.t -> t -> t
(** [mult p q]
@return the polynomial p*q with its sign and proof.
@raise InvalidProof if p is not a constant and p is not an equality *)
+ val mult : LinPoly.t -> t -> t
- val cutting_plane : t -> t option
(** [cutting_plane p] does integer reasoning and adjust the constant to be integral *)
+ val cutting_plane : t -> t option
- val linear_pivot : t list -> t -> Vect.var -> t -> t option
(** [linear_pivot sys p x q]
@return the polynomial [q] where [x] is eliminated using the polynomial [p]
The pivoting operation is only defined if
- p is linear in x i.e p = a.x+b and x neither occurs in a and b
- The pivoting also requires some sign conditions for [a]
*)
+ val linear_pivot : t list -> t -> Vect.var -> t -> t option
(** [subst sys] performs the equivalent of the 'subst' tactic of Coq.
For every p=0 \in sys such that p is linear in x with coefficient +/- 1
@@ -371,8 +371,8 @@ module WithProof : sig
val subst : t list -> t list
- val subst1 : t list -> t list
(** [subst1 sys] performs a single substitution *)
+ val subst1 : t list -> t list
val saturate_subst : bool -> t list -> t list
val is_substitution : bool -> t -> var option
diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml
index 702099a95d..eaa26ded62 100644
--- a/plugins/micromega/simplex.ml
+++ b/plugins/micromega/simplex.ml
@@ -62,9 +62,9 @@ let get_profile_info () =
type iset = unit IMap.t
-type tableau = Vect.t IMap.t
(** Mapping basic variables to their equation.
All variables >= than a threshold rst are restricted.*)
+type tableau = Vect.t IMap.t
module Restricted = struct
type t =
@@ -366,9 +366,9 @@ let push_real (opt : bool) (nw : var) (v : Vect.t) (rst : Restricted.t)
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'))) )
-open Mutils
(** One complication is that equalities needs some pre-processing.
*)
+open Mutils
open Polynomial
diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml
index 1742f81b34..3e0b1f2cd9 100644
--- a/plugins/micromega/vect.ml
+++ b/plugins/micromega/vect.ml
@@ -12,14 +12,15 @@ open NumCompat
open Q.Notations
open Mutils
-type var = int
(** [t] is the type of vectors.
A vector [(x1,v1) ; ... ; (xn,vn)] is such that:
- variables indexes are ordered (x1 < ... < xn
- values are all non-zero
*)
+type var = int
-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,25 @@ 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 +56,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 +84,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 +93,71 @@ let to_list m =
let rec xto_list i l =
match l with
| [] -> []
- | (x, v) :: l' ->
- if 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 (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 +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 (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 +176,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 +185,49 @@ 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 ->
- if 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, 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 +235,12 @@ 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 +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 (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 +276,26 @@ let dotproduct v1 v2 =
let rec dot acc v1 v2 =
match (v1, v2) with
| [], _ | _, [] -> acc
- | (x1, n1) :: v1', (x2, n2) :: v2' ->
- if x1 == x2 then dot (acc +/ (n1 */ n2)) v1' 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 (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 +303,9 @@ 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 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
diff --git a/plugins/micromega/vect.mli b/plugins/micromega/vect.mli
index 8a26337602..9db6c075f8 100644
--- a/plugins/micromega/vect.mli
+++ b/plugins/micromega/vect.mli
@@ -11,10 +11,9 @@
open NumCompat
open Mutils
-type var = int
(** Variables are simply (positive) integers. *)
+type var = int
-type t
(** The type of vectors or equivalently linear expressions.
The current implementation is using association lists.
A list [(0,c),(x1,ai),...,(xn,an)] represents the linear expression
@@ -24,6 +23,7 @@ type t
Moreover, the representation is spare and variables with a zero coefficient
are not represented.
*)
+type t
type vector = t
@@ -38,147 +38,147 @@ val compare : t -> t -> int
(** {1 Basic accessors and utility functions} *)
-val pp_gen : (out_channel -> var -> unit) -> out_channel -> t -> unit
(** [pp_gen pp_var o v] prints the representation of the vector [v] over the channel [o] *)
+val pp_gen : (out_channel -> var -> unit) -> out_channel -> t -> unit
-val pp : out_channel -> t -> unit
(** [pp o v] prints the representation of the vector [v] over the channel [o] *)
+val pp : out_channel -> t -> unit
-val pp_smt : out_channel -> t -> unit
(** [pp_smt o v] prints the representation of the vector [v] over the channel [o] using SMTLIB conventions *)
+val pp_smt : out_channel -> t -> unit
-val variables : t -> ISet.t
(** [variables v] returns the set of variables with non-zero coefficients *)
+val variables : t -> ISet.t
-val get_cst : t -> Q.t
(** [get_cst v] returns c i.e. the coefficient of the variable zero *)
+val get_cst : t -> Q.t
-val decomp_cst : t -> Q.t * t
(** [decomp_cst v] returns the pair (c,a1.x1+...+an.xn) *)
+val decomp_cst : t -> Q.t * t
-val decomp_at : int -> t -> Q.t * t
(** [decomp_cst v] returns the pair (ai, ai+1.xi+...+an.xn) *)
+val decomp_at : int -> t -> Q.t * t
val decomp_fst : t -> (var * Q.t) * t
-val cst : Q.t -> t
(** [cst c] returns the vector v=c+0.x1+...+0.xn *)
+val cst : Q.t -> t
-val is_constant : t -> bool
(** [is_constant v] holds if [v] is a constant vector i.e. v=c+0.x1+...+0.xn
*)
+val is_constant : t -> bool
-val null : t
(** [null] is the empty vector i.e. 0+0.x1+...+0.xn *)
+val null : t
-val is_null : t -> bool
(** [is_null v] returns whether [v] is the [null] vector i.e [equal v null] *)
+val is_null : t -> bool
-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 get : var -> t -> Q.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 set : var -> Q.t -> t -> t
-val mkvar : var -> t
(** [mkvar xi] returns 1.xi *)
+val mkvar : var -> t
-val update : var -> (Q.t -> Q.t) -> t -> t
(** [update xi f v] returns c+a1.x1+...+f(ai).xi+...+an.xn *)
+val update : var -> (Q.t -> Q.t) -> t -> t
-val fresh : t -> int
(** [fresh v] return the fresh variable with index 1+ max (variables v) *)
+val fresh : t -> int
-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 choose : t -> (var * Q.t * t) option
-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 from_list : Q.t list -> t
-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 *)
+val to_list : t -> Q.t list
-val decr_var : int -> t -> t
(** [decr_var i v] decrements the variables of the vector [v] by the amount [i].
Beware, it is only defined if all the variables of v are greater than i
*)
+val decr_var : int -> t -> t
-val incr_var : int -> t -> t
(** [incr_var i v] increments the variables of the vector [v] by the amount [i].
*)
+val incr_var : int -> t -> t
-val gcd : t -> Z.t
(** [gcd v] returns gcd(num(c),num(a1),...,num(an)) where num extracts
the numerator of a rational value. *)
+val gcd : t -> Z.t
-val normalise : t -> t
(** [normalise v] returns a vector with only integer coefficients *)
+val normalise : t -> t
(** {1 Linear arithmetics} *)
-val add : t -> t -> t
(** [add v1 v2] is vector addition.
@param v1 is of the form c +a1.x1 +...+an.xn
@param v2 is of the form c'+a1'.x1 +...+an'.xn
@return c1+c1'+ (a1+a1').x1 + ... + (an+an').xn
*)
+val add : t -> 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 : Q.t -> 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 mul_add : Q.t -> t -> Q.t -> t -> t
-val subst : int -> t -> t -> t
(** [subst x v v'] replaces x by v in vector v' *)
+val subst : int -> t -> 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 div : Q.t -> t -> t
-val uminus : t -> t
(** [uminus v] @return -v the opposite vector of v i.e. (-1).v *)
+val uminus : t -> t
(** {1 Iterators} *)
-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 : ('acc -> var -> Q.t -> 'acc) -> 'acc -> t -> 'acc
-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 fold_error : ('acc -> var -> Q.t -> 'acc option) -> 'acc -> t -> 'acc 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 find : (var -> Q.t -> 'c option) -> t -> 'c option
-val for_all : (var -> Q.t -> bool) -> t -> bool
(** [for_all p v] returns /\_{i>=0} (f xi ai) *)
+val for_all : (var -> Q.t -> bool) -> t -> bool
-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 exists2 : (Q.t -> Q.t -> bool) -> t -> t -> (var * Q.t * Q.t) option
-val dotproduct : t -> t -> Q.t
(** [dotproduct v1 v2] is the dot product of v1 and v2. *)
+val dotproduct : t -> t -> Q.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 : Q.t; var : var; coeff : Q.t}
(** represents a0 + ai.xi *)
+ type t = {cst : Q.t; var : var; coeff : Q.t}
val of_vect : vector -> t option
end
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 53a58342d2..41579d5792 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -326,20 +326,20 @@ type term_kind = Application of EConstr.constr | OtherTerm of EConstr.constr
module type Elt = sig
type elt
- val name : string
(** name *)
+ val name : string
val table : (term_kind * decl_kind) HConstr.t ref
val cast : elt decl -> decl_kind
val dest : decl_kind -> elt decl option
- val get_key : int
(** [get_key] is the type-index used as key for the instance *)
+ val get_key : int
- val mk_elt : Evd.evar_map -> EConstr.t -> EConstr.t array -> elt
(** [mk_elt evd i [a0,..,an] returns the element of the table
built from the type-instance i and the arguments (type indexes and projections)
of the type-class constructor. *)
+ val mk_elt : Evd.evar_map -> EConstr.t -> EConstr.t array -> elt
(* val arity : int*)
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 01:43:24 +0000