Crate vampire_sys

Expand description

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§

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_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_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_var^⚠: Create a variable term. @param index Variable index (0, 1, 2, …) @return Term handle

Type Aliases§

vampire_inference_rule_t: Inference rules (subset of commonly used rules)
vampire_input_type_t: Input type for units
vampire_proof_result_t: Result of a proving attempt
wchar_t