Crate vampire_sys 

Low-level FFI bindings to the Vampire theorem prover.

This crate provides unsafe, raw bindings to the Vampire C API. It is intended as an implementation detail of the vampire crate and is not meant to be used directly.

Usage

You probably want the vampire-prover crate instead.

The vampire crate provides a safe, ergonomic Rust API on top of these raw bindings. This crate (vampire-sys) only provides the low-level unsafe functions and types needed to interface with the Vampire C++ library.

Building

This crate automatically builds the Vampire library from source using CMake during compilation. You need:

• CMake 3.10 or later
• A C++ compiler (GCC, Clang, or MSVC)
• Standard C++ library

Thread Safety

The underlying Vampire library is not thread-safe. The vampire crate handles this by protecting all calls with a global mutex. If you use this crate directly, you must implement your own synchronization.

Platform Support

This crate supports:

• Linux (links against libstdc++)
• macOS (links against libc++)
• Other platforms may work but are untested

License

This FFI crate is dual-licensed under MIT OR Apache-2.0 (your choice).

The Vampire theorem prover library that this crate links to is licensed under the BSD 3-Clause License. Applications using this crate must comply with both the Rust bindings license and the Vampire BSD 3-Clause license.

Structs

max_align_t

vampire_clause_t

vampire_formula_t

vampire_literal_t

vampire_problem_t

vampire_proof_step_t

A single step in a proof

vampire_term_t

vampire_unit_t

Constants

__bool_true_false_are_defined

false_

true_

vampire_inference_rule_t_ADD_SORT_FUNCTIONS

vampire_inference_rule_t_ADD_SORT_PREDICATES

vampire_inference_rule_t_ALASCA_ABSTRACTION

vampire_inference_rule_t_ALASCA_BWD_DEMODULATION

vampire_inference_rule_t_ALASCA_COHERENCE

vampire_inference_rule_t_ALASCA_COHERENCE_NORMALIZATION

vampire_inference_rule_t_ALASCA_EQ_FACTORING

vampire_inference_rule_t_ALASCA_FLOOR_BOUNDS

vampire_inference_rule_t_ALASCA_FLOOR_ELIMINATION

vampire_inference_rule_t_ALASCA_FOURIER_MOTZKIN

vampire_inference_rule_t_ALASCA_FWD_DEMODULATION

vampire_inference_rule_t_ALASCA_INTEGER_FOURIER_MOTZKIN

vampire_inference_rule_t_ALASCA_INTEGER_TRANSFORMATION

vampire_inference_rule_t_ALASCA_LITERAL_FACTORING

vampire_inference_rule_t_ALASCA_NORMALIZATION

vampire_inference_rule_t_ALASCA_SUPERPOSITION

vampire_inference_rule_t_ALASCA_TERM_FACTORING

vampire_inference_rule_t_ALASCA_VARIABLE_ELIMINATION

vampire_inference_rule_t_ALASCA_VIRAS_QE

vampire_inference_rule_t_ANSWER_LITERAL_INJECTION

vampire_inference_rule_t_ANSWER_LITERAL_INPUT_SKOLEMISATION

vampire_inference_rule_t_ANSWER_LITERAL_JOIN_AS_ITE

vampire_inference_rule_t_ANSWER_LITERAL_JOIN_WITH_CONSTRAINTS

vampire_inference_rule_t_ANSWER_LITERAL_REMOVAL

vampire_inference_rule_t_ANSWER_LITERAL_RESOLVER

vampire_inference_rule_t_ARG_CONG

vampire_inference_rule_t_ARITHMETIC_SUBTERM_GENERALIZATION

vampire_inference_rule_t_AVATAR_ASSERTION_REINTRODUCTION

vampire_inference_rule_t_AVATAR_COMPONENT

vampire_inference_rule_t_AVATAR_CONTRADICTION_CLAUSE

vampire_inference_rule_t_AVATAR_DEFINITION

vampire_inference_rule_t_AVATAR_REFUTATION

vampire_inference_rule_t_AVATAR_REFUTATION_SMT

