1 files changed, 92 insertions, 0 deletions
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli
new file mode 100644
index 0000000..b90e3ff
--- /dev/null
+++ b/src/trace/smtCommands.mli
@@ -0,0 +1,92 @@
+val euf_checker_modules : string list list
+val certif_ops :
+  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
+val cCertif : Term.constr lazy_t
+val ccertif : Term.constr lazy_t
+val cchecker : Term.constr lazy_t
+val cchecker_correct : Term.constr lazy_t
+val cchecker_b_correct : Term.constr lazy_t
+val cchecker_b : Term.constr lazy_t
+val cchecker_eq_correct : Term.constr lazy_t
+val cchecker_eq : Term.constr lazy_t
+val compute_roots :
+  SmtAtom.Form.t list -> SmtAtom.Form.t SmtCertif.clause -> int list
+val interp_uf :
+  (int, Term.constr) Hashtbl.t ->
+  (int, Term.constr) Hashtbl.t -> SmtAtom.Form.t list -> Term.constr
+val interp_conseq_uf :
+  SmtAtom.Form.t list list * SmtAtom.Form.t list -> Term.types
+val print_assm : Term.constr -> unit
+val parse_certif :
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
+  SmtAtom.Form.reify * SmtAtom.Form.t list * int *
+  SmtAtom.Form.t SmtCertif.clause -> unit
+val interp_roots : SmtAtom.Form.t list -> Term.constr
+val theorem :
+  Names.identifier ->
+  SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
+  SmtAtom.Form.reify * SmtAtom.Form.t list * int *
+  SmtAtom.Form.t SmtCertif.clause -> unit
+val checker :
+  SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
+  SmtAtom.Form.reify * SmtAtom.Form.t list * int *
+  SmtAtom.Form.t SmtCertif.clause -> unit
+val build_body :
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify ->
+  Term.constr ->
+  Term.constr ->
+  int * SmtAtom.Form.t SmtCertif.clause ->
+  Term.constr * Term.constr * (Names.identifier * Term.types) list
+val build_body_eq :
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify ->
+  Term.constr ->
+  Term.constr ->
+  Term.constr ->
+  int * SmtAtom.Form.t SmtCertif.clause ->
+  Term.constr * Term.constr * (Names.identifier * Term.types) list
+val get_arguments : Term.constr -> Term.constr * Term.constr
+val make_proof :
+  ('a ->
+   'b ->
+   SmtAtom.Form.t -> SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> 'c) ->
+  'a -> 'b -> SmtAtom.Form.reify -> SmtAtom.Form.t -> 'c
+val core_tactic :
+  (SmtAtom.Btype.reify_tbl ->
+   SmtAtom.Op.reify_tbl ->
+   SmtAtom.Form.t ->
+   SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
+   int * SmtAtom.Form.t SmtCertif.clause) ->
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify ->
+  Environ.env -> Evd.evar_map -> Term.constr -> Proof_type.tactic
+val tactic :
+  (SmtAtom.Btype.reify_tbl ->
+   SmtAtom.Op.reify_tbl ->
+   SmtAtom.Form.t ->
+   SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
+   int * SmtAtom.Form.t SmtCertif.clause) ->
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Proof_type.tactic