diff options
| author | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2017-11-24 18:06:20 +0100 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2017-11-24 18:06:20 +0100 |
| commit | a11eaaddc674c8dbce54c0a0c3ceb1059a0059f0 (patch) | |
| tree | 4a934a82dc23b9fa8d0089dc2a95cbbe820733ca /src/extraction/verit_checker.mli | |
| parent | 6566176e1f87838bada8c04ba80e608e8c7e958f (diff) | |
| download | smtcoq-a11eaaddc674c8dbce54c0a0c3ceb1059a0059f0.tar.gz smtcoq-a11eaaddc674c8dbce54c0a0c3ceb1059a0059f0.zip | |
- auto-generated mli files for future documentation
- new Makefiles to handle these mli
Diffstat (limited to 'src/extraction/verit_checker.mli')
| -rw-r--r-- | src/extraction/verit_checker.mli | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/src/extraction/verit_checker.mli b/src/extraction/verit_checker.mli new file mode 100644 index 0000000..3c43d22 --- /dev/null +++ b/src/extraction/verit_checker.mli @@ -0,0 +1,45 @@ +module Mc = Structures.Micromega_plugin_Certificate.Mc +val mkInt : int -> ExtrNative.uint +val mkArray : 'a array -> 'a ExtrNative.parray +val dump_nat : Mc.nat -> Smt_checker.nat +val dump_positive : Mc.positive -> Smt_checker.positive +val dump_z : Mc.z -> Smt_checker.z +val dump_pol : Mc.z Mc.pol -> Smt_checker.z Smt_checker.pol +val dump_psatz : Mc.z Mc.psatz -> Smt_checker.z Smt_checker.psatz +val dump_list : ('a -> 'b) -> 'a list -> 'b Smt_checker.list +val dump_proof_term : Micromega.zArithProof -> Smt_checker.zArithProof +val to_coq : + ('a -> Smt_checker.int) -> + 'a SmtCertif.clause -> + Smt_checker.Euf_Checker.step ExtrNative.parray ExtrNative.parray * + 'a SmtCertif.clause +val btype_to_coq : SmtAtom.btype -> Smt_checker.Typ.coq_type +val c_to_coq : SmtAtom.cop -> Smt_checker.Atom.cop +val u_to_coq : SmtAtom.uop -> Smt_checker.Atom.unop +val b_to_coq : SmtAtom.bop -> Smt_checker.Atom.binop +val n_to_coq : SmtAtom.nop -> Smt_checker.Typ.coq_type +val i_to_coq : SmtAtom.indexed_op -> ExtrNative.uint +val a_to_coq : SmtAtom.atom -> Smt_checker.Atom.atom +val atom_interp_tbl : + SmtAtom.Atom.reify_tbl -> Smt_checker.Atom.atom ExtrNative.parray +val form_to_coq : SmtAtom.Form.t -> ExtrNative.uint +val args_to_coq : SmtAtom.Form.t array -> ExtrNative.uint ExtrNative.parray +val pf_to_coq : + (SmtAtom.hatom, SmtAtom.Form.t) SmtForm.gen_pform -> Smt_checker.Form.form +val form_interp_tbl : + SmtAtom.Form.reify -> Smt_checker.Form.form ExtrNative.parray +val count_btype : int ref +val count_op : int ref +val declare_sort : Smtlib2_ast.symbol -> SmtAtom.btype +val declare_fun : + Smtlib2_ast.symbol -> + Smtlib2_ast.sort list -> Smtlib2_ast.sort -> SmtAtom.indexed_op +val declare_commands : + SmtAtom.Atom.reify_tbl -> + SmtAtom.Form.reify -> + SmtAtom.Form.t list -> Smtlib2_ast.command -> SmtAtom.Form.t list +val import_smtlib2 : + SmtAtom.Atom.reify_tbl -> + SmtAtom.Form.reify -> string -> SmtAtom.Form.t list +val this_clear_all : unit -> unit +val checker : string -> string -> bool |