vampire_inference_rule_t_AVATAR_SPLIT_CLAUSE

vampire_inference_rule_t_BACKWARD_DEMODULATION

vampire_inference_rule_t_BACKWARD_SUBSUMPTION_DEMODULATION

vampire_inference_rule_t_BACKWARD_SUBSUMPTION_RESOLUTION

vampire_inference_rule_t_BINARY_CONN_ELIMINATION

vampire_inference_rule_t_BOOLEAN_TERM_ENCODING

vampire_inference_rule_t_BOOL_SIMP

vampire_inference_rule_t_CANCELLATION

vampire_inference_rule_t_CASES_SIMP

vampire_inference_rule_t_CLAIM_DEFINITION

vampire_inference_rule_t_CLAUSIFY

vampire_inference_rule_t_CLOSURE

vampire_inference_rule_t_COLOR_UNBLOCKING

vampire_inference_rule_t_CONDENSATION

vampire_inference_rule_t_CONSTRAINED_FACTORING

vampire_inference_rule_t_CONSTRAINED_RESOLUTION

vampire_inference_rule_t_CONSTRAINED_SUPERPOSITION

vampire_inference_rule_t_DEFINITION_FOLDING

vampire_inference_rule_t_DEFINITION_UNFOLDING

vampire_inference_rule_t_DISTINCTNESS_AXIOM

vampire_inference_rule_t_DISTINCT_EQUALITY_REMOVAL

vampire_inference_rule_t_ENNF

vampire_inference_rule_t_EQUALITY_FACTORING

vampire_inference_rule_t_EQUALITY_PROXY_AXIOM1

vampire_inference_rule_t_EQUALITY_PROXY_AXIOM2

vampire_inference_rule_t_EQUALITY_PROXY_REPLACEMENT

vampire_inference_rule_t_EQUALITY_RESOLUTION

vampire_inference_rule_t_EQUALITY_RESOLUTION_WITH_DELETION

vampire_inference_rule_t_EQ_TO_DISEQ

vampire_inference_rule_t_EVALUATION

vampire_inference_rule_t_EXTENSIONALITY_RESOLUTION

vampire_inference_rule_t_FACTORING

vampire_inference_rule_t_FLATTEN

vampire_inference_rule_t_FMB_DEF_INTRO

vampire_inference_rule_t_FMB_FLATTENING

vampire_inference_rule_t_FMB_FUNC_DEF

vampire_inference_rule_t_FOOL_AXIOM_ALL_IS_TRUE_OR_FALSE

vampire_inference_rule_t_FOOL_AXIOM_TRUE_NEQ_FALSE

vampire_inference_rule_t_FOOL_ELIMINATION

vampire_inference_rule_t_FOOL_FORMULA_DEFINITION

vampire_inference_rule_t_FOOL_ITE_DEFINITION

vampire_inference_rule_t_FOOL_LET_DEFINITION

vampire_inference_rule_t_FOOL_MATCH_DEFINITION

vampire_inference_rule_t_FOOL_PARAMODULATION

vampire_inference_rule_t_FORMULIFY

vampire_inference_rule_t_FORWARD_DEMODULATION

vampire_inference_rule_t_FORWARD_LITERAL_REWRITING

vampire_inference_rule_t_FORWARD_SUBSUMPTION_DEMODULATION

vampire_inference_rule_t_FORWARD_SUBSUMPTION_RESOLUTION

vampire_inference_rule_t_FUNCTION_DEFINITION

vampire_inference_rule_t_FUNCTION_DEFINITION_DEMODULATION

vampire_inference_rule_t_FUNCTION_DEFINITION_REWRITING

vampire_inference_rule_t_GAUSSIAN_VARIABLE_ELIMINIATION

vampire_inference_rule_t_GENERAL_SPLITTING

vampire_inference_rule_t_GENERAL_SPLITTING_COMPONENT

vampire_inference_rule_t_GENERIC_AVATAR_INFERENCE

vampire_inference_rule_t_GENERIC_AVATAR_INFERENCE_LAST

