cvc5_sys/lib.rs
1//! # cvc5-sys
2//!
3//! Low-level FFI bindings for the [cvc5](https://cvc5.github.io/) SMT solver.
4//!
5//! This crate provides raw C API bindings generated by `bindgen` from the
6//! cvc5 C header (`cvc5/c/cvc5.h`). For a safe, idiomatic Rust API, see the
7//! higher-level `cvc5` crate.
8//!
9//! # Build
10//!
11//! cvc5 must be built from source first. Point `CVC5_DIR` to the cvc5 source
12//! root (containing `include/` and `build/`), or place a built cvc5 checkout
13//! as a sibling `cvc5/` directory.
14//!
15//! ```text
16//! CVC5_DIR=/path/to/cvc5 cargo build
17//! ```
18//!
19//! # Example
20//!
21//! ```no_run
22//! use cvc5_sys::*;
23//!
24//! unsafe {
25//! let tm = cvc5_term_manager_new();
26//! let slv = cvc5_new(tm);
27//!
28//! cvc5_set_logic(slv, c"QF_LIA".as_ptr());
29//! cvc5_set_option(slv, c"produce-models".as_ptr(), c"true".as_ptr());
30//!
31//! let int_sort = cvc5_get_integer_sort(tm);
32//! let x = cvc5_mk_const(tm, int_sort, c"x".as_ptr());
33//! let zero = cvc5_mk_integer_int64(tm, 0);
34//!
35//! let gt = cvc5_mk_term(tm, Cvc5Kind::CVC5_KIND_GT, 2, [x, zero].as_ptr());
36//! cvc5_assert_formula(slv, gt);
37//!
38//! let result = cvc5_check_sat(slv);
39//! assert!(cvc5_result_is_sat(result));
40//!
41//! cvc5_delete(slv);
42//! cvc5_term_manager_delete(tm);
43//! }
44//! ```
45
46#![allow(non_camel_case_types)]
47#![allow(non_upper_case_globals)]
48#![allow(non_snake_case)]
49#![allow(clippy::unreadable_literal)]
50
51include!(concat!(env!("OUT_DIR"), "/bindings.rs"));
52
53#[cfg(feature = "parser")]
54pub mod parser {
55 include!(concat!(env!("OUT_DIR"), "/parser_bindings.rs"));
56}