pub const true_: u32 = 1;
pub const false_: u32 = 0;
pub const __bool_true_false_are_defined: u32 = 1;
pub type wchar_t = ::std::os::raw::c_int;
#[repr(C)]
#[repr(align(16))]
#[derive(Debug, Copy, Clone)]
pub struct max_align_t {
pub __clang_max_align_nonce1: ::std::os::raw::c_longlong,
pub __bindgen_padding_0: u64,
pub __clang_max_align_nonce2: u128,
}
#[allow(clippy::unnecessary_operation, clippy::identity_op)]
const _: () = {
["Size of max_align_t"][::std::mem::size_of::<max_align_t>() - 32usize];
["Alignment of max_align_t"][::std::mem::align_of::<max_align_t>() - 16usize];
["Offset of field: max_align_t::__clang_max_align_nonce1"]
[::std::mem::offset_of!(max_align_t, __clang_max_align_nonce1) - 0usize];
["Offset of field: max_align_t::__clang_max_align_nonce2"]
[::std::mem::offset_of!(max_align_t, __clang_max_align_nonce2) - 16usize];
};
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct vampire_term_t {
_unused: [u8; 0],
}
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct vampire_literal_t {
_unused: [u8; 0],
}
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct vampire_formula_t {
_unused: [u8; 0],
}
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct vampire_unit_t {
_unused: [u8; 0],
}
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct vampire_clause_t {
_unused: [u8; 0],
}
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct vampire_problem_t {
_unused: [u8; 0],
}
pub const vampire_proof_result_t_VAMPIRE_PROOF: vampire_proof_result_t = 0;
pub const vampire_proof_result_t_VAMPIRE_SATISFIABLE: vampire_proof_result_t = 1;
pub const vampire_proof_result_t_VAMPIRE_TIMEOUT: vampire_proof_result_t = 2;
pub const vampire_proof_result_t_VAMPIRE_MEMORY_LIMIT: vampire_proof_result_t = 3;
pub const vampire_proof_result_t_VAMPIRE_UNKNOWN: vampire_proof_result_t = 4;
pub const vampire_proof_result_t_VAMPIRE_INCOMPLETE: vampire_proof_result_t = 5;
#[doc = " Result of a proving attempt"]
pub type vampire_proof_result_t = ::std::os::raw::c_uint;
pub const vampire_input_type_t_VAMPIRE_AXIOM: vampire_input_type_t = 0;
pub const vampire_input_type_t_VAMPIRE_NEGATED_CONJECTURE: vampire_input_type_t = 1;
pub const vampire_input_type_t_VAMPIRE_CONJECTURE: vampire_input_type_t = 2;
#[doc = " Input type for units"]
pub type vampire_input_type_t = ::std::os::raw::c_uint;
pub const vampire_inference_rule_t_INPUT: vampire_inference_rule_t = 0;
pub const vampire_inference_rule_t_GENERIC_FORMULA_CLAUSE_TRANSFORMATION: vampire_inference_rule_t =
1;
pub const vampire_inference_rule_t_NEGATED_CONJECTURE: vampire_inference_rule_t = 2;
pub const vampire_inference_rule_t_ANSWER_LITERAL_INJECTION: vampire_inference_rule_t = 3;
pub const vampire_inference_rule_t_ANSWER_LITERAL_INPUT_SKOLEMISATION: vampire_inference_rule_t = 4;
pub const vampire_inference_rule_t_CLAIM_DEFINITION: vampire_inference_rule_t = 5;
pub const vampire_inference_rule_t_RECTIFY: vampire_inference_rule_t = 6;
pub const vampire_inference_rule_t_CLOSURE: vampire_inference_rule_t = 7;
pub const vampire_inference_rule_t_FLATTEN: vampire_inference_rule_t = 8;
pub const vampire_inference_rule_t_ENNF: vampire_inference_rule_t = 9;
pub const vampire_inference_rule_t_NNF: vampire_inference_rule_t = 10;
pub const vampire_inference_rule_t_REDUCE_FALSE_TRUE: vampire_inference_rule_t = 11;
pub const vampire_inference_rule_t_DEFINITION_FOLDING: vampire_inference_rule_t = 12;
pub const vampire_inference_rule_t_THEORY_NORMALIZATION: vampire_inference_rule_t = 13;
pub const vampire_inference_rule_t_ALASCA_INTEGER_TRANSFORMATION: vampire_inference_rule_t = 14;
pub const vampire_inference_rule_t_SKOLEMIZE: vampire_inference_rule_t = 15;
pub const vampire_inference_rule_t_SKOLEM_SYMBOL_INTRODUCTION: vampire_inference_rule_t = 16;
pub const vampire_inference_rule_t_CLAUSIFY: vampire_inference_rule_t = 17;
pub const vampire_inference_rule_t_REORIENT_EQUATIONS: vampire_inference_rule_t = 18;
pub const vampire_inference_rule_t_GENERIC_FORMULA_CLAUSE_TRANSFORMATION_LAST:
vampire_inference_rule_t = 19;
pub const vampire_inference_rule_t_GENERIC_SIMPLIFYING_INFERENCE: vampire_inference_rule_t = 20;
pub const vampire_inference_rule_t_REORDER_LITERALS: vampire_inference_rule_t = 21;
pub const vampire_inference_rule_t_REMOVE_DUPLICATE_LITERALS: vampire_inference_rule_t = 22;
pub const vampire_inference_rule_t_TRIVIAL_INEQUALITY_REMOVAL: vampire_inference_rule_t = 23;
pub const vampire_inference_rule_t_EQUALITY_RESOLUTION_WITH_DELETION: vampire_inference_rule_t = 24;
pub const vampire_inference_rule_t_FORWARD_SUBSUMPTION_RESOLUTION: vampire_inference_rule_t = 25;
pub const vampire_inference_rule_t_BACKWARD_SUBSUMPTION_RESOLUTION: vampire_inference_rule_t = 26;
pub const vampire_inference_rule_t_FORWARD_DEMODULATION: vampire_inference_rule_t = 27;
pub const vampire_inference_rule_t_BACKWARD_DEMODULATION: vampire_inference_rule_t = 28;
pub const vampire_inference_rule_t_ALASCA_FWD_DEMODULATION: vampire_inference_rule_t = 29;
pub const vampire_inference_rule_t_ALASCA_BWD_DEMODULATION: vampire_inference_rule_t = 30;
pub const vampire_inference_rule_t_FORWARD_SUBSUMPTION_DEMODULATION: vampire_inference_rule_t = 31;
pub const vampire_inference_rule_t_BACKWARD_SUBSUMPTION_DEMODULATION: vampire_inference_rule_t = 32;
pub const vampire_inference_rule_t_FORWARD_LITERAL_REWRITING: vampire_inference_rule_t = 33;
pub const vampire_inference_rule_t_INNER_REWRITING: vampire_inference_rule_t = 34;
pub const vampire_inference_rule_t_CONDENSATION: vampire_inference_rule_t = 35;
pub const vampire_inference_rule_t_EVALUATION: vampire_inference_rule_t = 36;
pub const vampire_inference_rule_t_ALASCA_NORMALIZATION: vampire_inference_rule_t = 37;
pub const vampire_inference_rule_t_ALASCA_ABSTRACTION: vampire_inference_rule_t = 38;
pub const vampire_inference_rule_t_ALASCA_FLOOR_ELIMINATION: vampire_inference_rule_t = 39;
pub const vampire_inference_rule_t_CANCELLATION: vampire_inference_rule_t = 40;
pub const vampire_inference_rule_t_INTERPRETED_SIMPLIFICATION: vampire_inference_rule_t = 41;
pub const vampire_inference_rule_t_THEORY_FLATTENING: vampire_inference_rule_t = 42;
pub const vampire_inference_rule_t_TERM_ALGEBRA_DISTINCTNESS: vampire_inference_rule_t = 43;
pub const vampire_inference_rule_t_TERM_ALGEBRA_POSITIVE_INJECTIVITY_SIMPLIFYING:
vampire_inference_rule_t = 44;
pub const vampire_inference_rule_t_TERM_ALGEBRA_NEGATIVE_INJECTIVITY_SIMPLIFYING:
vampire_inference_rule_t = 45;
pub const vampire_inference_rule_t_GLOBAL_SUBSUMPTION: vampire_inference_rule_t = 46;
pub const vampire_inference_rule_t_DISTINCT_EQUALITY_REMOVAL: vampire_inference_rule_t = 47;
pub const vampire_inference_rule_t_GAUSSIAN_VARIABLE_ELIMINIATION: vampire_inference_rule_t = 48;
pub const vampire_inference_rule_t_ARITHMETIC_SUBTERM_GENERALIZATION: vampire_inference_rule_t = 49;
pub const vampire_inference_rule_t_ANSWER_LITERAL_REMOVAL: vampire_inference_rule_t = 50;
pub const vampire_inference_rule_t_ANSWER_LITERAL_JOIN_WITH_CONSTRAINTS: vampire_inference_rule_t =
51;
pub const vampire_inference_rule_t_ANSWER_LITERAL_JOIN_AS_ITE: vampire_inference_rule_t = 52;
pub const vampire_inference_rule_t_AVATAR_ASSERTION_REINTRODUCTION: vampire_inference_rule_t = 53;
pub const vampire_inference_rule_t_CASES_SIMP: vampire_inference_rule_t = 54;
pub const vampire_inference_rule_t_ALASCA_VIRAS_QE: vampire_inference_rule_t = 55;
pub const vampire_inference_rule_t_BOOL_SIMP: vampire_inference_rule_t = 56;
pub const vampire_inference_rule_t_FUNCTION_DEFINITION_DEMODULATION: vampire_inference_rule_t = 57;
pub const vampire_inference_rule_t_GENERIC_SIMPLIFYING_INFERENCE_LAST: vampire_inference_rule_t =
58;
pub const vampire_inference_rule_t_GENERIC_GENERATING_INFERENCE: vampire_inference_rule_t = 59;
pub const vampire_inference_rule_t_RESOLUTION: vampire_inference_rule_t = 60;
pub const vampire_inference_rule_t_CONSTRAINED_RESOLUTION: vampire_inference_rule_t = 61;
pub const vampire_inference_rule_t_FACTORING: vampire_inference_rule_t = 62;
pub const vampire_inference_rule_t_CONSTRAINED_FACTORING: vampire_inference_rule_t = 63;
pub const vampire_inference_rule_t_SUPERPOSITION: vampire_inference_rule_t = 64;
pub const vampire_inference_rule_t_FUNCTION_DEFINITION_REWRITING: vampire_inference_rule_t = 65;
pub const vampire_inference_rule_t_CONSTRAINED_SUPERPOSITION: vampire_inference_rule_t = 66;
pub const vampire_inference_rule_t_EQUALITY_FACTORING: vampire_inference_rule_t = 67;
pub const vampire_inference_rule_t_EQUALITY_RESOLUTION: vampire_inference_rule_t = 68;
pub const vampire_inference_rule_t_EXTENSIONALITY_RESOLUTION: vampire_inference_rule_t = 69;
pub const vampire_inference_rule_t_TERM_ALGEBRA_INJECTIVITY_GENERATING: vampire_inference_rule_t =
70;
pub const vampire_inference_rule_t_TERM_ALGEBRA_ACYCLICITY: vampire_inference_rule_t = 71;
pub const vampire_inference_rule_t_FOOL_PARAMODULATION: vampire_inference_rule_t = 72;
pub const vampire_inference_rule_t_UNIT_RESULTING_RESOLUTION: vampire_inference_rule_t = 73;
pub const vampire_inference_rule_t_INDUCTION_HYPERRESOLUTION: vampire_inference_rule_t = 74;
pub const vampire_inference_rule_t_INSTANTIATION: vampire_inference_rule_t = 75;
pub const vampire_inference_rule_t_ALASCA_FOURIER_MOTZKIN: vampire_inference_rule_t = 76;
pub const vampire_inference_rule_t_ALASCA_INTEGER_FOURIER_MOTZKIN: vampire_inference_rule_t = 77;
pub const vampire_inference_rule_t_ALASCA_TERM_FACTORING: vampire_inference_rule_t = 78;
pub const vampire_inference_rule_t_ALASCA_FLOOR_BOUNDS: vampire_inference_rule_t = 79;
pub const vampire_inference_rule_t_ALASCA_EQ_FACTORING: vampire_inference_rule_t = 80;
pub const vampire_inference_rule_t_ALASCA_LITERAL_FACTORING: vampire_inference_rule_t = 81;
pub const vampire_inference_rule_t_ALASCA_SUPERPOSITION: vampire_inference_rule_t = 82;
pub const vampire_inference_rule_t_ALASCA_COHERENCE: vampire_inference_rule_t = 83;
pub const vampire_inference_rule_t_ALASCA_COHERENCE_NORMALIZATION: vampire_inference_rule_t = 84;
pub const vampire_inference_rule_t_ALASCA_VARIABLE_ELIMINATION: vampire_inference_rule_t = 85;
pub const vampire_inference_rule_t_ARG_CONG: vampire_inference_rule_t = 86;
pub const vampire_inference_rule_t_INJECTIVITY: vampire_inference_rule_t = 87;
pub const vampire_inference_rule_t_PRIMITIVE_INSTANTIATION: vampire_inference_rule_t = 88;
pub const vampire_inference_rule_t_LEIBNIZ_ELIMINATION: vampire_inference_rule_t = 89;
pub const vampire_inference_rule_t_HILBERTS_CHOICE_INSTANCE: vampire_inference_rule_t = 90;
pub const vampire_inference_rule_t_NEGATIVE_EXT: vampire_inference_rule_t = 91;
pub const vampire_inference_rule_t_EQ_TO_DISEQ: vampire_inference_rule_t = 92;
pub const vampire_inference_rule_t_HOL_NOT_ELIMINATION: vampire_inference_rule_t = 93;
pub const vampire_inference_rule_t_BINARY_CONN_ELIMINATION: vampire_inference_rule_t = 94;
pub const vampire_inference_rule_t_VSIGMA_ELIMINATION: vampire_inference_rule_t = 95;
pub const vampire_inference_rule_t_VPI_ELIMINATION: vampire_inference_rule_t = 96;
pub const vampire_inference_rule_t_HOL_EQUALITY_ELIMINATION: vampire_inference_rule_t = 97;
pub const vampire_inference_rule_t_GENERIC_GENERATING_INFERENCE_LAST: vampire_inference_rule_t = 98;
pub const vampire_inference_rule_t_EQUALITY_PROXY_REPLACEMENT: vampire_inference_rule_t = 99;
pub const vampire_inference_rule_t_EQUALITY_PROXY_AXIOM1: vampire_inference_rule_t = 100;
pub const vampire_inference_rule_t_EQUALITY_PROXY_AXIOM2: vampire_inference_rule_t = 101;
pub const vampire_inference_rule_t_DEFINITION_UNFOLDING: vampire_inference_rule_t = 102;
pub const vampire_inference_rule_t_FUNCTION_DEFINITION: vampire_inference_rule_t = 103;
pub const vampire_inference_rule_t_PREDICATE_DEFINITION: vampire_inference_rule_t = 104;
pub const vampire_inference_rule_t_PREDICATE_DEFINITION_UNFOLDING: vampire_inference_rule_t = 105;
pub const vampire_inference_rule_t_PREDICATE_DEFINITION_MERGING: vampire_inference_rule_t = 106;
pub const vampire_inference_rule_t_POLARITY_FLIPPING: vampire_inference_rule_t = 107;
pub const vampire_inference_rule_t_UNUSED_PREDICATE_DEFINITION_REMOVAL: vampire_inference_rule_t =
108;
pub const vampire_inference_rule_t_PURE_PREDICATE_REMOVAL: vampire_inference_rule_t = 109;
pub const vampire_inference_rule_t_INEQUALITY_SPLITTING: vampire_inference_rule_t = 110;
pub const vampire_inference_rule_t_INEQUALITY_SPLITTING_NAME_INTRODUCTION:
vampire_inference_rule_t = 111;
pub const vampire_inference_rule_t_DISTINCTNESS_AXIOM: vampire_inference_rule_t = 112;
pub const vampire_inference_rule_t_BOOLEAN_TERM_ENCODING: vampire_inference_rule_t = 113;
pub const vampire_inference_rule_t_FOOL_ELIMINATION: vampire_inference_rule_t = 114;
pub const vampire_inference_rule_t_FOOL_ITE_DEFINITION: vampire_inference_rule_t = 115;
pub const vampire_inference_rule_t_FOOL_LET_DEFINITION: vampire_inference_rule_t = 116;
pub const vampire_inference_rule_t_FOOL_FORMULA_DEFINITION: vampire_inference_rule_t = 117;
pub const vampire_inference_rule_t_FOOL_MATCH_DEFINITION: vampire_inference_rule_t = 118;
pub const vampire_inference_rule_t_GENERAL_SPLITTING: vampire_inference_rule_t = 119;
pub const vampire_inference_rule_t_GENERAL_SPLITTING_COMPONENT: vampire_inference_rule_t = 120;
pub const vampire_inference_rule_t_COLOR_UNBLOCKING: vampire_inference_rule_t = 121;
pub const vampire_inference_rule_t_SAT_COLOR_ELIMINATION: vampire_inference_rule_t = 122;
pub const vampire_inference_rule_t_FORMULIFY: vampire_inference_rule_t = 123;
pub const vampire_inference_rule_t_FMB_FLATTENING: vampire_inference_rule_t = 124;
pub const vampire_inference_rule_t_FMB_FUNC_DEF: vampire_inference_rule_t = 125;
pub const vampire_inference_rule_t_FMB_DEF_INTRO: vampire_inference_rule_t = 126;
pub const vampire_inference_rule_t_MODEL_NOT_FOUND: vampire_inference_rule_t = 127;
pub const vampire_inference_rule_t_ADD_SORT_PREDICATES: vampire_inference_rule_t = 128;
pub const vampire_inference_rule_t_ADD_SORT_FUNCTIONS: vampire_inference_rule_t = 129;
pub const vampire_inference_rule_t_ANSWER_LITERAL_RESOLVER: vampire_inference_rule_t = 130;
pub const vampire_inference_rule_t_THEORY_TAUTOLOGY_SAT_CONFLICT: vampire_inference_rule_t = 131;
pub const vampire_inference_rule_t_GENERIC_AVATAR_INFERENCE: vampire_inference_rule_t = 132;
pub const vampire_inference_rule_t_AVATAR_DEFINITION: vampire_inference_rule_t = 133;
pub const vampire_inference_rule_t_AVATAR_COMPONENT: vampire_inference_rule_t = 134;
pub const vampire_inference_rule_t_AVATAR_REFUTATION: vampire_inference_rule_t = 135;
pub const vampire_inference_rule_t_AVATAR_REFUTATION_SMT: vampire_inference_rule_t = 136;
pub const vampire_inference_rule_t_AVATAR_SPLIT_CLAUSE: vampire_inference_rule_t = 137;
pub const vampire_inference_rule_t_AVATAR_CONTRADICTION_CLAUSE: vampire_inference_rule_t = 138;
pub const vampire_inference_rule_t_GENERIC_AVATAR_INFERENCE_LAST: vampire_inference_rule_t = 139;
pub const vampire_inference_rule_t_GENERIC_THEORY_AXIOM: vampire_inference_rule_t = 140;
pub const vampire_inference_rule_t_THA_COMMUTATIVITY: vampire_inference_rule_t = 141;
pub const vampire_inference_rule_t_THA_ASSOCIATIVITY: vampire_inference_rule_t = 142;
pub const vampire_inference_rule_t_THA_RIGHT_IDENTITY: vampire_inference_rule_t = 143;
pub const vampire_inference_rule_t_THA_LEFT_IDENTITY: vampire_inference_rule_t = 144;
pub const vampire_inference_rule_t_THA_INVERSE_OP_OP_INVERSES: vampire_inference_rule_t = 145;
pub const vampire_inference_rule_t_THA_INVERSE_OP_UNIT: vampire_inference_rule_t = 146;
pub const vampire_inference_rule_t_THA_INVERSE_ASSOC: vampire_inference_rule_t = 147;
pub const vampire_inference_rule_t_THA_NONREFLEX: vampire_inference_rule_t = 148;
pub const vampire_inference_rule_t_THA_TRANSITIVITY: vampire_inference_rule_t = 149;
pub const vampire_inference_rule_t_THA_ORDER_TOTALITY: vampire_inference_rule_t = 150;
pub const vampire_inference_rule_t_THA_ORDER_MONOTONICITY: vampire_inference_rule_t = 151;
pub const vampire_inference_rule_t_THA_ALASCA: vampire_inference_rule_t = 152;
pub const vampire_inference_rule_t_THA_PLUS_ONE_GREATER: vampire_inference_rule_t = 153;
pub const vampire_inference_rule_t_THA_ORDER_PLUS_ONE_DICHOTOMY: vampire_inference_rule_t = 154;
pub const vampire_inference_rule_t_THA_MINUS_MINUS_X: vampire_inference_rule_t = 155;
pub const vampire_inference_rule_t_THA_TIMES_ZERO: vampire_inference_rule_t = 156;
pub const vampire_inference_rule_t_THA_DISTRIBUTIVITY: vampire_inference_rule_t = 157;
pub const vampire_inference_rule_t_THA_DIVISIBILITY: vampire_inference_rule_t = 158;
pub const vampire_inference_rule_t_THA_MODULO_MULTIPLY: vampire_inference_rule_t = 159;
pub const vampire_inference_rule_t_THA_MODULO_POSITIVE: vampire_inference_rule_t = 160;
pub const vampire_inference_rule_t_THA_MODULO_SMALL: vampire_inference_rule_t = 161;
pub const vampire_inference_rule_t_THA_DIVIDES_MULTIPLY: vampire_inference_rule_t = 162;
pub const vampire_inference_rule_t_THA_NONDIVIDES_SKOLEM: vampire_inference_rule_t = 163;
pub const vampire_inference_rule_t_THA_ABS_EQUALS: vampire_inference_rule_t = 164;
pub const vampire_inference_rule_t_THA_ABS_MINUS_EQUALS: vampire_inference_rule_t = 165;
pub const vampire_inference_rule_t_THA_QUOTIENT_NON_ZERO: vampire_inference_rule_t = 166;
pub const vampire_inference_rule_t_THA_QUOTIENT_MULTIPLY: vampire_inference_rule_t = 167;
pub const vampire_inference_rule_t_THA_EXTRA_INTEGER_ORDERING: vampire_inference_rule_t = 168;
pub const vampire_inference_rule_t_THA_FLOOR_SMALL: vampire_inference_rule_t = 169;
pub const vampire_inference_rule_t_THA_FLOOR_BIG: vampire_inference_rule_t = 170;
pub const vampire_inference_rule_t_THA_CEILING_BIG: vampire_inference_rule_t = 171;
pub const vampire_inference_rule_t_THA_CEILING_SMALL: vampire_inference_rule_t = 172;
pub const vampire_inference_rule_t_THA_TRUNC1: vampire_inference_rule_t = 173;
pub const vampire_inference_rule_t_THA_TRUNC2: vampire_inference_rule_t = 174;
pub const vampire_inference_rule_t_THA_TRUNC3: vampire_inference_rule_t = 175;
pub const vampire_inference_rule_t_THA_TRUNC4: vampire_inference_rule_t = 176;
pub const vampire_inference_rule_t_THA_ARRAY_EXTENSIONALITY: vampire_inference_rule_t = 177;
pub const vampire_inference_rule_t_THA_BOOLEAN_ARRAY_EXTENSIONALITY: vampire_inference_rule_t = 178;
pub const vampire_inference_rule_t_THA_BOOLEAN_ARRAY_WRITE1: vampire_inference_rule_t = 179;
pub const vampire_inference_rule_t_THA_BOOLEAN_ARRAY_WRITE2: vampire_inference_rule_t = 180;
pub const vampire_inference_rule_t_THA_ARRAY_WRITE1: vampire_inference_rule_t = 181;
pub const vampire_inference_rule_t_THA_ARRAY_WRITE2: vampire_inference_rule_t = 182;
pub const vampire_inference_rule_t_TERM_ALGEBRA_ACYCLICITY_AXIOM: vampire_inference_rule_t = 183;
pub const vampire_inference_rule_t_TERM_ALGEBRA_DIRECT_SUBTERMS_AXIOM: vampire_inference_rule_t =
184;
pub const vampire_inference_rule_t_TERM_ALGEBRA_SUBTERMS_TRANSITIVE_AXIOM:
vampire_inference_rule_t = 185;
pub const vampire_inference_rule_t_TERM_ALGEBRA_DISCRIMINATION_AXIOM: vampire_inference_rule_t =
186;
pub const vampire_inference_rule_t_TERM_ALGEBRA_DISTINCTNESS_AXIOM: vampire_inference_rule_t = 187;
pub const vampire_inference_rule_t_TERM_ALGEBRA_EXHAUSTIVENESS_AXIOM: vampire_inference_rule_t =
188;
pub const vampire_inference_rule_t_TERM_ALGEBRA_INJECTIVITY_AXIOM: vampire_inference_rule_t = 189;
pub const vampire_inference_rule_t_FOOL_AXIOM_TRUE_NEQ_FALSE: vampire_inference_rule_t = 190;
pub const vampire_inference_rule_t_FOOL_AXIOM_ALL_IS_TRUE_OR_FALSE: vampire_inference_rule_t = 191;
pub const vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_ONE: vampire_inference_rule_t = 192;
pub const vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_TWO: vampire_inference_rule_t = 193;
pub const vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_THREE: vampire_inference_rule_t = 194;
pub const vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_RECURSION: vampire_inference_rule_t = 195;
pub const vampire_inference_rule_t_INT_INF_UP_INDUCTION_AXIOM: vampire_inference_rule_t = 196;
pub const vampire_inference_rule_t_INT_INF_DOWN_INDUCTION_AXIOM: vampire_inference_rule_t = 197;
pub const vampire_inference_rule_t_INT_FIN_UP_INDUCTION_AXIOM: vampire_inference_rule_t = 198;
pub const vampire_inference_rule_t_INT_FIN_DOWN_INDUCTION_AXIOM: vampire_inference_rule_t = 199;
pub const vampire_inference_rule_t_INT_DB_UP_INDUCTION_AXIOM: vampire_inference_rule_t = 200;
pub const vampire_inference_rule_t_INT_DB_DOWN_INDUCTION_AXIOM: vampire_inference_rule_t = 201;
#[doc = " Inference rules"]
pub type vampire_inference_rule_t = ::std::os::raw::c_uint;
#[doc = " A single step in a proof"]
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct vampire_proof_step_t {
pub id: ::std::os::raw::c_uint,
pub rule: vampire_inference_rule_t,
pub input_type: vampire_input_type_t,
pub premise_ids: *mut ::std::os::raw::c_uint,
pub premise_count: usize,
pub unit: *mut vampire_unit_t,
}
#[allow(clippy::unnecessary_operation, clippy::identity_op)]
const _: () = {
["Size of vampire_proof_step_t"][::std::mem::size_of::<vampire_proof_step_t>() - 40usize];
["Alignment of vampire_proof_step_t"][::std::mem::align_of::<vampire_proof_step_t>() - 8usize];
["Offset of field: vampire_proof_step_t::id"]
[::std::mem::offset_of!(vampire_proof_step_t, id) - 0usize];
["Offset of field: vampire_proof_step_t::rule"]
[::std::mem::offset_of!(vampire_proof_step_t, rule) - 4usize];
["Offset of field: vampire_proof_step_t::input_type"]
[::std::mem::offset_of!(vampire_proof_step_t, input_type) - 8usize];
["Offset of field: vampire_proof_step_t::premise_ids"]
[::std::mem::offset_of!(vampire_proof_step_t, premise_ids) - 16usize];
["Offset of field: vampire_proof_step_t::premise_count"]
[::std::mem::offset_of!(vampire_proof_step_t, premise_count) - 24usize];
["Offset of field: vampire_proof_step_t::unit"]
[::std::mem::offset_of!(vampire_proof_step_t, unit) - 32usize];
};
unsafe extern "C" {
#[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."]
pub fn vampire_prepare_for_next_proof();
}
unsafe extern "C" {
#[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."]
pub fn vampire_reset();
}
unsafe extern "C" {
#[doc = " Set a time limit in seconds (0 = no limit)."]
pub fn vampire_set_time_limit(seconds: ::std::os::raw::c_int);
}
unsafe extern "C" {
#[doc = " Set a time limit in deciseconds (10 = 1 second, 0 = no limit)."]
pub fn vampire_set_time_limit_deciseconds(deciseconds: ::std::os::raw::c_int);
}
unsafe extern "C" {
#[doc = " Set a time limit in milliseconds (1000 = 1 second, 0 = no limit)."]
pub fn vampire_set_time_limit_milliseconds(milliseconds: ::std::os::raw::c_int);
}
unsafe extern "C" {
#[doc = " Enable or disable proof output."]
pub fn vampire_set_show_proof(show: bool);
}
unsafe extern "C" {
#[doc = " Set saturation algorithm.\n @param algorithm Name of algorithm (e.g., \"lrs\", \"discount\", \"otter\")"]
pub fn vampire_set_saturation_algorithm(algorithm: *const ::std::os::raw::c_char);
}
unsafe extern "C" {
#[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"]
pub fn vampire_add_function(
name: *const ::std::os::raw::c_char,
arity: ::std::os::raw::c_uint,
) -> ::std::os::raw::c_uint;
}
unsafe extern "C" {
#[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"]
pub fn vampire_add_predicate(
name: *const ::std::os::raw::c_char,
arity: ::std::os::raw::c_uint,
) -> ::std::os::raw::c_uint;
}
unsafe extern "C" {
#[doc = " Create a variable term.\n @param index Variable index (0, 1, 2, ...)\n @return Term handle"]
pub fn vampire_var(index: ::std::os::raw::c_uint) -> *mut vampire_term_t;
}
unsafe extern "C" {
#[doc = " Create a constant term (0-arity function application).\n @param functor Function symbol index from vampire_add_function\n @return Term handle"]
pub fn vampire_constant(functor: ::std::os::raw::c_uint) -> *mut vampire_term_t;
}
unsafe extern "C" {
#[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"]
pub fn vampire_term(
functor: ::std::os::raw::c_uint,
args: *mut *mut vampire_term_t,
arg_count: usize,
) -> *mut vampire_term_t;
}
unsafe extern "C" {
#[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"]
pub fn vampire_eq(
positive: bool,
lhs: *mut vampire_term_t,
rhs: *mut vampire_term_t,
) -> *mut vampire_literal_t;
}
unsafe extern "C" {
#[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"]
pub fn vampire_lit(
pred: ::std::os::raw::c_uint,
positive: bool,
args: *mut *mut vampire_term_t,
arg_count: usize,
) -> *mut vampire_literal_t;
}
unsafe extern "C" {
#[doc = " Get the complementary (negated) literal.\n @param l The literal to negate\n @return Literal handle"]
pub fn vampire_neg(l: *mut vampire_literal_t) -> *mut vampire_literal_t;
}
unsafe extern "C" {
#[doc = " Create an atomic formula from a literal.\n @param l The literal\n @return Formula handle"]
pub fn vampire_atom(l: *mut vampire_literal_t) -> *mut vampire_formula_t;
}
unsafe extern "C" {
#[doc = " Create a negated formula (NOT f).\n @param f The formula to negate\n @return Formula handle"]
pub fn vampire_not(f: *mut vampire_formula_t) -> *mut vampire_formula_t;
}
unsafe extern "C" {
#[doc = " Create a conjunction (f1 AND f2 AND ...).\n @param formulas Array of formulas\n @param count Number of formulas\n @return Formula handle"]
pub fn vampire_and(
formulas: *mut *mut vampire_formula_t,
count: usize,
) -> *mut vampire_formula_t;
}
unsafe extern "C" {
#[doc = " Create a disjunction (f1 OR f2 OR ...).\n @param formulas Array of formulas\n @param count Number of formulas\n @return Formula handle"]
pub fn vampire_or(
formulas: *mut *mut vampire_formula_t,
count: usize,
) -> *mut vampire_formula_t;
}
unsafe extern "C" {
#[doc = " Create an implication (f1 => f2).\n @param lhs The antecedent\n @param rhs The consequent\n @return Formula handle"]
pub fn vampire_imp(
lhs: *mut vampire_formula_t,
rhs: *mut vampire_formula_t,
) -> *mut vampire_formula_t;
}
unsafe extern "C" {
#[doc = " Create an equivalence (f1 <=> f2).\n @param lhs Left-hand side\n @param rhs Right-hand side\n @return Formula handle"]
pub fn vampire_iff(
lhs: *mut vampire_formula_t,
rhs: *mut vampire_formula_t,
) -> *mut vampire_formula_t;
}
unsafe extern "C" {
#[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"]
pub fn vampire_forall(
var_index: ::std::os::raw::c_uint,
f: *mut vampire_formula_t,
) -> *mut vampire_formula_t;
}
unsafe extern "C" {
#[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"]
pub fn vampire_exists(
var_index: ::std::os::raw::c_uint,
f: *mut vampire_formula_t,
) -> *mut vampire_formula_t;
}
unsafe extern "C" {
#[doc = " Create a true (tautology) formula.\n @return Formula handle"]
pub fn vampire_true() -> *mut vampire_formula_t;
}
unsafe extern "C" {
#[doc = " Create a false (contradiction) formula.\n @return Formula handle"]
pub fn vampire_false() -> *mut vampire_formula_t;
}
unsafe extern "C" {
#[doc = " Create an axiom formula unit.\n @param f The formula\n @return Unit handle"]
pub fn vampire_axiom_formula(f: *mut vampire_formula_t) -> *mut vampire_unit_t;
}
unsafe extern "C" {
#[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"]
pub fn vampire_conjecture_formula(f: *mut vampire_formula_t) -> *mut vampire_unit_t;
}
unsafe extern "C" {
#[doc = " Create an axiom clause (disjunction of literals).\n @param literals Array of literals\n @param count Number of literals\n @return Clause handle"]
pub fn vampire_axiom_clause(
literals: *mut *mut vampire_literal_t,
count: usize,
) -> *mut vampire_clause_t;
}
unsafe extern "C" {
#[doc = " Create a conjecture clause (to be refuted).\n @param literals Array of literals\n @param count Number of literals\n @return Clause handle"]
pub fn vampire_conjecture_clause(
literals: *mut *mut vampire_literal_t,
count: usize,
) -> *mut vampire_clause_t;
}
unsafe extern "C" {
#[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"]
pub fn vampire_clause(
literals: *mut *mut vampire_literal_t,
count: usize,
input_type: vampire_input_type_t,
) -> *mut vampire_clause_t;
}
unsafe extern "C" {
#[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"]
pub fn vampire_problem_from_clauses(
clauses: *mut *mut vampire_clause_t,
count: usize,
) -> *mut vampire_problem_t;
}
unsafe extern "C" {
#[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"]
pub fn vampire_problem_from_units(
units: *mut *mut vampire_unit_t,
count: usize,
) -> *mut vampire_problem_t;
}
unsafe extern "C" {
#[doc = " Run the prover on a problem.\n @param problem The problem to solve\n @return The proof result"]
pub fn vampire_prove(problem: *mut vampire_problem_t) -> vampire_proof_result_t;
}
unsafe extern "C" {
#[doc = " Get the refutation (proof) after a successful vampire_prove() call.\n @return The empty clause with inference chain, or NULL if no proof"]
pub fn vampire_get_refutation() -> *mut vampire_unit_t;
}
unsafe extern "C" {
#[doc = " Print the proof to stdout.\n @param refutation The refutation from vampire_get_refutation()"]
pub fn vampire_print_proof(refutation: *mut vampire_unit_t);
}
unsafe extern "C" {
#[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"]
pub fn vampire_print_proof_to_file(
filename: *const ::std::os::raw::c_char,
refutation: *mut vampire_unit_t,
) -> ::std::os::raw::c_int;
}
unsafe extern "C" {
#[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."]
pub fn vampire_extract_proof(
refutation: *mut vampire_unit_t,
out_steps: *mut *mut vampire_proof_step_t,
out_count: *mut usize,
) -> ::std::os::raw::c_int;
}
unsafe extern "C" {
#[doc = " Free the proof steps array returned by vampire_extract_proof().\n @param steps The array to free\n @param count Number of steps"]
pub fn vampire_free_proof_steps(steps: *mut vampire_proof_step_t, count: usize);
}
unsafe extern "C" {
#[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."]
pub fn vampire_get_literals(
clause: *mut vampire_clause_t,
out_literals: *mut *mut *mut vampire_literal_t,
out_count: *mut usize,
) -> ::std::os::raw::c_int;
}
unsafe extern "C" {
#[doc = " Free the literals array returned by vampire_get_literals().\n @param literals The array to free"]
pub fn vampire_free_literals(literals: *mut *mut vampire_literal_t);
}
unsafe extern "C" {
#[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"]
pub fn vampire_unit_as_clause(unit: *mut vampire_unit_t) -> *mut vampire_clause_t;
}
unsafe extern "C" {
#[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"]
pub fn vampire_unit_as_formula(unit: *mut vampire_unit_t) -> *mut vampire_formula_t;
}
unsafe extern "C" {
#[doc = " Check if a clause is empty (represents false).\n @param clause The clause\n @return true if empty, false otherwise"]
pub fn vampire_clause_is_empty(clause: *mut vampire_clause_t) -> bool;
}
unsafe extern "C" {
#[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"]
pub fn vampire_term_to_string(term: *mut vampire_term_t) -> *mut ::std::os::raw::c_char;
}
unsafe extern "C" {
#[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"]
pub fn vampire_literal_to_string(
literal: *mut vampire_literal_t,
) -> *mut ::std::os::raw::c_char;
}
unsafe extern "C" {
#[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"]
pub fn vampire_clause_to_string(clause: *mut vampire_clause_t) -> *mut ::std::os::raw::c_char;
}
unsafe extern "C" {
#[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"]
pub fn vampire_formula_to_string(
formula: *mut vampire_formula_t,
) -> *mut ::std::os::raw::c_char;
}
unsafe extern "C" {
#[doc = " Free a string allocated by vampire_*_to_string functions.\n @param str The string to free"]
pub fn vampire_free_string(str: *mut ::std::os::raw::c_char);
}
unsafe extern "C" {
#[doc = " Get the name of an inference rule.\n @param rule The inference rule\n @return String name (static, do not free)"]
pub fn vampire_rule_name(rule: vampire_inference_rule_t) -> *const ::std::os::raw::c_char;
}
unsafe extern "C" {
#[doc = " Get the name of an input type.\n @param input_type The input type\n @return String name (static, do not free)"]
pub fn vampire_input_type_name(
input_type: vampire_input_type_t,
) -> *const ::std::os::raw::c_char;
}
unsafe extern "C" {
pub fn vampire_term_equal(a: *mut vampire_term_t, b: *mut vampire_term_t) -> bool;
}
unsafe extern "C" {
pub fn vampire_term_hash(a: *mut vampire_term_t) -> u64;
}
unsafe extern "C" {
pub fn vampire_formula_equal(a: *mut vampire_formula_t, b: *mut vampire_formula_t) -> bool;
}
unsafe extern "C" {
pub fn vampire_formula_hash(a: *mut vampire_formula_t) -> u64;
}