blob: 5d4201b1e91d259d638383586f5c23d7767bb6a0 (
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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
module Atom :
sig
type t = int
val index : 'a -> 'a
val equal : 'a -> 'a -> bool
val is_bool_type : 'a -> bool
type reify_tbl = {
mutable count : int;
tbl : (Term.constr, int) Hashtbl.t;
}
val create : unit -> reify_tbl
val declare : reify_tbl -> Term.constr -> int
val get : reify_tbl -> Term.constr -> int
val atom_tbl : reify_tbl -> Term.constr array
val interp_tbl : reify_tbl -> Term.constr
end
module Form :
sig
type hatom = Atom.t
type t = SmtForm.Make(Atom).t
type pform = (hatom, t) SmtForm.gen_pform
val pform_true : pform
val pform_false : pform
val equal : t -> t -> bool
val to_lit : t -> int
val index : t -> int
val pform : t -> pform
val neg : t -> t
val is_pos : t -> bool
val is_neg : t -> bool
val to_smt :
(Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit
exception NotWellTyped of pform
type reify = SmtForm.Make(Atom).reify
val create : unit -> reify
val clear : reify -> unit
val get : reify -> pform -> t
val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
val flatten : reify -> t -> t
val to_coq : t -> Term.constr
val pform_tbl : reify -> pform array
val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
val interp_tbl : reify -> Term.constr * Term.constr
val nvars : reify -> int
val interp_to_coq :
(hatom -> Term.constr) ->
(int, Term.constr) Hashtbl.t -> t -> Term.constr
end
module Trace :
sig
val share_value : Form.t SmtCertif.clause -> unit
module HashedHeadRes :
sig
type t = Form.t SmtCertif.resolution
val equal :
'a SmtCertif.resolution -> 'b SmtCertif.resolution -> bool
val hash : 'a SmtCertif.resolution -> int
end
module HRtbl :
sig
type key = HashedHeadRes.t
type 'a t = 'a Hashtbl.Make(HashedHeadRes).t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
val common_head :
'a SmtCertif.clause list ->
'b SmtCertif.clause list ->
'a SmtCertif.clause list * 'a SmtCertif.clause list *
'b SmtCertif.clause list
val share_prefix : Form.t SmtCertif.clause -> int -> unit
end
module Cnf :
sig
type form_info =
SmtCnf.MakeCnf(Form).form_info =
Immediate of bool
| Done
| Todo
val info : (int, form_info) Hashtbl.t
val init_last : Form.t SmtCertif.clause
val last : Form.t SmtCertif.clause ref
val cnf_todo : Form.t array list ref
val clear : unit -> unit
val push_cnf : Form.t array -> unit
val get_info : Form.t -> form_info
val set_done : Form.t -> unit
val set_immediate : Form.t -> unit
val test_immediate : Form.t -> bool
val check_trivial : Form.t list -> bool
val link_Other : Form.t SmtCertif.rule -> Form.t list -> unit
val both_lit : Form.t -> Form.t * Form.t
val or_of_imp : Form.t array -> Form.t array
val cnf : Form.t -> unit
exception Cnf_done
val imm_link_Other : Form.t SmtCertif.rule -> Form.t -> unit
val imm_cnf : Form.t SmtCertif.clause -> unit
val make_cnf :
Form.reify -> Form.t SmtCertif.clause -> Form.t SmtCertif.clause
end
|
