15026055704

Committed 14 May 2025 09:46AM UTC coverage: 57.602% (-0.06%) from 57.664%

Build # 15026055704

Build Type

push

github

Committed by

chrjabs

Commit Message

feat(batsat): track state and return state errors

Run Details

10 of 42 new or added lines in 1 file covered. (23.81%)

40 existing lines in 1 file now uncovered.

13181 of 22883 relevant lines covered (57.6%)

42469.33 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

47.67

/batsat/src/lib.rs

//! # rustsat-batsat - Interface to the BatSat SAT Solver for RustSAT
//!
//! Interface to the [BatSat](https://github.com/c-cube/batsat) incremental SAT-Solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library.
//!
//! BatSat is fully implemented in Rust which has advantages in restricted compilation scenarios like WebAssembly.
//!
//! # BatSat Version
//!
//! The version of BatSat in this crate is Version 0.6.0.
//!
//! ## Minimum Supported Rust Version (MSRV)
//!
//! Currently, the MSRV is 1.76.0, the plan is to always support an MSRV that is at least a year
//! old.
//!
//! Bumps in the MSRV will _not_ be considered breaking changes. If you need a specific MSRV, make
//! sure to pin a precise version of RustSAT.

// NOTE: For some reason, batsat flipped the memory representation of the sign bit in the literal
// representation compared to Minisat and therefore RustSAT
// https://github.com/c-cube/batsat/commit/8563ae6e3a59478a0d414fe647d99ad9b989841f
// For this reason we cannot transmute RustSAT literals to batsat literals and we have to recreate
// the literals through batsat's API

#![warn(clippy::pedantic)]
#![warn(missing_docs)]
#![warn(missing_debug_implementations)]

use std::time::Duration;

use batsat::{intmap::AsIndex, lbool, Callbacks, SolverInterface};
use cpu_time::ProcessTime;
use rustsat::{
    solvers::{
        Solve, SolveIncremental, SolveStats, SolverResult, SolverState, SolverStats, StateError,
    },
    types::{Cl, Clause, Lit, TernaryVal, Var},
};

/// RustSAT wrapper for [`batsat::BasicSolver`]
pub type BasicSolver = Solver<batsat::BasicCallbacks>;

#[derive(Debug, PartialEq, Eq, Default)]
enum InternalSolverState {
    #[default]
    Input,
    Sat,
    Unsat(bool),
}

impl InternalSolverState {
    fn to_external(&self) -> SolverState {
        match self {
            InternalSolverState::Input => SolverState::Input,
            InternalSolverState::Sat => SolverState::Sat,
            InternalSolverState::Unsat(_) => SolverState::Unsat,
        }
    }
}

/// RustSAT wrapper for a [`batsat::Solver`] Solver from BatSat
#[derive(Default)]
pub struct Solver<Cb: Callbacks> {
    internal: batsat::Solver<Cb>,
    state: InternalSolverState,
    n_sat: usize,
    n_unsat: usize,
    n_terminated: usize,
    avg_clause_len: f32,
    cpu_time: Duration,
}

impl<Cb: Callbacks> std::fmt::Debug for Solver<Cb> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        f.debug_struct("Solver")
            .field("internal", &"omitted")
            .field("state", &self.state)
            .field("n_sat", &self.n_sat)
            .field("n_unsat", &self.n_unsat)
            .field("n_terminated", &self.n_terminated)
            .field("avg_clause_len", &self.avg_clause_len)
            .field("cpu_time", &self.cpu_time)
            .finish()
    }
}

impl<Cb: Callbacks> Solver<Cb> {
    /// Gets a reference to the internal [`BasicSolver`]
    #[must_use]
    pub fn batsat_ref(&self) -> &batsat::Solver<Cb> {
        &self.internal
    }

    /// Gets a mutable reference to the internal [`BasicSolver`]
    #[must_use]
    pub fn batsat_mut(&mut self) -> &mut batsat::Solver<Cb> {
        &mut self.internal
    }

    #[allow(clippy::cast_precision_loss)]
    #[inline]
    fn update_avg_clause_len(&mut self, clause: &Cl) {
        self.avg_clause_len = (self.avg_clause_len * ((self.n_clauses()) as f32)
            + clause.len() as f32)
            / (self.n_clauses() + 1) as f32;
    }

