vampire_sys/lib.rs
1//! Low-level FFI bindings to the Vampire theorem prover.
2//!
3//! This crate provides unsafe, raw bindings to the Vampire C API. It is intended
4//! as an implementation detail of the `vampire` crate and is not meant to be used
5//! directly.
6//!
7//! # Usage
8//!
9//! **You probably want the [`vampire-prover`](https://docs.rs/vampire-prover) crate instead.**
10//!
11//! The `vampire` crate provides a safe, ergonomic Rust API on top of these raw
12//! bindings. This crate (`vampire-sys`) only provides the low-level unsafe
13//! functions and types needed to interface with the Vampire C++ library.
14//!
15//! # Building
16//!
17//! This crate automatically builds the Vampire library from source using CMake
18//! during compilation. You need:
19//! - CMake 3.10 or later
20//! - A C++ compiler (GCC, Clang, or MSVC)
21//! - Standard C++ library
22//!
23//! # Thread Safety
24//!
25//! The underlying Vampire library is **not thread-safe**. The `vampire` crate
26//! handles this by protecting all calls with a global mutex. If you use this
27//! crate directly, you must implement your own synchronization.
28//!
29//! # Platform Support
30//!
31//! This crate supports:
32//! - Linux (links against libstdc++)
33//! - macOS (links against libc++)
34//! - Other platforms may work but are untested
35//!
36//! # License
37//!
38//! This FFI crate is dual-licensed under MIT OR Apache-2.0 (your choice).
39//!
40//! The Vampire theorem prover library that this crate links to is licensed under
41//! the BSD 3-Clause License. Applications using this crate must comply with both
42//! the Rust bindings license and the Vampire BSD 3-Clause license.
43
44#![allow(non_upper_case_globals)]
45#![allow(non_camel_case_types)]
46#![allow(non_snake_case)]
47
48mod bindings;
49pub use bindings::*;