Skip to content

Commit

Permalink
Rectify invalid assumption in the IPASIR-UP's check model callback
Browse files Browse the repository at this point in the history
  • Loading branch information
Dekker1 committed Apr 3, 2024
1 parent 3486ff9 commit 8a6d0a1
Showing 1 changed file with 5 additions and 11 deletions.
16 changes: 5 additions & 11 deletions crates/pindakaas/src/solver/libloading.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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::<i32>::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<Var, bool> = sol
.into_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")]
Expand Down

0 comments on commit 8a6d0a1

Please sign in to comment.