    fn solve_track_stats(&mut self, assumps: &[Lit]) -> SolverResult {
        let assumps = assumps
            .iter()
            .map(|l| batsat::Lit::new(self.internal.var_of_int(l.vidx32()), l.is_pos()))
            .collect::<Vec<_>>();

        let start = ProcessTime::now();
        let ret = match self.internal.solve_limited(&assumps) {
            x if x == lbool::TRUE => {
                self.n_sat += 1;
                self.state = InternalSolverState::Sat;
                SolverResult::Sat
            }
            x if x == lbool::FALSE => {
                self.n_unsat += 1;
                self.state = InternalSolverState::Unsat(!assumps.is_empty());
                SolverResult::Unsat
            }
            x if x == lbool::UNDEF => {
                self.n_terminated += 1;
                self.state = InternalSolverState::Input;
                SolverResult::Interrupted
            }
            _ => unreachable!(),
        };
        self.cpu_time += start.elapsed();
        ret
    }
}

impl<Cb: Callbacks> Extend<Clause> for Solver<Cb> {
    fn extend<T: IntoIterator<Item = Clause>>(&mut self, iter: T) {
        iter.into_iter()
            .for_each(|cl| self.add_clause(cl).expect("Error adding clause in extend"));
    }
}

impl<'a, C, Cb> Extend<&'a C> for Solver<Cb>
where
    C: AsRef<Cl> + ?Sized,
    Cb: Callbacks,
{
    fn extend<T: IntoIterator<Item = &'a C>>(&mut self, iter: T) {
        iter.into_iter().for_each(|cl| {
            self.add_clause_ref(cl)
                .expect("Error adding clause in extend");
        });
    }
}

impl<Cb: Callbacks> Solve for Solver<Cb> {
    fn signature(&self) -> &'static str {
        "BatSat 0.6.0"
    }

    fn solve(&mut self) -> anyhow::Result<SolverResult> {
        // If already solved, return state
        if let InternalSolverState::Sat = self.state {
            return Ok(SolverResult::Sat);
        }
        if let InternalSolverState::Unsat(under_assumps) = &self.state {
            if !under_assumps {
                return Ok(SolverResult::Unsat);
            }
        }
        Ok(self.solve_track_stats(&[]))
    }

    fn lit_val(&self, lit: Lit) -> anyhow::Result<TernaryVal> {
        if self.state != InternalSolverState::Sat {
            return Err(StateError {
                required_state: SolverState::Sat,
                actual_state: self.state.to_external(),
            }
            .into());
        }

        let lit = batsat::Lit::new(batsat::Var::from_index(lit.vidx()), lit.is_pos());

        match self.internal.value_lit(lit) {
            x if x == lbool::TRUE => Ok(TernaryVal::True),
            x if x == lbool::FALSE => Ok(TernaryVal::False),
            x if x == lbool::UNDEF => Ok(TernaryVal::DontCare),
            _ => unreachable!(),
        }
    }

    fn add_clause_ref<C>(&mut self, clause: &C) -> anyhow::Result<()>
    where
        C: AsRef<Cl> + ?Sized,
    {
        let clause = clause.as_ref();
        self.update_avg_clause_len(clause);

        let mut clause: Vec<_> = clause
            .iter()
            .map(|l| batsat::Lit::new(self.internal.var_of_int(l.vidx32()), l.is_pos()))
            .collect();

        self.internal.add_clause_reuse(&mut clause);

        Ok(())
    }

    fn reserve(&mut self, max_var: Var) -> anyhow::Result<()> {
        while self.internal.num_vars() <= max_var.idx32() {
            self.internal.new_var_default();
        }
        Ok(())
    }
}

impl<Cb: Callbacks> SolveIncremental for Solver<Cb> {
    fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result<SolverResult> {
        Ok(self.solve_track_stats(assumps))
    }

    fn core(&mut self) -> anyhow::Result<Vec<Lit>> {
        match &self.state {
            InternalSolverState::Unsat(under_assumps) => {
                if *under_assumps {
                    Ok(self
                        .internal
                        .unsat_core()
                        .iter()
                        .map(|l| Lit::new(l.var().idx(), !l.sign()))
                        .collect::<Vec<_>>())
                } else {
                    Ok(vec![])
                }
            }
            other => Err(StateError {
                required_state: SolverState::Unsat,
                actual_state: other.to_external(),
            }
            .into()),
        }
    }
}

impl<Cb: Callbacks> SolveStats for Solver<Cb> {
    fn stats(&self) -> SolverStats {
        SolverStats {
            n_sat: self.n_sat,
            n_unsat: self.n_unsat,
            n_terminated: self.n_terminated,
            n_clauses: self.n_clauses(),
            max_var: self.max_var(),
            avg_clause_len: self.avg_clause_len,
            cpu_solve_time: self.cpu_time,
        }
    }

    fn n_sat_solves(&self) -> usize {
        self.n_sat
    }

