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§

__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