Module Micromega_plugin.Micromega
type nat
=
|
O
|
S of nat
type ('a, 'b) sum
=
|
Inl of 'a
|
Inr of 'b
val compOpp : comparison -> comparison
val add : nat -> nat -> nat
val nth : nat -> 'a1 list -> 'a1 -> 'a1
val rev_append : 'a1 list -> 'a1 list -> 'a1 list
val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1
val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1
type positive
=
|
XI of positive
|
XO of positive
|
XH
type n
=
|
N0
|
Npos of positive
type z
=
|
Z0
|
Zpos of positive
|
Zneg of positive
module Pos : sig ... end
module Coq_Pos : sig ... end
module N : sig ... end
val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1
module Z : sig ... end
val p0 : 'a1 -> 'a1 pol
val p1 : 'a1 -> 'a1 pol
val peq : ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> bool
val mkPinj : positive -> 'a1 pol -> 'a1 pol
val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol
val mkPX : 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol
val mkX : 'a1 -> 'a1 -> 'a1 pol
val popp : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol
val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
val paddI : ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val psubI : ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val paddX : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val psubX : 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val padd : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
val psub : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
val pmulC_aux : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol
val pmulC : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol
val pmulI : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val pmul : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
val psquare : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol
type 'c pExpr
=
|
PEc of 'c
|
PEX of positive
|
PEadd of 'c pExpr * 'c pExpr
|
PEsub of 'c pExpr * 'c pExpr
|
PEmul of 'c pExpr * 'c pExpr
|
PEopp of 'c pExpr
|
PEpow of 'c pExpr * n
val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol
val ppow_pos : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol
val ppow_N : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol
val norm_aux : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
type ('tA, 'tX, 'aA, 'aF) gFormula
=
|
TT
|
FF
|
X of 'tX
|
A of 'tA * 'aA
|
Cj of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
|
D of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
|
N of ('tA, 'tX, 'aA, 'aF) gFormula
|
I of ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option * ('tA, 'tX, 'aA, 'aF) gFormula
val mapX : ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula
val foldA : ('a5 -> 'a3 -> 'a5) -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5
val cons_id : 'a1 option -> 'a1 list -> 'a1 list
val ids_of_formula : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list
val collect_annot : ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list
type ('x, 'annot) clause
= ('x * 'annot) list
type ('x, 'annot) cnf
= ('x, 'annot) clause list
val cnf_tt : ('a1, 'a2) cnf
val cnf_ff : ('a1, 'a2) cnf
val add_term : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> ('a1, 'a2) clause option
val or_clause : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) clause -> ('a1, 'a2) clause option
val xor_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
val or_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
val or_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
val and_cnf : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
type ('term, 'annot, 'tX, 'aF) tFormula
= ('term, 'tX, 'annot, 'aF) gFormula
val is_cnf_tt : ('a1, 'a2) cnf -> bool
val is_cnf_ff : ('a1, 'a2) cnf -> bool
val and_cnf_opt : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
val or_cnf_opt : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
val xcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
val radd_term : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> (('a1, 'a2) clause, 'a2 list) sum
val ror_clause : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause -> (('a1, 'a2) clause, 'a2 list) sum
val xror_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list * 'a2 list
val ror_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list * 'a2 list
val ror_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list -> ('a1, 'a2) cnf * 'a2 list
val ror_cnf_opt : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf * 'a2 list
val ratom : ('a1, 'a2) cnf -> 'a2 -> ('a1, 'a2) cnf * 'a2 list
val rxcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 list
type ('term, 'annot, 'tX) to_constrT
=
{
mkTT : 'tX;
mkFF : 'tX;
mkA : 'term -> 'annot -> 'tX;
mkCj : 'tX -> 'tX -> 'tX;
mkD : 'tX -> 'tX -> 'tX;
mkI : 'tX -> 'tX -> 'tX;
mkN : 'tX -> 'tX;
}
val aformula : ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3
val is_X : ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option
val abs_and : ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> (('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula
val abs_or : ('a1, 'a2, 'a3) to_constrT -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> (('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula
val mk_arrow : 'a4 option -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
val abst_form : ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a3, 'a2, 'a4) gFormula
val cnf_checker : (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool
val tauto_checker : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) -> ('a1, __, 'a3, unit0) gFormula -> 'a4 list -> bool
val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
val cltb : ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
type 'c polC
= 'c pol
type op1
=
|
Equal
|
NonEqual
|
Strict
|
NonStrict
type 'c nFormula
= 'c polC * op1
type 'c psatz
=
|
PsatzIn of nat
|
PsatzSquare of 'c polC
|
PsatzMulC of 'c polC * 'c psatz
|
PsatzMulE of 'c psatz * 'c psatz
|
PsatzAdd of 'c psatz * 'c psatz
|
PsatzC of 'c
|
PsatzZ
val map_option : ('a1 -> 'a2 option) -> 'a1 option -> 'a2 option
val map_option2 : ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option
val pexpr_times_nformula : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option
val nformula_times_nformula : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option
val nformula_plus_nformula : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option
val eval_Psatz : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1 nFormula option
val check_inconsistent : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> bool
val check_normalised_formulas : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool
type op2
=
|
OpEq
|
OpNEq
|
OpLe
|
OpGe
|
OpLt
|
OpGt
type 't formula
=
{
flhs : 't pExpr;
fop : op2;
frhs : 't pExpr;
}
val norm : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
val psub0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
val padd0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
val popp0 : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol
val normalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
val xnormalise : ('a1 -> 'a1) -> 'a1 nFormula -> 'a1 nFormula list
val xnegate : ('a1 -> 'a1) -> 'a1 nFormula -> 'a1 nFormula list
val cnf_of_list : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a2 -> ('a1 nFormula, 'a2) cnf
val cnf_normalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf
val cnf_negate : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf
val xdenorm : positive -> 'a1 pol -> 'a1 pExpr
val denorm : 'a1 pol -> 'a1 pExpr
val map_PExpr : ('a2 -> 'a1) -> 'a2 pExpr -> 'a1 pExpr
val map_Formula : ('a2 -> 'a1) -> 'a2 formula -> 'a1 formula
val simpl_cone : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz -> 'a1 psatz
val qeq_bool : q -> q -> bool
val qle_bool : q -> q -> bool
val qplus : q -> q -> q
val qmult : q -> q -> q
val qopp : q -> q
val qminus : q -> q -> q
val qinv : q -> q
val qpower_positive : q -> positive -> q
val qpower : q -> z -> q
val find : 'a1 -> 'a1 t -> positive -> 'a1
val singleton : 'a1 -> positive -> 'a1 -> 'a1 t
val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t
val zeval_const : z pExpr -> z option
val zWeakChecker : z nFormula list -> z psatz -> bool
val psub1 : z pol -> z pol -> z pol
val padd1 : z pol -> z pol -> z pol
val normZ : z pExpr -> z pol
val zunsat : z nFormula -> bool
val zdeduce : z nFormula -> z nFormula -> z nFormula option
val xnnormalise : z formula -> z nFormula
val xnormalise0 : z nFormula -> z nFormula list
val cnf_of_list0 : 'a1 -> z nFormula list -> (z nFormula * 'a1) list list
val normalise0 : z formula -> 'a1 -> (z nFormula, 'a1) cnf
val xnegate0 : z nFormula -> z nFormula list
val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf
val cnfZ : (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 list
val ceiling : z -> z -> z
type zArithProof
=
|
DoneProof
|
RatProof of zWitness * zArithProof
|
CutProof of zWitness * zArithProof
|
EnumProof of zWitness * zWitness * zArithProof list
|
ExProof of positive * zArithProof
val zgcdM : z -> z -> z
val zgcd_pol : z polC -> z * z
val zdiv_pol : z polC -> z -> z polC
val makeCuttingPlane : z polC -> z polC * z
val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option
val nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula
val is_pol_Z0 : z polC -> bool
val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option
val valid_cut_sign : op1 -> bool
val bound_var : positive -> z formula
val mk_eq_pos : positive -> positive -> positive -> z formula
val max_var : positive -> z pol -> positive
val max_var_nformulae : z nFormula list -> positive
val zChecker : z nFormula list -> zArithProof -> bool
val zTautoChecker : z formula bFormula -> zArithProof list -> bool
val qWeakChecker : q nFormula list -> q psatz -> bool
val qnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf
val qnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf
val qunsat : q nFormula -> bool
val qdeduce : q nFormula -> q nFormula -> q nFormula option
val normQ : q pExpr -> q pol
val cnfQ : (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) cnf * 'a1 list
val qTautoChecker : q formula bFormula -> qWitness list -> bool
type rcst
=
|
C0
|
C1
|
CQ of q
|
CZ of z
|
CPlus of rcst * rcst
|
CMinus of rcst * rcst
|
CMult of rcst * rcst
|
CPow of rcst * (z, nat) sum
|
CInv of rcst
|
COpp of rcst
val rWeakChecker : q nFormula list -> q psatz -> bool
val rnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf
val rnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf
val runsat : q nFormula -> bool
val rdeduce : q nFormula -> q nFormula -> q nFormula option
val rTautoChecker : rcst formula bFormula -> rWitness list -> bool