    fn n_unsat_solves(&self) -> usize {
        self.n_unsat
    }

    fn n_terminated(&self) -> usize {
        self.n_terminated
    }

    fn n_clauses(&self) -> usize {
        usize::try_from(self.internal.num_clauses()).expect("more than `usize::MAX` clauses")
    }

    fn max_var(&self) -> Option<Var> {
        let num = self.internal.num_vars();
        if num > 0 {
            Some(Var::new(num - 1))
        } else {
            None
        }
    }

    fn avg_clause_len(&self) -> f32 {
        self.avg_clause_len
    }

    fn cpu_solve_time(&self) -> Duration {
        self.cpu_time
    }
}

#[cfg(test)]
mod test {
    rustsat_solvertests::basic_unittests!(super::BasicSolver, false);
}

1	//! # rustsat-batsat - Interface to the BatSat SAT Solver for RustSAT
2	//!
3	//! Interface to the [BatSat](https://github.com/c-cube/batsat) incremental SAT-Solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library.
4	//!
5	//! BatSat is fully implemented in Rust which has advantages in restricted compilation scenarios like WebAssembly.
6	//!
7	//! # BatSat Version
8	//!
9	//! The version of BatSat in this crate is Version 0.6.0.
10	//!
11	//! ## Minimum Supported Rust Version (MSRV)
12	//!
13	//! Currently, the MSRV is 1.76.0, the plan is to always support an MSRV that is at least a year
14	//! old.
15	//!
16	//! Bumps in the MSRV will _not_ be considered breaking changes. If you need a specific MSRV, make
17	//! sure to pin a precise version of RustSAT.
18
19	// NOTE: For some reason, batsat flipped the memory representation of the sign bit in the literal
20	// representation compared to Minisat and therefore RustSAT
21	// https://github.com/c-cube/batsat/commit/8563ae6e3a59478a0d414fe647d99ad9b989841f
22	// For this reason we cannot transmute RustSAT literals to batsat literals and we have to recreate
23	// the literals through batsat's API
24
25	#![warn(clippy::pedantic)]
26	#![warn(missing_docs)]
27	#![warn(missing_debug_implementations)]
28
29	use std::time::Duration;
30
31	use batsat::{intmap::AsIndex, lbool, Callbacks, SolverInterface};
32	use cpu_time::ProcessTime;
33	use rustsat::{
34	solvers::{
35	Solve, SolveIncremental, SolveStats, SolverResult, SolverState, SolverStats, StateError,
36	},
37	types::{Cl, Clause, Lit, TernaryVal, Var},
38	};
39
40	/// RustSAT wrapper for [`batsat::BasicSolver`]
41	pub type BasicSolver = Solver<batsat::BasicCallbacks>;
42
43	#[derive(Debug, PartialEq, Eq, Default)]
44	enum InternalSolverState {
45	#[default]
46	Input,
47	Sat,
48	Unsat(bool),
49	}
50
51	impl InternalSolverState {
NEW 52	fn to_external(&self) -> SolverState {	×
NEW 53	match self {	×
NEW 54	InternalSolverState::Input => SolverState::Input,	×
NEW 55	InternalSolverState::Sat => SolverState::Sat,	×
NEW 56	InternalSolverState::Unsat(_) => SolverState::Unsat,	×
57	}
NEW 58	}	×
59	}
60
61	/// RustSAT wrapper for a [`batsat::Solver`] Solver from BatSat
62	#[derive(Default)]
63	pub struct Solver<Cb: Callbacks> {
64	internal: batsat::Solver<Cb>,
65	state: InternalSolverState,
66	n_sat: usize,
67	n_unsat: usize,
68	n_terminated: usize,
69	avg_clause_len: f32,
70	cpu_time: Duration,
71	}
72
73	impl<Cb: Callbacks> std::fmt::Debug for Solver<Cb> {
74	fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {	×
75	f.debug_struct("Solver")	×
76	.field("internal", &"omitted")	×
NEW 77	.field("state", &self.state)	×
UNCOV 78	.field("n_sat", &self.n_sat)	×
UNCOV 79	.field("n_unsat", &self.n_unsat)	×
UNCOV 80	.field("n_terminated", &self.n_terminated)	×
UNCOV 81	.field("avg_clause_len", &self.avg_clause_len)	×
UNCOV 82	.field("cpu_time", &self.cpu_time)	×
UNCOV 83	.finish()	×
84	}	×
85	}
86
87	impl<Cb: Callbacks> Solver<Cb> {
88	/// Gets a reference to the internal [`BasicSolver`]
89	#[must_use]
90	pub fn batsat_ref(&self) -> &batsat::Solver<Cb> {	×
91	&self.internal	×
92	}	×
93
94	/// Gets a mutable reference to the internal [`BasicSolver`]
95	#[must_use]
UNCOV 96	pub fn batsat_mut(&mut self) -> &mut batsat::Solver<Cb> {	×
UNCOV 97	&mut self.internal	×
UNCOV 98	}	×
99
100	#[allow(clippy::cast_precision_loss)]
101	#[inline]
102	fn update_avg_clause_len(&mut self, clause: &Cl) {	149,599✔
103	self.avg_clause_len = (self.avg_clause_len * ((self.n_clauses()) as f32)	149,599✔
104	+ clause.len() as f32)	149,599✔
105	/ (self.n_clauses() + 1) as f32;	149,599✔
106	}	149,599✔
107
108	fn solve_track_stats(&mut self, assumps: &[Lit]) -> SolverResult {	23✔
109	let assumps = assumps	23✔
110	.iter()	23✔
111	.map(\|l\| batsat::Lit::new(self.internal.var_of_int(l.vidx32()), l.is_pos()))	66✔
112	.collect::<Vec<_>>();	23✔
113		23✔
114	let start = ProcessTime::now();	23✔
115	let ret = match self.internal.solve_limited(&assumps) {	23✔
116	x if x == lbool::TRUE => {	23✔
117	self.n_sat += 1;	8✔
118	self.state = InternalSolverState::Sat;	8✔
119	SolverResult::Sat	8✔
120	}
121	x if x == lbool::FALSE => {	15✔
122	self.n_unsat += 1;	15✔
123	self.state = InternalSolverState::Unsat(!assumps.is_empty());	15✔
124	SolverResult::Unsat	15✔
125	}
UNCOV 126	x if x == lbool::UNDEF => {	×
UNCOV 127	self.n_terminated += 1;	×
NEW 128	self.state = InternalSolverState::Input;	×
UNCOV 129	SolverResult::Interrupted	×
130	}
UNCOV 131	_ => unreachable!(),	×
132	};
133	self.cpu_time += start.elapsed();	23✔
134	ret	23✔
135	}	23✔
136	}
137
138	impl<Cb: Callbacks> Extend<Clause> for Solver<Cb> {
UNCOV 139	fn extend<T: IntoIterator<Item = Clause>>(&mut self, iter: T) {	×
UNCOV 140	iter.into_iter()	×
UNCOV 141	.for_each(\|cl\| self.add_clause(cl).expect("Error adding clause in extend"));	×
UNCOV 142	}	×
143	}
144
145	impl<'a, C, Cb> Extend<&'a C> for Solver<Cb>
146	where
147	C: AsRef<Cl> + ?Sized,
148	Cb: Callbacks,
149	{
UNCOV 150	fn extend<T: IntoIterator<Item = &'a C>>(&mut self, iter: T) {	×
UNCOV 151	iter.into_iter().for_each(\|cl\| {	×
UNCOV 152	self.add_clause_ref(cl)	×
153	.expect("Error adding clause in extend");	×
154	});	×
155	}	×
156	}
157
158	impl<Cb: Callbacks> Solve for Solver<Cb> {
UNCOV 159	fn signature(&self) -> &'static str {	×
UNCOV 160	"BatSat 0.6.0"	×
UNCOV 161	}	×
162
163	fn solve(&mut self) -> anyhow::Result<SolverResult> {	6✔
164	// If already solved, return state	6✔
165	if let InternalSolverState::Sat = self.state {	6✔
NEW 166	return Ok(SolverResult::Sat);	×
167	}	6✔
168	if let InternalSolverState::Unsat(under_assumps) = &self.state {	6✔
NEW 169	if !under_assumps {	×
NEW 170	return Ok(SolverResult::Unsat);	×
NEW 171	}	×
172	}	6✔
173	Ok(self.solve_track_stats(&[]))	6✔
174	}	6✔
175
176	fn lit_val(&self, lit: Lit) -> anyhow::Result<TernaryVal> {	44,805✔
177	if self.state != InternalSolverState::Sat {	44,805✔
NEW 178	return Err(StateError {	×
NEW 179	required_state: SolverState::Sat,	×
NEW 180	actual_state: self.state.to_external(),	×
NEW 181	}	×
NEW 182	.into());	×
183	}	44,805✔
184		44,805✔
185	let lit = batsat::Lit::new(batsat::Var::from_index(lit.vidx()), lit.is_pos());	44,805✔
186		44,805✔
187	match self.internal.value_lit(lit) {	44,805✔
188	x if x == lbool::TRUE => Ok(TernaryVal::True),	44,805✔
189	x if x == lbool::FALSE => Ok(TernaryVal::False),	38,409✔
UNCOV 190	x if x == lbool::UNDEF => Ok(TernaryVal::DontCare),	×
UNCOV 191	_ => unreachable!(),	×
192	}
193	}	44,805✔
194
195	fn add_clause_ref<C>(&mut self, clause: &C) -> anyhow::Result<()>	149,599✔
196	where	149,599✔
197	C: AsRef<Cl> + ?Sized,	149,599✔
198	{	149,599✔
199	let clause = clause.as_ref();	149,599✔
200	self.update_avg_clause_len(clause);	149,599✔
201		149,599✔
202	let mut clause: Vec<_> = clause	149,599✔
203	.iter()	149,599✔
204	.map(\|l\| batsat::Lit::new(self.internal.var_of_int(l.vidx32()), l.is_pos()))	389,450✔
205	.collect();	149,599✔
206		149,599✔
207	self.internal.add_clause_reuse(&mut clause);	149,599✔
208		149,599✔
209	Ok(())	149,599✔
210	}	149,599✔
211
212	fn reserve(&mut self, max_var: Var) -> anyhow::Result<()> {	×
213	while self.internal.num_vars() <= max_var.idx32() {	×
214	self.internal.new_var_default();	×
215	}	×
216	Ok(())	×
217	}	×
218	}
219
220	impl<Cb: Callbacks> SolveIncremental for Solver<Cb> {
221	fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result<SolverResult> {	17✔
222	Ok(self.solve_track_stats(assumps))	17✔
223	}	17✔
224
225	fn core(&mut self) -> anyhow::Result<Vec<Lit>> {	×
NEW 226	match &self.state {	×
NEW 227	InternalSolverState::Unsat(under_assumps) => {	×
NEW 228	if *under_assumps {	×
NEW 229	Ok(self	×
NEW 230	.internal	×
NEW 231	.unsat_core()	×
NEW 232	.iter()	×
NEW 233	.map(\|l\| Lit::new(l.var().idx(), !l.sign()))	×
NEW 234	.collect::<Vec<_>>())	×
235	} else {
NEW 236	Ok(vec![])	×
237	}
238	}
NEW 239	other => Err(StateError {	×
NEW 240	required_state: SolverState::Unsat,	×
NEW 241	actual_state: other.to_external(),	×
NEW 242	}	×
NEW 243	.into()),	×
244	}
245	}	×
246	}
247
248	impl<Cb: Callbacks> SolveStats for Solver<Cb> {
UNCOV 249	fn stats(&self) -> SolverStats {	×
UNCOV 250	SolverStats {	×
UNCOV 251	n_sat: self.n_sat,	×
UNCOV 252	n_unsat: self.n_unsat,	×
UNCOV 253	n_terminated: self.n_terminated,	×
UNCOV 254	n_clauses: self.n_clauses(),	×
UNCOV 255	max_var: self.max_var(),	×
UNCOV 256	avg_clause_len: self.avg_clause_len,	×
UNCOV 257	cpu_solve_time: self.cpu_time,	×
UNCOV 258	}	×
UNCOV 259	}	×
260
261	fn n_sat_solves(&self) -> usize {	4✔
262	self.n_sat	4✔
263	}	4✔
264
265	fn n_unsat_solves(&self) -> usize {	4✔
266	self.n_unsat	4✔
267	}	4✔
268
269	fn n_terminated(&self) -> usize {	4✔
270	self.n_terminated	4✔
271	}	4✔
272
273	fn n_clauses(&self) -> usize {	299,199✔
274	usize::try_from(self.internal.num_clauses()).expect("more than `usize::MAX` clauses")	299,199✔
275	}	299,199✔
276
277	fn max_var(&self) -> Option<Var> {	2✔
278	let num = self.internal.num_vars();	2✔
279	if num > 0 {	2✔
280	Some(Var::new(num - 1))	2✔
281	} else {
UNCOV 282	None	×
283	}
284	}	2✔
285
286	fn avg_clause_len(&self) -> f32 {	1✔
287	self.avg_clause_len	1✔
288	}	1✔
289
UNCOV 290	fn cpu_solve_time(&self) -> Duration {	×
UNCOV 291	self.cpu_time	×
UNCOV 292	}	×
293	}
294
295	#[cfg(test)]
296	mod test {
297	rustsat_solvertests::basic_unittests!(super::BasicSolver, false);	2✔
298	}

chrjabs / rustsat / 15026055704

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous