Skip to content

Commit

Permalink
chore(assumptions): simplify return type of incremental_push_all
Browse files Browse the repository at this point in the history
The ordering of the `Vec<bool>` result could be problematic if the input `impl IntoIterator<Item = Lit>` is a collection that, if cloned, wouldn't necessarily be iterated in the same order (like a `HashMap`). This could cause confusion or bugs. If one wants the boolean result of making each assumption (true if it was new, false if already held), one should use `incremental_push`, not `incremental_push_all`.
  • Loading branch information
nrealus committed Jan 10, 2025
1 parent ce0e9e5 commit 6f8c783
Showing 1 changed file with 3 additions and 4 deletions.
7 changes: 3 additions & 4 deletions solver/src/solver/solver_impl.rs
Original file line number Diff line number Diff line change
Expand Up @@ -597,15 +597,14 @@ impl<Lbl: Label> Solver<Lbl> {
pub fn incremental_push_all(
&mut self,
assumptions: impl IntoIterator<Item = Lit>,
) -> Result<Vec<bool>, (usize, UnsatCore)> {
let mut res_ok = Vec::new();
) -> Result<(), (usize, UnsatCore)> {
for (i, lit) in assumptions.into_iter().enumerate() {
match self.assume_and_propagate(lit) {
Ok(b) => res_ok.push(b),
Ok(_) => (),
Err(unsat_core) => return Err((i, unsat_core)),
}
}
Ok(res_ok)
Ok(())
}

/// Incremental solving: Removes the last assumption that was pushed and
Expand Down

0 comments on commit 6f8c783

Please sign in to comment.