vampire_inference_rule_t_GENERIC_FORMULA_CLAUSE_TRANSFORMATION

vampire_inference_rule_t_GENERIC_FORMULA_CLAUSE_TRANSFORMATION_LAST

vampire_inference_rule_t_GENERIC_GENERATING_INFERENCE

vampire_inference_rule_t_GENERIC_GENERATING_INFERENCE_LAST

vampire_inference_rule_t_GENERIC_SIMPLIFYING_INFERENCE

vampire_inference_rule_t_GENERIC_SIMPLIFYING_INFERENCE_LAST

vampire_inference_rule_t_GENERIC_THEORY_AXIOM

vampire_inference_rule_t_GLOBAL_SUBSUMPTION

vampire_inference_rule_t_HILBERTS_CHOICE_INSTANCE

vampire_inference_rule_t_HOL_EQUALITY_ELIMINATION

vampire_inference_rule_t_HOL_NOT_ELIMINATION

vampire_inference_rule_t_INDUCTION_HYPERRESOLUTION

vampire_inference_rule_t_INEQUALITY_SPLITTING

vampire_inference_rule_t_INEQUALITY_SPLITTING_NAME_INTRODUCTION

vampire_inference_rule_t_INJECTIVITY

vampire_inference_rule_t_INNER_REWRITING

vampire_inference_rule_t_INPUT

vampire_inference_rule_t_INSTANTIATION

vampire_inference_rule_t_INTERPRETED_SIMPLIFICATION

vampire_inference_rule_t_INT_DB_DOWN_INDUCTION_AXIOM

vampire_inference_rule_t_INT_DB_UP_INDUCTION_AXIOM

vampire_inference_rule_t_INT_FIN_DOWN_INDUCTION_AXIOM

vampire_inference_rule_t_INT_FIN_UP_INDUCTION_AXIOM

vampire_inference_rule_t_INT_INF_DOWN_INDUCTION_AXIOM

vampire_inference_rule_t_INT_INF_UP_INDUCTION_AXIOM

vampire_inference_rule_t_LEIBNIZ_ELIMINATION

vampire_inference_rule_t_MODEL_NOT_FOUND

vampire_inference_rule_t_NEGATED_CONJECTURE

vampire_inference_rule_t_NEGATIVE_EXT

vampire_inference_rule_t_NNF

vampire_inference_rule_t_POLARITY_FLIPPING

vampire_inference_rule_t_PREDICATE_DEFINITION

vampire_inference_rule_t_PREDICATE_DEFINITION_MERGING

vampire_inference_rule_t_PREDICATE_DEFINITION_UNFOLDING

vampire_inference_rule_t_PRIMITIVE_INSTANTIATION

vampire_inference_rule_t_PURE_PREDICATE_REMOVAL

vampire_inference_rule_t_RECTIFY

vampire_inference_rule_t_REDUCE_FALSE_TRUE

vampire_inference_rule_t_REMOVE_DUPLICATE_LITERALS

vampire_inference_rule_t_REORDER_LITERALS

vampire_inference_rule_t_REORIENT_EQUATIONS

vampire_inference_rule_t_RESOLUTION

vampire_inference_rule_t_SAT_COLOR_ELIMINATION

vampire_inference_rule_t_SKOLEMIZE

vampire_inference_rule_t_SKOLEM_SYMBOL_INTRODUCTION

vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_ONE

vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_RECURSION

vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_THREE

vampire_inference_rule_t_STRUCT_INDUCTION_AXIOM_TWO

vampire_inference_rule_t_SUPERPOSITION

vampire_inference_rule_t_TERM_ALGEBRA_ACYCLICITY

vampire_inference_rule_t_TERM_ALGEBRA_ACYCLICITY_AXIOM

vampire_inference_rule_t_TERM_ALGEBRA_DIRECT_SUBTERMS_AXIOM

vampire_inference_rule_t_TERM_ALGEBRA_DISCRIMINATION_AXIOM

vampire_inference_rule_t_TERM_ALGEBRA_DISTINCTNESS

vampire_inference_rule_t_TERM_ALGEBRA_DISTINCTNESS_AXIOM

