cvc5-sys 0.4.0

//! # cvc5-sys
//!
//! Low-level FFI bindings for the [cvc5](https://cvc5.github.io/) SMT solver.
//!
//! This crate provides raw C API bindings generated by `bindgen` from the
//! cvc5 C header (`cvc5/c/cvc5.h`). For a safe, idiomatic Rust API, see the
//! higher-level `cvc5` crate.
//!
//! # Build
//!
//! cvc5 must be built from source first. Point `CVC5_DIR` to the cvc5 source
//! root (containing `include/` and `build/`), or place a built cvc5 checkout
//! as a sibling `cvc5/` directory.
//!
//! ```text
//! CVC5_DIR=/path/to/cvc5 cargo build
//! ```
//!
//! # Example
//!
//! ```no_run
//! use cvc5_sys::*;
//!
//! unsafe {
//!     let tm = term_manager_new();
//!     let slv = new(tm);
//!
//!     set_logic(slv, c"QF_LIA".as_ptr());
//!     set_option(slv, c"produce-models".as_ptr(), c"true".as_ptr());
//!
//!     let int_sort = get_integer_sort(tm);
//!     let x = mk_const(tm, int_sort, c"x".as_ptr());
//!     let zero = mk_integer_int64(tm, 0);
//!
//!     let gt = mk_term(tm, Kind::Gt, 2, [x, zero].as_ptr());
//!     assert_formula(slv, gt);
//!
//!     let result = check_sat(slv);
//!     assert!(result_is_sat(result));
//!
//!     delete(slv);
//!     term_manager_delete(tm);
//! }
//! ```

#![allow(non_camel_case_types)]
#![allow(non_upper_case_globals)]
#![allow(non_snake_case)]
#![allow(clippy::unreadable_literal)]

include!(concat!(env!("OUT_DIR"), "/bindings.rs"));

#[cfg(feature = "parser")]
pub mod parser {
    include!(concat!(env!("OUT_DIR"), "/parser_bindings.rs"));
}