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_VAMPIRE_RULE_INPUT: vampire_inference_rule_t = 0;
68pub const vampire_inference_rule_t_VAMPIRE_RULE_RESOLUTION: vampire_inference_rule_t = 1;
69pub const vampire_inference_rule_t_VAMPIRE_RULE_FACTORING: vampire_inference_rule_t = 2;
70pub const vampire_inference_rule_t_VAMPIRE_RULE_SUPERPOSITION: vampire_inference_rule_t = 3;
71pub const vampire_inference_rule_t_VAMPIRE_RULE_EQUALITY_RESOLUTION: vampire_inference_rule_t = 4;
72pub const vampire_inference_rule_t_VAMPIRE_RULE_EQUALITY_FACTORING: vampire_inference_rule_t = 5;
73pub const vampire_inference_rule_t_VAMPIRE_RULE_CLAUSIFY: vampire_inference_rule_t = 6;
74pub const vampire_inference_rule_t_VAMPIRE_RULE_OTHER: vampire_inference_rule_t = 99;
75#[doc = " Inference rules (subset of commonly used rules)"]
76pub type vampire_inference_rule_t = ::std::os::raw::c_uint;
77#[doc = " A single step in a proof"]
78#[repr(C)]
79#[derive(Debug, Copy, Clone)]
80pub struct vampire_proof_step_t {
81 pub id: ::std::os::raw::c_uint,
82 pub rule: vampire_inference_rule_t,
83 pub input_type: vampire_input_type_t,
84 pub premise_ids: *mut ::std::os::raw::c_uint,
85 pub premise_count: usize,
86 pub unit: *mut vampire_unit_t,
87}
88#[allow(clippy::unnecessary_operation, clippy::identity_op)]
89const _: () = {
90 ["Size of vampire_proof_step_t"][::std::mem::size_of::<vampire_proof_step_t>() - 40usize];
91 ["Alignment of vampire_proof_step_t"][::std::mem::align_of::<vampire_proof_step_t>() - 8usize];
92 ["Offset of field: vampire_proof_step_t::id"]
93 [::std::mem::offset_of!(vampire_proof_step_t, id) - 0usize];
94 ["Offset of field: vampire_proof_step_t::rule"]
95 [::std::mem::offset_of!(vampire_proof_step_t, rule) - 4usize];
96 ["Offset of field: vampire_proof_step_t::input_type"]
97 [::std::mem::offset_of!(vampire_proof_step_t, input_type) - 8usize];
98 ["Offset of field: vampire_proof_step_t::premise_ids"]
99 [::std::mem::offset_of!(vampire_proof_step_t, premise_ids) - 16usize];
100 ["Offset of field: vampire_proof_step_t::premise_count"]
101 [::std::mem::offset_of!(vampire_proof_step_t, premise_count) - 24usize];
102 ["Offset of field: vampire_proof_step_t::unit"]
103 [::std::mem::offset_of!(vampire_proof_step_t, unit) - 32usize];
104};
105unsafe extern "C" {
106 #[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."]
107 pub fn vampire_prepare_for_next_proof();
108}
109unsafe extern "C" {
110 #[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."]
111 pub fn vampire_reset();
112}
113unsafe extern "C" {
114 #[doc = " Set a time limit in seconds (0 = no limit)."]
115 pub fn vampire_set_time_limit(seconds: ::std::os::raw::c_int);
116}
117unsafe extern "C" {
118 #[doc = " Set a time limit in deciseconds (10 = 1 second, 0 = no limit)."]
119 pub fn vampire_set_time_limit_deciseconds(deciseconds: ::std::os::raw::c_int);
120}
121unsafe extern "C" {
122 #[doc = " Set a time limit in milliseconds (1000 = 1 second, 0 = no limit)."]
123 pub fn vampire_set_time_limit_milliseconds(milliseconds: ::std::os::raw::c_int);
124}
125unsafe extern "C" {
126 #[doc = " Enable or disable proof output."]
127 pub fn vampire_set_show_proof(show: bool);
128}
129unsafe extern "C" {
130 #[doc = " Set saturation algorithm.\n @param algorithm Name of algorithm (e.g., \"lrs\", \"discount\", \"otter\")"]
131 pub fn vampire_set_saturation_algorithm(algorithm: *const ::std::os::raw::c_char);
132}
133unsafe extern "C" {
134 #[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"]
135 pub fn vampire_add_function(
136 name: *const ::std::os::raw::c_char,
137 arity: ::std::os::raw::c_uint,
138 ) -> ::std::os::raw::c_uint;
139}
140unsafe extern "C" {
141 #[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"]
142 pub fn vampire_add_predicate(
143 name: *const ::std::os::raw::c_char,
144 arity: ::std::os::raw::c_uint,
145 ) -> ::std::os::raw::c_uint;
146}
147unsafe extern "C" {
148 #[doc = " Create a variable term.\n @param index Variable index (0, 1, 2, ...)\n @return Term handle"]
149 pub fn vampire_var(index: ::std::os::raw::c_uint) -> *mut vampire_term_t;
150}
151unsafe extern "C" {
152 #[doc = " Create a constant term (0-arity function application).\n @param functor Function symbol index from vampire_add_function\n @return Term handle"]
153 pub fn vampire_constant(functor: ::std::os::raw::c_uint) -> *mut vampire_term_t;
154}
155unsafe extern "C" {
156 #[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"]
157 pub fn vampire_term(
158 functor: ::std::os::raw::c_uint,
159 args: *mut *mut vampire_term_t,
160 arg_count: usize,
161 ) -> *mut vampire_term_t;
162}
163unsafe extern "C" {
164 #[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"]
165 pub fn vampire_eq(
166 positive: bool,
167 lhs: *mut vampire_term_t,
168 rhs: *mut vampire_term_t,
169 ) -> *mut vampire_literal_t;
170}
171unsafe extern "C" {
172 #[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"]
173 pub fn vampire_lit(
174 pred: ::std::os::raw::c_uint,
175 positive: bool,
176 args: *mut *mut vampire_term_t,
177 arg_count: usize,
178 ) -> *mut vampire_literal_t;
179}
180unsafe extern "C" {
181 #[doc = " Get the complementary (negated) literal.\n @param l The literal to negate\n @return Literal handle"]
182 pub fn vampire_neg(l: *mut vampire_literal_t) -> *mut vampire_literal_t;
183}
184unsafe extern "C" {
185 #[doc = " Create an atomic formula from a literal.\n @param l The literal\n @return Formula handle"]
186 pub fn vampire_atom(l: *mut vampire_literal_t) -> *mut vampire_formula_t;
187}
188unsafe extern "C" {
189 #[doc = " Create a negated formula (NOT f).\n @param f The formula to negate\n @return Formula handle"]
190 pub fn vampire_not(f: *mut vampire_formula_t) -> *mut vampire_formula_t;
191}
192unsafe extern "C" {
193 #[doc = " Create a conjunction (f1 AND f2 AND ...).\n @param formulas Array of formulas\n @param count Number of formulas\n @return Formula handle"]
194 pub fn vampire_and(
195 formulas: *mut *mut vampire_formula_t,
196 count: usize,
197 ) -> *mut vampire_formula_t;
198}
199unsafe extern "C" {
200 #[doc = " Create a disjunction (f1 OR f2 OR ...).\n @param formulas Array of formulas\n @param count Number of formulas\n @return Formula handle"]
201 pub fn vampire_or(
202 formulas: *mut *mut vampire_formula_t,
203 count: usize,
204 ) -> *mut vampire_formula_t;
205}
206unsafe extern "C" {
207 #[doc = " Create an implication (f1 => f2).\n @param lhs The antecedent\n @param rhs The consequent\n @return Formula handle"]
208 pub fn vampire_imp(
209 lhs: *mut vampire_formula_t,
210 rhs: *mut vampire_formula_t,
211 ) -> *mut vampire_formula_t;
212}
213unsafe extern "C" {
214 #[doc = " Create an equivalence (f1 <=> f2).\n @param lhs Left-hand side\n @param rhs Right-hand side\n @return Formula handle"]
215 pub fn vampire_iff(
216 lhs: *mut vampire_formula_t,
217 rhs: *mut vampire_formula_t,
218 ) -> *mut vampire_formula_t;
219}
220unsafe extern "C" {
221 #[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"]
222 pub fn vampire_forall(
223 var_index: ::std::os::raw::c_uint,
224 f: *mut vampire_formula_t,
225 ) -> *mut vampire_formula_t;
226}
227unsafe extern "C" {
228 #[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"]
229 pub fn vampire_exists(
230 var_index: ::std::os::raw::c_uint,
231 f: *mut vampire_formula_t,
232 ) -> *mut vampire_formula_t;
233}
234unsafe extern "C" {
235 #[doc = " Create a true (tautology) formula.\n @return Formula handle"]
236 pub fn vampire_true() -> *mut vampire_formula_t;
237}
238unsafe extern "C" {
239 #[doc = " Create a false (contradiction) formula.\n @return Formula handle"]
240 pub fn vampire_false() -> *mut vampire_formula_t;
241}
242unsafe extern "C" {
243 #[doc = " Create an axiom formula unit.\n @param f The formula\n @return Unit handle"]
244 pub fn vampire_axiom_formula(f: *mut vampire_formula_t) -> *mut vampire_unit_t;
245}
246unsafe extern "C" {
247 #[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"]
248 pub fn vampire_conjecture_formula(f: *mut vampire_formula_t) -> *mut vampire_unit_t;
249}
250unsafe extern "C" {
251 #[doc = " Create an axiom clause (disjunction of literals).\n @param literals Array of literals\n @param count Number of literals\n @return Clause handle"]
252 pub fn vampire_axiom_clause(
253 literals: *mut *mut vampire_literal_t,
254 count: usize,
255 ) -> *mut vampire_clause_t;
256}
257unsafe extern "C" {
258 #[doc = " Create a conjecture clause (to be refuted).\n @param literals Array of literals\n @param count Number of literals\n @return Clause handle"]
259 pub fn vampire_conjecture_clause(
260 literals: *mut *mut vampire_literal_t,
261 count: usize,
262 ) -> *mut vampire_clause_t;
263}
264unsafe extern "C" {
265 #[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"]
266 pub fn vampire_clause(
267 literals: *mut *mut vampire_literal_t,
268 count: usize,
269 input_type: vampire_input_type_t,
270 ) -> *mut vampire_clause_t;
271}
272unsafe extern "C" {
273 #[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"]
274 pub fn vampire_problem_from_clauses(
275 clauses: *mut *mut vampire_clause_t,
276 count: usize,
277 ) -> *mut vampire_problem_t;
278}
279unsafe extern "C" {
280 #[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"]
281 pub fn vampire_problem_from_units(
282 units: *mut *mut vampire_unit_t,
283 count: usize,
284 ) -> *mut vampire_problem_t;
285}
286unsafe extern "C" {
287 #[doc = " Run the prover on a problem.\n @param problem The problem to solve\n @return The proof result"]
288 pub fn vampire_prove(problem: *mut vampire_problem_t) -> vampire_proof_result_t;
289}
290unsafe extern "C" {
291 #[doc = " Get the refutation (proof) after a successful vampire_prove() call.\n @return The empty clause with inference chain, or NULL if no proof"]
292 pub fn vampire_get_refutation() -> *mut vampire_unit_t;
293}
294unsafe extern "C" {
295 #[doc = " Print the proof to stdout.\n @param refutation The refutation from vampire_get_refutation()"]
296 pub fn vampire_print_proof(refutation: *mut vampire_unit_t);
297}
298unsafe extern "C" {
299 #[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"]
300 pub fn vampire_print_proof_to_file(
301 filename: *const ::std::os::raw::c_char,
302 refutation: *mut vampire_unit_t,
303 ) -> ::std::os::raw::c_int;
304}
305unsafe extern "C" {
306 #[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."]
307 pub fn vampire_extract_proof(
308 refutation: *mut vampire_unit_t,
309 out_steps: *mut *mut vampire_proof_step_t,
310 out_count: *mut usize,
311 ) -> ::std::os::raw::c_int;
312}
313unsafe extern "C" {
314 #[doc = " Free the proof steps array returned by vampire_extract_proof().\n @param steps The array to free\n @param count Number of steps"]
315 pub fn vampire_free_proof_steps(steps: *mut vampire_proof_step_t, count: usize);
316}
317unsafe extern "C" {
318 #[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."]
319 pub fn vampire_get_literals(
320 clause: *mut vampire_clause_t,
321 out_literals: *mut *mut *mut vampire_literal_t,
322 out_count: *mut usize,
323 ) -> ::std::os::raw::c_int;
324}
325unsafe extern "C" {
326 #[doc = " Free the literals array returned by vampire_get_literals().\n @param literals The array to free"]
327 pub fn vampire_free_literals(literals: *mut *mut vampire_literal_t);
328}
329unsafe extern "C" {
330 #[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"]
331 pub fn vampire_unit_as_clause(unit: *mut vampire_unit_t) -> *mut vampire_clause_t;
332}
333unsafe extern "C" {
334 #[doc = " Check if a clause is empty (represents false).\n @param clause The clause\n @return true if empty, false otherwise"]
335 pub fn vampire_clause_is_empty(clause: *mut vampire_clause_t) -> bool;
336}
337unsafe extern "C" {
338 #[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"]
339 pub fn vampire_term_to_string(term: *mut vampire_term_t) -> *mut ::std::os::raw::c_char;
340}
341unsafe extern "C" {
342 #[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"]
343 pub fn vampire_literal_to_string(
344 literal: *mut vampire_literal_t,
345 ) -> *mut ::std::os::raw::c_char;
346}
347unsafe extern "C" {
348 #[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"]
349 pub fn vampire_clause_to_string(clause: *mut vampire_clause_t) -> *mut ::std::os::raw::c_char;
350}
351unsafe extern "C" {
352 #[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"]
353 pub fn vampire_formula_to_string(
354 formula: *mut vampire_formula_t,
355 ) -> *mut ::std::os::raw::c_char;
356}
357unsafe extern "C" {
358 #[doc = " Free a string allocated by vampire_*_to_string functions.\n @param str The string to free"]
359 pub fn vampire_free_string(str: *mut ::std::os::raw::c_char);
360}
361unsafe extern "C" {
362 #[doc = " Get the name of an inference rule.\n @param rule The inference rule\n @return String name (static, do not free)"]
363 pub fn vampire_rule_name(rule: vampire_inference_rule_t) -> *const ::std::os::raw::c_char;
364}
365unsafe extern "C" {
366 #[doc = " Get the name of an input type.\n @param input_type The input type\n @return String name (static, do not free)"]
367 pub fn vampire_input_type_name(
368 input_type: vampire_input_type_t,
369 ) -> *const ::std::os::raw::c_char;
370}