#![warn(clippy::pedantic)]
#![warn(missing_docs)]
use rustsat::{
solvers::SolverState,
types::{Lit, Var},
};
use std::{ffi::c_int, fmt};
use thiserror::Error;
pub mod core;
pub mod simp;
#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
#[error("glucose c-api returned an invalid value: {api_call} -> {value}")]
pub struct InvalidApiReturn {
api_call: &'static str,
value: c_int,
}
#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
#[error("assumption variable {0} has been eliminated by glucose simplification")]
pub struct AssumpEliminated(Var);
#[derive(Debug, PartialEq, Eq, Default)]
enum InternalSolverState {
#[default]
Configuring,
Input,
Sat,
Unsat(Vec<Lit>),
}
impl InternalSolverState {
fn to_external(&self) -> SolverState {
match self {
InternalSolverState::Configuring => SolverState::Configuring,
InternalSolverState::Input => SolverState::Input,
InternalSolverState::Sat => SolverState::Sat,
InternalSolverState::Unsat(_) => SolverState::Unsat,
}
}
}
#[derive(Debug, Clone, Copy)]
pub enum Limit {
None,
Conflicts(i64),
Propagations(i64),
}
impl fmt::Display for Limit {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
Limit::None => write!(f, "none"),
Limit::Conflicts(val) => write!(f, "conflicts ({val})"),
Limit::Propagations(val) => write!(f, "propagations ({val})"),
}
}
}
macro_rules! handle_oom {
($val:expr) => {{
let val = $val;
if val == $crate::ffi::OUT_OF_MEM {
return anyhow::Context::context(
Err(rustsat::OutOfMemory::ExternalApi),
"glucose out of memory",
);
}
val
}};
}
pub(crate) use handle_oom;
pub(crate) mod ffi {
#![allow(non_upper_case_globals)]
#![allow(non_camel_case_types)]
#![allow(non_snake_case)]
use std::os::raw::{c_int, c_void};
use rustsat::types::Lit;
include!(concat!(env!("OUT_DIR"), "/bindings.rs"));
pub extern "C" fn rustsat_glucose_collect_lits(vec: *mut c_void, lit: c_int) {
let vec = vec.cast::<Vec<Lit>>();
let lit = Lit::from_ipasir(lit).expect("got invalid IPASIR lit from Glucose");
unsafe { (*vec).push(lit) };
}
}