aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.ocamlformat1
-rw-r--r--plugins/micromega/certificate.ml2
-rw-r--r--plugins/micromega/certificate.mli16
-rw-r--r--plugins/micromega/coq_micromega.ml6
-rw-r--r--plugins/micromega/coq_micromega.mli2
-rw-r--r--plugins/micromega/mfourier.ml4
-rw-r--r--plugins/micromega/mutils.mli2
-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.ml2
-rw-r--r--plugins/micromega/vect.mli76
-rw-r--r--plugins/micromega/zify.ml6
13 files changed, 121 insertions, 120 deletions
diff --git a/.ocamlformat b/.ocamlformat
index d5608839fb..6d73a5297f 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -6,3 +6,4 @@ cases-exp-indent=2
field-space=loose
exp-grouping=preserve
break-cases=fit
+doc-comments=before
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 82f8b5b3e2..43f6f5a35e 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1476,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*)
@@ -1485,9 +1488,6 @@ type ('synt_c, 'prf) domain_spec =
; proof_typ : EConstr.constr
; dump_proof : 'prf -> EConstr.constr
; coeff_eq : 'synt_c -> 'synt_c -> bool }
-(**
- * The datastructures that aggregate theory-dependent proof values.
- *)
let zz_domain_spec =
lazy
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.mli b/plugins/micromega/mutils.mli
index 146860ca00..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
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 15f37868f7..3e0b1f2cd9 100644
--- a/plugins/micromega/vect.ml
+++ b/plugins/micromega/vect.ml
@@ -12,12 +12,12 @@ 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 mono = {var : var; coe : Q.t}
type t = mono list
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-01-31 10:23:20 +0000