cvc5-sys 0.3.1

//! # 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 = cvc5_term_manager_new();
//!     let slv = cvc5_new(tm);
//!
//!     cvc5_set_logic(slv, c"QF_LIA".as_ptr());
//!     cvc5_set_option(slv, c"produce-models".as_ptr(), c"true".as_ptr());
//!
//!     let int_sort = cvc5_get_integer_sort(tm);
//!     let x = cvc5_mk_const(tm, int_sort, c"x".as_ptr());
//!     let zero = cvc5_mk_integer_int64(tm, 0);
//!
//!     let gt = cvc5_mk_term(tm, Cvc5Kind::CVC5_KIND_GT, 2, [x, zero].as_ptr());
//!     cvc5_assert_formula(slv, gt);
//!
//!     let result = cvc5_check_sat(slv);
//!     assert!(cvc5_result_is_sat(result));
//!
//!     cvc5_delete(slv);
//!     cvc5_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"));
}