pindakaas_intel_sat/
lib.rs

1//! This crate provides low-level bindings to the [Intel
2//! SAT](https://github.com/alexander-nadel/intel_sat_solver) solver aimed at
3//! the [Pindakaas](https://crates.io/crates/pindakaas) library.
4
5use std::ffi::{c_char, c_int, c_void};
6
7extern "C" {
8	// IPASIR definitions
9	/// Intel SAT `ipasir_signature` implementation.
10	pub fn intel_sat_signature() -> *const c_char;
11	/// Intel SAT `ipasir_init` implementation.
12	pub fn intel_sat_init() -> *mut c_void;
13	/// Intel SAT `ipasir_release` implementation.
14	pub fn intel_sat_release(slv: *mut c_void);
15	/// Intel SAT `ipasir_add` implementation.
16	pub fn intel_sat_add(slv: *mut c_void, lit: i32);
17	/// Intel SAT `ipasir_assume` implementation.
18	pub fn intel_sat_assume(slv: *mut c_void, lit: i32);
19	/// Intel SAT `ipasir_solve` implementation.
20	pub fn intel_sat_solve(slv: *mut c_void) -> c_int;
21	/// Intel SAT `ipasir_val` implementation.
22	pub fn intel_sat_val(slv: *mut c_void, lit: i32) -> i32;
23	/// Intel SAT `ipasir_failed` implementation.
24	pub fn intel_sat_failed(slv: *mut c_void, lit: i32) -> c_int;
25	/// Intel SAT `ipasir_set_terminate` implementation.
26	pub fn intel_sat_set_terminate(
27		slv: *mut c_void,
28		data: *mut c_void,
29		cb: Option<unsafe extern "C" fn(*mut c_void) -> c_int>,
30	);
31	/// Intel SAT `ipasir_set_learn` implementation.
32	pub fn intel_sat_set_learn(
33		slv: *mut c_void,
34		data: *mut c_void,
35		max_len: c_int,
36		cb: Option<unsafe extern "C" fn(*mut c_void, *const i32)>,
37	);
38}
pindakaas_intel_sat/lib.rs

pindakaas_intel_sat/
lib.rs
