From 6f8c7836783aa4c8be32685e9b0dff5a8a505b2b Mon Sep 17 00:00:00 2001 From: Nika Beriachvili Date: Fri, 10 Jan 2025 15:32:23 +0100 Subject: [PATCH] chore(assumptions): simplify return type of `incremental_push_all` The ordering of the `Vec` result could be problematic if the input `impl IntoIterator` 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`. --- solver/src/solver/solver_impl.rs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index 75c9b7bc..bba2ae2c 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -597,15 +597,14 @@ impl Solver { pub fn incremental_push_all( &mut self, assumptions: impl IntoIterator, - ) -> Result, (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