vampire-sys 0.1.0

Low-level FFI bindings to the Vampire theorem prover (use the 'vampire' crate instead)
Documentation

vampire-sys

Low-level FFI bindings to the Vampire theorem prover.

⚠️ You probably want the vampire crate instead

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

For safe, ergonomic Rust bindings, use the vampire crate.

What This Crate Provides

  • Raw C function bindings generated from the Vampire C API
  • Unsafe types and structures matching the C interface
  • Automatic building of the Vampire C++ library via CMake

Building

This crate automatically compiles the Vampire library from source using CMake. You need:

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

The build process:

  1. Uses CMake to configure the Vampire C++ library
  2. Builds the vampire_lib static library target
  3. Links against the appropriate C++ standard library for your platform

Platform Support

Tested and supported platforms:

  • Linux - Links against libstdc++
  • macOS - Links against libc++
  • Windows - Should work with MSVC (untested)

Thread Safety

The Vampire library is NOT thread-safe. If you use this crate directly, you must implement your own synchronization (e.g., with a global mutex). The vampire crate handles this for you.

License

Rust Bindings

This FFI crate is licensed under either of:

at your option.

Vampire Theorem Prover

The underlying Vampire theorem prover library that this crate links to is licensed under the BSD 3-Clause License. See vampire-lib/LICENCE for the complete license text.

When distributing applications using this crate, you must comply with both the Rust bindings license and the Vampire BSD 3-Clause license requirements.

Links