Update pindakaas library

huub-solver · Oct 8, 2024 · eda6718 · eda6718
1 parent e4e26fb
commit eda6718
Show file tree

Hide file tree

Showing 13 changed files with 102 additions and 213 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/crates/huub/src/model.rs b/crates/huub/src/model.rs
@@ -80,7 +80,7 @@ impl Model {
 		let mut map = VariableMap::default();
 
 		// TODO: run SAT simplification
-		let mut slv: Solver<Sat> = self.cnf.clone().into();
+		let mut slv = Solver::<Sat>::from(&self.cnf);
 		let any_slv: &mut dyn Any = &mut slv.oracle;
 		if let Some(r) = any_slv.downcast_mut::<Cadical>() {
 			r.set_option("restart", config.restart() as i32);

diff --git a/crates/huub/src/propagator/all_different_int.rs b/crates/huub/src/propagator/all_different_int.rs
@@ -97,7 +97,7 @@ mod tests {
 	#[test]
 	#[traced_test]
 	fn test_all_different_value_sat() {
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let a = IntVar::new_in(
 			&mut slv,
 			RangeList::from_iter([1..=4]),
@@ -125,7 +125,7 @@ mod tests {
 	#[test]
 	#[traced_test]
 	fn test_all_different_value_unsat() {
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let a = IntVar::new_in(
 			&mut slv,
 			RangeList::from_iter([1..=2]),
@@ -151,7 +151,7 @@ mod tests {
 	}
 
 	fn test_sudoku(grid: &[&str], expected: SolveResult) {
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let mut all_vars = vec![];
 		// create variables and add all different propagator for each row
 		grid.iter().for_each(|row| {

diff --git a/crates/huub/src/propagator/array_var_int_element.rs b/crates/huub/src/propagator/array_var_int_element.rs
@@ -252,7 +252,7 @@ mod tests {
 	#[test]
 	#[traced_test]
 	fn test_element_bounds_sat() {
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let a = IntVar::new_in(
 			&mut slv,
 			RangeList::from_iter([3..=4]),
@@ -325,7 +325,7 @@ mod tests {
 	#[test]
 	#[traced_test]
 	fn test_element_holes() {
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let a = IntVar::new_in(
 			&mut slv,
 			RangeList::from_iter([1..=3]),

diff --git a/crates/huub/src/propagator/disjunctive_strict.rs b/crates/huub/src/propagator/disjunctive_strict.rs
@@ -582,7 +582,7 @@ mod tests {
 	#[test]
 	#[traced_test]
 	fn test_disjunctive_sat() {
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let a = IntVar::new_in(
 			&mut slv,
 			RangeList::from_iter([0..=4]),

diff --git a/crates/huub/src/propagator/int_abs.rs b/crates/huub/src/propagator/int_abs.rs
@@ -123,7 +123,7 @@ mod tests {
 	#[test]
 	#[traced_test]
 	fn test_int_abs_sat() {
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let a = IntVar::new_in(
 			&mut slv,
 			(-3..=3).into(),

diff --git a/crates/huub/src/propagator/int_div.rs b/crates/huub/src/propagator/int_div.rs
@@ -265,7 +265,7 @@ mod tests {
 	#[test]
 	#[traced_test]
 	fn test_int_div_sat() {
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let a = IntVar::new_in(
 			&mut slv,
 			(-7..=7).into(),

diff --git a/crates/huub/src/propagator/int_lin_le.rs b/crates/huub/src/propagator/int_lin_le.rs
@@ -197,7 +197,7 @@ mod tests {
 	#[test]
 	#[traced_test]
 	fn test_linear_le_sat() {
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let a = IntVar::new_in(
 			&mut slv,
 			RangeList::from_iter([1..=2]),
@@ -249,7 +249,7 @@ mod tests {
 	#[test]
 	#[traced_test]
 	fn test_linear_ge_sat() {
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let a = IntVar::new_in(
 			&mut slv,
 			RangeList::from_iter([1..=2]),

diff --git a/crates/huub/src/propagator/int_lin_ne.rs b/crates/huub/src/propagator/int_lin_ne.rs
@@ -195,7 +195,7 @@ mod tests {
 	#[test]
 	#[traced_test]
 	fn test_linear_ne_sat() {
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let a = IntVar::new_in(
 			&mut slv,
 			RangeList::from_iter([1..=2]),

diff --git a/crates/huub/src/propagator/int_pow.rs b/crates/huub/src/propagator/int_pow.rs
@@ -327,7 +327,7 @@ mod tests {
 	#[test]
 	#[traced_test]
 	fn test_int_pow_sat() {
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let a = IntVar::new_in(
 			&mut slv,
 			(-2..=3).into(),

diff --git a/crates/huub/src/propagator/int_times.rs b/crates/huub/src/propagator/int_times.rs
@@ -155,7 +155,7 @@ mod tests {
 	#[test]
 	#[traced_test]
 	fn test_int_times_sat() {
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let a = IntVar::new_in(
 			&mut slv,
 			(-2..=1).into(),

diff --git a/crates/huub/src/solver.rs b/crates/huub/src/solver.rs
@@ -72,7 +72,12 @@ pub struct InitStatistics {
 }
 
 pub trait SatSolver:
-	PropagatingSolver + TermCallback + LearnCallback + SolveAssuming + NextVarRange + From<Cnf>
+	PropagatingSolver
+	+ TermCallback
+	+ LearnCallback
+	+ SolveAssuming
+	+ NextVarRange
+	+ for<'a> From<&'a Cnf>
 where
 	<Self as SolverTrait>::ValueFn: PropagatorAccess,
 {
@@ -463,8 +468,12 @@ where
 
 impl<Slv> SatSolver for Slv
 where
-	Slv:
-		PropagatingSolver + TermCallback + LearnCallback + SolveAssuming + NextVarRange + From<Cnf>,
+	Slv: PropagatingSolver
+		+ TermCallback
+		+ LearnCallback
+		+ SolveAssuming
+		+ NextVarRange
+		+ for<'a> From<&'a Cnf>,
 	<Slv as SolverTrait>::ValueFn: PropagatorAccess,
 {
 }
@@ -482,12 +491,12 @@ where
 	}
 }
 
-impl<Sol, Sat> From<Cnf> for Solver<Sat>
+impl<Sol, Sat> From<&Cnf> for Solver<Sat>
 where
 	Sol: PropagatorAccess + SatValuation,
 	Sat: SatSolver + SolverTrait<ValueFn = Sol>,
 {
-	fn from(value: Cnf) -> Self {
+	fn from(value: &Cnf) -> Self {
 		let mut core: Sat = value.into();
 		core.set_external_propagator(Some(Engine::default()));
 		core.set_learn_callback(Some(trace_learned_clause));

diff --git a/crates/huub/src/solver/engine/int_var.rs b/crates/huub/src/solver/engine/int_var.rs
@@ -1203,7 +1203,7 @@ mod tests {
 				unreachable!()
 			}
 		};
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let a = IntVar::new_in(
 			&mut slv,
 			RangeList::from(1..=4),
@@ -1233,7 +1233,7 @@ mod tests {
 		let lit = a.get_bool_lit(LitMeaning::Eq(4)).unwrap();
 		assert_eq!(get_lit(lit), 3);
 
-		let mut slv: Solver<Cadical> = Cnf::default().into();
+		let mut slv = Solver::<Cadical>::from(&Cnf::default());
 		let a = IntVar::new_in(
 			&mut slv,
 			RangeList::from_iter([1..=3, 8..=10]),