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 = " Enable or disable proof output."]
123 pub fn vampire_set_show_proof(show: bool);
124}
125unsafe extern "C" {
126 #[doc = " Set saturation algorithm.\n @param algorithm Name of algorithm (e.g., \"lrs\", \"discount\", \"otter\")"]
127 pub fn vampire_set_saturation_algorithm(algorithm: *const ::std::os::raw::c_char);
128}
129unsafe extern "C" {
130 #[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"]
131 pub fn vampire_add_function(
132 name: *const ::std::os::raw::c_char,
133 arity: ::std::os::raw::c_uint,
134 ) -> ::std::os::raw::c_uint;
135}
136unsafe extern "C" {
137 #[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"]
138 pub fn vampire_add_predicate(
139 name: *const ::std::os::raw::c_char,
140 arity: ::std::os::raw::c_uint,
141 ) -> ::std::os::raw::c_uint;
142}
143unsafe extern "C" {
144 #[doc = " Create a variable term.\n @param index Variable index (0, 1, 2, ...)\n @return Term handle"]
145 pub fn vampire_var(index: ::std::os::raw::c_uint) -> *mut vampire_term_t;
146}
147unsafe extern "C" {
148 #[doc = " Create a constant term (0-arity function application).\n @param functor Function symbol index from vampire_add_function\n @return Term handle"]
149 pub fn vampire_constant(functor: ::std::os::raw::c_uint) -> *mut vampire_term_t;
150}
151unsafe extern "C" {
152 #[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"]
153 pub fn vampire_term(
154 functor: ::std::os::raw::c_uint,
155 args: *mut *mut vampire_term_t,
156 arg_count: usize,
157 ) -> *mut vampire_term_t;
158}
159unsafe extern "C" {
160 #[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"]
161 pub fn vampire_eq(
162 positive: bool,
163 lhs: *mut vampire_term_t,
164 rhs: *mut vampire_term_t,
165 ) -> *mut vampire_literal_t;
166}
167unsafe extern "C" {
168 #[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"]
169 pub fn vampire_lit(
170 pred: ::std::os::raw::c_uint,
171 positive: bool,
172 args: *mut *mut vampire_term_t,
173 arg_count: usize,
174 ) -> *mut vampire_literal_t;
175}
176unsafe extern "C" {
177 #[doc = " Get the complementary (negated) literal.\n @param l The literal to negate\n @return Literal handle"]
178 pub fn vampire_neg(l: *mut vampire_literal_t) -> *mut vampire_literal_t;
179}
180unsafe extern "C" {
181 #[doc = " Create an atomic formula from a literal.\n @param l The literal\n @return Formula handle"]
182 pub fn vampire_atom(l: *mut vampire_literal_t) -> *mut vampire_formula_t;
183}
184unsafe extern "C" {
185 #[doc = " Create a negated formula (NOT f).\n @param f The formula to negate\n @return Formula handle"]
186 pub fn vampire_not(f: *mut vampire_formula_t) -> *mut vampire_formula_t;
187}
188unsafe extern "C" {
189 #[doc = " Create a conjunction (f1 AND f2 AND ...).\n @param formulas Array of formulas\n @param count Number of formulas\n @return Formula handle"]
190 pub fn vampire_and(
191 formulas: *mut *mut vampire_formula_t,
192 count: usize,
193 ) -> *mut vampire_formula_t;
194}
195unsafe extern "C" {
196 #[doc = " Create a disjunction (f1 OR f2 OR ...).\n @param formulas Array of formulas\n @param count Number of formulas\n @return Formula handle"]
197 pub fn vampire_or(
198 formulas: *mut *mut vampire_formula_t,
199 count: usize,
200 ) -> *mut vampire_formula_t;
201}
202unsafe extern "C" {
203 #[doc = " Create an implication (f1 => f2).\n @param lhs The antecedent\n @param rhs The consequent\n @return Formula handle"]
204 pub fn vampire_imp(
205 lhs: *mut vampire_formula_t,
206 rhs: *mut vampire_formula_t,
207 ) -> *mut vampire_formula_t;
208}
209unsafe extern "C" {
210 #[doc = " Create an equivalence (f1 <=> f2).\n @param lhs Left-hand side\n @param rhs Right-hand side\n @return Formula handle"]
211 pub fn vampire_iff(
212 lhs: *mut vampire_formula_t,
213 rhs: *mut vampire_formula_t,
214 ) -> *mut vampire_formula_t;
215}
216unsafe extern "C" {
217 #[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"]
218 pub fn vampire_forall(
219 var_index: ::std::os::raw::c_uint,
220 f: *mut vampire_formula_t,
221 ) -> *mut vampire_formula_t;
222}
223unsafe extern "C" {
224 #[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"]
225 pub fn vampire_exists(
226 var_index: ::std::os::raw::c_uint,
227 f: *mut vampire_formula_t,
228 ) -> *mut vampire_formula_t;
229}
230unsafe extern "C" {
231 #[doc = " Create an axiom formula unit.\n @param f The formula\n @return Unit handle"]
232 pub fn vampire_axiom_formula(f: *mut vampire_formula_t) -> *mut vampire_unit_t;
233}
234unsafe extern "C" {
235 #[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"]
236 pub fn vampire_conjecture_formula(f: *mut vampire_formula_t) -> *mut vampire_unit_t;
237}
238unsafe extern "C" {
239 #[doc = " Create an axiom clause (disjunction of literals).\n @param literals Array of literals\n @param count Number of literals\n @return Clause handle"]
240 pub fn vampire_axiom_clause(
241 literals: *mut *mut vampire_literal_t,
242 count: usize,
243 ) -> *mut vampire_clause_t;
244}
245unsafe extern "C" {
246 #[doc = " Create a conjecture clause (to be refuted).\n @param literals Array of literals\n @param count Number of literals\n @return Clause handle"]
247 pub fn vampire_conjecture_clause(
248 literals: *mut *mut vampire_literal_t,
249 count: usize,
250 ) -> *mut vampire_clause_t;
251}
252unsafe extern "C" {
253 #[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"]
254 pub fn vampire_clause(
255 literals: *mut *mut vampire_literal_t,
256 count: usize,
257 input_type: vampire_input_type_t,
258 ) -> *mut vampire_clause_t;
259}
260unsafe extern "C" {
261 #[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"]
262 pub fn vampire_problem_from_clauses(
263 clauses: *mut *mut vampire_clause_t,
264 count: usize,
265 ) -> *mut vampire_problem_t;
266}
267unsafe extern "C" {
268 #[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"]
269 pub fn vampire_problem_from_units(
270 units: *mut *mut vampire_unit_t,
271 count: usize,
272 ) -> *mut vampire_problem_t;
273}
274unsafe extern "C" {
275 #[doc = " Run the prover on a problem.\n @param problem The problem to solve\n @return The proof result"]
276 pub fn vampire_prove(problem: *mut vampire_problem_t) -> vampire_proof_result_t;
277}
278unsafe extern "C" {
279 #[doc = " Get the refutation (proof) after a successful vampire_prove() call.\n @return The empty clause with inference chain, or NULL if no proof"]
280 pub fn vampire_get_refutation() -> *mut vampire_unit_t;
281}
282unsafe extern "C" {
283 #[doc = " Print the proof to stdout.\n @param refutation The refutation from vampire_get_refutation()"]
284 pub fn vampire_print_proof(refutation: *mut vampire_unit_t);
285}
286unsafe extern "C" {
287 #[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"]
288 pub fn vampire_print_proof_to_file(
289 filename: *const ::std::os::raw::c_char,
290 refutation: *mut vampire_unit_t,
291 ) -> ::std::os::raw::c_int;
292}
293unsafe extern "C" {
294 #[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."]
295 pub fn vampire_extract_proof(
296 refutation: *mut vampire_unit_t,
297 out_steps: *mut *mut vampire_proof_step_t,
298 out_count: *mut usize,
299 ) -> ::std::os::raw::c_int;
300}
301unsafe extern "C" {
302 #[doc = " Free the proof steps array returned by vampire_extract_proof().\n @param steps The array to free\n @param count Number of steps"]
303 pub fn vampire_free_proof_steps(steps: *mut vampire_proof_step_t, count: usize);
304}
305unsafe extern "C" {
306 #[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."]
307 pub fn vampire_get_literals(
308 clause: *mut vampire_clause_t,
309 out_literals: *mut *mut *mut vampire_literal_t,
310 out_count: *mut usize,
311 ) -> ::std::os::raw::c_int;
312}
313unsafe extern "C" {
314 #[doc = " Free the literals array returned by vampire_get_literals().\n @param literals The array to free"]
315 pub fn vampire_free_literals(literals: *mut *mut vampire_literal_t);
316}
317unsafe extern "C" {
318 #[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"]
319 pub fn vampire_unit_as_clause(unit: *mut vampire_unit_t) -> *mut vampire_clause_t;
320}
321unsafe extern "C" {
322 #[doc = " Check if a clause is empty (represents false).\n @param clause The clause\n @return true if empty, false otherwise"]
323 pub fn vampire_clause_is_empty(clause: *mut vampire_clause_t) -> bool;
324}
325unsafe extern "C" {
326 #[doc = " Convert a term to a string representation.\n @param term The term\n @param buffer Output buffer (must be allocated by caller)\n @param buffer_size Size of the buffer\n @return Number of characters written (excluding null terminator),\n or -1 if buffer too small"]
327 pub fn vampire_term_to_string(
328 term: *mut vampire_term_t,
329 buffer: *mut ::std::os::raw::c_char,
330 buffer_size: usize,
331 ) -> ::std::os::raw::c_int;
332}
333unsafe extern "C" {
334 #[doc = " Convert a literal to a string representation.\n @param literal The literal\n @param buffer Output buffer (must be allocated by caller)\n @param buffer_size Size of the buffer\n @return Number of characters written (excluding null terminator),\n or -1 if buffer too small"]
335 pub fn vampire_literal_to_string(
336 literal: *mut vampire_literal_t,
337 buffer: *mut ::std::os::raw::c_char,
338 buffer_size: usize,
339 ) -> ::std::os::raw::c_int;
340}
341unsafe extern "C" {
342 #[doc = " Convert a clause to a string representation.\n @param clause The clause\n @param buffer Output buffer (must be allocated by caller)\n @param buffer_size Size of the buffer\n @return Number of characters written (excluding null terminator),\n or -1 if buffer too small"]
343 pub fn vampire_clause_to_string(
344 clause: *mut vampire_clause_t,
345 buffer: *mut ::std::os::raw::c_char,
346 buffer_size: usize,
347 ) -> ::std::os::raw::c_int;
348}
349unsafe extern "C" {
350 #[doc = " Get the name of an inference rule.\n @param rule The inference rule\n @return String name (static, do not free)"]
351 pub fn vampire_rule_name(rule: vampire_inference_rule_t) -> *const ::std::os::raw::c_char;
352}
353unsafe extern "C" {
354 #[doc = " Get the name of an input type.\n @param input_type The input type\n @return String name (static, do not free)"]
355 pub fn vampire_input_type_name(
356 input_type: vampire_input_type_t,
357 ) -> *const ::std::os::raw::c_char;
358}