aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/coqTerms.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/trace/coqTerms.mli')
-rw-r--r--src/trace/coqTerms.mli186
1 files changed, 167 insertions, 19 deletions
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
index 7d7fe6a..b21bef8 100644
--- a/src/trace/coqTerms.mli
+++ b/src/trace/coqTerms.mli
@@ -1,14 +1,43 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
val gen_constant : string list list -> string -> Term.constr lazy_t
+
+(* Int63 *)
val cint : Term.constr lazy_t
val ceq63 : Term.constr lazy_t
+
+(* PArray *)
val carray : Term.constr lazy_t
-val positive_modules : string list list
+
+(* nat *)
+val cnat : Term.constr lazy_t
+val cO : Term.constr lazy_t
+val cS : Term.constr lazy_t
+
+(* Positive *)
val cpositive : Term.constr lazy_t
val cxI : Term.constr lazy_t
val cxO : Term.constr lazy_t
val cxH : Term.constr lazy_t
val ceqbP : Term.constr lazy_t
-val z_modules : string list list
+
+(* N *)
+val cN : Term.constr lazy_t
+val cN0 : Term.constr lazy_t
+val cNpos : Term.constr lazy_t
+val cof_nat : Term.constr lazy_t
+
+(* Z *)
val cZ : Term.constr lazy_t
val cZ0 : Term.constr lazy_t
val cZpos : Term.constr lazy_t
@@ -22,7 +51,8 @@ val cleb : Term.constr lazy_t
val cgeb : Term.constr lazy_t
val cgtb : Term.constr lazy_t
val ceqbZ : Term.constr lazy_t
-val bool_modules : string list list
+
+(* Booleans *)
val cbool : Term.constr lazy_t
val ctrue : Term.constr lazy_t
val cfalse : Term.constr lazy_t
@@ -33,43 +63,119 @@ val cnegb : Term.constr lazy_t
val cimplb : Term.constr lazy_t
val ceqb : Term.constr lazy_t
val cifb : Term.constr lazy_t
+val ciff : Term.constr lazy_t
val creflect : Term.constr lazy_t
+
+(* Lists *)
val clist : Term.constr lazy_t
val cnil : Term.constr lazy_t
val ccons : Term.constr lazy_t
+val clength : Term.constr lazy_t
+
+(* Option *)
val coption : Term.constr lazy_t
val cSome : Term.constr lazy_t
val cNone : Term.constr lazy_t
+
+(* Pairs *)
val cpair : Term.constr lazy_t
+val cprod : Term.constr lazy_t
+
+(* Dependent pairs *)
val csigT : Term.constr lazy_t
+
+(* Logical Operators *)
val cnot : Term.constr lazy_t
val ceq : Term.constr lazy_t
val crefl_equal : Term.constr lazy_t
val cconj : Term.constr lazy_t
val cand : Term.constr lazy_t
-val smt_modules : string list list
+
+(* Bit vectors *)
+val cbitvector : Term.constr lazy_t
+val cof_bits : Term.constr lazy_t
+val cbitOf : Term.constr lazy_t
+val cbv_eq : Term.constr lazy_t
+val cbv_not : Term.constr lazy_t
+val cbv_neg : Term.constr lazy_t
+val cbv_and : Term.constr lazy_t
+val cbv_or : Term.constr lazy_t
+val cbv_xor : Term.constr lazy_t
+val cbv_add : Term.constr lazy_t
+val cbv_mult : Term.constr lazy_t
+val cbv_ult : Term.constr lazy_t
+val cbv_slt : Term.constr lazy_t
+val cbv_concat : Term.constr lazy_t
+val cbv_extr : Term.constr lazy_t
+val cbv_zextn : Term.constr lazy_t
+val cbv_sextn : Term.constr lazy_t
+val cbv_shl : Term.constr lazy_t
+val cbv_shr : Term.constr lazy_t
+
+(* Arrays *)
+val cfarray : Term.constr lazy_t
+val cselect : Term.constr lazy_t
+val cstore : Term.constr lazy_t
+val cdiff : Term.constr lazy_t
+val cequalarray : Term.constr lazy_t
+
+(* OrderedType *)
+
+(* SMT_terms *)
val cState_C_t : Term.constr lazy_t
+val cState_S_t : Term.constr lazy_t
+
val cdistinct : Term.constr lazy_t
+
val ctype : Term.constr lazy_t
val cTZ : Term.constr lazy_t
val cTbool : Term.constr lazy_t
val cTpositive : Term.constr lazy_t
+val cTBV : Term.constr lazy_t
+val cTFArray : Term.constr lazy_t
val cTindex : Term.constr lazy_t
-val ctyp_eqb : Term.constr lazy_t
-val cTyp_eqb : Term.constr lazy_t
+
+val cinterp_t : Term.constr lazy_t
+val cdec_interp : Term.constr lazy_t
+val cord_interp : Term.constr lazy_t
+val ccomp_interp : Term.constr lazy_t
+val cinh_interp : Term.constr lazy_t
+
+val cinterp_eqb : Term.constr lazy_t
+
+val ctyp_compdec : Term.constr lazy_t
+val cTyp_compdec : Term.constr lazy_t
+val cunit_typ_compdec : Term.constr lazy_t
val cte_carrier : Term.constr lazy_t
-val cte_eqb : Term.constr lazy_t
-val ctyp_eqb_of_typ_eqb_param : Term.constr lazy_t
-val cunit_typ_eqb : Term.constr lazy_t
+val cte_compdec : Term.constr lazy_t
+val ceqb_of_compdec : Term.constr lazy_t
+val cCompDec : Term.constr lazy_t
+
+val cbool_compdec : Term.constr lazy_t
+val cZ_compdec : Term.constr lazy_t
+val cPositive_compdec : Term.constr lazy_t
+val cBV_compdec : Term.constr lazy_t
+val cFArray_compdec : Term.constr lazy_t
+
val ctval : Term.constr lazy_t
val cTval : Term.constr lazy_t
+
val cCO_xH : Term.constr lazy_t
val cCO_Z0 : Term.constr lazy_t
+val cCO_BV : Term.constr lazy_t
+
val cUO_xO : Term.constr lazy_t
val cUO_xI : Term.constr lazy_t
val cUO_Zpos : Term.constr lazy_t
val cUO_Zneg : Term.constr lazy_t
val cUO_Zopp : Term.constr lazy_t
+val cUO_BVbitOf : Term.constr lazy_t
+val cUO_BVnot : Term.constr lazy_t
+val cUO_BVneg : Term.constr lazy_t
+val cUO_BVextr : Term.constr lazy_t
+val cUO_BVzextn : Term.constr lazy_t
+val cUO_BVsextn : Term.constr lazy_t
+
val cBO_Zplus : Term.constr lazy_t
val cBO_Zminus : Term.constr lazy_t
val cBO_Zmult : Term.constr lazy_t
@@ -78,13 +184,31 @@ val cBO_Zle : Term.constr lazy_t
val cBO_Zge : Term.constr lazy_t
val cBO_Zgt : Term.constr lazy_t
val cBO_eq : Term.constr lazy_t
+val cBO_BVand : Term.constr lazy_t
+val cBO_BVor : Term.constr lazy_t
+val cBO_BVxor : Term.constr lazy_t
+val cBO_BVadd : Term.constr lazy_t
+val cBO_BVmult : Term.constr lazy_t
+val cBO_BVult : Term.constr lazy_t
+val cBO_BVslt : Term.constr lazy_t
+val cBO_BVconcat : Term.constr lazy_t
+val cBO_BVshl : Term.constr lazy_t
+val cBO_BVshr : Term.constr lazy_t
+val cBO_select : Term.constr lazy_t
+val cBO_diffarray : Term.constr lazy_t
+
+val cTO_store : Term.constr lazy_t
+
val cNO_distinct : Term.constr lazy_t
+
val catom : Term.constr lazy_t
val cAcop : Term.constr lazy_t
val cAuop : Term.constr lazy_t
val cAbop : Term.constr lazy_t
+val cAtop : Term.constr lazy_t
val cAnop : Term.constr lazy_t
val cAapp : Term.constr lazy_t
+
val cform : Term.constr lazy_t
val cFatom : Term.constr lazy_t
val cFtrue : Term.constr lazy_t
@@ -96,19 +220,43 @@ val cFxor : Term.constr lazy_t
val cFimp : Term.constr lazy_t
val cFiff : Term.constr lazy_t
val cFite : Term.constr lazy_t
+val cFbbT : Term.constr lazy_t
+
val cis_true : Term.constr lazy_t
+
val cvalid_sat_checker : Term.constr lazy_t
val cinterp_var_sat_checker : Term.constr lazy_t
+
val make_certif_ops :
- string list list ->
- Term.constr array option ->
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t
+ string list list ->
+ Term.constr array option ->
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t
+
+(* Some constructions *)
val ceq_refl_true : Term.constr lazy_t
val eq_refl_true : unit -> Term.constr
-val vm_cast_true : Term.constr -> Term.constr
+val vm_cast_true_no_check : Term.constr -> Term.constr
+val vm_cast_true : Environ.env -> Term.constr -> Term.constr
+val mkNat : int -> Term.constr
+val mkN : int -> Term.constr
+val mk_bv_list : bool list -> Term.constr
+
+(* Reification *)
+val mk_bool : Term.constr -> bool
+val mk_bool_list : Term.constr -> bool list
+val mk_nat : Term.constr -> int
+val mk_N : Term.constr -> int
+val mk_bvsize : Term.constr -> int
generated by cgit (git 2.34.1) at 2024-06-29 00:00:48 +0000