vampire_inference_rule_t_TERM_ALGEBRA_EXHAUSTIVENESS_AXIOM

vampire_inference_rule_t_TERM_ALGEBRA_INJECTIVITY_AXIOM

vampire_inference_rule_t_TERM_ALGEBRA_INJECTIVITY_GENERATING

vampire_inference_rule_t_TERM_ALGEBRA_NEGATIVE_INJECTIVITY_SIMPLIFYING

vampire_inference_rule_t_TERM_ALGEBRA_POSITIVE_INJECTIVITY_SIMPLIFYING

vampire_inference_rule_t_TERM_ALGEBRA_SUBTERMS_TRANSITIVE_AXIOM

vampire_inference_rule_t_THA_ABS_EQUALS

vampire_inference_rule_t_THA_ABS_MINUS_EQUALS

vampire_inference_rule_t_THA_ALASCA

vampire_inference_rule_t_THA_ARRAY_EXTENSIONALITY

vampire_inference_rule_t_THA_ARRAY_WRITE1

vampire_inference_rule_t_THA_ARRAY_WRITE2

vampire_inference_rule_t_THA_ASSOCIATIVITY

vampire_inference_rule_t_THA_BOOLEAN_ARRAY_EXTENSIONALITY

vampire_inference_rule_t_THA_BOOLEAN_ARRAY_WRITE1

vampire_inference_rule_t_THA_BOOLEAN_ARRAY_WRITE2

vampire_inference_rule_t_THA_CEILING_BIG

vampire_inference_rule_t_THA_CEILING_SMALL

vampire_inference_rule_t_THA_COMMUTATIVITY

vampire_inference_rule_t_THA_DISTRIBUTIVITY

vampire_inference_rule_t_THA_DIVIDES_MULTIPLY

vampire_inference_rule_t_THA_DIVISIBILITY

vampire_inference_rule_t_THA_EXTRA_INTEGER_ORDERING

vampire_inference_rule_t_THA_FLOOR_BIG

vampire_inference_rule_t_THA_FLOOR_SMALL

vampire_inference_rule_t_THA_INVERSE_ASSOC

vampire_inference_rule_t_THA_INVERSE_OP_OP_INVERSES

vampire_inference_rule_t_THA_INVERSE_OP_UNIT

vampire_inference_rule_t_THA_LEFT_IDENTITY

vampire_inference_rule_t_THA_MINUS_MINUS_X

vampire_inference_rule_t_THA_MODULO_MULTIPLY

vampire_inference_rule_t_THA_MODULO_POSITIVE

vampire_inference_rule_t_THA_MODULO_SMALL

vampire_inference_rule_t_THA_NONDIVIDES_SKOLEM

vampire_inference_rule_t_THA_NONREFLEX

vampire_inference_rule_t_THA_ORDER_MONOTONICITY

vampire_inference_rule_t_THA_ORDER_PLUS_ONE_DICHOTOMY

vampire_inference_rule_t_THA_ORDER_TOTALITY

vampire_inference_rule_t_THA_PLUS_ONE_GREATER

vampire_inference_rule_t_THA_QUOTIENT_MULTIPLY

vampire_inference_rule_t_THA_QUOTIENT_NON_ZERO

vampire_inference_rule_t_THA_RIGHT_IDENTITY

vampire_inference_rule_t_THA_TIMES_ZERO

vampire_inference_rule_t_THA_TRANSITIVITY

vampire_inference_rule_t_THA_TRUNC1

vampire_inference_rule_t_THA_TRUNC2

vampire_inference_rule_t_THA_TRUNC3

vampire_inference_rule_t_THA_TRUNC4

vampire_inference_rule_t_THEORY_FLATTENING

vampire_inference_rule_t_THEORY_NORMALIZATION

vampire_inference_rule_t_THEORY_TAUTOLOGY_SAT_CONFLICT

vampire_inference_rule_t_TRIVIAL_INEQUALITY_REMOVAL

vampire_inference_rule_t_UNIT_RESULTING_RESOLUTION

vampire_inference_rule_t_UNUSED_PREDICATE_DEFINITION_REMOVAL

vampire_inference_rule_t_VPI_ELIMINATION

vampire_inference_rule_t_VSIGMA_ELIMINATION

vampire_input_type_t_VAMPIRE_AXIOM

vampire_input_type_t_VAMPIRE_CONJECTURE

vampire_input_type_t_VAMPIRE_NEGATED_CONJECTURE

vampire_proof_result_t_VAMPIRE_INCOMPLETE

vampire_proof_result_t_VAMPIRE_MEMORY_LIMIT

vampire_proof_result_t_VAMPIRE_PROOF

vampire_proof_result_t_VAMPIRE_SATISFIABLE

vampire_proof_result_t_VAMPIRE_TIMEOUT

vampire_proof_result_t_VAMPIRE_UNKNOWN

Functions

vampire_add_function^⚠

Register a function symbol with the given name and arity. For constants, use arity 0. @param name Symbol name (null-terminated string) @param arity Number of arguments @return functor index for use in term construction

vampire_add_predicate^⚠

Register a predicate symbol with the given name and arity. @param name Symbol name (null-terminated string) @param arity Number of arguments @return predicate index for use in literal construction

vampire_and^⚠

Create a conjunction (f1 AND f2 AND …). @param formulas Array of formulas @param count Number of formulas @return Formula handle

vampire_atom^⚠

Create an atomic formula from a literal. @param l The literal @return Formula handle

vampire_axiom_clause^⚠

Create an axiom clause (disjunction of literals). @param literals Array of literals @param count Number of literals @return Clause handle

vampire_axiom_formula^⚠

Create an axiom formula unit. @param f The formula @return Unit handle

vampire_clause^⚠

Create a clause with specified input type. @param literals Array of literals @param count Number of literals @param input_type The type of input @return Clause handle

vampire_clause_is_empty^⚠

Check if a clause is empty (represents false). @param clause The clause @return true if empty, false otherwise

vampire_clause_to_string^⚠

Convert a clause to a string representation. @param clause The clause @return Allocated string (must be freed with vampire_free_string), or NULL on error

vampire_conjecture_clause^⚠

Create a conjecture clause (to be refuted). @param literals Array of literals @param count Number of literals @return Clause handle

vampire_conjecture_formula^⚠

Create a conjecture formula unit (to be proven). The formula is automatically negated for refutation-based proving. @param f The formula to prove @return Unit handle

vampire_constant^⚠

Create a constant term (0-arity function application). @param functor Function symbol index from vampire_add_function @return Term handle

vampire_eq^⚠

Create an equality literal (s = t or s != t). @param positive true for equality, false for disequality @param lhs Left-hand side term @param rhs Right-hand side term @return Literal handle

vampire_exists^⚠

Create an existentially quantified formula (exists x. f). @param var_index The variable index to bind @param f The body formula @return Formula handle

vampire_extract_proof^⚠

Extract the proof as a sequence of steps. Steps are returned in topological order (premises before conclusions). The last step is the empty clause (refutation).

vampire_false^⚠

Create a false (contradiction) formula. @return Formula handle

vampire_forall^⚠

Create a universally quantified formula (forall x. f). @param var_index The variable index to bind @param f The body formula @return Formula handle

vampire_formula_equal^⚠

vampire_formula_hash^⚠

vampire_formula_to_string^⚠

Convert a formula to a string representation. @param formula The formula @return Allocated string (must be freed with vampire_free_string), or NULL on error

vampire_free_literals^⚠

Free the literals array returned by vampire_get_literals(). @param literals The array to free

vampire_free_proof_steps^⚠

Free the proof steps array returned by vampire_extract_proof(). @param steps The array to free @param count Number of steps

vampire_free_string^⚠

Free a string allocated by vampire_*_to_string functions. @param str The string to free

vampire_get_literals^⚠

Get the literals of a clause as an array. @param clause The clause @param out_literals Pointer to receive the array of literals @param out_count Pointer to receive the number of literals @return 0 on success, -1 on error

