1pub const true_: u32 = 1;
4pub const false_: u32 = 0;
5pub const __bool_true_false_are_defined: u32 = 1;
6pub type wchar_t = ::std::os::raw::c_int;
7#[repr(C)]
8#[repr(align(16))]
9#[derive(Debug, Copy, Clone)]
10pub struct max_align_t {
11 pub __clang_max_align_nonce1: ::std::os::raw::c_longlong,
12 pub __bindgen_padding_0: u64,
13 pub __clang_max_align_nonce2: u128,
14}
15#[allow(clippy::unnecessary_operation, clippy::identity_op)]
16const _: () = {
17 ["Size of max_align_t"][::std::mem::size_of::<max_align_t>() - 32usize];
18 ["Alignment of max_align_t"][::std::mem::align_of::<max_align_t>() - 16usize];
19 ["Offset of field: max_align_t::__clang_max_align_nonce1"]
20 [::std::mem::offset_of!(max_align_t, __clang_max_align_nonce1) - 0usize];
21 ["Offset of field: max_align_t::__clang_max_align_nonce2"]
22 [::std::mem::offset_of!(max_align_t, __clang_max_align_nonce2) - 16usize];
23};
24#[repr(C)]
25#[derive(Debug, Copy, Clone)]
26pub struct vampire_term_t {
27 _unused: [u8; 0],
28}
29#[repr(C)]
30#[derive(Debug, Copy, Clone)]
31pub struct vampire_literal_t {
32 _unused: [u8; 0],
33}
34#[repr(C)]
35#[derive(Debug, Copy, Clone)]
36pub struct vampire_formula_t {
37 _unused: [u8; 0],
38}
39#[repr(C)]
40#[derive(Debug, Copy, Clone)]
41pub struct vampire_unit_t {
42 _unused: [u8; 0],
43}
44#[repr(C)]
45#[derive(Debug, Copy, Clone)]
46pub struct vampire_clause_t {
47 _unused: [u8; 0],
48}
49#[repr(C)]
50#[derive(Debug, Copy, Clone)]
51pub struct vampire_problem_t {
52 _unused: [u8; 0],
53}
54pub const vampire_proof_result_t_VAMPIRE_PROOF: vampire_proof_result_t = 0;
55pub const vampire_proof_result_t_VAMPIRE_SATISFIABLE: vampire_proof_result_t = 1;
56pub const vampire_proof_result_t_VAMPIRE_TIMEOUT: vampire_proof_result_t = 2;
57pub const vampire_proof_result_t_VAMPIRE_MEMORY_LIMIT: vampire_proof_result_t = 3;
58pub const vampire_proof_result_t_VAMPIRE_UNKNOWN: vampire_proof_result_t = 4;
59pub const vampire_proof_result_t_VAMPIRE_INCOMPLETE: vampire_proof_result_t = 5;
60#[doc = " Result of a proving attempt"]
61pub type vampire_proof_result_t = ::std::os::raw::c_uint;
62pub const vampire_input_type_t_VAMPIRE_AXIOM: vampire_input_type_t = 0;
63pub const vampire_input_type_t_VAMPIRE_NEGATED_CONJECTURE: vampire_input_type_t = 1;
64pub const vampire_input_type_t_VAMPIRE_CONJECTURE: vampire_input_type_t = 2;
65#[doc = " Input type for units"]
66pub type vampire_input_type_t = ::std::os::raw::c_uint;
67pub const vampire_inference_rule_t_INPUT: vampire_inference_rule_t = 0;
68pub const vampire_inference_rule_t_GENERIC_FORMULA_CLAUSE_TRANSFORMATION: vampire_inference_rule_t =
69 1;
70pub const vampire_inference_rule_t_NEGATED_CONJECTURE: vampire_inference_rule_t = 2;
71pub const vampire_inference_rule_t_ANSWER_LITERAL_INJECTION: vampire_inference_rule_t = 3;
72pub const vampire_inference_rule_t_ANSWER_LITERAL_INPUT_SKOLEMISATION: vampire_inference_rule_t = 4;
73pub const vampire_inference_rule_t_CLAIM_DEFINITION: vampire_inference_rule_t = 5;
74pub const vampire_inference_rule_t_RECTIFY: vampire_inference_rule_t = 6;
75pub const vampire_inference_rule_t_CLOSURE: vampire_inference_rule_t = 7;
76pub const vampire_inference_rule_t_FLATTEN: vampire_inference_rule_t = 8;
77pub const vampire_inference_rule_t_ENNF: vampire_inference_rule_t = 9;
78pub const vampire_inference_rule_t_NNF: vampire_inference_rule_t = 10;
79pub const vampire_inference_rule_t_REDUCE_FALSE_TRUE: vampire_inference_rule_t = 11;
80pub const vampire_inference_rule_t_DEFINITION_FOLDING: vampire_inference_rule_t = 12;
81pub const vampire_inference_rule_t_THEORY_NORMALIZATION: vampire_inference_rule_t = 13;
82pub const vampire_inference_rule_t_ALASCA_INTEGER_TRANSFORMATION: vampire_inference_rule_t = 14;
83pub const vampire_inference_rule_t_SKOLEMIZE: vampire_inference_rule_t = 15;
84pub const vampire_inference_rule_t_SKOLEM_SYMBOL_INTRODUCTION: vampire_inference_rule_t = 16;
85pub const vampire_inference_rule_t_CLAUSIFY: vampire_inference_rule_t = 17;
86pub const vampire_inference_rule_t_REORIENT_EQUATIONS: vampire_inference_rule_t = 18;
87pub const vampire_inference_rule_t_GENERIC_FORMULA_CLAUSE_TRANSFORMATION_LAST:
88 vampire_inference_rule_t = 19;
89pub const vampire_inference_rule_t_GENERIC_SIMPLIFYING_INFERENCE: vampire_inference_rule_t = 20;
90pub const vampire_inference_rule_t_REORDER_LITERALS: vampire_inference_rule_t = 21;
91pub const vampire_inference_rule_t_REMOVE_DUPLICATE_LITERALS: vampire_inference_rule_t = 22;
92pub const vampire_inference_rule_t_TRIVIAL_INEQUALITY_REMOVAL: vampire_inference_rule_t = 23;
93pub const vampire_inference_rule_t_EQUALITY_RESOLUTION_WITH_DELETION: vampire_inference_rule_t = 24;
94pub const vampire_inference_rule_t_FORWARD_SUBSUMPTION_RESOLUTION: vampire_inference_rule_t = 25;
95pub const vampire_inference_rule_t_BACKWARD_SUBSUMPTION_RESOLUTION: vampire_inference_rule_t = 26;
96pub const vampire_inference_rule_t_FORWARD_DEMODULATION: vampire_inference_rule_t = 27;
97pub const vampire_inference_rule_t_BACKWARD_DEMODULATION: vampire_inference_rule_t = 28;
98pub const vampire_inference_rule_t_ALASCA_FWD_DEMODULATION: vampire_inference_rule_t = 29;
99pub const vampire_inference_rule_t_ALASCA_BWD_DEMODULATION: vampire_inference_rule_t = 30;
100pub const vampire_inference_rule_t_FORWARD_SUBSUMPTION_DEMODULATION: vampire_inference_rule_t = 31;
101pub const vampire_inference_rule_t_BACKWARD_SUBSUMPTION_DEMODULATION: vampire_inference_rule_t = 32;
102pub const vampire_inference_rule_t_FORWARD_LITERAL_REWRITING: vampire_inference_rule_t = 33;
103pub const vampire_inference_rule_t_INNER_REWRITING: vampire_inference_rule_t = 34;
104pub const vampire_inference_rule_t_CONDENSATION: vampire_inference_rule_t = 35;
105pub const vampire_inference_rule_t_EVALUATION: vampire_inference_rule_t = 36;
106pub const vampire_inference_rule_t_ALASCA_NORMALIZATION: vampire_inference_rule_t = 37;
107pub const vampire_inference_rule_t_ALASCA_ABSTRACTION: vampire_inference_rule_t = 38;
108pub const vampire_inference_rule_t_ALASCA_FLOOR_ELIMINATION: vampire_inference_rule_t = 39;
109pub const vampire_inference_rule_t_CANCELLATION: vampire_inference_rule_t = 40;
110pub const vampire_inference_rule_t_INTERPRETED_SIMPLIFICATION: vampire_inference_rule_t = 41;
111pub const vampire_inference_rule_t_THEORY_FLATTENING: vampire_inference_rule_t = 42;
112pub const vampire_inference_rule_t_TERM_ALGEBRA_DISTINCTNESS: vampire_inference_rule_t = 43;
113pub const vampire_inference_rule_t_TERM_ALGEBRA_POSITIVE_INJECTIVITY_SIMPLIFYING:
114 vampire_inference_rule_t = 44;
115pub const vampire_inference_rule_t_TERM_ALGEBRA_NEGATIVE_INJECTIVITY_SIMPLIFYING:
116 vampire_inference_rule_t = 45;
117pub const vampire_inference_rule_t_GLOBAL_SUBSUMPTION: vampire_inference_rule_t = 46;
118pub const vampire_inference_rule_t_DISTINCT_EQUALITY_REMOVAL: vampire_inference_rule_t = 47;
119pub const vampire_inference_rule_t_GAUSSIAN_VARIABLE_ELIMINIATION: vampire_inference_rule_t = 48;
120pub const vampire_inference_rule_t_ARITHMETIC_SUBTERM_GENERALIZATION: vampire_inference_rule_t = 49;
121pub const vampire_inference_rule_t_ANSWER_LITERAL_REMOVAL: vampire_inference_rule_t = 50;
122pub const vampire_inference_rule_t_ANSWER_LITERAL_JOIN_WITH_CONSTRAINTS: vampire_inference_rule_t =
123 51;
124pub const vampire_inference_rule_t_ANSWER_LITERAL_JOIN_AS_ITE: vampire_inference_rule_t = 52;
125pub const vampire_inference_rule_t_AVATAR_ASSERTION_REINTRODUCTION: vampire_inference_rule_t = 53;
126pub const vampire_inference_rule_t_CASES_SIMP: vampire_inference_rule_t = 54;
127pub const vampire_inference_rule_t_ALASCA_VIRAS_QE: vampire_inference_rule_t = 55;
128pub const vampire_inference_rule_t_BOOL_SIMP: vampire_inference_rule_t = 56;
129pub const vampire_inference_rule_t_FUNCTION_DEFINITION_DEMODULATION: vampire_inference_rule_t = 57;
130pub const vampire_inference_rule_t_GENERIC_SIMPLIFYING_INFERENCE_LAST: vampire_inference_rule_t =
131 58;
132pub const vampire_inference_rule_t_GENERIC_GENERATING_INFERENCE: vampire_inference_rule_t = 59;
133pub const vampire_inference_rule_t_RESOLUTION: vampire_inference_rule_t = 60;
134pub const vampire_inference_rule_t_CONSTRAINED_RESOLUTION: vampire_inference_rule_t = 61;
135pub const vampire_inference_rule_t_FACTORING: vampire_inference_rule_t = 62;
136pub const vampire_inference_rule_t_CONSTRAINED_FACTORING: vampire_inference_rule_t = 63;
137pub const vampire_inference_rule_t_SUPERPOSITION: vampire_inference_rule_t = 64;
138pub const vampire_inference_rule_t_FUNCTION_DEFINITION_REWRITING: vampire_inference_rule_t = 65;
139pub const vampire_inference_rule_t_CONSTRAINED_SUPERPOSITION: vampire_inference_rule_t = 66;
140pub const vampire_inference_rule_t_EQUALITY_FACTORING: vampire_inference_rule_t = 67;
141pub const vampire_inference_rule_t_EQUALITY_RESOLUTION: vampire_inference_rule_t = 68;
142pub const vampire_inference_rule_t_EXTENSIONALITY_RESOLUTION: vampire_inference_rule_t = 69;
143pub const vampire_inference_rule_t_TERM_ALGEBRA_INJECTIVITY_GENERATING: vampire_inference_rule_t =
144 70;
145pub const vampire_inference_rule_t_TERM_ALGEBRA_ACYCLICITY: vampire_inference_rule_t = 71;
146pub const vampire_inference_rule_t_FOOL_PARAMODULATION: vampire_inference_rule_t = 72;
147pub const vampire_inference_rule_t_UNIT_RESULTING_RESOLUTION: vampire_inference_rule_t = 73;
148pub const vampire_inference_rule_t_INDUCTION_HYPERRESOLUTION: vampire_inference_rule_t = 74;
149pub const vampire_inference_rule_t_INSTANTIATION: vampire_inference_rule_t = 75;
150pub const vampire_inference_rule_t_ALASCA_FOURIER_MOTZKIN: vampire_inference_rule_t = 76;
151pub const vampire_inference_rule_t_ALASCA_INTEGER_FOURIER_MOTZKIN: vampire_inference_rule_t = 77;
152pub const vampire_inference_rule_t_ALASCA_TERM_FACTORING: vampire_inference_rule_t = 78;
153pub const vampire_inference_rule_t_ALASCA_FLOOR_BOUNDS: vampire_inference_rule_t = 79;
154pub const vampire_inference_rule_t_ALASCA_EQ_FACTORING: vampire_inference_rule_t = 80;
155pub const vampire_inference_rule_t_ALASCA_LITERAL_FACTORING: vampire_inference_rule_t = 81;
156pub const vampire_inference_rule_t_ALASCA_SUPERPOSITION: vampire_inference_rule_t = 82;
157pub const vampire_inference_rule_t_ALASCA_COHERENCE: vampire_inference_rule_t = 83;
158pub const vampire_inference_rule_t_ALASCA_COHERENCE_NORMALIZATION: vampire_inference_rule_t = 84;
159pub const vampire_inference_rule_t_ALASCA_VARIABLE_ELIMINATION: vampire_inference_rule_t = 85;
160pub const vampire_inference_rule_t_ARG_CONG: vampire_inference_rule_t = 86;
161pub const vampire_inference_rule_t_INJECTIVITY: vampire_inference_rule_t = 87;
162pub const vampire_inference_rule_t_PRIMITIVE_INSTANTIATION: vampire_inference_rule_t = 88;
163pub const vampire_inference_rule_t_LEIBNIZ_ELIMINATION: vampire_inference_rule_t = 89;
164pub const vampire_inference_rule_t_HILBERTS_CHOICE_INSTANCE: vampire_inference_rule_t = 90;
165pub const vampire_inference_rule_t_NEGATIVE_EXT: vampire_inference_rule_t = 91;
166pub const vampire_inference_rule_t_EQ_TO_DISEQ: vampire_inference_rule_t = 92;
167pub const vampire_inference_rule_t_HOL_NOT_ELIMINATION: vampire_inference_rule_t = 93;
168pub const vampire_inference_rule_t_BINARY_CONN_ELIMINATION: vampire_inference_rule_t = 94;
169pub const vampire_inference_rule_t_VSIGMA_ELIMINATION: vampire_inference_rule_t = 95;
170pub const vampire_inference_rule_t_VPI_ELIMINATION: vampire_inference_rule_t = 96;
171pub const vampire_inference_rule_t_HOL_EQUALITY_ELIMINATION: vampire_inference_rule_t = 97;
172pub const vampire_inference_rule_t_GENERIC_GENERATING_INFERENCE_LAST: vampire_inference_rule_t = 98;
173pub const vampire_inference_rule_t_EQUALITY_PROXY_REPLACEMENT: vampire_inference_rule_t = 99;
174pub const vampire_inference_rule_t_EQUALITY_PROXY_AXIOM1: vampire_inference_rule_t = 100;
175pub const vampire_inference_rule_t_EQUALITY_PROXY_AXIOM2: vampire_inference_rule_t = 101;
176pub const vampire_inference_rule_t_DEFINITION_UNFOLDING: vampire_inference_rule_t = 102;
177pub const vampire_inference_rule_t_FUNCTION_DEFINITION: vampire_inference_rule_t = 103;
178pub const vampire_inference_rule_t_PREDICATE_DEFINITION: vampire_inference_rule_t = 104;
179pub const vampire_inference_rule_t_PREDICATE_DEFINITION_UNFOLDING: vampire_inference_rule_t = 105;
180pub const vampire_inference_rule_t_PREDICATE_DEFINITION_MERGING: vampire_inference_rule_t = 106;
181pub const vampire_inference_rule_t_POLARITY_FLIPPING: vampire_inference_rule_t = 107;
182pub const vampire_inference_rule_t_UNUSED_PREDICATE_DEFINITION_REMOVAL: vampire_inference_rule_t =
183 108;
184pub const vampire_inference_rule_t_PURE_PREDICATE_REMOVAL: vampire_inference_rule_t = 109;
185pub const vampire_inference_rule_t_INEQUALITY_SPLITTING: vampire_inference_rule_t = 110;
186pub const vampire_inference_rule_t_INEQUALITY_SPLITTING_NAME_INTRODUCTION:
187 vampire_inference_rule_t = 111;
188pub const vampire_inference_rule_t_DISTINCTNESS_AXIOM: vampire_inference_rule_t = 112;
189pub const vampire_inference_rule_t_BOOLEAN_TERM_ENCODING: vampire_inference_rule_t = 113;
190pub const vampire_inference_rule_t_FOOL_ELIMINATION: vampire_inference_rule_t = 114;
191pub const vampire_inference_rule_t_FOOL_ITE_DEFINITION: vampire_inference_rule_t = 115;
192pub const vampire_inference_rule_t_FOOL_LET_DEFINITION: vampire_inference_rule_t = 116;
193pub const vampire_inference_rule_t_FOOL_FORMULA_DEFINITION: vampire_inference_rule_t = 117;
194pub const vampire_inference_rule_t_FOOL_MATCH_DEFINITION: vampire_inference_rule_t = 118;
195pub const vampire_inference_rule_t_GENERAL_SPLITTING: vampire_inference_rule_t = 119;
196pub const vampire_inference_rule_t_GENERAL_SPLITTING_COMPONENT: vampire_inference_rule_t = 120;
197pub const vampire_inference_rule_t_COLOR_UNBLOCKING: vampire_inference_rule_t = 121;
198pub const vampire_inference_rule_t_SAT_COLOR_ELIMINATION: vampire_inference_rule_t = 122;
199pub const vampire_inference_rule_t_FORMULIFY: vampire_inference_rule_t = 123;
200pub const vampire_inference_rule_t_FMB_FLATTENING: vampire_inference_rule_t = 124;
201pub const vampire_inference_rule_t_FMB_FUNC_DEF: vampire_inference_rule_t = 125;
202pub const vampire_inference_rule_t_FMB_DEF_INTRO: vampire_inference_rule_t = 126;
203pub const vampire_inference_rule_t_MODEL_NOT_FOUND: vampire_inference_rule_t = 127;
204pub const vampire_inference_rule_t_ADD_SORT_PREDICATES: vampire_inference_rule_t = 128;
205pub const vampire_inference_rule_t_ADD_SORT_FUNCTIONS: vampire_inference_rule_t = 129;
206pub const vampire_inference_rule_t_ANSWER_LITERAL_RESOLVER: vampire_inference_rule_t = 130;
207pub const vampire_inference_rule_t_THEORY_TAUTOLOGY_SAT_CONFLICT: vampire_inference_rule_t = 131;
208pub const vampire_inference_rule_t_GENERIC_AVATAR_INFERENCE: vampire_inference_rule_t = 132;
209pub const vampire_inference_rule_t_AVATAR_DEFINITION: vampire_inference_rule_t = 133;
210pub const vampire_inference_rule_t_AVATAR_COMPONENT: vampire_inference_rule_t = 134;
211pub const vampire_inference_rule_t_AVATAR_REFUTATION: vampire_inference_rule_t = 135;
212pub const vampire_inference_rule_t_AVATAR_REFUTATION_SMT: vampire_inference_rule_t = 136;
213pub const vampire_inference_rule_t_AVATAR_SPLIT_CLAUSE: vampire_inference_rule_t = 137;
214pub const vampire_inference_rule_t_AVATAR_CONTRADICTION_CLAUSE: vampire_inference_rule_t = 138;
215pub const vampire_inference_rule_t_GENERIC_AVATAR_INFERENCE_LAST: vampire_inference_rule_t = 139;
216pub const vampire_inference_rule_t_GENERIC_THEORY_AXIOM: vampire_inference_rule_t = 140;
217pub const vampire_inference_rule_t_THA_COMMUTATIVITY: vampire_inference_rule_t = 141;
218pub const vampire_inference_rule_t_THA_ASSOCIATIVITY: vampire_inference_rule_t = 142;
219pub const vampire_inference_rule_t_THA_RIGHT_IDENTITY: vampire_inference_rule_t = 143;
220pub const vampire_inference_rule_t_THA_LEFT_IDENTITY: vampire_inference_rule_t = 144;
221pub const vampire_inference_rule_t_THA_INVERSE_OP_OP_INVERSES: vampire_inference_rule_t = 145;
222pub const vampire_inference_rule_t_THA_INVERSE_OP_UNIT: vampire_inference_rule_t = 146;
223pub const vampire_inference_rule_t_THA_INVERSE_ASSOC: vampire_inference_rule_t = 147;
224pub const vampire_inference_rule_t_THA_NONREFLEX: vampire_inference_rule_t = 148;
225pub const vampire_inference_rule_t_THA_TRANSITIVITY: vampire_inference_rule_t = 149;
226pub const vampire_inference_rule_t_THA_ORDER_TOTALITY: vampire_inference_rule_t = 150;
227pub const vampire_inference_rule_t_THA_ORDER_MONOTONICITY: vampire_inference_rule_t = 151;
228pub const vampire_inference_rule_t_THA_ALASCA: vampire_inference_rule_t = 152;
229pub const vampire_inference_rule_t_THA_PLUS_ONE_GREATER: vampire_inference_rule_t = 153;
230pub const vampire_inference_rule_t_THA_ORDER_PLUS_ONE_DICHOTOMY: vampire_inference_rule_t = 154;
231pub const vampire_inference_rule_t_THA_MINUS_MINUS_X: vampire_inference_rule_t = 155;
232pub const vampire_inference_rule_t_THA_TIMES_ZERO: vampire_inference_rule_t = 156;
233pub const vampire_inference_rule_t_THA_DISTRIBUTIVITY: vampire_inference_rule_t = 157;
234pub const vampire_inference_rule_t_THA_DIVISIBILITY: vampire_inference_rule_t = 158;
235pub const vampire_inference_rule_t_THA_MODULO_MULTIPLY: vampire_inference_rule_t = 159;
236pub const vampire_inference_rule_t_THA_MODULO_POSITIVE: vampire_inference_rule_t = 160;
237pub const vampire_inference_rule_t_THA_MODULO_SMALL: vampire_inference_rule_t = 161;
238pub const vampire_inference_rule_t_THA_DIVIDES_MULTIPLY: vampire_inference_rule_t = 162;
239pub const vampire_inference_rule_t_THA_NONDIVIDES_SKOLEM: vampire_inference_rule_t = 163;
240pub const vampire_inference_rule_t_THA_ABS_EQUALS: vampire_inference_rule_t = 164;
241pub const vampire_inference_rule_t_THA_ABS_MINUS_EQUALS: vampire_inference_rule_t = 165;
242pub const vampire_inference_rule_t_THA_QUOTIENT_NON_ZERO: vampire_inference_rule_t = 166;
243pub const vampire_inference_rule_t_THA_QUOTIENT_MULTIPLY: vampire_inference_rule_t = 167;
244pub const vampire_inference_rule_t_THA_EXTRA_INTEGER_ORDERING: vampire_inference_rule_t = 168;
245pub const vampire_inference_rule_t_THA_FLOOR_SMALL: vampire_inference_rule_t = 169;
246pub const vampire_inference_rule_t_THA_FLOOR_BIG: vampire_inference_rule_t = 170;
247pub const vampire_inference_rule_t_THA_CEILING_BIG: vampire_inference_rule_t = 171;
248pub const vampire_inference_rule_t_THA_CEILING_SMALL: vampire_inference_rule_t = 172;
249pub const vampire_inference_rule_t_THA_TRUNC1: vampire_inference_rule_t = 173;
250pub const vampire_inference_rule_t_THA_TRUNC2: vampire_inference_rule_t = 174;
251pub const vampire_inference_rule_t_THA_TRUNC3: vampire_inference_rule_t = 175;
252pub const vampire_inference_rule_t_THA_TRUNC4: vampire_inference_rule_t = 176;
253pub const vampire_inference_rule_t_THA_ARRAY_EXTENSIONALITY: vampire_inference_rule_t = 177;
254pub const vampire_inference_rule_t_THA_BOOLEAN_ARRAY_EXTENSIONALITY: vampire_inference_rule_t = 178;
255pub const vampire_inference_rule_t_THA_BOOLEAN_ARRAY_WRITE1: vampire_inference_rule_t = 179;
256pub const vampire_inference_rule_t_THA_BOOLEAN_ARRAY_WRITE2: vampire_inference_rule_t = 180;
257pub const vampire_inference_rule_t_THA_ARRAY_WRITE1: vampire_inference_rule_t = 181;
258pub const vampire_inference_rule_t_THA_ARRAY_WRITE2: vampire_inference_rule_t = 182;
259pub const vampire_inference_rule_t_TERM_ALGEBRA_ACYCLICITY_AXIOM: vampire_inference_rule_t = 183;
260pub const vampire_inference_rule_t_TERM_ALGEBRA_DIRECT_SUBTERMS_AXIOM: vampire_inference_rule_t =
261 184;
262pub const vampire_inference_rule_t_TERM_ALGEBRA_SUBTERMS_TRANSITIVE_AXIOM:
263 vampire_inference_rule_t = 185;
264pub const vampire_inference_rule_t_TERM_ALGEBRA_DISCRIMINATION_AXIOM: vampire_inference_rule_t =
265 186;
266pub const vampire_inference_rule_t_TERM_ALGEBRA_DISTINCTNESS_AXIOM: vampire_inference_rule_t = 187;
267pub const vampire_inference_rule_t_TERM_ALGEBRA_EXHAUSTIVENESS_AXIOM: vampire_inference_rule_t =
268 188;
269pub const vampire_inference_rule_t_TERM_ALGEBRA_INJECTIVITY_AXIOM: vampire_inference_rule_t = 189;
270pub const vampire_inference_rule_t_FOOL_AXIOM_TRUE_NEQ_FALSE: vampire_inference_rule_t = 190;
271pub const vampire_inference_rule_t_FOOL_AXIOM_ALL_IS_TRUE_OR_FALSE: vampire_inference_rule_t = 191;
272pub const vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_ONE: vampire_inference_rule_t = 192;
273pub const vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_TWO: vampire_inference_rule_t = 193;
274pub const vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_THREE: vampire_inference_rule_t = 194;
275pub const vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_RECURSION: vampire_inference_rule_t = 195;
276pub const vampire_inference_rule_t_INT_INF_UP_INDUCTION_AXIOM: vampire_inference_rule_t = 196;
277pub const vampire_inference_rule_t_INT_INF_DOWN_INDUCTION_AXIOM: vampire_inference_rule_t = 197;
278pub const vampire_inference_rule_t_INT_FIN_UP_INDUCTION_AXIOM: vampire_inference_rule_t = 198;
279pub const vampire_inference_rule_t_INT_FIN_DOWN_INDUCTION_AXIOM: vampire_inference_rule_t = 199;
280pub const vampire_inference_rule_t_INT_DB_UP_INDUCTION_AXIOM: vampire_inference_rule_t = 200;
281pub const vampire_inference_rule_t_INT_DB_DOWN_INDUCTION_AXIOM: vampire_inference_rule_t = 201;
282#[doc = " Inference rules"]
283pub type vampire_inference_rule_t = ::std::os::raw::c_uint;
284#[doc = " A single step in a proof"]
285#[repr(C)]
286#[derive(Debug, Copy, Clone)]
287pub struct vampire_proof_step_t {
288 pub id: ::std::os::raw::c_uint,
289 pub rule: vampire_inference_rule_t,
290 pub input_type: vampire_input_type_t,
291 pub premise_ids: *mut ::std::os::raw::c_uint,
292 pub premise_count: usize,
293 pub unit: *mut vampire_unit_t,
294}
295#[allow(clippy::unnecessary_operation, clippy::identity_op)]
296const _: () = {
297 ["Size of vampire_proof_step_t"][::std::mem::size_of::<vampire_proof_step_t>() - 40usize];
298 ["Alignment of vampire_proof_step_t"][::std::mem::align_of::<vampire_proof_step_t>() - 8usize];
299 ["Offset of field: vampire_proof_step_t::id"]
300 [::std::mem::offset_of!(vampire_proof_step_t, id) - 0usize];
301 ["Offset of field: vampire_proof_step_t::rule"]
302 [::std::mem::offset_of!(vampire_proof_step_t, rule) - 4usize];
303 ["Offset of field: vampire_proof_step_t::input_type"]
304 [::std::mem::offset_of!(vampire_proof_step_t, input_type) - 8usize];
305 ["Offset of field: vampire_proof_step_t::premise_ids"]
306 [::std::mem::offset_of!(vampire_proof_step_t, premise_ids) - 16usize];
307 ["Offset of field: vampire_proof_step_t::premise_count"]
308 [::std::mem::offset_of!(vampire_proof_step_t, premise_count) - 24usize];
309 ["Offset of field: vampire_proof_step_t::unit"]
310 [::std::mem::offset_of!(vampire_proof_step_t, unit) - 32usize];
311};
312unsafe extern "C" {
313 #[doc = " Prepare for running another proof (light reset).\n Call this between independent proving attempts to reset\n the global ordering and other per-proof state.\n\n Note: This does NOT reset the signature - symbols accumulate\n between proofs. Use vampire_reset() for a full reset."]
314 pub fn vampire_prepare_for_next_proof();
315}
316unsafe extern "C" {
317 #[doc = " Fully reset the Vampire state for a fresh start.\n This resets all static caches, clears the signature, and\n reinitializes the environment. After calling this, the\n state is as if Vampire was just started.\n\n Call this between proofs if you want to reuse symbol names\n without conflicts, or to prevent memory growth from accumulated\n symbols and caches."]
318 pub fn vampire_reset();
319}
320unsafe extern "C" {
321 #[doc = " Set a time limit in seconds (0 = no limit)."]
322 pub fn vampire_set_time_limit(seconds: ::std::os::raw::c_int);
323}
324unsafe extern "C" {
325 #[doc = " Set a time limit in deciseconds (10 = 1 second, 0 = no limit)."]
326 pub fn vampire_set_time_limit_deciseconds(deciseconds: ::std::os::raw::c_int);
327}
328unsafe extern "C" {
329 #[doc = " Set a time limit in milliseconds (1000 = 1 second, 0 = no limit)."]
330 pub fn vampire_set_time_limit_milliseconds(milliseconds: ::std::os::raw::c_int);
331}
332unsafe extern "C" {
333 #[doc = " Enable or disable proof output."]
334 pub fn vampire_set_show_proof(show: bool);
335}
336unsafe extern "C" {
337 #[doc = " Set saturation algorithm.\n @param algorithm Name of algorithm (e.g., \"lrs\", \"discount\", \"otter\")"]
338 pub fn vampire_set_saturation_algorithm(algorithm: *const ::std::os::raw::c_char);
339}
340unsafe extern "C" {
341 #[doc = " Register a function symbol with the given name and arity.\n For constants, use arity 0.\n @param name Symbol name (null-terminated string)\n @param arity Number of arguments\n @return functor index for use in term construction"]
342 pub fn vampire_add_function(
343 name: *const ::std::os::raw::c_char,
344 arity: ::std::os::raw::c_uint,
345 ) -> ::std::os::raw::c_uint;
346}
347unsafe extern "C" {
348 #[doc = " Register a predicate symbol with the given name and arity.\n @param name Symbol name (null-terminated string)\n @param arity Number of arguments\n @return predicate index for use in literal construction"]
349 pub fn vampire_add_predicate(
350 name: *const ::std::os::raw::c_char,
351 arity: ::std::os::raw::c_uint,
352 ) -> ::std::os::raw::c_uint;
353}
354unsafe extern "C" {
355 #[doc = " Create a variable term.\n @param index Variable index (0, 1, 2, ...)\n @return Term handle"]
356 pub fn vampire_var(index: ::std::os::raw::c_uint) -> *mut vampire_term_t;
357}
358unsafe extern "C" {
359 #[doc = " Create a constant term (0-arity function application).\n @param functor Function symbol index from vampire_add_function\n @return Term handle"]
360 pub fn vampire_constant(functor: ::std::os::raw::c_uint) -> *mut vampire_term_t;
361}
362unsafe extern "C" {
363 #[doc = " Create a function application term.\n @param functor Function symbol index from vampire_add_function\n @param args Array of argument terms\n @param arg_count Number of arguments\n @return Term handle"]
364 pub fn vampire_term(
365 functor: ::std::os::raw::c_uint,
366 args: *mut *mut vampire_term_t,
367 arg_count: usize,
368 ) -> *mut vampire_term_t;
369}
370unsafe extern "C" {
371 #[doc = " Create an equality literal (s = t or s != t).\n @param positive true for equality, false for disequality\n @param lhs Left-hand side term\n @param rhs Right-hand side term\n @return Literal handle"]
372 pub fn vampire_eq(
373 positive: bool,
374 lhs: *mut vampire_term_t,
375 rhs: *mut vampire_term_t,
376 ) -> *mut vampire_literal_t;
377}
378unsafe extern "C" {
379 #[doc = " Create a predicate literal.\n @param pred Predicate symbol index from vampire_add_predicate\n @param positive true for positive literal, false for negated\n @param args Array of argument terms\n @param arg_count Number of arguments\n @return Literal handle"]
380 pub fn vampire_lit(
381 pred: ::std::os::raw::c_uint,
382 positive: bool,
383 args: *mut *mut vampire_term_t,
384 arg_count: usize,
385 ) -> *mut vampire_literal_t;
386}
387unsafe extern "C" {
388 #[doc = " Get the complementary (negated) literal.\n @param l The literal to negate\n @return Literal handle"]
389 pub fn vampire_neg(l: *mut vampire_literal_t) -> *mut vampire_literal_t;
390}
391unsafe extern "C" {
392 #[doc = " Create an atomic formula from a literal.\n @param l The literal\n @return Formula handle"]
393 pub fn vampire_atom(l: *mut vampire_literal_t) -> *mut vampire_formula_t;
394}
395unsafe extern "C" {
396 #[doc = " Create a negated formula (NOT f).\n @param f The formula to negate\n @return Formula handle"]
397 pub fn vampire_not(f: *mut vampire_formula_t) -> *mut vampire_formula_t;
398}
399unsafe extern "C" {
400 #[doc = " Create a conjunction (f1 AND f2 AND ...).\n @param formulas Array of formulas\n @param count Number of formulas\n @return Formula handle"]
401 pub fn vampire_and(
402 formulas: *mut *mut vampire_formula_t,
403 count: usize,
404 ) -> *mut vampire_formula_t;
405}
406unsafe extern "C" {
407 #[doc = " Create a disjunction (f1 OR f2 OR ...).\n @param formulas Array of formulas\n @param count Number of formulas\n @return Formula handle"]
408 pub fn vampire_or(
409 formulas: *mut *mut vampire_formula_t,
410 count: usize,
411 ) -> *mut vampire_formula_t;
412}
413unsafe extern "C" {
414 #[doc = " Create an implication (f1 => f2).\n @param lhs The antecedent\n @param rhs The consequent\n @return Formula handle"]
415 pub fn vampire_imp(
416 lhs: *mut vampire_formula_t,
417 rhs: *mut vampire_formula_t,
418 ) -> *mut vampire_formula_t;
419}
420unsafe extern "C" {
421 #[doc = " Create an equivalence (f1 <=> f2).\n @param lhs Left-hand side\n @param rhs Right-hand side\n @return Formula handle"]
422 pub fn vampire_iff(
423 lhs: *mut vampire_formula_t,
424 rhs: *mut vampire_formula_t,
425 ) -> *mut vampire_formula_t;
426}
427unsafe extern "C" {
428 #[doc = " Create a universally quantified formula (forall x. f).\n @param var_index The variable index to bind\n @param f The body formula\n @return Formula handle"]
429 pub fn vampire_forall(
430 var_index: ::std::os::raw::c_uint,
431 f: *mut vampire_formula_t,
432 ) -> *mut vampire_formula_t;
433}
434unsafe extern "C" {
435 #[doc = " Create an existentially quantified formula (exists x. f).\n @param var_index The variable index to bind\n @param f The body formula\n @return Formula handle"]
436 pub fn vampire_exists(
437 var_index: ::std::os::raw::c_uint,
438 f: *mut vampire_formula_t,
439 ) -> *mut vampire_formula_t;
440}
441unsafe extern "C" {
442 #[doc = " Create a true (tautology) formula.\n @return Formula handle"]
443 pub fn vampire_true() -> *mut vampire_formula_t;
444}
445unsafe extern "C" {
446 #[doc = " Create a false (contradiction) formula.\n @return Formula handle"]
447 pub fn vampire_false() -> *mut vampire_formula_t;
448}
449unsafe extern "C" {
450 #[doc = " Create an axiom formula unit.\n @param f The formula\n @return Unit handle"]
451 pub fn vampire_axiom_formula(f: *mut vampire_formula_t) -> *mut vampire_unit_t;
452}
453unsafe extern "C" {
454 #[doc = " Create a conjecture formula unit (to be proven).\n The formula is automatically negated for refutation-based proving.\n @param f The formula to prove\n @return Unit handle"]
455 pub fn vampire_conjecture_formula(f: *mut vampire_formula_t) -> *mut vampire_unit_t;
456}
457unsafe extern "C" {
458 #[doc = " Create an axiom clause (disjunction of literals).\n @param literals Array of literals\n @param count Number of literals\n @return Clause handle"]
459 pub fn vampire_axiom_clause(
460 literals: *mut *mut vampire_literal_t,
461 count: usize,
462 ) -> *mut vampire_clause_t;
463}
464unsafe extern "C" {
465 #[doc = " Create a conjecture clause (to be refuted).\n @param literals Array of literals\n @param count Number of literals\n @return Clause handle"]
466 pub fn vampire_conjecture_clause(
467 literals: *mut *mut vampire_literal_t,
468 count: usize,
469 ) -> *mut vampire_clause_t;
470}
471unsafe extern "C" {
472 #[doc = " Create a clause with specified input type.\n @param literals Array of literals\n @param count Number of literals\n @param input_type The type of input\n @return Clause handle"]
473 pub fn vampire_clause(
474 literals: *mut *mut vampire_literal_t,
475 count: usize,
476 input_type: vampire_input_type_t,
477 ) -> *mut vampire_clause_t;
478}
479unsafe extern "C" {
480 #[doc = " Create a problem from an array of clauses.\n @param clauses Array of clause handles\n @param count Number of clauses\n @return Problem handle"]
481 pub fn vampire_problem_from_clauses(
482 clauses: *mut *mut vampire_clause_t,
483 count: usize,
484 ) -> *mut vampire_problem_t;
485}
486unsafe extern "C" {
487 #[doc = " Create a problem from an array of units (clauses or formulas).\n Formulas will be clausified during preprocessing.\n @param units Array of unit handles\n @param count Number of units\n @return Problem handle"]
488 pub fn vampire_problem_from_units(
489 units: *mut *mut vampire_unit_t,
490 count: usize,
491 ) -> *mut vampire_problem_t;
492}
493unsafe extern "C" {
494 #[doc = " Run the prover on a problem.\n @param problem The problem to solve\n @return The proof result"]
495 pub fn vampire_prove(problem: *mut vampire_problem_t) -> vampire_proof_result_t;
496}
497unsafe extern "C" {
498 #[doc = " Get the refutation (proof) after a successful vampire_prove() call.\n @return The empty clause with inference chain, or NULL if no proof"]
499 pub fn vampire_get_refutation() -> *mut vampire_unit_t;
500}
501unsafe extern "C" {
502 #[doc = " Print the proof to stdout.\n @param refutation The refutation from vampire_get_refutation()"]
503 pub fn vampire_print_proof(refutation: *mut vampire_unit_t);
504}
505unsafe extern "C" {
506 #[doc = " Print the proof to a file.\n @param filename Path to output file (null-terminated string)\n @param refutation The refutation from vampire_get_refutation()\n @return 0 on success, -1 on error"]
507 pub fn vampire_print_proof_to_file(
508 filename: *const ::std::os::raw::c_char,
509 refutation: *mut vampire_unit_t,
510 ) -> ::std::os::raw::c_int;
511}
512unsafe extern "C" {
513 #[doc = " Extract the proof as a sequence of steps.\n Steps are returned in topological order (premises before conclusions).\n The last step is the empty clause (refutation).\n\n @param refutation The refutation from vampire_get_refutation()\n @param out_steps Pointer to receive the array of proof steps\n @param out_count Pointer to receive the number of steps\n @return 0 on success, -1 on error\n\n Note: The caller must free the returned array and each step's premise_ids array."]
514 pub fn vampire_extract_proof(
515 refutation: *mut vampire_unit_t,
516 out_steps: *mut *mut vampire_proof_step_t,
517 out_count: *mut usize,
518 ) -> ::std::os::raw::c_int;
519}
520unsafe extern "C" {
521 #[doc = " Free the proof steps array returned by vampire_extract_proof().\n @param steps The array to free\n @param count Number of steps"]
522 pub fn vampire_free_proof_steps(steps: *mut vampire_proof_step_t, count: usize);
523}
524unsafe extern "C" {
525 #[doc = " Get the literals of a clause as an array.\n @param clause The clause\n @param out_literals Pointer to receive the array of literals\n @param out_count Pointer to receive the number of literals\n @return 0 on success, -1 on error\n\n Note: The caller must free the returned array."]
526 pub fn vampire_get_literals(
527 clause: *mut vampire_clause_t,
528 out_literals: *mut *mut *mut vampire_literal_t,
529 out_count: *mut usize,
530 ) -> ::std::os::raw::c_int;
531}
532unsafe extern "C" {
533 #[doc = " Free the literals array returned by vampire_get_literals().\n @param literals The array to free"]
534 pub fn vampire_free_literals(literals: *mut *mut vampire_literal_t);
535}
536unsafe extern "C" {
537 #[doc = " Get the clause from a unit (if the unit is a clause).\n @param unit The unit\n @return Clause handle, or NULL if unit is not a clause"]
538 pub fn vampire_unit_as_clause(unit: *mut vampire_unit_t) -> *mut vampire_clause_t;
539}
540unsafe extern "C" {
541 #[doc = " Get the formula from a unit (if the unit is a formula).\n @param unit The unit\n @return Formula handle, or NULL if unit is not a formula"]
542 pub fn vampire_unit_as_formula(unit: *mut vampire_unit_t) -> *mut vampire_formula_t;
543}
544unsafe extern "C" {
545 #[doc = " Check if a clause is empty (represents false).\n @param clause The clause\n @return true if empty, false otherwise"]
546 pub fn vampire_clause_is_empty(clause: *mut vampire_clause_t) -> bool;
547}
548unsafe extern "C" {
549 #[doc = " Convert a term to a string representation.\n @param term The term\n @return Allocated string (must be freed with vampire_free_string), or NULL on error"]
550 pub fn vampire_term_to_string(term: *mut vampire_term_t) -> *mut ::std::os::raw::c_char;
551}
552unsafe extern "C" {
553 #[doc = " Convert a literal to a string representation.\n @param literal The literal\n @return Allocated string (must be freed with vampire_free_string), or NULL on error"]
554 pub fn vampire_literal_to_string(
555 literal: *mut vampire_literal_t,
556 ) -> *mut ::std::os::raw::c_char;
557}
558unsafe extern "C" {
559 #[doc = " Convert a clause to a string representation.\n @param clause The clause\n @return Allocated string (must be freed with vampire_free_string), or NULL on error"]
560 pub fn vampire_clause_to_string(clause: *mut vampire_clause_t) -> *mut ::std::os::raw::c_char;
561}
562unsafe extern "C" {
563 #[doc = " Convert a formula to a string representation.\n @param formula The formula\n @return Allocated string (must be freed with vampire_free_string), or NULL on error"]
564 pub fn vampire_formula_to_string(
565 formula: *mut vampire_formula_t,
566 ) -> *mut ::std::os::raw::c_char;
567}
568unsafe extern "C" {
569 #[doc = " Free a string allocated by vampire_*_to_string functions.\n @param str The string to free"]
570 pub fn vampire_free_string(str: *mut ::std::os::raw::c_char);
571}
572unsafe extern "C" {
573 #[doc = " Get the name of an inference rule.\n @param rule The inference rule\n @return String name (static, do not free)"]
574 pub fn vampire_rule_name(rule: vampire_inference_rule_t) -> *const ::std::os::raw::c_char;
575}
576unsafe extern "C" {
577 #[doc = " Get the name of an input type.\n @param input_type The input type\n @return String name (static, do not free)"]
578 pub fn vampire_input_type_name(
579 input_type: vampire_input_type_t,
580 ) -> *const ::std::os::raw::c_char;
581}
582unsafe extern "C" {
583 pub fn vampire_term_equal(a: *mut vampire_term_t, b: *mut vampire_term_t) -> bool;
584}
585unsafe extern "C" {
586 pub fn vampire_term_hash(a: *mut vampire_term_t) -> u64;
587}
588unsafe extern "C" {
589 pub fn vampire_formula_equal(a: *mut vampire_formula_t, b: *mut vampire_formula_t) -> bool;
590}
591unsafe extern "C" {
592 pub fn vampire_formula_hash(a: *mut vampire_formula_t) -> u64;
593}