rustsat_glucose/
lib.rs

1//! # rustsat-glucose - Interface to the Glucose SAT Solver for RustSAT
2//!
3//! The Glucose SAT solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library.
4//!
5//! ## Features
6//!
7//! - `debug`: if this feature is enables, the Cpp library will be built with debug and check functionality if the Rust project is built in debug mode
8//! - `quiet`: disable all glucose-internal printing to `stdout` during solving (on by default)
9//!
10//! ## Glucose Version
11//!
12//! The version of Glucose in this crate is Version 4.2.1.
13//! The used Cpp source can be found
14//! [here](https://github.com/chrjabs/rustsat/tree/main/glucose/cppsrc).
15//!
16//! ## Minimum Supported Rust Version (MSRV)
17//!
18//! Currently, the MSRV is 1.76.0, the plan is to always support an MSRV that is at least a year
19//! old.
20//!
21//! Bumps in the MSRV will _not_ be considered breaking changes. If you need a specific MSRV, make
22//! sure to pin a precise version of RustSAT.
23
24#![warn(clippy::pedantic)]
25#![warn(missing_docs)]
26#![warn(missing_debug_implementations)]
27
28use rustsat::{solvers::SolverState, types::Var};
29use std::{ffi::c_int, fmt};
30use thiserror::Error;
31
32pub mod core;
33pub mod simp;
34
35/// Fatal error returned if the Glucose API returns an invalid value
36#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
37#[error("glucose c-api returned an invalid value: {api_call} -> {value}")]
38pub struct InvalidApiReturn {
39    api_call: &'static str,
40    value: c_int,
41}
42
43/// Error returned if a provided assumption variable was eliminated in preprocessing by the solver
44///
45/// Glucose does not support assumptions over eliminated variables. To prevent this, variables that
46/// will be used as assumptions can be frozen via [`rustsat::solvers::FreezeVar`]
47#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
48#[error("assumption variable {0} has been eliminated by glucose simplification")]
49pub struct AssumpEliminated(Var);
50
51#[derive(Debug, PartialEq, Eq, Default)]
52enum InternalSolverState {
53    #[default]
54    Configuring,
55    Input,
56    Sat,
57    Unsat(bool),
58}
59
60impl InternalSolverState {
61    fn to_external(&self) -> SolverState {
62        match self {
63            InternalSolverState::Configuring => SolverState::Configuring,
64            InternalSolverState::Input => SolverState::Input,
65            InternalSolverState::Sat => SolverState::Sat,
66            InternalSolverState::Unsat(_) => SolverState::Unsat,
67        }
68    }
69}
70
71/// Possible Glucose limits
72#[derive(Debug, Clone, Copy)]
73pub enum Limit {
74    /// No limits
75    None,
76    /// A limit on the number of conflicts
77    Conflicts(i64),
78    /// A limit on the number of propagations
79    Propagations(i64),
80}
81
82impl fmt::Display for Limit {
83    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
84        match self {
85            Limit::None => write!(f, "none"),
86            Limit::Conflicts(val) => write!(f, "conflicts ({val})"),
87            Limit::Propagations(val) => write!(f, "propagations ({val})"),
88        }
89    }
90}
91
92macro_rules! handle_oom {
93    ($val:expr) => {{
94        let val = $val;
95        if val == $crate::ffi::OUT_OF_MEM {
96            return anyhow::Context::context(
97                Err(rustsat::OutOfMemory::ExternalApi),
98                "glucose out of memory",
99            );
100        }
101        val
102    }};
103}
104pub(crate) use handle_oom;
105
106pub(crate) mod ffi {
107    #![allow(non_upper_case_globals)]
108    #![allow(non_camel_case_types)]
109    #![allow(non_snake_case)]
110
111    use std::os::raw::c_void;
112
113    use rustsat::types::Lit;
114
115    include!(concat!(env!("OUT_DIR"), "/bindings.rs"));
116
117    impl From<Lit> for c_Lit {
118        fn from(value: Lit) -> Self {
119            unsafe { std::mem::transmute::<Lit, c_Lit>(value) }
120        }
121    }
122
123    pub extern "C" fn rustsat_glucose_collect_lits(vec: *mut c_void, lit: c_Lit) {
124        let vec = vec.cast::<Vec<Lit>>();
125        unsafe { (*vec).push(std::mem::transmute::<c_Lit, Lit>(lit)) };
126    }
127}
rustsat_glucose/lib.rs

rustsat_glucose/
lib.rs