vampire_get_refutation^⚠

Get the refutation (proof) after a successful vampire_prove() call. @return The empty clause with inference chain, or NULL if no proof

vampire_iff^⚠

Create an equivalence (f1 <=> f2). @param lhs Left-hand side @param rhs Right-hand side @return Formula handle

vampire_imp^⚠

Create an implication (f1 => f2). @param lhs The antecedent @param rhs The consequent @return Formula handle

vampire_input_type_name^⚠

Get the name of an input type. @param input_type The input type @return String name (static, do not free)

vampire_lit^⚠

Create a predicate literal. @param pred Predicate symbol index from vampire_add_predicate @param positive true for positive literal, false for negated @param args Array of argument terms @param arg_count Number of arguments @return Literal handle

vampire_literal_to_string^⚠

Convert a literal to a string representation. @param literal The literal @return Allocated string (must be freed with vampire_free_string), or NULL on error

vampire_neg^⚠

Get the complementary (negated) literal. @param l The literal to negate @return Literal handle

vampire_not^⚠

Create a negated formula (NOT f). @param f The formula to negate @return Formula handle

vampire_or^⚠

Create a disjunction (f1 OR f2 OR …). @param formulas Array of formulas @param count Number of formulas @return Formula handle

vampire_prepare_for_next_proof^⚠

Prepare for running another proof (light reset). Call this between independent proving attempts to reset the global ordering and other per-proof state.

vampire_print_proof^⚠

Print the proof to stdout. @param refutation The refutation from vampire_get_refutation()

vampire_print_proof_to_file^⚠

Print the proof to a file. @param filename Path to output file (null-terminated string) @param refutation The refutation from vampire_get_refutation() @return 0 on success, -1 on error

vampire_problem_from_clauses^⚠

Create a problem from an array of clauses. @param clauses Array of clause handles @param count Number of clauses @return Problem handle

vampire_problem_from_units^⚠

Create a problem from an array of units (clauses or formulas). Formulas will be clausified during preprocessing. @param units Array of unit handles @param count Number of units @return Problem handle

vampire_prove^⚠

Run the prover on a problem. @param problem The problem to solve @return The proof result

vampire_reset^⚠

Fully reset the Vampire state for a fresh start. This resets all static caches, clears the signature, and reinitializes the environment. After calling this, the state is as if Vampire was just started.

vampire_rule_name^⚠

Get the name of an inference rule. @param rule The inference rule @return String name (static, do not free)

vampire_set_saturation_algorithm^⚠

Set saturation algorithm. @param algorithm Name of algorithm (e.g., “lrs”, “discount”, “otter”)

vampire_set_show_proof^⚠

Enable or disable proof output.

vampire_set_time_limit^⚠

Set a time limit in seconds (0 = no limit).

vampire_set_time_limit_deciseconds^⚠

Set a time limit in deciseconds (10 = 1 second, 0 = no limit).

vampire_set_time_limit_milliseconds^⚠

Set a time limit in milliseconds (1000 = 1 second, 0 = no limit).

vampire_term^⚠

Create a function application term. @param functor Function symbol index from vampire_add_function @param args Array of argument terms @param arg_count Number of arguments @return Term handle

vampire_term_equal^⚠

vampire_term_hash^⚠

vampire_term_to_string^⚠

Convert a term to a string representation. @param term The term @return Allocated string (must be freed with vampire_free_string), or NULL on error

vampire_true^⚠

Create a true (tautology) formula. @return Formula handle

vampire_unit_as_clause^⚠

Get the clause from a unit (if the unit is a clause). @param unit The unit @return Clause handle, or NULL if unit is not a clause

vampire_unit_as_formula^⚠

Get the formula from a unit (if the unit is a formula). @param unit The unit @return Formula handle, or NULL if unit is not a formula

vampire_var^⚠

Create a variable term. @param index Variable index (0, 1, 2, …) @return Term handle

Type Aliases

vampire_inference_rule_t

Inference rules

vampire_input_type_t

Input type for units

vampire_proof_result_t

Result of a proving attempt

wchar_t