diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index b84574b51..30055537f 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -254,9 +254,7 @@ impl VarFactory { /// Return the next [`size`] variables that can be stored as an inclusive range. pub fn new_var_range(&mut self, size: usize) -> Option { - let Some(start) = self.next_var else { - return None; - }; + let start = self.next_var?; match size { 0 => Some(VarRange::new( Var(NonZeroI32::new(2).unwrap()), diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index d6ae4ba7a..1a471c00e 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -376,17 +376,11 @@ pub(crate) unsafe extern "C" fn ipasir_check_model_cb( ) -> bool { let prop = &mut *(state as *mut IpasirPropStore); let sol = std::slice::from_raw_parts(model, len); - let value = |l: Lit| { - let abs: Lit = l.var().into(); - let v = Into::::into(abs) as usize; - if v <= sol.len() { - // TODO: is this correct here? - debug_assert_eq!(sol[v - 1].abs(), l.var().into()); - Some(sol[v - 1] == l.into()) - } else { - None - } - }; + let sol: std::collections::HashMap = sol + .iter() + .map(|&i| (Var(NonZeroI32::new(i.abs()).unwrap()), i >= 0)) + .collect(); + let value = |l: Lit| sol.get(&l.var()).copied(); prop.prop.check_model(&value) } #[cfg(feature = "ipasir-up")]