blob: bdd187c3c25ae4ccc257cab060c0af437d3d86a6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2021 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
val pos_of_int : int -> Structures.Micromega_plugin_Micromega.positive
val z_of_int : int -> Structures.Micromega_plugin_Micromega.z
type my_tbl
val get_atom_var : my_tbl -> SmtAtom.hatom -> int
val create_tbl : int -> my_tbl
val smt_Atom_to_micromega_pos :
SmtAtom.hatom -> Structures.Micromega_plugin_Micromega.positive
val smt_Atom_to_micromega_Z :
SmtAtom.hatom -> Structures.Micromega_plugin_Micromega.z
val smt_Atom_to_micromega_pExpr :
my_tbl ->
SmtAtom.hatom ->
Structures.Micromega_plugin_Micromega.z
Structures.Micromega_plugin_Micromega.pExpr
val smt_binop_to_micromega_formula :
my_tbl ->
SmtAtom.bop ->
SmtAtom.hatom ->
SmtAtom.hatom ->
Structures.Micromega_plugin_Micromega.z
Structures.Micromega_plugin_Micromega.formula
val smt_Atom_to_micromega_formula :
my_tbl ->
SmtAtom.hatom ->
Structures.Micromega_plugin_Micromega.z
Structures.Micromega_plugin_Micromega.formula
val binop_array :
('a -> 'b -> 'c) -> 'a -> ('c -> 'c -> 'c) -> 'c -> 'b array -> 'c
val smt_Form_to_coq_micromega_formula :
my_tbl ->
SmtAtom.Form.t ->
Structures.Micromega_plugin_Micromega.z
Structures.Micromega_plugin_Coq_micromega.formula
val binop_list :
my_tbl ->
(Structures.Micromega_plugin_Micromega.z
Structures.Micromega_plugin_Coq_micromega.formula ->
Structures.Micromega_plugin_Micromega.z
Structures.Micromega_plugin_Coq_micromega.formula ->
Structures.Micromega_plugin_Micromega.z
Structures.Micromega_plugin_Coq_micromega.formula) ->
Structures.Micromega_plugin_Micromega.z
Structures.Micromega_plugin_Coq_micromega.formula ->
SmtAtom.Form.t list ->
Structures.Micromega_plugin_Micromega.z
Structures.Micromega_plugin_Coq_micromega.formula
val smt_clause_to_coq_micromega_formula :
my_tbl ->
SmtAtom.Form.t list ->
Structures.Micromega_plugin_Micromega.z
Structures.Micromega_plugin_Coq_micromega.formula
val build_lia_certif :
SmtAtom.Form.t list ->
my_tbl *
Structures.Micromega_plugin_Micromega.z
Structures.Micromega_plugin_Coq_micromega.formula *
Structures.Micromega_plugin_Certificate.Mc.zArithProof list option
|
