blob: 3ddb6e51b99039134542b90a5498dfa0ffb9bcc9 (
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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2022 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
val negb : bool -> bool
type 'a list =
| Nil
| Cons of 'a * 'a list
val existsb : ('a1 -> bool) -> 'a1 list -> bool
type int = ExtrNative.uint
val lsl0 : int -> int -> int
val lsr0 : int -> int -> int
val land0 : int -> int -> int
val lxor0 : int -> int -> int
val sub : int -> int -> int
val eqb : int -> int -> bool
val foldi_cont :
(int -> ('a1 -> 'a2) -> 'a1 -> 'a2) -> int -> int -> ('a1 -> 'a2) -> 'a1 ->
'a2
val foldi_down_cont :
(int -> ('a1 -> 'a2) -> 'a1 -> 'a2) -> int -> int -> ('a1 -> 'a2) -> 'a1 ->
'a2
val is_zero : int -> bool
val is_even : int -> bool
val compare : int -> int -> ExtrNative.comparison
val foldi : (int -> 'a1 -> 'a1) -> int -> int -> 'a1 -> 'a1
val foldi_down : (int -> 'a1 -> 'a1) -> int -> int -> 'a1 -> 'a1
type 'a array = 'a ExtrNative.parray
val make : int -> 'a1 -> 'a1 array
val get : 'a1 array -> int -> 'a1
val set : 'a1 array -> int -> 'a1 -> 'a1 array
val length : 'a1 array -> int
val to_list : 'a1 array -> 'a1 list
val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 array -> 'a1
val foldi_right : (int -> 'a1 -> 'a2 -> 'a2) -> 'a1 array -> 'a2 -> 'a2
module Valuation :
sig
type t = int -> bool
end
module Var :
sig
val _true : int
val _false : int
val interp : Valuation.t -> int -> bool
end
module Lit :
sig
val is_pos : int -> bool
val blit : int -> int
val lit : int -> int
val neg : int -> int
val nlit : int -> int
val _true : int
val _false : int
val eqb : int -> int -> bool
val interp : Valuation.t -> int -> bool
end
module C :
sig
type t = int list
val interp : Valuation.t -> t -> bool
val _true : t
val is_false : t -> bool
val or_aux : (t -> t -> t) -> int -> t -> t -> int list
val coq_or : t -> t -> t
val resolve_aux : (t -> t -> t) -> int -> t -> t -> t
val resolve : t -> t -> t
end
module S :
sig
type t = C.t array
val get : t -> int -> C.t
val internal_set : t -> int -> C.t -> t
val make : int -> t
val insert : int -> int list -> int list
val sort_uniq : int list -> int list
val set_clause : t -> int -> C.t -> t
val set_resolve : t -> int -> int array -> t
end
val afold_left :
'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a2 -> 'a1) -> 'a2 array -> 'a1
type 'step _trace_ = 'step array array
val _checker_ :
(S.t -> 'a1 -> S.t) -> (C.t -> bool) -> S.t -> 'a1 _trace_ -> int -> bool
module Sat_Checker :
sig
type step =
| Res of int * int array
val step_rect : (int -> int array -> 'a1) -> step -> 'a1
val step_rec : (int -> int array -> 'a1) -> step -> 'a1
val resolution_checker :
(C.t -> bool) -> S.t -> step _trace_ -> int -> bool
type dimacs = int array array
val coq_C_interp_or : Valuation.t -> int array -> bool
val valid : Valuation.t -> dimacs -> bool
type certif =
| Certif of int * step _trace_ * int
val certif_rect : (int -> step _trace_ -> int -> 'a1) -> certif -> 'a1
val certif_rec : (int -> step _trace_ -> int -> 'a1) -> certif -> 'a1
val add_roots : S.t -> dimacs -> S.t
val checker : dimacs -> certif -> bool
val interp_var : (int -> bool) -> int -> bool
end
|
